%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO044-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:38 PM UTC 2026
% Result : Unsatisfiable 127.93s 16.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO044-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n005.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 20 08:37:04 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 127.93/16.87 % Refutation found
% 127.93/16.87 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 127.93/16.87 % SZS output start CNFRefutation for theBenchmark
% 127.93/16.87 fof(f4,axiom,(
% 127.93/16.87 (![X,Y,W,V]: (between(X,Y,extension(X,Y,W,V)) ))),
% 127.93/16.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 127.93/16.87 fof(f5,axiom,(
% 127.93/16.87 (![Y,X,W,V]: (equidistant(Y,extension(X,Y,W,V),W,V) ))),
% 127.93/16.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 127.93/16.87 fof(f21,axiom,(
% 127.93/16.87 (![U,V,W,X]: (( ~ equidistant(U,V,W,X)| equidistant(W,X,U,V) ) ))),
% 127.93/16.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 127.93/16.87 fof(f38,axiom,(
% 127.93/16.87 (![U,V,W,X]: (( ~ between(U,V,W)| ~ between(U,V,X)| ~ equidistant(V,W,V,X)| U = V| W = X ) ))),
% 127.93/16.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 127.93/16.87 fof(f53,axiom,(
% 127.93/16.87 (![U,V,W,X]: (( ~ between(U,V,W)| ~ between(U,W,X)| between(V,W,X) ) ))),
% 127.93/16.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 127.93/16.87 fof(f54,hypothesis,(
% 127.93/16.87 between(u,v,w) ),
% 127.93/16.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 127.93/16.87 fof(f55,hypothesis,(
% 127.93/16.87 between(v,w,x) ),
% 127.93/16.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 127.93/16.87 fof(f56,hypothesis,(
% 127.93/16.87 v != w ),
% 127.93/16.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 127.93/16.87 fof(f57,negated_conjecture,(
% 127.93/16.87 ~ between(u,w,x) ),
% 127.93/16.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 127.93/16.87 fof(f63,plain,(
% 127.93/16.87 ![X0,X1,X2,X3]: (between(X0,X1,extension(X0,X1,X2,X3)))),
% 127.93/16.87 inference(cnf_transformation,[status(thm)],[f4])).
% 127.93/16.87 fof(f64,plain,(
% 127.93/16.87 ![X0,X1,X2,X3]: (equidistant(X0,extension(X1,X0,X2,X3),X2,X3))),
% 127.93/16.87 inference(cnf_transformation,[status(thm)],[f5])).
% 127.93/16.87 fof(f82,plain,(
% 127.93/16.87 ![X0,X1,X2,X3]: (~equidistant(X0,X1,X2,X3)|equidistant(X2,X3,X0,X1))),
% 127.93/16.87 inference(cnf_transformation,[status(thm)],[f21])).
% 127.93/16.87 fof(f102,plain,(
% 127.93/16.87 ![W,X]: ((![U,V]: (((~between(U,V,W)|~between(U,V,X))|~equidistant(V,W,V,X))|U=V))|W=X)),
% 127.93/16.87 inference(miniscoping,[status(thm)],[f38])).
% 127.93/16.87 fof(f103,plain,(
% 127.93/16.87 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X1,X3)|~equidistant(X1,X2,X1,X3)|X0=X1|X2=X3)),
% 127.93/16.87 inference(cnf_transformation,[status(thm)],[f102])).
% 127.93/16.87 fof(f125,plain,(
% 127.93/16.87 ![V,W,X]: ((![U]: (~between(U,V,W)|~between(U,W,X)))|between(V,W,X))),
% 127.93/16.87 inference(miniscoping,[status(thm)],[f53])).
% 127.93/16.87 fof(f126,plain,(
% 127.93/16.87 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X2,X3)|between(X1,X2,X3))),
% 127.93/16.87 inference(cnf_transformation,[status(thm)],[f125])).
% 127.93/16.87 fof(f127,plain,(
% 127.93/16.87 between(u,v,w)),
% 127.93/16.87 inference(cnf_transformation,[status(thm)],[f54])).
% 127.93/16.87 fof(f128,plain,(
% 127.93/16.87 between(v,w,x)),
% 127.93/16.87 inference(cnf_transformation,[status(thm)],[f55])).
% 127.93/16.87 fof(f129,plain,(
% 127.93/16.87 ~v=w),
% 127.93/16.87 inference(cnf_transformation,[status(thm)],[f56])).
% 127.93/16.87 fof(f130,plain,(
% 127.93/16.87 ~between(u,w,x)),
% 127.93/16.87 inference(cnf_transformation,[status(thm)],[f57])).
% 127.93/16.87 fof(f158,definition,(
% 127.93/16.87 sQ3_spl <=> (v=w)),
% 127.93/16.87 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 127.93/16.87 fof(f159,plain,(
% 127.93/16.87 v=w|~sQ3_spl),
% 127.93/16.87 inference(component_clause,[status(thm)],[f158])).
% 127.93/16.87 fof(f168,plain,(
% 127.93/16.87 $false|~sQ3_spl),
% 127.93/16.87 inference(forward_subsumption_resolution,[status(thm)],[f159,f129])).
% 127.93/16.87 fof(f169,plain,(
% 127.93/16.87 ~sQ3_spl),
% 127.93/16.87 inference(contradiction_clause,[status(thm)],[f168])).
% 127.93/16.87 fof(f245,plain,(
% 127.93/16.87 ![X0]: (~between(u,w,X0)|between(v,w,X0))),
% 127.93/16.87 inference(resolution,[status(thm)],[f127,f126])).
% 127.93/16.87 fof(f413,plain,(
% 127.93/16.87 ![X0,X1,X2,X3]: (equidistant(X0,X1,X2,extension(X3,X2,X0,X1)))),
% 127.93/16.87 inference(resolution,[status(thm)],[f82,f64])).
% 127.93/16.87 fof(f674,plain,(
% 127.93/16.87 ![X0,X1]: (between(v,w,extension(u,w,X0,X1)))),
% 127.93/16.87 inference(resolution,[status(thm)],[f245,f63])).
% 127.93/16.87 fof(f836,plain,(
% 127.93/16.87 ![X0]: (~between(v,w,X0)|~equidistant(w,x,w,X0)|v=w|x=X0)),
% 127.93/16.87 inference(resolution,[status(thm)],[f103,f128])).
% 127.93/16.87 fof(f859,definition,(
% 127.93/16.87 ![X0]: (sQ26_spl <=> (~between(v,w,X0)|~equidistant(w,x,w,X0)|x=X0))),
% 127.93/16.87 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 127.93/16.87 fof(f860,plain,(
% 127.93/16.87 ![X0]: (~between(v,w,X0)|~equidistant(w,x,w,X0)|x=X0|~sQ26_spl)),
% 127.93/16.87 inference(component_clause,[status(thm)],[f859])).
% 127.93/16.87 fof(f862,plain,(
% 127.93/16.87 sQ26_spl|sQ3_spl),
% 127.93/16.87 inference(split_clause,[status(thm)],[f836,f859,f158])).
% 127.93/16.87 fof(f1981,plain,(
% 127.93/16.87 ![X0]: (~between(v,w,extension(X0,w,w,x))|x=extension(X0,w,w,x)|~sQ26_spl)),
% 110.84/16.91 inference(resolution,[status(thm)],[f413,f860])).
% 110.84/16.91 fof(f29321,plain,(
% 110.84/16.91 x=extension(u,w,w,x)|~sQ26_spl),
% 110.84/16.91 inference(resolution,[status(thm)],[f1981,f674])).
% 110.84/16.91 fof(f29516,plain,(
% 110.84/16.91 between(u,w,x)|~sQ26_spl),
% 110.84/16.91 inference(paramodulation,[status(thm)],[f29321,f63])).
% 110.84/16.91 fof(f29834,plain,(
% 110.84/16.91 $false|~sQ26_spl),
% 110.84/16.91 inference(forward_subsumption_resolution,[status(thm)],[f29516,f130])).
% 110.84/16.91 fof(f29835,plain,(
% 110.84/16.91 ~sQ26_spl),
% 110.84/16.91 inference(contradiction_clause,[status(thm)],[f29834])).
% 110.84/16.91 fof(f29836,plain,(
% 110.84/16.91 $false),
% 110.84/16.91 inference(sat_refutation,[status(thm)],[f169,f862,f29835])).
% 110.84/16.91 % SZS output end CNFRefutation for theBenchmark.p
% 110.84/16.92 % Elapsed time: 16.534828 seconds
% 110.84/16.92 % CPU time: 131.013316 seconds
% 110.84/16.92 % Total memory used: 337.618 MB
% 110.84/16.92 % Net memory used: 302.327 MB
%------------------------------------------------------------------------------