%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO462+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 2.24s 2.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO462+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 16:32:42 UTC 2026
% 0.13/0.36 % CPUTime :
% 2.06/2.37 % Drodi V4.1.1
% 2.24/2.87 % Refutation found
% 2.24/2.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.24/2.87 % SZS output start CNFRefutation for theBenchmark
% 2.24/2.87 fof(f1684,axiom,(
% 2.24/2.87 (! [A,X] : ~ p(s(bool,i(s(fun(fun(A,bool),bool),i(s(fun(A,fun(fun(A,bool),bool)),in),s(A,X))),s(fun(A,bool),empty)))) )),
% 2.24/2.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.24/2.87 fof(f3294,axiom,(
% 2.24/2.87 (! [Q121390,S0] :( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))<=> ( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))& (! [X,Y] :( ( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))& p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),Y))),s(fun(cart(real,Q121390),bool),S0)))) )=> p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(cart(real,Q121390),fun(cart(real,Q121390),cart(real,Q121390))),vectoru_add),s(cart(real,Q121390),X))),s(cart(real,Q121390),Y))))),s(fun(cart(real,Q121390),bool),S0)))) ))& (! [C0,X] :( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))=> p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0)))) ) )) ) )),
% 2.24/2.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.24/2.87 fof(f3299,conjecture,(
% 2.24/2.87 (! [Q121443,S0] :( p(s(bool,i(s(fun(fun(cart(real,Q121443),bool),bool),subspace),s(fun(cart(real,Q121443),bool),S0))))=> s(fun(cart(real,Q121443),bool),S0) != s(fun(cart(real,Q121443),bool),empty) ) )),
% 2.24/2.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.24/2.87 fof(f3300,negated_conjecture,(
% 2.24/2.87 ~((! [Q121443,S0] :( p(s(bool,i(s(fun(fun(cart(real,Q121443),bool),bool),subspace),s(fun(cart(real,Q121443),bool),S0))))=> s(fun(cart(real,Q121443),bool),S0) != s(fun(cart(real,Q121443),bool),empty) ) ))),
% 2.24/2.87 inference(negated_conjecture,[status(cth)],[f3299])).
% 2.24/2.87 fof(f8053,plain,(
% 2.24/2.87 ![X0,X1]: (~p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(X0,fun(fun(X0,bool),bool)),in),s(X0,X1))),s(fun(X0,bool),empty)))))),
% 2.24/2.87 inference(cnf_transformation,[status(thm)],[f1684])).
% 2.24/2.87 fof(f14382,plain,(
% 2.24/2.87 ![Q121390,S0]: (p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))<=>((p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))&(![X,Y]: ((~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))|~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),Y))),s(fun(cart(real,Q121390),bool),S0)))))|p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(cart(real,Q121390),fun(cart(real,Q121390),cart(real,Q121390))),vectoru_add),s(cart(real,Q121390),X))),s(cart(real,Q121390),Y))))),s(fun(cart(real,Q121390),bool),S0)))))))&(![C0,X]: (~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))|p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))))))),
% 2.24/2.87 inference(pre_NNF_transformation,[status(thm)],[f3294])).
% 2.24/2.87 fof(f14383,definition,(
% 2.24/2.87 ![Q121390,S0,X,Y]: (sP256_prd(Y,X,S0,Q121390)<=>((~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))|~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),Y))),s(fun(cart(real,Q121390),bool),S0)))))|p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(cart(real,Q121390),fun(cart(real,Q121390),cart(real,Q121390))),vectoru_add),s(cart(real,Q121390),X))),s(cart(real,Q121390),Y))))),s(fun(cart(real,Q121390),bool),S0))))))),
% 2.24/2.87 introduced(definition,[new_symbols(definition,[sP256_prd])],[])).
% 2.24/2.87 fof(f14384,plain,(
% 2.24/2.87 ![Q121390,S0]: (p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))<=>((p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))&(![X,Y]: sP256_prd(Y,X,S0,Q121390)))&(![C0,X]: (~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))|p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))))))),
% 2.24/2.87 inference(formula_renaming,[status(thm)],[f14382,f14383])).
% 2.24/2.87 fof(f14385,plain,(
% 2.24/2.87 ![Q121390,S0]: ((~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))|((p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))&(![X,Y]: sP256_prd(Y,X,S0,Q121390)))&(![C0,X]: (~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))|p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))))))&(p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))|((~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))|(?[X,Y]: ~sP256_prd(Y,X,S0,Q121390)))|(?[C0,X]: (p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))&~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0)))))))))),
% 2.24/2.87 inference(NNF_transformation,[status(thm)],[f14384])).
% 2.24/2.87 fof(f14386,plain,(
% 2.24/2.87 (![Q121390,S0]: (~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))|((p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))&(![X,Y]: sP256_prd(Y,X,S0,Q121390)))&(![X]: (~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))|(![C0]: p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))))))))&(![Q121390,S0]: (p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))|((~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))|(?[X,Y]: ~sP256_prd(Y,X,S0,Q121390)))|(?[X]: (p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))&(?[C0]: ~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))))))))),
% 2.24/2.87 inference(miniscoping,[status(thm)],[f14385])).
% 2.24/2.87 fof(f14387,plain,(
% 2.24/2.87 (![Q121390,S0]: (~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))|((p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))&(![X,Y]: sP256_prd(Y,X,S0,Q121390)))&(![X]: (~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))|(![C0]: p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))))))))&(![Q121390,S0]: (p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))|((~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))|~sP256_prd(sK3450_skl(S0,Q121390),sK3449_skl(S0,Q121390),S0,Q121390))|(p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),sK3451_skl(S0,Q121390)))),s(fun(cart(real,Q121390),bool),S0))))&~p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,sK3452_skl(S0,Q121390)))),s(cart(real,Q121390),sK3451_skl(S0,Q121390)))))),s(fun(cart(real,Q121390),bool),S0))))))))),
% 2.25/3.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK3449_skl,sK3450_skl,sK3451_skl,sK3452_skl]),skolemize(X,sK3449_skl(S0,Q121390)),skolemize(Y,sK3450_skl(S0,Q121390)),skolemize(X,sK3451_skl(S0,Q121390)),skolemize(C0,sK3452_skl(S0,Q121390))],[f14386])).
% 2.25/3.00 fof(f14388,plain,(
% 2.25/3.00 ![X0,X1]: (~p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),subspace),s(fun(cart(real,X0),bool),X1))))|p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),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(fun(cart(real,X0),bool),X1)))))),
% 2.25/3.00 inference(cnf_transformation,[status(thm)],[f14387])).
% 2.25/3.00 fof(f14405,plain,(
% 2.25/3.00 (?[Q121443,S0]: (p(s(bool,i(s(fun(fun(cart(real,Q121443),bool),bool),subspace),s(fun(cart(real,Q121443),bool),S0))))&s(fun(cart(real,Q121443),bool),S0)=s(fun(cart(real,Q121443),bool),empty)))),
% 2.25/3.00 inference(pre_NNF_transformation,[status(thm)],[f3300])).
% 2.25/3.00 fof(f14406,plain,(
% 2.25/3.00 (p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),subspace),s(fun(cart(real,sK3454_skl),bool),sK3455_skl))))&s(fun(cart(real,sK3454_skl),bool),sK3455_skl)=s(fun(cart(real,sK3454_skl),bool),empty))),
% 2.25/3.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK3454_skl,sK3455_skl]),skolemize(Q121443,sK3454_skl),skolemize(S0,sK3455_skl)],[f14405])).
% 2.25/3.00 fof(f14407,plain,(
% 2.25/3.00 p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),subspace),s(fun(cart(real,sK3454_skl),bool),sK3455_skl))))),
% 2.25/3.00 inference(cnf_transformation,[status(thm)],[f14406])).
% 2.25/3.00 fof(f14408,plain,(
% 2.25/3.00 s(fun(cart(real,sK3454_skl),bool),sK3455_skl)=s(fun(cart(real,sK3454_skl),bool),empty)),
% 2.25/3.00 inference(cnf_transformation,[status(thm)],[f14406])).
% 2.25/3.00 fof(f17020,plain,(
% 2.25/3.00 ![X0]: (~p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(cart(real,sK3454_skl),fun(fun(cart(real,sK3454_skl),bool),bool)),in),s(cart(real,sK3454_skl),X0))),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))))),
% 2.25/3.00 inference(paramodulation,[status(thm)],[f14408,f8053])).
% 2.25/3.00 fof(f17362,plain,(
% 2.25/3.00 p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(cart(real,sK3454_skl),fun(fun(cart(real,sK3454_skl),bool),bool)),in),s(cart(real,sK3454_skl),i(s(fun(num,cart(real,sK3454_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,sK3454_skl),bool),sK3455_skl))))),
% 2.25/3.00 inference(resolution,[status(thm)],[f14388,f14407])).
% 2.25/3.00 fof(f17366,plain,(
% 2.25/3.00 $false),
% 2.25/3.00 inference(forward_subsumption_resolution,[status(thm)],[f17362,f17020])).
% 2.25/3.00 % SZS output end CNFRefutation for theBenchmark.p
% 2.25/3.07 % Elapsed time: 2.671729 seconds
% 2.25/3.07 % CPU time: 6.034378 seconds
% 2.25/3.07 % Total memory used: 1.457 GB
% 2.25/3.07 % Net memory used: 1.453 GB
%------------------------------------------------------------------------------