%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP124-6.004 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 3.05s 1.33s
% Output : Refutation 3.78s
% 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(f1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
fof(f2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
fof(f3,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
fof(f4,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
fof(f5,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f6,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f7,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f9,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f10,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f13,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f17,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/sandbox2/benchmark/theBenchmark.p',product1_total_function1) ).
fof(f19,axiom,
! [X2,X3,X0,X1] :
( equalish(X1,X3)
| ~ product1(X0,X3,X2)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product1_right_cancellation) ).
fof(f20,axiom,
! [X2,X3,X0,X1] :
( equalish(X0,X3)
| ~ product1(X3,X1,X2)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product1_left_cancellation) ).
fof(f21,axiom,
! [X0] : product1(X0,X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product1_idempotence) ).
fof(f23,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ product2(X0,X1,X3)
| ~ product2(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product2_total_function2) ).
fof(f26,axiom,
! [X0] : product2(X0,X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product2_idempotence) ).
fof(f27,negated_conjecture,
! [X2,X3,X0,X1] :
( product2(X3,X1,X0)
| ~ product1(X2,X0,X3)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg2a) ).
fof(f41,plain,
! [X0,X1] :
( ~ product1(X0,e_2,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f19,f5]) ).
fof(f42,plain,
! [X0,X1] :
( ~ product1(X0,e_3,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f19,f6]) ).
fof(f43,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f19,f7]) ).
fof(f45,plain,
! [X0,X1] :
( ~ product1(X0,e_3,X1)
| ~ product1(X0,e_2,X1) ),
inference(resolution,[],[f19,f9]) ).
fof(f46,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_2,X1) ),
inference(resolution,[],[f19,f10]) ).
fof(f49,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_3,X1) ),
inference(resolution,[],[f19,f13]) ).
fof(f53,plain,
! [X0,X1] :
( ~ product1(e_2,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f20,f5]) ).
fof(f54,plain,
! [X0,X1] :
( ~ product1(e_3,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f20,f6]) ).
fof(f55,plain,
! [X0,X1] :
( ~ product1(e_4,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f20,f7]) ).
fof(f57,plain,
! [X0,X1] :
( ~ product1(e_3,X0,X1)
| ~ product1(e_2,X0,X1) ),
inference(resolution,[],[f20,f9]) ).
fof(f58,plain,
! [X0,X1] :
( ~ product1(e_4,X0,X1)
| ~ product1(e_2,X0,X1) ),
inference(resolution,[],[f20,f10]) ).
fof(f66,plain,
! [X0,X1] :
( ~ product2(X0,X1,e_2)
| ~ product2(X0,X1,e_1) ),
inference(resolution,[],[f23,f5]) ).
fof(f67,plain,
! [X0,X1] :
( ~ product2(X0,X1,e_3)
| ~ product2(X0,X1,e_1) ),
inference(resolution,[],[f23,f6]) ).
fof(f109,plain,
~ product1(e_2,e_1,e_2),
inference(resolution,[],[f41,f21]) ).
fof(f110,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,[],[f41,f17]) ).
fof(f112,definition,
( spl0_1
<=> group_element(e_2) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f113,plain,
( ~ group_element(e_2)
| spl0_1 ),
inference(avatar_component_clause,[],[f112]) ).
fof(f115,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(f116,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,[],[f115]) ).
fof(f117,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f110,f115,f112]) ).
fof(f118,plain,
( $false
| spl0_1 ),
inference(resolution,[],[f113,f2]) ).
fof(f119,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f118]) ).
fof(f122,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,[],[f116,f3]) ).
fof(f138,definition,
( spl0_7
<=> product1(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f139,plain,
( product1(e_3,e_2,e_1)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f138]) ).
fof(f141,definition,
( spl0_8
<=> product1(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f142,plain,
( product1(e_3,e_2,e_2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f141]) ).
fof(f144,definition,
( spl0_9
<=> product1(e_3,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f145,plain,
( product1(e_3,e_2,e_3)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f147,definition,
( spl0_10
<=> product1(e_3,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f148,plain,
( ~ product1(e_3,e_1,e_4)
| spl0_10 ),
inference(avatar_component_clause,[],[f147]) ).
fof(f149,plain,
( spl0_7
| spl0_8
| spl0_9
| ~ spl0_10
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f122,f115,f147,f144,f141,f138]) ).
fof(f151,definition,
( spl0_11
<=> product1(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f152,plain,
( product1(e_1,e_2,e_1)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f154,definition,
( spl0_12
<=> product1(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f155,plain,
( product1(e_1,e_2,e_2)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f157,definition,
( spl0_13
<=> product1(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f158,plain,
( product1(e_1,e_2,e_3)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f157]) ).
fof(f165,definition,
( spl0_15
<=> group_element(e_4) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f166,plain,
( ~ group_element(e_4)
| spl0_15 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f177,definition,
( spl0_19
<=> group_element(e_1) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f178,plain,
( ~ group_element(e_1)
| spl0_19 ),
inference(avatar_component_clause,[],[f177]) ).
fof(f182,definition,
( spl0_20
<=> group_element(e_3) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f183,plain,
( ~ group_element(e_3)
| spl0_20 ),
inference(avatar_component_clause,[],[f182]) ).
fof(f185,definition,
( spl0_21
<=> product1(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f186,plain,
( product1(e_3,e_1,e_3)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f185]) ).
fof(f188,definition,
( spl0_22
<=> product1(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f189,plain,
( product1(e_3,e_1,e_2)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f191,definition,
( spl0_23
<=> product1(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f192,plain,
( product1(e_3,e_1,e_1)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f194,plain,
( $false
| spl0_15 ),
inference(resolution,[],[f166,f4]) ).
fof(f195,plain,
spl0_15,
inference(avatar_contradiction_clause,[],[f194]) ).
fof(f198,plain,
( $false
| spl0_19 ),
inference(resolution,[],[f178,f1]) ).
fof(f199,plain,
spl0_19,
inference(avatar_contradiction_clause,[],[f198]) ).
fof(f203,plain,
( $false
| spl0_20 ),
inference(resolution,[],[f183,f3]) ).
fof(f204,plain,
spl0_20,
inference(avatar_contradiction_clause,[],[f203]) ).
fof(f205,plain,
( ~ product1(e_3,e_1,e_1)
| ~ spl0_7 ),
inference(resolution,[],[f139,f41]) ).
fof(f206,plain,
~ product1(e_3,e_1,e_3),
inference(resolution,[],[f42,f21]) ).
fof(f207,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,[],[f42,f17]) ).
fof(f209,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(f210,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,[],[f209]) ).
fof(f211,plain,
( ~ spl0_20
| spl0_24 ),
inference(avatar_split_clause,[],[f207,f209,f182]) ).
fof(f213,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,[],[f210,f2]) ).
fof(f227,definition,
( spl0_28
<=> product1(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f228,plain,
( product1(e_2,e_3,e_1)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f227]) ).
fof(f230,definition,
( spl0_29
<=> product1(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f231,plain,
( product1(e_2,e_3,e_2)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f233,definition,
( spl0_30
<=> product1(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f234,plain,
( product1(e_2,e_3,e_3)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f236,definition,
( spl0_31
<=> product1(e_2,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f237,plain,
( ~ product1(e_2,e_1,e_4)
| spl0_31 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f238,plain,
( spl0_28
| spl0_29
| spl0_30
| ~ spl0_31
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f213,f209,f236,f233,f230,f227]) ).
fof(f243,definition,
( spl0_32
<=> product1(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f244,plain,
( product1(e_2,e_1,e_3)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f246,definition,
( spl0_33
<=> product1(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f247,plain,
( product1(e_2,e_1,e_2)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f249,definition,
( spl0_34
<=> product1(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f250,plain,
( product1(e_2,e_1,e_1)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f252,plain,
( ~ product1(e_2,e_1,e_1)
| ~ spl0_28 ),
inference(resolution,[],[f228,f42]) ).
fof(f269,definition,
( spl0_36
<=> product1(e_3,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f270,plain,
( product1(e_3,e_4,e_1)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f272,definition,
( spl0_37
<=> product1(e_3,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f273,plain,
( product1(e_3,e_4,e_2)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f275,definition,
( spl0_38
<=> product1(e_3,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f276,plain,
( product1(e_3,e_4,e_3)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f279,definition,
( spl0_39
<=> product1(e_2,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f280,plain,
( product1(e_2,e_4,e_1)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f282,definition,
( spl0_40
<=> product1(e_2,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f283,plain,
( product1(e_2,e_4,e_2)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f285,definition,
( spl0_41
<=> product1(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f286,plain,
( product1(e_2,e_4,e_3)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f292,plain,
( $false
| ~ spl0_21 ),
inference(resolution,[],[f186,f206]) ).
fof(f295,plain,
~ spl0_21,
inference(avatar_contradiction_clause,[],[f292]) ).
fof(f299,plain,
~ product1(e_3,e_2,e_3),
inference(resolution,[],[f45,f21]) ).
fof(f315,definition,
( spl0_44
<=> product1(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f316,plain,
( product1(e_1,e_3,e_1)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f318,definition,
( spl0_45
<=> product1(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f319,plain,
( product1(e_1,e_3,e_2)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f321,definition,
( spl0_46
<=> product1(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f322,plain,
( product1(e_1,e_3,e_3)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f324,definition,
( spl0_47
<=> product1(e_1,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f325,plain,
( ~ product1(e_1,e_2,e_4)
| spl0_47 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f330,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_11 ),
inference(resolution,[],[f152,f41]) ).
fof(f331,plain,
( $false
| ~ spl0_11 ),
inference(resolution,[],[f330,f21]) ).
fof(f332,plain,
~ spl0_11,
inference(avatar_contradiction_clause,[],[f331]) ).
fof(f336,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,[],[f46,f17]) ).
fof(f338,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(f339,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,[],[f338]) ).
fof(f340,plain,
( ~ spl0_15
| spl0_48 ),
inference(avatar_split_clause,[],[f336,f338,f165]) ).
fof(f343,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,[],[f339,f3]) ).
fof(f346,definition,
( spl0_49
<=> product1(e_3,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f347,plain,
( ~ product1(e_3,e_2,e_4)
| spl0_49 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f348,plain,
( spl0_36
| spl0_37
| spl0_38
| ~ spl0_49
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f343,f338,f346,f275,f272,f269]) ).
fof(f353,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,[],[f347,f17]) ).
fof(f388,definition,
( spl0_58
<=> product1(e_1,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f389,plain,
( product1(e_1,e_4,e_1)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f391,definition,
( spl0_59
<=> product1(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f392,plain,
( product1(e_1,e_4,e_2)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f391]) ).
fof(f394,definition,
( spl0_60
<=> product1(e_1,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f395,plain,
( product1(e_1,e_4,e_3)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f397,definition,
( spl0_61
<=> product1(e_1,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f398,plain,
( ~ product1(e_1,e_3,e_4)
| spl0_61 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f407,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,[],[f398,f17]) ).
fof(f408,plain,
( ~ spl0_19
| spl0_46
| spl0_45
| spl0_44
| ~ spl0_20
| spl0_61 ),
inference(avatar_split_clause,[],[f407,f397,f182,f315,f318,f321,f177]) ).
fof(f410,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_44 ),
inference(resolution,[],[f316,f42]) ).
fof(f411,plain,
( $false
| ~ spl0_44 ),
inference(resolution,[],[f410,f21]) ).
fof(f412,plain,
~ spl0_44,
inference(avatar_contradiction_clause,[],[f411]) ).
fof(f413,plain,
( ~ product1(e_1,e_2,e_2)
| ~ spl0_45 ),
inference(resolution,[],[f319,f45]) ).
fof(f416,plain,
( $false
| ~ spl0_12
| ~ spl0_45 ),
inference(resolution,[],[f413,f155]) ).
fof(f417,plain,
( ~ spl0_12
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f416]) ).
fof(f424,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,[],[f53,f17]) ).
fof(f426,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(f427,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,[],[f426]) ).
fof(f428,plain,
( ~ spl0_1
| spl0_62 ),
inference(avatar_split_clause,[],[f424,f426,f112]) ).
fof(f431,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,[],[f427,f3]) ).
fof(f434,definition,
( spl0_63
<=> product1(e_1,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f435,plain,
( ~ product1(e_1,e_4,e_4)
| spl0_63 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f437,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,[],[f435,f17]) ).
fof(f438,plain,
( ~ spl0_19
| spl0_60
| spl0_59
| spl0_58
| ~ spl0_15
| spl0_63 ),
inference(avatar_split_clause,[],[f437,f434,f165,f388,f391,f394,f177]) ).
fof(f441,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_58 ),
inference(resolution,[],[f389,f43]) ).
fof(f444,plain,
~ product1(e_1,e_3,e_3),
inference(resolution,[],[f54,f21]) ).
fof(f445,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,[],[f54,f17]) ).
fof(f447,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(f448,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,[],[f447]) ).
fof(f449,plain,
( ~ spl0_20
| spl0_64 ),
inference(avatar_split_clause,[],[f445,f447,f182]) ).
fof(f451,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,[],[f448,f2]) ).
fof(f454,plain,
( $false
| ~ spl0_58 ),
inference(resolution,[],[f441,f21]) ).
fof(f455,plain,
~ spl0_58,
inference(avatar_contradiction_clause,[],[f454]) ).
fof(f456,plain,
( ~ product1(e_1,e_3,e_2)
| ~ spl0_59 ),
inference(resolution,[],[f392,f49]) ).
fof(f457,plain,
( ~ product1(e_1,e_2,e_2)
| ~ spl0_59 ),
inference(resolution,[],[f392,f46]) ).
fof(f460,plain,
( $false
| ~ spl0_45
| ~ spl0_59 ),
inference(resolution,[],[f456,f319]) ).
fof(f461,plain,
( ~ spl0_45
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f460]) ).
fof(f470,plain,
( $false
| ~ spl0_12
| ~ spl0_59 ),
inference(resolution,[],[f457,f155]) ).
fof(f471,plain,
( ~ spl0_12
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f470]) ).
fof(f475,plain,
~ product1(e_1,e_4,e_4),
inference(resolution,[],[f55,f21]) ).
fof(f485,plain,
( $false
| ~ spl0_46 ),
inference(resolution,[],[f444,f322]) ).
fof(f486,plain,
~ spl0_46,
inference(avatar_contradiction_clause,[],[f485]) ).
fof(f492,plain,
( ~ product1(e_1,e_2,e_3)
| ~ spl0_60 ),
inference(resolution,[],[f395,f46]) ).
fof(f498,plain,
~ product1(e_2,e_3,e_3),
inference(resolution,[],[f57,f21]) ).
fof(f499,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,[],[f57,f17]) ).
fof(f501,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(f502,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,[],[f501]) ).
fof(f503,plain,
( ~ spl0_20
| spl0_66 ),
inference(avatar_split_clause,[],[f499,f501,f182]) ).
fof(f504,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,[],[f502,f1]) ).
fof(f509,definition,
( spl0_67
<=> product1(e_2,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f510,plain,
( ~ product1(e_2,e_4,e_4)
| spl0_67 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f512,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,[],[f510,f17]) ).
fof(f513,plain,
( ~ spl0_1
| spl0_41
| spl0_40
| spl0_39
| ~ spl0_15
| spl0_67 ),
inference(avatar_split_clause,[],[f512,f509,f165,f279,f282,f285,f112]) ).
fof(f515,plain,
( ~ product1(e_2,e_3,e_1)
| ~ spl0_39 ),
inference(resolution,[],[f280,f49]) ).
fof(f517,plain,
( ~ product1(e_2,e_1,e_1)
| ~ spl0_39 ),
inference(resolution,[],[f280,f43]) ).
fof(f518,plain,
( $false
| ~ spl0_28
| ~ spl0_39 ),
inference(resolution,[],[f515,f228]) ).
fof(f519,plain,
( ~ spl0_28
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f518]) ).
fof(f522,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_29 ),
inference(resolution,[],[f231,f45]) ).
fof(f534,plain,
( $false
| ~ spl0_33 ),
inference(resolution,[],[f247,f109]) ).
fof(f537,plain,
~ spl0_33,
inference(avatar_contradiction_clause,[],[f534]) ).
fof(f541,plain,
~ product1(e_2,e_4,e_4),
inference(resolution,[],[f58,f21]) ).
fof(f551,plain,
( $false
| ~ spl0_30 ),
inference(resolution,[],[f498,f234]) ).
fof(f552,plain,
~ spl0_30,
inference(avatar_contradiction_clause,[],[f551]) ).
fof(f558,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_40 ),
inference(resolution,[],[f283,f46]) ).
fof(f568,plain,
( $false
| ~ spl0_40 ),
inference(resolution,[],[f558,f21]) ).
fof(f569,plain,
~ spl0_40,
inference(avatar_contradiction_clause,[],[f568]) ).
fof(f570,plain,
( ~ product1(e_1,e_4,e_3)
| ~ spl0_41 ),
inference(resolution,[],[f286,f53]) ).
fof(f584,plain,
( $false
| ~ spl0_41
| ~ spl0_60 ),
inference(resolution,[],[f570,f395]) ).
fof(f585,plain,
( ~ spl0_41
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f584]) ).
fof(f625,plain,
( ~ product1(e_3,e_1,e_1)
| ~ spl0_36 ),
inference(resolution,[],[f270,f43]) ).
fof(f629,plain,
( ~ product1(e_1,e_4,e_2)
| ~ spl0_37 ),
inference(resolution,[],[f273,f54]) ).
fof(f636,plain,
( $false
| ~ spl0_7
| ~ spl0_23 ),
inference(resolution,[],[f192,f205]) ).
fof(f639,plain,
( ~ spl0_7
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f636]) ).
fof(f640,plain,
! [X2,X0,X1] :
( ~ product2(X0,X1,e_1)
| ~ product1(X2,e_2,X0)
| ~ product1(e_2,X1,X2) ),
inference(resolution,[],[f66,f27]) ).
fof(f642,plain,
! [X2,X0,X1] :
( ~ product2(X0,X1,e_1)
| ~ product1(X2,e_3,X0)
| ~ product1(e_3,X1,X2) ),
inference(resolution,[],[f67,f27]) ).
fof(f645,plain,
! [X0] :
( ~ product1(X0,e_2,e_1)
| ~ product1(e_2,e_1,X0) ),
inference(resolution,[],[f640,f26]) ).
fof(f649,plain,
( ~ product1(e_2,e_1,e_3)
| ~ spl0_7 ),
inference(resolution,[],[f645,f139]) ).
fof(f650,plain,
( $false
| ~ spl0_7
| ~ spl0_32 ),
inference(resolution,[],[f649,f244]) ).
fof(f651,plain,
( ~ spl0_7
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f650]) ).
fof(f652,plain,
( $false
| ~ spl0_34
| ~ spl0_39 ),
inference(resolution,[],[f250,f517]) ).
fof(f655,plain,
( ~ spl0_34
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f652]) ).
fof(f656,plain,
( ~ spl0_61
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f431,f426,f233,f230,f227,f397]) ).
fof(f657,plain,
( ~ spl0_31
| spl0_23
| spl0_22
| spl0_21
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f504,f501,f185,f188,f191,f236]) ).
fof(f658,plain,
( ~ spl0_20
| spl0_9
| spl0_8
| spl0_7
| ~ spl0_1
| spl0_49 ),
inference(avatar_split_clause,[],[f353,f346,f112,f138,f141,f144,f182]) ).
fof(f659,plain,
( ~ spl0_47
| spl0_7
| spl0_8
| spl0_9
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f451,f447,f144,f141,f138,f324]) ).
fof(f660,plain,
( $false
| ~ spl0_9 ),
inference(resolution,[],[f145,f299]) ).
fof(f666,plain,
~ spl0_9,
inference(avatar_contradiction_clause,[],[f660]) ).
fof(f668,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_8 ),
inference(resolution,[],[f142,f57]) ).
fof(f679,plain,
( ~ product1(e_2,e_4,e_3)
| ~ spl0_38 ),
inference(resolution,[],[f276,f57]) ).
fof(f689,plain,
( $false
| ~ spl0_29 ),
inference(resolution,[],[f522,f21]) ).
fof(f690,plain,
~ spl0_29,
inference(avatar_contradiction_clause,[],[f689]) ).
fof(f700,plain,
( $false
| ~ spl0_8 ),
inference(resolution,[],[f668,f21]) ).
fof(f701,plain,
~ spl0_8,
inference(avatar_contradiction_clause,[],[f700]) ).
fof(f702,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,[],[f148,f17]) ).
fof(f717,plain,
! [X0] :
( ~ product1(X0,e_3,e_1)
| ~ product1(e_3,e_1,X0) ),
inference(resolution,[],[f642,f26]) ).
fof(f718,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,[],[f325,f17]) ).
fof(f726,plain,
( $false
| ~ spl0_13
| ~ spl0_60 ),
inference(resolution,[],[f492,f158]) ).
fof(f727,plain,
( ~ spl0_13
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f726]) ).
fof(f728,plain,
~ spl0_67,
inference(avatar_split_clause,[],[f541,f509]) ).
fof(f731,plain,
( ~ spl0_19
| spl0_13
| spl0_12
| spl0_11
| ~ spl0_1
| spl0_47 ),
inference(avatar_split_clause,[],[f718,f324,f112,f151,f154,f157,f177]) ).
fof(f732,plain,
~ spl0_63,
inference(avatar_split_clause,[],[f475,f434]) ).
fof(f763,plain,
( $false
| ~ spl0_38
| ~ spl0_41 ),
inference(resolution,[],[f679,f286]) ).
fof(f764,plain,
( ~ spl0_38
| ~ spl0_41 ),
inference(avatar_contradiction_clause,[],[f763]) ).
fof(f771,plain,
( $false
| ~ spl0_23
| ~ spl0_36 ),
inference(resolution,[],[f625,f192]) ).
fof(f772,plain,
( ~ spl0_23
| ~ spl0_36 ),
inference(avatar_contradiction_clause,[],[f771]) ).
fof(f779,plain,
( $false
| ~ spl0_37
| ~ spl0_59 ),
inference(resolution,[],[f629,f392]) ).
fof(f780,plain,
( ~ spl0_37
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f779]) ).
fof(f781,plain,
( ~ spl0_20
| spl0_21
| spl0_22
| spl0_23
| ~ spl0_19
| spl0_10 ),
inference(avatar_split_clause,[],[f702,f147,f177,f191,f188,f185,f182]) ).
fof(f787,plain,
( ~ product1(e_2,e_3,e_1)
| ~ spl0_22 ),
inference(resolution,[],[f189,f717]) ).
fof(f791,plain,
( $false
| ~ spl0_22
| ~ spl0_28 ),
inference(resolution,[],[f787,f228]) ).
fof(f792,plain,
( ~ spl0_22
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f791]) ).
fof(f797,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,[],[f237,f17]) ).
fof(f798,plain,
( ~ spl0_1
| spl0_32
| spl0_33
| spl0_34
| ~ spl0_19
| spl0_31 ),
inference(avatar_split_clause,[],[f797,f236,f177,f249,f246,f243,f112]) ).
fof(f799,plain,
( $false
| ~ spl0_28
| ~ spl0_34 ),
inference(resolution,[],[f250,f252]) ).
fof(f802,plain,
( ~ spl0_28
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f799]) ).
cnf(s1,plain,
( ~ spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f117]) ).
cnf(s2,plain,
spl0_1,
inference(sat_conversion,[],[f119]) ).
cnf(s4,plain,
( ~ spl0_2
| spl0_7
| spl0_8
| spl0_9
| ~ spl0_10 ),
inference(sat_conversion,[],[f149]) ).
cnf(s8,plain,
spl0_15,
inference(sat_conversion,[],[f195]) ).
cnf(s9,plain,
spl0_19,
inference(sat_conversion,[],[f199]) ).
cnf(s10,plain,
spl0_20,
inference(sat_conversion,[],[f204]) ).
cnf(s11,plain,
( ~ spl0_20
| spl0_24 ),
inference(sat_conversion,[],[f211]) ).
cnf(s13,plain,
( ~ spl0_24
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_31 ),
inference(sat_conversion,[],[f238]) ).
cnf(s22,plain,
~ spl0_21,
inference(sat_conversion,[],[f295]) ).
cnf(s27,plain,
~ spl0_11,
inference(sat_conversion,[],[f332]) ).
cnf(s28,plain,
( ~ spl0_15
| spl0_48 ),
inference(sat_conversion,[],[f340]) ).
cnf(s29,plain,
( spl0_36
| spl0_37
| spl0_38
| ~ spl0_48
| ~ spl0_49 ),
inference(sat_conversion,[],[f348]) ).
cnf(s37,plain,
( ~ spl0_19
| ~ spl0_20
| spl0_44
| spl0_45
| spl0_46
| spl0_61 ),
inference(sat_conversion,[],[f408]) ).
cnf(s38,plain,
~ spl0_44,
inference(sat_conversion,[],[f412]) ).
cnf(s39,plain,
( ~ spl0_12
| ~ spl0_45 ),
inference(sat_conversion,[],[f417]) ).
cnf(s40,plain,
( ~ spl0_1
| spl0_62 ),
inference(sat_conversion,[],[f428]) ).
cnf(s42,plain,
( ~ spl0_15
| ~ spl0_19
| spl0_58
| spl0_59
| spl0_60
| spl0_63 ),
inference(sat_conversion,[],[f438]) ).
cnf(s43,plain,
( ~ spl0_20
| spl0_64 ),
inference(sat_conversion,[],[f449]) ).
cnf(s44,plain,
~ spl0_58,
inference(sat_conversion,[],[f455]) ).
cnf(s45,plain,
( ~ spl0_45
| ~ spl0_59 ),
inference(sat_conversion,[],[f461]) ).
cnf(s47,plain,
( ~ spl0_12
| ~ spl0_59 ),
inference(sat_conversion,[],[f471]) ).
cnf(s49,plain,
~ spl0_46,
inference(sat_conversion,[],[f486]) ).
cnf(s51,plain,
( ~ spl0_20
| spl0_66 ),
inference(sat_conversion,[],[f503]) ).
cnf(s53,plain,
( ~ spl0_1
| ~ spl0_15
| spl0_39
| spl0_40
| spl0_41
| spl0_67 ),
inference(sat_conversion,[],[f513]) ).
cnf(s54,plain,
( ~ spl0_28
| ~ spl0_39 ),
inference(sat_conversion,[],[f519]) ).
cnf(s58,plain,
~ spl0_33,
inference(sat_conversion,[],[f537]) ).
cnf(s60,plain,
~ spl0_30,
inference(sat_conversion,[],[f552]) ).
cnf(s62,plain,
~ spl0_40,
inference(sat_conversion,[],[f569]) ).
cnf(s64,plain,
( ~ spl0_41
| ~ spl0_60 ),
inference(sat_conversion,[],[f585]) ).
cnf(s73,plain,
( ~ spl0_7
| ~ spl0_23 ),
inference(sat_conversion,[],[f639]) ).
cnf(s74,plain,
( ~ spl0_7
| ~ spl0_32 ),
inference(sat_conversion,[],[f651]) ).
cnf(s75,plain,
( ~ spl0_34
| ~ spl0_39 ),
inference(sat_conversion,[],[f655]) ).
cnf(s76,plain,
( spl0_28
| spl0_29
| spl0_30
| ~ spl0_61
| ~ spl0_62 ),
inference(sat_conversion,[],[f656]) ).
cnf(s77,plain,
( spl0_21
| spl0_22
| spl0_23
| ~ spl0_31
| ~ spl0_66 ),
inference(sat_conversion,[],[f657]) ).
cnf(s78,plain,
( ~ spl0_1
| spl0_7
| spl0_8
| spl0_9
| ~ spl0_20
| spl0_49 ),
inference(sat_conversion,[],[f658]) ).
cnf(s79,plain,
( spl0_7
| spl0_8
| spl0_9
| ~ spl0_47
| ~ spl0_64 ),
inference(sat_conversion,[],[f659]) ).
cnf(s80,plain,
~ spl0_9,
inference(sat_conversion,[],[f666]) ).
cnf(s82,plain,
~ spl0_29,
inference(sat_conversion,[],[f690]) ).
cnf(s84,plain,
~ spl0_8,
inference(sat_conversion,[],[f701]) ).
cnf(s90,plain,
( ~ spl0_13
| ~ spl0_60 ),
inference(sat_conversion,[],[f727]) ).
cnf(s91,plain,
~ spl0_67,
inference(sat_conversion,[],[f728]) ).
cnf(s94,plain,
( ~ spl0_1
| spl0_11
| spl0_12
| spl0_13
| ~ spl0_19
| spl0_47 ),
inference(sat_conversion,[],[f731]) ).
cnf(s95,plain,
~ spl0_63,
inference(sat_conversion,[],[f732]) ).
cnf(s98,plain,
( ~ spl0_38
| ~ spl0_41 ),
inference(sat_conversion,[],[f764]) ).
cnf(s99,plain,
( ~ spl0_23
| ~ spl0_36 ),
inference(sat_conversion,[],[f772]) ).
cnf(s100,plain,
( ~ spl0_37
| ~ spl0_59 ),
inference(sat_conversion,[],[f780]) ).
cnf(s101,plain,
( spl0_10
| ~ spl0_19
| ~ spl0_20
| spl0_21
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f781]) ).
cnf(s102,plain,
( ~ spl0_22
| ~ spl0_28 ),
inference(sat_conversion,[],[f792]) ).
cnf(s103,plain,
( ~ spl0_1
| ~ spl0_19
| spl0_31
| spl0_32
| spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f798]) ).
cnf(s104,plain,
( ~ spl0_28
| ~ spl0_34 ),
inference(sat_conversion,[],[f802]) ).
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(f803,plain,
$false,
inference(avatar_sat_refutation,[],[s162]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP124-6.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 % Computer : n002.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 09:24:21 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.44 Running first-order theorem proving
% 0.13/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.05/1.33 % (3280484)Input is clausal, will run a generic CNF schedule.
% 3.05/1.33 % (3280489)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=3687499282:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.05/1.33 % (3280492)lrs+10_1_sil=8000:sp=occurrence:random_seed=2445561319:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.05/1.33 % (3280494)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1287791134:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.05/1.33 % (3280491)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=451407986:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.05/1.33 % (3280495)dis-21_1_sil=8000:lcm=predicate:random_seed=3526704137:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.05/1.33 % (3280493)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1376963002:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.05/1.33 % (3280490)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2773143213:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.05/1.33 % (3280495)First to succeed.
% 3.05/1.33 % (3280495)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3280484"
% 3.05/1.33 % (3280494)Also succeeded, but the first one will report.
% 3.05/1.33 % (3280492)Instruction limit reached!
% 3.05/1.33 % (3280492)------------------------------
% 3.05/1.33 % (3280492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.33 % (3280492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.33 % (3280492)CaDiCaL version: 2.1.3
% 3.05/1.33 % (3280492)Termination reason: Instruction limit
% 3.05/1.33 % (3280492)Termination phase: Saturation
% 3.05/1.33 % (3280492)Time elapsed: 0.062 s
% 3.05/1.33 % (3280492)Peak memory usage: 88 MB
% 3.05/1.33 % (3280492)Instructions burned: 108 (million)
% 3.05/1.33 % (3280493)Instruction limit reached!
% 3.05/1.33 % (3280493)------------------------------
% 3.05/1.33 % (3280493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.33 % (3280493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.33 % (3280493)CaDiCaL version: 2.1.3
% 3.05/1.33 % (3280493)Termination reason: Instruction limit
% 3.05/1.33 % (3280493)Termination phase: Saturation
% 3.05/1.33 % (3280493)Time elapsed: 0.062 s
% 3.05/1.33 % (3280493)Peak memory usage: 88 MB
% 3.05/1.33 % (3280493)Instructions burned: 114 (million)
% 3.05/1.33 % (3280503)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=924962645:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 3.05/1.33 % (3280504)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=762076842:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 3.05/1.33 % (3280504)Refutation not found, incomplete strategy
% 3.05/1.33 % (3280504)------------------------------
% 3.05/1.33 % (3280504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.33 % (3280504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.33 % (3280504)CaDiCaL version: 2.1.3
% 3.05/1.33 % (3280504)Termination reason: Refutation not found, incomplete strategy
% 3.05/1.33 % (3280504)Time elapsed: 0.002 s
% 3.05/1.33 % (3280504)Peak memory usage: 87 MB
% 3.05/1.33 % (3280504)Instructions burned: 1 (million)
% 3.05/1.33 % (3280495)Refutation found. Thanks to Tanya!
% 3.05/1.33 % SZS status Unsatisfiable for theBenchmark
% 3.05/1.33 % SZS output start Proof for theBenchmark
% See solution above
% 3.78/1.52 % (3280495)------------------------------
% 3.78/1.52 % (3280495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.78/1.52 % (3280495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.78/1.52 % (3280495)CaDiCaL version: 2.1.3
% 3.78/1.52 % (3280495)Termination reason: Refutation
% 3.78/1.52 % (3280495)Time elapsed: 0.015 s
% 3.78/1.52 % (3280495)Peak memory usage: 89 MB
% 3.78/1.52 % (3280495)Instructions burned: 22 (million)
% 3.78/1.52 % (3280495)------------------------------
% 3.78/1.52 % (3280495)------------------------------
% 3.78/1.52 % (3280484)Success in time 0.446 s
% 3.78/1.52 % Vampire exiting
%------------------------------------------------------------------------------