%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO085+1 : TPTP v9.3.1. Released v2.4.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:25:44 PM UTC 2026
% Result : Theorem 0.19s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO085+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n018.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Sun Sep 20 10:21:42 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.48 % Drodi V4.1.1
% 0.19/0.51 % Refutation found
% 0.19/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.51 % SZS output start CNFRefutation for theBenchmark
% 0.19/0.51 fof(f6,axiom,(
% 0.19/0.51 (! [C] :( closed(C)<=> ~ (? [P] : end_point(P,C) )) )),
% 0.19/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.51 fof(f7,axiom,(
% 0.19/0.51 (! [C] :( open(C)<=> (? [P] : end_point(P,C) )) )),
% 0.19/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.51 fof(f13,axiom,(
% 0.19/0.51 (! [C,P] :( end_point(P,C)=> (? [Q] :( end_point(Q,C)& P != Q ) )) )),
% 0.19/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.51 fof(f17,conjecture,(
% 0.19/0.51 (! [C] :( open(C)=> (? [P,Q] :( P != Q& end_point(P,C)& end_point(Q,C) ) )) )),
% 0.19/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.51 fof(f18,negated_conjecture,(
% 0.19/0.51 ~((! [C] :( open(C)=> (? [P,Q] :( P != Q& end_point(P,C)& end_point(Q,C) ) )) ))),
% 0.19/0.51 inference(negated_conjecture,[status(cth)],[f17])).
% 0.19/0.51 fof(f63,plain,(
% 0.19/0.51 ![C]: (closed(C)<=>(![P]: ~end_point(P,C)))),
% 0.19/0.51 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.19/0.51 fof(f64,plain,(
% 0.19/0.51 ![C]: ((~closed(C)|(![P]: ~end_point(P,C)))&(closed(C)|(?[P]: end_point(P,C))))),
% 0.19/0.51 inference(NNF_transformation,[status(thm)],[f63])).
% 0.19/0.51 fof(f65,plain,(
% 0.19/0.51 (![C]: (~closed(C)|(![P]: ~end_point(P,C))))&(![C]: (closed(C)|(?[P]: end_point(P,C))))),
% 0.19/0.51 inference(miniscoping,[status(thm)],[f64])).
% 0.19/0.51 fof(f66,plain,(
% 0.19/0.51 (![C]: (~closed(C)|(![P]: ~end_point(P,C))))&(![C]: (closed(C)|end_point(sK5_skl(C),C)))),
% 0.19/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(P,sK5_skl(C))],[f65])).
% 0.19/0.51 fof(f67,plain,(
% 0.19/0.51 ![X0,X1]: (~closed(X0)|~end_point(X1,X0))),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f66])).
% 0.19/0.51 fof(f68,plain,(
% 0.19/0.51 ![X0]: (closed(X0)|end_point(sK5_skl(X0),X0))),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f66])).
% 0.19/0.51 fof(f69,plain,(
% 0.19/0.51 ![C]: ((~open(C)|(?[P]: end_point(P,C)))&(open(C)|(![P]: ~end_point(P,C))))),
% 0.19/0.51 inference(NNF_transformation,[status(thm)],[f7])).
% 0.19/0.51 fof(f70,plain,(
% 0.19/0.51 (![C]: (~open(C)|(?[P]: end_point(P,C))))&(![C]: (open(C)|(![P]: ~end_point(P,C))))),
% 0.19/0.51 inference(miniscoping,[status(thm)],[f69])).
% 0.19/0.51 fof(f71,plain,(
% 0.19/0.51 (![C]: (~open(C)|end_point(sK6_skl(C),C)))&(![C]: (open(C)|(![P]: ~end_point(P,C))))),
% 0.19/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(P,sK6_skl(C))],[f70])).
% 0.19/0.51 fof(f72,plain,(
% 0.19/0.51 ![X0]: (~open(X0)|end_point(sK6_skl(X0),X0))),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f71])).
% 0.19/0.51 fof(f89,plain,(
% 0.19/0.51 ![C,P]: (~end_point(P,C)|(?[Q]: (end_point(Q,C)&~P=Q)))),
% 0.19/0.51 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.19/0.51 fof(f90,plain,(
% 0.19/0.51 ![C,P]: (~end_point(P,C)|(end_point(sK10_skl(P,C),C)&~P=sK10_skl(P,C)))),
% 0.19/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Q,sK10_skl(P,C))],[f89])).
% 0.19/0.51 fof(f91,plain,(
% 0.19/0.51 ![X0,X1]: (~end_point(X0,X1)|end_point(sK10_skl(X0,X1),X1))),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f90])).
% 0.19/0.51 fof(f92,plain,(
% 0.19/0.51 ![X0,X1]: (~end_point(X0,X1)|~X0=sK10_skl(X0,X1))),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f90])).
% 0.19/0.51 fof(f104,plain,(
% 0.19/0.51 (?[C]: (open(C)&(![P,Q]: ((P=Q|~end_point(P,C))|~end_point(Q,C)))))),
% 0.19/0.51 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.19/0.51 fof(f105,plain,(
% 0.19/0.51 ?[C]: (open(C)&(![Q]: ((![P]: (P=Q|~end_point(P,C)))|~end_point(Q,C))))),
% 0.19/0.51 inference(miniscoping,[status(thm)],[f104])).
% 0.19/0.51 fof(f106,plain,(
% 0.19/0.51 (open(sK13_skl)&(![Q]: ((![P]: (P=Q|~end_point(P,sK13_skl)))|~end_point(Q,sK13_skl))))),
% 0.19/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(C,sK13_skl)],[f105])).
% 0.19/0.51 fof(f107,plain,(
% 0.19/0.51 open(sK13_skl)),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f106])).
% 0.19/0.51 fof(f108,plain,(
% 0.19/0.51 ![X0,X1]: (X0=X1|~end_point(X0,sK13_skl)|~end_point(X1,sK13_skl))),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f106])).
% 0.19/0.51 fof(f118,plain,(
% 0.19/0.51 ![X0]: (closed(sK13_skl)|X0=sK5_skl(sK13_skl)|~end_point(X0,sK13_skl))),
% 0.19/0.51 inference(resolution,[status(thm)],[f68,f108])).
% 0.19/0.51 fof(f125,plain,(
% 0.19/0.51 ![X0]: (X0=sK5_skl(sK13_skl)|~end_point(X0,sK13_skl))),
% 0.19/0.51 inference(forward_subsumption_resolution,[status(thm)],[f118,f67])).
% 0.19/0.51 fof(f131,plain,(
% 0.19/0.51 end_point(sK6_skl(sK13_skl),sK13_skl)),
% 0.19/0.51 inference(resolution,[status(thm)],[f72,f107])).
% 0.19/0.51 fof(f132,plain,(
% 0.19/0.52 sK6_skl(sK13_skl)=sK5_skl(sK13_skl)),
% 0.19/0.52 inference(resolution,[status(thm)],[f131,f125])).
% 0.19/0.52 fof(f141,plain,(
% 0.19/0.52 end_point(sK5_skl(sK13_skl),sK13_skl)),
% 0.19/0.52 inference(backward_demodulation,[status(thm)],[f132,f131])).
% 0.19/0.52 fof(f165,plain,(
% 0.19/0.52 end_point(sK10_skl(sK5_skl(sK13_skl),sK13_skl),sK13_skl)),
% 0.19/0.52 inference(resolution,[status(thm)],[f91,f141])).
% 0.19/0.52 fof(f167,plain,(
% 0.19/0.52 sK10_skl(sK5_skl(sK13_skl),sK13_skl)=sK5_skl(sK13_skl)),
% 0.19/0.52 inference(resolution,[status(thm)],[f165,f125])).
% 0.19/0.52 fof(f178,plain,(
% 0.19/0.52 ~end_point(sK5_skl(sK13_skl),sK13_skl)),
% 0.19/0.52 inference(resolution,[status(thm)],[f167,f92])).
% 0.19/0.52 fof(f180,plain,(
% 0.19/0.52 $false),
% 0.19/0.52 inference(forward_subsumption_resolution,[status(thm)],[f178,f141])).
% 0.19/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.55 % Elapsed time: 0.082357 seconds
% 0.19/0.55 % CPU time: 0.235095 seconds
% 0.19/0.55 % Total memory used: 59.963 MB
% 0.19/0.55 % Net memory used: 59.808 MB
%------------------------------------------------------------------------------