%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP124-9.004 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:35:48 PM UTC 2026
% Result : Unsatisfiable 0.17s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP124-9.004 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n004.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 20 19:59:04 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 0.17/0.48 % Refutation found
% 0.17/0.48 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.17/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.48 fof(f3,axiom,(
% 0.17/0.48 group_element(e_1) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f4,axiom,(
% 0.17/0.48 group_element(e_2) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f5,axiom,(
% 0.17/0.48 group_element(e_3) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f6,axiom,(
% 0.17/0.48 group_element(e_4) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f7,axiom,(
% 0.17/0.48 ~ equalish(e_1,e_2) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f8,axiom,(
% 0.17/0.48 ~ equalish(e_1,e_3) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f9,axiom,(
% 0.17/0.48 ~ equalish(e_1,e_4) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f10,axiom,(
% 0.17/0.48 ~ equalish(e_2,e_1) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f11,axiom,(
% 0.17/0.48 ~ equalish(e_2,e_3) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f12,axiom,(
% 0.17/0.48 ~ equalish(e_2,e_4) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f13,axiom,(
% 0.17/0.48 ~ equalish(e_3,e_1) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f14,axiom,(
% 0.17/0.48 ~ equalish(e_3,e_2) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f15,axiom,(
% 0.17/0.48 ~ equalish(e_3,e_4) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f16,axiom,(
% 0.17/0.48 ~ equalish(e_4,e_1) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f17,axiom,(
% 0.17/0.48 ~ equalish(e_4,e_2) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f18,axiom,(
% 0.17/0.48 ~ equalish(e_4,e_3) ),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f19,axiom,(
% 0.17/0.48 (![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.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f20,axiom,(
% 0.17/0.48 (![X,Y,W,Z]: (( ~ product1(X,Y,W)| ~ product1(X,Y,Z)| equalish(W,Z) ) ))),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f21,axiom,(
% 0.17/0.48 (![X,W,Y,Z]: (( ~ product1(X,W,Y)| ~ product1(X,Z,Y)| equalish(W,Z) ) ))),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f22,axiom,(
% 0.17/0.48 (![W,Y,X,Z]: (( ~ product1(W,Y,X)| ~ product1(Z,Y,X)| equalish(W,Z) ) ))),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f23,axiom,(
% 0.17/0.48 (![X]: (product1(X,X,X) ))),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f25,axiom,(
% 0.17/0.48 (![X,Y,W,Z]: (( ~ product2(X,Y,W)| ~ product2(X,Y,Z)| equalish(W,Z) ) ))),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f28,axiom,(
% 0.17/0.48 (![X]: (product2(X,X,X) ))),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f29,negated_conjecture,(
% 0.17/0.48 (![X,Y,Z1,Z2]: (( ~ product1(X,Y,Z1)| ~ product1(Z1,X,Z2)| product2(Z2,Y,X) ) ))),
% 0.17/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.48 fof(f32,plain,(
% 0.17/0.48 group_element(e_1)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f3])).
% 0.17/0.48 fof(f33,plain,(
% 0.17/0.48 group_element(e_2)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f4])).
% 0.17/0.48 fof(f34,plain,(
% 0.17/0.48 group_element(e_3)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.48 fof(f35,plain,(
% 0.17/0.48 group_element(e_4)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.48 fof(f36,plain,(
% 0.17/0.48 ~equalish(e_1,e_2)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f7])).
% 0.17/0.48 fof(f37,plain,(
% 0.17/0.48 ~equalish(e_1,e_3)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f8])).
% 0.17/0.48 fof(f38,plain,(
% 0.17/0.48 ~equalish(e_1,e_4)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f9])).
% 0.17/0.48 fof(f39,plain,(
% 0.17/0.48 ~equalish(e_2,e_1)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f10])).
% 0.17/0.48 fof(f40,plain,(
% 0.17/0.48 ~equalish(e_2,e_3)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f11])).
% 0.17/0.48 fof(f41,plain,(
% 0.17/0.48 ~equalish(e_2,e_4)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.48 fof(f42,plain,(
% 0.17/0.48 ~equalish(e_3,e_1)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f13])).
% 0.17/0.48 fof(f43,plain,(
% 0.17/0.48 ~equalish(e_3,e_2)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f14])).
% 0.17/0.48 fof(f44,plain,(
% 0.17/0.48 ~equalish(e_3,e_4)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f15])).
% 0.17/0.48 fof(f45,plain,(
% 0.17/0.48 ~equalish(e_4,e_1)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f16])).
% 0.17/0.48 fof(f46,plain,(
% 0.17/0.48 ~equalish(e_4,e_2)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f17])).
% 0.17/0.48 fof(f47,plain,(
% 0.17/0.48 ~equalish(e_4,e_3)),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f18])).
% 0.17/0.48 fof(f48,plain,(
% 0.17/0.48 ![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.17/0.48 inference(cnf_transformation,[status(thm)],[f19])).
% 0.17/0.48 fof(f49,plain,(
% 0.17/0.48 ![W,Z]: ((![X,Y]: (~product1(X,Y,W)|~product1(X,Y,Z)))|equalish(W,Z))),
% 0.17/0.48 inference(miniscoping,[status(thm)],[f20])).
% 0.17/0.48 fof(f50,plain,(
% 0.17/0.48 ![X0,X1,X2,X3]: (~product1(X0,X1,X2)|~product1(X0,X1,X3)|equalish(X2,X3))),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f49])).
% 0.17/0.48 fof(f51,plain,(
% 0.17/0.48 ![W,Z]: ((![X,Y]: (~product1(X,W,Y)|~product1(X,Z,Y)))|equalish(W,Z))),
% 0.17/0.48 inference(miniscoping,[status(thm)],[f21])).
% 0.17/0.48 fof(f52,plain,(
% 0.17/0.48 ![X0,X1,X2,X3]: (~product1(X0,X1,X2)|~product1(X0,X3,X2)|equalish(X1,X3))),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f51])).
% 0.17/0.48 fof(f53,plain,(
% 0.17/0.48 ![W,Z]: ((![Y,X]: (~product1(W,Y,X)|~product1(Z,Y,X)))|equalish(W,Z))),
% 0.17/0.48 inference(miniscoping,[status(thm)],[f22])).
% 0.17/0.48 fof(f54,plain,(
% 0.17/0.48 ![X0,X1,X2,X3]: (~product1(X0,X1,X2)|~product1(X3,X1,X2)|equalish(X0,X3))),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f53])).
% 0.17/0.48 fof(f55,plain,(
% 0.17/0.48 ![X0]: (product1(X0,X0,X0))),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f23])).
% 0.17/0.48 fof(f57,plain,(
% 0.17/0.48 ![W,Z]: ((![X,Y]: (~product2(X,Y,W)|~product2(X,Y,Z)))|equalish(W,Z))),
% 0.17/0.48 inference(miniscoping,[status(thm)],[f25])).
% 0.17/0.48 fof(f58,plain,(
% 0.17/0.48 ![X0,X1,X2,X3]: (~product2(X0,X1,X2)|~product2(X0,X1,X3)|equalish(X2,X3))),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f57])).
% 0.17/0.48 fof(f63,plain,(
% 0.17/0.48 ![X0]: (product2(X0,X0,X0))),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f28])).
% 0.17/0.48 fof(f64,plain,(
% 0.17/0.48 ![X,Y,Z2]: ((![Z1]: (~product1(X,Y,Z1)|~product1(Z1,X,Z2)))|product2(Z2,Y,X))),
% 0.17/0.48 inference(miniscoping,[status(thm)],[f29])).
% 0.17/0.48 fof(f65,plain,(
% 0.17/0.48 ![X0,X1,X2,X3]: (~product1(X0,X1,X2)|~product1(X2,X0,X3)|product2(X3,X1,X0))),
% 0.17/0.48 inference(cnf_transformation,[status(thm)],[f64])).
% 0.17/0.48 fof(f68,plain,(
% 0.17/0.48 ![X0,X1]: (~product1(X0,X0,X1)|equalish(X1,X0))),
% 0.17/0.48 inference(resolution,[status(thm)],[f50,f55])).
% 0.17/0.48 fof(f70,plain,(
% 0.17/0.48 ![X0,X1]: (~product1(X0,X1,X0)|equalish(X1,X0))),
% 0.17/0.48 inference(resolution,[status(thm)],[f52,f55])).
% 0.17/0.48 fof(f71,plain,(
% 0.17/0.48 ![X0,X1]: (~product1(X0,X1,X1)|equalish(X0,X1))),
% 0.17/0.48 inference(resolution,[status(thm)],[f54,f55])).
% 0.17/0.48 fof(f80,plain,(
% 0.17/0.48 ![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.17/0.48 inference(resolution,[status(thm)],[f48,f35])).
% 0.17/0.48 fof(f81,plain,(
% 0.17/0.48 ![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.17/0.48 inference(resolution,[status(thm)],[f48,f34])).
% 0.17/0.48 fof(f82,plain,(
% 0.17/0.48 ![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.17/0.48 inference(resolution,[status(thm)],[f48,f33])).
% 0.17/0.48 fof(f83,plain,(
% 0.17/0.48 ![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.17/0.48 inference(resolution,[status(thm)],[f48,f32])).
% 0.17/0.48 fof(f345,plain,(
% 0.17/0.48 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.17/0.48 inference(resolution,[status(thm)],[f80,f34])).
% 0.17/0.48 fof(f347,plain,(
% 0.17/0.48 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.17/0.48 inference(resolution,[status(thm)],[f80,f32])).
% 0.17/0.48 fof(f361,definition,(
% 0.17/0.48 sQ68_spl <=> (product1(e_4,e_3,e_1))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f362,plain,(
% 0.17/0.48 product1(e_4,e_3,e_1)|~sQ68_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f361])).
% 0.17/0.48 fof(f364,definition,(
% 0.17/0.48 sQ69_spl <=> (product1(e_4,e_3,e_2))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f365,plain,(
% 0.17/0.48 product1(e_4,e_3,e_2)|~sQ69_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f364])).
% 0.17/0.48 fof(f367,definition,(
% 0.17/0.48 sQ70_spl <=> (product1(e_4,e_3,e_3))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f368,plain,(
% 0.17/0.48 product1(e_4,e_3,e_3)|~sQ70_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f367])).
% 0.17/0.48 fof(f370,definition,(
% 0.17/0.48 sQ71_spl <=> (product1(e_4,e_3,e_4))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f371,plain,(
% 0.17/0.48 product1(e_4,e_3,e_4)|~sQ71_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f370])).
% 0.17/0.48 fof(f373,plain,(
% 0.17/0.48 sQ68_spl|sQ69_spl|sQ70_spl|sQ71_spl),
% 0.17/0.48 inference(split_clause,[status(thm)],[f345,f361,f364,f367,f370])).
% 0.17/0.48 fof(f377,definition,(
% 0.17/0.48 sQ73_spl <=> (product1(e_4,e_2,e_2))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f378,plain,(
% 0.17/0.48 product1(e_4,e_2,e_2)|~sQ73_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f377])).
% 0.17/0.48 fof(f383,definition,(
% 0.17/0.48 sQ75_spl <=> (product1(e_4,e_2,e_4))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f384,plain,(
% 0.17/0.48 product1(e_4,e_2,e_4)|~sQ75_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f383])).
% 0.17/0.48 fof(f387,definition,(
% 0.17/0.48 sQ76_spl <=> (product1(e_4,e_1,e_1))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f388,plain,(
% 0.17/0.48 product1(e_4,e_1,e_1)|~sQ76_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f387])).
% 0.17/0.48 fof(f390,definition,(
% 0.17/0.48 sQ77_spl <=> (product1(e_4,e_1,e_2))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f391,plain,(
% 0.17/0.48 product1(e_4,e_1,e_2)|~sQ77_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f390])).
% 0.17/0.48 fof(f393,definition,(
% 0.17/0.48 sQ78_spl <=> (product1(e_4,e_1,e_3))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f394,plain,(
% 0.17/0.48 product1(e_4,e_1,e_3)|~sQ78_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f393])).
% 0.17/0.48 fof(f396,definition,(
% 0.17/0.48 sQ79_spl <=> (product1(e_4,e_1,e_4))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f397,plain,(
% 0.17/0.48 product1(e_4,e_1,e_4)|~sQ79_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f396])).
% 0.17/0.48 fof(f399,plain,(
% 0.17/0.48 sQ76_spl|sQ77_spl|sQ78_spl|sQ79_spl),
% 0.17/0.48 inference(split_clause,[status(thm)],[f347,f387,f390,f393,f396])).
% 0.17/0.48 fof(f403,plain,(
% 0.17/0.48 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.17/0.48 inference(resolution,[status(thm)],[f81,f32])).
% 0.17/0.48 fof(f410,definition,(
% 0.17/0.48 sQ82_spl <=> (product1(e_3,e_4,e_3))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f411,plain,(
% 0.17/0.48 product1(e_3,e_4,e_3)|~sQ82_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f410])).
% 0.17/0.48 fof(f413,definition,(
% 0.17/0.48 sQ83_spl <=> (product1(e_3,e_4,e_4))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f414,plain,(
% 0.17/0.48 product1(e_3,e_4,e_4)|~sQ83_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f413])).
% 0.17/0.48 fof(f426,definition,(
% 0.17/0.48 sQ87_spl <=> (product1(e_3,e_3,e_4))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f427,plain,(
% 0.17/0.48 product1(e_3,e_3,e_4)|~sQ87_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f426])).
% 0.17/0.48 fof(f443,definition,(
% 0.17/0.48 sQ92_spl <=> (product1(e_3,e_1,e_1))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f444,plain,(
% 0.17/0.48 product1(e_3,e_1,e_1)|~sQ92_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f443])).
% 0.17/0.48 fof(f446,definition,(
% 0.17/0.48 sQ93_spl <=> (product1(e_3,e_1,e_2))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f447,plain,(
% 0.17/0.48 product1(e_3,e_1,e_2)|~sQ93_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f446])).
% 0.17/0.48 fof(f449,definition,(
% 0.17/0.48 sQ94_spl <=> (product1(e_3,e_1,e_3))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f450,plain,(
% 0.17/0.48 product1(e_3,e_1,e_3)|~sQ94_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f449])).
% 0.17/0.48 fof(f452,definition,(
% 0.17/0.48 sQ95_spl <=> (product1(e_3,e_1,e_4))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f453,plain,(
% 0.17/0.48 product1(e_3,e_1,e_4)|~sQ95_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f452])).
% 0.17/0.48 fof(f455,plain,(
% 0.17/0.48 sQ92_spl|sQ93_spl|sQ94_spl|sQ95_spl),
% 0.17/0.48 inference(split_clause,[status(thm)],[f403,f443,f446,f449,f452])).
% 0.17/0.48 fof(f457,plain,(
% 0.17/0.48 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.17/0.48 inference(resolution,[status(thm)],[f82,f34])).
% 0.17/0.48 fof(f459,plain,(
% 0.17/0.48 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.17/0.48 inference(resolution,[status(thm)],[f82,f32])).
% 0.17/0.48 fof(f463,definition,(
% 0.17/0.48 sQ97_spl <=> (product1(e_2,e_4,e_2))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f464,plain,(
% 0.17/0.48 product1(e_2,e_4,e_2)|~sQ97_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f463])).
% 0.17/0.48 fof(f473,definition,(
% 0.17/0.48 sQ100_spl <=> (product1(e_2,e_3,e_1))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f474,plain,(
% 0.17/0.48 product1(e_2,e_3,e_1)|~sQ100_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f473])).
% 0.17/0.48 fof(f476,definition,(
% 0.17/0.48 sQ101_spl <=> (product1(e_2,e_3,e_2))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f477,plain,(
% 0.17/0.48 product1(e_2,e_3,e_2)|~sQ101_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f476])).
% 0.17/0.48 fof(f479,definition,(
% 0.17/0.48 sQ102_spl <=> (product1(e_2,e_3,e_3))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f480,plain,(
% 0.17/0.48 product1(e_2,e_3,e_3)|~sQ102_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f479])).
% 0.17/0.48 fof(f482,definition,(
% 0.17/0.48 sQ103_spl <=> (product1(e_2,e_3,e_4))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f483,plain,(
% 0.17/0.48 product1(e_2,e_3,e_4)|~sQ103_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f482])).
% 0.17/0.48 fof(f485,plain,(
% 0.17/0.48 sQ100_spl|sQ101_spl|sQ102_spl|sQ103_spl),
% 0.17/0.48 inference(split_clause,[status(thm)],[f457,f473,f476,f479,f482])).
% 0.17/0.48 fof(f486,definition,(
% 0.17/0.48 sQ104_spl <=> (product1(e_2,e_2,e_1))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f487,plain,(
% 0.17/0.48 product1(e_2,e_2,e_1)|~sQ104_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f486])).
% 0.17/0.48 fof(f499,definition,(
% 0.17/0.48 sQ108_spl <=> (product1(e_2,e_1,e_1))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f500,plain,(
% 0.17/0.48 product1(e_2,e_1,e_1)|~sQ108_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f499])).
% 0.17/0.48 fof(f502,definition,(
% 0.17/0.48 sQ109_spl <=> (product1(e_2,e_1,e_2))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f503,plain,(
% 0.17/0.48 product1(e_2,e_1,e_2)|~sQ109_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f502])).
% 0.17/0.48 fof(f505,definition,(
% 0.17/0.48 sQ110_spl <=> (product1(e_2,e_1,e_3))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f506,plain,(
% 0.17/0.48 product1(e_2,e_1,e_3)|~sQ110_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f505])).
% 0.17/0.48 fof(f508,definition,(
% 0.17/0.48 sQ111_spl <=> (product1(e_2,e_1,e_4))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f509,plain,(
% 0.17/0.48 product1(e_2,e_1,e_4)|~sQ111_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f508])).
% 0.17/0.48 fof(f511,plain,(
% 0.17/0.48 sQ108_spl|sQ109_spl|sQ110_spl|sQ111_spl),
% 0.17/0.48 inference(split_clause,[status(thm)],[f459,f499,f502,f505,f508])).
% 0.17/0.48 fof(f513,plain,(
% 0.17/0.48 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.17/0.48 inference(resolution,[status(thm)],[f83,f34])).
% 0.17/0.48 fof(f529,definition,(
% 0.17/0.48 sQ116_spl <=> (product1(e_1,e_3,e_1))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f530,plain,(
% 0.17/0.48 product1(e_1,e_3,e_1)|~sQ116_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f529])).
% 0.17/0.48 fof(f532,definition,(
% 0.17/0.48 sQ117_spl <=> (product1(e_1,e_3,e_2))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f533,plain,(
% 0.17/0.48 product1(e_1,e_3,e_2)|~sQ117_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f532])).
% 0.17/0.48 fof(f535,definition,(
% 0.17/0.48 sQ118_spl <=> (product1(e_1,e_3,e_3))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f536,plain,(
% 0.17/0.48 product1(e_1,e_3,e_3)|~sQ118_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f535])).
% 0.17/0.48 fof(f538,definition,(
% 0.17/0.48 sQ119_spl <=> (product1(e_1,e_3,e_4))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f539,plain,(
% 0.17/0.48 product1(e_1,e_3,e_4)|~sQ119_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f538])).
% 0.17/0.48 fof(f541,plain,(
% 0.17/0.48 sQ116_spl|sQ117_spl|sQ118_spl|sQ119_spl),
% 0.17/0.48 inference(split_clause,[status(thm)],[f513,f529,f532,f535,f538])).
% 0.17/0.48 fof(f545,definition,(
% 0.17/0.48 sQ121_spl <=> (product1(e_1,e_2,e_2))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f546,plain,(
% 0.17/0.48 product1(e_1,e_2,e_2)|~sQ121_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f545])).
% 0.17/0.48 fof(f558,definition,(
% 0.17/0.48 sQ125_spl <=> (product1(e_1,e_1,e_2))),
% 0.17/0.48 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.17/0.48 fof(f559,plain,(
% 0.17/0.48 product1(e_1,e_1,e_2)|~sQ125_spl),
% 0.17/0.48 inference(component_clause,[status(thm)],[f558])).
% 0.17/0.48 fof(f794,plain,(
% 0.17/0.48 ![X0,X1]: (~product2(X0,X0,X1)|equalish(X1,X0))),
% 0.17/0.48 inference(resolution,[status(thm)],[f58,f63])).
% 0.17/0.48 fof(f800,plain,(
% 0.17/0.48 equalish(e_1,e_4)|~sQ79_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f397,f70])).
% 0.17/0.48 fof(f806,plain,(
% 0.17/0.48 $false|~sQ79_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f800,f38])).
% 0.17/0.48 fof(f807,plain,(
% 0.17/0.48 ~sQ79_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f806])).
% 0.17/0.48 fof(f808,plain,(
% 0.17/0.48 ![X0]: (~product1(X0,e_1,e_3)|equalish(X0,e_4)|~sQ78_spl)),
% 0.17/0.48 inference(resolution,[status(thm)],[f394,f54])).
% 0.17/0.48 fof(f811,plain,(
% 0.17/0.48 ![X0]: (~product1(e_1,X0,e_4)|product2(e_3,X0,e_1)|~sQ78_spl)),
% 0.17/0.48 inference(resolution,[status(thm)],[f394,f65])).
% 0.17/0.48 fof(f816,plain,(
% 0.17/0.48 ![X0]: (~product1(X0,e_1,e_2)|equalish(X0,e_4)|~sQ77_spl)),
% 0.17/0.48 inference(resolution,[status(thm)],[f391,f54])).
% 0.17/0.48 fof(f817,plain,(
% 0.17/0.48 ![X0]: (~product1(e_4,X0,e_2)|equalish(X0,e_1)|~sQ77_spl)),
% 0.17/0.48 inference(resolution,[status(thm)],[f391,f52])).
% 0.17/0.48 fof(f822,plain,(
% 0.17/0.48 equalish(e_4,e_1)|~sQ76_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f388,f71])).
% 0.17/0.48 fof(f827,plain,(
% 0.17/0.48 $false|~sQ76_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f822,f45])).
% 0.17/0.48 fof(f828,plain,(
% 0.17/0.48 ~sQ76_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f827])).
% 0.17/0.48 fof(f829,plain,(
% 0.17/0.48 equalish(e_2,e_4)|~sQ75_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f384,f70])).
% 0.17/0.48 fof(f835,plain,(
% 0.17/0.48 $false|~sQ75_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f829,f41])).
% 0.17/0.48 fof(f836,plain,(
% 0.17/0.48 ~sQ75_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f835])).
% 0.17/0.48 fof(f846,plain,(
% 0.17/0.48 equalish(e_4,e_2)|~sQ73_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f378,f71])).
% 0.17/0.48 fof(f860,plain,(
% 0.17/0.48 equalish(e_3,e_4)|~sQ71_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f371,f70])).
% 0.17/0.48 fof(f866,plain,(
% 0.17/0.48 $false|~sQ71_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f860,f44])).
% 0.17/0.48 fof(f867,plain,(
% 0.17/0.48 ~sQ71_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f866])).
% 0.17/0.48 fof(f868,plain,(
% 0.17/0.48 equalish(e_4,e_3)|~sQ70_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f368,f71])).
% 0.17/0.48 fof(f873,plain,(
% 0.17/0.48 $false|~sQ70_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f868,f47])).
% 0.17/0.48 fof(f874,plain,(
% 0.17/0.48 ~sQ70_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f873])).
% 0.17/0.48 fof(f875,plain,(
% 0.17/0.48 equalish(e_3,e_1)|~sQ69_spl|~sQ77_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f365,f817])).
% 0.17/0.48 fof(f876,plain,(
% 0.17/0.48 ![X0]: (~product1(X0,e_3,e_2)|equalish(X0,e_4)|~sQ69_spl)),
% 0.17/0.48 inference(resolution,[status(thm)],[f365,f54])).
% 0.17/0.48 fof(f880,plain,(
% 0.17/0.48 $false|~sQ69_spl|~sQ77_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f875,f42])).
% 0.17/0.48 fof(f881,plain,(
% 0.17/0.48 ~sQ69_spl|~sQ77_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f880])).
% 0.17/0.48 fof(f883,plain,(
% 0.17/0.48 ![X0]: (~product1(X0,e_3,e_1)|equalish(X0,e_4)|~sQ68_spl)),
% 0.17/0.48 inference(resolution,[status(thm)],[f362,f54])).
% 0.17/0.48 fof(f886,plain,(
% 0.17/0.48 ![X0]: (~product1(e_3,X0,e_4)|product2(e_1,X0,e_3)|~sQ68_spl)),
% 0.17/0.48 inference(resolution,[status(thm)],[f362,f65])).
% 0.17/0.48 fof(f894,plain,(
% 0.17/0.48 product2(e_1,e_1,e_3)|~sQ95_spl|~sQ68_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f453,f886])).
% 0.17/0.48 fof(f901,plain,(
% 0.17/0.48 equalish(e_3,e_1)|~sQ95_spl|~sQ68_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f894,f794])).
% 0.17/0.48 fof(f903,plain,(
% 0.17/0.48 $false|~sQ95_spl|~sQ68_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f901,f42])).
% 0.17/0.48 fof(f904,plain,(
% 0.17/0.48 ~sQ95_spl|~sQ68_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f903])).
% 0.17/0.48 fof(f905,plain,(
% 0.17/0.48 equalish(e_1,e_3)|~sQ94_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f450,f70])).
% 0.17/0.48 fof(f911,plain,(
% 0.17/0.48 $false|~sQ94_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f905,f37])).
% 0.17/0.48 fof(f912,plain,(
% 0.17/0.48 ~sQ94_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f911])).
% 0.17/0.48 fof(f913,plain,(
% 0.17/0.48 equalish(e_3,e_4)|~sQ93_spl|~sQ77_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f447,f816])).
% 0.17/0.48 fof(f918,plain,(
% 0.17/0.48 $false|~sQ93_spl|~sQ77_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f913,f44])).
% 0.17/0.48 fof(f919,plain,(
% 0.17/0.48 ~sQ93_spl|~sQ77_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f918])).
% 0.17/0.48 fof(f920,plain,(
% 0.17/0.48 equalish(e_3,e_1)|~sQ92_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f444,f71])).
% 0.17/0.48 fof(f925,plain,(
% 0.17/0.48 $false|~sQ92_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f920,f42])).
% 0.17/0.48 fof(f926,plain,(
% 0.17/0.48 ~sQ92_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f925])).
% 0.17/0.48 fof(f927,plain,(
% 0.17/0.48 $false|~sQ73_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f846,f46])).
% 0.17/0.48 fof(f928,plain,(
% 0.17/0.48 ~sQ73_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f927])).
% 0.17/0.48 fof(f971,plain,(
% 0.17/0.48 equalish(e_4,e_3)|~sQ87_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f427,f68])).
% 0.17/0.48 fof(f974,plain,(
% 0.17/0.48 $false|~sQ87_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f971,f47])).
% 0.17/0.48 fof(f975,plain,(
% 0.17/0.48 ~sQ87_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f974])).
% 0.17/0.48 fof(f994,plain,(
% 0.17/0.48 equalish(e_3,e_4)|~sQ83_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f414,f71])).
% 0.17/0.48 fof(f999,plain,(
% 0.17/0.48 $false|~sQ83_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f994,f44])).
% 0.17/0.48 fof(f1000,plain,(
% 0.17/0.48 ~sQ83_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f999])).
% 0.17/0.48 fof(f1001,plain,(
% 0.17/0.48 equalish(e_4,e_3)|~sQ82_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f411,f70])).
% 0.17/0.48 fof(f1007,plain,(
% 0.17/0.48 $false|~sQ82_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1001,f47])).
% 0.17/0.48 fof(f1008,plain,(
% 0.17/0.48 ~sQ82_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1007])).
% 0.17/0.48 fof(f1027,plain,(
% 0.17/0.48 ![X0]: (~product1(e_2,X0,e_4)|equalish(X0,e_1)|~sQ111_spl)),
% 0.17/0.48 inference(resolution,[status(thm)],[f509,f52])).
% 0.17/0.48 fof(f1030,plain,(
% 0.17/0.48 equalish(e_2,e_4)|~sQ110_spl|~sQ78_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f506,f808])).
% 0.17/0.48 fof(f1035,plain,(
% 0.17/0.48 $false|~sQ110_spl|~sQ78_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1030,f41])).
% 0.17/0.48 fof(f1036,plain,(
% 0.17/0.48 ~sQ110_spl|~sQ78_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1035])).
% 0.17/0.48 fof(f1038,plain,(
% 0.17/0.48 equalish(e_1,e_2)|~sQ109_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f503,f70])).
% 0.17/0.48 fof(f1046,plain,(
% 0.17/0.48 equalish(e_2,e_1)|~sQ108_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f500,f71])).
% 0.17/0.48 fof(f1051,plain,(
% 0.17/0.48 $false|~sQ108_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1046,f39])).
% 0.17/0.48 fof(f1052,plain,(
% 0.17/0.48 ~sQ108_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1051])).
% 0.17/0.48 fof(f1081,plain,(
% 0.17/0.48 $false|~sQ109_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1038,f36])).
% 0.17/0.48 fof(f1082,plain,(
% 0.17/0.48 ~sQ109_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1081])).
% 0.17/0.48 fof(f1106,plain,(
% 0.17/0.48 equalish(e_1,e_2)|~sQ104_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f487,f68])).
% 0.17/0.48 fof(f1109,plain,(
% 0.17/0.48 $false|~sQ104_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1106,f36])).
% 0.17/0.48 fof(f1110,plain,(
% 0.17/0.48 ~sQ104_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1109])).
% 0.17/0.48 fof(f1111,plain,(
% 0.17/0.48 equalish(e_3,e_1)|~sQ103_spl|~sQ111_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f483,f1027])).
% 0.17/0.48 fof(f1117,plain,(
% 0.17/0.48 $false|~sQ103_spl|~sQ111_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1111,f42])).
% 0.17/0.48 fof(f1118,plain,(
% 0.17/0.48 ~sQ103_spl|~sQ111_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1117])).
% 0.17/0.48 fof(f1120,plain,(
% 0.17/0.48 equalish(e_2,e_3)|~sQ102_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f480,f71])).
% 0.17/0.48 fof(f1125,plain,(
% 0.17/0.48 $false|~sQ102_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1120,f40])).
% 0.17/0.48 fof(f1126,plain,(
% 0.17/0.48 ~sQ102_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1125])).
% 0.17/0.48 fof(f1127,plain,(
% 0.17/0.48 equalish(e_3,e_2)|~sQ101_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f477,f70])).
% 0.17/0.48 fof(f1133,plain,(
% 0.17/0.48 $false|~sQ101_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1127,f43])).
% 0.17/0.48 fof(f1134,plain,(
% 0.17/0.48 ~sQ101_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1133])).
% 0.17/0.48 fof(f1135,plain,(
% 0.17/0.48 equalish(e_2,e_4)|~sQ100_spl|~sQ68_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f474,f883])).
% 0.17/0.48 fof(f1136,plain,(
% 0.17/0.48 ![X0]: (~product1(X0,e_3,e_1)|equalish(X0,e_2)|~sQ100_spl)),
% 0.17/0.48 inference(resolution,[status(thm)],[f474,f54])).
% 0.17/0.48 fof(f1140,plain,(
% 0.17/0.48 $false|~sQ100_spl|~sQ68_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1135,f41])).
% 0.17/0.48 fof(f1141,plain,(
% 0.17/0.48 ~sQ100_spl|~sQ68_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1140])).
% 0.17/0.48 fof(f1165,plain,(
% 0.17/0.48 equalish(e_4,e_2)|~sQ97_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f464,f70])).
% 0.17/0.48 fof(f1171,plain,(
% 0.17/0.48 $false|~sQ97_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1165,f46])).
% 0.17/0.48 fof(f1172,plain,(
% 0.17/0.48 ~sQ97_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1171])).
% 0.17/0.48 fof(f1201,plain,(
% 0.17/0.48 equalish(e_2,e_1)|~sQ125_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f559,f68])).
% 0.17/0.48 fof(f1204,plain,(
% 0.17/0.48 $false|~sQ125_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1201,f39])).
% 0.17/0.48 fof(f1205,plain,(
% 0.17/0.48 ~sQ125_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1204])).
% 0.17/0.48 fof(f1219,plain,(
% 0.17/0.48 equalish(e_1,e_2)|~sQ121_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f546,f71])).
% 0.17/0.48 fof(f1224,plain,(
% 0.17/0.48 $false|~sQ121_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1219,f36])).
% 0.17/0.48 fof(f1225,plain,(
% 0.17/0.48 ~sQ121_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1224])).
% 0.17/0.48 fof(f1235,plain,(
% 0.17/0.48 product2(e_3,e_3,e_1)|~sQ119_spl|~sQ78_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f539,f811])).
% 0.17/0.48 fof(f1240,plain,(
% 0.17/0.48 equalish(e_1,e_3)|~sQ118_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f536,f71])).
% 0.17/0.48 fof(f1245,plain,(
% 0.17/0.48 $false|~sQ118_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1240,f37])).
% 0.17/0.48 fof(f1246,plain,(
% 0.17/0.48 ~sQ118_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1245])).
% 0.17/0.48 fof(f1252,plain,(
% 0.17/0.48 equalish(e_1,e_3)|~sQ119_spl|~sQ78_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f1235,f794])).
% 0.17/0.48 fof(f1254,plain,(
% 0.17/0.48 $false|~sQ119_spl|~sQ78_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1252,f37])).
% 0.17/0.48 fof(f1255,plain,(
% 0.17/0.48 ~sQ119_spl|~sQ78_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1254])).
% 0.17/0.48 fof(f1270,plain,(
% 0.17/0.48 equalish(e_1,e_4)|~sQ117_spl|~sQ69_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f533,f876])).
% 0.17/0.48 fof(f1275,plain,(
% 0.17/0.48 $false|~sQ117_spl|~sQ69_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1270,f38])).
% 0.17/0.48 fof(f1276,plain,(
% 0.17/0.48 ~sQ117_spl|~sQ69_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1275])).
% 0.17/0.48 fof(f1277,plain,(
% 0.17/0.48 equalish(e_1,e_2)|~sQ116_spl|~sQ100_spl),
% 0.17/0.48 inference(resolution,[status(thm)],[f530,f1136])).
% 0.17/0.48 fof(f1284,plain,(
% 0.17/0.48 $false|~sQ116_spl|~sQ100_spl),
% 0.17/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1277,f36])).
% 0.17/0.48 fof(f1285,plain,(
% 0.17/0.48 ~sQ116_spl|~sQ100_spl),
% 0.17/0.48 inference(contradiction_clause,[status(thm)],[f1284])).
% 0.17/0.48 fof(f1286,plain,(
% 0.17/0.48 $false),
% 0.17/0.48 inference(sat_refutation,[status(thm)],[f373,f399,f455,f485,f511,f541,f807,f828,f836,f867,f874,f881,f904,f912,f919,f926,f928,f975,f1000,f1008,f1036,f1052,f1082,f1110,f1118,f1126,f1134,f1141,f1172,f1205,f1225,f1246,f1255,f1276,f1285])).
% 0.17/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/0.52 % Elapsed time: 0.067405 seconds
% 0.23/0.52 % CPU time: 0.197814 seconds
% 0.23/0.52 % Total memory used: 19.039 MB
% 0.23/0.52 % Net memory used: 18.779 MB
%------------------------------------------------------------------------------