%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO443+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 : n004.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:30 PM UTC 2026
% Result : Theorem 170.48s 22.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO443+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.36 % Computer : n004.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 16:16:34 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.81/1.11 % Drodi V4.1.1
% 170.48/22.62 % Refutation found
% 170.48/22.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 170.48/22.62 % SZS output start CNFRefutation for theBenchmark
% 170.48/22.62 fof(f2817,axiom,(
% 170.48/22.62 (! [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))))) )),
% 170.48/22.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 170.48/22.62 fof(f2848,axiom,(
% 170.48/22.62 (! [Q102210,X,Y] : s(real,i(s(fun(cart(real,Q102210),real),vectoru_norm),s(cart(real,Q102210),i(s(fun(cart(real,Q102210),cart(real,Q102210)),i(s(fun(cart(real,Q102210),fun(cart(real,Q102210),cart(real,Q102210))),vectoru_sub),s(cart(real,Q102210),X))),s(cart(real,Q102210),Y))))) = s(real,i(s(fun(cart(real,Q102210),real),vectoru_norm),s(cart(real,Q102210),i(s(fun(cart(real,Q102210),cart(real,Q102210)),i(s(fun(cart(real,Q102210),fun(cart(real,Q102210),cart(real,Q102210))),vectoru_sub),s(cart(real,Q102210),Y))),s(cart(real,Q102210),X))))) )),
% 170.48/22.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 170.48/22.62 fof(f2891,conjecture,(
% 170.48/22.62 (! [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))))) )),
% 170.48/22.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 170.48/22.62 fof(f2892,negated_conjecture,(
% 170.48/22.62 ~((! [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))))) ))),
% 170.48/22.62 inference(negated_conjecture,[status(cth)],[f2891])).
% 170.48/22.62 fof(f12617,plain,(
% 170.48/22.62 ![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))))))),
% 170.48/22.62 inference(cnf_transformation,[status(thm)],[f2817])).
% 170.48/22.62 fof(f12692,plain,(
% 170.48/22.62 ![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(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),X2))),s(cart(real,X0),X1))))))),
% 170.48/22.62 inference(cnf_transformation,[status(thm)],[f2848])).
% 170.48/22.62 fof(f12810,plain,(
% 170.48/22.62 (?[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))))))),
% 170.48/22.62 inference(pre_NNF_transformation,[status(thm)],[f2892])).
% 170.48/22.62 fof(f12811,plain,(
% 170.48/22.62 ~s(real,i(s(fun(prod(cart(real,sK2957_skl),cart(real,sK2957_skl)),real),distance),s(prod(cart(real,sK2957_skl),cart(real,sK2957_skl)),i(s(fun(cart(real,sK2957_skl),prod(cart(real,sK2957_skl),cart(real,sK2957_skl))),i(s(fun(cart(real,sK2957_skl),fun(cart(real,sK2957_skl),prod(cart(real,sK2957_skl),cart(real,sK2957_skl)))),c_),s(cart(real,sK2957_skl),sK2958_skl))),s(cart(real,sK2957_skl),sK2959_skl)))))=s(real,i(s(fun(prod(cart(real,sK2957_skl),cart(real,sK2957_skl)),real),distance),s(prod(cart(real,sK2957_skl),cart(real,sK2957_skl)),i(s(fun(cart(real,sK2957_skl),prod(cart(real,sK2957_skl),cart(real,sK2957_skl))),i(s(fun(cart(real,sK2957_skl),fun(cart(real,sK2957_skl),prod(cart(real,sK2957_skl),cart(real,sK2957_skl)))),c_),s(cart(real,sK2957_skl),sK2959_skl))),s(cart(real,sK2957_skl),sK2958_skl)))))),
% 170.48/22.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK2957_skl,sK2958_skl,sK2959_skl]),skolemize(Q104680,sK2957_skl),skolemize(X,sK2958_skl),skolemize(Y,sK2959_skl)],[f12810])).
% 170.48/22.62 fof(f12812,plain,(
% 170.48/22.62 ~s(real,i(s(fun(prod(cart(real,sK2957_skl),cart(real,sK2957_skl)),real),distance),s(prod(cart(real,sK2957_skl),cart(real,sK2957_skl)),i(s(fun(cart(real,sK2957_skl),prod(cart(real,sK2957_skl),cart(real,sK2957_skl))),i(s(fun(cart(real,sK2957_skl),fun(cart(real,sK2957_skl),prod(cart(real,sK2957_skl),cart(real,sK2957_skl)))),c_),s(cart(real,sK2957_skl),sK2958_skl))),s(cart(real,sK2957_skl),sK2959_skl)))))=s(real,i(s(fun(prod(cart(real,sK2957_skl),cart(real,sK2957_skl)),real),distance),s(prod(cart(real,sK2957_skl),cart(real,sK2957_skl)),i(s(fun(cart(real,sK2957_skl),prod(cart(real,sK2957_skl),cart(real,sK2957_skl))),i(s(fun(cart(real,sK2957_skl),fun(cart(real,sK2957_skl),prod(cart(real,sK2957_skl),cart(real,sK2957_skl)))),c_),s(cart(real,sK2957_skl),sK2959_skl))),s(cart(real,sK2957_skl),sK2958_skl)))))),
% 170.48/22.62 inference(cnf_transformation,[status(thm)],[f12811])).
% 170.48/22.62 fof(f20473,plain,(
% 170.48/22.62 ~s(real,i(s(fun(cart(real,sK2957_skl),real),vectoru_norm),s(cart(real,sK2957_skl),i(s(fun(cart(real,sK2957_skl),cart(real,sK2957_skl)),i(s(fun(cart(real,sK2957_skl),fun(cart(real,sK2957_skl),cart(real,sK2957_skl))),vectoru_sub),s(cart(real,sK2957_skl),sK2958_skl))),s(cart(real,sK2957_skl),sK2959_skl)))))=s(real,i(s(fun(prod(cart(real,sK2957_skl),cart(real,sK2957_skl)),real),distance),s(prod(cart(real,sK2957_skl),cart(real,sK2957_skl)),i(s(fun(cart(real,sK2957_skl),prod(cart(real,sK2957_skl),cart(real,sK2957_skl))),i(s(fun(cart(real,sK2957_skl),fun(cart(real,sK2957_skl),prod(cart(real,sK2957_skl),cart(real,sK2957_skl)))),c_),s(cart(real,sK2957_skl),sK2959_skl))),s(cart(real,sK2957_skl),sK2958_skl)))))),
% 170.48/22.62 inference(forward_demodulation,[status(thm)],[f12617,f12812])).
% 170.48/22.62 fof(f20474,plain,(
% 170.48/22.62 ~s(real,i(s(fun(cart(real,sK2957_skl),real),vectoru_norm),s(cart(real,sK2957_skl),i(s(fun(cart(real,sK2957_skl),cart(real,sK2957_skl)),i(s(fun(cart(real,sK2957_skl),fun(cart(real,sK2957_skl),cart(real,sK2957_skl))),vectoru_sub),s(cart(real,sK2957_skl),sK2958_skl))),s(cart(real,sK2957_skl),sK2959_skl)))))=s(real,i(s(fun(cart(real,sK2957_skl),real),vectoru_norm),s(cart(real,sK2957_skl),i(s(fun(cart(real,sK2957_skl),cart(real,sK2957_skl)),i(s(fun(cart(real,sK2957_skl),fun(cart(real,sK2957_skl),cart(real,sK2957_skl))),vectoru_sub),s(cart(real,sK2957_skl),sK2959_skl))),s(cart(real,sK2957_skl),sK2958_skl)))))),
% 55.86/22.89 inference(forward_demodulation,[status(thm)],[f12617,f20473])).
% 55.86/22.89 fof(f20475,plain,(
% 55.86/22.89 $false),
% 55.86/22.89 inference(forward_subsumption_resolution,[status(thm)],[f20474,f12692])).
% 55.86/22.89 % SZS output end CNFRefutation for theBenchmark.p
% 11.66/22.98 % Elapsed time: 22.589604 seconds
% 11.66/22.98 % CPU time: 172.970145 seconds
% 11.66/22.98 % Total memory used: 2.479 GB
% 11.66/22.98 % Net memory used: 2.463 GB
%------------------------------------------------------------------------------