%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO011-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:32 PM UTC 2026
% Result : Unsatisfiable 1.43s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO011-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n015.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sun Sep 20 08:20:05 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.35 % Drodi V4.1.1
% 1.43/0.59 % Refutation found
% 1.43/0.59 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.43/0.59 % SZS output start CNFRefutation for theBenchmark
% 1.43/0.59 fof(f1,axiom,(
% 1.43/0.59 (![X,Y]: (( ~ between(X,Y,X)| X = Y ) ))),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f2,axiom,(
% 1.43/0.59 (![X,Y,V,Z]: (( ~ between(X,Y,V)| ~ between(Y,Z,V)| between(X,Y,Z) ) ))),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f5,axiom,(
% 1.43/0.59 (![X,Y,Z]: (( ~ equidistant(X,Y,Z,Z)| X = Y ) ))),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f7,axiom,(
% 1.43/0.59 (![X,W,V,Y,Z]: (( ~ between(X,W,V)| ~ between(Y,V,Z)| between(X,outer_pasch(W,X,Y,Z,V),Y) ) ))),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f8,axiom,(
% 1.43/0.59 (![X,W,V,Y,Z]: (( ~ between(X,W,V)| ~ between(Y,V,Z)| between(Z,W,outer_pasch(W,X,Y,Z,V)) ) ))),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f13,axiom,(
% 1.43/0.59 (![X,Y,W,V]: (between(X,Y,extension(X,Y,W,V)) ))),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f14,axiom,(
% 1.43/0.59 (![Y,X,W,V]: (equidistant(Y,extension(X,Y,W,V),W,V) ))),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f15,axiom,(
% 1.43/0.59 ~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3) ),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f16,axiom,(
% 1.43/0.59 ~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1) ),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f17,axiom,(
% 1.43/0.59 ~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2) ),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f21,axiom,(
% 1.43/0.59 (![X,Y,Z]: (( ~ colinear(X,Y,Z)| between(X,Y,Z)| between(Y,X,Z)| between(X,Z,Y) ) ))),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f25,negated_conjecture,(
% 1.43/0.59 colinear(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3) ),
% 1.43/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.43/0.59 fof(f26,plain,(
% 1.43/0.59 ![X0,X1]: (~between(X0,X1,X0)|X0=X1)),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f1])).
% 1.43/0.59 fof(f27,plain,(
% 1.43/0.59 ![X,Y,Z]: ((![V]: (~between(X,Y,V)|~between(Y,Z,V)))|between(X,Y,Z))),
% 1.43/0.59 inference(miniscoping,[status(thm)],[f2])).
% 1.43/0.59 fof(f28,plain,(
% 1.43/0.59 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X1,X3,X2)|between(X0,X1,X3))),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f27])).
% 1.43/0.59 fof(f32,plain,(
% 1.43/0.59 ![X,Y]: ((![Z]: ~equidistant(X,Y,Z,Z))|X=Y)),
% 1.43/0.59 inference(miniscoping,[status(thm)],[f5])).
% 1.43/0.59 fof(f33,plain,(
% 1.43/0.59 ![X0,X1,X2]: (~equidistant(X0,X1,X2,X2)|X0=X1)),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f32])).
% 1.43/0.59 fof(f36,plain,(
% 1.43/0.59 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X2,X4)|between(X0,outer_pasch(X1,X0,X3,X4,X2),X3))),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f7])).
% 1.43/0.59 fof(f37,plain,(
% 1.43/0.59 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X2,X4)|between(X4,X1,outer_pasch(X1,X0,X3,X4,X2)))),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f8])).
% 1.43/0.59 fof(f43,plain,(
% 1.43/0.59 ![X0,X1,X2,X3]: (between(X0,X1,extension(X0,X1,X2,X3)))),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f13])).
% 1.43/0.59 fof(f44,plain,(
% 1.43/0.59 ![X0,X1,X2,X3]: (equidistant(X0,extension(X1,X0,X2,X3),X2,X3))),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f14])).
% 1.43/0.59 fof(f45,plain,(
% 1.43/0.59 ~between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3)),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f15])).
% 1.43/0.59 fof(f46,plain,(
% 1.43/0.59 ~between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1)),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f16])).
% 1.43/0.59 fof(f47,plain,(
% 1.43/0.59 ~between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2)),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f17])).
% 1.43/0.59 fof(f52,plain,(
% 1.43/0.59 ![X0,X1,X2]: (~colinear(X0,X1,X2)|between(X0,X1,X2)|between(X1,X0,X2)|between(X0,X2,X1))),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f21])).
% 1.43/0.59 fof(f56,plain,(
% 1.43/0.59 colinear(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3)),
% 1.43/0.59 inference(cnf_transformation,[status(thm)],[f25])).
% 1.43/0.59 fof(f57,plain,(
% 1.43/0.59 between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3)|between(lower_dimension_point_2,lower_dimension_point_1,lower_dimension_point_3)|between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2)),
% 1.43/0.59 inference(resolution,[status(thm)],[f52,f56])).
% 1.43/0.59 fof(f59,plain,(
% 1.43/0.59 between(lower_dimension_point_2,lower_dimension_point_1,lower_dimension_point_3)|between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2)),
% 1.43/0.59 inference(forward_subsumption_resolution,[status(thm)],[f57,f45])).
% 1.43/0.59 fof(f82,plain,(
% 1.43/0.59 ![X0,X1,X2]: (X0=extension(X1,X0,X2,X2))),
% 1.43/0.59 inference(resolution,[status(thm)],[f44,f33])).
% 1.43/0.59 fof(f86,plain,(
% 1.43/0.59 ![X0,X1]: (between(X0,X1,X1))),
% 1.43/0.59 inference(paramodulation,[status(thm)],[f82,f43])).
% 1.43/0.59 fof(f108,plain,(
% 1.43/0.59 ![X0,X1]: (~between(X0,X1,lower_dimension_point_1)|between(X0,outer_pasch(X1,X0,lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),lower_dimension_point_2)|between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2))),
% 1.43/0.59 inference(resolution,[status(thm)],[f36,f59])).
% 1.43/0.59 fof(f110,plain,(
% 1.43/0.59 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|between(X0,outer_pasch(X1,X0,X3,X2,X2),X3))),
% 1.43/0.59 inference(resolution,[status(thm)],[f36,f86])).
% 1.43/0.59 fof(f111,plain,(
% 1.43/0.59 ![X0,X1]: (~between(X0,X1,lower_dimension_point_1)|between(lower_dimension_point_3,X1,outer_pasch(X1,X0,lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1))|between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2))),
% 1.43/0.59 inference(resolution,[status(thm)],[f37,f59])).
% 1.43/0.59 fof(f113,plain,(
% 1.43/0.59 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|between(X2,X1,outer_pasch(X1,X0,X3,X2,X2)))),
% 1.43/0.59 inference(resolution,[status(thm)],[f37,f86])).
% 1.43/0.59 fof(f117,plain,(
% 1.43/0.59 ![X0]: (between(X0,outer_pasch(lower_dimension_point_1,X0,lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),lower_dimension_point_2)|between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2))),
% 1.43/0.59 inference(resolution,[status(thm)],[f108,f86])).
% 1.43/0.59 fof(f122,plain,(
% 1.43/0.59 ![X0,X1]: (between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2)|~between(X0,X1,lower_dimension_point_2)|between(X0,X1,outer_pasch(lower_dimension_point_1,X1,lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1)))),
% 1.43/0.59 inference(resolution,[status(thm)],[f117,f28])).
% 1.43/0.59 fof(f135,plain,(
% 1.43/0.59 ![X0]: (between(lower_dimension_point_3,lower_dimension_point_1,outer_pasch(lower_dimension_point_1,X0,lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1))|between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2))),
% 1.43/0.59 inference(resolution,[status(thm)],[f111,f86])).
% 1.43/0.59 fof(f148,plain,(
% 1.43/0.59 ![X0]: (between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2)|between(X0,lower_dimension_point_2,outer_pasch(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1)))),
% 1.43/0.59 inference(resolution,[status(thm)],[f122,f86])).
% 1.43/0.59 fof(f154,plain,(
% 1.43/0.59 ![X0,X1]: (between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2)|~between(X0,X1,outer_pasch(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1))|between(X0,X1,lower_dimension_point_2))),
% 1.43/0.59 inference(resolution,[status(thm)],[f148,f28])).
% 1.43/0.59 fof(f158,plain,(
% 1.43/0.59 between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2)|between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2)|between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2)),
% 1.43/0.59 inference(resolution,[status(thm)],[f154,f135])).
% 1.43/0.59 fof(f161,plain,(
% 1.43/0.59 between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2)|between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2)),
% 1.43/0.59 inference(duplicate_literals_removal,[status(thm)],[f158])).
% 1.43/0.59 fof(f162,plain,(
% 1.43/0.59 between(lower_dimension_point_1,lower_dimension_point_3,lower_dimension_point_2)),
% 1.43/0.59 inference(forward_subsumption_resolution,[status(thm)],[f161,f47])).
% 1.43/0.59 fof(f176,plain,(
% 1.43/0.60 ![X0]: (between(lower_dimension_point_1,outer_pasch(lower_dimension_point_3,lower_dimension_point_1,X0,lower_dimension_point_2,lower_dimension_point_2),X0))),
% 1.43/0.60 inference(resolution,[status(thm)],[f110,f162])).
% 1.43/0.60 fof(f194,plain,(
% 1.43/0.60 ![X0]: (between(lower_dimension_point_2,lower_dimension_point_3,outer_pasch(lower_dimension_point_3,lower_dimension_point_1,X0,lower_dimension_point_2,lower_dimension_point_2)))),
% 1.43/0.60 inference(resolution,[status(thm)],[f113,f162])).
% 1.43/0.60 fof(f295,plain,(
% 1.43/0.60 lower_dimension_point_1=outer_pasch(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_2)),
% 1.43/0.60 inference(resolution,[status(thm)],[f176,f26])).
% 1.43/0.60 fof(f362,plain,(
% 1.43/0.60 between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1)),
% 1.43/0.60 inference(paramodulation,[status(thm)],[f295,f194])).
% 1.43/0.60 fof(f363,plain,(
% 1.43/0.60 $false),
% 1.43/0.60 inference(forward_subsumption_resolution,[status(thm)],[f362,f46])).
% 1.43/0.60 % SZS output end CNFRefutation for theBenchmark.p
% 1.43/0.61 % Elapsed time: 0.254304 seconds
% 1.43/0.61 % CPU time: 1.735509 seconds
% 1.43/0.61 % Total memory used: 97.442 MB
% 1.43/0.61 % Net memory used: 94.010 MB
%------------------------------------------------------------------------------