%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP124-7.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 : n015.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:47 PM UTC 2026
% Result : Unsatisfiable 0.08s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP124-7.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.08/0.36 % Computer : n015.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 20:02:35 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.08/0.42 % Refutation found
% 0.08/0.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.08/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.42 fof(f11,axiom,(
% 0.08/0.42 group_element(e_1) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f12,axiom,(
% 0.08/0.42 group_element(e_2) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f13,axiom,(
% 0.08/0.42 group_element(e_3) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f14,axiom,(
% 0.08/0.42 group_element(e_4) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f15,axiom,(
% 0.08/0.42 ~ equalish(e_1,e_2) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f16,axiom,(
% 0.08/0.42 ~ equalish(e_1,e_3) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f17,axiom,(
% 0.08/0.42 ~ equalish(e_1,e_4) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f18,axiom,(
% 0.08/0.42 ~ equalish(e_2,e_1) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f19,axiom,(
% 0.08/0.42 ~ equalish(e_2,e_3) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f20,axiom,(
% 0.08/0.42 ~ equalish(e_2,e_4) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f21,axiom,(
% 0.08/0.42 ~ equalish(e_3,e_1) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f22,axiom,(
% 0.08/0.42 ~ equalish(e_3,e_2) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f23,axiom,(
% 0.08/0.42 ~ equalish(e_3,e_4) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f24,axiom,(
% 0.08/0.42 ~ equalish(e_4,e_1) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f25,axiom,(
% 0.08/0.42 ~ equalish(e_4,e_2) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f26,axiom,(
% 0.08/0.42 ~ equalish(e_4,e_3) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f27,axiom,(
% 0.08/0.42 (![X,Y]: (( ~ group_element(X)| ~ group_element(Y)| product1(X,Y,e_1)| product1(X,Y,e_2)| product1(X,Y,e_3)| product1(X,Y,e_4) ) ))),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f28,axiom,(
% 0.08/0.42 (![X,Y,W,Z]: (( ~ product1(X,Y,W)| ~ product1(X,Y,Z)| equalish(W,Z) ) ))),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f29,axiom,(
% 0.08/0.42 (![X,W,Y,Z]: (( ~ product1(X,W,Y)| ~ product1(X,Z,Y)| equalish(W,Z) ) ))),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f30,axiom,(
% 0.08/0.42 (![W,Y,X,Z]: (( ~ product1(W,Y,X)| ~ product1(Z,Y,X)| equalish(W,Z) ) ))),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f31,axiom,(
% 0.08/0.42 (![X]: (product1(X,X,X) ))),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f33,axiom,(
% 0.08/0.42 (![X,Y,W,Z]: (( ~ product2(X,Y,W)| ~ product2(X,Y,Z)| equalish(W,Z) ) ))),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f36,axiom,(
% 0.08/0.42 (![X]: (product2(X,X,X) ))),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f37,negated_conjecture,(
% 0.08/0.42 (![X,Y,Z1,Z2]: (( ~ product1(X,Y,Z1)| ~ product1(Z1,X,Z2)| product2(Z2,Y,X) ) ))),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f49,plain,(
% 0.08/0.42 group_element(e_1)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f11])).
% 0.08/0.42 fof(f50,plain,(
% 0.08/0.42 group_element(e_2)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f12])).
% 0.08/0.42 fof(f51,plain,(
% 0.08/0.42 group_element(e_3)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f13])).
% 0.08/0.42 fof(f52,plain,(
% 0.08/0.42 group_element(e_4)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f14])).
% 0.08/0.42 fof(f53,plain,(
% 0.08/0.42 ~equalish(e_1,e_2)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f15])).
% 0.08/0.42 fof(f54,plain,(
% 0.08/0.42 ~equalish(e_1,e_3)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f16])).
% 0.08/0.42 fof(f55,plain,(
% 0.08/0.42 ~equalish(e_1,e_4)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f17])).
% 0.08/0.42 fof(f56,plain,(
% 0.08/0.42 ~equalish(e_2,e_1)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f18])).
% 0.08/0.42 fof(f57,plain,(
% 0.08/0.42 ~equalish(e_2,e_3)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f19])).
% 0.08/0.42 fof(f58,plain,(
% 0.08/0.42 ~equalish(e_2,e_4)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f20])).
% 0.08/0.42 fof(f59,plain,(
% 0.08/0.42 ~equalish(e_3,e_1)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f21])).
% 0.08/0.42 fof(f60,plain,(
% 0.08/0.42 ~equalish(e_3,e_2)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f22])).
% 0.08/0.42 fof(f61,plain,(
% 0.08/0.42 ~equalish(e_3,e_4)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f23])).
% 0.08/0.42 fof(f62,plain,(
% 0.08/0.42 ~equalish(e_4,e_1)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f24])).
% 0.08/0.42 fof(f63,plain,(
% 0.08/0.42 ~equalish(e_4,e_2)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f25])).
% 0.08/0.42 fof(f64,plain,(
% 0.08/0.42 ~equalish(e_4,e_3)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f26])).
% 0.08/0.42 fof(f65,plain,(
% 0.08/0.42 ![X0,X1]: (~group_element(X0)|~group_element(X1)|product1(X0,X1,e_1)|product1(X0,X1,e_2)|product1(X0,X1,e_3)|product1(X0,X1,e_4))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f27])).
% 0.08/0.42 fof(f66,plain,(
% 0.08/0.42 ![W,Z]: ((![X,Y]: (~product1(X,Y,W)|~product1(X,Y,Z)))|equalish(W,Z))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f28])).
% 0.08/0.42 fof(f67,plain,(
% 0.08/0.42 ![X0,X1,X2,X3]: (~product1(X0,X1,X2)|~product1(X0,X1,X3)|equalish(X2,X3))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f66])).
% 0.08/0.42 fof(f68,plain,(
% 0.08/0.42 ![W,Z]: ((![X,Y]: (~product1(X,W,Y)|~product1(X,Z,Y)))|equalish(W,Z))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f29])).
% 0.08/0.42 fof(f69,plain,(
% 0.08/0.42 ![X0,X1,X2,X3]: (~product1(X0,X1,X2)|~product1(X0,X3,X2)|equalish(X1,X3))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f68])).
% 0.08/0.42 fof(f70,plain,(
% 0.08/0.42 ![W,Z]: ((![Y,X]: (~product1(W,Y,X)|~product1(Z,Y,X)))|equalish(W,Z))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f30])).
% 0.08/0.42 fof(f71,plain,(
% 0.08/0.42 ![X0,X1,X2,X3]: (~product1(X0,X1,X2)|~product1(X3,X1,X2)|equalish(X0,X3))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f70])).
% 0.08/0.42 fof(f72,plain,(
% 0.08/0.42 ![X0]: (product1(X0,X0,X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f31])).
% 0.08/0.42 fof(f74,plain,(
% 0.08/0.42 ![W,Z]: ((![X,Y]: (~product2(X,Y,W)|~product2(X,Y,Z)))|equalish(W,Z))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f33])).
% 0.08/0.42 fof(f75,plain,(
% 0.08/0.42 ![X0,X1,X2,X3]: (~product2(X0,X1,X2)|~product2(X0,X1,X3)|equalish(X2,X3))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f74])).
% 0.08/0.42 fof(f80,plain,(
% 0.08/0.42 ![X0]: (product2(X0,X0,X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f36])).
% 0.08/0.42 fof(f81,plain,(
% 0.08/0.42 ![X,Y,Z2]: ((![Z1]: (~product1(X,Y,Z1)|~product1(Z1,X,Z2)))|product2(Z2,Y,X))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f37])).
% 0.08/0.42 fof(f82,plain,(
% 0.08/0.42 ![X0,X1,X2,X3]: (~product1(X0,X1,X2)|~product1(X2,X0,X3)|product2(X3,X1,X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f81])).
% 0.08/0.42 fof(f85,plain,(
% 0.08/0.42 ![X0,X1]: (~product1(X0,X0,X1)|equalish(X1,X0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f67,f72])).
% 0.08/0.42 fof(f87,plain,(
% 0.08/0.42 ![X0,X1]: (~product1(X0,X1,X0)|equalish(X1,X0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f69,f72])).
% 0.08/0.42 fof(f88,plain,(
% 0.08/0.42 ![X0,X1]: (~product1(X0,X1,X1)|equalish(X0,X1))),
% 0.08/0.42 inference(resolution,[status(thm)],[f71,f72])).
% 0.08/0.42 fof(f89,plain,(
% 0.08/0.42 ![X0]: (~group_element(X0)|product1(e_4,X0,e_1)|product1(e_4,X0,e_2)|product1(e_4,X0,e_3)|product1(e_4,X0,e_4))),
% 0.08/0.42 inference(resolution,[status(thm)],[f65,f52])).
% 0.08/0.42 fof(f90,plain,(
% 0.08/0.42 ![X0]: (~group_element(X0)|product1(e_3,X0,e_1)|product1(e_3,X0,e_2)|product1(e_3,X0,e_3)|product1(e_3,X0,e_4))),
% 0.08/0.42 inference(resolution,[status(thm)],[f65,f51])).
% 0.08/0.42 fof(f91,plain,(
% 0.08/0.42 ![X0]: (~group_element(X0)|product1(e_2,X0,e_1)|product1(e_2,X0,e_2)|product1(e_2,X0,e_3)|product1(e_2,X0,e_4))),
% 0.08/0.42 inference(resolution,[status(thm)],[f65,f50])).
% 0.08/0.42 fof(f92,plain,(
% 0.08/0.42 ![X0]: (~group_element(X0)|product1(e_1,X0,e_1)|product1(e_1,X0,e_2)|product1(e_1,X0,e_3)|product1(e_1,X0,e_4))),
% 0.08/0.42 inference(resolution,[status(thm)],[f65,f49])).
% 0.08/0.42 fof(f98,plain,(
% 0.08/0.42 product1(e_4,e_3,e_1)|product1(e_4,e_3,e_2)|product1(e_4,e_3,e_3)|product1(e_4,e_3,e_4)),
% 0.08/0.42 inference(resolution,[status(thm)],[f89,f51])).
% 0.08/0.42 fof(f100,plain,(
% 0.08/0.42 product1(e_4,e_1,e_1)|product1(e_4,e_1,e_2)|product1(e_4,e_1,e_3)|product1(e_4,e_1,e_4)),
% 0.08/0.42 inference(resolution,[status(thm)],[f89,f49])).
% 0.08/0.42 fof(f114,definition,(
% 0.08/0.42 sQ4_spl <=> (product1(e_4,e_3,e_1))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f115,plain,(
% 0.08/0.42 product1(e_4,e_3,e_1)|~sQ4_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f114])).
% 0.08/0.42 fof(f117,definition,(
% 0.08/0.42 sQ5_spl <=> (product1(e_4,e_3,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f118,plain,(
% 0.08/0.42 product1(e_4,e_3,e_2)|~sQ5_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f117])).
% 0.08/0.42 fof(f120,definition,(
% 0.08/0.42 sQ6_spl <=> (product1(e_4,e_3,e_3))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f121,plain,(
% 0.08/0.42 product1(e_4,e_3,e_3)|~sQ6_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f120])).
% 0.08/0.42 fof(f123,definition,(
% 0.08/0.42 sQ7_spl <=> (product1(e_4,e_3,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f124,plain,(
% 0.08/0.42 product1(e_4,e_3,e_4)|~sQ7_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f123])).
% 0.08/0.42 fof(f126,plain,(
% 0.08/0.42 sQ4_spl|sQ5_spl|sQ6_spl|sQ7_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f98,f114,f117,f120,f123])).
% 0.08/0.42 fof(f130,definition,(
% 0.08/0.42 sQ9_spl <=> (product1(e_4,e_2,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f131,plain,(
% 0.08/0.42 product1(e_4,e_2,e_2)|~sQ9_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f130])).
% 0.08/0.42 fof(f136,definition,(
% 0.08/0.42 sQ11_spl <=> (product1(e_4,e_2,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f137,plain,(
% 0.08/0.42 product1(e_4,e_2,e_4)|~sQ11_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f136])).
% 0.08/0.42 fof(f140,definition,(
% 0.08/0.42 sQ12_spl <=> (product1(e_4,e_1,e_1))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f141,plain,(
% 0.08/0.42 product1(e_4,e_1,e_1)|~sQ12_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f140])).
% 0.08/0.42 fof(f143,definition,(
% 0.08/0.42 sQ13_spl <=> (product1(e_4,e_1,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f144,plain,(
% 0.08/0.42 product1(e_4,e_1,e_2)|~sQ13_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f143])).
% 0.08/0.42 fof(f146,definition,(
% 0.08/0.42 sQ14_spl <=> (product1(e_4,e_1,e_3))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f147,plain,(
% 0.08/0.42 product1(e_4,e_1,e_3)|~sQ14_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f146])).
% 0.08/0.42 fof(f149,definition,(
% 0.08/0.42 sQ15_spl <=> (product1(e_4,e_1,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f150,plain,(
% 0.08/0.42 product1(e_4,e_1,e_4)|~sQ15_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f149])).
% 0.08/0.42 fof(f152,plain,(
% 0.08/0.42 sQ12_spl|sQ13_spl|sQ14_spl|sQ15_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f100,f140,f143,f146,f149])).
% 0.08/0.42 fof(f155,plain,(
% 0.08/0.42 product1(e_3,e_2,e_1)|product1(e_3,e_2,e_2)|product1(e_3,e_2,e_3)|product1(e_3,e_2,e_4)),
% 0.08/0.42 inference(resolution,[status(thm)],[f90,f50])).
% 0.08/0.42 fof(f156,plain,(
% 0.08/0.42 product1(e_3,e_1,e_1)|product1(e_3,e_1,e_2)|product1(e_3,e_1,e_3)|product1(e_3,e_1,e_4)),
% 0.08/0.42 inference(resolution,[status(thm)],[f90,f49])).
% 0.08/0.42 fof(f163,definition,(
% 0.08/0.42 sQ18_spl <=> (product1(e_3,e_4,e_3))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f164,plain,(
% 0.08/0.42 product1(e_3,e_4,e_3)|~sQ18_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f163])).
% 0.08/0.42 fof(f166,definition,(
% 0.08/0.42 sQ19_spl <=> (product1(e_3,e_4,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f167,plain,(
% 0.08/0.42 product1(e_3,e_4,e_4)|~sQ19_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f166])).
% 0.08/0.42 fof(f173,definition,(
% 0.08/0.42 sQ21_spl <=> (product1(e_3,e_3,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f174,plain,(
% 0.08/0.42 product1(e_3,e_3,e_2)|~sQ21_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f173])).
% 0.08/0.42 fof(f179,definition,(
% 0.08/0.42 sQ23_spl <=> (product1(e_3,e_3,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f180,plain,(
% 0.08/0.42 product1(e_3,e_3,e_4)|~sQ23_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f179])).
% 0.08/0.42 fof(f183,definition,(
% 0.08/0.42 sQ24_spl <=> (product1(e_3,e_2,e_1))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f184,plain,(
% 0.08/0.42 product1(e_3,e_2,e_1)|~sQ24_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f183])).
% 0.08/0.42 fof(f186,definition,(
% 0.08/0.42 sQ25_spl <=> (product1(e_3,e_2,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f187,plain,(
% 0.08/0.42 product1(e_3,e_2,e_2)|~sQ25_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f186])).
% 0.08/0.42 fof(f189,definition,(
% 0.08/0.42 sQ26_spl <=> (product1(e_3,e_2,e_3))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f190,plain,(
% 0.08/0.42 product1(e_3,e_2,e_3)|~sQ26_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f189])).
% 0.08/0.42 fof(f192,definition,(
% 0.08/0.42 sQ27_spl <=> (product1(e_3,e_2,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f193,plain,(
% 0.08/0.42 product1(e_3,e_2,e_4)|~sQ27_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f192])).
% 0.08/0.42 fof(f195,plain,(
% 0.08/0.42 sQ24_spl|sQ25_spl|sQ26_spl|sQ27_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f155,f183,f186,f189,f192])).
% 0.08/0.42 fof(f196,definition,(
% 0.08/0.42 sQ28_spl <=> (product1(e_3,e_1,e_1))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f197,plain,(
% 0.08/0.42 product1(e_3,e_1,e_1)|~sQ28_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f196])).
% 0.08/0.42 fof(f199,definition,(
% 0.08/0.42 sQ29_spl <=> (product1(e_3,e_1,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f200,plain,(
% 0.08/0.42 product1(e_3,e_1,e_2)|~sQ29_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f199])).
% 0.08/0.42 fof(f202,definition,(
% 0.08/0.42 sQ30_spl <=> (product1(e_3,e_1,e_3))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f203,plain,(
% 0.08/0.42 product1(e_3,e_1,e_3)|~sQ30_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f202])).
% 0.08/0.42 fof(f205,definition,(
% 0.08/0.42 sQ31_spl <=> (product1(e_3,e_1,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f206,plain,(
% 0.08/0.42 product1(e_3,e_1,e_4)|~sQ31_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f205])).
% 0.08/0.42 fof(f208,plain,(
% 0.08/0.42 sQ28_spl|sQ29_spl|sQ30_spl|sQ31_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f156,f196,f199,f202,f205])).
% 0.08/0.42 fof(f209,plain,(
% 0.08/0.42 product1(e_2,e_4,e_1)|product1(e_2,e_4,e_2)|product1(e_2,e_4,e_3)|product1(e_2,e_4,e_4)),
% 0.08/0.42 inference(resolution,[status(thm)],[f91,f52])).
% 0.08/0.42 fof(f210,plain,(
% 0.08/0.42 product1(e_2,e_3,e_1)|product1(e_2,e_3,e_2)|product1(e_2,e_3,e_3)|product1(e_2,e_3,e_4)),
% 0.08/0.42 inference(resolution,[status(thm)],[f91,f51])).
% 0.08/0.42 fof(f212,plain,(
% 0.08/0.42 product1(e_2,e_1,e_1)|product1(e_2,e_1,e_2)|product1(e_2,e_1,e_3)|product1(e_2,e_1,e_4)),
% 0.08/0.42 inference(resolution,[status(thm)],[f91,f49])).
% 0.08/0.42 fof(f213,definition,(
% 0.08/0.42 sQ32_spl <=> (product1(e_2,e_4,e_1))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f214,plain,(
% 0.08/0.42 product1(e_2,e_4,e_1)|~sQ32_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f213])).
% 0.08/0.42 fof(f216,definition,(
% 0.08/0.42 sQ33_spl <=> (product1(e_2,e_4,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f217,plain,(
% 0.08/0.42 product1(e_2,e_4,e_2)|~sQ33_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f216])).
% 0.08/0.42 fof(f219,definition,(
% 0.08/0.42 sQ34_spl <=> (product1(e_2,e_4,e_3))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f220,plain,(
% 0.08/0.42 product1(e_2,e_4,e_3)|~sQ34_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f219])).
% 0.08/0.42 fof(f222,definition,(
% 0.08/0.42 sQ35_spl <=> (product1(e_2,e_4,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f223,plain,(
% 0.08/0.42 product1(e_2,e_4,e_4)|~sQ35_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f222])).
% 0.08/0.42 fof(f225,plain,(
% 0.08/0.42 sQ32_spl|sQ33_spl|sQ34_spl|sQ35_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f209,f213,f216,f219,f222])).
% 0.08/0.42 fof(f226,definition,(
% 0.08/0.42 sQ36_spl <=> (product1(e_2,e_3,e_1))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f227,plain,(
% 0.08/0.42 product1(e_2,e_3,e_1)|~sQ36_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f226])).
% 0.08/0.42 fof(f229,definition,(
% 0.08/0.42 sQ37_spl <=> (product1(e_2,e_3,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f230,plain,(
% 0.08/0.42 product1(e_2,e_3,e_2)|~sQ37_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f229])).
% 0.08/0.42 fof(f232,definition,(
% 0.08/0.42 sQ38_spl <=> (product1(e_2,e_3,e_3))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f233,plain,(
% 0.08/0.42 product1(e_2,e_3,e_3)|~sQ38_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f232])).
% 0.08/0.42 fof(f235,definition,(
% 0.08/0.42 sQ39_spl <=> (product1(e_2,e_3,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f236,plain,(
% 0.08/0.42 product1(e_2,e_3,e_4)|~sQ39_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f235])).
% 0.08/0.42 fof(f238,plain,(
% 0.08/0.42 sQ36_spl|sQ37_spl|sQ38_spl|sQ39_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f210,f226,f229,f232,f235])).
% 0.08/0.42 fof(f239,definition,(
% 0.08/0.42 sQ40_spl <=> (product1(e_2,e_2,e_1))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f240,plain,(
% 0.08/0.42 product1(e_2,e_2,e_1)|~sQ40_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f239])).
% 0.08/0.42 fof(f252,definition,(
% 0.08/0.42 sQ44_spl <=> (product1(e_2,e_1,e_1))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f253,plain,(
% 0.08/0.42 product1(e_2,e_1,e_1)|~sQ44_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f252])).
% 0.08/0.42 fof(f255,definition,(
% 0.08/0.42 sQ45_spl <=> (product1(e_2,e_1,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f256,plain,(
% 0.08/0.42 product1(e_2,e_1,e_2)|~sQ45_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f255])).
% 0.08/0.42 fof(f258,definition,(
% 0.08/0.42 sQ46_spl <=> (product1(e_2,e_1,e_3))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f259,plain,(
% 0.08/0.42 product1(e_2,e_1,e_3)|~sQ46_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f258])).
% 0.08/0.42 fof(f261,definition,(
% 0.08/0.42 sQ47_spl <=> (product1(e_2,e_1,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f262,plain,(
% 0.08/0.42 product1(e_2,e_1,e_4)|~sQ47_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f261])).
% 0.08/0.42 fof(f264,plain,(
% 0.08/0.42 sQ44_spl|sQ45_spl|sQ46_spl|sQ47_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f212,f252,f255,f258,f261])).
% 0.08/0.42 fof(f266,plain,(
% 0.08/0.42 product1(e_1,e_3,e_1)|product1(e_1,e_3,e_2)|product1(e_1,e_3,e_3)|product1(e_1,e_3,e_4)),
% 0.08/0.42 inference(resolution,[status(thm)],[f92,f51])).
% 0.08/0.42 fof(f267,plain,(
% 0.08/0.42 product1(e_1,e_2,e_1)|product1(e_1,e_2,e_2)|product1(e_1,e_2,e_3)|product1(e_1,e_2,e_4)),
% 0.08/0.42 inference(resolution,[status(thm)],[f92,f50])).
% 0.08/0.42 fof(f282,definition,(
% 0.08/0.42 sQ52_spl <=> (product1(e_1,e_3,e_1))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f283,plain,(
% 0.08/0.42 product1(e_1,e_3,e_1)|~sQ52_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f282])).
% 0.08/0.42 fof(f285,definition,(
% 0.08/0.42 sQ53_spl <=> (product1(e_1,e_3,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f286,plain,(
% 0.08/0.42 product1(e_1,e_3,e_2)|~sQ53_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f285])).
% 0.08/0.42 fof(f288,definition,(
% 0.08/0.42 sQ54_spl <=> (product1(e_1,e_3,e_3))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f289,plain,(
% 0.08/0.42 product1(e_1,e_3,e_3)|~sQ54_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f288])).
% 0.08/0.42 fof(f291,definition,(
% 0.08/0.42 sQ55_spl <=> (product1(e_1,e_3,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f292,plain,(
% 0.08/0.42 product1(e_1,e_3,e_4)|~sQ55_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f291])).
% 0.08/0.42 fof(f294,plain,(
% 0.08/0.42 sQ52_spl|sQ53_spl|sQ54_spl|sQ55_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f266,f282,f285,f288,f291])).
% 0.08/0.42 fof(f295,definition,(
% 0.08/0.42 sQ56_spl <=> (product1(e_1,e_2,e_1))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f296,plain,(
% 0.08/0.42 product1(e_1,e_2,e_1)|~sQ56_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f295])).
% 0.08/0.42 fof(f298,definition,(
% 0.08/0.42 sQ57_spl <=> (product1(e_1,e_2,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f299,plain,(
% 0.08/0.42 product1(e_1,e_2,e_2)|~sQ57_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f298])).
% 0.08/0.42 fof(f301,definition,(
% 0.08/0.42 sQ58_spl <=> (product1(e_1,e_2,e_3))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f302,plain,(
% 0.08/0.42 product1(e_1,e_2,e_3)|~sQ58_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f301])).
% 0.08/0.42 fof(f304,definition,(
% 0.08/0.42 sQ59_spl <=> (product1(e_1,e_2,e_4))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f305,plain,(
% 0.08/0.42 product1(e_1,e_2,e_4)|~sQ59_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f304])).
% 0.08/0.42 fof(f307,plain,(
% 0.08/0.42 sQ56_spl|sQ57_spl|sQ58_spl|sQ59_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f267,f295,f298,f301,f304])).
% 0.08/0.42 fof(f311,definition,(
% 0.08/0.42 sQ61_spl <=> (product1(e_1,e_1,e_2))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f312,plain,(
% 0.08/0.42 product1(e_1,e_1,e_2)|~sQ61_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f311])).
% 0.08/0.42 fof(f545,plain,(
% 0.08/0.42 ![X0,X1]: (~product2(X0,X0,X1)|equalish(X1,X0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f75,f80])).
% 0.08/0.42 fof(f553,plain,(
% 0.08/0.42 equalish(e_1,e_4)|~sQ15_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f150,f87])).
% 0.08/0.42 fof(f559,plain,(
% 0.08/0.42 $false|~sQ15_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f553,f55])).
% 0.08/0.42 fof(f560,plain,(
% 0.08/0.42 ~sQ15_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f559])).
% 0.08/0.42 fof(f561,plain,(
% 0.08/0.42 ![X0]: (~product1(X0,e_1,e_3)|equalish(X0,e_4)|~sQ14_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f147,f71])).
% 0.08/0.42 fof(f569,plain,(
% 0.08/0.42 ![X0]: (~product1(X0,e_1,e_2)|equalish(X0,e_4)|~sQ13_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f144,f71])).
% 0.08/0.42 fof(f570,plain,(
% 0.08/0.42 ![X0]: (~product1(e_4,X0,e_2)|equalish(X0,e_1)|~sQ13_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f144,f69])).
% 0.08/0.42 fof(f575,plain,(
% 0.08/0.42 equalish(e_4,e_1)|~sQ12_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f141,f88])).
% 0.08/0.42 fof(f580,plain,(
% 0.08/0.42 $false|~sQ12_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f575,f62])).
% 0.08/0.42 fof(f581,plain,(
% 0.08/0.42 ~sQ12_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f580])).
% 0.08/0.42 fof(f582,plain,(
% 0.08/0.42 equalish(e_2,e_4)|~sQ11_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f137,f87])).
% 0.08/0.42 fof(f588,plain,(
% 0.08/0.42 $false|~sQ11_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f582,f58])).
% 0.08/0.42 fof(f589,plain,(
% 0.08/0.42 ~sQ11_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f588])).
% 0.08/0.42 fof(f599,plain,(
% 0.08/0.42 equalish(e_4,e_2)|~sQ9_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f131,f88])).
% 0.08/0.42 fof(f613,plain,(
% 0.08/0.42 equalish(e_3,e_4)|~sQ7_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f124,f87])).
% 0.08/0.42 fof(f619,plain,(
% 0.08/0.42 $false|~sQ7_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f613,f61])).
% 0.08/0.42 fof(f620,plain,(
% 0.08/0.42 ~sQ7_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f619])).
% 0.08/0.42 fof(f621,plain,(
% 0.08/0.42 equalish(e_4,e_3)|~sQ6_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f121,f88])).
% 0.08/0.42 fof(f626,plain,(
% 0.08/0.42 $false|~sQ6_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f621,f64])).
% 0.08/0.42 fof(f627,plain,(
% 0.08/0.42 ~sQ6_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f626])).
% 0.08/0.42 fof(f628,plain,(
% 0.08/0.42 equalish(e_3,e_1)|~sQ5_spl|~sQ13_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f118,f570])).
% 0.08/0.42 fof(f629,plain,(
% 0.08/0.42 ![X0]: (~product1(X0,e_3,e_2)|equalish(X0,e_4)|~sQ5_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f118,f71])).
% 0.08/0.42 fof(f633,plain,(
% 0.08/0.42 $false|~sQ5_spl|~sQ13_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f628,f59])).
% 0.08/0.42 fof(f634,plain,(
% 0.08/0.42 ~sQ5_spl|~sQ13_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f633])).
% 0.08/0.42 fof(f636,plain,(
% 0.08/0.42 ![X0]: (~product1(X0,e_3,e_1)|equalish(X0,e_4)|~sQ4_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f115,f71])).
% 0.08/0.42 fof(f639,plain,(
% 0.08/0.42 ![X0]: (~product1(e_3,X0,e_4)|product2(e_1,X0,e_3)|~sQ4_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f115,f82])).
% 0.08/0.42 fof(f647,plain,(
% 0.08/0.42 product2(e_1,e_1,e_3)|~sQ31_spl|~sQ4_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f206,f639])).
% 0.08/0.42 fof(f653,plain,(
% 0.08/0.42 equalish(e_3,e_1)|~sQ31_spl|~sQ4_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f647,f545])).
% 0.08/0.42 fof(f656,plain,(
% 0.08/0.42 $false|~sQ31_spl|~sQ4_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f653,f59])).
% 0.08/0.42 fof(f657,plain,(
% 0.08/0.42 ~sQ31_spl|~sQ4_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f656])).
% 0.08/0.42 fof(f658,plain,(
% 0.08/0.42 equalish(e_1,e_3)|~sQ30_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f203,f87])).
% 0.08/0.42 fof(f664,plain,(
% 0.08/0.42 $false|~sQ30_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f658,f54])).
% 0.08/0.42 fof(f665,plain,(
% 0.08/0.42 ~sQ30_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f664])).
% 0.08/0.42 fof(f666,plain,(
% 0.08/0.42 equalish(e_3,e_4)|~sQ29_spl|~sQ13_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f200,f569])).
% 0.08/0.42 fof(f671,plain,(
% 0.08/0.42 $false|~sQ29_spl|~sQ13_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f666,f61])).
% 0.08/0.42 fof(f672,plain,(
% 0.08/0.42 ~sQ29_spl|~sQ13_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f671])).
% 0.08/0.42 fof(f673,plain,(
% 0.08/0.42 equalish(e_3,e_1)|~sQ28_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f197,f88])).
% 0.08/0.42 fof(f678,plain,(
% 0.08/0.42 $false|~sQ28_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f673,f59])).
% 0.08/0.42 fof(f679,plain,(
% 0.08/0.42 ~sQ28_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f678])).
% 0.08/0.42 fof(f680,plain,(
% 0.08/0.42 $false|~sQ9_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f599,f63])).
% 0.08/0.42 fof(f681,plain,(
% 0.08/0.42 ~sQ9_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f680])).
% 0.08/0.42 fof(f686,plain,(
% 0.08/0.42 ![X0]: (~product1(e_2,X0,e_3)|product2(e_4,X0,e_2)|~sQ27_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f193,f82])).
% 0.08/0.42 fof(f687,plain,(
% 0.08/0.42 equalish(e_2,e_3)|~sQ26_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f190,f87])).
% 0.08/0.42 fof(f693,plain,(
% 0.08/0.42 $false|~sQ26_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f687,f57])).
% 0.08/0.42 fof(f694,plain,(
% 0.08/0.42 ~sQ26_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f693])).
% 0.08/0.42 fof(f695,plain,(
% 0.08/0.42 equalish(e_3,e_2)|~sQ25_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f187,f88])).
% 0.08/0.42 fof(f700,plain,(
% 0.08/0.42 $false|~sQ25_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f695,f60])).
% 0.08/0.42 fof(f701,plain,(
% 0.08/0.42 ~sQ25_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f700])).
% 0.08/0.42 fof(f702,plain,(
% 0.08/0.42 ![X0]: (~product1(X0,e_2,e_1)|equalish(X0,e_3)|~sQ24_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f184,f71])).
% 0.08/0.42 fof(f709,plain,(
% 0.08/0.42 equalish(e_4,e_3)|~sQ23_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f180,f85])).
% 0.08/0.42 fof(f712,plain,(
% 0.08/0.42 $false|~sQ23_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f709,f64])).
% 0.08/0.42 fof(f713,plain,(
% 0.08/0.42 ~sQ23_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f712])).
% 0.08/0.42 fof(f716,plain,(
% 0.08/0.42 equalish(e_2,e_3)|~sQ21_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f174,f85])).
% 0.08/0.42 fof(f719,plain,(
% 0.08/0.42 $false|~sQ21_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f716,f57])).
% 0.08/0.42 fof(f720,plain,(
% 0.08/0.42 ~sQ21_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f719])).
% 0.08/0.42 fof(f730,plain,(
% 0.08/0.42 equalish(e_3,e_4)|~sQ19_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f167,f88])).
% 0.08/0.42 fof(f735,plain,(
% 0.08/0.42 $false|~sQ19_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f730,f61])).
% 0.08/0.42 fof(f736,plain,(
% 0.08/0.42 ~sQ19_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f735])).
% 0.08/0.42 fof(f737,plain,(
% 0.08/0.42 equalish(e_4,e_3)|~sQ18_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f164,f87])).
% 0.08/0.42 fof(f743,plain,(
% 0.08/0.42 $false|~sQ18_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f737,f64])).
% 0.08/0.42 fof(f744,plain,(
% 0.08/0.42 ~sQ18_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f743])).
% 0.08/0.42 fof(f785,plain,(
% 0.08/0.42 ![X0]: (~product1(e_2,X0,e_4)|equalish(X0,e_1)|~sQ47_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f262,f69])).
% 0.08/0.42 fof(f799,plain,(
% 0.08/0.42 equalish(e_2,e_4)|~sQ46_spl|~sQ14_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f259,f561])).
% 0.08/0.42 fof(f807,plain,(
% 0.08/0.42 equalish(e_1,e_2)|~sQ45_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f256,f87])).
% 0.08/0.42 fof(f815,plain,(
% 0.08/0.42 equalish(e_2,e_1)|~sQ44_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f253,f88])).
% 0.08/0.42 fof(f820,plain,(
% 0.08/0.42 $false|~sQ44_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f815,f56])).
% 0.08/0.42 fof(f821,plain,(
% 0.08/0.42 ~sQ44_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f820])).
% 0.08/0.42 fof(f822,plain,(
% 0.08/0.42 $false|~sQ46_spl|~sQ14_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f799,f58])).
% 0.08/0.42 fof(f823,plain,(
% 0.08/0.42 ~sQ46_spl|~sQ14_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f822])).
% 0.08/0.42 fof(f824,plain,(
% 0.08/0.42 $false|~sQ45_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f807,f53])).
% 0.08/0.42 fof(f825,plain,(
% 0.08/0.42 ~sQ45_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f824])).
% 0.08/0.42 fof(f858,plain,(
% 0.08/0.42 equalish(e_1,e_2)|~sQ40_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f240,f85])).
% 0.08/0.42 fof(f861,plain,(
% 0.08/0.42 $false|~sQ40_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f858,f53])).
% 0.08/0.42 fof(f862,plain,(
% 0.08/0.42 ~sQ40_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f861])).
% 0.08/0.42 fof(f863,plain,(
% 0.08/0.42 equalish(e_3,e_1)|~sQ39_spl|~sQ47_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f236,f785])).
% 0.08/0.42 fof(f869,plain,(
% 0.08/0.42 $false|~sQ39_spl|~sQ47_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f863,f59])).
% 0.08/0.42 fof(f870,plain,(
% 0.08/0.42 ~sQ39_spl|~sQ47_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f869])).
% 0.08/0.42 fof(f872,plain,(
% 0.08/0.42 equalish(e_2,e_3)|~sQ38_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f233,f88])).
% 0.08/0.42 fof(f877,plain,(
% 0.08/0.42 $false|~sQ38_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f872,f57])).
% 0.08/0.42 fof(f878,plain,(
% 0.08/0.42 ~sQ38_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f877])).
% 0.08/0.42 fof(f879,plain,(
% 0.08/0.42 equalish(e_3,e_2)|~sQ37_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f230,f87])).
% 0.08/0.42 fof(f885,plain,(
% 0.08/0.42 $false|~sQ37_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f879,f60])).
% 0.08/0.42 fof(f886,plain,(
% 0.08/0.42 ~sQ37_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f885])).
% 0.08/0.42 fof(f887,plain,(
% 0.08/0.42 equalish(e_2,e_4)|~sQ36_spl|~sQ4_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f227,f636])).
% 0.08/0.42 fof(f888,plain,(
% 0.08/0.42 ![X0]: (~product1(X0,e_3,e_1)|equalish(X0,e_2)|~sQ36_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f227,f71])).
% 0.08/0.42 fof(f889,plain,(
% 0.08/0.42 ![X0]: (~product1(e_2,X0,e_1)|equalish(X0,e_3)|~sQ36_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f227,f69])).
% 0.08/0.42 fof(f892,plain,(
% 0.08/0.42 $false|~sQ36_spl|~sQ4_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f887,f58])).
% 0.08/0.42 fof(f893,plain,(
% 0.08/0.42 ~sQ36_spl|~sQ4_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f892])).
% 0.08/0.42 fof(f894,plain,(
% 0.08/0.42 equalish(e_4,e_1)|~sQ35_spl|~sQ47_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f223,f785])).
% 0.08/0.42 fof(f901,plain,(
% 0.08/0.42 $false|~sQ35_spl|~sQ47_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f894,f62])).
% 0.08/0.42 fof(f902,plain,(
% 0.08/0.42 ~sQ35_spl|~sQ47_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f901])).
% 0.08/0.42 fof(f903,plain,(
% 0.08/0.42 product2(e_4,e_4,e_2)|~sQ34_spl|~sQ27_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f220,f686])).
% 0.08/0.42 fof(f909,plain,(
% 0.08/0.42 equalish(e_2,e_4)|~sQ34_spl|~sQ27_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f903,f545])).
% 0.08/0.42 fof(f912,plain,(
% 0.08/0.42 $false|~sQ34_spl|~sQ27_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f909,f58])).
% 0.08/0.42 fof(f913,plain,(
% 0.08/0.42 ~sQ34_spl|~sQ27_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f912])).
% 0.08/0.42 fof(f917,plain,(
% 0.08/0.42 equalish(e_4,e_2)|~sQ33_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f217,f87])).
% 0.08/0.42 fof(f923,plain,(
% 0.08/0.42 $false|~sQ33_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f917,f63])).
% 0.08/0.42 fof(f924,plain,(
% 0.08/0.42 ~sQ33_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f923])).
% 0.08/0.42 fof(f925,plain,(
% 0.08/0.42 equalish(e_4,e_3)|~sQ32_spl|~sQ36_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f214,f889])).
% 0.08/0.42 fof(f931,plain,(
% 0.08/0.42 $false|~sQ32_spl|~sQ36_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f925,f64])).
% 0.08/0.42 fof(f932,plain,(
% 0.08/0.42 ~sQ32_spl|~sQ36_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f931])).
% 0.08/0.42 fof(f955,plain,(
% 0.08/0.42 equalish(e_2,e_1)|~sQ61_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f312,f85])).
% 0.08/0.42 fof(f958,plain,(
% 0.08/0.42 $false|~sQ61_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f955,f56])).
% 0.08/0.42 fof(f959,plain,(
% 0.08/0.42 ~sQ61_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f958])).
% 0.08/0.42 fof(f962,plain,(
% 0.08/0.42 ![X0]: (~product1(e_1,X0,e_4)|equalish(X0,e_2)|~sQ59_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f305,f69])).
% 0.08/0.42 fof(f987,plain,(
% 0.08/0.42 ![X0]: (~product1(e_2,X0,e_1)|product2(e_3,X0,e_2)|~sQ58_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f302,f82])).
% 0.08/0.42 fof(f991,plain,(
% 0.08/0.42 equalish(e_1,e_2)|~sQ57_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f299,f88])).
% 0.08/0.42 fof(f996,plain,(
% 0.08/0.42 $false|~sQ57_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f991,f53])).
% 0.08/0.42 fof(f997,plain,(
% 0.08/0.42 ~sQ57_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f996])).
% 0.08/0.42 fof(f998,plain,(
% 0.08/0.42 equalish(e_1,e_3)|~sQ56_spl|~sQ24_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f296,f702])).
% 0.08/0.42 fof(f1005,plain,(
% 0.08/0.42 $false|~sQ56_spl|~sQ24_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f998,f54])).
% 0.08/0.42 fof(f1006,plain,(
% 0.08/0.42 ~sQ56_spl|~sQ24_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f1005])).
% 0.08/0.42 fof(f1015,plain,(
% 0.08/0.42 product2(e_3,e_3,e_2)|~sQ58_spl|~sQ36_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f987,f227])).
% 0.08/0.42 fof(f1017,plain,(
% 0.08/0.42 equalish(e_2,e_3)|~sQ58_spl|~sQ36_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f1015,f545])).
% 0.08/0.42 fof(f1020,plain,(
% 0.08/0.42 $false|~sQ58_spl|~sQ36_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1017,f57])).
% 0.08/0.42 fof(f1021,plain,(
% 0.08/0.42 ~sQ58_spl|~sQ36_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f1020])).
% 0.08/0.42 fof(f1041,plain,(
% 0.08/0.42 equalish(e_3,e_2)|~sQ55_spl|~sQ59_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f292,f962])).
% 0.08/0.42 fof(f1047,plain,(
% 0.08/0.42 $false|~sQ55_spl|~sQ59_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1041,f60])).
% 0.08/0.42 fof(f1048,plain,(
% 0.08/0.42 ~sQ55_spl|~sQ59_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f1047])).
% 0.08/0.42 fof(f1050,plain,(
% 0.08/0.42 equalish(e_1,e_3)|~sQ54_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f289,f88])).
% 0.08/0.42 fof(f1055,plain,(
% 0.08/0.42 $false|~sQ54_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1050,f54])).
% 0.08/0.42 fof(f1056,plain,(
% 0.08/0.42 ~sQ54_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f1055])).
% 0.08/0.42 fof(f1058,plain,(
% 0.08/0.42 equalish(e_1,e_4)|~sQ53_spl|~sQ5_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f286,f629])).
% 0.08/0.42 fof(f1063,plain,(
% 0.08/0.42 $false|~sQ53_spl|~sQ5_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1058,f55])).
% 0.08/0.42 fof(f1064,plain,(
% 0.08/0.42 ~sQ53_spl|~sQ5_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f1063])).
% 0.08/0.42 fof(f1065,plain,(
% 0.08/0.42 equalish(e_1,e_2)|~sQ52_spl|~sQ36_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f283,f888])).
% 0.08/0.42 fof(f1072,plain,(
% 0.08/0.42 $false|~sQ52_spl|~sQ36_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1065,f53])).
% 0.08/0.42 fof(f1073,plain,(
% 0.08/0.42 ~sQ52_spl|~sQ36_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f1072])).
% 0.08/0.42 fof(f1074,plain,(
% 0.08/0.42 $false),
% 0.08/0.42 inference(sat_refutation,[status(thm)],[f126,f152,f195,f208,f225,f238,f264,f294,f307,f560,f581,f589,f620,f627,f634,f657,f665,f672,f679,f681,f694,f701,f713,f720,f736,f744,f821,f823,f825,f862,f870,f878,f886,f893,f902,f913,f924,f932,f959,f997,f1006,f1021,f1048,f1056,f1064,f1073])).
% 0.08/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.08/0.43 % Elapsed time: 0.061292 seconds
% 0.08/0.43 % CPU time: 0.281749 seconds
% 0.08/0.43 % Total memory used: 20.337 MB
% 0.08/0.43 % Net memory used: 20.119 MB
%------------------------------------------------------------------------------