%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP123-3.003 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:35:42 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP123-3.003 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n006.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 20 19:58:13 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.39 % Refutation found
% 0.12/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.39 fof(f17,axiom,(
% 0.12/0.39 group_element(e_1) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f18,axiom,(
% 0.12/0.39 group_element(e_2) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f19,axiom,(
% 0.12/0.39 group_element(e_3) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f20,axiom,(
% 0.12/0.39 ~ equalish(e_1,e_2) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f21,axiom,(
% 0.12/0.39 ~ equalish(e_1,e_3) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f23,axiom,(
% 0.12/0.39 ~ equalish(e_2,e_3) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f24,axiom,(
% 0.12/0.39 ~ equalish(e_3,e_1) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f25,axiom,(
% 0.12/0.39 ~ equalish(e_3,e_2) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f26,axiom,(
% 0.12/0.39 (![X,Y]: (( ~ group_element(X)| ~ group_element(Y)| product(X,Y,e_1)| product(X,Y,e_2)| product(X,Y,e_3) ) ))),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f28,axiom,(
% 0.12/0.39 (![X,W,Y,Z]: (( ~ product(X,W,Y)| ~ product(X,Z,Y)| equalish(W,Z) ) ))),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f29,axiom,(
% 0.12/0.39 (![W,Y,X,Z]: (( ~ product(W,Y,X)| ~ product(Z,Y,X)| equalish(W,Z) ) ))),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f30,axiom,(
% 0.12/0.39 (![X]: (product(X,X,X) ))),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f31,negated_conjecture,(
% 0.12/0.39 (![X1,Y1,Z1,X2,Y2,Z2]: (( ~ product(X1,Y1,Z1)| ~ product(X2,Y2,Z1)| ~ product(Z2,Y1,X1)| ~ product(Z2,Y2,X2)| equalish(X1,X2) ) ))),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f53,plain,(
% 0.12/0.39 group_element(e_1)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.39 fof(f54,plain,(
% 0.12/0.39 group_element(e_2)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f18])).
% 0.12/0.39 fof(f55,plain,(
% 0.12/0.39 group_element(e_3)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f19])).
% 0.12/0.39 fof(f56,plain,(
% 0.12/0.39 ~equalish(e_1,e_2)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f20])).
% 0.12/0.39 fof(f57,plain,(
% 0.12/0.39 ~equalish(e_1,e_3)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f21])).
% 0.12/0.39 fof(f59,plain,(
% 0.12/0.39 ~equalish(e_2,e_3)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f23])).
% 0.12/0.39 fof(f60,plain,(
% 0.12/0.39 ~equalish(e_3,e_1)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f24])).
% 0.12/0.39 fof(f61,plain,(
% 0.12/0.39 ~equalish(e_3,e_2)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f25])).
% 0.12/0.39 fof(f62,plain,(
% 0.12/0.39 ![X0,X1]: (~group_element(X0)|~group_element(X1)|product(X0,X1,e_1)|product(X0,X1,e_2)|product(X0,X1,e_3))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f26])).
% 0.12/0.39 fof(f65,plain,(
% 0.12/0.39 ![W,Z]: ((![X,Y]: (~product(X,W,Y)|~product(X,Z,Y)))|equalish(W,Z))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f28])).
% 0.12/0.39 fof(f66,plain,(
% 0.12/0.39 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X3,X2)|equalish(X1,X3))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f65])).
% 0.12/0.39 fof(f67,plain,(
% 0.12/0.39 ![W,Z]: ((![Y,X]: (~product(W,Y,X)|~product(Z,Y,X)))|equalish(W,Z))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f29])).
% 0.12/0.39 fof(f68,plain,(
% 0.12/0.39 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X3,X1,X2)|equalish(X0,X3))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f67])).
% 0.12/0.39 fof(f69,plain,(
% 0.12/0.39 ![X0]: (product(X0,X0,X0))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f30])).
% 0.12/0.39 fof(f70,plain,(
% 0.12/0.39 ![X1,X2]: ((![Y2,Z2]: ((![Y1]: ((![Z1]: (~product(X1,Y1,Z1)|~product(X2,Y2,Z1)))|~product(Z2,Y1,X1)))|~product(Z2,Y2,X2)))|equalish(X1,X2))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f31])).
% 0.12/0.39 fof(f71,plain,(
% 0.12/0.39 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~product(X3,X4,X2)|~product(X5,X1,X0)|~product(X5,X4,X3)|equalish(X0,X3))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f70])).
% 0.12/0.39 fof(f76,plain,(
% 0.12/0.39 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X3,X2,X2)|~product(X3,X1,X0)|equalish(X2,X0))),
% 0.12/0.39 inference(resolution,[status(thm)],[f69,f71])).
% 0.12/0.39 fof(f78,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,X1,X0)|equalish(X0,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f66,f69])).
% 0.12/0.39 fof(f79,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,X1,X1)|equalish(X1,X0))),
% 0.12/0.39 inference(resolution,[status(thm)],[f68,f69])).
% 0.12/0.39 fof(f117,plain,(
% 0.12/0.39 ![X0]: (~group_element(X0)|product(e_3,X0,e_1)|product(e_3,X0,e_2)|product(e_3,X0,e_3))),
% 0.12/0.39 inference(resolution,[status(thm)],[f62,f55])).
% 0.12/0.39 fof(f118,plain,(
% 0.12/0.39 ![X0]: (~group_element(X0)|product(e_2,X0,e_1)|product(e_2,X0,e_2)|product(e_2,X0,e_3))),
% 0.12/0.39 inference(resolution,[status(thm)],[f62,f54])).
% 0.12/0.39 fof(f122,plain,(
% 0.12/0.39 product(e_3,e_1,e_1)|product(e_3,e_1,e_2)|product(e_3,e_1,e_3)),
% 0.12/0.39 inference(resolution,[status(thm)],[f117,f53])).
% 0.12/0.39 fof(f143,definition,(
% 0.12/0.39 sQ15_spl <=> (product(e_3,e_1,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f144,plain,(
% 0.12/0.39 product(e_3,e_1,e_1)|~sQ15_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f143])).
% 0.12/0.39 fof(f146,definition,(
% 0.12/0.39 sQ16_spl <=> (product(e_3,e_1,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f147,plain,(
% 0.12/0.39 product(e_3,e_1,e_2)|~sQ16_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f146])).
% 0.12/0.39 fof(f149,definition,(
% 0.12/0.39 sQ17_spl <=> (product(e_3,e_1,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f150,plain,(
% 0.12/0.39 product(e_3,e_1,e_3)|~sQ17_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f149])).
% 0.12/0.39 fof(f152,plain,(
% 0.12/0.39 sQ15_spl|sQ16_spl|sQ17_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f122,f143,f146,f149])).
% 0.12/0.39 fof(f155,plain,(
% 0.12/0.39 product(e_2,e_1,e_1)|product(e_2,e_1,e_2)|product(e_2,e_1,e_3)),
% 0.12/0.39 inference(resolution,[status(thm)],[f118,f53])).
% 0.12/0.39 fof(f176,definition,(
% 0.12/0.39 sQ24_spl <=> (product(e_2,e_1,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f177,plain,(
% 0.12/0.39 product(e_2,e_1,e_1)|~sQ24_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f176])).
% 0.12/0.39 fof(f179,definition,(
% 0.12/0.39 sQ25_spl <=> (product(e_2,e_1,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f180,plain,(
% 0.12/0.39 product(e_2,e_1,e_2)|~sQ25_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f179])).
% 0.12/0.39 fof(f182,definition,(
% 0.12/0.39 sQ26_spl <=> (product(e_2,e_1,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f185,plain,(
% 0.12/0.39 sQ24_spl|sQ25_spl|sQ26_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f155,f176,f179,f182])).
% 0.12/0.39 fof(f344,plain,(
% 0.12/0.39 equalish(e_3,e_1)|~sQ17_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f150,f78])).
% 0.12/0.39 fof(f356,plain,(
% 0.12/0.39 $false|~sQ17_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f344,f60])).
% 0.12/0.39 fof(f357,plain,(
% 0.12/0.39 ~sQ17_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f356])).
% 0.12/0.39 fof(f372,plain,(
% 0.12/0.39 ![X0]: (~product(X0,e_2,e_2)|~product(X0,e_1,e_3)|equalish(e_2,e_3)|~sQ16_spl)),
% 0.12/0.39 inference(resolution,[status(thm)],[f147,f76])).
% 0.12/0.39 fof(f374,plain,(
% 0.12/0.39 ![X0]: (~product(X0,e_1,e_2)|equalish(e_3,X0)|~sQ16_spl)),
% 0.12/0.39 inference(resolution,[status(thm)],[f147,f68])).
% 0.12/0.39 fof(f383,definition,(
% 0.12/0.39 ![X0]: (sQ56_spl <=> (~product(X0,e_2,e_2)|~product(X0,e_1,e_3)))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f384,plain,(
% 0.12/0.39 ![X0]: (~product(X0,e_2,e_2)|~product(X0,e_1,e_3)|~sQ56_spl)),
% 0.12/0.39 inference(component_clause,[status(thm)],[f383])).
% 0.12/0.39 fof(f386,definition,(
% 0.12/0.39 sQ57_spl <=> (equalish(e_2,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f387,plain,(
% 0.12/0.39 equalish(e_2,e_3)|~sQ57_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f386])).
% 0.12/0.39 fof(f389,plain,(
% 0.12/0.39 sQ56_spl|sQ57_spl|~sQ16_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f372,f383,f386,f146])).
% 0.12/0.39 fof(f396,plain,(
% 0.12/0.39 $false|~sQ57_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f387,f59])).
% 0.12/0.39 fof(f397,plain,(
% 0.12/0.39 ~sQ57_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f396])).
% 0.12/0.39 fof(f409,definition,(
% 0.12/0.39 sQ61_spl <=> (equalish(e_1,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f410,plain,(
% 0.12/0.39 equalish(e_1,e_2)|~sQ61_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f409])).
% 0.12/0.39 fof(f414,plain,(
% 0.12/0.39 $false|~sQ61_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f410,f56])).
% 0.12/0.39 fof(f415,plain,(
% 0.12/0.39 ~sQ61_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f414])).
% 0.12/0.39 fof(f422,definition,(
% 0.12/0.39 sQ63_spl <=> (equalish(e_3,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f423,plain,(
% 0.12/0.39 equalish(e_3,e_2)|~sQ63_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f422])).
% 0.12/0.39 fof(f426,plain,(
% 0.12/0.39 $false|~sQ63_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f423,f61])).
% 0.12/0.39 fof(f427,plain,(
% 0.12/0.39 ~sQ63_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f426])).
% 0.12/0.39 fof(f428,plain,(
% 0.12/0.39 ~product(e_2,e_1,e_3)|~sQ56_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f384,f69])).
% 0.12/0.39 fof(f435,plain,(
% 0.12/0.39 equalish(e_1,e_3)|~sQ15_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f144,f79])).
% 0.12/0.39 fof(f448,plain,(
% 0.12/0.39 $false|~sQ15_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f435,f57])).
% 0.12/0.39 fof(f449,plain,(
% 0.12/0.39 ~sQ15_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f448])).
% 0.12/0.39 fof(f494,definition,(
% 0.12/0.39 sQ69_spl <=> (equalish(e_1,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f495,plain,(
% 0.12/0.39 equalish(e_1,e_3)|~sQ69_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f494])).
% 0.12/0.39 fof(f499,plain,(
% 0.12/0.39 $false|~sQ69_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f495,f57])).
% 0.12/0.39 fof(f500,plain,(
% 0.12/0.39 ~sQ69_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f499])).
% 0.12/0.39 fof(f512,definition,(
% 0.12/0.39 sQ71_spl <=> (equalish(e_3,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f513,plain,(
% 0.12/0.39 equalish(e_3,e_1)|~sQ71_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f512])).
% 0.12/0.39 fof(f516,plain,(
% 0.12/0.39 $false|~sQ71_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f513,f60])).
% 0.12/0.39 fof(f517,plain,(
% 0.12/0.39 ~sQ71_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f516])).
% 0.12/0.39 fof(f556,plain,(
% 0.12/0.39 equalish(e_3,e_2)|~sQ25_spl|~sQ16_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f180,f374])).
% 0.12/0.39 fof(f566,plain,(
% 0.12/0.39 sQ63_spl|~sQ25_spl|~sQ16_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f556,f422,f179,f146])).
% 0.12/0.39 fof(f578,plain,(
% 0.12/0.39 equalish(e_1,e_2)|~sQ24_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f177,f79])).
% 0.12/0.39 fof(f590,plain,(
% 0.12/0.39 sQ61_spl|~sQ24_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f578,f409,f176])).
% 0.12/0.39 fof(f596,plain,(
% 0.12/0.39 ~sQ26_spl|~sQ56_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f428,f182,f383])).
% 0.12/0.39 fof(f597,plain,(
% 0.12/0.39 $false),
% 0.12/0.39 inference(sat_refutation,[status(thm)],[f152,f185,f357,f389,f397,f415,f427,f449,f500,f517,f566,f590,f596])).
% 0.12/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.40 % Elapsed time: 0.042559 seconds
% 0.12/0.40 % CPU time: 0.151747 seconds
% 0.12/0.40 % Total memory used: 18.690 MB
% 0.12/0.40 % Net memory used: 18.392 MB
%------------------------------------------------------------------------------