%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO111-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:47 PM UTC 2026
% Result : Unsatisfiable 0.14s 5.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO111-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n003.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Sun Sep 20 11:28:21 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.39 % Drodi V4.1.1
% 0.14/5.63 % Refutation found
% 0.14/5.63 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/5.63 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.63 fof(f1,axiom,(
% 0.14/5.63 (![A,B,C]: (( ~ part_of(A,B)| ~ incident_c(C,A)| incident_c(C,B) ) ))),
% 0.14/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.63 fof(f13,axiom,(
% 0.14/5.63 (![A,B]: (( ~ end_point(A,B)| incident_c(A,B) ) ))),
% 0.14/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.63 fof(f21,axiom,(
% 0.14/5.63 (![A,B]: (( ~ inner_point(A,B)| incident_c(A,B) ) ))),
% 0.14/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.63 fof(f22,axiom,(
% 0.14/5.63 (![A,B]: (( ~ inner_point(A,B)| ~ end_point(A,B) ) ))),
% 0.14/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.63 fof(f49,axiom,(
% 0.14/5.63 (![A,B,C,D]: (( ~ between_c(A,B,C,D)| B != D ) ))),
% 0.14/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.63 fof(f50,axiom,(
% 0.14/5.63 (![A,B,C,D]: (( ~ between_c(A,B,C,D)| part_of(ax1_sk1(D,C,B,A),A) ) ))),
% 0.14/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.63 fof(f51,axiom,(
% 0.14/5.63 (![A,B,C,D]: (( ~ between_c(A,B,C,D)| end_point(B,ax1_sk1(D,C,B,A)) ) ))),
% 0.14/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.63 fof(f52,axiom,(
% 0.14/5.63 (![A,B,C,D]: (( ~ between_c(A,B,C,D)| end_point(D,ax1_sk1(D,C,B,A)) ) ))),
% 0.14/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.63 fof(f53,axiom,(
% 0.14/5.63 (![A,B,C,D]: (( ~ between_c(A,B,C,D)| inner_point(C,ax1_sk1(D,C,B,A)) ) ))),
% 0.14/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.63 fof(f55,negated_conjecture,(
% 0.14/5.63 between_c(sk15,sk16,sk17,sk18) ),
% 0.14/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.63 fof(f56,negated_conjecture,(
% 0.14/5.63 ( ~ incident_c(sk16,sk15)| ~ incident_c(sk17,sk15)| ~ incident_c(sk18,sk15)| sk16 = sk17| sk17 = sk18| sk16 = sk18 ) ),
% 0.14/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.63 fof(f57,plain,(
% 0.14/5.63 ![B,C]: ((![A]: (~part_of(A,B)|~incident_c(C,A)))|incident_c(C,B))),
% 0.14/5.63 inference(miniscoping,[status(thm)],[f1])).
% 0.14/5.63 fof(f58,plain,(
% 0.14/5.63 ![X0,X1,X2]: (~part_of(X0,X1)|~incident_c(X2,X0)|incident_c(X2,X1))),
% 0.14/5.63 inference(cnf_transformation,[status(thm)],[f57])).
% 0.14/5.63 fof(f73,plain,(
% 0.14/5.63 ![X0,X1]: (~end_point(X0,X1)|incident_c(X0,X1))),
% 0.14/5.63 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/5.63 fof(f82,plain,(
% 0.14/5.63 ![X0,X1]: (~inner_point(X0,X1)|incident_c(X0,X1))),
% 0.14/5.63 inference(cnf_transformation,[status(thm)],[f21])).
% 0.14/5.63 fof(f83,plain,(
% 0.14/5.63 ![X0,X1]: (~inner_point(X0,X1)|~end_point(X0,X1))),
% 0.14/5.63 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/5.63 fof(f121,plain,(
% 0.14/5.63 ![B,D]: ((![A,C]: ~between_c(A,B,C,D))|~B=D)),
% 0.14/5.63 inference(miniscoping,[status(thm)],[f49])).
% 0.14/5.63 fof(f122,plain,(
% 0.14/5.63 ![X0,X1,X2,X3]: (~between_c(X0,X1,X2,X3)|~X1=X3)),
% 0.14/5.63 inference(cnf_transformation,[status(thm)],[f121])).
% 0.14/5.63 fof(f123,plain,(
% 0.14/5.63 ![X0,X1,X2,X3]: (~between_c(X0,X1,X2,X3)|part_of(ax1_sk1(X3,X2,X1,X0),X0))),
% 0.14/5.63 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/5.63 fof(f124,plain,(
% 0.14/5.63 ![X0,X1,X2,X3]: (~between_c(X0,X1,X2,X3)|end_point(X1,ax1_sk1(X3,X2,X1,X0)))),
% 0.14/5.63 inference(cnf_transformation,[status(thm)],[f51])).
% 0.14/5.63 fof(f125,plain,(
% 0.14/5.63 ![X0,X1,X2,X3]: (~between_c(X0,X1,X2,X3)|end_point(X3,ax1_sk1(X3,X2,X1,X0)))),
% 0.14/5.63 inference(cnf_transformation,[status(thm)],[f52])).
% 0.14/5.63 fof(f126,plain,(
% 0.14/5.63 ![X0,X1,X2,X3]: (~between_c(X0,X1,X2,X3)|inner_point(X2,ax1_sk1(X3,X2,X1,X0)))),
% 0.14/5.63 inference(cnf_transformation,[status(thm)],[f53])).
% 0.14/5.63 fof(f129,plain,(
% 0.14/5.63 between_c(sk15,sk16,sk17,sk18)),
% 0.14/5.63 inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/5.63 fof(f130,plain,(
% 0.14/5.63 ~incident_c(sk16,sk15)|~incident_c(sk17,sk15)|~incident_c(sk18,sk15)|sk16=sk17|sk17=sk18|sk16=sk18),
% 0.14/5.63 inference(cnf_transformation,[status(thm)],[f56])).
% 0.14/5.63 fof(f131,plain,(
% 0.14/5.63 ![X0,X1,X2]: (~between_c(X0,X1,X2,X1))),
% 0.14/5.63 inference(destructive_equality_resolution,[status(thm)],[f122])).
% 0.14/5.63 fof(f139,plain,(
% 0.14/5.63 part_of(ax1_sk1(sk18,sk17,sk16,sk15),sk15)),
% 0.14/5.63 inference(resolution,[status(thm)],[f123,f129])).
% 0.14/5.63 fof(f141,plain,(
% 0.14/5.63 ![X0]: (~incident_c(X0,ax1_sk1(sk18,sk17,sk16,sk15))|incident_c(X0,sk15))),
% 0.14/5.63 inference(resolution,[status(thm)],[f139,f58])).
% 0.14/5.63 fof(f142,plain,(
% 0.14/5.63 end_point(sk16,ax1_sk1(sk18,sk17,sk16,sk15))),
% 0.14/5.63 inference(resolution,[status(thm)],[f124,f129])).
% 0.14/5.63 fof(f143,plain,(
% 0.14/5.63 incident_c(sk16,ax1_sk1(sk18,sk17,sk16,sk15))),
% 0.14/5.64 inference(resolution,[status(thm)],[f142,f73])).
% 0.14/5.64 fof(f146,plain,(
% 0.14/5.64 end_point(sk18,ax1_sk1(sk18,sk17,sk16,sk15))),
% 0.14/5.64 inference(resolution,[status(thm)],[f125,f129])).
% 0.14/5.64 fof(f147,plain,(
% 0.14/5.64 incident_c(sk18,ax1_sk1(sk18,sk17,sk16,sk15))),
% 0.14/5.64 inference(resolution,[status(thm)],[f146,f73])).
% 0.14/5.64 fof(f170,plain,(
% 0.14/5.64 incident_c(sk18,sk15)),
% 0.14/5.64 inference(resolution,[status(thm)],[f141,f147])).
% 0.14/5.64 fof(f171,plain,(
% 0.14/5.64 incident_c(sk16,sk15)),
% 0.14/5.64 inference(resolution,[status(thm)],[f141,f143])).
% 0.14/5.64 fof(f179,plain,(
% 0.14/5.64 ~incident_c(sk16,sk15)|~incident_c(sk17,sk15)|sk16=sk17|sk17=sk18|sk16=sk18),
% 0.14/5.64 inference(backward_subsumption_resolution,[status(thm)],[f130,f170])).
% 0.14/5.64 fof(f180,plain,(
% 0.14/5.64 ~incident_c(sk17,sk15)|sk16=sk17|sk17=sk18|sk16=sk18),
% 0.14/5.64 inference(forward_subsumption_resolution,[status(thm)],[f179,f171])).
% 0.14/5.64 fof(f249,plain,(
% 0.14/5.64 inner_point(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),
% 0.14/5.64 inference(resolution,[status(thm)],[f126,f129])).
% 0.14/5.64 fof(f250,plain,(
% 0.14/5.64 ~end_point(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),
% 0.14/5.64 inference(resolution,[status(thm)],[f249,f83])).
% 0.14/5.64 fof(f251,plain,(
% 0.14/5.64 incident_c(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),
% 0.14/5.64 inference(resolution,[status(thm)],[f249,f82])).
% 0.14/5.64 fof(f409,plain,(
% 0.14/5.64 incident_c(sk17,sk15)),
% 0.14/5.64 inference(resolution,[status(thm)],[f251,f141])).
% 0.14/5.64 fof(f412,plain,(
% 0.14/5.64 sk16=sk17|sk17=sk18|sk16=sk18),
% 0.14/5.64 inference(backward_subsumption_resolution,[status(thm)],[f180,f409])).
% 0.14/5.64 fof(f473,plain,(
% 0.14/5.64 end_point(sk17,ax1_sk1(sk18,sk17,sk16,sk15))|sk16=sk17|sk16=sk18),
% 0.14/5.64 inference(paramodulation,[status(thm)],[f412,f146])).
% 0.14/5.64 fof(f478,plain,(
% 0.14/5.64 sk16=sk17|sk16=sk18),
% 0.14/5.64 inference(forward_subsumption_resolution,[status(thm)],[f473,f250])).
% 0.14/5.64 fof(f503,plain,(
% 0.14/5.64 between_c(sk15,sk16,sk17,sk16)|sk16=sk17),
% 0.14/5.64 inference(paramodulation,[status(thm)],[f478,f129])).
% 0.14/5.64 fof(f510,plain,(
% 0.14/5.64 ~end_point(sk17,ax1_sk1(sk18,sk16,sk16,sk15))),
% 0.14/5.64 inference(backward_demodulation,[status(thm)],[f604,f250])).
% 0.14/5.64 fof(f521,plain,(
% 0.14/5.64 end_point(sk16,ax1_sk1(sk18,sk16,sk16,sk15))),
% 0.14/5.64 inference(backward_demodulation,[status(thm)],[f604,f142])).
% 0.14/5.64 fof(f604,plain,(
% 0.14/5.64 sk16=sk17),
% 0.14/5.64 inference(forward_subsumption_resolution,[status(thm)],[f503,f131])).
% 0.14/5.64 fof(f609,plain,(
% 0.14/5.64 ~end_point(sk16,ax1_sk1(sk18,sk16,sk16,sk15))),
% 0.14/5.64 inference(forward_demodulation,[status(thm)],[f604,f510])).
% 0.14/5.64 fof(f618,plain,(
% 0.14/5.64 $false),
% 0.14/5.64 inference(forward_subsumption_resolution,[status(thm)],[f521,f609])).
% 0.14/5.64 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.64 % Elapsed time: 0.261051 seconds
% 0.14/5.64 % CPU time: 1.805741 seconds
% 0.14/5.64 % Total memory used: 99.338 MB
% 0.14/5.64 % Net memory used: 97.261 MB
%------------------------------------------------------------------------------