%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO523+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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 66.35s 13.96s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO523+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.40 % Computer : n010.cluster.edu
% 0.09/5.40 % Model : x86_64 x86_64
% 0.09/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.40 % Memory : 8046.5625MB
% 0.09/5.40 % OS : Linux 6.8.0-71-generic
% 0.09/5.40 % CPULimit : 300
% 0.09/5.40 % WCLimit : 300
% 0.09/5.40 % DateTime : Sun Sep 20 17:12:30 UTC 2026
% 0.09/5.40 % CPUTime :
% 0.09/5.43 % Drodi V4.1.1
% 66.35/13.96 % Refutation found
% 66.35/13.96 % SZS status Theorem for theBenchmark: Theorem is valid
% 66.35/13.96 % SZS output start CNFRefutation for theBenchmark
% 66.35/13.96 fof(f98,axiom,(
% 66.35/13.96 (! [Xp,Xa,Xq] :( ~ s_m(Xp,Xa,Xq)| Xq = s(Xa,Xp) ) )),
% 66.35/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.35/13.96 fof(f99,axiom,(
% 66.35/13.96 (! [Xa,Xp] : s(Xa,s(Xa,Xp)) = Xp )),
% 66.35/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.35/13.96 fof(f110,axiom,(
% 66.35/13.96 (! [Xa,Xp,Xb] :( s(Xa,Xp) != s(Xb,Xp)| Xa = Xb ) )),
% 66.35/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.35/13.96 fof(f146,axiom,(
% 66.35/13.96 (! [Xa,Xb] : s_m(Xa,midpoint(Xa,Xb),Xb) )),
% 66.35/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.35/13.96 fof(f154,axiom,(
% 66.35/13.96 (! [Xa,Xb,Xp,Xq] :( ~ perp(Xa,Xb,Xp,Xq)| perp(Xa,Xb,Xq,Xp) ) )),
% 66.35/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.35/13.96 fof(f184,axiom,(
% 66.35/13.96 (! [Xa,Xb,Xp] :( ( Xa = Xb| s_col(Xa,Xb,midpoint(Xp,reflect(Xa,Xb,Xp))) )& ( Xa = Xb| Xp = reflect(Xa,Xb,Xp)| perp(Xa,Xb,Xp,reflect(Xa,Xb,Xp)) ) ) )),
% 66.35/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.35/13.96 fof(f185,axiom,(
% 66.35/13.96 (! [Xa,Xb,Xp,Xp1] :( ( Xa = Xb| ~ s_col(Xa,Xb,midpoint(Xp,Xp1))| ~ perp(Xa,Xb,Xp,Xp1)| Xp1 = reflect(Xa,Xb,Xp) )& ( Xa = Xb| ~ s_col(Xa,Xb,midpoint(Xp,Xp1))| Xp != Xp1| Xp1 = reflect(Xa,Xb,Xp) ) ) )),
% 66.35/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.35/13.96 fof(f186,conjecture,(
% 66.35/13.96 (! [Xa,Xb,Xp,Xp1] :( Xa = Xb| reflect(Xa,Xb,Xp) != Xp1| reflect(Xa,Xb,Xp1) = Xp ) )),
% 66.35/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.35/13.96 fof(f187,negated_conjecture,(
% 66.35/13.96 ~((! [Xa,Xb,Xp,Xp1] :( Xa = Xb| reflect(Xa,Xb,Xp) != Xp1| reflect(Xa,Xb,Xp1) = Xp ) ))),
% 66.35/13.96 inference(negated_conjecture,[status(cth)],[f186])).
% 66.35/13.96 fof(f366,plain,(
% 66.35/13.96 ![X0,X1,X2]: (~s_m(X0,X1,X2)|X2=s(X1,X0))),
% 66.35/13.96 inference(cnf_transformation,[status(thm)],[f98])).
% 66.35/13.96 fof(f367,plain,(
% 66.35/13.96 ![X0,X1]: (s(X0,s(X0,X1))=X1)),
% 66.35/13.96 inference(cnf_transformation,[status(thm)],[f99])).
% 66.35/13.96 fof(f385,plain,(
% 66.35/13.96 ![Xa,Xb]: ((![Xp]: ~s(Xa,Xp)=s(Xb,Xp))|Xa=Xb)),
% 66.35/13.96 inference(miniscoping,[status(thm)],[f110])).
% 66.35/13.96 fof(f386,plain,(
% 66.35/13.96 ![X0,X1,X2]: (~s(X0,X1)=s(X2,X1)|X0=X2)),
% 66.35/13.96 inference(cnf_transformation,[status(thm)],[f385])).
% 66.35/13.96 fof(f458,plain,(
% 66.35/13.96 ![X0,X1]: (s_m(X0,midpoint(X0,X1),X1))),
% 66.35/13.96 inference(cnf_transformation,[status(thm)],[f146])).
% 66.35/13.96 fof(f473,plain,(
% 66.35/13.96 ![X0,X1,X2,X3]: (~perp(X0,X1,X2,X3)|perp(X0,X1,X3,X2))),
% 66.35/13.96 inference(cnf_transformation,[status(thm)],[f154])).
% 66.35/13.96 fof(f526,plain,(
% 66.35/13.96 (![Xa,Xb]: (Xa=Xb|(![Xp]: s_col(Xa,Xb,midpoint(Xp,reflect(Xa,Xb,Xp))))))&(![Xa,Xb,Xp]: ((Xa=Xb|Xp=reflect(Xa,Xb,Xp))|perp(Xa,Xb,Xp,reflect(Xa,Xb,Xp))))),
% 66.35/13.96 inference(miniscoping,[status(thm)],[f184])).
% 66.35/13.96 fof(f527,plain,(
% 66.35/13.96 ![X0,X1,X2]: (X0=X1|s_col(X0,X1,midpoint(X2,reflect(X0,X1,X2))))),
% 66.35/13.96 inference(cnf_transformation,[status(thm)],[f526])).
% 66.35/13.96 fof(f528,plain,(
% 66.35/13.96 ![X0,X1,X2]: (X0=X1|X2=reflect(X0,X1,X2)|perp(X0,X1,X2,reflect(X0,X1,X2)))),
% 66.35/13.96 inference(cnf_transformation,[status(thm)],[f526])).
% 66.35/13.96 fof(f529,plain,(
% 66.35/13.96 (![Xa,Xb,Xp,Xp1]: (((Xa=Xb|~s_col(Xa,Xb,midpoint(Xp,Xp1)))|~perp(Xa,Xb,Xp,Xp1))|Xp1=reflect(Xa,Xb,Xp)))&(![Xa,Xb,Xp,Xp1]: (((Xa=Xb|~s_col(Xa,Xb,midpoint(Xp,Xp1)))|~Xp=Xp1)|Xp1=reflect(Xa,Xb,Xp)))),
% 66.35/13.96 inference(miniscoping,[status(thm)],[f185])).
% 66.35/13.96 fof(f530,plain,(
% 66.35/13.96 ![X0,X1,X2,X3]: (X0=X1|~s_col(X0,X1,midpoint(X2,X3))|~perp(X0,X1,X2,X3)|X3=reflect(X0,X1,X2))),
% 66.35/13.96 inference(cnf_transformation,[status(thm)],[f529])).
% 66.35/13.96 fof(f532,plain,(
% 66.35/13.96 (?[Xa,Xb,Xp,Xp1]: ((~Xa=Xb&reflect(Xa,Xb,Xp)=Xp1)&~reflect(Xa,Xb,Xp1)=Xp))),
% 66.35/13.96 inference(pre_NNF_transformation,[status(thm)],[f187])).
% 66.35/13.96 fof(f533,plain,(
% 66.35/13.96 ((~sK0_skl=sK1_skl&reflect(sK0_skl,sK1_skl,sK2_skl)=sK3_skl)&~reflect(sK0_skl,sK1_skl,sK3_skl)=sK2_skl)),
% 66.35/13.96 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(Xa,sK0_skl),skolemize(Xb,sK1_skl),skolemize(Xp,sK2_skl),skolemize(Xp1,sK3_skl)],[f532])).
% 66.35/13.96 fof(f534,plain,(
% 66.35/13.96 ~sK0_skl=sK1_skl),
% 66.35/13.96 inference(cnf_transformation,[status(thm)],[f533])).
% 66.35/13.96 fof(f535,plain,(
% 66.35/13.96 reflect(sK0_skl,sK1_skl,sK2_skl)=sK3_skl),
% 66.35/13.96 inference(cnf_transformation,[status(thm)],[f533])).
% 66.35/13.96 fof(f536,plain,(
% 66.35/13.96 ~reflect(sK0_skl,sK1_skl,sK3_skl)=sK2_skl),
% 66.35/13.96 inference(cnf_transformation,[status(thm)],[f533])).
% 66.35/13.96 fof(f861,plain,(
% 66.35/13.99 ![X0,X1]: (X0=s(midpoint(X1,X0),X1))),
% 66.35/13.99 inference(resolution,[status(thm)],[f366,f458])).
% 66.35/13.99 fof(f884,plain,(
% 66.35/13.99 ![X0,X1]: (s(midpoint(X0,X1),X1)=X0)),
% 66.35/13.99 inference(paramodulation,[status(thm)],[f861,f367])).
% 66.35/13.99 fof(f1044,plain,(
% 66.35/13.99 ![X0,X1]: (midpoint(s(X0,X1),X1)=X0)),
% 66.35/13.99 inference(resolution,[status(thm)],[f386,f884])).
% 66.35/13.99 fof(f1077,plain,(
% 66.35/13.99 ![X0,X1]: (midpoint(X0,X1)=midpoint(X1,X0))),
% 66.35/13.99 inference(paramodulation,[status(thm)],[f861,f1044])).
% 66.35/13.99 fof(f2029,plain,(
% 66.35/13.99 ![X0,X1,X2]: (perp(X0,X1,reflect(X0,X1,X2),X2)|X0=X1|X2=reflect(X0,X1,X2))),
% 66.35/13.99 inference(resolution,[status(thm)],[f473,f528])).
% 66.35/13.99 fof(f2831,plain,(
% 66.35/13.99 ![X0,X1,X2]: (X0=X1|~s_col(X0,X1,midpoint(reflect(X0,X1,X2),X2))|X2=reflect(X0,X1,reflect(X0,X1,X2))|X0=X1|X2=reflect(X0,X1,X2))),
% 66.35/13.99 inference(resolution,[status(thm)],[f530,f2029])).
% 66.35/13.99 fof(f2842,plain,(
% 66.35/13.99 ![X0,X1,X2]: (X0=X1|~s_col(X0,X1,midpoint(reflect(X0,X1,X2),X2))|X2=reflect(X0,X1,reflect(X0,X1,X2))|X2=reflect(X0,X1,X2))),
% 66.35/13.99 inference(duplicate_literals_removal,[status(thm)],[f2831])).
% 66.35/13.99 fof(f6710,plain,(
% 66.35/13.99 ![X0,X1,X2]: (X0=X1|~s_col(X0,X1,midpoint(X2,reflect(X0,X1,X2)))|X2=reflect(X0,X1,reflect(X0,X1,X2))|X2=reflect(X0,X1,X2))),
% 66.35/13.99 inference(paramodulation,[status(thm)],[f1077,f2842])).
% 66.35/13.99 fof(f6718,plain,(
% 66.35/13.99 ![X0,X1,X2]: (X0=X1|X2=reflect(X0,X1,reflect(X0,X1,X2))|X2=reflect(X0,X1,X2))),
% 66.35/13.99 inference(forward_subsumption_resolution,[status(thm)],[f6710,f527])).
% 66.35/13.99 fof(f6882,plain,(
% 66.35/13.99 sK0_skl=sK1_skl|sK2_skl=reflect(sK0_skl,sK1_skl,sK3_skl)|sK2_skl=reflect(sK0_skl,sK1_skl,sK2_skl)),
% 66.35/13.99 inference(paramodulation,[status(thm)],[f535,f6718])).
% 66.35/13.99 fof(f6967,plain,(
% 66.35/13.99 sK0_skl=sK1_skl|sK2_skl=reflect(sK0_skl,sK1_skl,sK3_skl)|sK2_skl=sK3_skl),
% 66.35/13.99 inference(forward_demodulation,[status(thm)],[f535,f6882])).
% 66.35/13.99 fof(f6968,plain,(
% 66.35/13.99 sK2_skl=reflect(sK0_skl,sK1_skl,sK3_skl)|sK2_skl=sK3_skl),
% 66.35/13.99 inference(forward_subsumption_resolution,[status(thm)],[f6967,f534])).
% 66.35/13.99 fof(f7146,plain,(
% 66.35/13.99 ~reflect(sK0_skl,sK1_skl,sK2_skl)=sK2_skl),
% 66.35/13.99 inference(backward_demodulation,[status(thm)],[f7148,f536])).
% 66.35/13.99 fof(f7147,plain,(
% 66.35/13.99 reflect(sK0_skl,sK1_skl,sK2_skl)=sK2_skl),
% 66.35/13.99 inference(backward_demodulation,[status(thm)],[f7148,f535])).
% 66.35/13.99 fof(f7148,plain,(
% 66.35/13.99 sK2_skl=sK3_skl),
% 66.35/13.99 inference(forward_subsumption_resolution,[status(thm)],[f6968,f536])).
% 66.35/13.99 fof(f7246,plain,(
% 66.35/13.99 $false),
% 66.35/13.99 inference(forward_subsumption_resolution,[status(thm)],[f7147,f7146])).
% 66.35/13.99 % SZS output end CNFRefutation for theBenchmark.p
% 66.35/14.01 % Elapsed time: 8.592821 seconds
% 66.35/14.01 % CPU time: 67.946643 seconds
% 66.35/14.01 % Total memory used: 297.269 MB
% 66.35/14.01 % Net memory used: 260.933 MB
%------------------------------------------------------------------------------