%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP194+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:36:14 PM UTC 2026
% Result : Theorem 0.13s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP194+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.35 % Computer : n004.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Sun Sep 20 20:05:35 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.39 % Refutation found
% 0.13/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.39 fof(f3,axiom,(
% 0.13/0.39 (! [X] :( group_member(X,f)=> group_member(phi(X),h) ) )),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f4,axiom,(
% 0.13/0.39 (! [X,Y] :( ( group_member(X,f)& group_member(Y,f) )=> multiply(h,phi(X),phi(Y)) = phi(multiply(f,X,Y)) ) )),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f5,axiom,(
% 0.13/0.39 (! [X] :( group_member(X,h)=> (? [Y] :( group_member(Y,f)& phi(Y) = X ) )) )),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f6,axiom,(
% 0.13/0.39 (! [G,X] :( left_zero(G,X)<=> ( group_member(X,G)& (! [Y] :( group_member(Y,G)=> multiply(G,X,Y) = X ) )) ) )),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f7,hypothesis,(
% 0.13/0.39 left_zero(f,f_left_zero) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f8,conjecture,(
% 0.13/0.39 left_zero(h,phi(f_left_zero)) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f9,negated_conjecture,(
% 0.13/0.39 ~(left_zero(h,phi(f_left_zero)) )),
% 0.13/0.39 inference(negated_conjecture,[status(cth)],[f8])).
% 0.13/0.39 fof(f14,plain,(
% 0.13/0.39 ![X]: (~group_member(X,f)|group_member(phi(X),h))),
% 0.13/0.39 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.13/0.39 fof(f15,plain,(
% 0.13/0.39 ![X0]: (~group_member(X0,f)|group_member(phi(X0),h))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f14])).
% 0.13/0.39 fof(f16,plain,(
% 0.13/0.39 ![X,Y]: ((~group_member(X,f)|~group_member(Y,f))|multiply(h,phi(X),phi(Y))=phi(multiply(f,X,Y)))),
% 0.13/0.39 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.13/0.39 fof(f17,plain,(
% 0.13/0.39 ![X0,X1]: (~group_member(X0,f)|~group_member(X1,f)|multiply(h,phi(X0),phi(X1))=phi(multiply(f,X0,X1)))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f16])).
% 0.13/0.39 fof(f18,plain,(
% 0.13/0.39 ![X]: (~group_member(X,h)|(?[Y]: (group_member(Y,f)&phi(Y)=X)))),
% 0.13/0.39 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.13/0.39 fof(f19,plain,(
% 0.13/0.39 ![X]: (~group_member(X,h)|(group_member(sK0_skl(X),f)&phi(sK0_skl(X))=X))),
% 0.13/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y,sK0_skl(X))],[f18])).
% 0.13/0.40 fof(f20,plain,(
% 0.13/0.40 ![X0]: (~group_member(X0,h)|group_member(sK0_skl(X0),f))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/0.40 fof(f21,plain,(
% 0.13/0.40 ![X0]: (~group_member(X0,h)|phi(sK0_skl(X0))=X0)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/0.40 fof(f22,plain,(
% 0.13/0.40 ![G,X]: (left_zero(G,X)<=>(group_member(X,G)&(![Y]: (~group_member(Y,G)|multiply(G,X,Y)=X))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.13/0.40 fof(f23,plain,(
% 0.13/0.40 ![G,X]: ((~left_zero(G,X)|(group_member(X,G)&(![Y]: (~group_member(Y,G)|multiply(G,X,Y)=X))))&(left_zero(G,X)|(~group_member(X,G)|(?[Y]: (group_member(Y,G)&~multiply(G,X,Y)=X)))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f22])).
% 0.13/0.40 fof(f24,plain,(
% 0.13/0.40 (![G,X]: (~left_zero(G,X)|(group_member(X,G)&(![Y]: (~group_member(Y,G)|multiply(G,X,Y)=X)))))&(![G,X]: (left_zero(G,X)|(~group_member(X,G)|(?[Y]: (group_member(Y,G)&~multiply(G,X,Y)=X)))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f23])).
% 0.13/0.40 fof(f25,plain,(
% 0.13/0.40 (![G,X]: (~left_zero(G,X)|(group_member(X,G)&(![Y]: (~group_member(Y,G)|multiply(G,X,Y)=X)))))&(![G,X]: (left_zero(G,X)|(~group_member(X,G)|(group_member(sK1_skl(X,G),G)&~multiply(G,X,sK1_skl(X,G))=X))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y,sK1_skl(X,G))],[f24])).
% 0.13/0.40 fof(f26,plain,(
% 0.13/0.40 ![X0,X1]: (~left_zero(X0,X1)|group_member(X1,X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/0.40 fof(f27,plain,(
% 0.13/0.40 ![X0,X1,X2]: (~left_zero(X0,X1)|~group_member(X2,X0)|multiply(X0,X1,X2)=X1)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/0.40 fof(f28,plain,(
% 0.13/0.40 ![X0,X1]: (left_zero(X0,X1)|~group_member(X1,X0)|group_member(sK1_skl(X1,X0),X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/0.40 fof(f29,plain,(
% 0.13/0.40 ![X0,X1]: (left_zero(X0,X1)|~group_member(X1,X0)|~multiply(X0,X1,sK1_skl(X1,X0))=X1)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/0.40 fof(f30,plain,(
% 0.13/0.40 left_zero(f,f_left_zero)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.40 fof(f31,plain,(
% 0.13/0.40 ~left_zero(h,phi(f_left_zero))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/0.40 fof(f32,plain,(
% 0.13/0.40 group_member(f_left_zero,f)),
% 0.13/0.40 inference(resolution,[status(thm)],[f26,f30])).
% 0.13/0.40 fof(f33,plain,(
% 0.13/0.40 ![X0]: (~group_member(X0,f)|multiply(f,f_left_zero,X0)=f_left_zero)),
% 0.13/0.40 inference(resolution,[status(thm)],[f27,f30])).
% 0.13/0.40 fof(f34,plain,(
% 0.13/0.40 ![X0]: (~group_member(X0,f)|multiply(h,phi(f_left_zero),phi(X0))=phi(multiply(f,f_left_zero,X0)))),
% 0.13/0.40 inference(resolution,[status(thm)],[f32,f17])).
% 0.13/0.40 fof(f35,plain,(
% 0.13/0.40 group_member(phi(f_left_zero),h)),
% 0.13/0.40 inference(resolution,[status(thm)],[f32,f15])).
% 0.13/0.40 fof(f45,plain,(
% 0.13/0.40 left_zero(h,phi(f_left_zero))|~multiply(h,phi(f_left_zero),sK1_skl(phi(f_left_zero),h))=phi(f_left_zero)),
% 0.13/0.40 inference(resolution,[status(thm)],[f29,f35])).
% 0.13/0.40 fof(f47,definition,(
% 0.13/0.40 sQ0_spl <=> (left_zero(h,phi(f_left_zero)))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f48,plain,(
% 0.13/0.40 left_zero(h,phi(f_left_zero))|~sQ0_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f47])).
% 0.13/0.40 fof(f50,definition,(
% 0.13/0.40 sQ1_spl <=> (multiply(h,phi(f_left_zero),sK1_skl(phi(f_left_zero),h))=phi(f_left_zero))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f52,plain,(
% 0.13/0.40 ~multiply(h,phi(f_left_zero),sK1_skl(phi(f_left_zero),h))=phi(f_left_zero)|sQ1_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f50])).
% 0.13/0.40 fof(f53,plain,(
% 0.13/0.40 sQ0_spl|~sQ1_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f45,f47,f50])).
% 0.13/0.40 fof(f61,plain,(
% 0.13/0.40 $false|~sQ0_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f48,f31])).
% 0.13/0.40 fof(f62,plain,(
% 0.13/0.40 ~sQ0_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f61])).
% 0.13/0.40 fof(f67,plain,(
% 0.13/0.40 left_zero(h,phi(f_left_zero))|group_member(sK1_skl(phi(f_left_zero),h),h)),
% 0.13/0.40 inference(resolution,[status(thm)],[f28,f35])).
% 0.13/0.40 fof(f69,definition,(
% 0.13/0.40 sQ4_spl <=> (group_member(sK1_skl(phi(f_left_zero),h),h))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f70,plain,(
% 0.13/0.40 group_member(sK1_skl(phi(f_left_zero),h),h)|~sQ4_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f69])).
% 0.13/0.40 fof(f72,plain,(
% 0.13/0.40 sQ0_spl|sQ4_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f67,f47,f69])).
% 0.13/0.40 fof(f119,plain,(
% 0.13/0.40 group_member(sK0_skl(sK1_skl(phi(f_left_zero),h)),f)|~sQ4_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f70,f20])).
% 0.13/0.40 fof(f120,plain,(
% 0.13/0.40 phi(sK0_skl(sK1_skl(phi(f_left_zero),h)))=sK1_skl(phi(f_left_zero),h)|~sQ4_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f70,f21])).
% 0.13/0.40 fof(f147,plain,(
% 0.13/0.40 multiply(h,phi(f_left_zero),phi(sK0_skl(sK1_skl(phi(f_left_zero),h))))=phi(multiply(f,f_left_zero,sK0_skl(sK1_skl(phi(f_left_zero),h))))|~sQ4_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f119,f34])).
% 0.13/0.40 fof(f148,plain,(
% 0.13/0.40 multiply(f,f_left_zero,sK0_skl(sK1_skl(phi(f_left_zero),h)))=f_left_zero|~sQ4_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f119,f33])).
% 0.13/0.40 fof(f156,plain,(
% 0.13/0.40 multiply(h,phi(f_left_zero),sK1_skl(phi(f_left_zero),h))=phi(multiply(f,f_left_zero,sK0_skl(sK1_skl(phi(f_left_zero),h))))|~sQ4_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f120,f147])).
% 0.13/0.40 fof(f157,plain,(
% 0.13/0.40 multiply(h,phi(f_left_zero),sK1_skl(phi(f_left_zero),h))=phi(f_left_zero)|~sQ4_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f148,f156])).
% 0.13/0.40 fof(f174,plain,(
% 0.13/0.40 $false|sQ1_spl|~sQ4_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f157,f52])).
% 0.13/0.40 fof(f175,plain,(
% 0.13/0.40 sQ1_spl|~sQ4_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f174])).
% 0.13/0.40 fof(f176,plain,(
% 0.13/0.40 $false),
% 0.13/0.40 inference(sat_refutation,[status(thm)],[f53,f62,f72,f175])).
% 0.13/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.43 % Elapsed time: 0.060864 seconds
% 0.13/0.43 % CPU time: 0.210073 seconds
% 0.13/0.43 % Total memory used: 81.135 MB
% 0.13/0.43 % Net memory used: 80.680 MB
%------------------------------------------------------------------------------