%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET766+4 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 02:10:34 PM UTC 2026
% Result : Theorem 0.15s 0.45s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 5
% Syntax : Number of formulae : 35 ( 6 unt; 2 def)
% Number of atoms : 199 ( 0 equ)
% Maximal formula atoms : 16 ( 5 avg)
% Number of connectives : 257 ( 93 ~; 88 |; 62 &)
% ( 7 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-3 aty)
% Number of variables : 138 ( 123 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f14,axiom,
! [A,R] :
( equivalence(R,A)
<=> ( ! [X,Y,Z] :
( ( member(Z,A)
& member(Y,A)
& member(X,A) )
=> ( ( apply(R,Y,Z)
& apply(R,X,Y) )
=> apply(R,X,Z) ) )
& ! [X,Y] :
( ( member(Y,A)
& member(X,A) )
=> ( apply(R,X,Y)
=> apply(R,Y,X) ) )
& ! [X] :
( member(X,A)
=> apply(R,X,X) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [R,E,A,X] :
( member(X,equivalence_class(A,E,R))
<=> ( apply(R,A,X)
& member(X,E) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,conjecture,
! [E,R,A] :
( ( member(A,E)
& equivalence(R,E) )
=> member(A,equivalence_class(A,E,R)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
~ ! [E,R,A] :
( ( member(A,E)
& equivalence(R,E) )
=> member(A,equivalence_class(A,E,R)) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f93,plain,
! [A,R] :
( equivalence(R,A)
<=> ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,A)
| ~ member(Y,A)
| ~ member(X,A) )
& ! [X,Y] :
( apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,A)
| ~ member(X,A) )
& ! [X] :
( apply(R,X,X)
| ~ member(X,A) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f94,definition,
! [A,R] :
( sP1_prd(R,A)
<=> ( ! [X,Y] :
( apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,A)
| ~ member(X,A) )
& ! [X] :
( apply(R,X,X)
| ~ member(X,A) ) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f95,plain,
! [A,R] :
( equivalence(R,A)
<=> ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,A)
| ~ member(Y,A)
| ~ member(X,A) )
& sP1_prd(R,A) ) ),
inference(formula_renaming,[status(thm)],[f93,f94]) ).
fof(f96,plain,
! [A,R] :
( ( ? [X,Y,Z] :
( ~ apply(R,X,Z)
& apply(R,Y,Z)
& apply(R,X,Y)
& member(Z,A)
& member(Y,A)
& member(X,A) )
| ~ sP1_prd(R,A)
| equivalence(R,A) )
& ( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,A)
| ~ member(Y,A)
| ~ member(X,A) )
& sP1_prd(R,A) )
| ~ equivalence(R,A) ) ),
inference(NNF_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
( ! [A,R] :
( ? [X,Y,Z] :
( ~ apply(R,X,Z)
& apply(R,Y,Z)
& apply(R,X,Y)
& member(Z,A)
& member(Y,A)
& member(X,A) )
| ~ sP1_prd(R,A)
| equivalence(R,A) )
& ! [A,R] :
( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,A)
| ~ member(Y,A)
| ~ member(X,A) )
& sP1_prd(R,A) )
| ~ equivalence(R,A) ) ),
inference(miniscoping,[status(thm)],[f96]) ).
fof(f98,plain,
( ! [A,R] :
( ( ~ apply(R,sK7_skl(R,A),sK9_skl(R,A))
& apply(R,sK8_skl(R,A),sK9_skl(R,A))
& apply(R,sK7_skl(R,A),sK8_skl(R,A))
& member(sK9_skl(R,A),A)
& member(sK8_skl(R,A),A)
& member(sK7_skl(R,A),A) )
| ~ sP1_prd(R,A)
| equivalence(R,A) )
& ! [A,R] :
( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,A)
| ~ member(Y,A)
| ~ member(X,A) )
& sP1_prd(R,A) )
| ~ equivalence(R,A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl]),skolemize(X,sK7_skl(R,A)),skolemize(Y,sK8_skl(R,A)),skolemize(Z,sK9_skl(R,A))],[f97]) ).
fof(f99,plain,
! [X0,X1] :
( sP1_prd(X0,X1)
| ~ equivalence(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f107,plain,
! [R,E,A,X] :
( ( ~ apply(R,A,X)
| ~ member(X,E)
| member(X,equivalence_class(A,E,R)) )
& ( ( apply(R,A,X)
& member(X,E) )
| ~ member(X,equivalence_class(A,E,R)) ) ),
inference(NNF_transformation,[status(thm)],[f15]) ).
fof(f108,plain,
( ! [R,E,A,X] :
( ~ apply(R,A,X)
| ~ member(X,E)
| member(X,equivalence_class(A,E,R)) )
& ! [R,E,A,X] :
( ( apply(R,A,X)
& member(X,E) )
| ~ member(X,equivalence_class(A,E,R)) ) ),
inference(miniscoping,[status(thm)],[f107]) ).
fof(f111,plain,
! [X0,X1,X2,X3] :
( ~ apply(X3,X1,X0)
| ~ member(X0,X2)
| member(X0,equivalence_class(X1,X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f126,plain,
? [E,R,A] :
( ~ member(A,equivalence_class(A,E,R))
& member(A,E)
& equivalence(R,E) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f127,plain,
( ~ member(sK16_skl,equivalence_class(sK16_skl,sK14_skl,sK15_skl))
& member(sK16_skl,sK14_skl)
& equivalence(sK15_skl,sK14_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(E,sK14_skl),skolemize(R,sK15_skl),skolemize(A,sK16_skl)],[f126]) ).
fof(f128,plain,
equivalence(sK15_skl,sK14_skl),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
member(sK16_skl,sK14_skl),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f130,plain,
~ member(sK16_skl,equivalence_class(sK16_skl,sK14_skl,sK15_skl)),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f141,definition,
! [A,R,X] :
( sP3_prd(X,R,A)
<=> ( apply(R,X,X)
| ~ member(X,A) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f142,plain,
! [A,R] :
( sP1_prd(R,A)
<=> ( ! [X,Y] :
( apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,A)
| ~ member(X,A) )
& ! [X] : sP3_prd(X,R,A) ) ),
inference(formula_renaming,[status(thm)],[f94,f141]) ).
fof(f143,plain,
! [A,R] :
( ( ? [X,Y] :
( ~ apply(R,Y,X)
& apply(R,X,Y)
& member(Y,A)
& member(X,A) )
| ? [X] : ~ sP3_prd(X,R,A)
| sP1_prd(R,A) )
& ( ( ! [X,Y] :
( apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,A)
| ~ member(X,A) )
& ! [X] : sP3_prd(X,R,A) )
| ~ sP1_prd(R,A) ) ),
inference(NNF_transformation,[status(thm)],[f142]) ).
fof(f144,plain,
( ! [A,R] :
( ? [X,Y] :
( ~ apply(R,Y,X)
& apply(R,X,Y)
& member(Y,A)
& member(X,A) )
| ? [X] : ~ sP3_prd(X,R,A)
| sP1_prd(R,A) )
& ! [A,R] :
( ( ! [X,Y] :
( apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,A)
| ~ member(X,A) )
& ! [X] : sP3_prd(X,R,A) )
| ~ sP1_prd(R,A) ) ),
inference(miniscoping,[status(thm)],[f143]) ).
fof(f145,plain,
( ! [A,R] :
( ( ~ apply(R,sK22_skl(R,A),sK21_skl(R,A))
& apply(R,sK21_skl(R,A),sK22_skl(R,A))
& member(sK22_skl(R,A),A)
& member(sK21_skl(R,A),A) )
| ~ sP3_prd(sK20_skl(R,A),R,A)
| sP1_prd(R,A) )
& ! [A,R] :
( ( ! [X,Y] :
( apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,A)
| ~ member(X,A) )
& ! [X] : sP3_prd(X,R,A) )
| ~ sP1_prd(R,A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl]),skolemize(X,sK20_skl(R,A)),skolemize(X,sK21_skl(R,A)),skolemize(Y,sK22_skl(R,A))],[f144]) ).
fof(f146,plain,
! [X0,X1,X2] :
( sP3_prd(X2,X0,X1)
| ~ sP1_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f157,plain,
! [A,R,X] :
( ( ( ~ apply(R,X,X)
& member(X,A) )
| sP3_prd(X,R,A) )
& ( apply(R,X,X)
| ~ member(X,A)
| ~ sP3_prd(X,R,A) ) ),
inference(NNF_transformation,[status(thm)],[f141]) ).
fof(f158,plain,
( ! [A,R,X] :
( ( ~ apply(R,X,X)
& member(X,A) )
| sP3_prd(X,R,A) )
& ! [A,R,X] :
( apply(R,X,X)
| ~ member(X,A)
| ~ sP3_prd(X,R,A) ) ),
inference(miniscoping,[status(thm)],[f157]) ).
fof(f159,plain,
! [X0,X1,X2] :
( apply(X1,X0,X0)
| ~ member(X0,X2)
| ~ sP3_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f192,plain,
! [X0,X1,X2] :
( ~ sP1_prd(X2,X1)
| apply(X2,X0,X0)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f159,f146]) ).
fof(f193,plain,
! [X0,X1,X2] :
( ~ equivalence(X2,X1)
| apply(X2,X0,X0)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f192,f99]) ).
fof(f194,plain,
! [X0] :
( apply(sK15_skl,X0,X0)
| ~ member(X0,sK14_skl) ),
inference(resolution,[status(thm)],[f193,f128]) ).
fof(f195,plain,
apply(sK15_skl,sK16_skl,sK16_skl),
inference(resolution,[status(thm)],[f194,f129]) ).
fof(f199,plain,
! [X0] :
( ~ member(sK16_skl,X0)
| member(sK16_skl,equivalence_class(sK16_skl,X0,sK15_skl)) ),
inference(resolution,[status(thm)],[f195,f111]) ).
fof(f248,plain,
~ member(sK16_skl,sK14_skl),
inference(resolution,[status(thm)],[f199,f130]) ).
fof(f252,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f248,f129]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET766+4 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n013.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 05:36:20 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 0.15/0.45 % Refutation found
% 0.15/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.51 % Elapsed time: 0.077780 seconds
% 0.15/0.51 % CPU time: 0.111362 seconds
% 0.15/0.51 % Total memory used: 5.362 MB
% 0.15/0.51 % Net memory used: 5.341 MB
%------------------------------------------------------------------------------