%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP124-2.004 : 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 : 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:35:45 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.03 % Problem : GRP124-2.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n004.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 19:58:35 UTC 2026
% 0.08/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(f11,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(f12,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(f13,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(f14,axiom,(
% 0.12/0.39 group_element(e_4) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f15,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(f16,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(f17,axiom,(
% 0.12/0.39 ~ equalish(e_1,e_4) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f19,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(f20,axiom,(
% 0.12/0.39 ~ equalish(e_2,e_4) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f23,axiom,(
% 0.12/0.39 ~ equalish(e_3,e_4) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f27,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)| product(X,Y,e_4) ) ))),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f28,axiom,(
% 0.12/0.39 (![X,Y,W,Z]: (( ~ product(X,Y,W)| ~ product(X,Y,Z)| 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 (![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(f30,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(f31,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(f33,negated_conjecture,(
% 0.12/0.39 (![X1,Y1,Z1,X2,Y2,Z2]: (( ~ product(X1,Y1,Z1)| ~ product(X2,Y2,Z1)| ~ product(Z2,X1,Y1)| ~ product(Z2,X2,Y2)| equalish(Y1,Y2) ) ))),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f45,plain,(
% 0.12/0.39 group_element(e_1)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f11])).
% 0.12/0.39 fof(f46,plain,(
% 0.12/0.39 group_element(e_2)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.39 fof(f47,plain,(
% 0.12/0.39 group_element(e_3)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f13])).
% 0.12/0.39 fof(f48,plain,(
% 0.12/0.39 group_element(e_4)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f14])).
% 0.12/0.39 fof(f49,plain,(
% 0.12/0.39 ~equalish(e_1,e_2)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f15])).
% 0.12/0.39 fof(f50,plain,(
% 0.12/0.39 ~equalish(e_1,e_3)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f16])).
% 0.12/0.39 fof(f51,plain,(
% 0.12/0.39 ~equalish(e_1,e_4)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.39 fof(f53,plain,(
% 0.12/0.39 ~equalish(e_2,e_3)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f19])).
% 0.12/0.39 fof(f54,plain,(
% 0.12/0.39 ~equalish(e_2,e_4)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f20])).
% 0.12/0.39 fof(f57,plain,(
% 0.12/0.39 ~equalish(e_3,e_4)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f23])).
% 0.12/0.39 fof(f61,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)|product(X0,X1,e_4))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f27])).
% 0.12/0.39 fof(f62,plain,(
% 0.12/0.39 ![W,Z]: ((![X,Y]: (~product(X,Y,W)|~product(X,Y,Z)))|equalish(W,Z))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f28])).
% 0.12/0.39 fof(f63,plain,(
% 0.12/0.39 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|equalish(X2,X3))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f62])).
% 0.12/0.39 fof(f64,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)],[f29])).
% 0.12/0.39 fof(f65,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)],[f64])).
% 0.12/0.39 fof(f66,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)],[f30])).
% 0.12/0.39 fof(f67,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)],[f66])).
% 0.12/0.39 fof(f68,plain,(
% 0.12/0.39 ![X0]: (product(X0,X0,X0))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f31])).
% 0.12/0.39 fof(f71,plain,(
% 0.12/0.39 ![Y1,Y2]: ((![X2,Z2]: ((![X1]: ((![Z1]: (~product(X1,Y1,Z1)|~product(X2,Y2,Z1)))|~product(Z2,X1,Y1)))|~product(Z2,X2,Y2)))|equalish(Y1,Y2))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f33])).
% 0.12/0.39 fof(f72,plain,(
% 0.12/0.39 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~product(X3,X4,X2)|~product(X5,X0,X1)|~product(X5,X3,X4)|equalish(X1,X4))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/0.39 fof(f73,plain,(
% 0.12/0.39 ![X0,X1]: (~product(e_1,X0,X1)|~product(e_2,X0,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f49,f67])).
% 0.12/0.39 fof(f74,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,e_1,X1)|~product(X0,e_2,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f49,f65])).
% 0.12/0.39 fof(f75,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,X1,e_1)|~product(X0,X1,e_2))),
% 0.12/0.39 inference(resolution,[status(thm)],[f49,f63])).
% 0.12/0.39 fof(f76,plain,(
% 0.12/0.39 ![X0,X1,X2,X3]: (~product(X0,e_1,X1)|~product(X2,e_2,X1)|~product(X3,X0,e_1)|~product(X3,X2,e_2))),
% 0.12/0.39 inference(resolution,[status(thm)],[f49,f72])).
% 0.12/0.39 fof(f78,plain,(
% 0.12/0.39 ![X0,X1]: (~product(e_1,X0,X1)|~product(e_3,X0,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f50,f67])).
% 0.12/0.39 fof(f79,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,e_1,X1)|~product(X0,e_3,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f50,f65])).
% 0.12/0.39 fof(f80,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,X1,e_1)|~product(X0,X1,e_3))),
% 0.12/0.39 inference(resolution,[status(thm)],[f50,f63])).
% 0.12/0.39 fof(f84,plain,(
% 0.12/0.39 ![X0,X1]: (~product(e_1,X0,X1)|~product(e_4,X0,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f51,f67])).
% 0.12/0.39 fof(f85,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,e_1,X1)|~product(X0,e_4,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f51,f65])).
% 0.12/0.39 fof(f86,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,X1,e_1)|~product(X0,X1,e_4))),
% 0.12/0.39 inference(resolution,[status(thm)],[f51,f63])).
% 0.12/0.39 fof(f94,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,e_1,e_2)|~product(X1,X0,e_1)|~product(X1,e_2,e_2))),
% 0.12/0.39 inference(resolution,[status(thm)],[f76,f68])).
% 0.12/0.39 fof(f97,plain,(
% 0.12/0.39 ~product(e_1,e_2,e_2)),
% 0.12/0.39 inference(resolution,[status(thm)],[f73,f68])).
% 0.12/0.39 fof(f98,plain,(
% 0.12/0.39 ~product(e_2,e_1,e_2)),
% 0.12/0.39 inference(resolution,[status(thm)],[f74,f68])).
% 0.12/0.39 fof(f99,plain,(
% 0.12/0.39 ~product(e_2,e_2,e_1)),
% 0.12/0.39 inference(resolution,[status(thm)],[f75,f68])).
% 0.12/0.39 fof(f100,plain,(
% 0.12/0.39 ~product(e_1,e_3,e_3)),
% 0.12/0.39 inference(resolution,[status(thm)],[f78,f68])).
% 0.12/0.39 fof(f101,plain,(
% 0.12/0.39 ~product(e_3,e_1,e_3)),
% 0.12/0.39 inference(resolution,[status(thm)],[f79,f68])).
% 0.12/0.39 fof(f102,plain,(
% 0.12/0.39 ![X0,X1]: (~product(e_2,X0,X1)|~product(e_3,X0,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f53,f67])).
% 0.12/0.39 fof(f103,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,e_2,X1)|~product(X0,e_3,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f53,f65])).
% 0.12/0.39 fof(f104,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,X1,e_2)|~product(X0,X1,e_3))),
% 0.12/0.39 inference(resolution,[status(thm)],[f53,f63])).
% 0.12/0.39 fof(f107,plain,(
% 0.12/0.39 ![X0,X1]: (~product(e_2,X0,X1)|~product(e_4,X0,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f54,f67])).
% 0.12/0.39 fof(f108,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,e_2,X1)|~product(X0,e_4,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f54,f65])).
% 0.12/0.39 fof(f122,plain,(
% 0.12/0.39 ![X0,X1]: (~product(e_3,X0,X1)|~product(e_4,X0,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f57,f67])).
% 0.12/0.39 fof(f123,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,e_3,X1)|~product(X0,e_4,X1))),
% 0.12/0.39 inference(resolution,[status(thm)],[f57,f65])).
% 0.12/0.39 fof(f124,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,X1,e_3)|~product(X0,X1,e_4))),
% 0.12/0.39 inference(resolution,[status(thm)],[f57,f63])).
% 0.12/0.39 fof(f125,plain,(
% 0.12/0.39 ![X0,X1,X2,X3]: (~product(X0,e_3,X1)|~product(X2,e_4,X1)|~product(X3,X0,e_3)|~product(X3,X2,e_4))),
% 0.12/0.39 inference(resolution,[status(thm)],[f57,f72])).
% 0.12/0.39 fof(f142,plain,(
% 0.12/0.39 ![X0]: (~group_element(X0)|product(X0,e_4,e_1)|product(X0,e_4,e_2)|product(X0,e_4,e_3)|product(X0,e_4,e_4))),
% 0.12/0.39 inference(resolution,[status(thm)],[f61,f48])).
% 0.12/0.39 fof(f143,plain,(
% 0.12/0.39 ![X0]: (~group_element(X0)|product(X0,e_3,e_1)|product(X0,e_3,e_2)|product(X0,e_3,e_3)|product(X0,e_3,e_4))),
% 0.12/0.39 inference(resolution,[status(thm)],[f61,f47])).
% 0.12/0.39 fof(f144,plain,(
% 0.12/0.39 ![X0]: (~group_element(X0)|product(X0,e_2,e_1)|product(X0,e_2,e_2)|product(X0,e_2,e_3)|product(X0,e_2,e_4))),
% 0.12/0.39 inference(resolution,[status(thm)],[f61,f46])).
% 0.12/0.39 fof(f145,plain,(
% 0.12/0.39 ![X0]: (~group_element(X0)|product(X0,e_1,e_1)|product(X0,e_1,e_2)|product(X0,e_1,e_3)|product(X0,e_1,e_4))),
% 0.12/0.39 inference(resolution,[status(thm)],[f61,f45])).
% 0.12/0.39 fof(f146,plain,(
% 0.12/0.39 ~product(e_3,e_3,e_1)),
% 0.12/0.39 inference(resolution,[status(thm)],[f80,f68])).
% 0.12/0.39 fof(f149,plain,(
% 0.12/0.39 ~product(e_1,e_4,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f84,f68])).
% 0.12/0.39 fof(f150,plain,(
% 0.12/0.39 ~product(e_4,e_1,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f85,f68])).
% 0.12/0.39 fof(f153,plain,(
% 0.12/0.39 ~product(e_2,e_3,e_3)),
% 0.12/0.39 inference(resolution,[status(thm)],[f102,f68])).
% 0.12/0.39 fof(f154,plain,(
% 0.12/0.39 ~product(e_3,e_2,e_3)),
% 0.12/0.39 inference(resolution,[status(thm)],[f103,f68])).
% 0.12/0.39 fof(f155,plain,(
% 0.12/0.39 ~product(e_3,e_3,e_2)),
% 0.12/0.39 inference(resolution,[status(thm)],[f104,f68])).
% 0.12/0.39 fof(f158,plain,(
% 0.12/0.39 ~product(e_2,e_4,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f107,f68])).
% 0.12/0.39 fof(f159,plain,(
% 0.12/0.39 ~product(e_4,e_2,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f108,f68])).
% 0.12/0.39 fof(f163,plain,(
% 0.12/0.39 ~product(e_3,e_4,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f122,f68])).
% 0.12/0.39 fof(f164,plain,(
% 0.12/0.39 ~product(e_4,e_3,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f123,f68])).
% 0.12/0.39 fof(f165,plain,(
% 0.12/0.39 ![X0,X1]: (~product(X0,e_3,e_4)|~product(X1,X0,e_3)|~product(X1,e_4,e_4))),
% 0.12/0.39 inference(resolution,[status(thm)],[f125,f68])).
% 0.12/0.39 fof(f170,plain,(
% 0.12/0.39 product(e_2,e_4,e_1)|product(e_2,e_4,e_2)|product(e_2,e_4,e_3)|product(e_2,e_4,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f142,f46])).
% 0.12/0.39 fof(f171,plain,(
% 0.12/0.39 product(e_1,e_4,e_1)|product(e_1,e_4,e_2)|product(e_1,e_4,e_3)|product(e_1,e_4,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f142,f45])).
% 0.12/0.39 fof(f194,definition,(
% 0.12/0.39 sQ7_spl <=> (product(e_3,e_4,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f195,plain,(
% 0.12/0.39 product(e_3,e_4,e_4)|~sQ7_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f194])).
% 0.12/0.39 fof(f198,definition,(
% 0.12/0.39 sQ8_spl <=> (product(e_2,e_4,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f199,plain,(
% 0.12/0.39 product(e_2,e_4,e_1)|~sQ8_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f198])).
% 0.12/0.39 fof(f201,definition,(
% 0.12/0.39 sQ9_spl <=> (product(e_2,e_4,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f202,plain,(
% 0.12/0.39 product(e_2,e_4,e_2)|~sQ9_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f201])).
% 0.12/0.39 fof(f204,definition,(
% 0.12/0.39 sQ10_spl <=> (product(e_2,e_4,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f205,plain,(
% 0.12/0.39 product(e_2,e_4,e_3)|~sQ10_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f204])).
% 0.12/0.39 fof(f207,definition,(
% 0.12/0.39 sQ11_spl <=> (product(e_2,e_4,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f208,plain,(
% 0.12/0.39 product(e_2,e_4,e_4)|~sQ11_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f207])).
% 0.12/0.39 fof(f210,plain,(
% 0.12/0.39 sQ8_spl|sQ9_spl|sQ10_spl|sQ11_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f170,f198,f201,f204,f207])).
% 0.12/0.39 fof(f211,definition,(
% 0.12/0.39 sQ12_spl <=> (product(e_1,e_4,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f212,plain,(
% 0.12/0.39 product(e_1,e_4,e_1)|~sQ12_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f211])).
% 0.12/0.39 fof(f214,definition,(
% 0.12/0.39 sQ13_spl <=> (product(e_1,e_4,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f215,plain,(
% 0.12/0.39 product(e_1,e_4,e_2)|~sQ13_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f214])).
% 0.12/0.39 fof(f217,definition,(
% 0.12/0.39 sQ14_spl <=> (product(e_1,e_4,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f220,definition,(
% 0.12/0.39 sQ15_spl <=> (product(e_1,e_4,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f221,plain,(
% 0.12/0.39 product(e_1,e_4,e_4)|~sQ15_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f220])).
% 0.12/0.39 fof(f223,plain,(
% 0.12/0.39 sQ12_spl|sQ13_spl|sQ14_spl|sQ15_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f171,f211,f214,f217,f220])).
% 0.12/0.39 fof(f224,plain,(
% 0.12/0.39 $false|~sQ15_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f221,f149])).
% 0.12/0.39 fof(f225,plain,(
% 0.12/0.39 ~sQ15_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f224])).
% 0.12/0.39 fof(f226,plain,(
% 0.12/0.39 $false|~sQ11_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f208,f158])).
% 0.12/0.39 fof(f227,plain,(
% 0.12/0.39 ~sQ11_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f226])).
% 0.12/0.39 fof(f228,plain,(
% 0.12/0.39 $false|~sQ7_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f195,f163])).
% 0.12/0.39 fof(f229,plain,(
% 0.12/0.39 ~sQ7_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f228])).
% 0.12/0.39 fof(f239,plain,(
% 0.12/0.39 product(e_4,e_3,e_1)|product(e_4,e_3,e_2)|product(e_4,e_3,e_3)|product(e_4,e_3,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f143,f48])).
% 0.12/0.39 fof(f240,plain,(
% 0.12/0.39 product(e_3,e_3,e_1)|product(e_3,e_3,e_2)|product(e_3,e_3,e_3)|product(e_3,e_3,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f143,f47])).
% 0.12/0.39 fof(f241,plain,(
% 0.12/0.39 product(e_2,e_3,e_1)|product(e_2,e_3,e_2)|product(e_2,e_3,e_3)|product(e_2,e_3,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f143,f46])).
% 0.12/0.39 fof(f242,plain,(
% 0.12/0.39 product(e_1,e_3,e_1)|product(e_1,e_3,e_2)|product(e_1,e_3,e_3)|product(e_1,e_3,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f143,f45])).
% 0.12/0.39 fof(f243,definition,(
% 0.12/0.39 sQ16_spl <=> (product(e_4,e_3,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f244,plain,(
% 0.12/0.39 product(e_4,e_3,e_1)|~sQ16_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f243])).
% 0.12/0.39 fof(f246,definition,(
% 0.12/0.39 sQ17_spl <=> (product(e_4,e_3,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f247,plain,(
% 0.12/0.39 product(e_4,e_3,e_2)|~sQ17_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f246])).
% 0.12/0.39 fof(f249,definition,(
% 0.12/0.39 sQ18_spl <=> (product(e_4,e_3,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f250,plain,(
% 0.12/0.39 product(e_4,e_3,e_3)|~sQ18_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f249])).
% 0.12/0.39 fof(f252,definition,(
% 0.12/0.39 sQ19_spl <=> (product(e_4,e_3,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f253,plain,(
% 0.12/0.39 product(e_4,e_3,e_4)|~sQ19_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f252])).
% 0.12/0.39 fof(f255,plain,(
% 0.12/0.39 sQ16_spl|sQ17_spl|sQ18_spl|sQ19_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f239,f243,f246,f249,f252])).
% 0.12/0.39 fof(f256,definition,(
% 0.12/0.39 sQ20_spl <=> (product(e_3,e_3,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f257,plain,(
% 0.12/0.39 product(e_3,e_3,e_1)|~sQ20_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f256])).
% 0.12/0.39 fof(f259,definition,(
% 0.12/0.39 sQ21_spl <=> (product(e_3,e_3,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f260,plain,(
% 0.12/0.39 product(e_3,e_3,e_2)|~sQ21_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f259])).
% 0.12/0.39 fof(f262,definition,(
% 0.12/0.39 sQ22_spl <=> (product(e_3,e_3,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f265,definition,(
% 0.12/0.39 sQ23_spl <=> (product(e_3,e_3,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f266,plain,(
% 0.12/0.39 product(e_3,e_3,e_4)|~sQ23_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f265])).
% 0.12/0.39 fof(f268,plain,(
% 0.12/0.39 sQ20_spl|sQ21_spl|sQ22_spl|sQ23_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f240,f256,f259,f262,f265])).
% 0.12/0.39 fof(f269,definition,(
% 0.12/0.39 sQ24_spl <=> (product(e_2,e_3,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f270,plain,(
% 0.12/0.39 product(e_2,e_3,e_1)|~sQ24_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f269])).
% 0.12/0.39 fof(f272,definition,(
% 0.12/0.39 sQ25_spl <=> (product(e_2,e_3,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f273,plain,(
% 0.12/0.39 product(e_2,e_3,e_2)|~sQ25_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f272])).
% 0.12/0.39 fof(f275,definition,(
% 0.12/0.39 sQ26_spl <=> (product(e_2,e_3,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f276,plain,(
% 0.12/0.39 product(e_2,e_3,e_3)|~sQ26_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f275])).
% 0.12/0.39 fof(f278,definition,(
% 0.12/0.39 sQ27_spl <=> (product(e_2,e_3,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f279,plain,(
% 0.12/0.39 product(e_2,e_3,e_4)|~sQ27_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f278])).
% 0.12/0.39 fof(f281,plain,(
% 0.12/0.39 sQ24_spl|sQ25_spl|sQ26_spl|sQ27_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f241,f269,f272,f275,f278])).
% 0.12/0.39 fof(f282,definition,(
% 0.12/0.39 sQ28_spl <=> (product(e_1,e_3,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f283,plain,(
% 0.12/0.39 product(e_1,e_3,e_1)|~sQ28_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f282])).
% 0.12/0.39 fof(f285,definition,(
% 0.12/0.39 sQ29_spl <=> (product(e_1,e_3,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f288,definition,(
% 0.12/0.39 sQ30_spl <=> (product(e_1,e_3,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f289,plain,(
% 0.12/0.39 product(e_1,e_3,e_3)|~sQ30_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f288])).
% 0.12/0.39 fof(f291,definition,(
% 0.12/0.39 sQ31_spl <=> (product(e_1,e_3,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f292,plain,(
% 0.12/0.39 product(e_1,e_3,e_4)|~sQ31_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f291])).
% 0.12/0.39 fof(f294,plain,(
% 0.12/0.39 sQ28_spl|sQ29_spl|sQ30_spl|sQ31_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f242,f282,f285,f288,f291])).
% 0.12/0.39 fof(f295,plain,(
% 0.12/0.39 $false|~sQ30_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f289,f100])).
% 0.12/0.39 fof(f296,plain,(
% 0.12/0.39 ~sQ30_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f295])).
% 0.12/0.39 fof(f297,plain,(
% 0.12/0.39 $false|~sQ26_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f276,f153])).
% 0.12/0.39 fof(f298,plain,(
% 0.12/0.39 ~sQ26_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f297])).
% 0.12/0.39 fof(f299,plain,(
% 0.12/0.39 $false|~sQ21_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f260,f155])).
% 0.12/0.39 fof(f300,plain,(
% 0.12/0.39 ~sQ21_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f299])).
% 0.12/0.39 fof(f301,plain,(
% 0.12/0.39 $false|~sQ20_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f257,f146])).
% 0.12/0.39 fof(f302,plain,(
% 0.12/0.39 ~sQ20_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f301])).
% 0.12/0.39 fof(f303,plain,(
% 0.12/0.39 $false|~sQ19_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f253,f164])).
% 0.12/0.39 fof(f304,plain,(
% 0.12/0.39 ~sQ19_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f303])).
% 0.12/0.39 fof(f311,plain,(
% 0.12/0.39 ~product(e_1,e_1,e_1)|~sQ12_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f212,f85])).
% 0.12/0.39 fof(f313,plain,(
% 0.12/0.39 $false|~sQ12_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f311,f68])).
% 0.12/0.39 fof(f314,plain,(
% 0.12/0.39 ~sQ12_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f313])).
% 0.12/0.39 fof(f322,plain,(
% 0.12/0.39 ~product(e_2,e_1,e_3)|~sQ10_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f205,f85])).
% 0.12/0.39 fof(f331,plain,(
% 0.12/0.39 ~product(e_2,e_2,e_2)|~sQ9_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f202,f108])).
% 0.12/0.39 fof(f335,plain,(
% 0.12/0.39 $false|~sQ9_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f331,f68])).
% 0.12/0.39 fof(f336,plain,(
% 0.12/0.39 ~sQ9_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f335])).
% 0.12/0.39 fof(f340,plain,(
% 0.12/0.39 ~product(e_2,e_3,e_1)|~sQ8_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f199,f123])).
% 0.12/0.39 fof(f391,plain,(
% 0.12/0.39 product(e_4,e_2,e_1)|product(e_4,e_2,e_2)|product(e_4,e_2,e_3)|product(e_4,e_2,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f144,f48])).
% 0.12/0.39 fof(f395,definition,(
% 0.12/0.39 sQ32_spl <=> (product(e_4,e_2,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f396,plain,(
% 0.12/0.39 product(e_4,e_2,e_1)|~sQ32_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f395])).
% 0.12/0.39 fof(f398,definition,(
% 0.12/0.39 sQ33_spl <=> (product(e_4,e_2,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f399,plain,(
% 0.12/0.39 product(e_4,e_2,e_2)|~sQ33_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f398])).
% 0.12/0.39 fof(f401,definition,(
% 0.12/0.39 sQ34_spl <=> (product(e_4,e_2,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f402,plain,(
% 0.12/0.39 product(e_4,e_2,e_3)|~sQ34_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f401])).
% 0.12/0.39 fof(f404,definition,(
% 0.12/0.39 sQ35_spl <=> (product(e_4,e_2,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f405,plain,(
% 0.12/0.39 product(e_4,e_2,e_4)|~sQ35_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f404])).
% 0.12/0.39 fof(f407,plain,(
% 0.12/0.39 sQ32_spl|sQ33_spl|sQ34_spl|sQ35_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f391,f395,f398,f401,f404])).
% 0.12/0.39 fof(f411,definition,(
% 0.12/0.39 sQ37_spl <=> (product(e_3,e_2,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f412,plain,(
% 0.12/0.39 product(e_3,e_2,e_2)|~sQ37_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f411])).
% 0.12/0.39 fof(f414,definition,(
% 0.12/0.39 sQ38_spl <=> (product(e_3,e_2,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f415,plain,(
% 0.12/0.39 product(e_3,e_2,e_3)|~sQ38_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f414])).
% 0.12/0.39 fof(f421,definition,(
% 0.12/0.39 sQ40_spl <=> (product(e_2,e_2,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f422,plain,(
% 0.12/0.39 product(e_2,e_2,e_1)|~sQ40_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f421])).
% 0.12/0.39 fof(f434,definition,(
% 0.12/0.39 sQ44_spl <=> (product(e_1,e_2,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f435,plain,(
% 0.12/0.39 product(e_1,e_2,e_1)|~sQ44_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f434])).
% 0.12/0.39 fof(f437,definition,(
% 0.12/0.39 sQ45_spl <=> (product(e_1,e_2,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f438,plain,(
% 0.12/0.39 product(e_1,e_2,e_2)|~sQ45_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f437])).
% 0.12/0.39 fof(f447,plain,(
% 0.12/0.39 $false|~sQ45_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f438,f97])).
% 0.12/0.39 fof(f448,plain,(
% 0.12/0.39 ~sQ45_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f447])).
% 0.12/0.39 fof(f449,plain,(
% 0.12/0.39 $false|~sQ40_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f422,f99])).
% 0.12/0.39 fof(f450,plain,(
% 0.12/0.39 ~sQ40_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f449])).
% 0.12/0.39 fof(f451,plain,(
% 0.12/0.39 $false|~sQ38_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f415,f154])).
% 0.12/0.39 fof(f452,plain,(
% 0.12/0.39 ~sQ38_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f451])).
% 0.12/0.39 fof(f453,plain,(
% 0.12/0.39 $false|~sQ35_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f405,f159])).
% 0.12/0.39 fof(f454,plain,(
% 0.12/0.39 ~sQ35_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f453])).
% 0.12/0.39 fof(f456,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)|product(e_3,e_1,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f145,f47])).
% 0.12/0.39 fof(f457,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)|product(e_2,e_1,e_4)),
% 0.12/0.39 inference(resolution,[status(thm)],[f145,f46])).
% 0.12/0.39 fof(f468,definition,(
% 0.12/0.39 sQ51_spl <=> (product(e_4,e_1,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f469,plain,(
% 0.12/0.39 product(e_4,e_1,e_4)|~sQ51_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f468])).
% 0.12/0.39 fof(f472,definition,(
% 0.12/0.39 sQ52_spl <=> (product(e_3,e_1,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f473,plain,(
% 0.12/0.39 product(e_3,e_1,e_1)|~sQ52_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f472])).
% 0.12/0.39 fof(f475,definition,(
% 0.12/0.39 sQ53_spl <=> (product(e_3,e_1,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f476,plain,(
% 0.12/0.39 product(e_3,e_1,e_2)|~sQ53_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f475])).
% 0.12/0.39 fof(f478,definition,(
% 0.12/0.39 sQ54_spl <=> (product(e_3,e_1,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f479,plain,(
% 0.12/0.39 product(e_3,e_1,e_3)|~sQ54_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f478])).
% 0.12/0.39 fof(f481,definition,(
% 0.12/0.39 sQ55_spl <=> (product(e_3,e_1,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f482,plain,(
% 0.12/0.39 product(e_3,e_1,e_4)|~sQ55_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f481])).
% 0.12/0.39 fof(f484,plain,(
% 0.12/0.39 sQ52_spl|sQ53_spl|sQ54_spl|sQ55_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f456,f472,f475,f478,f481])).
% 0.12/0.39 fof(f485,definition,(
% 0.12/0.39 sQ56_spl <=> (product(e_2,e_1,e_1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f486,plain,(
% 0.12/0.39 product(e_2,e_1,e_1)|~sQ56_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f485])).
% 0.12/0.39 fof(f488,definition,(
% 0.12/0.39 sQ57_spl <=> (product(e_2,e_1,e_2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f489,plain,(
% 0.12/0.39 product(e_2,e_1,e_2)|~sQ57_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f488])).
% 0.12/0.39 fof(f491,definition,(
% 0.12/0.39 sQ58_spl <=> (product(e_2,e_1,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f492,plain,(
% 0.12/0.39 product(e_2,e_1,e_3)|~sQ58_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f491])).
% 0.12/0.39 fof(f494,definition,(
% 0.12/0.39 sQ59_spl <=> (product(e_2,e_1,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f495,plain,(
% 0.12/0.39 product(e_2,e_1,e_4)|~sQ59_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f494])).
% 0.12/0.39 fof(f497,plain,(
% 0.12/0.39 sQ56_spl|sQ57_spl|sQ58_spl|sQ59_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f457,f485,f488,f491,f494])).
% 0.12/0.39 fof(f504,definition,(
% 0.12/0.39 sQ62_spl <=> (product(e_1,e_1,e_3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f505,plain,(
% 0.12/0.39 product(e_1,e_1,e_3)|~sQ62_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f504])).
% 0.12/0.39 fof(f507,definition,(
% 0.12/0.39 sQ63_spl <=> (product(e_1,e_1,e_4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f508,plain,(
% 0.12/0.39 product(e_1,e_1,e_4)|~sQ63_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f507])).
% 0.12/0.39 fof(f511,plain,(
% 0.12/0.39 $false|~sQ57_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f489,f98])).
% 0.12/0.39 fof(f512,plain,(
% 0.12/0.39 ~sQ57_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f511])).
% 0.12/0.39 fof(f513,plain,(
% 0.12/0.39 $false|~sQ54_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f479,f101])).
% 0.12/0.39 fof(f514,plain,(
% 0.12/0.39 ~sQ54_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f513])).
% 0.12/0.39 fof(f515,plain,(
% 0.12/0.39 $false|~sQ51_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f469,f150])).
% 0.12/0.39 fof(f516,plain,(
% 0.12/0.39 ~sQ51_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f515])).
% 0.12/0.39 fof(f526,plain,(
% 0.12/0.39 ~product(e_1,e_1,e_1)|~sQ28_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f283,f79])).
% 0.12/0.39 fof(f528,plain,(
% 0.12/0.39 $false|~sQ28_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f526,f68])).
% 0.12/0.39 fof(f529,plain,(
% 0.12/0.39 ~sQ28_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f528])).
% 0.12/0.39 fof(f531,plain,(
% 0.12/0.39 ~product(e_1,e_3,e_4)|~sQ27_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f279,f73])).
% 0.12/0.39 fof(f533,plain,(
% 0.12/0.39 ![X0]: (~product(X0,e_2,e_3)|~product(X0,e_4,e_4)|~sQ27_spl)),
% 0.12/0.39 inference(resolution,[status(thm)],[f279,f165])).
% 0.12/0.39 fof(f541,plain,(
% 0.12/0.39 $false|~sQ31_spl|~sQ27_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f531,f292])).
% 0.12/0.39 fof(f542,plain,(
% 0.12/0.39 ~sQ31_spl|~sQ27_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f541])).
% 0.12/0.39 fof(f546,plain,(
% 0.12/0.39 ~product(e_2,e_2,e_2)|~sQ25_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f273,f103])).
% 0.12/0.39 fof(f552,plain,(
% 0.12/0.39 $false|~sQ8_spl|~sQ24_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f270,f340])).
% 0.12/0.39 fof(f553,plain,(
% 0.12/0.39 ~sQ8_spl|~sQ24_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f552])).
% 0.12/0.39 fof(f554,plain,(
% 0.12/0.39 $false|~sQ25_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f546,f68])).
% 0.12/0.39 fof(f555,plain,(
% 0.12/0.39 ~sQ25_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f554])).
% 0.12/0.39 fof(f566,plain,(
% 0.12/0.39 ~product(e_3,e_3,e_3)|~sQ23_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f266,f124])).
% 0.12/0.39 fof(f570,plain,(
% 0.12/0.39 $false|~sQ23_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f566,f68])).
% 0.12/0.39 fof(f571,plain,(
% 0.12/0.39 ~sQ23_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f570])).
% 0.12/0.39 fof(f573,plain,(
% 0.12/0.39 ~product(e_3,e_3,e_3)|~sQ18_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f250,f122])).
% 0.12/0.39 fof(f584,plain,(
% 0.12/0.39 $false|~sQ18_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f573,f68])).
% 0.12/0.39 fof(f585,plain,(
% 0.12/0.39 ~sQ18_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f584])).
% 0.12/0.39 fof(f591,plain,(
% 0.12/0.39 ~product(e_1,e_3,e_2)|~sQ17_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f247,f84])).
% 0.12/0.39 fof(f597,plain,(
% 0.12/0.39 ~sQ29_spl|~sQ17_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f591,f285,f246])).
% 0.12/0.39 fof(f606,plain,(
% 0.12/0.39 ~product(e_4,e_2,e_1)|~sQ16_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f244,f103])).
% 0.12/0.39 fof(f628,plain,(
% 0.12/0.39 ~product(e_1,e_1,e_1)|~sQ44_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f435,f74])).
% 0.12/0.39 fof(f630,plain,(
% 0.12/0.39 $false|~sQ44_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f628,f68])).
% 0.12/0.39 fof(f631,plain,(
% 0.12/0.39 ~sQ44_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f630])).
% 0.12/0.39 fof(f661,plain,(
% 0.12/0.39 ~product(e_2,e_2,e_2)|~sQ37_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f412,f102])).
% 0.12/0.39 fof(f667,plain,(
% 0.12/0.39 $false|~sQ37_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f661,f68])).
% 0.12/0.39 fof(f668,plain,(
% 0.12/0.39 ~sQ37_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f667])).
% 0.12/0.39 fof(f682,plain,(
% 0.12/0.39 ~product(e_4,e_4,e_4)|~sQ34_spl|~sQ27_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f402,f533])).
% 0.12/0.39 fof(f689,plain,(
% 0.12/0.39 $false|~sQ34_spl|~sQ27_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f682,f68])).
% 0.12/0.39 fof(f690,plain,(
% 0.12/0.39 ~sQ34_spl|~sQ27_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f689])).
% 0.12/0.39 fof(f694,plain,(
% 0.12/0.39 ~product(e_2,e_2,e_2)|~sQ33_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f399,f107])).
% 0.12/0.39 fof(f700,plain,(
% 0.12/0.39 $false|~sQ33_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f694,f68])).
% 0.12/0.39 fof(f701,plain,(
% 0.12/0.39 ~sQ33_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f700])).
% 0.12/0.39 fof(f718,plain,(
% 0.12/0.39 ~product(e_1,e_1,e_1)|~sQ63_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f508,f86])).
% 0.12/0.39 fof(f719,plain,(
% 0.12/0.39 $false|~sQ63_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f718,f68])).
% 0.12/0.39 fof(f720,plain,(
% 0.12/0.39 ~sQ63_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f719])).
% 0.12/0.39 fof(f721,plain,(
% 0.12/0.39 $false|~sQ32_spl|~sQ16_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f606,f396])).
% 0.12/0.39 fof(f722,plain,(
% 0.12/0.39 ~sQ32_spl|~sQ16_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f721])).
% 0.12/0.39 fof(f730,plain,(
% 0.12/0.39 ~product(e_1,e_1,e_1)|~sQ62_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f505,f80])).
% 0.12/0.39 fof(f731,plain,(
% 0.12/0.39 $false|~sQ62_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f730,f68])).
% 0.12/0.39 fof(f732,plain,(
% 0.12/0.39 ~sQ62_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f731])).
% 0.12/0.39 fof(f755,plain,(
% 0.12/0.39 ~product(e_1,e_1,e_1)|~sQ56_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f486,f73])).
% 0.12/0.39 fof(f758,plain,(
% 0.12/0.39 $false|~sQ56_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f755,f68])).
% 0.12/0.39 fof(f759,plain,(
% 0.12/0.39 ~sQ56_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f758])).
% 0.12/0.39 fof(f762,plain,(
% 0.12/0.39 ~product(e_2,e_1,e_4)|~sQ55_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f482,f102])).
% 0.12/0.39 fof(f770,plain,(
% 0.12/0.39 $false|~sQ59_spl|~sQ55_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f762,f495])).
% 0.12/0.39 fof(f771,plain,(
% 0.12/0.39 ~sQ59_spl|~sQ55_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f770])).
% 0.12/0.39 fof(f776,plain,(
% 0.12/0.39 ![X0]: (~product(X0,e_3,e_1)|~product(X0,e_2,e_2)|~sQ53_spl)),
% 0.12/0.39 inference(resolution,[status(thm)],[f476,f94])).
% 0.12/0.39 fof(f783,plain,(
% 0.12/0.39 ~product(e_1,e_1,e_1)|~sQ52_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f473,f78])).
% 0.12/0.39 fof(f785,plain,(
% 0.12/0.39 $false|~sQ52_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f783,f68])).
% 0.12/0.39 fof(f786,plain,(
% 0.12/0.39 ~sQ52_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f785])).
% 0.12/0.39 fof(f823,plain,(
% 0.12/0.39 ~product(e_1,e_3,e_2)|~sQ13_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f215,f123])).
% 0.12/0.39 fof(f829,plain,(
% 0.12/0.39 ~sQ29_spl|~sQ13_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f823,f285,f214])).
% 0.12/0.39 fof(f831,plain,(
% 0.12/0.39 $false|~sQ10_spl|~sQ58_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f492,f322])).
% 0.12/0.39 fof(f832,plain,(
% 0.12/0.39 ~sQ10_spl|~sQ58_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f831])).
% 0.12/0.39 fof(f859,plain,(
% 0.12/0.39 ~product(e_2,e_2,e_2)|~sQ24_spl|~sQ53_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f270,f776])).
% 0.12/0.39 fof(f864,plain,(
% 0.12/0.39 $false|~sQ24_spl|~sQ53_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f859,f68])).
% 0.12/0.39 fof(f865,plain,(
% 0.12/0.39 ~sQ24_spl|~sQ53_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f864])).
% 0.12/0.39 fof(f866,plain,(
% 0.12/0.39 $false),
% 0.12/0.39 inference(sat_refutation,[status(thm)],[f210,f223,f225,f227,f229,f255,f268,f281,f294,f296,f298,f300,f302,f304,f314,f336,f407,f448,f450,f452,f454,f484,f497,f512,f514,f516,f529,f542,f553,f555,f571,f585,f597,f631,f668,f690,f701,f720,f722,f732,f759,f771,f786,f829,f832,f865])).
% 0.12/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.41 % Elapsed time: 0.055382 seconds
% 0.12/0.41 % CPU time: 0.178928 seconds
% 0.12/0.41 % Total memory used: 19.087 MB
% 0.12/0.41 % Net memory used: 18.777 MB
%------------------------------------------------------------------------------