%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP124-7.004 : 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 : n009.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:42 AM UTC 2026
% Result : Unsatisfiable 2.75s 1.32s
% Output : Refutation 3.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 61
% Syntax : Number of formulae : 332 ( 79 unt; 44 def)
% Number of atoms : 832 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 923 ( 423 ~; 456 |; 0 &)
% ( 44 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 49 ( 48 usr; 45 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 72 ( 0 sgn 72 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
fof(f12,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
fof(f13,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
fof(f14,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
fof(f15,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f16,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f17,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f19,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f20,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f23,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f27,axiom,
! [X0,X1] :
( product1(X0,X1,e_4)
| ~ group_element(X1)
| product1(X0,X1,e_1)
| product1(X0,X1,e_2)
| product1(X0,X1,e_3)
| ~ group_element(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_total_function1) ).
fof(f29,axiom,
! [X2,X3,X0,X1] :
( equalish(X1,X3)
| ~ product1(X0,X3,X2)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_right_cancellation) ).
fof(f30,axiom,
! [X2,X3,X0,X1] :
( equalish(X0,X3)
| ~ product1(X3,X1,X2)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_left_cancellation) ).
fof(f31,axiom,
! [X0] : product1(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_idempotence) ).
fof(f33,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ product2(X0,X1,X3)
| ~ product2(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_total_function2) ).
fof(f36,axiom,
! [X0] : product2(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_idempotence) ).
fof(f37,negated_conjecture,
! [X2,X3,X0,X1] :
( product2(X3,X1,X0)
| ~ product1(X2,X0,X3)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg2a) ).
fof(f51,plain,
! [X0,X1] :
( ~ product1(X0,e_2,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f29,f15]) ).
fof(f52,plain,
! [X0,X1] :
( ~ product1(X0,e_3,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f29,f16]) ).
fof(f53,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f29,f17]) ).
fof(f55,plain,
! [X0,X1] :
( ~ product1(X0,e_3,X1)
| ~ product1(X0,e_2,X1) ),
inference(resolution,[],[f29,f19]) ).
fof(f56,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_2,X1) ),
inference(resolution,[],[f29,f20]) ).
fof(f59,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_3,X1) ),
inference(resolution,[],[f29,f23]) ).
fof(f63,plain,
! [X0,X1] :
( ~ product1(e_2,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f30,f15]) ).
fof(f64,plain,
! [X0,X1] :
( ~ product1(e_3,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f30,f16]) ).
fof(f65,plain,
! [X0,X1] :
( ~ product1(e_4,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f30,f17]) ).
fof(f67,plain,
! [X0,X1] :
( ~ product1(e_3,X0,X1)
| ~ product1(e_2,X0,X1) ),
inference(resolution,[],[f30,f19]) ).
fof(f68,plain,
! [X0,X1] :
( ~ product1(e_4,X0,X1)
| ~ product1(e_2,X0,X1) ),
inference(resolution,[],[f30,f20]) ).
fof(f76,plain,
! [X0,X1] :
( ~ product2(X0,X1,e_2)
| ~ product2(X0,X1,e_1) ),
inference(resolution,[],[f33,f15]) ).
fof(f77,plain,
! [X0,X1] :
( ~ product2(X0,X1,e_3)
| ~ product2(X0,X1,e_1) ),
inference(resolution,[],[f33,f16]) ).
fof(f119,plain,
~ product1(e_2,e_1,e_2),
inference(resolution,[],[f51,f31]) ).
fof(f120,plain,
! [X0] :
( ~ product1(X0,e_1,e_4)
| ~ group_element(e_2)
| product1(X0,e_2,e_1)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f51,f27]) ).
fof(f122,definition,
( spl0_1
<=> group_element(e_2) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f123,plain,
( ~ group_element(e_2)
| spl0_1 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f125,definition,
( spl0_2
<=> ! [X0] :
( ~ product1(X0,e_1,e_4)
| ~ group_element(X0)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f126,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product1(X0,e_1,e_4)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f125]) ).
fof(f127,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f120,f125,f122]) ).
fof(f128,plain,
( $false
| spl0_1 ),
inference(resolution,[],[f123,f12]) ).
fof(f129,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f128]) ).
fof(f132,plain,
( ~ product1(e_3,e_1,e_4)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_1)
| ~ spl0_2 ),
inference(resolution,[],[f126,f13]) ).
fof(f148,definition,
( spl0_7
<=> product1(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f149,plain,
( product1(e_3,e_2,e_1)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f148]) ).
fof(f151,definition,
( spl0_8
<=> product1(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f152,plain,
( product1(e_3,e_2,e_2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f154,definition,
( spl0_9
<=> product1(e_3,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f155,plain,
( product1(e_3,e_2,e_3)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f157,definition,
( spl0_10
<=> product1(e_3,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f158,plain,
( ~ product1(e_3,e_1,e_4)
| spl0_10 ),
inference(avatar_component_clause,[],[f157]) ).
fof(f159,plain,
( spl0_7
| spl0_8
| spl0_9
| ~ spl0_10
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f132,f125,f157,f154,f151,f148]) ).
fof(f161,definition,
( spl0_11
<=> product1(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f162,plain,
( product1(e_1,e_2,e_1)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f164,definition,
( spl0_12
<=> product1(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f165,plain,
( product1(e_1,e_2,e_2)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f164]) ).
fof(f167,definition,
( spl0_13
<=> product1(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f168,plain,
( product1(e_1,e_2,e_3)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f175,definition,
( spl0_15
<=> group_element(e_4) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f176,plain,
( ~ group_element(e_4)
| spl0_15 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f187,definition,
( spl0_19
<=> group_element(e_1) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f188,plain,
( ~ group_element(e_1)
| spl0_19 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f192,definition,
( spl0_20
<=> group_element(e_3) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f193,plain,
( ~ group_element(e_3)
| spl0_20 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f195,definition,
( spl0_21
<=> product1(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f196,plain,
( product1(e_3,e_1,e_3)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f198,definition,
( spl0_22
<=> product1(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f199,plain,
( product1(e_3,e_1,e_2)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f201,definition,
( spl0_23
<=> product1(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f202,plain,
( product1(e_3,e_1,e_1)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f204,plain,
( $false
| spl0_15 ),
inference(resolution,[],[f176,f14]) ).
fof(f205,plain,
spl0_15,
inference(avatar_contradiction_clause,[],[f204]) ).
fof(f208,plain,
( $false
| spl0_19 ),
inference(resolution,[],[f188,f11]) ).
fof(f209,plain,
spl0_19,
inference(avatar_contradiction_clause,[],[f208]) ).
fof(f213,plain,
( $false
| spl0_20 ),
inference(resolution,[],[f193,f13]) ).
fof(f214,plain,
spl0_20,
inference(avatar_contradiction_clause,[],[f213]) ).
fof(f215,plain,
( ~ product1(e_3,e_1,e_1)
| ~ spl0_7 ),
inference(resolution,[],[f149,f51]) ).
fof(f216,plain,
~ product1(e_3,e_1,e_3),
inference(resolution,[],[f52,f31]) ).
fof(f217,plain,
! [X0] :
( ~ product1(X0,e_1,e_4)
| ~ group_element(e_3)
| product1(X0,e_3,e_1)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f52,f27]) ).
fof(f219,definition,
( spl0_24
<=> ! [X0] :
( ~ product1(X0,e_1,e_4)
| ~ group_element(X0)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f220,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product1(X0,e_1,e_4)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_1) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f221,plain,
( ~ spl0_20
| spl0_24 ),
inference(avatar_split_clause,[],[f217,f219,f192]) ).
fof(f223,plain,
( ~ product1(e_2,e_1,e_4)
| product1(e_2,e_3,e_3)
| product1(e_2,e_3,e_2)
| product1(e_2,e_3,e_1)
| ~ spl0_24 ),
inference(resolution,[],[f220,f12]) ).
fof(f237,definition,
( spl0_28
<=> product1(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f238,plain,
( product1(e_2,e_3,e_1)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f240,definition,
( spl0_29
<=> product1(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f241,plain,
( product1(e_2,e_3,e_2)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f243,definition,
( spl0_30
<=> product1(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f244,plain,
( product1(e_2,e_3,e_3)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f246,definition,
( spl0_31
<=> product1(e_2,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f247,plain,
( ~ product1(e_2,e_1,e_4)
| spl0_31 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f248,plain,
( spl0_28
| spl0_29
| spl0_30
| ~ spl0_31
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f223,f219,f246,f243,f240,f237]) ).
fof(f253,definition,
( spl0_32
<=> product1(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f254,plain,
( product1(e_2,e_1,e_3)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f256,definition,
( spl0_33
<=> product1(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f257,plain,
( product1(e_2,e_1,e_2)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f259,definition,
( spl0_34
<=> product1(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f260,plain,
( product1(e_2,e_1,e_1)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f262,plain,
( ~ product1(e_2,e_1,e_1)
| ~ spl0_28 ),
inference(resolution,[],[f238,f52]) ).
fof(f279,definition,
( spl0_36
<=> product1(e_3,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f280,plain,
( product1(e_3,e_4,e_1)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f282,definition,
( spl0_37
<=> product1(e_3,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f283,plain,
( product1(e_3,e_4,e_2)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f285,definition,
( spl0_38
<=> product1(e_3,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f286,plain,
( product1(e_3,e_4,e_3)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f289,definition,
( spl0_39
<=> product1(e_2,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f290,plain,
( product1(e_2,e_4,e_1)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f292,definition,
( spl0_40
<=> product1(e_2,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f293,plain,
( product1(e_2,e_4,e_2)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f295,definition,
( spl0_41
<=> product1(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f296,plain,
( product1(e_2,e_4,e_3)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f302,plain,
( $false
| ~ spl0_21 ),
inference(resolution,[],[f196,f216]) ).
fof(f305,plain,
~ spl0_21,
inference(avatar_contradiction_clause,[],[f302]) ).
fof(f309,plain,
~ product1(e_3,e_2,e_3),
inference(resolution,[],[f55,f31]) ).
fof(f325,definition,
( spl0_44
<=> product1(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f326,plain,
( product1(e_1,e_3,e_1)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f328,definition,
( spl0_45
<=> product1(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f329,plain,
( product1(e_1,e_3,e_2)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f331,definition,
( spl0_46
<=> product1(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f332,plain,
( product1(e_1,e_3,e_3)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f334,definition,
( spl0_47
<=> product1(e_1,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f335,plain,
( ~ product1(e_1,e_2,e_4)
| spl0_47 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f340,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_11 ),
inference(resolution,[],[f162,f51]) ).
fof(f341,plain,
( $false
| ~ spl0_11 ),
inference(resolution,[],[f340,f31]) ).
fof(f342,plain,
~ spl0_11,
inference(avatar_contradiction_clause,[],[f341]) ).
fof(f346,plain,
! [X0] :
( ~ product1(X0,e_2,e_4)
| ~ group_element(e_4)
| product1(X0,e_4,e_1)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f56,f27]) ).
fof(f348,definition,
( spl0_48
<=> ! [X0] :
( ~ product1(X0,e_2,e_4)
| ~ group_element(X0)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f349,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product1(X0,e_2,e_4)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_1) )
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f350,plain,
( ~ spl0_15
| spl0_48 ),
inference(avatar_split_clause,[],[f346,f348,f175]) ).
fof(f353,plain,
( ~ product1(e_3,e_2,e_4)
| product1(e_3,e_4,e_3)
| product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1)
| ~ spl0_48 ),
inference(resolution,[],[f349,f13]) ).
fof(f356,definition,
( spl0_49
<=> product1(e_3,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f357,plain,
( ~ product1(e_3,e_2,e_4)
| spl0_49 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f358,plain,
( spl0_36
| spl0_37
| spl0_38
| ~ spl0_49
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f353,f348,f356,f285,f282,f279]) ).
fof(f363,plain,
( ~ group_element(e_2)
| product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_3)
| ~ group_element(e_3)
| spl0_49 ),
inference(resolution,[],[f357,f27]) ).
fof(f398,definition,
( spl0_58
<=> product1(e_1,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f399,plain,
( product1(e_1,e_4,e_1)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f398]) ).
fof(f401,definition,
( spl0_59
<=> product1(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f402,plain,
( product1(e_1,e_4,e_2)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f404,definition,
( spl0_60
<=> product1(e_1,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f405,plain,
( product1(e_1,e_4,e_3)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f407,definition,
( spl0_61
<=> product1(e_1,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f408,plain,
( ~ product1(e_1,e_3,e_4)
| spl0_61 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f417,plain,
( ~ group_element(e_3)
| product1(e_1,e_3,e_1)
| product1(e_1,e_3,e_2)
| product1(e_1,e_3,e_3)
| ~ group_element(e_1)
| spl0_61 ),
inference(resolution,[],[f408,f27]) ).
fof(f418,plain,
( ~ spl0_19
| spl0_46
| spl0_45
| spl0_44
| ~ spl0_20
| spl0_61 ),
inference(avatar_split_clause,[],[f417,f407,f192,f325,f328,f331,f187]) ).
fof(f420,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_44 ),
inference(resolution,[],[f326,f52]) ).
fof(f421,plain,
( $false
| ~ spl0_44 ),
inference(resolution,[],[f420,f31]) ).
fof(f422,plain,
~ spl0_44,
inference(avatar_contradiction_clause,[],[f421]) ).
fof(f423,plain,
( ~ product1(e_1,e_2,e_2)
| ~ spl0_45 ),
inference(resolution,[],[f329,f55]) ).
fof(f426,plain,
( $false
| ~ spl0_12
| ~ spl0_45 ),
inference(resolution,[],[f423,f165]) ).
fof(f427,plain,
( ~ spl0_12
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f426]) ).
fof(f434,plain,
! [X0] :
( ~ product1(e_1,X0,e_4)
| ~ group_element(X0)
| product1(e_2,X0,e_1)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_3)
| ~ group_element(e_2) ),
inference(resolution,[],[f63,f27]) ).
fof(f436,definition,
( spl0_62
<=> ! [X0] :
( ~ product1(e_1,X0,e_4)
| product1(e_2,X0,e_3)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_1)
| ~ group_element(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f437,plain,
( ! [X0] :
( ~ group_element(X0)
| product1(e_2,X0,e_3)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_1)
| ~ product1(e_1,X0,e_4) )
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f438,plain,
( ~ spl0_1
| spl0_62 ),
inference(avatar_split_clause,[],[f434,f436,f122]) ).
fof(f441,plain,
( product1(e_2,e_3,e_3)
| product1(e_2,e_3,e_2)
| product1(e_2,e_3,e_1)
| ~ product1(e_1,e_3,e_4)
| ~ spl0_62 ),
inference(resolution,[],[f437,f13]) ).
fof(f444,definition,
( spl0_63
<=> product1(e_1,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f445,plain,
( ~ product1(e_1,e_4,e_4)
| spl0_63 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f447,plain,
( ~ group_element(e_4)
| product1(e_1,e_4,e_1)
| product1(e_1,e_4,e_2)
| product1(e_1,e_4,e_3)
| ~ group_element(e_1)
| spl0_63 ),
inference(resolution,[],[f445,f27]) ).
fof(f448,plain,
( ~ spl0_19
| spl0_60
| spl0_59
| spl0_58
| ~ spl0_15
| spl0_63 ),
inference(avatar_split_clause,[],[f447,f444,f175,f398,f401,f404,f187]) ).
fof(f451,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_58 ),
inference(resolution,[],[f399,f53]) ).
fof(f454,plain,
~ product1(e_1,e_3,e_3),
inference(resolution,[],[f64,f31]) ).
fof(f455,plain,
! [X0] :
( ~ product1(e_1,X0,e_4)
| ~ group_element(X0)
| product1(e_3,X0,e_1)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_3)
| ~ group_element(e_3) ),
inference(resolution,[],[f64,f27]) ).
fof(f457,definition,
( spl0_64
<=> ! [X0] :
( ~ product1(e_1,X0,e_4)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_1)
| ~ group_element(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f458,plain,
( ! [X0] :
( ~ group_element(X0)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_1)
| ~ product1(e_1,X0,e_4) )
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f459,plain,
( ~ spl0_20
| spl0_64 ),
inference(avatar_split_clause,[],[f455,f457,f192]) ).
fof(f461,plain,
( product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_1)
| ~ product1(e_1,e_2,e_4)
| ~ spl0_64 ),
inference(resolution,[],[f458,f12]) ).
fof(f464,plain,
( $false
| ~ spl0_58 ),
inference(resolution,[],[f451,f31]) ).
fof(f465,plain,
~ spl0_58,
inference(avatar_contradiction_clause,[],[f464]) ).
fof(f466,plain,
( ~ product1(e_1,e_3,e_2)
| ~ spl0_59 ),
inference(resolution,[],[f402,f59]) ).
fof(f467,plain,
( ~ product1(e_1,e_2,e_2)
| ~ spl0_59 ),
inference(resolution,[],[f402,f56]) ).
fof(f470,plain,
( $false
| ~ spl0_45
| ~ spl0_59 ),
inference(resolution,[],[f466,f329]) ).
fof(f471,plain,
( ~ spl0_45
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f470]) ).
fof(f480,plain,
( $false
| ~ spl0_12
| ~ spl0_59 ),
inference(resolution,[],[f467,f165]) ).
fof(f481,plain,
( ~ spl0_12
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f480]) ).
fof(f485,plain,
~ product1(e_1,e_4,e_4),
inference(resolution,[],[f65,f31]) ).
fof(f495,plain,
( $false
| ~ spl0_46 ),
inference(resolution,[],[f454,f332]) ).
fof(f496,plain,
~ spl0_46,
inference(avatar_contradiction_clause,[],[f495]) ).
fof(f502,plain,
( ~ product1(e_1,e_2,e_3)
| ~ spl0_60 ),
inference(resolution,[],[f405,f56]) ).
fof(f508,plain,
~ product1(e_2,e_3,e_3),
inference(resolution,[],[f67,f31]) ).
fof(f509,plain,
! [X0] :
( ~ product1(e_2,X0,e_4)
| ~ group_element(X0)
| product1(e_3,X0,e_1)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_3)
| ~ group_element(e_3) ),
inference(resolution,[],[f67,f27]) ).
fof(f511,definition,
( spl0_66
<=> ! [X0] :
( ~ product1(e_2,X0,e_4)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_1)
| ~ group_element(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f512,plain,
( ! [X0] :
( ~ group_element(X0)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_1)
| ~ product1(e_2,X0,e_4) )
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f513,plain,
( ~ spl0_20
| spl0_66 ),
inference(avatar_split_clause,[],[f509,f511,f192]) ).
fof(f514,plain,
( product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_1)
| ~ product1(e_2,e_1,e_4)
| ~ spl0_66 ),
inference(resolution,[],[f512,f11]) ).
fof(f519,definition,
( spl0_67
<=> product1(e_2,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f520,plain,
( ~ product1(e_2,e_4,e_4)
| spl0_67 ),
inference(avatar_component_clause,[],[f519]) ).
fof(f522,plain,
( ~ group_element(e_4)
| product1(e_2,e_4,e_1)
| product1(e_2,e_4,e_2)
| product1(e_2,e_4,e_3)
| ~ group_element(e_2)
| spl0_67 ),
inference(resolution,[],[f520,f27]) ).
fof(f523,plain,
( ~ spl0_1
| spl0_41
| spl0_40
| spl0_39
| ~ spl0_15
| spl0_67 ),
inference(avatar_split_clause,[],[f522,f519,f175,f289,f292,f295,f122]) ).
fof(f525,plain,
( ~ product1(e_2,e_3,e_1)
| ~ spl0_39 ),
inference(resolution,[],[f290,f59]) ).
fof(f527,plain,
( ~ product1(e_2,e_1,e_1)
| ~ spl0_39 ),
inference(resolution,[],[f290,f53]) ).
fof(f528,plain,
( $false
| ~ spl0_28
| ~ spl0_39 ),
inference(resolution,[],[f525,f238]) ).
fof(f529,plain,
( ~ spl0_28
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f528]) ).
fof(f532,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_29 ),
inference(resolution,[],[f241,f55]) ).
fof(f544,plain,
( $false
| ~ spl0_33 ),
inference(resolution,[],[f257,f119]) ).
fof(f547,plain,
~ spl0_33,
inference(avatar_contradiction_clause,[],[f544]) ).
fof(f551,plain,
~ product1(e_2,e_4,e_4),
inference(resolution,[],[f68,f31]) ).
fof(f561,plain,
( $false
| ~ spl0_30 ),
inference(resolution,[],[f508,f244]) ).
fof(f562,plain,
~ spl0_30,
inference(avatar_contradiction_clause,[],[f561]) ).
fof(f568,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_40 ),
inference(resolution,[],[f293,f56]) ).
fof(f578,plain,
( $false
| ~ spl0_40 ),
inference(resolution,[],[f568,f31]) ).
fof(f579,plain,
~ spl0_40,
inference(avatar_contradiction_clause,[],[f578]) ).
fof(f580,plain,
( ~ product1(e_1,e_4,e_3)
| ~ spl0_41 ),
inference(resolution,[],[f296,f63]) ).
fof(f594,plain,
( $false
| ~ spl0_41
| ~ spl0_60 ),
inference(resolution,[],[f580,f405]) ).
fof(f595,plain,
( ~ spl0_41
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f594]) ).
fof(f635,plain,
( ~ product1(e_3,e_1,e_1)
| ~ spl0_36 ),
inference(resolution,[],[f280,f53]) ).
fof(f639,plain,
( ~ product1(e_1,e_4,e_2)
| ~ spl0_37 ),
inference(resolution,[],[f283,f64]) ).
fof(f646,plain,
( $false
| ~ spl0_7
| ~ spl0_23 ),
inference(resolution,[],[f202,f215]) ).
fof(f649,plain,
( ~ spl0_7
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f646]) ).
fof(f650,plain,
! [X2,X0,X1] :
( ~ product2(X0,X1,e_1)
| ~ product1(X2,e_2,X0)
| ~ product1(e_2,X1,X2) ),
inference(resolution,[],[f76,f37]) ).
fof(f652,plain,
! [X2,X0,X1] :
( ~ product2(X0,X1,e_1)
| ~ product1(X2,e_3,X0)
| ~ product1(e_3,X1,X2) ),
inference(resolution,[],[f77,f37]) ).
fof(f655,plain,
! [X0] :
( ~ product1(X0,e_2,e_1)
| ~ product1(e_2,e_1,X0) ),
inference(resolution,[],[f650,f36]) ).
fof(f659,plain,
( ~ product1(e_2,e_1,e_3)
| ~ spl0_7 ),
inference(resolution,[],[f655,f149]) ).
fof(f660,plain,
( $false
| ~ spl0_7
| ~ spl0_32 ),
inference(resolution,[],[f659,f254]) ).
fof(f661,plain,
( ~ spl0_7
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f660]) ).
fof(f662,plain,
( $false
| ~ spl0_34
| ~ spl0_39 ),
inference(resolution,[],[f260,f527]) ).
fof(f665,plain,
( ~ spl0_34
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f662]) ).
fof(f666,plain,
( ~ spl0_61
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f441,f436,f243,f240,f237,f407]) ).
fof(f667,plain,
( ~ spl0_31
| spl0_23
| spl0_22
| spl0_21
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f514,f511,f195,f198,f201,f246]) ).
fof(f668,plain,
( ~ spl0_20
| spl0_9
| spl0_8
| spl0_7
| ~ spl0_1
| spl0_49 ),
inference(avatar_split_clause,[],[f363,f356,f122,f148,f151,f154,f192]) ).
fof(f669,plain,
( ~ spl0_47
| spl0_7
| spl0_8
| spl0_9
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f461,f457,f154,f151,f148,f334]) ).
fof(f670,plain,
( $false
| ~ spl0_9 ),
inference(resolution,[],[f155,f309]) ).
fof(f676,plain,
~ spl0_9,
inference(avatar_contradiction_clause,[],[f670]) ).
fof(f678,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_8 ),
inference(resolution,[],[f152,f67]) ).
fof(f689,plain,
( ~ product1(e_2,e_4,e_3)
| ~ spl0_38 ),
inference(resolution,[],[f286,f67]) ).
fof(f699,plain,
( $false
| ~ spl0_29 ),
inference(resolution,[],[f532,f31]) ).
fof(f700,plain,
~ spl0_29,
inference(avatar_contradiction_clause,[],[f699]) ).
fof(f710,plain,
( $false
| ~ spl0_8 ),
inference(resolution,[],[f678,f31]) ).
fof(f711,plain,
~ spl0_8,
inference(avatar_contradiction_clause,[],[f710]) ).
fof(f712,plain,
( ~ group_element(e_1)
| product1(e_3,e_1,e_1)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| ~ group_element(e_3)
| spl0_10 ),
inference(resolution,[],[f158,f27]) ).
fof(f727,plain,
! [X0] :
( ~ product1(X0,e_3,e_1)
| ~ product1(e_3,e_1,X0) ),
inference(resolution,[],[f652,f36]) ).
fof(f728,plain,
( ~ group_element(e_2)
| product1(e_1,e_2,e_1)
| product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| ~ group_element(e_1)
| spl0_47 ),
inference(resolution,[],[f335,f27]) ).
fof(f736,plain,
( $false
| ~ spl0_13
| ~ spl0_60 ),
inference(resolution,[],[f502,f168]) ).
fof(f737,plain,
( ~ spl0_13
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f736]) ).
fof(f738,plain,
~ spl0_67,
inference(avatar_split_clause,[],[f551,f519]) ).
fof(f741,plain,
( ~ spl0_19
| spl0_13
| spl0_12
| spl0_11
| ~ spl0_1
| spl0_47 ),
inference(avatar_split_clause,[],[f728,f334,f122,f161,f164,f167,f187]) ).
fof(f742,plain,
~ spl0_63,
inference(avatar_split_clause,[],[f485,f444]) ).
fof(f773,plain,
( $false
| ~ spl0_38
| ~ spl0_41 ),
inference(resolution,[],[f689,f296]) ).
fof(f774,plain,
( ~ spl0_38
| ~ spl0_41 ),
inference(avatar_contradiction_clause,[],[f773]) ).
fof(f781,plain,
( $false
| ~ spl0_23
| ~ spl0_36 ),
inference(resolution,[],[f635,f202]) ).
fof(f782,plain,
( ~ spl0_23
| ~ spl0_36 ),
inference(avatar_contradiction_clause,[],[f781]) ).
fof(f789,plain,
( $false
| ~ spl0_37
| ~ spl0_59 ),
inference(resolution,[],[f639,f402]) ).
fof(f790,plain,
( ~ spl0_37
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f789]) ).
fof(f791,plain,
( ~ spl0_20
| spl0_21
| spl0_22
| spl0_23
| ~ spl0_19
| spl0_10 ),
inference(avatar_split_clause,[],[f712,f157,f187,f201,f198,f195,f192]) ).
fof(f797,plain,
( ~ product1(e_2,e_3,e_1)
| ~ spl0_22 ),
inference(resolution,[],[f199,f727]) ).
fof(f801,plain,
( $false
| ~ spl0_22
| ~ spl0_28 ),
inference(resolution,[],[f797,f238]) ).
fof(f802,plain,
( ~ spl0_22
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f801]) ).
fof(f807,plain,
( ~ group_element(e_1)
| product1(e_2,e_1,e_1)
| product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| ~ group_element(e_2)
| spl0_31 ),
inference(resolution,[],[f247,f27]) ).
fof(f808,plain,
( ~ spl0_1
| spl0_32
| spl0_33
| spl0_34
| ~ spl0_19
| spl0_31 ),
inference(avatar_split_clause,[],[f807,f246,f187,f259,f256,f253,f122]) ).
fof(f809,plain,
( $false
| ~ spl0_28
| ~ spl0_34 ),
inference(resolution,[],[f260,f262]) ).
fof(f812,plain,
( ~ spl0_28
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f809]) ).
cnf(s1,plain,
( ~ spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f127]) ).
cnf(s2,plain,
spl0_1,
inference(sat_conversion,[],[f129]) ).
cnf(s4,plain,
( ~ spl0_2
| spl0_7
| spl0_8
| spl0_9
| ~ spl0_10 ),
inference(sat_conversion,[],[f159]) ).
cnf(s8,plain,
spl0_15,
inference(sat_conversion,[],[f205]) ).
cnf(s9,plain,
spl0_19,
inference(sat_conversion,[],[f209]) ).
cnf(s10,plain,
spl0_20,
inference(sat_conversion,[],[f214]) ).
cnf(s11,plain,
( ~ spl0_20
| spl0_24 ),
inference(sat_conversion,[],[f221]) ).
cnf(s13,plain,
( ~ spl0_24
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_31 ),
inference(sat_conversion,[],[f248]) ).
cnf(s22,plain,
~ spl0_21,
inference(sat_conversion,[],[f305]) ).
cnf(s27,plain,
~ spl0_11,
inference(sat_conversion,[],[f342]) ).
cnf(s28,plain,
( ~ spl0_15
| spl0_48 ),
inference(sat_conversion,[],[f350]) ).
cnf(s29,plain,
( spl0_36
| spl0_37
| spl0_38
| ~ spl0_48
| ~ spl0_49 ),
inference(sat_conversion,[],[f358]) ).
cnf(s37,plain,
( ~ spl0_19
| ~ spl0_20
| spl0_44
| spl0_45
| spl0_46
| spl0_61 ),
inference(sat_conversion,[],[f418]) ).
cnf(s38,plain,
~ spl0_44,
inference(sat_conversion,[],[f422]) ).
cnf(s39,plain,
( ~ spl0_12
| ~ spl0_45 ),
inference(sat_conversion,[],[f427]) ).
cnf(s40,plain,
( ~ spl0_1
| spl0_62 ),
inference(sat_conversion,[],[f438]) ).
cnf(s42,plain,
( ~ spl0_15
| ~ spl0_19
| spl0_58
| spl0_59
| spl0_60
| spl0_63 ),
inference(sat_conversion,[],[f448]) ).
cnf(s43,plain,
( ~ spl0_20
| spl0_64 ),
inference(sat_conversion,[],[f459]) ).
cnf(s44,plain,
~ spl0_58,
inference(sat_conversion,[],[f465]) ).
cnf(s45,plain,
( ~ spl0_45
| ~ spl0_59 ),
inference(sat_conversion,[],[f471]) ).
cnf(s47,plain,
( ~ spl0_12
| ~ spl0_59 ),
inference(sat_conversion,[],[f481]) ).
cnf(s49,plain,
~ spl0_46,
inference(sat_conversion,[],[f496]) ).
cnf(s51,plain,
( ~ spl0_20
| spl0_66 ),
inference(sat_conversion,[],[f513]) ).
cnf(s53,plain,
( ~ spl0_1
| ~ spl0_15
| spl0_39
| spl0_40
| spl0_41
| spl0_67 ),
inference(sat_conversion,[],[f523]) ).
cnf(s54,plain,
( ~ spl0_28
| ~ spl0_39 ),
inference(sat_conversion,[],[f529]) ).
cnf(s58,plain,
~ spl0_33,
inference(sat_conversion,[],[f547]) ).
cnf(s60,plain,
~ spl0_30,
inference(sat_conversion,[],[f562]) ).
cnf(s62,plain,
~ spl0_40,
inference(sat_conversion,[],[f579]) ).
cnf(s64,plain,
( ~ spl0_41
| ~ spl0_60 ),
inference(sat_conversion,[],[f595]) ).
cnf(s73,plain,
( ~ spl0_7
| ~ spl0_23 ),
inference(sat_conversion,[],[f649]) ).
cnf(s74,plain,
( ~ spl0_7
| ~ spl0_32 ),
inference(sat_conversion,[],[f661]) ).
cnf(s75,plain,
( ~ spl0_34
| ~ spl0_39 ),
inference(sat_conversion,[],[f665]) ).
cnf(s76,plain,
( spl0_28
| spl0_29
| spl0_30
| ~ spl0_61
| ~ spl0_62 ),
inference(sat_conversion,[],[f666]) ).
cnf(s77,plain,
( spl0_21
| spl0_22
| spl0_23
| ~ spl0_31
| ~ spl0_66 ),
inference(sat_conversion,[],[f667]) ).
cnf(s78,plain,
( ~ spl0_1
| spl0_7
| spl0_8
| spl0_9
| ~ spl0_20
| spl0_49 ),
inference(sat_conversion,[],[f668]) ).
cnf(s79,plain,
( spl0_7
| spl0_8
| spl0_9
| ~ spl0_47
| ~ spl0_64 ),
inference(sat_conversion,[],[f669]) ).
cnf(s80,plain,
~ spl0_9,
inference(sat_conversion,[],[f676]) ).
cnf(s82,plain,
~ spl0_29,
inference(sat_conversion,[],[f700]) ).
cnf(s84,plain,
~ spl0_8,
inference(sat_conversion,[],[f711]) ).
cnf(s90,plain,
( ~ spl0_13
| ~ spl0_60 ),
inference(sat_conversion,[],[f737]) ).
cnf(s91,plain,
~ spl0_67,
inference(sat_conversion,[],[f738]) ).
cnf(s94,plain,
( ~ spl0_1
| spl0_11
| spl0_12
| spl0_13
| ~ spl0_19
| spl0_47 ),
inference(sat_conversion,[],[f741]) ).
cnf(s95,plain,
~ spl0_63,
inference(sat_conversion,[],[f742]) ).
cnf(s98,plain,
( ~ spl0_38
| ~ spl0_41 ),
inference(sat_conversion,[],[f774]) ).
cnf(s99,plain,
( ~ spl0_23
| ~ spl0_36 ),
inference(sat_conversion,[],[f782]) ).
cnf(s100,plain,
( ~ spl0_37
| ~ spl0_59 ),
inference(sat_conversion,[],[f790]) ).
cnf(s101,plain,
( spl0_10
| ~ spl0_19
| ~ spl0_20
| spl0_21
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f791]) ).
cnf(s102,plain,
( ~ spl0_22
| ~ spl0_28 ),
inference(sat_conversion,[],[f802]) ).
cnf(s103,plain,
( ~ spl0_1
| ~ spl0_19
| spl0_31
| spl0_32
| spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f808]) ).
cnf(s104,plain,
( ~ spl0_28
| ~ spl0_34 ),
inference(sat_conversion,[],[f812]) ).
cnf(s105,plain,
( spl0_7
| ~ spl0_47
| ~ spl0_64 ),
inference(rat,[],[s79,s80,s84]) ).
cnf(s106,plain,
( ~ spl0_1
| spl0_7
| ~ spl0_20
| spl0_49 ),
inference(rat,[],[s78,s80,s84]) ).
cnf(s107,plain,
( spl0_28
| spl0_30
| ~ spl0_61
| ~ spl0_62 ),
inference(rat,[],[s76,s82]) ).
cnf(s109,plain,
( ~ spl0_1
| ~ spl0_15
| spl0_39
| spl0_41 ),
inference(rat,[],[s53,s91,s62]) ).
cnf(s110,plain,
( ~ spl0_15
| ~ spl0_19
| spl0_59
| spl0_60 ),
inference(rat,[],[s42,s95,s44]) ).
cnf(s111,plain,
( ~ spl0_19
| ~ spl0_20
| spl0_45
| spl0_61 ),
inference(rat,[],[s37,s49,s38]) ).
cnf(s121,plain,
( ~ spl0_24
| spl0_28
| ~ spl0_31 ),
inference(rat,[],[s13,s60,s82]) ).
cnf(s122,plain,
spl0_66,
inference(rat,[],[s51,s10]) ).
cnf(s123,plain,
spl0_64,
inference(rat,[],[s43,s10]) ).
cnf(s125,plain,
spl0_24,
inference(rat,[],[s11,s10]) ).
cnf(s130,plain,
spl0_48,
inference(rat,[],[s28,s8]) ).
cnf(s135,plain,
( ~ spl0_2
| spl0_7
| ~ spl0_10 ),
inference(rat,[],[s4,s80,s84]) ).
cnf(s136,plain,
spl0_62,
inference(rat,[],[s40,s2]) ).
cnf(s137,plain,
spl0_2,
inference(rat,[],[s1,s2]) ).
cnf(s138,plain,
( spl0_28
| spl0_32 ),
inference(rat,[],[s64,s109,s110,s75,s45,s103,s111,s121,s107,s8,s2,s9,s58,s10,s125,s60,s136]) ).
cnf(s139,plain,
~ spl0_7,
inference(rat,[],[s77,s103,s102,s104,s138,s73,s74,s22,s122,s9,s2,s58]) ).
cnf(s140,plain,
~ spl0_47,
inference(rat,[],[s105,s123,s139]) ).
cnf(s141,plain,
spl0_49,
inference(rat,[],[s106,s2,s10,s139]) ).
cnf(s142,plain,
~ spl0_10,
inference(rat,[],[s135,s137,s139]) ).
cnf(s143,plain,
~ spl0_12,
inference(rat,[],[s54,s109,s107,s64,s111,s110,s39,s47,s8,s2,s60,s136,s10,s9]) ).
cnf(s144,plain,
spl0_13,
inference(rat,[],[s94,s140,s9,s2,s27,s143]) ).
cnf(s145,plain,
~ spl0_60,
inference(rat,[],[s90,s144]) ).
cnf(s147,plain,
spl0_59,
inference(rat,[],[s110,s8,s9,s145]) ).
cnf(s148,plain,
~ spl0_37,
inference(rat,[],[s100,s147]) ).
cnf(s149,plain,
~ spl0_45,
inference(rat,[],[s45,s147]) ).
cnf(s150,plain,
spl0_61,
inference(rat,[],[s111,s9,s10,s149]) ).
cnf(s151,plain,
spl0_28,
inference(rat,[],[s107,s136,s60,s150]) ).
cnf(s153,plain,
~ spl0_22,
inference(rat,[],[s102,s151]) ).
cnf(s155,plain,
~ spl0_39,
inference(rat,[],[s54,s151]) ).
cnf(s156,plain,
spl0_23,
inference(rat,[],[s101,s142,s9,s22,s10,s153]) ).
cnf(s157,plain,
spl0_41,
inference(rat,[],[s109,s2,s8,s155]) ).
cnf(s158,plain,
~ spl0_36,
inference(rat,[],[s99,s156]) ).
cnf(s159,plain,
~ spl0_38,
inference(rat,[],[s98,s157]) ).
cnf(s162,plain,
$false,
inference(rat,[],[s29,s141,s130,s148,s159,s158]) ).
fof(f813,plain,
$false,
inference(avatar_sat_refutation,[],[s162]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP124-7.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n009.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 09:21:29 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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.75/1.32 % (1766265)Input is clausal, will run a generic CNF schedule.
% 2.75/1.32 % (1766270)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=1720984445:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.75/1.32 % (1766274)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=684472976:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.75/1.32 % (1766276)dis-21_1_sil=8000:lcm=predicate:random_seed=4044471804: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.75/1.32 % (1766271)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2059935462:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.75/1.32 % (1766272)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2375593183:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.75/1.32 % (1766273)lrs+10_1_sil=8000:sp=occurrence:random_seed=4083435742:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.75/1.32 % (1766275)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=667917529:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.75/1.32 % (1766276)First to succeed.
% 2.75/1.32 % (1766276)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1766265"
% 2.75/1.32 % (1766275)Also succeeded, but the first one will report.
% 2.75/1.32 % (1766273)Instruction limit reached!
% 2.75/1.32 % (1766273)------------------------------
% 2.75/1.32 % (1766273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.75/1.32 % (1766273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.75/1.32 % (1766273)CaDiCaL version: 2.1.3
% 2.75/1.32 % (1766273)Termination reason: Instruction limit
% 2.75/1.32 % (1766273)Termination phase: Saturation
% 2.75/1.32 % (1766273)Time elapsed: 0.060 s
% 2.75/1.32 % (1766273)Peak memory usage: 88 MB
% 2.75/1.32 % (1766273)Instructions burned: 107 (million)
% 2.75/1.32 % (1766274)Instruction limit reached!
% 2.75/1.32 % (1766274)------------------------------
% 2.75/1.32 % (1766274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.75/1.32 % (1766274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.75/1.32 % (1766274)CaDiCaL version: 2.1.3
% 2.75/1.32 % (1766274)Termination reason: Instruction limit
% 2.75/1.32 % (1766274)Termination phase: Saturation
% 2.75/1.32 % (1766274)Time elapsed: 0.061 s
% 2.75/1.32 % (1766274)Peak memory usage: 88 MB
% 2.75/1.32 % (1766274)Instructions burned: 115 (million)
% 2.75/1.32 % (1766284)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=4248653541:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 2.75/1.32 % (1766285)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2744772625: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)
% 2.75/1.32 % (1766285)Refutation not found, incomplete strategy
% 2.75/1.32 % (1766285)------------------------------
% 2.75/1.32 % (1766285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.75/1.32 % (1766285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.75/1.32 % (1766285)CaDiCaL version: 2.1.3
% 2.75/1.32 % (1766285)Termination reason: Refutation not found, incomplete strategy
% 2.75/1.32 % (1766285)Time elapsed: 0.002 s
% 2.75/1.32 % (1766285)Peak memory usage: 87 MB
% 2.75/1.32 % (1766285)Instructions burned: 1 (million)
% 2.75/1.32 % (1766276)Refutation found. Thanks to Tanya!
% 2.75/1.32 % SZS status Unsatisfiable for theBenchmark
% 2.75/1.32 % SZS output start Proof for theBenchmark
% See solution above
% 3.76/1.42 % (1766276)------------------------------
% 3.76/1.42 % (1766276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.42 % (1766276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.42 % (1766276)CaDiCaL version: 2.1.3
% 3.76/1.42 % (1766276)Termination reason: Refutation
% 3.76/1.42 % (1766276)Time elapsed: 0.016 s
% 3.76/1.42 % (1766276)Peak memory usage: 89 MB
% 3.76/1.42 % (1766276)Instructions burned: 22 (million)
% 3.76/1.42 % (1766276)------------------------------
% 3.76/1.42 % (1766276)------------------------------
% 3.76/1.42 % (1766265)Success in time 0.46 s
% 3.76/1.42 % Vampire exiting
%------------------------------------------------------------------------------