%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET809+4 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:10:39 PM UTC 2026
% Result : Theorem 0.13s 5.95s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 9
% Syntax : Number of formulae : 52 ( 5 unt; 4 def)
% Number of atoms : 255 ( 0 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 325 ( 122 ~; 112 |; 72 &)
% ( 12 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 4 prp; 0-4 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-3 aty)
% Number of variables : 151 ( 129 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [A] :
( member(A,on)
<=> ( ! [X] :
( member(X,A)
=> subset(X,A) )
& strict_well_order(member_predicate,A)
& set(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [R,E] :
( strict_well_order(R,E)
<=> ( ! [A] :
( ( ? [X] : member(X,A)
& subset(A,E) )
=> ? [Y] : least(Y,R,A) )
& strict_order(R,E) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X,Y] :
( apply(member_predicate,X,Y)
<=> member(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [R,E] :
( strict_order(R,E)
<=> ( ! [X,Y,Z] :
( ( member(Z,E)
& member(Y,E)
& member(X,E) )
=> ( ( apply(R,Y,Z)
& apply(R,X,Y) )
=> apply(R,X,Z) ) )
& ! [X,Y] :
( ( member(Y,E)
& member(X,E) )
=> ~ ( apply(R,Y,X)
& apply(R,X,Y) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,conjecture,
! [A] :
( member(A,on)
=> ~ member(A,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
~ ! [A] :
( member(A,on)
=> ~ member(A,A) ),
inference(negated_conjecture,[status(cth)],[f20]) ).
fof(f76,plain,
! [A] :
( member(A,on)
<=> ( ! [X] :
( subset(X,A)
| ~ member(X,A) )
& strict_well_order(member_predicate,A)
& set(A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f77,plain,
! [A] :
( ( ? [X] :
( ~ subset(X,A)
& member(X,A) )
| ~ strict_well_order(member_predicate,A)
| ~ set(A)
| member(A,on) )
& ( ( ! [X] :
( subset(X,A)
| ~ member(X,A) )
& strict_well_order(member_predicate,A)
& set(A) )
| ~ member(A,on) ) ),
inference(NNF_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
( ! [A] :
( ? [X] :
( ~ subset(X,A)
& member(X,A) )
| ~ strict_well_order(member_predicate,A)
| ~ set(A)
| member(A,on) )
& ! [A] :
( ( ! [X] :
( subset(X,A)
| ~ member(X,A) )
& strict_well_order(member_predicate,A)
& set(A) )
| ~ member(A,on) ) ),
inference(miniscoping,[status(thm)],[f77]) ).
fof(f79,plain,
( ! [A] :
( ( ~ subset(sK3_skl(A),A)
& member(sK3_skl(A),A) )
| ~ strict_well_order(member_predicate,A)
| ~ set(A)
| member(A,on) )
& ! [A] :
( ( ! [X] :
( subset(X,A)
| ~ member(X,A) )
& strict_well_order(member_predicate,A)
& set(A) )
| ~ member(A,on) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X,sK3_skl(A))],[f78]) ).
fof(f81,plain,
! [X0] :
( strict_well_order(member_predicate,X0)
| ~ member(X0,on) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f85,plain,
! [R,E] :
( strict_well_order(R,E)
<=> ( ! [A] :
( ? [Y] : least(Y,R,A)
| ! [X] : ~ member(X,A)
| ~ subset(A,E) )
& strict_order(R,E) ) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f86,plain,
! [R,E] :
( ( ? [A] :
( ! [Y] : ~ least(Y,R,A)
& ? [X] : member(X,A)
& subset(A,E) )
| ~ strict_order(R,E)
| strict_well_order(R,E) )
& ( ( ! [A] :
( ? [Y] : least(Y,R,A)
| ! [X] : ~ member(X,A)
| ~ subset(A,E) )
& strict_order(R,E) )
| ~ strict_well_order(R,E) ) ),
inference(NNF_transformation,[status(thm)],[f85]) ).
fof(f87,plain,
( ! [R,E] :
( ? [A] :
( ! [Y] : ~ least(Y,R,A)
& ? [X] : member(X,A)
& subset(A,E) )
| ~ strict_order(R,E)
| strict_well_order(R,E) )
& ! [R,E] :
( ( ! [A] :
( ? [Y] : least(Y,R,A)
| ! [X] : ~ member(X,A)
| ~ subset(A,E) )
& strict_order(R,E) )
| ~ strict_well_order(R,E) ) ),
inference(miniscoping,[status(thm)],[f86]) ).
fof(f88,plain,
( ! [R,E] :
( ( ! [Y] : ~ least(Y,R,sK5_skl(E,R))
& member(sK6_skl(E,R),sK5_skl(E,R))
& subset(sK5_skl(E,R),E) )
| ~ strict_order(R,E)
| strict_well_order(R,E) )
& ! [R,E] :
( ( ! [A] :
( least(sK4_skl(A,E,R),R,A)
| ! [X] : ~ member(X,A)
| ~ subset(A,E) )
& strict_order(R,E) )
| ~ strict_well_order(R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(Y,sK4_skl(A,E,R)),skolemize(A,sK5_skl(E,R)),skolemize(X,sK6_skl(E,R))],[f87]) ).
fof(f89,plain,
! [X0,X1] :
( strict_order(X0,X1)
| ~ strict_well_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f103,plain,
! [X,Y] :
( ( ~ member(X,Y)
| apply(member_predicate,X,Y) )
& ( member(X,Y)
| ~ apply(member_predicate,X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f15]) ).
fof(f104,plain,
( ! [X,Y] :
( ~ member(X,Y)
| apply(member_predicate,X,Y) )
& ! [X,Y] :
( member(X,Y)
| ~ apply(member_predicate,X,Y) ) ),
inference(miniscoping,[status(thm)],[f103]) ).
fof(f106,plain,
! [X0,X1] :
( ~ member(X0,X1)
| apply(member_predicate,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f107,plain,
! [R,E] :
( strict_order(R,E)
<=> ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] :
( ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f108,definition,
! [R,E,X,Y] :
( sP0_prd(Y,X,E,R)
<=> ( ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f109,plain,
! [R,E] :
( strict_order(R,E)
<=> ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] : sP0_prd(Y,X,E,R) ) ),
inference(formula_renaming,[status(thm)],[f107,f108]) ).
fof(f110,plain,
! [R,E] :
( ( ? [X,Y,Z] :
( ~ apply(R,X,Z)
& apply(R,Y,Z)
& apply(R,X,Y)
& member(Z,E)
& member(Y,E)
& member(X,E) )
| ? [X,Y] : ~ sP0_prd(Y,X,E,R)
| strict_order(R,E) )
& ( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] : sP0_prd(Y,X,E,R) )
| ~ strict_order(R,E) ) ),
inference(NNF_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
( ! [R,E] :
( ? [X,Y,Z] :
( ~ apply(R,X,Z)
& apply(R,Y,Z)
& apply(R,X,Y)
& member(Z,E)
& member(Y,E)
& member(X,E) )
| ? [X,Y] : ~ sP0_prd(Y,X,E,R)
| strict_order(R,E) )
& ! [R,E] :
( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] : sP0_prd(Y,X,E,R) )
| ~ strict_order(R,E) ) ),
inference(miniscoping,[status(thm)],[f110]) ).
fof(f112,plain,
( ! [R,E] :
( ( ~ apply(R,sK10_skl(E,R),sK12_skl(E,R))
& apply(R,sK11_skl(E,R),sK12_skl(E,R))
& apply(R,sK10_skl(E,R),sK11_skl(E,R))
& member(sK12_skl(E,R),E)
& member(sK11_skl(E,R),E)
& member(sK10_skl(E,R),E) )
| ~ sP0_prd(sK9_skl(E,R),sK8_skl(E,R),E,R)
| strict_order(R,E) )
& ! [R,E] :
( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] : sP0_prd(Y,X,E,R) )
| ~ strict_order(R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl]),skolemize(X,sK8_skl(E,R)),skolemize(Y,sK9_skl(E,R)),skolemize(X,sK10_skl(E,R)),skolemize(Y,sK11_skl(E,R)),skolemize(Z,sK12_skl(E,R))],[f111]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( sP0_prd(X2,X3,X1,X0)
| ~ strict_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f132,plain,
? [A] :
( member(A,A)
& member(A,on) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f133,plain,
( member(sK13_skl,sK13_skl)
& member(sK13_skl,on) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f132]) ).
fof(f134,plain,
member(sK13_skl,on),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
member(sK13_skl,sK13_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f136,plain,
! [R,E,X,Y] :
( ( ( apply(R,Y,X)
& apply(R,X,Y)
& member(Y,E)
& member(X,E) )
| sP0_prd(Y,X,E,R) )
& ( ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E)
| ~ sP0_prd(Y,X,E,R) ) ),
inference(NNF_transformation,[status(thm)],[f108]) ).
fof(f137,plain,
( ! [R,E,X,Y] :
( ( apply(R,Y,X)
& apply(R,X,Y)
& member(Y,E)
& member(X,E) )
| sP0_prd(Y,X,E,R) )
& ! [R,E,X,Y] :
( ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E)
| ~ sP0_prd(Y,X,E,R) ) ),
inference(miniscoping,[status(thm)],[f136]) ).
fof(f138,plain,
! [X0,X1,X2,X3] :
( ~ apply(X3,X0,X1)
| ~ apply(X3,X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f2143,plain,
! [X0,X1,X2,X3] :
( ~ strict_order(X3,X1)
| ~ apply(X3,X2,X0)
| ~ apply(X3,X0,X2)
| ~ member(X2,X1)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f138,f113]) ).
fof(f5596,plain,
! [X0] :
( ~ strict_order(X0,sK13_skl)
| ~ apply(X0,sK13_skl,sK13_skl)
| ~ apply(X0,sK13_skl,sK13_skl) ),
inference(resolution,[status(thm)],[f2143,f135]) ).
fof(f5762,plain,
! [X0] :
( ~ strict_order(X0,sK13_skl)
| ~ apply(X0,sK13_skl,sK13_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f5596]) ).
fof(f5836,definition,
( sQ165_spl
<=> member(sK13_skl,sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f5838,plain,
( sQ165_spl
| ~ member(sK13_skl,sK13_skl) ),
inference(component_clause,[status(thm)],[f5836]) ).
fof(f5849,plain,
( sQ165_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5838,f135]) ).
fof(f5850,plain,
sQ165_spl,
inference(contradiction_clause,[status(thm)],[f5849]) ).
fof(f5869,definition,
( sQ168_spl
<=> member(sK13_skl,on) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f5871,plain,
( sQ168_spl
| ~ member(sK13_skl,on) ),
inference(component_clause,[status(thm)],[f5869]) ).
fof(f5894,plain,
( sQ168_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5871,f134]) ).
fof(f5895,plain,
sQ168_spl,
inference(contradiction_clause,[status(thm)],[f5894]) ).
fof(f5897,plain,
( ~ member(sK13_skl,sK13_skl)
| ~ strict_order(member_predicate,sK13_skl) ),
inference(resolution,[status(thm)],[f5762,f106]) ).
fof(f5901,definition,
( sQ174_spl
<=> strict_order(member_predicate,sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f5903,plain,
( sQ174_spl
| ~ strict_order(member_predicate,sK13_skl) ),
inference(component_clause,[status(thm)],[f5901]) ).
fof(f5904,plain,
( ~ sQ165_spl
| ~ sQ174_spl ),
inference(split_clause,[status(thm)],[f5897,f5901,f5836]) ).
fof(f5911,plain,
( sQ174_spl
| ~ strict_well_order(member_predicate,sK13_skl) ),
inference(resolution,[status(thm)],[f5903,f89]) ).
fof(f5920,plain,
( sQ174_spl
| ~ member(sK13_skl,on) ),
inference(resolution,[status(thm)],[f5911,f81]) ).
fof(f5922,plain,
( sQ174_spl
| ~ sQ168_spl ),
inference(split_clause,[status(thm)],[f5920,f5869,f5901]) ).
fof(f5927,plain,
$false,
inference(sat_refutation,[status(thm)],[f5850,f5895,f5904,f5922]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET809+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n006.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 05:39:03 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 0.13/5.95 % Refutation found
% 0.13/5.95 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.95 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/5.97 % Elapsed time: 0.591260 seconds
% 0.13/5.97 % CPU time: 4.532314 seconds
% 0.13/5.97 % Total memory used: 143.662 MB
% 0.13/5.97 % Net memory used: 134.471 MB
%------------------------------------------------------------------------------