%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO009-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 17.27s 2.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO009-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n006.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 08:14:44 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 17.27/2.66 % Refutation found
% 17.27/2.66 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 17.27/2.66 % SZS output start CNFRefutation for theBenchmark
% 17.27/2.66 fof(f32,axiom,(
% 17.27/2.66 (![U,V]: (between(U,V,reflection(U,V)) ))),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f34,axiom,(
% 17.27/2.66 (![U,V]: (( U != V| V = reflection(U,V) ) ))),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f36,axiom,(
% 17.27/2.66 (![V,U]: (( V != reflection(U,V)| U = V ) ))),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f47,axiom,(
% 17.27/2.66 (![U,V,W]: (( ~ between(U,V,W)| between(W,V,U) ) ))),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f48,axiom,(
% 17.27/2.66 (![U,V]: (between(U,U,V) ))),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f54,axiom,(
% 17.27/2.66 (![U,V,W,X]: (( ~ between(U,V,W)| ~ between(U,W,X)| between(V,W,X) ) ))),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f58,axiom,(
% 17.27/2.66 (![U,V,W,X]: (( ~ between(U,V,W)| ~ between(U,W,X)| between(U,V,X) ) ))),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f78,axiom,(
% 17.27/2.66 (![U,V,W,X]: (( ~ between(U,V,W)| ~ between(U,V,X)| U = V| between(V,W,X)| between(V,X,W) ) ))),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f80,hypothesis,(
% 17.27/2.66 between(a,c,e) ),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f81,hypothesis,(
% 17.27/2.66 between(a,d,e) ),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f82,hypothesis,(
% 17.27/2.66 ~ between(a,c,d) ),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f83,negated_conjecture,(
% 17.27/2.66 ~ between(a,d,c) ),
% 17.27/2.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.27/2.66 fof(f121,plain,(
% 17.27/2.66 ![X0,X1]: (between(X0,X1,reflection(X0,X1)))),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f32])).
% 17.27/2.66 fof(f123,plain,(
% 17.27/2.66 ![X0,X1]: (~X0=X1|X1=reflection(X0,X1))),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f34])).
% 17.27/2.66 fof(f125,plain,(
% 17.27/2.66 ![X0,X1]: (~X0=reflection(X1,X0)|X1=X0)),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f36])).
% 17.27/2.66 fof(f140,plain,(
% 17.27/2.66 ![X0,X1,X2]: (~between(X0,X1,X2)|between(X2,X1,X0))),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f47])).
% 17.27/2.66 fof(f141,plain,(
% 17.27/2.66 ![X0,X1]: (between(X0,X0,X1))),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f48])).
% 17.27/2.66 fof(f152,plain,(
% 17.27/2.66 ![V,W,X]: ((![U]: (~between(U,V,W)|~between(U,W,X)))|between(V,W,X))),
% 17.27/2.66 inference(miniscoping,[status(thm)],[f54])).
% 17.27/2.66 fof(f153,plain,(
% 17.27/2.66 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X2,X3)|between(X1,X2,X3))),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f152])).
% 17.27/2.66 fof(f160,plain,(
% 17.27/2.66 ![U,V,X]: ((![W]: (~between(U,V,W)|~between(U,W,X)))|between(U,V,X))),
% 17.27/2.66 inference(miniscoping,[status(thm)],[f58])).
% 17.27/2.66 fof(f161,plain,(
% 17.27/2.66 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X2,X3)|between(X0,X1,X3))),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f160])).
% 17.27/2.66 fof(f190,plain,(
% 17.27/2.66 ![V,W,X]: (((![U]: ((~between(U,V,W)|~between(U,V,X))|U=V))|between(V,W,X))|between(V,X,W))),
% 17.27/2.66 inference(miniscoping,[status(thm)],[f78])).
% 17.27/2.66 fof(f191,plain,(
% 17.27/2.66 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X1,X3)|X0=X1|between(X1,X2,X3)|between(X1,X3,X2))),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f190])).
% 17.27/2.66 fof(f194,plain,(
% 17.27/2.66 between(a,c,e)),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f80])).
% 17.27/2.66 fof(f195,plain,(
% 17.27/2.66 between(a,d,e)),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f81])).
% 17.27/2.66 fof(f196,plain,(
% 17.27/2.66 ~between(a,c,d)),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f82])).
% 17.27/2.66 fof(f197,plain,(
% 17.27/2.66 ~between(a,d,c)),
% 17.27/2.66 inference(cnf_transformation,[status(thm)],[f83])).
% 17.27/2.66 fof(f199,plain,(
% 17.27/2.66 ![X0]: (X0=reflection(X0,X0))),
% 17.27/2.66 inference(destructive_equality_resolution,[status(thm)],[f123])).
% 17.27/2.66 fof(f406,plain,(
% 17.27/2.66 ![X0]: (~between(a,d,X0)|~between(a,X0,c))),
% 17.27/2.66 inference(resolution,[status(thm)],[f161,f197])).
% 17.27/2.66 fof(f448,plain,(
% 17.27/2.66 ![X0,X1,X2]: (~between(X0,X1,X2)|between(X1,X2,reflection(X0,X2)))),
% 17.27/2.66 inference(resolution,[status(thm)],[f121,f153])).
% 17.27/2.66 fof(f469,plain,(
% 17.27/2.66 between(e,c,a)),
% 17.27/2.66 inference(resolution,[status(thm)],[f194,f140])).
% 17.27/2.66 fof(f480,plain,(
% 17.27/2.66 between(e,d,a)),
% 17.27/2.66 inference(resolution,[status(thm)],[f195,f140])).
% 17.27/2.66 fof(f621,plain,(
% 17.27/2.67 ~between(a,e,c)),
% 17.27/2.67 inference(resolution,[status(thm)],[f406,f195])).
% 17.27/2.67 fof(f635,plain,(
% 17.27/2.67 ![X0]: (~between(a,e,X0)|~between(a,X0,c))),
% 17.27/2.67 inference(resolution,[status(thm)],[f621,f161])).
% 17.27/2.67 fof(f883,plain,(
% 17.27/2.67 ![X0]: (~between(X0,a,c)|~between(X0,a,d)|X0=a|between(a,d,c))),
% 17.27/2.67 inference(resolution,[status(thm)],[f191,f196])).
% 17.27/2.67 fof(f994,plain,(
% 17.27/2.67 ![X0]: (~between(X0,a,c)|~between(X0,a,d)|X0=a)),
% 17.27/2.67 inference(forward_subsumption_resolution,[status(thm)],[f883,f197])).
% 17.27/2.67 fof(f1853,plain,(
% 17.27/2.67 ~between(a,reflection(a,e),c)),
% 17.27/2.67 inference(resolution,[status(thm)],[f635,f121])).
% 17.27/2.67 fof(f3277,plain,(
% 17.27/2.67 between(d,a,reflection(e,a))),
% 17.27/2.67 inference(resolution,[status(thm)],[f448,f480])).
% 17.27/2.67 fof(f3279,plain,(
% 17.27/2.67 between(c,a,reflection(e,a))),
% 17.27/2.67 inference(resolution,[status(thm)],[f448,f469])).
% 17.27/2.67 fof(f3746,plain,(
% 17.27/2.67 between(reflection(e,a),a,d)),
% 17.27/2.67 inference(resolution,[status(thm)],[f3277,f140])).
% 17.27/2.67 fof(f3780,plain,(
% 17.27/2.67 between(reflection(e,a),a,c)),
% 17.27/2.67 inference(resolution,[status(thm)],[f3279,f140])).
% 17.27/2.67 fof(f4091,plain,(
% 17.27/2.67 ~between(reflection(e,a),a,d)|reflection(e,a)=a),
% 17.27/2.67 inference(resolution,[status(thm)],[f3780,f994])).
% 17.27/2.67 fof(f4127,plain,(
% 17.27/2.67 reflection(e,a)=a),
% 17.27/2.67 inference(forward_subsumption_resolution,[status(thm)],[f4091,f3746])).
% 17.27/2.67 fof(f4138,plain,(
% 17.27/2.67 e=a),
% 17.27/2.67 inference(resolution,[status(thm)],[f4127,f125])).
% 17.27/2.67 fof(f4181,plain,(
% 17.27/2.67 ~between(a,reflection(e,e),c)),
% 17.27/2.67 inference(backward_demodulation,[status(thm)],[f4138,f1853])).
% 17.27/2.67 fof(f4234,plain,(
% 17.27/2.67 ~between(e,reflection(e,e),c)),
% 17.27/2.67 inference(forward_demodulation,[status(thm)],[f4138,f4181])).
% 17.27/2.67 fof(f4235,plain,(
% 17.27/2.67 ~between(e,e,c)),
% 17.27/2.67 inference(forward_demodulation,[status(thm)],[f199,f4234])).
% 17.27/2.67 fof(f4236,plain,(
% 17.27/2.67 $false),
% 17.27/2.67 inference(forward_subsumption_resolution,[status(thm)],[f4235,f141])).
% 17.27/2.67 % SZS output end CNFRefutation for theBenchmark.p
% 17.27/2.68 % Elapsed time: 2.291437 seconds
% 17.27/2.68 % CPU time: 17.933807 seconds
% 17.27/2.68 % Total memory used: 175.702 MB
% 17.27/2.68 % Net memory used: 163.129 MB
%------------------------------------------------------------------------------