%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP711+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:37:13 PM UTC 2026
% Result : Theorem 0.03s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP711+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.03/0.36 % WCLimit : 300
% 0.03/0.36 % DateTime : Sun Sep 20 20:32:35 UTC 2026
% 0.03/0.36 % CPUTime :
% 0.03/0.37 % Drodi V4.1.1
% 0.03/0.56 % Refutation found
% 0.03/0.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.03/0.56 % SZS output start CNFRefutation for theBenchmark
% 0.03/0.56 fof(f1,axiom,(
% 0.03/0.56 (! [A] : mult(A,unit) = A )),
% 0.03/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.56 fof(f2,axiom,(
% 0.03/0.56 (! [A] : mult(unit,A) = A )),
% 0.03/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.56 fof(f3,axiom,(
% 0.03/0.56 (! [C,B,A] : mult(A,mult(B,mult(B,C))) = mult(mult(mult(A,B),B),C) )),
% 0.03/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.56 fof(f4,axiom,(
% 0.03/0.56 (! [A] : mult(A,i(A)) = unit )),
% 0.03/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.56 fof(f5,axiom,(
% 0.03/0.56 (! [A] : mult(i(A),A) = unit )),
% 0.03/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.56 fof(f6,conjecture,(
% 0.03/0.56 (! [X6,X7,X8] :( ( mult(X6,X7) = mult(X6,X8)=> X7 = X8 )& ( mult(X7,X6) = mult(X8,X6)=> X7 = X8 ) ) )),
% 0.03/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.56 fof(f7,negated_conjecture,(
% 0.03/0.56 ~((! [X6,X7,X8] :( ( mult(X6,X7) = mult(X6,X8)=> X7 = X8 )& ( mult(X7,X6) = mult(X8,X6)=> X7 = X8 ) ) ))),
% 0.03/0.56 inference(negated_conjecture,[status(cth)],[f6])).
% 0.03/0.56 fof(f8,plain,(
% 0.03/0.56 ![X0]: (mult(X0,unit)=X0)),
% 0.03/0.56 inference(cnf_transformation,[status(thm)],[f1])).
% 0.03/0.56 fof(f9,plain,(
% 0.03/0.56 ![X0]: (mult(unit,X0)=X0)),
% 0.03/0.56 inference(cnf_transformation,[status(thm)],[f2])).
% 0.03/0.56 fof(f10,plain,(
% 0.03/0.56 ![X0,X1,X2]: (mult(X0,mult(X1,mult(X1,X2)))=mult(mult(mult(X0,X1),X1),X2))),
% 0.03/0.56 inference(cnf_transformation,[status(thm)],[f3])).
% 0.03/0.56 fof(f11,plain,(
% 0.03/0.56 ![X0]: (mult(X0,i(X0))=unit)),
% 0.03/0.56 inference(cnf_transformation,[status(thm)],[f4])).
% 0.03/0.56 fof(f12,plain,(
% 0.03/0.56 ![X0]: (mult(i(X0),X0)=unit)),
% 0.03/0.56 inference(cnf_transformation,[status(thm)],[f5])).
% 0.03/0.56 fof(f13,plain,(
% 0.03/0.56 (?[X6,X7,X8]: ((mult(X6,X7)=mult(X6,X8)&~X7=X8)|(mult(X7,X6)=mult(X8,X6)&~X7=X8)))),
% 0.03/0.56 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.03/0.56 fof(f14,definition,(
% 0.03/0.56 ![X6,X7,X8]: (sP0_prd(X8,X7,X6)<=>(mult(X6,X7)=mult(X6,X8)&~X7=X8))),
% 0.03/0.56 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.03/0.56 fof(f15,plain,(
% 0.03/0.56 ?[X6,X7,X8]: (sP0_prd(X8,X7,X6)|(mult(X7,X6)=mult(X8,X6)&~X7=X8))),
% 0.03/0.56 inference(formula_renaming,[status(thm)],[f13,f14])).
% 0.03/0.56 fof(f16,plain,(
% 0.03/0.56 (?[X6,X7,X8]: sP0_prd(X8,X7,X6))|(?[X7,X8]: ((?[X6]: mult(X7,X6)=mult(X8,X6))&~X7=X8))),
% 0.03/0.56 inference(miniscoping,[status(thm)],[f15])).
% 0.03/0.56 fof(f17,plain,(
% 0.03/0.56 sP0_prd(sK2_skl,sK1_skl,sK0_skl)|(mult(sK3_skl,sK5_skl)=mult(sK4_skl,sK5_skl)&~sK3_skl=sK4_skl)),
% 0.03/0.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(X6,sK0_skl),skolemize(X7,sK1_skl),skolemize(X8,sK2_skl),skolemize(X7,sK3_skl),skolemize(X8,sK4_skl),skolemize(X6,sK5_skl)],[f16])).
% 0.03/0.56 fof(f18,plain,(
% 0.03/0.56 sP0_prd(sK2_skl,sK1_skl,sK0_skl)|mult(sK3_skl,sK5_skl)=mult(sK4_skl,sK5_skl)),
% 0.03/0.56 inference(cnf_transformation,[status(thm)],[f17])).
% 0.03/0.56 fof(f19,plain,(
% 0.03/0.56 sP0_prd(sK2_skl,sK1_skl,sK0_skl)|~sK3_skl=sK4_skl),
% 0.03/0.56 inference(cnf_transformation,[status(thm)],[f17])).
% 0.03/0.56 fof(f20,plain,(
% 0.03/0.56 ![X6,X7,X8]: ((~sP0_prd(X8,X7,X6)|(mult(X6,X7)=mult(X6,X8)&~X7=X8))&(sP0_prd(X8,X7,X6)|(~mult(X6,X7)=mult(X6,X8)|X7=X8)))),
% 0.03/0.56 inference(NNF_transformation,[status(thm)],[f14])).
% 0.03/0.56 fof(f21,plain,(
% 0.03/0.56 (![X6,X7,X8]: (~sP0_prd(X8,X7,X6)|(mult(X6,X7)=mult(X6,X8)&~X7=X8)))&(![X6,X7,X8]: (sP0_prd(X8,X7,X6)|(~mult(X6,X7)=mult(X6,X8)|X7=X8)))),
% 0.03/0.56 inference(miniscoping,[status(thm)],[f20])).
% 0.03/0.56 fof(f22,plain,(
% 0.03/0.56 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|mult(X2,X1)=mult(X2,X0))),
% 0.03/0.56 inference(cnf_transformation,[status(thm)],[f21])).
% 0.03/0.56 fof(f23,plain,(
% 0.03/0.56 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~X1=X0)),
% 0.03/0.56 inference(cnf_transformation,[status(thm)],[f21])).
% 0.03/0.56 fof(f24,plain,(
% 0.03/0.56 ![X0,X1,X2]: (sP0_prd(X0,X1,X2)|~mult(X2,X1)=mult(X2,X0)|X1=X0)),
% 0.03/0.56 inference(cnf_transformation,[status(thm)],[f21])).
% 0.03/0.56 fof(f25,definition,(
% 0.03/0.56 sQ0_spl <=> (sP0_prd(sK2_skl,sK1_skl,sK0_skl))),
% 0.03/0.56 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.03/0.56 fof(f26,plain,(
% 0.03/0.56 sP0_prd(sK2_skl,sK1_skl,sK0_skl)|~sQ0_spl),
% 0.03/0.56 inference(component_clause,[status(thm)],[f25])).
% 0.03/0.56 fof(f28,definition,(
% 0.03/0.56 sQ1_spl <=> (mult(sK3_skl,sK5_skl)=mult(sK4_skl,sK5_skl))),
% 0.03/0.56 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.03/0.56 fof(f29,plain,(
% 0.03/0.56 mult(sK3_skl,sK5_skl)=mult(sK4_skl,sK5_skl)|~sQ1_spl),
% 0.03/0.56 inference(component_clause,[status(thm)],[f28])).
% 0.03/0.56 fof(f31,plain,(
% 0.03/0.56 sQ0_spl|sQ1_spl),
% 0.03/0.56 inference(split_clause,[status(thm)],[f18,f25,f28])).
% 0.03/0.56 fof(f32,definition,(
% 0.03/0.56 sQ2_spl <=> (sK3_skl=sK4_skl)),
% 0.03/0.56 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.03/0.56 fof(f34,plain,(
% 0.03/0.56 ~sK3_skl=sK4_skl|sQ2_spl),
% 0.03/0.56 inference(component_clause,[status(thm)],[f32])).
% 0.03/0.56 fof(f35,plain,(
% 0.03/0.56 sQ0_spl|~sQ2_spl),
% 0.03/0.56 inference(split_clause,[status(thm)],[f19,f25,f32])).
% 0.03/0.56 fof(f36,plain,(
% 0.03/0.56 ![X0,X1]: (~sP0_prd(X0,X0,X1))),
% 0.03/0.56 inference(destructive_equality_resolution,[status(thm)],[f23])).
% 0.03/0.56 fof(f37,plain,(
% 0.03/0.56 mult(sK0_skl,sK1_skl)=mult(sK0_skl,sK2_skl)|~sQ0_spl),
% 0.03/0.56 inference(resolution,[status(thm)],[f22,f26])).
% 0.03/0.56 fof(f40,plain,(
% 0.03/0.56 sP0_prd(sK1_skl,sK2_skl,sK0_skl)|sK2_skl=sK1_skl|~sQ0_spl),
% 0.03/0.56 inference(resolution,[status(thm)],[f37,f24])).
% 0.03/0.56 fof(f43,definition,(
% 0.03/0.56 sQ3_spl <=> (sK1_skl=sK2_skl)),
% 0.03/0.56 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.03/0.56 fof(f44,plain,(
% 0.03/0.56 sK1_skl=sK2_skl|~sQ3_spl),
% 0.03/0.56 inference(component_clause,[status(thm)],[f43])).
% 0.03/0.56 fof(f45,plain,(
% 0.03/0.56 ~sK1_skl=sK2_skl|sQ3_spl),
% 0.03/0.56 inference(component_clause,[status(thm)],[f43])).
% 0.03/0.56 fof(f47,definition,(
% 0.03/0.56 sQ4_spl <=> (sP0_prd(sK1_skl,sK2_skl,sK0_skl))),
% 0.03/0.56 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.03/0.56 fof(f48,plain,(
% 0.03/0.56 sP0_prd(sK1_skl,sK2_skl,sK0_skl)|~sQ4_spl),
% 0.03/0.56 inference(component_clause,[status(thm)],[f47])).
% 0.03/0.56 fof(f50,plain,(
% 0.03/0.56 sQ4_spl|sQ3_spl|~sQ0_spl),
% 0.03/0.56 inference(split_clause,[status(thm)],[f40,f47,f43,f25])).
% 0.03/0.56 fof(f51,plain,(
% 0.03/0.56 mult(sK0_skl,sK2_skl)=mult(sK0_skl,sK1_skl)|~sQ4_spl),
% 0.03/0.56 inference(resolution,[status(thm)],[f48,f22])).
% 0.03/0.56 fof(f62,definition,(
% 0.03/0.56 sQ5_spl <=> (mult(sK0_skl,sK2_skl)=mult(sK0_skl,sK1_skl))),
% 0.03/0.56 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.03/0.56 fof(f63,plain,(
% 0.03/0.56 mult(sK0_skl,sK2_skl)=mult(sK0_skl,sK1_skl)|~sQ5_spl),
% 0.03/0.56 inference(component_clause,[status(thm)],[f62])).
% 0.03/0.56 fof(f64,plain,(
% 0.03/0.56 ~mult(sK0_skl,sK2_skl)=mult(sK0_skl,sK1_skl)|sQ5_spl),
% 0.03/0.56 inference(component_clause,[status(thm)],[f62])).
% 0.03/0.56 fof(f69,plain,(
% 0.03/0.56 ![X0]: (mult(sK4_skl,mult(sK5_skl,mult(sK5_skl,X0)))=mult(mult(mult(sK3_skl,sK5_skl),sK5_skl),X0)|~sQ1_spl)),
% 0.03/0.56 inference(paramodulation,[status(thm)],[f29,f10])).
% 0.03/0.56 fof(f72,plain,(
% 0.03/0.56 ![X0]: (mult(sK4_skl,mult(sK5_skl,mult(sK5_skl,X0)))=mult(sK3_skl,mult(sK5_skl,mult(sK5_skl,X0)))|~sQ1_spl)),
% 0.03/0.56 inference(forward_demodulation,[status(thm)],[f10,f69])).
% 0.03/0.56 fof(f163,plain,(
% 0.03/0.56 ![X0,X1]: (mult(X0,mult(X1,mult(X1,unit)))=mult(mult(X0,X1),X1))),
% 0.03/0.56 inference(paramodulation,[status(thm)],[f10,f8])).
% 0.03/0.56 fof(f173,plain,(
% 0.03/0.56 ![X0,X1]: (sP0_prd(unit,X0,X1)|~mult(X1,X0)=X1|X0=unit)),
% 0.03/0.56 inference(paramodulation,[status(thm)],[f8,f24])).
% 0.03/0.56 fof(f176,plain,(
% 0.03/0.56 ![X0,X1]: (mult(X0,mult(X1,X1))=mult(mult(X0,X1),X1))),
% 0.03/0.56 inference(forward_demodulation,[status(thm)],[f8,f163])).
% 0.03/0.56 fof(f222,plain,(
% 0.03/0.56 ![X0,X1]: (mult(X0,mult(X1,mult(X1,i(mult(mult(X0,X1),X1)))))=unit)),
% 0.03/0.56 inference(paramodulation,[status(thm)],[f10,f11])).
% 0.03/0.56 fof(f248,plain,(
% 0.03/0.56 $false|sQ5_spl|~sQ4_spl),
% 0.03/0.56 inference(forward_subsumption_resolution,[status(thm)],[f51,f64])).
% 0.03/0.56 fof(f249,plain,(
% 0.03/0.56 sQ5_spl|~sQ4_spl),
% 0.03/0.56 inference(contradiction_clause,[status(thm)],[f248])).
% 0.03/0.56 fof(f302,plain,(
% 0.03/0.56 ![X0]: (~mult(X0,unit)=X0|unit=unit)),
% 0.03/0.56 inference(resolution,[status(thm)],[f173,f36])).
% 0.03/0.56 fof(f303,definition,(
% 0.03/0.56 ![X0]: (sQ7_spl <=> (~mult(X0,unit)=X0))),
% 0.03/0.56 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.03/0.56 fof(f304,plain,(
% 0.03/0.56 ![X0]: (~mult(X0,unit)=X0|~sQ7_spl)),
% 0.03/0.56 inference(component_clause,[status(thm)],[f303])).
% 0.03/0.56 fof(f306,definition,(
% 0.03/0.56 sQ8_spl <=> (unit=unit)),
% 0.03/0.56 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.03/0.56 fof(f309,plain,(
% 0.03/0.56 sQ7_spl|sQ8_spl),
% 0.03/0.56 inference(split_clause,[status(thm)],[f302,f303,f306])).
% 0.03/0.56 fof(f310,plain,(
% 0.03/0.56 ![X0]: (~X0=X0|~sQ7_spl)),
% 0.03/0.56 inference(forward_demodulation,[status(thm)],[f8,f304])).
% 0.03/0.56 fof(f311,plain,(
% 0.03/0.56 $false|~sQ7_spl),
% 0.03/0.56 inference(trivial_equality_resolution,[status(thm)],[f310])).
% 0.03/0.57 fof(f312,plain,(
% 0.03/0.57 ~sQ7_spl),
% 0.03/0.57 inference(contradiction_clause,[status(thm)],[f311])).
% 0.03/0.57 fof(f322,plain,(
% 0.03/0.57 sP0_prd(sK1_skl,sK1_skl,sK0_skl)|~sQ3_spl|~sQ0_spl),
% 0.03/0.57 inference(forward_demodulation,[status(thm)],[f44,f26])).
% 0.03/0.57 fof(f323,plain,(
% 0.03/0.57 $false|~sQ3_spl|~sQ0_spl),
% 0.03/0.57 inference(forward_subsumption_resolution,[status(thm)],[f322,f36])).
% 0.03/0.57 fof(f324,plain,(
% 0.03/0.57 ~sQ3_spl|~sQ0_spl),
% 0.03/0.57 inference(contradiction_clause,[status(thm)],[f323])).
% 0.03/0.57 fof(f343,plain,(
% 0.03/0.57 ![X0,X1,X2]: (mult(X0,mult(X1,mult(X1,X2)))=mult(mult(X0,mult(X1,X1)),X2))),
% 0.03/0.57 inference(backward_demodulation,[status(thm)],[f176,f10])).
% 0.03/0.57 fof(f524,plain,(
% 0.03/0.57 ![X0,X1]: (mult(i(mult(X0,X0)),mult(X0,mult(X0,X1)))=mult(unit,X1))),
% 0.03/0.57 inference(paramodulation,[status(thm)],[f12,f343])).
% 0.03/0.57 fof(f564,plain,(
% 0.03/0.57 ![X0,X1]: (mult(i(mult(X0,X0)),mult(X0,mult(X0,X1)))=X1)),
% 0.03/0.57 inference(forward_demodulation,[status(thm)],[f9,f524])).
% 0.03/0.57 fof(f614,plain,(
% 0.03/0.57 ![X0,X1]: (mult(X0,mult(X1,mult(X1,i(mult(X0,mult(X1,X1))))))=unit)),
% 0.03/0.57 inference(forward_demodulation,[status(thm)],[f176,f222])).
% 0.03/0.57 fof(f892,plain,(
% 0.03/0.57 mult(i(mult(sK0_skl,sK0_skl)),mult(sK0_skl,mult(sK0_skl,sK1_skl)))=sK2_skl|~sQ5_spl),
% 0.03/0.57 inference(paramodulation,[status(thm)],[f63,f564])).
% 0.03/0.57 fof(f939,plain,(
% 0.03/0.57 sK1_skl=sK2_skl|~sQ5_spl),
% 0.03/0.57 inference(forward_demodulation,[status(thm)],[f564,f892])).
% 0.03/0.57 fof(f940,plain,(
% 0.03/0.57 $false|sQ3_spl|~sQ5_spl),
% 0.03/0.57 inference(forward_subsumption_resolution,[status(thm)],[f939,f45])).
% 0.03/0.57 fof(f941,plain,(
% 0.03/0.57 sQ3_spl|~sQ5_spl),
% 0.03/0.57 inference(contradiction_clause,[status(thm)],[f940])).
% 0.03/0.57 fof(f2676,plain,(
% 0.03/0.57 mult(sK4_skl,unit)=mult(sK3_skl,mult(sK5_skl,mult(sK5_skl,mult(sK5_skl,i(mult(sK5_skl,mult(sK5_skl,sK5_skl)))))))|~sQ1_spl),
% 0.03/0.57 inference(paramodulation,[status(thm)],[f614,f72])).
% 0.03/0.57 fof(f2699,plain,(
% 0.03/0.57 sK4_skl=mult(sK3_skl,mult(sK5_skl,mult(sK5_skl,mult(sK5_skl,i(mult(sK5_skl,mult(sK5_skl,sK5_skl)))))))|~sQ1_spl),
% 0.03/0.57 inference(forward_demodulation,[status(thm)],[f8,f2676])).
% 0.03/0.57 fof(f2700,plain,(
% 0.03/0.57 sK4_skl=mult(sK3_skl,unit)|~sQ1_spl),
% 0.03/0.57 inference(forward_demodulation,[status(thm)],[f614,f2699])).
% 0.03/0.57 fof(f2701,plain,(
% 0.03/0.57 sK4_skl=sK3_skl|~sQ1_spl),
% 0.03/0.57 inference(forward_demodulation,[status(thm)],[f8,f2700])).
% 0.03/0.57 fof(f2702,plain,(
% 0.03/0.57 $false|sQ2_spl|~sQ1_spl),
% 0.03/0.57 inference(forward_subsumption_resolution,[status(thm)],[f2701,f34])).
% 0.03/0.57 fof(f2703,plain,(
% 0.03/0.57 sQ2_spl|~sQ1_spl),
% 0.03/0.57 inference(contradiction_clause,[status(thm)],[f2702])).
% 0.03/0.57 fof(f2704,plain,(
% 0.03/0.57 $false),
% 0.03/0.57 inference(sat_refutation,[status(thm)],[f31,f35,f50,f249,f309,f312,f324,f941,f2703])).
% 0.03/0.57 % SZS output end CNFRefutation for theBenchmark.p
% 0.03/0.58 % Elapsed time: 0.211792 seconds
% 0.03/0.58 % CPU time: 1.386733 seconds
% 0.03/0.58 % Total memory used: 139.835 MB
% 0.03/0.58 % Net memory used: 138.285 MB
%------------------------------------------------------------------------------