%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO461+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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 12:25:05 PM UTC 2026
% Result : Theorem 211.65s 28.96s
% Output : CNFRefutation 180.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 23 ( 23 unt; 0 def)
% Number of atoms : 23 ( 22 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 9 ( 9 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 15 con; 0-2 aty)
% Number of variables : 50 ( 45 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f200,axiom,
! [N0] : s(num,i(s(fun(num,num),numeral),s(num,N0))) = s(num,N0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2763,axiom,
! [Q99591,X] : s(cart(real,Q99591),i(s(fun(cart(real,Q99591),cart(real,Q99591)),i(s(fun(cart(real,Q99591),fun(cart(real,Q99591),cart(real,Q99591))),vectoru_sub),s(cart(real,Q99591),X))),s(cart(real,Q99591),X))) = s(cart(real,Q99591),i(s(fun(num,cart(real,Q99591)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2817,axiom,
! [Q100698,X,Y] : s(real,i(s(fun(prod(cart(real,Q100698),cart(real,Q100698)),real),distance),s(prod(cart(real,Q100698),cart(real,Q100698)),i(s(fun(cart(real,Q100698),prod(cart(real,Q100698),cart(real,Q100698))),i(s(fun(cart(real,Q100698),fun(cart(real,Q100698),prod(cart(real,Q100698),cart(real,Q100698)))),c_),s(cart(real,Q100698),X))),s(cart(real,Q100698),Y))))) = s(real,i(s(fun(cart(real,Q100698),real),vectoru_norm),s(cart(real,Q100698),i(s(fun(cart(real,Q100698),cart(real,Q100698)),i(s(fun(cart(real,Q100698),fun(cart(real,Q100698),cart(real,Q100698))),vectoru_sub),s(cart(real,Q100698),X))),s(cart(real,Q100698),Y))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3279,axiom,
! [M,N,X1,Y1,X2,Y2] : s(cart(real,finite_sum(M,N)),i(s(fun(cart(real,finite_sum(M,N)),cart(real,finite_sum(M,N))),i(s(fun(cart(real,finite_sum(M,N)),fun(cart(real,finite_sum(M,N)),cart(real,finite_sum(M,N)))),vectoru_sub),s(cart(real,finite_sum(M,N)),i(s(fun(cart(real,N),cart(real,finite_sum(M,N))),i(s(fun(cart(real,M),fun(cart(real,N),cart(real,finite_sum(M,N)))),pastecart),s(cart(real,M),X1))),s(cart(real,N),Y1))))),s(cart(real,finite_sum(M,N)),i(s(fun(cart(real,N),cart(real,finite_sum(M,N))),i(s(fun(cart(real,M),fun(cart(real,N),cart(real,finite_sum(M,N)))),pastecart),s(cart(real,M),X2))),s(cart(real,N),Y2))))) = s(cart(real,finite_sum(M,N)),i(s(fun(cart(real,N),cart(real,finite_sum(M,N))),i(s(fun(cart(real,M),fun(cart(real,N),cart(real,finite_sum(M,N)))),pastecart),s(cart(real,M),i(s(fun(cart(real,M),cart(real,M)),i(s(fun(cart(real,M),fun(cart(real,M),cart(real,M))),vectoru_sub),s(cart(real,M),X1))),s(cart(real,M),X2))))),s(cart(real,N),i(s(fun(cart(real,N),cart(real,N)),i(s(fun(cart(real,N),fun(cart(real,N),cart(real,N))),vectoru_sub),s(cart(real,N),Y1))),s(cart(real,N),Y2))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3291,axiom,
! [Q121236,Q121234,Y] : s(real,i(s(fun(cart(real,finite_sum(Q121236,Q121234)),real),vectoru_norm),s(cart(real,finite_sum(Q121236,Q121234)),i(s(fun(cart(real,Q121234),cart(real,finite_sum(Q121236,Q121234))),i(s(fun(cart(real,Q121236),fun(cart(real,Q121234),cart(real,finite_sum(Q121236,Q121234)))),pastecart),s(cart(real,Q121236),i(s(fun(num,cart(real,Q121236)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(cart(real,Q121234),Y))))) = s(real,i(s(fun(cart(real,Q121234),real),vectoru_norm),s(cart(real,Q121234),Y))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3293,conjecture,
! [Q121316,Q121317,X,Y,YI_] : s(real,i(s(fun(prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317))),real),distance),s(prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317))),i(s(fun(cart(real,finite_sum(Q121316,Q121317)),prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317)))),i(s(fun(cart(real,finite_sum(Q121316,Q121317)),fun(cart(real,finite_sum(Q121316,Q121317)),prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317))))),c_),s(cart(real,finite_sum(Q121316,Q121317)),i(s(fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317))),i(s(fun(cart(real,Q121316),fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317)))),pastecart),s(cart(real,Q121316),X))),s(cart(real,Q121317),Y))))),s(cart(real,finite_sum(Q121316,Q121317)),i(s(fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317))),i(s(fun(cart(real,Q121316),fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317)))),pastecart),s(cart(real,Q121316),X))),s(cart(real,Q121317),YI_))))))) = s(real,i(s(fun(prod(cart(real,Q121317),cart(real,Q121317)),real),distance),s(prod(cart(real,Q121317),cart(real,Q121317)),i(s(fun(cart(real,Q121317),prod(cart(real,Q121317),cart(real,Q121317))),i(s(fun(cart(real,Q121317),fun(cart(real,Q121317),prod(cart(real,Q121317),cart(real,Q121317)))),c_),s(cart(real,Q121317),Y))),s(cart(real,Q121317),YI_))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3294,negated_conjecture,
~ ! [Q121316,Q121317,X,Y,YI_] : s(real,i(s(fun(prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317))),real),distance),s(prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317))),i(s(fun(cart(real,finite_sum(Q121316,Q121317)),prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317)))),i(s(fun(cart(real,finite_sum(Q121316,Q121317)),fun(cart(real,finite_sum(Q121316,Q121317)),prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317))))),c_),s(cart(real,finite_sum(Q121316,Q121317)),i(s(fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317))),i(s(fun(cart(real,Q121316),fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317)))),pastecart),s(cart(real,Q121316),X))),s(cart(real,Q121317),Y))))),s(cart(real,finite_sum(Q121316,Q121317)),i(s(fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317))),i(s(fun(cart(real,Q121316),fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317)))),pastecart),s(cart(real,Q121316),X))),s(cart(real,Q121317),YI_))))))) = s(real,i(s(fun(prod(cart(real,Q121317),cart(real,Q121317)),real),distance),s(prod(cart(real,Q121317),cart(real,Q121317)),i(s(fun(cart(real,Q121317),prod(cart(real,Q121317),cart(real,Q121317))),i(s(fun(cart(real,Q121317),fun(cart(real,Q121317),prod(cart(real,Q121317),cart(real,Q121317)))),c_),s(cart(real,Q121317),Y))),s(cart(real,Q121317),YI_))))),
inference(negated_conjecture,[status(cth)],[f3293]) ).
fof(f4311,plain,
! [X0] : s(num,i(s(fun(num,num),numeral),s(num,X0))) = s(num,X0),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f12927,plain,
! [X0,X1] : s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X1))) = s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))),
inference(cnf_transformation,[status(thm)],[f2763]) ).
fof(f13019,plain,
! [X0,X1,X2] : s(real,i(s(fun(prod(cart(real,X0),cart(real,X0)),real),distance),s(prod(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),prod(cart(real,X0),cart(real,X0))),i(s(fun(cart(real,X0),fun(cart(real,X0),prod(cart(real,X0),cart(real,X0)))),c_),s(cart(real,X0),X1))),s(cart(real,X0),X2))))) = s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X2))))),
inference(cnf_transformation,[status(thm)],[f2817]) ).
fof(f14352,plain,
! [X0,X1,X2,X3,X4,X5] : s(cart(real,finite_sum(X0,X1)),i(s(fun(cart(real,finite_sum(X0,X1)),cart(real,finite_sum(X0,X1))),i(s(fun(cart(real,finite_sum(X0,X1)),fun(cart(real,finite_sum(X0,X1)),cart(real,finite_sum(X0,X1)))),vectoru_sub),s(cart(real,finite_sum(X0,X1)),i(s(fun(cart(real,X1),cart(real,finite_sum(X0,X1))),i(s(fun(cart(real,X0),fun(cart(real,X1),cart(real,finite_sum(X0,X1)))),pastecart),s(cart(real,X0),X2))),s(cart(real,X1),X3))))),s(cart(real,finite_sum(X0,X1)),i(s(fun(cart(real,X1),cart(real,finite_sum(X0,X1))),i(s(fun(cart(real,X0),fun(cart(real,X1),cart(real,finite_sum(X0,X1)))),pastecart),s(cart(real,X0),X4))),s(cart(real,X1),X5))))) = s(cart(real,finite_sum(X0,X1)),i(s(fun(cart(real,X1),cart(real,finite_sum(X0,X1))),i(s(fun(cart(real,X0),fun(cart(real,X1),cart(real,finite_sum(X0,X1)))),pastecart),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X2))),s(cart(real,X0),X4))))),s(cart(real,X1),i(s(fun(cart(real,X1),cart(real,X1)),i(s(fun(cart(real,X1),fun(cart(real,X1),cart(real,X1))),vectoru_sub),s(cart(real,X1),X3))),s(cart(real,X1),X5))))),
inference(cnf_transformation,[status(thm)],[f3279]) ).
fof(f14373,plain,
! [X0,X1,X2] : s(real,i(s(fun(cart(real,finite_sum(X0,X1)),real),vectoru_norm),s(cart(real,finite_sum(X0,X1)),i(s(fun(cart(real,X1),cart(real,finite_sum(X0,X1))),i(s(fun(cart(real,X0),fun(cart(real,X1),cart(real,finite_sum(X0,X1)))),pastecart),s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(cart(real,X1),X2))))) = s(real,i(s(fun(cart(real,X1),real),vectoru_norm),s(cart(real,X1),X2))),
inference(cnf_transformation,[status(thm)],[f3291]) ).
fof(f14375,plain,
? [Q121316,Q121317,X,Y,YI_] : s(real,i(s(fun(prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317))),real),distance),s(prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317))),i(s(fun(cart(real,finite_sum(Q121316,Q121317)),prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317)))),i(s(fun(cart(real,finite_sum(Q121316,Q121317)),fun(cart(real,finite_sum(Q121316,Q121317)),prod(cart(real,finite_sum(Q121316,Q121317)),cart(real,finite_sum(Q121316,Q121317))))),c_),s(cart(real,finite_sum(Q121316,Q121317)),i(s(fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317))),i(s(fun(cart(real,Q121316),fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317)))),pastecart),s(cart(real,Q121316),X))),s(cart(real,Q121317),Y))))),s(cart(real,finite_sum(Q121316,Q121317)),i(s(fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317))),i(s(fun(cart(real,Q121316),fun(cart(real,Q121317),cart(real,finite_sum(Q121316,Q121317)))),pastecart),s(cart(real,Q121316),X))),s(cart(real,Q121317),YI_))))))) != s(real,i(s(fun(prod(cart(real,Q121317),cart(real,Q121317)),real),distance),s(prod(cart(real,Q121317),cart(real,Q121317)),i(s(fun(cart(real,Q121317),prod(cart(real,Q121317),cart(real,Q121317))),i(s(fun(cart(real,Q121317),fun(cart(real,Q121317),prod(cart(real,Q121317),cart(real,Q121317)))),c_),s(cart(real,Q121317),Y))),s(cart(real,Q121317),YI_))))),
inference(pre_NNF_transformation,[status(thm)],[f3294]) ).
fof(f14376,plain,
s(real,i(s(fun(prod(cart(real,finite_sum(sK3449_skl,sK3450_skl)),cart(real,finite_sum(sK3449_skl,sK3450_skl))),real),distance),s(prod(cart(real,finite_sum(sK3449_skl,sK3450_skl)),cart(real,finite_sum(sK3449_skl,sK3450_skl))),i(s(fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),prod(cart(real,finite_sum(sK3449_skl,sK3450_skl)),cart(real,finite_sum(sK3449_skl,sK3450_skl)))),i(s(fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),prod(cart(real,finite_sum(sK3449_skl,sK3450_skl)),cart(real,finite_sum(sK3449_skl,sK3450_skl))))),c_),s(cart(real,finite_sum(sK3449_skl,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl))),i(s(fun(cart(real,sK3449_skl),fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl)))),pastecart),s(cart(real,sK3449_skl),sK3451_skl))),s(cart(real,sK3450_skl),sK3452_skl))))),s(cart(real,finite_sum(sK3449_skl,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl))),i(s(fun(cart(real,sK3449_skl),fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl)))),pastecart),s(cart(real,sK3449_skl),sK3451_skl))),s(cart(real,sK3450_skl),sK3453_skl))))))) != s(real,i(s(fun(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),real),distance),s(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl))),i(s(fun(cart(real,sK3450_skl),fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl)))),c_),s(cart(real,sK3450_skl),sK3452_skl))),s(cart(real,sK3450_skl),sK3453_skl))))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3449_skl,sK3450_skl,sK3451_skl,sK3452_skl,sK3453_skl]),skolemize(Q121316,sK3449_skl),skolemize(Q121317,sK3450_skl),skolemize(X,sK3451_skl),skolemize(Y,sK3452_skl),skolemize(YI_,sK3453_skl)],[f14375]) ).
fof(f14377,plain,
s(real,i(s(fun(prod(cart(real,finite_sum(sK3449_skl,sK3450_skl)),cart(real,finite_sum(sK3449_skl,sK3450_skl))),real),distance),s(prod(cart(real,finite_sum(sK3449_skl,sK3450_skl)),cart(real,finite_sum(sK3449_skl,sK3450_skl))),i(s(fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),prod(cart(real,finite_sum(sK3449_skl,sK3450_skl)),cart(real,finite_sum(sK3449_skl,sK3450_skl)))),i(s(fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),prod(cart(real,finite_sum(sK3449_skl,sK3450_skl)),cart(real,finite_sum(sK3449_skl,sK3450_skl))))),c_),s(cart(real,finite_sum(sK3449_skl,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl))),i(s(fun(cart(real,sK3449_skl),fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl)))),pastecart),s(cart(real,sK3449_skl),sK3451_skl))),s(cart(real,sK3450_skl),sK3452_skl))))),s(cart(real,finite_sum(sK3449_skl,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl))),i(s(fun(cart(real,sK3449_skl),fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl)))),pastecart),s(cart(real,sK3449_skl),sK3451_skl))),s(cart(real,sK3450_skl),sK3453_skl))))))) != s(real,i(s(fun(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),real),distance),s(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl))),i(s(fun(cart(real,sK3450_skl),fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl)))),c_),s(cart(real,sK3450_skl),sK3452_skl))),s(cart(real,sK3450_skl),sK3453_skl))))),
inference(cnf_transformation,[status(thm)],[f14376]) ).
fof(f21856,plain,
! [X0,X1] : s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X1))) = s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,u_0))),
inference(forward_demodulation,[status(thm)],[f4311,f12927]) ).
fof(f22704,plain,
! [X0,X1,X2] : s(real,i(s(fun(cart(real,finite_sum(X0,X1)),real),vectoru_norm),s(cart(real,finite_sum(X0,X1)),i(s(fun(cart(real,X1),cart(real,finite_sum(X0,X1))),i(s(fun(cart(real,X0),fun(cart(real,X1),cart(real,finite_sum(X0,X1)))),pastecart),s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,u_0))))),s(cart(real,X1),X2))))) = s(real,i(s(fun(cart(real,X1),real),vectoru_norm),s(cart(real,X1),X2))),
inference(forward_demodulation,[status(thm)],[f4311,f14373]) ).
fof(f22709,plain,
s(real,i(s(fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),real),vectoru_norm),s(cart(real,finite_sum(sK3449_skl,sK3450_skl)),i(s(fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),cart(real,finite_sum(sK3449_skl,sK3450_skl))),i(s(fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),cart(real,finite_sum(sK3449_skl,sK3450_skl)))),vectoru_sub),s(cart(real,finite_sum(sK3449_skl,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl))),i(s(fun(cart(real,sK3449_skl),fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl)))),pastecart),s(cart(real,sK3449_skl),sK3451_skl))),s(cart(real,sK3450_skl),sK3452_skl))))),s(cart(real,finite_sum(sK3449_skl,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl))),i(s(fun(cart(real,sK3449_skl),fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl)))),pastecart),s(cart(real,sK3449_skl),sK3451_skl))),s(cart(real,sK3450_skl),sK3453_skl))))))) != s(real,i(s(fun(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),real),distance),s(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl))),i(s(fun(cart(real,sK3450_skl),fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl)))),c_),s(cart(real,sK3450_skl),sK3452_skl))),s(cart(real,sK3450_skl),sK3453_skl))))),
inference(forward_demodulation,[status(thm)],[f13019,f14377]) ).
fof(f22710,plain,
s(real,i(s(fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),real),vectoru_norm),s(cart(real,finite_sum(sK3449_skl,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl))),i(s(fun(cart(real,sK3449_skl),fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl)))),pastecart),s(cart(real,sK3449_skl),i(s(fun(cart(real,sK3449_skl),cart(real,sK3449_skl)),i(s(fun(cart(real,sK3449_skl),fun(cart(real,sK3449_skl),cart(real,sK3449_skl))),vectoru_sub),s(cart(real,sK3449_skl),sK3451_skl))),s(cart(real,sK3449_skl),sK3451_skl))))),s(cart(real,sK3450_skl),i(s(fun(cart(real,sK3450_skl),cart(real,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),fun(cart(real,sK3450_skl),cart(real,sK3450_skl))),vectoru_sub),s(cart(real,sK3450_skl),sK3452_skl))),s(cart(real,sK3450_skl),sK3453_skl))))))) != s(real,i(s(fun(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),real),distance),s(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl))),i(s(fun(cart(real,sK3450_skl),fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl)))),c_),s(cart(real,sK3450_skl),sK3452_skl))),s(cart(real,sK3450_skl),sK3453_skl))))),
inference(forward_demodulation,[status(thm)],[f14352,f22709]) ).
fof(f22711,plain,
s(real,i(s(fun(cart(real,finite_sum(sK3449_skl,sK3450_skl)),real),vectoru_norm),s(cart(real,finite_sum(sK3449_skl,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl))),i(s(fun(cart(real,sK3449_skl),fun(cart(real,sK3450_skl),cart(real,finite_sum(sK3449_skl,sK3450_skl)))),pastecart),s(cart(real,sK3449_skl),i(s(fun(num,cart(real,sK3449_skl)),vec),s(num,u_0))))),s(cart(real,sK3450_skl),i(s(fun(cart(real,sK3450_skl),cart(real,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),fun(cart(real,sK3450_skl),cart(real,sK3450_skl))),vectoru_sub),s(cart(real,sK3450_skl),sK3452_skl))),s(cart(real,sK3450_skl),sK3453_skl))))))) != s(real,i(s(fun(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),real),distance),s(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl))),i(s(fun(cart(real,sK3450_skl),fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl)))),c_),s(cart(real,sK3450_skl),sK3452_skl))),s(cart(real,sK3450_skl),sK3453_skl))))),
inference(forward_demodulation,[status(thm)],[f21856,f22710]) ).
fof(f22712,plain,
s(real,i(s(fun(cart(real,sK3450_skl),real),vectoru_norm),s(cart(real,sK3450_skl),i(s(fun(cart(real,sK3450_skl),cart(real,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),fun(cart(real,sK3450_skl),cart(real,sK3450_skl))),vectoru_sub),s(cart(real,sK3450_skl),sK3452_skl))),s(cart(real,sK3450_skl),sK3453_skl))))) != s(real,i(s(fun(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),real),distance),s(prod(cart(real,sK3450_skl),cart(real,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl))),i(s(fun(cart(real,sK3450_skl),fun(cart(real,sK3450_skl),prod(cart(real,sK3450_skl),cart(real,sK3450_skl)))),c_),s(cart(real,sK3450_skl),sK3452_skl))),s(cart(real,sK3450_skl),sK3453_skl))))),
inference(forward_demodulation,[status(thm)],[f22704,f22711]) ).
fof(f22713,plain,
s(real,i(s(fun(cart(real,sK3450_skl),real),vectoru_norm),s(cart(real,sK3450_skl),i(s(fun(cart(real,sK3450_skl),cart(real,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),fun(cart(real,sK3450_skl),cart(real,sK3450_skl))),vectoru_sub),s(cart(real,sK3450_skl),sK3452_skl))),s(cart(real,sK3450_skl),sK3453_skl))))) != s(real,i(s(fun(cart(real,sK3450_skl),real),vectoru_norm),s(cart(real,sK3450_skl),i(s(fun(cart(real,sK3450_skl),cart(real,sK3450_skl)),i(s(fun(cart(real,sK3450_skl),fun(cart(real,sK3450_skl),cart(real,sK3450_skl))),vectoru_sub),s(cart(real,sK3450_skl),sK3452_skl))),s(cart(real,sK3450_skl),sK3453_skl))))),
inference(forward_demodulation,[status(thm)],[f13019,f22712]) ).
fof(f22714,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f22713]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO461+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n002.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 16:28:02 UTC 2026
% 0.10/0.38 % CPUTime :
% 2.14/2.49 % Drodi V4.1.1
% 211.65/28.96 % Refutation found
% 211.65/28.96 % SZS status Theorem for theBenchmark: Theorem is valid
% 211.65/28.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.21/29.48 % Elapsed time: 29.059819 seconds
% 8.21/29.48 % CPU time: 213.449869 seconds
% 8.21/29.48 % Total memory used: 2.566 GB
% 8.21/29.48 % Net memory used: 2.556 GB
%------------------------------------------------------------------------------