%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO504+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 : 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:26:34 PM UTC 2026
% Result : Theorem 1.30s 0.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO504+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.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 16:57:02 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 1.30/0.70 % Refutation found
% 1.30/0.70 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.30/0.70 % SZS output start CNFRefutation for theBenchmark
% 1.30/0.70 fof(f2,axiom,(
% 1.30/0.70 (! [X,Y,Z,V,Z2,V2] :( ~ s_e(X,Y,Z,V)| ~ s_e(X,Y,Z2,V2)| s_e(Z,V,Z2,V2) ) )),
% 1.30/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.30/0.70 fof(f18,axiom,(
% 1.30/0.70 (! [Xa,Xb,Xc,Xd] :( ~ s_e(Xa,Xb,Xc,Xd)| s_e(Xb,Xa,Xd,Xc) ) )),
% 1.30/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.30/0.70 fof(f99,axiom,(
% 1.30/0.70 (! [Xa,Xp] : s(Xa,s(Xa,Xp)) = Xp )),
% 1.30/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.30/0.70 fof(f104,axiom,(
% 1.30/0.70 (! [Xp,Xq,Xa] : s_e(Xp,Xq,s(Xa,Xp),s(Xa,Xq)) )),
% 1.30/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.30/0.70 fof(f107,axiom,(
% 1.30/0.70 (! [Xp,Xq,Xr,Xcs,Xa] :( ~ s_e(Xp,Xq,Xr,Xcs)| s_e(s(Xa,Xp),s(Xa,Xq),s(Xa,Xr),s(Xa,Xcs)) ) )),
% 1.30/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.30/0.70 fof(f118,conjecture,(
% 1.30/0.70 (! [Xa,Xb,Xc] :( ~ s_r(Xa,Xb,Xc)| s_r(Xc,Xb,Xa) ) )),
% 1.30/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.30/0.70 fof(f119,negated_conjecture,(
% 1.30/0.70 ~((! [Xa,Xb,Xc] :( ~ s_r(Xa,Xb,Xc)| s_r(Xc,Xb,Xa) ) ))),
% 1.30/0.70 inference(negated_conjecture,[status(cth)],[f118])).
% 1.30/0.70 fof(f130,axiom,(
% 1.30/0.70 (! [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)) ) ) )),
% 1.30/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.30/0.70 fof(f134,plain,(
% 1.30/0.70 ![Z,V,Z2,V2]: ((![X,Y]: (~s_e(X,Y,Z,V)|~s_e(X,Y,Z2,V2)))|s_e(Z,V,Z2,V2))),
% 1.30/0.70 inference(miniscoping,[status(thm)],[f2])).
% 1.30/0.70 fof(f135,plain,(
% 1.30/0.70 ![X0,X1,X2,X3,X4,X5]: (~s_e(X0,X1,X2,X3)|~s_e(X0,X1,X4,X5)|s_e(X2,X3,X4,X5))),
% 1.30/0.70 inference(cnf_transformation,[status(thm)],[f134])).
% 1.30/0.70 fof(f162,plain,(
% 1.30/0.70 ![X0,X1,X2,X3]: (~s_e(X0,X1,X2,X3)|s_e(X1,X0,X3,X2))),
% 1.30/0.70 inference(cnf_transformation,[status(thm)],[f18])).
% 1.30/0.70 fof(f297,plain,(
% 1.30/0.70 ![X0,X1]: (s(X0,s(X0,X1))=X1)),
% 1.30/0.70 inference(cnf_transformation,[status(thm)],[f99])).
% 1.30/0.70 fof(f304,plain,(
% 1.30/0.70 ![X0,X1,X2]: (s_e(X0,X1,s(X2,X0),s(X2,X1)))),
% 1.30/0.70 inference(cnf_transformation,[status(thm)],[f104])).
% 1.30/0.70 fof(f309,plain,(
% 1.30/0.70 ![Xp,Xq,Xr,Xcs]: (~s_e(Xp,Xq,Xr,Xcs)|(![Xa]: s_e(s(Xa,Xp),s(Xa,Xq),s(Xa,Xr),s(Xa,Xcs))))),
% 1.30/0.70 inference(miniscoping,[status(thm)],[f107])).
% 1.30/0.70 fof(f310,plain,(
% 1.30/0.70 ![X0,X1,X2,X3,X4]: (~s_e(X0,X1,X2,X3)|s_e(s(X4,X0),s(X4,X1),s(X4,X2),s(X4,X3)))),
% 1.30/0.70 inference(cnf_transformation,[status(thm)],[f309])).
% 1.30/0.70 fof(f329,plain,(
% 1.30/0.70 (?[Xa,Xb,Xc]: (s_r(Xa,Xb,Xc)&~s_r(Xc,Xb,Xa)))),
% 1.30/0.70 inference(pre_NNF_transformation,[status(thm)],[f119])).
% 1.30/0.70 fof(f330,plain,(
% 1.30/0.70 (s_r(sK0_skl,sK1_skl,sK2_skl)&~s_r(sK2_skl,sK1_skl,sK0_skl))),
% 1.30/0.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(Xa,sK0_skl),skolemize(Xb,sK1_skl),skolemize(Xc,sK2_skl)],[f329])).
% 1.30/0.70 fof(f331,plain,(
% 1.30/0.70 s_r(sK0_skl,sK1_skl,sK2_skl)),
% 1.30/0.70 inference(cnf_transformation,[status(thm)],[f330])).
% 1.30/0.70 fof(f332,plain,(
% 1.30/0.70 ~s_r(sK2_skl,sK1_skl,sK0_skl)),
% 1.30/0.70 inference(cnf_transformation,[status(thm)],[f330])).
% 1.30/0.70 fof(f388,plain,(
% 1.30/0.70 (![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))))),
% 1.30/0.70 inference(miniscoping,[status(thm)],[f130])).
% 1.30/0.70 fof(f389,plain,(
% 1.30/0.70 ![X0,X1,X2]: (~s_r(X0,X1,X2)|s_e(X0,X2,X0,s(X1,X2)))),
% 1.30/0.70 inference(cnf_transformation,[status(thm)],[f388])).
% 1.30/0.70 fof(f390,plain,(
% 1.30/0.70 ![X0,X1,X2]: (s_r(X0,X1,X2)|~s_e(X0,X2,X0,s(X1,X2)))),
% 1.30/0.70 inference(cnf_transformation,[status(thm)],[f388])).
% 1.30/0.70 fof(f414,plain,(
% 1.30/0.70 ![X0,X1,X2,X3,X4]: (~s_e(X0,X1,X2,X3)|~s_e(X0,X1,X2,s(X4,X3))|s_r(X2,X4,X3))),
% 1.30/0.70 inference(resolution,[status(thm)],[f135,f390])).
% 1.30/0.70 fof(f606,plain,(
% 1.30/0.70 ![X0,X1,X2]: (s_e(X0,X1,s(X2,X0),X1)|~s_r(X1,X2,X0))),
% 1.30/0.70 inference(resolution,[status(thm)],[f162,f389])).
% 1.30/0.70 fof(f665,plain,(
% 1.30/0.70 s_e(sK2_skl,sK0_skl,s(sK1_skl,sK2_skl),sK0_skl)),
% 1.30/0.70 inference(resolution,[status(thm)],[f606,f331])).
% 1.30/0.70 fof(f915,plain,(
% 1.30/0.70 ![X0,X1,X2,X3,X4]: (~s_e(X0,X1,X2,s(X3,X4))|~s_e(X0,X1,X2,X4)|s_r(X2,X3,s(X3,X4)))),
% 1.30/0.70 inference(paramodulation,[status(thm)],[f297,f414])).
% 1.30/0.70 fof(f1549,plain,(
% 1.30/0.70 ![X0,X1,X2]: (~s_e(X0,X1,s(X2,X0),X1)|s_r(s(X2,X0),X2,s(X2,X1)))),
% 1.30/0.70 inference(resolution,[status(thm)],[f304,f915])).
% 1.30/0.70 fof(f1646,plain,(
% 1.30/0.70 ![X0]: (s_e(s(X0,sK2_skl),s(X0,sK0_skl),s(X0,s(sK1_skl,sK2_skl)),s(X0,sK0_skl)))),
% 1.30/0.70 inference(resolution,[status(thm)],[f310,f665])).
% 1.30/0.71 fof(f1720,plain,(
% 1.30/0.71 s_r(s(sK1_skl,s(sK1_skl,sK2_skl)),sK1_skl,s(sK1_skl,s(sK1_skl,sK0_skl)))),
% 1.30/0.71 inference(resolution,[status(thm)],[f1646,f1549])).
% 1.30/0.71 fof(f1742,plain,(
% 1.30/0.71 s_r(sK2_skl,sK1_skl,s(sK1_skl,s(sK1_skl,sK0_skl)))),
% 1.30/0.71 inference(forward_demodulation,[status(thm)],[f297,f1720])).
% 1.30/0.71 fof(f1743,plain,(
% 1.30/0.71 s_r(sK2_skl,sK1_skl,sK0_skl)),
% 1.30/0.71 inference(forward_demodulation,[status(thm)],[f297,f1742])).
% 1.30/0.71 fof(f1744,plain,(
% 1.30/0.71 $false),
% 1.30/0.71 inference(forward_subsumption_resolution,[status(thm)],[f1743,f332])).
% 1.30/0.71 % SZS output end CNFRefutation for theBenchmark.p
% 1.30/0.73 % Elapsed time: 0.356662 seconds
% 1.30/0.73 % CPU time: 2.208729 seconds
% 1.30/0.73 % Total memory used: 125.594 MB
% 1.30/0.73 % Net memory used: 122.059 MB
%------------------------------------------------------------------------------