%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP129-2.004 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:56 PM UTC 2026
% Result : Unsatisfiable 1.76s 0.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP129-2.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n003.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 20 20:02:15 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 1.76/0.71 % Refutation found
% 1.76/0.71 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.76/0.71 % SZS output start CNFRefutation for theBenchmark
% 1.76/0.71 fof(f11,axiom,(
% 1.76/0.71 group_element(e_1) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f12,axiom,(
% 1.76/0.71 group_element(e_2) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f13,axiom,(
% 1.76/0.71 group_element(e_3) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f14,axiom,(
% 1.76/0.71 group_element(e_4) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f15,axiom,(
% 1.76/0.71 ~ equalish(e_1,e_2) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f16,axiom,(
% 1.76/0.71 ~ equalish(e_1,e_3) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f17,axiom,(
% 1.76/0.71 ~ equalish(e_1,e_4) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f18,axiom,(
% 1.76/0.71 ~ equalish(e_2,e_1) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f19,axiom,(
% 1.76/0.71 ~ equalish(e_2,e_3) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f20,axiom,(
% 1.76/0.71 ~ equalish(e_2,e_4) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f21,axiom,(
% 1.76/0.71 ~ equalish(e_3,e_1) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f22,axiom,(
% 1.76/0.71 ~ equalish(e_3,e_2) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f23,axiom,(
% 1.76/0.71 ~ equalish(e_3,e_4) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f24,axiom,(
% 1.76/0.71 ~ equalish(e_4,e_1) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f25,axiom,(
% 1.76/0.71 ~ equalish(e_4,e_2) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f26,axiom,(
% 1.76/0.71 ~ equalish(e_4,e_3) ),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f27,axiom,(
% 1.76/0.71 (![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) ) ))),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f28,axiom,(
% 1.76/0.71 (![X,Y,W,Z]: (( ~ product(X,Y,W)| ~ product(X,Y,Z)| equalish(W,Z) ) ))),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f29,axiom,(
% 1.76/0.71 (![X,W,Y,Z]: (( ~ product(X,W,Y)| ~ product(X,Z,Y)| equalish(W,Z) ) ))),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f30,axiom,(
% 1.76/0.71 (![W,Y,X,Z]: (( ~ product(W,Y,X)| ~ product(Z,Y,X)| equalish(W,Z) ) ))),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f31,negated_conjecture,(
% 1.76/0.71 (![Y,X,Z1,Z2]: (( ~ product(Y,X,Z1)| ~ product(X,Z1,Z2)| product(Z1,Y,Z2) ) ))),
% 1.76/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.76/0.71 fof(f43,plain,(
% 1.76/0.71 group_element(e_1)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f11])).
% 1.76/0.71 fof(f44,plain,(
% 1.76/0.71 group_element(e_2)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f12])).
% 1.76/0.71 fof(f45,plain,(
% 1.76/0.71 group_element(e_3)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f13])).
% 1.76/0.71 fof(f46,plain,(
% 1.76/0.71 group_element(e_4)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f14])).
% 1.76/0.71 fof(f47,plain,(
% 1.76/0.71 ~equalish(e_1,e_2)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f15])).
% 1.76/0.71 fof(f48,plain,(
% 1.76/0.71 ~equalish(e_1,e_3)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f16])).
% 1.76/0.71 fof(f49,plain,(
% 1.76/0.71 ~equalish(e_1,e_4)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f17])).
% 1.76/0.71 fof(f50,plain,(
% 1.76/0.71 ~equalish(e_2,e_1)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f18])).
% 1.76/0.71 fof(f51,plain,(
% 1.76/0.71 ~equalish(e_2,e_3)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f19])).
% 1.76/0.71 fof(f52,plain,(
% 1.76/0.71 ~equalish(e_2,e_4)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f20])).
% 1.76/0.71 fof(f53,plain,(
% 1.76/0.71 ~equalish(e_3,e_1)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f21])).
% 1.76/0.71 fof(f54,plain,(
% 1.76/0.71 ~equalish(e_3,e_2)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f22])).
% 1.76/0.71 fof(f55,plain,(
% 1.76/0.71 ~equalish(e_3,e_4)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f23])).
% 1.76/0.71 fof(f56,plain,(
% 1.76/0.71 ~equalish(e_4,e_1)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f24])).
% 1.76/0.71 fof(f57,plain,(
% 1.76/0.71 ~equalish(e_4,e_2)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f25])).
% 1.76/0.71 fof(f58,plain,(
% 1.76/0.71 ~equalish(e_4,e_3)),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f26])).
% 1.76/0.71 fof(f59,plain,(
% 1.76/0.71 ![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))),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f27])).
% 1.76/0.71 fof(f60,plain,(
% 1.76/0.71 ![W,Z]: ((![X,Y]: (~product(X,Y,W)|~product(X,Y,Z)))|equalish(W,Z))),
% 1.76/0.71 inference(miniscoping,[status(thm)],[f28])).
% 1.76/0.71 fof(f61,plain,(
% 1.76/0.71 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|equalish(X2,X3))),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f60])).
% 1.76/0.71 fof(f62,plain,(
% 1.76/0.71 ![W,Z]: ((![X,Y]: (~product(X,W,Y)|~product(X,Z,Y)))|equalish(W,Z))),
% 1.76/0.71 inference(miniscoping,[status(thm)],[f29])).
% 1.76/0.71 fof(f63,plain,(
% 1.76/0.71 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X3,X2)|equalish(X1,X3))),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f62])).
% 1.76/0.71 fof(f64,plain,(
% 1.76/0.71 ![W,Z]: ((![Y,X]: (~product(W,Y,X)|~product(Z,Y,X)))|equalish(W,Z))),
% 1.76/0.71 inference(miniscoping,[status(thm)],[f30])).
% 1.76/0.71 fof(f65,plain,(
% 1.76/0.71 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X3,X1,X2)|equalish(X0,X3))),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f64])).
% 1.76/0.71 fof(f66,plain,(
% 1.76/0.71 ![Y,Z1,Z2]: ((![X]: (~product(Y,X,Z1)|~product(X,Z1,Z2)))|product(Z1,Y,Z2))),
% 1.76/0.71 inference(miniscoping,[status(thm)],[f31])).
% 1.76/0.71 fof(f67,plain,(
% 1.76/0.71 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X1,X2,X3)|product(X2,X0,X3))),
% 1.76/0.71 inference(cnf_transformation,[status(thm)],[f66])).
% 1.76/0.71 fof(f68,plain,(
% 1.76/0.71 ![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))),
% 1.76/0.71 inference(resolution,[status(thm)],[f59,f45])).
% 1.76/0.71 fof(f69,plain,(
% 1.76/0.71 ![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))),
% 1.76/0.71 inference(resolution,[status(thm)],[f59,f44])).
% 1.76/0.71 fof(f70,plain,(
% 1.76/0.71 ![X0]: (~group_element(X0)|product(e_1,X0,e_1)|product(e_1,X0,e_2)|product(e_1,X0,e_3)|product(e_1,X0,e_4))),
% 1.76/0.71 inference(resolution,[status(thm)],[f59,f43])).
% 1.76/0.71 fof(f71,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f68,f45])).
% 1.76/0.71 fof(f72,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f68,f44])).
% 1.76/0.71 fof(f73,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f68,f43])).
% 1.76/0.71 fof(f74,definition,(
% 1.76/0.71 sQ0_spl <=> (product(e_3,e_3,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f75,plain,(
% 1.76/0.71 product(e_3,e_3,e_1)|~sQ0_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f74])).
% 1.76/0.71 fof(f77,definition,(
% 1.76/0.71 sQ1_spl <=> (product(e_3,e_3,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f78,plain,(
% 1.76/0.71 product(e_3,e_3,e_2)|~sQ1_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f77])).
% 1.76/0.71 fof(f80,definition,(
% 1.76/0.71 sQ2_spl <=> (product(e_3,e_3,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f81,plain,(
% 1.76/0.71 product(e_3,e_3,e_3)|~sQ2_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f80])).
% 1.76/0.71 fof(f83,definition,(
% 1.76/0.71 sQ3_spl <=> (product(e_3,e_3,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f84,plain,(
% 1.76/0.71 product(e_3,e_3,e_4)|~sQ3_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f83])).
% 1.76/0.71 fof(f86,plain,(
% 1.76/0.71 sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f71,f74,f77,f80,f83])).
% 1.76/0.71 fof(f87,definition,(
% 1.76/0.71 sQ4_spl <=> (product(e_3,e_2,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f88,plain,(
% 1.76/0.71 product(e_3,e_2,e_1)|~sQ4_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f87])).
% 1.76/0.71 fof(f90,definition,(
% 1.76/0.71 sQ5_spl <=> (product(e_3,e_2,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f91,plain,(
% 1.76/0.71 product(e_3,e_2,e_2)|~sQ5_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f90])).
% 1.76/0.71 fof(f93,definition,(
% 1.76/0.71 sQ6_spl <=> (product(e_3,e_2,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f94,plain,(
% 1.76/0.71 product(e_3,e_2,e_3)|~sQ6_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f93])).
% 1.76/0.71 fof(f96,definition,(
% 1.76/0.71 sQ7_spl <=> (product(e_3,e_2,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f97,plain,(
% 1.76/0.71 product(e_3,e_2,e_4)|~sQ7_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f96])).
% 1.76/0.71 fof(f99,plain,(
% 1.76/0.71 sQ4_spl|sQ5_spl|sQ6_spl|sQ7_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f72,f87,f90,f93,f96])).
% 1.76/0.71 fof(f100,definition,(
% 1.76/0.71 sQ8_spl <=> (product(e_3,e_1,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f101,plain,(
% 1.76/0.71 product(e_3,e_1,e_1)|~sQ8_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f100])).
% 1.76/0.71 fof(f103,definition,(
% 1.76/0.71 sQ9_spl <=> (product(e_3,e_1,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f104,plain,(
% 1.76/0.71 product(e_3,e_1,e_2)|~sQ9_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f103])).
% 1.76/0.71 fof(f106,definition,(
% 1.76/0.71 sQ10_spl <=> (product(e_3,e_1,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f107,plain,(
% 1.76/0.71 product(e_3,e_1,e_3)|~sQ10_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f106])).
% 1.76/0.71 fof(f109,definition,(
% 1.76/0.71 sQ11_spl <=> (product(e_3,e_1,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f110,plain,(
% 1.76/0.71 product(e_3,e_1,e_4)|~sQ11_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f109])).
% 1.76/0.71 fof(f112,plain,(
% 1.76/0.71 sQ8_spl|sQ9_spl|sQ10_spl|sQ11_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f73,f100,f103,f106,f109])).
% 1.76/0.71 fof(f113,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f69,f45])).
% 1.76/0.71 fof(f114,plain,(
% 1.76/0.71 product(e_2,e_2,e_1)|product(e_2,e_2,e_2)|product(e_2,e_2,e_3)|product(e_2,e_2,e_4)),
% 1.76/0.71 inference(resolution,[status(thm)],[f69,f44])).
% 1.76/0.71 fof(f115,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f69,f43])).
% 1.76/0.71 fof(f116,definition,(
% 1.76/0.71 sQ12_spl <=> (product(e_2,e_3,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f117,plain,(
% 1.76/0.71 product(e_2,e_3,e_1)|~sQ12_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f116])).
% 1.76/0.71 fof(f119,definition,(
% 1.76/0.71 sQ13_spl <=> (product(e_2,e_3,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f120,plain,(
% 1.76/0.71 product(e_2,e_3,e_2)|~sQ13_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f119])).
% 1.76/0.71 fof(f122,definition,(
% 1.76/0.71 sQ14_spl <=> (product(e_2,e_3,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f123,plain,(
% 1.76/0.71 product(e_2,e_3,e_3)|~sQ14_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f122])).
% 1.76/0.71 fof(f125,definition,(
% 1.76/0.71 sQ15_spl <=> (product(e_2,e_3,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f126,plain,(
% 1.76/0.71 product(e_2,e_3,e_4)|~sQ15_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f125])).
% 1.76/0.71 fof(f128,plain,(
% 1.76/0.71 sQ12_spl|sQ13_spl|sQ14_spl|sQ15_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f113,f116,f119,f122,f125])).
% 1.76/0.71 fof(f129,definition,(
% 1.76/0.71 sQ16_spl <=> (product(e_2,e_2,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f130,plain,(
% 1.76/0.71 product(e_2,e_2,e_1)|~sQ16_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f129])).
% 1.76/0.71 fof(f132,definition,(
% 1.76/0.71 sQ17_spl <=> (product(e_2,e_2,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f133,plain,(
% 1.76/0.71 product(e_2,e_2,e_2)|~sQ17_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f132])).
% 1.76/0.71 fof(f135,definition,(
% 1.76/0.71 sQ18_spl <=> (product(e_2,e_2,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f136,plain,(
% 1.76/0.71 product(e_2,e_2,e_3)|~sQ18_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f135])).
% 1.76/0.71 fof(f138,definition,(
% 1.76/0.71 sQ19_spl <=> (product(e_2,e_2,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f139,plain,(
% 1.76/0.71 product(e_2,e_2,e_4)|~sQ19_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f138])).
% 1.76/0.71 fof(f141,plain,(
% 1.76/0.71 sQ16_spl|sQ17_spl|sQ18_spl|sQ19_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f114,f129,f132,f135,f138])).
% 1.76/0.71 fof(f142,definition,(
% 1.76/0.71 sQ20_spl <=> (product(e_2,e_1,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f143,plain,(
% 1.76/0.71 product(e_2,e_1,e_1)|~sQ20_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f142])).
% 1.76/0.71 fof(f145,definition,(
% 1.76/0.71 sQ21_spl <=> (product(e_2,e_1,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f146,plain,(
% 1.76/0.71 product(e_2,e_1,e_2)|~sQ21_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f145])).
% 1.76/0.71 fof(f148,definition,(
% 1.76/0.71 sQ22_spl <=> (product(e_2,e_1,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f149,plain,(
% 1.76/0.71 product(e_2,e_1,e_3)|~sQ22_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f148])).
% 1.76/0.71 fof(f151,definition,(
% 1.76/0.71 sQ23_spl <=> (product(e_2,e_1,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f152,plain,(
% 1.76/0.71 product(e_2,e_1,e_4)|~sQ23_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f151])).
% 1.76/0.71 fof(f154,plain,(
% 1.76/0.71 sQ20_spl|sQ21_spl|sQ22_spl|sQ23_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f115,f142,f145,f148,f151])).
% 1.76/0.71 fof(f155,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f70,f45])).
% 1.76/0.71 fof(f156,plain,(
% 1.76/0.71 product(e_1,e_2,e_1)|product(e_1,e_2,e_2)|product(e_1,e_2,e_3)|product(e_1,e_2,e_4)),
% 1.76/0.71 inference(resolution,[status(thm)],[f70,f44])).
% 1.76/0.71 fof(f157,plain,(
% 1.76/0.71 product(e_1,e_1,e_1)|product(e_1,e_1,e_2)|product(e_1,e_1,e_3)|product(e_1,e_1,e_4)),
% 1.76/0.71 inference(resolution,[status(thm)],[f70,f43])).
% 1.76/0.71 fof(f158,definition,(
% 1.76/0.71 sQ24_spl <=> (product(e_1,e_3,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f159,plain,(
% 1.76/0.71 product(e_1,e_3,e_1)|~sQ24_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f158])).
% 1.76/0.71 fof(f161,definition,(
% 1.76/0.71 sQ25_spl <=> (product(e_1,e_3,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f162,plain,(
% 1.76/0.71 product(e_1,e_3,e_2)|~sQ25_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f161])).
% 1.76/0.71 fof(f164,definition,(
% 1.76/0.71 sQ26_spl <=> (product(e_1,e_3,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f165,plain,(
% 1.76/0.71 product(e_1,e_3,e_3)|~sQ26_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f164])).
% 1.76/0.71 fof(f167,definition,(
% 1.76/0.71 sQ27_spl <=> (product(e_1,e_3,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f168,plain,(
% 1.76/0.71 product(e_1,e_3,e_4)|~sQ27_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f167])).
% 1.76/0.71 fof(f170,plain,(
% 1.76/0.71 sQ24_spl|sQ25_spl|sQ26_spl|sQ27_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f155,f158,f161,f164,f167])).
% 1.76/0.71 fof(f171,definition,(
% 1.76/0.71 sQ28_spl <=> (product(e_1,e_2,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f172,plain,(
% 1.76/0.71 product(e_1,e_2,e_1)|~sQ28_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f171])).
% 1.76/0.71 fof(f174,definition,(
% 1.76/0.71 sQ29_spl <=> (product(e_1,e_2,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f175,plain,(
% 1.76/0.71 product(e_1,e_2,e_2)|~sQ29_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f174])).
% 1.76/0.71 fof(f177,definition,(
% 1.76/0.71 sQ30_spl <=> (product(e_1,e_2,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f178,plain,(
% 1.76/0.71 product(e_1,e_2,e_3)|~sQ30_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f177])).
% 1.76/0.71 fof(f180,definition,(
% 1.76/0.71 sQ31_spl <=> (product(e_1,e_2,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f181,plain,(
% 1.76/0.71 product(e_1,e_2,e_4)|~sQ31_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f180])).
% 1.76/0.71 fof(f183,plain,(
% 1.76/0.71 sQ28_spl|sQ29_spl|sQ30_spl|sQ31_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f156,f171,f174,f177,f180])).
% 1.76/0.71 fof(f184,definition,(
% 1.76/0.71 sQ32_spl <=> (product(e_1,e_1,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f185,plain,(
% 1.76/0.71 product(e_1,e_1,e_1)|~sQ32_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f184])).
% 1.76/0.71 fof(f187,definition,(
% 1.76/0.71 sQ33_spl <=> (product(e_1,e_1,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f188,plain,(
% 1.76/0.71 product(e_1,e_1,e_2)|~sQ33_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f187])).
% 1.76/0.71 fof(f190,definition,(
% 1.76/0.71 sQ34_spl <=> (product(e_1,e_1,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f191,plain,(
% 1.76/0.71 product(e_1,e_1,e_3)|~sQ34_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f190])).
% 1.76/0.71 fof(f193,definition,(
% 1.76/0.71 sQ35_spl <=> (product(e_1,e_1,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f194,plain,(
% 1.76/0.71 product(e_1,e_1,e_4)|~sQ35_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f193])).
% 1.76/0.71 fof(f196,plain,(
% 1.76/0.71 sQ32_spl|sQ33_spl|sQ34_spl|sQ35_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f157,f184,f187,f190,f193])).
% 1.76/0.71 fof(f197,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f46,f70])).
% 1.76/0.71 fof(f198,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f46,f69])).
% 1.76/0.71 fof(f199,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f46,f68])).
% 1.76/0.71 fof(f200,plain,(
% 1.76/0.71 ![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))),
% 1.76/0.71 inference(resolution,[status(thm)],[f46,f59])).
% 1.76/0.71 fof(f201,definition,(
% 1.76/0.71 sQ36_spl <=> (product(e_1,e_4,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f202,plain,(
% 1.76/0.71 product(e_1,e_4,e_1)|~sQ36_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f201])).
% 1.76/0.71 fof(f204,definition,(
% 1.76/0.71 sQ37_spl <=> (product(e_1,e_4,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f205,plain,(
% 1.76/0.71 product(e_1,e_4,e_2)|~sQ37_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f204])).
% 1.76/0.71 fof(f207,definition,(
% 1.76/0.71 sQ38_spl <=> (product(e_1,e_4,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f208,plain,(
% 1.76/0.71 product(e_1,e_4,e_3)|~sQ38_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f207])).
% 1.76/0.71 fof(f210,definition,(
% 1.76/0.71 sQ39_spl <=> (product(e_1,e_4,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f211,plain,(
% 1.76/0.71 product(e_1,e_4,e_4)|~sQ39_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f210])).
% 1.76/0.71 fof(f213,plain,(
% 1.76/0.71 sQ36_spl|sQ37_spl|sQ38_spl|sQ39_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f197,f201,f204,f207,f210])).
% 1.76/0.71 fof(f214,definition,(
% 1.76/0.71 sQ40_spl <=> (product(e_2,e_4,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f215,plain,(
% 1.76/0.71 product(e_2,e_4,e_1)|~sQ40_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f214])).
% 1.76/0.71 fof(f217,definition,(
% 1.76/0.71 sQ41_spl <=> (product(e_2,e_4,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f218,plain,(
% 1.76/0.71 product(e_2,e_4,e_2)|~sQ41_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f217])).
% 1.76/0.71 fof(f220,definition,(
% 1.76/0.71 sQ42_spl <=> (product(e_2,e_4,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f221,plain,(
% 1.76/0.71 product(e_2,e_4,e_3)|~sQ42_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f220])).
% 1.76/0.71 fof(f223,definition,(
% 1.76/0.71 sQ43_spl <=> (product(e_2,e_4,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f224,plain,(
% 1.76/0.71 product(e_2,e_4,e_4)|~sQ43_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f223])).
% 1.76/0.71 fof(f226,plain,(
% 1.76/0.71 sQ40_spl|sQ41_spl|sQ42_spl|sQ43_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f198,f214,f217,f220,f223])).
% 1.76/0.71 fof(f227,definition,(
% 1.76/0.71 sQ44_spl <=> (product(e_3,e_4,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f228,plain,(
% 1.76/0.71 product(e_3,e_4,e_1)|~sQ44_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f227])).
% 1.76/0.71 fof(f230,definition,(
% 1.76/0.71 sQ45_spl <=> (product(e_3,e_4,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f231,plain,(
% 1.76/0.71 product(e_3,e_4,e_2)|~sQ45_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f230])).
% 1.76/0.71 fof(f233,definition,(
% 1.76/0.71 sQ46_spl <=> (product(e_3,e_4,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f234,plain,(
% 1.76/0.71 product(e_3,e_4,e_3)|~sQ46_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f233])).
% 1.76/0.71 fof(f236,definition,(
% 1.76/0.71 sQ47_spl <=> (product(e_3,e_4,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f237,plain,(
% 1.76/0.71 product(e_3,e_4,e_4)|~sQ47_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f236])).
% 1.76/0.71 fof(f239,plain,(
% 1.76/0.71 sQ44_spl|sQ45_spl|sQ46_spl|sQ47_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f199,f227,f230,f233,f236])).
% 1.76/0.71 fof(f240,plain,(
% 1.76/0.71 product(e_4,e_4,e_1)|product(e_4,e_4,e_2)|product(e_4,e_4,e_3)|product(e_4,e_4,e_4)),
% 1.76/0.71 inference(resolution,[status(thm)],[f200,f46])).
% 1.76/0.71 fof(f241,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f200,f45])).
% 1.76/0.71 fof(f242,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f200,f44])).
% 1.76/0.71 fof(f243,plain,(
% 1.76/0.71 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)),
% 1.76/0.71 inference(resolution,[status(thm)],[f200,f43])).
% 1.76/0.71 fof(f244,definition,(
% 1.76/0.71 sQ48_spl <=> (product(e_4,e_4,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f245,plain,(
% 1.76/0.71 product(e_4,e_4,e_1)|~sQ48_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f244])).
% 1.76/0.71 fof(f247,definition,(
% 1.76/0.71 sQ49_spl <=> (product(e_4,e_4,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f248,plain,(
% 1.76/0.71 product(e_4,e_4,e_2)|~sQ49_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f247])).
% 1.76/0.71 fof(f250,definition,(
% 1.76/0.71 sQ50_spl <=> (product(e_4,e_4,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f251,plain,(
% 1.76/0.71 product(e_4,e_4,e_3)|~sQ50_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f250])).
% 1.76/0.71 fof(f253,definition,(
% 1.76/0.71 sQ51_spl <=> (product(e_4,e_4,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f254,plain,(
% 1.76/0.71 product(e_4,e_4,e_4)|~sQ51_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f253])).
% 1.76/0.71 fof(f256,plain,(
% 1.76/0.71 sQ48_spl|sQ49_spl|sQ50_spl|sQ51_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f240,f244,f247,f250,f253])).
% 1.76/0.71 fof(f257,definition,(
% 1.76/0.71 sQ52_spl <=> (product(e_4,e_3,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f258,plain,(
% 1.76/0.71 product(e_4,e_3,e_1)|~sQ52_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f257])).
% 1.76/0.71 fof(f260,definition,(
% 1.76/0.71 sQ53_spl <=> (product(e_4,e_3,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f261,plain,(
% 1.76/0.71 product(e_4,e_3,e_2)|~sQ53_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f260])).
% 1.76/0.71 fof(f263,definition,(
% 1.76/0.71 sQ54_spl <=> (product(e_4,e_3,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f264,plain,(
% 1.76/0.71 product(e_4,e_3,e_3)|~sQ54_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f263])).
% 1.76/0.71 fof(f266,definition,(
% 1.76/0.71 sQ55_spl <=> (product(e_4,e_3,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f267,plain,(
% 1.76/0.71 product(e_4,e_3,e_4)|~sQ55_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f266])).
% 1.76/0.71 fof(f269,plain,(
% 1.76/0.71 sQ52_spl|sQ53_spl|sQ54_spl|sQ55_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f241,f257,f260,f263,f266])).
% 1.76/0.71 fof(f270,definition,(
% 1.76/0.71 sQ56_spl <=> (product(e_4,e_2,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f271,plain,(
% 1.76/0.71 product(e_4,e_2,e_1)|~sQ56_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f270])).
% 1.76/0.71 fof(f273,definition,(
% 1.76/0.71 sQ57_spl <=> (product(e_4,e_2,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f274,plain,(
% 1.76/0.71 product(e_4,e_2,e_2)|~sQ57_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f273])).
% 1.76/0.71 fof(f276,definition,(
% 1.76/0.71 sQ58_spl <=> (product(e_4,e_2,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f277,plain,(
% 1.76/0.71 product(e_4,e_2,e_3)|~sQ58_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f276])).
% 1.76/0.71 fof(f279,definition,(
% 1.76/0.71 sQ59_spl <=> (product(e_4,e_2,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f280,plain,(
% 1.76/0.71 product(e_4,e_2,e_4)|~sQ59_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f279])).
% 1.76/0.71 fof(f282,plain,(
% 1.76/0.71 sQ56_spl|sQ57_spl|sQ58_spl|sQ59_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f242,f270,f273,f276,f279])).
% 1.76/0.71 fof(f283,definition,(
% 1.76/0.71 sQ60_spl <=> (product(e_4,e_1,e_1))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f284,plain,(
% 1.76/0.71 product(e_4,e_1,e_1)|~sQ60_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f283])).
% 1.76/0.71 fof(f286,definition,(
% 1.76/0.71 sQ61_spl <=> (product(e_4,e_1,e_2))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f287,plain,(
% 1.76/0.71 product(e_4,e_1,e_2)|~sQ61_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f286])).
% 1.76/0.71 fof(f289,definition,(
% 1.76/0.71 sQ62_spl <=> (product(e_4,e_1,e_3))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f290,plain,(
% 1.76/0.71 product(e_4,e_1,e_3)|~sQ62_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f289])).
% 1.76/0.71 fof(f291,plain,(
% 1.76/0.71 ~product(e_4,e_1,e_3)|sQ62_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f289])).
% 1.76/0.71 fof(f292,definition,(
% 1.76/0.71 sQ63_spl <=> (product(e_4,e_1,e_4))),
% 1.76/0.71 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 1.76/0.71 fof(f293,plain,(
% 1.76/0.71 product(e_4,e_1,e_4)|~sQ63_spl),
% 1.76/0.71 inference(component_clause,[status(thm)],[f292])).
% 1.76/0.71 fof(f295,plain,(
% 1.76/0.71 sQ60_spl|sQ61_spl|sQ62_spl|sQ63_spl),
% 1.76/0.71 inference(split_clause,[status(thm)],[f243,f283,f286,f289,f292])).
% 1.76/0.71 fof(f299,plain,(
% 1.76/0.71 ![X0]: (~product(e_3,e_1,X0)|equalish(X0,e_4)|~sQ11_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f110,f61])).
% 1.76/0.71 fof(f300,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_1)|product(e_1,X0,e_4)|~sQ11_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f110,f67])).
% 1.76/0.71 fof(f304,plain,(
% 1.76/0.71 equalish(e_3,e_4)|~sQ10_spl|~sQ11_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f107,f299])).
% 1.76/0.71 fof(f306,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_1,e_3)|equalish(X0,e_3)|~sQ10_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f107,f65])).
% 1.76/0.71 fof(f309,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_1)|product(e_1,X0,e_3)|~sQ10_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f107,f67])).
% 1.76/0.71 fof(f310,plain,(
% 1.76/0.71 $false|~sQ10_spl|~sQ11_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f304,f55])).
% 1.76/0.71 fof(f311,plain,(
% 1.76/0.71 ~sQ10_spl|~sQ11_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f310])).
% 1.76/0.71 fof(f313,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_1,e_2)|equalish(X0,e_3)|~sQ9_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f104,f65])).
% 1.76/0.71 fof(f314,plain,(
% 1.76/0.71 ![X0]: (~product(e_3,X0,e_2)|equalish(X0,e_1)|~sQ9_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f104,f63])).
% 1.76/0.71 fof(f315,plain,(
% 1.76/0.71 ![X0]: (~product(e_3,e_1,X0)|equalish(X0,e_2)|~sQ9_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f104,f61])).
% 1.76/0.71 fof(f316,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_1)|product(e_1,X0,e_2)|~sQ9_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f104,f67])).
% 1.76/0.71 fof(f320,plain,(
% 1.76/0.71 equalish(e_1,e_2)|~sQ8_spl|~sQ9_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f101,f315])).
% 1.76/0.71 fof(f322,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_1,e_1)|equalish(X0,e_3)|~sQ8_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f101,f65])).
% 1.76/0.71 fof(f323,plain,(
% 1.76/0.71 ![X0]: (~product(e_3,X0,e_1)|equalish(X0,e_1)|~sQ8_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f101,f63])).
% 1.76/0.71 fof(f325,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_1)|product(e_1,X0,e_1)|~sQ8_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f101,f67])).
% 1.76/0.71 fof(f326,plain,(
% 1.76/0.71 $false|~sQ8_spl|~sQ9_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f320,f47])).
% 1.76/0.71 fof(f327,plain,(
% 1.76/0.71 ~sQ8_spl|~sQ9_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f326])).
% 1.76/0.71 fof(f329,plain,(
% 1.76/0.71 ![X0]: (~product(e_3,X0,e_4)|equalish(X0,e_2)|~sQ7_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f97,f63])).
% 1.76/0.71 fof(f330,plain,(
% 1.76/0.71 ![X0]: (~product(e_3,e_2,X0)|equalish(X0,e_4)|~sQ7_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f97,f61])).
% 1.76/0.71 fof(f331,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_2)|product(e_2,X0,e_4)|~sQ7_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f97,f67])).
% 1.76/0.71 fof(f335,plain,(
% 1.76/0.71 equalish(e_3,e_4)|~sQ6_spl|~sQ7_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f94,f330])).
% 1.76/0.71 fof(f336,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_3)|equalish(X0,e_3)|~sQ6_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f94,f65])).
% 1.76/0.71 fof(f339,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_2)|product(e_2,X0,e_3)|~sQ6_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f94,f67])).
% 1.76/0.71 fof(f340,plain,(
% 1.76/0.71 $false|~sQ6_spl|~sQ7_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f335,f55])).
% 1.76/0.71 fof(f341,plain,(
% 1.76/0.71 ~sQ6_spl|~sQ7_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f340])).
% 1.76/0.71 fof(f342,plain,(
% 1.76/0.71 equalish(e_2,e_1)|~sQ5_spl|~sQ9_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f91,f314])).
% 1.76/0.71 fof(f343,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_2)|equalish(X0,e_3)|~sQ5_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f91,f65])).
% 1.76/0.71 fof(f344,plain,(
% 1.76/0.71 ![X0]: (~product(e_3,X0,e_2)|equalish(X0,e_2)|~sQ5_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f91,f63])).
% 1.76/0.71 fof(f346,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_2)|product(e_2,X0,e_2)|~sQ5_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f91,f67])).
% 1.76/0.71 fof(f347,plain,(
% 1.76/0.71 $false|~sQ5_spl|~sQ9_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f342,f50])).
% 1.76/0.71 fof(f348,plain,(
% 1.76/0.71 ~sQ5_spl|~sQ9_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f347])).
% 1.76/0.71 fof(f349,plain,(
% 1.76/0.71 equalish(e_2,e_1)|~sQ4_spl|~sQ8_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f88,f323])).
% 1.76/0.71 fof(f350,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_1)|equalish(X0,e_3)|~sQ4_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f88,f65])).
% 1.76/0.71 fof(f351,plain,(
% 1.76/0.71 ![X0]: (~product(e_3,X0,e_1)|equalish(X0,e_2)|~sQ4_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f88,f63])).
% 1.76/0.71 fof(f353,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_2)|product(e_2,X0,e_1)|~sQ4_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f88,f67])).
% 1.76/0.71 fof(f354,plain,(
% 1.76/0.71 $false|~sQ4_spl|~sQ8_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f349,f50])).
% 1.76/0.71 fof(f355,plain,(
% 1.76/0.71 ~sQ4_spl|~sQ8_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f354])).
% 1.76/0.71 fof(f356,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_4)|equalish(X0,e_3)|~sQ3_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f84,f65])).
% 1.76/0.71 fof(f357,plain,(
% 1.76/0.71 ![X0]: (~product(e_3,X0,e_4)|equalish(X0,e_3)|~sQ3_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f84,f63])).
% 1.76/0.71 fof(f359,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_3)|product(e_3,X0,e_4)|~sQ3_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f84,f67])).
% 1.76/0.71 fof(f361,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_1,e_4)|equalish(X0,e_2)|~sQ23_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f152,f65])).
% 1.76/0.71 fof(f362,plain,(
% 1.76/0.71 ![X0]: (~product(e_2,X0,e_4)|equalish(X0,e_1)|~sQ23_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f152,f63])).
% 1.76/0.71 fof(f364,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_1)|product(e_1,X0,e_4)|~sQ23_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f152,f67])).
% 1.76/0.71 fof(f366,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_1,e_3)|equalish(X0,e_2)|~sQ22_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f149,f65])).
% 1.76/0.71 fof(f367,plain,(
% 1.76/0.71 ![X0]: (~product(e_2,X0,e_3)|equalish(X0,e_1)|~sQ22_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f149,f63])).
% 1.76/0.71 fof(f369,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_1)|product(e_1,X0,e_3)|~sQ22_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f149,f67])).
% 1.76/0.71 fof(f371,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_1,e_2)|equalish(X0,e_2)|~sQ21_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f146,f65])).
% 1.76/0.71 fof(f372,plain,(
% 1.76/0.71 ![X0]: (~product(e_2,X0,e_2)|equalish(X0,e_1)|~sQ21_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f146,f63])).
% 1.76/0.71 fof(f373,plain,(
% 1.76/0.71 ![X0]: (~product(e_2,e_1,X0)|equalish(X0,e_2)|~sQ21_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f146,f61])).
% 1.76/0.71 fof(f374,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_1)|product(e_1,X0,e_2)|~sQ21_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f146,f67])).
% 1.76/0.71 fof(f376,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_1,e_1)|equalish(X0,e_2)|~sQ20_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f143,f65])).
% 1.76/0.71 fof(f377,plain,(
% 1.76/0.71 ![X0]: (~product(e_2,X0,e_1)|equalish(X0,e_1)|~sQ20_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f143,f63])).
% 1.76/0.71 fof(f379,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_1)|product(e_1,X0,e_1)|~sQ20_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f143,f67])).
% 1.76/0.71 fof(f380,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_4)|equalish(X0,e_2)|~sQ19_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f139,f65])).
% 1.76/0.71 fof(f381,plain,(
% 1.76/0.71 ![X0]: (~product(e_2,X0,e_4)|equalish(X0,e_2)|~sQ19_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f139,f63])).
% 1.76/0.71 fof(f383,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_2)|product(e_2,X0,e_4)|~sQ19_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f139,f67])).
% 1.76/0.71 fof(f384,plain,(
% 1.76/0.71 product(e_1,e_3,e_4)|~sQ23_spl|~sQ4_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f364,f88])).
% 1.76/0.71 fof(f385,plain,(
% 1.76/0.71 product(e_1,e_3,e_3)|~sQ22_spl|~sQ4_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f369,f88])).
% 1.76/0.71 fof(f387,plain,(
% 1.76/0.71 product(e_1,e_3,e_1)|~sQ20_spl|~sQ4_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f379,f88])).
% 1.76/0.71 fof(f391,plain,(
% 1.76/0.71 equalish(e_2,e_3)|~sQ10_spl|~sQ22_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f306,f149])).
% 1.76/0.71 fof(f392,plain,(
% 1.76/0.71 $false|~sQ10_spl|~sQ22_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f391,f51])).
% 1.76/0.71 fof(f393,plain,(
% 1.76/0.71 ~sQ10_spl|~sQ22_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f392])).
% 1.76/0.71 fof(f398,plain,(
% 1.76/0.71 equalish(e_2,e_1)|~sQ23_spl|~sQ19_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f362,f139])).
% 1.76/0.71 fof(f400,plain,(
% 1.76/0.71 $false|~sQ23_spl|~sQ19_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f398,f50])).
% 1.76/0.71 fof(f401,plain,(
% 1.76/0.71 ~sQ23_spl|~sQ19_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f400])).
% 1.76/0.71 fof(f404,plain,(
% 1.76/0.71 equalish(e_1,e_2)|~sQ21_spl|~sQ20_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f373,f143])).
% 1.76/0.71 fof(f406,plain,(
% 1.76/0.71 $false|~sQ21_spl|~sQ20_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f404,f47])).
% 1.76/0.71 fof(f407,plain,(
% 1.76/0.71 ~sQ21_spl|~sQ20_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f406])).
% 1.76/0.71 fof(f411,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_3)|equalish(X0,e_2)|~sQ18_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f136,f65])).
% 1.76/0.71 fof(f412,plain,(
% 1.76/0.71 ![X0]: (~product(e_2,X0,e_3)|equalish(X0,e_2)|~sQ18_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f136,f63])).
% 1.76/0.71 fof(f413,plain,(
% 1.76/0.71 ![X0]: (~product(e_2,e_2,X0)|equalish(X0,e_3)|~sQ18_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f136,f61])).
% 1.76/0.71 fof(f414,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_2)|product(e_2,X0,e_3)|~sQ18_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f136,f67])).
% 1.76/0.71 fof(f418,plain,(
% 1.76/0.71 equalish(e_2,e_3)|~sQ17_spl|~sQ18_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f133,f413])).
% 1.76/0.71 fof(f420,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_2)|equalish(X0,e_2)|~sQ17_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f133,f65])).
% 1.76/0.71 fof(f421,plain,(
% 1.76/0.71 ![X0]: (~product(e_2,X0,e_2)|equalish(X0,e_2)|~sQ17_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f133,f63])).
% 1.76/0.71 fof(f423,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_2)|product(e_2,X0,e_2)|~sQ17_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f133,f67])).
% 1.76/0.71 fof(f424,plain,(
% 1.76/0.71 $false|~sQ17_spl|~sQ18_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f418,f51])).
% 1.76/0.71 fof(f425,plain,(
% 1.76/0.71 ~sQ17_spl|~sQ18_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f424])).
% 1.76/0.71 fof(f426,plain,(
% 1.76/0.71 equalish(e_2,e_1)|~sQ16_spl|~sQ20_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f130,f377])).
% 1.76/0.71 fof(f427,plain,(
% 1.76/0.71 equalish(e_2,e_3)|~sQ16_spl|~sQ4_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f130,f350])).
% 1.76/0.71 fof(f429,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_1)|equalish(X0,e_2)|~sQ16_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f130,f65])).
% 1.76/0.71 fof(f430,plain,(
% 1.76/0.71 ![X0]: (~product(e_2,X0,e_1)|equalish(X0,e_2)|~sQ16_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f130,f63])).
% 1.76/0.71 fof(f433,plain,(
% 1.76/0.71 $false|~sQ16_spl|~sQ20_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f426,f50])).
% 1.76/0.71 fof(f434,plain,(
% 1.76/0.71 ~sQ16_spl|~sQ20_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f433])).
% 1.76/0.71 fof(f435,plain,(
% 1.76/0.71 $false|~sQ16_spl|~sQ4_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f427,f51])).
% 1.76/0.71 fof(f436,plain,(
% 1.76/0.71 ~sQ16_spl|~sQ4_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f435])).
% 1.76/0.71 fof(f437,plain,(
% 1.76/0.71 product(e_1,e_3,e_2)|~sQ21_spl|~sQ4_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f374,f88])).
% 1.76/0.71 fof(f438,plain,(
% 1.76/0.71 equalish(e_2,e_3)|~sQ15_spl|~sQ3_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f126,f356])).
% 1.76/0.71 fof(f439,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_4)|equalish(X0,e_2)|~sQ15_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f126,f65])).
% 1.76/0.71 fof(f442,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_3)|product(e_3,X0,e_4)|~sQ15_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f126,f67])).
% 1.76/0.71 fof(f443,plain,(
% 1.76/0.71 $false|~sQ15_spl|~sQ3_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f438,f51])).
% 1.76/0.71 fof(f444,plain,(
% 1.76/0.71 ~sQ15_spl|~sQ3_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f443])).
% 1.76/0.71 fof(f445,plain,(
% 1.76/0.71 equalish(e_3,e_2)|~sQ14_spl|~sQ18_spl),
% 1.76/0.71 inference(resolution,[status(thm)],[f123,f412])).
% 1.76/0.71 fof(f446,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_3,e_3)|equalish(X0,e_2)|~sQ14_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f123,f65])).
% 1.76/0.71 fof(f447,plain,(
% 1.76/0.71 ![X0]: (~product(e_2,X0,e_3)|equalish(X0,e_3)|~sQ14_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f123,f63])).
% 1.76/0.71 fof(f449,plain,(
% 1.76/0.71 ![X0]: (~product(X0,e_2,e_3)|product(e_3,X0,e_3)|~sQ14_spl)),
% 1.76/0.71 inference(resolution,[status(thm)],[f123,f67])).
% 1.76/0.71 fof(f450,plain,(
% 1.76/0.71 $false|~sQ14_spl|~sQ18_spl),
% 1.76/0.71 inference(forward_subsumption_resolution,[status(thm)],[f445,f54])).
% 1.76/0.71 fof(f451,plain,(
% 1.76/0.71 ~sQ14_spl|~sQ18_spl),
% 1.76/0.71 inference(contradiction_clause,[status(thm)],[f450])).
% 1.76/0.72 fof(f452,plain,(
% 1.76/0.72 equalish(e_3,e_2)|~sQ13_spl|~sQ17_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f120,f421])).
% 1.76/0.72 fof(f453,plain,(
% 1.76/0.72 equalish(e_3,e_1)|~sQ13_spl|~sQ21_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f120,f372])).
% 1.76/0.72 fof(f454,plain,(
% 1.76/0.72 product(e_2,e_2,e_1)|~sQ13_spl|~sQ4_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f120,f353])).
% 1.76/0.72 fof(f459,plain,(
% 1.76/0.72 $false|~sQ13_spl|~sQ17_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f452,f54])).
% 1.76/0.72 fof(f460,plain,(
% 1.76/0.72 ~sQ13_spl|~sQ17_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f459])).
% 1.76/0.72 fof(f461,plain,(
% 1.76/0.72 product(e_1,e_2,e_2)|~sQ12_spl|~sQ9_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f117,f316])).
% 1.76/0.72 fof(f462,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_1)|equalish(X0,e_2)|~sQ12_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f117,f65])).
% 1.76/0.72 fof(f465,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_2,e_3)|product(e_3,X0,e_1)|~sQ12_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f117,f67])).
% 1.76/0.72 fof(f467,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_4)|equalish(X0,e_1)|~sQ35_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f194,f65])).
% 1.76/0.72 fof(f468,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,X0,e_4)|equalish(X0,e_1)|~sQ35_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f194,f63])).
% 1.76/0.72 fof(f469,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,e_1,X0)|equalish(X0,e_4)|~sQ35_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f194,f61])).
% 1.76/0.72 fof(f470,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_1)|product(e_1,X0,e_4)|~sQ35_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f194,f67])).
% 1.76/0.72 fof(f473,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,X0,e_3)|equalish(X0,e_1)|~sQ34_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f191,f63])).
% 1.76/0.72 fof(f475,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_1)|product(e_1,X0,e_3)|~sQ34_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f191,f67])).
% 1.76/0.72 fof(f476,plain,(
% 1.76/0.72 equalish(e_3,e_2)|~sQ16_spl|~sQ12_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f430,f117])).
% 1.76/0.72 fof(f477,plain,(
% 1.76/0.72 $false|~sQ16_spl|~sQ12_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f476,f54])).
% 1.76/0.72 fof(f478,plain,(
% 1.76/0.72 ~sQ16_spl|~sQ12_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f477])).
% 1.76/0.72 fof(f484,plain,(
% 1.76/0.72 equalish(e_3,e_4)|~sQ35_spl|~sQ34_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f469,f191])).
% 1.76/0.72 fof(f486,plain,(
% 1.76/0.72 $false|~sQ35_spl|~sQ34_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f484,f55])).
% 1.76/0.72 fof(f487,plain,(
% 1.76/0.72 ~sQ35_spl|~sQ34_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f486])).
% 1.76/0.72 fof(f488,plain,(
% 1.76/0.72 equalish(e_1,e_2)|~sQ33_spl|~sQ21_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f188,f371])).
% 1.76/0.72 fof(f489,plain,(
% 1.76/0.72 equalish(e_1,e_3)|~sQ33_spl|~sQ9_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f188,f313])).
% 1.76/0.72 fof(f492,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,X0,e_2)|equalish(X0,e_1)|~sQ33_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f188,f63])).
% 1.76/0.72 fof(f494,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_1)|product(e_1,X0,e_2)|~sQ33_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f188,f67])).
% 1.76/0.72 fof(f495,plain,(
% 1.76/0.72 $false|~sQ33_spl|~sQ21_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f488,f47])).
% 1.76/0.72 fof(f496,plain,(
% 1.76/0.72 ~sQ33_spl|~sQ21_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f495])).
% 1.76/0.72 fof(f497,plain,(
% 1.76/0.72 equalish(e_3,e_1)|~sQ20_spl|~sQ12_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f377,f117])).
% 1.76/0.72 fof(f498,plain,(
% 1.76/0.72 $false|~sQ20_spl|~sQ12_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f497,f53])).
% 1.76/0.72 fof(f499,plain,(
% 1.76/0.72 ~sQ20_spl|~sQ12_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f498])).
% 1.76/0.72 fof(f501,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_1)|equalish(X0,e_1)|~sQ32_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f185,f65])).
% 1.76/0.72 fof(f502,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,X0,e_1)|equalish(X0,e_1)|~sQ32_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f185,f63])).
% 1.76/0.72 fof(f504,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_1)|product(e_1,X0,e_1)|~sQ32_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f185,f67])).
% 1.76/0.72 fof(f511,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,e_2,X0)|equalish(X0,e_4)|~sQ31_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f181,f61])).
% 1.76/0.72 fof(f512,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_2)|product(e_2,X0,e_4)|~sQ31_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f181,f67])).
% 1.76/0.72 fof(f516,plain,(
% 1.76/0.72 equalish(e_3,e_4)|~sQ30_spl|~sQ31_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f178,f511])).
% 1.76/0.72 fof(f517,plain,(
% 1.76/0.72 equalish(e_1,e_2)|~sQ30_spl|~sQ18_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f178,f411])).
% 1.76/0.72 fof(f518,plain,(
% 1.76/0.72 equalish(e_1,e_3)|~sQ30_spl|~sQ6_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f178,f336])).
% 1.76/0.72 fof(f519,plain,(
% 1.76/0.72 product(e_3,e_1,e_1)|~sQ30_spl|~sQ12_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f178,f465])).
% 1.76/0.72 fof(f523,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_2)|product(e_2,X0,e_3)|~sQ30_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f178,f67])).
% 1.76/0.72 fof(f524,plain,(
% 1.76/0.72 $false|~sQ30_spl|~sQ31_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f516,f55])).
% 1.76/0.72 fof(f525,plain,(
% 1.76/0.72 ~sQ30_spl|~sQ31_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f524])).
% 1.76/0.72 fof(f526,plain,(
% 1.76/0.72 product(e_2,e_1,e_3)|~sQ29_spl|~sQ18_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f175,f414])).
% 1.76/0.72 fof(f527,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_2,e_2)|equalish(X0,e_1)|~sQ29_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f175,f65])).
% 1.76/0.72 fof(f528,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,X0,e_2)|equalish(X0,e_2)|~sQ29_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f175,f63])).
% 1.76/0.72 fof(f529,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,e_2,X0)|equalish(X0,e_2)|~sQ29_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f175,f61])).
% 1.76/0.72 fof(f530,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_2)|product(e_2,X0,e_2)|~sQ29_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f175,f67])).
% 1.76/0.72 fof(f534,plain,(
% 1.76/0.72 equalish(e_1,e_2)|~sQ28_spl|~sQ29_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f172,f529])).
% 1.76/0.72 fof(f535,plain,(
% 1.76/0.72 equalish(e_2,e_1)|~sQ28_spl|~sQ32_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f172,f502])).
% 1.76/0.72 fof(f536,plain,(
% 1.76/0.72 product(e_1,e_1,e_3)|~sQ28_spl|~sQ22_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f172,f369])).
% 1.76/0.72 fof(f537,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_2,e_1)|equalish(X0,e_1)|~sQ28_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f172,f65])).
% 1.76/0.72 fof(f539,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,e_2,X0)|equalish(X0,e_1)|~sQ28_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f172,f61])).
% 1.76/0.72 fof(f540,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_2)|product(e_2,X0,e_1)|~sQ28_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f172,f67])).
% 1.76/0.72 fof(f541,plain,(
% 1.76/0.72 $false|~sQ28_spl|~sQ29_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f534,f47])).
% 1.76/0.72 fof(f542,plain,(
% 1.76/0.72 ~sQ28_spl|~sQ29_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f541])).
% 1.76/0.72 fof(f543,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_4)|equalish(X0,e_1)|~sQ27_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f168,f65])).
% 1.76/0.72 fof(f544,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,X0,e_4)|equalish(X0,e_3)|~sQ27_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f168,f63])).
% 1.76/0.72 fof(f545,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,e_3,X0)|equalish(X0,e_4)|~sQ27_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f168,f61])).
% 1.76/0.72 fof(f550,plain,(
% 1.76/0.72 equalish(e_3,e_4)|~sQ26_spl|~sQ27_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f165,f545])).
% 1.76/0.72 fof(f551,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_3)|equalish(X0,e_1)|~sQ26_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f165,f65])).
% 1.76/0.72 fof(f554,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_3)|product(e_3,X0,e_3)|~sQ26_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f165,f67])).
% 1.76/0.72 fof(f555,plain,(
% 1.76/0.72 $false|~sQ26_spl|~sQ27_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f550,f55])).
% 1.76/0.72 fof(f556,plain,(
% 1.76/0.72 ~sQ26_spl|~sQ27_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f555])).
% 1.76/0.72 fof(f557,plain,(
% 1.76/0.72 equalish(e_3,e_2)|~sQ25_spl|~sQ29_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f162,f528])).
% 1.76/0.72 fof(f558,plain,(
% 1.76/0.72 product(e_2,e_1,e_3)|~sQ25_spl|~sQ6_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f162,f339])).
% 1.76/0.72 fof(f559,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_2)|equalish(X0,e_1)|~sQ25_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f162,f65])).
% 1.76/0.72 fof(f562,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_3)|product(e_3,X0,e_2)|~sQ25_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f162,f67])).
% 1.76/0.72 fof(f563,plain,(
% 1.76/0.72 $false|~sQ25_spl|~sQ29_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f557,f54])).
% 1.76/0.72 fof(f564,plain,(
% 1.76/0.72 ~sQ25_spl|~sQ29_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f563])).
% 1.76/0.72 fof(f565,plain,(
% 1.76/0.72 sQ29_spl|~sQ12_spl|~sQ9_spl),
% 1.76/0.72 inference(split_clause,[status(thm)],[f461,f174,f116,f103])).
% 1.76/0.72 fof(f566,plain,(
% 1.76/0.72 $false|~sQ28_spl|~sQ32_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f535,f50])).
% 1.76/0.72 fof(f567,plain,(
% 1.76/0.72 ~sQ28_spl|~sQ32_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f566])).
% 1.76/0.72 fof(f568,plain,(
% 1.76/0.72 equalish(e_3,e_1)|~sQ24_spl|~sQ32_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f159,f502])).
% 1.76/0.72 fof(f569,plain,(
% 1.76/0.72 equalish(e_1,e_2)|~sQ24_spl|~sQ12_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f159,f462])).
% 1.76/0.72 fof(f570,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_1)|equalish(X0,e_1)|~sQ24_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f159,f65])).
% 1.76/0.72 fof(f573,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_3)|product(e_3,X0,e_1)|~sQ24_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f159,f67])).
% 1.76/0.72 fof(f574,plain,(
% 1.76/0.72 $false|~sQ24_spl|~sQ32_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f568,f53])).
% 1.76/0.72 fof(f575,plain,(
% 1.76/0.72 ~sQ24_spl|~sQ32_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f574])).
% 1.76/0.72 fof(f576,plain,(
% 1.76/0.72 $false|~sQ24_spl|~sQ12_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f569,f47])).
% 1.76/0.72 fof(f577,plain,(
% 1.76/0.72 ~sQ24_spl|~sQ12_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f576])).
% 1.76/0.72 fof(f579,plain,(
% 1.76/0.72 ![X0]: (~product(e_3,X0,e_4)|equalish(X0,e_4)|~sQ47_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f237,f63])).
% 1.76/0.72 fof(f580,plain,(
% 1.76/0.72 ![X0]: (~product(e_3,e_4,X0)|equalish(X0,e_4)|~sQ47_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f237,f61])).
% 1.76/0.72 fof(f581,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_4)|product(e_4,X0,e_4)|~sQ47_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f237,f67])).
% 1.76/0.72 fof(f582,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_3)|equalish(X0,e_3)|~sQ46_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f234,f65])).
% 1.76/0.72 fof(f583,plain,(
% 1.76/0.72 ![X0]: (~product(e_3,X0,e_3)|equalish(X0,e_4)|~sQ46_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f234,f63])).
% 1.76/0.72 fof(f585,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_4)|product(e_4,X0,e_3)|~sQ46_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f234,f67])).
% 1.76/0.72 fof(f586,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_2)|equalish(X0,e_3)|~sQ45_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f231,f65])).
% 1.76/0.72 fof(f587,plain,(
% 1.76/0.72 ![X0]: (~product(e_3,X0,e_2)|equalish(X0,e_4)|~sQ45_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f231,f63])).
% 1.76/0.72 fof(f589,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_4)|product(e_4,X0,e_2)|~sQ45_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f231,f67])).
% 1.76/0.72 fof(f590,plain,(
% 1.76/0.72 equalish(e_4,e_2)|~sQ5_spl|~sQ45_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f344,f231])).
% 1.76/0.72 fof(f591,plain,(
% 1.76/0.72 $false|~sQ5_spl|~sQ45_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f590,f57])).
% 1.76/0.72 fof(f592,plain,(
% 1.76/0.72 ~sQ5_spl|~sQ45_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f591])).
% 1.76/0.72 fof(f595,plain,(
% 1.76/0.72 equalish(e_3,e_4)|~sQ47_spl|~sQ46_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f580,f234])).
% 1.76/0.72 fof(f597,plain,(
% 1.76/0.72 $false|~sQ47_spl|~sQ46_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f595,f55])).
% 1.76/0.72 fof(f598,plain,(
% 1.76/0.72 ~sQ47_spl|~sQ46_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f597])).
% 1.76/0.72 fof(f599,plain,(
% 1.76/0.72 equalish(e_4,e_1)|~sQ44_spl|~sQ8_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f228,f323])).
% 1.76/0.72 fof(f600,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_1)|equalish(X0,e_3)|~sQ44_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f228,f65])).
% 1.76/0.72 fof(f601,plain,(
% 1.76/0.72 ![X0]: (~product(e_3,X0,e_1)|equalish(X0,e_4)|~sQ44_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f228,f63])).
% 1.76/0.72 fof(f603,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_4)|product(e_4,X0,e_1)|~sQ44_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f228,f67])).
% 1.76/0.72 fof(f604,plain,(
% 1.76/0.72 $false|~sQ44_spl|~sQ8_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f599,f56])).
% 1.76/0.72 fof(f605,plain,(
% 1.76/0.72 ~sQ44_spl|~sQ8_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f604])).
% 1.76/0.72 fof(f606,plain,(
% 1.76/0.72 $false|~sQ13_spl|~sQ21_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f453,f53])).
% 1.76/0.72 fof(f607,plain,(
% 1.76/0.72 ~sQ13_spl|~sQ21_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f606])).
% 1.76/0.72 fof(f608,plain,(
% 1.76/0.72 sQ16_spl|~sQ13_spl|~sQ4_spl),
% 1.76/0.72 inference(split_clause,[status(thm)],[f454,f129,f119,f87])).
% 1.76/0.72 fof(f609,plain,(
% 1.76/0.72 sQ22_spl|~sQ29_spl|~sQ18_spl),
% 1.76/0.72 inference(split_clause,[status(thm)],[f526,f148,f174,f135])).
% 1.76/0.72 fof(f610,plain,(
% 1.76/0.72 sQ24_spl|~sQ20_spl|~sQ4_spl),
% 1.76/0.72 inference(split_clause,[status(thm)],[f387,f158,f142,f87])).
% 1.76/0.72 fof(f611,plain,(
% 1.76/0.72 $false|~sQ33_spl|~sQ9_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f489,f48])).
% 1.76/0.72 fof(f612,plain,(
% 1.76/0.72 ~sQ33_spl|~sQ9_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f611])).
% 1.76/0.72 fof(f613,plain,(
% 1.76/0.72 $false|~sQ30_spl|~sQ6_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f518,f48])).
% 1.76/0.72 fof(f614,plain,(
% 1.76/0.72 ~sQ30_spl|~sQ6_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f613])).
% 1.76/0.72 fof(f615,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_4)|equalish(X0,e_2)|~sQ43_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f224,f65])).
% 1.76/0.72 fof(f616,plain,(
% 1.76/0.72 ![X0]: (~product(e_2,X0,e_4)|equalish(X0,e_4)|~sQ43_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f224,f63])).
% 1.76/0.72 fof(f618,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_2,e_4)|product(e_4,X0,e_4)|~sQ43_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f224,f67])).
% 1.76/0.72 fof(f619,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_3)|equalish(X0,e_2)|~sQ42_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f221,f65])).
% 1.76/0.72 fof(f622,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_2,e_4)|product(e_4,X0,e_3)|~sQ42_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f221,f67])).
% 1.76/0.72 fof(f624,plain,(
% 1.76/0.72 ![X0]: (~product(e_2,X0,e_2)|equalish(X0,e_4)|~sQ41_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f218,f63])).
% 1.76/0.72 fof(f625,plain,(
% 1.76/0.72 ![X0]: (~product(e_2,e_4,X0)|equalish(X0,e_2)|~sQ41_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f218,f61])).
% 1.76/0.72 fof(f626,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_2,e_4)|product(e_4,X0,e_2)|~sQ41_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f218,f67])).
% 1.76/0.72 fof(f627,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_1)|equalish(X0,e_2)|~sQ40_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f215,f65])).
% 1.76/0.72 fof(f628,plain,(
% 1.76/0.72 ![X0]: (~product(e_2,X0,e_1)|equalish(X0,e_4)|~sQ40_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f215,f63])).
% 1.76/0.72 fof(f630,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_2,e_4)|product(e_4,X0,e_1)|~sQ40_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f215,f67])).
% 1.76/0.72 fof(f634,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_4)|product(e_4,X0,e_4)|~sQ39_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f211,f67])).
% 1.76/0.72 fof(f635,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_3)|equalish(X0,e_1)|~sQ38_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f208,f65])).
% 1.76/0.72 fof(f638,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_4)|product(e_4,X0,e_3)|~sQ38_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f208,f67])).
% 1.76/0.72 fof(f639,plain,(
% 1.76/0.72 equalish(e_4,e_1)|~sQ22_spl|~sQ42_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f367,f221])).
% 1.76/0.72 fof(f640,plain,(
% 1.76/0.72 $false|~sQ22_spl|~sQ42_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f639,f56])).
% 1.76/0.72 fof(f641,plain,(
% 1.76/0.72 ~sQ22_spl|~sQ42_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f640])).
% 1.76/0.72 fof(f642,plain,(
% 1.76/0.72 equalish(e_4,e_2)|~sQ17_spl|~sQ41_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f421,f218])).
% 1.76/0.72 fof(f643,plain,(
% 1.76/0.72 $false|~sQ17_spl|~sQ41_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f642,f57])).
% 1.76/0.72 fof(f644,plain,(
% 1.76/0.72 ~sQ17_spl|~sQ41_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f643])).
% 1.76/0.72 fof(f645,plain,(
% 1.76/0.72 equalish(e_1,e_2)|~sQ43_spl|~sQ39_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f615,f211])).
% 1.76/0.72 fof(f647,plain,(
% 1.76/0.72 $false|~sQ43_spl|~sQ39_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f645,f47])).
% 1.76/0.72 fof(f648,plain,(
% 1.76/0.72 ~sQ43_spl|~sQ39_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f647])).
% 1.76/0.72 fof(f655,plain,(
% 1.76/0.72 equalish(e_4,e_1)|~sQ34_spl|~sQ38_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f473,f208])).
% 1.76/0.72 fof(f656,plain,(
% 1.76/0.72 $false|~sQ34_spl|~sQ38_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f655,f56])).
% 1.76/0.72 fof(f657,plain,(
% 1.76/0.72 ~sQ34_spl|~sQ38_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f656])).
% 1.76/0.72 fof(f658,plain,(
% 1.76/0.72 equalish(e_4,e_2)|~sQ16_spl|~sQ40_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f430,f215])).
% 1.76/0.72 fof(f659,plain,(
% 1.76/0.72 $false|~sQ16_spl|~sQ40_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f658,f57])).
% 1.76/0.72 fof(f660,plain,(
% 1.76/0.72 ~sQ16_spl|~sQ40_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f659])).
% 1.76/0.72 fof(f661,plain,(
% 1.76/0.72 $false|~sQ30_spl|~sQ18_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f517,f47])).
% 1.76/0.72 fof(f662,plain,(
% 1.76/0.72 ~sQ30_spl|~sQ18_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f661])).
% 1.76/0.72 fof(f664,plain,(
% 1.76/0.72 ![X0]: (~product(e_1,X0,e_2)|equalish(X0,e_4)|~sQ37_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f205,f63])).
% 1.76/0.72 fof(f666,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_4)|product(e_4,X0,e_2)|~sQ37_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f205,f67])).
% 1.76/0.72 fof(f667,plain,(
% 1.76/0.72 equalish(e_1,e_2)|~sQ36_spl|~sQ40_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f202,f627])).
% 1.76/0.72 fof(f671,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_1,e_4)|product(e_4,X0,e_1)|~sQ36_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f202,f67])).
% 1.76/0.72 fof(f672,plain,(
% 1.76/0.72 $false|~sQ36_spl|~sQ40_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f667,f47])).
% 1.76/0.72 fof(f673,plain,(
% 1.76/0.72 ~sQ36_spl|~sQ40_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f672])).
% 1.76/0.72 fof(f676,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,X0,e_4)|equalish(X0,e_1)|~sQ63_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f293,f63])).
% 1.76/0.72 fof(f677,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,e_1,X0)|equalish(X0,e_4)|~sQ63_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f293,f61])).
% 1.76/0.72 fof(f678,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_1)|product(e_1,X0,e_4)|~sQ63_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f293,f67])).
% 1.76/0.72 fof(f683,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_1)|product(e_1,X0,e_3)|~sQ62_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f290,f67])).
% 1.76/0.72 fof(f686,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,X0,e_2)|equalish(X0,e_1)|~sQ61_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f287,f63])).
% 1.76/0.72 fof(f687,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,e_1,X0)|equalish(X0,e_2)|~sQ61_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f287,f61])).
% 1.76/0.72 fof(f688,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_1)|product(e_1,X0,e_2)|~sQ61_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f287,f67])).
% 1.76/0.72 fof(f689,plain,(
% 1.76/0.72 product(e_2,e_4,e_3)|~sQ30_spl|~sQ61_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f523,f287])).
% 1.76/0.72 fof(f690,plain,(
% 1.76/0.72 sQ42_spl|~sQ30_spl|~sQ61_spl),
% 1.76/0.72 inference(split_clause,[status(thm)],[f689,f220,f177,f286])).
% 1.76/0.72 fof(f691,plain,(
% 1.76/0.72 product(e_4,e_4,e_2)|~sQ37_spl|~sQ63_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f666,f293])).
% 1.76/0.72 fof(f692,plain,(
% 1.76/0.72 product(e_3,e_4,e_2)|~sQ25_spl|~sQ62_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f562,f290])).
% 1.76/0.72 fof(f693,plain,(
% 1.76/0.72 sQ45_spl|~sQ25_spl|~sQ62_spl),
% 1.76/0.72 inference(split_clause,[status(thm)],[f692,f230,f161,f289])).
% 1.76/0.72 fof(f700,plain,(
% 1.76/0.72 equalish(e_4,e_2)|~sQ29_spl|~sQ37_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f528,f205])).
% 1.76/0.72 fof(f701,plain,(
% 1.76/0.72 $false|~sQ29_spl|~sQ37_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f700,f57])).
% 1.76/0.72 fof(f702,plain,(
% 1.76/0.72 ~sQ29_spl|~sQ37_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f701])).
% 1.76/0.72 fof(f703,plain,(
% 1.76/0.72 equalish(e_1,e_4)|~sQ60_spl|~sQ63_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f284,f677])).
% 1.76/0.72 fof(f704,plain,(
% 1.76/0.72 equalish(e_4,e_1)|~sQ60_spl|~sQ32_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f284,f501])).
% 1.76/0.72 fof(f706,plain,(
% 1.76/0.72 equalish(e_4,e_3)|~sQ60_spl|~sQ8_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f284,f322])).
% 1.76/0.72 fof(f709,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,X0,e_1)|equalish(X0,e_1)|~sQ60_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f284,f63])).
% 1.76/0.72 fof(f712,plain,(
% 1.76/0.72 $false|~sQ60_spl|~sQ63_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f703,f49])).
% 1.76/0.72 fof(f713,plain,(
% 1.76/0.72 ~sQ60_spl|~sQ63_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f712])).
% 1.76/0.72 fof(f714,plain,(
% 1.76/0.72 equalish(e_2,e_1)|~sQ59_spl|~sQ63_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f280,f676])).
% 1.76/0.72 fof(f715,plain,(
% 1.76/0.72 product(e_4,e_4,e_3)|~sQ59_spl|~sQ42_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f280,f622])).
% 1.76/0.72 fof(f716,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_2,e_4)|equalish(X0,e_4)|~sQ59_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f280,f65])).
% 1.76/0.72 fof(f717,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,X0,e_4)|equalish(X0,e_2)|~sQ59_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f280,f63])).
% 1.76/0.72 fof(f719,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_2)|product(e_2,X0,e_4)|~sQ59_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f280,f67])).
% 1.76/0.72 fof(f720,plain,(
% 1.76/0.72 $false|~sQ59_spl|~sQ63_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f714,f50])).
% 1.76/0.72 fof(f721,plain,(
% 1.76/0.72 ~sQ59_spl|~sQ63_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f720])).
% 1.76/0.72 fof(f722,plain,(
% 1.76/0.72 $false|~sQ60_spl|~sQ32_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f704,f56])).
% 1.76/0.72 fof(f723,plain,(
% 1.76/0.72 ~sQ60_spl|~sQ32_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f722])).
% 1.76/0.72 fof(f726,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,X0,e_3)|equalish(X0,e_2)|~sQ58_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f277,f63])).
% 1.76/0.72 fof(f727,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,e_2,X0)|equalish(X0,e_3)|~sQ58_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f277,f61])).
% 1.76/0.72 fof(f728,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_2)|product(e_2,X0,e_3)|~sQ58_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f277,f67])).
% 1.76/0.72 fof(f729,plain,(
% 1.76/0.72 equalish(e_4,e_2)|~sQ57_spl|~sQ17_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f274,f420])).
% 1.76/0.72 fof(f730,plain,(
% 1.76/0.72 equalish(e_4,e_3)|~sQ57_spl|~sQ5_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f274,f343])).
% 1.76/0.72 fof(f735,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_2)|product(e_2,X0,e_2)|~sQ57_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f274,f67])).
% 1.76/0.72 fof(f736,plain,(
% 1.76/0.72 $false|~sQ57_spl|~sQ17_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f729,f57])).
% 1.76/0.72 fof(f737,plain,(
% 1.76/0.72 ~sQ57_spl|~sQ17_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f736])).
% 1.76/0.72 fof(f738,plain,(
% 1.76/0.72 $false|~sQ57_spl|~sQ5_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f730,f58])).
% 1.76/0.72 fof(f739,plain,(
% 1.76/0.72 ~sQ57_spl|~sQ5_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f738])).
% 1.76/0.72 fof(f740,plain,(
% 1.76/0.72 sQ34_spl|~sQ28_spl|~sQ22_spl),
% 1.76/0.72 inference(split_clause,[status(thm)],[f536,f190,f171,f148])).
% 1.76/0.72 fof(f741,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_2,e_1)|equalish(X0,e_4)|~sQ56_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f271,f65])).
% 1.76/0.72 fof(f742,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,X0,e_1)|equalish(X0,e_2)|~sQ56_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f271,f63])).
% 1.76/0.72 fof(f744,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_2)|product(e_2,X0,e_1)|~sQ56_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f271,f67])).
% 1.76/0.72 fof(f745,plain,(
% 1.76/0.72 product(e_4,e_4,e_3)|~sQ55_spl|~sQ46_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f267,f585])).
% 1.76/0.72 fof(f746,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_4)|equalish(X0,e_4)|~sQ55_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f267,f65])).
% 1.76/0.72 fof(f747,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,X0,e_4)|equalish(X0,e_3)|~sQ55_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f267,f63])).
% 1.76/0.72 fof(f749,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_3)|product(e_3,X0,e_4)|~sQ55_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f267,f67])).
% 1.76/0.72 fof(f750,plain,(
% 1.76/0.72 product(e_1,e_4,e_3)|~sQ22_spl|~sQ56_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f369,f271])).
% 1.76/0.72 fof(f751,plain,(
% 1.76/0.72 product(e_4,e_4,e_2)|~sQ45_spl|~sQ55_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f589,f267])).
% 1.76/0.72 fof(f752,plain,(
% 1.76/0.72 product(e_3,e_4,e_3)|~sQ14_spl|~sQ58_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f449,f277])).
% 1.76/0.72 fof(f755,plain,(
% 1.76/0.72 equalish(e_1,e_3)|~sQ58_spl|~sQ56_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f727,f271])).
% 1.76/0.72 fof(f757,plain,(
% 1.76/0.72 $false|~sQ58_spl|~sQ56_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f755,f48])).
% 1.76/0.72 fof(f758,plain,(
% 1.76/0.72 ~sQ58_spl|~sQ56_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f757])).
% 1.76/0.72 fof(f759,plain,(
% 1.76/0.72 equalish(e_4,e_2)|~sQ16_spl|~sQ56_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f429,f271])).
% 1.76/0.72 fof(f760,plain,(
% 1.76/0.72 $false|~sQ16_spl|~sQ56_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f759,f57])).
% 1.76/0.72 fof(f761,plain,(
% 1.76/0.72 ~sQ16_spl|~sQ56_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f760])).
% 1.76/0.72 fof(f762,plain,(
% 1.76/0.72 sQ22_spl|~sQ25_spl|~sQ6_spl),
% 1.76/0.72 inference(split_clause,[status(thm)],[f558,f148,f161,f93])).
% 1.76/0.72 fof(f766,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,X0,e_3)|equalish(X0,e_3)|~sQ54_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f264,f63])).
% 1.76/0.72 fof(f768,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_3)|product(e_3,X0,e_3)|~sQ54_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f264,f67])).
% 1.76/0.72 fof(f769,plain,(
% 1.76/0.72 equalish(e_3,e_1)|~sQ53_spl|~sQ61_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f261,f686])).
% 1.76/0.72 fof(f770,plain,(
% 1.76/0.72 product(e_2,e_4,e_3)|~sQ53_spl|~sQ6_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f261,f339])).
% 1.76/0.72 fof(f771,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_2)|equalish(X0,e_4)|~sQ53_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f261,f65])).
% 1.76/0.72 fof(f772,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,X0,e_2)|equalish(X0,e_3)|~sQ53_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f261,f63])).
% 1.76/0.72 fof(f773,plain,(
% 1.76/0.72 ![X0]: (~product(e_4,e_3,X0)|equalish(X0,e_2)|~sQ53_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f261,f61])).
% 1.76/0.72 fof(f774,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_3)|product(e_3,X0,e_2)|~sQ53_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f261,f67])).
% 1.76/0.72 fof(f775,plain,(
% 1.76/0.72 $false|~sQ53_spl|~sQ61_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f769,f53])).
% 1.76/0.72 fof(f776,plain,(
% 1.76/0.72 ~sQ53_spl|~sQ61_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f775])).
% 1.76/0.72 fof(f777,plain,(
% 1.76/0.72 sQ42_spl|~sQ53_spl|~sQ6_spl),
% 1.76/0.72 inference(split_clause,[status(thm)],[f770,f220,f260,f93])).
% 1.76/0.72 fof(f778,plain,(
% 1.76/0.72 product(e_1,e_4,e_1)|~sQ52_spl|~sQ8_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f258,f325])).
% 1.76/0.72 fof(f779,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_3,e_1)|equalish(X0,e_4)|~sQ52_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f258,f65])).
% 1.76/0.72 fof(f782,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_3)|product(e_3,X0,e_1)|~sQ52_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f258,f67])).
% 1.76/0.72 fof(f783,plain,(
% 1.76/0.72 equalish(e_4,e_3)|~sQ51_spl|~sQ55_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f254,f747])).
% 1.76/0.72 fof(f784,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_4)|equalish(X0,e_4)|~sQ51_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f254,f65])).
% 1.76/0.72 fof(f788,plain,(
% 1.76/0.72 $false|~sQ51_spl|~sQ55_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f783,f58])).
% 1.76/0.72 fof(f789,plain,(
% 1.76/0.72 ~sQ51_spl|~sQ55_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f788])).
% 1.76/0.72 fof(f797,plain,(
% 1.76/0.72 product(e_1,e_1,e_2)|~sQ61_spl|~sQ52_spl|~sQ8_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f688,f778])).
% 1.76/0.72 fof(f798,plain,(
% 1.76/0.72 sQ33_spl|~sQ61_spl|~sQ52_spl|~sQ8_spl),
% 1.76/0.72 inference(split_clause,[status(thm)],[f797,f187,f286,f257,f100])).
% 1.76/0.72 fof(f805,plain,(
% 1.76/0.72 product(e_1,e_4,e_3)|~sQ10_spl|~sQ52_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f309,f258])).
% 1.76/0.72 fof(f809,plain,(
% 1.76/0.72 equalish(e_3,e_2)|~sQ58_spl|~sQ54_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f726,f264])).
% 1.76/0.72 fof(f810,plain,(
% 1.76/0.72 $false|~sQ58_spl|~sQ54_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f809,f54])).
% 1.76/0.72 fof(f811,plain,(
% 1.76/0.72 ~sQ58_spl|~sQ54_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f810])).
% 1.76/0.72 fof(f812,plain,(
% 1.76/0.72 equalish(e_4,e_1)|~sQ24_spl|~sQ52_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f570,f258])).
% 1.76/0.72 fof(f813,plain,(
% 1.76/0.72 $false|~sQ24_spl|~sQ52_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f812,f56])).
% 1.76/0.72 fof(f814,plain,(
% 1.76/0.72 ~sQ24_spl|~sQ52_spl),
% 1.76/0.72 inference(contradiction_clause,[status(thm)],[f813])).
% 1.76/0.72 fof(f818,plain,(
% 1.76/0.72 equalish(e_4,e_3)|~sQ50_spl|~sQ54_spl),
% 1.76/0.72 inference(resolution,[status(thm)],[f251,f766])).
% 1.76/0.72 fof(f823,plain,(
% 1.76/0.72 ![X0]: (~product(X0,e_4,e_4)|product(e_4,X0,e_3)|~sQ50_spl)),
% 1.76/0.72 inference(resolution,[status(thm)],[f251,f67])).
% 1.76/0.72 fof(f824,plain,(
% 1.76/0.72 $false|~sQ50_spl|~sQ54_spl),
% 1.76/0.72 inference(forward_subsumption_resolution,[status(thm)],[f818,f58])).
% 1.76/0.73 fof(f825,plain,(
% 1.76/0.73 ~sQ50_spl|~sQ54_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f824])).
% 1.76/0.73 fof(f826,plain,(
% 1.76/0.73 product(e_2,e_4,e_1)|~sQ49_spl|~sQ56_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f248,f744])).
% 1.76/0.73 fof(f831,plain,(
% 1.76/0.73 sQ40_spl|~sQ49_spl|~sQ56_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f826,f214,f247,f270])).
% 1.76/0.73 fof(f832,plain,(
% 1.76/0.73 product(e_1,e_4,e_4)|~sQ48_spl|~sQ63_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f245,f678])).
% 1.76/0.73 fof(f834,plain,(
% 1.76/0.73 ![X0]: (~product(e_4,X0,e_1)|equalish(X0,e_4)|~sQ48_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f245,f63])).
% 1.76/0.73 fof(f836,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_4,e_4)|product(e_4,X0,e_1)|~sQ48_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f245,f67])).
% 1.76/0.73 fof(f838,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_4,e_2)|equalish(X0,e_4)|~sQ37_spl|~sQ63_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f691,f65])).
% 1.76/0.73 fof(f856,plain,(
% 1.76/0.73 equalish(e_3,e_1)|~sQ2_spl|~sQ26_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f81,f551])).
% 1.76/0.73 fof(f857,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_3,e_3)|equalish(X0,e_3)|~sQ2_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f81,f65])).
% 1.76/0.73 fof(f861,plain,(
% 1.76/0.73 $false|~sQ2_spl|~sQ26_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f856,f53])).
% 1.76/0.73 fof(f862,plain,(
% 1.76/0.73 ~sQ2_spl|~sQ26_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f861])).
% 1.76/0.73 fof(f863,plain,(
% 1.76/0.73 sQ26_spl|~sQ22_spl|~sQ4_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f385,f164,f148,f87])).
% 1.76/0.73 fof(f865,plain,(
% 1.76/0.73 equalish(e_4,e_1)|~sQ60_spl|~sQ48_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f709,f245])).
% 1.76/0.73 fof(f866,plain,(
% 1.76/0.73 $false|~sQ60_spl|~sQ48_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f865,f56])).
% 1.76/0.73 fof(f867,plain,(
% 1.76/0.73 ~sQ60_spl|~sQ48_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f866])).
% 1.76/0.73 fof(f868,plain,(
% 1.76/0.73 equalish(e_3,e_4)|~sQ1_spl|~sQ45_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f78,f587])).
% 1.76/0.73 fof(f869,plain,(
% 1.76/0.73 equalish(e_3,e_1)|~sQ1_spl|~sQ9_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f78,f314])).
% 1.76/0.73 fof(f870,plain,(
% 1.76/0.73 product(e_2,e_3,e_3)|~sQ1_spl|~sQ6_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f78,f339])).
% 1.76/0.73 fof(f871,plain,(
% 1.76/0.73 equalish(e_3,e_4)|~sQ1_spl|~sQ53_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f78,f771])).
% 1.76/0.73 fof(f875,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_3,e_3)|product(e_3,X0,e_2)|~sQ1_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f78,f67])).
% 1.76/0.73 fof(f876,plain,(
% 1.76/0.73 $false|~sQ1_spl|~sQ45_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f868,f55])).
% 1.76/0.73 fof(f877,plain,(
% 1.76/0.73 ~sQ1_spl|~sQ45_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f876])).
% 1.76/0.73 fof(f878,plain,(
% 1.76/0.73 equalish(e_3,e_1)|~sQ0_spl|~sQ24_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f75,f570])).
% 1.76/0.73 fof(f879,plain,(
% 1.76/0.73 product(e_1,e_3,e_2)|~sQ0_spl|~sQ9_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f75,f316])).
% 1.76/0.73 fof(f880,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_3,e_1)|equalish(X0,e_3)|~sQ0_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f75,f65])).
% 1.76/0.73 fof(f881,plain,(
% 1.76/0.73 ![X0]: (~product(e_3,X0,e_1)|equalish(X0,e_3)|~sQ0_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f75,f63])).
% 1.76/0.73 fof(f883,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_3,e_3)|product(e_3,X0,e_1)|~sQ0_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f75,f67])).
% 1.76/0.73 fof(f884,plain,(
% 1.76/0.73 $false|~sQ0_spl|~sQ24_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f878,f53])).
% 1.76/0.73 fof(f885,plain,(
% 1.76/0.73 ~sQ0_spl|~sQ24_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f884])).
% 1.76/0.73 fof(f888,plain,(
% 1.76/0.73 product(e_1,e_1,e_4)|~sQ52_spl|~sQ8_spl|~sQ63_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f778,f678])).
% 1.76/0.73 fof(f893,plain,(
% 1.76/0.73 sQ35_spl|~sQ52_spl|~sQ8_spl|~sQ63_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f888,f193,f257,f100,f292])).
% 1.76/0.73 fof(f901,plain,(
% 1.76/0.73 product(e_1,e_3,e_3)|~sQ10_spl|~sQ0_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f309,f75])).
% 1.76/0.73 fof(f902,plain,(
% 1.76/0.73 sQ26_spl|~sQ10_spl|~sQ0_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f901,f164,f106,f74])).
% 1.76/0.73 fof(f906,plain,(
% 1.76/0.73 product(e_2,e_1,e_2)|~sQ25_spl|~sQ5_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f162,f346])).
% 1.76/0.73 fof(f913,plain,(
% 1.76/0.73 equalish(e_1,e_3)|~sQ38_spl|~sQ46_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f208,f582])).
% 1.76/0.73 fof(f914,plain,(
% 1.76/0.73 equalish(e_1,e_2)|~sQ38_spl|~sQ42_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f208,f619])).
% 1.76/0.73 fof(f916,plain,(
% 1.76/0.73 product(e_3,e_1,e_3)|~sQ38_spl|~sQ54_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f208,f768])).
% 1.76/0.73 fof(f921,plain,(
% 1.76/0.73 $false|~sQ38_spl|~sQ46_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f913,f48])).
% 1.76/0.73 fof(f922,plain,(
% 1.76/0.73 ~sQ38_spl|~sQ46_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f921])).
% 1.76/0.73 fof(f923,plain,(
% 1.76/0.73 equalish(e_3,e_4)|~sQ37_spl|~sQ25_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f664,f162])).
% 1.76/0.73 fof(f924,plain,(
% 1.76/0.73 $false|~sQ37_spl|~sQ25_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f923,f55])).
% 1.76/0.73 fof(f925,plain,(
% 1.76/0.73 ~sQ37_spl|~sQ25_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f924])).
% 1.76/0.73 fof(f928,plain,(
% 1.76/0.73 equalish(e_2,e_4)|~sQ12_spl|~sQ52_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f117,f779])).
% 1.76/0.73 fof(f929,plain,(
% 1.76/0.73 product(e_1,e_2,e_4)|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f117,f300])).
% 1.76/0.73 fof(f935,plain,(
% 1.76/0.73 $false|~sQ12_spl|~sQ52_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f928,f52])).
% 1.76/0.73 fof(f936,plain,(
% 1.76/0.73 ~sQ12_spl|~sQ52_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f935])).
% 1.76/0.73 fof(f937,plain,(
% 1.76/0.73 sQ46_spl|~sQ14_spl|~sQ58_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f752,f233,f122,f276])).
% 1.76/0.73 fof(f940,plain,(
% 1.76/0.73 product(e_2,e_4,e_2)|~sQ61_spl|~sQ29_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f287,f530])).
% 1.76/0.73 fof(f949,plain,(
% 1.76/0.73 equalish(e_3,e_1)|~sQ5_spl|~sQ29_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f91,f527])).
% 1.76/0.73 fof(f955,plain,(
% 1.76/0.73 $false|~sQ5_spl|~sQ29_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f949,f53])).
% 1.76/0.73 fof(f956,plain,(
% 1.76/0.73 ~sQ5_spl|~sQ29_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f955])).
% 1.76/0.73 fof(f957,plain,(
% 1.76/0.73 sQ25_spl|~sQ0_spl|~sQ9_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f879,f161,f74,f103])).
% 1.76/0.73 fof(f958,plain,(
% 1.76/0.73 sQ38_spl|~sQ10_spl|~sQ52_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f805,f207,f106,f257])).
% 1.76/0.73 fof(f963,plain,(
% 1.76/0.73 product(e_4,e_1,e_1)|~sQ63_spl|~sQ48_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f832,f836])).
% 1.76/0.73 fof(f968,plain,(
% 1.76/0.73 sQ60_spl|~sQ63_spl|~sQ48_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f963,f283,f292,f244])).
% 1.76/0.73 fof(f969,plain,(
% 1.76/0.73 product(e_2,e_1,e_1)|~sQ21_spl|~sQ4_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f353,f437])).
% 1.76/0.73 fof(f970,plain,(
% 1.76/0.73 sQ20_spl|~sQ21_spl|~sQ4_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f969,f142,f145,f87])).
% 1.76/0.73 fof(f972,plain,(
% 1.76/0.73 equalish(e_4,e_3)|~sQ42_spl|~sQ14_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f221,f447])).
% 1.76/0.73 fof(f974,plain,(
% 1.76/0.73 product(e_3,e_2,e_2)|~sQ42_spl|~sQ53_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f221,f774])).
% 1.76/0.73 fof(f980,plain,(
% 1.76/0.73 $false|~sQ42_spl|~sQ14_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f972,f58])).
% 1.76/0.73 fof(f981,plain,(
% 1.76/0.73 ~sQ42_spl|~sQ14_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f980])).
% 1.76/0.73 fof(f982,plain,(
% 1.76/0.73 sQ5_spl|~sQ42_spl|~sQ53_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f974,f90,f220,f260])).
% 1.76/0.73 fof(f983,plain,(
% 1.76/0.73 sQ8_spl|~sQ30_spl|~sQ12_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f519,f100,f177,f116])).
% 1.76/0.73 fof(f984,plain,(
% 1.76/0.73 $false|~sQ1_spl|~sQ53_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f871,f55])).
% 1.76/0.73 fof(f985,plain,(
% 1.76/0.73 ~sQ1_spl|~sQ53_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f984])).
% 1.76/0.73 fof(f986,plain,(
% 1.76/0.73 $false|~sQ60_spl|~sQ8_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f706,f58])).
% 1.76/0.73 fof(f987,plain,(
% 1.76/0.73 ~sQ60_spl|~sQ8_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f986])).
% 1.76/0.73 fof(f989,plain,(
% 1.76/0.73 equalish(e_3,e_4)|~sQ13_spl|~sQ41_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f120,f624])).
% 1.76/0.73 fof(f991,plain,(
% 1.76/0.73 equalish(e_2,e_1)|~sQ13_spl|~sQ25_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f120,f559])).
% 1.76/0.73 fof(f993,plain,(
% 1.76/0.73 product(e_2,e_2,e_3)|~sQ13_spl|~sQ6_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f120,f339])).
% 1.76/0.73 fof(f994,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_3,e_2)|equalish(X0,e_2)|~sQ13_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f120,f65])).
% 1.76/0.73 fof(f997,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_2,e_3)|product(e_3,X0,e_2)|~sQ13_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f120,f67])).
% 1.76/0.73 fof(f998,plain,(
% 1.76/0.73 $false|~sQ13_spl|~sQ41_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f989,f55])).
% 1.76/0.73 fof(f999,plain,(
% 1.76/0.73 ~sQ13_spl|~sQ41_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f998])).
% 1.76/0.73 fof(f1002,plain,(
% 1.76/0.73 product(e_1,e_2,e_2)|~sQ16_spl|~sQ21_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f130,f374])).
% 1.76/0.73 fof(f1003,plain,(
% 1.76/0.73 equalish(e_2,e_1)|~sQ16_spl|~sQ28_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f130,f537])).
% 1.76/0.73 fof(f1009,plain,(
% 1.76/0.73 sQ29_spl|~sQ16_spl|~sQ21_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1002,f174,f129,f145])).
% 1.76/0.73 fof(f1010,plain,(
% 1.76/0.73 $false|~sQ16_spl|~sQ28_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1003,f50])).
% 1.76/0.73 fof(f1011,plain,(
% 1.76/0.73 ~sQ16_spl|~sQ28_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1010])).
% 1.76/0.73 fof(f1014,plain,(
% 1.76/0.73 equalish(e_4,e_2)|~sQ54_spl|~sQ14_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f264,f446])).
% 1.76/0.73 fof(f1015,plain,(
% 1.76/0.73 equalish(e_4,e_3)|~sQ54_spl|~sQ2_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f264,f857])).
% 1.76/0.73 fof(f1022,plain,(
% 1.76/0.73 $false|~sQ54_spl|~sQ14_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1014,f57])).
% 1.76/0.73 fof(f1023,plain,(
% 1.76/0.73 ~sQ54_spl|~sQ14_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1022])).
% 1.76/0.73 fof(f1026,plain,(
% 1.76/0.73 equalish(e_1,e_4)|~sQ28_spl|~sQ56_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f172,f741])).
% 1.76/0.73 fof(f1032,plain,(
% 1.76/0.73 $false|~sQ28_spl|~sQ56_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1026,f49])).
% 1.76/0.73 fof(f1033,plain,(
% 1.76/0.73 ~sQ28_spl|~sQ56_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1032])).
% 1.76/0.73 fof(f1034,plain,(
% 1.76/0.73 sQ41_spl|~sQ61_spl|~sQ29_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f940,f217,f286,f174])).
% 1.76/0.73 fof(f1035,plain,(
% 1.76/0.73 product(e_3,e_4,e_1)|~sQ0_spl|~sQ54_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f883,f264])).
% 1.76/0.73 fof(f1036,plain,(
% 1.76/0.73 sQ44_spl|~sQ0_spl|~sQ54_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1035,f227,f74,f263])).
% 1.76/0.73 fof(f1037,plain,(
% 1.76/0.73 sQ14_spl|~sQ1_spl|~sQ6_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f870,f122,f77,f93])).
% 1.76/0.73 fof(f1048,plain,(
% 1.76/0.73 equalish(e_1,e_3)|~sQ8_spl|~sQ0_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f101,f881])).
% 1.76/0.73 fof(f1051,plain,(
% 1.76/0.73 product(e_1,e_3,e_2)|~sQ8_spl|~sQ33_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f101,f494])).
% 1.76/0.73 fof(f1057,plain,(
% 1.76/0.73 $false|~sQ8_spl|~sQ0_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1048,f48])).
% 1.76/0.73 fof(f1058,plain,(
% 1.76/0.73 ~sQ8_spl|~sQ0_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1057])).
% 1.76/0.73 fof(f1059,plain,(
% 1.76/0.73 $false|~sQ1_spl|~sQ9_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f869,f53])).
% 1.76/0.73 fof(f1060,plain,(
% 1.76/0.73 ~sQ1_spl|~sQ9_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1059])).
% 1.76/0.73 fof(f1063,plain,(
% 1.76/0.73 equalish(e_2,e_3)|~sQ14_spl|~sQ2_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f123,f857])).
% 1.76/0.73 fof(f1070,plain,(
% 1.76/0.73 $false|~sQ14_spl|~sQ2_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1063,f51])).
% 1.76/0.73 fof(f1071,plain,(
% 1.76/0.73 ~sQ14_spl|~sQ2_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1070])).
% 1.76/0.73 fof(f1072,plain,(
% 1.76/0.73 $false|~sQ13_spl|~sQ25_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f991,f50])).
% 1.76/0.73 fof(f1073,plain,(
% 1.76/0.73 ~sQ13_spl|~sQ25_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1072])).
% 1.76/0.73 fof(f1074,plain,(
% 1.76/0.73 $false|~sQ54_spl|~sQ2_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1015,f58])).
% 1.76/0.73 fof(f1075,plain,(
% 1.76/0.73 ~sQ54_spl|~sQ2_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1074])).
% 1.76/0.73 fof(f1077,plain,(
% 1.76/0.73 equalish(e_3,e_4)|~sQ12_spl|~sQ40_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f117,f628])).
% 1.76/0.73 fof(f1079,plain,(
% 1.76/0.73 equalish(e_2,e_3)|~sQ12_spl|~sQ0_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f117,f880])).
% 1.76/0.73 fof(f1081,plain,(
% 1.76/0.73 product(e_1,e_2,e_3)|~sQ12_spl|~sQ10_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f117,f309])).
% 1.76/0.73 fof(f1085,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_2,e_3)|product(e_3,X0,e_1)|~sQ12_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f117,f67])).
% 1.76/0.73 fof(f1086,plain,(
% 1.76/0.73 $false|~sQ12_spl|~sQ40_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1077,f55])).
% 1.76/0.73 fof(f1087,plain,(
% 1.76/0.73 ~sQ12_spl|~sQ40_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1086])).
% 1.76/0.73 fof(f1090,plain,(
% 1.76/0.73 product(e_3,e_3,e_1)|~sQ10_spl|~sQ24_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f107,f573])).
% 1.76/0.73 fof(f1097,plain,(
% 1.76/0.73 sQ0_spl|~sQ10_spl|~sQ24_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1090,f74,f106,f158])).
% 1.76/0.73 fof(f1099,plain,(
% 1.76/0.73 equalish(e_1,e_2)|~sQ60_spl|~sQ56_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f284,f742])).
% 1.76/0.73 fof(f1101,plain,(
% 1.76/0.73 equalish(e_4,e_2)|~sQ60_spl|~sQ20_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f284,f376])).
% 1.76/0.73 fof(f1103,plain,(
% 1.76/0.73 product(e_1,e_4,e_4)|~sQ60_spl|~sQ35_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f284,f470])).
% 1.76/0.73 fof(f1109,plain,(
% 1.76/0.73 $false|~sQ60_spl|~sQ56_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1099,f47])).
% 1.76/0.73 fof(f1110,plain,(
% 1.76/0.73 ~sQ60_spl|~sQ56_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1109])).
% 1.76/0.73 fof(f1111,plain,(
% 1.76/0.73 $false|~sQ60_spl|~sQ20_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1101,f57])).
% 1.76/0.73 fof(f1112,plain,(
% 1.76/0.73 ~sQ60_spl|~sQ20_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1111])).
% 1.76/0.73 fof(f1113,plain,(
% 1.76/0.73 $false|~sQ38_spl|~sQ42_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f914,f47])).
% 1.76/0.73 fof(f1114,plain,(
% 1.76/0.73 ~sQ38_spl|~sQ42_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1113])).
% 1.76/0.73 fof(f1125,plain,(
% 1.76/0.73 product(e_1,e_3,e_2)|~sQ44_spl|~sQ61_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f228,f688])).
% 1.76/0.73 fof(f1131,plain,(
% 1.76/0.73 sQ25_spl|~sQ44_spl|~sQ61_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1125,f161,f227,f286])).
% 1.76/0.73 fof(f1132,plain,(
% 1.76/0.73 product(e_4,e_1,e_3)|~sQ38_spl|~sQ35_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f638,f194])).
% 1.76/0.73 fof(f1133,plain,(
% 1.76/0.73 product(e_3,e_4,e_3)|~sQ38_spl|~sQ35_spl|~sQ26_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1132,f554])).
% 1.76/0.73 fof(f1138,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_4,e_1)|product(e_1,X0,e_3)|~sQ38_spl|~sQ35_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f1132,f67])).
% 1.76/0.73 fof(f1139,plain,(
% 1.76/0.73 sQ46_spl|~sQ38_spl|~sQ35_spl|~sQ26_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1133,f233,f207,f193,f164])).
% 1.76/0.73 fof(f1141,plain,(
% 1.76/0.73 equalish(e_4,e_1)|~sQ49_spl|~sQ61_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f248,f686])).
% 1.76/0.73 fof(f1143,plain,(
% 1.76/0.73 product(e_2,e_4,e_3)|~sQ49_spl|~sQ58_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f248,f728])).
% 1.76/0.73 fof(f1149,plain,(
% 1.76/0.73 $false|~sQ49_spl|~sQ61_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1141,f56])).
% 1.76/0.73 fof(f1150,plain,(
% 1.76/0.73 ~sQ49_spl|~sQ61_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1149])).
% 1.76/0.73 fof(f1151,plain,(
% 1.76/0.73 sQ42_spl|~sQ49_spl|~sQ58_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1143,f220,f247,f276])).
% 1.76/0.73 fof(f1152,plain,(
% 1.76/0.73 $false|~sQ12_spl|~sQ0_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1079,f51])).
% 1.76/0.73 fof(f1153,plain,(
% 1.76/0.73 ~sQ12_spl|~sQ0_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1152])).
% 1.76/0.73 fof(f1154,plain,(
% 1.76/0.73 sQ25_spl|~sQ8_spl|~sQ33_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1051,f161,f100,f187])).
% 1.76/0.73 fof(f1157,plain,(
% 1.76/0.73 product(e_2,e_3,e_4)|~sQ5_spl|~sQ19_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f91,f383])).
% 1.76/0.73 fof(f1163,plain,(
% 1.76/0.73 sQ15_spl|~sQ5_spl|~sQ19_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1157,f125,f90,f138])).
% 1.76/0.73 fof(f1164,plain,(
% 1.76/0.73 product(e_2,e_3,e_3)|~sQ18_spl|~sQ5_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f414,f91])).
% 1.76/0.73 fof(f1165,plain,(
% 1.76/0.73 sQ14_spl|~sQ18_spl|~sQ5_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1164,f122,f135,f90])).
% 1.76/0.73 fof(f1166,plain,(
% 1.76/0.73 product(e_2,e_3,e_2)|~sQ17_spl|~sQ5_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f423,f91])).
% 1.76/0.73 fof(f1167,plain,(
% 1.76/0.73 sQ13_spl|~sQ17_spl|~sQ5_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1166,f119,f132,f90])).
% 1.76/0.73 fof(f1175,plain,(
% 1.76/0.73 product(e_3,e_4,e_1)|~sQ24_spl|~sQ38_spl|~sQ35_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f573,f1132])).
% 1.76/0.73 fof(f1196,plain,(
% 1.76/0.73 product(e_1,e_3,e_3)|~sQ24_spl|~sQ38_spl|~sQ35_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1138,f1175])).
% 1.76/0.73 fof(f1197,plain,(
% 1.76/0.73 sQ26_spl|~sQ24_spl|~sQ38_spl|~sQ35_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1196,f164,f158,f207,f193])).
% 1.76/0.73 fof(f1201,plain,(
% 1.76/0.73 product(e_4,e_2,e_1)|~sQ15_spl|~sQ44_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f126,f603])).
% 1.76/0.73 fof(f1208,plain,(
% 1.76/0.73 equalish(e_4,e_1)|~sQ63_spl|~sQ35_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f293,f467])).
% 1.76/0.73 fof(f1210,plain,(
% 1.76/0.73 product(e_4,e_4,e_4)|~sQ63_spl|~sQ39_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f293,f634])).
% 1.76/0.73 fof(f1216,plain,(
% 1.76/0.73 $false|~sQ63_spl|~sQ35_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1208,f56])).
% 1.76/0.73 fof(f1217,plain,(
% 1.76/0.73 ~sQ63_spl|~sQ35_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1216])).
% 1.76/0.73 fof(f1225,plain,(
% 1.76/0.73 equalish(e_4,e_1)|~sQ60_spl|~sQ35_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1103,f468])).
% 1.76/0.73 fof(f1231,plain,(
% 1.76/0.73 $false|~sQ60_spl|~sQ35_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1225,f56])).
% 1.76/0.73 fof(f1232,plain,(
% 1.76/0.73 ~sQ60_spl|~sQ35_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1231])).
% 1.76/0.73 fof(f1233,plain,(
% 1.76/0.73 sQ56_spl|~sQ15_spl|~sQ44_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1201,f270,f125,f227])).
% 1.76/0.73 fof(f1234,plain,(
% 1.76/0.73 $false|~sQ38_spl|~sQ35_spl|sQ62_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f291,f1132])).
% 1.76/0.73 fof(f1235,plain,(
% 1.76/0.73 ~sQ38_spl|~sQ35_spl|sQ62_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1234])).
% 1.76/0.73 fof(f1247,plain,(
% 1.76/0.73 equalish(e_3,e_2)|~sQ61_spl|~sQ38_spl|~sQ35_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f687,f1132])).
% 1.76/0.73 fof(f1248,plain,(
% 1.76/0.73 $false|~sQ61_spl|~sQ38_spl|~sQ35_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1247,f54])).
% 1.76/0.73 fof(f1249,plain,(
% 1.76/0.73 ~sQ61_spl|~sQ38_spl|~sQ35_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1248])).
% 1.76/0.73 fof(f1251,plain,(
% 1.76/0.73 equalish(e_3,e_4)|~sQ52_spl|~sQ48_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f258,f834])).
% 1.76/0.73 fof(f1259,plain,(
% 1.76/0.73 $false|~sQ52_spl|~sQ48_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1251,f55])).
% 1.76/0.73 fof(f1260,plain,(
% 1.76/0.73 ~sQ52_spl|~sQ48_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1259])).
% 1.76/0.73 fof(f1261,plain,(
% 1.76/0.73 sQ30_spl|~sQ12_spl|~sQ10_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1081,f177,f116,f106])).
% 1.76/0.73 fof(f1262,plain,(
% 1.76/0.73 sQ27_spl|~sQ23_spl|~sQ4_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f384,f167,f151,f87])).
% 1.76/0.73 fof(f1263,plain,(
% 1.76/0.73 sQ50_spl|~sQ59_spl|~sQ42_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f715,f250,f279,f220])).
% 1.76/0.73 fof(f1266,plain,(
% 1.76/0.73 product(e_2,e_4,e_4)|~sQ61_spl|~sQ31_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f287,f512])).
% 1.76/0.73 fof(f1274,plain,(
% 1.76/0.73 equalish(e_3,e_2)|~sQ1_spl|~sQ5_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f78,f344])).
% 1.76/0.73 fof(f1276,plain,(
% 1.76/0.73 equalish(e_3,e_2)|~sQ1_spl|~sQ13_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f78,f994])).
% 1.76/0.73 fof(f1283,plain,(
% 1.76/0.73 $false|~sQ1_spl|~sQ5_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1274,f54])).
% 1.76/0.73 fof(f1284,plain,(
% 1.76/0.73 ~sQ1_spl|~sQ5_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1283])).
% 1.76/0.73 fof(f1285,plain,(
% 1.76/0.73 sQ10_spl|~sQ38_spl|~sQ54_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f916,f106,f207,f263])).
% 1.76/0.73 fof(f1295,plain,(
% 1.76/0.73 product(e_3,e_1,e_4)|~sQ26_spl|~sQ3_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f165,f359])).
% 1.76/0.73 fof(f1313,plain,(
% 1.76/0.73 equalish(e_1,e_2)|~sQ14_spl|~sQ26_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f446,f165])).
% 1.76/0.73 fof(f1314,plain,(
% 1.76/0.73 $false|~sQ14_spl|~sQ26_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1313,f47])).
% 1.76/0.73 fof(f1315,plain,(
% 1.76/0.73 ~sQ14_spl|~sQ26_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1314])).
% 1.76/0.73 fof(f1316,plain,(
% 1.76/0.73 sQ51_spl|~sQ63_spl|~sQ39_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1210,f253,f292,f210])).
% 1.76/0.73 fof(f1317,plain,(
% 1.76/0.73 sQ18_spl|~sQ13_spl|~sQ6_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f993,f135,f119,f93])).
% 1.76/0.73 fof(f1342,plain,(
% 1.76/0.73 equalish(e_1,e_2)|~sQ29_spl|~sQ17_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f175,f420])).
% 1.76/0.73 fof(f1349,plain,(
% 1.76/0.73 $false|~sQ29_spl|~sQ17_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1342,f47])).
% 1.76/0.73 fof(f1350,plain,(
% 1.76/0.73 ~sQ29_spl|~sQ17_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1349])).
% 1.76/0.73 fof(f1352,plain,(
% 1.76/0.73 equalish(e_4,e_2)|~sQ26_spl|~sQ3_spl|~sQ9_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1295,f315])).
% 1.76/0.73 fof(f1359,plain,(
% 1.76/0.73 $false|~sQ26_spl|~sQ3_spl|~sQ9_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1352,f57])).
% 1.76/0.73 fof(f1360,plain,(
% 1.76/0.73 ~sQ26_spl|~sQ3_spl|~sQ9_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1359])).
% 1.76/0.73 fof(f1361,plain,(
% 1.76/0.73 equalish(e_4,e_2)|~sQ12_spl|~sQ11_spl|~sQ29_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f929,f529])).
% 1.76/0.73 fof(f1366,plain,(
% 1.76/0.73 $false|~sQ12_spl|~sQ11_spl|~sQ29_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1361,f57])).
% 1.76/0.73 fof(f1367,plain,(
% 1.76/0.73 ~sQ12_spl|~sQ11_spl|~sQ29_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1366])).
% 1.76/0.73 fof(f1370,plain,(
% 1.76/0.73 product(e_4,e_1,e_2)|~sQ41_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f626,f929])).
% 1.76/0.73 fof(f1371,plain,(
% 1.76/0.73 sQ61_spl|~sQ41_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1370,f286,f217,f116,f109])).
% 1.76/0.73 fof(f1373,plain,(
% 1.76/0.73 equalish(e_4,e_1)|~sQ28_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f539,f929])).
% 1.76/0.73 fof(f1374,plain,(
% 1.76/0.73 $false|~sQ28_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1373,f56])).
% 1.76/0.73 fof(f1375,plain,(
% 1.76/0.73 ~sQ28_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1374])).
% 1.76/0.73 fof(f1376,plain,(
% 1.76/0.73 equalish(e_4,e_2)|~sQ61_spl|~sQ31_spl|~sQ41_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1266,f625])).
% 1.76/0.73 fof(f1377,plain,(
% 1.76/0.73 product(e_4,e_2,e_1)|~sQ61_spl|~sQ31_spl|~sQ48_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1266,f836])).
% 1.76/0.73 fof(f1382,plain,(
% 1.76/0.73 $false|~sQ61_spl|~sQ31_spl|~sQ41_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1376,f57])).
% 1.76/0.73 fof(f1383,plain,(
% 1.76/0.73 ~sQ61_spl|~sQ31_spl|~sQ41_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1382])).
% 1.76/0.73 fof(f1384,plain,(
% 1.76/0.73 product(e_4,e_1,e_3)|~sQ42_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f622,f929])).
% 1.76/0.73 fof(f1395,plain,(
% 1.76/0.73 equalish(e_1,e_3)|~sQ54_spl|~sQ42_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f766,f1384])).
% 1.76/0.73 fof(f1396,plain,(
% 1.76/0.73 $false|~sQ54_spl|~sQ42_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1395,f48])).
% 1.76/0.73 fof(f1397,plain,(
% 1.76/0.73 ~sQ54_spl|~sQ42_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1396])).
% 1.76/0.73 fof(f1411,plain,(
% 1.76/0.73 equalish(e_2,e_3)|~sQ27_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f544,f929])).
% 1.76/0.73 fof(f1412,plain,(
% 1.76/0.73 $false|~sQ27_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1411,f51])).
% 1.76/0.73 fof(f1413,plain,(
% 1.76/0.73 ~sQ27_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1412])).
% 1.76/0.73 fof(f1414,plain,(
% 1.76/0.73 product(e_4,e_1,e_4)|~sQ43_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f618,f929])).
% 1.76/0.73 fof(f1415,plain,(
% 1.76/0.73 sQ63_spl|~sQ43_spl|~sQ12_spl|~sQ11_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1414,f292,f223,f116,f109])).
% 1.76/0.73 fof(f1425,plain,(
% 1.76/0.73 equalish(e_2,e_1)|~sQ18_spl|~sQ22_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f136,f367])).
% 1.76/0.73 fof(f1428,plain,(
% 1.76/0.73 product(e_3,e_2,e_1)|~sQ18_spl|~sQ12_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f136,f1085])).
% 1.76/0.73 fof(f1433,plain,(
% 1.76/0.73 $false|~sQ18_spl|~sQ22_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1425,f50])).
% 1.76/0.73 fof(f1434,plain,(
% 1.76/0.73 ~sQ18_spl|~sQ22_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1433])).
% 1.76/0.73 fof(f1437,plain,(
% 1.76/0.73 product(e_2,e_1,e_3)|~sQ33_spl|~sQ30_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f188,f523])).
% 1.76/0.73 fof(f1446,plain,(
% 1.76/0.73 product(e_4,e_3,e_4)|~sQ11_spl|~sQ39_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f110,f634])).
% 1.76/0.73 fof(f1453,plain,(
% 1.76/0.73 equalish(e_4,e_2)|~sQ11_spl|~sQ39_spl|~sQ53_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1446,f773])).
% 1.76/0.73 fof(f1454,plain,(
% 1.76/0.73 equalish(e_3,e_2)|~sQ11_spl|~sQ39_spl|~sQ59_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1446,f717])).
% 1.76/0.73 fof(f1455,plain,(
% 1.76/0.73 equalish(e_4,e_1)|~sQ11_spl|~sQ39_spl|~sQ27_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1446,f543])).
% 1.76/0.73 fof(f1459,plain,(
% 1.76/0.73 ![X0]: (~product(e_4,e_3,X0)|equalish(X0,e_4)|~sQ11_spl|~sQ39_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f1446,f61])).
% 1.76/0.73 fof(f1461,plain,(
% 1.76/0.73 $false|~sQ11_spl|~sQ39_spl|~sQ53_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1453,f57])).
% 1.76/0.73 fof(f1462,plain,(
% 1.76/0.73 ~sQ11_spl|~sQ39_spl|~sQ53_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1461])).
% 1.76/0.73 fof(f1463,plain,(
% 1.76/0.73 $false|~sQ11_spl|~sQ39_spl|~sQ59_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1454,f54])).
% 1.76/0.73 fof(f1464,plain,(
% 1.76/0.73 ~sQ11_spl|~sQ39_spl|~sQ59_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1463])).
% 1.76/0.73 fof(f1465,plain,(
% 1.76/0.73 product(e_2,e_1,e_2)|~sQ29_spl|~sQ33_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f530,f188])).
% 1.76/0.73 fof(f1466,plain,(
% 1.76/0.73 sQ21_spl|~sQ29_spl|~sQ33_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1465,f145,f174,f187])).
% 1.76/0.73 fof(f1474,plain,(
% 1.76/0.73 product(e_4,e_3,e_1)|~sQ36_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f671,f110])).
% 1.76/0.73 fof(f1475,plain,(
% 1.76/0.73 sQ52_spl|~sQ36_spl|~sQ11_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1474,f257,f201,f109])).
% 1.76/0.73 fof(f1482,plain,(
% 1.76/0.73 product(e_4,e_3,e_4)|~sQ39_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f634,f110])).
% 1.76/0.73 fof(f1483,plain,(
% 1.76/0.73 equalish(e_1,e_4)|~sQ47_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f579,f110])).
% 1.76/0.73 fof(f1484,plain,(
% 1.76/0.73 $false|~sQ47_spl|~sQ11_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1483,f49])).
% 1.76/0.73 fof(f1485,plain,(
% 1.76/0.73 ~sQ47_spl|~sQ11_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1484])).
% 1.76/0.73 fof(f1486,plain,(
% 1.76/0.73 product(e_3,e_4,e_4)|~sQ46_spl|~sQ55_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f745,f749])).
% 1.76/0.73 fof(f1491,plain,(
% 1.76/0.73 sQ47_spl|~sQ46_spl|~sQ55_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1486,f236,f233,f266])).
% 1.76/0.73 fof(f1502,plain,(
% 1.76/0.73 product(e_3,e_2,e_2)|~sQ14_spl|~sQ1_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f123,f875])).
% 1.76/0.73 fof(f1508,plain,(
% 1.76/0.73 sQ5_spl|~sQ14_spl|~sQ1_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1502,f90,f122,f77])).
% 1.76/0.73 fof(f1517,plain,(
% 1.76/0.73 product(e_2,e_2,e_4)|~sQ41_spl|~sQ59_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f218,f719])).
% 1.76/0.73 fof(f1523,plain,(
% 1.76/0.73 sQ19_spl|~sQ41_spl|~sQ59_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1517,f138,f217,f279])).
% 1.76/0.73 fof(f1524,plain,(
% 1.76/0.73 product(e_2,e_2,e_3)|~sQ58_spl|~sQ41_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f728,f218])).
% 1.76/0.73 fof(f1525,plain,(
% 1.76/0.73 equalish(e_2,e_3)|~sQ45_spl|~sQ41_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f586,f218])).
% 1.76/0.73 fof(f1526,plain,(
% 1.76/0.73 $false|~sQ45_spl|~sQ41_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1525,f51])).
% 1.76/0.73 fof(f1527,plain,(
% 1.76/0.73 ~sQ45_spl|~sQ41_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1526])).
% 1.76/0.73 fof(f1529,plain,(
% 1.76/0.73 equalish(e_4,e_1)|~sQ39_spl|~sQ35_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f211,f468])).
% 1.76/0.73 fof(f1531,plain,(
% 1.76/0.73 product(e_4,e_1,e_3)|~sQ39_spl|~sQ50_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f211,f823])).
% 1.76/0.73 fof(f1537,plain,(
% 1.76/0.73 $false|~sQ39_spl|~sQ35_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1529,f56])).
% 1.76/0.73 fof(f1538,plain,(
% 1.76/0.73 ~sQ39_spl|~sQ35_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1537])).
% 1.76/0.73 fof(f1539,plain,(
% 1.76/0.73 product(e_4,e_2,e_3)|~sQ61_spl|~sQ31_spl|~sQ50_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1266,f823])).
% 1.76/0.73 fof(f1544,plain,(
% 1.76/0.73 sQ58_spl|~sQ61_spl|~sQ31_spl|~sQ50_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1539,f276,f286,f180,f250])).
% 1.76/0.73 fof(f1547,plain,(
% 1.76/0.73 product(e_2,e_3,e_4)|~sQ45_spl|~sQ59_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f231,f719])).
% 1.76/0.73 fof(f1553,plain,(
% 1.76/0.73 sQ15_spl|~sQ45_spl|~sQ59_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1547,f125,f230,f279])).
% 1.76/0.73 fof(f1554,plain,(
% 1.76/0.73 sQ22_spl|~sQ33_spl|~sQ30_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1437,f148,f187,f177])).
% 1.76/0.73 fof(f1557,plain,(
% 1.76/0.73 equalish(e_3,e_1)|~sQ4_spl|~sQ28_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f88,f537])).
% 1.76/0.73 fof(f1559,plain,(
% 1.76/0.73 product(e_1,e_3,e_1)|~sQ4_spl|~sQ20_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f88,f379])).
% 1.76/0.73 fof(f1564,plain,(
% 1.76/0.73 $false|~sQ4_spl|~sQ28_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1557,f53])).
% 1.76/0.73 fof(f1565,plain,(
% 1.76/0.73 ~sQ4_spl|~sQ28_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1564])).
% 1.76/0.73 fof(f1567,plain,(
% 1.76/0.73 equalish(e_4,e_2)|~sQ51_spl|~sQ59_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f254,f717])).
% 1.76/0.73 fof(f1569,plain,(
% 1.76/0.73 equalish(e_4,e_2)|~sQ51_spl|~sQ43_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f254,f615])).
% 1.76/0.73 fof(f1576,plain,(
% 1.76/0.73 $false|~sQ51_spl|~sQ59_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1567,f57])).
% 1.76/0.73 fof(f1577,plain,(
% 1.76/0.73 ~sQ51_spl|~sQ59_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1576])).
% 1.76/0.73 fof(f1581,plain,(
% 1.76/0.73 product(e_3,e_1,e_1)|~sQ38_spl|~sQ52_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f208,f782])).
% 1.76/0.73 fof(f1586,plain,(
% 1.76/0.73 sQ8_spl|~sQ38_spl|~sQ52_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1581,f100,f207,f257])).
% 1.76/0.73 fof(f1587,plain,(
% 1.76/0.73 sQ55_spl|~sQ39_spl|~sQ11_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1482,f266,f210,f109])).
% 1.76/0.73 fof(f1589,plain,(
% 1.76/0.73 $false|~sQ11_spl|~sQ39_spl|~sQ27_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1455,f56])).
% 1.76/0.73 fof(f1590,plain,(
% 1.76/0.73 ~sQ11_spl|~sQ39_spl|~sQ27_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1589])).
% 1.76/0.73 fof(f1602,plain,(
% 1.76/0.73 equalish(e_1,e_4)|~sQ11_spl|~sQ39_spl|~sQ52_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1459,f258])).
% 1.76/0.73 fof(f1603,plain,(
% 1.76/0.73 $false|~sQ11_spl|~sQ39_spl|~sQ52_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1602,f49])).
% 1.76/0.73 fof(f1604,plain,(
% 1.76/0.73 ~sQ11_spl|~sQ39_spl|~sQ52_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1603])).
% 1.76/0.73 fof(f1605,plain,(
% 1.76/0.73 product(e_1,e_4,e_4)|~sQ11_spl|~sQ52_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f300,f258])).
% 1.76/0.73 fof(f1606,plain,(
% 1.76/0.73 sQ39_spl|~sQ11_spl|~sQ52_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1605,f210,f109,f257])).
% 1.76/0.73 fof(f1609,plain,(
% 1.76/0.73 product(e_2,e_2,e_1)|~sQ21_spl|~sQ28_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f146,f540])).
% 1.76/0.73 fof(f1616,plain,(
% 1.76/0.73 sQ16_spl|~sQ21_spl|~sQ28_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1609,f129,f145,f171])).
% 1.76/0.73 fof(f1618,plain,(
% 1.76/0.73 equalish(e_1,e_2)|~sQ11_spl|~sQ7_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f110,f329])).
% 1.76/0.73 fof(f1626,plain,(
% 1.76/0.73 $false|~sQ11_spl|~sQ7_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1618,f47])).
% 1.76/0.73 fof(f1627,plain,(
% 1.76/0.73 ~sQ11_spl|~sQ7_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1626])).
% 1.76/0.73 fof(f1628,plain,(
% 1.76/0.73 sQ43_spl|~sQ61_spl|~sQ31_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1266,f223,f286,f180])).
% 1.76/0.73 fof(f1636,plain,(
% 1.76/0.73 equalish(e_2,e_4)|~sQ61_spl|~sQ31_spl|~sQ48_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f834,f1377])).
% 1.76/0.73 fof(f1637,plain,(
% 1.76/0.73 $false|~sQ61_spl|~sQ31_spl|~sQ48_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1636,f52])).
% 1.76/0.73 fof(f1638,plain,(
% 1.76/0.73 ~sQ61_spl|~sQ31_spl|~sQ48_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1637])).
% 1.76/0.73 fof(f1641,plain,(
% 1.76/0.73 equalish(e_2,e_1)|~sQ15_spl|~sQ27_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f126,f543])).
% 1.76/0.73 fof(f1642,plain,(
% 1.76/0.73 product(e_4,e_2,e_3)|~sQ15_spl|~sQ46_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f126,f585])).
% 1.76/0.73 fof(f1648,plain,(
% 1.76/0.73 $false|~sQ15_spl|~sQ27_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1641,f50])).
% 1.76/0.73 fof(f1649,plain,(
% 1.76/0.73 ~sQ15_spl|~sQ27_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1648])).
% 1.76/0.73 fof(f1650,plain,(
% 1.76/0.73 sQ58_spl|~sQ15_spl|~sQ46_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1642,f276,f125,f233])).
% 1.76/0.73 fof(f1651,plain,(
% 1.76/0.73 product(e_4,e_2,e_4)|~sQ47_spl|~sQ15_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f581,f126])).
% 1.76/0.73 fof(f1652,plain,(
% 1.76/0.73 sQ59_spl|~sQ47_spl|~sQ15_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1651,f279,f236,f125])).
% 1.76/0.73 fof(f1653,plain,(
% 1.76/0.73 sQ49_spl|~sQ45_spl|~sQ55_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f751,f247,f230,f266])).
% 1.76/0.73 fof(f1654,plain,(
% 1.76/0.73 sQ11_spl|~sQ26_spl|~sQ3_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1295,f109,f164,f83])).
% 1.76/0.73 fof(f1670,plain,(
% 1.76/0.73 equalish(e_2,e_3)|~sQ57_spl|~sQ53_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f274,f772])).
% 1.76/0.73 fof(f1673,plain,(
% 1.76/0.73 product(e_2,e_4,e_3)|~sQ57_spl|~sQ18_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f274,f414])).
% 1.76/0.73 fof(f1678,plain,(
% 1.76/0.73 $false|~sQ57_spl|~sQ53_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1670,f51])).
% 1.76/0.73 fof(f1679,plain,(
% 1.76/0.73 ~sQ57_spl|~sQ53_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1678])).
% 1.76/0.73 fof(f1682,plain,(
% 1.76/0.73 equalish(e_2,e_3)|~sQ18_spl|~sQ6_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f136,f336])).
% 1.76/0.73 fof(f1684,plain,(
% 1.76/0.73 product(e_3,e_2,e_2)|~sQ18_spl|~sQ13_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f136,f997])).
% 1.76/0.73 fof(f1689,plain,(
% 1.76/0.73 $false|~sQ18_spl|~sQ6_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1682,f51])).
% 1.76/0.73 fof(f1690,plain,(
% 1.76/0.73 ~sQ18_spl|~sQ6_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1689])).
% 1.76/0.73 fof(f1693,plain,(
% 1.76/0.73 product(e_1,e_1,e_4)|~sQ24_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f159,f300])).
% 1.76/0.73 fof(f1699,plain,(
% 1.76/0.73 sQ35_spl|~sQ24_spl|~sQ11_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1693,f193,f158,f109])).
% 1.76/0.73 fof(f1709,plain,(
% 1.76/0.73 equalish(e_4,e_1)|~sQ40_spl|~sQ20_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f215,f377])).
% 1.76/0.73 fof(f1712,plain,(
% 1.76/0.73 product(e_1,e_2,e_3)|~sQ40_spl|~sQ62_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f215,f683])).
% 1.76/0.73 fof(f1713,plain,(
% 1.76/0.73 equalish(e_2,e_3)|~sQ40_spl|~sQ44_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f215,f600])).
% 1.76/0.73 fof(f1719,plain,(
% 1.76/0.73 $false|~sQ40_spl|~sQ20_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1709,f56])).
% 1.76/0.73 fof(f1720,plain,(
% 1.76/0.73 ~sQ40_spl|~sQ20_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1719])).
% 1.76/0.73 fof(f1723,plain,(
% 1.76/0.73 product(e_4,e_1,e_3)|~sQ31_spl|~sQ42_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f181,f622])).
% 1.76/0.73 fof(f1724,plain,(
% 1.76/0.73 equalish(e_1,e_2)|~sQ31_spl|~sQ19_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f181,f380])).
% 1.76/0.73 fof(f1726,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_2,e_4)|equalish(X0,e_1)|~sQ31_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f181,f65])).
% 1.76/0.73 fof(f1729,plain,(
% 1.76/0.73 ![X0]: (~product(X0,e_1,e_2)|product(e_2,X0,e_4)|~sQ31_spl)),
% 1.76/0.73 inference(resolution,[status(thm)],[f181,f67])).
% 1.76/0.73 fof(f1730,plain,(
% 1.76/0.73 $false|~sQ31_spl|~sQ19_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1724,f47])).
% 1.76/0.73 fof(f1731,plain,(
% 1.76/0.73 ~sQ31_spl|~sQ19_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1730])).
% 1.76/0.73 fof(f1750,plain,(
% 1.76/0.73 equalish(e_3,e_2)|~sQ15_spl|~sQ19_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f126,f381])).
% 1.76/0.73 fof(f1752,plain,(
% 1.76/0.73 product(e_4,e_2,e_3)|~sQ15_spl|~sQ46_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f126,f585])).
% 1.76/0.73 fof(f1758,plain,(
% 1.76/0.73 $false|~sQ15_spl|~sQ19_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1750,f54])).
% 1.76/0.73 fof(f1759,plain,(
% 1.76/0.73 ~sQ15_spl|~sQ19_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1758])).
% 1.76/0.73 fof(f1760,plain,(
% 1.76/0.73 product(e_4,e_3,e_3)|~sQ38_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f638,f110])).
% 1.76/0.73 fof(f1761,plain,(
% 1.76/0.73 sQ54_spl|~sQ38_spl|~sQ11_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1760,f263,f207,f109])).
% 1.76/0.73 fof(f1762,plain,(
% 1.76/0.73 product(e_4,e_3,e_2)|~sQ37_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f666,f110])).
% 1.76/0.73 fof(f1763,plain,(
% 1.76/0.73 equalish(e_3,e_2)|~sQ23_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f361,f110])).
% 1.76/0.73 fof(f1764,plain,(
% 1.76/0.73 $false|~sQ23_spl|~sQ11_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1763,f54])).
% 1.76/0.73 fof(f1765,plain,(
% 1.76/0.73 ~sQ23_spl|~sQ11_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1764])).
% 1.76/0.73 fof(f1788,plain,(
% 1.76/0.73 equalish(e_1,e_4)|~sQ27_spl|~sQ55_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f168,f746])).
% 1.76/0.73 fof(f1789,plain,(
% 1.76/0.73 product(e_4,e_1,e_1)|~sQ27_spl|~sQ44_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f168,f603])).
% 1.76/0.73 fof(f1795,plain,(
% 1.76/0.73 $false|~sQ27_spl|~sQ55_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1788,f49])).
% 1.76/0.73 fof(f1796,plain,(
% 1.76/0.73 ~sQ27_spl|~sQ55_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1795])).
% 1.76/0.73 fof(f1798,plain,(
% 1.76/0.73 equalish(e_1,e_4)|~sQ9_spl|~sQ45_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f104,f587])).
% 1.76/0.73 fof(f1800,plain,(
% 1.76/0.73 product(e_2,e_3,e_4)|~sQ9_spl|~sQ31_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f104,f1729])).
% 1.76/0.73 fof(f1807,plain,(
% 1.76/0.73 $false|~sQ9_spl|~sQ45_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1798,f49])).
% 1.76/0.73 fof(f1808,plain,(
% 1.76/0.73 ~sQ9_spl|~sQ45_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1807])).
% 1.76/0.73 fof(f1809,plain,(
% 1.76/0.73 $false|~sQ1_spl|~sQ13_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1276,f54])).
% 1.76/0.73 fof(f1810,plain,(
% 1.76/0.73 ~sQ1_spl|~sQ13_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1809])).
% 1.76/0.73 fof(f1821,plain,(
% 1.76/0.73 product(e_3,e_4,e_1)|~sQ24_spl|~sQ31_spl|~sQ42_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f573,f1723])).
% 1.76/0.73 fof(f1822,plain,(
% 1.76/0.73 sQ44_spl|~sQ24_spl|~sQ31_spl|~sQ42_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1821,f227,f158,f180,f220])).
% 1.76/0.73 fof(f1823,plain,(
% 1.76/0.73 sQ21_spl|~sQ25_spl|~sQ5_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f906,f145,f161,f90])).
% 1.76/0.73 fof(f1824,plain,(
% 1.76/0.73 $false|~sQ31_spl|~sQ42_spl|sQ62_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f291,f1723])).
% 1.76/0.73 fof(f1825,plain,(
% 1.76/0.73 ~sQ31_spl|~sQ42_spl|sQ62_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1824])).
% 1.76/0.73 fof(f1829,plain,(
% 1.76/0.73 product(e_1,e_3,e_3)|~sQ8_spl|~sQ34_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f101,f475])).
% 1.76/0.73 fof(f1835,plain,(
% 1.76/0.73 sQ26_spl|~sQ8_spl|~sQ34_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1829,f164,f100,f190])).
% 1.76/0.73 fof(f1845,plain,(
% 1.76/0.73 product(e_1,e_3,e_1)|~sQ32_spl|~sQ8_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f504,f101])).
% 1.76/0.73 fof(f1846,plain,(
% 1.76/0.73 sQ24_spl|~sQ32_spl|~sQ8_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1845,f158,f184,f100])).
% 1.76/0.73 fof(f1847,plain,(
% 1.76/0.73 product(e_1,e_1,e_2)|~sQ4_spl|~sQ20_spl|~sQ9_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1559,f316])).
% 1.76/0.73 fof(f1852,plain,(
% 1.76/0.73 sQ33_spl|~sQ4_spl|~sQ20_spl|~sQ9_spl),
% 1.76/0.73 inference(split_clause,[status(thm)],[f1847,f187,f87,f142,f103])).
% 1.76/0.73 fof(f1854,plain,(
% 1.76/0.73 equalish(e_3,e_4)|~sQ2_spl|~sQ46_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f81,f583])).
% 1.76/0.73 fof(f1862,plain,(
% 1.76/0.73 $false|~sQ2_spl|~sQ46_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1854,f55])).
% 1.76/0.73 fof(f1863,plain,(
% 1.76/0.73 ~sQ2_spl|~sQ46_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1862])).
% 1.76/0.73 fof(f1864,plain,(
% 1.76/0.73 product(e_1,e_1,e_4)|~sQ4_spl|~sQ20_spl|~sQ11_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f1559,f300])).
% 1.76/0.73 fof(f1873,plain,(
% 1.76/0.73 equalish(e_2,e_1)|~sQ31_spl|~sQ35_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f181,f468])).
% 1.76/0.73 fof(f1877,plain,(
% 1.76/0.73 product(e_4,e_1,e_4)|~sQ31_spl|~sQ43_spl),
% 1.76/0.73 inference(resolution,[status(thm)],[f181,f618])).
% 1.76/0.73 fof(f1882,plain,(
% 1.76/0.73 $false|~sQ31_spl|~sQ35_spl),
% 1.76/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1873,f50])).
% 1.76/0.73 fof(f1883,plain,(
% 1.76/0.73 ~sQ31_spl|~sQ35_spl),
% 1.76/0.73 inference(contradiction_clause,[status(thm)],[f1882])).
% 1.76/0.74 fof(f1884,plain,(
% 1.76/0.74 sQ5_spl|~sQ18_spl|~sQ13_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1684,f90,f135,f119])).
% 1.76/0.74 fof(f1886,plain,(
% 1.76/0.74 equalish(e_4,e_1)|~sQ37_spl|~sQ33_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f205,f492])).
% 1.76/0.74 fof(f1888,plain,(
% 1.76/0.74 product(e_2,e_1,e_2)|~sQ37_spl|~sQ57_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f205,f735])).
% 1.76/0.74 fof(f1889,plain,(
% 1.76/0.74 equalish(e_1,e_4)|~sQ37_spl|~sQ63_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f205,f838])).
% 1.76/0.74 fof(f1895,plain,(
% 1.76/0.74 $false|~sQ37_spl|~sQ33_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1886,f56])).
% 1.76/0.74 fof(f1896,plain,(
% 1.76/0.74 ~sQ37_spl|~sQ33_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f1895])).
% 1.76/0.74 fof(f1899,plain,(
% 1.76/0.74 equalish(e_2,e_1)|~sQ20_spl|~sQ32_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f143,f501])).
% 1.76/0.74 fof(f1907,plain,(
% 1.76/0.74 $false|~sQ20_spl|~sQ32_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1899,f50])).
% 1.76/0.74 fof(f1908,plain,(
% 1.76/0.74 ~sQ20_spl|~sQ32_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f1907])).
% 1.76/0.74 fof(f1909,plain,(
% 1.76/0.74 sQ63_spl|~sQ31_spl|~sQ43_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1877,f292,f180,f223])).
% 1.76/0.74 fof(f1920,plain,(
% 1.76/0.74 product(e_3,e_4,e_3)|~sQ26_spl|~sQ31_spl|~sQ42_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f554,f1723])).
% 1.76/0.74 fof(f1921,plain,(
% 1.76/0.74 sQ46_spl|~sQ26_spl|~sQ31_spl|~sQ42_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1920,f233,f164,f180,f220])).
% 1.76/0.74 fof(f1922,plain,(
% 1.76/0.74 sQ15_spl|~sQ9_spl|~sQ31_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1800,f125,f103,f180])).
% 1.76/0.74 fof(f1923,plain,(
% 1.76/0.74 sQ36_spl|~sQ52_spl|~sQ8_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f778,f201,f257,f100])).
% 1.76/0.74 fof(f1924,plain,(
% 1.76/0.74 sQ30_spl|~sQ40_spl|~sQ62_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1712,f177,f214,f289])).
% 1.76/0.74 fof(f1925,plain,(
% 1.76/0.74 sQ38_spl|~sQ22_spl|~sQ56_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f750,f207,f148,f270])).
% 1.76/0.74 fof(f1926,plain,(
% 1.76/0.74 $false|~sQ51_spl|~sQ43_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1569,f57])).
% 1.76/0.74 fof(f1927,plain,(
% 1.76/0.74 ~sQ51_spl|~sQ43_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f1926])).
% 1.76/0.74 fof(f1931,plain,(
% 1.76/0.74 equalish(e_1,e_3)|~sQ27_spl|~sQ3_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f168,f356])).
% 1.76/0.74 fof(f1932,plain,(
% 1.76/0.74 product(e_4,e_1,e_4)|~sQ27_spl|~sQ47_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f168,f581])).
% 1.76/0.74 fof(f1938,plain,(
% 1.76/0.74 $false|~sQ27_spl|~sQ3_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1931,f48])).
% 1.76/0.74 fof(f1939,plain,(
% 1.76/0.74 ~sQ27_spl|~sQ3_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f1938])).
% 1.76/0.74 fof(f1940,plain,(
% 1.76/0.74 sQ42_spl|~sQ57_spl|~sQ18_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1673,f220,f273,f135])).
% 1.76/0.74 fof(f1941,plain,(
% 1.76/0.74 sQ4_spl|~sQ18_spl|~sQ12_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1428,f87,f135,f116])).
% 1.76/0.74 fof(f1942,plain,(
% 1.76/0.74 sQ18_spl|~sQ58_spl|~sQ41_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1524,f135,f276,f217])).
% 1.76/0.74 fof(f1945,plain,(
% 1.76/0.74 equalish(e_3,e_1)|~sQ1_spl|~sQ25_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f78,f559])).
% 1.76/0.74 fof(f1947,plain,(
% 1.76/0.74 product(e_2,e_3,e_4)|~sQ1_spl|~sQ7_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f78,f331])).
% 1.76/0.74 fof(f1952,plain,(
% 1.76/0.74 $false|~sQ1_spl|~sQ25_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1945,f53])).
% 1.76/0.74 fof(f1953,plain,(
% 1.76/0.74 ~sQ1_spl|~sQ25_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f1952])).
% 1.76/0.74 fof(f1957,plain,(
% 1.76/0.74 product(e_4,e_3,e_4)|~sQ7_spl|~sQ43_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f97,f618])).
% 1.76/0.74 fof(f1962,plain,(
% 1.76/0.74 equalish(e_3,e_4)|~sQ59_spl|~sQ7_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f716,f97])).
% 1.76/0.74 fof(f1963,plain,(
% 1.76/0.74 $false|~sQ59_spl|~sQ7_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1962,f55])).
% 1.76/0.74 fof(f1964,plain,(
% 1.76/0.74 ~sQ59_spl|~sQ7_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f1963])).
% 1.76/0.74 fof(f1974,plain,(
% 1.76/0.74 equalish(e_4,e_1)|~sQ43_spl|~sQ23_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f224,f362])).
% 1.76/0.74 fof(f1976,plain,(
% 1.76/0.74 product(e_4,e_2,e_3)|~sQ43_spl|~sQ50_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f224,f823])).
% 1.76/0.74 fof(f1982,plain,(
% 1.76/0.74 $false|~sQ43_spl|~sQ23_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1974,f56])).
% 1.76/0.74 fof(f1983,plain,(
% 1.76/0.74 ~sQ43_spl|~sQ23_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f1982])).
% 1.76/0.74 fof(f1984,plain,(
% 1.76/0.74 sQ63_spl|~sQ27_spl|~sQ47_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1932,f292,f167,f236])).
% 1.76/0.74 fof(f1985,plain,(
% 1.76/0.74 sQ15_spl|~sQ1_spl|~sQ7_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1947,f125,f77,f96])).
% 1.76/0.74 fof(f1986,plain,(
% 1.76/0.74 sQ60_spl|~sQ27_spl|~sQ44_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1789,f283,f167,f227])).
% 1.76/0.74 fof(f1989,plain,(
% 1.76/0.74 equalish(e_4,e_1)|~sQ50_spl|~sQ38_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f251,f635])).
% 1.76/0.74 fof(f1990,plain,(
% 1.76/0.74 product(e_3,e_4,e_2)|~sQ50_spl|~sQ53_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f251,f774])).
% 1.76/0.74 fof(f1996,plain,(
% 1.76/0.74 $false|~sQ50_spl|~sQ38_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1989,f56])).
% 1.76/0.74 fof(f1997,plain,(
% 1.76/0.74 ~sQ50_spl|~sQ38_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f1996])).
% 1.76/0.74 fof(f2000,plain,(
% 1.76/0.74 product(e_2,e_2,e_2)|~sQ41_spl|~sQ57_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f218,f735])).
% 1.76/0.74 fof(f2006,plain,(
% 1.76/0.74 sQ17_spl|~sQ41_spl|~sQ57_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2000,f132,f217,f273])).
% 1.76/0.74 fof(f2017,plain,(
% 1.76/0.74 equalish(e_3,e_2)|~sQ0_spl|~sQ4_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f75,f351])).
% 1.76/0.74 fof(f2025,plain,(
% 1.76/0.74 $false|~sQ0_spl|~sQ4_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2017,f54])).
% 1.76/0.74 fof(f2026,plain,(
% 1.76/0.74 ~sQ0_spl|~sQ4_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2025])).
% 1.76/0.74 fof(f2027,plain,(
% 1.76/0.74 $false|~sQ40_spl|~sQ44_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1713,f51])).
% 1.76/0.74 fof(f2028,plain,(
% 1.76/0.74 ~sQ40_spl|~sQ44_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2027])).
% 1.76/0.74 fof(f2029,plain,(
% 1.76/0.74 sQ55_spl|~sQ7_spl|~sQ43_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1957,f266,f96,f223])).
% 1.76/0.74 fof(f2030,plain,(
% 1.76/0.74 sQ45_spl|~sQ50_spl|~sQ53_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1990,f230,f250,f260])).
% 1.76/0.74 fof(f2031,plain,(
% 1.76/0.74 product(e_2,e_3,e_3)|~sQ30_spl|~sQ9_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f523,f104])).
% 1.76/0.74 fof(f2033,plain,(
% 1.76/0.74 equalish(e_3,e_1)|~sQ14_spl|~sQ22_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f123,f367])).
% 1.76/0.74 fof(f2035,plain,(
% 1.76/0.74 product(e_3,e_2,e_4)|~sQ14_spl|~sQ3_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f123,f359])).
% 1.76/0.74 fof(f2041,plain,(
% 1.76/0.74 $false|~sQ14_spl|~sQ22_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2033,f53])).
% 1.76/0.74 fof(f2042,plain,(
% 1.76/0.74 ~sQ14_spl|~sQ22_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2041])).
% 1.76/0.74 fof(f2045,plain,(
% 1.76/0.74 product(e_2,e_1,e_4)|~sQ25_spl|~sQ7_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f162,f331])).
% 1.76/0.74 fof(f2051,plain,(
% 1.76/0.74 sQ23_spl|~sQ25_spl|~sQ7_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2045,f151,f161,f96])).
% 1.76/0.74 fof(f2052,plain,(
% 1.76/0.74 sQ7_spl|~sQ14_spl|~sQ3_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2035,f96,f122,f83])).
% 1.76/0.74 fof(f2053,plain,(
% 1.76/0.74 sQ53_spl|~sQ37_spl|~sQ11_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1762,f260,f204,f109])).
% 1.76/0.74 fof(f2068,plain,(
% 1.76/0.74 product(e_4,e_1,e_2)|~sQ37_spl|~sQ4_spl|~sQ20_spl|~sQ11_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f666,f1864])).
% 1.76/0.74 fof(f2069,plain,(
% 1.76/0.74 sQ61_spl|~sQ37_spl|~sQ4_spl|~sQ20_spl|~sQ11_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2068,f286,f204,f87,f142,f109])).
% 1.76/0.74 fof(f2073,plain,(
% 1.76/0.74 product(e_2,e_4,e_4)|~sQ53_spl|~sQ7_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f261,f331])).
% 1.76/0.74 fof(f2078,plain,(
% 1.76/0.74 sQ43_spl|~sQ53_spl|~sQ7_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2073,f223,f260,f96])).
% 1.76/0.74 fof(f2079,plain,(
% 1.76/0.74 $false|~sQ37_spl|~sQ63_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1889,f49])).
% 1.76/0.74 fof(f2080,plain,(
% 1.76/0.74 ~sQ37_spl|~sQ63_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2079])).
% 1.76/0.74 fof(f2083,plain,(
% 1.76/0.74 product(e_2,e_3,e_2)|~sQ9_spl|~sQ29_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f104,f530])).
% 1.76/0.74 fof(f2090,plain,(
% 1.76/0.74 sQ13_spl|~sQ9_spl|~sQ29_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2083,f119,f103,f174])).
% 1.76/0.74 fof(f2093,plain,(
% 1.76/0.74 product(e_4,e_3,e_3)|~sQ7_spl|~sQ42_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f97,f622])).
% 1.76/0.74 fof(f2099,plain,(
% 1.76/0.74 sQ54_spl|~sQ7_spl|~sQ42_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2093,f263,f96,f220])).
% 1.76/0.74 fof(f2111,plain,(
% 1.76/0.74 equalish(e_3,e_1)|~sQ31_spl|~sQ7_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f1726,f97])).
% 1.76/0.74 fof(f2112,plain,(
% 1.76/0.74 $false|~sQ31_spl|~sQ7_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2111,f53])).
% 1.76/0.74 fof(f2113,plain,(
% 1.76/0.74 ~sQ31_spl|~sQ7_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2112])).
% 1.76/0.74 fof(f2114,plain,(
% 1.76/0.74 sQ14_spl|~sQ30_spl|~sQ9_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2031,f122,f177,f103])).
% 1.76/0.74 fof(f2116,plain,(
% 1.76/0.74 product(e_4,e_3,e_1)|~sQ40_spl|~sQ7_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f630,f97])).
% 1.76/0.74 fof(f2117,plain,(
% 1.76/0.74 equalish(e_3,e_2)|~sQ19_spl|~sQ7_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f380,f97])).
% 1.76/0.74 fof(f2118,plain,(
% 1.76/0.74 $false|~sQ19_spl|~sQ7_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2117,f54])).
% 1.76/0.74 fof(f2119,plain,(
% 1.76/0.74 ~sQ19_spl|~sQ7_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2118])).
% 1.76/0.74 fof(f2133,plain,(
% 1.76/0.74 equalish(e_4,e_3)|~sQ10_spl|~sQ31_spl|~sQ42_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f306,f1723])).
% 1.76/0.74 fof(f2134,plain,(
% 1.76/0.74 $false|~sQ10_spl|~sQ31_spl|~sQ42_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2133,f58])).
% 1.76/0.74 fof(f2135,plain,(
% 1.76/0.74 ~sQ10_spl|~sQ31_spl|~sQ42_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2134])).
% 1.76/0.74 fof(f2138,plain,(
% 1.76/0.74 product(e_2,e_2,e_2)|~sQ13_spl|~sQ5_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f120,f346])).
% 1.76/0.74 fof(f2144,plain,(
% 1.76/0.74 sQ17_spl|~sQ13_spl|~sQ5_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2138,f132,f119,f90])).
% 1.76/0.74 fof(f2149,plain,(
% 1.76/0.74 product(e_3,e_4,e_1)|~sQ12_spl|~sQ43_spl|~sQ50_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f1085,f1976])).
% 1.76/0.74 fof(f2150,plain,(
% 1.76/0.74 sQ44_spl|~sQ12_spl|~sQ43_spl|~sQ50_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2149,f227,f116,f223,f250])).
% 1.76/0.74 fof(f2153,plain,(
% 1.76/0.74 product(e_1,e_3,e_4)|~sQ8_spl|~sQ35_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f101,f470])).
% 1.76/0.74 fof(f2160,plain,(
% 1.76/0.74 sQ27_spl|~sQ8_spl|~sQ35_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2153,f167,f100,f193])).
% 1.76/0.74 fof(f2163,plain,(
% 1.76/0.74 equalish(e_3,e_1)|~sQ55_spl|~sQ63_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f267,f676])).
% 1.76/0.74 fof(f2165,plain,(
% 1.76/0.74 equalish(e_4,e_2)|~sQ55_spl|~sQ15_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f267,f439])).
% 1.76/0.74 fof(f2172,plain,(
% 1.76/0.74 $false|~sQ55_spl|~sQ63_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2163,f53])).
% 1.76/0.74 fof(f2173,plain,(
% 1.76/0.74 ~sQ55_spl|~sQ63_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2172])).
% 1.76/0.74 fof(f2174,plain,(
% 1.76/0.74 $false|~sQ55_spl|~sQ15_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2165,f57])).
% 1.76/0.74 fof(f2175,plain,(
% 1.76/0.74 ~sQ55_spl|~sQ15_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2174])).
% 1.76/0.74 fof(f2176,plain,(
% 1.76/0.74 product(e_3,e_4,e_4)|~sQ46_spl|~sQ15_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f1752,f442])).
% 1.76/0.74 fof(f2181,plain,(
% 1.76/0.74 sQ47_spl|~sQ46_spl|~sQ15_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2176,f236,f233,f125])).
% 1.76/0.74 fof(f2203,plain,(
% 1.76/0.74 equalish(e_4,e_3)|~sQ6_spl|~sQ43_spl|~sQ50_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f336,f1976])).
% 1.76/0.74 fof(f2204,plain,(
% 1.76/0.74 $false|~sQ6_spl|~sQ43_spl|~sQ50_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2203,f58])).
% 1.76/0.74 fof(f2205,plain,(
% 1.76/0.74 ~sQ6_spl|~sQ43_spl|~sQ50_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2204])).
% 1.76/0.74 fof(f2206,plain,(
% 1.76/0.74 sQ62_spl|~sQ39_spl|~sQ50_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1531,f289,f210,f250])).
% 1.76/0.74 fof(f2210,plain,(
% 1.76/0.74 equalish(e_3,e_4)|~sQ43_spl|~sQ15_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f616,f126])).
% 1.76/0.74 fof(f2211,plain,(
% 1.76/0.74 $false|~sQ43_spl|~sQ15_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2210,f55])).
% 1.76/0.74 fof(f2212,plain,(
% 1.76/0.74 ~sQ43_spl|~sQ15_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2211])).
% 1.76/0.74 fof(f2215,plain,(
% 1.76/0.74 equalish(e_1,e_2)|~sQ34_spl|~sQ22_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f191,f366])).
% 1.76/0.74 fof(f2223,plain,(
% 1.76/0.74 $false|~sQ34_spl|~sQ22_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2215,f47])).
% 1.76/0.74 fof(f2224,plain,(
% 1.76/0.74 ~sQ34_spl|~sQ22_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2223])).
% 1.76/0.74 fof(f2225,plain,(
% 1.76/0.74 product(e_4,e_2,e_2)|~sQ45_spl|~sQ15_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f589,f126])).
% 1.76/0.74 fof(f2226,plain,(
% 1.76/0.74 sQ57_spl|~sQ45_spl|~sQ15_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2225,f273,f230,f125])).
% 1.76/0.74 fof(f2228,plain,(
% 1.76/0.74 equalish(e_3,e_1)|~sQ23_spl|~sQ15_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f362,f126])).
% 1.76/0.74 fof(f2229,plain,(
% 1.76/0.74 $false|~sQ23_spl|~sQ15_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2228,f53])).
% 1.76/0.74 fof(f2230,plain,(
% 1.76/0.74 ~sQ23_spl|~sQ15_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2229])).
% 1.76/0.74 fof(f2247,plain,(
% 1.76/0.74 equalish(e_1,e_4)|~sQ51_spl|~sQ39_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f784,f211])).
% 1.76/0.74 fof(f2248,plain,(
% 1.76/0.74 $false|~sQ51_spl|~sQ39_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2247,f49])).
% 1.76/0.74 fof(f2249,plain,(
% 1.76/0.74 ~sQ51_spl|~sQ39_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2248])).
% 1.76/0.74 fof(f2250,plain,(
% 1.76/0.74 sQ21_spl|~sQ37_spl|~sQ57_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f1888,f145,f204,f273])).
% 1.76/0.74 fof(f2253,plain,(
% 1.76/0.74 product(e_4,e_3,e_3)|~sQ7_spl|~sQ42_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f97,f622])).
% 1.76/0.74 fof(f2260,plain,(
% 1.76/0.74 equalish(e_3,e_4)|~sQ0_spl|~sQ44_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f75,f601])).
% 1.76/0.74 fof(f2268,plain,(
% 1.76/0.74 $false|~sQ0_spl|~sQ44_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2260,f55])).
% 1.76/0.74 fof(f2269,plain,(
% 1.76/0.74 ~sQ0_spl|~sQ44_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2268])).
% 1.76/0.74 fof(f2270,plain,(
% 1.76/0.74 sQ52_spl|~sQ40_spl|~sQ7_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2116,f257,f214,f96])).
% 1.76/0.74 fof(f2276,plain,(
% 1.76/0.74 product(e_3,e_4,e_2)|~sQ1_spl|~sQ7_spl|~sQ42_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f875,f2253])).
% 1.76/0.74 fof(f2277,plain,(
% 1.76/0.74 sQ45_spl|~sQ1_spl|~sQ7_spl|~sQ42_spl),
% 1.76/0.74 inference(split_clause,[status(thm)],[f2276,f230,f77,f96,f220])).
% 1.76/0.74 fof(f2279,plain,(
% 1.76/0.74 equalish(e_2,e_3)|~sQ3_spl|~sQ7_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f357,f97])).
% 1.76/0.74 fof(f2280,plain,(
% 1.76/0.74 $false|~sQ3_spl|~sQ7_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2279,f51])).
% 1.76/0.74 fof(f2281,plain,(
% 1.76/0.74 ~sQ3_spl|~sQ7_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2280])).
% 1.76/0.74 fof(f2284,plain,(
% 1.76/0.74 equalish(e_4,e_2)|~sQ62_spl|~sQ22_spl),
% 1.76/0.74 inference(resolution,[status(thm)],[f290,f366])).
% 1.76/0.74 fof(f2292,plain,(
% 1.76/0.74 $false|~sQ62_spl|~sQ22_spl),
% 1.76/0.74 inference(forward_subsumption_resolution,[status(thm)],[f2284,f57])).
% 1.76/0.74 fof(f2293,plain,(
% 1.76/0.74 ~sQ62_spl|~sQ22_spl),
% 1.76/0.74 inference(contradiction_clause,[status(thm)],[f2292])).
% 1.76/0.74 fof(f2294,plain,(
% 1.76/0.74 $false),
% 1.76/0.74 inference(sat_refutation,[status(thm)],[f86,f99,f112,f128,f141,f154,f170,f183,f196,f213,f226,f239,f256,f269,f282,f295,f311,f327,f341,f348,f355,f393,f401,f407,f425,f434,f436,f444,f451,f460,f478,f487,f496,f499,f525,f542,f556,f564,f565,f567,f575,f577,f592,f598,f605,f607,f608,f609,f610,f612,f614,f641,f644,f648,f657,f660,f662,f673,f690,f693,f702,f713,f721,f723,f737,f739,f740,f758,f761,f762,f776,f777,f789,f798,f811,f814,f825,f831,f862,f863,f867,f877,f885,f893,f902,f922,f925,f936,f937,f956,f957,f958,f968,f970,f981,f982,f983,f985,f987,f999,f1009,f1011,f1023,f1033,f1034,f1036,f1037,f1058,f1060,f1071,f1073,f1075,f1087,f1097,f1110,f1112,f1114,f1131,f1139,f1150,f1151,f1153,f1154,f1163,f1165,f1167,f1197,f1217,f1232,f1233,f1235,f1249,f1260,f1261,f1262,f1263,f1284,f1285,f1315,f1316,f1317,f1350,f1360,f1367,f1371,f1375,f1383,f1397,f1413,f1415,f1434,f1462,f1464,f1466,f1475,f1485,f1491,f1508,f1523,f1527,f1538,f1544,f1553,f1554,f1565,f1577,f1586,f1587,f1590,f1604,f1606,f1616,f1627,f1628,f1638,f1649,f1650,f1652,f1653,f1654,f1679,f1690,f1699,f1720,f1731,f1759,f1761,f1765,f1796,f1808,f1810,f1822,f1823,f1825,f1835,f1846,f1852,f1863,f1883,f1884,f1896,f1908,f1909,f1921,f1922,f1923,f1924,f1925,f1927,f1939,f1940,f1941,f1942,f1953,f1964,f1983,f1984,f1985,f1986,f1997,f2006,f2026,f2028,f2029,f2030,f2042,f2051,f2052,f2053,f2069,f2078,f2080,f2090,f2099,f2113,f2114,f2119,f2135,f2144,f2150,f2160,f2173,f2175,f2181,f2205,f2206,f2212,f2224,f2226,f2230,f2249,f2250,f2269,f2270,f2277,f2281,f2293])).
% 1.76/0.74 % SZS output end CNFRefutation for theBenchmark.p
% 1.76/0.74 % Elapsed time: 0.368549 seconds
% 1.76/0.74 % CPU time: 2.592290 seconds
% 1.76/0.74 % Total memory used: 24.144 MB
% 1.76/0.74 % Net memory used: 23.663 MB
%------------------------------------------------------------------------------