%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP134-1.003 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:13:03 AM UTC 2026
% Result : Unsatisfiable 2.37s 1.16s
% Output : Refutation 2.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 57
% Syntax : Number of formulae : 409 ( 42 unt; 47 def)
% Number of atoms : 1179 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1491 ( 721 ~; 723 |; 0 &)
% ( 47 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 51 ( 50 usr; 48 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 136 ( 0 sgn 136 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
fof(f2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
fof(f3,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
fof(f4,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f5,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f7,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f10,axiom,
! [X0,X1] :
( product(X0,X1,e_3)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| ~ group_element(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
fof(f11,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function2) ).
fof(f12,axiom,
! [X2,X3,X0,X1] :
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f14,negated_conjecture,
! [X2,X3,X0,X1] :
( product(X2,X3,X1)
| ~ product(X1,X0,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg4) ).
fof(f15,plain,
! [X0,X1] :
( ~ product(X0,X1,e_2)
| ~ product(X0,X1,e_1) ),
inference(resolution,[],[f11,f4]) ).
fof(f16,plain,
! [X0,X1] :
( ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_1) ),
inference(resolution,[],[f11,f5]) ).
fof(f18,plain,
! [X0,X1] :
( ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_2) ),
inference(resolution,[],[f11,f7]) ).
fof(f21,plain,
! [X0,X1] :
( ~ product(X0,e_2,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f12,f4]) ).
fof(f22,plain,
! [X0,X1] :
( ~ product(X0,e_3,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f12,f5]) ).
fof(f24,plain,
! [X0,X1] :
( ~ product(X0,e_3,X1)
| ~ product(X0,e_2,X1) ),
inference(resolution,[],[f12,f7]) ).
fof(f27,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,e_1)
| ~ product(e_2,X2,X1)
| ~ product(X2,e_2,X0) ),
inference(resolution,[],[f15,f14]) ).
fof(f37,plain,
( ~ product(e_2,e_1,e_1)
| ~ product(e_1,e_2,e_2) ),
inference(factoring,[],[f27]) ).
fof(f40,definition,
( spl0_1
<=> product(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f41,plain,
( ~ product(e_1,e_2,e_2)
| spl0_1 ),
inference(avatar_component_clause,[],[f40]) ).
fof(f43,definition,
( spl0_2
<=> product(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f44,plain,
( ~ product(e_2,e_1,e_1)
| spl0_2 ),
inference(avatar_component_clause,[],[f43]) ).
fof(f45,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f37,f43,f40]) ).
fof(f46,plain,
( ! [X0] :
( ~ product(e_2,X0,e_2)
| ~ product(X0,e_2,e_1) )
| spl0_1 ),
inference(resolution,[],[f41,f14]) ).
fof(f48,plain,
( ! [X0,X1] :
( ~ product(e_2,X0,e_2)
| ~ product(e_1,X1,e_2)
| ~ product(X1,e_1,X0) )
| spl0_1 ),
inference(resolution,[],[f46,f14]) ).
fof(f49,plain,
! [X0,X1] :
( ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| ~ group_element(X0)
| ~ product(e_3,X1,e_1)
| ~ product(e_2,X0,X1) ),
inference(resolution,[],[f10,f27]) ).
fof(f50,plain,
! [X0,X1] :
( ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| ~ group_element(e_2)
| ~ product(X1,e_3,e_1)
| ~ product(X0,e_2,X1) ),
inference(resolution,[],[f10,f27]) ).
fof(f52,definition,
( spl0_3
<=> group_element(e_2) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f53,plain,
( ~ group_element(e_2)
| spl0_3 ),
inference(avatar_component_clause,[],[f52]) ).
fof(f55,definition,
( spl0_4
<=> ! [X0,X1] :
( ~ group_element(X0)
| ~ product(X0,e_2,X1)
| ~ product(X1,e_3,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f56,plain,
( ! [X0,X1] :
( ~ group_element(X0)
| ~ product(X0,e_2,X1)
| ~ product(X1,e_3,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_1) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f55]) ).
fof(f57,plain,
( ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f50,f55,f52]) ).
fof(f59,definition,
( spl0_5
<=> ! [X0,X1] :
( product(X0,e_2,e_1)
| ~ product(e_2,X0,X1)
| ~ product(e_3,X1,e_1)
| ~ group_element(X0)
| product(X0,e_2,e_2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f60,plain,
( ! [X0,X1] :
( ~ group_element(X0)
| ~ product(e_2,X0,X1)
| ~ product(e_3,X1,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f59]) ).
fof(f61,plain,
( spl0_5
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f49,f52,f59]) ).
fof(f62,plain,
( $false
| spl0_3 ),
inference(resolution,[],[f53,f2]) ).
fof(f63,plain,
spl0_3,
inference(avatar_contradiction_clause,[],[f62]) ).
fof(f64,plain,
( ! [X0] :
( ~ product(e_1,e_2,X0)
| ~ product(X0,e_3,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) )
| ~ spl0_4 ),
inference(resolution,[],[f56,f1]) ).
fof(f68,definition,
( spl0_6
<=> product(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f69,plain,
( product(e_2,e_3,e_1)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f68]) ).
fof(f71,definition,
( spl0_7
<=> product(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f72,plain,
( product(e_2,e_3,e_2)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f71]) ).
fof(f78,definition,
( spl0_9
<=> product(e_2,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f79,plain,
( product(e_2,e_2,e_1)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f78]) ).
fof(f81,definition,
( spl0_10
<=> product(e_2,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f82,plain,
( product(e_2,e_2,e_2)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f81]) ).
fof(f87,plain,
( product(e_2,e_1,e_1)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f43]) ).
fof(f89,definition,
( spl0_12
<=> product(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f90,plain,
( product(e_2,e_1,e_2)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f92,definition,
( spl0_13
<=> ! [X0] :
( ~ product(e_1,e_2,X0)
| ~ product(X0,e_3,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f93,plain,
( ! [X0] :
( ~ product(e_1,e_2,X0)
| ~ product(X0,e_3,e_1) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f92]) ).
fof(f94,plain,
( spl0_2
| spl0_12
| spl0_13
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f64,f55,f92,f89,f43]) ).
fof(f96,plain,
( ! [X0] :
( ~ product(e_2,e_1,X0)
| ~ product(e_3,X0,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2) )
| ~ spl0_5 ),
inference(resolution,[],[f60,f1]) ).
fof(f100,definition,
( spl0_14
<=> product(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f101,plain,
( product(e_3,e_2,e_2)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f103,definition,
( spl0_15
<=> product(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f104,plain,
( product(e_3,e_2,e_1)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f115,definition,
( spl0_18
<=> product(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f116,plain,
( product(e_1,e_2,e_1)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f115]) ).
fof(f118,definition,
( spl0_19
<=> ! [X0] :
( ~ product(e_2,e_1,X0)
| ~ product(e_3,X0,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f119,plain,
( ! [X0] :
( ~ product(e_3,X0,e_1)
| ~ product(e_2,e_1,X0) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f120,plain,
( spl0_1
| spl0_18
| spl0_19
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f96,f59,f118,f115,f40]) ).
fof(f123,plain,
( ! [X0] :
( ~ product(e_2,X0,e_2)
| ~ product(X0,e_2,e_2) )
| ~ spl0_9 ),
inference(resolution,[],[f79,f27]) ).
fof(f139,plain,
( ~ product(e_1,e_2,e_2)
| ~ spl0_6
| ~ spl0_13 ),
inference(resolution,[],[f93,f69]) ).
fof(f164,plain,
( ~ product(e_2,e_3,e_2)
| ~ spl0_9
| ~ spl0_14 ),
inference(resolution,[],[f123,f101]) ).
fof(f166,plain,
( $false
| ~ spl0_7
| ~ spl0_9
| ~ spl0_14 ),
inference(resolution,[],[f164,f72]) ).
fof(f168,plain,
( ~ spl0_7
| ~ spl0_9
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f166]) ).
fof(f192,definition,
( spl0_21
<=> group_element(e_1) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f193,plain,
( ~ group_element(e_1)
| spl0_21 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f199,plain,
( $false
| spl0_21 ),
inference(resolution,[],[f193,f1]) ).
fof(f200,plain,
spl0_21,
inference(avatar_contradiction_clause,[],[f199]) ).
fof(f212,definition,
( spl0_24
<=> product(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f216,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,e_1)
| ~ product(e_3,X2,X1)
| ~ product(X2,e_3,X0) ),
inference(resolution,[],[f16,f14]) ).
fof(f228,definition,
( spl0_26
<=> product(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f249,definition,
( spl0_28
<=> product(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f250,plain,
( ~ product(e_1,e_2,e_3)
| spl0_28 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f259,plain,
( ! [X0] :
( ~ product(X0,e_2,e_1)
| ~ product(e_1,e_2,X0) )
| ~ spl0_12 ),
inference(resolution,[],[f90,f27]) ).
fof(f263,plain,
( ! [X0,X1] :
( ~ product(e_2,e_1,X0)
| ~ product(e_1,X1,X0)
| ~ product(X1,e_1,e_3) )
| ~ spl0_19 ),
inference(resolution,[],[f119,f14]) ).
fof(f268,plain,
( ~ product(e_1,e_2,e_1)
| ~ spl0_12 ),
inference(factoring,[],[f259]) ).
fof(f283,definition,
( spl0_32
<=> product(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f284,plain,
( ~ product(e_2,e_3,e_3)
| spl0_32 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f287,definition,
( spl0_33
<=> group_element(e_3) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f288,plain,
( ~ group_element(e_3)
| spl0_33 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f290,definition,
( spl0_34
<=> ! [X0] :
( ~ product(e_1,X0,e_3)
| ~ product(X0,e_1,e_3) ) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f291,plain,
( ! [X0] :
( ~ product(e_1,X0,e_3)
| ~ product(X0,e_1,e_3) )
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f301,plain,
( ! [X0] :
( ~ product(X0,e_2,e_1)
| ~ product(e_2,e_3,X0) )
| ~ spl0_14 ),
inference(resolution,[],[f216,f101]) ).
fof(f303,plain,
! [X0,X1] :
( ~ product(X1,e_3,e_1)
| ~ product(X0,e_3,X1)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| ~ group_element(e_3) ),
inference(resolution,[],[f216,f10]) ).
fof(f305,plain,
! [X0,X1] :
( ~ product(e_3,X1,e_1)
| ~ product(e_3,X0,X1)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| ~ group_element(X0) ),
inference(resolution,[],[f216,f10]) ).
fof(f306,plain,
( ~ product(e_3,e_1,e_1)
| ~ product(e_1,e_3,e_3) ),
inference(factoring,[],[f216]) ).
fof(f309,definition,
( spl0_35
<=> product(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f310,plain,
( ~ product(e_1,e_3,e_3)
| spl0_35 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f312,definition,
( spl0_36
<=> product(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f314,plain,
( ~ spl0_35
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f306,f312,f309]) ).
fof(f316,definition,
( spl0_37
<=> ! [X0,X1] :
( ~ product(e_3,X1,e_1)
| ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_1)
| ~ product(e_3,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f317,plain,
( ! [X0,X1] :
( ~ group_element(X0)
| ~ product(e_3,X1,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_1)
| ~ product(e_3,X0,X1) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f316]) ).
fof(f318,plain,
( ~ spl0_33
| spl0_37 ),
inference(avatar_split_clause,[],[f305,f316,f287]) ).
fof(f320,definition,
( spl0_38
<=> ! [X0,X1] :
( ~ product(X1,e_3,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0)
| ~ product(X0,e_3,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f321,plain,
( ! [X0,X1] :
( ~ group_element(X0)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ product(X1,e_3,e_1)
| ~ product(X0,e_3,X1) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f322,plain,
( ~ spl0_33
| spl0_38 ),
inference(avatar_split_clause,[],[f303,f320,f287]) ).
fof(f323,plain,
( $false
| spl0_33 ),
inference(resolution,[],[f288,f3]) ).
fof(f324,plain,
spl0_33,
inference(avatar_contradiction_clause,[],[f323]) ).
fof(f336,definition,
( spl0_40
<=> product(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f337,plain,
( product(e_1,e_3,e_2)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f338,plain,
( product(e_1,e_3,e_1)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f345,plain,
( ! [X0] :
( ~ product(e_3,X0,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| ~ product(e_3,e_2,X0) )
| ~ spl0_37 ),
inference(resolution,[],[f317,f2]) ).
fof(f348,definition,
( spl0_41
<=> product(e_3,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f349,plain,
( product(e_3,e_3,e_1)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f351,definition,
( spl0_42
<=> product(e_3,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f352,plain,
( product(e_3,e_3,e_2)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f351]) ).
fof(f358,definition,
( spl0_44
<=> ! [X0] :
( ~ product(e_3,X0,e_1)
| ~ product(e_3,e_2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f359,plain,
( ! [X0] :
( ~ product(e_3,X0,e_1)
| ~ product(e_3,e_2,X0) )
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f360,plain,
( spl0_6
| spl0_7
| spl0_44
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f345,f316,f358,f71,f68]) ).
fof(f369,plain,
( ! [X0] :
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_1)
| ~ product(X0,e_3,e_1)
| ~ product(e_1,e_3,X0) )
| ~ spl0_38 ),
inference(resolution,[],[f321,f1]) ).
fof(f377,definition,
( spl0_47
<=> ! [X0] :
( ~ product(X0,e_3,e_1)
| ~ product(e_1,e_3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f378,plain,
( ! [X0] :
( ~ product(X0,e_3,e_1)
| ~ product(e_1,e_3,X0) )
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f379,plain,
( product(e_3,e_1,e_1)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f380,plain,
( product(e_3,e_1,e_2)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f381,plain,
( spl0_47
| spl0_36
| spl0_24
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f369,f320,f212,f312,f377]) ).
fof(f392,plain,
( ~ product(e_2,e_1,e_2)
| ~ product(e_1,e_3,e_2)
| spl0_1
| ~ spl0_36 ),
inference(resolution,[],[f379,f48]) ).
fof(f397,plain,
( ~ spl0_40
| ~ spl0_12
| spl0_1
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f392,f312,f40,f89,f336]) ).
fof(f426,plain,
( ! [X0] :
( ~ product(e_1,X0,e_1)
| ~ product(X0,e_1,e_2) )
| spl0_2 ),
inference(resolution,[],[f44,f14]) ).
fof(f433,plain,
( ! [X0,X1] :
( ~ product(e_1,e_3,X0)
| ~ product(e_1,X1,e_3)
| ~ product(X1,e_1,X0) )
| ~ spl0_47 ),
inference(resolution,[],[f378,f14]) ).
fof(f437,plain,
( ~ product(e_1,e_3,e_1)
| ~ spl0_47 ),
inference(factoring,[],[f378]) ).
fof(f438,plain,
( ~ spl0_26
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f437,f377,f228]) ).
fof(f453,plain,
( ~ product(e_1,e_2,e_1)
| ~ spl0_6
| ~ spl0_14 ),
inference(resolution,[],[f301,f69]) ).
fof(f482,plain,
( ~ group_element(e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| ~ group_element(e_2)
| spl0_32 ),
inference(resolution,[],[f284,f10]) ).
fof(f491,plain,
( ~ product(e_2,e_1,e_3)
| ~ product(e_1,e_2,e_3)
| ~ spl0_19 ),
inference(factoring,[],[f263]) ).
fof(f493,definition,
( spl0_49
<=> product(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f494,plain,
( ~ product(e_2,e_1,e_3)
| spl0_49 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f508,definition,
( spl0_51
<=> product(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f509,plain,
( ~ product(e_3,e_1,e_3)
| spl0_51 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f515,plain,
( ~ group_element(e_1)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| ~ group_element(e_2)
| spl0_49 ),
inference(resolution,[],[f494,f10]) ).
fof(f522,plain,
( ~ group_element(e_1)
| product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| ~ group_element(e_3)
| spl0_51 ),
inference(resolution,[],[f509,f10]) ).
fof(f524,plain,
( ~ spl0_33
| spl0_24
| spl0_36
| ~ spl0_21
| spl0_51 ),
inference(avatar_split_clause,[],[f522,f508,f192,f312,f212,f287]) ).
fof(f526,plain,
( ! [X0] :
( ~ product(e_1,X0,e_3)
| ~ product(X0,e_1,e_3)
| ~ group_element(e_3)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| ~ group_element(e_1) )
| ~ spl0_47 ),
inference(resolution,[],[f433,f10]) ).
fof(f531,plain,
( ~ product(e_1,e_3,e_2)
| ~ product(e_1,e_2,e_3)
| ~ spl0_12
| ~ spl0_47 ),
inference(resolution,[],[f433,f90]) ).
fof(f537,plain,
( ~ spl0_21
| spl0_40
| spl0_26
| ~ spl0_33
| spl0_34
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f526,f377,f290,f287,f228,f336,f192]) ).
fof(f542,plain,
( ~ product(e_1,e_1,e_3)
| ~ spl0_34 ),
inference(factoring,[],[f291]) ).
fof(f551,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,e_2)
| ~ product(e_3,X2,X1)
| ~ product(X2,e_3,X0) ),
inference(resolution,[],[f18,f14]) ).
fof(f552,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ group_element(e_1)
| ~ spl0_34 ),
inference(resolution,[],[f542,f10]) ).
fof(f554,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ spl0_34 ),
inference(duplicate_literal_removal,[],[f552]) ).
fof(f556,definition,
( spl0_54
<=> product(e_1,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f559,definition,
( spl0_55
<=> product(e_1,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f561,plain,
( spl0_54
| spl0_55
| ~ spl0_21
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f554,f290,f192,f559,f556]) ).
fof(f612,plain,
( ! [X0] :
( ~ product(e_1,X0,e_2)
| ~ product(X0,e_1,e_2) )
| spl0_1
| ~ spl0_10 ),
inference(resolution,[],[f82,f48]) ).
fof(f628,plain,
( ! [X0] :
( ~ product(e_3,X0,e_2)
| ~ product(X0,e_3,e_3) )
| ~ spl0_14 ),
inference(resolution,[],[f551,f101]) ).
fof(f633,plain,
! [X0,X1] :
( ~ product(X1,e_3,e_2)
| ~ product(X0,e_3,X1)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| ~ group_element(e_3) ),
inference(resolution,[],[f551,f10]) ).
fof(f637,plain,
( ~ product(e_3,e_2,e_2)
| ~ product(e_2,e_3,e_3) ),
inference(factoring,[],[f551]) ).
fof(f644,definition,
( spl0_60
<=> ! [X0,X1] :
( ~ product(X1,e_3,e_2)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0)
| ~ product(X0,e_3,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f645,plain,
( ! [X0,X1] :
( ~ group_element(X0)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ product(X1,e_3,e_2)
| ~ product(X0,e_3,X1) )
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f644]) ).
fof(f646,plain,
( ~ spl0_33
| spl0_60 ),
inference(avatar_split_clause,[],[f633,f644,f287]) ).
fof(f661,plain,
( ! [X0] :
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_1)
| ~ product(X0,e_3,e_2)
| ~ product(e_1,e_3,X0) )
| ~ spl0_60 ),
inference(resolution,[],[f645,f1]) ).
fof(f662,plain,
( ! [X0] :
( product(e_3,e_2,e_2)
| product(e_3,e_2,e_1)
| ~ product(X0,e_3,e_2)
| ~ product(e_2,e_3,X0) )
| ~ spl0_60 ),
inference(resolution,[],[f645,f2]) ).
fof(f669,definition,
( spl0_64
<=> ! [X0] :
( ~ product(X0,e_3,e_2)
| ~ product(e_1,e_3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f670,plain,
( ! [X0] :
( ~ product(X0,e_3,e_2)
| ~ product(e_1,e_3,X0) )
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f671,plain,
( spl0_64
| spl0_36
| spl0_24
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f661,f644,f212,f312,f669]) ).
fof(f698,plain,
( ~ product(e_2,e_3,e_3)
| ~ spl0_14 ),
inference(resolution,[],[f628,f101]) ).
fof(f717,plain,
( ~ spl0_3
| spl0_12
| spl0_2
| ~ spl0_21
| spl0_49 ),
inference(avatar_split_clause,[],[f515,f493,f192,f43,f89,f52]) ).
fof(f725,plain,
( ~ spl0_3
| spl0_7
| spl0_6
| ~ spl0_33
| spl0_32 ),
inference(avatar_split_clause,[],[f482,f283,f287,f68,f71,f52]) ).
fof(f730,plain,
( ~ spl0_32
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f698,f100,f283]) ).
fof(f736,definition,
( spl0_68
<=> ! [X0] :
( ~ product(X0,e_3,e_2)
| ~ product(e_2,e_3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f737,plain,
( ! [X0] :
( ~ product(X0,e_3,e_2)
| ~ product(e_2,e_3,X0) )
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f736]) ).
fof(f738,plain,
( spl0_68
| spl0_15
| spl0_14
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f662,f644,f100,f103,f736]) ).
fof(f739,plain,
( ~ product(e_3,e_2,e_2)
| spl0_14 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f740,plain,
( ~ spl0_32
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f637,f100,f283]) ).
fof(f741,plain,
( ! [X0] :
( ~ product(e_2,X0,e_2)
| ~ product(X0,e_2,e_3) )
| spl0_14 ),
inference(resolution,[],[f739,f14]) ).
fof(f745,plain,
( ! [X0,X1] :
( ~ product(e_3,e_2,X0)
| ~ product(e_1,X1,X0)
| ~ product(X1,e_1,e_3) )
| ~ spl0_44 ),
inference(resolution,[],[f359,f14]) ).
fof(f754,plain,
( ~ product(e_2,e_3,e_2)
| ~ spl0_68 ),
inference(factoring,[],[f737]) ).
fof(f790,plain,
( ~ product(e_1,e_1,e_2)
| spl0_1
| ~ spl0_10 ),
inference(factoring,[],[f612]) ).
fof(f826,definition,
( spl0_73
<=> ! [X0] :
( ~ product(e_2,X0,e_3)
| ~ product(X0,e_2,e_3) ) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f827,plain,
( ! [X0] :
( ~ product(e_2,X0,e_3)
| ~ product(X0,e_2,e_3) )
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f826]) ).
fof(f837,plain,
( ~ product(e_1,e_3,e_1)
| spl0_2
| ~ spl0_24 ),
inference(resolution,[],[f380,f426]) ).
fof(f929,plain,
( ~ product(e_3,e_3,e_1)
| spl0_41 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f941,plain,
( ! [X0] :
( ~ product(e_1,X0,e_3)
| ~ product(X0,e_1,e_3) )
| spl0_41 ),
inference(resolution,[],[f929,f14]) ).
fof(f974,definition,
( spl0_78
<=> product(e_2,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f975,plain,
( ~ product(e_2,e_2,e_3)
| spl0_78 ),
inference(avatar_component_clause,[],[f974]) ).
fof(f1011,plain,
( ~ spl0_26
| spl0_2
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f837,f212,f43,f228]) ).
fof(f1033,plain,
( ~ product(e_2,e_2,e_3)
| ~ spl0_73 ),
inference(factoring,[],[f827]) ).
fof(f1087,plain,
( ~ product(e_2,e_3,e_2)
| spl0_1
| ~ spl0_15 ),
inference(resolution,[],[f104,f46]) ).
fof(f1101,plain,
! [X2,X0,X1] :
( ~ product(X0,e_1,X1)
| ~ product(X1,X2,e_2)
| ~ product(X2,X1,X0) ),
inference(resolution,[],[f21,f14]) ).
fof(f1102,plain,
! [X0] :
( ~ product(X0,e_1,e_3)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| ~ group_element(X0) ),
inference(resolution,[],[f21,f10]) ).
fof(f1103,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_18 ),
inference(resolution,[],[f21,f116]) ).
fof(f1104,plain,
( ~ product(e_2,e_1,e_2)
| ~ spl0_10 ),
inference(resolution,[],[f21,f82]) ).
fof(f1106,plain,
( ~ spl0_55
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f1103,f115,f559]) ).
fof(f1108,definition,
( spl0_82
<=> ! [X0] :
( ~ product(X0,e_1,e_3)
| ~ group_element(X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f1109,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product(X0,e_1,e_3)
| product(X0,e_2,e_2)
| product(X0,e_2,e_1) )
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f1108]) ).
fof(f1110,plain,
( ~ spl0_3
| spl0_82 ),
inference(avatar_split_clause,[],[f1102,f1108,f52]) ).
fof(f1123,plain,
( ~ product(e_1,e_1,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_1)
| ~ spl0_82 ),
inference(resolution,[],[f1109,f1]) ).
fof(f1124,plain,
( ~ product(e_2,e_1,e_3)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1)
| ~ spl0_82 ),
inference(resolution,[],[f1109,f2]) ).
fof(f1154,plain,
( ! [X0] :
( ~ product(e_1,X0,e_3)
| ~ product(X0,e_1,e_3)
| ~ group_element(e_2)
| product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| ~ group_element(e_3) )
| ~ spl0_44 ),
inference(resolution,[],[f745,f10]) ).
fof(f1174,plain,
! [X0,X1] :
( ~ product(e_3,X1,e_2)
| ~ product(X1,e_3,X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| ~ group_element(X0) ),
inference(resolution,[],[f1101,f10]) ).
fof(f1180,plain,
( ~ product(e_2,e_1,e_2)
| ~ product(e_1,e_2,e_2) ),
inference(factoring,[],[f1101]) ).
fof(f1181,plain,
! [X0] :
( ~ product(e_2,e_1,X0)
| ~ product(X0,X0,e_2) ),
inference(factoring,[],[f1101]) ).
fof(f1183,definition,
( spl0_84
<=> ! [X0,X1] :
( ~ product(e_3,X1,e_2)
| ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_1)
| ~ product(X1,e_3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f1184,plain,
( ! [X0,X1] :
( ~ group_element(X0)
| ~ product(e_3,X1,e_2)
| product(X0,e_1,e_2)
| product(X0,e_1,e_1)
| ~ product(X1,e_3,X0) )
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f1183]) ).
fof(f1185,plain,
( ~ spl0_21
| spl0_84 ),
inference(avatar_split_clause,[],[f1174,f1183,f192]) ).
fof(f1187,plain,
( ! [X0] :
( ~ product(e_3,X0,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| ~ product(X0,e_3,e_2) )
| ~ spl0_84 ),
inference(resolution,[],[f1184,f2]) ).
fof(f1190,definition,
( spl0_85
<=> ! [X0] :
( ~ product(e_3,X0,e_2)
| ~ product(X0,e_3,e_2) ) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f1191,plain,
( ! [X0] :
( ~ product(e_3,X0,e_2)
| ~ product(X0,e_3,e_2) )
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f1190]) ).
fof(f1192,plain,
( spl0_2
| spl0_12
| spl0_85
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f1187,f1183,f1190,f89,f43]) ).
fof(f1262,plain,
! [X2,X0,X1] :
( ~ product(X0,e_1,X1)
| ~ product(X1,X2,e_3)
| ~ product(X2,X1,X0) ),
inference(resolution,[],[f22,f14]) ).
fof(f1263,plain,
! [X0] :
( ~ product(X0,e_1,e_3)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| ~ group_element(X0) ),
inference(resolution,[],[f22,f10]) ).
fof(f1264,plain,
( ~ product(e_1,e_1,e_2)
| ~ spl0_40 ),
inference(resolution,[],[f22,f337]) ).
fof(f1266,definition,
( spl0_90
<=> ! [X0] :
( ~ product(X0,e_1,e_3)
| ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f1267,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product(X0,e_1,e_3)
| product(X0,e_3,e_2)
| product(X0,e_3,e_1) )
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f1266]) ).
fof(f1268,plain,
( ~ spl0_33
| spl0_90 ),
inference(avatar_split_clause,[],[f1263,f1266,f287]) ).
fof(f1276,plain,
( spl0_34
| spl0_41 ),
inference(avatar_split_clause,[],[f941,f348,f290]) ).
fof(f1286,plain,
( ~ product(e_1,e_1,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| ~ spl0_90 ),
inference(resolution,[],[f1267,f1]) ).
fof(f1287,plain,
( ~ product(e_2,e_1,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| ~ spl0_90 ),
inference(resolution,[],[f1267,f2]) ).
fof(f1288,plain,
( ~ product(e_3,e_1,e_3)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_1)
| ~ spl0_90 ),
inference(resolution,[],[f1267,f3]) ).
fof(f1289,plain,
( spl0_41
| spl0_42
| ~ spl0_51
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f1288,f1266,f508,f351,f348]) ).
fof(f1290,plain,
( spl0_6
| spl0_7
| ~ spl0_49
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f1287,f1266,f493,f71,f68]) ).
fof(f1293,plain,
( ~ spl0_18
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f268,f89,f115]) ).
fof(f1294,plain,
( ~ spl0_28
| ~ spl0_40
| ~ spl0_12
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f531,f377,f89,f336,f249]) ).
fof(f1295,plain,
( ~ spl0_7
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f754,f736,f71]) ).
fof(f1302,plain,
( ~ product(e_1,e_3,e_2)
| ~ spl0_7
| ~ spl0_64 ),
inference(resolution,[],[f72,f670]) ).
fof(f1304,plain,
( ~ product(e_2,e_1,e_2)
| ~ spl0_7 ),
inference(resolution,[],[f72,f22]) ).
fof(f1306,plain,
( ~ spl0_12
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f1304,f71,f89]) ).
fof(f1307,plain,
( ~ spl0_40
| ~ spl0_7
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f1302,f669,f71,f336]) ).
fof(f1310,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f139,f92,f68,f40]) ).
fof(f1312,plain,
( ~ spl0_7
| spl0_1
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f1087,f103,f40,f71]) ).
fof(f1322,plain,
( ~ product(e_2,e_1,e_1)
| ~ spl0_6 ),
inference(resolution,[],[f69,f22]) ).
fof(f1340,plain,
( ~ product(e_3,e_1,e_1)
| ~ spl0_41 ),
inference(resolution,[],[f349,f22]) ).
fof(f1350,plain,
( ~ product(e_1,e_3,e_2)
| ~ spl0_24
| ~ spl0_85 ),
inference(resolution,[],[f380,f1191]) ).
fof(f1365,plain,
( ~ spl0_40
| ~ spl0_24
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f1350,f1190,f212,f336]) ).
fof(f1367,plain,
( ~ spl0_12
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f1104,f81,f89]) ).
fof(f1370,definition,
( spl0_92
<=> product(e_1,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f1371,plain,
( ~ product(e_1,e_1,e_3)
| spl0_92 ),
inference(avatar_component_clause,[],[f1370]) ).
fof(f1372,plain,
( spl0_18
| spl0_1
| ~ spl0_92
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f1123,f1108,f1370,f40,f115]) ).
fof(f1373,plain,
( spl0_9
| spl0_10
| ~ spl0_49
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f1124,f1108,f493,f81,f78]) ).
fof(f1375,plain,
( ~ spl0_1
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1180,f89,f40]) ).
fof(f1382,plain,
( ~ spl0_78
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1033,f826,f974]) ).
fof(f1388,plain,
( spl0_26
| spl0_40
| ~ spl0_92
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f1286,f1266,f1370,f336,f228]) ).
fof(f1396,plain,
( ~ spl0_2
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f1322,f68,f43]) ).
fof(f1398,plain,
( ~ spl0_92
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f542,f290,f1370]) ).
fof(f1404,plain,
( ~ spl0_33
| spl0_14
| spl0_15
| ~ spl0_3
| spl0_34
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f1154,f358,f290,f52,f103,f100,f287]) ).
fof(f1406,definition,
( spl0_93
<=> ! [X0] :
( ~ product(e_3,X0,e_2)
| ~ product(X0,e_3,e_3) ) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f1407,plain,
( ! [X0] :
( ~ product(e_3,X0,e_2)
| ~ product(X0,e_3,e_3) )
| ~ spl0_93 ),
inference(avatar_component_clause,[],[f1406]) ).
fof(f1428,plain,
( ~ spl0_36
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f1340,f348,f312]) ).
fof(f1431,plain,
( ~ spl0_28
| ~ spl0_49
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f491,f118,f493,f249]) ).
fof(f1434,plain,
( ~ product(e_1,e_2,e_3)
| ~ spl0_12
| spl0_14 ),
inference(resolution,[],[f90,f741]) ).
fof(f1440,plain,
( ~ spl0_28
| ~ spl0_12
| spl0_14 ),
inference(avatar_split_clause,[],[f1434,f100,f89,f249]) ).
fof(f1441,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ group_element(e_1)
| spl0_92 ),
inference(resolution,[],[f1371,f10]) ).
fof(f1442,plain,
( ! [X0] :
( ~ product(e_3,X0,e_1)
| ~ product(X0,e_3,e_1) )
| spl0_92 ),
inference(resolution,[],[f1371,f14]) ).
fof(f1443,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| spl0_92 ),
inference(duplicate_literal_removal,[],[f1441]) ).
fof(f1444,plain,
( spl0_54
| spl0_55
| ~ spl0_21
| spl0_92 ),
inference(avatar_split_clause,[],[f1443,f1370,f192,f559,f556]) ).
fof(f1458,plain,
( ~ product(e_2,e_1,e_3)
| ~ spl0_42 ),
inference(resolution,[],[f352,f1181]) ).
fof(f1462,plain,
( ~ spl0_49
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f1458,f351,f493]) ).
fof(f1472,plain,
( ~ product(e_1,e_1,e_1)
| ~ product(e_1,e_3,e_2)
| ~ spl0_36 ),
inference(resolution,[],[f379,f1101]) ).
fof(f1473,plain,
( ~ spl0_40
| ~ spl0_55
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f1472,f312,f559,f336]) ).
fof(f1483,plain,
( ~ product(e_1,e_2,e_1)
| ~ spl0_13
| ~ spl0_26 ),
inference(resolution,[],[f93,f338]) ).
fof(f1485,plain,
( ~ spl0_18
| ~ spl0_13
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1483,f228,f92,f115]) ).
fof(f1491,plain,
( ~ spl0_18
| ~ spl0_6
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f453,f100,f68,f115]) ).
fof(f1497,plain,
( ~ product(e_3,e_1,e_2)
| ~ spl0_14 ),
inference(resolution,[],[f101,f21]) ).
fof(f1506,plain,
( ~ spl0_24
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1497,f100,f212]) ).
fof(f1526,plain,
( ~ product(e_1,e_3,e_2)
| ~ spl0_6
| ~ spl0_68 ),
inference(resolution,[],[f737,f69]) ).
fof(f1529,plain,
( ~ spl0_40
| ~ spl0_6
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f1526,f736,f68,f336]) ).
fof(f1542,plain,
( ~ group_element(e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| ~ group_element(e_1)
| spl0_28 ),
inference(resolution,[],[f250,f10]) ).
fof(f1545,plain,
( ~ spl0_21
| spl0_1
| spl0_18
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f1542,f249,f52,f115,f40,f192]) ).
fof(f1563,plain,
( ~ product(e_1,e_3,e_1)
| ~ spl0_36
| spl0_92 ),
inference(resolution,[],[f1442,f379]) ).
fof(f1568,plain,
( ~ spl0_26
| ~ spl0_36
| spl0_92 ),
inference(avatar_split_clause,[],[f1563,f1370,f312,f228]) ).
fof(f1582,plain,
( ~ product(e_3,e_1,e_3)
| ~ product(e_1,e_3,e_3) ),
inference(factoring,[],[f1262]) ).
fof(f1584,plain,
( ~ spl0_35
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f1582,f508,f309]) ).
fof(f1615,plain,
( ~ product(e_1,e_3,e_3)
| ~ spl0_24
| ~ spl0_93 ),
inference(resolution,[],[f380,f1407]) ).
fof(f1622,plain,
( ! [X0] :
( ~ product(e_2,X0,e_3)
| ~ product(X0,e_2,e_3) )
| ~ spl0_24 ),
inference(resolution,[],[f380,f1262]) ).
fof(f1628,plain,
( spl0_73
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f1622,f212,f826]) ).
fof(f1629,plain,
( ~ spl0_35
| ~ spl0_24
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f1615,f1406,f212,f309]) ).
fof(f1652,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| ~ group_element(e_2)
| spl0_78 ),
inference(resolution,[],[f975,f10]) ).
fof(f1654,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| spl0_78 ),
inference(duplicate_literal_removal,[],[f1652]) ).
fof(f1659,plain,
! [X0] :
( ~ product(X0,e_2,e_3)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| ~ group_element(X0) ),
inference(resolution,[],[f24,f10]) ).
fof(f1660,plain,
( ~ product(e_2,e_2,e_1)
| ~ spl0_6 ),
inference(resolution,[],[f24,f69]) ).
fof(f1661,plain,
( ~ spl0_9
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f1660,f68,f78]) ).
fof(f1663,definition,
( spl0_98
<=> ! [X0] :
( ~ product(X0,e_2,e_3)
| ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f1664,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product(X0,e_2,e_3)
| product(X0,e_3,e_2)
| product(X0,e_3,e_1) )
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f1663]) ).
fof(f1665,plain,
( ~ spl0_33
| spl0_98 ),
inference(avatar_split_clause,[],[f1659,f1663,f287]) ).
fof(f1671,plain,
( ~ spl0_54
| spl0_1
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f790,f81,f40,f556]) ).
fof(f1673,plain,
( ~ spl0_54
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1264,f336,f556]) ).
fof(f1678,plain,
( spl0_10
| spl0_9
| ~ spl0_3
| spl0_78 ),
inference(avatar_split_clause,[],[f1654,f974,f52,f78,f81]) ).
fof(f1679,plain,
( ~ group_element(e_3)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| ~ group_element(e_1)
| spl0_35 ),
inference(resolution,[],[f310,f10]) ).
fof(f1682,plain,
( ~ spl0_21
| spl0_40
| spl0_26
| ~ spl0_33
| spl0_35 ),
inference(avatar_split_clause,[],[f1679,f309,f287,f228,f336,f192]) ).
fof(f1683,plain,
( ~ product(e_1,e_2,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| ~ spl0_98 ),
inference(resolution,[],[f1664,f1]) ).
fof(f1687,plain,
( spl0_26
| spl0_40
| ~ spl0_28
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f1683,f1663,f249,f336,f228]) ).
fof(f1698,plain,
( ~ product(e_1,e_1,e_2)
| ~ spl0_2 ),
inference(resolution,[],[f87,f1181]) ).
fof(f1704,plain,
( ~ product(e_1,e_1,e_1)
| ~ product(e_1,e_2,e_3)
| ~ spl0_2 ),
inference(resolution,[],[f87,f1262]) ).
fof(f1706,plain,
( ~ spl0_28
| ~ spl0_55
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f1704,f43,f559,f249]) ).
fof(f1708,plain,
( ~ spl0_54
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f1698,f43,f556]) ).
fof(f1717,plain,
( ! [X0] :
( ~ product(e_3,X0,e_2)
| ~ product(X0,e_3,e_3) )
| ~ spl0_15 ),
inference(resolution,[],[f104,f216]) ).
fof(f1722,plain,
( spl0_93
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f1717,f103,f1406]) ).
fof(f1737,plain,
( ~ product(e_3,e_2,e_1)
| ~ spl0_41 ),
inference(resolution,[],[f349,f24]) ).
fof(f1745,plain,
( ~ spl0_15
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f1737,f348,f103]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f45]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f57]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_5 ),
inference(sat_conversion,[],[f61]) ).
cnf(s4,plain,
spl0_3,
inference(sat_conversion,[],[f63]) ).
cnf(s7,plain,
( spl0_2
| ~ spl0_4
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f94]) ).
cnf(s10,plain,
( spl0_1
| ~ spl0_5
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f120]) ).
cnf(s14,plain,
( ~ spl0_7
| ~ spl0_9
| ~ spl0_14 ),
inference(sat_conversion,[],[f168]) ).
cnf(s18,plain,
spl0_21,
inference(sat_conversion,[],[f200]) ).
cnf(s26,plain,
( ~ spl0_35
| ~ spl0_36 ),
inference(sat_conversion,[],[f314]) ).
cnf(s27,plain,
( ~ spl0_33
| spl0_37 ),
inference(sat_conversion,[],[f318]) ).
cnf(s28,plain,
( ~ spl0_33
| spl0_38 ),
inference(sat_conversion,[],[f322]) ).
cnf(s29,plain,
spl0_33,
inference(sat_conversion,[],[f324]) ).
cnf(s33,plain,
( spl0_6
| spl0_7
| ~ spl0_37
| spl0_44 ),
inference(sat_conversion,[],[f360]) ).
cnf(s38,plain,
( spl0_24
| spl0_36
| ~ spl0_38
| spl0_47 ),
inference(sat_conversion,[],[f381]) ).
cnf(s39,plain,
( spl0_1
| ~ spl0_12
| ~ spl0_36
| ~ spl0_40 ),
inference(sat_conversion,[],[f397]) ).
cnf(s48,plain,
( ~ spl0_26
| ~ spl0_47 ),
inference(sat_conversion,[],[f438]) ).
cnf(s60,plain,
( ~ spl0_21
| spl0_24
| ~ spl0_33
| spl0_36
| spl0_51 ),
inference(sat_conversion,[],[f524]) ).
cnf(s63,plain,
( ~ spl0_21
| spl0_26
| ~ spl0_33
| spl0_34
| spl0_40
| ~ spl0_47 ),
inference(sat_conversion,[],[f537]) ).
cnf(s66,plain,
( ~ spl0_21
| ~ spl0_34
| spl0_54
| spl0_55 ),
inference(sat_conversion,[],[f561]) ).
cnf(s72,plain,
( ~ spl0_33
| spl0_60 ),
inference(sat_conversion,[],[f646]) ).
cnf(s77,plain,
( spl0_24
| spl0_36
| ~ spl0_60
| spl0_64 ),
inference(sat_conversion,[],[f671]) ).
cnf(s80,plain,
( spl0_2
| ~ spl0_3
| spl0_12
| ~ spl0_21
| spl0_49 ),
inference(sat_conversion,[],[f717]) ).
cnf(s82,plain,
( ~ spl0_3
| spl0_6
| spl0_7
| spl0_32
| ~ spl0_33 ),
inference(sat_conversion,[],[f725]) ).
cnf(s84,plain,
( ~ spl0_14
| ~ spl0_32 ),
inference(sat_conversion,[],[f730]) ).
cnf(s87,plain,
( spl0_14
| spl0_15
| ~ spl0_60
| spl0_68 ),
inference(sat_conversion,[],[f738]) ).
cnf(s88,plain,
( ~ spl0_14
| ~ spl0_32 ),
inference(sat_conversion,[],[f740]) ).
cnf(s120,plain,
( spl0_2
| ~ spl0_24
| ~ spl0_26 ),
inference(sat_conversion,[],[f1011]) ).
cnf(s133,plain,
( ~ spl0_18
| ~ spl0_55 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s134,plain,
( ~ spl0_3
| spl0_82 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s144,plain,
( ~ spl0_21
| spl0_84 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s145,plain,
( spl0_2
| spl0_12
| ~ spl0_84
| spl0_85 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s155,plain,
( ~ spl0_33
| spl0_90 ),
inference(sat_conversion,[],[f1268]) ).
cnf(s158,plain,
( spl0_34
| spl0_41 ),
inference(sat_conversion,[],[f1276]) ).
cnf(s171,plain,
( spl0_41
| spl0_42
| ~ spl0_51
| ~ spl0_90 ),
inference(sat_conversion,[],[f1289]) ).
cnf(s172,plain,
( spl0_6
| spl0_7
| ~ spl0_49
| ~ spl0_90 ),
inference(sat_conversion,[],[f1290]) ).
cnf(s177,plain,
( ~ spl0_12
| ~ spl0_18 ),
inference(sat_conversion,[],[f1293]) ).
cnf(s182,plain,
( ~ spl0_12
| ~ spl0_28
| ~ spl0_40
| ~ spl0_47 ),
inference(sat_conversion,[],[f1294]) ).
cnf(s183,plain,
( ~ spl0_7
| ~ spl0_68 ),
inference(sat_conversion,[],[f1295]) ).
cnf(s184,plain,
( ~ spl0_7
| ~ spl0_12 ),
inference(sat_conversion,[],[f1306]) ).
cnf(s185,plain,
( ~ spl0_7
| ~ spl0_40
| ~ spl0_64 ),
inference(sat_conversion,[],[f1307]) ).
cnf(s188,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_13 ),
inference(sat_conversion,[],[f1310]) ).
cnf(s191,plain,
( spl0_1
| ~ spl0_7
| ~ spl0_15 ),
inference(sat_conversion,[],[f1312]) ).
cnf(s198,plain,
( ~ spl0_24
| ~ spl0_40
| ~ spl0_85 ),
inference(sat_conversion,[],[f1365]) ).
cnf(s200,plain,
( ~ spl0_10
| ~ spl0_12 ),
inference(sat_conversion,[],[f1367]) ).
cnf(s207,plain,
( spl0_1
| spl0_18
| ~ spl0_82
| ~ spl0_92 ),
inference(sat_conversion,[],[f1372]) ).
cnf(s208,plain,
( spl0_9
| spl0_10
| ~ spl0_49
| ~ spl0_82 ),
inference(sat_conversion,[],[f1373]) ).
cnf(s210,plain,
( ~ spl0_1
| ~ spl0_12 ),
inference(sat_conversion,[],[f1375]) ).
cnf(s220,plain,
( ~ spl0_73
| ~ spl0_78 ),
inference(sat_conversion,[],[f1382]) ).
cnf(s228,plain,
( spl0_26
| spl0_40
| ~ spl0_90
| ~ spl0_92 ),
inference(sat_conversion,[],[f1388]) ).
cnf(s236,plain,
( ~ spl0_2
| ~ spl0_6 ),
inference(sat_conversion,[],[f1396]) ).
cnf(s241,plain,
( ~ spl0_34
| ~ spl0_92 ),
inference(sat_conversion,[],[f1398]) ).
cnf(s252,plain,
( ~ spl0_3
| spl0_14
| spl0_15
| ~ spl0_33
| spl0_34
| ~ spl0_44 ),
inference(sat_conversion,[],[f1404]) ).
cnf(s271,plain,
( ~ spl0_36
| ~ spl0_41 ),
inference(sat_conversion,[],[f1428]) ).
cnf(s282,plain,
( ~ spl0_19
| ~ spl0_28
| ~ spl0_49 ),
inference(sat_conversion,[],[f1431]) ).
cnf(s296,plain,
( ~ spl0_12
| spl0_14
| ~ spl0_28 ),
inference(sat_conversion,[],[f1440]) ).
cnf(s297,plain,
( ~ spl0_21
| spl0_54
| spl0_55
| spl0_92 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s299,plain,
( ~ spl0_42
| ~ spl0_49 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s303,plain,
( ~ spl0_36
| ~ spl0_40
| ~ spl0_55 ),
inference(sat_conversion,[],[f1473]) ).
cnf(s308,plain,
( ~ spl0_13
| ~ spl0_18
| ~ spl0_26 ),
inference(sat_conversion,[],[f1485]) ).
cnf(s314,plain,
( ~ spl0_6
| ~ spl0_14
| ~ spl0_18 ),
inference(sat_conversion,[],[f1491]) ).
cnf(s323,plain,
( ~ spl0_14
| ~ spl0_24 ),
inference(sat_conversion,[],[f1506]) ).
cnf(s330,plain,
( ~ spl0_6
| ~ spl0_40
| ~ spl0_68 ),
inference(sat_conversion,[],[f1529]) ).
cnf(s336,plain,
( spl0_1
| ~ spl0_3
| spl0_18
| ~ spl0_21
| spl0_28 ),
inference(sat_conversion,[],[f1545]) ).
cnf(s342,plain,
( ~ spl0_26
| ~ spl0_36
| spl0_92 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s365,plain,
( ~ spl0_35
| ~ spl0_51 ),
inference(sat_conversion,[],[f1584]) ).
cnf(s373,plain,
( ~ spl0_24
| spl0_73 ),
inference(sat_conversion,[],[f1628]) ).
cnf(s375,plain,
( ~ spl0_24
| ~ spl0_35
| ~ spl0_93 ),
inference(sat_conversion,[],[f1629]) ).
cnf(s379,plain,
( ~ spl0_6
| ~ spl0_9 ),
inference(sat_conversion,[],[f1661]) ).
cnf(s380,plain,
( ~ spl0_33
| spl0_98 ),
inference(sat_conversion,[],[f1665]) ).
cnf(s387,plain,
( spl0_1
| ~ spl0_10
| ~ spl0_54 ),
inference(sat_conversion,[],[f1671]) ).
cnf(s392,plain,
( ~ spl0_40
| ~ spl0_54 ),
inference(sat_conversion,[],[f1673]) ).
cnf(s412,plain,
( ~ spl0_3
| spl0_9
| spl0_10
| spl0_78 ),
inference(sat_conversion,[],[f1678]) ).
cnf(s414,plain,
( ~ spl0_21
| spl0_26
| ~ spl0_33
| spl0_35
| spl0_40 ),
inference(sat_conversion,[],[f1682]) ).
cnf(s416,plain,
( spl0_26
| ~ spl0_28
| spl0_40
| ~ spl0_98 ),
inference(sat_conversion,[],[f1687]) ).
cnf(s420,plain,
( ~ spl0_2
| ~ spl0_28
| ~ spl0_55 ),
inference(sat_conversion,[],[f1706]) ).
cnf(s422,plain,
( ~ spl0_2
| ~ spl0_54 ),
inference(sat_conversion,[],[f1708]) ).
cnf(s424,plain,
( ~ spl0_15
| spl0_93 ),
inference(sat_conversion,[],[f1722]) ).
cnf(s429,plain,
( ~ spl0_15
| ~ spl0_41 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s434,plain,
spl0_98,
inference(rat,[],[s380,s29]) ).
cnf(s435,plain,
spl0_90,
inference(rat,[],[s155,s29]) ).
cnf(s436,plain,
spl0_60,
inference(rat,[],[s72,s29]) ).
cnf(s438,plain,
spl0_38,
inference(rat,[],[s28,s29]) ).
cnf(s439,plain,
spl0_37,
inference(rat,[],[s27,s29]) ).
cnf(s442,plain,
spl0_84,
inference(rat,[],[s144,s18]) ).
cnf(s444,plain,
spl0_82,
inference(rat,[],[s134,s4]) ).
cnf(s445,plain,
spl0_5,
inference(rat,[],[s3,s4]) ).
cnf(s446,plain,
spl0_4,
inference(rat,[],[s2,s4]) ).
cnf(s447,plain,
( spl0_7
| spl0_6
| spl0_2
| spl0_1 ),
inference(rat,[],[s336,s296,s177,s88,s80,s82,s172,s4,s18,s29,s435]) ).
cnf(s448,plain,
( spl0_18
| ~ spl0_49
| spl0_1 ),
inference(rat,[],[s282,s10,s336,s445,s4,s18]) ).
cnf(s449,plain,
( ~ spl0_7
| spl0_2
| spl0_1 ),
inference(rat,[],[s77,s271,s185,s158,s228,s66,s297,s133,s308,s448,s387,s208,s14,s323,s87,s7,s80,s183,s184,s191,s436,s435,s18,s444,s446,s4]) ).
cnf(s450,plain,
( spl0_12
| spl0_2
| spl0_1 ),
inference(rat,[],[s87,s429,s330,s158,s228,s66,s297,s387,s314,s133,s308,s208,s448,s7,s80,s379,s447,s449,s436,s435,s18,s444,s446,s4]) ).
cnf(s451,plain,
( ~ spl0_40
| spl0_2
| spl0_1 ),
inference(rat,[],[s38,s39,s182,s336,s177,s373,s220,s412,s200,s450,s379,s447,s449,s438,s4,s18]) ).
cnf(s452,plain,
( spl0_7
| spl0_2
| spl0_1 ),
inference(rat,[],[s38,s48,s342,s416,s451,s373,s220,s336,s207,s412,s177,s200,s450,s379,s447,s444,s18,s4,s434,s438]) ).
cnf(s453,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s452,s449]) ).
cnf(s454,plain,
( spl0_18
| spl0_1 ),
inference(rat,[],[s420,s297,s336,s207,s422,s453,s18,s4,s444]) ).
cnf(s455,plain,
( spl0_7
| spl0_1 ),
inference(rat,[],[s84,s252,s82,s33,s236,s429,s158,s66,s133,s454,s422,s453,s4,s29,s439,s18]) ).
cnf(s456,plain,
spl0_1,
inference(rat,[],[s63,s48,s185,s38,s77,s323,s87,s183,s455,s429,s271,s158,s66,s133,s454,s422,s453,s29,s18,s438,s436]) ).
cnf(s457,plain,
~ spl0_12,
inference(rat,[],[s210,s456]) ).
cnf(s458,plain,
~ spl0_2,
inference(rat,[],[s1,s456]) ).
cnf(s460,plain,
spl0_85,
inference(rat,[],[s145,s458,s442,s457]) ).
cnf(s461,plain,
spl0_49,
inference(rat,[],[s80,s458,s18,s4,s457]) ).
cnf(s462,plain,
spl0_13,
inference(rat,[],[s7,s458,s446,s457]) ).
cnf(s464,plain,
~ spl0_42,
inference(rat,[],[s299,s461]) ).
cnf(s466,plain,
~ spl0_6,
inference(rat,[],[s188,s456,s462]) ).
cnf(s470,plain,
spl0_7,
inference(rat,[],[s172,s435,s461,s466]) ).
cnf(s471,plain,
~ spl0_68,
inference(rat,[],[s183,s470]) ).
cnf(s472,plain,
( ~ spl0_40
| spl0_41 ),
inference(rat,[],[s303,s60,s66,s198,s392,s158,s171,s29,s18,s460,s435,s464]) ).
cnf(s475,plain,
~ spl0_40,
inference(rat,[],[s271,s77,s472,s185,s198,s436,s470,s460]) ).
cnf(s477,plain,
( ~ spl0_24
| ~ spl0_35 ),
inference(rat,[],[s87,s424,s323,s375,s471,s436]) ).
cnf(s478,plain,
~ spl0_35,
inference(rat,[],[s477,s60,s26,s365,s29,s18]) ).
cnf(s481,plain,
spl0_26,
inference(rat,[],[s414,s475,s18,s29,s478]) ).
cnf(s483,plain,
~ spl0_47,
inference(rat,[],[s48,s481]) ).
cnf(s484,plain,
~ spl0_24,
inference(rat,[],[s120,s458,s481]) ).
cnf(s486,plain,
spl0_36,
inference(rat,[],[s38,s484,s438,s483]) ).
cnf(s487,plain,
spl0_92,
inference(rat,[],[s342,s481,s486]) ).
cnf(s488,plain,
~ spl0_41,
inference(rat,[],[s271,s486]) ).
cnf(s492,plain,
~ spl0_34,
inference(rat,[],[s241,s487]) ).
cnf(s493,plain,
$false,
inference(rat,[],[s158,s488,s492]) ).
fof(f1746,plain,
$false,
inference(avatar_sat_refutation,[],[s493]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP134-1.003 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n018.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 09:33:23 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.37/1.16 % (2072921)Input is clausal, will run a generic CNF schedule.
% 2.37/1.16 % (2072932)dis-21_1_sil=8000:lcm=predicate:random_seed=382634128: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)
% 2.37/1.16 % (2072932)First to succeed.
% 2.37/1.16 % (2072932)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2072921"
% 2.37/1.16 % (2072927)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1105306076:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.37/1.16 % (2072928)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3857050943:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.37/1.16 % (2072926)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=1888231440:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.37/1.16 % (2072929)lrs+10_1_sil=8000:sp=occurrence:random_seed=453841241:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.37/1.16 % (2072930)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1719377779:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.37/1.16 % (2072931)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1608903153:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.37/1.16 % (2072931)Also succeeded, but the first one will report.
% 2.37/1.16 % (2072930)Instruction limit reached!
% 2.37/1.16 % (2072930)------------------------------
% 2.37/1.16 % (2072930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.37/1.16 % (2072930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.37/1.16 % (2072930)CaDiCaL version: 2.1.3
% 2.37/1.16 % (2072930)Termination reason: Instruction limit
% 2.37/1.16 % (2072930)Termination phase: Saturation
% 2.37/1.16 % (2072930)Time elapsed: 0.061 s
% 2.37/1.16 % (2072930)Peak memory usage: 87 MB
% 2.37/1.16 % (2072930)Instructions burned: 115 (million)
% 2.37/1.16 % (2072929)Instruction limit reached!
% 2.37/1.16 % (2072929)------------------------------
% 2.37/1.16 % (2072929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.37/1.16 % (2072929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.37/1.16 % (2072929)CaDiCaL version: 2.1.3
% 2.37/1.16 % (2072929)Termination reason: Instruction limit
% 2.37/1.16 % (2072929)Termination phase: Saturation
% 2.37/1.16 % (2072929)Time elapsed: 0.066 s
% 2.37/1.16 % (2072929)Peak memory usage: 88 MB
% 2.37/1.16 % (2072929)Instructions burned: 108 (million)
% 2.37/1.16 % (2072932)Refutation found. Thanks to Tanya!
% 2.37/1.16 % SZS status Unsatisfiable for theBenchmark
% 2.37/1.16 % SZS output start Proof for theBenchmark
% See solution above
% 2.71/1.26 % (2072932)------------------------------
% 2.71/1.26 % (2072932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.71/1.26 % (2072932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.26 % (2072932)CaDiCaL version: 2.1.3
% 2.71/1.26 % (2072932)Termination reason: Refutation
% 2.71/1.26 % (2072932)Time elapsed: 0.023 s
% 2.71/1.26 % (2072932)Peak memory usage: 89 MB
% 2.71/1.26 % (2072932)Instructions burned: 61 (million)
% 2.71/1.26 % (2072932)------------------------------
% 2.71/1.26 % (2072932)------------------------------
% 2.71/1.26 % (2072921)Success in time 0.313 s
% 2.71/1.26 % Vampire exiting
%------------------------------------------------------------------------------