%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO447+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 : 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:30 PM UTC 2026
% Result : Theorem 45.16s 7.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO447+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.08/0.37 % Computer : n018.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Sun Sep 20 16:26:58 UTC 2026
% 0.08/0.38 % CPUTime :
% 1.95/2.23 % Drodi V4.1.1
% 45.16/7.80 % Refutation found
% 45.16/7.80 % SZS status Theorem for theBenchmark: Theorem is valid
% 45.16/7.80 % SZS output start CNFRefutation for theBenchmark
% 45.16/7.80 fof(f3,axiom,(
% 45.16/7.80 p(s(bool,t)) ),
% 45.16/7.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.16/7.80 fof(f42,axiom,(
% 45.16/7.80 (! [T0] :( ( s(bool,t) = s(bool,T0)<=> p(s(bool,T0)) )& ( s(bool,T0) = s(bool,t)<=> p(s(bool,T0)) )& ( s(bool,f0) = s(bool,T0)<=> ~ p(s(bool,T0)) )& ( s(bool,T0) = s(bool,f0)<=> ~ p(s(bool,T0)) ) ) )),
% 45.16/7.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.16/7.80 fof(f43,axiom,(
% 45.16/7.80 ~ p(s(bool,f0)) ),
% 45.16/7.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.16/7.80 fof(f3007,axiom,(
% 45.16/7.80 (! [Q110681,X,Y] : s(bool,i(s(fun(cart(real,Q110681),bool),i(s(fun(cart(real,Q110681),fun(cart(real,Q110681),bool)),orthogonal),s(cart(real,Q110681),X))),s(cart(real,Q110681),Y))) = s(bool,i(s(fun(cart(real,Q110681),bool),i(s(fun(cart(real,Q110681),fun(cart(real,Q110681),bool)),orthogonal),s(cart(real,Q110681),Y))),s(cart(real,Q110681),X))) )),
% 45.16/7.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.16/7.80 fof(f3015,axiom,(
% 45.16/7.80 (! [Q111054,A5,X,Y] :( ( p(s(bool,i(s(fun(cart(real,Q111054),bool),i(s(fun(cart(real,Q111054),fun(cart(real,Q111054),bool)),orthogonal),s(cart(real,Q111054),A5))),s(cart(real,Q111054),X))))& p(s(bool,i(s(fun(cart(real,Q111054),bool),i(s(fun(cart(real,Q111054),fun(cart(real,Q111054),bool)),orthogonal),s(cart(real,Q111054),A5))),s(cart(real,Q111054),Y)))) )=> p(s(bool,i(s(fun(cart(real,Q111054),bool),i(s(fun(cart(real,Q111054),fun(cart(real,Q111054),bool)),orthogonal),s(cart(real,Q111054),A5))),s(cart(real,Q111054),i(s(fun(cart(real,Q111054),cart(real,Q111054)),i(s(fun(cart(real,Q111054),fun(cart(real,Q111054),cart(real,Q111054))),vectoru_add),s(cart(real,Q111054),X))),s(cart(real,Q111054),Y)))))) ) )),
% 45.16/7.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.16/7.80 fof(f3020,conjecture,(
% 45.16/7.80 (! [Q111057,A5,X,Y] :( ( p(s(bool,i(s(fun(cart(real,Q111057),bool),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),bool)),orthogonal),s(cart(real,Q111057),X))),s(cart(real,Q111057),A5))))& p(s(bool,i(s(fun(cart(real,Q111057),bool),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),bool)),orthogonal),s(cart(real,Q111057),Y))),s(cart(real,Q111057),A5)))) )=> p(s(bool,i(s(fun(cart(real,Q111057),bool),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),bool)),orthogonal),s(cart(real,Q111057),i(s(fun(cart(real,Q111057),cart(real,Q111057)),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),cart(real,Q111057))),vectoru_add),s(cart(real,Q111057),X))),s(cart(real,Q111057),Y))))),s(cart(real,Q111057),A5)))) ) )),
% 45.16/7.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.16/7.80 fof(f3021,negated_conjecture,(
% 45.16/7.80 ~((! [Q111057,A5,X,Y] :( ( p(s(bool,i(s(fun(cart(real,Q111057),bool),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),bool)),orthogonal),s(cart(real,Q111057),X))),s(cart(real,Q111057),A5))))& p(s(bool,i(s(fun(cart(real,Q111057),bool),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),bool)),orthogonal),s(cart(real,Q111057),Y))),s(cart(real,Q111057),A5)))) )=> p(s(bool,i(s(fun(cart(real,Q111057),bool),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),bool)),orthogonal),s(cart(real,Q111057),i(s(fun(cart(real,Q111057),cart(real,Q111057)),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),cart(real,Q111057))),vectoru_add),s(cart(real,Q111057),X))),s(cart(real,Q111057),Y))))),s(cart(real,Q111057),A5)))) ) ))),
% 45.16/7.80 inference(negated_conjecture,[status(cth)],[f3020])).
% 45.16/7.80 fof(f3024,plain,(
% 45.16/7.80 p(s(bool,t))),
% 45.16/7.80 inference(cnf_transformation,[status(thm)],[f3])).
% 45.16/7.80 fof(f3230,plain,(
% 45.16/7.80 ![T0]: (((((~s(bool,t)=s(bool,T0)|p(s(bool,T0)))&(s(bool,t)=s(bool,T0)|~p(s(bool,T0))))&((~s(bool,T0)=s(bool,t)|p(s(bool,T0)))&(s(bool,T0)=s(bool,t)|~p(s(bool,T0)))))&((~s(bool,f0)=s(bool,T0)|~p(s(bool,T0)))&(s(bool,f0)=s(bool,T0)|p(s(bool,T0)))))&((~s(bool,T0)=s(bool,f0)|~p(s(bool,T0)))&(s(bool,T0)=s(bool,f0)|p(s(bool,T0)))))),
% 45.16/7.80 inference(NNF_transformation,[status(thm)],[f42])).
% 45.16/7.80 fof(f3231,plain,(
% 45.16/7.80 ((((![T0]: (~s(bool,t)=s(bool,T0)|p(s(bool,T0))))&(![T0]: (s(bool,t)=s(bool,T0)|~p(s(bool,T0)))))&((![T0]: (~s(bool,T0)=s(bool,t)|p(s(bool,T0))))&(![T0]: (s(bool,T0)=s(bool,t)|~p(s(bool,T0))))))&((![T0]: (~s(bool,f0)=s(bool,T0)|~p(s(bool,T0))))&(![T0]: (s(bool,f0)=s(bool,T0)|p(s(bool,T0))))))&((![T0]: (~s(bool,T0)=s(bool,f0)|~p(s(bool,T0))))&(![T0]: (s(bool,T0)=s(bool,f0)|p(s(bool,T0)))))),
% 45.16/7.80 inference(miniscoping,[status(thm)],[f3230])).
% 45.16/7.80 fof(f3233,plain,(
% 45.16/7.80 ![X0]: (s(bool,t)=s(bool,X0)|~p(s(bool,X0)))),
% 45.16/7.80 inference(cnf_transformation,[status(thm)],[f3231])).
% 45.16/7.80 fof(f3237,plain,(
% 45.16/7.80 ![X0]: (s(bool,f0)=s(bool,X0)|p(s(bool,X0)))),
% 45.16/7.80 inference(cnf_transformation,[status(thm)],[f3231])).
% 45.16/7.80 fof(f3240,plain,(
% 45.16/7.80 ~p(s(bool,f0))),
% 45.16/7.80 inference(cnf_transformation,[status(thm)],[f43])).
% 45.16/7.80 fof(f13402,plain,(
% 45.16/7.80 ![X0,X1,X2]: (s(bool,i(s(fun(cart(real,X0),bool),i(s(fun(cart(real,X0),fun(cart(real,X0),bool)),orthogonal),s(cart(real,X0),X1))),s(cart(real,X0),X2)))=s(bool,i(s(fun(cart(real,X0),bool),i(s(fun(cart(real,X0),fun(cart(real,X0),bool)),orthogonal),s(cart(real,X0),X2))),s(cart(real,X0),X1))))),
% 45.16/7.80 inference(cnf_transformation,[status(thm)],[f3007])).
% 45.16/7.80 fof(f13420,plain,(
% 45.16/7.80 ![Q111054,A5,X,Y]: ((~p(s(bool,i(s(fun(cart(real,Q111054),bool),i(s(fun(cart(real,Q111054),fun(cart(real,Q111054),bool)),orthogonal),s(cart(real,Q111054),A5))),s(cart(real,Q111054),X))))|~p(s(bool,i(s(fun(cart(real,Q111054),bool),i(s(fun(cart(real,Q111054),fun(cart(real,Q111054),bool)),orthogonal),s(cart(real,Q111054),A5))),s(cart(real,Q111054),Y)))))|p(s(bool,i(s(fun(cart(real,Q111054),bool),i(s(fun(cart(real,Q111054),fun(cart(real,Q111054),bool)),orthogonal),s(cart(real,Q111054),A5))),s(cart(real,Q111054),i(s(fun(cart(real,Q111054),cart(real,Q111054)),i(s(fun(cart(real,Q111054),fun(cart(real,Q111054),cart(real,Q111054))),vectoru_add),s(cart(real,Q111054),X))),s(cart(real,Q111054),Y)))))))),
% 45.16/7.80 inference(pre_NNF_transformation,[status(thm)],[f3015])).
% 45.16/7.80 fof(f13421,plain,(
% 45.16/7.80 ![X0,X1,X2,X3]: (~p(s(bool,i(s(fun(cart(real,X0),bool),i(s(fun(cart(real,X0),fun(cart(real,X0),bool)),orthogonal),s(cart(real,X0),X1))),s(cart(real,X0),X2))))|~p(s(bool,i(s(fun(cart(real,X0),bool),i(s(fun(cart(real,X0),fun(cart(real,X0),bool)),orthogonal),s(cart(real,X0),X1))),s(cart(real,X0),X3))))|p(s(bool,i(s(fun(cart(real,X0),bool),i(s(fun(cart(real,X0),fun(cart(real,X0),bool)),orthogonal),s(cart(real,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_add),s(cart(real,X0),X2))),s(cart(real,X0),X3)))))))),
% 45.16/7.80 inference(cnf_transformation,[status(thm)],[f13420])).
% 45.16/7.80 fof(f13430,plain,(
% 45.16/7.80 (?[Q111057,A5,X,Y]: ((p(s(bool,i(s(fun(cart(real,Q111057),bool),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),bool)),orthogonal),s(cart(real,Q111057),X))),s(cart(real,Q111057),A5))))&p(s(bool,i(s(fun(cart(real,Q111057),bool),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),bool)),orthogonal),s(cart(real,Q111057),Y))),s(cart(real,Q111057),A5)))))&~p(s(bool,i(s(fun(cart(real,Q111057),bool),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),bool)),orthogonal),s(cart(real,Q111057),i(s(fun(cart(real,Q111057),cart(real,Q111057)),i(s(fun(cart(real,Q111057),fun(cart(real,Q111057),cart(real,Q111057))),vectoru_add),s(cart(real,Q111057),X))),s(cart(real,Q111057),Y))))),s(cart(real,Q111057),A5))))))),
% 45.16/7.80 inference(pre_NNF_transformation,[status(thm)],[f3021])).
% 45.16/7.80 fof(f13431,plain,(
% 45.16/7.80 ((p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3166_skl))),s(cart(real,sK3164_skl),sK3165_skl))))&p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3167_skl))),s(cart(real,sK3164_skl),sK3165_skl)))))&~p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),i(s(fun(cart(real,sK3164_skl),cart(real,sK3164_skl)),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),cart(real,sK3164_skl))),vectoru_add),s(cart(real,sK3164_skl),sK3166_skl))),s(cart(real,sK3164_skl),sK3167_skl))))),s(cart(real,sK3164_skl),sK3165_skl)))))),
% 45.16/7.80 inference(skolemize,[status(esa),new_symbols(skolem,[sK3164_skl,sK3165_skl,sK3166_skl,sK3167_skl]),skolemize(Q111057,sK3164_skl),skolemize(A5,sK3165_skl),skolemize(X,sK3166_skl),skolemize(Y,sK3167_skl)],[f13430])).
% 45.16/7.80 fof(f13432,plain,(
% 45.16/7.80 p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3166_skl))),s(cart(real,sK3164_skl),sK3165_skl))))),
% 45.16/7.80 inference(cnf_transformation,[status(thm)],[f13431])).
% 45.16/7.80 fof(f13433,plain,(
% 45.16/7.80 p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3167_skl))),s(cart(real,sK3164_skl),sK3165_skl))))),
% 45.16/7.80 inference(cnf_transformation,[status(thm)],[f13431])).
% 45.16/7.80 fof(f13434,plain,(
% 45.16/7.80 ~p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),i(s(fun(cart(real,sK3164_skl),cart(real,sK3164_skl)),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),cart(real,sK3164_skl))),vectoru_add),s(cart(real,sK3164_skl),sK3166_skl))),s(cart(real,sK3164_skl),sK3167_skl))))),s(cart(real,sK3164_skl),sK3165_skl))))),
% 45.16/7.80 inference(cnf_transformation,[status(thm)],[f13431])).
% 45.16/7.80 fof(f16272,plain,(
% 45.16/7.80 ~p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3165_skl))),s(cart(real,sK3164_skl),i(s(fun(cart(real,sK3164_skl),cart(real,sK3164_skl)),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),cart(real,sK3164_skl))),vectoru_add),s(cart(real,sK3164_skl),sK3166_skl))),s(cart(real,sK3164_skl),sK3167_skl))))))),
% 45.16/7.80 inference(backward_demodulation,[status(thm)],[f13402,f13434])).
% 45.16/7.80 fof(f16276,plain,(
% 45.16/7.80 p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3165_skl))),s(cart(real,sK3164_skl),sK3167_skl))))),
% 45.16/7.80 inference(backward_demodulation,[status(thm)],[f13402,f13433])).
% 45.16/7.80 fof(f16280,plain,(
% 45.16/7.80 p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3165_skl))),s(cart(real,sK3164_skl),sK3166_skl))))),
% 45.16/7.80 inference(backward_demodulation,[status(thm)],[f13402,f13432])).
% 45.16/7.80 fof(f19806,plain,(
% 45.16/7.80 s(bool,t)=s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3165_skl))),s(cart(real,sK3164_skl),sK3167_skl)))),
% 45.16/7.80 inference(resolution,[status(thm)],[f3233,f16276])).
% 45.16/7.80 fof(f20347,plain,(
% 45.16/7.80 s(bool,f0)=s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3165_skl))),s(cart(real,sK3164_skl),i(s(fun(cart(real,sK3164_skl),cart(real,sK3164_skl)),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),cart(real,sK3164_skl))),vectoru_add),s(cart(real,sK3164_skl),sK3166_skl))),s(cart(real,sK3164_skl),sK3167_skl)))))),
% 45.16/7.80 inference(resolution,[status(thm)],[f3237,f16272])).
% 45.16/7.80 fof(f21043,plain,(
% 45.16/7.80 ![X0]: (~p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3165_skl))),s(cart(real,sK3164_skl),X0))))|p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3165_skl))),s(cart(real,sK3164_skl),i(s(fun(cart(real,sK3164_skl),cart(real,sK3164_skl)),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),cart(real,sK3164_skl))),vectoru_add),s(cart(real,sK3164_skl),sK3166_skl))),s(cart(real,sK3164_skl),X0)))))))),
% 45.16/7.80 inference(resolution,[status(thm)],[f13421,f16280])).
% 45.16/7.80 fof(f29385,plain,(
% 45.16/7.80 ~p(s(bool,t))|p(s(bool,i(s(fun(cart(real,sK3164_skl),bool),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),bool)),orthogonal),s(cart(real,sK3164_skl),sK3165_skl))),s(cart(real,sK3164_skl),i(s(fun(cart(real,sK3164_skl),cart(real,sK3164_skl)),i(s(fun(cart(real,sK3164_skl),fun(cart(real,sK3164_skl),cart(real,sK3164_skl))),vectoru_add),s(cart(real,sK3164_skl),sK3166_skl))),s(cart(real,sK3164_skl),sK3167_skl))))))),
% 12.11/8.06 inference(paramodulation,[status(thm)],[f19806,f21043])).
% 12.11/8.06 fof(f29409,plain,(
% 12.11/8.06 ~p(s(bool,t))|p(s(bool,f0))),
% 12.11/8.06 inference(forward_demodulation,[status(thm)],[f20347,f29385])).
% 12.11/8.06 fof(f29410,plain,(
% 12.11/8.06 p(s(bool,f0))),
% 12.11/8.06 inference(forward_subsumption_resolution,[status(thm)],[f29409,f3024])).
% 12.11/8.06 fof(f29427,plain,(
% 12.11/8.06 $false),
% 12.11/8.06 inference(forward_subsumption_resolution,[status(thm)],[f29410,f3240])).
% 12.11/8.06 % SZS output end CNFRefutation for theBenchmark.p
% 12.11/8.06 % Elapsed time: 7.661099 seconds
% 12.11/8.06 % CPU time: 46.658850 seconds
% 12.11/8.06 % Total memory used: 1.906 GB
% 12.11/8.06 % Net memory used: 1.898 GB
%------------------------------------------------------------------------------