%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP133-1.003 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:36:02 PM UTC 2026
% Result : Unsatisfiable 0.02s 0.34s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP133-1.003 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Sun Sep 20 20:01:21 UTC 2026
% 0.02/0.30 % CPUTime :
% 0.02/0.30 % Drodi V4.1.1
% 0.02/0.34 % Refutation found
% 0.02/0.34 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.02/0.34 % SZS output start CNFRefutation for theBenchmark
% 0.02/0.34 fof(f1,axiom,(
% 0.02/0.34 group_element(e_1) ),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f2,axiom,(
% 0.02/0.34 group_element(e_2) ),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f3,axiom,(
% 0.02/0.34 group_element(e_3) ),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f4,axiom,(
% 0.02/0.34 ~ equalish(e_1,e_2) ),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f5,axiom,(
% 0.02/0.34 ~ equalish(e_1,e_3) ),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f6,axiom,(
% 0.02/0.34 ~ equalish(e_2,e_1) ),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f7,axiom,(
% 0.02/0.34 ~ equalish(e_2,e_3) ),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f8,axiom,(
% 0.02/0.34 ~ equalish(e_3,e_1) ),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f9,axiom,(
% 0.02/0.34 ~ equalish(e_3,e_2) ),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f10,axiom,(
% 0.02/0.34 (![X,Y]: (( ~ group_element(X)| ~ group_element(Y)| product(X,Y,e_1)| product(X,Y,e_2)| product(X,Y,e_3) ) ))),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f11,axiom,(
% 0.02/0.34 (![X,Y,W,Z]: (( ~ product(X,Y,W)| ~ product(X,Y,Z)| equalish(W,Z) ) ))),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f12,axiom,(
% 0.02/0.34 (![X,W,Y,Z]: (( ~ product(X,W,Y)| ~ product(X,Z,Y)| equalish(W,Z) ) ))),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f13,axiom,(
% 0.02/0.34 (![W,Y,X,Z]: (( ~ product(W,Y,X)| ~ product(Z,Y,X)| equalish(W,Z) ) ))),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f14,negated_conjecture,(
% 0.02/0.34 (![X,Y,Z1,Z2]: (( ~ product(X,Y,Z1)| ~ product(Y,X,Z2)| product(Z1,Z2,X) ) ))),
% 0.02/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.34 fof(f15,plain,(
% 0.02/0.34 group_element(e_1)),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.34 fof(f16,plain,(
% 0.02/0.34 group_element(e_2)),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.34 fof(f17,plain,(
% 0.02/0.34 group_element(e_3)),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.34 fof(f18,plain,(
% 0.02/0.34 ~equalish(e_1,e_2)),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f4])).
% 0.02/0.34 fof(f19,plain,(
% 0.02/0.34 ~equalish(e_1,e_3)),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f5])).
% 0.02/0.34 fof(f20,plain,(
% 0.02/0.34 ~equalish(e_2,e_1)),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f6])).
% 0.02/0.34 fof(f21,plain,(
% 0.02/0.34 ~equalish(e_2,e_3)),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f7])).
% 0.02/0.34 fof(f22,plain,(
% 0.02/0.34 ~equalish(e_3,e_1)),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f8])).
% 0.02/0.34 fof(f23,plain,(
% 0.02/0.34 ~equalish(e_3,e_2)),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f9])).
% 0.02/0.34 fof(f24,plain,(
% 0.02/0.34 ![X0,X1]: (~group_element(X0)|~group_element(X1)|product(X0,X1,e_1)|product(X0,X1,e_2)|product(X0,X1,e_3))),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f10])).
% 0.02/0.34 fof(f25,plain,(
% 0.02/0.34 ![W,Z]: ((![X,Y]: (~product(X,Y,W)|~product(X,Y,Z)))|equalish(W,Z))),
% 0.02/0.34 inference(miniscoping,[status(thm)],[f11])).
% 0.02/0.34 fof(f26,plain,(
% 0.02/0.34 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|equalish(X2,X3))),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f25])).
% 0.02/0.34 fof(f27,plain,(
% 0.02/0.34 ![W,Z]: ((![X,Y]: (~product(X,W,Y)|~product(X,Z,Y)))|equalish(W,Z))),
% 0.02/0.34 inference(miniscoping,[status(thm)],[f12])).
% 0.02/0.34 fof(f28,plain,(
% 0.02/0.34 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X3,X2)|equalish(X1,X3))),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f27])).
% 0.02/0.34 fof(f29,plain,(
% 0.02/0.34 ![W,Z]: ((![Y,X]: (~product(W,Y,X)|~product(Z,Y,X)))|equalish(W,Z))),
% 0.02/0.34 inference(miniscoping,[status(thm)],[f13])).
% 0.02/0.34 fof(f30,plain,(
% 0.02/0.34 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X3,X1,X2)|equalish(X0,X3))),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f29])).
% 0.02/0.34 fof(f31,plain,(
% 0.02/0.34 ![X,Z1,Z2]: ((![Y]: (~product(X,Y,Z1)|~product(Y,X,Z2)))|product(Z1,Z2,X))),
% 0.02/0.34 inference(miniscoping,[status(thm)],[f14])).
% 0.02/0.34 fof(f32,plain,(
% 0.02/0.34 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X1,X0,X3)|product(X2,X3,X0))),
% 0.02/0.34 inference(cnf_transformation,[status(thm)],[f31])).
% 0.02/0.34 fof(f33,plain,(
% 0.02/0.34 ![X0]: (~group_element(X0)|product(e_3,X0,e_1)|product(e_3,X0,e_2)|product(e_3,X0,e_3))),
% 0.02/0.34 inference(resolution,[status(thm)],[f24,f17])).
% 0.02/0.34 fof(f34,plain,(
% 0.02/0.34 ![X0]: (~group_element(X0)|product(e_2,X0,e_1)|product(e_2,X0,e_2)|product(e_2,X0,e_3))),
% 0.02/0.34 inference(resolution,[status(thm)],[f24,f16])).
% 0.02/0.34 fof(f35,plain,(
% 0.02/0.34 ![X0]: (~group_element(X0)|product(e_1,X0,e_1)|product(e_1,X0,e_2)|product(e_1,X0,e_3))),
% 0.02/0.34 inference(resolution,[status(thm)],[f24,f15])).
% 0.02/0.34 fof(f36,plain,(
% 0.02/0.34 product(e_3,e_3,e_1)|product(e_3,e_3,e_2)|product(e_3,e_3,e_3)),
% 0.02/0.34 inference(resolution,[status(thm)],[f33,f17])).
% 0.02/0.34 fof(f37,plain,(
% 0.02/0.34 product(e_3,e_2,e_1)|product(e_3,e_2,e_2)|product(e_3,e_2,e_3)),
% 0.02/0.34 inference(resolution,[status(thm)],[f33,f16])).
% 0.02/0.34 fof(f38,plain,(
% 0.02/0.34 product(e_3,e_1,e_1)|product(e_3,e_1,e_2)|product(e_3,e_1,e_3)),
% 0.02/0.34 inference(resolution,[status(thm)],[f33,f15])).
% 0.02/0.34 fof(f39,definition,(
% 0.02/0.34 sQ0_spl <=> (product(e_3,e_3,e_1))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f40,plain,(
% 0.02/0.34 product(e_3,e_3,e_1)|~sQ0_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f39])).
% 0.02/0.34 fof(f42,definition,(
% 0.02/0.34 sQ1_spl <=> (product(e_3,e_3,e_2))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f43,plain,(
% 0.02/0.34 product(e_3,e_3,e_2)|~sQ1_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f42])).
% 0.02/0.34 fof(f45,definition,(
% 0.02/0.34 sQ2_spl <=> (product(e_3,e_3,e_3))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f46,plain,(
% 0.02/0.34 product(e_3,e_3,e_3)|~sQ2_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f45])).
% 0.02/0.34 fof(f48,plain,(
% 0.02/0.34 sQ0_spl|sQ1_spl|sQ2_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f36,f39,f42,f45])).
% 0.02/0.34 fof(f49,definition,(
% 0.02/0.34 sQ3_spl <=> (product(e_3,e_2,e_1))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f50,plain,(
% 0.02/0.34 product(e_3,e_2,e_1)|~sQ3_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f49])).
% 0.02/0.34 fof(f52,definition,(
% 0.02/0.34 sQ4_spl <=> (product(e_3,e_2,e_2))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f53,plain,(
% 0.02/0.34 product(e_3,e_2,e_2)|~sQ4_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f52])).
% 0.02/0.34 fof(f55,definition,(
% 0.02/0.34 sQ5_spl <=> (product(e_3,e_2,e_3))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f56,plain,(
% 0.02/0.34 product(e_3,e_2,e_3)|~sQ5_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f55])).
% 0.02/0.34 fof(f58,plain,(
% 0.02/0.34 sQ3_spl|sQ4_spl|sQ5_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f37,f49,f52,f55])).
% 0.02/0.34 fof(f59,definition,(
% 0.02/0.34 sQ6_spl <=> (product(e_3,e_1,e_1))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f60,plain,(
% 0.02/0.34 product(e_3,e_1,e_1)|~sQ6_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f59])).
% 0.02/0.34 fof(f62,definition,(
% 0.02/0.34 sQ7_spl <=> (product(e_3,e_1,e_2))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f63,plain,(
% 0.02/0.34 product(e_3,e_1,e_2)|~sQ7_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f62])).
% 0.02/0.34 fof(f65,definition,(
% 0.02/0.34 sQ8_spl <=> (product(e_3,e_1,e_3))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f66,plain,(
% 0.02/0.34 product(e_3,e_1,e_3)|~sQ8_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f65])).
% 0.02/0.34 fof(f68,plain,(
% 0.02/0.34 sQ6_spl|sQ7_spl|sQ8_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f38,f59,f62,f65])).
% 0.02/0.34 fof(f72,plain,(
% 0.02/0.34 ![X0]: (~product(e_1,e_3,X0)|product(e_3,X0,e_3)|~sQ8_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f66,f32])).
% 0.02/0.34 fof(f76,plain,(
% 0.02/0.34 ![X0]: (~product(e_1,e_3,X0)|product(e_2,X0,e_3)|~sQ7_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f63,f32])).
% 0.02/0.34 fof(f81,plain,(
% 0.02/0.34 product(e_2,e_3,e_1)|product(e_2,e_3,e_2)|product(e_2,e_3,e_3)),
% 0.02/0.34 inference(resolution,[status(thm)],[f34,f17])).
% 0.02/0.34 fof(f82,plain,(
% 0.02/0.34 product(e_2,e_2,e_1)|product(e_2,e_2,e_2)|product(e_2,e_2,e_3)),
% 0.02/0.34 inference(resolution,[status(thm)],[f34,f16])).
% 0.02/0.34 fof(f83,plain,(
% 0.02/0.34 product(e_2,e_1,e_1)|product(e_2,e_1,e_2)|product(e_2,e_1,e_3)),
% 0.02/0.34 inference(resolution,[status(thm)],[f34,f15])).
% 0.02/0.34 fof(f84,definition,(
% 0.02/0.34 sQ9_spl <=> (product(e_2,e_3,e_1))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f85,plain,(
% 0.02/0.34 product(e_2,e_3,e_1)|~sQ9_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f84])).
% 0.02/0.34 fof(f87,definition,(
% 0.02/0.34 sQ10_spl <=> (product(e_2,e_3,e_2))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f88,plain,(
% 0.02/0.34 product(e_2,e_3,e_2)|~sQ10_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f87])).
% 0.02/0.34 fof(f90,definition,(
% 0.02/0.34 sQ11_spl <=> (product(e_2,e_3,e_3))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f91,plain,(
% 0.02/0.34 product(e_2,e_3,e_3)|~sQ11_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f90])).
% 0.02/0.34 fof(f93,plain,(
% 0.02/0.34 sQ9_spl|sQ10_spl|sQ11_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f81,f84,f87,f90])).
% 0.02/0.34 fof(f94,definition,(
% 0.02/0.34 sQ12_spl <=> (product(e_2,e_2,e_1))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f95,plain,(
% 0.02/0.34 product(e_2,e_2,e_1)|~sQ12_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f94])).
% 0.02/0.34 fof(f97,definition,(
% 0.02/0.34 sQ13_spl <=> (product(e_2,e_2,e_2))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f98,plain,(
% 0.02/0.34 product(e_2,e_2,e_2)|~sQ13_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f97])).
% 0.02/0.34 fof(f100,definition,(
% 0.02/0.34 sQ14_spl <=> (product(e_2,e_2,e_3))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f101,plain,(
% 0.02/0.34 product(e_2,e_2,e_3)|~sQ14_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f100])).
% 0.02/0.34 fof(f103,plain,(
% 0.02/0.34 sQ12_spl|sQ13_spl|sQ14_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f82,f94,f97,f100])).
% 0.02/0.34 fof(f104,definition,(
% 0.02/0.34 sQ15_spl <=> (product(e_2,e_1,e_1))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f105,plain,(
% 0.02/0.34 product(e_2,e_1,e_1)|~sQ15_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f104])).
% 0.02/0.34 fof(f107,definition,(
% 0.02/0.34 sQ16_spl <=> (product(e_2,e_1,e_2))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f108,plain,(
% 0.02/0.34 product(e_2,e_1,e_2)|~sQ16_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f107])).
% 0.02/0.34 fof(f110,definition,(
% 0.02/0.34 sQ17_spl <=> (product(e_2,e_1,e_3))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f111,plain,(
% 0.02/0.34 product(e_2,e_1,e_3)|~sQ17_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f110])).
% 0.02/0.34 fof(f113,plain,(
% 0.02/0.34 sQ15_spl|sQ16_spl|sQ17_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f83,f104,f107,f110])).
% 0.02/0.34 fof(f114,plain,(
% 0.02/0.34 product(e_1,e_3,e_1)|product(e_1,e_3,e_2)|product(e_1,e_3,e_3)),
% 0.02/0.34 inference(resolution,[status(thm)],[f35,f17])).
% 0.02/0.34 fof(f115,plain,(
% 0.02/0.34 product(e_1,e_2,e_1)|product(e_1,e_2,e_2)|product(e_1,e_2,e_3)),
% 0.02/0.34 inference(resolution,[status(thm)],[f35,f16])).
% 0.02/0.34 fof(f116,plain,(
% 0.02/0.34 product(e_1,e_1,e_1)|product(e_1,e_1,e_2)|product(e_1,e_1,e_3)),
% 0.02/0.34 inference(resolution,[status(thm)],[f35,f15])).
% 0.02/0.34 fof(f117,definition,(
% 0.02/0.34 sQ18_spl <=> (product(e_1,e_3,e_1))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f118,plain,(
% 0.02/0.34 product(e_1,e_3,e_1)|~sQ18_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f117])).
% 0.02/0.34 fof(f120,definition,(
% 0.02/0.34 sQ19_spl <=> (product(e_1,e_3,e_2))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f121,plain,(
% 0.02/0.34 product(e_1,e_3,e_2)|~sQ19_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f120])).
% 0.02/0.34 fof(f123,definition,(
% 0.02/0.34 sQ20_spl <=> (product(e_1,e_3,e_3))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f124,plain,(
% 0.02/0.34 product(e_1,e_3,e_3)|~sQ20_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f123])).
% 0.02/0.34 fof(f126,plain,(
% 0.02/0.34 sQ18_spl|sQ19_spl|sQ20_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f114,f117,f120,f123])).
% 0.02/0.34 fof(f127,definition,(
% 0.02/0.34 sQ21_spl <=> (product(e_1,e_2,e_1))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f128,plain,(
% 0.02/0.34 product(e_1,e_2,e_1)|~sQ21_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f127])).
% 0.02/0.34 fof(f130,definition,(
% 0.02/0.34 sQ22_spl <=> (product(e_1,e_2,e_2))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f131,plain,(
% 0.02/0.34 product(e_1,e_2,e_2)|~sQ22_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f130])).
% 0.02/0.34 fof(f133,definition,(
% 0.02/0.34 sQ23_spl <=> (product(e_1,e_2,e_3))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f134,plain,(
% 0.02/0.34 product(e_1,e_2,e_3)|~sQ23_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f133])).
% 0.02/0.34 fof(f136,plain,(
% 0.02/0.34 sQ21_spl|sQ22_spl|sQ23_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f115,f127,f130,f133])).
% 0.02/0.34 fof(f137,definition,(
% 0.02/0.34 sQ24_spl <=> (product(e_1,e_1,e_1))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f138,plain,(
% 0.02/0.34 product(e_1,e_1,e_1)|~sQ24_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f137])).
% 0.02/0.34 fof(f140,definition,(
% 0.02/0.34 sQ25_spl <=> (product(e_1,e_1,e_2))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f141,plain,(
% 0.02/0.34 product(e_1,e_1,e_2)|~sQ25_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f140])).
% 0.02/0.34 fof(f143,definition,(
% 0.02/0.34 sQ26_spl <=> (product(e_1,e_1,e_3))),
% 0.02/0.34 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.02/0.34 fof(f144,plain,(
% 0.02/0.34 product(e_1,e_1,e_3)|~sQ26_spl),
% 0.02/0.34 inference(component_clause,[status(thm)],[f143])).
% 0.02/0.34 fof(f146,plain,(
% 0.02/0.34 sQ24_spl|sQ25_spl|sQ26_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f116,f137,f140,f143])).
% 0.02/0.34 fof(f150,plain,(
% 0.02/0.34 ![X0]: (~product(e_2,e_3,X0)|product(e_3,X0,e_3)|~sQ5_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f56,f32])).
% 0.02/0.34 fof(f154,plain,(
% 0.02/0.34 ![X0]: (~product(e_2,e_3,X0)|product(e_2,X0,e_3)|~sQ4_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f53,f32])).
% 0.02/0.34 fof(f158,plain,(
% 0.02/0.34 ![X0]: (~product(e_2,e_3,X0)|product(e_1,X0,e_3)|~sQ3_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f50,f32])).
% 0.02/0.34 fof(f159,plain,(
% 0.02/0.34 ![X0]: (~product(X0,e_3,e_3)|equalish(e_3,X0)|~sQ2_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f46,f30])).
% 0.02/0.34 fof(f162,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,e_3,X0)|product(e_3,X0,e_3)|~sQ2_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f46,f32])).
% 0.02/0.34 fof(f167,plain,(
% 0.02/0.34 ![X0]: (~product(e_1,e_2,X0)|product(e_3,X0,e_2)|~sQ17_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f111,f32])).
% 0.02/0.34 fof(f171,plain,(
% 0.02/0.34 ![X0]: (~product(e_1,e_2,X0)|product(e_2,X0,e_2)|~sQ16_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f108,f32])).
% 0.02/0.34 fof(f175,plain,(
% 0.02/0.34 ![X0]: (~product(e_1,e_2,X0)|product(e_1,X0,e_2)|~sQ15_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f105,f32])).
% 0.02/0.34 fof(f179,plain,(
% 0.02/0.34 ![X0]: (~product(e_2,e_2,X0)|product(e_3,X0,e_2)|~sQ14_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f101,f32])).
% 0.02/0.34 fof(f180,plain,(
% 0.02/0.34 product(e_3,e_3,e_2)|~sQ14_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f179,f101])).
% 0.02/0.34 fof(f182,plain,(
% 0.02/0.34 ![X0]: (~product(X0,e_3,e_2)|equalish(e_3,X0)|~sQ14_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f180,f30])).
% 0.02/0.34 fof(f183,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,X0,e_2)|equalish(e_3,X0)|~sQ14_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f180,f28])).
% 0.02/0.34 fof(f184,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,e_3,X0)|equalish(e_2,X0)|~sQ14_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f180,f26])).
% 0.02/0.34 fof(f188,plain,(
% 0.02/0.34 equalish(e_3,e_2)|~sQ14_spl|~sQ4_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f183,f53])).
% 0.02/0.34 fof(f189,plain,(
% 0.02/0.34 equalish(e_3,e_1)|~sQ14_spl|~sQ7_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f183,f63])).
% 0.02/0.34 fof(f190,plain,(
% 0.02/0.34 $false|~sQ14_spl|~sQ4_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f188,f23])).
% 0.02/0.34 fof(f191,plain,(
% 0.02/0.34 ~sQ14_spl|~sQ4_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f190])).
% 0.02/0.34 fof(f201,plain,(
% 0.02/0.34 ![X0]: (~product(e_2,e_2,X0)|product(e_1,X0,e_2)|~sQ12_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f95,f32])).
% 0.02/0.34 fof(f202,plain,(
% 0.02/0.34 product(e_1,e_1,e_2)|~sQ12_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f201,f95])).
% 0.02/0.34 fof(f204,plain,(
% 0.02/0.34 ![X0]: (~product(X0,e_1,e_2)|equalish(e_1,X0)|~sQ12_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f202,f30])).
% 0.02/0.34 fof(f207,plain,(
% 0.02/0.34 ![X0]: (~product(e_1,e_1,X0)|product(e_2,X0,e_1)|~sQ12_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f202,f32])).
% 0.02/0.34 fof(f216,plain,(
% 0.02/0.34 equalish(e_1,e_2)|~sQ12_spl|~sQ16_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f204,f108])).
% 0.02/0.34 fof(f218,plain,(
% 0.02/0.34 $false|~sQ12_spl|~sQ16_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f216,f18])).
% 0.02/0.34 fof(f219,plain,(
% 0.02/0.34 ~sQ12_spl|~sQ16_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f218])).
% 0.02/0.34 fof(f220,plain,(
% 0.02/0.34 product(e_1,e_3,e_3)|~sQ11_spl|~sQ3_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f91,f158])).
% 0.02/0.34 fof(f221,plain,(
% 0.02/0.34 product(e_3,e_3,e_3)|~sQ11_spl|~sQ5_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f91,f150])).
% 0.02/0.34 fof(f231,plain,(
% 0.02/0.34 ![X0]: (~product(X0,e_3,e_3)|equalish(e_1,X0)|~sQ11_spl|~sQ3_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f220,f30])).
% 0.02/0.34 fof(f241,plain,(
% 0.02/0.34 equalish(e_1,e_2)|~sQ3_spl|~sQ11_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f231,f91])).
% 0.02/0.34 fof(f243,plain,(
% 0.02/0.34 $false|~sQ3_spl|~sQ11_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f241,f18])).
% 0.02/0.34 fof(f244,plain,(
% 0.02/0.34 ~sQ3_spl|~sQ11_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f243])).
% 0.02/0.34 fof(f249,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,e_2,X0)|product(e_2,X0,e_2)|~sQ10_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f88,f32])).
% 0.02/0.34 fof(f251,plain,(
% 0.02/0.34 product(e_3,e_1,e_3)|~sQ9_spl|~sQ5_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f85,f150])).
% 0.02/0.34 fof(f255,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,e_2,X0)|product(e_1,X0,e_2)|~sQ9_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f85,f32])).
% 0.02/0.34 fof(f265,plain,(
% 0.02/0.34 product(e_2,e_2,e_3)|~sQ4_spl|~sQ10_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f154,f88])).
% 0.02/0.34 fof(f266,plain,(
% 0.02/0.34 sQ14_spl|~sQ4_spl|~sQ10_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f265,f100,f52,f87])).
% 0.02/0.34 fof(f270,plain,(
% 0.02/0.34 ![X0]: (~product(e_1,e_1,X0)|product(e_3,X0,e_1)|~sQ26_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f144,f32])).
% 0.02/0.34 fof(f271,plain,(
% 0.02/0.34 product(e_3,e_3,e_1)|~sQ26_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f270,f144])).
% 0.02/0.34 fof(f273,plain,(
% 0.02/0.34 ![X0]: (~product(X0,e_3,e_1)|equalish(e_3,X0)|~sQ26_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f271,f30])).
% 0.02/0.34 fof(f274,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,X0,e_1)|equalish(e_3,X0)|~sQ26_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f271,f28])).
% 0.02/0.34 fof(f276,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,e_3,X0)|product(e_1,X0,e_3)|~sQ26_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f271,f32])).
% 0.02/0.34 fof(f279,plain,(
% 0.02/0.34 equalish(e_3,e_1)|~sQ26_spl|~sQ6_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f274,f60])).
% 0.02/0.34 fof(f280,plain,(
% 0.02/0.34 $false|~sQ26_spl|~sQ6_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f279,f22])).
% 0.02/0.34 fof(f281,plain,(
% 0.02/0.34 ~sQ26_spl|~sQ6_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f280])).
% 0.02/0.34 fof(f285,plain,(
% 0.02/0.34 ![X0]: (~product(e_1,e_1,X0)|product(e_2,X0,e_1)|~sQ25_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f141,f32])).
% 0.02/0.34 fof(f286,plain,(
% 0.02/0.34 product(e_2,e_2,e_1)|~sQ25_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f285,f141])).
% 0.02/0.34 fof(f287,plain,(
% 0.02/0.34 sQ12_spl|~sQ25_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f286,f94,f140])).
% 0.02/0.34 fof(f295,plain,(
% 0.02/0.34 equalish(e_2,e_3)|~sQ14_spl|~sQ2_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f184,f46])).
% 0.02/0.34 fof(f296,plain,(
% 0.02/0.34 $false|~sQ14_spl|~sQ2_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f295,f21])).
% 0.02/0.34 fof(f297,plain,(
% 0.02/0.34 ~sQ14_spl|~sQ2_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f296])).
% 0.02/0.34 fof(f304,plain,(
% 0.02/0.34 product(e_2,e_2,e_1)|~sQ12_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f207,f202])).
% 0.02/0.34 fof(f308,plain,(
% 0.02/0.34 ![X0]: (~product(e_2,X0,e_1)|equalish(e_2,X0)|~sQ12_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f304,f28])).
% 0.02/0.34 fof(f331,plain,(
% 0.02/0.34 ![X0]: (~product(e_2,e_1,X0)|product(e_3,X0,e_1)|~sQ23_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f134,f32])).
% 0.02/0.34 fof(f332,plain,(
% 0.02/0.34 product(e_3,e_2,e_2)|~sQ22_spl|~sQ17_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f131,f167])).
% 0.02/0.34 fof(f337,plain,(
% 0.02/0.34 sQ4_spl|~sQ22_spl|~sQ17_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f332,f52,f130,f110])).
% 0.02/0.34 fof(f342,plain,(
% 0.02/0.34 product(e_3,e_3,e_3)|~sQ20_spl|~sQ8_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f124,f72])).
% 0.02/0.34 fof(f346,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,e_1,X0)|product(e_3,X0,e_1)|~sQ20_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f124,f32])).
% 0.02/0.34 fof(f347,plain,(
% 0.02/0.34 sQ2_spl|~sQ20_spl|~sQ8_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f342,f45,f123,f65])).
% 0.02/0.34 fof(f348,plain,(
% 0.02/0.34 product(e_3,e_2,e_3)|~sQ19_spl|~sQ8_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f121,f72])).
% 0.02/0.34 fof(f349,plain,(
% 0.02/0.34 equalish(e_3,e_1)|~sQ19_spl|~sQ14_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f121,f182])).
% 0.02/0.34 fof(f354,plain,(
% 0.02/0.34 $false|~sQ19_spl|~sQ14_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f349,f22])).
% 0.02/0.34 fof(f355,plain,(
% 0.02/0.34 ~sQ19_spl|~sQ14_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f354])).
% 0.02/0.34 fof(f360,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,e_1,X0)|product(e_1,X0,e_1)|~sQ18_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f118,f32])).
% 0.02/0.34 fof(f361,plain,(
% 0.02/0.34 product(e_1,e_1,e_3)|~sQ9_spl|~sQ3_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f85,f158])).
% 0.02/0.34 fof(f366,plain,(
% 0.02/0.34 sQ26_spl|~sQ9_spl|~sQ3_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f361,f143,f84,f49])).
% 0.02/0.34 fof(f377,plain,(
% 0.02/0.34 product(e_2,e_1,e_2)|~sQ16_spl|~sQ21_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f171,f128])).
% 0.02/0.34 fof(f378,plain,(
% 0.02/0.34 product(e_2,e_3,e_2)|~sQ16_spl|~sQ23_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f171,f134])).
% 0.02/0.34 fof(f381,plain,(
% 0.02/0.34 product(e_3,e_1,e_1)|~sQ26_spl|~sQ24_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f270,f138])).
% 0.02/0.34 fof(f382,plain,(
% 0.02/0.34 sQ6_spl|~sQ26_spl|~sQ24_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f381,f59,f143,f137])).
% 0.02/0.34 fof(f386,plain,(
% 0.02/0.34 ![X0]: (~product(e_2,X0,e_2)|equalish(e_1,X0)|~sQ16_spl|~sQ21_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f377,f28])).
% 0.02/0.34 fof(f423,plain,(
% 0.02/0.34 equalish(e_1,e_3)|~sQ21_spl|~sQ16_spl|~sQ23_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f386,f378])).
% 0.02/0.34 fof(f425,plain,(
% 0.02/0.34 $false|~sQ21_spl|~sQ16_spl|~sQ23_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f423,f19])).
% 0.02/0.34 fof(f426,plain,(
% 0.02/0.34 ~sQ21_spl|~sQ16_spl|~sQ23_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f425])).
% 0.02/0.34 fof(f427,plain,(
% 0.02/0.34 product(e_1,e_1,e_2)|~sQ15_spl|~sQ21_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f175,f128])).
% 0.02/0.34 fof(f428,plain,(
% 0.02/0.34 sQ25_spl|~sQ15_spl|~sQ21_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f427,f140,f104,f127])).
% 0.02/0.34 fof(f430,plain,(
% 0.02/0.34 product(e_1,e_1,e_3)|~sQ26_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f276,f271])).
% 0.02/0.34 fof(f442,plain,(
% 0.02/0.34 ![X0]: (~product(X0,e_1,e_3)|equalish(e_1,X0)|~sQ26_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f430,f30])).
% 0.02/0.34 fof(f448,plain,(
% 0.02/0.34 equalish(e_3,e_1)|~sQ26_spl|~sQ18_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f273,f118])).
% 0.02/0.34 fof(f451,plain,(
% 0.02/0.34 $false|~sQ26_spl|~sQ18_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f448,f22])).
% 0.02/0.34 fof(f452,plain,(
% 0.02/0.34 ~sQ26_spl|~sQ18_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f451])).
% 0.02/0.34 fof(f494,plain,(
% 0.02/0.34 equalish(e_3,e_2)|~sQ3_spl|~sQ26_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f50,f274])).
% 0.02/0.34 fof(f502,plain,(
% 0.02/0.34 $false|~sQ3_spl|~sQ26_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f494,f23])).
% 0.02/0.34 fof(f503,plain,(
% 0.02/0.34 ~sQ3_spl|~sQ26_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f502])).
% 0.02/0.34 fof(f506,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,X0,e_3)|equalish(e_2,X0)|~sQ19_spl|~sQ8_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f348,f28])).
% 0.02/0.34 fof(f540,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,e_3,X0)|product(e_2,X0,e_3)|~sQ1_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f43,f32])).
% 0.02/0.34 fof(f551,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,e_3,X0)|product(e_1,X0,e_3)|~sQ0_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f40,f32])).
% 0.02/0.34 fof(f563,plain,(
% 0.02/0.34 product(e_1,e_1,e_3)|~sQ0_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f551,f40])).
% 0.02/0.34 fof(f564,plain,(
% 0.02/0.34 sQ26_spl|~sQ0_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f563,f143,f39])).
% 0.02/0.34 fof(f565,plain,(
% 0.02/0.34 product(e_3,e_2,e_1)|~sQ26_spl|~sQ12_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f270,f202])).
% 0.02/0.34 fof(f566,plain,(
% 0.02/0.34 sQ3_spl|~sQ26_spl|~sQ12_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f565,f49,f143,f94])).
% 0.02/0.34 fof(f567,plain,(
% 0.02/0.34 product(e_1,e_3,e_1)|~sQ8_spl|~sQ18_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f66,f360])).
% 0.02/0.34 fof(f574,plain,(
% 0.02/0.34 ![X0]: (~product(e_1,X0,e_1)|equalish(e_3,X0)|~sQ8_spl|~sQ18_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f567,f28])).
% 0.02/0.34 fof(f581,plain,(
% 0.02/0.34 equalish(e_2,e_3)|~sQ9_spl|~sQ12_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f85,f308])).
% 0.02/0.34 fof(f587,plain,(
% 0.02/0.34 $false|~sQ9_spl|~sQ12_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f581,f21])).
% 0.02/0.34 fof(f588,plain,(
% 0.02/0.34 ~sQ9_spl|~sQ12_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f587])).
% 0.02/0.34 fof(f589,plain,(
% 0.02/0.34 product(e_3,e_3,e_1)|~sQ20_spl|~sQ8_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f346,f66])).
% 0.02/0.34 fof(f595,plain,(
% 0.02/0.34 product(e_3,e_1,e_3)|~sQ26_spl|~sQ2_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f271,f162])).
% 0.02/0.34 fof(f602,plain,(
% 0.02/0.34 equalish(e_3,e_2)|~sQ26_spl|~sQ9_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f273,f85])).
% 0.02/0.34 fof(f603,plain,(
% 0.02/0.34 $false|~sQ26_spl|~sQ9_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f602,f23])).
% 0.02/0.34 fof(f604,plain,(
% 0.02/0.34 ~sQ26_spl|~sQ9_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f603])).
% 0.02/0.34 fof(f611,plain,(
% 0.02/0.34 product(e_2,e_1,e_2)|~sQ3_spl|~sQ10_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f50,f249])).
% 0.02/0.34 fof(f616,plain,(
% 0.02/0.34 sQ16_spl|~sQ3_spl|~sQ10_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f611,f107,f49,f87])).
% 0.02/0.34 fof(f622,plain,(
% 0.02/0.34 product(e_3,e_1,e_2)|~sQ12_spl|~sQ14_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f304,f179])).
% 0.02/0.34 fof(f628,plain,(
% 0.02/0.34 sQ7_spl|~sQ12_spl|~sQ14_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f622,f62,f94,f100])).
% 0.02/0.34 fof(f629,plain,(
% 0.02/0.34 $false|~sQ14_spl|~sQ7_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f189,f22])).
% 0.02/0.34 fof(f630,plain,(
% 0.02/0.34 ~sQ14_spl|~sQ7_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f629])).
% 0.02/0.34 fof(f663,plain,(
% 0.02/0.34 product(e_3,e_1,e_2)|~sQ21_spl|~sQ17_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f128,f167])).
% 0.02/0.34 fof(f669,plain,(
% 0.02/0.34 sQ7_spl|~sQ21_spl|~sQ17_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f663,f62,f127,f110])).
% 0.02/0.34 fof(f695,plain,(
% 0.02/0.34 equalish(e_1,e_3)|~sQ10_spl|~sQ16_spl|~sQ21_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f88,f386])).
% 0.02/0.34 fof(f700,plain,(
% 0.02/0.34 $false|~sQ10_spl|~sQ16_spl|~sQ21_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f695,f19])).
% 0.02/0.34 fof(f701,plain,(
% 0.02/0.34 ~sQ10_spl|~sQ16_spl|~sQ21_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f700])).
% 0.02/0.34 fof(f717,plain,(
% 0.02/0.34 product(e_2,e_2,e_3)|~sQ19_spl|~sQ7_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f121,f76])).
% 0.02/0.34 fof(f722,plain,(
% 0.02/0.34 sQ14_spl|~sQ19_spl|~sQ7_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f717,f100,f120,f62])).
% 0.02/0.34 fof(f723,plain,(
% 0.02/0.34 product(e_3,e_2,e_1)|~sQ7_spl|~sQ20_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f63,f346])).
% 0.02/0.34 fof(f728,plain,(
% 0.02/0.34 sQ3_spl|~sQ7_spl|~sQ20_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f723,f49,f62,f123])).
% 0.02/0.34 fof(f731,plain,(
% 0.02/0.34 equalish(e_1,e_3)|~sQ2_spl|~sQ26_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f595,f442])).
% 0.02/0.34 fof(f736,plain,(
% 0.02/0.34 $false|~sQ2_spl|~sQ26_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f731,f19])).
% 0.02/0.34 fof(f737,plain,(
% 0.02/0.34 ~sQ2_spl|~sQ26_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f736])).
% 0.02/0.34 fof(f815,plain,(
% 0.02/0.34 product(e_3,e_3,e_1)|~sQ23_spl|~sQ17_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f331,f111])).
% 0.02/0.34 fof(f816,plain,(
% 0.02/0.34 sQ0_spl|~sQ23_spl|~sQ17_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f815,f39,f133,f110])).
% 0.02/0.34 fof(f820,plain,(
% 0.02/0.34 product(e_1,e_2,e_3)|~sQ10_spl|~sQ3_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f88,f158])).
% 0.02/0.34 fof(f826,plain,(
% 0.02/0.34 product(e_1,e_3,e_2)|~sQ10_spl|~sQ3_spl|~sQ15_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f820,f175])).
% 0.02/0.34 fof(f827,plain,(
% 0.02/0.34 ![X0]: (~product(X0,e_2,e_3)|equalish(e_1,X0)|~sQ10_spl|~sQ3_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f820,f30])).
% 0.02/0.34 fof(f831,plain,(
% 0.02/0.34 sQ19_spl|~sQ10_spl|~sQ3_spl|~sQ15_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f826,f120,f87,f49,f104])).
% 0.02/0.34 fof(f832,plain,(
% 0.02/0.34 product(e_3,e_2,e_3)|~sQ5_spl|~sQ10_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f150,f88])).
% 0.02/0.34 fof(f835,plain,(
% 0.02/0.34 ![X0]: (~product(e_3,X0,e_3)|equalish(e_2,X0)|~sQ5_spl|~sQ10_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f832,f28])).
% 0.02/0.34 fof(f840,plain,(
% 0.02/0.34 equalish(e_2,e_3)|~sQ5_spl|~sQ10_spl|~sQ2_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f835,f46])).
% 0.02/0.34 fof(f841,plain,(
% 0.02/0.34 equalish(e_2,e_1)|~sQ5_spl|~sQ10_spl|~sQ8_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f835,f66])).
% 0.02/0.34 fof(f842,plain,(
% 0.02/0.34 $false|~sQ5_spl|~sQ10_spl|~sQ2_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f840,f21])).
% 0.02/0.34 fof(f843,plain,(
% 0.02/0.34 ~sQ5_spl|~sQ10_spl|~sQ2_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f842])).
% 0.02/0.34 fof(f876,plain,(
% 0.02/0.34 equalish(e_3,e_1)|~sQ24_spl|~sQ8_spl|~sQ18_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f138,f574])).
% 0.02/0.34 fof(f881,plain,(
% 0.02/0.34 $false|~sQ24_spl|~sQ8_spl|~sQ18_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f876,f22])).
% 0.02/0.34 fof(f882,plain,(
% 0.02/0.34 ~sQ24_spl|~sQ8_spl|~sQ18_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f881])).
% 0.02/0.34 fof(f938,plain,(
% 0.02/0.34 equalish(e_2,e_1)|~sQ19_spl|~sQ8_spl|~sQ9_spl|~sQ5_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f506,f251])).
% 0.02/0.34 fof(f941,plain,(
% 0.02/0.34 $false|~sQ19_spl|~sQ8_spl|~sQ9_spl|~sQ5_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f938,f20])).
% 0.02/0.34 fof(f942,plain,(
% 0.02/0.34 ~sQ19_spl|~sQ8_spl|~sQ9_spl|~sQ5_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f941])).
% 0.02/0.34 fof(f945,plain,(
% 0.02/0.34 sQ5_spl|~sQ19_spl|~sQ8_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f348,f55,f120,f65])).
% 0.02/0.34 fof(f964,plain,(
% 0.02/0.34 product(e_1,e_2,e_2)|~sQ4_spl|~sQ9_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f53,f255])).
% 0.02/0.34 fof(f970,plain,(
% 0.02/0.34 ![X0]: (~product(X0,e_2,e_2)|equalish(e_1,X0)|~sQ4_spl|~sQ9_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f964,f30])).
% 0.02/0.34 fof(f974,plain,(
% 0.02/0.34 equalish(e_1,e_2)|~sQ4_spl|~sQ9_spl|~sQ13_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f970,f98])).
% 0.02/0.34 fof(f977,plain,(
% 0.02/0.34 $false|~sQ4_spl|~sQ9_spl|~sQ13_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f974,f18])).
% 0.02/0.34 fof(f978,plain,(
% 0.02/0.34 ~sQ4_spl|~sQ9_spl|~sQ13_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f977])).
% 0.02/0.34 fof(f979,plain,(
% 0.02/0.34 product(e_2,e_3,e_2)|~sQ10_spl|~sQ3_spl|~sQ16_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f820,f171])).
% 0.02/0.34 fof(f989,plain,(
% 0.02/0.34 ![X0]: (~product(e_2,X0,e_2)|equalish(e_3,X0)|~sQ10_spl|~sQ3_spl|~sQ16_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f979,f28])).
% 0.02/0.34 fof(f994,plain,(
% 0.02/0.34 equalish(e_3,e_2)|~sQ10_spl|~sQ3_spl|~sQ16_spl|~sQ13_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f989,f98])).
% 0.02/0.34 fof(f995,plain,(
% 0.02/0.34 $false|~sQ10_spl|~sQ3_spl|~sQ16_spl|~sQ13_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f994,f23])).
% 0.02/0.34 fof(f996,plain,(
% 0.02/0.34 ~sQ10_spl|~sQ3_spl|~sQ16_spl|~sQ13_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f995])).
% 0.02/0.34 fof(f1027,plain,(
% 0.02/0.34 equalish(e_3,e_2)|~sQ2_spl|~sQ11_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f159,f91])).
% 0.02/0.34 fof(f1029,plain,(
% 0.02/0.34 $false|~sQ2_spl|~sQ11_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f1027,f23])).
% 0.02/0.34 fof(f1030,plain,(
% 0.02/0.34 ~sQ2_spl|~sQ11_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f1029])).
% 0.02/0.34 fof(f1031,plain,(
% 0.02/0.34 $false|~sQ5_spl|~sQ10_spl|~sQ8_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f841,f20])).
% 0.02/0.34 fof(f1032,plain,(
% 0.02/0.34 ~sQ5_spl|~sQ10_spl|~sQ8_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f1031])).
% 0.02/0.34 fof(f1042,plain,(
% 0.02/0.34 product(e_2,e_3,e_2)|~sQ5_spl|~sQ10_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f249,f832])).
% 0.02/0.34 fof(f1049,plain,(
% 0.02/0.34 sQ2_spl|~sQ11_spl|~sQ5_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f221,f45,f90,f55])).
% 0.02/0.34 fof(f1065,plain,(
% 0.02/0.34 ![X0]: (~product(X0,e_3,e_2)|equalish(e_2,X0)|~sQ5_spl|~sQ10_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f1042,f30])).
% 0.02/0.34 fof(f1066,plain,(
% 0.02/0.34 ![X0]: (~product(e_2,X0,e_2)|equalish(e_3,X0)|~sQ5_spl|~sQ10_spl)),
% 0.02/0.34 inference(resolution,[status(thm)],[f1042,f28])).
% 0.02/0.34 fof(f1071,plain,(
% 0.02/0.34 equalish(e_3,e_2)|~sQ5_spl|~sQ10_spl|~sQ13_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f1066,f98])).
% 0.02/0.34 fof(f1072,plain,(
% 0.02/0.34 $false|~sQ5_spl|~sQ10_spl|~sQ13_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f1071,f23])).
% 0.02/0.34 fof(f1073,plain,(
% 0.02/0.34 ~sQ5_spl|~sQ10_spl|~sQ13_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f1072])).
% 0.02/0.34 fof(f1074,plain,(
% 0.02/0.34 product(e_2,e_2,e_3)|~sQ14_spl|~sQ1_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f180,f540])).
% 0.02/0.34 fof(f1075,plain,(
% 0.02/0.34 equalish(e_2,e_3)|~sQ14_spl|~sQ5_spl|~sQ10_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f180,f1065])).
% 0.02/0.34 fof(f1080,plain,(
% 0.02/0.34 $false|~sQ14_spl|~sQ5_spl|~sQ10_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f1075,f21])).
% 0.02/0.34 fof(f1081,plain,(
% 0.02/0.34 ~sQ14_spl|~sQ5_spl|~sQ10_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f1080])).
% 0.02/0.34 fof(f1087,plain,(
% 0.02/0.34 product(e_2,e_2,e_3)|~sQ1_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f43,f540])).
% 0.02/0.34 fof(f1092,plain,(
% 0.02/0.34 sQ14_spl|~sQ1_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f1087,f100,f42])).
% 0.02/0.34 fof(f1094,plain,(
% 0.02/0.34 sQ8_spl|~sQ9_spl|~sQ5_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f251,f65,f84,f55])).
% 0.02/0.34 fof(f1097,plain,(
% 0.02/0.34 sQ0_spl|~sQ20_spl|~sQ8_spl),
% 0.02/0.34 inference(split_clause,[status(thm)],[f589,f39,f123,f65])).
% 0.02/0.34 fof(f1117,plain,(
% 0.02/0.34 equalish(e_1,e_2)|~sQ14_spl|~sQ1_spl|~sQ10_spl|~sQ3_spl),
% 0.02/0.34 inference(resolution,[status(thm)],[f1074,f827])).
% 0.02/0.34 fof(f1122,plain,(
% 0.02/0.34 $false|~sQ14_spl|~sQ1_spl|~sQ10_spl|~sQ3_spl),
% 0.02/0.34 inference(forward_subsumption_resolution,[status(thm)],[f1117,f18])).
% 0.02/0.34 fof(f1123,plain,(
% 0.02/0.34 ~sQ14_spl|~sQ1_spl|~sQ10_spl|~sQ3_spl),
% 0.02/0.34 inference(contradiction_clause,[status(thm)],[f1122])).
% 0.02/0.34 fof(f1124,plain,(
% 0.02/0.34 $false),
% 0.02/0.34 inference(sat_refutation,[status(thm)],[f48,f58,f68,f93,f103,f113,f126,f136,f146,f191,f219,f244,f266,f281,f287,f297,f337,f347,f355,f366,f382,f426,f428,f452,f503,f564,f566,f588,f604,f616,f628,f630,f669,f701,f722,f728,f737,f816,f831,f843,f882,f942,f945,f978,f996,f1030,f1032,f1049,f1073,f1081,f1092,f1094,f1097,f1123])).
% 0.02/0.34 % SZS output end CNFRefutation for theBenchmark.p
% 0.02/0.35 % Elapsed time: 0.049325 seconds
% 0.02/0.35 % CPU time: 0.270811 seconds
% 0.02/0.35 % Total memory used: 19.054 MB
% 0.02/0.35 % Net memory used: 18.717 MB
%------------------------------------------------------------------------------