%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP665+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:07 PM UTC 2026
% Result : Theorem 0.23s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP665+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.50 % Computer : n018.cluster.edu
% 0.18/0.50 % Model : x86_64 x86_64
% 0.18/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.50 % Memory : 8046.5625MB
% 0.18/0.50 % OS : Linux 6.8.0-71-generic
% 0.18/0.50 % CPULimit : 300
% 0.18/0.50 % WCLimit : 300
% 0.18/0.50 % DateTime : Sun Sep 20 20:32:43 UTC 2026
% 0.18/0.51 % CPUTime :
% 0.23/0.53 % Drodi V4.1.1
% 0.23/0.54 % Refutation found
% 0.23/0.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.23/0.54 % SZS output start CNFRefutation for theBenchmark
% 0.23/0.54 fof(f1,axiom,(
% 0.23/0.54 (! [B,A] : mult(A,ld(A,B)) = B )),
% 0.23/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.54 fof(f2,axiom,(
% 0.23/0.54 (! [B,A] : ld(A,mult(A,B)) = B )),
% 0.23/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.54 fof(f4,axiom,(
% 0.23/0.54 (! [B,A] : rd(mult(A,B),B) = A )),
% 0.23/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.54 fof(f7,axiom,(
% 0.23/0.54 (! [C,B,A] : mult(A,mult(B,C)) = mult(rd(mult(A,B),A),mult(A,C)) )),
% 0.23/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.54 fof(f8,axiom,(
% 0.23/0.54 (! [C,B,A] : mult(mult(A,B),C) = mult(mult(A,C),ld(C,mult(B,C))) )),
% 0.23/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.54 fof(f9,axiom,(
% 0.23/0.54 (! [A] : mult(op_c,A) = mult(A,op_c) )),
% 0.23/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.54 fof(f10,conjecture,(
% 0.23/0.54 (! [X0,X1] :( mult(op_c,mult(X0,X1)) = mult(mult(op_c,X0),X1)& mult(mult(X0,op_c),X1) = mult(X0,mult(op_c,X1))& mult(mult(X0,X1),op_c) = mult(X0,mult(X1,op_c)) ) )),
% 0.23/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.54 fof(f11,negated_conjecture,(
% 0.23/0.54 ~((! [X0,X1] :( mult(op_c,mult(X0,X1)) = mult(mult(op_c,X0),X1)& mult(mult(X0,op_c),X1) = mult(X0,mult(op_c,X1))& mult(mult(X0,X1),op_c) = mult(X0,mult(X1,op_c)) ) ))),
% 0.23/0.54 inference(negated_conjecture,[status(cth)],[f10])).
% 0.23/0.54 fof(f12,plain,(
% 0.23/0.54 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 0.23/0.54 inference(cnf_transformation,[status(thm)],[f1])).
% 0.23/0.54 fof(f13,plain,(
% 0.23/0.54 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 0.23/0.54 inference(cnf_transformation,[status(thm)],[f2])).
% 0.23/0.54 fof(f15,plain,(
% 0.23/0.54 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 0.23/0.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.23/0.54 fof(f18,plain,(
% 0.23/0.54 ![X0,X1,X2]: (mult(X0,mult(X1,X2))=mult(rd(mult(X0,X1),X0),mult(X0,X2)))),
% 0.23/0.54 inference(cnf_transformation,[status(thm)],[f7])).
% 0.23/0.54 fof(f19,plain,(
% 0.23/0.54 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(X0,X2),ld(X2,mult(X1,X2))))),
% 0.23/0.54 inference(cnf_transformation,[status(thm)],[f8])).
% 0.23/0.54 fof(f20,plain,(
% 0.23/0.54 ![X0]: (mult(op_c,X0)=mult(X0,op_c))),
% 0.23/0.54 inference(cnf_transformation,[status(thm)],[f9])).
% 0.23/0.54 fof(f21,plain,(
% 0.23/0.54 (?[X0,X1]: ((~mult(op_c,mult(X0,X1))=mult(mult(op_c,X0),X1)|~mult(mult(X0,op_c),X1)=mult(X0,mult(op_c,X1)))|~mult(mult(X0,X1),op_c)=mult(X0,mult(X1,op_c))))),
% 0.23/0.54 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.23/0.54 fof(f22,plain,(
% 0.23/0.54 ((?[X0,X1]: ~mult(op_c,mult(X0,X1))=mult(mult(op_c,X0),X1))|(?[X0,X1]: ~mult(mult(X0,op_c),X1)=mult(X0,mult(op_c,X1))))|(?[X0,X1]: ~mult(mult(X0,X1),op_c)=mult(X0,mult(X1,op_c)))),
% 0.23/0.54 inference(miniscoping,[status(thm)],[f21])).
% 0.23/0.54 fof(f23,plain,(
% 0.23/0.54 (~mult(op_c,mult(sK0_skl,sK1_skl))=mult(mult(op_c,sK0_skl),sK1_skl)|~mult(mult(sK2_skl,op_c),sK3_skl)=mult(sK2_skl,mult(op_c,sK3_skl)))|~mult(mult(sK4_skl,sK5_skl),op_c)=mult(sK4_skl,mult(sK5_skl,op_c))),
% 0.23/0.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl),skolemize(X0,sK2_skl),skolemize(X1,sK3_skl),skolemize(X0,sK4_skl),skolemize(X1,sK5_skl)],[f22])).
% 0.23/0.54 fof(f24,plain,(
% 0.23/0.54 ~mult(op_c,mult(sK0_skl,sK1_skl))=mult(mult(op_c,sK0_skl),sK1_skl)|~mult(mult(sK2_skl,op_c),sK3_skl)=mult(sK2_skl,mult(op_c,sK3_skl))|~mult(mult(sK4_skl,sK5_skl),op_c)=mult(sK4_skl,mult(sK5_skl,op_c))),
% 0.23/0.54 inference(cnf_transformation,[status(thm)],[f23])).
% 0.23/0.54 fof(f25,definition,(
% 0.23/0.54 sQ0_spl <=> (mult(op_c,mult(sK0_skl,sK1_skl))=mult(mult(op_c,sK0_skl),sK1_skl))),
% 0.23/0.54 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.23/0.54 fof(f27,plain,(
% 0.23/0.54 ~mult(op_c,mult(sK0_skl,sK1_skl))=mult(mult(op_c,sK0_skl),sK1_skl)|sQ0_spl),
% 0.23/0.54 inference(component_clause,[status(thm)],[f25])).
% 0.23/0.54 fof(f28,definition,(
% 0.23/0.54 sQ1_spl <=> (mult(mult(sK2_skl,op_c),sK3_skl)=mult(sK2_skl,mult(op_c,sK3_skl)))),
% 0.23/0.54 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.23/0.54 fof(f30,plain,(
% 0.23/0.54 ~mult(mult(sK2_skl,op_c),sK3_skl)=mult(sK2_skl,mult(op_c,sK3_skl))|sQ1_spl),
% 0.23/0.54 inference(component_clause,[status(thm)],[f28])).
% 0.23/0.54 fof(f31,definition,(
% 0.23/0.54 sQ2_spl <=> (mult(mult(sK4_skl,sK5_skl),op_c)=mult(sK4_skl,mult(sK5_skl,op_c)))),
% 0.23/0.54 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.23/0.54 fof(f33,plain,(
% 0.23/0.54 ~mult(mult(sK4_skl,sK5_skl),op_c)=mult(sK4_skl,mult(sK5_skl,op_c))|sQ2_spl),
% 0.23/0.54 inference(component_clause,[status(thm)],[f31])).
% 0.23/0.54 fof(f34,plain,(
% 0.23/0.54 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 0.23/0.54 inference(split_clause,[status(thm)],[f24,f25,f28,f31])).
% 0.23/0.54 fof(f35,plain,(
% 0.23/0.54 ~mult(op_c,mult(sK4_skl,sK5_skl))=mult(sK4_skl,mult(sK5_skl,op_c))|sQ2_spl),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f20,f33])).
% 0.23/0.54 fof(f66,plain,(
% 0.23/0.54 ![X0,X1,X2]: (mult(X0,mult(ld(X0,X1),X2))=mult(rd(X1,X0),mult(X0,X2)))),
% 0.23/0.54 inference(paramodulation,[status(thm)],[f12,f18])).
% 0.23/0.54 fof(f131,plain,(
% 0.23/0.54 ![X0,X1]: (mult(mult(X0,op_c),X1)=mult(mult(X0,X1),ld(X1,mult(X1,op_c))))),
% 0.23/0.54 inference(paramodulation,[status(thm)],[f20,f19])).
% 0.23/0.54 fof(f132,plain,(
% 0.23/0.54 ![X0,X1]: (mult(mult(op_c,X0),X1)=mult(mult(X1,op_c),ld(X1,mult(X0,X1))))),
% 0.23/0.54 inference(paramodulation,[status(thm)],[f20,f19])).
% 0.23/0.54 fof(f133,plain,(
% 0.23/0.54 ![X0]: (rd(mult(X0,op_c),X0)=op_c)),
% 0.23/0.54 inference(paramodulation,[status(thm)],[f20,f15])).
% 0.23/0.54 fof(f140,plain,(
% 0.23/0.54 ![X0,X1]: (mult(mult(X0,op_c),X1)=mult(mult(X0,X1),op_c))),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f13,f131])).
% 0.23/0.54 fof(f141,plain,(
% 0.23/0.54 ![X0,X1]: (mult(mult(X0,op_c),X1)=mult(op_c,mult(X0,X1)))),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f20,f140])).
% 0.23/0.54 fof(f142,plain,(
% 0.23/0.54 ![X0,X1]: (mult(mult(op_c,X0),X1)=mult(op_c,mult(X1,ld(X1,mult(X0,X1)))))),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f141,f132])).
% 0.23/0.54 fof(f143,plain,(
% 0.23/0.54 ![X0,X1]: (mult(mult(op_c,X0),X1)=mult(op_c,mult(X0,X1)))),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f12,f142])).
% 0.23/0.54 fof(f205,plain,(
% 0.23/0.54 ![X0,X1]: (mult(X0,mult(ld(X0,mult(X0,op_c)),X1))=mult(op_c,mult(X0,X1)))),
% 0.23/0.54 inference(paramodulation,[status(thm)],[f133,f66])).
% 0.23/0.54 fof(f210,plain,(
% 0.23/0.54 ~mult(sK4_skl,mult(op_c,sK5_skl))=mult(sK4_skl,mult(sK5_skl,op_c))|sQ2_spl),
% 0.23/0.54 inference(backward_demodulation,[status(thm)],[f211,f35])).
% 0.23/0.54 fof(f211,plain,(
% 0.23/0.54 ![X0,X1]: (mult(X0,mult(op_c,X1))=mult(op_c,mult(X0,X1)))),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f13,f205])).
% 0.23/0.54 fof(f213,plain,(
% 0.23/0.54 ~mult(sK4_skl,mult(sK5_skl,op_c))=mult(sK4_skl,mult(sK5_skl,op_c))|sQ2_spl),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f20,f210])).
% 0.23/0.54 fof(f214,plain,(
% 0.23/0.54 $false|sQ2_spl),
% 0.23/0.54 inference(trivial_equality_resolution,[status(thm)],[f213])).
% 0.23/0.54 fof(f215,plain,(
% 0.23/0.54 sQ2_spl),
% 0.23/0.54 inference(contradiction_clause,[status(thm)],[f214])).
% 0.23/0.54 fof(f216,plain,(
% 0.23/0.54 ~mult(sK0_skl,mult(op_c,sK1_skl))=mult(mult(op_c,sK0_skl),sK1_skl)|sQ0_spl),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f211,f27])).
% 0.23/0.54 fof(f217,plain,(
% 0.23/0.54 ~mult(sK0_skl,mult(sK1_skl,op_c))=mult(mult(op_c,sK0_skl),sK1_skl)|sQ0_spl),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f20,f216])).
% 0.23/0.54 fof(f218,plain,(
% 0.23/0.54 ~mult(sK0_skl,mult(sK1_skl,op_c))=mult(op_c,mult(sK0_skl,sK1_skl))|sQ0_spl),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f143,f217])).
% 0.23/0.54 fof(f219,plain,(
% 0.23/0.54 ~mult(sK0_skl,mult(sK1_skl,op_c))=mult(sK0_skl,mult(op_c,sK1_skl))|sQ0_spl),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f211,f218])).
% 0.23/0.54 fof(f220,plain,(
% 0.23/0.54 ~mult(sK0_skl,mult(sK1_skl,op_c))=mult(sK0_skl,mult(sK1_skl,op_c))|sQ0_spl),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f20,f219])).
% 0.23/0.54 fof(f221,plain,(
% 0.23/0.54 $false|sQ0_spl),
% 0.23/0.54 inference(trivial_equality_resolution,[status(thm)],[f220])).
% 0.23/0.54 fof(f222,plain,(
% 0.23/0.54 sQ0_spl),
% 0.23/0.54 inference(contradiction_clause,[status(thm)],[f221])).
% 0.23/0.54 fof(f225,plain,(
% 0.23/0.54 ~mult(op_c,mult(sK2_skl,sK3_skl))=mult(sK2_skl,mult(op_c,sK3_skl))|sQ1_spl),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f141,f30])).
% 0.23/0.54 fof(f226,plain,(
% 0.23/0.54 ~mult(sK2_skl,mult(op_c,sK3_skl))=mult(sK2_skl,mult(op_c,sK3_skl))|sQ1_spl),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f211,f225])).
% 0.23/0.54 fof(f227,plain,(
% 0.23/0.54 ~mult(sK2_skl,mult(sK3_skl,op_c))=mult(sK2_skl,mult(op_c,sK3_skl))|sQ1_spl),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f20,f226])).
% 0.23/0.54 fof(f228,plain,(
% 0.23/0.54 ~mult(sK2_skl,mult(sK3_skl,op_c))=mult(sK2_skl,mult(sK3_skl,op_c))|sQ1_spl),
% 0.23/0.54 inference(forward_demodulation,[status(thm)],[f20,f227])).
% 0.23/0.54 fof(f229,plain,(
% 0.23/0.54 $false|sQ1_spl),
% 0.23/0.54 inference(trivial_equality_resolution,[status(thm)],[f228])).
% 0.23/0.55 fof(f230,plain,(
% 0.23/0.55 sQ1_spl),
% 0.23/0.55 inference(contradiction_clause,[status(thm)],[f229])).
% 0.23/0.55 fof(f231,plain,(
% 0.23/0.55 $false),
% 0.23/0.55 inference(sat_refutation,[status(thm)],[f34,f215,f222,f230])).
% 0.23/0.55 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/0.61 % Elapsed time: 0.087923 seconds
% 0.23/0.61 % CPU time: 0.124064 seconds
% 0.23/0.61 % Total memory used: 8.731 MB
% 0.23/0.61 % Net memory used: 8.722 MB
%------------------------------------------------------------------------------