%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO526+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:26:35 PM UTC 2026
% Result : Theorem 28.36s 4.22s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO526+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.58 % Computer : n006.cluster.edu
% 0.10/0.58 % Model : x86_64 x86_64
% 0.10/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.58 % Memory : 8046.5625MB
% 0.10/0.58 % OS : Linux 6.8.0-71-generic
% 0.10/0.58 % CPULimit : 300
% 0.10/0.58 % WCLimit : 300
% 0.10/0.58 % DateTime : Sun Sep 20 17:12:27 UTC 2026
% 0.10/0.58 % CPUTime :
% 0.10/0.61 % Drodi V4.1.1
% 28.36/4.22 % Refutation found
% 28.36/4.22 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.36/4.22 % SZS output start CNFRefutation for theBenchmark
% 28.36/4.22 fof(f11,axiom,(
% 28.36/4.22 (! [Xa,Xb,Xc,Xd,Xe,Xf] :( ~ s_e(Xa,Xb,Xc,Xd)| ~ s_e(Xc,Xd,Xe,Xf)| s_e(Xa,Xb,Xe,Xf) ) )),
% 28.36/4.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.36/4.22 fof(f98,axiom,(
% 28.36/4.22 (! [Xp,Xa,Xq] :( ~ s_m(Xp,Xa,Xq)| Xq = s(Xa,Xp) ) )),
% 28.36/4.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.36/4.22 fof(f120,axiom,(
% 28.36/4.22 (! [Xa,Xb,Xc] :( ~ s_r(Xa,Xb,Xc)| s_r(Xa,Xb,s(Xb,Xc)) ) )),
% 28.36/4.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.36/4.22 fof(f146,axiom,(
% 28.36/4.22 (! [Xa,Xb] : s_m(Xa,midpoint(Xa,Xb),Xb) )),
% 28.36/4.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.36/4.22 fof(f194,axiom,(
% 28.36/4.22 (! [Xa,Xb,Xc,Xa1] :( ~ s_r(Xa,Xb,Xc)| ~ s_r(Xa1,Xb,Xc)| ~ s_e(Xa,Xb,Xa1,Xb)| s_e(Xa,Xc,Xa1,Xc) ) )),
% 28.36/4.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.36/4.22 fof(f195,conjecture,(
% 28.36/4.22 (! [Xa,Xb,Xc,Xa1,Xc1] :( ~ s_r(Xa,Xb,Xc)| ~ s_r(Xa1,Xb,Xc1)| ~ s_e(Xa,Xb,Xa1,Xb)| ~ s_e(Xb,Xc,Xb,Xc1)| s_e(Xa,Xc,Xa1,Xc1)| Xb != midpoint(Xc,Xc1)| Xc = Xc1 ) )),
% 28.36/4.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.36/4.22 fof(f196,negated_conjecture,(
% 28.36/4.22 ~((! [Xa,Xb,Xc,Xa1,Xc1] :( ~ s_r(Xa,Xb,Xc)| ~ s_r(Xa1,Xb,Xc1)| ~ s_e(Xa,Xb,Xa1,Xb)| ~ s_e(Xb,Xc,Xb,Xc1)| s_e(Xa,Xc,Xa1,Xc1)| Xb != midpoint(Xc,Xc1)| Xc = Xc1 ) ))),
% 28.36/4.22 inference(negated_conjecture,[status(cth)],[f195])).
% 28.36/4.22 fof(f207,axiom,(
% 28.36/4.22 (! [Xa,Xb,Xc] :( ( ~ s_r(Xa,Xb,Xc)| s_e(Xa,Xc,Xa,s(Xb,Xc)) )& ( s_r(Xa,Xb,Xc)| ~ s_e(Xa,Xc,Xa,s(Xb,Xc)) ) ) )),
% 28.36/4.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.36/4.22 fof(f231,plain,(
% 28.36/4.22 ![Xa,Xb,Xe,Xf]: ((![Xc,Xd]: (~s_e(Xa,Xb,Xc,Xd)|~s_e(Xc,Xd,Xe,Xf)))|s_e(Xa,Xb,Xe,Xf))),
% 28.36/4.22 inference(miniscoping,[status(thm)],[f11])).
% 28.36/4.22 fof(f232,plain,(
% 28.36/4.22 ![X0,X1,X2,X3,X4,X5]: (~s_e(X0,X1,X2,X3)|~s_e(X2,X3,X4,X5)|s_e(X0,X1,X4,X5))),
% 28.36/4.22 inference(cnf_transformation,[status(thm)],[f231])).
% 28.36/4.22 fof(f375,plain,(
% 28.36/4.22 ![X0,X1,X2]: (~s_m(X0,X1,X2)|X2=s(X1,X0))),
% 28.36/4.22 inference(cnf_transformation,[status(thm)],[f98])).
% 28.36/4.22 fof(f411,plain,(
% 28.36/4.22 ![X0,X1,X2]: (~s_r(X0,X1,X2)|s_r(X0,X1,s(X1,X2)))),
% 28.36/4.22 inference(cnf_transformation,[status(thm)],[f120])).
% 28.36/4.22 fof(f467,plain,(
% 28.36/4.22 ![X0,X1]: (s_m(X0,midpoint(X0,X1),X1))),
% 28.36/4.22 inference(cnf_transformation,[status(thm)],[f146])).
% 28.36/4.22 fof(f553,plain,(
% 28.36/4.22 ![Xa,Xc,Xa1]: ((![Xb]: ((~s_r(Xa,Xb,Xc)|~s_r(Xa1,Xb,Xc))|~s_e(Xa,Xb,Xa1,Xb)))|s_e(Xa,Xc,Xa1,Xc))),
% 28.36/4.22 inference(miniscoping,[status(thm)],[f194])).
% 28.36/4.22 fof(f554,plain,(
% 28.36/4.22 ![X0,X1,X2,X3]: (~s_r(X0,X1,X2)|~s_r(X3,X1,X2)|~s_e(X0,X1,X3,X1)|s_e(X0,X2,X3,X2))),
% 28.36/4.22 inference(cnf_transformation,[status(thm)],[f553])).
% 28.36/4.22 fof(f555,plain,(
% 28.36/4.22 (?[Xa,Xb,Xc,Xa1,Xc1]: ((((((s_r(Xa,Xb,Xc)&s_r(Xa1,Xb,Xc1))&s_e(Xa,Xb,Xa1,Xb))&s_e(Xb,Xc,Xb,Xc1))&~s_e(Xa,Xc,Xa1,Xc1))&Xb=midpoint(Xc,Xc1))&~Xc=Xc1))),
% 28.36/4.22 inference(pre_NNF_transformation,[status(thm)],[f196])).
% 28.36/4.22 fof(f556,plain,(
% 28.36/4.22 ?[Xc,Xc1]: ((?[Xb]: ((?[Xa,Xa1]: ((((s_r(Xa,Xb,Xc)&s_r(Xa1,Xb,Xc1))&s_e(Xa,Xb,Xa1,Xb))&s_e(Xb,Xc,Xb,Xc1))&~s_e(Xa,Xc,Xa1,Xc1)))&Xb=midpoint(Xc,Xc1)))&~Xc=Xc1)),
% 28.36/4.22 inference(miniscoping,[status(thm)],[f555])).
% 28.36/4.22 fof(f557,plain,(
% 28.36/4.22 ((((((s_r(sK3_skl,sK2_skl,sK0_skl)&s_r(sK4_skl,sK2_skl,sK1_skl))&s_e(sK3_skl,sK2_skl,sK4_skl,sK2_skl))&s_e(sK2_skl,sK0_skl,sK2_skl,sK1_skl))&~s_e(sK3_skl,sK0_skl,sK4_skl,sK1_skl))&sK2_skl=midpoint(sK0_skl,sK1_skl))&~sK0_skl=sK1_skl)),
% 28.36/4.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl]),skolemize(Xc,sK0_skl),skolemize(Xc1,sK1_skl),skolemize(Xb,sK2_skl),skolemize(Xa,sK3_skl),skolemize(Xa1,sK4_skl)],[f556])).
% 28.36/4.22 fof(f558,plain,(
% 28.36/4.22 s_r(sK3_skl,sK2_skl,sK0_skl)),
% 28.36/4.22 inference(cnf_transformation,[status(thm)],[f557])).
% 28.36/4.22 fof(f559,plain,(
% 28.36/4.22 s_r(sK4_skl,sK2_skl,sK1_skl)),
% 28.36/4.22 inference(cnf_transformation,[status(thm)],[f557])).
% 28.36/4.22 fof(f560,plain,(
% 28.36/4.22 s_e(sK3_skl,sK2_skl,sK4_skl,sK2_skl)),
% 28.36/4.22 inference(cnf_transformation,[status(thm)],[f557])).
% 28.36/4.22 fof(f562,plain,(
% 28.36/4.22 ~s_e(sK3_skl,sK0_skl,sK4_skl,sK1_skl)),
% 28.36/4.22 inference(cnf_transformation,[status(thm)],[f557])).
% 28.36/4.22 fof(f563,plain,(
% 28.36/4.22 sK2_skl=midpoint(sK0_skl,sK1_skl)),
% 28.36/4.22 inference(cnf_transformation,[status(thm)],[f557])).
% 28.36/4.22 fof(f620,plain,(
% 28.36/4.22 (![Xa,Xb,Xc]: (~s_r(Xa,Xb,Xc)|s_e(Xa,Xc,Xa,s(Xb,Xc))))&(![Xa,Xb,Xc]: (s_r(Xa,Xb,Xc)|~s_e(Xa,Xc,Xa,s(Xb,Xc))))),
% 28.36/4.23 inference(miniscoping,[status(thm)],[f207])).
% 28.36/4.23 fof(f621,plain,(
% 28.36/4.23 ![X0,X1,X2]: (~s_r(X0,X1,X2)|s_e(X0,X2,X0,s(X1,X2)))),
% 28.36/4.23 inference(cnf_transformation,[status(thm)],[f620])).
% 28.36/4.23 fof(f808,plain,(
% 28.36/4.23 ![X0,X1]: (~s_e(sK3_skl,sK0_skl,X0,X1)|~s_e(X0,X1,sK4_skl,sK1_skl))),
% 28.36/4.23 inference(resolution,[status(thm)],[f232,f562])).
% 28.36/4.23 fof(f1684,plain,(
% 28.36/4.23 s_r(sK3_skl,sK2_skl,s(sK2_skl,sK0_skl))),
% 28.36/4.23 inference(resolution,[status(thm)],[f411,f558])).
% 28.36/4.23 fof(f2416,plain,(
% 28.36/4.23 s_m(sK0_skl,sK2_skl,sK1_skl)),
% 28.36/4.23 inference(paramodulation,[status(thm)],[f563,f467])).
% 28.36/4.23 fof(f3120,plain,(
% 28.36/4.23 sK1_skl=s(sK2_skl,sK0_skl)),
% 28.36/4.23 inference(resolution,[status(thm)],[f2416,f375])).
% 28.36/4.23 fof(f3122,plain,(
% 28.36/4.23 s_r(sK3_skl,sK2_skl,sK1_skl)),
% 28.36/4.23 inference(backward_demodulation,[status(thm)],[f3120,f1684])).
% 28.36/4.23 fof(f3224,plain,(
% 28.36/4.23 ![X0]: (~s_r(X0,sK2_skl,sK1_skl)|~s_e(X0,sK2_skl,sK4_skl,sK2_skl)|s_e(X0,sK1_skl,sK4_skl,sK1_skl))),
% 28.36/4.23 inference(resolution,[status(thm)],[f554,f559])).
% 28.36/4.23 fof(f3677,plain,(
% 28.36/4.23 s_e(sK3_skl,sK0_skl,sK3_skl,s(sK2_skl,sK0_skl))),
% 28.36/4.23 inference(resolution,[status(thm)],[f621,f558])).
% 28.36/4.23 fof(f3685,plain,(
% 28.36/4.23 s_e(sK3_skl,sK0_skl,sK3_skl,sK1_skl)),
% 28.36/4.23 inference(forward_demodulation,[status(thm)],[f3120,f3677])).
% 28.36/4.23 fof(f3699,plain,(
% 28.36/4.23 ~s_e(sK3_skl,sK1_skl,sK4_skl,sK1_skl)),
% 28.36/4.23 inference(resolution,[status(thm)],[f3685,f808])).
% 28.36/4.23 fof(f3908,plain,(
% 28.36/4.23 ~s_e(sK3_skl,sK2_skl,sK4_skl,sK2_skl)|s_e(sK3_skl,sK1_skl,sK4_skl,sK1_skl)),
% 28.36/4.23 inference(resolution,[status(thm)],[f3224,f3122])).
% 28.36/4.23 fof(f3912,plain,(
% 28.36/4.23 s_e(sK3_skl,sK1_skl,sK4_skl,sK1_skl)),
% 28.36/4.23 inference(forward_subsumption_resolution,[status(thm)],[f3908,f560])).
% 28.36/4.23 fof(f3913,plain,(
% 28.36/4.23 $false),
% 28.36/4.23 inference(backward_subsumption_resolution,[status(thm)],[f3699,f3912])).
% 28.36/4.23 % SZS output end CNFRefutation for theBenchmark.p
% 28.36/4.25 % Elapsed time: 3.647356 seconds
% 28.36/4.25 % CPU time: 28.649163 seconds
% 28.36/4.25 % Total memory used: 201.954 MB
% 28.36/4.25 % Net memory used: 181.718 MB
%------------------------------------------------------------------------------