%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP125-3.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -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:32:43 PM UTC 2026
% Result : Unsatisfiable 69.75s 9.26s
% Output : CNFRefutation 69.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 234
% Syntax : Number of formulae : 1439 ( 169 unt; 182 def)
% Number of atoms : 3871 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 4617 (2185 ~;2250 |; 0 &)
% ( 182 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 189 ( 188 usr; 183 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 270 ( 270 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
next(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
next(e_4,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
greater(e_1,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
greater(e_2,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
greater(e_3,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
greater(e_4,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
greater(e_4,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
greater(e_5,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
greater(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
greater(e_5,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
greater(e_5,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
greater(e_5,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X] :
( cycle(X,e_4)
| cycle(X,e_3)
| cycle(X,e_2)
| cycle(X,e_1)
| cycle(X,e_0)
| ~ group_element(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
cycle(e_5,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X,Z1,Y,W,Z2] :
( ~ greater(Z1,Z2)
| ~ greater(Y,X)
| ~ next(Y,W)
| ~ cycle(W,Z2)
| ~ cycle(Y,e_0)
| ~ cycle(X,Z1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X,Y] :
( ~ greater(Y,X)
| ~ product(X,e_1,Y)
| ~ cycle(X,e_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [X,Y,Z,X1] :
( equalish(Z,X1)
| ~ next(X,X1)
| ~ greater(Y,e_0)
| ~ product(X,e_1,Z)
| ~ cycle(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
group_element(e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
~ equalish(e_1,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
~ equalish(e_2,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
~ equalish(e_3,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
~ equalish(e_4,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
~ equalish(e_5,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
~ equalish(e_5,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
~ equalish(e_5,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
~ equalish(e_5,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [X,Y] :
( product(X,Y,e_5)
| product(X,Y,e_4)
| product(X,Y,e_3)
| product(X,Y,e_2)
| product(X,Y,e_1)
| ~ group_element(Y)
| ~ group_element(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [X,Y,W,Z] :
( equalish(W,Z)
| ~ product(X,Y,Z)
| ~ product(X,Y,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [X,W,Y,Z] :
( equalish(W,Z)
| ~ product(X,Z,Y)
| ~ product(X,W,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [W,Y,X,Z] :
( equalish(W,Z)
| ~ product(Z,Y,X)
| ~ product(W,Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [X] : product(X,X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,negated_conjecture,
! [X,Y,Z1,Z2] :
( product(Z1,Z2,X)
| ~ product(Y,X,Z2)
| ~ product(X,Y,Z1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,plain,
next(e_1,e_2),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f61,plain,
next(e_2,e_3),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f62,plain,
next(e_3,e_4),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f63,plain,
next(e_4,e_5),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f64,plain,
greater(e_1,e_0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f65,plain,
greater(e_2,e_0),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f66,plain,
greater(e_3,e_0),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f67,plain,
greater(e_4,e_0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f71,plain,
greater(e_4,e_1),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f72,plain,
greater(e_5,e_1),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f73,plain,
greater(e_3,e_2),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f74,plain,
greater(e_4,e_2),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f75,plain,
greater(e_5,e_2),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f76,plain,
greater(e_4,e_3),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f77,plain,
greater(e_5,e_3),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f78,plain,
greater(e_5,e_4),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f81,plain,
! [X0] :
( cycle(X0,e_3)
| cycle(X0,e_2)
| cycle(X0,e_0)
| cycle(X0,e_1)
| cycle(X0,e_4)
| ~ group_element(X0) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f82,plain,
cycle(e_5,e_0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f85,plain,
! [Z1,Z2] :
( ~ greater(Z1,Z2)
| ! [X,Y] :
( ~ greater(Y,X)
| ! [W] :
( ~ next(Y,W)
| ~ cycle(W,Z2)
| ~ cycle(Y,e_0)
| ~ cycle(X,Z1) ) ) ),
inference(miniscoping,[status(thm)],[f25]) ).
fof(f86,plain,
! [X0,X1,X2,X3,X4] :
( ~ cycle(X3,X4)
| ~ cycle(X2,e_0)
| ~ next(X2,X0)
| ~ greater(X4,X1)
| ~ greater(X2,X3)
| ~ cycle(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f87,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ product(X0,e_1,X1)
| ~ cycle(X0,e_0) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f88,plain,
! [Z,X1] :
( equalish(Z,X1)
| ! [X] :
( ~ next(X,X1)
| ! [Y] :
( ~ greater(Y,e_0)
| ~ product(X,e_1,Z)
| ~ cycle(X,Y) ) ) ),
inference(miniscoping,[status(thm)],[f27]) ).
fof(f89,plain,
! [X0,X1,X2,X3] :
( ~ next(X2,X1)
| ~ greater(X3,e_0)
| ~ product(X2,e_1,X0)
| ~ cycle(X2,X3)
| equalish(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
group_element(e_1),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f91,plain,
group_element(e_2),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f92,plain,
group_element(e_3),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f93,plain,
group_element(e_4),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f94,plain,
group_element(e_5),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f95,plain,
~ equalish(e_1,e_2),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f96,plain,
~ equalish(e_1,e_3),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f97,plain,
~ equalish(e_1,e_4),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f98,plain,
~ equalish(e_1,e_5),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f99,plain,
~ equalish(e_2,e_1),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f100,plain,
~ equalish(e_2,e_3),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f101,plain,
~ equalish(e_2,e_4),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f102,plain,
~ equalish(e_2,e_5),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f103,plain,
~ equalish(e_3,e_1),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f104,plain,
~ equalish(e_3,e_2),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f105,plain,
~ equalish(e_3,e_4),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f106,plain,
~ equalish(e_3,e_5),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f107,plain,
~ equalish(e_4,e_1),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f108,plain,
~ equalish(e_4,e_2),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f109,plain,
~ equalish(e_4,e_3),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f110,plain,
~ equalish(e_4,e_5),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f111,plain,
~ equalish(e_5,e_1),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f112,plain,
~ equalish(e_5,e_2),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f113,plain,
~ equalish(e_5,e_3),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f114,plain,
~ equalish(e_5,e_4),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f115,plain,
! [X0,X1] :
( product(X0,X1,e_2)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_5)
| ~ group_element(X0)
| product(X0,X1,e_3)
| product(X0,X1,e_4) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f116,plain,
! [W,Z] :
( equalish(W,Z)
| ! [X,Y] :
( ~ product(X,Y,Z)
| ~ product(X,Y,W) ) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f117,plain,
! [X0,X1,X2,X3] :
( ~ product(X2,X3,X1)
| ~ product(X2,X3,X0)
| equalish(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f118,plain,
! [W,Z] :
( equalish(W,Z)
| ! [X,Y] :
( ~ product(X,Z,Y)
| ~ product(X,W,Y) ) ),
inference(miniscoping,[status(thm)],[f55]) ).
fof(f119,plain,
! [X0,X1,X2,X3] :
( ~ product(X2,X1,X3)
| ~ product(X2,X0,X3)
| equalish(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f120,plain,
! [W,Z] :
( equalish(W,Z)
| ! [Y,X] :
( ~ product(Z,Y,X)
| ~ product(W,Y,X) ) ),
inference(miniscoping,[status(thm)],[f56]) ).
fof(f121,plain,
! [X0,X1,X2,X3] :
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f122,plain,
! [X0] : product(X0,X0,X0),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f123,plain,
! [X,Z1,Z2] :
( product(Z1,Z2,X)
| ! [Y] :
( ~ product(Y,X,Z2)
| ~ product(X,Y,Z1) ) ),
inference(miniscoping,[status(thm)],[f58]) ).
fof(f124,plain,
! [X0,X1,X2,X3] :
( ~ product(X1,X0,X3)
| product(X2,X3,X0)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
! [X0] :
( product(e_1,X0,e_3)
| ~ group_element(X0)
| product(e_1,X0,e_5)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_4) ),
inference(resolution,[status(thm)],[f90,f115]) ).
fof(f126,plain,
( cycle(e_1,e_3)
| cycle(e_1,e_2)
| cycle(e_1,e_0)
| cycle(e_1,e_1)
| cycle(e_1,e_4) ),
inference(resolution,[status(thm)],[f90,f81]) ).
fof(f127,definition,
( sQ0_spl
<=> cycle(e_1,e_4) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f128,plain,
( ~ sQ0_spl
| cycle(e_1,e_4) ),
inference(component_clause,[status(thm)],[f127]) ).
fof(f130,definition,
( sQ1_spl
<=> cycle(e_1,e_1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f131,plain,
( ~ sQ1_spl
| cycle(e_1,e_1) ),
inference(component_clause,[status(thm)],[f130]) ).
fof(f133,definition,
( sQ2_spl
<=> cycle(e_1,e_0) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f134,plain,
( ~ sQ2_spl
| cycle(e_1,e_0) ),
inference(component_clause,[status(thm)],[f133]) ).
fof(f136,definition,
( sQ3_spl
<=> cycle(e_1,e_2) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f137,plain,
( ~ sQ3_spl
| cycle(e_1,e_2) ),
inference(component_clause,[status(thm)],[f136]) ).
fof(f139,definition,
( sQ4_spl
<=> cycle(e_1,e_3) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f140,plain,
( ~ sQ4_spl
| cycle(e_1,e_3) ),
inference(component_clause,[status(thm)],[f139]) ).
fof(f142,plain,
( sQ4_spl
| sQ3_spl
| sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f126,f127,f130,f133,f136,f139]) ).
fof(f143,plain,
( product(e_1,e_1,e_3)
| product(e_1,e_1,e_5)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_4) ),
inference(resolution,[status(thm)],[f125,f90]) ).
fof(f144,definition,
( sQ5_spl
<=> product(e_1,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f145,plain,
( ~ sQ5_spl
| product(e_1,e_1,e_4) ),
inference(component_clause,[status(thm)],[f144]) ).
fof(f147,definition,
( sQ6_spl
<=> product(e_1,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f148,plain,
( ~ sQ6_spl
| product(e_1,e_1,e_2) ),
inference(component_clause,[status(thm)],[f147]) ).
fof(f150,definition,
( sQ7_spl
<=> product(e_1,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f153,definition,
( sQ8_spl
<=> product(e_1,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f154,plain,
( ~ sQ8_spl
| product(e_1,e_1,e_5) ),
inference(component_clause,[status(thm)],[f153]) ).
fof(f156,definition,
( sQ9_spl
<=> product(e_1,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f157,plain,
( ~ sQ9_spl
| product(e_1,e_1,e_3) ),
inference(component_clause,[status(thm)],[f156]) ).
fof(f159,plain,
( sQ9_spl
| sQ8_spl
| sQ7_spl
| sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f143,f144,f147,f150,f153,f156]) ).
fof(f160,plain,
! [X0,X1] :
( equalish(X0,X1)
| ~ product(X0,X1,X0) ),
inference(resolution,[status(thm)],[f122,f119]) ).
fof(f161,plain,
! [X0,X1] :
( product(X0,X1,X0)
| ~ product(X0,X0,X1) ),
inference(resolution,[status(thm)],[f122,f124]) ).
fof(f163,plain,
! [X0,X1] :
( ~ product(X1,X0,X0)
| equalish(X0,X1) ),
inference(resolution,[status(thm)],[f121,f122]) ).
fof(f165,plain,
! [X0,X1] :
( ~ product(X0,X0,X1)
| equalish(X0,X1) ),
inference(resolution,[status(thm)],[f117,f122]) ).
fof(f168,plain,
( ~ greater(e_1,e_1)
| ~ cycle(e_1,e_0) ),
inference(resolution,[status(thm)],[f87,f122]) ).
fof(f169,definition,
( sQ10_spl
<=> greater(e_1,e_1) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f172,plain,
( ~ sQ10_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f168,f133,f169]) ).
fof(f173,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_4,e_5)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_4) ),
inference(resolution,[status(thm)],[f93,f125]) ).
fof(f174,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_5)
| product(e_4,X0,e_2)
| product(e_4,X0,e_4)
| product(e_4,X0,e_3) ),
inference(resolution,[status(thm)],[f93,f115]) ).
fof(f175,plain,
( cycle(e_4,e_3)
| cycle(e_4,e_2)
| cycle(e_4,e_0)
| cycle(e_4,e_1)
| cycle(e_4,e_4) ),
inference(resolution,[status(thm)],[f93,f81]) ).
fof(f176,definition,
( sQ11_spl
<=> cycle(e_4,e_4) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f177,plain,
( ~ sQ11_spl
| cycle(e_4,e_4) ),
inference(component_clause,[status(thm)],[f176]) ).
fof(f179,definition,
( sQ12_spl
<=> cycle(e_4,e_1) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f180,plain,
( ~ sQ12_spl
| cycle(e_4,e_1) ),
inference(component_clause,[status(thm)],[f179]) ).
fof(f182,definition,
( sQ13_spl
<=> cycle(e_4,e_0) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f183,plain,
( ~ sQ13_spl
| cycle(e_4,e_0) ),
inference(component_clause,[status(thm)],[f182]) ).
fof(f185,definition,
( sQ14_spl
<=> cycle(e_4,e_2) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f186,plain,
( ~ sQ14_spl
| cycle(e_4,e_2) ),
inference(component_clause,[status(thm)],[f185]) ).
fof(f188,definition,
( sQ15_spl
<=> cycle(e_4,e_3) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f189,plain,
( ~ sQ15_spl
| cycle(e_4,e_3) ),
inference(component_clause,[status(thm)],[f188]) ).
fof(f191,plain,
( sQ15_spl
| sQ14_spl
| sQ13_spl
| sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f175,f176,f179,f182,f185,f188]) ).
fof(f192,definition,
( sQ16_spl
<=> product(e_1,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f193,plain,
( ~ sQ16_spl
| product(e_1,e_4,e_4) ),
inference(component_clause,[status(thm)],[f192]) ).
fof(f195,definition,
( sQ17_spl
<=> product(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f196,plain,
( ~ sQ17_spl
| product(e_1,e_4,e_2) ),
inference(component_clause,[status(thm)],[f195]) ).
fof(f198,definition,
( sQ18_spl
<=> product(e_1,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f199,plain,
( ~ sQ18_spl
| product(e_1,e_4,e_1) ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f201,definition,
( sQ19_spl
<=> product(e_1,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f202,plain,
( ~ sQ19_spl
| product(e_1,e_4,e_5) ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f204,definition,
( sQ20_spl
<=> product(e_1,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f205,plain,
( ~ sQ20_spl
| product(e_1,e_4,e_3) ),
inference(component_clause,[status(thm)],[f204]) ).
fof(f207,plain,
( sQ20_spl
| sQ19_spl
| sQ18_spl
| sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f173,f192,f195,f198,f201,f204]) ).
fof(f208,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_5)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_4)
| product(e_4,e_4,e_3) ),
inference(resolution,[status(thm)],[f174,f93]) ).
fof(f209,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_5)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[f174,f90]) ).
fof(f210,definition,
( sQ21_spl
<=> product(e_4,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f211,plain,
( ~ sQ21_spl
| product(e_4,e_1,e_3) ),
inference(component_clause,[status(thm)],[f210]) ).
fof(f213,definition,
( sQ22_spl
<=> product(e_4,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f214,plain,
( ~ sQ22_spl
| product(e_4,e_1,e_4) ),
inference(component_clause,[status(thm)],[f213]) ).
fof(f216,definition,
( sQ23_spl
<=> product(e_4,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f217,plain,
( ~ sQ23_spl
| product(e_4,e_1,e_2) ),
inference(component_clause,[status(thm)],[f216]) ).
fof(f219,definition,
( sQ24_spl
<=> product(e_4,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f220,plain,
( ~ sQ24_spl
| product(e_4,e_1,e_5) ),
inference(component_clause,[status(thm)],[f219]) ).
fof(f221,plain,
( sQ24_spl
| ~ product(e_4,e_1,e_5) ),
inference(component_clause,[status(thm)],[f219]) ).
fof(f222,definition,
( sQ25_spl
<=> product(e_4,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f223,plain,
( ~ sQ25_spl
| product(e_4,e_1,e_1) ),
inference(component_clause,[status(thm)],[f222]) ).
fof(f225,plain,
( sQ25_spl
| sQ24_spl
| sQ23_spl
| sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f209,f210,f213,f216,f219,f222]) ).
fof(f226,definition,
( sQ26_spl
<=> product(e_4,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f227,plain,
( ~ sQ26_spl
| product(e_4,e_4,e_3) ),
inference(component_clause,[status(thm)],[f226]) ).
fof(f229,definition,
( sQ27_spl
<=> product(e_4,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f232,definition,
( sQ28_spl
<=> product(e_4,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f235,definition,
( sQ29_spl
<=> product(e_4,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f236,plain,
( ~ sQ29_spl
| product(e_4,e_4,e_5) ),
inference(component_clause,[status(thm)],[f235]) ).
fof(f238,definition,
( sQ30_spl
<=> product(e_4,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f239,plain,
( ~ sQ30_spl
| product(e_4,e_4,e_1) ),
inference(component_clause,[status(thm)],[f238]) ).
fof(f241,plain,
( sQ30_spl
| sQ29_spl
| sQ28_spl
| sQ27_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f208,f226,f229,f232,f235,f238]) ).
fof(f242,plain,
( product(e_4,e_5,e_1)
| product(e_4,e_5,e_5)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_3) ),
inference(resolution,[status(thm)],[f94,f174]) ).
fof(f243,plain,
( product(e_1,e_5,e_3)
| product(e_1,e_5,e_5)
| product(e_1,e_5,e_1)
| product(e_1,e_5,e_2)
| product(e_1,e_5,e_4) ),
inference(resolution,[status(thm)],[f94,f125]) ).
fof(f244,plain,
! [X0] :
( product(e_5,X0,e_1)
| product(e_5,X0,e_5)
| product(e_5,X0,e_4)
| product(e_5,X0,e_2)
| ~ group_element(X0)
| product(e_5,X0,e_3) ),
inference(resolution,[status(thm)],[f94,f115]) ).
fof(f246,definition,
( sQ31_spl
<=> product(e_1,e_5,e_4) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f247,plain,
( ~ sQ31_spl
| product(e_1,e_5,e_4) ),
inference(component_clause,[status(thm)],[f246]) ).
fof(f249,definition,
( sQ32_spl
<=> product(e_1,e_5,e_2) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f250,plain,
( ~ sQ32_spl
| product(e_1,e_5,e_2) ),
inference(component_clause,[status(thm)],[f249]) ).
fof(f252,definition,
( sQ33_spl
<=> product(e_1,e_5,e_1) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f253,plain,
( ~ sQ33_spl
| product(e_1,e_5,e_1) ),
inference(component_clause,[status(thm)],[f252]) ).
fof(f255,definition,
( sQ34_spl
<=> product(e_1,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f256,plain,
( ~ sQ34_spl
| product(e_1,e_5,e_5) ),
inference(component_clause,[status(thm)],[f255]) ).
fof(f258,definition,
( sQ35_spl
<=> product(e_1,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f259,plain,
( ~ sQ35_spl
| product(e_1,e_5,e_3) ),
inference(component_clause,[status(thm)],[f258]) ).
fof(f261,plain,
( sQ35_spl
| sQ34_spl
| sQ33_spl
| sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f243,f246,f249,f252,f255,f258]) ).
fof(f262,definition,
( sQ36_spl
<=> product(e_4,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f263,plain,
( ~ sQ36_spl
| product(e_4,e_5,e_3) ),
inference(component_clause,[status(thm)],[f262]) ).
fof(f265,definition,
( sQ37_spl
<=> product(e_4,e_5,e_4) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f266,plain,
( ~ sQ37_spl
| product(e_4,e_5,e_4) ),
inference(component_clause,[status(thm)],[f265]) ).
fof(f268,definition,
( sQ38_spl
<=> product(e_4,e_5,e_2) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f269,plain,
( ~ sQ38_spl
| product(e_4,e_5,e_2) ),
inference(component_clause,[status(thm)],[f268]) ).
fof(f271,definition,
( sQ39_spl
<=> product(e_4,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f272,plain,
( ~ sQ39_spl
| product(e_4,e_5,e_5) ),
inference(component_clause,[status(thm)],[f271]) ).
fof(f274,definition,
( sQ40_spl
<=> product(e_4,e_5,e_1) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f275,plain,
( ~ sQ40_spl
| product(e_4,e_5,e_1) ),
inference(component_clause,[status(thm)],[f274]) ).
fof(f277,plain,
( sQ40_spl
| sQ39_spl
| sQ38_spl
| sQ37_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f242,f262,f265,f268,f271,f274]) ).
fof(f284,definition,
( sQ43_spl
<=> cycle(e_5,e_0) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f286,plain,
( sQ43_spl
| ~ cycle(e_5,e_0) ),
inference(component_clause,[status(thm)],[f284]) ).
fof(f294,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_5)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_4)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[f91,f174]) ).
fof(f295,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_5)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[f91,f125]) ).
fof(f296,plain,
! [X0] :
( product(e_2,X0,e_5)
| product(e_2,X0,e_4)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| ~ group_element(X0) ),
inference(resolution,[status(thm)],[f91,f115]) ).
fof(f297,plain,
( cycle(e_2,e_3)
| cycle(e_2,e_2)
| cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_4) ),
inference(resolution,[status(thm)],[f91,f81]) ).
fof(f298,definition,
( sQ46_spl
<=> cycle(e_2,e_4) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f299,plain,
( ~ sQ46_spl
| cycle(e_2,e_4) ),
inference(component_clause,[status(thm)],[f298]) ).
fof(f301,definition,
( sQ47_spl
<=> cycle(e_2,e_1) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f302,plain,
( ~ sQ47_spl
| cycle(e_2,e_1) ),
inference(component_clause,[status(thm)],[f301]) ).
fof(f304,definition,
( sQ48_spl
<=> cycle(e_2,e_0) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f307,definition,
( sQ49_spl
<=> cycle(e_2,e_2) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f308,plain,
( ~ sQ49_spl
| cycle(e_2,e_2) ),
inference(component_clause,[status(thm)],[f307]) ).
fof(f310,definition,
( sQ50_spl
<=> cycle(e_2,e_3) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f311,plain,
( ~ sQ50_spl
| cycle(e_2,e_3) ),
inference(component_clause,[status(thm)],[f310]) ).
fof(f313,plain,
( sQ50_spl
| sQ49_spl
| sQ48_spl
| sQ47_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f297,f298,f301,f304,f307,f310]) ).
fof(f314,definition,
( sQ51_spl
<=> product(e_1,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f315,plain,
( ~ sQ51_spl
| product(e_1,e_2,e_4) ),
inference(component_clause,[status(thm)],[f314]) ).
fof(f317,definition,
( sQ52_spl
<=> product(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f318,plain,
( ~ sQ52_spl
| product(e_1,e_2,e_2) ),
inference(component_clause,[status(thm)],[f317]) ).
fof(f320,definition,
( sQ53_spl
<=> product(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f321,plain,
( ~ sQ53_spl
| product(e_1,e_2,e_1) ),
inference(component_clause,[status(thm)],[f320]) ).
fof(f323,definition,
( sQ54_spl
<=> product(e_1,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f324,plain,
( ~ sQ54_spl
| product(e_1,e_2,e_5) ),
inference(component_clause,[status(thm)],[f323]) ).
fof(f326,definition,
( sQ55_spl
<=> product(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f327,plain,
( ~ sQ55_spl
| product(e_1,e_2,e_3) ),
inference(component_clause,[status(thm)],[f326]) ).
fof(f329,plain,
( sQ55_spl
| sQ54_spl
| sQ53_spl
| sQ52_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f295,f314,f317,f320,f323,f326]) ).
fof(f330,definition,
( sQ56_spl
<=> product(e_4,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f331,plain,
( ~ sQ56_spl
| product(e_4,e_2,e_3) ),
inference(component_clause,[status(thm)],[f330]) ).
fof(f333,definition,
( sQ57_spl
<=> product(e_4,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( ~ sQ57_spl
| product(e_4,e_2,e_4) ),
inference(component_clause,[status(thm)],[f333]) ).
fof(f336,definition,
( sQ58_spl
<=> product(e_4,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f337,plain,
( ~ sQ58_spl
| product(e_4,e_2,e_2) ),
inference(component_clause,[status(thm)],[f336]) ).
fof(f339,definition,
( sQ59_spl
<=> product(e_4,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f340,plain,
( ~ sQ59_spl
| product(e_4,e_2,e_5) ),
inference(component_clause,[status(thm)],[f339]) ).
fof(f342,definition,
( sQ60_spl
<=> product(e_4,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f343,plain,
( ~ sQ60_spl
| product(e_4,e_2,e_1) ),
inference(component_clause,[status(thm)],[f342]) ).
fof(f345,plain,
( sQ60_spl
| sQ59_spl
| sQ58_spl
| sQ57_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f294,f330,f333,f336,f339,f342]) ).
fof(f346,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_5)
| product(e_5,e_2,e_4)
| product(e_5,e_2,e_2)
| product(e_5,e_2,e_3) ),
inference(resolution,[status(thm)],[f244,f91]) ).
fof(f347,plain,
( product(e_5,e_5,e_1)
| product(e_5,e_5,e_5)
| product(e_5,e_5,e_4)
| product(e_5,e_5,e_2)
| product(e_5,e_5,e_3) ),
inference(resolution,[status(thm)],[f244,f94]) ).
fof(f348,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_5)
| product(e_5,e_4,e_4)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3) ),
inference(resolution,[status(thm)],[f244,f93]) ).
fof(f349,plain,
( product(e_5,e_1,e_1)
| product(e_5,e_1,e_5)
| product(e_5,e_1,e_4)
| product(e_5,e_1,e_2)
| product(e_5,e_1,e_3) ),
inference(resolution,[status(thm)],[f244,f90]) ).
fof(f350,definition,
( sQ61_spl
<=> product(e_5,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f351,plain,
( ~ sQ61_spl
| product(e_5,e_4,e_3) ),
inference(component_clause,[status(thm)],[f350]) ).
fof(f353,definition,
( sQ62_spl
<=> product(e_5,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f354,plain,
( ~ sQ62_spl
| product(e_5,e_4,e_2) ),
inference(component_clause,[status(thm)],[f353]) ).
fof(f356,definition,
( sQ63_spl
<=> product(e_5,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f357,plain,
( ~ sQ63_spl
| product(e_5,e_4,e_4) ),
inference(component_clause,[status(thm)],[f356]) ).
fof(f359,definition,
( sQ64_spl
<=> product(e_5,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f360,plain,
( ~ sQ64_spl
| product(e_5,e_4,e_5) ),
inference(component_clause,[status(thm)],[f359]) ).
fof(f362,definition,
( sQ65_spl
<=> product(e_5,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f363,plain,
( ~ sQ65_spl
| product(e_5,e_4,e_1) ),
inference(component_clause,[status(thm)],[f362]) ).
fof(f365,plain,
( sQ65_spl
| sQ64_spl
| sQ63_spl
| sQ62_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f348,f350,f353,f356,f359,f362]) ).
fof(f366,definition,
( sQ66_spl
<=> product(e_5,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f367,plain,
( ~ sQ66_spl
| product(e_5,e_2,e_3) ),
inference(component_clause,[status(thm)],[f366]) ).
fof(f368,plain,
( sQ66_spl
| ~ product(e_5,e_2,e_3) ),
inference(component_clause,[status(thm)],[f366]) ).
fof(f369,definition,
( sQ67_spl
<=> product(e_5,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f370,plain,
( ~ sQ67_spl
| product(e_5,e_2,e_2) ),
inference(component_clause,[status(thm)],[f369]) ).
fof(f372,definition,
( sQ68_spl
<=> product(e_5,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f373,plain,
( ~ sQ68_spl
| product(e_5,e_2,e_4) ),
inference(component_clause,[status(thm)],[f372]) ).
fof(f375,definition,
( sQ69_spl
<=> product(e_5,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f376,plain,
( ~ sQ69_spl
| product(e_5,e_2,e_5) ),
inference(component_clause,[status(thm)],[f375]) ).
fof(f378,definition,
( sQ70_spl
<=> product(e_5,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f379,plain,
( ~ sQ70_spl
| product(e_5,e_2,e_1) ),
inference(component_clause,[status(thm)],[f378]) ).
fof(f381,plain,
( sQ70_spl
| sQ69_spl
| sQ68_spl
| sQ67_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f346,f366,f369,f372,f375,f378]) ).
fof(f382,definition,
( sQ71_spl
<=> product(e_5,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f383,plain,
( ~ sQ71_spl
| product(e_5,e_1,e_3) ),
inference(component_clause,[status(thm)],[f382]) ).
fof(f384,plain,
( sQ71_spl
| ~ product(e_5,e_1,e_3) ),
inference(component_clause,[status(thm)],[f382]) ).
fof(f385,definition,
( sQ72_spl
<=> product(e_5,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f386,plain,
( ~ sQ72_spl
| product(e_5,e_1,e_2) ),
inference(component_clause,[status(thm)],[f385]) ).
fof(f388,definition,
( sQ73_spl
<=> product(e_5,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f389,plain,
( ~ sQ73_spl
| product(e_5,e_1,e_4) ),
inference(component_clause,[status(thm)],[f388]) ).
fof(f391,definition,
( sQ74_spl
<=> product(e_5,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f392,plain,
( ~ sQ74_spl
| product(e_5,e_1,e_5) ),
inference(component_clause,[status(thm)],[f391]) ).
fof(f394,definition,
( sQ75_spl
<=> product(e_5,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f395,plain,
( ~ sQ75_spl
| product(e_5,e_1,e_1) ),
inference(component_clause,[status(thm)],[f394]) ).
fof(f397,plain,
( sQ75_spl
| sQ74_spl
| sQ73_spl
| sQ72_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f349,f382,f385,f388,f391,f394]) ).
fof(f398,definition,
( sQ76_spl
<=> product(e_5,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f399,plain,
( ~ sQ76_spl
| product(e_5,e_5,e_3) ),
inference(component_clause,[status(thm)],[f398]) ).
fof(f401,definition,
( sQ77_spl
<=> product(e_5,e_5,e_2) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f402,plain,
( ~ sQ77_spl
| product(e_5,e_5,e_2) ),
inference(component_clause,[status(thm)],[f401]) ).
fof(f404,definition,
( sQ78_spl
<=> product(e_5,e_5,e_4) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f405,plain,
( ~ sQ78_spl
| product(e_5,e_5,e_4) ),
inference(component_clause,[status(thm)],[f404]) ).
fof(f407,definition,
( sQ79_spl
<=> product(e_5,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f410,definition,
( sQ80_spl
<=> product(e_5,e_5,e_1) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f411,plain,
( ~ sQ80_spl
| product(e_5,e_5,e_1) ),
inference(component_clause,[status(thm)],[f410]) ).
fof(f413,plain,
( sQ80_spl
| sQ79_spl
| sQ78_spl
| sQ77_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f347,f398,f401,f404,f407,f410]) ).
fof(f414,plain,
( product(e_2,e_2,e_5)
| product(e_2,e_2,e_4)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[f296,f91]) ).
fof(f415,plain,
( product(e_2,e_5,e_5)
| product(e_2,e_5,e_4)
| product(e_2,e_5,e_1)
| product(e_2,e_5,e_2)
| product(e_2,e_5,e_3) ),
inference(resolution,[status(thm)],[f296,f94]) ).
fof(f416,plain,
( product(e_2,e_4,e_5)
| product(e_2,e_4,e_4)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[f296,f93]) ).
fof(f417,plain,
( product(e_2,e_1,e_5)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[f296,f90]) ).
fof(f418,definition,
( sQ81_spl
<=> product(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f419,plain,
( ~ sQ81_spl
| product(e_2,e_1,e_3) ),
inference(component_clause,[status(thm)],[f418]) ).
fof(f421,definition,
( sQ82_spl
<=> product(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f422,plain,
( ~ sQ82_spl
| product(e_2,e_1,e_2) ),
inference(component_clause,[status(thm)],[f421]) ).
fof(f424,definition,
( sQ83_spl
<=> product(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f425,plain,
( ~ sQ83_spl
| product(e_2,e_1,e_1) ),
inference(component_clause,[status(thm)],[f424]) ).
fof(f427,definition,
( sQ84_spl
<=> product(e_2,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f428,plain,
( ~ sQ84_spl
| product(e_2,e_1,e_4) ),
inference(component_clause,[status(thm)],[f427]) ).
fof(f430,definition,
( sQ85_spl
<=> product(e_2,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f431,plain,
( ~ sQ85_spl
| product(e_2,e_1,e_5) ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f433,plain,
( sQ85_spl
| sQ84_spl
| sQ83_spl
| sQ82_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f417,f418,f421,f424,f427,f430]) ).
fof(f434,definition,
( sQ86_spl
<=> product(e_2,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f435,plain,
( ~ sQ86_spl
| product(e_2,e_2,e_3) ),
inference(component_clause,[status(thm)],[f434]) ).
fof(f437,definition,
( sQ87_spl
<=> product(e_2,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f440,definition,
( sQ88_spl
<=> product(e_2,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f441,plain,
( ~ sQ88_spl
| product(e_2,e_2,e_1) ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f443,definition,
( sQ89_spl
<=> product(e_2,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f444,plain,
( ~ sQ89_spl
| product(e_2,e_2,e_4) ),
inference(component_clause,[status(thm)],[f443]) ).
fof(f446,definition,
( sQ90_spl
<=> product(e_2,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f447,plain,
( ~ sQ90_spl
| product(e_2,e_2,e_5) ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f449,plain,
( sQ90_spl
| sQ89_spl
| sQ88_spl
| sQ87_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f414,f434,f437,f440,f443,f446]) ).
fof(f450,definition,
( sQ91_spl
<=> product(e_2,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f451,plain,
( ~ sQ91_spl
| product(e_2,e_5,e_3) ),
inference(component_clause,[status(thm)],[f450]) ).
fof(f453,definition,
( sQ92_spl
<=> product(e_2,e_5,e_2) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f454,plain,
( ~ sQ92_spl
| product(e_2,e_5,e_2) ),
inference(component_clause,[status(thm)],[f453]) ).
fof(f456,definition,
( sQ93_spl
<=> product(e_2,e_5,e_1) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( ~ sQ93_spl
| product(e_2,e_5,e_1) ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f459,definition,
( sQ94_spl
<=> product(e_2,e_5,e_4) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( ~ sQ94_spl
| product(e_2,e_5,e_4) ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,definition,
( sQ95_spl
<=> product(e_2,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f463,plain,
( ~ sQ95_spl
| product(e_2,e_5,e_5) ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,plain,
( sQ95_spl
| sQ94_spl
| sQ93_spl
| sQ92_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f415,f450,f453,f456,f459,f462]) ).
fof(f466,definition,
( sQ96_spl
<=> product(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( ~ sQ96_spl
| product(e_2,e_4,e_3) ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,definition,
( sQ97_spl
<=> product(e_2,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f470,plain,
( ~ sQ97_spl
| product(e_2,e_4,e_2) ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f472,definition,
( sQ98_spl
<=> product(e_2,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f473,plain,
( ~ sQ98_spl
| product(e_2,e_4,e_1) ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f475,definition,
( sQ99_spl
<=> product(e_2,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f476,plain,
( ~ sQ99_spl
| product(e_2,e_4,e_4) ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f478,definition,
( sQ100_spl
<=> product(e_2,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f479,plain,
( ~ sQ100_spl
| product(e_2,e_4,e_5) ),
inference(component_clause,[status(thm)],[f478]) ).
fof(f481,plain,
( sQ100_spl
| sQ99_spl
| sQ98_spl
| sQ97_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f416,f466,f469,f472,f475,f478]) ).
fof(f482,plain,
( product(e_2,e_3,e_5)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3) ),
inference(resolution,[status(thm)],[f92,f296]) ).
fof(f483,plain,
( product(e_5,e_3,e_1)
| product(e_5,e_3,e_5)
| product(e_5,e_3,e_4)
| product(e_5,e_3,e_2)
| product(e_5,e_3,e_3) ),
inference(resolution,[status(thm)],[f92,f244]) ).
fof(f484,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_5)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_4)
| product(e_4,e_3,e_3) ),
inference(resolution,[status(thm)],[f92,f174]) ).
fof(f485,plain,
( product(e_1,e_3,e_3)
| product(e_1,e_3,e_5)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_4) ),
inference(resolution,[status(thm)],[f92,f125]) ).
fof(f486,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_4)
| product(e_3,X0,e_5)
| product(e_3,X0,e_1) ),
inference(resolution,[status(thm)],[f92,f115]) ).
fof(f488,definition,
( sQ101_spl
<=> product(e_5,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f489,plain,
( ~ sQ101_spl
| product(e_5,e_3,e_3) ),
inference(component_clause,[status(thm)],[f488]) ).
fof(f491,definition,
( sQ102_spl
<=> product(e_5,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f492,plain,
( ~ sQ102_spl
| product(e_5,e_3,e_2) ),
inference(component_clause,[status(thm)],[f491]) ).
fof(f494,definition,
( sQ103_spl
<=> product(e_5,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f495,plain,
( ~ sQ103_spl
| product(e_5,e_3,e_4) ),
inference(component_clause,[status(thm)],[f494]) ).
fof(f497,definition,
( sQ104_spl
<=> product(e_5,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f498,plain,
( ~ sQ104_spl
| product(e_5,e_3,e_5) ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f500,definition,
( sQ105_spl
<=> product(e_5,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f501,plain,
( ~ sQ105_spl
| product(e_5,e_3,e_1) ),
inference(component_clause,[status(thm)],[f500]) ).
fof(f503,plain,
( sQ105_spl
| sQ104_spl
| sQ103_spl
| sQ102_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f483,f488,f491,f494,f497,f500]) ).
fof(f504,definition,
( sQ106_spl
<=> product(e_4,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f505,plain,
( ~ sQ106_spl
| product(e_4,e_3,e_3) ),
inference(component_clause,[status(thm)],[f504]) ).
fof(f507,definition,
( sQ107_spl
<=> product(e_4,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f508,plain,
( ~ sQ107_spl
| product(e_4,e_3,e_4) ),
inference(component_clause,[status(thm)],[f507]) ).
fof(f510,definition,
( sQ108_spl
<=> product(e_4,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f511,plain,
( ~ sQ108_spl
| product(e_4,e_3,e_2) ),
inference(component_clause,[status(thm)],[f510]) ).
fof(f513,definition,
( sQ109_spl
<=> product(e_4,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f514,plain,
( ~ sQ109_spl
| product(e_4,e_3,e_5) ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,definition,
( sQ110_spl
<=> product(e_4,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f517,plain,
( ~ sQ110_spl
| product(e_4,e_3,e_1) ),
inference(component_clause,[status(thm)],[f516]) ).
fof(f519,plain,
( sQ110_spl
| sQ109_spl
| sQ108_spl
| sQ107_spl
| sQ106_spl ),
inference(split_clause,[status(thm)],[f484,f504,f507,f510,f513,f516]) ).
fof(f520,definition,
( sQ111_spl
<=> product(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f521,plain,
( ~ sQ111_spl
| product(e_2,e_3,e_3) ),
inference(component_clause,[status(thm)],[f520]) ).
fof(f523,definition,
( sQ112_spl
<=> product(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f524,plain,
( ~ sQ112_spl
| product(e_2,e_3,e_2) ),
inference(component_clause,[status(thm)],[f523]) ).
fof(f526,definition,
( sQ113_spl
<=> product(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f527,plain,
( ~ sQ113_spl
| product(e_2,e_3,e_1) ),
inference(component_clause,[status(thm)],[f526]) ).
fof(f529,definition,
( sQ114_spl
<=> product(e_2,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f530,plain,
( ~ sQ114_spl
| product(e_2,e_3,e_4) ),
inference(component_clause,[status(thm)],[f529]) ).
fof(f532,definition,
( sQ115_spl
<=> product(e_2,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f533,plain,
( ~ sQ115_spl
| product(e_2,e_3,e_5) ),
inference(component_clause,[status(thm)],[f532]) ).
fof(f534,plain,
( sQ115_spl
| ~ product(e_2,e_3,e_5) ),
inference(component_clause,[status(thm)],[f532]) ).
fof(f535,plain,
( sQ115_spl
| sQ114_spl
| sQ113_spl
| sQ112_spl
| sQ111_spl ),
inference(split_clause,[status(thm)],[f482,f520,f523,f526,f529,f532]) ).
fof(f536,definition,
( sQ116_spl
<=> product(e_1,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f537,plain,
( ~ sQ116_spl
| product(e_1,e_3,e_4) ),
inference(component_clause,[status(thm)],[f536]) ).
fof(f539,definition,
( sQ117_spl
<=> product(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f540,plain,
( ~ sQ117_spl
| product(e_1,e_3,e_2) ),
inference(component_clause,[status(thm)],[f539]) ).
fof(f542,definition,
( sQ118_spl
<=> product(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( ~ sQ118_spl
| product(e_1,e_3,e_1) ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f545,definition,
( sQ119_spl
<=> product(e_1,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f546,plain,
( ~ sQ119_spl
| product(e_1,e_3,e_5) ),
inference(component_clause,[status(thm)],[f545]) ).
fof(f548,definition,
( sQ120_spl
<=> product(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f549,plain,
( ~ sQ120_spl
| product(e_1,e_3,e_3) ),
inference(component_clause,[status(thm)],[f548]) ).
fof(f551,plain,
( sQ120_spl
| sQ119_spl
| sQ118_spl
| sQ117_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f485,f536,f539,f542,f545,f548]) ).
fof(f558,definition,
( sQ123_spl
<=> cycle(e_3,e_0) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f568,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_4)
| product(e_3,e_3,e_5)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[f486,f92]) ).
fof(f569,plain,
( product(e_3,e_2,e_3)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[f486,f91]) ).
fof(f570,plain,
( product(e_3,e_5,e_3)
| product(e_3,e_5,e_2)
| product(e_3,e_5,e_4)
| product(e_3,e_5,e_5)
| product(e_3,e_5,e_1) ),
inference(resolution,[status(thm)],[f486,f94]) ).
fof(f571,plain,
( product(e_3,e_4,e_3)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_4)
| product(e_3,e_4,e_5)
| product(e_3,e_4,e_1) ),
inference(resolution,[status(thm)],[f486,f93]) ).
fof(f572,plain,
( product(e_3,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5)
| product(e_3,e_1,e_1) ),
inference(resolution,[status(thm)],[f486,f90]) ).
fof(f573,definition,
( sQ126_spl
<=> product(e_3,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f574,plain,
( ~ sQ126_spl
| product(e_3,e_4,e_1) ),
inference(component_clause,[status(thm)],[f573]) ).
fof(f576,definition,
( sQ127_spl
<=> product(e_3,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f577,plain,
( ~ sQ127_spl
| product(e_3,e_4,e_5) ),
inference(component_clause,[status(thm)],[f576]) ).
fof(f579,definition,
( sQ128_spl
<=> product(e_3,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f580,plain,
( ~ sQ128_spl
| product(e_3,e_4,e_4) ),
inference(component_clause,[status(thm)],[f579]) ).
fof(f582,definition,
( sQ129_spl
<=> product(e_3,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f583,plain,
( ~ sQ129_spl
| product(e_3,e_4,e_2) ),
inference(component_clause,[status(thm)],[f582]) ).
fof(f585,definition,
( sQ130_spl
<=> product(e_3,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f586,plain,
( ~ sQ130_spl
| product(e_3,e_4,e_3) ),
inference(component_clause,[status(thm)],[f585]) ).
fof(f588,plain,
( sQ130_spl
| sQ129_spl
| sQ128_spl
| sQ127_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f571,f573,f576,f579,f582,f585]) ).
fof(f589,definition,
( sQ131_spl
<=> product(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f590,plain,
( ~ sQ131_spl
| product(e_3,e_1,e_1) ),
inference(component_clause,[status(thm)],[f589]) ).
fof(f592,definition,
( sQ132_spl
<=> product(e_3,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f593,plain,
( ~ sQ132_spl
| product(e_3,e_1,e_5) ),
inference(component_clause,[status(thm)],[f592]) ).
fof(f594,plain,
( sQ132_spl
| ~ product(e_3,e_1,e_5) ),
inference(component_clause,[status(thm)],[f592]) ).
fof(f595,definition,
( sQ133_spl
<=> product(e_3,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f596,plain,
( ~ sQ133_spl
| product(e_3,e_1,e_4) ),
inference(component_clause,[status(thm)],[f595]) ).
fof(f598,definition,
( sQ134_spl
<=> product(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f599,plain,
( ~ sQ134_spl
| product(e_3,e_1,e_2) ),
inference(component_clause,[status(thm)],[f598]) ).
fof(f600,plain,
( sQ134_spl
| ~ product(e_3,e_1,e_2) ),
inference(component_clause,[status(thm)],[f598]) ).
fof(f601,definition,
( sQ135_spl
<=> product(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f602,plain,
( ~ sQ135_spl
| product(e_3,e_1,e_3) ),
inference(component_clause,[status(thm)],[f601]) ).
fof(f604,plain,
( sQ135_spl
| sQ134_spl
| sQ133_spl
| sQ132_spl
| sQ131_spl ),
inference(split_clause,[status(thm)],[f572,f589,f592,f595,f598,f601]) ).
fof(f605,definition,
( sQ136_spl
<=> product(e_3,e_5,e_1) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f606,plain,
( ~ sQ136_spl
| product(e_3,e_5,e_1) ),
inference(component_clause,[status(thm)],[f605]) ).
fof(f608,definition,
( sQ137_spl
<=> product(e_3,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f609,plain,
( ~ sQ137_spl
| product(e_3,e_5,e_5) ),
inference(component_clause,[status(thm)],[f608]) ).
fof(f611,definition,
( sQ138_spl
<=> product(e_3,e_5,e_4) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f612,plain,
( ~ sQ138_spl
| product(e_3,e_5,e_4) ),
inference(component_clause,[status(thm)],[f611]) ).
fof(f614,definition,
( sQ139_spl
<=> product(e_3,e_5,e_2) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f615,plain,
( ~ sQ139_spl
| product(e_3,e_5,e_2) ),
inference(component_clause,[status(thm)],[f614]) ).
fof(f617,definition,
( sQ140_spl
<=> product(e_3,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f618,plain,
( ~ sQ140_spl
| product(e_3,e_5,e_3) ),
inference(component_clause,[status(thm)],[f617]) ).
fof(f620,plain,
( sQ140_spl
| sQ139_spl
| sQ138_spl
| sQ137_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f570,f605,f608,f611,f614,f617]) ).
fof(f621,definition,
( sQ141_spl
<=> product(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f622,plain,
( ~ sQ141_spl
| product(e_3,e_2,e_1) ),
inference(component_clause,[status(thm)],[f621]) ).
fof(f624,definition,
( sQ142_spl
<=> product(e_3,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f625,plain,
( ~ sQ142_spl
| product(e_3,e_2,e_5) ),
inference(component_clause,[status(thm)],[f624]) ).
fof(f627,definition,
( sQ143_spl
<=> product(e_3,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f628,plain,
( ~ sQ143_spl
| product(e_3,e_2,e_4) ),
inference(component_clause,[status(thm)],[f627]) ).
fof(f630,definition,
( sQ144_spl
<=> product(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f631,plain,
( ~ sQ144_spl
| product(e_3,e_2,e_2) ),
inference(component_clause,[status(thm)],[f630]) ).
fof(f633,definition,
( sQ145_spl
<=> product(e_3,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f634,plain,
( ~ sQ145_spl
| product(e_3,e_2,e_3) ),
inference(component_clause,[status(thm)],[f633]) ).
fof(f636,plain,
( sQ145_spl
| sQ144_spl
| sQ143_spl
| sQ142_spl
| sQ141_spl ),
inference(split_clause,[status(thm)],[f569,f621,f624,f627,f630,f633]) ).
fof(f637,definition,
( sQ146_spl
<=> product(e_3,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f638,plain,
( ~ sQ146_spl
| product(e_3,e_3,e_1) ),
inference(component_clause,[status(thm)],[f637]) ).
fof(f640,definition,
( sQ147_spl
<=> product(e_3,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f641,plain,
( ~ sQ147_spl
| product(e_3,e_3,e_5) ),
inference(component_clause,[status(thm)],[f640]) ).
fof(f643,definition,
( sQ148_spl
<=> product(e_3,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f644,plain,
( ~ sQ148_spl
| product(e_3,e_3,e_4) ),
inference(component_clause,[status(thm)],[f643]) ).
fof(f646,definition,
( sQ149_spl
<=> product(e_3,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f647,plain,
( ~ sQ149_spl
| product(e_3,e_3,e_2) ),
inference(component_clause,[status(thm)],[f646]) ).
fof(f649,definition,
( sQ150_spl
<=> product(e_3,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f652,plain,
( sQ150_spl
| sQ149_spl
| sQ148_spl
| sQ147_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f568,f637,f640,f643,f646,f649]) ).
fof(f657,definition,
( sQ152_spl
<=> greater(e_0,e_0) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f662,plain,
! [X0,X1,X2] :
( ~ greater(X0,X1)
| ~ greater(X2,e_0)
| ~ cycle(X0,e_0)
| ~ cycle(X1,X2)
| ~ next(X0,e_5) ),
inference(resolution,[status(thm)],[f86,f82]) ).
fof(f671,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ next(e_1,X1)
| ~ greater(e_3,e_0)
| ~ product(e_1,e_1,X0)
| equalish(X0,X1) ),
inference(resolution,[status(thm)],[f140,f89]) ).
fof(f672,definition,
! [X0,X1] :
( sQ154_spl
<=> ( ~ next(e_1,X1)
| ~ product(e_1,e_1,X0)
| equalish(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f673,plain,
! [X0,X1] :
( ~ sQ154_spl
| equalish(X0,X1)
| ~ next(e_1,X1)
| ~ product(e_1,e_1,X0) ),
inference(component_clause,[status(thm)],[f672]) ).
fof(f675,definition,
( sQ155_spl
<=> greater(e_3,e_0) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f677,plain,
( sQ155_spl
| ~ greater(e_3,e_0) ),
inference(component_clause,[status(thm)],[f675]) ).
fof(f678,plain,
( ~ sQ4_spl
| ~ sQ155_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f671,f672,f675,f139]) ).
fof(f683,plain,
( sQ155_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f677,f66]) ).
fof(f684,plain,
sQ155_spl,
inference(contradiction_clause,[status(thm)],[f683]) ).
fof(f688,plain,
! [X0,X1] :
( ~ sQ15_spl
| ~ next(e_4,X1)
| ~ greater(e_3,e_0)
| ~ product(e_4,e_1,X0)
| equalish(X0,X1) ),
inference(resolution,[status(thm)],[f189,f89]) ).
fof(f693,definition,
! [X0,X1] :
( sQ158_spl
<=> ( ~ next(e_4,X1)
| ~ product(e_4,e_1,X0)
| equalish(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f694,plain,
! [X0,X1] :
( ~ sQ158_spl
| ~ next(e_4,X1)
| ~ product(e_4,e_1,X0)
| equalish(X0,X1) ),
inference(component_clause,[status(thm)],[f693]) ).
fof(f696,plain,
( ~ sQ15_spl
| ~ sQ155_spl
| sQ158_spl ),
inference(split_clause,[status(thm)],[f688,f693,f675,f188]) ).
fof(f700,plain,
! [X0,X1] :
( ~ sQ11_spl
| ~ next(e_4,X1)
| ~ greater(e_4,e_0)
| ~ product(e_4,e_1,X0)
| equalish(X0,X1) ),
inference(resolution,[status(thm)],[f177,f89]) ).
fof(f704,definition,
( sQ160_spl
<=> greater(e_4,e_0) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f706,plain,
( sQ160_spl
| ~ greater(e_4,e_0) ),
inference(component_clause,[status(thm)],[f704]) ).
fof(f708,plain,
( ~ sQ11_spl
| ~ sQ160_spl
| sQ158_spl ),
inference(split_clause,[status(thm)],[f700,f693,f704,f176]) ).
fof(f709,plain,
( sQ160_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f706,f67]) ).
fof(f710,plain,
sQ160_spl,
inference(contradiction_clause,[status(thm)],[f709]) ).
fof(f714,plain,
! [X0,X1] :
( ~ sQ14_spl
| ~ next(e_4,X1)
| ~ greater(e_2,e_0)
| ~ product(e_4,e_1,X0)
| equalish(X0,X1) ),
inference(resolution,[status(thm)],[f186,f89]) ).
fof(f715,definition,
( sQ161_spl
<=> greater(e_2,e_0) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f717,plain,
( sQ161_spl
| ~ greater(e_2,e_0) ),
inference(component_clause,[status(thm)],[f715]) ).
fof(f718,plain,
( ~ sQ14_spl
| ~ sQ161_spl
| sQ158_spl ),
inference(split_clause,[status(thm)],[f714,f693,f715,f185]) ).
fof(f723,plain,
( sQ161_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f65]) ).
fof(f724,plain,
sQ161_spl,
inference(contradiction_clause,[status(thm)],[f723]) ).
fof(f728,plain,
! [X0,X1] :
( ~ sQ12_spl
| ~ next(e_4,X1)
| ~ greater(e_1,e_0)
| ~ product(e_4,e_1,X0)
| equalish(X0,X1) ),
inference(resolution,[status(thm)],[f180,f89]) ).
fof(f732,definition,
( sQ164_spl
<=> greater(e_1,e_0) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f734,plain,
( sQ164_spl
| ~ greater(e_1,e_0) ),
inference(component_clause,[status(thm)],[f732]) ).
fof(f736,plain,
( ~ sQ12_spl
| ~ sQ164_spl
| sQ158_spl ),
inference(split_clause,[status(thm)],[f728,f693,f732,f179]) ).
fof(f737,plain,
( sQ164_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f734,f64]) ).
fof(f738,plain,
sQ164_spl,
inference(contradiction_clause,[status(thm)],[f737]) ).
fof(f883,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ next(e_1,X1)
| ~ greater(e_2,e_0)
| ~ product(e_1,e_1,X0)
| equalish(X0,X1) ),
inference(resolution,[status(thm)],[f137,f89]) ).
fof(f884,plain,
( ~ sQ3_spl
| ~ sQ161_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f883,f672,f715,f136]) ).
fof(f918,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ next(e_1,X1)
| ~ greater(e_4,e_0)
| ~ product(e_1,e_1,X0)
| equalish(X0,X1) ),
inference(resolution,[status(thm)],[f128,f89]) ).
fof(f927,plain,
( ~ sQ0_spl
| ~ sQ160_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f918,f672,f704,f127]) ).
fof(f932,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ next(e_1,X1)
| ~ greater(e_1,e_0)
| ~ product(e_1,e_1,X0)
| equalish(X0,X1) ),
inference(resolution,[status(thm)],[f131,f89]) ).
fof(f934,plain,
( ~ sQ1_spl
| ~ sQ164_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f932,f672,f732,f130]) ).
fof(f939,plain,
! [X0] :
( ~ sQ47_spl
| ~ greater(X0,e_2)
| ~ greater(e_1,e_0)
| ~ cycle(X0,e_0)
| ~ next(X0,e_5) ),
inference(resolution,[status(thm)],[f302,f662]) ).
fof(f945,definition,
! [X0] :
( sQ190_spl
<=> ( ~ greater(X0,e_2)
| ~ cycle(X0,e_0)
| ~ next(X0,e_5) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f946,plain,
! [X0] :
( ~ sQ190_spl
| ~ next(X0,e_5)
| ~ cycle(X0,e_0)
| ~ greater(X0,e_2) ),
inference(component_clause,[status(thm)],[f945]) ).
fof(f948,plain,
( ~ sQ47_spl
| ~ sQ164_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f939,f945,f732,f301]) ).
fof(f977,plain,
! [X0] :
( ~ sQ49_spl
| ~ greater(X0,e_2)
| ~ greater(e_2,e_0)
| ~ cycle(X0,e_0)
| ~ next(X0,e_5) ),
inference(resolution,[status(thm)],[f308,f662]) ).
fof(f983,plain,
( ~ sQ49_spl
| ~ sQ161_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f977,f945,f715,f307]) ).
fof(f1009,plain,
! [X0] :
( ~ sQ46_spl
| ~ greater(X0,e_2)
| ~ greater(e_4,e_0)
| ~ cycle(X0,e_0)
| ~ next(X0,e_5) ),
inference(resolution,[status(thm)],[f299,f662]) ).
fof(f1016,plain,
( ~ sQ46_spl
| ~ sQ160_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f1009,f945,f704,f298]) ).
fof(f1066,plain,
( ~ sQ9_spl
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[f157,f165]) ).
fof(f1072,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1066,f96]) ).
fof(f1073,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1072]) ).
fof(f1074,plain,
! [X0] :
( ~ sQ20_spl
| ~ product(e_1,e_4,X0)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f205,f117]) ).
fof(f1075,plain,
! [X0] :
( ~ sQ20_spl
| equalish(e_1,X0)
| ~ product(X0,e_4,e_3) ),
inference(resolution,[status(thm)],[f205,f121]) ).
fof(f1077,plain,
! [X0] :
( ~ sQ20_spl
| product(e_3,X0,e_1)
| ~ product(e_4,e_1,X0) ),
inference(resolution,[status(thm)],[f205,f124]) ).
fof(f1080,plain,
( ~ sQ16_spl
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[f193,f163]) ).
fof(f1085,plain,
( ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1080,f107]) ).
fof(f1086,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f1085]) ).
fof(f1091,plain,
( ~ sQ18_spl
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[f199,f160]) ).
fof(f1095,plain,
( ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1091,f97]) ).
fof(f1096,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f1095]) ).
fof(f1097,plain,
( ~ sQ20_spl
| ~ sQ19_spl
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[f202,f1074]) ).
fof(f1099,plain,
! [X0] :
( ~ sQ19_spl
| ~ product(X0,e_4,e_5)
| equalish(e_1,X0) ),
inference(resolution,[status(thm)],[f202,f121]) ).
fof(f1100,plain,
! [X0] :
( ~ sQ19_spl
| ~ product(e_1,X0,e_5)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f202,f119]) ).
fof(f1102,plain,
( ~ sQ20_spl
| ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1097,f106]) ).
fof(f1103,plain,
( ~ sQ20_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f1102]) ).
fof(f1106,plain,
! [X0] :
( ~ sQ17_spl
| ~ product(e_1,X0,e_2)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f196,f119]) ).
fof(f1107,plain,
! [X0] :
( ~ sQ17_spl
| ~ product(e_4,e_1,X0)
| product(e_2,X0,e_1) ),
inference(resolution,[status(thm)],[f196,f124]) ).
fof(f1114,plain,
( ~ sQ22_spl
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[f214,f160]) ).
fof(f1118,plain,
( ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1114,f107]) ).
fof(f1119,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f1118]) ).
fof(f1120,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| product(e_2,e_3,e_1) ),
inference(resolution,[status(thm)],[f211,f1107]) ).
fof(f1123,plain,
! [X0] :
( ~ sQ21_spl
| ~ product(X0,e_1,e_3)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f211,f121]) ).
fof(f1124,plain,
! [X0] :
( ~ sQ21_spl
| equalish(e_1,X0)
| ~ product(e_4,X0,e_3) ),
inference(resolution,[status(thm)],[f211,f119]) ).
fof(f1125,plain,
! [X0] :
( ~ sQ21_spl
| product(e_3,X0,e_4)
| ~ product(e_1,e_4,X0) ),
inference(resolution,[status(thm)],[f211,f124]) ).
fof(f1132,plain,
( ~ sQ25_spl
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[f223,f163]) ).
fof(f1141,plain,
( ~ sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1132,f97]) ).
fof(f1142,plain,
~ sQ25_spl,
inference(contradiction_clause,[status(thm)],[f1141]) ).
fof(f1143,plain,
( ~ sQ26_spl
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[f227,f165]) ).
fof(f1149,plain,
( ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1143,f109]) ).
fof(f1150,plain,
~ sQ26_spl,
inference(contradiction_clause,[status(thm)],[f1149]) ).
fof(f1151,plain,
( ~ sQ17_spl
| ~ sQ23_spl
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[f217,f1107]) ).
fof(f1154,plain,
! [X0] :
( ~ sQ23_spl
| equalish(e_4,X0)
| ~ product(X0,e_1,e_2) ),
inference(resolution,[status(thm)],[f217,f121]) ).
fof(f1155,plain,
! [X0] :
( ~ sQ23_spl
| equalish(e_1,X0)
| ~ product(e_4,X0,e_2) ),
inference(resolution,[status(thm)],[f217,f119]) ).
fof(f1161,plain,
( ~ sQ30_spl
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[f239,f165]) ).
fof(f1168,plain,
( ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1161,f107]) ).
fof(f1169,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1168]) ).
fof(f1179,plain,
( ~ sQ17_spl
| ~ sQ24_spl
| product(e_2,e_5,e_1) ),
inference(resolution,[status(thm)],[f220,f1107]) ).
fof(f1180,plain,
( ~ sQ24_spl
| ~ greater(e_5,e_4)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[f220,f87]) ).
fof(f1182,plain,
! [X0] :
( ~ sQ24_spl
| ~ product(X0,e_1,e_5)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f220,f121]) ).
fof(f1183,plain,
! [X0] :
( ~ sQ24_spl
| ~ product(e_4,X0,e_5)
| equalish(e_1,X0) ),
inference(resolution,[status(thm)],[f220,f119]) ).
fof(f1185,definition,
( sQ195_spl
<=> greater(e_5,e_4) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f1187,plain,
( sQ195_spl
| ~ greater(e_5,e_4) ),
inference(component_clause,[status(thm)],[f1185]) ).
fof(f1188,plain,
( ~ sQ24_spl
| ~ sQ195_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1180,f182,f1185,f219]) ).
fof(f1189,plain,
( sQ195_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1187,f78]) ).
fof(f1190,plain,
sQ195_spl,
inference(contradiction_clause,[status(thm)],[f1189]) ).
fof(f1191,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| product(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[f1125,f196]) ).
fof(f1192,plain,
! [X0] :
( ~ sQ17_spl
| ~ sQ21_spl
| equalish(e_1,X0)
| ~ product(e_2,e_3,X0) ),
inference(resolution,[status(thm)],[f1120,f117]) ).
fof(f1197,plain,
! [X0] :
( ~ sQ17_spl
| ~ sQ21_spl
| ~ product(X0,e_2,e_4)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f1191,f121]) ).
fof(f1199,plain,
! [X0] :
( ~ sQ17_spl
| ~ sQ21_spl
| ~ product(e_2,e_3,X0)
| product(e_4,X0,e_3) ),
inference(resolution,[status(thm)],[f1191,f124]) ).
fof(f1201,plain,
( ~ sQ29_spl
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[f236,f165]) ).
fof(f1207,plain,
( ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1201,f110]) ).
fof(f1208,plain,
~ sQ29_spl,
inference(contradiction_clause,[status(thm)],[f1207]) ).
fof(f1212,plain,
! [X0] :
( ~ sQ31_spl
| equalish(e_1,X0)
| ~ product(X0,e_5,e_4) ),
inference(resolution,[status(thm)],[f247,f121]) ).
fof(f1213,plain,
! [X0] :
( ~ sQ31_spl
| ~ product(e_1,X0,e_4)
| equalish(e_5,X0) ),
inference(resolution,[status(thm)],[f247,f119]) ).
fof(f1214,plain,
! [X0] :
( ~ sQ31_spl
| ~ product(e_5,e_1,X0)
| product(e_4,X0,e_1) ),
inference(resolution,[status(thm)],[f247,f124]) ).
fof(f1218,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[f1199,f1120]) ).
fof(f1233,plain,
( ~ sQ21_spl
| ~ sQ36_spl
| equalish(e_1,e_5) ),
inference(resolution,[status(thm)],[f263,f1124]) ).
fof(f1235,plain,
! [X0] :
( ~ sQ36_spl
| equalish(e_4,X0)
| ~ product(X0,e_5,e_3) ),
inference(resolution,[status(thm)],[f263,f121]) ).
fof(f1236,plain,
! [X0] :
( ~ sQ36_spl
| ~ product(e_4,X0,e_3)
| equalish(e_5,X0) ),
inference(resolution,[status(thm)],[f263,f119]) ).
fof(f1237,plain,
! [X0] :
( ~ sQ36_spl
| product(e_3,X0,e_4)
| ~ product(e_5,e_4,X0) ),
inference(resolution,[status(thm)],[f263,f124]) ).
fof(f1238,plain,
( ~ sQ21_spl
| ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1233,f98]) ).
fof(f1239,plain,
( ~ sQ21_spl
| ~ sQ36_spl ),
inference(contradiction_clause,[status(thm)],[f1238]) ).
fof(f1240,plain,
! [X0] :
( ~ sQ38_spl
| ~ product(e_4,e_5,X0)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f269,f117]) ).
fof(f1241,plain,
! [X0] :
( ~ sQ38_spl
| ~ product(X0,e_5,e_2)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f269,f121]) ).
fof(f1242,plain,
! [X0] :
( ~ sQ38_spl
| ~ product(e_4,X0,e_2)
| equalish(e_5,X0) ),
inference(resolution,[status(thm)],[f269,f119]) ).
fof(f1243,plain,
! [X0] :
( ~ sQ38_spl
| product(e_2,X0,e_4)
| ~ product(e_5,e_4,X0) ),
inference(resolution,[status(thm)],[f269,f124]) ).
fof(f1247,plain,
( ~ sQ34_spl
| equalish(e_5,e_1) ),
inference(resolution,[status(thm)],[f256,f163]) ).
fof(f1252,plain,
( ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1247,f111]) ).
fof(f1253,plain,
~ sQ34_spl,
inference(contradiction_clause,[status(thm)],[f1252]) ).
fof(f1257,plain,
( ~ sQ33_spl
| equalish(e_1,e_5) ),
inference(resolution,[status(thm)],[f253,f160]) ).
fof(f1261,plain,
( ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1257,f98]) ).
fof(f1262,plain,
~ sQ33_spl,
inference(contradiction_clause,[status(thm)],[f1261]) ).
fof(f1265,plain,
! [X0] :
( ~ sQ35_spl
| equalish(e_1,X0)
| ~ product(X0,e_5,e_3) ),
inference(resolution,[status(thm)],[f259,f121]) ).
fof(f1267,plain,
! [X0] :
( ~ sQ35_spl
| product(e_3,X0,e_1)
| ~ product(e_5,e_1,X0) ),
inference(resolution,[status(thm)],[f259,f124]) ).
fof(f1270,plain,
( ~ sQ17_spl
| ~ sQ32_spl
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[f250,f1106]) ).
fof(f1271,plain,
( ~ sQ38_spl
| ~ sQ32_spl
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[f250,f1241]) ).
fof(f1274,plain,
! [X0] :
( ~ sQ32_spl
| equalish(e_5,X0)
| ~ product(e_1,X0,e_2) ),
inference(resolution,[status(thm)],[f250,f119]) ).
fof(f1275,plain,
! [X0] :
( ~ sQ32_spl
| product(e_2,X0,e_1)
| ~ product(e_5,e_1,X0) ),
inference(resolution,[status(thm)],[f250,f124]) ).
fof(f1276,plain,
( ~ sQ17_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1270,f110]) ).
fof(f1277,plain,
( ~ sQ17_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f1276]) ).
fof(f1278,plain,
( ~ sQ38_spl
| ~ sQ40_spl
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[f275,f1240]) ).
fof(f1280,plain,
! [X0] :
( ~ sQ40_spl
| ~ product(X0,e_5,e_1)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f275,f121]) ).
fof(f1282,plain,
! [X0] :
( ~ sQ40_spl
| ~ product(e_5,e_4,X0)
| product(e_1,X0,e_4) ),
inference(resolution,[status(thm)],[f275,f124]) ).
fof(f1283,plain,
( ~ sQ38_spl
| ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1278,f99]) ).
fof(f1284,plain,
( ~ sQ38_spl
| ~ sQ40_spl ),
inference(contradiction_clause,[status(thm)],[f1283]) ).
fof(f1285,plain,
( ~ sQ39_spl
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[f272,f163]) ).
fof(f1290,plain,
( ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1285,f114]) ).
fof(f1291,plain,
~ sQ39_spl,
inference(contradiction_clause,[status(thm)],[f1290]) ).
fof(f1294,plain,
( ~ sQ37_spl
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[f266,f160]) ).
fof(f1300,plain,
( ~ sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1294,f110]) ).
fof(f1301,plain,
~ sQ37_spl,
inference(contradiction_clause,[status(thm)],[f1300]) ).
fof(f1302,plain,
( ~ sQ38_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1271,f107]) ).
fof(f1303,plain,
( ~ sQ38_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f1302]) ).
fof(f1304,plain,
( ~ sQ31_spl
| ~ sQ51_spl
| equalish(e_5,e_2) ),
inference(resolution,[status(thm)],[f315,f1213]) ).
fof(f1306,plain,
! [X0] :
( ~ sQ51_spl
| equalish(e_1,X0)
| ~ product(X0,e_2,e_4) ),
inference(resolution,[status(thm)],[f315,f121]) ).
fof(f1308,plain,
! [X0] :
( ~ sQ51_spl
| ~ product(e_2,e_1,X0)
| product(e_4,X0,e_1) ),
inference(resolution,[status(thm)],[f315,f124]) ).
fof(f1309,plain,
( ~ sQ31_spl
| ~ sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1304,f112]) ).
fof(f1310,plain,
( ~ sQ31_spl
| ~ sQ51_spl ),
inference(contradiction_clause,[status(thm)],[f1309]) ).
fof(f1311,plain,
( ~ sQ21_spl
| ~ sQ56_spl
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[f331,f1124]) ).
fof(f1313,plain,
! [X0] :
( ~ sQ56_spl
| equalish(e_4,X0)
| ~ product(X0,e_2,e_3) ),
inference(resolution,[status(thm)],[f331,f121]) ).
fof(f1315,plain,
! [X0] :
( ~ sQ56_spl
| product(e_3,X0,e_4)
| ~ product(e_2,e_4,X0) ),
inference(resolution,[status(thm)],[f331,f124]) ).
fof(f1316,plain,
( ~ sQ21_spl
| ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1311,f95]) ).
fof(f1317,plain,
( ~ sQ21_spl
| ~ sQ56_spl ),
inference(contradiction_clause,[status(thm)],[f1316]) ).
fof(f1319,plain,
( ~ sQ58_spl
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[f337,f163]) ).
fof(f1324,plain,
( ~ sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1319,f101]) ).
fof(f1325,plain,
~ sQ58_spl,
inference(contradiction_clause,[status(thm)],[f1324]) ).
fof(f1326,plain,
! [X0] :
( ~ sQ60_spl
| ~ product(e_4,e_2,X0)
| equalish(e_1,X0) ),
inference(resolution,[status(thm)],[f343,f117]) ).
fof(f1327,plain,
! [X0] :
( ~ sQ60_spl
| equalish(e_4,X0)
| ~ product(X0,e_2,e_1) ),
inference(resolution,[status(thm)],[f343,f121]) ).
fof(f1328,plain,
! [X0] :
( ~ sQ60_spl
| equalish(e_2,X0)
| ~ product(e_4,X0,e_1) ),
inference(resolution,[status(thm)],[f343,f119]) ).
fof(f1329,plain,
! [X0] :
( ~ sQ60_spl
| ~ product(e_2,e_4,X0)
| product(e_1,X0,e_4) ),
inference(resolution,[status(thm)],[f343,f124]) ).
fof(f1335,plain,
( ~ sQ53_spl
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[f321,f160]) ).
fof(f1339,plain,
( ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1335,f95]) ).
fof(f1340,plain,
~ sQ53_spl,
inference(contradiction_clause,[status(thm)],[f1339]) ).
fof(f1341,plain,
( ~ sQ19_spl
| ~ sQ54_spl
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[f324,f1100]) ).
fof(f1343,plain,
! [X0] :
( ~ sQ54_spl
| equalish(e_1,X0)
| ~ product(X0,e_2,e_5) ),
inference(resolution,[status(thm)],[f324,f121]) ).
fof(f1344,plain,
! [X0] :
( ~ sQ54_spl
| ~ product(e_1,X0,e_5)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f324,f119]) ).
fof(f1345,plain,
! [X0] :
( ~ sQ54_spl
| ~ product(e_2,e_1,X0)
| product(e_5,X0,e_1) ),
inference(resolution,[status(thm)],[f324,f124]) ).
fof(f1346,plain,
( ~ sQ19_spl
| ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1341,f108]) ).
fof(f1347,plain,
( ~ sQ19_spl
| ~ sQ54_spl ),
inference(contradiction_clause,[status(thm)],[f1346]) ).
fof(f1375,plain,
( ~ sQ60_spl
| ~ sQ59_spl
| equalish(e_1,e_5) ),
inference(resolution,[status(thm)],[f340,f1326]) ).
fof(f1379,plain,
! [X0] :
( ~ sQ59_spl
| ~ product(e_2,e_4,X0)
| product(e_5,X0,e_4) ),
inference(resolution,[status(thm)],[f340,f124]) ).
fof(f1380,plain,
( ~ sQ60_spl
| ~ sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1375,f98]) ).
fof(f1381,plain,
( ~ sQ60_spl
| ~ sQ59_spl ),
inference(contradiction_clause,[status(thm)],[f1380]) ).
fof(f1384,plain,
! [X0] :
( ~ sQ55_spl
| equalish(e_1,X0)
| ~ product(X0,e_2,e_3) ),
inference(resolution,[status(thm)],[f327,f121]) ).
fof(f1385,plain,
! [X0] :
( ~ sQ55_spl
| equalish(e_2,X0)
| ~ product(e_1,X0,e_3) ),
inference(resolution,[status(thm)],[f327,f119]) ).
fof(f1386,plain,
! [X0] :
( ~ sQ55_spl
| product(e_3,X0,e_1)
| ~ product(e_2,e_1,X0) ),
inference(resolution,[status(thm)],[f327,f124]) ).
fof(f1397,plain,
( ~ sQ57_spl
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[f334,f160]) ).
fof(f1403,plain,
( ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1397,f108]) ).
fof(f1404,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f1403]) ).
fof(f1407,plain,
( ~ sQ52_spl
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[f318,f163]) ).
fof(f1412,plain,
( ~ sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1407,f99]) ).
fof(f1413,plain,
~ sQ52_spl,
inference(contradiction_clause,[status(thm)],[f1412]) ).
fof(f1415,plain,
( ~ sQ77_spl
| equalish(e_5,e_2) ),
inference(resolution,[status(thm)],[f402,f165]) ).
fof(f1421,plain,
( ~ sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1415,f112]) ).
fof(f1422,plain,
~ sQ77_spl,
inference(contradiction_clause,[status(thm)],[f1421]) ).
fof(f1423,plain,
( ~ sQ55_spl
| ~ sQ66_spl
| equalish(e_1,e_5) ),
inference(resolution,[status(thm)],[f367,f1384]) ).
fof(f1427,plain,
! [X0] :
( ~ sQ66_spl
| ~ product(e_2,e_5,X0)
| product(e_3,X0,e_5) ),
inference(resolution,[status(thm)],[f367,f124]) ).
fof(f1428,plain,
( ~ sQ55_spl
| ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1423,f98]) ).
fof(f1429,plain,
( ~ sQ55_spl
| ~ sQ66_spl ),
inference(contradiction_clause,[status(thm)],[f1428]) ).
fof(f1459,plain,
( ~ sQ31_spl
| ~ sQ72_spl
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[f386,f1214]) ).
fof(f1461,plain,
( ~ sQ72_spl
| ~ greater(e_2,e_5)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[f386,f87]) ).
fof(f1462,plain,
! [X0] :
( ~ sQ72_spl
| equalish(e_2,X0)
| ~ product(e_5,e_1,X0) ),
inference(resolution,[status(thm)],[f386,f117]) ).
fof(f1465,plain,
! [X0] :
( ~ sQ72_spl
| ~ product(e_1,e_5,X0)
| product(e_2,X0,e_5) ),
inference(resolution,[status(thm)],[f386,f124]) ).
fof(f1466,definition,
( sQ196_spl
<=> greater(e_2,e_5) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f1469,plain,
( ~ sQ72_spl
| ~ sQ196_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1461,f284,f1466,f385]) ).
fof(f1470,plain,
( ~ sQ31_spl
| ~ sQ72_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1459,f342,f385,f246]) ).
fof(f1522,plain,
( ~ sQ78_spl
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[f405,f165]) ).
fof(f1528,plain,
( ~ sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1522,f114]) ).
fof(f1529,plain,
~ sQ78_spl,
inference(contradiction_clause,[status(thm)],[f1528]) ).
fof(f1532,plain,
( ~ sQ64_spl
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[f360,f160]) ).
fof(f1536,plain,
( ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1532,f114]) ).
fof(f1537,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f1536]) ).
fof(f1541,plain,
( ~ sQ75_spl
| equalish(e_1,e_5) ),
inference(resolution,[status(thm)],[f395,f163]) ).
fof(f1550,plain,
( ~ sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1541,f98]) ).
fof(f1551,plain,
~ sQ75_spl,
inference(contradiction_clause,[status(thm)],[f1550]) ).
fof(f1552,plain,
( ~ sQ38_spl
| ~ sQ61_spl
| product(e_2,e_3,e_4) ),
inference(resolution,[status(thm)],[f351,f1243]) ).
fof(f1556,plain,
! [X0] :
( ~ sQ61_spl
| ~ product(e_4,e_5,X0)
| product(e_3,X0,e_5) ),
inference(resolution,[status(thm)],[f351,f124]) ).
fof(f1558,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| ~ sQ38_spl
| ~ sQ61_spl
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[f1552,f1192]) ).
fof(f1561,plain,
! [X0] :
( ~ sQ38_spl
| ~ sQ61_spl
| ~ product(X0,e_3,e_4)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f1552,f121]) ).
fof(f1565,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| ~ sQ38_spl
| ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1558,f97]) ).
fof(f1566,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| ~ sQ38_spl
| ~ sQ61_spl ),
inference(contradiction_clause,[status(thm)],[f1565]) ).
fof(f1567,plain,
( ~ sQ67_spl
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[f370,f163]) ).
fof(f1572,plain,
( ~ sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1567,f102]) ).
fof(f1573,plain,
~ sQ67_spl,
inference(contradiction_clause,[status(thm)],[f1572]) ).
fof(f1574,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| ~ sQ68_spl
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[f373,f1197]) ).
fof(f1576,plain,
! [X0] :
( ~ sQ68_spl
| ~ product(X0,e_2,e_4)
| equalish(e_5,X0) ),
inference(resolution,[status(thm)],[f373,f121]) ).
fof(f1577,plain,
! [X0] :
( ~ sQ68_spl
| equalish(e_2,X0)
| ~ product(e_5,X0,e_4) ),
inference(resolution,[status(thm)],[f373,f119]) ).
fof(f1578,plain,
! [X0] :
( ~ sQ68_spl
| product(e_4,X0,e_5)
| ~ product(e_2,e_5,X0) ),
inference(resolution,[status(thm)],[f373,f124]) ).
fof(f1579,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1574,f106]) ).
fof(f1580,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| ~ sQ68_spl ),
inference(contradiction_clause,[status(thm)],[f1579]) ).
fof(f1581,plain,
( ~ sQ60_spl
| ~ sQ70_spl
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[f379,f1327]) ).
fof(f1585,plain,
! [X0] :
( ~ sQ70_spl
| product(e_1,X0,e_5)
| ~ product(e_2,e_5,X0) ),
inference(resolution,[status(thm)],[f379,f124]) ).
fof(f1586,plain,
( ~ sQ60_spl
| ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1581,f110]) ).
fof(f1587,plain,
( ~ sQ60_spl
| ~ sQ70_spl ),
inference(contradiction_clause,[status(thm)],[f1586]) ).
fof(f1589,plain,
( ~ sQ69_spl
| equalish(e_5,e_2) ),
inference(resolution,[status(thm)],[f376,f160]) ).
fof(f1593,plain,
( ~ sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1589,f112]) ).
fof(f1594,plain,
~ sQ69_spl,
inference(contradiction_clause,[status(thm)],[f1593]) ).
fof(f1596,plain,
! [X0] :
( ~ sQ65_spl
| equalish(e_5,X0)
| ~ product(X0,e_4,e_1) ),
inference(resolution,[status(thm)],[f363,f121]) ).
fof(f1597,plain,
! [X0] :
( ~ sQ65_spl
| ~ product(e_5,X0,e_1)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f363,f119]) ).
fof(f1598,plain,
! [X0] :
( ~ sQ65_spl
| product(e_1,X0,e_5)
| ~ product(e_4,e_5,X0) ),
inference(resolution,[status(thm)],[f363,f124]) ).
fof(f1599,plain,
( ~ sQ65_spl
| ~ sQ40_spl
| product(e_1,e_1,e_4) ),
inference(resolution,[status(thm)],[f1282,f363]) ).
fof(f1601,plain,
( ~ sQ65_spl
| ~ sQ40_spl
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[f1599,f165]) ).
fof(f1608,plain,
( ~ sQ65_spl
| ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1601,f97]) ).
fof(f1609,plain,
( ~ sQ65_spl
| ~ sQ40_spl ),
inference(contradiction_clause,[status(thm)],[f1608]) ).
fof(f1610,plain,
( ~ sQ40_spl
| ~ sQ62_spl
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[f354,f1282]) ).
fof(f1612,plain,
! [X0] :
( ~ sQ62_spl
| equalish(e_5,X0)
| ~ product(X0,e_4,e_2) ),
inference(resolution,[status(thm)],[f354,f121]) ).
fof(f1614,plain,
! [X0] :
( ~ sQ62_spl
| product(e_2,X0,e_5)
| ~ product(e_4,e_5,X0) ),
inference(resolution,[status(thm)],[f354,f124]) ).
fof(f1622,plain,
( ~ sQ32_spl
| ~ sQ71_spl
| product(e_2,e_3,e_1) ),
inference(resolution,[status(thm)],[f383,f1275]) ).
fof(f1624,plain,
( ~ sQ21_spl
| ~ sQ71_spl
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[f383,f1123]) ).
fof(f1625,plain,
( ~ sQ71_spl
| ~ greater(e_3,e_5)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[f383,f87]) ).
fof(f1626,plain,
! [X0] :
( ~ sQ71_spl
| ~ product(e_5,e_1,X0)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f383,f117]) ).
fof(f1627,plain,
! [X0] :
( ~ sQ71_spl
| equalish(e_5,X0)
| ~ product(X0,e_1,e_3) ),
inference(resolution,[status(thm)],[f383,f121]) ).
fof(f1628,plain,
! [X0] :
( ~ sQ71_spl
| ~ product(e_5,X0,e_3)
| equalish(e_1,X0) ),
inference(resolution,[status(thm)],[f383,f119]) ).
fof(f1629,plain,
! [X0] :
( ~ sQ71_spl
| ~ product(e_1,e_5,X0)
| product(e_3,X0,e_5) ),
inference(resolution,[status(thm)],[f383,f124]) ).
fof(f1630,plain,
( ~ sQ21_spl
| ~ sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1624,f110]) ).
fof(f1631,plain,
( ~ sQ21_spl
| ~ sQ71_spl ),
inference(contradiction_clause,[status(thm)],[f1630]) ).
fof(f1633,plain,
( ~ sQ63_spl
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[f357,f163]) ).
fof(f1638,plain,
( ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1633,f110]) ).
fof(f1639,plain,
~ sQ63_spl,
inference(contradiction_clause,[status(thm)],[f1638]) ).
fof(f1640,plain,
( ~ sQ40_spl
| ~ sQ80_spl
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[f411,f1280]) ).
fof(f1647,plain,
( ~ sQ40_spl
| ~ sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1640,f110]) ).
fof(f1648,plain,
( ~ sQ40_spl
| ~ sQ80_spl ),
inference(contradiction_clause,[status(thm)],[f1647]) ).
fof(f1649,plain,
( ~ sQ40_spl
| ~ sQ62_spl
| ~ sQ68_spl
| equalish(e_5,e_1) ),
inference(resolution,[status(thm)],[f1576,f1610]) ).
fof(f1650,plain,
( ~ sQ40_spl
| ~ sQ62_spl
| ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1649,f111]) ).
fof(f1651,plain,
( ~ sQ40_spl
| ~ sQ62_spl
| ~ sQ68_spl ),
inference(contradiction_clause,[status(thm)],[f1650]) ).
fof(f1652,plain,
( ~ sQ32_spl
| ~ sQ73_spl
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[f389,f1275]) ).
fof(f1654,plain,
( ~ sQ73_spl
| ~ greater(e_4,e_5)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[f389,f87]) ).
fof(f1658,plain,
! [X0] :
( ~ sQ73_spl
| product(e_4,X0,e_5)
| ~ product(e_1,e_5,X0) ),
inference(resolution,[status(thm)],[f389,f124]) ).
fof(f1659,definition,
( sQ198_spl
<=> greater(e_4,e_5) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f1662,plain,
( ~ sQ73_spl
| ~ sQ198_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1654,f284,f1659,f388]) ).
fof(f1665,plain,
( ~ sQ76_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f399,f165]) ).
fof(f1677,plain,
( ~ sQ74_spl
| equalish(e_5,e_1) ),
inference(resolution,[status(thm)],[f392,f160]) ).
fof(f1685,plain,
( ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1677,f111]) ).
fof(f1686,plain,
~ sQ74_spl,
inference(contradiction_clause,[status(thm)],[f1685]) ).
fof(f1688,plain,
( ~ sQ99_spl
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[f476,f163]) ).
fof(f1694,plain,
( ~ sQ99_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1688,f108]) ).
fof(f1695,plain,
~ sQ99_spl,
inference(contradiction_clause,[status(thm)],[f1694]) ).
fof(f1699,plain,
( ~ sQ92_spl
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[f454,f160]) ).
fof(f1706,plain,
( ~ sQ86_spl
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[f435,f165]) ).
fof(f1714,plain,
( ~ sQ66_spl
| ~ sQ91_spl
| product(e_3,e_3,e_5) ),
inference(resolution,[status(thm)],[f451,f1427]) ).
fof(f1718,plain,
! [X0] :
( ~ sQ91_spl
| product(e_3,X0,e_2)
| ~ product(e_5,e_2,X0) ),
inference(resolution,[status(thm)],[f451,f124]) ).
fof(f1719,plain,
( ~ sQ66_spl
| ~ sQ91_spl
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[f1714,f165]) ).
fof(f1725,plain,
( ~ sQ66_spl
| ~ sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1719,f106]) ).
fof(f1726,plain,
( ~ sQ66_spl
| ~ sQ91_spl ),
inference(contradiction_clause,[status(thm)],[f1725]) ).
fof(f1727,plain,
( ~ sQ59_spl
| ~ sQ98_spl
| product(e_5,e_1,e_4) ),
inference(resolution,[status(thm)],[f473,f1379]) ).
fof(f1729,plain,
! [X0] :
( ~ sQ98_spl
| ~ product(X0,e_4,e_1)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f473,f121]) ).
fof(f1731,plain,
! [X0] :
( ~ sQ98_spl
| ~ product(e_4,e_2,X0)
| product(e_1,X0,e_2) ),
inference(resolution,[status(thm)],[f473,f124]) ).
fof(f1733,plain,
( ~ sQ72_spl
| ~ sQ59_spl
| ~ sQ98_spl
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[f1727,f1462]) ).
fof(f1736,plain,
( ~ sQ59_spl
| ~ sQ98_spl
| ~ greater(e_4,e_5)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[f1727,f87]) ).
fof(f1741,plain,
( ~ sQ72_spl
| ~ sQ59_spl
| ~ sQ98_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1733,f101]) ).
fof(f1742,plain,
( ~ sQ72_spl
| ~ sQ59_spl
| ~ sQ98_spl ),
inference(contradiction_clause,[status(thm)],[f1741]) ).
fof(f1743,definition,
( sQ200_spl
<=> greater(e_3,e_5) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f1746,plain,
( ~ sQ71_spl
| ~ sQ200_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1625,f284,f1743,f382]) ).
fof(f1762,plain,
( ~ sQ51_spl
| ~ sQ85_spl
| product(e_4,e_5,e_1) ),
inference(resolution,[status(thm)],[f431,f1308]) ).
fof(f1763,plain,
( ~ sQ85_spl
| ~ greater(e_5,e_2)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[f431,f87]) ).
fof(f1768,definition,
( sQ201_spl
<=> greater(e_5,e_2) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f1770,plain,
( sQ201_spl
| ~ greater(e_5,e_2) ),
inference(component_clause,[status(thm)],[f1768]) ).
fof(f1771,plain,
( ~ sQ85_spl
| ~ sQ201_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f1763,f304,f1768,f430]) ).
fof(f1772,plain,
( sQ201_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1770,f75]) ).
fof(f1773,plain,
sQ201_spl,
inference(contradiction_clause,[status(thm)],[f1772]) ).
fof(f1774,plain,
( ~ sQ51_spl
| ~ sQ89_spl
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[f444,f1306]) ).
fof(f1781,plain,
( ~ sQ51_spl
| ~ sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1774,f95]) ).
fof(f1782,plain,
( ~ sQ51_spl
| ~ sQ89_spl ),
inference(contradiction_clause,[status(thm)],[f1781]) ).
fof(f1783,plain,
( ~ sQ17_spl
| ~ sQ23_spl
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[f1151,f165]) ).
fof(f1789,plain,
( ~ sQ17_spl
| ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1783,f99]) ).
fof(f1790,plain,
( ~ sQ17_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f1789]) ).
fof(f1792,plain,
! [X0] :
( ~ sQ94_spl
| ~ product(X0,e_5,e_4)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f460,f121]) ).
fof(f1794,plain,
! [X0] :
( ~ sQ94_spl
| product(e_4,X0,e_2)
| ~ product(e_5,e_2,X0) ),
inference(resolution,[status(thm)],[f460,f124]) ).
fof(f1795,plain,
( ~ sQ94_spl
| ~ sQ66_spl
| product(e_3,e_4,e_5) ),
inference(resolution,[status(thm)],[f1427,f460]) ).
fof(f1805,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| product(e_3,e_1,e_5) ),
inference(resolution,[status(thm)],[f457,f1427]) ).
fof(f1807,plain,
! [X0] :
( ~ sQ93_spl
| ~ product(X0,e_5,e_1)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f457,f121]) ).
fof(f1808,plain,
! [X0] :
( ~ sQ93_spl
| equalish(e_5,X0)
| ~ product(e_2,X0,e_1) ),
inference(resolution,[status(thm)],[f457,f119]) ).
fof(f1809,plain,
! [X0] :
( ~ sQ93_spl
| ~ product(e_5,e_2,X0)
| product(e_1,X0,e_2) ),
inference(resolution,[status(thm)],[f457,f124]) ).
fof(f1810,plain,
( ~ sQ56_spl
| ~ sQ96_spl
| product(e_3,e_3,e_4) ),
inference(resolution,[status(thm)],[f467,f1315]) ).
fof(f1812,plain,
! [X0] :
( ~ sQ96_spl
| equalish(e_2,X0)
| ~ product(X0,e_4,e_3) ),
inference(resolution,[status(thm)],[f467,f121]) ).
fof(f1814,plain,
! [X0] :
( ~ sQ96_spl
| ~ product(e_4,e_2,X0)
| product(e_3,X0,e_2) ),
inference(resolution,[status(thm)],[f467,f124]) ).
fof(f1815,plain,
( ~ sQ51_spl
| ~ sQ81_spl
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[f419,f1308]) ).
fof(f1816,plain,
( ~ sQ71_spl
| ~ sQ81_spl
| equalish(e_5,e_2) ),
inference(resolution,[status(thm)],[f419,f1627]) ).
fof(f1817,plain,
( ~ sQ81_spl
| ~ greater(e_3,e_2)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[f419,f87]) ).
fof(f1818,plain,
! [X0] :
( ~ sQ81_spl
| ~ product(e_2,e_1,X0)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f419,f117]) ).
fof(f1822,plain,
( ~ sQ71_spl
| ~ sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1816,f112]) ).
fof(f1823,plain,
( ~ sQ71_spl
| ~ sQ81_spl ),
inference(contradiction_clause,[status(thm)],[f1822]) ).
fof(f1824,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| ~ greater(e_5,e_3)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[f1805,f87]) ).
fof(f1826,plain,
! [X0] :
( ~ sQ66_spl
| ~ sQ93_spl
| ~ product(X0,e_1,e_5)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f1805,f121]) ).
fof(f1829,definition,
( sQ202_spl
<=> greater(e_5,e_3) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f1831,plain,
( sQ202_spl
| ~ greater(e_5,e_3) ),
inference(component_clause,[status(thm)],[f1829]) ).
fof(f1832,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ202_spl
| ~ sQ123_spl ),
inference(split_clause,[status(thm)],[f1824,f558,f1829,f456,f366]) ).
fof(f1833,plain,
( sQ202_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1831,f77]) ).
fof(f1834,plain,
sQ202_spl,
inference(contradiction_clause,[status(thm)],[f1833]) ).
fof(f1835,plain,
( ~ sQ56_spl
| ~ sQ96_spl
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[f1810,f165]) ).
fof(f1841,plain,
( ~ sQ56_spl
| ~ sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1835,f105]) ).
fof(f1842,plain,
( ~ sQ56_spl
| ~ sQ96_spl ),
inference(contradiction_clause,[status(thm)],[f1841]) ).
fof(f1857,plain,
( ~ sQ82_spl
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[f422,f160]) ).
fof(f1861,plain,
( ~ sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1857,f99]) ).
fof(f1862,plain,
~ sQ82_spl,
inference(contradiction_clause,[status(thm)],[f1861]) ).
fof(f1868,plain,
( ~ sQ97_spl
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[f470,f160]) ).
fof(f1872,plain,
( ~ sQ97_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1868,f101]) ).
fof(f1873,plain,
~ sQ97_spl,
inference(contradiction_clause,[status(thm)],[f1872]) ).
fof(f1874,plain,
( ~ sQ94_spl
| ~ sQ66_spl
| ~ sQ19_spl
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[f1099,f1795]) ).
fof(f1875,plain,
( ~ sQ94_spl
| ~ sQ66_spl
| ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1874,f96]) ).
fof(f1876,plain,
( ~ sQ94_spl
| ~ sQ66_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f1875]) ).
fof(f1877,plain,
( ~ sQ51_spl
| ~ sQ84_spl
| product(e_4,e_4,e_1) ),
inference(resolution,[status(thm)],[f428,f1308]) ).
fof(f1878,plain,
( ~ sQ84_spl
| ~ greater(e_4,e_2)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[f428,f87]) ).
fof(f1879,plain,
! [X0] :
( ~ sQ84_spl
| ~ product(e_2,e_1,X0)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f428,f117]) ).
fof(f1880,plain,
! [X0] :
( ~ sQ84_spl
| equalish(e_2,X0)
| ~ product(X0,e_1,e_4) ),
inference(resolution,[status(thm)],[f428,f121]) ).
fof(f1882,plain,
! [X0] :
( ~ sQ84_spl
| ~ product(e_1,e_2,X0)
| product(e_4,X0,e_2) ),
inference(resolution,[status(thm)],[f428,f124]) ).
fof(f1883,definition,
( sQ203_spl
<=> greater(e_4,e_2) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f1885,plain,
( sQ203_spl
| ~ greater(e_4,e_2) ),
inference(component_clause,[status(thm)],[f1883]) ).
fof(f1886,plain,
( ~ sQ84_spl
| ~ sQ203_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f1878,f304,f1883,f427]) ).
fof(f1887,plain,
( ~ sQ51_spl
| ~ sQ84_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f1877,f238,f427,f314]) ).
fof(f1888,plain,
( sQ203_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1885,f74]) ).
fof(f1889,plain,
sQ203_spl,
inference(contradiction_clause,[status(thm)],[f1888]) ).
fof(f1893,plain,
( ~ sQ83_spl
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[f425,f163]) ).
fof(f1902,plain,
( ~ sQ83_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1893,f95]) ).
fof(f1903,plain,
~ sQ83_spl,
inference(contradiction_clause,[status(thm)],[f1902]) ).
fof(f1914,plain,
! [X0] :
( ~ sQ17_spl
| ~ sQ24_spl
| ~ product(e_2,X0,e_1)
| equalish(e_5,X0) ),
inference(resolution,[status(thm)],[f1179,f119]) ).
fof(f1941,plain,
( ~ sQ56_spl
| ~ sQ100_spl
| product(e_3,e_5,e_4) ),
inference(resolution,[status(thm)],[f479,f1315]) ).
fof(f1943,plain,
! [X0] :
( ~ sQ100_spl
| ~ product(X0,e_4,e_5)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f479,f121]) ).
fof(f1944,plain,
! [X0] :
( ~ sQ100_spl
| ~ product(e_2,X0,e_5)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f479,f119]) ).
fof(f1945,plain,
! [X0] :
( ~ sQ100_spl
| product(e_5,X0,e_2)
| ~ product(e_4,e_2,X0) ),
inference(resolution,[status(thm)],[f479,f124]) ).
fof(f1950,plain,
! [X0] :
( ~ sQ56_spl
| ~ sQ100_spl
| ~ product(e_5,e_3,X0)
| product(e_4,X0,e_3) ),
inference(resolution,[status(thm)],[f1941,f124]) ).
fof(f2002,plain,
( ~ sQ95_spl
| equalish(e_5,e_2) ),
inference(resolution,[status(thm)],[f463,f163]) ).
fof(f2007,plain,
( ~ sQ95_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2002,f112]) ).
fof(f2008,plain,
~ sQ95_spl,
inference(contradiction_clause,[status(thm)],[f2007]) ).
fof(f2009,plain,
( ~ sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1706,f100]) ).
fof(f2010,plain,
~ sQ86_spl,
inference(contradiction_clause,[status(thm)],[f2009]) ).
fof(f2014,plain,
( ~ sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1699,f102]) ).
fof(f2015,plain,
~ sQ92_spl,
inference(contradiction_clause,[status(thm)],[f2014]) ).
fof(f2017,plain,
( ~ sQ88_spl
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[f441,f165]) ).
fof(f2023,plain,
( ~ sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2017,f99]) ).
fof(f2024,plain,
~ sQ88_spl,
inference(contradiction_clause,[status(thm)],[f2023]) ).
fof(f2030,plain,
( ~ sQ90_spl
| product(e_2,e_5,e_2) ),
inference(resolution,[status(thm)],[f447,f161]) ).
fof(f2033,plain,
( ~ sQ90_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f2030,f453,f446]) ).
fof(f2038,plain,
( ~ sQ101_spl
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[f489,f163]) ).
fof(f2043,plain,
( ~ sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2038,f106]) ).
fof(f2044,plain,
~ sQ101_spl,
inference(contradiction_clause,[status(thm)],[f2043]) ).
fof(f2045,plain,
( ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ105_spl
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[f501,f1950]) ).
fof(f2046,plain,
( ~ sQ65_spl
| ~ sQ105_spl
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[f501,f1597]) ).
fof(f2048,plain,
! [X0] :
( ~ sQ105_spl
| equalish(e_5,X0)
| ~ product(X0,e_3,e_1) ),
inference(resolution,[status(thm)],[f501,f121]) ).
fof(f2050,plain,
! [X0] :
( ~ sQ105_spl
| ~ product(e_3,e_5,X0)
| product(e_1,X0,e_5) ),
inference(resolution,[status(thm)],[f501,f124]) ).
fof(f2051,plain,
( ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ105_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f2045,f210,f500,f478,f330]) ).
fof(f2052,plain,
( ~ sQ65_spl
| ~ sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2046,f109]) ).
fof(f2053,plain,
( ~ sQ65_spl
| ~ sQ105_spl ),
inference(contradiction_clause,[status(thm)],[f2052]) ).
fof(f2054,plain,
( ~ sQ24_spl
| ~ sQ109_spl
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[f514,f1183]) ).
fof(f2058,plain,
! [X0] :
( ~ sQ109_spl
| product(e_5,X0,e_4)
| ~ product(e_3,e_4,X0) ),
inference(resolution,[status(thm)],[f514,f124]) ).
fof(f2059,plain,
( ~ sQ24_spl
| ~ sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2054,f96]) ).
fof(f2060,plain,
( ~ sQ24_spl
| ~ sQ109_spl ),
inference(contradiction_clause,[status(thm)],[f2059]) ).
fof(f2061,plain,
( ~ sQ17_spl
| ~ sQ24_spl
| ~ sQ113_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f527,f1914]) ).
fof(f2065,plain,
! [X0] :
( ~ sQ113_spl
| product(e_1,X0,e_2)
| ~ product(e_3,e_2,X0) ),
inference(resolution,[status(thm)],[f527,f124]) ).
fof(f2066,plain,
( ~ sQ17_spl
| ~ sQ24_spl
| ~ sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2061,f113]) ).
fof(f2067,plain,
( ~ sQ17_spl
| ~ sQ24_spl
| ~ sQ113_spl ),
inference(contradiction_clause,[status(thm)],[f2066]) ).
fof(f2069,plain,
( ~ sQ112_spl
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[f524,f160]) ).
fof(f2073,plain,
( ~ sQ112_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2069,f100]) ).
fof(f2074,plain,
~ sQ112_spl,
inference(contradiction_clause,[status(thm)],[f2073]) ).
fof(f2077,plain,
! [X0] :
( ~ sQ114_spl
| ~ product(X0,e_3,e_4)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f530,f121]) ).
fof(f2083,plain,
( ~ sQ118_spl
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[f543,f160]) ).
fof(f2087,plain,
( ~ sQ118_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2083,f96]) ).
fof(f2088,plain,
~ sQ118_spl,
inference(contradiction_clause,[status(thm)],[f2087]) ).
fof(f2089,plain,
! [X0] :
( ~ sQ110_spl
| equalish(e_1,X0)
| ~ product(e_4,e_3,X0) ),
inference(resolution,[status(thm)],[f517,f117]) ).
fof(f2091,plain,
! [X0] :
( ~ sQ110_spl
| ~ product(e_4,X0,e_1)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f517,f119]) ).
fof(f2096,plain,
( ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ102_spl
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[f492,f1950]) ).
fof(f2098,plain,
! [X0] :
( ~ sQ102_spl
| equalish(e_5,X0)
| ~ product(X0,e_3,e_2) ),
inference(resolution,[status(thm)],[f492,f121]) ).
fof(f2100,plain,
! [X0] :
( ~ sQ102_spl
| product(e_2,X0,e_5)
| ~ product(e_3,e_5,X0) ),
inference(resolution,[status(thm)],[f492,f124]) ).
fof(f2109,plain,
( ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ102_spl
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[f2100,f1941]) ).
fof(f2123,plain,
( ~ sQ106_spl
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[f505,f163]) ).
fof(f2128,plain,
( ~ sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2123,f105]) ).
fof(f2129,plain,
~ sQ106_spl,
inference(contradiction_clause,[status(thm)],[f2128]) ).
fof(f2130,plain,
( ~ sQ110_spl
| ~ sQ108_spl
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[f511,f2089]) ).
fof(f2131,plain,
( ~ sQ38_spl
| ~ sQ108_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f511,f1242]) ).
fof(f2132,plain,
( ~ sQ102_spl
| ~ sQ108_spl
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[f511,f2098]) ).
fof(f2136,plain,
! [X0] :
( ~ sQ108_spl
| ~ product(e_3,e_4,X0)
| product(e_2,X0,e_4) ),
inference(resolution,[status(thm)],[f511,f124]) ).
fof(f2137,plain,
( ~ sQ110_spl
| ~ sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2130,f95]) ).
fof(f2138,plain,
( ~ sQ110_spl
| ~ sQ108_spl ),
inference(contradiction_clause,[status(thm)],[f2137]) ).
fof(f2139,plain,
( ~ sQ54_spl
| ~ sQ119_spl
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[f546,f1344]) ).
fof(f2143,plain,
! [X0] :
( ~ sQ119_spl
| product(e_5,X0,e_1)
| ~ product(e_3,e_1,X0) ),
inference(resolution,[status(thm)],[f546,f124]) ).
fof(f2144,plain,
( ~ sQ54_spl
| ~ sQ119_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2139,f100]) ).
fof(f2145,plain,
( ~ sQ54_spl
| ~ sQ119_spl ),
inference(contradiction_clause,[status(thm)],[f2144]) ).
fof(f2146,plain,
( ~ sQ100_spl
| ~ sQ115_spl
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[f533,f1944]) ).
fof(f2149,plain,
! [X0] :
( ~ sQ115_spl
| equalish(e_3,X0)
| ~ product(e_2,X0,e_5) ),
inference(resolution,[status(thm)],[f533,f119]) ).
fof(f2151,plain,
( ~ sQ100_spl
| ~ sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2146,f109]) ).
fof(f2152,plain,
( ~ sQ100_spl
| ~ sQ115_spl ),
inference(contradiction_clause,[status(thm)],[f2151]) ).
fof(f2153,plain,
( ~ sQ111_spl
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[f521,f163]) ).
fof(f2158,plain,
( ~ sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2153,f104]) ).
fof(f2159,plain,
~ sQ111_spl,
inference(contradiction_clause,[status(thm)],[f2158]) ).
fof(f2160,plain,
( ~ sQ38_spl
| ~ sQ61_spl
| sQ114_spl ),
inference(split_clause,[status(thm)],[f1552,f529,f350,f268]) ).
fof(f2161,plain,
( ~ sQ31_spl
| ~ sQ116_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f537,f1213]) ).
fof(f2164,plain,
! [X0] :
( ~ sQ116_spl
| ~ product(e_1,X0,e_4)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f537,f119]) ).
fof(f2165,plain,
! [X0] :
( ~ sQ116_spl
| ~ product(e_3,e_1,X0)
| product(e_4,X0,e_1) ),
inference(resolution,[status(thm)],[f537,f124]) ).
fof(f2166,plain,
( ~ sQ31_spl
| ~ sQ116_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2161,f113]) ).
fof(f2167,plain,
( ~ sQ31_spl
| ~ sQ116_spl ),
inference(contradiction_clause,[status(thm)],[f2166]) ).
fof(f2170,plain,
( ~ sQ104_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f498,f160]) ).
fof(f2176,plain,
( ~ sQ68_spl
| ~ sQ103_spl
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[f495,f1577]) ).
fof(f2179,plain,
! [X0] :
( ~ sQ103_spl
| equalish(e_3,X0)
| ~ product(e_5,X0,e_4) ),
inference(resolution,[status(thm)],[f495,f119]) ).
fof(f2180,plain,
! [X0] :
( ~ sQ103_spl
| product(e_4,X0,e_5)
| ~ product(e_3,e_5,X0) ),
inference(resolution,[status(thm)],[f495,f124]) ).
fof(f2181,plain,
( ~ sQ68_spl
| ~ sQ103_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2176,f100]) ).
fof(f2182,plain,
( ~ sQ68_spl
| ~ sQ103_spl ),
inference(contradiction_clause,[status(thm)],[f2181]) ).
fof(f2183,plain,
( ~ sQ102_spl
| ~ sQ117_spl
| equalish(e_5,e_1) ),
inference(resolution,[status(thm)],[f540,f2098]) ).
fof(f2187,plain,
! [X0] :
( ~ sQ117_spl
| ~ product(e_3,e_1,X0)
| product(e_2,X0,e_1) ),
inference(resolution,[status(thm)],[f540,f124]) ).
fof(f2188,plain,
( ~ sQ102_spl
| ~ sQ117_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2183,f111]) ).
fof(f2189,plain,
( ~ sQ102_spl
| ~ sQ117_spl ),
inference(contradiction_clause,[status(thm)],[f2188]) ).
fof(f2191,plain,
( ~ sQ107_spl
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[f508,f160]) ).
fof(f2195,plain,
( ~ sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2191,f109]) ).
fof(f2196,plain,
~ sQ107_spl,
inference(contradiction_clause,[status(thm)],[f2195]) ).
fof(f2197,plain,
( ~ sQ102_spl
| ~ sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2132,f114]) ).
fof(f2198,plain,
( ~ sQ102_spl
| ~ sQ108_spl ),
inference(contradiction_clause,[status(thm)],[f2197]) ).
fof(f2200,plain,
( ~ sQ120_spl
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[f549,f163]) ).
fof(f2210,plain,
( ~ sQ140_spl
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[f618,f160]) ).
fof(f2216,plain,
( ~ sQ109_spl
| ~ sQ129_spl
| product(e_5,e_2,e_4) ),
inference(resolution,[status(thm)],[f583,f2058]) ).
fof(f2220,plain,
! [X0] :
( ~ sQ129_spl
| product(e_2,X0,e_3)
| ~ product(e_4,e_3,X0) ),
inference(resolution,[status(thm)],[f583,f124]) ).
fof(f2221,plain,
( ~ sQ93_spl
| ~ sQ109_spl
| ~ sQ129_spl
| product(e_1,e_4,e_2) ),
inference(resolution,[status(thm)],[f2216,f1809]) ).
fof(f2229,plain,
( ~ sQ93_spl
| ~ sQ109_spl
| ~ sQ129_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f2221,f195,f582,f513,f456]) ).
fof(f2230,plain,
( ~ sQ113_spl
| ~ sQ142_spl
| product(e_1,e_5,e_2) ),
inference(resolution,[status(thm)],[f625,f2065]) ).
fof(f2232,plain,
! [X0] :
( ~ sQ142_spl
| ~ product(X0,e_2,e_5)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f625,f121]) ).
fof(f2233,plain,
! [X0] :
( ~ sQ142_spl
| ~ product(e_3,X0,e_5)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f625,f119]) ).
fof(f2234,plain,
! [X0] :
( ~ sQ142_spl
| product(e_5,X0,e_3)
| ~ product(e_2,e_3,X0) ),
inference(resolution,[status(thm)],[f625,f124]) ).
fof(f2235,plain,
( ~ sQ113_spl
| ~ sQ142_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f2230,f249,f624,f526]) ).
fof(f2236,plain,
( ~ sQ102_spl
| ~ sQ136_spl
| product(e_2,e_1,e_5) ),
inference(resolution,[status(thm)],[f606,f2100]) ).
fof(f2238,plain,
! [X0] :
( ~ sQ136_spl
| ~ product(X0,e_5,e_1)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f606,f121]) ).
fof(f2240,plain,
! [X0] :
( ~ sQ136_spl
| product(e_1,X0,e_3)
| ~ product(e_5,e_3,X0) ),
inference(resolution,[status(thm)],[f606,f124]) ).
fof(f2242,plain,
( ~ sQ84_spl
| ~ sQ102_spl
| ~ sQ136_spl
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[f2236,f1879]) ).
fof(f2243,plain,
( ~ sQ102_spl
| ~ sQ136_spl
| ~ greater(e_5,e_2)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[f2236,f87]) ).
fof(f2248,plain,
( ~ sQ102_spl
| ~ sQ136_spl
| ~ sQ201_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f2243,f304,f1768,f605,f491]) ).
fof(f2249,plain,
( ~ sQ84_spl
| ~ sQ102_spl
| ~ sQ136_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2242,f110]) ).
fof(f2250,plain,
( ~ sQ84_spl
| ~ sQ102_spl
| ~ sQ136_spl ),
inference(contradiction_clause,[status(thm)],[f2249]) ).
fof(f2253,plain,
( ~ sQ130_spl
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[f586,f160]) ).
fof(f2258,plain,
( ~ sQ130_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2253,f105]) ).
fof(f2259,plain,
~ sQ130_spl,
inference(contradiction_clause,[status(thm)],[f2258]) ).
fof(f2264,plain,
( ~ sQ145_spl
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[f634,f160]) ).
fof(f2275,plain,
( ~ sQ135_spl
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[f602,f160]) ).
fof(f2281,plain,
( ~ sQ116_spl
| ~ sQ132_spl
| product(e_4,e_5,e_1) ),
inference(resolution,[status(thm)],[f593,f2165]) ).
fof(f2282,plain,
( ~ sQ132_spl
| ~ greater(e_5,e_3)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[f593,f87]) ).
fof(f2285,plain,
! [X0] :
( ~ sQ132_spl
| equalish(e_1,X0)
| ~ product(e_3,X0,e_5) ),
inference(resolution,[status(thm)],[f593,f119]) ).
fof(f2286,plain,
! [X0] :
( ~ sQ132_spl
| ~ product(e_1,e_3,X0)
| product(e_5,X0,e_3) ),
inference(resolution,[status(thm)],[f593,f124]) ).
fof(f2287,plain,
( ~ sQ116_spl
| ~ sQ132_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f2281,f274,f592,f536]) ).
fof(f2288,plain,
( ~ sQ132_spl
| ~ sQ202_spl
| ~ sQ123_spl ),
inference(split_clause,[status(thm)],[f2282,f558,f1829,f592]) ).
fof(f2291,plain,
( ~ sQ131_spl
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[f590,f163]) ).
fof(f2301,plain,
( ~ sQ131_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2291,f96]) ).
fof(f2302,plain,
~ sQ131_spl,
inference(contradiction_clause,[status(thm)],[f2301]) ).
fof(f2303,plain,
( ~ sQ113_spl
| ~ sQ143_spl
| product(e_1,e_4,e_2) ),
inference(resolution,[status(thm)],[f628,f2065]) ).
fof(f2304,plain,
( ~ sQ68_spl
| ~ sQ143_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f628,f1576]) ).
fof(f2306,plain,
! [X0] :
( ~ sQ143_spl
| ~ product(X0,e_2,e_4)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f628,f121]) ).
fof(f2308,plain,
! [X0] :
( ~ sQ143_spl
| product(e_4,X0,e_3)
| ~ product(e_2,e_3,X0) ),
inference(resolution,[status(thm)],[f628,f124]) ).
fof(f2309,plain,
( ~ sQ113_spl
| ~ sQ143_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f2303,f195,f627,f526]) ).
fof(f2310,plain,
( ~ sQ68_spl
| ~ sQ143_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2304,f113]) ).
fof(f2311,plain,
( ~ sQ68_spl
| ~ sQ143_spl ),
inference(contradiction_clause,[status(thm)],[f2310]) ).
fof(f2312,plain,
( ~ sQ109_spl
| ~ sQ126_spl
| product(e_5,e_1,e_4) ),
inference(resolution,[status(thm)],[f574,f2058]) ).
fof(f2313,plain,
( ~ sQ65_spl
| ~ sQ126_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f574,f1596]) ).
fof(f2314,plain,
( ~ sQ98_spl
| ~ sQ126_spl
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[f574,f1729]) ).
fof(f2317,plain,
! [X0] :
( ~ sQ126_spl
| ~ product(e_3,X0,e_1)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f574,f119]) ).
fof(f2318,plain,
! [X0] :
( ~ sQ126_spl
| ~ product(e_4,e_3,X0)
| product(e_1,X0,e_3) ),
inference(resolution,[status(thm)],[f574,f124]) ).
fof(f2319,plain,
( ~ sQ65_spl
| ~ sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2313,f113]) ).
fof(f2320,plain,
( ~ sQ65_spl
| ~ sQ126_spl ),
inference(contradiction_clause,[status(thm)],[f2319]) ).
fof(f2322,plain,
( ~ sQ149_spl
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[f647,f165]) ).
fof(f2329,plain,
( ~ sQ149_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2322,f104]) ).
fof(f2330,plain,
~ sQ149_spl,
inference(contradiction_clause,[status(thm)],[f2329]) ).
fof(f2335,plain,
( ~ sQ147_spl
| product(e_3,e_5,e_3) ),
inference(resolution,[status(thm)],[f641,f161]) ).
fof(f2338,plain,
( ~ sQ147_spl
| sQ140_spl ),
inference(split_clause,[status(thm)],[f2335,f617,f640]) ).
fof(f2342,plain,
( ~ sQ137_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f609,f163]) ).
fof(f2347,plain,
( ~ sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2342,f113]) ).
fof(f2348,plain,
~ sQ137_spl,
inference(contradiction_clause,[status(thm)],[f2347]) ).
fof(f2350,plain,
( ~ sQ148_spl
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[f644,f165]) ).
fof(f2356,plain,
( ~ sQ148_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2350,f105]) ).
fof(f2357,plain,
~ sQ148_spl,
inference(contradiction_clause,[status(thm)],[f2356]) ).
fof(f2358,plain,
( ~ sQ116_spl
| ~ sQ134_spl
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[f599,f2165]) ).
fof(f2359,plain,
( ~ sQ23_spl
| ~ sQ134_spl
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[f599,f1154]) ).
fof(f2364,plain,
! [X0] :
( ~ sQ134_spl
| ~ product(e_1,e_3,X0)
| product(e_2,X0,e_3) ),
inference(resolution,[status(thm)],[f599,f124]) ).
fof(f2369,plain,
( ~ sQ23_spl
| ~ sQ134_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2359,f109]) ).
fof(f2370,plain,
( ~ sQ23_spl
| ~ sQ134_spl ),
inference(contradiction_clause,[status(thm)],[f2369]) ).
fof(f2371,plain,
( ~ sQ59_spl
| ~ sQ98_spl
| ~ sQ198_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1736,f284,f1659,f472,f339]) ).
fof(f2381,plain,
( ~ sQ71_spl
| ~ sQ59_spl
| ~ sQ98_spl
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[f1727,f1626]) ).
fof(f2383,plain,
( ~ sQ68_spl
| ~ sQ59_spl
| ~ sQ98_spl
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[f1727,f1577]) ).
fof(f2391,plain,
( ~ sQ71_spl
| ~ sQ59_spl
| ~ sQ98_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2381,f105]) ).
fof(f2392,plain,
( ~ sQ71_spl
| ~ sQ59_spl
| ~ sQ98_spl ),
inference(contradiction_clause,[status(thm)],[f2391]) ).
fof(f2394,plain,
( ~ sQ128_spl
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[f580,f163]) ).
fof(f2399,plain,
( ~ sQ128_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2394,f109]) ).
fof(f2400,plain,
~ sQ128_spl,
inference(contradiction_clause,[status(thm)],[f2399]) ).
fof(f2401,plain,
( ~ sQ109_spl
| ~ sQ127_spl
| product(e_5,e_5,e_4) ),
inference(resolution,[status(thm)],[f577,f2058]) ).
fof(f2402,plain,
( ~ sQ132_spl
| ~ sQ127_spl
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[f577,f2285]) ).
fof(f2403,plain,
( ~ sQ100_spl
| ~ sQ127_spl
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[f577,f1943]) ).
fof(f2404,plain,
( ~ sQ19_spl
| ~ sQ127_spl
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[f577,f1099]) ).
fof(f2408,plain,
! [X0] :
( ~ sQ127_spl
| ~ product(e_4,e_3,X0)
| product(e_5,X0,e_3) ),
inference(resolution,[status(thm)],[f577,f124]) ).
fof(f2409,plain,
( ~ sQ132_spl
| ~ sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2402,f97]) ).
fof(f2410,plain,
( ~ sQ132_spl
| ~ sQ127_spl ),
inference(contradiction_clause,[status(thm)],[f2409]) ).
fof(f2411,plain,
( ~ sQ109_spl
| ~ sQ127_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f2401,f404,f576,f513]) ).
fof(f2412,plain,
( ~ sQ19_spl
| ~ sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2404,f96]) ).
fof(f2413,plain,
( ~ sQ19_spl
| ~ sQ127_spl ),
inference(contradiction_clause,[status(thm)],[f2412]) ).
fof(f2414,plain,
( ~ sQ140_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2210,f106]) ).
fof(f2415,plain,
~ sQ140_spl,
inference(contradiction_clause,[status(thm)],[f2414]) ).
fof(f2420,plain,
! [X0] :
( ~ sQ32_spl
| ~ sQ71_spl
| ~ product(X0,e_3,e_1)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f1622,f121]) ).
fof(f2432,plain,
( ~ sQ144_spl
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[f631,f163]) ).
fof(f2438,plain,
( ~ sQ144_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2432,f100]) ).
fof(f2439,plain,
~ sQ144_spl,
inference(contradiction_clause,[status(thm)],[f2438]) ).
fof(f2440,plain,
( ~ sQ103_spl
| ~ sQ138_spl
| product(e_4,e_4,e_5) ),
inference(resolution,[status(thm)],[f612,f2180]) ).
fof(f2442,plain,
! [X0] :
( ~ sQ138_spl
| ~ product(X0,e_5,e_4)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f612,f121]) ).
fof(f2445,plain,
( ~ sQ103_spl
| ~ sQ138_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f2440,f235,f611,f494]) ).
fof(f2447,plain,
( ~ sQ84_spl
| ~ sQ133_spl
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[f596,f1880]) ).
fof(f2450,plain,
! [X0] :
( ~ sQ133_spl
| ~ product(X0,e_1,e_4)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f596,f121]) ).
fof(f2451,plain,
! [X0] :
( ~ sQ133_spl
| equalish(e_1,X0)
| ~ product(e_3,X0,e_4) ),
inference(resolution,[status(thm)],[f596,f119]) ).
fof(f2452,plain,
! [X0] :
( ~ sQ133_spl
| ~ product(e_1,e_3,X0)
| product(e_4,X0,e_3) ),
inference(resolution,[status(thm)],[f596,f124]) ).
fof(f2454,plain,
( ~ sQ84_spl
| ~ sQ133_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2447,f100]) ).
fof(f2455,plain,
( ~ sQ84_spl
| ~ sQ133_spl ),
inference(contradiction_clause,[status(thm)],[f2454]) ).
fof(f2456,plain,
( ~ sQ98_spl
| ~ sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2314,f100]) ).
fof(f2457,plain,
( ~ sQ98_spl
| ~ sQ126_spl ),
inference(contradiction_clause,[status(thm)],[f2456]) ).
fof(f2458,plain,
( ~ sQ38_spl
| ~ sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2131,f113]) ).
fof(f2459,plain,
( ~ sQ38_spl
| ~ sQ108_spl ),
inference(contradiction_clause,[status(thm)],[f2458]) ).
fof(f2460,plain,
( ~ sQ71_spl
| ~ sQ109_spl
| ~ sQ126_spl
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[f2312,f1626]) ).
fof(f2462,plain,
( ~ sQ84_spl
| ~ sQ109_spl
| ~ sQ126_spl
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[f2312,f1880]) ).
fof(f2468,plain,
( ~ sQ71_spl
| ~ sQ109_spl
| ~ sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2460,f105]) ).
fof(f2469,plain,
( ~ sQ71_spl
| ~ sQ109_spl
| ~ sQ126_spl ),
inference(contradiction_clause,[status(thm)],[f2468]) ).
fof(f2470,plain,
( ~ sQ32_spl
| ~ sQ71_spl
| sQ113_spl ),
inference(split_clause,[status(thm)],[f1622,f526,f382,f249]) ).
fof(f2471,plain,
( ~ sQ117_spl
| ~ sQ66_spl
| ~ sQ93_spl
| product(e_2,e_5,e_1) ),
inference(resolution,[status(thm)],[f1805,f2187]) ).
fof(f2481,plain,
! [X0] :
( ~ sQ117_spl
| ~ sQ66_spl
| ~ sQ93_spl
| equalish(e_5,X0)
| ~ product(e_2,X0,e_1) ),
inference(resolution,[status(thm)],[f2471,f119]) ).
fof(f2500,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ116_spl
| product(e_4,e_5,e_1) ),
inference(resolution,[status(thm)],[f2165,f1805]) ).
fof(f2501,plain,
( ~ sQ126_spl
| ~ sQ141_spl
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[f622,f2317]) ).
fof(f2503,plain,
! [X0] :
( ~ sQ141_spl
| equalish(e_3,X0)
| ~ product(X0,e_2,e_1) ),
inference(resolution,[status(thm)],[f622,f121]) ).
fof(f2504,plain,
! [X0] :
( ~ sQ141_spl
| ~ product(e_3,X0,e_1)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f622,f119]) ).
fof(f2505,plain,
! [X0] :
( ~ sQ141_spl
| product(e_1,X0,e_3)
| ~ product(e_2,e_3,X0) ),
inference(resolution,[status(thm)],[f622,f124]) ).
fof(f2506,plain,
( ~ sQ126_spl
| ~ sQ141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2501,f108]) ).
fof(f2507,plain,
( ~ sQ126_spl
| ~ sQ141_spl ),
inference(contradiction_clause,[status(thm)],[f2506]) ).
fof(f2514,plain,
( ~ sQ103_spl
| ~ sQ139_spl
| product(e_4,e_2,e_5) ),
inference(resolution,[status(thm)],[f615,f2180]) ).
fof(f2517,plain,
! [X0] :
( ~ sQ139_spl
| equalish(e_5,X0)
| ~ product(e_3,X0,e_2) ),
inference(resolution,[status(thm)],[f615,f119]) ).
fof(f2519,plain,
( ~ sQ100_spl
| ~ sQ103_spl
| ~ sQ139_spl
| product(e_5,e_5,e_2) ),
inference(resolution,[status(thm)],[f2514,f1945]) ).
fof(f2522,plain,
( ~ sQ54_spl
| ~ sQ103_spl
| ~ sQ139_spl
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[f2514,f1343]) ).
fof(f2528,plain,
( ~ sQ100_spl
| ~ sQ103_spl
| ~ sQ139_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f2519,f401,f614,f494,f478]) ).
fof(f2529,plain,
( ~ sQ54_spl
| ~ sQ103_spl
| ~ sQ139_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2522,f97]) ).
fof(f2530,plain,
( ~ sQ54_spl
| ~ sQ103_spl
| ~ sQ139_spl ),
inference(contradiction_clause,[status(thm)],[f2529]) ).
fof(f2532,plain,
( ~ sQ126_spl
| ~ sQ146_spl
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[f638,f2317]) ).
fof(f2539,plain,
( ~ sQ126_spl
| ~ sQ146_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2532,f109]) ).
fof(f2540,plain,
( ~ sQ126_spl
| ~ sQ146_spl ),
inference(contradiction_clause,[status(thm)],[f2539]) ).
fof(f2549,definition,
( sQ208_spl
<=> equalish(e_3,e_1) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f2550,plain,
( ~ sQ208_spl
| equalish(e_3,e_1) ),
inference(component_clause,[status(thm)],[f2549]) ).
fof(f2563,definition,
( sQ212_spl
<=> equalish(e_3,e_4) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f2564,plain,
( ~ sQ212_spl
| equalish(e_3,e_4) ),
inference(component_clause,[status(thm)],[f2563]) ).
fof(f2570,definition,
( sQ214_spl
<=> equalish(e_3,e_5) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f2571,plain,
( ~ sQ214_spl
| equalish(e_3,e_5) ),
inference(component_clause,[status(thm)],[f2570]) ).
fof(f2577,definition,
( sQ216_spl
<=> equalish(e_3,e_2) ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f2578,plain,
( ~ sQ216_spl
| equalish(e_3,e_2) ),
inference(component_clause,[status(thm)],[f2577]) ).
fof(f2581,plain,
( ~ sQ208_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2550,f103]) ).
fof(f2582,plain,
~ sQ208_spl,
inference(contradiction_clause,[status(thm)],[f2581]) ).
fof(f2583,plain,
( ~ sQ216_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2578,f104]) ).
fof(f2584,plain,
~ sQ216_spl,
inference(contradiction_clause,[status(thm)],[f2583]) ).
fof(f2585,plain,
( ~ sQ214_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2571,f106]) ).
fof(f2586,plain,
~ sQ214_spl,
inference(contradiction_clause,[status(thm)],[f2585]) ).
fof(f2587,plain,
( ~ sQ212_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2564,f105]) ).
fof(f2588,plain,
~ sQ212_spl,
inference(contradiction_clause,[status(thm)],[f2587]) ).
fof(f2591,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ24_spl
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[f1182,f1805]) ).
fof(f2592,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2591,f109]) ).
fof(f2593,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ24_spl ),
inference(contradiction_clause,[status(thm)],[f2592]) ).
fof(f2594,plain,
( ~ sQ120_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f2200,f2549,f548]) ).
fof(f2603,plain,
! [X0] :
( ~ sQ154_spl
| ~ next(e_1,X0)
| equalish(e_1,X0) ),
inference(resolution,[status(thm)],[f673,f122]) ).
fof(f2613,plain,
( ~ sQ154_spl
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[f2603,f60]) ).
fof(f2614,plain,
( ~ sQ154_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2613,f95]) ).
fof(f2615,plain,
~ sQ154_spl,
inference(contradiction_clause,[status(thm)],[f2614]) ).
fof(f2620,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ next(e_1,X1)
| ~ greater(e_0,e_0)
| ~ product(e_1,e_1,X0)
| equalish(X0,X1) ),
inference(resolution,[status(thm)],[f134,f89]) ).
fof(f2622,plain,
( ~ sQ2_spl
| ~ sQ152_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f2620,f672,f657,f133]) ).
fof(f2629,plain,
( ~ sQ54_spl
| ~ sQ8_spl
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[f154,f1344]) ).
fof(f2630,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ8_spl
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[f154,f1826]) ).
fof(f2638,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ8_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f2630,f2549,f153,f456,f366]) ).
fof(f2639,plain,
( ~ sQ54_spl
| ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2629,f99]) ).
fof(f2640,plain,
( ~ sQ54_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f2639]) ).
fof(f2641,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ116_spl
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[f1807,f2500]) ).
fof(f2642,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ116_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2641,f101]) ).
fof(f2643,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ116_spl ),
inference(contradiction_clause,[status(thm)],[f2642]) ).
fof(f2644,plain,
( ~ sQ94_spl
| ~ sQ66_spl
| sQ127_spl ),
inference(split_clause,[status(thm)],[f1795,f576,f366,f459]) ).
fof(f2668,definition,
( sQ223_spl
<=> next(e_4,e_5) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f2670,plain,
( sQ223_spl
| ~ next(e_4,e_5) ),
inference(component_clause,[status(thm)],[f2668]) ).
fof(f2676,plain,
( sQ223_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2670,f63]) ).
fof(f2677,plain,
sQ223_spl,
inference(contradiction_clause,[status(thm)],[f2676]) ).
fof(f2720,definition,
( sQ230_spl
<=> equalish(e_2,e_3) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f2721,plain,
( ~ sQ230_spl
| equalish(e_2,e_3) ),
inference(component_clause,[status(thm)],[f2720]) ).
fof(f2727,definition,
( sQ232_spl
<=> equalish(e_2,e_5) ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f2728,plain,
( ~ sQ232_spl
| equalish(e_2,e_5) ),
inference(component_clause,[status(thm)],[f2727]) ).
fof(f2734,definition,
( sQ234_spl
<=> equalish(e_2,e_1) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f2735,plain,
( ~ sQ234_spl
| equalish(e_2,e_1) ),
inference(component_clause,[status(thm)],[f2734]) ).
fof(f2741,definition,
( sQ236_spl
<=> equalish(e_2,e_4) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f2742,plain,
( ~ sQ236_spl
| equalish(e_2,e_4) ),
inference(component_clause,[status(thm)],[f2741]) ).
fof(f2752,plain,
( ~ sQ234_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2735,f99]) ).
fof(f2753,plain,
~ sQ234_spl,
inference(contradiction_clause,[status(thm)],[f2752]) ).
fof(f2754,plain,
( ~ sQ230_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2721,f100]) ).
fof(f2755,plain,
~ sQ230_spl,
inference(contradiction_clause,[status(thm)],[f2754]) ).
fof(f2756,plain,
( ~ sQ232_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2728,f102]) ).
fof(f2757,plain,
~ sQ232_spl,
inference(contradiction_clause,[status(thm)],[f2756]) ).
fof(f2758,plain,
( ~ sQ236_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2742,f101]) ).
fof(f2759,plain,
~ sQ236_spl,
inference(contradiction_clause,[status(thm)],[f2758]) ).
fof(f2795,definition,
( sQ241_spl
<=> equalish(e_1,e_4) ),
introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition]) ).
fof(f2796,plain,
( ~ sQ241_spl
| equalish(e_1,e_4) ),
inference(component_clause,[status(thm)],[f2795]) ).
fof(f2803,definition,
( sQ243_spl
<=> equalish(e_1,e_2) ),
introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition]) ).
fof(f2804,plain,
( ~ sQ243_spl
| equalish(e_1,e_2) ),
inference(component_clause,[status(thm)],[f2803]) ).
fof(f2807,definition,
( sQ244_spl
<=> equalish(e_1,e_5) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f2808,plain,
( ~ sQ244_spl
| equalish(e_1,e_5) ),
inference(component_clause,[status(thm)],[f2807]) ).
fof(f2811,definition,
( sQ245_spl
<=> equalish(e_1,e_3) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f2812,plain,
( ~ sQ245_spl
| equalish(e_1,e_3) ),
inference(component_clause,[status(thm)],[f2811]) ).
fof(f2815,plain,
( ~ sQ244_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2808,f98]) ).
fof(f2816,plain,
~ sQ244_spl,
inference(contradiction_clause,[status(thm)],[f2815]) ).
fof(f2817,plain,
( ~ sQ241_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2796,f97]) ).
fof(f2818,plain,
~ sQ241_spl,
inference(contradiction_clause,[status(thm)],[f2817]) ).
fof(f2819,plain,
( ~ sQ245_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2812,f96]) ).
fof(f2820,plain,
~ sQ245_spl,
inference(contradiction_clause,[status(thm)],[f2819]) ).
fof(f2821,plain,
( ~ sQ243_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2804,f95]) ).
fof(f2822,plain,
~ sQ243_spl,
inference(contradiction_clause,[status(thm)],[f2821]) ).
fof(f2881,definition,
( sQ253_spl
<=> equalish(e_4,e_1) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f2882,plain,
( ~ sQ253_spl
| equalish(e_4,e_1) ),
inference(component_clause,[status(thm)],[f2881]) ).
fof(f2889,definition,
( sQ255_spl
<=> equalish(e_4,e_3) ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f2890,plain,
( ~ sQ255_spl
| equalish(e_4,e_3) ),
inference(component_clause,[status(thm)],[f2889]) ).
fof(f2893,definition,
( sQ256_spl
<=> equalish(e_4,e_2) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f2894,plain,
( ~ sQ256_spl
| equalish(e_4,e_2) ),
inference(component_clause,[status(thm)],[f2893]) ).
fof(f2897,definition,
( sQ257_spl
<=> equalish(e_4,e_5) ),
introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition]) ).
fof(f2898,plain,
( ~ sQ257_spl
| equalish(e_4,e_5) ),
inference(component_clause,[status(thm)],[f2897]) ).
fof(f2901,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f286,f82]) ).
fof(f2902,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f2901]) ).
fof(f2903,plain,
( ~ sQ256_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2894,f108]) ).
fof(f2904,plain,
~ sQ256_spl,
inference(contradiction_clause,[status(thm)],[f2903]) ).
fof(f2905,plain,
( ~ sQ255_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2890,f109]) ).
fof(f2906,plain,
~ sQ255_spl,
inference(contradiction_clause,[status(thm)],[f2905]) ).
fof(f2907,plain,
( ~ sQ257_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2898,f110]) ).
fof(f2908,plain,
~ sQ257_spl,
inference(contradiction_clause,[status(thm)],[f2907]) ).
fof(f2909,plain,
( ~ sQ100_spl
| ~ sQ127_spl
| sQ230_spl ),
inference(split_clause,[status(thm)],[f2403,f2720,f576,f478]) ).
fof(f2910,plain,
( ~ sQ253_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2882,f107]) ).
fof(f2911,plain,
~ sQ253_spl,
inference(contradiction_clause,[status(thm)],[f2910]) ).
fof(f2912,plain,
( ~ sQ66_spl
| ~ sQ93_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f1805,f592,f456,f366]) ).
fof(f2913,definition,
( sQ258_spl
<=> greater(e_3,e_2) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f2915,plain,
( sQ258_spl
| ~ greater(e_3,e_2) ),
inference(component_clause,[status(thm)],[f2913]) ).
fof(f2916,plain,
( ~ sQ81_spl
| ~ sQ258_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f1817,f304,f2913,f418]) ).
fof(f2917,plain,
( ~ sQ51_spl
| ~ sQ81_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f1815,f516,f418,f314]) ).
fof(f2918,plain,
( sQ258_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2915,f73]) ).
fof(f2919,plain,
sQ258_spl,
inference(contradiction_clause,[status(thm)],[f2918]) ).
fof(f2922,plain,
! [X0] :
( ~ sQ50_spl
| ~ greater(X0,e_2)
| ~ greater(e_3,e_0)
| ~ cycle(X0,e_0)
| ~ next(X0,e_5) ),
inference(resolution,[status(thm)],[f311,f662]) ).
fof(f2937,plain,
( ~ sQ50_spl
| ~ sQ155_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f2922,f945,f675,f310]) ).
fof(f2993,definition,
( sQ266_spl
<=> next(e_2,e_3) ),
introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition]) ).
fof(f2995,plain,
( sQ266_spl
| ~ next(e_2,e_3) ),
inference(component_clause,[status(thm)],[f2993]) ).
fof(f3004,plain,
( sQ266_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2995,f61]) ).
fof(f3005,plain,
sQ266_spl,
inference(contradiction_clause,[status(thm)],[f3004]) ).
fof(f3260,definition,
( sQ290_spl
<=> next(e_3,e_4) ),
introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition]) ).
fof(f3262,plain,
( sQ290_spl
| ~ next(e_3,e_4) ),
inference(component_clause,[status(thm)],[f3260]) ).
fof(f3272,plain,
( sQ290_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3262,f62]) ).
fof(f3273,plain,
sQ290_spl,
inference(contradiction_clause,[status(thm)],[f3272]) ).
fof(f3391,definition,
( sQ299_spl
<=> next(e_1,e_2) ),
introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition]) ).
fof(f3393,plain,
( sQ299_spl
| ~ next(e_1,e_2) ),
inference(component_clause,[status(thm)],[f3391]) ).
fof(f3395,plain,
( sQ299_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3393,f60]) ).
fof(f3396,plain,
sQ299_spl,
inference(contradiction_clause,[status(thm)],[f3395]) ).
fof(f3470,definition,
( sQ301_spl
<=> greater(e_5,e_1) ),
introduced(definition,[new_symbols(definition,[sQ301_spl])],[split_symbol_definition]) ).
fof(f3472,plain,
( sQ301_spl
| ~ greater(e_5,e_1) ),
inference(component_clause,[status(thm)],[f3470]) ).
fof(f3475,definition,
( sQ302_spl
<=> greater(e_4,e_1) ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f3477,plain,
( sQ302_spl
| ~ greater(e_4,e_1) ),
inference(component_clause,[status(thm)],[f3475]) ).
fof(f3479,plain,
( sQ301_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3472,f72]) ).
fof(f3480,plain,
sQ301_spl,
inference(contradiction_clause,[status(thm)],[f3479]) ).
fof(f3481,plain,
( sQ302_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3477,f71]) ).
fof(f3482,plain,
sQ302_spl,
inference(contradiction_clause,[status(thm)],[f3481]) ).
fof(f3493,plain,
( ~ sQ13_spl
| ~ sQ190_spl
| ~ next(e_4,e_5)
| ~ greater(e_4,e_2) ),
inference(resolution,[status(thm)],[f946,f183]) ).
fof(f3496,plain,
( ~ sQ13_spl
| ~ sQ190_spl
| ~ sQ223_spl
| ~ sQ203_spl ),
inference(split_clause,[status(thm)],[f3493,f1883,f2668,f945,f182]) ).
fof(f3573,plain,
( ~ sQ100_spl
| ~ sQ59_spl
| product(e_5,e_5,e_2) ),
inference(resolution,[status(thm)],[f340,f1945]) ).
fof(f3576,plain,
( ~ sQ142_spl
| ~ sQ59_spl
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[f340,f2232]) ).
fof(f3582,plain,
( ~ sQ100_spl
| ~ sQ59_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f3573,f401,f339,f478]) ).
fof(f3583,plain,
( ~ sQ142_spl
| ~ sQ59_spl
| sQ212_spl ),
inference(split_clause,[status(thm)],[f3576,f2563,f339,f624]) ).
fof(f3585,plain,
( ~ sQ61_spl
| ~ sQ40_spl
| product(e_3,e_1,e_5) ),
inference(resolution,[status(thm)],[f275,f1556]) ).
fof(f3586,plain,
( ~ sQ60_spl
| ~ sQ40_spl
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[f275,f1328]) ).
fof(f3587,plain,
( ~ sQ110_spl
| ~ sQ40_spl
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[f275,f2091]) ).
fof(f3589,plain,
( ~ sQ93_spl
| ~ sQ40_spl
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[f275,f1807]) ).
fof(f3595,plain,
( ~ sQ60_spl
| ~ sQ40_spl
| sQ232_spl ),
inference(split_clause,[status(thm)],[f3586,f2727,f274,f342]) ).
fof(f3596,plain,
( ~ sQ93_spl
| ~ sQ40_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f3589,f2741,f274,f456]) ).
fof(f3597,plain,
( ~ sQ110_spl
| ~ sQ40_spl
| sQ214_spl ),
inference(split_clause,[status(thm)],[f3587,f2570,f274,f516]) ).
fof(f3598,plain,
( ~ sQ116_spl
| ~ sQ134_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f2358,f342,f598,f536]) ).
fof(f3600,plain,
( ~ sQ61_spl
| ~ sQ40_spl
| ~ greater(e_5,e_3)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[f3585,f87]) ).
fof(f3605,plain,
( ~ sQ61_spl
| ~ sQ40_spl
| ~ sQ202_spl
| ~ sQ123_spl ),
inference(split_clause,[status(thm)],[f3600,f558,f1829,f274,f350]) ).
fof(f3606,plain,
( ~ sQ72_spl
| ~ sQ109_spl
| ~ sQ126_spl
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[f2312,f1462]) ).
fof(f3607,plain,
( ~ sQ32_spl
| ~ sQ109_spl
| ~ sQ126_spl
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[f2312,f1275]) ).
fof(f3615,plain,
( ~ sQ72_spl
| ~ sQ109_spl
| ~ sQ126_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f3606,f2741,f573,f513,f385]) ).
fof(f3616,plain,
( ~ sQ32_spl
| ~ sQ109_spl
| ~ sQ126_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f3607,f472,f573,f513,f249]) ).
fof(f3617,plain,
( ~ sQ145_spl
| sQ216_spl ),
inference(split_clause,[status(thm)],[f2264,f2577,f633]) ).
fof(f3619,plain,
( ~ sQ104_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2170,f113]) ).
fof(f3620,plain,
~ sQ104_spl,
inference(contradiction_clause,[status(thm)],[f3619]) ).
fof(f3621,plain,
( sQ132_spl
| ~ sQ61_spl
| ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f594,f3585]) ).
fof(f3622,plain,
( sQ132_spl
| ~ sQ61_spl
| ~ sQ40_spl ),
inference(contradiction_clause,[status(thm)],[f3621]) ).
fof(f3640,plain,
( ~ sQ5_spl
| ~ greater(e_4,e_1)
| ~ cycle(e_1,e_0) ),
inference(resolution,[status(thm)],[f145,f87]) ).
fof(f3647,plain,
( ~ sQ5_spl
| ~ sQ302_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f3640,f133,f3475,f144]) ).
fof(f3650,plain,
( ~ sQ61_spl
| ~ sQ40_spl
| ~ sQ117_spl
| product(e_2,e_5,e_1) ),
inference(resolution,[status(thm)],[f2187,f3585]) ).
fof(f3651,plain,
( ~ sQ61_spl
| ~ sQ40_spl
| ~ sQ117_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f3650,f456,f539,f274,f350]) ).
fof(f3657,plain,
( ~ sQ6_spl
| product(e_1,e_2,e_1) ),
inference(resolution,[status(thm)],[f148,f161]) ).
fof(f3660,plain,
( ~ sQ6_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f3657,f320,f147]) ).
fof(f3666,plain,
( ~ sQ40_spl
| ~ sQ61_spl
| product(e_1,e_3,e_4) ),
inference(resolution,[status(thm)],[f351,f1282]) ).
fof(f3681,plain,
( ~ sQ61_spl
| ~ sQ40_spl
| ~ sQ24_spl
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[f1182,f3585]) ).
fof(f3682,plain,
( ~ sQ61_spl
| ~ sQ40_spl
| ~ sQ24_spl
| sQ255_spl ),
inference(split_clause,[status(thm)],[f3681,f2889,f219,f274,f350]) ).
fof(f3684,plain,
( ~ sQ91_spl
| ~ sQ109_spl
| ~ sQ129_spl
| product(e_3,e_4,e_2) ),
inference(resolution,[status(thm)],[f2216,f1718]) ).
fof(f3691,plain,
( ~ sQ139_spl
| ~ sQ91_spl
| ~ sQ109_spl
| ~ sQ129_spl
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[f3684,f2517]) ).
fof(f3696,plain,
( ~ sQ139_spl
| ~ sQ91_spl
| ~ sQ109_spl
| ~ sQ129_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3691,f114]) ).
fof(f3697,plain,
( ~ sQ139_spl
| ~ sQ91_spl
| ~ sQ109_spl
| ~ sQ129_spl ),
inference(contradiction_clause,[status(thm)],[f3696]) ).
fof(f3698,plain,
( ~ sQ40_spl
| ~ sQ61_spl
| ~ sQ114_spl
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[f2077,f3666]) ).
fof(f3699,plain,
( ~ sQ40_spl
| ~ sQ61_spl
| ~ sQ114_spl
| sQ234_spl ),
inference(split_clause,[status(thm)],[f3698,f2734,f529,f350,f274]) ).
fof(f3700,plain,
( ~ sQ72_spl
| ~ sQ32_spl
| product(e_2,e_2,e_5) ),
inference(resolution,[status(thm)],[f250,f1465]) ).
fof(f3708,plain,
( ~ sQ72_spl
| ~ sQ32_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f3700,f446,f249,f385]) ).
fof(f3757,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| sQ113_spl ),
inference(split_clause,[status(thm)],[f1120,f526,f210,f195]) ).
fof(f3781,plain,
( ~ sQ17_spl
| ~ sQ21_spl
| product(e_2,e_3,e_1) ),
inference(resolution,[status(thm)],[f1218,f1107]) ).
fof(f3790,plain,
( ~ sQ117_spl
| ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ17_spl
| ~ sQ21_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f3781,f2481]) ).
fof(f3795,plain,
( ~ sQ117_spl
| ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ17_spl
| ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3790,f113]) ).
fof(f3796,plain,
( ~ sQ117_spl
| ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ17_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f3795]) ).
fof(f3797,plain,
( ~ sQ117_spl
| ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ136_spl
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[f2238,f2471]) ).
fof(f3798,plain,
( ~ sQ117_spl
| ~ sQ66_spl
| ~ sQ93_spl
| ~ sQ136_spl
| sQ216_spl ),
inference(split_clause,[status(thm)],[f3797,f2577,f605,f456,f366,f539]) ).
fof(f3799,plain,
( ~ sQ40_spl
| ~ sQ62_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1610,f314,f353,f274]) ).
fof(f3917,plain,
( ~ sQ103_spl
| ~ sQ136_spl
| product(e_4,e_1,e_5) ),
inference(resolution,[status(thm)],[f606,f2180]) ).
fof(f3918,plain,
( ~ sQ126_spl
| ~ sQ136_spl
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[f606,f2317]) ).
fof(f3925,plain,
( ~ sQ126_spl
| ~ sQ136_spl
| sQ257_spl ),
inference(split_clause,[status(thm)],[f3918,f2897,f605,f573]) ).
fof(f3926,definition,
( sQ315_spl
<=> greater(e_4,e_3) ),
introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition]) ).
fof(f3928,plain,
( sQ315_spl
| ~ greater(e_4,e_3) ),
inference(component_clause,[status(thm)],[f3926]) ).
fof(f3930,plain,
( sQ315_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3928,f76]) ).
fof(f3931,plain,
sQ315_spl,
inference(contradiction_clause,[status(thm)],[f3930]) ).
fof(f3936,plain,
( ~ sQ103_spl
| ~ sQ136_spl
| ~ greater(e_5,e_4)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[f3917,f87]) ).
fof(f3941,plain,
( ~ sQ103_spl
| ~ sQ136_spl
| ~ sQ195_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f3936,f182,f1185,f605,f494]) ).
fof(f3970,plain,
( ~ sQ136_spl
| ~ sQ103_spl
| product(e_1,e_4,e_3) ),
inference(resolution,[status(thm)],[f495,f2240]) ).
fof(f3972,plain,
( ~ sQ38_spl
| ~ sQ61_spl
| ~ sQ103_spl
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[f495,f1561]) ).
fof(f3978,plain,
( ~ sQ38_spl
| ~ sQ61_spl
| ~ sQ103_spl
| sQ232_spl ),
inference(split_clause,[status(thm)],[f3972,f2727,f494,f350,f268]) ).
fof(f3987,plain,
( ~ sQ103_spl
| ~ sQ114_spl
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[f2077,f495]) ).
fof(f3988,plain,
( ~ sQ103_spl
| ~ sQ114_spl
| sQ232_spl ),
inference(split_clause,[status(thm)],[f3987,f2727,f529,f494]) ).
fof(f3989,plain,
( sQ24_spl
| ~ sQ103_spl
| ~ sQ136_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f221,f3917]) ).
fof(f3990,plain,
( sQ24_spl
| ~ sQ103_spl
| ~ sQ136_spl ),
inference(contradiction_clause,[status(thm)],[f3989]) ).
fof(f4008,plain,
( ~ sQ84_spl
| ~ sQ109_spl
| ~ sQ126_spl
| sQ232_spl ),
inference(split_clause,[status(thm)],[f2462,f2727,f573,f513,f427]) ).
fof(f4049,plain,
( ~ sQ103_spl
| ~ sQ136_spl
| ~ sQ20_spl
| product(e_3,e_5,e_1) ),
inference(resolution,[status(thm)],[f1077,f3917]) ).
fof(f4094,plain,
( ~ sQ71_spl
| ~ sQ31_spl
| product(e_3,e_4,e_5) ),
inference(resolution,[status(thm)],[f247,f1629]) ).
fof(f4111,plain,
( ~ sQ136_spl
| ~ sQ103_spl
| ~ sQ55_spl
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[f1385,f3970]) ).
fof(f4112,plain,
( ~ sQ136_spl
| ~ sQ103_spl
| ~ sQ55_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f4111,f2741,f326,f494,f605]) ).
fof(f4137,plain,
( ~ sQ71_spl
| ~ sQ31_spl
| ~ sQ108_spl
| product(e_2,e_5,e_4) ),
inference(resolution,[status(thm)],[f2136,f4094]) ).
fof(f4140,plain,
( ~ sQ31_spl
| ~ sQ71_spl
| ~ sQ108_spl
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[f4137,f1212]) ).
fof(f4147,plain,
( ~ sQ31_spl
| ~ sQ71_spl
| ~ sQ108_spl
| sQ243_spl ),
inference(split_clause,[status(thm)],[f4140,f2803,f510,f382,f246]) ).
fof(f4158,plain,
( ~ sQ117_spl
| ~ sQ134_spl
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[f2364,f540]) ).
fof(f4159,plain,
( ~ sQ117_spl
| ~ sQ134_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f4158,f434,f598,f539]) ).
fof(f4170,plain,
( ~ sQ103_spl
| ~ sQ136_spl
| ~ sQ20_spl
| ~ sQ141_spl
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[f2504,f4049]) ).
fof(f4171,plain,
( ~ sQ103_spl
| ~ sQ136_spl
| ~ sQ20_spl
| ~ sQ141_spl
| sQ232_spl ),
inference(split_clause,[status(thm)],[f4170,f2727,f621,f204,f605,f494]) ).
fof(f4172,plain,
( ~ sQ103_spl
| ~ sQ139_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f2514,f339,f614,f494]) ).
fof(f4173,plain,
( ~ sQ135_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f2275,f2549,f601]) ).
fof(f4207,plain,
( ~ sQ117_spl
| ~ sQ133_spl
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[f2452,f540]) ).
fof(f4208,plain,
( ~ sQ31_spl
| ~ sQ72_spl
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[f1465,f247]) ).
fof(f4209,plain,
( ~ sQ31_spl
| ~ sQ72_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f4208,f478,f385,f246]) ).
fof(f4210,plain,
( ~ sQ71_spl
| ~ sQ31_spl
| sQ127_spl ),
inference(split_clause,[status(thm)],[f4094,f576,f246,f382]) ).
fof(f4219,plain,
( ~ sQ31_spl
| ~ sQ71_spl
| product(e_3,e_4,e_5) ),
inference(resolution,[status(thm)],[f1629,f247]) ).
fof(f4228,plain,
( ~ sQ31_spl
| ~ sQ71_spl
| ~ sQ142_spl
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[f2233,f4219]) ).
fof(f4229,plain,
( ~ sQ31_spl
| ~ sQ71_spl
| ~ sQ142_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f4228,f2741,f624,f382,f246]) ).
fof(f4230,plain,
( ~ sQ117_spl
| ~ sQ133_spl
| ~ sQ36_spl
| equalish(e_5,e_2) ),
inference(resolution,[status(thm)],[f1236,f4207]) ).
fof(f4231,plain,
( ~ sQ117_spl
| ~ sQ133_spl
| ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4230,f112]) ).
fof(f4232,plain,
( ~ sQ117_spl
| ~ sQ133_spl
| ~ sQ36_spl ),
inference(contradiction_clause,[status(thm)],[f4231]) ).
fof(f4245,plain,
( ~ sQ31_spl
| ~ sQ73_spl
| product(e_4,e_4,e_5) ),
inference(resolution,[status(thm)],[f1658,f247]) ).
fof(f4246,plain,
( ~ sQ31_spl
| ~ sQ73_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f4245,f235,f388,f246]) ).
fof(f4358,plain,
( ~ sQ56_spl
| ~ sQ98_spl
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[f473,f1315]) ).
fof(f4360,plain,
( ~ sQ65_spl
| ~ sQ98_spl
| equalish(e_5,e_2) ),
inference(resolution,[status(thm)],[f473,f1596]) ).
fof(f4366,plain,
( ~ sQ65_spl
| ~ sQ98_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4360,f112]) ).
fof(f4367,plain,
( ~ sQ65_spl
| ~ sQ98_spl ),
inference(contradiction_clause,[status(thm)],[f4366]) ).
fof(f4369,plain,
( ~ sQ119_spl
| ~ sQ56_spl
| ~ sQ98_spl
| product(e_5,e_4,e_1) ),
inference(resolution,[status(thm)],[f4358,f2143]) ).
fof(f4372,plain,
( ~ sQ56_spl
| ~ sQ98_spl
| ~ greater(e_4,e_3)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[f4358,f87]) ).
fof(f4377,plain,
( ~ sQ56_spl
| ~ sQ98_spl
| ~ sQ315_spl
| ~ sQ123_spl ),
inference(split_clause,[status(thm)],[f4372,f558,f3926,f472,f330]) ).
fof(f4378,plain,
( ~ sQ119_spl
| ~ sQ56_spl
| ~ sQ98_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f4369,f362,f472,f330,f545]) ).
fof(f4379,plain,
( ~ sQ98_spl
| ~ sQ60_spl
| product(e_1,e_1,e_4) ),
inference(resolution,[status(thm)],[f1329,f473]) ).
fof(f4380,plain,
( ~ sQ98_spl
| ~ sQ60_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f4379,f144,f342,f472]) ).
fof(f4381,plain,
( ~ sQ98_spl
| ~ sQ117_spl
| ~ sQ133_spl
| product(e_1,e_3,e_2) ),
inference(resolution,[status(thm)],[f4207,f1731]) ).
fof(f4390,plain,
! [X0] :
( ~ sQ56_spl
| ~ sQ98_spl
| ~ product(e_3,e_1,X0)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f4358,f117]) ).
fof(f4408,plain,
( ~ sQ31_spl
| ~ sQ94_spl
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[f1792,f247]) ).
fof(f4409,plain,
( ~ sQ31_spl
| ~ sQ94_spl
| sQ234_spl ),
inference(split_clause,[status(thm)],[f4408,f2734,f459,f246]) ).
fof(f4410,plain,
( ~ sQ31_spl
| ~ sQ72_spl
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[f1465,f247]) ).
fof(f4414,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ72_spl
| ~ product(e_2,X0,e_5)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f4410,f119]) ).
fof(f4419,plain,
( ~ sQ102_spl
| ~ sQ139_spl
| product(e_2,e_2,e_5) ),
inference(resolution,[status(thm)],[f615,f2100]) ).
fof(f4422,plain,
( ~ sQ38_spl
| ~ sQ139_spl
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[f615,f1241]) ).
fof(f4428,plain,
( ~ sQ102_spl
| ~ sQ139_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f4419,f446,f614,f491]) ).
fof(f4429,plain,
( ~ sQ38_spl
| ~ sQ139_spl
| sQ255_spl ),
inference(split_clause,[status(thm)],[f4422,f2889,f614,f268]) ).
fof(f4430,plain,
( ~ sQ55_spl
| ~ sQ102_spl
| ~ sQ136_spl
| product(e_3,e_5,e_1) ),
inference(resolution,[status(thm)],[f2236,f1386]) ).
fof(f4431,plain,
( ~ sQ24_spl
| ~ sQ102_spl
| ~ sQ136_spl
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[f2236,f1182]) ).
fof(f4437,plain,
( ~ sQ24_spl
| ~ sQ102_spl
| ~ sQ136_spl
| sQ256_spl ),
inference(split_clause,[status(thm)],[f4431,f2893,f605,f491,f219]) ).
fof(f4452,plain,
( ~ sQ93_spl
| ~ sQ55_spl
| ~ sQ102_spl
| ~ sQ136_spl
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[f4430,f1807]) ).
fof(f4457,plain,
( ~ sQ93_spl
| ~ sQ55_spl
| ~ sQ102_spl
| ~ sQ136_spl
| sQ230_spl ),
inference(split_clause,[status(thm)],[f4452,f2720,f605,f491,f326,f456]) ).
fof(f4473,plain,
( ~ sQ110_spl
| ~ sQ127_spl
| product(e_5,e_1,e_3) ),
inference(resolution,[status(thm)],[f2408,f517]) ).
fof(f4492,plain,
( ~ sQ141_spl
| ~ sQ114_spl
| product(e_1,e_4,e_3) ),
inference(resolution,[status(thm)],[f530,f2505]) ).
fof(f4508,plain,
( ~ sQ56_spl
| ~ sQ98_spl
| ~ sQ117_spl
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[f2187,f4358]) ).
fof(f4515,plain,
( ~ sQ56_spl
| ~ sQ98_spl
| ~ sQ117_spl
| ~ sQ93_spl
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[f1808,f4508]) ).
fof(f4516,plain,
( ~ sQ56_spl
| ~ sQ98_spl
| ~ sQ117_spl
| ~ sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4515,f114]) ).
fof(f4517,plain,
( ~ sQ56_spl
| ~ sQ98_spl
| ~ sQ117_spl
| ~ sQ93_spl ),
inference(contradiction_clause,[status(thm)],[f4516]) ).
fof(f4524,plain,
( ~ sQ110_spl
| ~ sQ105_spl
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[f2048,f517]) ).
fof(f4525,plain,
( ~ sQ110_spl
| ~ sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4524,f114]) ).
fof(f4526,plain,
( ~ sQ110_spl
| ~ sQ105_spl ),
inference(contradiction_clause,[status(thm)],[f4525]) ).
fof(f4527,plain,
( ~ sQ114_spl
| ~ sQ142_spl
| product(e_5,e_4,e_3) ),
inference(resolution,[status(thm)],[f2234,f530]) ).
fof(f4569,plain,
( ~ sQ110_spl
| ~ sQ126_spl
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[f2318,f517]) ).
fof(f4570,plain,
( ~ sQ110_spl
| ~ sQ126_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f4569,f156,f573,f516]) ).
fof(f4580,plain,
( ~ sQ110_spl
| ~ sQ129_spl
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[f2220,f517]) ).
fof(f4581,plain,
( ~ sQ55_spl
| ~ sQ110_spl
| ~ sQ129_spl
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[f4580,f1386]) ).
fof(f4582,plain,
( ~ sQ110_spl
| ~ sQ129_spl
| ~ greater(e_3,e_2)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[f4580,f87]) ).
fof(f4587,plain,
( ~ sQ110_spl
| ~ sQ129_spl
| ~ sQ258_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f4582,f304,f2913,f582,f516]) ).
fof(f4597,plain,
( ~ sQ55_spl
| ~ sQ110_spl
| ~ sQ129_spl
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[f4581,f165]) ).
fof(f4603,plain,
( ~ sQ55_spl
| ~ sQ110_spl
| ~ sQ129_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f4597,f2549,f582,f516,f326]) ).
fof(f4633,plain,
( ~ sQ141_spl
| ~ sQ114_spl
| ~ sQ55_spl
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[f1385,f4492]) ).
fof(f4634,plain,
( ~ sQ141_spl
| ~ sQ114_spl
| ~ sQ55_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f4633,f2741,f326,f529,f621]) ).
fof(f4649,plain,
( ~ sQ31_spl
| ~ sQ138_spl
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[f2442,f247]) ).
fof(f4650,plain,
( ~ sQ31_spl
| ~ sQ138_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f4649,f2549,f611,f246]) ).
fof(f4651,plain,
( ~ sQ110_spl
| ~ sQ129_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f4580,f418,f582,f516]) ).
fof(f4690,plain,
( ~ sQ141_spl
| ~ sQ114_spl
| ~ sQ21_spl
| product(e_3,e_3,e_4) ),
inference(resolution,[status(thm)],[f1125,f4492]) ).
fof(f4691,plain,
( ~ sQ141_spl
| ~ sQ114_spl
| ~ sQ21_spl
| sQ148_spl ),
inference(split_clause,[status(thm)],[f4690,f643,f210,f529,f621]) ).
fof(f4699,plain,
( ~ sQ61_spl
| ~ sQ38_spl
| product(e_3,e_2,e_5) ),
inference(resolution,[status(thm)],[f269,f1556]) ).
fof(f4707,plain,
( ~ sQ61_spl
| ~ sQ38_spl
| sQ142_spl ),
inference(split_clause,[status(thm)],[f4699,f624,f268,f350]) ).
fof(f4732,plain,
( ~ sQ91_spl
| ~ sQ109_spl
| ~ sQ129_spl
| ~ sQ62_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f1612,f3684]) ).
fof(f4733,plain,
( ~ sQ91_spl
| ~ sQ109_spl
| ~ sQ129_spl
| ~ sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4732,f113]) ).
fof(f4734,plain,
( ~ sQ91_spl
| ~ sQ109_spl
| ~ sQ129_spl
| ~ sQ62_spl ),
inference(contradiction_clause,[status(thm)],[f4733]) ).
fof(f4735,plain,
( ~ sQ36_spl
| ~ sQ114_spl
| ~ sQ142_spl
| product(e_3,e_3,e_4) ),
inference(resolution,[status(thm)],[f4527,f1237]) ).
fof(f4740,plain,
( ~ sQ36_spl
| ~ sQ114_spl
| ~ sQ142_spl
| sQ148_spl ),
inference(split_clause,[status(thm)],[f4735,f643,f624,f529,f262]) ).
fof(f4758,plain,
( ~ sQ81_spl
| ~ sQ102_spl
| ~ sQ136_spl
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[f2236,f1818]) ).
fof(f4759,plain,
( ~ sQ31_spl
| ~ sQ72_spl
| ~ sQ102_spl
| ~ sQ136_spl
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[f2236,f4414]) ).
fof(f4765,plain,
( ~ sQ81_spl
| ~ sQ102_spl
| ~ sQ136_spl
| sQ214_spl ),
inference(split_clause,[status(thm)],[f4758,f2570,f605,f491,f418]) ).
fof(f4767,plain,
( ~ sQ31_spl
| ~ sQ72_spl
| ~ sQ102_spl
| ~ sQ136_spl
| sQ253_spl ),
inference(split_clause,[status(thm)],[f4759,f2881,f605,f491,f385,f246]) ).
fof(f4844,plain,
( ~ sQ68_spl
| ~ sQ91_spl
| product(e_4,e_3,e_5) ),
inference(resolution,[status(thm)],[f451,f1578]) ).
fof(f4846,plain,
( ~ sQ36_spl
| ~ sQ91_spl
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[f451,f1235]) ).
fof(f4852,plain,
( ~ sQ36_spl
| ~ sQ91_spl
| sQ256_spl ),
inference(split_clause,[status(thm)],[f4846,f2893,f450,f262]) ).
fof(f4853,plain,
( ~ sQ68_spl
| ~ sQ91_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f4844,f513,f450,f372]) ).
fof(f4854,plain,
( ~ sQ93_spl
| ~ sQ68_spl
| product(e_1,e_4,e_2) ),
inference(resolution,[status(thm)],[f373,f1809]) ).
fof(f4862,plain,
( ~ sQ93_spl
| ~ sQ68_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f4854,f195,f372,f456]) ).
fof(f4863,plain,
( ~ sQ68_spl
| ~ sQ94_spl
| product(e_4,e_4,e_2) ),
inference(resolution,[status(thm)],[f1794,f373]) ).
fof(f4865,plain,
( ~ sQ68_spl
| ~ sQ94_spl
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[f4863,f165]) ).
fof(f4871,plain,
( ~ sQ68_spl
| ~ sQ94_spl
| sQ256_spl ),
inference(split_clause,[status(thm)],[f4865,f2893,f459,f372]) ).
fof(f4881,plain,
( ~ sQ60_spl
| ~ sQ96_spl
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[f1814,f343]) ).
fof(f4884,plain,
( ~ sQ139_spl
| ~ sQ60_spl
| ~ sQ96_spl
| equalish(e_5,e_1) ),
inference(resolution,[status(thm)],[f4881,f2517]) ).
fof(f4893,plain,
( ~ sQ139_spl
| ~ sQ60_spl
| ~ sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4884,f111]) ).
fof(f4894,plain,
( ~ sQ139_spl
| ~ sQ60_spl
| ~ sQ96_spl ),
inference(contradiction_clause,[status(thm)],[f4893]) ).
fof(f4915,plain,
( ~ sQ60_spl
| ~ sQ141_spl
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[f2503,f343]) ).
fof(f4916,plain,
( ~ sQ60_spl
| ~ sQ141_spl
| sQ212_spl ),
inference(split_clause,[status(thm)],[f4915,f2563,f621,f342]) ).
fof(f4922,plain,
( ~ sQ96_spl
| ~ sQ136_spl
| ~ sQ103_spl
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[f3970,f1812]) ).
fof(f4927,plain,
( ~ sQ96_spl
| ~ sQ136_spl
| ~ sQ103_spl
| sQ234_spl ),
inference(split_clause,[status(thm)],[f4922,f2734,f494,f605,f466]) ).
fof(f4929,plain,
( ~ sQ134_spl
| ~ sQ116_spl
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[f537,f2364]) ).
fof(f4944,plain,
( ~ sQ134_spl
| ~ sQ116_spl
| ~ sQ20_spl
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[f1075,f4929]) ).
fof(f4945,plain,
( ~ sQ134_spl
| ~ sQ116_spl
| ~ sQ20_spl
| sQ243_spl ),
inference(split_clause,[status(thm)],[f4944,f2803,f204,f536,f598]) ).
fof(f4956,plain,
( ~ sQ136_spl
| ~ sQ17_spl
| ~ sQ24_spl
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[f1179,f2238]) ).
fof(f4961,plain,
( ~ sQ136_spl
| ~ sQ17_spl
| ~ sQ24_spl
| sQ216_spl ),
inference(split_clause,[status(thm)],[f4956,f2577,f219,f195,f605]) ).
fof(f4963,plain,
( ~ sQ35_spl
| ~ sQ110_spl
| ~ sQ127_spl
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[f4473,f1267]) ).
fof(f4977,plain,
( ~ sQ35_spl
| ~ sQ110_spl
| ~ sQ127_spl
| product(e_3,e_1,e_3) ),
inference(resolution,[status(thm)],[f4963,f161]) ).
fof(f4980,plain,
( ~ sQ35_spl
| ~ sQ110_spl
| ~ sQ127_spl
| sQ135_spl ),
inference(split_clause,[status(thm)],[f4977,f601,f576,f516,f258]) ).
fof(f4987,plain,
( ~ sQ61_spl
| ~ sQ36_spl
| product(e_3,e_3,e_5) ),
inference(resolution,[status(thm)],[f263,f1556]) ).
fof(f4995,plain,
( ~ sQ61_spl
| ~ sQ36_spl
| sQ147_spl ),
inference(split_clause,[status(thm)],[f4987,f640,f262,f350]) ).
fof(f4996,plain,
( ~ sQ51_spl
| ~ sQ85_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f1762,f274,f430,f314]) ).
fof(f4997,plain,
( ~ sQ136_spl
| ~ sQ103_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f3970,f204,f494,f605]) ).
fof(f4998,plain,
( ~ sQ56_spl
| ~ sQ100_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f1941,f611,f478,f330]) ).
fof(f4999,plain,
( ~ sQ141_spl
| ~ sQ114_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f4492,f204,f529,f621]) ).
fof(f5000,plain,
( ~ sQ36_spl
| ~ sQ65_spl
| product(e_1,e_3,e_5) ),
inference(resolution,[status(thm)],[f1598,f263]) ).
fof(f5002,plain,
( ~ sQ36_spl
| ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ102_spl
| equalish(e_5,e_2) ),
inference(resolution,[status(thm)],[f2096,f1236]) ).
fof(f5007,plain,
( ~ sQ36_spl
| ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5002,f112]) ).
fof(f5008,plain,
( ~ sQ36_spl
| ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ102_spl ),
inference(contradiction_clause,[status(thm)],[f5007]) ).
fof(f5009,plain,
( ~ sQ114_spl
| ~ sQ142_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f4527,f350,f624,f529]) ).
fof(f5010,plain,
( ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ102_spl
| product(e_3,e_5,e_4) ),
inference(resolution,[status(thm)],[f2109,f1315]) ).
fof(f5058,plain,
( ~ sQ38_spl
| ~ sQ65_spl
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[f363,f1243]) ).
fof(f5063,plain,
( ~ sQ38_spl
| ~ sQ65_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f5058,f427,f362,f268]) ).
fof(f5064,plain,
( ~ sQ32_spl
| ~ sQ73_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f1652,f472,f388,f249]) ).
fof(f5069,plain,
( ~ sQ36_spl
| ~ sQ65_spl
| ~ sQ132_spl
| product(e_5,e_5,e_3) ),
inference(resolution,[status(thm)],[f2286,f5000]) ).
fof(f5070,plain,
( ~ sQ36_spl
| ~ sQ65_spl
| ~ sQ132_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f5069,f165]) ).
fof(f5076,plain,
( ~ sQ36_spl
| ~ sQ65_spl
| ~ sQ132_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5070,f113]) ).
fof(f5077,plain,
( ~ sQ36_spl
| ~ sQ65_spl
| ~ sQ132_spl ),
inference(contradiction_clause,[status(thm)],[f5076]) ).
fof(f5133,plain,
( ~ sQ40_spl
| ~ sQ61_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f3666,f536,f350,f274]) ).
fof(f5199,plain,
( ~ sQ59_spl
| ~ sQ96_spl
| product(e_5,e_3,e_4) ),
inference(resolution,[status(thm)],[f467,f1379]) ).
fof(f5208,plain,
! [X0] :
( ~ sQ59_spl
| ~ sQ96_spl
| ~ product(e_5,X0,e_4)
| equalish(e_3,X0) ),
inference(resolution,[status(thm)],[f5199,f119]) ).
fof(f5236,plain,
( ~ sQ96_spl
| ~ sQ59_spl
| product(e_3,e_5,e_2) ),
inference(resolution,[status(thm)],[f340,f1814]) ).
fof(f5256,plain,
( ~ sQ109_spl
| ~ sQ126_spl
| ~ sQ59_spl
| ~ sQ96_spl
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[f5208,f2312]) ).
fof(f5258,plain,
( ~ sQ109_spl
| ~ sQ126_spl
| ~ sQ59_spl
| ~ sQ96_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f5256,f2549,f466,f339,f573,f513]) ).
fof(f5260,plain,
! [X0] :
( ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ102_spl
| ~ product(X0,e_2,e_3)
| equalish(e_4,X0) ),
inference(resolution,[status(thm)],[f2096,f121]) ).
fof(f5283,plain,
( ~ sQ91_spl
| ~ sQ70_spl
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[f379,f1718]) ).
fof(f5291,plain,
( ~ sQ91_spl
| ~ sQ70_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f5283,f598,f378,f450]) ).
fof(f5292,plain,
( ~ sQ70_spl
| ~ sQ94_spl
| product(e_4,e_1,e_2) ),
inference(resolution,[status(thm)],[f1794,f379]) ).
fof(f5294,plain,
! [X0] :
( ~ sQ158_spl
| ~ sQ70_spl
| ~ sQ94_spl
| ~ next(e_4,X0)
| equalish(e_2,X0) ),
inference(resolution,[status(thm)],[f5292,f694]) ).
fof(f5304,plain,
( ~ sQ158_spl
| ~ sQ70_spl
| ~ sQ94_spl
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[f5294,f63]) ).
fof(f5305,plain,
( ~ sQ158_spl
| ~ sQ70_spl
| ~ sQ94_spl
| sQ232_spl ),
inference(split_clause,[status(thm)],[f5304,f2727,f459,f378,f693]) ).
fof(f5306,plain,
( ~ sQ56_spl
| ~ sQ98_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f4358,f595,f472,f330]) ).
fof(f5307,plain,
( ~ sQ96_spl
| ~ sQ59_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f5236,f614,f339,f466]) ).
fof(f5308,plain,
( ~ sQ59_spl
| ~ sQ96_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f5199,f494,f466,f339]) ).
fof(f5353,plain,
( ~ sQ61_spl
| ~ sQ40_spl
| ~ sQ56_spl
| ~ sQ98_spl
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[f4390,f3585]) ).
fof(f5354,plain,
( ~ sQ61_spl
| ~ sQ40_spl
| ~ sQ56_spl
| ~ sQ98_spl
| sQ257_spl ),
inference(split_clause,[status(thm)],[f5353,f2897,f472,f330,f274,f350]) ).
fof(f5399,plain,
( sQ134_spl
| ~ sQ60_spl
| ~ sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f600,f4881]) ).
fof(f5400,plain,
( sQ134_spl
| ~ sQ60_spl
| ~ sQ96_spl ),
inference(contradiction_clause,[status(thm)],[f5399]) ).
fof(f5435,plain,
( ~ sQ105_spl
| ~ sQ138_spl
| product(e_1,e_4,e_5) ),
inference(resolution,[status(thm)],[f612,f2050]) ).
fof(f5440,plain,
( ~ sQ105_spl
| ~ sQ138_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f5435,f201,f611,f500]) ).
fof(f5456,plain,
( ~ sQ138_spl
| ~ sQ102_spl
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[f2100,f612]) ).
fof(f5457,plain,
( ~ sQ138_spl
| ~ sQ102_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f5456,f478,f491,f611]) ).
fof(f5459,plain,
( ~ sQ72_spl
| ~ sQ35_spl
| product(e_2,e_3,e_5) ),
inference(resolution,[status(thm)],[f259,f1465]) ).
fof(f5466,plain,
( ~ sQ143_spl
| ~ sQ72_spl
| ~ sQ35_spl
| product(e_4,e_5,e_3) ),
inference(resolution,[status(thm)],[f5459,f2308]) ).
fof(f5472,plain,
( ~ sQ35_spl
| ~ sQ143_spl
| ~ sQ72_spl
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[f5466,f1265]) ).
fof(f5477,plain,
( ~ sQ35_spl
| ~ sQ143_spl
| ~ sQ72_spl
| sQ241_spl ),
inference(split_clause,[status(thm)],[f5472,f2795,f385,f627,f258]) ).
fof(f5482,plain,
( ~ sQ35_spl
| ~ sQ36_spl
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[f1235,f259]) ).
fof(f5483,plain,
( ~ sQ35_spl
| ~ sQ36_spl
| sQ253_spl ),
inference(split_clause,[status(thm)],[f5482,f2881,f262,f258]) ).
fof(f5484,plain,
( sQ115_spl
| ~ sQ72_spl
| ~ sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f534,f5459]) ).
fof(f5485,plain,
( sQ115_spl
| ~ sQ72_spl
| ~ sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f5484]) ).
fof(f5528,plain,
( ~ sQ35_spl
| ~ sQ71_spl
| product(e_3,e_3,e_5) ),
inference(resolution,[status(thm)],[f1629,f259]) ).
fof(f5529,plain,
( ~ sQ35_spl
| ~ sQ71_spl
| sQ147_spl ),
inference(split_clause,[status(thm)],[f5528,f640,f382,f258]) ).
fof(f5547,plain,
( ~ sQ35_spl
| ~ sQ73_spl
| product(e_4,e_3,e_5) ),
inference(resolution,[status(thm)],[f1658,f259]) ).
fof(f5548,plain,
( ~ sQ129_spl
| ~ sQ35_spl
| ~ sQ73_spl
| product(e_2,e_5,e_3) ),
inference(resolution,[status(thm)],[f5547,f2220]) ).
fof(f5556,plain,
( ~ sQ35_spl
| ~ sQ129_spl
| ~ sQ73_spl
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[f5548,f1265]) ).
fof(f5561,plain,
( ~ sQ35_spl
| ~ sQ129_spl
| ~ sQ73_spl
| sQ243_spl ),
inference(split_clause,[status(thm)],[f5556,f2803,f388,f582,f258]) ).
fof(f5580,plain,
( ~ sQ132_spl
| ~ sQ116_spl
| product(e_5,e_4,e_3) ),
inference(resolution,[status(thm)],[f537,f2286]) ).
fof(f5596,plain,
( ~ sQ113_spl
| ~ sQ141_spl
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[f622,f2065]) ).
fof(f5603,plain,
( ~ sQ113_spl
| ~ sQ141_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f5596,f147,f621,f526]) ).
fof(f5604,plain,
( ~ sQ68_spl
| ~ sQ59_spl
| ~ sQ98_spl
| sQ234_spl ),
inference(split_clause,[status(thm)],[f2383,f2734,f472,f339,f372]) ).
fof(f5645,plain,
( ~ sQ84_spl
| ~ sQ55_spl
| product(e_4,e_3,e_2) ),
inference(resolution,[status(thm)],[f327,f1882]) ).
fof(f5648,plain,
( ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ102_spl
| ~ sQ55_spl
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[f327,f5260]) ).
fof(f5653,plain,
( ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ102_spl
| ~ sQ55_spl
| sQ253_spl ),
inference(split_clause,[status(thm)],[f5648,f2881,f326,f491,f478,f330]) ).
fof(f5654,plain,
( ~ sQ84_spl
| ~ sQ55_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f5645,f510,f326,f427]) ).
fof(f5696,plain,
( ~ sQ132_spl
| ~ sQ116_spl
| ~ sQ71_spl
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[f1628,f5580]) ).
fof(f5697,plain,
( ~ sQ132_spl
| ~ sQ116_spl
| ~ sQ71_spl
| sQ241_spl ),
inference(split_clause,[status(thm)],[f5696,f2795,f382,f536,f592]) ).
fof(f5705,plain,
( ~ sQ32_spl
| ~ sQ98_spl
| ~ sQ117_spl
| ~ sQ133_spl
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[f4381,f1274]) ).
fof(f5710,plain,
( ~ sQ32_spl
| ~ sQ98_spl
| ~ sQ117_spl
| ~ sQ133_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5705,f113]) ).
fof(f5711,plain,
( ~ sQ32_spl
| ~ sQ98_spl
| ~ sQ117_spl
| ~ sQ133_spl ),
inference(contradiction_clause,[status(thm)],[f5710]) ).
fof(f5748,plain,
( ~ sQ62_spl
| ~ sQ40_spl
| product(e_2,e_1,e_5) ),
inference(resolution,[status(thm)],[f275,f1614]) ).
fof(f5755,plain,
( ~ sQ35_spl
| ~ sQ73_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f5547,f513,f388,f258]) ).
fof(f5760,plain,
! [X0] :
( ~ sQ62_spl
| ~ sQ40_spl
| ~ product(e_2,X0,e_5)
| equalish(e_1,X0) ),
inference(resolution,[status(thm)],[f5748,f119]) ).
fof(f5786,plain,
( ~ sQ59_spl
| ~ sQ98_spl
| ~ sQ103_spl
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[f2179,f1727]) ).
fof(f5787,plain,
( ~ sQ59_spl
| ~ sQ98_spl
| ~ sQ103_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f5786,f2549,f494,f472,f339]) ).
fof(f5791,plain,
( ~ sQ62_spl
| ~ sQ40_spl
| ~ sQ72_spl
| ~ sQ35_spl
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[f5459,f5760]) ).
fof(f5796,plain,
( ~ sQ62_spl
| ~ sQ40_spl
| ~ sQ72_spl
| ~ sQ35_spl
| sQ245_spl ),
inference(split_clause,[status(thm)],[f5791,f2811,f258,f385,f274,f353]) ).
fof(f5826,plain,
( ~ sQ129_spl
| ~ sQ108_spl
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[f511,f2220]) ).
fof(f5831,plain,
( ~ sQ129_spl
| ~ sQ108_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f5826,f434,f510,f582]) ).
fof(f5843,plain,
( ~ sQ108_spl
| ~ sQ127_spl
| product(e_5,e_2,e_3) ),
inference(resolution,[status(thm)],[f2408,f511]) ).
fof(f5884,plain,
( ~ sQ40_spl
| ~ sQ62_spl
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[f354,f1282]) ).
fof(f5899,plain,
( ~ sQ108_spl
| ~ sQ23_spl
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[f1155,f511]) ).
fof(f5900,plain,
( ~ sQ108_spl
| ~ sQ23_spl
| sQ245_spl ),
inference(split_clause,[status(thm)],[f5899,f2811,f216,f510]) ).
fof(f5901,plain,
( ~ sQ108_spl
| ~ sQ127_spl
| ~ sQ56_spl
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[f1313,f5843]) ).
fof(f5902,plain,
( ~ sQ108_spl
| ~ sQ127_spl
| ~ sQ56_spl
| sQ257_spl ),
inference(split_clause,[status(thm)],[f5901,f2897,f330,f576,f510]) ).
fof(f5922,plain,
( ~ sQ40_spl
| ~ sQ62_spl
| ~ sQ116_spl
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[f2164,f5884]) ).
fof(f5923,plain,
( ~ sQ40_spl
| ~ sQ62_spl
| ~ sQ116_spl
| sQ216_spl ),
inference(split_clause,[status(thm)],[f5922,f2577,f536,f353,f274]) ).
fof(f5924,plain,
( sQ66_spl
| ~ sQ108_spl
| ~ sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f368,f5843]) ).
fof(f5925,plain,
( sQ66_spl
| ~ sQ108_spl
| ~ sQ127_spl ),
inference(contradiction_clause,[status(thm)],[f5924]) ).
fof(f5927,plain,
( ~ sQ62_spl
| ~ sQ40_spl
| ~ sQ24_spl
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[f1182,f5748]) ).
fof(f5928,plain,
( ~ sQ62_spl
| ~ sQ40_spl
| ~ sQ24_spl
| sQ256_spl ),
inference(split_clause,[status(thm)],[f5927,f2893,f219,f274,f353]) ).
fof(f5929,plain,
( ~ sQ40_spl
| ~ sQ136_spl
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[f2238,f275]) ).
fof(f5930,plain,
( ~ sQ40_spl
| ~ sQ136_spl
| sQ212_spl ),
inference(split_clause,[status(thm)],[f5929,f2563,f605,f274]) ).
fof(f5931,plain,
( ~ sQ59_spl
| ~ sQ98_spl
| ~ sQ133_spl
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[f2450,f1727]) ).
fof(f5932,plain,
( ~ sQ59_spl
| ~ sQ98_spl
| ~ sQ133_spl
| sQ214_spl ),
inference(split_clause,[status(thm)],[f5931,f2570,f595,f472,f339]) ).
fof(f5933,plain,
( ~ sQ40_spl
| ~ sQ62_spl
| ~ sQ143_spl
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[f2306,f5884]) ).
fof(f5934,plain,
( ~ sQ40_spl
| ~ sQ62_spl
| ~ sQ143_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f5933,f2549,f627,f353,f274]) ).
fof(f5935,plain,
( ~ sQ62_spl
| ~ sQ40_spl
| ~ sQ115_spl
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[f2149,f5748]) ).
fof(f5936,plain,
( ~ sQ62_spl
| ~ sQ40_spl
| ~ sQ115_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f5935,f2549,f532,f274,f353]) ).
fof(f5952,plain,
( ~ sQ72_spl
| ~ sQ35_spl
| ~ sQ142_spl
| product(e_5,e_5,e_3) ),
inference(resolution,[status(thm)],[f2234,f5459]) ).
fof(f5953,plain,
( ~ sQ72_spl
| ~ sQ35_spl
| ~ sQ142_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f5952,f398,f624,f258,f385]) ).
fof(f5960,plain,
( ~ sQ136_spl
| ~ sQ105_spl
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[f501,f2240]) ).
fof(f5968,plain,
( ~ sQ136_spl
| ~ sQ105_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f5960,f156,f500,f605]) ).
fof(f5970,plain,
( ~ sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1665,f113]) ).
fof(f5971,plain,
~ sQ76_spl,
inference(contradiction_clause,[status(thm)],[f5970]) ).
fof(f5990,plain,
( ~ sQ109_spl
| ~ sQ126_spl
| ~ sQ68_spl
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[f1577,f2312]) ).
fof(f5991,plain,
( ~ sQ109_spl
| ~ sQ126_spl
| ~ sQ68_spl
| sQ234_spl ),
inference(split_clause,[status(thm)],[f5990,f2734,f372,f573,f513]) ).
fof(f5995,plain,
( ~ sQ133_spl
| ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ102_spl
| equalish(e_1,e_5) ),
inference(resolution,[status(thm)],[f5010,f2451]) ).
fof(f6001,plain,
( ~ sQ133_spl
| ~ sQ56_spl
| ~ sQ100_spl
| ~ sQ102_spl
| sQ244_spl ),
inference(split_clause,[status(thm)],[f5995,f2807,f491,f478,f330,f595]) ).
fof(f6048,plain,
( ~ sQ133_spl
| ~ sQ119_spl
| product(e_5,e_4,e_1) ),
inference(resolution,[status(thm)],[f2143,f596]) ).
fof(f6049,plain,
( ~ sQ133_spl
| ~ sQ119_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f6048,f362,f545,f595]) ).
fof(f6062,plain,
( ~ sQ70_spl
| ~ sQ93_spl
| product(e_1,e_1,e_5) ),
inference(resolution,[status(thm)],[f457,f1585]) ).
fof(f6069,plain,
( ~ sQ70_spl
| ~ sQ93_spl
| ~ greater(e_5,e_1)
| ~ cycle(e_1,e_0) ),
inference(resolution,[status(thm)],[f6062,f87]) ).
fof(f6073,plain,
( ~ sQ70_spl
| ~ sQ93_spl
| product(e_1,e_5,e_1) ),
inference(resolution,[status(thm)],[f6062,f161]) ).
fof(f6076,plain,
( ~ sQ70_spl
| ~ sQ93_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f6073,f252,f456,f378]) ).
fof(f6078,plain,
( ~ sQ70_spl
| ~ sQ93_spl
| ~ sQ301_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f6069,f133,f3470,f456,f378]) ).
fof(f6085,plain,
( ~ sQ102_spl
| ~ sQ136_spl
| ~ sQ54_spl
| product(e_5,e_5,e_1) ),
inference(resolution,[status(thm)],[f1345,f2236]) ).
fof(f6086,plain,
( ~ sQ102_spl
| ~ sQ136_spl
| ~ sQ54_spl
| equalish(e_5,e_1) ),
inference(resolution,[status(thm)],[f6085,f165]) ).
fof(f6092,plain,
( ~ sQ102_spl
| ~ sQ136_spl
| ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6086,f111]) ).
fof(f6093,plain,
( ~ sQ102_spl
| ~ sQ136_spl
| ~ sQ54_spl ),
inference(contradiction_clause,[status(thm)],[f6092]) ).
fof(f6130,plain,
( ~ sQ32_spl
| ~ sQ71_spl
| ~ sQ110_spl
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[f517,f2420]) ).
fof(f6135,plain,
( ~ sQ32_spl
| ~ sQ71_spl
| ~ sQ110_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f6130,f2741,f516,f382,f249]) ).
fof(f6136,plain,
( sQ71_spl
| ~ sQ110_spl
| ~ sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f384,f4473]) ).
fof(f6137,plain,
( sQ71_spl
| ~ sQ110_spl
| ~ sQ127_spl ),
inference(contradiction_clause,[status(thm)],[f6136]) ).
fof(f6138,plain,
$false,
inference(sat_refutation,[status(thm)],[f142,f159,f172,f191,f207,f225,f241,f261,f277,f313,f329,f345,f365,f381,f397,f413,f433,f449,f465,f481,f503,f519,f535,f551,f588,f604,f620,f636,f652,f678,f684,f696,f708,f710,f718,f724,f736,f738,f884,f927,f934,f948,f983,f1016,f1073,f1086,f1096,f1103,f1119,f1142,f1150,f1169,f1188,f1190,f1208,f1239,f1253,f1262,f1277,f1284,f1291,f1301,f1303,f1310,f1317,f1325,f1340,f1347,f1381,f1404,f1413,f1422,f1429,f1469,f1470,f1529,f1537,f1551,f1566,f1573,f1580,f1587,f1594,f1609,f1631,f1639,f1648,f1651,f1662,f1686,f1695,f1726,f1742,f1746,f1771,f1773,f1782,f1790,f1823,f1832,f1834,f1842,f1862,f1873,f1876,f1886,f1887,f1889,f1903,f2008,f2010,f2015,f2024,f2033,f2044,f2051,f2053,f2060,f2067,f2074,f2088,f2129,f2138,f2145,f2152,f2159,f2160,f2167,f2182,f2189,f2196,f2198,f2229,f2235,f2248,f2250,f2259,f2287,f2288,f2302,f2309,f2311,f2320,f2330,f2338,f2348,f2357,f2370,f2371,f2392,f2400,f2410,f2411,f2413,f2415,f2439,f2445,f2455,f2457,f2459,f2469,f2470,f2507,f2528,f2530,f2540,f2582,f2584,f2586,f2588,f2593,f2594,f2615,f2622,f2638,f2640,f2643,f2644,f2677,f2753,f2755,f2757,f2759,f2816,f2818,f2820,f2822,f2902,f2904,f2906,f2908,f2909,f2911,f2912,f2916,f2917,f2919,f2937,f3005,f3273,f3396,f3480,f3482,f3496,f3582,f3583,f3595,f3596,f3597,f3598,f3605,f3615,f3616,f3617,f3620,f3622,f3647,f3651,f3660,f3682,f3697,f3699,f3708,f3757,f3796,f3798,f3799,f3925,f3931,f3941,f3978,f3988,f3990,f4008,f4112,f4147,f4159,f4171,f4172,f4173,f4209,f4210,f4229,f4232,f4246,f4367,f4377,f4378,f4380,f4409,f4428,f4429,f4437,f4457,f4517,f4526,f4570,f4587,f4603,f4634,f4650,f4651,f4691,f4707,f4734,f4740,f4765,f4767,f4852,f4853,f4862,f4871,f4894,f4916,f4927,f4945,f4961,f4980,f4995,f4996,f4997,f4998,f4999,f5008,f5009,f5063,f5064,f5077,f5133,f5258,f5291,f5305,f5306,f5307,f5308,f5354,f5400,f5440,f5457,f5477,f5483,f5485,f5529,f5561,f5603,f5604,f5653,f5654,f5697,f5711,f5755,f5787,f5796,f5831,f5900,f5902,f5923,f5925,f5928,f5930,f5932,f5934,f5936,f5953,f5968,f5971,f5991,f6001,f6049,f6076,f6078,f6093,f6135,f6137]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP125-3.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 20:03:06 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 69.75/9.26 % Refutation found
% 69.75/9.26 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 69.75/9.26 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 69.75/9.30 % Elapsed time: 8.915707 seconds
% 69.75/9.30 % CPU time: 70.321886 seconds
% 69.75/9.30 % Total memory used: 94.942 MB
% 69.75/9.30 % Net memory used: 83.205 MB
%------------------------------------------------------------------------------