%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU425+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:20:33 PM UTC 2026
% Result : Theorem 147.41s 21.71s
% Output : CNFRefutation 21.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 7
% Syntax : Number of formulae : 52 ( 12 unt; 0 def)
% Number of atoms : 168 ( 33 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 196 ( 80 ~; 73 |; 29 &)
% ( 2 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 99 ( 91 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1333,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> v1_relat_1(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1344,axiom,
! [A,B] :
( v1_relat_1(B)
=> ( r1_tarski(k2_relat_1(B),A)
=> m2_relset_1(B,k1_relat_1(B),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1819,axiom,
! [A,B] :
( ( v1_funct_1(B)
& v1_relat_1(B) )
=> ( r1_tarski(k2_relat_1(B),A)
=> ( m2_relset_1(B,k1_relat_1(B),A)
& v1_funct_2(B,k1_relat_1(B),A)
& v1_funct_1(B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19060,axiom,
! [A,B] :
( v1_relat_1(B)
=> ( v1_funct_1(k5_relset_2(A,B))
& v1_relat_1(k5_relset_2(A,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19088,axiom,
! [A,B] :
( v1_relat_1(B)
=> ! [C] :
( ( v1_funct_1(C)
& v1_relat_1(C) )
=> ( C = k5_relset_2(A,B)
<=> ( ! [D] :
( r1_tarski(D,A)
=> k1_funct_1(C,D) = k9_relat_1(B,D) )
& k1_relat_1(C) = k1_zfmisc_1(A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19090,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> r1_tarski(k2_relat_1(k5_relset_2(A,C)),k1_zfmisc_1(k2_relat_1(C))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19091,conjecture,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> ( m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
& v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
& v1_funct_1(k5_relset_2(A,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19092,negated_conjecture,
~ ! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> ( m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
& v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
& v1_funct_1(k5_relset_2(A,C)) ) ),
inference(negated_conjecture,[status(cth)],[f19091]) ).
fof(f22445,plain,
! [A,B,C] :
( v1_relat_1(C)
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f1333]) ).
fof(f22446,plain,
! [C] :
( v1_relat_1(C)
| ! [A,B] : ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(miniscoping,[status(thm)],[f22445]) ).
fof(f22447,plain,
! [X0,X1,X2] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f22446]) ).
fof(f22466,plain,
! [A,B] :
( m2_relset_1(B,k1_relat_1(B),A)
| ~ r1_tarski(k2_relat_1(B),A)
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f1344]) ).
fof(f22467,plain,
! [B] :
( ! [A] :
( m2_relset_1(B,k1_relat_1(B),A)
| ~ r1_tarski(k2_relat_1(B),A) )
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f22466]) ).
fof(f22468,plain,
! [X0,X1] :
( m2_relset_1(X0,k1_relat_1(X0),X1)
| ~ r1_tarski(k2_relat_1(X0),X1)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f22467]) ).
fof(f23810,plain,
! [A,B] :
( ( m2_relset_1(B,k1_relat_1(B),A)
& v1_funct_2(B,k1_relat_1(B),A)
& v1_funct_1(B) )
| ~ r1_tarski(k2_relat_1(B),A)
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f1819]) ).
fof(f23811,plain,
! [B] :
( ! [A] :
( ( m2_relset_1(B,k1_relat_1(B),A)
& v1_funct_2(B,k1_relat_1(B),A)
& v1_funct_1(B) )
| ~ r1_tarski(k2_relat_1(B),A) )
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f23810]) ).
fof(f23813,plain,
! [X0,X1] :
( v1_funct_2(X0,k1_relat_1(X0),X1)
| ~ r1_tarski(k2_relat_1(X0),X1)
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f23811]) ).
fof(f89194,plain,
! [A,B] :
( ( v1_funct_1(k5_relset_2(A,B))
& v1_relat_1(k5_relset_2(A,B)) )
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f19060]) ).
fof(f89195,plain,
! [B] :
( ( ! [A] : v1_funct_1(k5_relset_2(A,B))
& ! [A] : v1_relat_1(k5_relset_2(A,B)) )
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f89194]) ).
fof(f89196,plain,
! [X0,X1] :
( v1_relat_1(k5_relset_2(X1,X0))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f89195]) ).
fof(f89197,plain,
! [X0,X1] :
( v1_funct_1(k5_relset_2(X1,X0))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f89195]) ).
fof(f89266,plain,
! [A,B] :
( ! [C] :
( ( C = k5_relset_2(A,B)
<=> ( ! [D] :
( k1_funct_1(C,D) = k9_relat_1(B,D)
| ~ r1_tarski(D,A) )
& k1_relat_1(C) = k1_zfmisc_1(A) ) )
| ~ v1_funct_1(C)
| ~ v1_relat_1(C) )
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f19088]) ).
fof(f89267,plain,
! [A,B] :
( ! [C] :
( ( ( ? [D] :
( k1_funct_1(C,D) != k9_relat_1(B,D)
& r1_tarski(D,A) )
| k1_relat_1(C) != k1_zfmisc_1(A)
| C = k5_relset_2(A,B) )
& ( ( ! [D] :
( k1_funct_1(C,D) = k9_relat_1(B,D)
| ~ r1_tarski(D,A) )
& k1_relat_1(C) = k1_zfmisc_1(A) )
| C != k5_relset_2(A,B) ) )
| ~ v1_funct_1(C)
| ~ v1_relat_1(C) )
| ~ v1_relat_1(B) ),
inference(NNF_transformation,[status(thm)],[f89266]) ).
fof(f89268,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ? [D] :
( k1_funct_1(C,D) != k9_relat_1(B,D)
& r1_tarski(D,A) )
| k1_relat_1(C) != k1_zfmisc_1(A)
| C = k5_relset_2(A,B) )
& ! [A] :
( ( ! [D] :
( k1_funct_1(C,D) = k9_relat_1(B,D)
| ~ r1_tarski(D,A) )
& k1_relat_1(C) = k1_zfmisc_1(A) )
| C != k5_relset_2(A,B) ) )
| ~ v1_funct_1(C)
| ~ v1_relat_1(C) )
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f89267]) ).
fof(f89269,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ( k1_funct_1(C,sK6521_skl(A,C,B)) != k9_relat_1(B,sK6521_skl(A,C,B))
& r1_tarski(sK6521_skl(A,C,B),A) )
| k1_relat_1(C) != k1_zfmisc_1(A)
| C = k5_relset_2(A,B) )
& ! [A] :
( ( ! [D] :
( k1_funct_1(C,D) = k9_relat_1(B,D)
| ~ r1_tarski(D,A) )
& k1_relat_1(C) = k1_zfmisc_1(A) )
| C != k5_relset_2(A,B) ) )
| ~ v1_funct_1(C)
| ~ v1_relat_1(C) )
| ~ v1_relat_1(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6521_skl]),skolemize(D,sK6521_skl(A,C,B))],[f89268]) ).
fof(f89270,plain,
! [X0,X1,X2] :
( k1_relat_1(X1) = k1_zfmisc_1(X2)
| X1 != k5_relset_2(X2,X0)
| ~ v1_funct_1(X1)
| ~ v1_relat_1(X1)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f89269]) ).
fof(f89277,plain,
! [A,B,C] :
( r1_tarski(k2_relat_1(k5_relset_2(A,C)),k1_zfmisc_1(k2_relat_1(C)))
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f19090]) ).
fof(f89278,plain,
! [A,C] :
( r1_tarski(k2_relat_1(k5_relset_2(A,C)),k1_zfmisc_1(k2_relat_1(C)))
| ! [B] : ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(miniscoping,[status(thm)],[f89277]) ).
fof(f89279,plain,
! [X0,X1,X2] :
( r1_tarski(k2_relat_1(k5_relset_2(X1,X0)),k1_zfmisc_1(k2_relat_1(X0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f89278]) ).
fof(f89280,plain,
? [A,B,C] :
( ( ~ m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
| ~ v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
| ~ v1_funct_1(k5_relset_2(A,C)) )
& m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f19092]) ).
fof(f89281,plain,
? [A,C] :
( ( ~ m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
| ~ v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
| ~ v1_funct_1(k5_relset_2(A,C)) )
& ? [B] : m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(miniscoping,[status(thm)],[f89280]) ).
fof(f89282,plain,
( ( ~ m2_relset_1(k5_relset_2(sK6522_skl,sK6523_skl),k1_zfmisc_1(sK6522_skl),k1_zfmisc_1(k2_relat_1(sK6523_skl)))
| ~ v1_funct_2(k5_relset_2(sK6522_skl,sK6523_skl),k1_zfmisc_1(sK6522_skl),k1_zfmisc_1(k2_relat_1(sK6523_skl)))
| ~ v1_funct_1(k5_relset_2(sK6522_skl,sK6523_skl)) )
& m1_subset_1(sK6523_skl,k1_zfmisc_1(k2_zfmisc_1(sK6522_skl,sK6524_skl))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6522_skl,sK6523_skl,sK6524_skl]),skolemize(A,sK6522_skl),skolemize(C,sK6523_skl),skolemize(B,sK6524_skl)],[f89281]) ).
fof(f89283,plain,
m1_subset_1(sK6523_skl,k1_zfmisc_1(k2_zfmisc_1(sK6522_skl,sK6524_skl))),
inference(cnf_transformation,[status(thm)],[f89282]) ).
fof(f89284,plain,
( ~ m2_relset_1(k5_relset_2(sK6522_skl,sK6523_skl),k1_zfmisc_1(sK6522_skl),k1_zfmisc_1(k2_relat_1(sK6523_skl)))
| ~ v1_funct_2(k5_relset_2(sK6522_skl,sK6523_skl),k1_zfmisc_1(sK6522_skl),k1_zfmisc_1(k2_relat_1(sK6523_skl)))
| ~ v1_funct_1(k5_relset_2(sK6522_skl,sK6523_skl)) ),
inference(cnf_transformation,[status(thm)],[f89282]) ).
fof(f97223,plain,
v1_relat_1(sK6523_skl),
inference(resolution,[status(thm)],[f22447,f89283]) ).
fof(f97272,plain,
! [X0] : v1_funct_1(k5_relset_2(X0,sK6523_skl)),
inference(resolution,[status(thm)],[f97223,f89197]) ).
fof(f97274,plain,
! [X0] : v1_relat_1(k5_relset_2(X0,sK6523_skl)),
inference(resolution,[status(thm)],[f97223,f89196]) ).
fof(f97275,plain,
( ~ m2_relset_1(k5_relset_2(sK6522_skl,sK6523_skl),k1_zfmisc_1(sK6522_skl),k1_zfmisc_1(k2_relat_1(sK6523_skl)))
| ~ v1_funct_2(k5_relset_2(sK6522_skl,sK6523_skl),k1_zfmisc_1(sK6522_skl),k1_zfmisc_1(k2_relat_1(sK6523_skl))) ),
inference(backward_subsumption_resolution,[status(thm)],[f89284,f97272]) ).
fof(f99243,plain,
! [X0,X1] :
( k1_relat_1(X0) = k1_zfmisc_1(X1)
| X0 != k5_relset_2(X1,sK6523_skl)
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(resolution,[status(thm)],[f89270,f97223]) ).
fof(f99548,plain,
! [X0,X1] :
( k1_relat_1(k5_relset_2(X0,sK6523_skl)) = k1_zfmisc_1(X1)
| k5_relset_2(X0,sK6523_skl) != k5_relset_2(X1,sK6523_skl)
| ~ v1_relat_1(k5_relset_2(X0,sK6523_skl)) ),
inference(resolution,[status(thm)],[f99243,f97272]) ).
fof(f99605,plain,
! [X0,X1] :
( k1_relat_1(k5_relset_2(X0,sK6523_skl)) = k1_zfmisc_1(X1)
| k5_relset_2(X0,sK6523_skl) != k5_relset_2(X1,sK6523_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f99548,f97274]) ).
fof(f99776,plain,
r1_tarski(k2_relat_1(k5_relset_2(sK6522_skl,sK6523_skl)),k1_zfmisc_1(k2_relat_1(sK6523_skl))),
inference(resolution,[status(thm)],[f89279,f89283]) ).
fof(f99945,plain,
( v1_funct_2(k5_relset_2(sK6522_skl,sK6523_skl),k1_relat_1(k5_relset_2(sK6522_skl,sK6523_skl)),k1_zfmisc_1(k2_relat_1(sK6523_skl)))
| ~ v1_funct_1(k5_relset_2(sK6522_skl,sK6523_skl))
| ~ v1_relat_1(k5_relset_2(sK6522_skl,sK6523_skl)) ),
inference(resolution,[status(thm)],[f99776,f23813]) ).
fof(f99946,plain,
( m2_relset_1(k5_relset_2(sK6522_skl,sK6523_skl),k1_relat_1(k5_relset_2(sK6522_skl,sK6523_skl)),k1_zfmisc_1(k2_relat_1(sK6523_skl)))
| ~ v1_relat_1(k5_relset_2(sK6522_skl,sK6523_skl)) ),
inference(resolution,[status(thm)],[f99776,f22468]) ).
fof(f99949,plain,
( v1_funct_2(k5_relset_2(sK6522_skl,sK6523_skl),k1_relat_1(k5_relset_2(sK6522_skl,sK6523_skl)),k1_zfmisc_1(k2_relat_1(sK6523_skl)))
| ~ v1_funct_1(k5_relset_2(sK6522_skl,sK6523_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f99945,f97274]) ).
fof(f99950,plain,
m2_relset_1(k5_relset_2(sK6522_skl,sK6523_skl),k1_relat_1(k5_relset_2(sK6522_skl,sK6523_skl)),k1_zfmisc_1(k2_relat_1(sK6523_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f99946,f97274]) ).
fof(f105745,plain,
v1_funct_2(k5_relset_2(sK6522_skl,sK6523_skl),k1_relat_1(k5_relset_2(sK6522_skl,sK6523_skl)),k1_zfmisc_1(k2_relat_1(sK6523_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f99949,f97272]) ).
fof(f130857,plain,
! [X0] : k1_relat_1(k5_relset_2(X0,sK6523_skl)) = k1_zfmisc_1(X0),
inference(equality_resolution,[status(thm)],[f99605]) ).
fof(f131124,plain,
m2_relset_1(k5_relset_2(sK6522_skl,sK6523_skl),k1_zfmisc_1(sK6522_skl),k1_zfmisc_1(k2_relat_1(sK6523_skl))),
inference(backward_demodulation,[status(thm)],[f130857,f99950]) ).
fof(f131125,plain,
v1_funct_2(k5_relset_2(sK6522_skl,sK6523_skl),k1_zfmisc_1(sK6522_skl),k1_zfmisc_1(k2_relat_1(sK6523_skl))),
inference(backward_demodulation,[status(thm)],[f130857,f105745]) ).
fof(f140432,plain,
~ v1_funct_2(k5_relset_2(sK6522_skl,sK6523_skl),k1_zfmisc_1(sK6522_skl),k1_zfmisc_1(k2_relat_1(sK6523_skl))),
inference(backward_subsumption_resolution,[status(thm)],[f97275,f131124]) ).
fof(f140637,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f131125,f140432]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU425+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:27:24 UTC 2026
% 0.09/0.36 % CPUTime :
% 3.05/3.38 % Drodi V4.1.1
% 147.41/21.71 % Refutation found
% 147.41/21.71 % SZS status Theorem for theBenchmark: Theorem is valid
% 147.41/21.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.67/22.36 % Elapsed time: 21.934100 seconds
% 7.67/22.36 % CPU time: 149.061931 seconds
% 7.67/22.36 % Total memory used: 5.593 GB
% 7.67/22.36 % Net memory used: 5.515 GB
%------------------------------------------------------------------------------