%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP127-4.004 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:57 AM UTC 2026
% Result : Unsatisfiable 3.12s 1.33s
% Output : Refutation 3.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 74
% Syntax : Number of formulae : 387 ( 43 unt; 57 def)
% Number of atoms : 1139 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1302 ( 550 ~; 695 |; 0 &)
% ( 57 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 61 ( 60 usr; 58 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 82 ( 0 sgn 82 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( product(e_4,X0,X1)
| ~ group_element(X1)
| product(e_1,X0,X1)
| product(e_2,X0,X1)
| product(e_3,X0,X1)
| ~ group_element(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',row_surjectivity) ).
fof(f2,axiom,
! [X0,X1] :
( product(X0,e_4,X1)
| ~ group_element(X1)
| product(X0,e_1,X1)
| product(X0,e_2,X1)
| product(X0,e_3,X1)
| ~ group_element(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',column_surjectivity) ).
fof(f3,negated_conjecture,
! [X2,X3,X0,X1] :
( product(X0,X1,X2)
| ~ product(X3,X0,X1)
| ~ product(X2,X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3_1) ).
fof(f4,negated_conjecture,
! [X2,X3,X0,X1] :
( product(X0,X1,X2)
| ~ product(X2,X1,X3)
| ~ product(X1,X3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3_2) ).
fof(f5,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
fof(f6,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
fof(f7,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
fof(f8,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
fof(f9,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f10,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f11,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f13,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f14,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f21,axiom,
! [X0,X1] :
( product(X0,X1,e_4)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| ~ group_element(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
fof(f22,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
fof(f25,axiom,
! [X0] : product(X0,X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_idempotence) ).
fof(f26,negated_conjecture,
! [X2,X3,X0,X1] :
( product(X3,X0,X1)
| ~ product(X2,X0,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
fof(f27,plain,
! [X0,X1] :
( ~ product(X0,X1,e_2)
| ~ product(X0,X1,e_1) ),
inference(resolution,[],[f22,f9]) ).
fof(f28,plain,
! [X0,X1] :
( ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_1) ),
inference(resolution,[],[f22,f10]) ).
fof(f29,plain,
! [X0,X1] :
( ~ product(X0,X1,e_4)
| ~ product(X0,X1,e_1) ),
inference(resolution,[],[f22,f11]) ).
fof(f31,plain,
! [X0,X1] :
( ~ product(X0,X1,e_3)
| ~ product(X0,X1,e_2) ),
inference(resolution,[],[f22,f13]) ).
fof(f32,plain,
! [X0,X1] :
( ~ product(X0,X1,e_4)
| ~ product(X0,X1,e_2) ),
inference(resolution,[],[f22,f14]) ).
fof(f51,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,e_1)
| ~ product(X2,X1,X0)
| ~ product(X1,e_2,X2) ),
inference(resolution,[],[f27,f26]) ).
fof(f52,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,e_1)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0) ),
inference(resolution,[],[f27,f4]) ).
fof(f73,plain,
! [X0] :
( ~ product(X0,X0,e_1)
| ~ product(X0,e_2,X0) ),
inference(resolution,[],[f51,f25]) ).
fof(f78,plain,
! [X0] :
( ~ product(e_1,X0,e_1)
| ~ product(X0,e_2,e_1) ),
inference(factoring,[],[f51]) ).
fof(f79,plain,
( ~ product(e_2,e_2,e_1)
| ~ product(e_1,e_2,e_2) ),
inference(factoring,[],[f51]) ).
fof(f82,definition,
( spl0_1
<=> product(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f83,plain,
( ~ product(e_1,e_2,e_2)
| spl0_1 ),
inference(avatar_component_clause,[],[f82]) ).
fof(f85,definition,
( spl0_2
<=> product(e_2,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f86,plain,
( ~ product(e_2,e_2,e_1)
| spl0_2 ),
inference(avatar_component_clause,[],[f85]) ).
fof(f87,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f79,f85,f82]) ).
fof(f88,plain,
( ! [X0] :
( ~ product(X0,e_2,e_1)
| ~ product(e_2,e_2,X0) )
| spl0_1 ),
inference(resolution,[],[f83,f26]) ).
fof(f90,plain,
( ! [X0] :
( ~ product(X0,e_1,e_2)
| ~ product(e_2,e_1,X0) )
| spl0_1 ),
inference(resolution,[],[f83,f3]) ).
fof(f97,plain,
( ~ product(e_2,e_2,e_1)
| spl0_1 ),
inference(resolution,[],[f88,f25]) ).
fof(f98,plain,
( ~ spl0_2
| spl0_1 ),
inference(avatar_split_clause,[],[f97,f82,f85]) ).
fof(f99,plain,
( ! [X0] :
( ~ product(X0,e_2,e_2)
| ~ product(e_2,e_1,X0) )
| spl0_2 ),
inference(resolution,[],[f86,f26]) ).
fof(f100,plain,
( ! [X0] :
( ~ product(e_2,X0,e_2)
| ~ product(e_1,e_2,X0) )
| spl0_2 ),
inference(resolution,[],[f86,f4]) ).
fof(f101,plain,
( ! [X0] :
( ~ product(X0,e_2,e_2)
| ~ product(e_1,e_2,X0) )
| spl0_2 ),
inference(resolution,[],[f86,f3]) ).
fof(f115,plain,
( ~ product(e_2,e_1,e_2)
| spl0_1 ),
inference(factoring,[],[f90]) ).
fof(f129,plain,
( ~ product(e_1,e_2,e_2)
| spl0_2 ),
inference(resolution,[],[f100,f25]) ).
fof(f130,plain,
! [X0] :
( ~ group_element(e_2)
| product(e_1,X0,e_2)
| product(e_2,X0,e_2)
| product(e_3,X0,e_2)
| ~ group_element(X0)
| ~ product(e_4,X0,e_1) ),
inference(resolution,[],[f1,f27]) ).
fof(f133,plain,
! [X0,X1] :
( ~ group_element(X0)
| product(e_1,e_2,X0)
| product(e_2,e_2,X0)
| product(e_3,e_2,X0)
| ~ group_element(e_2)
| ~ product(X1,e_4,e_1)
| ~ product(X0,e_4,X1) ),
inference(resolution,[],[f1,f51]) ).
fof(f139,definition,
( spl0_3
<=> product(e_2,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f140,plain,
( ~ product(e_2,e_1,e_4)
| spl0_3 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f142,definition,
( spl0_4
<=> group_element(e_1) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f143,plain,
( ~ group_element(e_1)
| spl0_4 ),
inference(avatar_component_clause,[],[f142]) ).
fof(f145,definition,
( spl0_5
<=> product(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f146,plain,
( product(e_3,e_1,e_2)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f145]) ).
fof(f148,definition,
( spl0_6
<=> product(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f149,plain,
( product(e_2,e_1,e_2)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f148]) ).
fof(f151,definition,
( spl0_7
<=> product(e_1,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f152,plain,
( product(e_1,e_1,e_2)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f154,definition,
( spl0_8
<=> group_element(e_2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f155,plain,
( ~ group_element(e_2)
| spl0_8 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f158,definition,
( spl0_9
<=> product(e_2,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f161,definition,
( spl0_10
<=> product(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f162,plain,
( product(e_3,e_2,e_1)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f165,definition,
( spl0_11
<=> product(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f166,plain,
( product(e_1,e_2,e_1)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f169,definition,
( spl0_12
<=> ! [X0,X1] :
( ~ group_element(X0)
| ~ product(X0,e_4,X1)
| ~ product(X1,e_4,e_1)
| product(e_3,e_2,X0)
| product(e_2,e_2,X0)
| product(e_1,e_2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f170,plain,
( ! [X0,X1] :
( ~ group_element(X0)
| ~ product(X0,e_4,X1)
| ~ product(X1,e_4,e_1)
| product(e_3,e_2,X0)
| product(e_2,e_2,X0)
| product(e_1,e_2,X0) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f169]) ).
fof(f171,plain,
( ~ spl0_8
| spl0_12 ),
inference(avatar_split_clause,[],[f133,f169,f154]) ).
fof(f177,definition,
( spl0_14
<=> ! [X0] :
( product(e_1,X0,e_2)
| ~ product(e_4,X0,e_1)
| ~ group_element(X0)
| product(e_3,X0,e_2)
| product(e_2,X0,e_2) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f178,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product(e_4,X0,e_1)
| product(e_1,X0,e_2)
| product(e_3,X0,e_2)
| product(e_2,X0,e_2) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f177]) ).
fof(f179,plain,
( spl0_14
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f130,f154,f177]) ).
fof(f189,plain,
( $false
| spl0_4 ),
inference(resolution,[],[f143,f5]) ).
fof(f190,plain,
spl0_4,
inference(avatar_contradiction_clause,[],[f189]) ).
fof(f196,definition,
( spl0_15
<=> product(e_2,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f199,definition,
( spl0_16
<=> product(e_3,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f200,plain,
( product(e_3,e_4,e_1)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f202,definition,
( spl0_17
<=> product(e_1,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f205,definition,
( spl0_18
<=> ! [X0] :
( ~ product(e_4,e_2,X0)
| ~ product(X0,e_4,e_4) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f206,plain,
( ! [X0] :
( ~ product(e_4,e_2,X0)
| ~ product(X0,e_4,e_4) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f209,definition,
( spl0_19
<=> product(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f212,definition,
( spl0_20
<=> product(e_3,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f213,plain,
( product(e_3,e_3,e_1)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f215,definition,
( spl0_21
<=> product(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f218,definition,
( spl0_22
<=> ! [X0] :
( ~ product(e_3,e_2,X0)
| ~ product(X0,e_3,e_4) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f219,plain,
( ! [X0] :
( ~ product(e_3,e_2,X0)
| ~ product(X0,e_3,e_4) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f218]) ).
fof(f225,plain,
( $false
| spl0_8 ),
inference(resolution,[],[f155,f6]) ).
fof(f226,plain,
spl0_8,
inference(avatar_contradiction_clause,[],[f225]) ).
fof(f227,plain,
( ~ product(e_4,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_3,e_1,e_2)
| product(e_2,e_1,e_2)
| ~ spl0_14 ),
inference(resolution,[],[f178,f5]) ).
fof(f232,definition,
( spl0_24
<=> product(e_2,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f233,plain,
( product(e_2,e_4,e_2)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f238,definition,
( spl0_26
<=> product(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f239,plain,
( product(e_1,e_4,e_2)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f241,definition,
( spl0_27
<=> product(e_4,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f242,plain,
( ~ product(e_4,e_4,e_1)
| spl0_27 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f251,definition,
( spl0_30
<=> product(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f252,plain,
( product(e_1,e_3,e_2)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f254,definition,
( spl0_31
<=> product(e_4,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f255,plain,
( ~ product(e_4,e_3,e_1)
| spl0_31 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f258,definition,
( spl0_32
<=> product(e_4,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f259,plain,
( ~ product(e_4,e_1,e_1)
| spl0_32 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f260,plain,
( spl0_6
| spl0_5
| spl0_7
| ~ spl0_32
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f227,f177,f258,f151,f145,f148]) ).
fof(f263,plain,
( ! [X0] :
( ~ product(e_1,e_4,X0)
| ~ product(X0,e_4,e_1)
| product(e_3,e_2,e_1)
| product(e_2,e_2,e_1)
| product(e_1,e_2,e_1) )
| ~ spl0_12 ),
inference(resolution,[],[f170,f5]) ).
fof(f268,definition,
( spl0_33
<=> product(e_1,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f279,definition,
( spl0_36
<=> product(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f282,definition,
( spl0_37
<=> product(e_2,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f283,plain,
( product(e_2,e_2,e_3)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f292,definition,
( spl0_40
<=> ! [X0] :
( ~ product(e_1,e_4,X0)
| ~ product(X0,e_4,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f293,plain,
( ! [X0] :
( ~ product(e_1,e_4,X0)
| ~ product(X0,e_4,e_1) )
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f294,plain,
( spl0_11
| spl0_2
| spl0_10
| spl0_40
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f263,f169,f292,f161,f85,f165]) ).
fof(f296,plain,
( ! [X0] :
( ~ product(X0,e_4,e_4)
| ~ product(e_4,e_1,X0) )
| spl0_27 ),
inference(resolution,[],[f242,f26]) ).
fof(f307,plain,
( ! [X0] :
( ~ product(X0,e_4,e_1)
| ~ product(e_1,e_4,X0) )
| spl0_32 ),
inference(resolution,[],[f259,f3]) ).
fof(f309,plain,
( spl0_40
| spl0_32 ),
inference(avatar_split_clause,[],[f307,f258,f292]) ).
fof(f313,plain,
( ~ product(e_4,e_1,e_4)
| spl0_27 ),
inference(resolution,[],[f296,f25]) ).
fof(f328,definition,
( spl0_43
<=> product(e_2,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f331,definition,
( spl0_44
<=> product(e_1,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f334,definition,
( spl0_45
<=> group_element(e_4) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f335,plain,
( ~ group_element(e_4)
| spl0_45 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f337,definition,
( spl0_46
<=> product(e_4,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f338,plain,
( ~ product(e_4,e_1,e_4)
| spl0_46 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f340,plain,
( ~ spl0_46
| spl0_27 ),
inference(avatar_split_clause,[],[f313,f241,f337]) ).
fof(f352,plain,
( ~ product(e_1,e_2,e_4)
| spl0_2
| ~ spl0_24 ),
inference(resolution,[],[f233,f100]) ).
fof(f359,definition,
( spl0_47
<=> product(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f371,definition,
( spl0_48
<=> group_element(e_3) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f372,plain,
( ~ group_element(e_3)
| spl0_48 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f377,definition,
( spl0_50
<=> product(e_2,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f378,plain,
( product(e_2,e_3,e_4)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f380,definition,
( spl0_51
<=> product(e_1,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f383,definition,
( spl0_52
<=> product(e_3,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f386,plain,
( $false
| spl0_45 ),
inference(resolution,[],[f335,f8]) ).
fof(f387,plain,
spl0_45,
inference(avatar_contradiction_clause,[],[f386]) ).
fof(f391,plain,
( $false
| spl0_48 ),
inference(resolution,[],[f372,f7]) ).
fof(f392,plain,
spl0_48,
inference(avatar_contradiction_clause,[],[f391]) ).
fof(f404,definition,
( spl0_54
<=> product(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f407,definition,
( spl0_55
<=> product(e_1,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f408,plain,
( product(e_1,e_4,e_3)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f409,plain,
( ~ product(e_1,e_4,e_4)
| spl0_44 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f450,plain,
! [X0] :
( ~ group_element(e_2)
| product(X0,e_1,e_2)
| product(X0,e_2,e_2)
| product(X0,e_3,e_2)
| ~ group_element(X0)
| ~ product(X0,e_4,e_1) ),
inference(resolution,[],[f2,f27]) ).
fof(f462,definition,
( spl0_58
<=> ! [X0] :
( product(X0,e_1,e_2)
| ~ product(X0,e_4,e_1)
| ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_2,e_2) ) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f463,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product(X0,e_4,e_1)
| product(X0,e_1,e_2)
| product(X0,e_3,e_2)
| product(X0,e_2,e_2) )
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f462]) ).
fof(f464,plain,
( spl0_58
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f450,f154,f462]) ).
fof(f466,definition,
( spl0_59
<=> product(e_4,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f467,plain,
( ~ product(e_4,e_2,e_4)
| spl0_59 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f468,plain,
( product(e_4,e_3,e_1)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f470,definition,
( spl0_60
<=> product(e_4,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f471,plain,
( product(e_4,e_2,e_1)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f474,plain,
( ~ product(e_1,e_4,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_3,e_2)
| product(e_1,e_2,e_2)
| ~ spl0_58 ),
inference(resolution,[],[f463,f5]) ).
fof(f479,definition,
( spl0_61
<=> product(e_4,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f480,plain,
( product(e_4,e_2,e_2)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f482,definition,
( spl0_62
<=> product(e_4,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f483,plain,
( product(e_4,e_3,e_2)
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f485,definition,
( spl0_63
<=> product(e_4,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f486,plain,
( product(e_4,e_1,e_2)
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f489,plain,
( ~ product(e_1,e_4,e_1)
| spl0_17 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f490,plain,
( spl0_1
| spl0_30
| spl0_7
| ~ spl0_17
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f474,f462,f202,f151,f251,f82]) ).
fof(f506,plain,
( product(e_3,e_1,e_4)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f509,definition,
( spl0_64
<=> product(e_1,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f510,plain,
( product(e_1,e_1,e_4)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f557,plain,
( ~ product(e_1,e_2,e_4)
| spl0_2
| ~ spl0_61 ),
inference(resolution,[],[f480,f101]) ).
fof(f558,plain,
( ~ product(e_2,e_1,e_4)
| spl0_2
| ~ spl0_61 ),
inference(resolution,[],[f480,f99]) ).
fof(f579,plain,
( ~ product(e_1,e_3,e_1)
| ~ spl0_30 ),
inference(resolution,[],[f252,f27]) ).
fof(f599,plain,
( ~ product(e_4,e_3,e_1)
| ~ spl0_62 ),
inference(resolution,[],[f483,f27]) ).
fof(f603,plain,
( ~ spl0_31
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f599,f482,f254]) ).
fof(f609,plain,
( ! [X0] :
( ~ product(e_3,X0,e_4)
| ~ product(e_1,e_3,X0) )
| spl0_31 ),
inference(resolution,[],[f255,f4]) ).
fof(f620,plain,
( ~ product(e_1,e_3,e_1)
| spl0_31
| ~ spl0_52 ),
inference(resolution,[],[f609,f506]) ).
fof(f674,plain,
( ~ product(e_2,e_1,e_4)
| spl0_1
| ~ spl0_63 ),
inference(resolution,[],[f486,f90]) ).
fof(f684,definition,
( spl0_75
<=> product(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f697,definition,
( spl0_77
<=> product(e_4,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f698,plain,
( product(e_4,e_2,e_3)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f697]) ).
fof(f718,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f129,f85,f82]) ).
fof(f721,plain,
( ! [X0] :
( ~ product(X0,e_1,e_2)
| ~ product(e_2,e_1,X0) )
| spl0_1 ),
inference(resolution,[],[f83,f3]) ).
fof(f745,plain,
( ~ product(e_1,e_4,e_3)
| ~ spl0_16
| ~ spl0_40 ),
inference(resolution,[],[f293,f200]) ).
fof(f747,plain,
( ~ product(e_1,e_4,e_1)
| ~ spl0_40 ),
inference(factoring,[],[f293]) ).
fof(f748,plain,
( ~ spl0_17
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f747,f292,f202]) ).
fof(f759,plain,
( ! [X0] :
( ~ product(e_4,X0,e_1)
| ~ product(e_1,e_4,X0) )
| spl0_17 ),
inference(resolution,[],[f489,f4]) ).
fof(f825,plain,
( ~ product(e_2,e_1,e_4)
| ~ group_element(e_2)
| product(e_1,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_3,e_1,e_2)
| ~ group_element(e_1)
| spl0_1 ),
inference(resolution,[],[f721,f1]) ).
fof(f850,plain,
( ~ product(e_1,e_4,e_2)
| spl0_17
| ~ spl0_60 ),
inference(resolution,[],[f759,f471]) ).
fof(f867,plain,
( ! [X0] :
( ~ product(X0,e_3,e_4)
| ~ product(e_3,e_2,X0) )
| ~ spl0_31 ),
inference(resolution,[],[f468,f51]) ).
fof(f869,plain,
( spl0_22
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f867,f254,f218]) ).
fof(f875,plain,
( ~ product(e_3,e_4,e_1)
| spl0_16 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f895,plain,
( ~ spl0_3
| spl0_1
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f674,f485,f82,f139]) ).
fof(f896,plain,
( ~ spl0_4
| spl0_5
| spl0_6
| spl0_7
| ~ spl0_8
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f825,f82,f139,f154,f151,f148,f145,f142]) ).
fof(f918,definition,
( spl0_87
<=> product(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f949,definition,
( spl0_91
<=> product(e_1,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f950,plain,
( ~ product(e_1,e_1,e_1)
| spl0_91 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f963,plain,
( ~ product(e_1,e_2,e_4)
| spl0_33 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f968,plain,
( ~ product(e_3,e_1,e_1)
| ~ spl0_5 ),
inference(resolution,[],[f146,f27]) ).
fof(f970,plain,
( ~ spl0_87
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f968,f145,f918]) ).
fof(f974,plain,
( ! [X0] :
( ~ product(e_4,X0,e_4)
| ~ product(e_1,e_4,X0) )
| spl0_27 ),
inference(resolution,[],[f242,f4]) ).
fof(f989,plain,
( ~ product(e_4,e_2,e_4)
| ~ spl0_18 ),
inference(resolution,[],[f206,f25]) ).
fof(f992,plain,
( ~ spl0_59
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f989,f205,f466]) ).
fof(f1006,plain,
( $false
| spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f149,f115]) ).
fof(f1010,plain,
( spl0_1
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[],[f1006]) ).
fof(f1014,definition,
( spl0_95
<=> product(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f1015,plain,
( product(e_2,e_3,e_3)
| ~ spl0_95 ),
inference(avatar_component_clause,[],[f1014]) ).
fof(f1016,plain,
( ~ product(e_2,e_4,e_1)
| spl0_15 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f1018,plain,
( ~ group_element(e_1)
| product(e_3,e_1,e_1)
| product(e_3,e_2,e_1)
| product(e_3,e_3,e_1)
| ~ group_element(e_3)
| spl0_16 ),
inference(resolution,[],[f875,f2]) ).
fof(f1022,plain,
( ~ spl0_48
| spl0_20
| spl0_10
| spl0_87
| ~ spl0_4
| spl0_16 ),
inference(avatar_split_clause,[],[f1018,f199,f142,f918,f161,f212,f371]) ).
fof(f1025,plain,
( ~ product(e_2,e_3,e_1)
| ~ spl0_95 ),
inference(resolution,[],[f1015,f28]) ).
fof(f1026,plain,
( ~ spl0_19
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f1025,f1014,f209]) ).
fof(f1179,plain,
~ product(e_4,e_4,e_1),
inference(resolution,[],[f29,f25]) ).
fof(f1198,plain,
( ~ product(e_4,e_2,e_1)
| spl0_60 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f1225,plain,
( ~ product(e_1,e_4,e_4)
| spl0_27 ),
inference(resolution,[],[f974,f25]) ).
fof(f1236,plain,
( ~ product(e_2,e_3,e_1)
| ~ spl0_50 ),
inference(resolution,[],[f378,f29]) ).
fof(f1283,plain,
( $false
| spl0_17
| ~ spl0_26
| ~ spl0_60 ),
inference(resolution,[],[f850,f239]) ).
fof(f1288,plain,
( spl0_17
| ~ spl0_26
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f1283]) ).
fof(f1321,plain,
! [X0] :
( ~ product(X0,X0,e_1)
| ~ product(e_2,X0,X0) ),
inference(resolution,[],[f52,f25]) ).
fof(f1329,plain,
! [X0] :
( ~ product(e_2,X0,e_1)
| ~ product(X0,e_1,e_2) ),
inference(factoring,[],[f52]) ).
fof(f1362,plain,
( $false
| spl0_91 ),
inference(resolution,[],[f950,f25]) ).
fof(f1363,plain,
spl0_91,
inference(avatar_contradiction_clause,[],[f1362]) ).
fof(f1382,definition,
( spl0_120
<=> ! [X0] :
( ~ product(e_2,e_4,X0)
| ~ product(e_4,X0,e_2) ) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f1383,plain,
( ! [X0] :
( ~ product(e_4,X0,e_2)
| ~ product(e_2,e_4,X0) )
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f1382]) ).
fof(f1399,plain,
( ~ product(e_1,e_3,e_4)
| ~ spl0_10
| ~ spl0_22 ),
inference(resolution,[],[f162,f219]) ).
fof(f1400,plain,
( ~ product(e_1,e_3,e_1)
| ~ spl0_10 ),
inference(resolution,[],[f162,f78]) ).
fof(f1409,plain,
( ~ spl0_21
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f1400,f161,f215]) ).
fof(f1475,plain,
( ~ spl0_44
| spl0_27 ),
inference(avatar_split_clause,[],[f1225,f241,f331]) ).
fof(f1476,plain,
( ~ spl0_33
| spl0_2
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f557,f479,f85,f268]) ).
fof(f1477,plain,
~ spl0_27,
inference(avatar_split_clause,[],[f1179,f241]) ).
fof(f1481,plain,
( ~ group_element(e_1)
| product(e_1,e_4,e_1)
| product(e_2,e_4,e_1)
| product(e_3,e_4,e_1)
| ~ group_element(e_4)
| spl0_27 ),
inference(resolution,[],[f242,f1]) ).
fof(f1482,plain,
( ~ group_element(e_1)
| product(e_4,e_1,e_1)
| product(e_4,e_2,e_1)
| product(e_4,e_3,e_1)
| ~ group_element(e_4)
| spl0_27 ),
inference(resolution,[],[f242,f2]) ).
fof(f1483,plain,
( ! [X0] :
( ~ product(X0,e_4,e_4)
| ~ product(e_4,e_1,X0) )
| spl0_27 ),
inference(resolution,[],[f242,f26]) ).
fof(f1486,plain,
( ~ spl0_45
| spl0_31
| spl0_60
| spl0_32
| ~ spl0_4
| spl0_27 ),
inference(avatar_split_clause,[],[f1482,f241,f142,f258,f470,f254,f334]) ).
fof(f1494,plain,
( ~ group_element(e_1)
| product(e_1,e_3,e_1)
| product(e_2,e_3,e_1)
| product(e_3,e_3,e_1)
| ~ group_element(e_3)
| spl0_31 ),
inference(resolution,[],[f255,f1]) ).
fof(f1522,plain,
( ~ group_element(e_4)
| product(e_1,e_1,e_4)
| product(e_2,e_1,e_4)
| product(e_3,e_1,e_4)
| ~ group_element(e_1)
| spl0_46 ),
inference(resolution,[],[f338,f1]) ).
fof(f1527,plain,
( ~ spl0_4
| spl0_52
| spl0_3
| spl0_64
| ~ spl0_45
| spl0_46 ),
inference(avatar_split_clause,[],[f1522,f337,f334,f509,f139,f383,f142]) ).
fof(f1549,plain,
( ~ spl0_21
| spl0_31
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f620,f383,f254,f215]) ).
fof(f1550,plain,
( ~ group_element(e_4)
| product(e_1,e_1,e_4)
| product(e_1,e_2,e_4)
| product(e_1,e_3,e_4)
| ~ group_element(e_1)
| spl0_44 ),
inference(resolution,[],[f409,f2]) ).
fof(f1551,plain,
( ~ group_element(e_4)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| spl0_44 ),
inference(resolution,[],[f409,f21]) ).
fof(f1588,plain,
( ~ product(e_2,e_3,e_3)
| ~ spl0_20 ),
inference(resolution,[],[f1321,f213]) ).
fof(f1594,plain,
( ~ spl0_95
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f1588,f212,f1014]) ).
fof(f1692,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_64 ),
inference(resolution,[],[f510,f29]) ).
fof(f1693,plain,
( ~ spl0_91
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f1692,f509,f949]) ).
fof(f1699,plain,
! [X0] :
( ~ product(X0,e_4,e_2)
| ~ group_element(e_3)
| product(X0,e_1,e_3)
| product(X0,e_2,e_3)
| product(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f31,f2]) ).
fof(f1709,definition,
( spl0_132
<=> ! [X0] :
( ~ product(X0,e_4,e_2)
| ~ group_element(X0)
| product(X0,e_3,e_3)
| product(X0,e_2,e_3)
| product(X0,e_1,e_3) ) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f1710,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product(X0,e_4,e_2)
| product(X0,e_3,e_3)
| product(X0,e_2,e_3)
| product(X0,e_1,e_3) )
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f1709]) ).
fof(f1711,plain,
( ~ spl0_48
| spl0_132 ),
inference(avatar_split_clause,[],[f1699,f1709,f371]) ).
fof(f1719,plain,
( ~ product(e_4,e_1,e_2)
| spl0_63 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f1726,plain,
( ~ product(e_2,e_4,e_2)
| product(e_2,e_3,e_3)
| product(e_2,e_2,e_3)
| product(e_2,e_1,e_3)
| ~ spl0_132 ),
inference(resolution,[],[f1710,f6]) ).
fof(f1732,plain,
( ~ group_element(e_2)
| product(e_1,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_3,e_1,e_2)
| ~ group_element(e_1)
| spl0_63 ),
inference(resolution,[],[f1719,f1]) ).
fof(f1736,plain,
( ~ spl0_4
| spl0_5
| spl0_6
| spl0_7
| ~ spl0_8
| spl0_63 ),
inference(avatar_split_clause,[],[f1732,f485,f154,f151,f148,f145,f142]) ).
fof(f1738,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_7 ),
inference(resolution,[],[f152,f27]) ).
fof(f1740,plain,
( ~ spl0_91
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f1738,f151,f949]) ).
fof(f1743,plain,
( ~ product(e_2,e_4,e_2)
| spl0_24 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f1744,plain,
( spl0_75
| spl0_37
| spl0_95
| ~ spl0_24
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f1726,f1709,f232,f1014,f282,f684]) ).
fof(f1750,definition,
( spl0_134
<=> product(e_4,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f1751,plain,
( ~ product(e_4,e_4,e_2)
| spl0_134 ),
inference(avatar_component_clause,[],[f1750]) ).
fof(f1763,plain,
( ~ spl0_21
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f579,f251,f215]) ).
fof(f1764,plain,
( ~ spl0_48
| spl0_20
| spl0_19
| spl0_21
| ~ spl0_4
| spl0_31 ),
inference(avatar_split_clause,[],[f1494,f254,f142,f215,f209,f212,f371]) ).
fof(f1767,plain,
( ~ product(e_2,e_4,e_4)
| spl0_43 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f1770,plain,
( ~ spl0_4
| spl0_51
| spl0_33
| spl0_64
| ~ spl0_45
| spl0_44 ),
inference(avatar_split_clause,[],[f1550,f331,f334,f509,f268,f380,f142]) ).
fof(f1793,plain,
( ! [X0] :
( ~ product(e_2,e_4,X0)
| ~ product(e_4,X0,e_2) )
| spl0_24 ),
inference(resolution,[],[f1743,f4]) ).
fof(f1797,plain,
( spl0_120
| spl0_24 ),
inference(avatar_split_clause,[],[f1793,f232,f1382]) ).
fof(f1799,plain,
( ~ spl0_33
| spl0_2
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f352,f232,f85,f268]) ).
fof(f1801,plain,
( ~ product(e_2,e_2,e_2)
| ~ spl0_37 ),
inference(resolution,[],[f283,f31]) ).
fof(f1830,plain,
( ~ product(e_2,e_4,e_1)
| ~ group_element(e_2)
| product(e_1,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_3,e_1,e_2)
| ~ group_element(e_1) ),
inference(resolution,[],[f1329,f1]) ).
fof(f1831,plain,
( ~ spl0_4
| spl0_5
| spl0_6
| spl0_7
| ~ spl0_8
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f1830,f196,f154,f151,f148,f145,f142]) ).
fof(f1834,plain,
( ! [X0] :
( ~ product(X0,e_4,e_4)
| ~ product(e_4,e_2,X0) )
| spl0_134 ),
inference(resolution,[],[f1751,f26]) ).
fof(f1838,plain,
( spl0_18
| spl0_134 ),
inference(avatar_split_clause,[],[f1834,f1750,f205]) ).
fof(f1841,plain,
( ~ group_element(e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| spl0_33 ),
inference(resolution,[],[f963,f21]) ).
fof(f1845,plain,
( ~ spl0_4
| spl0_36
| spl0_1
| spl0_11
| ~ spl0_8
| spl0_33 ),
inference(avatar_split_clause,[],[f1841,f268,f154,f165,f82,f279,f142]) ).
fof(f1869,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_11 ),
inference(resolution,[],[f166,f73]) ).
fof(f1871,plain,
( ~ spl0_91
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1869,f165,f949]) ).
fof(f1877,plain,
( ~ product(e_2,e_4,e_3)
| spl0_54 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f1881,plain,
( ~ group_element(e_2)
| product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| ~ group_element(e_4)
| spl0_59 ),
inference(resolution,[],[f467,f21]) ).
fof(f1885,plain,
( ~ spl0_45
| spl0_77
| spl0_61
| spl0_60
| ~ spl0_8
| spl0_59 ),
inference(avatar_split_clause,[],[f1881,f466,f154,f470,f479,f697,f334]) ).
fof(f1894,plain,
( ~ group_element(e_3)
| product(e_2,e_1,e_3)
| product(e_2,e_2,e_3)
| product(e_2,e_3,e_3)
| ~ group_element(e_2)
| spl0_54 ),
inference(resolution,[],[f1877,f2]) ).
fof(f1930,plain,
( $false
| ~ spl0_16
| ~ spl0_40
| ~ spl0_55 ),
inference(resolution,[],[f745,f408]) ).
fof(f1935,plain,
( ~ spl0_16
| ~ spl0_40
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f1930]) ).
fof(f1944,plain,
~ product(e_4,e_4,e_2),
inference(resolution,[],[f32,f25]) ).
fof(f1957,plain,
~ spl0_134,
inference(avatar_split_clause,[],[f1944,f1750]) ).
fof(f1996,plain,
( ~ group_element(e_2)
| product(e_4,e_1,e_2)
| product(e_4,e_2,e_2)
| product(e_4,e_3,e_2)
| ~ group_element(e_4)
| spl0_134 ),
inference(resolution,[],[f1751,f2]) ).
fof(f2003,plain,
( $false
| ~ spl0_37 ),
inference(resolution,[],[f1801,f25]) ).
fof(f2004,plain,
~ spl0_37,
inference(avatar_contradiction_clause,[],[f2003]) ).
fof(f2005,plain,
( ~ spl0_51
| ~ spl0_10
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1399,f218,f161,f380]) ).
fof(f2006,plain,
( ~ spl0_3
| spl0_2
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f558,f479,f85,f139]) ).
fof(f2009,plain,
( ~ spl0_45
| spl0_62
| spl0_61
| spl0_63
| ~ spl0_8
| spl0_134 ),
inference(avatar_split_clause,[],[f1996,f1750,f154,f485,f479,f482,f334]) ).
fof(f2011,plain,
( ~ spl0_4
| spl0_55
| spl0_26
| spl0_17
| ~ spl0_45
| spl0_44 ),
inference(avatar_split_clause,[],[f1551,f331,f334,f202,f238,f407,f142]) ).
fof(f2012,plain,
( ~ spl0_8
| spl0_95
| spl0_37
| spl0_75
| ~ spl0_48
| spl0_54 ),
inference(avatar_split_clause,[],[f1894,f404,f371,f684,f282,f1014,f154]) ).
fof(f2019,plain,
( ~ spl0_45
| spl0_16
| spl0_15
| spl0_17
| ~ spl0_4
| spl0_27 ),
inference(avatar_split_clause,[],[f1481,f241,f142,f202,f196,f199,f334]) ).
fof(f2039,plain,
( ~ group_element(e_1)
| product(e_2,e_1,e_1)
| product(e_2,e_2,e_1)
| product(e_2,e_3,e_1)
| ~ group_element(e_2)
| spl0_15 ),
inference(resolution,[],[f1016,f2]) ).
fof(f2043,plain,
( ~ spl0_8
| spl0_19
| spl0_2
| spl0_47
| ~ spl0_4
| spl0_15 ),
inference(avatar_split_clause,[],[f2039,f196,f142,f359,f85,f209,f154]) ).
fof(f2044,plain,
( ~ group_element(e_1)
| product(e_1,e_2,e_1)
| product(e_2,e_2,e_1)
| product(e_3,e_2,e_1)
| ~ group_element(e_2)
| spl0_60 ),
inference(resolution,[],[f1198,f1]) ).
fof(f2048,plain,
( ~ spl0_8
| spl0_10
| spl0_2
| spl0_11
| ~ spl0_4
| spl0_60 ),
inference(avatar_split_clause,[],[f2044,f470,f142,f165,f85,f161,f154]) ).
fof(f2123,plain,
( ~ product(e_3,e_2,e_1)
| ~ product(e_2,e_2,e_4)
| ~ spl0_77 ),
inference(resolution,[],[f698,f51]) ).
fof(f2124,plain,
( ~ spl0_9
| ~ spl0_10
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f2123,f697,f161,f158]) ).
fof(f2134,plain,
( ~ group_element(e_1)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ group_element(e_2)
| spl0_3 ),
inference(resolution,[],[f140,f21]) ).
fof(f2138,plain,
( ~ spl0_8
| spl0_75
| spl0_6
| spl0_47
| ~ spl0_4
| spl0_3 ),
inference(avatar_split_clause,[],[f2134,f139,f142,f359,f148,f684,f154]) ).
fof(f2144,plain,
( ~ product(e_2,e_1,e_3)
| spl0_1
| ~ spl0_5 ),
inference(resolution,[],[f146,f721]) ).
fof(f2148,plain,
( ~ product(e_2,e_1,e_1)
| ~ product(e_1,e_2,e_3)
| ~ spl0_5 ),
inference(resolution,[],[f146,f51]) ).
fof(f2150,plain,
( ~ spl0_36
| ~ spl0_47
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f2148,f145,f359,f279]) ).
fof(f2153,plain,
( ~ spl0_75
| spl0_1
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f2144,f145,f82,f684]) ).
fof(f2353,plain,
( ~ product(e_2,e_4,e_3)
| ~ spl0_62
| ~ spl0_120 ),
inference(resolution,[],[f1383,f483]) ).
fof(f2358,plain,
( ~ spl0_54
| ~ spl0_62
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f2353,f1382,f482,f404]) ).
fof(f2363,plain,
( ~ spl0_19
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f1236,f377,f209]) ).
fof(f2389,plain,
( ~ product(e_2,e_4,e_4)
| spl0_27
| ~ spl0_63 ),
inference(resolution,[],[f486,f1483]) ).
fof(f2396,plain,
( ~ product(e_2,e_1,e_1)
| ~ product(e_1,e_2,e_4)
| ~ spl0_63 ),
inference(resolution,[],[f486,f51]) ).
fof(f2398,plain,
( ~ spl0_33
| ~ spl0_47
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f2396,f485,f359,f268]) ).
fof(f2399,plain,
( ~ spl0_43
| spl0_27
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f2389,f485,f241,f328]) ).
fof(f2400,plain,
( ~ group_element(e_4)
| product(e_2,e_1,e_4)
| product(e_2,e_2,e_4)
| product(e_2,e_3,e_4)
| ~ group_element(e_2)
| spl0_43 ),
inference(resolution,[],[f1767,f2]) ).
fof(f2405,plain,
( ~ spl0_8
| spl0_50
| spl0_9
| spl0_3
| ~ spl0_45
| spl0_43 ),
inference(avatar_split_clause,[],[f2400,f328,f334,f139,f158,f377,f154]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f87]) ).
cnf(s2,plain,
( spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f98]) ).
cnf(s5,plain,
( ~ spl0_8
| spl0_12 ),
inference(sat_conversion,[],[f171]) ).
cnf(s7,plain,
( ~ spl0_8
| spl0_14 ),
inference(sat_conversion,[],[f179]) ).
cnf(s8,plain,
spl0_4,
inference(sat_conversion,[],[f190]) ).
cnf(s12,plain,
spl0_8,
inference(sat_conversion,[],[f226]) ).
cnf(s15,plain,
( spl0_5
| spl0_6
| spl0_7
| ~ spl0_14
| ~ spl0_32 ),
inference(sat_conversion,[],[f260]) ).
cnf(s19,plain,
( spl0_2
| spl0_10
| spl0_11
| ~ spl0_12
| spl0_40 ),
inference(sat_conversion,[],[f294]) ).
cnf(s20,plain,
( spl0_32
| spl0_40 ),
inference(sat_conversion,[],[f309]) ).
cnf(s23,plain,
( spl0_27
| ~ spl0_46 ),
inference(sat_conversion,[],[f340]) ).
cnf(s26,plain,
spl0_45,
inference(sat_conversion,[],[f387]) ).
cnf(s27,plain,
spl0_48,
inference(sat_conversion,[],[f392]) ).
cnf(s36,plain,
( ~ spl0_8
| spl0_58 ),
inference(sat_conversion,[],[f464]) ).
cnf(s39,plain,
( spl0_1
| spl0_7
| ~ spl0_17
| spl0_30
| ~ spl0_58 ),
inference(sat_conversion,[],[f490]) ).
cnf(s56,plain,
( ~ spl0_31
| ~ spl0_62 ),
inference(sat_conversion,[],[f603]) ).
cnf(s73,plain,
( ~ spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f718]) ).
cnf(s77,plain,
( ~ spl0_17
| ~ spl0_40 ),
inference(sat_conversion,[],[f748]) ).
cnf(s85,plain,
( spl0_22
| ~ spl0_31 ),
inference(sat_conversion,[],[f869]) ).
cnf(s95,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_63 ),
inference(sat_conversion,[],[f895]) ).
cnf(s96,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_4
| spl0_5
| spl0_6
| spl0_7
| ~ spl0_8 ),
inference(sat_conversion,[],[f896]) ).
cnf(s115,plain,
( ~ spl0_5
| ~ spl0_87 ),
inference(sat_conversion,[],[f970]) ).
cnf(s116,plain,
( ~ spl0_18
| ~ spl0_59 ),
inference(sat_conversion,[],[f992]) ).
cnf(s121,plain,
( spl0_1
| ~ spl0_6 ),
inference(sat_conversion,[],[f1010]) ).
cnf(s127,plain,
( ~ spl0_4
| spl0_10
| spl0_16
| spl0_20
| ~ spl0_48
| spl0_87 ),
inference(sat_conversion,[],[f1022]) ).
cnf(s128,plain,
( ~ spl0_19
| ~ spl0_95 ),
inference(sat_conversion,[],[f1026]) ).
cnf(s171,plain,
( spl0_17
| ~ spl0_26
| ~ spl0_60 ),
inference(sat_conversion,[],[f1288]) ).
cnf(s179,plain,
spl0_91,
inference(sat_conversion,[],[f1363]) ).
cnf(s188,plain,
( ~ spl0_10
| ~ spl0_21 ),
inference(sat_conversion,[],[f1409]) ).
cnf(s198,plain,
( spl0_27
| ~ spl0_44 ),
inference(sat_conversion,[],[f1475]) ).
cnf(s200,plain,
( spl0_2
| ~ spl0_33
| ~ spl0_61 ),
inference(sat_conversion,[],[f1476]) ).
cnf(s201,plain,
~ spl0_27,
inference(sat_conversion,[],[f1477]) ).
cnf(s212,plain,
( ~ spl0_4
| spl0_27
| spl0_31
| spl0_32
| ~ spl0_45
| spl0_60 ),
inference(sat_conversion,[],[f1486]) ).
cnf(s218,plain,
( spl0_3
| ~ spl0_4
| ~ spl0_45
| spl0_46
| spl0_52
| spl0_64 ),
inference(sat_conversion,[],[f1527]) ).
cnf(s222,plain,
( ~ spl0_21
| spl0_31
| ~ spl0_52 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s228,plain,
( ~ spl0_20
| ~ spl0_95 ),
inference(sat_conversion,[],[f1594]) ).
cnf(s241,plain,
( ~ spl0_64
| ~ spl0_91 ),
inference(sat_conversion,[],[f1693]) ).
cnf(s245,plain,
( ~ spl0_48
| spl0_132 ),
inference(sat_conversion,[],[f1711]) ).
cnf(s248,plain,
( ~ spl0_4
| spl0_5
| spl0_6
| spl0_7
| ~ spl0_8
| spl0_63 ),
inference(sat_conversion,[],[f1736]) ).
cnf(s250,plain,
( ~ spl0_7
| ~ spl0_91 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s256,plain,
( ~ spl0_24
| spl0_37
| spl0_75
| spl0_95
| ~ spl0_132 ),
inference(sat_conversion,[],[f1744]) ).
cnf(s268,plain,
( ~ spl0_21
| ~ spl0_30 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s269,plain,
( ~ spl0_4
| spl0_19
| spl0_20
| spl0_21
| spl0_31
| ~ spl0_48 ),
inference(sat_conversion,[],[f1764]) ).
cnf(s274,plain,
( ~ spl0_4
| spl0_33
| spl0_44
| ~ spl0_45
| spl0_51
| spl0_64 ),
inference(sat_conversion,[],[f1770]) ).
cnf(s286,plain,
( spl0_24
| spl0_120 ),
inference(sat_conversion,[],[f1797]) ).
cnf(s288,plain,
( spl0_2
| ~ spl0_24
| ~ spl0_33 ),
inference(sat_conversion,[],[f1799]) ).
cnf(s301,plain,
( ~ spl0_4
| spl0_5
| spl0_6
| spl0_7
| ~ spl0_8
| ~ spl0_15 ),
inference(sat_conversion,[],[f1831]) ).
cnf(s303,plain,
( spl0_18
| spl0_134 ),
inference(sat_conversion,[],[f1838]) ).
cnf(s306,plain,
( spl0_1
| ~ spl0_4
| ~ spl0_8
| spl0_11
| spl0_33
| spl0_36 ),
inference(sat_conversion,[],[f1845]) ).
cnf(s310,plain,
( ~ spl0_11
| ~ spl0_91 ),
inference(sat_conversion,[],[f1871]) ).
cnf(s316,plain,
( ~ spl0_8
| ~ spl0_45
| spl0_59
| spl0_60
| spl0_61
| spl0_77 ),
inference(sat_conversion,[],[f1885]) ).
cnf(s321,plain,
( ~ spl0_16
| ~ spl0_40
| ~ spl0_55 ),
inference(sat_conversion,[],[f1935]) ).
cnf(s325,plain,
~ spl0_134,
inference(sat_conversion,[],[f1957]) ).
cnf(s335,plain,
~ spl0_37,
inference(sat_conversion,[],[f2004]) ).
cnf(s338,plain,
( ~ spl0_10
| ~ spl0_22
| ~ spl0_51 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s344,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_61 ),
inference(sat_conversion,[],[f2006]) ).
cnf(s347,plain,
( ~ spl0_8
| ~ spl0_45
| spl0_61
| spl0_62
| spl0_63
| spl0_134 ),
inference(sat_conversion,[],[f2009]) ).
cnf(s349,plain,
( ~ spl0_4
| spl0_17
| spl0_26
| spl0_44
| ~ spl0_45
| spl0_55 ),
inference(sat_conversion,[],[f2011]) ).
cnf(s350,plain,
( ~ spl0_8
| spl0_37
| ~ spl0_48
| spl0_54
| spl0_75
| spl0_95 ),
inference(sat_conversion,[],[f2012]) ).
cnf(s357,plain,
( ~ spl0_4
| spl0_15
| spl0_16
| spl0_17
| spl0_27
| ~ spl0_45 ),
inference(sat_conversion,[],[f2019]) ).
cnf(s381,plain,
( spl0_2
| ~ spl0_4
| ~ spl0_8
| spl0_15
| spl0_19
| spl0_47 ),
inference(sat_conversion,[],[f2043]) ).
cnf(s389,plain,
( spl0_2
| ~ spl0_4
| ~ spl0_8
| spl0_10
| spl0_11
| spl0_60 ),
inference(sat_conversion,[],[f2048]) ).
cnf(s399,plain,
( ~ spl0_9
| ~ spl0_10
| ~ spl0_77 ),
inference(sat_conversion,[],[f2124]) ).
cnf(s404,plain,
( spl0_3
| ~ spl0_4
| spl0_6
| ~ spl0_8
| spl0_47
| spl0_75 ),
inference(sat_conversion,[],[f2138]) ).
cnf(s405,plain,
( ~ spl0_5
| ~ spl0_36
| ~ spl0_47 ),
inference(sat_conversion,[],[f2150]) ).
cnf(s407,plain,
( spl0_1
| ~ spl0_5
| ~ spl0_75 ),
inference(sat_conversion,[],[f2153]) ).
cnf(s440,plain,
( ~ spl0_54
| ~ spl0_62
| ~ spl0_120 ),
inference(sat_conversion,[],[f2358]) ).
cnf(s444,plain,
( ~ spl0_19
| ~ spl0_50 ),
inference(sat_conversion,[],[f2363]) ).
cnf(s455,plain,
( ~ spl0_33
| ~ spl0_47
| ~ spl0_63 ),
inference(sat_conversion,[],[f2398]) ).
cnf(s456,plain,
( spl0_27
| ~ spl0_43
| ~ spl0_63 ),
inference(sat_conversion,[],[f2399]) ).
cnf(s457,plain,
( spl0_3
| ~ spl0_8
| spl0_9
| spl0_43
| ~ spl0_45
| spl0_50 ),
inference(sat_conversion,[],[f2405]) ).
cnf(s460,plain,
spl0_18,
inference(rat,[],[s303,s325]) ).
cnf(s464,plain,
( ~ spl0_24
| spl0_75
| spl0_95
| ~ spl0_132 ),
inference(rat,[],[s256,s335]) ).
cnf(s465,plain,
~ spl0_44,
inference(rat,[],[s198,s201]) ).
cnf(s468,plain,
~ spl0_11,
inference(rat,[],[s310,s179]) ).
cnf(s469,plain,
~ spl0_7,
inference(rat,[],[s250,s179]) ).
cnf(s470,plain,
~ spl0_64,
inference(rat,[],[s241,s179]) ).
cnf(s493,plain,
~ spl0_59,
inference(rat,[],[s116,s460]) ).
cnf(s495,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_4
| spl0_5
| spl0_6
| ~ spl0_8 ),
inference(rat,[],[s96,s469]) ).
cnf(s498,plain,
( spl0_1
| ~ spl0_17
| spl0_30
| ~ spl0_58 ),
inference(rat,[],[s39,s469]) ).
cnf(s500,plain,
spl0_132,
inference(rat,[],[s245,s27]) ).
cnf(s519,plain,
~ spl0_46,
inference(rat,[],[s23,s201]) ).
cnf(s521,plain,
( spl0_2
| spl0_10
| ~ spl0_12
| spl0_40 ),
inference(rat,[],[s19,s468]) ).
cnf(s523,plain,
( spl0_5
| spl0_6
| ~ spl0_14
| ~ spl0_32 ),
inference(rat,[],[s15,s469]) ).
cnf(s528,plain,
spl0_58,
inference(rat,[],[s36,s12]) ).
cnf(s538,plain,
spl0_14,
inference(rat,[],[s7,s12]) ).
cnf(s540,plain,
spl0_12,
inference(rat,[],[s5,s12]) ).
cnf(s543,plain,
( spl0_5
| spl0_3
| spl0_1 ),
inference(rat,[],[s457,s444,s399,s381,s316,s455,s200,s274,s338,s85,s389,s212,s171,s349,s321,s357,s77,s456,s20,s301,s248,s523,s121,s2,s12,s26,s8,s493,s465,s470,s468,s201,s469,s538]) ).
cnf(s544,plain,
( spl0_3
| spl0_1 ),
inference(rat,[],[s269,s128,s228,s222,s350,s56,s440,s347,s286,s455,s200,s288,s306,s405,s404,s407,s543,s218,s121,s2,s8,s27,s335,s12,s26,s325,s468,s519,s470]) ).
cnf(s545,plain,
( spl0_95
| spl0_1 ),
inference(rat,[],[s440,s286,s350,s464,s347,s95,s344,s2,s407,s495,s544,s121,s335,s27,s12,s500,s8,s325,s26]) ).
cnf(s546,plain,
spl0_1,
inference(rat,[],[s349,s171,s321,s389,s521,s127,s498,s188,s268,s269,s128,s228,s545,s56,s115,s347,s344,s495,s95,s544,s2,s121,s8,s465,s26,s12,s468,s540,s27,s528,s325]) ).
cnf(s547,plain,
spl0_2,
inference(rat,[],[s73,s546]) ).
cnf(s548,plain,
$false,
inference(rat,[],[s1,s547,s546]) ).
fof(f2406,plain,
$false,
inference(avatar_sat_refutation,[],[s548]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP127-4.004 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n017.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 09:22:05 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 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.12/1.33 % (2281775)Input is clausal, will run a generic CNF schedule.
% 3.12/1.33 % (2281783)lrs+10_1_sil=8000:sp=occurrence:random_seed=4171455137:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.12/1.33 % (2281783)Refutation not found, incomplete strategy
% 3.12/1.33 % (2281783)------------------------------
% 3.12/1.33 % (2281783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.12/1.33 % (2281783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/1.33 % (2281783)CaDiCaL version: 2.1.3
% 3.12/1.33 % (2281783)Termination reason: Refutation not found, incomplete strategy
% 3.12/1.33 % (2281783)Time elapsed: 0.001 s
% 3.12/1.33 % (2281783)Peak memory usage: 87 MB
% 3.12/1.33 % (2281786)dis-21_1_sil=8000:lcm=predicate:random_seed=1470807799: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.12/1.33 % (2281784)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3133048854:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.12/1.33 % (2281785)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3892524379:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.12/1.33 % (2281782)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3083244858:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.12/1.33 % (2281781)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3752312943:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.12/1.33 % (2281780)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=1292951568:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.12/1.33 % (2281786)First to succeed.
% 3.12/1.33 % (2281786)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2281775"
% 3.12/1.33 % (2281785)Also succeeded, but the first one will report.
% 3.12/1.33 % (2281784)Instruction limit reached!
% 3.12/1.33 % (2281784)------------------------------
% 3.12/1.33 % (2281784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.12/1.33 % (2281784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/1.33 % (2281784)CaDiCaL version: 2.1.3
% 3.12/1.33 % (2281784)Termination reason: Instruction limit
% 3.12/1.33 % (2281784)Termination phase: Saturation
% 3.12/1.33 % (2281784)Time elapsed: 0.056 s
% 3.12/1.33 % (2281784)Peak memory usage: 87 MB
% 3.12/1.33 % (2281784)Instructions burned: 115 (million)
% 3.12/1.33 % (2281783)------------------------------
% 3.12/1.33 % (2281783)------------------------------
% 3.12/1.33 % (2281795)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3439808448: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.12/1.33 % (2281795)Refutation not found, incomplete strategy
% 3.12/1.33 % (2281795)------------------------------
% 3.12/1.33 % (2281795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.12/1.33 % (2281795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/1.33 % (2281795)CaDiCaL version: 2.1.3
% 3.12/1.33 % (2281795)Termination reason: Refutation not found, incomplete strategy
% 3.12/1.33 % (2281795)Time elapsed: 0.001 s
% 3.12/1.33 % (2281795)Peak memory usage: 87 MB
% 3.12/1.33 % (2281795)Instructions burned: 1 (million)
% 3.12/1.33 % (2281794)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=1528342157:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 3.12/1.33 % (2281794)Also succeeded, but the first one will report.
% 3.12/1.33 % (2281786)Refutation found. Thanks to Tanya!
% 3.12/1.33 % SZS status Unsatisfiable for theBenchmark
% 3.12/1.33 % SZS output start Proof for theBenchmark
% See solution above
% 3.95/1.53 % (2281786)------------------------------
% 3.95/1.53 % (2281786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.95/1.53 % (2281786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.95/1.53 % (2281786)CaDiCaL version: 2.1.3
% 3.95/1.53 % (2281786)Termination reason: Refutation
% 3.95/1.53 % (2281786)Time elapsed: 0.048 s
% 3.95/1.53 % (2281786)Peak memory usage: 90 MB
% 3.95/1.53 % (2281786)Instructions burned: 72 (million)
% 3.95/1.53 % (2281786)------------------------------
% 3.95/1.53 % (2281786)------------------------------
% 3.95/1.53 % (2281775)Success in time 0.466 s
% 3.95/1.53 % Vampire exiting
%------------------------------------------------------------------------------