%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO127-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 : n013.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:50 PM UTC 2026
% Result : Unsatisfiable 0.11s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO127-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n013.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 20 12:06:51 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.40 % Drodi V4.1.1
% 0.11/0.46 % Refutation found
% 0.11/0.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.11/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.46 fof(f13,axiom,(
% 0.11/0.46 (![A,B]: (( ~ end_point(A,B)| incident_c(A,B) ) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f33,axiom,(
% 0.11/0.46 (![A]: (( ~ open(A)| end_point(ax0_sk7(A),A) ) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f41,axiom,(
% 0.11/0.46 (![A,B]: (( ~ end_point(A,B)| end_point(ax0_sk11(A,B),B) ) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f42,axiom,(
% 0.11/0.46 (![A,B]: (( ~ end_point(A,B)| A != ax0_sk11(A,B) ) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f62,axiom,(
% 0.11/0.46 (![A,B,C]: (( ~ start_point(A,B)| A = C| ~ incident_o(C,B)| ordered_by(B,A,C) ) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f71,axiom,(
% 0.11/0.46 (![A,B,C]: (( ~ ordered_by(A,B,C)| incident_o(B,A) ) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f72,axiom,(
% 0.11/0.46 (![A,B,C]: (( ~ ordered_by(A,B,C)| incident_o(C,A) ) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f73,axiom,(
% 0.11/0.46 (![A]: (open(ax2_sk3(A)) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f75,axiom,(
% 0.11/0.46 (![A,B]: (( ~ incident_c(A,ax2_sk3(B))| incident_o(A,B) ) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f83,axiom,(
% 0.11/0.46 (![A]: (start_point(ax2_sk6(A),A) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f97,negated_conjecture,(
% 0.11/0.46 ( incident_o(sk26,sk25)| ordered_by(sk25,sk26,sk27)| ordered_by(sk25,sk27,sk26) ) ),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f101,negated_conjecture,(
% 0.11/0.46 (![A]: (( ~ ordered_by(sk25,sk26,A)| ~ incident_o(sk26,sk25) ) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f102,negated_conjecture,(
% 0.11/0.46 (![A]: (( ~ ordered_by(sk25,A,sk26)| ~ incident_o(sk26,sk25) ) ))),
% 0.11/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.46 fof(f119,plain,(
% 0.11/0.46 ![X0,X1]: (~end_point(X0,X1)|incident_c(X0,X1))),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f13])).
% 0.11/0.46 fof(f145,plain,(
% 0.11/0.46 ![X0]: (~open(X0)|end_point(ax0_sk7(X0),X0))),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f33])).
% 0.11/0.46 fof(f157,plain,(
% 0.11/0.46 ![X0,X1]: (~end_point(X0,X1)|end_point(ax0_sk11(X0,X1),X1))),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f41])).
% 0.11/0.46 fof(f158,plain,(
% 0.11/0.46 ![X0,X1]: (~end_point(X0,X1)|~X0=ax0_sk11(X0,X1))),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f42])).
% 0.11/0.46 fof(f186,plain,(
% 0.11/0.46 ![X0,X1,X2]: (~start_point(X0,X1)|X0=X2|~incident_o(X2,X1)|ordered_by(X1,X0,X2))),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f62])).
% 0.11/0.46 fof(f195,plain,(
% 0.11/0.46 ![A,B]: ((![C]: ~ordered_by(A,B,C))|incident_o(B,A))),
% 0.11/0.46 inference(miniscoping,[status(thm)],[f71])).
% 0.11/0.46 fof(f196,plain,(
% 0.11/0.46 ![X0,X1,X2]: (~ordered_by(X0,X1,X2)|incident_o(X1,X0))),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f195])).
% 0.11/0.46 fof(f197,plain,(
% 0.11/0.46 ![A,C]: ((![B]: ~ordered_by(A,B,C))|incident_o(C,A))),
% 0.11/0.46 inference(miniscoping,[status(thm)],[f72])).
% 0.11/0.46 fof(f198,plain,(
% 0.11/0.46 ![X0,X1,X2]: (~ordered_by(X0,X1,X2)|incident_o(X2,X0))),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f197])).
% 0.11/0.46 fof(f199,plain,(
% 0.11/0.46 ![X0]: (open(ax2_sk3(X0)))),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f73])).
% 0.11/0.46 fof(f201,plain,(
% 0.11/0.46 ![X0,X1]: (~incident_c(X0,ax2_sk3(X1))|incident_o(X0,X1))),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f75])).
% 0.11/0.46 fof(f214,plain,(
% 0.11/0.46 ![X0]: (start_point(ax2_sk6(X0),X0))),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f83])).
% 0.11/0.46 fof(f231,plain,(
% 0.11/0.46 incident_o(sk26,sk25)|ordered_by(sk25,sk26,sk27)|ordered_by(sk25,sk27,sk26)),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f97])).
% 0.11/0.46 fof(f237,plain,(
% 0.11/0.46 (![A]: ~ordered_by(sk25,sk26,A))|~incident_o(sk26,sk25)),
% 0.11/0.46 inference(miniscoping,[status(thm)],[f101])).
% 0.11/0.46 fof(f238,plain,(
% 0.11/0.46 ![X0]: (~ordered_by(sk25,sk26,X0)|~incident_o(sk26,sk25))),
% 0.11/0.46 inference(cnf_transformation,[status(thm)],[f237])).
% 0.11/0.46 fof(f239,plain,(
% 0.11/0.46 (![A]: ~ordered_by(sk25,A,sk26))|~incident_o(sk26,sk25)),
% 0.11/0.46 inference(miniscoping,[status(thm)],[f102])).
% 0.11/0.46 fof(f240,plain,(
% 0.11/0.46 ![X0]: (~ordered_by(sk25,X0,sk26)|~incident_o(sk26,sk25))),
% 0.11/0.47 inference(cnf_transformation,[status(thm)],[f239])).
% 0.11/0.47 fof(f250,plain,(
% 0.11/0.47 incident_o(sk26,sk25)|ordered_by(sk25,sk26,sk27)),
% 0.11/0.47 inference(forward_subsumption_resolution,[status(thm)],[f231,f198])).
% 0.11/0.47 fof(f252,plain,(
% 0.11/0.47 incident_o(sk26,sk25)),
% 0.11/0.47 inference(backward_subsumption_resolution,[status(thm)],[f250,f253])).
% 0.11/0.47 fof(f253,plain,(
% 0.11/0.47 ![X0]: (~ordered_by(sk25,sk26,X0))),
% 0.11/0.47 inference(forward_subsumption_resolution,[status(thm)],[f238,f196])).
% 0.11/0.47 fof(f254,plain,(
% 0.11/0.47 ![X0]: (~ordered_by(sk25,X0,sk26))),
% 0.11/0.47 inference(forward_subsumption_resolution,[status(thm)],[f240,f198])).
% 0.11/0.47 fof(f259,plain,(
% 0.11/0.47 ![X0]: (end_point(ax0_sk7(ax2_sk3(X0)),ax2_sk3(X0)))),
% 0.11/0.47 inference(resolution,[status(thm)],[f145,f199])).
% 0.11/0.47 fof(f278,plain,(
% 0.11/0.47 ![X0,X1]: (incident_o(X0,X1)|~end_point(X0,ax2_sk3(X1)))),
% 0.11/0.47 inference(resolution,[status(thm)],[f201,f119])).
% 0.11/0.47 fof(f284,plain,(
% 0.11/0.47 ![X0]: (~ax0_sk7(ax2_sk3(X0))=ax0_sk11(ax0_sk7(ax2_sk3(X0)),ax2_sk3(X0)))),
% 0.11/0.47 inference(resolution,[status(thm)],[f259,f158])).
% 0.11/0.47 fof(f288,plain,(
% 0.11/0.47 ![X0]: (incident_o(ax0_sk7(ax2_sk3(X0)),X0))),
% 0.11/0.47 inference(resolution,[status(thm)],[f278,f259])).
% 0.11/0.47 fof(f322,plain,(
% 0.11/0.47 ![X0]: (end_point(ax0_sk11(ax0_sk7(ax2_sk3(X0)),ax2_sk3(X0)),ax2_sk3(X0)))),
% 0.11/0.47 inference(resolution,[status(thm)],[f157,f259])).
% 0.11/0.47 fof(f406,plain,(
% 0.11/0.47 ![X0,X1]: (ax2_sk6(X0)=X1|~incident_o(X1,X0)|ordered_by(X0,ax2_sk6(X0),X1))),
% 0.11/0.47 inference(resolution,[status(thm)],[f186,f214])).
% 0.11/0.47 fof(f486,plain,(
% 0.11/0.47 ![X0]: (incident_o(ax0_sk11(ax0_sk7(ax2_sk3(X0)),ax2_sk3(X0)),X0))),
% 0.11/0.47 inference(resolution,[status(thm)],[f322,f278])).
% 0.11/0.47 fof(f603,plain,(
% 0.11/0.47 ax2_sk6(sk25)=sk26|~incident_o(sk26,sk25)),
% 0.11/0.47 inference(resolution,[status(thm)],[f406,f254])).
% 0.11/0.47 fof(f607,plain,(
% 0.11/0.47 ax2_sk6(sk25)=sk26),
% 0.11/0.47 inference(forward_subsumption_resolution,[status(thm)],[f603,f252])).
% 0.11/0.47 fof(f608,plain,(
% 0.11/0.47 ![X0]: (ax2_sk6(sk25)=X0|~incident_o(X0,sk25)|ordered_by(sk25,sk26,X0))),
% 0.11/0.47 inference(paramodulation,[status(thm)],[f607,f406])).
% 0.11/0.47 fof(f612,plain,(
% 0.11/0.47 ![X0]: (sk26=X0|~incident_o(X0,sk25)|ordered_by(sk25,sk26,X0))),
% 0.11/0.47 inference(forward_demodulation,[status(thm)],[f607,f608])).
% 0.11/0.47 fof(f613,plain,(
% 0.11/0.47 ![X0]: (sk26=X0|~incident_o(X0,sk25))),
% 0.11/0.47 inference(forward_subsumption_resolution,[status(thm)],[f612,f253])).
% 0.11/0.47 fof(f618,plain,(
% 0.11/0.47 sk26=ax0_sk11(ax0_sk7(ax2_sk3(sk25)),ax2_sk3(sk25))),
% 0.11/0.47 inference(resolution,[status(thm)],[f613,f486])).
% 0.11/0.47 fof(f625,plain,(
% 0.11/0.47 sk26=ax0_sk7(ax2_sk3(sk25))),
% 0.11/0.47 inference(resolution,[status(thm)],[f613,f288])).
% 0.11/0.47 fof(f631,plain,(
% 0.11/0.47 sk26=ax0_sk11(sk26,ax2_sk3(sk25))),
% 0.11/0.47 inference(backward_demodulation,[status(thm)],[f625,f618])).
% 0.11/0.47 fof(f634,plain,(
% 0.11/0.47 ~ax0_sk7(ax2_sk3(sk25))=ax0_sk11(sk26,ax2_sk3(sk25))),
% 0.11/0.47 inference(paramodulation,[status(thm)],[f625,f284])).
% 0.11/0.47 fof(f641,plain,(
% 0.11/0.47 ~sk26=ax0_sk11(sk26,ax2_sk3(sk25))),
% 0.11/0.47 inference(forward_demodulation,[status(thm)],[f625,f634])).
% 0.11/0.47 fof(f642,plain,(
% 0.11/0.47 ~sk26=sk26),
% 0.11/0.47 inference(forward_demodulation,[status(thm)],[f631,f641])).
% 0.11/0.47 fof(f643,plain,(
% 0.11/0.47 $false),
% 0.11/0.47 inference(trivial_equality_resolution,[status(thm)],[f642])).
% 0.11/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/0.50 % Elapsed time: 0.102264 seconds
% 0.18/0.50 % CPU time: 0.496092 seconds
% 0.18/0.50 % Total memory used: 86.732 MB
% 0.18/0.50 % Net memory used: 86.344 MB
%------------------------------------------------------------------------------