%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO461+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:26:31 PM UTC 2026
% Result : Theorem 222.24s 30.22s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO461+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.39 % Computer : n026.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 20 16:28:21 UTC 2026
% 0.11/0.40 % CPUTime :
% 2.13/2.44 % Drodi V4.1.1
% 222.24/30.22 % Refutation found
% 222.24/30.22 % SZS status Theorem for theBenchmark: Theorem is valid
% 222.24/30.22 % SZS output start CNFRefutation for theBenchmark
% 222.24/30.22 fof(f200,axiom,(
% 222.24/30.22 (! [N0] : s(num,i(s(fun(num,num),numeral),s(num,N0))) = s(num,N0) )),
% 222.24/30.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 222.24/30.22 fof(f2763,axiom,(
% 222.24/30.22 (! [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))))) )),
% 222.24/30.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 222.24/30.22 fof(f2817,axiom,(
% 222.24/30.22 (! [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))))) )),
% 222.24/30.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 222.24/30.22 fof(f2891,axiom,(
% 222.24/30.22 (! [Q104680,X,Y] : s(real,i(s(fun(prod(cart(real,Q104680),cart(real,Q104680)),real),distance),s(prod(cart(real,Q104680),cart(real,Q104680)),i(s(fun(cart(real,Q104680),prod(cart(real,Q104680),cart(real,Q104680))),i(s(fun(cart(real,Q104680),fun(cart(real,Q104680),prod(cart(real,Q104680),cart(real,Q104680)))),c_),s(cart(real,Q104680),X))),s(cart(real,Q104680),Y))))) = s(real,i(s(fun(prod(cart(real,Q104680),cart(real,Q104680)),real),distance),s(prod(cart(real,Q104680),cart(real,Q104680)),i(s(fun(cart(real,Q104680),prod(cart(real,Q104680),cart(real,Q104680))),i(s(fun(cart(real,Q104680),fun(cart(real,Q104680),prod(cart(real,Q104680),cart(real,Q104680)))),c_),s(cart(real,Q104680),Y))),s(cart(real,Q104680),X))))) )),
% 222.24/30.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 222.24/30.22 fof(f3279,axiom,(
% 222.24/30.22 (! [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))))) )),
% 222.24/30.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 222.24/30.22 fof(f3291,axiom,(
% 222.24/30.22 (! [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))) )),
% 222.24/30.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 222.24/30.22 fof(f3293,conjecture,(
% 222.24/30.22 (! [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_))))) )),
% 222.24/30.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 222.24/30.22 fof(f3294,negated_conjecture,(
% 222.24/30.22 ~((! [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_))))) ))),
% 222.24/30.22 inference(negated_conjecture,[status(cth)],[f3293])).
% 222.24/30.22 fof(f4311,plain,(
% 222.24/30.22 ![X0]: (s(num,i(s(fun(num,num),numeral),s(num,X0)))=s(num,X0))),
% 222.24/30.22 inference(cnf_transformation,[status(thm)],[f200])).
% 222.24/30.22 fof(f12927,plain,(
% 222.24/30.22 ![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))))))),
% 222.24/30.22 inference(cnf_transformation,[status(thm)],[f2763])).
% 222.24/30.22 fof(f13019,plain,(
% 222.24/30.22 ![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))))))),
% 222.24/30.22 inference(cnf_transformation,[status(thm)],[f2817])).
% 222.24/30.22 fof(f13212,plain,(
% 222.24/30.22 ![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(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),X2))),s(cart(real,X0),X1))))))),
% 222.24/30.22 inference(cnf_transformation,[status(thm)],[f2891])).
% 222.24/30.22 fof(f14352,plain,(
% 222.24/30.22 ![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))))))),
% 222.24/30.22 inference(cnf_transformation,[status(thm)],[f3279])).
% 222.24/30.22 fof(f14373,plain,(
% 222.24/30.22 ![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))))),
% 222.24/30.22 inference(cnf_transformation,[status(thm)],[f3291])).
% 222.24/30.22 fof(f14375,plain,(
% 222.24/30.22 (?[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_))))))),
% 222.24/30.22 inference(pre_NNF_transformation,[status(thm)],[f3294])).
% 222.24/30.22 fof(f14376,plain,(
% 222.24/30.22 ~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)))))),
% 222.24/30.22 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])).
% 222.24/30.22 fof(f14377,plain,(
% 222.24/30.22 ~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)))))),
% 222.24/30.22 inference(cnf_transformation,[status(thm)],[f14376])).
% 222.24/30.22 fof(f21730,plain,(
% 222.24/30.22 ![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))))),
% 222.24/30.22 inference(forward_demodulation,[status(thm)],[f4311,f12927])).
% 222.24/30.22 fof(f22094,plain,(
% 222.24/30.22 ![X0,X1,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)))))=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),X2))),s(cart(real,X0),X1))))))),
% 222.24/30.22 inference(forward_demodulation,[status(thm)],[f13019,f13212])).
% 222.24/30.22 fof(f23006,plain,(
% 222.24/30.22 ![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))))),
% 222.24/30.22 inference(forward_demodulation,[status(thm)],[f4311,f14373])).
% 222.24/30.22 fof(f23011,plain,(
% 222.24/30.22 ~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),sK3453_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),sK3452_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)))))),
% 222.24/30.22 inference(forward_demodulation,[status(thm)],[f22094,f14377])).
% 222.24/30.22 fof(f23012,plain,(
% 222.24/30.22 ~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),sK3453_skl))),s(cart(real,sK3450_skl),sK3452_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)))))),
% 222.24/30.22 inference(forward_demodulation,[status(thm)],[f14352,f23011])).
% 222.24/30.22 fof(f23013,plain,(
% 222.24/30.22 ~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),sK3453_skl))),s(cart(real,sK3450_skl),sK3452_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)))))),
% 56.69/30.73 inference(forward_demodulation,[status(thm)],[f21730,f23012])).
% 56.69/30.73 fof(f23014,plain,(
% 56.69/30.73 ~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),sK3453_skl))),s(cart(real,sK3450_skl),sK3452_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)))))),
% 56.69/30.73 inference(forward_demodulation,[status(thm)],[f23006,f23013])).
% 56.69/30.73 fof(f23015,plain,(
% 56.69/30.73 ~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),sK3453_skl))),s(cart(real,sK3450_skl),sK3452_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),sK3453_skl))),s(cart(real,sK3450_skl),sK3452_skl)))))),
% 56.69/30.73 inference(forward_demodulation,[status(thm)],[f22094,f23014])).
% 56.69/30.73 fof(f23016,plain,(
% 56.69/30.73 $false),
% 56.69/30.73 inference(trivial_equality_resolution,[status(thm)],[f23015])).
% 56.69/30.73 % SZS output end CNFRefutation for theBenchmark.p
% 56.69/30.73 % Elapsed time: 30.307196 seconds
% 56.69/30.73 % CPU time: 224.676992 seconds
% 56.69/30.73 % Total memory used: 3.650 GB
% 56.69/30.73 % Net memory used: 3.633 GB
%------------------------------------------------------------------------------