%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP129-3.004 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.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 : Tue Sep 29 10:12:59 AM UTC 2026
% Result : Unsatisfiable 3.22s 1.42s
% Output : Refutation 4.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 84
% Syntax : Number of formulae : 1011 ( 57 unt; 69 def)
% Number of atoms : 3436 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 3930 (1505 ~;2356 |; 0 &)
% ( 69 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 73 ( 72 usr; 70 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 250 ( 0 sgn 250 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f22,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
fof(f23,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
fof(f24,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
fof(f25,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
fof(f26,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f27,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f28,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f30,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f31,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f34,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f38,axiom,
! [X0,X1] :
( product(X0,X1,e_4)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| ~ group_element(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
fof(f39,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
fof(f40,axiom,
! [X2,X3,X0,X1] :
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f41,axiom,
! [X2,X3,X0,X1] :
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
fof(f42,negated_conjecture,
! [X2,X3,X0,X1] :
( product(X2,X0,X3)
| ~ product(X1,X2,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
fof(f48,plain,
! [X0,X1] :
( ~ product(e_2,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[],[f26,f41]) ).
fof(f49,plain,
! [X0,X1] :
( ~ product(X0,e_2,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f26,f40]) ).
fof(f50,plain,
! [X0,X1] :
( ~ product(X0,X1,e_2)
| ~ product(X0,X1,e_1) ),
inference(resolution,[],[f26,f39]) ).
fof(f51,plain,
! [X0,X1] :
( ~ product(e_3,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[],[f27,f41]) ).
fof(f52,plain,
! [X0,X1] :
( ~ product(X0,e_3,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f27,f40]) ).
fof(f54,plain,
! [X0,X1] :
( ~ product(e_4,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[],[f28,f41]) ).
fof(f55,plain,
! [X0,X1] :
( ~ product(X0,e_4,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f28,f40]) ).
fof(f56,plain,
! [X0,X1] :
( ~ product(X0,X1,e_1)
| ~ product(X0,X1,e_4) ),
inference(resolution,[],[f28,f39]) ).
fof(f60,plain,
! [X0,X1] :
( ~ product(e_3,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(resolution,[],[f30,f41]) ).
fof(f61,plain,
! [X0,X1] :
( ~ product(X0,e_3,X1)
| ~ product(X0,e_2,X1) ),
inference(resolution,[],[f30,f40]) ).
fof(f62,plain,
! [X0,X1] :
( ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_2) ),
inference(resolution,[],[f30,f39]) ).
fof(f63,plain,
! [X0,X1] :
( ~ product(e_4,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(resolution,[],[f31,f41]) ).
fof(f64,plain,
! [X0,X1] :
( ~ product(X0,e_4,X1)
| ~ product(X0,e_2,X1) ),
inference(resolution,[],[f31,f40]) ).
fof(f65,plain,
! [X0,X1] :
( ~ product(X0,X1,e_2)
| ~ product(X0,X1,e_4) ),
inference(resolution,[],[f31,f39]) ).
fof(f72,plain,
! [X0,X1] :
( ~ product(e_3,X0,X1)
| ~ product(e_4,X0,X1) ),
inference(resolution,[],[f34,f41]) ).
fof(f73,plain,
! [X0,X1] :
( ~ product(X0,e_4,X1)
| ~ product(X0,e_3,X1) ),
inference(resolution,[],[f34,f40]) ).
fof(f74,plain,
! [X0,X1] :
( ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_4) ),
inference(resolution,[],[f34,f39]) ).
fof(f102,plain,
! [X2,X0,X1] :
( ~ product(X0,X2,e_2)
| ~ product(X2,e_2,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[],[f48,f42]) ).
fof(f103,plain,
! [X0] :
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| ~ group_element(e_2) ),
inference(resolution,[],[f48,f38]) ).
fof(f104,plain,
! [X0] :
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f103,f23]) ).
fof(f106,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f49,f38]) ).
fof(f107,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f106,f23]) ).
fof(f111,plain,
! [X2,X0,X1] :
( ~ product(X2,X0,e_2)
| ~ product(X0,X1,e_1)
| ~ product(X1,X2,X0) ),
inference(resolution,[],[f50,f42]) ).
fof(f117,definition,
( spl0_3
<=> product(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f118,plain,
( product(e_1,e_2,e_2)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f117]) ).
fof(f119,plain,
( ~ product(e_1,e_2,e_2)
| spl0_3 ),
inference(avatar_component_clause,[],[f117]) ).
fof(f121,definition,
( spl0_4
<=> product(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f122,plain,
( product(e_2,e_1,e_2)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f123,plain,
( ~ product(e_2,e_1,e_2)
| spl0_4 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f127,plain,
! [X0] :
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| ~ group_element(e_3) ),
inference(resolution,[],[f51,f38]) ).
fof(f128,plain,
! [X0] :
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f127,f24]) ).
fof(f129,plain,
( ! [X0] :
( ~ product(e_2,X0,e_1)
| ~ product(X0,e_1,e_2) )
| spl0_3 ),
inference(resolution,[],[f119,f42]) ).
fof(f130,plain,
! [X2,X0,X1] :
( ~ product(e_3,X2,X0)
| ~ product(X2,X0,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f52,f42]) ).
fof(f131,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f52,f38]) ).
fof(f132,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f131,f24]) ).
fof(f137,plain,
! [X2,X0,X1] :
( ~ product(e_1,X0,X1)
| ~ product(X2,e_4,X1)
| ~ product(X0,X2,e_4) ),
inference(resolution,[],[f54,f42]) ).
fof(f138,plain,
! [X0] :
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| ~ group_element(e_4) ),
inference(resolution,[],[f54,f38]) ).
fof(f139,plain,
! [X0] :
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f138,f25]) ).
fof(f143,plain,
! [X2,X0,X1] :
( ~ product(e_4,X2,X0)
| ~ product(X2,X0,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f55,f42]) ).
fof(f144,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| ~ group_element(e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f55,f38]) ).
fof(f145,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f144,f25]) ).
fof(f146,plain,
! [X2,X3,X0,X1] :
( ~ product(X3,e_3,X1)
| ~ product(X1,e_1,X2)
| ~ product(X0,X1,X2)
| ~ product(X0,X3,e_3) ),
inference(resolution,[],[f130,f42]) ).
fof(f149,plain,
( ~ product(e_3,e_1,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(factoring,[],[f130]) ).
fof(f151,definition,
( spl0_5
<=> product(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f152,plain,
( product(e_1,e_3,e_3)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f153,plain,
( ~ product(e_1,e_3,e_3)
| spl0_5 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f155,definition,
( spl0_6
<=> product(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f157,plain,
( ~ product(e_3,e_1,e_3)
| spl0_6 ),
inference(avatar_component_clause,[],[f155]) ).
fof(f158,plain,
( ~ spl0_5
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f149,f155,f151]) ).
fof(f161,plain,
( ! [X0] :
( ~ product(e_3,X0,e_1)
| ~ product(X0,e_1,e_3) )
| spl0_5 ),
inference(resolution,[],[f153,f42]) ).
fof(f167,plain,
! [X0] :
( ~ product(e_1,e_4,X0)
| ~ product(e_4,e_1,e_4) ),
inference(factoring,[],[f137]) ).
fof(f170,definition,
( spl0_7
<=> product(e_4,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f172,plain,
( ~ product(e_4,e_1,e_4)
| spl0_7 ),
inference(avatar_component_clause,[],[f170]) ).
fof(f174,definition,
( spl0_8
<=> ! [X0] : ~ product(e_1,e_4,X0) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f175,plain,
( ! [X0] : ~ product(e_1,e_4,X0)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f174]) ).
fof(f176,plain,
( ~ spl0_7
| spl0_8 ),
inference(avatar_split_clause,[],[f167,f174,f170]) ).
fof(f178,plain,
! [X2,X0,X1] :
( ~ product(e_2,X0,X1)
| ~ product(X2,e_3,X1)
| ~ product(X0,X2,e_3) ),
inference(resolution,[],[f60,f42]) ).
fof(f179,plain,
! [X0] :
( ~ product(e_2,X0,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| ~ group_element(e_3) ),
inference(resolution,[],[f60,f38]) ).
fof(f180,plain,
! [X0] :
( ~ product(e_2,X0,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f179,f24]) ).
fof(f186,definition,
( spl0_9
<=> product(e_4,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f188,plain,
( product(e_4,e_1,e_3)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f186]) ).
fof(f190,definition,
( spl0_10
<=> product(e_4,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f192,plain,
( product(e_4,e_1,e_2)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f190]) ).
fof(f194,definition,
( spl0_11
<=> product(e_4,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f196,plain,
( product(e_4,e_1,e_1)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f198,plain,
! [X2,X0,X1] :
( ~ product(e_3,X2,X0)
| ~ product(X2,X0,X1)
| ~ product(X0,e_2,X1) ),
inference(resolution,[],[f61,f42]) ).
fof(f199,plain,
! [X0] :
( ~ product(X0,e_2,e_4)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f61,f38]) ).
fof(f200,plain,
! [X0] :
( ~ product(X0,e_2,e_4)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f199,f24]) ).
fof(f202,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,e_2)
| ~ product(X2,X0,e_3)
| ~ product(X1,X2,X0) ),
inference(resolution,[],[f62,f42]) ).
fof(f204,plain,
( ~ group_element(e_4)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| ~ spl0_8 ),
inference(resolution,[],[f175,f38]) ).
fof(f205,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f204,f25]) ).
fof(f206,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| ~ group_element(e_1)
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f205,f175]) ).
fof(f207,plain,
( product(e_1,e_4,e_1)
| ~ group_element(e_1)
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f206,f175]) ).
fof(f208,plain,
( ~ group_element(e_1)
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f207,f175]) ).
fof(f209,plain,
( $false
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f208,f22]) ).
fof(f210,plain,
~ spl0_8,
inference(avatar_contradiction_clause,[],[f209]) ).
fof(f211,plain,
! [X2,X0,X1] :
( ~ product(e_2,X0,X1)
| ~ product(X2,e_4,X1)
| ~ product(X0,X2,e_4) ),
inference(resolution,[],[f63,f42]) ).
fof(f212,plain,
! [X0] :
( ~ product(e_2,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| ~ group_element(e_4) ),
inference(resolution,[],[f63,f38]) ).
fof(f213,plain,
! [X0] :
( ~ product(e_2,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f212,f25]) ).
fof(f214,plain,
( ~ group_element(e_1)
| product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| ~ group_element(e_4)
| spl0_7 ),
inference(resolution,[],[f172,f38]) ).
fof(f215,plain,
( ! [X0] :
( ~ product(e_1,X0,e_4)
| ~ product(X0,e_4,e_4) )
| spl0_7 ),
inference(resolution,[],[f172,f42]) ).
fof(f216,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| ~ group_element(e_4)
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f214,f22]) ).
fof(f217,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f216,f25]) ).
fof(f218,plain,
( spl0_9
| spl0_10
| spl0_11
| spl0_7 ),
inference(avatar_split_clause,[],[f217,f170,f194,f190,f186]) ).
fof(f219,plain,
! [X2,X0,X1] :
( ~ product(X0,e_2,X1)
| ~ product(X2,X0,X1)
| ~ product(e_4,X2,X0) ),
inference(resolution,[],[f64,f42]) ).
fof(f220,plain,
! [X0] :
( ~ product(X0,e_2,e_4)
| ~ group_element(e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f64,f38]) ).
fof(f221,plain,
! [X0] :
( ~ product(X0,e_2,e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f220,f25]) ).
fof(f226,plain,
( ~ product(e_2,e_1,e_3)
| ~ spl0_9 ),
inference(resolution,[],[f188,f63]) ).
fof(f244,definition,
( spl0_12
<=> product(e_1,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f248,definition,
( spl0_13
<=> product(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f249,plain,
( ~ product(e_1,e_4,e_2)
| spl0_13 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f250,plain,
( product(e_1,e_4,e_2)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f252,definition,
( spl0_14
<=> product(e_1,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f254,plain,
( product(e_1,e_4,e_1)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f256,definition,
( spl0_15
<=> product(e_1,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f257,plain,
( product(e_1,e_3,e_4)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f258,plain,
( ~ product(e_1,e_3,e_4)
| spl0_15 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f260,plain,
! [X2,X0,X1] :
( ~ product(X0,X2,e_3)
| ~ product(X2,e_3,X1)
| ~ product(e_4,X0,X1) ),
inference(resolution,[],[f72,f42]) ).
fof(f261,plain,
! [X0] :
( ~ product(e_4,X0,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| ~ group_element(e_3) ),
inference(resolution,[],[f72,f38]) ).
fof(f262,plain,
! [X0] :
( ~ product(e_4,X0,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f261,f24]) ).
fof(f269,definition,
( spl0_16
<=> product(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f270,plain,
( ~ product(e_1,e_3,e_2)
| spl0_16 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f271,plain,
( product(e_1,e_3,e_2)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f273,definition,
( spl0_17
<=> product(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f275,plain,
( product(e_1,e_3,e_1)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f277,plain,
! [X2,X0,X1] :
( ~ product(e_4,X2,X0)
| ~ product(X2,X0,X1)
| ~ product(X0,e_3,X1) ),
inference(resolution,[],[f73,f42]) ).
fof(f278,plain,
! [X0] :
( ~ product(X0,e_3,e_4)
| ~ group_element(e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f73,f38]) ).
fof(f279,plain,
! [X0] :
( ~ product(X0,e_3,e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f278,f25]) ).
fof(f287,plain,
( ~ product(e_1,e_1,e_2)
| ~ spl0_10 ),
inference(resolution,[],[f192,f54]) ).
fof(f291,plain,
( ~ product(e_3,e_4,e_4)
| spl0_7
| ~ spl0_15 ),
inference(resolution,[],[f257,f215]) ).
fof(f295,plain,
( ~ group_element(e_4)
| product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| ~ group_element(e_3)
| spl0_7
| ~ spl0_15 ),
inference(resolution,[],[f291,f38]) ).
fof(f297,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| ~ group_element(e_3)
| spl0_7
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f295,f25]) ).
fof(f298,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| spl0_7
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f297,f24]) ).
fof(f300,definition,
( spl0_18
<=> product(e_3,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f302,plain,
( product(e_3,e_4,e_3)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f304,definition,
( spl0_19
<=> product(e_3,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f306,plain,
( product(e_3,e_4,e_2)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f308,definition,
( spl0_20
<=> product(e_3,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f310,plain,
( product(e_3,e_4,e_1)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f311,plain,
( spl0_18
| spl0_19
| spl0_20
| spl0_7
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f298,f256,f170,f308,f304,f300]) ).
fof(f312,plain,
( ~ group_element(e_3)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| ~ group_element(e_1)
| spl0_15 ),
inference(resolution,[],[f258,f38]) ).
fof(f314,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| ~ group_element(e_1)
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f312,f24]) ).
fof(f315,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| ~ group_element(e_1)
| spl0_5
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f314,f153]) ).
fof(f316,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| spl0_5
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f315,f22]) ).
fof(f317,plain,
( spl0_16
| spl0_17
| spl0_5
| spl0_15 ),
inference(avatar_split_clause,[],[f316,f256,f151,f273,f269]) ).
fof(f342,definition,
( spl0_21
<=> product(e_3,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f343,plain,
( ~ product(e_3,e_2,e_3)
| spl0_21 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f346,definition,
( spl0_22
<=> product(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f348,plain,
( product(e_3,e_2,e_2)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f350,definition,
( spl0_23
<=> product(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f354,definition,
( spl0_24
<=> product(e_1,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f356,plain,
( ~ product(e_1,e_1,e_4)
| spl0_24 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f358,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ group_element(e_1)
| spl0_24 ),
inference(resolution,[],[f356,f38]) ).
fof(f360,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| spl0_24 ),
inference(duplicate_literal_removal,[],[f358]) ).
fof(f361,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f360,f22]) ).
fof(f362,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| ~ spl0_10
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f361,f287]) ).
fof(f364,definition,
( spl0_25
<=> product(e_1,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f368,definition,
( spl0_26
<=> product(e_1,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f371,plain,
( spl0_25
| spl0_26
| ~ spl0_10
| spl0_24 ),
inference(avatar_split_clause,[],[f362,f354,f190,f368,f364]) ).
fof(f374,definition,
( spl0_27
<=> product(e_1,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f377,plain,
( spl0_25
| spl0_27
| spl0_26
| spl0_24 ),
inference(avatar_split_clause,[],[f361,f354,f368,f374,f364]) ).
fof(f416,plain,
! [X2,X3,X0,X1] :
( ~ product(X0,X3,e_4)
| ~ product(X1,e_1,X2)
| ~ product(X3,e_4,X1)
| ~ product(X0,X1,X2) ),
inference(resolution,[],[f143,f42]) ).
fof(f427,plain,
( ~ product(e_1,e_2,e_1)
| ~ spl0_17 ),
inference(resolution,[],[f275,f61]) ).
fof(f428,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_17 ),
inference(resolution,[],[f275,f52]) ).
fof(f429,plain,
( ~ spl0_26
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f428,f273,f368]) ).
fof(f432,plain,
! [X0] :
( ~ product(e_2,e_3,X0)
| ~ product(e_3,e_2,e_3) ),
inference(factoring,[],[f178]) ).
fof(f435,definition,
( spl0_34
<=> ! [X0] : ~ product(e_2,e_3,X0) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f436,plain,
( ! [X0] : ~ product(e_2,e_3,X0)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f435]) ).
fof(f437,plain,
( ~ spl0_21
| spl0_34 ),
inference(avatar_split_clause,[],[f432,f435,f342]) ).
fof(f445,definition,
( spl0_35
<=> product(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f446,plain,
( product(e_2,e_3,e_3)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f447,plain,
( ~ product(e_2,e_3,e_3)
| spl0_35 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f455,plain,
! [X2,X3,X0,X1] :
( ~ product(X2,X0,e_4)
| ~ product(X0,e_4,X1)
| ~ product(X3,e_2,X1)
| ~ product(X2,X3,e_2) ),
inference(resolution,[],[f211,f42]) ).
fof(f456,plain,
! [X0,X1] :
( ~ product(X0,e_4,e_4)
| ~ product(X1,X0,e_4)
| ~ group_element(X1)
| product(e_2,X1,e_1)
| product(e_2,X1,e_2)
| product(e_2,X1,e_3)
| ~ group_element(e_2) ),
inference(resolution,[],[f211,f38]) ).
fof(f457,plain,
! [X0] :
( ~ product(e_2,e_4,X0)
| ~ product(e_4,e_2,e_4) ),
inference(factoring,[],[f211]) ).
fof(f460,definition,
( spl0_36
<=> product(e_4,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f462,plain,
( ~ product(e_4,e_2,e_4)
| spl0_36 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f464,definition,
( spl0_37
<=> ! [X0] : ~ product(e_2,e_4,X0) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f465,plain,
( ! [X0] : ~ product(e_2,e_4,X0)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f466,plain,
( ~ spl0_36
| spl0_37 ),
inference(avatar_split_clause,[],[f457,f464,f460]) ).
fof(f467,plain,
! [X0,X1] :
( ~ product(X0,e_4,e_4)
| ~ product(X1,X0,e_4)
| ~ group_element(X1)
| product(e_2,X1,e_1)
| product(e_2,X1,e_2)
| product(e_2,X1,e_3) ),
inference(forward_subsumption_resolution,[],[f456,f23]) ).
fof(f473,definition,
( spl0_38
<=> product(e_4,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f475,plain,
( product(e_4,e_2,e_3)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f477,definition,
( spl0_39
<=> product(e_4,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f478,plain,
( ~ product(e_4,e_2,e_2)
| spl0_39 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f481,definition,
( spl0_40
<=> product(e_4,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f483,plain,
( product(e_4,e_2,e_1)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f485,plain,
! [X2,X3,X0,X1] :
( ~ product(e_2,X3,X1)
| ~ product(e_4,X0,X1)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
inference(resolution,[],[f219,f42]) ).
fof(f486,plain,
! [X0,X1] :
( ~ product(X0,X1,e_4)
| ~ product(e_4,X0,X1)
| ~ group_element(e_2)
| product(X1,e_2,e_1)
| product(X1,e_2,e_2)
| product(X1,e_2,e_3)
| ~ group_element(X1) ),
inference(resolution,[],[f219,f38]) ).
fof(f487,plain,
! [X0] :
( ~ product(e_2,e_2,X0)
| ~ product(e_4,e_2,e_2) ),
inference(factoring,[],[f219]) ).
fof(f490,definition,
( spl0_41
<=> product(e_2,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f491,plain,
( product(e_2,e_4,e_4)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f490]) ).
fof(f492,plain,
( ~ product(e_2,e_4,e_4)
| spl0_41 ),
inference(avatar_component_clause,[],[f490]) ).
fof(f495,definition,
( spl0_42
<=> ! [X0] : ~ product(e_2,e_2,X0) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f496,plain,
( ! [X0] : ~ product(e_2,e_2,X0)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f495]) ).
fof(f497,plain,
( ~ spl0_39
| spl0_42 ),
inference(avatar_split_clause,[],[f487,f495,f477]) ).
fof(f498,plain,
! [X0,X1] :
( ~ product(X0,X1,e_4)
| ~ product(e_4,X0,X1)
| product(X1,e_2,e_1)
| product(X1,e_2,e_2)
| product(X1,e_2,e_3)
| ~ group_element(X1) ),
inference(forward_subsumption_resolution,[],[f486,f23]) ).
fof(f507,plain,
( ~ group_element(e_4)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| ~ group_element(e_2)
| ~ spl0_37 ),
inference(resolution,[],[f465,f38]) ).
fof(f508,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| ~ group_element(e_2)
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f507,f25]) ).
fof(f509,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| ~ group_element(e_2)
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f508,f465]) ).
fof(f510,plain,
( product(e_2,e_4,e_1)
| ~ group_element(e_2)
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f509,f465]) ).
fof(f511,plain,
( ~ group_element(e_2)
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f510,f465]) ).
fof(f512,plain,
( $false
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f511,f23]) ).
fof(f513,plain,
~ spl0_37,
inference(avatar_contradiction_clause,[],[f512]) ).
fof(f514,plain,
! [X2,X3,X0,X1] :
( ~ product(X3,X2,e_3)
| ~ product(e_4,X2,X1)
| ~ product(X0,e_3,X1)
| ~ product(X0,X3,X2) ),
inference(resolution,[],[f260,f42]) ).
fof(f518,plain,
( ~ group_element(e_2)
| product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| ~ group_element(e_4)
| spl0_36 ),
inference(resolution,[],[f462,f38]) ).
fof(f520,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| ~ group_element(e_4)
| spl0_36 ),
inference(forward_subsumption_resolution,[],[f518,f23]) ).
fof(f521,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| spl0_36 ),
inference(forward_subsumption_resolution,[],[f520,f25]) ).
fof(f522,plain,
( spl0_38
| spl0_39
| spl0_40
| spl0_36 ),
inference(avatar_split_clause,[],[f521,f460,f481,f477,f473]) ).
fof(f524,plain,
! [X2,X3,X0,X1] :
( ~ product(X0,X3,e_4)
| ~ product(X1,e_3,X2)
| ~ product(X3,e_4,X1)
| ~ product(X0,X1,X2) ),
inference(resolution,[],[f277,f42]) ).
fof(f529,definition,
( spl0_43
<=> product(e_3,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f531,plain,
( ~ product(e_3,e_4,e_4)
| spl0_43 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f533,definition,
( spl0_44
<=> product(e_4,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f534,plain,
( product(e_4,e_3,e_4)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f535,plain,
( ~ product(e_4,e_3,e_4)
| spl0_44 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f543,definition,
( spl0_45
<=> product(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f545,plain,
( product(e_2,e_4,e_3)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f543]) ).
fof(f547,definition,
( spl0_46
<=> product(e_2,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f548,plain,
( ~ product(e_2,e_4,e_2)
| spl0_46 ),
inference(avatar_component_clause,[],[f547]) ).
fof(f549,plain,
( product(e_2,e_4,e_2)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f547]) ).
fof(f551,definition,
( spl0_47
<=> product(e_2,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f553,plain,
( product(e_2,e_4,e_1)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f551]) ).
fof(f561,plain,
( ~ product(e_1,e_4,e_4)
| ~ spl0_41 ),
inference(resolution,[],[f491,f48]) ).
fof(f566,plain,
( ! [X0] :
( ~ product(e_4,X0,e_3)
| ~ product(X0,e_3,e_4) )
| spl0_43 ),
inference(resolution,[],[f531,f42]) ).
fof(f582,plain,
( ~ product(e_2,e_2,e_3)
| ~ spl0_38 ),
inference(resolution,[],[f475,f63]) ).
fof(f583,plain,
( ~ product(e_1,e_2,e_3)
| ~ spl0_38 ),
inference(resolution,[],[f475,f54]) ).
fof(f585,plain,
( ~ product(e_4,e_1,e_3)
| ~ spl0_38 ),
inference(resolution,[],[f475,f49]) ).
fof(f586,plain,
( $false
| ~ spl0_9
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f585,f188]) ).
fof(f587,plain,
( ~ spl0_9
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f586]) ).
fof(f590,plain,
( ~ spl0_27
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f287,f190,f374]) ).
fof(f591,plain,
( ~ spl0_9
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f585,f473,f186]) ).
fof(f647,plain,
! [X0] :
( ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| ~ group_element(e_1) ),
inference(resolution,[],[f104,f38]) ).
fof(f649,plain,
! [X0] :
( ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| ~ group_element(e_1) ),
inference(duplicate_literal_removal,[],[f647]) ).
fof(f650,plain,
! [X0] :
( ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f649,f22]) ).
fof(f654,definition,
( spl0_56
<=> product(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f658,definition,
( spl0_57
<=> product(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f668,plain,
( ! [X0] :
( ~ product(e_1,e_2,X0)
| ~ product(e_1,e_2,X0) )
| ~ spl0_4 ),
inference(resolution,[],[f122,f102]) ).
fof(f673,plain,
( ! [X0] : ~ product(e_1,e_2,X0)
| ~ spl0_4 ),
inference(duplicate_literal_removal,[],[f668]) ).
fof(f676,plain,
! [X0] :
( product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f107,f38]) ).
fof(f677,plain,
! [X0,X1] :
( ~ product(e_1,X1,X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0)
| ~ product(X1,X0,e_4)
| product(X0,e_2,e_1) ),
inference(resolution,[],[f107,f42]) ).
fof(f679,plain,
! [X0] :
( product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(duplicate_literal_removal,[],[f676]) ).
fof(f681,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(forward_subsumption_resolution,[],[f679,f22]) ).
fof(f686,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| ~ group_element(e_1) ),
inference(resolution,[],[f128,f38]) ).
fof(f688,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| ~ group_element(e_1) ),
inference(duplicate_literal_removal,[],[f686]) ).
fof(f689,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f688,f22]) ).
fof(f692,definition,
( spl0_58
<=> product(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f696,definition,
( spl0_59
<=> product(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f703,plain,
( ! [X0] :
( ~ product(e_1,e_1,X0)
| ~ product(e_1,e_1,X0) )
| ~ spl0_11 ),
inference(resolution,[],[f196,f143]) ).
fof(f706,plain,
( ! [X0] : ~ product(e_1,e_1,X0)
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f703]) ).
fof(f709,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f132,f38]) ).
fof(f710,plain,
! [X0,X1] :
( ~ product(e_1,X1,X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0)
| ~ product(X1,X0,e_4)
| product(X0,e_3,e_1) ),
inference(resolution,[],[f132,f42]) ).
fof(f711,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(duplicate_literal_removal,[],[f709]) ).
fof(f712,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(forward_subsumption_resolution,[],[f711,f22]) ).
fof(f714,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| ~ group_element(e_1) ),
inference(resolution,[],[f139,f38]) ).
fof(f716,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| ~ group_element(e_1) ),
inference(duplicate_literal_removal,[],[f714]) ).
fof(f717,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f716,f22]) ).
fof(f723,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f145,f38]) ).
fof(f725,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(duplicate_literal_removal,[],[f723]) ).
fof(f726,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(forward_subsumption_resolution,[],[f725,f22]) ).
fof(f732,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| ~ group_element(e_2) ),
inference(resolution,[],[f180,f38]) ).
fof(f734,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| ~ group_element(e_2) ),
inference(duplicate_literal_removal,[],[f732]) ).
fof(f735,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f734,f23]) ).
fof(f746,plain,
( ~ product(e_1,e_4,e_3)
| ~ spl0_45 ),
inference(resolution,[],[f545,f48]) ).
fof(f747,plain,
( ~ product(e_2,e_3,e_3)
| ~ spl0_45 ),
inference(resolution,[],[f545,f73]) ).
fof(f748,plain,
( ~ product(e_2,e_2,e_3)
| ~ spl0_45 ),
inference(resolution,[],[f545,f64]) ).
fof(f751,plain,
( ~ spl0_35
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f747,f543,f445]) ).
fof(f752,plain,
( ~ spl0_12
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f746,f543,f244]) ).
fof(f755,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f200,f38]) ).
fof(f756,plain,
! [X0,X1] :
( ~ product(e_2,X1,X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0)
| ~ product(X1,X0,e_4)
| product(X0,e_3,e_1) ),
inference(resolution,[],[f200,f42]) ).
fof(f757,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3) ),
inference(duplicate_literal_removal,[],[f755]) ).
fof(f758,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3) ),
inference(forward_subsumption_resolution,[],[f757,f23]) ).
fof(f759,plain,
( ! [X0] :
( ~ product(e_3,X0,e_2)
| ~ product(X0,e_2,e_3) )
| spl0_35 ),
inference(resolution,[],[f447,f42]) ).
fof(f760,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| ~ group_element(e_2) ),
inference(resolution,[],[f213,f38]) ).
fof(f762,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| ~ group_element(e_2) ),
inference(duplicate_literal_removal,[],[f760]) ).
fof(f763,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f762,f23]) ).
fof(f765,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f221,f38]) ).
fof(f767,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3) ),
inference(duplicate_literal_removal,[],[f765]) ).
fof(f768,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3) ),
inference(forward_subsumption_resolution,[],[f767,f23]) ).
fof(f770,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| ~ group_element(e_4) ),
inference(resolution,[],[f262,f38]) ).
fof(f772,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| ~ group_element(e_4) ),
inference(duplicate_literal_removal,[],[f770]) ).
fof(f773,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f772,f25]) ).
fof(f776,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f279,f38]) ).
fof(f777,plain,
! [X0,X1] :
( ~ product(e_3,X1,X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ product(X1,X0,e_4)
| product(X0,e_4,e_1) ),
inference(resolution,[],[f279,f42]) ).
fof(f778,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3) ),
inference(duplicate_literal_removal,[],[f776]) ).
fof(f779,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_1)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3) ),
inference(forward_subsumption_resolution,[],[f778,f24]) ).
fof(f781,plain,
( ~ group_element(e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| ~ spl0_4 ),
inference(resolution,[],[f673,f38]) ).
fof(f782,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f781,f23]) ).
fof(f789,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| ~ group_element(e_1)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f782,f673]) ).
fof(f790,plain,
( product(e_1,e_2,e_1)
| ~ group_element(e_1)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f789,f673]) ).
fof(f791,plain,
( ~ group_element(e_1)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f790,f673]) ).
fof(f792,plain,
( $false
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f791,f22]) ).
fof(f793,plain,
~ spl0_4,
inference(avatar_contradiction_clause,[],[f792]) ).
fof(f828,plain,
( ! [X0] :
( ~ product(e_1,X0,e_2)
| ~ product(X0,e_2,e_2) )
| spl0_4 ),
inference(resolution,[],[f123,f42]) ).
fof(f843,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ group_element(e_1)
| ~ spl0_11 ),
inference(resolution,[],[f706,f38]) ).
fof(f844,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f843]) ).
fof(f845,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f844,f22]) ).
fof(f846,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f845,f706]) ).
fof(f847,plain,
( product(e_1,e_1,e_1)
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f846,f706]) ).
fof(f848,plain,
( $false
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f847,f706]) ).
fof(f849,plain,
~ spl0_11,
inference(avatar_contradiction_clause,[],[f848]) ).
fof(f857,definition,
( spl0_67
<=> ! [X1] :
( ~ product(X1,e_3,e_3)
| ~ product(e_1,X1,e_3) ) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f858,plain,
( ! [X1] :
( ~ product(e_1,X1,e_3)
| ~ product(X1,e_3,e_3) )
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f879,plain,
! [X0] :
( ~ product(X0,e_3,e_3)
| ~ product(e_3,e_1,e_3)
| ~ product(X0,X0,e_3) ),
inference(factoring,[],[f146]) ).
fof(f882,definition,
( spl0_69
<=> ! [X0] :
( ~ product(X0,e_3,e_3)
| ~ product(X0,X0,e_3) ) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f883,plain,
( ! [X0] :
( ~ product(X0,e_3,e_3)
| ~ product(X0,X0,e_3) )
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f882]) ).
fof(f884,plain,
( ~ spl0_6
| spl0_69 ),
inference(avatar_split_clause,[],[f879,f882,f155]) ).
fof(f886,plain,
( ! [X0] :
( ~ product(X0,e_3,e_3)
| ~ product(e_1,X0,e_3) )
| spl0_6 ),
inference(resolution,[],[f157,f42]) ).
fof(f887,plain,
( spl0_67
| spl0_6 ),
inference(avatar_split_clause,[],[f886,f155,f857]) ).
fof(f899,plain,
! [X0,X1] :
( ~ product(X1,e_1,e_4)
| ~ product(X0,X1,e_4)
| ~ product(X1,e_4,X1) ),
inference(factoring,[],[f416]) ).
fof(f916,plain,
( ~ product(e_1,e_2,e_2)
| ~ spl0_16 ),
inference(resolution,[],[f271,f61]) ).
fof(f939,plain,
( ~ product(e_4,e_4,e_3)
| ~ spl0_18 ),
inference(resolution,[],[f302,f72]) ).
fof(f940,plain,
( ~ product(e_2,e_4,e_3)
| ~ spl0_18 ),
inference(resolution,[],[f302,f60]) ).
fof(f942,plain,
( ~ product(e_1,e_4,e_3)
| ~ spl0_18 ),
inference(resolution,[],[f302,f51]) ).
fof(f943,plain,
( ~ product(e_3,e_3,e_3)
| ~ spl0_18 ),
inference(resolution,[],[f302,f73]) ).
fof(f945,plain,
( ~ product(e_3,e_1,e_3)
| ~ spl0_18 ),
inference(resolution,[],[f302,f55]) ).
fof(f959,plain,
! [X0] :
( ~ product(e_4,e_4,e_4)
| ~ product(X0,e_2,e_4)
| ~ product(e_4,X0,e_2) ),
inference(factoring,[],[f455]) ).
fof(f962,definition,
( spl0_70
<=> ! [X0] :
( ~ product(X0,e_2,e_4)
| ~ product(e_4,X0,e_2) ) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f963,plain,
( ! [X0] :
( ~ product(e_4,X0,e_2)
| ~ product(X0,e_2,e_4) )
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f965,definition,
( spl0_71
<=> product(e_4,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f966,plain,
( product(e_4,e_4,e_4)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f965]) ).
fof(f967,plain,
( ~ product(e_4,e_4,e_4)
| spl0_71 ),
inference(avatar_component_clause,[],[f965]) ).
fof(f968,plain,
( spl0_70
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f959,f965,f962]) ).
fof(f974,definition,
( spl0_72
<=> product(e_4,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f975,plain,
( ~ product(e_4,e_4,e_3)
| spl0_72 ),
inference(avatar_component_clause,[],[f974]) ).
fof(f976,plain,
( product(e_4,e_4,e_3)
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f974]) ).
fof(f978,definition,
( spl0_73
<=> product(e_4,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f979,plain,
( ~ product(e_4,e_4,e_2)
| spl0_73 ),
inference(avatar_component_clause,[],[f978]) ).
fof(f980,plain,
( product(e_4,e_4,e_2)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f978]) ).
fof(f982,definition,
( spl0_74
<=> product(e_4,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f983,plain,
( ~ product(e_4,e_4,e_1)
| spl0_74 ),
inference(avatar_component_clause,[],[f982]) ).
fof(f984,plain,
( product(e_4,e_4,e_1)
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f982]) ).
fof(f998,plain,
( ~ product(e_1,e_4,e_4)
| ~ spl0_71 ),
inference(resolution,[],[f966,f54]) ).
fof(f1011,definition,
( spl0_75
<=> product(e_4,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f1012,plain,
( ~ product(e_4,e_3,e_3)
| spl0_75 ),
inference(avatar_component_clause,[],[f1011]) ).
fof(f1013,plain,
( product(e_4,e_3,e_3)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f1011]) ).
fof(f1015,definition,
( spl0_76
<=> product(e_4,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f1016,plain,
( ~ product(e_4,e_3,e_2)
| spl0_76 ),
inference(avatar_component_clause,[],[f1015]) ).
fof(f1017,plain,
( product(e_4,e_3,e_2)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f1015]) ).
fof(f1019,definition,
( spl0_77
<=> product(e_4,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f1020,plain,
( ~ product(e_4,e_3,e_1)
| spl0_77 ),
inference(avatar_component_clause,[],[f1019]) ).
fof(f1021,plain,
( product(e_4,e_3,e_1)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f1019]) ).
fof(f1039,definition,
( spl0_78
<=> product(e_3,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f1041,plain,
( product(e_3,e_3,e_3)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f1039]) ).
fof(f1043,definition,
( spl0_79
<=> product(e_3,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f1044,plain,
( ~ product(e_3,e_3,e_2)
| spl0_79 ),
inference(avatar_component_clause,[],[f1043]) ).
fof(f1045,plain,
( product(e_3,e_3,e_2)
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f1043]) ).
fof(f1047,definition,
( spl0_80
<=> product(e_3,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f1049,plain,
( product(e_3,e_3,e_1)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f1047]) ).
fof(f1073,plain,
( ! [X0] :
( ~ product(e_3,e_3,X0)
| ~ product(e_3,e_3,X0) )
| ~ spl0_75 ),
inference(resolution,[],[f1013,f277]) ).
fof(f1081,plain,
( ! [X0] : ~ product(e_3,e_3,X0)
| ~ spl0_75 ),
inference(duplicate_literal_removal,[],[f1073]) ).
fof(f1087,definition,
( spl0_81
<=> product(e_2,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f1088,plain,
( product(e_2,e_2,e_3)
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1089,plain,
( ~ product(e_2,e_2,e_3)
| spl0_81 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1108,plain,
! [X0,X1] :
( ~ product(X1,e_3,e_4)
| ~ product(X0,X1,e_4)
| ~ product(X1,e_4,X1) ),
inference(factoring,[],[f524]) ).
fof(f1116,plain,
( ~ product(e_2,e_2,e_1)
| ~ spl0_40 ),
inference(resolution,[],[f483,f63]) ).
fof(f1117,plain,
( ~ product(e_1,e_2,e_1)
| ~ spl0_40 ),
inference(resolution,[],[f483,f54]) ).
fof(f1152,plain,
( ~ product(e_2,e_4,e_3)
| ~ spl0_72 ),
inference(resolution,[],[f976,f63]) ).
fof(f1153,plain,
( ~ product(e_1,e_4,e_3)
| ~ spl0_72 ),
inference(resolution,[],[f976,f54]) ).
fof(f1155,plain,
( ~ product(e_4,e_2,e_3)
| ~ spl0_72 ),
inference(resolution,[],[f976,f64]) ).
fof(f1156,plain,
( ~ product(e_4,e_1,e_3)
| ~ spl0_72 ),
inference(resolution,[],[f976,f55]) ).
fof(f1182,plain,
( ~ product(e_2,e_4,e_2)
| ~ spl0_73 ),
inference(resolution,[],[f980,f63]) ).
fof(f1183,plain,
( ~ product(e_1,e_4,e_2)
| ~ spl0_73 ),
inference(resolution,[],[f980,f54]) ).
fof(f1184,plain,
( ~ product(e_4,e_3,e_2)
| ~ spl0_73 ),
inference(resolution,[],[f980,f73]) ).
fof(f1186,plain,
( ~ product(e_4,e_1,e_2)
| ~ spl0_73 ),
inference(resolution,[],[f980,f55]) ).
fof(f1189,plain,
( ~ spl0_13
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1183,f978,f248]) ).
fof(f1193,plain,
( ~ product(e_4,e_4,e_4)
| ~ group_element(e_4)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3) ),
inference(factoring,[],[f467]) ).
fof(f1207,plain,
( ~ product(e_2,e_4,e_1)
| ~ spl0_74 ),
inference(resolution,[],[f984,f63]) ).
fof(f1208,plain,
( ~ product(e_1,e_4,e_1)
| ~ spl0_74 ),
inference(resolution,[],[f984,f54]) ).
fof(f1209,plain,
( ~ product(e_4,e_3,e_1)
| ~ spl0_74 ),
inference(resolution,[],[f984,f73]) ).
fof(f1210,plain,
( ~ product(e_4,e_2,e_1)
| ~ spl0_74 ),
inference(resolution,[],[f984,f64]) ).
fof(f1214,plain,
( ~ spl0_14
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f1208,f982,f252]) ).
fof(f1216,plain,
( ~ spl0_40
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f1210,f982,f481]) ).
fof(f1220,definition,
( spl0_83
<=> ! [X0] :
( ~ product(X0,e_4,e_4)
| product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f1221,plain,
( ! [X0] :
( ~ product(X0,e_4,e_4)
| product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0) )
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f1220]) ).
fof(f1224,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ group_element(e_2)
| ~ spl0_42 ),
inference(resolution,[],[f496,f38]) ).
fof(f1225,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ spl0_42 ),
inference(duplicate_literal_removal,[],[f1224]) ).
fof(f1226,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f1225,f23]) ).
fof(f1227,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f1226,f496]) ).
fof(f1228,plain,
( product(e_2,e_2,e_1)
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f1227,f496]) ).
fof(f1229,plain,
( $false
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f1228,f496]) ).
fof(f1230,plain,
~ spl0_42,
inference(avatar_contradiction_clause,[],[f1229]) ).
fof(f1282,definition,
( spl0_84
<=> product(e_2,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f1284,plain,
( product(e_2,e_2,e_1)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f1282]) ).
fof(f1286,definition,
( spl0_85
<=> product(e_3,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f1288,plain,
( ~ product(e_3,e_2,e_4)
| spl0_85 ),
inference(avatar_component_clause,[],[f1286]) ).
fof(f1290,definition,
( spl0_86
<=> product(e_2,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f1292,plain,
( product(e_2,e_2,e_2)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f1290]) ).
fof(f1304,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| ~ group_element(e_2)
| ~ product(e_3,e_2,e_4)
| product(e_2,e_3,e_1)
| ~ spl0_16 ),
inference(resolution,[],[f710,f271]) ).
fof(f1307,plain,
( product(e_2,e_3,e_2)
| ~ group_element(e_2)
| ~ product(e_3,e_2,e_4)
| product(e_2,e_3,e_1)
| ~ spl0_16
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f1304,f447]) ).
fof(f1308,plain,
( product(e_2,e_3,e_2)
| ~ product(e_3,e_2,e_4)
| product(e_2,e_3,e_1)
| ~ spl0_16
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f1307,f23]) ).
fof(f1310,definition,
( spl0_87
<=> product(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f1311,plain,
( ~ product(e_2,e_3,e_1)
| spl0_87 ),
inference(avatar_component_clause,[],[f1310]) ).
fof(f1314,definition,
( spl0_88
<=> product(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f1316,plain,
( product(e_2,e_3,e_2)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f1314]) ).
fof(f1317,plain,
( spl0_87
| ~ spl0_85
| spl0_88
| ~ spl0_16
| spl0_35 ),
inference(avatar_split_clause,[],[f1308,f445,f269,f1314,f1286,f1310]) ).
fof(f1319,plain,
( ~ group_element(e_3)
| product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| ~ group_element(e_3)
| ~ spl0_75 ),
inference(resolution,[],[f1081,f38]) ).
fof(f1320,plain,
( ~ group_element(e_3)
| product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| ~ spl0_75 ),
inference(duplicate_literal_removal,[],[f1319]) ).
fof(f1321,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f1320,f24]) ).
fof(f1322,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f1321,f1081]) ).
fof(f1323,plain,
( product(e_3,e_3,e_1)
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f1322,f1081]) ).
fof(f1324,plain,
( $false
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f1323,f1081]) ).
fof(f1325,plain,
~ spl0_75,
inference(avatar_contradiction_clause,[],[f1324]) ).
fof(f1356,plain,
( ~ spl0_45
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f1152,f974,f543]) ).
fof(f1376,plain,
( ~ product(e_4,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(forward_subsumption_resolution,[],[f1193,f25]) ).
fof(f1383,plain,
( ! [X0] :
( ~ product(X0,e_2,e_4)
| ~ product(e_4,X0,e_2) )
| spl0_41 ),
inference(resolution,[],[f492,f42]) ).
fof(f1384,plain,
( spl0_70
| spl0_41 ),
inference(avatar_split_clause,[],[f1383,f490,f962]) ).
fof(f1418,plain,
( ~ product(e_1,e_4,e_2)
| ~ spl0_46 ),
inference(resolution,[],[f549,f48]) ).
fof(f1419,plain,
( ~ product(e_2,e_3,e_2)
| ~ spl0_46 ),
inference(resolution,[],[f549,f73]) ).
fof(f1420,plain,
( ~ product(e_2,e_2,e_2)
| ~ spl0_46 ),
inference(resolution,[],[f549,f64]) ).
fof(f1422,plain,
( ~ spl0_86
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f1420,f547,f1290]) ).
fof(f1423,plain,
( ~ spl0_88
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f1419,f547,f1314]) ).
fof(f1424,plain,
( ~ spl0_13
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f1418,f547,f248]) ).
fof(f1443,plain,
( ~ product(e_4,e_1,e_2)
| spl0_3
| ~ spl0_47 ),
inference(resolution,[],[f553,f129]) ).
fof(f1449,plain,
( ~ product(e_1,e_4,e_1)
| ~ spl0_47 ),
inference(resolution,[],[f553,f48]) ).
fof(f1456,plain,
( ~ product(e_2,e_3,e_1)
| ~ spl0_47 ),
inference(resolution,[],[f553,f73]) ).
fof(f1457,plain,
( ~ product(e_2,e_2,e_1)
| ~ spl0_47 ),
inference(resolution,[],[f553,f64]) ).
fof(f1458,plain,
( ~ product(e_2,e_1,e_1)
| ~ spl0_47 ),
inference(resolution,[],[f553,f55]) ).
fof(f1459,plain,
( ~ spl0_57
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1458,f551,f658]) ).
fof(f1460,plain,
( ~ spl0_84
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1457,f551,f1282]) ).
fof(f1461,plain,
( ~ spl0_87
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1456,f551,f1310]) ).
fof(f1462,plain,
( ~ spl0_14
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1449,f551,f252]) ).
fof(f1465,plain,
( ~ spl0_56
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f226,f186,f654]) ).
fof(f1469,plain,
( ~ spl0_10
| spl0_3
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1443,f551,f117,f190]) ).
fof(f1470,plain,
( ~ spl0_9
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f1156,f974,f186]) ).
fof(f1480,plain,
( ~ spl0_47
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f1207,f982,f551]) ).
fof(f1509,plain,
! [X0] :
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| ~ group_element(e_4)
| ~ product(X0,e_4,e_4)
| product(e_4,e_4,e_1)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| ~ group_element(e_3) ),
inference(resolution,[],[f777,f38]) ).
fof(f1607,plain,
( ~ product(e_4,e_3,e_4)
| ~ spl0_76 ),
inference(resolution,[],[f1017,f65]) ).
fof(f1619,plain,
( ~ product(e_2,e_3,e_2)
| ~ spl0_76 ),
inference(resolution,[],[f1017,f63]) ).
fof(f1620,plain,
( ~ product(e_1,e_3,e_2)
| ~ spl0_76 ),
inference(resolution,[],[f1017,f54]) ).
fof(f1624,plain,
( ~ product(e_4,e_1,e_2)
| ~ spl0_76 ),
inference(resolution,[],[f1017,f52]) ).
fof(f1627,plain,
( $false
| ~ spl0_16
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f1620,f271]) ).
fof(f1628,plain,
( ~ spl0_16
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f1627]) ).
fof(f1629,plain,
( ~ spl0_88
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f1619,f1015,f1314]) ).
fof(f1633,plain,
( ~ spl0_77
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f1209,f982,f1019]) ).
fof(f1698,plain,
( ~ product(e_3,e_1,e_3)
| spl0_5
| ~ spl0_80 ),
inference(resolution,[],[f1049,f161]) ).
fof(f1706,plain,
( ~ product(e_4,e_3,e_1)
| ~ spl0_80 ),
inference(resolution,[],[f1049,f72]) ).
fof(f1712,plain,
( ~ product(e_3,e_2,e_1)
| ~ spl0_80 ),
inference(resolution,[],[f1049,f61]) ).
fof(f1715,plain,
( ~ spl0_23
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f1712,f1047,f350]) ).
fof(f1720,definition,
( spl0_98
<=> product(e_3,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f1721,plain,
( product(e_3,e_1,e_4)
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f1720]) ).
fof(f1722,plain,
( ~ product(e_3,e_1,e_4)
| spl0_98 ),
inference(avatar_component_clause,[],[f1720]) ).
fof(f1726,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3) ),
inference(resolution,[],[f650,f24]) ).
fof(f1733,definition,
( spl0_99
<=> product(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f1734,plain,
( ~ product(e_1,e_2,e_3)
| spl0_99 ),
inference(avatar_component_clause,[],[f1733]) ).
fof(f1735,plain,
( product(e_1,e_2,e_3)
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f1733]) ).
fof(f1737,definition,
( spl0_100
<=> product(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f1738,plain,
( ~ product(e_1,e_2,e_1)
| spl0_100 ),
inference(avatar_component_clause,[],[f1737]) ).
fof(f1739,plain,
( product(e_1,e_2,e_1)
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f1737]) ).
fof(f1743,plain,
( product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_1)
| product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3) ),
inference(resolution,[],[f681,f24]) ).
fof(f1765,plain,
( ~ product(e_4,e_3,e_2)
| ~ spl0_79 ),
inference(resolution,[],[f1045,f72]) ).
fof(f1766,plain,
( ~ product(e_2,e_3,e_2)
| ~ spl0_79 ),
inference(resolution,[],[f1045,f60]) ).
fof(f1768,plain,
( ~ product(e_1,e_3,e_2)
| ~ spl0_79 ),
inference(resolution,[],[f1045,f51]) ).
fof(f1772,plain,
( ~ product(e_3,e_1,e_2)
| ~ spl0_79 ),
inference(resolution,[],[f1045,f52]) ).
fof(f1773,plain,
( ~ spl0_58
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f1772,f1043,f692]) ).
fof(f1775,plain,
( $false
| ~ spl0_16
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f1768,f271]) ).
fof(f1776,plain,
( ~ spl0_16
| ~ spl0_79 ),
inference(avatar_contradiction_clause,[],[f1775]) ).
fof(f1777,plain,
( ~ spl0_88
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f1766,f1043,f1314]) ).
fof(f1780,plain,
( ~ spl0_6
| spl0_5
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f1698,f1047,f151,f155]) ).
fof(f1784,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3) ),
inference(resolution,[],[f689,f22]) ).
fof(f1785,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[],[f689,f23]) ).
fof(f1786,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3) ),
inference(resolution,[],[f689,f24]) ).
fof(f1817,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3) ),
inference(resolution,[],[f712,f23]) ).
fof(f1838,plain,
( ~ product(e_1,e_1,e_3)
| ~ spl0_99 ),
inference(resolution,[],[f1735,f49]) ).
fof(f1839,plain,
( ~ spl0_25
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f1838,f1733,f364]) ).
fof(f1843,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3) ),
inference(resolution,[],[f717,f24]) ).
fof(f1844,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3) ),
inference(resolution,[],[f717,f25]) ).
fof(f1849,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3) ),
inference(resolution,[],[f726,f22]) ).
fof(f1860,plain,
( ~ spl0_99
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f583,f473,f1733]) ).
fof(f1862,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3) ),
inference(resolution,[],[f735,f23]) ).
fof(f1863,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3) ),
inference(resolution,[],[f735,f24]) ).
fof(f1872,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[],[f758,f22]) ).
fof(f1873,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3) ),
inference(resolution,[],[f758,f23]) ).
fof(f1874,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_1)
| product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3) ),
inference(resolution,[],[f758,f24]) ).
fof(f1875,plain,
( product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_1)
| product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3) ),
inference(resolution,[],[f758,f25]) ).
fof(f1883,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3) ),
inference(resolution,[],[f763,f25]) ).
fof(f1901,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[],[f768,f22]) ).
fof(f1916,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3) ),
inference(resolution,[],[f773,f25]) ).
fof(f1920,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3) ),
inference(resolution,[],[f779,f22]) ).
fof(f1922,plain,
( product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| product(e_3,e_4,e_1)
| product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3) ),
inference(resolution,[],[f779,f24]) ).
fof(f1923,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_1)
| product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3) ),
inference(resolution,[],[f779,f25]) ).
fof(f1951,plain,
( ~ product(e_1,e_3,e_2)
| ~ spl0_13 ),
inference(resolution,[],[f250,f73]) ).
fof(f1952,plain,
( ~ product(e_1,e_2,e_2)
| ~ spl0_13 ),
inference(resolution,[],[f250,f64]) ).
fof(f1953,plain,
( ~ product(e_1,e_1,e_2)
| ~ spl0_13 ),
inference(resolution,[],[f250,f55]) ).
fof(f1954,plain,
( ~ spl0_27
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1953,f248,f374]) ).
fof(f1973,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_100 ),
inference(resolution,[],[f1739,f49]) ).
fof(f1974,plain,
( ~ spl0_26
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f1973,f1737,f368]) ).
fof(f1978,definition,
( spl0_101
<=> product(e_2,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f1979,plain,
( product(e_2,e_1,e_4)
| ~ spl0_101 ),
inference(avatar_component_clause,[],[f1978]) ).
fof(f1980,plain,
( ~ product(e_2,e_1,e_4)
| spl0_101 ),
inference(avatar_component_clause,[],[f1978]) ).
fof(f1982,plain,
( ~ spl0_16
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1951,f248,f269]) ).
fof(f2010,plain,
( ~ spl0_100
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f427,f273,f1737]) ).
fof(f2022,plain,
( ~ spl0_77
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f1706,f1047,f1019]) ).
fof(f2059,plain,
( ~ group_element(e_3)
| product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| ~ group_element(e_4)
| spl0_44 ),
inference(resolution,[],[f535,f38]) ).
fof(f2060,plain,
( ! [X0] :
( ~ product(e_3,X0,e_4)
| ~ product(X0,e_4,e_4) )
| spl0_44 ),
inference(resolution,[],[f535,f42]) ).
fof(f2061,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| ~ group_element(e_4)
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f2059,f24]) ).
fof(f2097,plain,
( ~ product(e_2,e_3,e_1)
| ~ spl0_77 ),
inference(resolution,[],[f1021,f63]) ).
fof(f2098,plain,
( ~ product(e_1,e_3,e_1)
| ~ spl0_77 ),
inference(resolution,[],[f1021,f54]) ).
fof(f2101,plain,
( ~ product(e_4,e_2,e_1)
| ~ spl0_77 ),
inference(resolution,[],[f1021,f61]) ).
fof(f2103,plain,
( ~ spl0_17
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f2098,f1019,f273]) ).
fof(f2104,plain,
( ~ spl0_87
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f2097,f1019,f1310]) ).
fof(f2118,plain,
( ~ product(e_1,e_3,e_3)
| ~ spl0_78 ),
inference(resolution,[],[f1041,f51]) ).
fof(f2162,plain,
( ~ product(e_3,e_3,e_3)
| ~ spl0_69 ),
inference(factoring,[],[f883]) ).
fof(f2169,plain,
( ~ product(e_1,e_2,e_4)
| ~ spl0_10
| ~ spl0_70 ),
inference(resolution,[],[f963,f192]) ).
fof(f2177,plain,
( ! [X0] :
( ~ product(X0,e_4,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| ~ group_element(e_3) )
| spl0_44 ),
inference(resolution,[],[f2060,f38]) ).
fof(f2179,plain,
( ! [X0] :
( ~ product(X0,e_4,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3) )
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f2177,f24]) ).
fof(f2180,plain,
( spl0_83
| spl0_44 ),
inference(avatar_split_clause,[],[f2179,f533,f1220]) ).
fof(f2221,plain,
( ~ group_element(e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| ~ spl0_15 ),
inference(resolution,[],[f257,f104]) ).
fof(f2240,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f2221,f24]) ).
fof(f2256,plain,
( ~ product(e_1,e_1,e_4)
| ~ product(e_1,e_4,e_1) ),
inference(factoring,[],[f899]) ).
fof(f2263,plain,
( ~ product(e_4,e_2,e_3)
| ~ spl0_19
| spl0_35 ),
inference(resolution,[],[f306,f759]) ).
fof(f2276,plain,
( ~ product(e_4,e_4,e_2)
| ~ spl0_19 ),
inference(resolution,[],[f306,f72]) ).
fof(f2277,plain,
( ~ product(e_2,e_4,e_2)
| ~ spl0_19 ),
inference(resolution,[],[f306,f60]) ).
fof(f2279,plain,
( ~ product(e_1,e_4,e_2)
| ~ spl0_19 ),
inference(resolution,[],[f306,f51]) ).
fof(f2280,plain,
( ~ product(e_3,e_3,e_2)
| ~ spl0_19 ),
inference(resolution,[],[f306,f73]) ).
fof(f2285,plain,
( $false
| ~ spl0_13
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2279,f250]) ).
fof(f2286,plain,
( ~ spl0_13
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2285]) ).
fof(f2299,plain,
( ~ product(e_4,e_1,e_3)
| spl0_5
| ~ spl0_20 ),
inference(resolution,[],[f310,f161]) ).
fof(f2307,plain,
( ~ product(e_4,e_4,e_1)
| ~ spl0_20 ),
inference(resolution,[],[f310,f72]) ).
fof(f2310,plain,
( ~ product(e_1,e_4,e_1)
| ~ spl0_20 ),
inference(resolution,[],[f310,f51]) ).
fof(f2312,plain,
( ~ product(e_3,e_2,e_1)
| ~ spl0_20 ),
inference(resolution,[],[f310,f64]) ).
fof(f2313,plain,
( ~ product(e_3,e_1,e_1)
| ~ spl0_20 ),
inference(resolution,[],[f310,f55]) ).
fof(f2314,plain,
( ~ spl0_59
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f2313,f308,f696]) ).
fof(f2315,plain,
( ~ spl0_23
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f2312,f308,f350]) ).
fof(f2325,plain,
( ~ group_element(e_2)
| product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| ~ group_element(e_3)
| spl0_85 ),
inference(resolution,[],[f1288,f38]) ).
fof(f2327,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| ~ group_element(e_3)
| spl0_85 ),
inference(forward_subsumption_resolution,[],[f2325,f23]) ).
fof(f2328,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| ~ group_element(e_3)
| spl0_21
| spl0_85 ),
inference(forward_subsumption_resolution,[],[f2327,f343]) ).
fof(f2329,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| spl0_21
| spl0_85 ),
inference(forward_subsumption_resolution,[],[f2328,f24]) ).
fof(f2330,plain,
( spl0_22
| spl0_23
| spl0_21
| spl0_85 ),
inference(avatar_split_clause,[],[f2329,f1286,f342,f350,f346]) ).
fof(f2334,plain,
( ~ product(e_3,e_3,e_4)
| ~ product(e_3,e_4,e_3) ),
inference(factoring,[],[f1108]) ).
fof(f2386,plain,
( ~ product(e_2,e_2,e_2)
| ~ spl0_88 ),
inference(resolution,[],[f1316,f61]) ).
fof(f2388,plain,
( $false
| ~ spl0_86
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f2386,f1292]) ).
fof(f2389,plain,
( ~ spl0_86
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f2388]) ).
fof(f2390,plain,
( ~ spl0_86
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f2386,f1314,f1290]) ).
fof(f2419,plain,
( ! [X0] :
( ~ product(e_2,e_2,X0)
| ~ product(e_2,e_2,X0) )
| ~ spl0_22 ),
inference(resolution,[],[f348,f198]) ).
fof(f2427,plain,
( ! [X0] : ~ product(e_2,e_2,X0)
| ~ spl0_22 ),
inference(duplicate_literal_removal,[],[f2419]) ).
fof(f2429,plain,
( spl0_42
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f2427,f346,f495]) ).
fof(f2431,plain,
( ~ spl0_81
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f582,f473,f1087]) ).
fof(f2432,plain,
( ~ spl0_81
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f748,f543,f1087]) ).
fof(f2452,plain,
( ~ product(e_1,e_2,e_1)
| ~ spl0_84 ),
inference(resolution,[],[f1284,f48]) ).
fof(f2463,plain,
( $false
| ~ spl0_84
| ~ spl0_100 ),
inference(forward_subsumption_resolution,[],[f2452,f1739]) ).
fof(f2464,plain,
( ~ spl0_84
| ~ spl0_100 ),
inference(avatar_contradiction_clause,[],[f2463]) ).
fof(f2472,plain,
( ~ spl0_84
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1116,f481,f1282]) ).
fof(f2477,plain,
( ~ spl0_78
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f2162,f882,f1039]) ).
fof(f2478,plain,
( ~ spl0_38
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f1155,f974,f473]) ).
fof(f2489,plain,
( ~ spl0_40
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f2101,f1019,f481]) ).
fof(f2500,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| ~ spl0_15
| spl0_87 ),
inference(forward_subsumption_resolution,[],[f2240,f1311]) ).
fof(f2501,plain,
( spl0_25
| spl0_27
| spl0_26
| spl0_6
| spl0_58
| spl0_59 ),
inference(avatar_split_clause,[],[f1784,f696,f692,f155,f368,f374,f364]) ).
fof(f2504,plain,
( spl0_6
| spl0_58
| spl0_59
| spl0_23
| spl0_21
| spl0_22 ),
inference(avatar_split_clause,[],[f1743,f346,f342,f350,f696,f692,f155]) ).
fof(f2520,plain,
( spl0_35
| spl0_88
| ~ spl0_15
| spl0_87 ),
inference(avatar_split_clause,[],[f2500,f1310,f256,f1314,f445]) ).
fof(f2546,plain,
( ~ spl0_76
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1184,f978,f1015]) ).
fof(f2547,plain,
( ~ spl0_10
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1186,f978,f190]) ).
fof(f2549,plain,
( ~ spl0_10
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f1624,f1015,f190]) ).
fof(f2554,plain,
( ~ spl0_100
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1117,f481,f1737]) ).
fof(f2560,plain,
( product(e_4,e_3,e_2)
| product(e_4,e_3,e_1)
| product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| spl0_75 ),
inference(forward_subsumption_resolution,[],[f1875,f1012]) ).
fof(f2562,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| spl0_75 ),
inference(forward_subsumption_resolution,[],[f1843,f1012]) ).
fof(f2563,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| ~ group_element(e_4)
| spl0_44
| spl0_75 ),
inference(forward_subsumption_resolution,[],[f2061,f1012]) ).
fof(f2564,plain,
( ~ spl0_76
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f1765,f1043,f1015]) ).
fof(f2571,plain,
( ~ spl0_14
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f2256,f354,f252]) ).
fof(f2572,plain,
( ~ spl0_14
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f2310,f308,f252]) ).
fof(f2586,plain,
( ~ spl0_9
| spl0_5
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f2299,f308,f151,f186]) ).
fof(f2593,plain,
( product(e_4,e_3,e_2)
| product(e_4,e_3,e_1)
| product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| spl0_39
| spl0_75 ),
inference(forward_subsumption_resolution,[],[f2560,f478]) ).
fof(f2596,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| spl0_44
| spl0_75 ),
inference(forward_subsumption_resolution,[],[f2563,f25]) ).
fof(f2616,plain,
( spl0_38
| spl0_40
| spl0_77
| spl0_76
| spl0_39
| spl0_75 ),
inference(avatar_split_clause,[],[f2593,f1011,f477,f1015,f1019,f481,f473]) ).
fof(f2619,plain,
( spl0_76
| spl0_77
| spl0_44
| spl0_75 ),
inference(avatar_split_clause,[],[f2596,f1011,f533,f1019,f1015]) ).
fof(f2635,plain,
( ~ spl0_78
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f943,f300,f1039]) ).
fof(f2637,plain,
( ~ spl0_6
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f945,f300,f155]) ).
fof(f2638,plain,
( ~ spl0_72
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f939,f300,f974]) ).
fof(f2639,plain,
( ~ spl0_45
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f940,f300,f543]) ).
fof(f2656,definition,
( spl0_104
<=> product(e_3,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f2658,plain,
( ~ product(e_3,e_3,e_4)
| spl0_104 ),
inference(avatar_component_clause,[],[f2656]) ).
fof(f2659,plain,
( ~ spl0_18
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f2334,f2656,f300]) ).
fof(f2698,plain,
( ! [X0,X1] :
( ~ product(X1,e_2,e_3)
| ~ product(X1,e_3,X0)
| ~ product(e_4,e_3,X0) )
| ~ spl0_35 ),
inference(resolution,[],[f446,f514]) ).
fof(f2705,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| ~ group_element(e_3)
| ~ product(e_3,e_3,e_4)
| product(e_3,e_3,e_1)
| ~ spl0_35 ),
inference(resolution,[],[f446,f756]) ).
fof(f2713,plain,
( product(e_3,e_3,e_3)
| ~ group_element(e_3)
| ~ product(e_3,e_3,e_4)
| product(e_3,e_3,e_1)
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f2705,f65]) ).
fof(f2716,plain,
( ~ group_element(e_3)
| ~ product(e_3,e_3,e_4)
| product(e_3,e_3,e_1)
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f2713,f74]) ).
fof(f2717,plain,
( ~ product(e_3,e_3,e_4)
| product(e_3,e_3,e_1)
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f2716,f24]) ).
fof(f2718,plain,
( ~ product(e_3,e_3,e_4)
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f2717,f56]) ).
fof(f2719,plain,
( ~ spl0_104
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f2718,f445,f2656]) ).
fof(f2793,plain,
( ~ product(e_4,e_4,e_4)
| product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| ~ group_element(e_4)
| ~ spl0_71 ),
inference(resolution,[],[f966,f498]) ).
fof(f2900,plain,
( ~ group_element(e_3)
| product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| ~ group_element(e_3)
| spl0_104 ),
inference(resolution,[],[f2658,f38]) ).
fof(f2902,plain,
( ~ group_element(e_3)
| product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| spl0_104 ),
inference(duplicate_literal_removal,[],[f2900]) ).
fof(f2911,plain,
( ! [X0] :
( ~ product(e_4,e_3,X0)
| ~ product(e_4,e_3,X0) )
| ~ spl0_35
| ~ spl0_38 ),
inference(resolution,[],[f2698,f475]) ).
fof(f2912,plain,
( ! [X0] : ~ product(e_4,e_3,X0)
| ~ spl0_35
| ~ spl0_38 ),
inference(duplicate_literal_removal,[],[f2911]) ).
fof(f2922,plain,
( $false
| ~ spl0_35
| ~ spl0_38
| ~ spl0_77 ),
inference(resolution,[],[f2912,f1021]) ).
fof(f2925,plain,
( ~ spl0_35
| ~ spl0_38
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f2922]) ).
fof(f2928,plain,
( ~ spl0_13
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f2279,f304,f248]) ).
fof(f2929,plain,
( ~ spl0_79
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f2280,f304,f1043]) ).
fof(f2934,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| spl0_104 ),
inference(forward_subsumption_resolution,[],[f2902,f24]) ).
fof(f2936,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| ~ group_element(e_4)
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f2793,f966]) ).
fof(f2947,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| ~ group_element(e_4)
| spl0_39
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f2936,f478]) ).
fof(f2955,definition,
( spl0_106
<=> product(e_1,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f2956,plain,
( product(e_1,e_2,e_4)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f2955]) ).
fof(f2957,plain,
( ~ product(e_1,e_2,e_4)
| spl0_106 ),
inference(avatar_component_clause,[],[f2955]) ).
fof(f2960,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| spl0_39
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f2947,f25]) ).
fof(f2962,plain,
( spl0_38
| spl0_40
| spl0_39
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f2960,f965,f477,f481,f473]) ).
fof(f2988,plain,
( ~ spl0_46
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1182,f978,f547]) ).
fof(f3019,plain,
( ! [X0] :
( ~ product(e_3,e_4,X0)
| ~ product(e_4,e_3,X0) )
| ~ spl0_44 ),
inference(resolution,[],[f534,f277]) ).
fof(f3040,plain,
( ~ product(e_1,e_3,e_4)
| ~ spl0_9
| spl0_43 ),
inference(resolution,[],[f188,f566]) ).
fof(f3057,plain,
( ~ spl0_15
| ~ spl0_9
| spl0_43 ),
inference(avatar_split_clause,[],[f3040,f529,f186,f256]) ).
fof(f3126,plain,
( ~ product(e_2,e_3,e_3)
| ~ spl0_67
| ~ spl0_99 ),
inference(resolution,[],[f1735,f858]) ).
fof(f3149,plain,
( spl0_25
| spl0_27
| spl0_26
| spl0_14
| spl0_12
| spl0_13 ),
inference(avatar_split_clause,[],[f1849,f248,f244,f252,f368,f374,f364]) ).
fof(f3154,plain,
( ~ spl0_12
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f942,f300,f244]) ).
fof(f3162,plain,
( spl0_99
| spl0_3
| spl0_100
| spl0_21
| spl0_22
| spl0_23 ),
inference(avatar_split_clause,[],[f1785,f350,f346,f342,f1737,f117,f1733]) ).
fof(f3166,plain,
( spl0_99
| spl0_3
| spl0_100
| spl0_14
| spl0_12
| spl0_13 ),
inference(avatar_split_clause,[],[f1901,f248,f244,f252,f1737,f117,f1733]) ).
fof(f3168,plain,
( ~ spl0_106
| ~ spl0_10
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f2169,f962,f190,f2955]) ).
fof(f3169,plain,
( ~ spl0_3
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1952,f248,f117]) ).
fof(f3208,plain,
( ~ group_element(e_4)
| product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| ~ spl0_41 ),
inference(resolution,[],[f491,f213]) ).
fof(f3211,plain,
( product(e_3,e_2,e_3)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1)
| ~ group_element(e_2)
| ~ spl0_41
| ~ spl0_83 ),
inference(resolution,[],[f491,f1221]) ).
fof(f3226,plain,
( ! [X0,X1] :
( ~ product(e_4,X0,e_4)
| ~ product(e_4,e_4,X1)
| ~ product(X0,e_4,X1) )
| ~ spl0_41 ),
inference(resolution,[],[f491,f485]) ).
fof(f3232,plain,
( ! [X0,X1] :
( ~ product(e_4,X0,e_4)
| ~ product(X0,e_4,X1) )
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f3226,f42]) ).
fof(f3233,plain,
( product(e_3,e_2,e_3)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1)
| ~ spl0_41
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f3211,f23]) ).
fof(f3236,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f3208,f25]) ).
fof(f3237,plain,
( spl0_23
| spl0_22
| spl0_21
| ~ spl0_41
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f3233,f1220,f490,f342,f346,f350]) ).
fof(f3240,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| ~ spl0_41
| spl0_72 ),
inference(forward_subsumption_resolution,[],[f3236,f975]) ).
fof(f3242,plain,
( spl0_73
| spl0_74
| ~ spl0_41
| spl0_72 ),
inference(avatar_split_clause,[],[f3240,f974,f490,f982,f978]) ).
fof(f3243,plain,
( ~ spl0_35
| ~ spl0_67
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f3126,f1733,f857,f445]) ).
fof(f3244,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1817,f123]) ).
fof(f3248,plain,
( ! [X0] :
( product(e_4,e_4,e_2)
| ~ group_element(e_4)
| ~ product(X0,e_4,e_4)
| product(e_4,e_4,e_1)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| ~ group_element(e_3) )
| spl0_72 ),
inference(forward_subsumption_resolution,[],[f1509,f975]) ).
fof(f3251,plain,
( spl0_56
| spl0_57
| spl0_87
| spl0_35
| spl0_88
| spl0_4 ),
inference(avatar_split_clause,[],[f3244,f121,f1314,f445,f1310,f658,f654]) ).
fof(f3255,plain,
( ! [X0] :
( product(e_4,e_4,e_2)
| ~ product(X0,e_4,e_4)
| product(e_4,e_4,e_1)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| ~ group_element(e_3) )
| spl0_72 ),
inference(forward_subsumption_resolution,[],[f3248,f25]) ).
fof(f3260,plain,
( ! [X0] :
( product(e_4,e_4,e_2)
| ~ product(X0,e_4,e_4)
| product(e_4,e_4,e_1)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3) )
| spl0_72 ),
inference(forward_subsumption_resolution,[],[f3255,f24]) ).
fof(f3263,plain,
( spl0_74
| spl0_83
| spl0_73
| spl0_72 ),
inference(avatar_split_clause,[],[f3260,f974,f978,f1220,f982]) ).
fof(f3264,plain,
( ~ spl0_38
| ~ spl0_19
| spl0_35 ),
inference(avatar_split_clause,[],[f2263,f445,f304,f473]) ).
fof(f3265,plain,
( ~ spl0_73
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f2276,f304,f978]) ).
fof(f3268,plain,
( spl0_81
| spl0_86
| spl0_84
| spl0_21
| spl0_22
| spl0_23 ),
inference(avatar_split_clause,[],[f1862,f350,f346,f342,f1282,f1290,f1087]) ).
fof(f3272,plain,
( spl0_81
| spl0_86
| spl0_84
| spl0_87
| spl0_35
| spl0_88 ),
inference(avatar_split_clause,[],[f1873,f1314,f445,f1310,f1282,f1290,f1087]) ).
fof(f3311,plain,
( ~ group_element(e_4)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| ~ spl0_41 ),
inference(resolution,[],[f561,f38]) ).
fof(f3313,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f3311,f25]) ).
fof(f3314,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f3313,f22]) ).
fof(f3315,plain,
( spl0_12
| spl0_13
| spl0_14
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f3314,f490,f252,f248,f244]) ).
fof(f3363,plain,
( ~ product(e_1,e_2,e_3)
| ~ spl0_81 ),
inference(resolution,[],[f1088,f48]) ).
fof(f3374,plain,
( ~ spl0_99
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f3363,f1087,f1733]) ).
fof(f3418,plain,
( ~ product(e_4,e_3,e_4)
| ~ group_element(e_4)
| product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| ~ group_element(e_3)
| ~ spl0_44 ),
inference(resolution,[],[f3019,f38]) ).
fof(f3419,plain,
( ~ group_element(e_4)
| product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| ~ group_element(e_3)
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f3418,f534]) ).
fof(f3420,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| ~ group_element(e_3)
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f3419,f25]) ).
fof(f3421,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f3420,f24]) ).
fof(f3422,plain,
( spl0_18
| spl0_19
| spl0_20
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f3421,f533,f308,f304,f300]) ).
fof(f3426,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| ~ group_element(e_3)
| ~ spl0_98 ),
inference(resolution,[],[f1721,f107]) ).
fof(f3453,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| ~ spl0_98 ),
inference(forward_subsumption_resolution,[],[f3426,f24]) ).
fof(f3455,plain,
( spl0_21
| spl0_22
| spl0_23
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f3453,f1720,f350,f346,f342]) ).
fof(f3464,plain,
( ~ group_element(e_1)
| product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| ~ group_element(e_3)
| spl0_98 ),
inference(resolution,[],[f1722,f38]) ).
fof(f3466,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| ~ group_element(e_3)
| spl0_98 ),
inference(forward_subsumption_resolution,[],[f3464,f22]) ).
fof(f3467,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| ~ group_element(e_3)
| spl0_6
| spl0_98 ),
inference(forward_subsumption_resolution,[],[f3466,f157]) ).
fof(f3468,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| spl0_6
| spl0_98 ),
inference(forward_subsumption_resolution,[],[f3467,f24]) ).
fof(f3469,plain,
( spl0_58
| spl0_59
| spl0_6
| spl0_98 ),
inference(avatar_split_clause,[],[f3468,f1720,f155,f696,f692]) ).
fof(f3483,plain,
( ~ group_element(e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| spl0_106 ),
inference(resolution,[],[f2957,f38]) ).
fof(f3485,plain,
( ! [X0] : ~ product(e_3,e_4,X0)
| ~ spl0_41
| ~ spl0_44 ),
inference(resolution,[],[f3232,f534]) ).
fof(f3491,plain,
( ~ group_element(e_4)
| product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| ~ group_element(e_3)
| ~ spl0_41
| ~ spl0_44 ),
inference(resolution,[],[f3485,f38]) ).
fof(f3492,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| ~ group_element(e_3)
| ~ spl0_41
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f3491,f25]) ).
fof(f3493,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| ~ group_element(e_3)
| ~ spl0_41
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f3492,f3485]) ).
fof(f3494,plain,
( product(e_3,e_4,e_1)
| ~ group_element(e_3)
| ~ spl0_41
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f3493,f3485]) ).
fof(f3495,plain,
( ~ group_element(e_3)
| ~ spl0_41
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f3494,f3485]) ).
fof(f3496,plain,
( $false
| ~ spl0_41
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f3495,f24]) ).
fof(f3497,plain,
( ~ spl0_41
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f3496]) ).
fof(f3498,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| spl0_106 ),
inference(forward_subsumption_resolution,[],[f3483,f23]) ).
fof(f3522,plain,
( ~ product(e_2,e_2,e_2)
| ~ spl0_3
| spl0_4 ),
inference(resolution,[],[f118,f828]) ).
fof(f3536,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ group_element(e_2)
| ~ product(e_2,e_2,e_4)
| product(e_2,e_2,e_1)
| ~ spl0_3 ),
inference(resolution,[],[f118,f677]) ).
fof(f3540,plain,
( ! [X0] :
( ~ product(e_4,X0,e_1)
| ~ product(X0,e_1,e_2) )
| ~ spl0_3 ),
inference(resolution,[],[f118,f219]) ).
fof(f3544,plain,
( ~ spl0_86
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f3522,f121,f117,f1290]) ).
fof(f3548,plain,
( ~ group_element(e_4)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| ~ group_element(e_2)
| spl0_41 ),
inference(resolution,[],[f492,f38]) ).
fof(f3550,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| ~ group_element(e_2)
| spl0_41 ),
inference(forward_subsumption_resolution,[],[f3548,f25]) ).
fof(f3628,plain,
( product(e_2,e_2,e_3)
| ~ group_element(e_2)
| ~ product(e_2,e_2,e_4)
| product(e_2,e_2,e_1)
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f3536,f65]) ).
fof(f3629,plain,
( ~ group_element(e_2)
| ~ product(e_2,e_2,e_4)
| product(e_2,e_2,e_1)
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f3628,f74]) ).
fof(f3630,plain,
( ~ product(e_2,e_2,e_4)
| product(e_2,e_2,e_1)
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f3629,f23]) ).
fof(f3631,plain,
( ~ product(e_2,e_2,e_4)
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f3630,f56]) ).
fof(f3632,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ group_element(e_2)
| ~ spl0_3 ),
inference(resolution,[],[f3631,f38]) ).
fof(f3634,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ spl0_3 ),
inference(duplicate_literal_removal,[],[f3632]) ).
fof(f3635,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f3634,f23]) ).
fof(f3636,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| ~ spl0_3
| spl0_81 ),
inference(forward_subsumption_resolution,[],[f3635,f1089]) ).
fof(f3637,plain,
( spl0_86
| spl0_84
| ~ spl0_3
| spl0_81 ),
inference(avatar_split_clause,[],[f3636,f1087,f117,f1282,f1290]) ).
fof(f3675,plain,
( ~ product(e_4,e_1,e_2)
| ~ spl0_3
| ~ spl0_74 ),
inference(resolution,[],[f3540,f984]) ).
fof(f3677,plain,
( $false
| ~ spl0_3
| ~ spl0_10
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f3675,f192]) ).
fof(f3678,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f3677]) ).
fof(f3682,plain,
( product(e_1,e_3,e_3)
| product(e_1,e_3,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1872,f270]) ).
fof(f3710,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| ~ group_element(e_3)
| ~ product(e_3,e_3,e_4)
| product(e_3,e_3,e_1)
| ~ spl0_5 ),
inference(resolution,[],[f152,f710]) ).
fof(f3716,plain,
( ~ product(e_1,e_2,e_3)
| ~ spl0_5 ),
inference(resolution,[],[f152,f61]) ).
fof(f3717,plain,
( ~ product(e_1,e_1,e_3)
| ~ spl0_5 ),
inference(resolution,[],[f152,f52]) ).
fof(f3718,plain,
( ~ spl0_25
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f3717,f151,f364]) ).
fof(f3721,plain,
( ~ spl0_74
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f2307,f308,f982]) ).
fof(f3722,plain,
( $false
| ~ spl0_5
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f2118,f152]) ).
fof(f3723,plain,
( ~ spl0_5
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f3722]) ).
fof(f3726,plain,
( ~ spl0_99
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f3716,f151,f1733]) ).
fof(f3753,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f1863,f447]) ).
fof(f3754,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_80
| spl0_78
| spl0_79 ),
inference(avatar_split_clause,[],[f1874,f1043,f1039,f1047,f350,f346,f342]) ).
fof(f3756,plain,
( spl0_78
| spl0_79
| spl0_80
| spl0_20
| spl0_18
| spl0_19 ),
inference(avatar_split_clause,[],[f1922,f304,f300,f308,f1047,f1043,f1039]) ).
fof(f3757,plain,
( spl0_78
| spl0_79
| spl0_80
| spl0_104 ),
inference(avatar_split_clause,[],[f2934,f2656,f1047,f1043,f1039]) ).
fof(f3761,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| spl0_41 ),
inference(forward_subsumption_resolution,[],[f3550,f23]) ).
fof(f3768,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| spl0_106 ),
inference(forward_subsumption_resolution,[],[f3498,f22]) ).
fof(f3770,plain,
( spl0_88
| spl0_87
| spl0_78
| spl0_79
| spl0_80
| spl0_35 ),
inference(avatar_split_clause,[],[f3753,f445,f1047,f1043,f1039,f1310,f1314]) ).
fof(f3772,plain,
( spl0_45
| spl0_46
| spl0_47
| spl0_41 ),
inference(avatar_split_clause,[],[f3761,f490,f551,f547,f543]) ).
fof(f3776,plain,
( spl0_99
| spl0_3
| spl0_100
| spl0_106 ),
inference(avatar_split_clause,[],[f3768,f2955,f1737,f117,f1733]) ).
fof(f3787,plain,
( ~ spl0_44
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f1607,f1015,f533]) ).
fof(f3789,plain,
( product(e_3,e_3,e_3)
| ~ group_element(e_3)
| ~ product(e_3,e_3,e_4)
| product(e_3,e_3,e_1)
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f3710,f65]) ).
fof(f3794,plain,
( spl0_45
| spl0_46
| spl0_47
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f1376,f965,f551,f547,f543]) ).
fof(f3799,plain,
( ~ group_element(e_3)
| ~ product(e_3,e_3,e_4)
| product(e_3,e_3,e_1)
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f3789,f74]) ).
fof(f3806,plain,
( ~ product(e_3,e_3,e_4)
| product(e_3,e_3,e_1)
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f3799,f24]) ).
fof(f3807,plain,
( ~ product(e_3,e_3,e_4)
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f3806,f56]) ).
fof(f3808,plain,
( ~ spl0_104
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f3807,f151,f2656]) ).
fof(f3811,plain,
( ~ spl0_46
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f2277,f304,f547]) ).
fof(f3812,plain,
( spl0_99
| spl0_3
| spl0_100
| spl0_17
| spl0_5
| spl0_16 ),
inference(avatar_split_clause,[],[f3682,f269,f151,f273,f1737,f117,f1733]) ).
fof(f3821,plain,
( ~ group_element(e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| ~ group_element(e_2)
| ~ spl0_34 ),
inference(resolution,[],[f436,f38]) ).
fof(f3822,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| ~ group_element(e_2)
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f3821,f24]) ).
fof(f3823,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| ~ group_element(e_2)
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f3822,f436]) ).
fof(f3824,plain,
( product(e_2,e_3,e_1)
| ~ group_element(e_2)
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f3823,f436]) ).
fof(f3825,plain,
( ~ group_element(e_2)
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f3824,f436]) ).
fof(f3826,plain,
( $false
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f3825,f23]) ).
fof(f3827,plain,
~ spl0_34,
inference(avatar_contradiction_clause,[],[f3826]) ).
fof(f3911,plain,
( ~ product(e_3,e_2,e_4)
| ~ spl0_70
| ~ spl0_76 ),
inference(resolution,[],[f1017,f963]) ).
fof(f3931,plain,
( ~ spl0_85
| ~ spl0_70
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f3911,f1015,f962,f1286]) ).
fof(f3944,plain,
( ~ group_element(e_4)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| ~ spl0_71 ),
inference(resolution,[],[f998,f38]) ).
fof(f3946,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f3944,f25]) ).
fof(f3947,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| spl0_13
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f3946,f249]) ).
fof(f3948,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_3)
| spl0_13
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f3947,f22]) ).
fof(f3949,plain,
( spl0_12
| spl0_14
| spl0_13
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f3948,f965,f248,f252,f244]) ).
fof(f3956,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ group_element(e_2)
| ~ spl0_101 ),
inference(resolution,[],[f1979,f107]) ).
fof(f3964,plain,
( ~ product(e_4,e_2,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| ~ spl0_101 ),
inference(resolution,[],[f1979,f498]) ).
fof(f3978,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| ~ spl0_40
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f3964,f483]) ).
fof(f3980,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| ~ group_element(e_2)
| spl0_81
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f3956,f1089]) ).
fof(f3982,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| ~ spl0_40
| spl0_100
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f3978,f1738]) ).
fof(f3984,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| spl0_81
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f3980,f23]) ).
fof(f3986,plain,
( product(e_1,e_2,e_3)
| ~ group_element(e_1)
| spl0_3
| ~ spl0_40
| spl0_100
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f3982,f119]) ).
fof(f3988,plain,
( spl0_86
| spl0_84
| spl0_81
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f3984,f1978,f1087,f1282,f1290]) ).
fof(f3990,plain,
( ~ group_element(e_1)
| spl0_3
| ~ spl0_40
| spl0_99
| spl0_100
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f3986,f1734]) ).
fof(f3991,plain,
( $false
| spl0_3
| ~ spl0_40
| spl0_99
| spl0_100
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f3990,f22]) ).
fof(f3992,plain,
( spl0_3
| ~ spl0_40
| spl0_99
| spl0_100
| ~ spl0_101 ),
inference(avatar_contradiction_clause,[],[f3991]) ).
fof(f3995,plain,
( product(e_3,e_4,e_3)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_1)
| ~ group_element(e_4)
| ~ spl0_71
| ~ spl0_83 ),
inference(resolution,[],[f1221,f966]) ).
fof(f3997,plain,
( product(e_3,e_4,e_3)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_1)
| ~ spl0_71
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f3995,f25]) ).
fof(f3999,plain,
( spl0_20
| spl0_19
| spl0_18
| ~ spl0_71
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f3997,f1220,f965,f300,f304,f308]) ).
fof(f4000,plain,
( ~ group_element(e_1)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ group_element(e_2)
| spl0_101 ),
inference(resolution,[],[f1980,f38]) ).
fof(f4002,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ group_element(e_2)
| spl0_101 ),
inference(forward_subsumption_resolution,[],[f4000,f22]) ).
fof(f4003,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| ~ group_element(e_2)
| spl0_4
| spl0_101 ),
inference(forward_subsumption_resolution,[],[f4002,f123]) ).
fof(f4004,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| spl0_4
| spl0_101 ),
inference(forward_subsumption_resolution,[],[f4003,f23]) ).
fof(f4005,plain,
( spl0_56
| spl0_57
| spl0_4
| spl0_101 ),
inference(avatar_split_clause,[],[f4004,f1978,f121,f658,f654]) ).
fof(f4057,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| ~ spl0_106 ),
inference(resolution,[],[f2956,f221]) ).
fof(f4076,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| spl0_13
| ~ spl0_106 ),
inference(forward_subsumption_resolution,[],[f4057,f249]) ).
fof(f4080,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_3)
| spl0_13
| ~ spl0_106 ),
inference(forward_subsumption_resolution,[],[f4076,f22]) ).
fof(f4084,plain,
( spl0_12
| spl0_14
| spl0_13
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f4080,f2955,f248,f252,f244]) ).
fof(f4138,plain,
( ~ product(e_1,e_3,e_1)
| ~ spl0_14 ),
inference(resolution,[],[f254,f73]) ).
fof(f4140,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_14 ),
inference(resolution,[],[f254,f55]) ).
fof(f4141,plain,
( ~ spl0_26
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f4140,f252,f368]) ).
fof(f4142,plain,
( ~ spl0_17
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f4138,f252,f273]) ).
fof(f4144,plain,
( ~ spl0_43
| spl0_7
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f291,f256,f170,f529]) ).
fof(f4149,plain,
( ~ spl0_12
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f1153,f974,f244]) ).
fof(f4150,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f1883,f983]) ).
fof(f4151,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f1844,f983]) ).
fof(f4154,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f1916,f983]) ).
fof(f4155,plain,
( product(e_4,e_4,e_3)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| spl0_73
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f4150,f979]) ).
fof(f4160,plain,
( product(e_4,e_4,e_3)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| spl0_46
| spl0_73
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f4155,f548]) ).
fof(f4165,plain,
( spl0_45
| spl0_47
| spl0_72
| spl0_46
| spl0_73
| spl0_74 ),
inference(avatar_split_clause,[],[f4160,f982,f978,f547,f974,f551,f543]) ).
fof(f4176,plain,
( ! [X0] :
( ~ product(e_2,X0,e_1)
| ~ product(X0,e_1,e_2) )
| ~ spl0_3 ),
inference(resolution,[],[f118,f111]) ).
fof(f4179,plain,
( ! [X0] :
( ~ product(e_2,X0,e_1)
| ~ product(X0,e_1,e_3) )
| ~ spl0_3 ),
inference(resolution,[],[f118,f202]) ).
fof(f4207,plain,
( ~ product(e_4,e_4,e_3)
| product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| ~ group_element(e_3)
| ~ spl0_44 ),
inference(resolution,[],[f534,f498]) ).
fof(f4223,plain,
( ~ product(e_4,e_4,e_3)
| product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f4207,f24]) ).
fof(f4227,plain,
( spl0_21
| spl0_22
| spl0_23
| ~ spl0_72
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f4223,f533,f974,f350,f346,f342]) ).
fof(f4273,plain,
( ~ group_element(e_4)
| product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| ~ group_element(e_4)
| spl0_71 ),
inference(resolution,[],[f967,f38]) ).
fof(f4275,plain,
( ~ group_element(e_4)
| product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| spl0_71 ),
inference(duplicate_literal_removal,[],[f4273]) ).
fof(f4276,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| spl0_71 ),
inference(forward_subsumption_resolution,[],[f4275,f25]) ).
fof(f4277,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| spl0_71
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f4276,f983]) ).
fof(f4354,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| ~ group_element(e_2)
| ~ spl0_101 ),
inference(resolution,[],[f1979,f132]) ).
fof(f4376,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| ~ group_element(e_2)
| spl0_35
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f4354,f447]) ).
fof(f4379,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| spl0_35
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f4376,f23]) ).
fof(f4382,plain,
( spl0_88
| spl0_87
| spl0_35
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f4379,f1978,f445,f1310,f1314]) ).
fof(f4385,plain,
( ~ product(e_4,e_1,e_2)
| ~ spl0_3
| ~ spl0_47 ),
inference(resolution,[],[f4176,f553]) ).
fof(f4392,plain,
( $false
| ~ spl0_3
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f916,f118]) ).
fof(f4393,plain,
( ~ spl0_3
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f4392]) ).
fof(f4396,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f1923,f983]) ).
fof(f4398,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_3)
| spl0_13
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f4151,f249]) ).
fof(f4399,plain,
( spl0_72
| spl0_73
| spl0_18
| spl0_19
| spl0_20
| spl0_74 ),
inference(avatar_split_clause,[],[f4154,f982,f308,f304,f300,f978,f974]) ).
fof(f4401,plain,
( spl0_72
| spl0_73
| spl0_71
| spl0_74 ),
inference(avatar_split_clause,[],[f4277,f982,f965,f978,f974]) ).
fof(f4402,plain,
( product(e_4,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| spl0_75
| spl0_77 ),
inference(forward_subsumption_resolution,[],[f2562,f1020]) ).
fof(f4403,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1920,f249]) ).
fof(f4404,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f1726,f447]) ).
fof(f4406,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_3)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f1786,f1044]) ).
fof(f4410,plain,
( ~ spl0_10
| ~ spl0_3
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f4385,f551,f117,f190]) ).
fof(f4412,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| spl0_74
| spl0_77 ),
inference(forward_subsumption_resolution,[],[f4396,f1020]) ).
fof(f4414,plain,
( spl0_12
| spl0_14
| spl0_72
| spl0_73
| spl0_13
| spl0_74 ),
inference(avatar_split_clause,[],[f4398,f982,f248,f978,f974,f252,f244]) ).
fof(f4416,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| spl0_75
| spl0_76
| spl0_77 ),
inference(forward_subsumption_resolution,[],[f4402,f1016]) ).
fof(f4423,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_4,e_3,e_3)
| spl0_74
| spl0_76
| spl0_77 ),
inference(forward_subsumption_resolution,[],[f4412,f1016]) ).
fof(f4430,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| spl0_74
| spl0_75
| spl0_76
| spl0_77 ),
inference(forward_subsumption_resolution,[],[f4423,f1012]) ).
fof(f4432,plain,
( spl0_72
| spl0_73
| spl0_74
| spl0_75
| spl0_76
| spl0_77 ),
inference(avatar_split_clause,[],[f4430,f1019,f1015,f1011,f982,f978,f974]) ).
fof(f4435,plain,
( spl0_5
| spl0_16
| spl0_17
| spl0_14
| spl0_12
| spl0_13 ),
inference(avatar_split_clause,[],[f4403,f248,f244,f252,f273,f269,f151]) ).
fof(f4436,plain,
( spl0_5
| spl0_16
| spl0_17
| spl0_88
| spl0_87
| spl0_35 ),
inference(avatar_split_clause,[],[f4404,f445,f1310,f1314,f273,f269,f151]) ).
fof(f4437,plain,
( spl0_5
| spl0_16
| spl0_17
| spl0_78
| spl0_80
| spl0_79 ),
inference(avatar_split_clause,[],[f4406,f1043,f1047,f1039,f273,f269,f151]) ).
fof(f4438,plain,
( spl0_5
| spl0_16
| spl0_17
| spl0_75
| spl0_76
| spl0_77 ),
inference(avatar_split_clause,[],[f4416,f1019,f1015,f1011,f273,f269,f151]) ).
fof(f4502,plain,
( ~ product(e_4,e_1,e_3)
| ~ spl0_3
| ~ spl0_47 ),
inference(resolution,[],[f4179,f553]) ).
fof(f4504,plain,
( $false
| ~ spl0_3
| ~ spl0_9
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f4502,f188]) ).
fof(f4505,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_47 ),
inference(avatar_contradiction_clause,[],[f4504]) ).
cnf(s3,plain,
( ~ spl0_5
| ~ spl0_6 ),
inference(sat_conversion,[],[f158]) ).
cnf(s4,plain,
( ~ spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f176]) ).
cnf(s6,plain,
~ spl0_8,
inference(sat_conversion,[],[f210]) ).
cnf(s7,plain,
( spl0_7
| spl0_9
| spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f218]) ).
cnf(s13,plain,
( spl0_7
| ~ spl0_15
| spl0_18
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f311]) ).
cnf(s14,plain,
( spl0_5
| spl0_15
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f317]) ).
cnf(s17,plain,
( ~ spl0_10
| spl0_24
| spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f371]) ).
cnf(s20,plain,
( spl0_24
| spl0_25
| spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f377]) ).
cnf(s26,plain,
( ~ spl0_17
| ~ spl0_26 ),
inference(sat_conversion,[],[f429]) ).
cnf(s27,plain,
( ~ spl0_21
| spl0_34 ),
inference(sat_conversion,[],[f437]) ).
cnf(s29,plain,
( ~ spl0_36
| spl0_37 ),
inference(sat_conversion,[],[f466]) ).
cnf(s32,plain,
( ~ spl0_39
| spl0_42 ),
inference(sat_conversion,[],[f497]) ).
cnf(s33,plain,
~ spl0_37,
inference(sat_conversion,[],[f513]) ).
cnf(s34,plain,
( spl0_36
| spl0_38
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f522]) ).
cnf(s39,plain,
( ~ spl0_9
| ~ spl0_38 ),
inference(sat_conversion,[],[f587]) ).
cnf(s42,plain,
( ~ spl0_10
| ~ spl0_27 ),
inference(sat_conversion,[],[f590]) ).
cnf(s43,plain,
( ~ spl0_9
| ~ spl0_38 ),
inference(sat_conversion,[],[f591]) ).
cnf(s60,plain,
( ~ spl0_35
| ~ spl0_45 ),
inference(sat_conversion,[],[f751]) ).
cnf(s61,plain,
( ~ spl0_12
| ~ spl0_45 ),
inference(sat_conversion,[],[f752]) ).
cnf(s67,plain,
~ spl0_4,
inference(sat_conversion,[],[f793]) ).
cnf(s71,plain,
~ spl0_11,
inference(sat_conversion,[],[f849]) ).
cnf(s79,plain,
( ~ spl0_6
| spl0_69 ),
inference(sat_conversion,[],[f884]) ).
cnf(s80,plain,
( spl0_6
| spl0_67 ),
inference(sat_conversion,[],[f887]) ).
cnf(s86,plain,
( spl0_70
| ~ spl0_71 ),
inference(sat_conversion,[],[f968]) ).
cnf(s106,plain,
( ~ spl0_13
| ~ spl0_73 ),
inference(sat_conversion,[],[f1189]) ).
cnf(s109,plain,
( ~ spl0_14
| ~ spl0_74 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s110,plain,
( ~ spl0_40
| ~ spl0_74 ),
inference(sat_conversion,[],[f1216]) ).
cnf(s112,plain,
~ spl0_42,
inference(sat_conversion,[],[f1230]) ).
cnf(s118,plain,
( ~ spl0_16
| spl0_35
| ~ spl0_85
| spl0_87
| spl0_88 ),
inference(sat_conversion,[],[f1317]) ).
cnf(s119,plain,
~ spl0_75,
inference(sat_conversion,[],[f1325]) ).
cnf(s125,plain,
( ~ spl0_45
| ~ spl0_72 ),
inference(sat_conversion,[],[f1356]) ).
cnf(s135,plain,
( spl0_41
| spl0_70 ),
inference(sat_conversion,[],[f1384]) ).
cnf(s138,plain,
( ~ spl0_46
| ~ spl0_86 ),
inference(sat_conversion,[],[f1422]) ).
cnf(s139,plain,
( ~ spl0_46
| ~ spl0_88 ),
inference(sat_conversion,[],[f1423]) ).
cnf(s140,plain,
( ~ spl0_13
| ~ spl0_46 ),
inference(sat_conversion,[],[f1424]) ).
cnf(s145,plain,
( ~ spl0_47
| ~ spl0_57 ),
inference(sat_conversion,[],[f1459]) ).
cnf(s146,plain,
( ~ spl0_47
| ~ spl0_84 ),
inference(sat_conversion,[],[f1460]) ).
cnf(s147,plain,
( ~ spl0_47
| ~ spl0_87 ),
inference(sat_conversion,[],[f1461]) ).
cnf(s148,plain,
( ~ spl0_14
| ~ spl0_47 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s151,plain,
( ~ spl0_9
| ~ spl0_56 ),
inference(sat_conversion,[],[f1465]) ).
cnf(s155,plain,
( spl0_3
| ~ spl0_10
| ~ spl0_47 ),
inference(sat_conversion,[],[f1469]) ).
cnf(s156,plain,
( ~ spl0_9
| ~ spl0_72 ),
inference(sat_conversion,[],[f1470]) ).
cnf(s167,plain,
( ~ spl0_47
| ~ spl0_74 ),
inference(sat_conversion,[],[f1480]) ).
cnf(s191,plain,
( ~ spl0_16
| ~ spl0_76 ),
inference(sat_conversion,[],[f1628]) ).
cnf(s192,plain,
( ~ spl0_76
| ~ spl0_88 ),
inference(sat_conversion,[],[f1629]) ).
cnf(s193,plain,
( ~ spl0_74
| ~ spl0_77 ),
inference(sat_conversion,[],[f1633]) ).
cnf(s205,plain,
( ~ spl0_23
| ~ spl0_80 ),
inference(sat_conversion,[],[f1715]) ).
cnf(s213,plain,
( ~ spl0_58
| ~ spl0_79 ),
inference(sat_conversion,[],[f1773]) ).
cnf(s215,plain,
( ~ spl0_16
| ~ spl0_79 ),
inference(sat_conversion,[],[f1776]) ).
cnf(s216,plain,
( ~ spl0_79
| ~ spl0_88 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s219,plain,
( spl0_5
| ~ spl0_6
| ~ spl0_80 ),
inference(sat_conversion,[],[f1780]) ).
cnf(s234,plain,
( ~ spl0_25
| ~ spl0_99 ),
inference(sat_conversion,[],[f1839]) ).
cnf(s240,plain,
( ~ spl0_38
| ~ spl0_99 ),
inference(sat_conversion,[],[f1860]) ).
cnf(s250,plain,
( ~ spl0_13
| ~ spl0_27 ),
inference(sat_conversion,[],[f1954]) ).
cnf(s254,plain,
( ~ spl0_26
| ~ spl0_100 ),
inference(sat_conversion,[],[f1974]) ).
cnf(s257,plain,
( ~ spl0_13
| ~ spl0_16 ),
inference(sat_conversion,[],[f1982]) ).
cnf(s269,plain,
( ~ spl0_17
| ~ spl0_100 ),
inference(sat_conversion,[],[f2010]) ).
cnf(s282,plain,
( ~ spl0_77
| ~ spl0_80 ),
inference(sat_conversion,[],[f2022]) ).
cnf(s299,plain,
( ~ spl0_17
| ~ spl0_77 ),
inference(sat_conversion,[],[f2103]) ).
cnf(s300,plain,
( ~ spl0_77
| ~ spl0_87 ),
inference(sat_conversion,[],[f2104]) ).
cnf(s310,plain,
( spl0_44
| spl0_83 ),
inference(sat_conversion,[],[f2180]) ).
cnf(s320,plain,
( ~ spl0_13
| ~ spl0_19 ),
inference(sat_conversion,[],[f2286]) ).
cnf(s323,plain,
( ~ spl0_20
| ~ spl0_59 ),
inference(sat_conversion,[],[f2314]) ).
cnf(s324,plain,
( ~ spl0_20
| ~ spl0_23 ),
inference(sat_conversion,[],[f2315]) ).
cnf(s325,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_85 ),
inference(sat_conversion,[],[f2330]) ).
cnf(s326,plain,
( ~ spl0_86
| ~ spl0_88 ),
inference(sat_conversion,[],[f2389]) ).
cnf(s327,plain,
( ~ spl0_86
| ~ spl0_88 ),
inference(sat_conversion,[],[f2390]) ).
cnf(s330,plain,
( ~ spl0_22
| spl0_42 ),
inference(sat_conversion,[],[f2429]) ).
cnf(s332,plain,
( ~ spl0_38
| ~ spl0_81 ),
inference(sat_conversion,[],[f2431]) ).
cnf(s333,plain,
( ~ spl0_45
| ~ spl0_81 ),
inference(sat_conversion,[],[f2432]) ).
cnf(s341,plain,
( ~ spl0_84
| ~ spl0_100 ),
inference(sat_conversion,[],[f2464]) ).
cnf(s346,plain,
( ~ spl0_40
| ~ spl0_84 ),
inference(sat_conversion,[],[f2472]) ).
cnf(s350,plain,
( ~ spl0_69
| ~ spl0_78 ),
inference(sat_conversion,[],[f2477]) ).
cnf(s353,plain,
( ~ spl0_38
| ~ spl0_72 ),
inference(sat_conversion,[],[f2478]) ).
cnf(s358,plain,
( ~ spl0_40
| ~ spl0_77 ),
inference(sat_conversion,[],[f2489]) ).
cnf(s360,plain,
( spl0_6
| spl0_25
| spl0_26
| spl0_27
| spl0_58
| spl0_59 ),
inference(sat_conversion,[],[f2501]) ).
cnf(s361,plain,
( spl0_6
| spl0_21
| spl0_22
| spl0_23
| spl0_58
| spl0_59 ),
inference(sat_conversion,[],[f2504]) ).
cnf(s365,plain,
( ~ spl0_15
| spl0_35
| spl0_87
| spl0_88 ),
inference(sat_conversion,[],[f2520]) ).
cnf(s386,plain,
( ~ spl0_73
| ~ spl0_76 ),
inference(sat_conversion,[],[f2546]) ).
cnf(s387,plain,
( ~ spl0_10
| ~ spl0_73 ),
inference(sat_conversion,[],[f2547]) ).
cnf(s390,plain,
( ~ spl0_10
| ~ spl0_76 ),
inference(sat_conversion,[],[f2549]) ).
cnf(s396,plain,
( ~ spl0_40
| ~ spl0_100 ),
inference(sat_conversion,[],[f2554]) ).
cnf(s399,plain,
( ~ spl0_76
| ~ spl0_79 ),
inference(sat_conversion,[],[f2564]) ).
cnf(s401,plain,
( ~ spl0_14
| ~ spl0_24 ),
inference(sat_conversion,[],[f2571]) ).
cnf(s402,plain,
( ~ spl0_14
| ~ spl0_20 ),
inference(sat_conversion,[],[f2572]) ).
cnf(s404,plain,
( spl0_5
| ~ spl0_9
| ~ spl0_20 ),
inference(sat_conversion,[],[f2586]) ).
cnf(s414,plain,
( spl0_38
| spl0_39
| spl0_40
| spl0_75
| spl0_76
| spl0_77 ),
inference(sat_conversion,[],[f2616]) ).
cnf(s416,plain,
( spl0_44
| spl0_75
| spl0_76
| spl0_77 ),
inference(sat_conversion,[],[f2619]) ).
cnf(s434,plain,
( ~ spl0_18
| ~ spl0_78 ),
inference(sat_conversion,[],[f2635]) ).
cnf(s436,plain,
( ~ spl0_6
| ~ spl0_18 ),
inference(sat_conversion,[],[f2637]) ).
cnf(s437,plain,
( ~ spl0_18
| ~ spl0_72 ),
inference(sat_conversion,[],[f2638]) ).
cnf(s438,plain,
( ~ spl0_18
| ~ spl0_45 ),
inference(sat_conversion,[],[f2639]) ).
cnf(s460,plain,
( ~ spl0_18
| ~ spl0_104 ),
inference(sat_conversion,[],[f2659]) ).
cnf(s479,plain,
( ~ spl0_35
| ~ spl0_104 ),
inference(sat_conversion,[],[f2719]) ).
cnf(s500,plain,
( ~ spl0_35
| ~ spl0_38
| ~ spl0_77 ),
inference(sat_conversion,[],[f2925]) ).
cnf(s509,plain,
( ~ spl0_13
| ~ spl0_19 ),
inference(sat_conversion,[],[f2928]) ).
cnf(s510,plain,
( ~ spl0_19
| ~ spl0_79 ),
inference(sat_conversion,[],[f2929]) ).
cnf(s534,plain,
( spl0_38
| spl0_39
| spl0_40
| ~ spl0_71 ),
inference(sat_conversion,[],[f2962]) ).
cnf(s568,plain,
( ~ spl0_46
| ~ spl0_73 ),
inference(sat_conversion,[],[f2988]) ).
cnf(s588,plain,
( ~ spl0_9
| ~ spl0_15
| spl0_43 ),
inference(sat_conversion,[],[f3057]) ).
cnf(s604,plain,
( spl0_12
| spl0_13
| spl0_14
| spl0_25
| spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f3149]) ).
cnf(s606,plain,
( ~ spl0_12
| ~ spl0_18 ),
inference(sat_conversion,[],[f3154]) ).
cnf(s612,plain,
( spl0_3
| spl0_21
| spl0_22
| spl0_23
| spl0_99
| spl0_100 ),
inference(sat_conversion,[],[f3162]) ).
cnf(s617,plain,
( spl0_3
| spl0_12
| spl0_13
| spl0_14
| spl0_99
| spl0_100 ),
inference(sat_conversion,[],[f3166]) ).
cnf(s622,plain,
( ~ spl0_10
| ~ spl0_70
| ~ spl0_106 ),
inference(sat_conversion,[],[f3168]) ).
cnf(s627,plain,
( ~ spl0_3
| ~ spl0_13 ),
inference(sat_conversion,[],[f3169]) ).
cnf(s662,plain,
( spl0_21
| spl0_22
| spl0_23
| ~ spl0_41
| ~ spl0_83 ),
inference(sat_conversion,[],[f3237]) ).
cnf(s665,plain,
( ~ spl0_41
| spl0_72
| spl0_73
| spl0_74 ),
inference(sat_conversion,[],[f3242]) ).
cnf(s690,plain,
( ~ spl0_35
| ~ spl0_67
| ~ spl0_99 ),
inference(sat_conversion,[],[f3243]) ).
cnf(s693,plain,
( spl0_4
| spl0_35
| spl0_56
| spl0_57
| spl0_87
| spl0_88 ),
inference(sat_conversion,[],[f3251]) ).
cnf(s699,plain,
( spl0_72
| spl0_73
| spl0_74
| spl0_83 ),
inference(sat_conversion,[],[f3263]) ).
cnf(s700,plain,
( ~ spl0_19
| spl0_35
| ~ spl0_38 ),
inference(sat_conversion,[],[f3264]) ).
cnf(s703,plain,
( ~ spl0_19
| ~ spl0_73 ),
inference(sat_conversion,[],[f3265]) ).
cnf(s726,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_81
| spl0_84
| spl0_86 ),
inference(sat_conversion,[],[f3268]) ).
cnf(s728,plain,
( spl0_35
| spl0_81
| spl0_84
| spl0_86
| spl0_87
| spl0_88 ),
inference(sat_conversion,[],[f3272]) ).
cnf(s738,plain,
( spl0_12
| spl0_13
| spl0_14
| ~ spl0_41 ),
inference(sat_conversion,[],[f3315]) ).
cnf(s747,plain,
( ~ spl0_81
| ~ spl0_99 ),
inference(sat_conversion,[],[f3374]) ).
cnf(s756,plain,
( spl0_18
| spl0_19
| spl0_20
| ~ spl0_44 ),
inference(sat_conversion,[],[f3422]) ).
cnf(s761,plain,
( spl0_21
| spl0_22
| spl0_23
| ~ spl0_98 ),
inference(sat_conversion,[],[f3455]) ).
cnf(s763,plain,
( spl0_6
| spl0_58
| spl0_59
| spl0_98 ),
inference(sat_conversion,[],[f3469]) ).
cnf(s766,plain,
( ~ spl0_41
| ~ spl0_44 ),
inference(sat_conversion,[],[f3497]) ).
cnf(s802,plain,
( ~ spl0_3
| spl0_4
| ~ spl0_86 ),
inference(sat_conversion,[],[f3544]) ).
cnf(s812,plain,
( ~ spl0_3
| spl0_81
| spl0_84
| spl0_86 ),
inference(sat_conversion,[],[f3637]) ).
cnf(s819,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_74 ),
inference(sat_conversion,[],[f3678]) ).
cnf(s832,plain,
( ~ spl0_5
| ~ spl0_25 ),
inference(sat_conversion,[],[f3718]) ).
cnf(s848,plain,
( ~ spl0_20
| ~ spl0_74 ),
inference(sat_conversion,[],[f3721]) ).
cnf(s873,plain,
( ~ spl0_5
| ~ spl0_78 ),
inference(sat_conversion,[],[f3723]) ).
cnf(s882,plain,
( ~ spl0_5
| ~ spl0_99 ),
inference(sat_conversion,[],[f3726]) ).
cnf(s922,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_78
| spl0_79
| spl0_80 ),
inference(sat_conversion,[],[f3754]) ).
cnf(s923,plain,
( spl0_18
| spl0_19
| spl0_20
| spl0_78
| spl0_79
| spl0_80 ),
inference(sat_conversion,[],[f3756]) ).
cnf(s924,plain,
( spl0_78
| spl0_79
| spl0_80
| spl0_104 ),
inference(sat_conversion,[],[f3757]) ).
cnf(s932,plain,
( spl0_35
| spl0_78
| spl0_79
| spl0_80
| spl0_87
| spl0_88 ),
inference(sat_conversion,[],[f3770]) ).
cnf(s933,plain,
( spl0_41
| spl0_45
| spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f3772]) ).
cnf(s936,plain,
( spl0_3
| spl0_99
| spl0_100
| spl0_106 ),
inference(sat_conversion,[],[f3776]) ).
cnf(s959,plain,
( ~ spl0_44
| ~ spl0_76 ),
inference(sat_conversion,[],[f3787]) ).
cnf(s962,plain,
( spl0_45
| spl0_46
| spl0_47
| ~ spl0_71 ),
inference(sat_conversion,[],[f3794]) ).
cnf(s971,plain,
( ~ spl0_5
| ~ spl0_104 ),
inference(sat_conversion,[],[f3808]) ).
cnf(s979,plain,
( ~ spl0_19
| ~ spl0_46 ),
inference(sat_conversion,[],[f3811]) ).
cnf(s995,plain,
( spl0_3
| spl0_5
| spl0_16
| spl0_17
| spl0_99
| spl0_100 ),
inference(sat_conversion,[],[f3812]) ).
cnf(s1001,plain,
~ spl0_34,
inference(sat_conversion,[],[f3827]) ).
cnf(s1019,plain,
( ~ spl0_70
| ~ spl0_76
| ~ spl0_85 ),
inference(sat_conversion,[],[f3931]) ).
cnf(s1020,plain,
( spl0_12
| spl0_13
| spl0_14
| ~ spl0_71 ),
inference(sat_conversion,[],[f3949]) ).
cnf(s1024,plain,
( spl0_81
| spl0_84
| spl0_86
| ~ spl0_101 ),
inference(sat_conversion,[],[f3988]) ).
cnf(s1026,plain,
( spl0_3
| ~ spl0_40
| spl0_99
| spl0_100
| ~ spl0_101 ),
inference(sat_conversion,[],[f3992]) ).
cnf(s1027,plain,
( spl0_18
| spl0_19
| spl0_20
| ~ spl0_71
| ~ spl0_83 ),
inference(sat_conversion,[],[f3999]) ).
cnf(s1028,plain,
( spl0_4
| spl0_56
| spl0_57
| spl0_101 ),
inference(sat_conversion,[],[f4005]) ).
cnf(s1036,plain,
( spl0_12
| spl0_13
| spl0_14
| ~ spl0_106 ),
inference(sat_conversion,[],[f4084]) ).
cnf(s1042,plain,
( ~ spl0_14
| ~ spl0_26 ),
inference(sat_conversion,[],[f4141]) ).
cnf(s1043,plain,
( ~ spl0_14
| ~ spl0_17 ),
inference(sat_conversion,[],[f4142]) ).
cnf(s1044,plain,
( spl0_7
| ~ spl0_15
| ~ spl0_43 ),
inference(sat_conversion,[],[f4144]) ).
cnf(s1088,plain,
( ~ spl0_12
| ~ spl0_72 ),
inference(sat_conversion,[],[f4149]) ).
cnf(s1099,plain,
( spl0_45
| spl0_46
| spl0_47
| spl0_72
| spl0_73
| spl0_74 ),
inference(sat_conversion,[],[f4165]) ).
cnf(s1110,plain,
( spl0_21
| spl0_22
| spl0_23
| ~ spl0_44
| ~ spl0_72 ),
inference(sat_conversion,[],[f4227]) ).
cnf(s1132,plain,
( spl0_35
| spl0_87
| spl0_88
| ~ spl0_101 ),
inference(sat_conversion,[],[f4382]) ).
cnf(s1158,plain,
( ~ spl0_3
| ~ spl0_16 ),
inference(sat_conversion,[],[f4393]) ).
cnf(s1180,plain,
( spl0_18
| spl0_19
| spl0_20
| spl0_72
| spl0_73
| spl0_74 ),
inference(sat_conversion,[],[f4399]) ).
cnf(s1181,plain,
( spl0_71
| spl0_72
| spl0_73
| spl0_74 ),
inference(sat_conversion,[],[f4401]) ).
cnf(s1183,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_47 ),
inference(sat_conversion,[],[f4410]) ).
cnf(s1185,plain,
( spl0_12
| spl0_13
| spl0_14
| spl0_72
| spl0_73
| spl0_74 ),
inference(sat_conversion,[],[f4414]) ).
cnf(s1195,plain,
( spl0_72
| spl0_73
| spl0_74
| spl0_75
| spl0_76
| spl0_77 ),
inference(sat_conversion,[],[f4432]) ).
cnf(s1203,plain,
( spl0_5
| spl0_12
| spl0_13
| spl0_14
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f4435]) ).
cnf(s1204,plain,
( spl0_5
| spl0_16
| spl0_17
| spl0_35
| spl0_87
| spl0_88 ),
inference(sat_conversion,[],[f4436]) ).
cnf(s1205,plain,
( spl0_5
| spl0_16
| spl0_17
| spl0_78
| spl0_79
| spl0_80 ),
inference(sat_conversion,[],[f4437]) ).
cnf(s1206,plain,
( spl0_5
| spl0_16
| spl0_17
| spl0_75
| spl0_76
| spl0_77 ),
inference(sat_conversion,[],[f4438]) ).
cnf(s1222,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_47 ),
inference(sat_conversion,[],[f4505]) ).
cnf(s1223,plain,
~ spl0_22,
inference(rat,[],[s330,s112]) ).
cnf(s1228,plain,
~ spl0_39,
inference(rat,[],[s32,s112]) ).
cnf(s1230,plain,
~ spl0_36,
inference(rat,[],[s29,s33]) ).
cnf(s1232,plain,
~ spl0_21,
inference(rat,[],[s27,s1001]) ).
cnf(s1236,plain,
( spl0_7
| spl0_9
| spl0_10 ),
inference(rat,[],[s7,s71]) ).
cnf(s1238,plain,
~ spl0_7,
inference(rat,[],[s4,s6]) ).
cnf(s1239,plain,
( ~ spl0_17
| spl0_14
| spl0_13
| spl0_12
| spl0_27
| spl0_3 ),
inference(rat,[],[s234,s604,s936,s26,s269,s1036]) ).
cnf(s1240,plain,
( ~ spl0_19
| ~ spl0_38
| spl0_41
| spl0_47 ),
inference(rat,[],[s60,s933,s700,s979]) ).
cnf(s1241,plain,
( ~ spl0_100
| spl0_79
| spl0_71
| spl0_41
| spl0_47
| spl0_73
| spl0_76 ),
inference(rat,[],[s726,s205,s138,s924,s933,s434,s438,s460,s756,s1240,s416,s193,s848,s1181,s332,s353,s34,s341,s396,s1223,s1232,s119,s1228,s1230]) ).
cnf(s1242,plain,
( spl0_14
| spl0_13
| spl0_12
| ~ spl0_10
| spl0_5
| spl0_3 ),
inference(rat,[],[s756,s979,s324,s933,s1110,s125,s437,s1195,s416,s110,s358,s34,s240,s936,s1241,s215,s1203,s1239,s1020,s738,s1036,s390,s387,s155,s42,s1223,s1232,s119,s1228,s1230]) ).
cnf(s1243,plain,
( ~ spl0_100
| ~ spl0_14
| spl0_47
| spl0_73
| spl0_76 ),
inference(rat,[],[s728,s138,s139,s1099,s438,s1027,s500,s300,s1240,s699,s1195,s665,s1181,s332,s353,s34,s341,s396,s402,s109,s119,s1228,s1230]) ).
cnf(s1244,plain,
( ~ spl0_14
| ~ spl0_10
| spl0_3 ),
inference(rat,[],[s34,s358,s353,s416,s665,s766,s135,s622,s936,s1243,s234,s20,s109,s401,s1042,s390,s387,s155,s42,s1228,s1230,s119]) ).
cnf(s1245,plain,
( ~ spl0_100
| ~ spl0_13
| spl0_47
| spl0_73
| spl0_76
| spl0_5 ),
inference(rat,[],[s324,s726,s13,s327,s438,s365,s1099,s500,s193,s300,s332,s353,s1206,s14,s34,s269,s341,s396,s509,s257,s140,s1223,s1232,s1238,s119,s1228,s1230]) ).
cnf(s1246,plain,
( spl0_99
| ~ spl0_13
| ~ spl0_10
| spl0_5
| spl0_3 ),
inference(rat,[],[s766,s135,s416,s622,s299,s936,s995,s257,s1245,s155,s387,s390,s119]) ).
cnf(s1247,plain,
( ~ spl0_13
| ~ spl0_10
| spl0_5
| spl0_3 ),
inference(rat,[],[s933,s125,s766,s1195,s416,s110,s358,s34,s240,s1246,s140,s390,s387,s155,s119,s1228,s1230]) ).
cnf(s1248,plain,
( spl0_77
| ~ spl0_38
| spl0_18
| spl0_72
| spl0_47
| spl0_73
| spl0_76 ),
inference(rat,[],[s756,s1240,s848,s766,s1195,s416,s119]) ).
cnf(s1249,plain,
( ~ spl0_38
| spl0_45
| spl0_18
| spl0_72
| spl0_47
| spl0_73
| spl0_76
| spl0_5 ),
inference(rat,[],[s325,s324,s118,s1204,s1027,s139,s700,s1181,s1099,s699,s500,s193,s299,s300,s1248,s1223,s1232]) ).
cnf(s1250,plain,
( spl0_45
| spl0_18
| spl0_5
| spl0_72
| spl0_47
| spl0_73
| spl0_76 ),
inference(rat,[],[s1195,s110,s358,s34,s1249,s1230,s1228,s119]) ).
cnf(s1251,plain,
( ~ spl0_10
| spl0_5
| spl0_3 ),
inference(rat,[],[s1250,s61,s606,s1088,s1242,s1247,s1244,s155,s387,s390]) ).
cnf(s1252,plain,
( spl0_76
| ~ spl0_67
| spl0_5
| spl0_3 ),
inference(rat,[],[s326,s1132,s1024,s690,s747,s1028,s617,s145,s147,s148,s933,s438,s606,s756,s106,s568,s703,s766,s1195,s416,s404,s156,s151,s396,s358,s346,s110,s34,s43,s1236,s1251,s67,s119,s1230,s1228,s1238]) ).
cnf(s1253,plain,
( ~ spl0_15
| ~ spl0_9 ),
inference(rat,[],[s588,s1044,s1238]) ).
cnf(s1254,plain,
( ~ spl0_18
| spl0_80
| spl0_79 ),
inference(rat,[],[s924,s434,s460]) ).
cnf(s1255,plain,
( ~ spl0_67
| spl0_5
| spl0_3 ),
inference(rat,[],[s690,s1026,s693,s1028,s145,s147,s1099,s61,s1020,s509,s979,s1180,s1254,s1043,s14,s205,s325,s1019,s86,s1181,s191,s192,s386,s399,s1252,s404,s156,s151,s396,s110,s34,s43,s1253,s1236,s1251,s67,s1223,s1232,s1238,s1230,s1228]) ).
cnf(s1256,plain,
( spl0_76
| spl0_18
| spl0_74
| spl0_77
| spl0_72
| spl0_20 ),
inference(rat,[],[s703,s756,s1195,s416,s119]) ).
cnf(s1257,plain,
( spl0_5
| spl0_3 ),
inference(rat,[],[s1099,s61,s147,s1020,s932,s509,s979,s479,s1043,s1181,s923,s924,s1205,s191,s192,s386,s399,s1256,s350,s79,s219,s436,s80,s1255,s110,s358,s34,s43,s156,s404,s1236,s1251,s1238,s1230,s1228]) ).
cnf(s1258,plain,
( ~ spl0_74
| spl0_14
| spl0_13
| spl0_73
| spl0_72
| spl0_76
| spl0_3 ),
inference(rat,[],[s254,s604,s617,s42,s606,s1236,s1248,s43,s414,s110,s167,s193,s882,s832,s1257,s1238,s1228,s119]) ).
cnf(s1259,plain,
( spl0_14
| spl0_13
| spl0_73
| spl0_72
| spl0_76
| spl0_3 ),
inference(rat,[],[s361,s323,s324,s1180,s213,s510,s924,s606,s282,s1185,s1195,s1258,s971,s873,s3,s1257,s1223,s1232,s119]) ).
cnf(s1260,plain,
( ~ spl0_14
| spl0_73
| spl0_72
| spl0_76
| spl0_3 ),
inference(rat,[],[s39,s534,s358,s1236,s1181,s1195,s1244,s109,s1228,s1238,s119]) ).
cnf(s1261,plain,
( ~ spl0_74
| spl0_46
| spl0_73
| spl0_72
| spl0_76 ),
inference(rat,[],[s933,s438,s766,s1248,s416,s414,s110,s167,s193,s119,s1228]) ).
cnf(s1262,plain,
( spl0_73
| spl0_72
| spl0_76
| spl0_3 ),
inference(rat,[],[s323,s360,s1180,s254,s438,s936,s1099,s622,s155,s1236,s213,s43,s924,s534,s86,s282,s358,s1181,s1195,s1261,s140,s250,s509,s1259,s1260,s971,s882,s873,s832,s3,s1257,s1238,s1228,s119]) ).
cnf(s1263,plain,
( ~ spl0_73
| spl0_76
| spl0_3 ),
inference(rat,[],[s933,s438,s145,s756,s766,s324,s1028,s416,s612,s1026,s358,s396,s34,s43,s151,s1236,s387,s568,s703,s882,s1257,s67,s119,s1223,s1232,s1228,s1230,s1238]) ).
cnf(s1264,plain,
( spl0_76
| spl0_3 ),
inference(rat,[],[s320,s756,s324,s617,s416,s612,s1244,s358,s396,s1236,s34,s156,s353,s437,s1088,s1262,s1263,s882,s1257,s119,s1223,s1232,s1238,s1228,s1230]) ).
cnf(s1265,plain,
spl0_3,
inference(rat,[],[s1019,s135,s325,s662,s205,s924,s310,s399,s959,s1264,s873,s971,s1257,s1223,s1232]) ).
cnf(s1266,plain,
~ spl0_16,
inference(rat,[],[s1158,s1265]) ).
cnf(s1269,plain,
~ spl0_86,
inference(rat,[],[s802,s67,s1265]) ).
cnf(s1271,plain,
~ spl0_13,
inference(rat,[],[s627,s1265]) ).
cnf(s1273,plain,
~ spl0_74,
inference(rat,[],[s39,s1236,s34,s819,s110,s1238,s1228,s1230,s1265]) ).
cnf(s1274,plain,
( ~ spl0_12
| spl0_73
| spl0_72
| spl0_76 ),
inference(rat,[],[s213,s763,s761,s922,s3,s873,s323,s324,s1250,s1180,s61,s606,s282,s700,s500,s146,s812,s332,s534,s1181,s358,s1195,s1223,s1232,s1273,s1269,s1265,s119,s1228]) ).
cnf(s1275,plain,
( spl0_73
| spl0_72
| spl0_76 ),
inference(rat,[],[s1204,s216,s832,s1254,s17,s1027,s401,s402,s1042,s1020,s1274,s700,s1236,s500,s43,s534,s282,s299,s300,s358,s1181,s699,s1195,s119,s1273,s1228,s1238,s1271,s1266]) ).
cnf(s1276,plain,
( ~ spl0_73
| spl0_76 ),
inference(rat,[],[s933,s333,s766,s812,s416,s346,s358,s34,s1222,s43,s1236,s387,s568,s1265,s1269,s119,s1228,s1230,s1238]) ).
cnf(s1277,plain,
( spl0_73
| spl0_76 ),
inference(rat,[],[s756,s979,s324,s933,s1110,s766,s416,s1183,s358,s1236,s34,s125,s156,s353,s437,s1275,s1230,s1228,s1238,s1265,s119,s1232,s1223]) ).
cnf(s1278,plain,
spl0_76,
inference(rat,[],[s1277,s1276]) ).
cnf(s1280,plain,
~ spl0_79,
inference(rat,[],[s399,s1278]) ).
cnf(s1281,plain,
~ spl0_10,
inference(rat,[],[s390,s1278]) ).
cnf(s1283,plain,
~ spl0_73,
inference(rat,[],[s386,s1278]) ).
cnf(s1286,plain,
spl0_9,
inference(rat,[],[s1236,s1238,s1281]) ).
cnf(s1287,plain,
~ spl0_72,
inference(rat,[],[s156,s1286]) ).
cnf(s1289,plain,
~ spl0_38,
inference(rat,[],[s43,s1286]) ).
cnf(s1292,plain,
~ spl0_47,
inference(rat,[],[s1222,s1265,s1286]) ).
cnf(s1294,plain,
spl0_71,
inference(rat,[],[s1181,s1273,s1283,s1287]) ).
cnf(s1296,plain,
spl0_40,
inference(rat,[],[s34,s1230,s1228,s1289]) ).
cnf(s1298,plain,
spl0_70,
inference(rat,[],[s86,s1294]) ).
cnf(s1299,plain,
~ spl0_84,
inference(rat,[],[s346,s1296]) ).
cnf(s1300,plain,
~ spl0_85,
inference(rat,[],[s1019,s1278,s1298]) ).
cnf(s1301,plain,
spl0_81,
inference(rat,[],[s812,s1269,s1265,s1299]) ).
cnf(s1302,plain,
spl0_23,
inference(rat,[],[s325,s1232,s1223,s1300]) ).
cnf(s1305,plain,
~ spl0_45,
inference(rat,[],[s333,s1301]) ).
cnf(s1306,plain,
~ spl0_20,
inference(rat,[],[s324,s1302]) ).
cnf(s1307,plain,
~ spl0_80,
inference(rat,[],[s205,s1302]) ).
cnf(s1308,plain,
spl0_46,
inference(rat,[],[s962,s1294,s1292,s1305]) ).
cnf(s1309,plain,
~ spl0_18,
inference(rat,[],[s1254,s1280,s1307]) ).
cnf(s1310,plain,
~ spl0_19,
inference(rat,[],[s979,s1308]) ).
cnf(s1311,plain,
$false,
inference(rat,[],[s1180,s1273,s1283,s1306,s1287,s1310,s1309]) ).
fof(f4506,plain,
$false,
inference(avatar_sat_refutation,[],[s1311]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP129-3.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n011.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 09:28:00 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.22/1.42 % (2145569)Input is clausal, will run a generic CNF schedule.
% 3.22/1.42 % (2145577)lrs+10_1_sil=8000:sp=occurrence:random_seed=2716066139:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.22/1.42 % (2145577)Instruction limit reached!
% 3.22/1.42 % (2145577)------------------------------
% 3.22/1.42 % (2145577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.42 % (2145577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.42 % (2145577)CaDiCaL version: 2.1.3
% 3.22/1.42 % (2145577)Termination reason: Instruction limit
% 3.22/1.42 % (2145577)Termination phase: Saturation
% 3.22/1.42 % (2145577)Time elapsed: 0.035 s
% 3.22/1.42 % (2145577)Peak memory usage: 88 MB
% 3.22/1.42 % (2145577)Instructions burned: 107 (million)
% 3.22/1.42 % (2145575)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2790934675:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.22/1.42 % (2145574)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=574839304:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.22/1.42 % (2145578)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2401271725:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.22/1.42 % (2145580)dis-21_1_sil=8000:lcm=predicate:random_seed=1822702959:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.22/1.42 % (2145576)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=116875678:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.22/1.42 % (2145579)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4016075871:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.22/1.42 % (2145578)Instruction limit reached!
% 3.22/1.42 % (2145578)------------------------------
% 3.22/1.42 % (2145578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.42 % (2145578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.42 % (2145578)CaDiCaL version: 2.1.3
% 3.22/1.42 % (2145578)Termination reason: Instruction limit
% 3.22/1.42 % (2145578)Termination phase: Saturation
% 3.22/1.42 % (2145578)Time elapsed: 0.066 s
% 3.22/1.42 % (2145578)Peak memory usage: 88 MB
% 3.22/1.42 % (2145578)Instructions burned: 115 (million)
% 3.22/1.42 % (2145580)Instruction limit reached!
% 3.22/1.42 % (2145580)------------------------------
% 3.22/1.42 % (2145580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.42 % (2145580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.42 % (2145580)CaDiCaL version: 2.1.3
% 3.22/1.42 % (2145580)Termination reason: Instruction limit
% 3.22/1.42 % (2145580)Termination phase: Saturation
% 3.22/1.42 % (2145580)Time elapsed: 0.075 s
% 3.22/1.42 % (2145580)Peak memory usage: 88 MB
% 3.22/1.42 % (2145580)Instructions burned: 118 (million)
% 3.22/1.42 % (2145582)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2134606718:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.22/1.42 % (2145579)First to succeed.
% 3.22/1.42 % (2145579)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2145569"
% 3.22/1.42 % (2145582)Instruction limit reached!
% 3.22/1.42 % (2145582)------------------------------
% 3.22/1.42 % (2145582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.42 % (2145582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.42 % (2145582)CaDiCaL version: 2.1.3
% 3.22/1.42 % (2145582)Termination reason: Instruction limit
% 3.22/1.42 % (2145582)Termination phase: Saturation
% 3.22/1.42 % (2145582)Time elapsed: 0.046 s
% 3.22/1.42 % (2145582)Peak memory usage: 89 MB
% 3.22/1.42 % (2145582)Instructions burned: 144 (million)
% 3.22/1.42 % (2145590)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=236695221:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 3.22/1.42 % (2145589)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2595450906:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 3.22/1.42 % (2145589)Refutation not found, incomplete strategy
% 3.22/1.42 % (2145589)------------------------------
% 3.22/1.42 % (2145589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.42 % (2145589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.42 % (2145589)CaDiCaL version: 2.1.3
% 3.22/1.42 % (2145589)Termination reason: Refutation not found, incomplete strategy
% 3.22/1.42 % (2145589)Time elapsed: 0.002 s
% 3.22/1.42 % (2145589)Peak memory usage: 87 MB
% 3.22/1.42 % (2145589)Instructions burned: 2 (million)
% 3.22/1.42 % (2145592)lrs+10_64_to=lpo:sil=8000:random_seed=2543111365:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 3.22/1.42 % (2145592)Also succeeded, but the first one will report.
% 3.22/1.42 % (2145590)Instruction limit reached!
% 3.22/1.42 % (2145590)------------------------------
% 3.22/1.42 % (2145590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.42 % (2145590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.42 % (2145590)CaDiCaL version: 2.1.3
% 3.22/1.42 % (2145590)Termination reason: Instruction limit
% 3.22/1.42 % (2145590)Termination phase: Saturation
% 3.22/1.42 % (2145590)Time elapsed: 0.125 s
% 3.22/1.42 % (2145590)Peak memory usage: 88 MB
% 3.22/1.42 % (2145590)Instructions burned: 220 (million)
% 3.22/1.42 % (2145579)Refutation found. Thanks to Tanya!
% 3.22/1.42 % SZS status Unsatisfiable for theBenchmark
% 3.22/1.42 % SZS output start Proof for theBenchmark
% See solution above
% 4.60/1.62 % (2145579)------------------------------
% 4.60/1.62 % (2145579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.60/1.62 % (2145579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.60/1.62 % (2145579)CaDiCaL version: 2.1.3
% 4.60/1.62 % (2145579)Termination reason: Refutation
% 4.60/1.62 % (2145579)Time elapsed: 0.126 s
% 4.60/1.62 % (2145579)Peak memory usage: 90 MB
% 4.60/1.62 % (2145579)Instructions burned: 200 (million)
% 4.60/1.62 % (2145579)------------------------------
% 4.60/1.62 % (2145579)------------------------------
% 4.60/1.62 % (2145569)Success in time 0.563 s
% 4.60/1.62 % Vampire exiting
%------------------------------------------------------------------------------