%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP126-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 : n026.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:51 PM UTC 2026
% Result : Unsatisfiable 0.08s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP126-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 : n026.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 20:02:23 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.08/0.40 % Refutation found
% 0.08/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.08/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.40 fof(f2,axiom,(
% 0.08/0.40 next(e_2,e_3) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f9,axiom,(
% 0.08/0.40 greater(e_4,e_3) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f10,axiom,(
% 0.08/0.40 (![X,Y,X1]: (( ~ product(X,e_1,Y)| ~ next(X,X1)| ~ greater(Y,X1) ) ))),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f11,axiom,(
% 0.08/0.40 group_element(e_1) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f12,axiom,(
% 0.08/0.40 group_element(e_2) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f13,axiom,(
% 0.08/0.40 group_element(e_3) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f14,axiom,(
% 0.08/0.40 group_element(e_4) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f15,axiom,(
% 0.08/0.40 ~ equalish(e_1,e_2) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f16,axiom,(
% 0.08/0.40 ~ equalish(e_1,e_3) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f17,axiom,(
% 0.08/0.40 ~ equalish(e_1,e_4) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f18,axiom,(
% 0.08/0.40 ~ equalish(e_2,e_1) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f19,axiom,(
% 0.08/0.40 ~ equalish(e_2,e_3) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f20,axiom,(
% 0.08/0.40 ~ equalish(e_2,e_4) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f21,axiom,(
% 0.08/0.40 ~ equalish(e_3,e_1) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f22,axiom,(
% 0.08/0.40 ~ equalish(e_3,e_2) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f23,axiom,(
% 0.08/0.40 ~ equalish(e_3,e_4) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f24,axiom,(
% 0.08/0.40 ~ equalish(e_4,e_1) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f25,axiom,(
% 0.08/0.40 ~ equalish(e_4,e_2) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f26,axiom,(
% 0.08/0.40 ~ equalish(e_4,e_3) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f27,axiom,(
% 0.08/0.40 (![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.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f28,axiom,(
% 0.08/0.40 (![X,Y,W,Z]: (( ~ product(X,Y,W)| ~ product(X,Y,Z)| equalish(W,Z) ) ))),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f29,axiom,(
% 0.08/0.40 (![X,W,Y,Z]: (( ~ product(X,W,Y)| ~ product(X,Z,Y)| equalish(W,Z) ) ))),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f30,axiom,(
% 0.08/0.40 (![W,Y,X,Z]: (( ~ product(W,Y,X)| ~ product(Z,Y,X)| equalish(W,Z) ) ))),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f31,axiom,(
% 0.08/0.40 (![X]: (product(X,X,X) ))),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f32,negated_conjecture,(
% 0.08/0.40 (![X,Y,Z1,Z2]: (( ~ product(X,Y,Z1)| ~ product(Y,X,Z2)| product(Z1,Z2,Y) ) ))),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f34,plain,(
% 0.08/0.40 next(e_2,e_3)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f2])).
% 0.08/0.40 fof(f41,plain,(
% 0.08/0.40 greater(e_4,e_3)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f9])).
% 0.08/0.40 fof(f42,plain,(
% 0.08/0.40 ![Y,X1]: ((![X]: (~product(X,e_1,Y)|~next(X,X1)))|~greater(Y,X1))),
% 0.08/0.40 inference(miniscoping,[status(thm)],[f10])).
% 0.08/0.40 fof(f43,plain,(
% 0.08/0.40 ![X0,X1,X2]: (~product(X0,e_1,X1)|~next(X0,X2)|~greater(X1,X2))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.08/0.40 fof(f44,plain,(
% 0.08/0.40 group_element(e_1)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f11])).
% 0.08/0.40 fof(f45,plain,(
% 0.08/0.40 group_element(e_2)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.08/0.40 fof(f46,plain,(
% 0.08/0.40 group_element(e_3)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f13])).
% 0.08/0.40 fof(f47,plain,(
% 0.08/0.40 group_element(e_4)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f14])).
% 0.08/0.40 fof(f48,plain,(
% 0.08/0.40 ~equalish(e_1,e_2)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f15])).
% 0.08/0.40 fof(f49,plain,(
% 0.08/0.40 ~equalish(e_1,e_3)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f16])).
% 0.08/0.40 fof(f50,plain,(
% 0.08/0.40 ~equalish(e_1,e_4)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f17])).
% 0.08/0.40 fof(f51,plain,(
% 0.08/0.40 ~equalish(e_2,e_1)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f18])).
% 0.08/0.40 fof(f52,plain,(
% 0.08/0.40 ~equalish(e_2,e_3)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f19])).
% 0.08/0.40 fof(f53,plain,(
% 0.08/0.40 ~equalish(e_2,e_4)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f20])).
% 0.08/0.40 fof(f54,plain,(
% 0.08/0.40 ~equalish(e_3,e_1)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f21])).
% 0.08/0.40 fof(f55,plain,(
% 0.08/0.40 ~equalish(e_3,e_2)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.08/0.40 fof(f56,plain,(
% 0.08/0.40 ~equalish(e_3,e_4)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f23])).
% 0.08/0.40 fof(f57,plain,(
% 0.08/0.40 ~equalish(e_4,e_1)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f24])).
% 0.08/0.40 fof(f58,plain,(
% 0.08/0.40 ~equalish(e_4,e_2)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f25])).
% 0.08/0.40 fof(f59,plain,(
% 0.08/0.40 ~equalish(e_4,e_3)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f26])).
% 0.08/0.40 fof(f60,plain,(
% 0.08/0.40 ![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.08/0.40 inference(cnf_transformation,[status(thm)],[f27])).
% 0.08/0.40 fof(f61,plain,(
% 0.08/0.40 ![W,Z]: ((![X,Y]: (~product(X,Y,W)|~product(X,Y,Z)))|equalish(W,Z))),
% 0.08/0.40 inference(miniscoping,[status(thm)],[f28])).
% 0.08/0.40 fof(f62,plain,(
% 0.08/0.40 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|equalish(X2,X3))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f61])).
% 0.08/0.40 fof(f63,plain,(
% 0.08/0.40 ![W,Z]: ((![X,Y]: (~product(X,W,Y)|~product(X,Z,Y)))|equalish(W,Z))),
% 0.08/0.40 inference(miniscoping,[status(thm)],[f29])).
% 0.08/0.40 fof(f64,plain,(
% 0.08/0.40 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X3,X2)|equalish(X1,X3))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.08/0.40 fof(f65,plain,(
% 0.08/0.40 ![W,Z]: ((![Y,X]: (~product(W,Y,X)|~product(Z,Y,X)))|equalish(W,Z))),
% 0.08/0.40 inference(miniscoping,[status(thm)],[f30])).
% 0.08/0.40 fof(f66,plain,(
% 0.08/0.40 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X3,X1,X2)|equalish(X0,X3))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f65])).
% 0.08/0.40 fof(f67,plain,(
% 0.08/0.40 ![X0]: (product(X0,X0,X0))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f31])).
% 0.08/0.40 fof(f68,plain,(
% 0.08/0.40 ![Y,Z1,Z2]: ((![X]: (~product(X,Y,Z1)|~product(Y,X,Z2)))|product(Z1,Z2,Y))),
% 0.08/0.40 inference(miniscoping,[status(thm)],[f32])).
% 0.08/0.40 fof(f69,plain,(
% 0.08/0.40 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X1,X0,X3)|product(X2,X3,X1))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f68])).
% 0.08/0.40 fof(f72,plain,(
% 0.08/0.40 ![X0,X1]: (~product(X0,X0,X1)|equalish(X1,X0))),
% 0.08/0.40 inference(resolution,[status(thm)],[f62,f67])).
% 0.08/0.40 fof(f74,plain,(
% 0.08/0.40 ![X0,X1]: (~product(X0,X1,X0)|equalish(X1,X0))),
% 0.08/0.40 inference(resolution,[status(thm)],[f64,f67])).
% 0.08/0.40 fof(f75,plain,(
% 0.08/0.40 ![X0,X1]: (~product(X0,X1,X1)|equalish(X0,X1))),
% 0.08/0.40 inference(resolution,[status(thm)],[f66,f67])).
% 0.08/0.40 fof(f77,plain,(
% 0.08/0.40 ![X0]: (~group_element(X0)|product(e_4,X0,e_1)|product(e_4,X0,e_2)|product(e_4,X0,e_3)|product(e_4,X0,e_4))),
% 0.08/0.40 inference(resolution,[status(thm)],[f60,f47])).
% 0.08/0.40 fof(f78,plain,(
% 0.08/0.40 ![X0]: (~group_element(X0)|product(e_3,X0,e_1)|product(e_3,X0,e_2)|product(e_3,X0,e_3)|product(e_3,X0,e_4))),
% 0.08/0.40 inference(resolution,[status(thm)],[f60,f46])).
% 0.08/0.40 fof(f79,plain,(
% 0.08/0.40 ![X0]: (~group_element(X0)|product(e_2,X0,e_1)|product(e_2,X0,e_2)|product(e_2,X0,e_3)|product(e_2,X0,e_4))),
% 0.08/0.40 inference(resolution,[status(thm)],[f60,f45])).
% 0.08/0.40 fof(f82,plain,(
% 0.08/0.40 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.08/0.40 inference(resolution,[status(thm)],[f77,f46])).
% 0.08/0.40 fof(f84,plain,(
% 0.08/0.40 product(e_4,e_1,e_1)|product(e_4,e_1,e_2)|product(e_4,e_1,e_3)|product(e_4,e_1,e_4)),
% 0.08/0.40 inference(resolution,[status(thm)],[f77,f44])).
% 0.08/0.40 fof(f98,definition,(
% 0.08/0.40 sQ4_spl <=> (product(e_4,e_3,e_1))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f99,plain,(
% 0.08/0.40 product(e_4,e_3,e_1)|~sQ4_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f98])).
% 0.08/0.40 fof(f101,definition,(
% 0.08/0.40 sQ5_spl <=> (product(e_4,e_3,e_2))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f102,plain,(
% 0.08/0.40 product(e_4,e_3,e_2)|~sQ5_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f101])).
% 0.08/0.40 fof(f104,definition,(
% 0.08/0.40 sQ6_spl <=> (product(e_4,e_3,e_3))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f105,plain,(
% 0.08/0.40 product(e_4,e_3,e_3)|~sQ6_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f104])).
% 0.08/0.40 fof(f107,definition,(
% 0.08/0.40 sQ7_spl <=> (product(e_4,e_3,e_4))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f108,plain,(
% 0.08/0.40 product(e_4,e_3,e_4)|~sQ7_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f107])).
% 0.08/0.40 fof(f110,plain,(
% 0.08/0.40 sQ4_spl|sQ5_spl|sQ6_spl|sQ7_spl),
% 0.08/0.40 inference(split_clause,[status(thm)],[f82,f98,f101,f104,f107])).
% 0.08/0.40 fof(f114,definition,(
% 0.08/0.40 sQ9_spl <=> (product(e_4,e_2,e_2))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f115,plain,(
% 0.08/0.40 product(e_4,e_2,e_2)|~sQ9_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f114])).
% 0.08/0.40 fof(f120,definition,(
% 0.08/0.40 sQ11_spl <=> (product(e_4,e_2,e_4))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f121,plain,(
% 0.08/0.40 product(e_4,e_2,e_4)|~sQ11_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f120])).
% 0.08/0.40 fof(f124,definition,(
% 0.08/0.40 sQ12_spl <=> (product(e_4,e_1,e_1))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f125,plain,(
% 0.08/0.40 product(e_4,e_1,e_1)|~sQ12_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f124])).
% 0.08/0.40 fof(f127,definition,(
% 0.08/0.40 sQ13_spl <=> (product(e_4,e_1,e_2))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f128,plain,(
% 0.08/0.40 product(e_4,e_1,e_2)|~sQ13_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f127])).
% 0.08/0.40 fof(f130,definition,(
% 0.08/0.40 sQ14_spl <=> (product(e_4,e_1,e_3))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f131,plain,(
% 0.08/0.40 product(e_4,e_1,e_3)|~sQ14_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f130])).
% 0.08/0.40 fof(f133,definition,(
% 0.08/0.40 sQ15_spl <=> (product(e_4,e_1,e_4))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f134,plain,(
% 0.08/0.40 product(e_4,e_1,e_4)|~sQ15_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f133])).
% 0.08/0.40 fof(f136,plain,(
% 0.08/0.40 sQ12_spl|sQ13_spl|sQ14_spl|sQ15_spl),
% 0.08/0.40 inference(split_clause,[status(thm)],[f84,f124,f127,f130,f133])).
% 0.08/0.40 fof(f137,plain,(
% 0.08/0.40 product(e_3,e_4,e_1)|product(e_3,e_4,e_2)|product(e_3,e_4,e_3)|product(e_3,e_4,e_4)),
% 0.08/0.40 inference(resolution,[status(thm)],[f78,f47])).
% 0.08/0.40 fof(f139,plain,(
% 0.08/0.40 product(e_3,e_2,e_1)|product(e_3,e_2,e_2)|product(e_3,e_2,e_3)|product(e_3,e_2,e_4)),
% 0.08/0.40 inference(resolution,[status(thm)],[f78,f45])).
% 0.08/0.40 fof(f140,plain,(
% 0.08/0.40 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.08/0.40 inference(resolution,[status(thm)],[f78,f44])).
% 0.08/0.40 fof(f141,definition,(
% 0.08/0.40 sQ16_spl <=> (product(e_3,e_4,e_1))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f142,plain,(
% 0.08/0.40 product(e_3,e_4,e_1)|~sQ16_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f141])).
% 0.08/0.40 fof(f144,definition,(
% 0.08/0.40 sQ17_spl <=> (product(e_3,e_4,e_2))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f145,plain,(
% 0.08/0.40 product(e_3,e_4,e_2)|~sQ17_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f144])).
% 0.08/0.40 fof(f147,definition,(
% 0.08/0.40 sQ18_spl <=> (product(e_3,e_4,e_3))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f148,plain,(
% 0.08/0.40 product(e_3,e_4,e_3)|~sQ18_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f147])).
% 0.08/0.40 fof(f150,definition,(
% 0.08/0.40 sQ19_spl <=> (product(e_3,e_4,e_4))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f151,plain,(
% 0.08/0.40 product(e_3,e_4,e_4)|~sQ19_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f150])).
% 0.08/0.40 fof(f153,plain,(
% 0.08/0.40 sQ16_spl|sQ17_spl|sQ18_spl|sQ19_spl),
% 0.08/0.40 inference(split_clause,[status(thm)],[f137,f141,f144,f147,f150])).
% 0.08/0.40 fof(f157,definition,(
% 0.08/0.40 sQ21_spl <=> (product(e_3,e_3,e_2))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f158,plain,(
% 0.08/0.40 product(e_3,e_3,e_2)|~sQ21_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f157])).
% 0.08/0.40 fof(f167,definition,(
% 0.08/0.40 sQ24_spl <=> (product(e_3,e_2,e_1))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f168,plain,(
% 0.08/0.40 product(e_3,e_2,e_1)|~sQ24_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f167])).
% 0.08/0.40 fof(f170,definition,(
% 0.08/0.40 sQ25_spl <=> (product(e_3,e_2,e_2))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f171,plain,(
% 0.08/0.40 product(e_3,e_2,e_2)|~sQ25_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f170])).
% 0.08/0.40 fof(f173,definition,(
% 0.08/0.40 sQ26_spl <=> (product(e_3,e_2,e_3))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f174,plain,(
% 0.08/0.40 product(e_3,e_2,e_3)|~sQ26_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f173])).
% 0.08/0.40 fof(f176,definition,(
% 0.08/0.40 sQ27_spl <=> (product(e_3,e_2,e_4))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f177,plain,(
% 0.08/0.40 product(e_3,e_2,e_4)|~sQ27_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f176])).
% 0.08/0.40 fof(f179,plain,(
% 0.08/0.40 sQ24_spl|sQ25_spl|sQ26_spl|sQ27_spl),
% 0.08/0.40 inference(split_clause,[status(thm)],[f139,f167,f170,f173,f176])).
% 0.08/0.40 fof(f180,definition,(
% 0.08/0.40 sQ28_spl <=> (product(e_3,e_1,e_1))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f181,plain,(
% 0.08/0.40 product(e_3,e_1,e_1)|~sQ28_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f180])).
% 0.08/0.40 fof(f183,definition,(
% 0.08/0.40 sQ29_spl <=> (product(e_3,e_1,e_2))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f186,definition,(
% 0.08/0.40 sQ30_spl <=> (product(e_3,e_1,e_3))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f187,plain,(
% 0.08/0.40 product(e_3,e_1,e_3)|~sQ30_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f186])).
% 0.08/0.40 fof(f189,definition,(
% 0.08/0.40 sQ31_spl <=> (product(e_3,e_1,e_4))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f190,plain,(
% 0.08/0.40 product(e_3,e_1,e_4)|~sQ31_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f189])).
% 0.08/0.40 fof(f192,plain,(
% 0.08/0.40 sQ28_spl|sQ29_spl|sQ30_spl|sQ31_spl),
% 0.08/0.40 inference(split_clause,[status(thm)],[f140,f180,f183,f186,f189])).
% 0.08/0.40 fof(f194,plain,(
% 0.08/0.40 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.08/0.40 inference(resolution,[status(thm)],[f79,f46])).
% 0.08/0.40 fof(f196,plain,(
% 0.08/0.40 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.08/0.40 inference(resolution,[status(thm)],[f79,f44])).
% 0.08/0.40 fof(f210,definition,(
% 0.08/0.40 sQ36_spl <=> (product(e_2,e_3,e_1))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f211,plain,(
% 0.08/0.40 product(e_2,e_3,e_1)|~sQ36_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f210])).
% 0.08/0.40 fof(f213,definition,(
% 0.08/0.40 sQ37_spl <=> (product(e_2,e_3,e_2))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f214,plain,(
% 0.08/0.40 product(e_2,e_3,e_2)|~sQ37_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f213])).
% 0.08/0.40 fof(f216,definition,(
% 0.08/0.40 sQ38_spl <=> (product(e_2,e_3,e_3))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f217,plain,(
% 0.08/0.40 product(e_2,e_3,e_3)|~sQ38_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f216])).
% 0.08/0.40 fof(f219,definition,(
% 0.08/0.40 sQ39_spl <=> (product(e_2,e_3,e_4))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f220,plain,(
% 0.08/0.40 product(e_2,e_3,e_4)|~sQ39_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f219])).
% 0.08/0.40 fof(f222,plain,(
% 0.08/0.40 sQ36_spl|sQ37_spl|sQ38_spl|sQ39_spl),
% 0.08/0.40 inference(split_clause,[status(thm)],[f194,f210,f213,f216,f219])).
% 0.08/0.40 fof(f232,definition,(
% 0.08/0.40 sQ43_spl <=> (product(e_2,e_2,e_4))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f233,plain,(
% 0.08/0.40 product(e_2,e_2,e_4)|~sQ43_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f232])).
% 0.08/0.40 fof(f236,definition,(
% 0.08/0.40 sQ44_spl <=> (product(e_2,e_1,e_1))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f237,plain,(
% 0.08/0.40 product(e_2,e_1,e_1)|~sQ44_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f236])).
% 0.08/0.40 fof(f239,definition,(
% 0.08/0.40 sQ45_spl <=> (product(e_2,e_1,e_2))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f240,plain,(
% 0.08/0.40 product(e_2,e_1,e_2)|~sQ45_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f239])).
% 0.08/0.40 fof(f242,definition,(
% 0.08/0.40 sQ46_spl <=> (product(e_2,e_1,e_3))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f243,plain,(
% 0.08/0.40 product(e_2,e_1,e_3)|~sQ46_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f242])).
% 0.08/0.40 fof(f245,definition,(
% 0.08/0.40 sQ47_spl <=> (product(e_2,e_1,e_4))),
% 0.08/0.40 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.08/0.40 fof(f246,plain,(
% 0.08/0.40 product(e_2,e_1,e_4)|~sQ47_spl),
% 0.08/0.40 inference(component_clause,[status(thm)],[f245])).
% 0.08/0.40 fof(f248,plain,(
% 0.08/0.40 sQ44_spl|sQ45_spl|sQ46_spl|sQ47_spl),
% 0.08/0.40 inference(split_clause,[status(thm)],[f196,f236,f239,f242,f245])).
% 0.08/0.40 fof(f308,plain,(
% 0.08/0.40 equalish(e_1,e_4)|~sQ15_spl),
% 0.08/0.40 inference(resolution,[status(thm)],[f134,f74])).
% 0.08/0.40 fof(f313,plain,(
% 0.08/0.40 $false|~sQ15_spl),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f308,f50])).
% 0.08/0.40 fof(f314,plain,(
% 0.08/0.40 ~sQ15_spl),
% 0.08/0.40 inference(contradiction_clause,[status(thm)],[f313])).
% 0.08/0.40 fof(f316,plain,(
% 0.08/0.40 ![X0]: (~product(X0,e_1,e_3)|equalish(X0,e_4)|~sQ14_spl)),
% 0.08/0.40 inference(resolution,[status(thm)],[f131,f66])).
% 0.08/0.40 fof(f319,plain,(
% 0.08/0.40 ![X0]: (~product(e_1,e_4,X0)|product(X0,e_3,e_4)|~sQ14_spl)),
% 0.08/0.40 inference(resolution,[status(thm)],[f131,f69])).
% 0.08/0.40 fof(f326,plain,(
% 0.08/0.40 ![X0]: (~product(e_4,X0,e_2)|equalish(X0,e_1)|~sQ13_spl)),
% 0.08/0.40 inference(resolution,[status(thm)],[f128,f64])).
% 0.08/0.40 fof(f332,plain,(
% 0.08/0.40 equalish(e_4,e_1)|~sQ12_spl),
% 0.08/0.40 inference(resolution,[status(thm)],[f125,f75])).
% 0.08/0.40 fof(f337,plain,(
% 0.08/0.40 $false|~sQ12_spl),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f332,f57])).
% 0.08/0.40 fof(f338,plain,(
% 0.08/0.40 ~sQ12_spl),
% 0.08/0.40 inference(contradiction_clause,[status(thm)],[f337])).
% 0.08/0.40 fof(f339,plain,(
% 0.08/0.40 equalish(e_2,e_4)|~sQ11_spl),
% 0.08/0.40 inference(resolution,[status(thm)],[f121,f74])).
% 0.08/0.40 fof(f344,plain,(
% 0.08/0.40 $false|~sQ11_spl),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f339,f53])).
% 0.08/0.40 fof(f345,plain,(
% 0.08/0.40 ~sQ11_spl),
% 0.08/0.40 inference(contradiction_clause,[status(thm)],[f344])).
% 0.08/0.40 fof(f355,plain,(
% 0.08/0.40 equalish(e_4,e_2)|~sQ9_spl),
% 0.08/0.40 inference(resolution,[status(thm)],[f115,f75])).
% 0.08/0.40 fof(f369,plain,(
% 0.08/0.40 equalish(e_3,e_4)|~sQ7_spl),
% 0.08/0.40 inference(resolution,[status(thm)],[f108,f74])).
% 0.08/0.40 fof(f374,plain,(
% 0.08/0.40 $false|~sQ7_spl),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f369,f56])).
% 0.08/0.40 fof(f375,plain,(
% 0.08/0.40 ~sQ7_spl),
% 0.08/0.40 inference(contradiction_clause,[status(thm)],[f374])).
% 0.08/0.40 fof(f376,plain,(
% 0.08/0.40 equalish(e_4,e_3)|~sQ6_spl),
% 0.08/0.40 inference(resolution,[status(thm)],[f105,f75])).
% 0.08/0.40 fof(f381,plain,(
% 0.08/0.40 $false|~sQ6_spl),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f376,f59])).
% 0.08/0.40 fof(f382,plain,(
% 0.08/0.40 ~sQ6_spl),
% 0.08/0.40 inference(contradiction_clause,[status(thm)],[f381])).
% 0.08/0.40 fof(f383,plain,(
% 0.08/0.40 equalish(e_3,e_1)|~sQ5_spl|~sQ13_spl),
% 0.08/0.40 inference(resolution,[status(thm)],[f102,f326])).
% 0.08/0.40 fof(f384,plain,(
% 0.08/0.40 ![X0]: (~product(X0,e_3,e_2)|equalish(X0,e_4)|~sQ5_spl)),
% 0.08/0.40 inference(resolution,[status(thm)],[f102,f66])).
% 0.08/0.40 fof(f388,plain,(
% 0.08/0.40 $false|~sQ5_spl|~sQ13_spl),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f383,f54])).
% 0.08/0.40 fof(f389,plain,(
% 0.08/0.40 ~sQ5_spl|~sQ13_spl),
% 0.08/0.40 inference(contradiction_clause,[status(thm)],[f388])).
% 0.08/0.40 fof(f394,plain,(
% 0.08/0.40 ![X0]: (~product(e_3,e_4,X0)|product(X0,e_1,e_4)|~sQ4_spl)),
% 0.08/0.40 inference(resolution,[status(thm)],[f99,f69])).
% 0.08/0.40 fof(f403,plain,(
% 0.08/0.40 ![X0]: (~product(X0,e_1,e_4)|equalish(X0,e_3)|~sQ31_spl)),
% 0.08/0.40 inference(resolution,[status(thm)],[f190,f66])).
% 0.08/0.40 fof(f412,plain,(
% 0.08/0.40 equalish(e_1,e_3)|~sQ30_spl),
% 0.08/0.40 inference(resolution,[status(thm)],[f187,f74])).
% 0.08/0.40 fof(f428,plain,(
% 0.08/0.40 equalish(e_3,e_1)|~sQ28_spl),
% 0.08/0.40 inference(resolution,[status(thm)],[f181,f75])).
% 0.08/0.40 fof(f433,plain,(
% 0.08/0.40 $false|~sQ28_spl),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f428,f54])).
% 0.08/0.40 fof(f434,plain,(
% 0.08/0.40 ~sQ28_spl),
% 0.08/0.40 inference(contradiction_clause,[status(thm)],[f433])).
% 0.08/0.40 fof(f435,plain,(
% 0.08/0.40 $false|~sQ30_spl),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f412,f49])).
% 0.08/0.40 fof(f436,plain,(
% 0.08/0.40 ~sQ30_spl),
% 0.08/0.40 inference(contradiction_clause,[status(thm)],[f435])).
% 0.08/0.40 fof(f439,plain,(
% 0.08/0.40 ![X0]: (~product(e_3,X0,e_4)|equalish(X0,e_2)|~sQ27_spl)),
% 0.08/0.40 inference(resolution,[status(thm)],[f177,f64])).
% 0.08/0.40 fof(f441,plain,(
% 0.08/0.40 ![X0]: (~product(e_2,e_3,X0)|product(X0,e_4,e_3)|~sQ27_spl)),
% 0.08/0.40 inference(resolution,[status(thm)],[f177,f69])).
% 0.08/0.40 fof(f445,plain,(
% 0.08/0.40 equalish(e_2,e_3)|~sQ26_spl),
% 0.08/0.40 inference(resolution,[status(thm)],[f174,f74])).
% 0.08/0.40 fof(f452,plain,(
% 0.08/0.40 equalish(e_3,e_2)|~sQ25_spl),
% 0.08/0.40 inference(resolution,[status(thm)],[f171,f75])).
% 0.08/0.40 fof(f457,plain,(
% 0.08/0.40 $false|~sQ25_spl),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f452,f55])).
% 0.08/0.40 fof(f458,plain,(
% 0.08/0.40 ~sQ25_spl),
% 0.08/0.40 inference(contradiction_clause,[status(thm)],[f457])).
% 0.08/0.40 fof(f462,plain,(
% 0.08/0.40 ![X0]: (~product(e_2,e_3,X0)|product(X0,e_1,e_3)|~sQ24_spl)),
% 0.08/0.40 inference(resolution,[status(thm)],[f168,f69])).
% 0.08/0.40 fof(f477,plain,(
% 0.08/0.40 equalish(e_2,e_3)|~sQ21_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f158,f72])).
% 0.08/0.41 fof(f481,plain,(
% 0.08/0.41 $false|~sQ21_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f477,f52])).
% 0.08/0.41 fof(f482,plain,(
% 0.08/0.41 ~sQ21_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f481])).
% 0.08/0.41 fof(f493,plain,(
% 0.08/0.41 product(e_4,e_1,e_4)|~sQ19_spl|~sQ4_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f151,f394])).
% 0.08/0.41 fof(f500,plain,(
% 0.08/0.41 sQ15_spl|~sQ19_spl|~sQ4_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f493,f133,f150,f98])).
% 0.08/0.41 fof(f504,plain,(
% 0.08/0.41 equalish(e_4,e_3)|~sQ18_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f148,f74])).
% 0.08/0.41 fof(f509,plain,(
% 0.08/0.41 $false|~sQ18_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f504,f59])).
% 0.08/0.41 fof(f510,plain,(
% 0.08/0.41 ~sQ18_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f509])).
% 0.08/0.41 fof(f511,plain,(
% 0.08/0.41 product(e_2,e_1,e_4)|~sQ17_spl|~sQ4_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f145,f394])).
% 0.08/0.41 fof(f516,plain,(
% 0.08/0.41 product(e_1,e_1,e_4)|~sQ16_spl|~sQ4_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f142,f394])).
% 0.08/0.41 fof(f524,plain,(
% 0.08/0.41 equalish(e_2,e_3)|~sQ47_spl|~sQ31_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f246,f403])).
% 0.08/0.41 fof(f527,plain,(
% 0.08/0.41 ![X0]: (~product(e_2,X0,e_4)|equalish(X0,e_1)|~sQ47_spl)),
% 0.08/0.41 inference(resolution,[status(thm)],[f246,f64])).
% 0.08/0.41 fof(f530,plain,(
% 0.08/0.41 $false|~sQ47_spl|~sQ31_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f524,f52])).
% 0.08/0.41 fof(f531,plain,(
% 0.08/0.41 ~sQ47_spl|~sQ31_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f530])).
% 0.08/0.41 fof(f539,plain,(
% 0.08/0.41 equalish(e_1,e_2)|~sQ45_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f240,f74])).
% 0.08/0.41 fof(f547,plain,(
% 0.08/0.41 ![X0]: (~next(e_2,X0)|~greater(e_4,X0)|~sQ17_spl|~sQ4_spl)),
% 0.08/0.41 inference(resolution,[status(thm)],[f511,f43])).
% 0.08/0.41 fof(f554,plain,(
% 0.08/0.41 $false|~sQ9_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f355,f58])).
% 0.08/0.41 fof(f555,plain,(
% 0.08/0.41 ~sQ9_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f554])).
% 0.08/0.41 fof(f559,plain,(
% 0.08/0.41 equalish(e_4,e_1)|~sQ16_spl|~sQ4_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f516,f72])).
% 0.08/0.41 fof(f563,plain,(
% 0.08/0.41 $false|~sQ16_spl|~sQ4_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f559,f57])).
% 0.08/0.41 fof(f564,plain,(
% 0.08/0.41 ~sQ16_spl|~sQ4_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f563])).
% 0.08/0.41 fof(f570,plain,(
% 0.08/0.41 ~next(e_2,e_3)|~sQ17_spl|~sQ4_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f547,f41])).
% 0.08/0.41 fof(f573,plain,(
% 0.08/0.41 $false|~sQ17_spl|~sQ4_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f570,f34])).
% 0.08/0.41 fof(f574,plain,(
% 0.08/0.41 ~sQ17_spl|~sQ4_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f573])).
% 0.08/0.41 fof(f578,plain,(
% 0.08/0.41 equalish(e_2,e_4)|~sQ14_spl|~sQ46_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f316,f243])).
% 0.08/0.41 fof(f579,plain,(
% 0.08/0.41 $false|~sQ14_spl|~sQ46_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f578,f53])).
% 0.08/0.41 fof(f580,plain,(
% 0.08/0.41 ~sQ14_spl|~sQ46_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f579])).
% 0.08/0.41 fof(f582,plain,(
% 0.08/0.41 equalish(e_2,e_1)|~sQ44_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f237,f75])).
% 0.08/0.41 fof(f587,plain,(
% 0.08/0.41 $false|~sQ44_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f582,f51])).
% 0.08/0.41 fof(f588,plain,(
% 0.08/0.41 ~sQ44_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f587])).
% 0.08/0.41 fof(f589,plain,(
% 0.08/0.41 $false|~sQ45_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f539,f48])).
% 0.08/0.41 fof(f590,plain,(
% 0.08/0.41 ~sQ45_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f589])).
% 0.08/0.41 fof(f591,plain,(
% 0.08/0.41 equalish(e_2,e_1)|~sQ43_spl|~sQ47_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f233,f527])).
% 0.08/0.41 fof(f598,plain,(
% 0.08/0.41 $false|~sQ43_spl|~sQ47_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f591,f51])).
% 0.08/0.41 fof(f599,plain,(
% 0.08/0.41 ~sQ43_spl|~sQ47_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f598])).
% 0.08/0.41 fof(f619,plain,(
% 0.08/0.41 equalish(e_3,e_1)|~sQ39_spl|~sQ47_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f220,f527])).
% 0.08/0.41 fof(f624,plain,(
% 0.08/0.41 $false|~sQ39_spl|~sQ47_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f619,f54])).
% 0.08/0.41 fof(f625,plain,(
% 0.08/0.41 ~sQ39_spl|~sQ47_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f624])).
% 0.08/0.41 fof(f627,plain,(
% 0.08/0.41 equalish(e_2,e_3)|~sQ38_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f217,f75])).
% 0.08/0.41 fof(f633,plain,(
% 0.08/0.41 $false|~sQ38_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f627,f52])).
% 0.08/0.41 fof(f634,plain,(
% 0.08/0.41 ~sQ38_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f633])).
% 0.08/0.41 fof(f636,plain,(
% 0.08/0.41 equalish(e_2,e_4)|~sQ37_spl|~sQ5_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f214,f384])).
% 0.08/0.41 fof(f643,plain,(
% 0.08/0.41 $false|~sQ37_spl|~sQ5_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f636,f53])).
% 0.08/0.41 fof(f644,plain,(
% 0.08/0.41 ~sQ37_spl|~sQ5_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f643])).
% 0.08/0.41 fof(f645,plain,(
% 0.08/0.41 $false|~sQ26_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f445,f52])).
% 0.08/0.41 fof(f646,plain,(
% 0.08/0.41 ~sQ26_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f645])).
% 0.08/0.41 fof(f647,plain,(
% 0.08/0.41 product(e_1,e_4,e_3)|~sQ36_spl|~sQ27_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f211,f441])).
% 0.08/0.41 fof(f652,plain,(
% 0.08/0.41 product(e_3,e_3,e_4)|~sQ36_spl|~sQ27_spl|~sQ14_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f647,f319])).
% 0.08/0.41 fof(f657,plain,(
% 0.08/0.41 equalish(e_3,e_2)|~sQ36_spl|~sQ14_spl|~sQ27_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f652,f439])).
% 0.08/0.41 fof(f664,plain,(
% 0.08/0.41 $false|~sQ36_spl|~sQ14_spl|~sQ27_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f657,f55])).
% 0.08/0.41 fof(f665,plain,(
% 0.08/0.41 ~sQ36_spl|~sQ14_spl|~sQ27_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f664])).
% 0.08/0.41 fof(f666,plain,(
% 0.08/0.41 product(e_1,e_1,e_3)|~sQ24_spl|~sQ36_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f462,f211])).
% 0.08/0.41 fof(f667,plain,(
% 0.08/0.41 equalish(e_1,e_4)|~sQ24_spl|~sQ36_spl|~sQ14_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f666,f316])).
% 0.08/0.41 fof(f675,plain,(
% 0.08/0.41 $false|~sQ24_spl|~sQ36_spl|~sQ14_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f667,f50])).
% 0.08/0.41 fof(f676,plain,(
% 0.08/0.41 ~sQ24_spl|~sQ36_spl|~sQ14_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f675])).
% 0.08/0.41 fof(f677,plain,(
% 0.08/0.41 $false),
% 0.08/0.41 inference(sat_refutation,[status(thm)],[f110,f136,f153,f179,f192,f222,f248,f314,f338,f345,f375,f382,f389,f434,f436,f458,f482,f500,f510,f531,f555,f564,f574,f580,f588,f590,f599,f625,f634,f644,f646,f665,f676])).
% 0.08/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.08/0.44 % Elapsed time: 0.067941 seconds
% 0.08/0.44 % CPU time: 0.223859 seconds
% 0.08/0.44 % Total memory used: 18.297 MB
% 0.08/0.44 % Net memory used: 18.044 MB
%------------------------------------------------------------------------------