%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU235+3 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:50 PM UTC 2026
% Result : Theorem 2.44s 0.86s
% Output : CNFRefutation 2.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 20
% Syntax : Number of formulae : 157 ( 20 unt; 0 def)
% Number of atoms : 521 ( 76 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 648 ( 284 ~; 276 |; 63 &)
% ( 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 : 230 ( 218 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A] :
( ordinal(A)
=> ( epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] :
( empty(A)
=> ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B] :
( ( ordinal(B)
& ordinal(A) )
=> ( ordinal_subset(B,A)
| ordinal_subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A] :
( epsilon_transitive(A)
<=> ! [B] :
( in(B,A)
=> subset(B,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A,B] :
( ( ordinal(B)
& ordinal(A) )
=> ( ordinal_subset(A,B)
<=> subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A,B] :
( ordinal(B)
=> ( in(A,B)
=> ordinal(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
( ordinal(A)
=> ! [B] :
( ordinal(B)
=> ~ ( ~ in(B,A)
& A != B
& ~ in(A,B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,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)],[f35]) ).
fof(f37,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [A,B] :
~ ( ! [C] :
~ ( ! [D] :
~ ( in(D,C)
& in(D,B) )
& in(C,B) )
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [A,B] :
~ ( empty(B)
& A != B
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,plain,
! [A] :
( ( epsilon_connected(A)
& epsilon_transitive(A) )
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f49,plain,
! [X0] :
( epsilon_transitive(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f59,plain,
! [A] :
( ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f62,plain,
! [X0] :
( ordinal(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f63,plain,
! [A,B] :
( ordinal_subset(B,A)
| ordinal_subset(A,B)
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f64,plain,
! [X0,X1] :
( ordinal_subset(X1,X0)
| ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [A] :
( epsilon_transitive(A)
<=> ! [B] :
( subset(B,A)
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f66,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)],[f65]) ).
fof(f67,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)],[f66]) ).
fof(f68,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))],[f67]) ).
fof(f69,plain,
! [X0,X1] :
( subset(X1,X0)
| ~ in(X1,X0)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f72,plain,
! [A] : element(sK1_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f10]) ).
fof(f73,plain,
! [X0] : element(sK1_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f74,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f85,plain,
ordinal(empty_set),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f95,plain,
( relation(sK4_skl)
& empty(sK4_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f17]) ).
fof(f96,plain,
empty(sK4_skl),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f137,plain,
! [A,B] :
( ( ordinal_subset(A,B)
<=> subset(A,B) )
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f138,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)],[f137]) ).
fof(f139,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f140,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f148,plain,
! [A,B] :
( ordinal(A)
| ~ in(A,B)
| ~ ordinal(B) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f149,plain,
! [B] :
( ! [A] :
( ordinal(A)
| ~ in(A,B) )
| ~ ordinal(B) ),
inference(miniscoping,[status(thm)],[f148]) ).
fof(f150,plain,
! [X0,X1] :
( ordinal(X1)
| ~ in(X1,X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f151,plain,
! [A] :
( ! [B] :
( in(B,A)
| A = B
| in(A,B)
| ~ ordinal(B) )
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f152,plain,
! [X0,X1] :
( in(X1,X0)
| X0 = X1
| in(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f154,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f155,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)],[f36]) ).
fof(f156,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)],[f155]) ).
fof(f157,plain,
( ! [C] :
( ( ~ ordinal_subset(C,sK17_skl(C))
& in(sK17_skl(C),sK16_skl)
& ordinal(sK17_skl(C)) )
| ~ in(C,sK16_skl)
| ~ ordinal(C) )
& sK16_skl != empty_set
& subset(sK16_skl,sK15_skl)
& ordinal(sK15_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(B,sK15_skl),skolemize(A,sK16_skl),skolemize(D,sK17_skl(C))],[f156]) ).
fof(f158,plain,
ordinal(sK15_skl),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f159,plain,
subset(sK16_skl,sK15_skl),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f160,plain,
sK16_skl != empty_set,
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f161,plain,
! [X0] :
( ordinal(sK17_skl(X0))
| ~ in(X0,sK16_skl)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f162,plain,
! [X0] :
( in(sK17_skl(X0),sK16_skl)
| ~ in(X0,sK16_skl)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f163,plain,
! [X0] :
( ~ ordinal_subset(X0,sK17_skl(X0))
| ~ in(X0,sK16_skl)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f164,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(NNF_transformation,[status(thm)],[f37]) ).
fof(f165,plain,
( ! [A,B] :
( ~ subset(A,B)
| element(A,powerset(B)) )
& ! [A,B] :
( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(miniscoping,[status(thm)],[f164]) ).
fof(f167,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f168,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f169,plain,
! [A,C] :
( element(A,C)
| ! [B] :
( ~ element(B,powerset(C))
| ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f168]) ).
fof(f170,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f171,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f172,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f171]) ).
fof(f173,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f174,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f175,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f176,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f177,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f176]) ).
fof(f178,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f179,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f180,plain,
! [B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f179]) ).
fof(f181,plain,
! [B] :
( ( ! [D] :
( ~ in(D,sK18_skl(B))
| ~ in(D,B) )
& in(sK18_skl(B),B) )
| ! [A] : ~ in(A,B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(C,sK18_skl(B))],[f180]) ).
fof(f182,plain,
! [X0,X1] :
( in(sK18_skl(X1),X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f183,plain,
! [X0,X1,X2] :
( ~ in(X2,sK18_skl(X1))
| ~ in(X2,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f184,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f185,plain,
! [B] :
( ~ empty(B)
| ! [A] :
( A = B
| ~ empty(A) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f186,plain,
! [X0,X1] :
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f189,plain,
! [X0] : ~ in(X0,empty_set),
inference(resolution,[status(thm)],[f178,f74]) ).
fof(f194,plain,
! [X0] :
( ~ in(X0,sK16_skl)
| ~ ordinal(X0)
| ~ subset(X0,sK17_skl(X0))
| ~ ordinal(sK17_skl(X0))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f140,f163]) ).
fof(f195,plain,
! [X0] :
( ~ in(X0,sK16_skl)
| ~ subset(X0,sK17_skl(X0))
| ~ ordinal(sK17_skl(X0))
| ~ ordinal(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f194]) ).
fof(f196,plain,
! [X0] :
( ~ in(X0,sK16_skl)
| ~ subset(X0,sK17_skl(X0))
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f195,f161]) ).
fof(f201,plain,
! [X0] :
( empty_set = X0
| in(empty_set,X0)
| ~ ordinal(X0)
| ~ ordinal(empty_set) ),
inference(resolution,[status(thm)],[f152,f189]) ).
fof(f204,plain,
! [X0] :
( empty_set = X0
| in(empty_set,X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f201,f85]) ).
fof(f251,plain,
! [X0] :
( in(sK1_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f154,f73]) ).
fof(f255,plain,
sK4_skl = empty_set,
inference(resolution,[status(thm)],[f96,f175]) ).
fof(f264,plain,
! [X0] :
( sK4_skl = X0
| in(empty_set,X0)
| ~ ordinal(X0) ),
inference(backward_demodulation,[status(thm)],[f255,f204]) ).
fof(f275,plain,
sK16_skl != sK4_skl,
inference(backward_demodulation,[status(thm)],[f255,f160]) ).
fof(f292,plain,
! [X0] :
( sK4_skl = X0
| in(sK4_skl,X0)
| ~ ordinal(X0) ),
inference(forward_demodulation,[status(thm)],[f255,f264]) ).
fof(f390,plain,
! [X0] :
( ~ subset(sK18_skl(sK16_skl),sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f182,f196]) ).
fof(f392,plain,
! [X0] :
( ~ ordinal_subset(sK18_skl(sK16_skl),sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f390,f139]) ).
fof(f393,plain,
! [X0] :
( ~ in(sK18_skl(sK16_skl),sK17_skl(sK18_skl(sK16_skl)))
| ~ epsilon_transitive(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f390,f69]) ).
fof(f394,plain,
! [X0] :
( ~ ordinal_subset(sK18_skl(sK16_skl),sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f392]) ).
fof(f396,plain,
! [X0] :
( ordinal_subset(sK17_skl(sK18_skl(sK16_skl)),sK18_skl(sK16_skl))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f394,f64]) ).
fof(f398,plain,
! [X0] :
( ordinal_subset(sK17_skl(sK18_skl(sK16_skl)),sK18_skl(sK16_skl))
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f396]) ).
fof(f399,plain,
! [X0] :
( sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| in(sK17_skl(sK18_skl(sK16_skl)),sK18_skl(sK16_skl))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ epsilon_transitive(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f393,f152]) ).
fof(f400,plain,
! [X0] :
( sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| in(sK17_skl(sK18_skl(sK16_skl)),sK18_skl(sK16_skl))
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ epsilon_transitive(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f399]) ).
fof(f401,plain,
! [X0] :
( sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| in(sK17_skl(sK18_skl(sK16_skl)),sK18_skl(sK16_skl))
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f400,f49]) ).
fof(f412,plain,
! [X0,X1] :
( ~ element(X1,powerset(sK4_skl))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f173,f96]) ).
fof(f414,plain,
! [X0,X1] :
( ~ subset(X1,sK4_skl)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f412,f167]) ).
fof(f417,plain,
! [X0,X1,X2] :
( ~ subset(X1,X2)
| element(X0,X2)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f170,f167]) ).
fof(f422,plain,
! [X0,X1] :
( sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X1,sK16_skl)
| ~ in(sK17_skl(sK18_skl(sK16_skl)),sK16_skl)
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f183,f401]) ).
fof(f428,plain,
! [X0,X1] :
( ~ in(sK18_skl(sK16_skl),sK16_skl)
| ~ ordinal(sK18_skl(sK16_skl))
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X1,sK16_skl)
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f422,f162]) ).
fof(f430,plain,
! [X0,X1] :
( ~ in(sK18_skl(sK16_skl),sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X1,sK16_skl)
| ~ in(X0,sK16_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f428]) ).
fof(f431,plain,
! [X0,X1] :
( ~ in(sK18_skl(sK16_skl),sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X1,sK16_skl)
| ~ in(X0,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f430,f161]) ).
fof(f433,plain,
! [X0,X1,X2] :
( ~ in(X2,sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X1,sK16_skl)
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f431,f182]) ).
fof(f438,plain,
! [X0,X1,X2,X3] :
( ~ in(sK18_skl(sK16_skl),X3)
| ~ ordinal(X3)
| ~ in(X2,sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| ~ in(X1,sK16_skl)
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f433,f150]) ).
fof(f525,plain,
! [X0,X1,X2] :
( in(X0,X2)
| empty(X2)
| ~ subset(X1,X2)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f417,f154]) ).
fof(f716,plain,
! [X0] :
( in(X0,sK15_skl)
| empty(sK15_skl)
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f525,f159]) ).
fof(f725,plain,
! [X0,X1] :
( X1 = sK15_skl
| ~ empty(X1)
| in(X0,sK15_skl)
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f716,f186]) ).
fof(f795,plain,
! [X0,X1] :
( ~ in(X1,sK16_skl)
| X0 = sK15_skl
| ~ empty(X0)
| in(sK18_skl(sK16_skl),sK15_skl) ),
inference(resolution,[status(thm)],[f725,f182]) ).
fof(f802,plain,
! [X0] :
( empty(sK16_skl)
| X0 = sK15_skl
| ~ empty(X0)
| in(sK18_skl(sK16_skl),sK15_skl) ),
inference(resolution,[status(thm)],[f795,f251]) ).
fof(f803,plain,
! [X0] :
( sK4_skl = sK16_skl
| ~ ordinal(sK16_skl)
| X0 = sK15_skl
| ~ empty(X0)
| in(sK18_skl(sK16_skl),sK15_skl) ),
inference(resolution,[status(thm)],[f795,f292]) ).
fof(f806,plain,
! [X0] :
( ~ ordinal(sK16_skl)
| X0 = sK15_skl
| ~ empty(X0)
| in(sK18_skl(sK16_skl),sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f803,f275]) ).
fof(f809,plain,
! [X0] :
( ~ empty(sK16_skl)
| X0 = sK15_skl
| ~ empty(X0)
| in(sK18_skl(sK16_skl),sK15_skl) ),
inference(resolution,[status(thm)],[f806,f62]) ).
fof(f810,plain,
! [X0] :
( X0 = sK15_skl
| ~ empty(X0)
| in(sK18_skl(sK16_skl),sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f809,f802]) ).
fof(f815,plain,
( sK4_skl = sK15_skl
| in(sK18_skl(sK16_skl),sK15_skl) ),
inference(resolution,[status(thm)],[f810,f96]) ).
fof(f829,plain,
! [X0,X1,X2] :
( ~ ordinal(sK15_skl)
| ~ in(X2,sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| ~ in(X1,sK16_skl)
| ~ in(X0,sK16_skl)
| sK4_skl = sK15_skl ),
inference(resolution,[status(thm)],[f815,f438]) ).
fof(f835,plain,
! [X0,X1,X2] :
( ~ in(X2,sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| ~ in(X1,sK16_skl)
| ~ in(X0,sK16_skl)
| sK4_skl = sK15_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f829,f158]) ).
fof(f959,plain,
! [X0] :
( empty(sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| ~ in(X0,sK16_skl)
| sK4_skl = sK15_skl ),
inference(resolution,[status(thm)],[f835,f251]) ).
fof(f972,plain,
! [X0] :
( sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| ~ in(X0,sK16_skl)
| sK4_skl = sK15_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f959,f178]) ).
fof(f974,plain,
( empty(sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| sK4_skl = sK15_skl ),
inference(resolution,[status(thm)],[f972,f251]) ).
fof(f975,plain,
( sK4_skl = sK16_skl
| ~ ordinal(sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| sK4_skl = sK15_skl ),
inference(resolution,[status(thm)],[f972,f292]) ).
fof(f978,plain,
( ~ ordinal(sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| sK4_skl = sK15_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f975,f275]) ).
fof(f981,plain,
( ~ empty(sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| sK4_skl = sK15_skl ),
inference(resolution,[status(thm)],[f978,f62]) ).
fof(f982,plain,
( sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| sK4_skl = sK15_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f981,f974]) ).
fof(f991,plain,
( sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl)
| subset(sK16_skl,sK4_skl) ),
inference(paramodulation,[status(thm)],[f982,f159]) ).
fof(f1001,plain,
! [X0] :
( ~ in(X0,sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl) ),
inference(resolution,[status(thm)],[f991,f414]) ).
fof(f1005,plain,
( empty(sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl) ),
inference(resolution,[status(thm)],[f1001,f251]) ).
fof(f1006,plain,
( sK4_skl = sK16_skl
| ~ ordinal(sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl) ),
inference(resolution,[status(thm)],[f1001,f292]) ).
fof(f1009,plain,
( ~ ordinal(sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1006,f275]) ).
fof(f1012,plain,
( ~ empty(sK16_skl)
| sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl) ),
inference(resolution,[status(thm)],[f1009,f62]) ).
fof(f1018,plain,
! [X0] :
( ordinal_subset(sK18_skl(sK16_skl),sK18_skl(sK16_skl))
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(backward_demodulation,[status(thm)],[f1031,f398]) ).
fof(f1020,plain,
! [X0] :
( ~ ordinal_subset(sK18_skl(sK16_skl),sK18_skl(sK16_skl))
| ~ ordinal(sK17_skl(sK18_skl(sK16_skl)))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(backward_demodulation,[status(thm)],[f1031,f394]) ).
fof(f1031,plain,
sK17_skl(sK18_skl(sK16_skl)) = sK18_skl(sK16_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1012,f1005]) ).
fof(f1032,plain,
! [X0] :
( ordinal_subset(sK18_skl(sK16_skl),sK18_skl(sK16_skl))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(forward_demodulation,[status(thm)],[f1031,f1018]) ).
fof(f1033,plain,
! [X0] :
( ordinal_subset(sK18_skl(sK16_skl),sK18_skl(sK16_skl))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1032]) ).
fof(f1036,plain,
! [X0] :
( ~ ordinal_subset(sK18_skl(sK16_skl),sK18_skl(sK16_skl))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(forward_demodulation,[status(thm)],[f1031,f1020]) ).
fof(f1037,plain,
! [X0] :
( ~ ordinal_subset(sK18_skl(sK16_skl),sK18_skl(sK16_skl))
| ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1036]) ).
fof(f1038,plain,
! [X0] :
( ~ ordinal(sK18_skl(sK16_skl))
| ~ in(X0,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1037,f1033]) ).
fof(f1105,plain,
! [X0,X1] :
( ~ in(sK18_skl(sK16_skl),X1)
| ~ ordinal(X1)
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f1038,f150]) ).
fof(f1108,plain,
! [X0] :
( sK4_skl = sK15_skl
| ~ ordinal(sK15_skl)
| ~ in(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f1105,f815]) ).
fof(f1112,plain,
! [X0] :
( sK4_skl = sK15_skl
| ~ in(X0,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1108,f158]) ).
fof(f1115,plain,
( empty(sK16_skl)
| sK4_skl = sK15_skl ),
inference(resolution,[status(thm)],[f1112,f251]) ).
fof(f1116,plain,
( sK4_skl = sK16_skl
| ~ ordinal(sK16_skl)
| sK4_skl = sK15_skl ),
inference(resolution,[status(thm)],[f1112,f292]) ).
fof(f1119,plain,
( ~ ordinal(sK16_skl)
| sK4_skl = sK15_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f1116,f275]) ).
fof(f1122,plain,
( ~ empty(sK16_skl)
| sK4_skl = sK15_skl ),
inference(resolution,[status(thm)],[f1119,f62]) ).
fof(f1134,plain,
subset(sK16_skl,sK4_skl),
inference(backward_demodulation,[status(thm)],[f1152,f159]) ).
fof(f1152,plain,
sK4_skl = sK15_skl,
inference(forward_subsumption_resolution,[status(thm)],[f1122,f1115]) ).
fof(f1174,plain,
! [X0] : ~ in(X0,sK16_skl),
inference(resolution,[status(thm)],[f1134,f414]) ).
fof(f1181,plain,
empty(sK16_skl),
inference(resolution,[status(thm)],[f1174,f251]) ).
fof(f1182,plain,
( sK4_skl = sK16_skl
| ~ ordinal(sK16_skl) ),
inference(resolution,[status(thm)],[f1174,f292]) ).
fof(f1188,plain,
~ ordinal(sK16_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1182,f275]) ).
fof(f1191,plain,
~ empty(sK16_skl),
inference(resolution,[status(thm)],[f1188,f62]) ).
fof(f1193,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1191,f1181]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU235+3 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n012.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 06:01:37 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 2.44/0.86 % Refutation found
% 2.44/0.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.44/0.86 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.44/0.90 % Elapsed time: 0.527788 seconds
% 2.44/0.90 % CPU time: 3.892916 seconds
% 2.44/0.90 % Total memory used: 134.232 MB
% 2.44/0.90 % Net memory used: 128.441 MB
%------------------------------------------------------------------------------