%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEV668+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:33:09 PM UTC 2026
% Result : Theorem 35.74s 29.94s
% Output : CNFRefutation 35.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 2
% Syntax : Number of formulae : 8 ( 4 unt; 0 def)
% Number of atoms : 28 ( 7 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 25 ( 5 ~; 0 |; 10 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-5 aty)
% Number of variables : 25 ( 20 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f303,axiom,
! [Vvar__0___24Anonymous__3183,Vvar__1___24Anonymous__3184,Vvar__2___24Anonymous__3185,Vvar__3___24Anonymous__3186,Vvar__4___24Anonymous__3187] : cRedblack_2eTREES_2eE != cRedblack_2eTREES_2eT___24a5(Vvar__0___24Anonymous__3183,Vvar__1___24Anonymous__3184,Vvar__2___24Anonymous__3185,Vvar__3___24Anonymous__3186,Vvar__4___24Anonymous__3187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2821,conjecture,
! [V0__c] :
( cRedblack_2ecolor___24t(V0__c)
=> ! [V1__l] :
( cRedblack_2eTREES_2etree___24t(V1__l)
=> ! [V2__k] :
( cRedblack_2ekey___24t(V2__k)
=> ! [V3__v] :
( cV___24t(V3__v)
=> ! [V4__r] :
( cRedblack_2eTREES_2etree___24t(V4__r)
=> cRedblack_2eTREES_2eT___24a5(V0__c,V1__l,V2__k,V3__v,V4__r) != cRedblack_2eTREES_2eE ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2822,negated_conjecture,
~ ! [V0__c] :
( cRedblack_2ecolor___24t(V0__c)
=> ! [V1__l] :
( cRedblack_2eTREES_2etree___24t(V1__l)
=> ! [V2__k] :
( cRedblack_2ekey___24t(V2__k)
=> ! [V3__v] :
( cV___24t(V3__v)
=> ! [V4__r] :
( cRedblack_2eTREES_2etree___24t(V4__r)
=> cRedblack_2eTREES_2eT___24a5(V0__c,V1__l,V2__k,V3__v,V4__r) != cRedblack_2eTREES_2eE ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2821]) ).
fof(f4598,plain,
! [X0,X1,X2,X3,X4] : cRedblack_2eTREES_2eE != cRedblack_2eTREES_2eT___24a5(X0,X1,X2,X3,X4),
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f12985,plain,
? [V0__c] :
( ? [V1__l] :
( ? [V2__k] :
( ? [V3__v] :
( ? [V4__r] :
( cRedblack_2eTREES_2eT___24a5(V0__c,V1__l,V2__k,V3__v,V4__r) = cRedblack_2eTREES_2eE
& cRedblack_2eTREES_2etree___24t(V4__r) )
& cV___24t(V3__v) )
& cRedblack_2ekey___24t(V2__k) )
& cRedblack_2eTREES_2etree___24t(V1__l) )
& cRedblack_2ecolor___24t(V0__c) ),
inference(pre_NNF_transformation,[status(thm)],[f2822]) ).
fof(f12986,plain,
( cRedblack_2eTREES_2eT___24a5(sK1182_skl,sK1183_skl,sK1184_skl,sK1185_skl,sK1186_skl) = cRedblack_2eTREES_2eE
& cRedblack_2eTREES_2etree___24t(sK1186_skl)
& cV___24t(sK1185_skl)
& cRedblack_2ekey___24t(sK1184_skl)
& cRedblack_2eTREES_2etree___24t(sK1183_skl)
& cRedblack_2ecolor___24t(sK1182_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1182_skl,sK1183_skl,sK1184_skl,sK1185_skl,sK1186_skl]),skolemize(V0__c,sK1182_skl),skolemize(V1__l,sK1183_skl),skolemize(V2__k,sK1184_skl),skolemize(V3__v,sK1185_skl),skolemize(V4__r,sK1186_skl)],[f12985]) ).
fof(f12992,plain,
cRedblack_2eTREES_2eT___24a5(sK1182_skl,sK1183_skl,sK1184_skl,sK1185_skl,sK1186_skl) = cRedblack_2eTREES_2eE,
inference(cnf_transformation,[status(thm)],[f12986]) ).
fof(f30047,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f12992,f4598]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEV668+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n007.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 07:33:06 UTC 2026
% 0.19/0.45 % CPUTime :
% 28.56/28.86 % Drodi V4.1.1
% 35.74/29.94 % Refutation found
% 35.74/29.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 35.74/29.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 35.74/30.00 % Elapsed time: 29.525859 seconds
% 35.74/30.00 % CPU time: 36.090624 seconds
% 35.74/30.00 % Total memory used: 1.246 GB
% 35.74/30.00 % Net memory used: 1.238 GB
%------------------------------------------------------------------------------