%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP127-3.004 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 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:16:49 AM UTC 2026
% Result : Unsatisfiable 0.14s 0.47s
% Output : Refutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 54
% Syntax : Number of formulae : 261 ( 59 unt; 33 def)
% Number of atoms : 591 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 575 ( 245 ~; 297 |; 0 &)
% ( 33 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 37 ( 36 usr; 34 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 33 ( 0 sgn 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f22,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
fof(f23,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
fof(f24,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
fof(f25,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
fof(f26,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f27,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f28,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f29,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
fof(f30,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f31,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f32,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
fof(f33,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
fof(f34,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f35,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
fof(f36,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
fof(f37,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
fof(f38,axiom,
! [X0,X1] :
( ~ group_element(X0)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
fof(f40,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X2)
| ~ product(X0,X3,X2)
| equalish(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f41,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X2)
| ~ product(X3,X1,X2)
| equalish(X0,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_left_cancellation) ).
fof(f42,axiom,
! [X0] : product(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_idempotence) ).
fof(f43,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X2)
| ~ product(X2,X0,X3)
| product(X3,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3) ).
fof(f50,plain,
! [X0,X1] :
( ~ product(X0,X1,X0)
| equalish(X0,X1) ),
inference(resolution,[],[f40,f42]) ).
fof(f51,plain,
! [X0,X1] :
( ~ product(X0,X1,X1)
| equalish(X1,X0) ),
inference(resolution,[],[f41,f42]) ).
fof(f137,plain,
! [X0] :
( ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ),
inference(resolution,[],[f38,f22]) ).
fof(f138,plain,
! [X0] :
( ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ),
inference(resolution,[],[f38,f23]) ).
fof(f139,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ),
inference(resolution,[],[f38,f24]) ).
fof(f140,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ),
inference(resolution,[],[f38,f25]) ).
fof(f155,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4) ),
inference(resolution,[],[f137,f23]) ).
fof(f156,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_4) ),
inference(resolution,[],[f137,f24]) ).
fof(f157,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4) ),
inference(resolution,[],[f137,f25]) ).
fof(f159,definition,
( spl0_17
<=> product(e_1,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f161,plain,
( product(e_1,e_4,e_4)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f159]) ).
fof(f163,definition,
( spl0_18
<=> product(e_1,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f165,plain,
( product(e_1,e_4,e_3)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f163]) ).
fof(f167,definition,
( spl0_19
<=> product(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f169,plain,
( product(e_1,e_4,e_2)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f171,definition,
( spl0_20
<=> product(e_1,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f173,plain,
( product(e_1,e_4,e_1)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f171]) ).
fof(f174,plain,
( spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f157,f171,f167,f163,f159]) ).
fof(f176,definition,
( spl0_21
<=> product(e_1,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f178,plain,
( product(e_1,e_3,e_4)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f180,definition,
( spl0_22
<=> product(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f182,plain,
( product(e_1,e_3,e_3)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f184,definition,
( spl0_23
<=> product(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f186,plain,
( product(e_1,e_3,e_2)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f188,definition,
( spl0_24
<=> product(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f190,plain,
( product(e_1,e_3,e_1)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f191,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(avatar_split_clause,[],[f156,f188,f184,f180,f176]) ).
fof(f193,definition,
( spl0_25
<=> product(e_1,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f195,plain,
( product(e_1,e_2,e_4)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f193]) ).
fof(f197,definition,
( spl0_26
<=> product(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f199,plain,
( product(e_1,e_2,e_3)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f197]) ).
fof(f201,definition,
( spl0_27
<=> product(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f203,plain,
( product(e_1,e_2,e_2)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f205,definition,
( spl0_28
<=> product(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f207,plain,
( product(e_1,e_2,e_1)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f208,plain,
( spl0_25
| spl0_26
| spl0_27
| spl0_28 ),
inference(avatar_split_clause,[],[f155,f205,f201,f197,f193]) ).
fof(f213,plain,
( equalish(e_4,e_1)
| ~ spl0_17 ),
inference(resolution,[],[f161,f51]) ).
fof(f214,plain,
( $false
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f213,f35]) ).
fof(f215,plain,
~ spl0_17,
inference(avatar_contradiction_clause,[],[f214]) ).
fof(f218,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_4) ),
inference(resolution,[],[f138,f24]) ).
fof(f219,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4) ),
inference(resolution,[],[f138,f25]) ).
fof(f221,definition,
( spl0_29
<=> product(e_2,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f223,plain,
( product(e_2,e_4,e_4)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f225,definition,
( spl0_30
<=> product(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f227,plain,
( product(e_2,e_4,e_3)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f229,definition,
( spl0_31
<=> product(e_2,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f231,plain,
( product(e_2,e_4,e_2)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f233,definition,
( spl0_32
<=> product(e_2,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f235,plain,
( product(e_2,e_4,e_1)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f236,plain,
( spl0_29
| spl0_30
| spl0_31
| spl0_32 ),
inference(avatar_split_clause,[],[f219,f233,f229,f225,f221]) ).
fof(f238,definition,
( spl0_33
<=> product(e_2,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f240,plain,
( product(e_2,e_3,e_4)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f242,definition,
( spl0_34
<=> product(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f244,plain,
( product(e_2,e_3,e_3)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f246,definition,
( spl0_35
<=> product(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f247,plain,
( ~ product(e_2,e_3,e_2)
| spl0_35 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f248,plain,
( product(e_2,e_3,e_2)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f250,definition,
( spl0_36
<=> product(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f252,plain,
( product(e_2,e_3,e_1)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f253,plain,
( spl0_33
| spl0_34
| spl0_35
| spl0_36 ),
inference(avatar_split_clause,[],[f218,f250,f246,f242,f238]) ).
fof(f272,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4) ),
inference(resolution,[],[f139,f23]) ).
fof(f274,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| product(e_3,e_4,e_4) ),
inference(resolution,[],[f139,f25]) ).
fof(f276,definition,
( spl0_41
<=> product(e_3,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f278,plain,
( product(e_3,e_4,e_4)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f280,definition,
( spl0_42
<=> product(e_3,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f281,plain,
( ~ product(e_3,e_4,e_3)
| spl0_42 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f282,plain,
( product(e_3,e_4,e_3)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f284,definition,
( spl0_43
<=> product(e_3,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f286,plain,
( product(e_3,e_4,e_2)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f288,definition,
( spl0_44
<=> product(e_3,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f290,plain,
( product(e_3,e_4,e_1)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f291,plain,
( spl0_41
| spl0_42
| spl0_43
| spl0_44 ),
inference(avatar_split_clause,[],[f274,f288,f284,f280,f276]) ).
fof(f293,definition,
( spl0_45
<=> product(e_3,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f295,plain,
( product(e_3,e_2,e_4)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f297,definition,
( spl0_46
<=> product(e_3,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f299,plain,
( product(e_3,e_2,e_3)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f301,definition,
( spl0_47
<=> product(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f303,plain,
( product(e_3,e_2,e_2)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f305,definition,
( spl0_48
<=> product(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f307,plain,
( product(e_3,e_2,e_1)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f308,plain,
( spl0_45
| spl0_46
| spl0_47
| spl0_48 ),
inference(avatar_split_clause,[],[f272,f305,f301,f297,f293]) ).
fof(f332,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_4) ),
inference(resolution,[],[f140,f24]) ).
fof(f335,definition,
( spl0_53
<=> product(e_4,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f336,plain,
( ~ product(e_4,e_3,e_4)
| spl0_53 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f337,plain,
( product(e_4,e_3,e_4)
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f339,definition,
( spl0_54
<=> product(e_4,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f341,plain,
( product(e_4,e_3,e_3)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f343,definition,
( spl0_55
<=> product(e_4,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f344,plain,
( ~ product(e_4,e_3,e_2)
| spl0_55 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f345,plain,
( product(e_4,e_3,e_2)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f347,definition,
( spl0_56
<=> product(e_4,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f349,plain,
( product(e_4,e_3,e_1)
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f350,plain,
( spl0_53
| spl0_54
| spl0_55
| spl0_56 ),
inference(avatar_split_clause,[],[f332,f347,f343,f339,f335]) ).
fof(f352,definition,
( spl0_57
<=> product(e_4,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f353,plain,
( ~ product(e_4,e_2,e_4)
| spl0_57 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f354,plain,
( product(e_4,e_2,e_4)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f397,plain,
( equalish(e_4,e_2)
| ~ spl0_29 ),
inference(resolution,[],[f223,f51]) ).
fof(f398,plain,
( $false
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f397,f36]) ).
fof(f399,plain,
~ spl0_29,
inference(avatar_contradiction_clause,[],[f398]) ).
fof(f416,plain,
( equalish(e_4,e_3)
| ~ spl0_41 ),
inference(resolution,[],[f278,f51]) ).
fof(f417,plain,
( $false
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f416,f37]) ).
fof(f418,plain,
~ spl0_41,
inference(avatar_contradiction_clause,[],[f417]) ).
fof(f423,plain,
( equalish(e_3,e_4)
| ~ spl0_42 ),
inference(resolution,[],[f282,f50]) ).
fof(f424,plain,
( $false
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f423,f34]) ).
fof(f425,plain,
~ spl0_42,
inference(avatar_contradiction_clause,[],[f424]) ).
fof(f429,plain,
( ! [X0] :
( ~ product(e_2,e_3,X0)
| product(X0,e_3,e_4) )
| ~ spl0_43 ),
inference(resolution,[],[f286,f43]) ).
fof(f430,plain,
( product(e_4,e_3,e_4)
| ~ spl0_33
| ~ spl0_43 ),
inference(resolution,[],[f429,f240]) ).
fof(f435,plain,
( ! [X0] :
( ~ product(e_4,e_3,X0)
| product(X0,e_3,e_2) )
| ~ spl0_45 ),
inference(resolution,[],[f295,f43]) ).
fof(f447,plain,
( equalish(e_4,e_3)
| ~ spl0_53 ),
inference(resolution,[],[f337,f50]) ).
fof(f448,plain,
( $false
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f447,f37]) ).
fof(f449,plain,
~ spl0_53,
inference(avatar_contradiction_clause,[],[f448]) ).
fof(f452,plain,
( $false
| ~ spl0_33
| ~ spl0_43
| spl0_53 ),
inference(forward_subsumption_resolution,[],[f430,f336]) ).
fof(f453,plain,
( ~ spl0_33
| ~ spl0_43
| spl0_53 ),
inference(avatar_contradiction_clause,[],[f452]) ).
fof(f459,plain,
( equalish(e_3,e_2)
| ~ spl0_34 ),
inference(resolution,[],[f244,f51]) ).
fof(f460,plain,
( $false
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f459,f33]) ).
fof(f461,plain,
~ spl0_34,
inference(avatar_contradiction_clause,[],[f460]) ).
fof(f467,plain,
( equalish(e_2,e_3)
| ~ spl0_35 ),
inference(resolution,[],[f248,f50]) ).
fof(f468,plain,
( $false
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f467,f30]) ).
fof(f469,plain,
~ spl0_35,
inference(avatar_contradiction_clause,[],[f468]) ).
fof(f476,plain,
( ! [X0] :
( ~ product(e_1,e_2,X0)
| product(X0,e_2,e_3) )
| ~ spl0_36 ),
inference(resolution,[],[f252,f43]) ).
fof(f479,plain,
( product(e_3,e_2,e_3)
| ~ spl0_26
| ~ spl0_36 ),
inference(resolution,[],[f199,f476]) ).
fof(f484,plain,
( spl0_46
| ~ spl0_26
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f479,f250,f197,f297]) ).
fof(f490,plain,
( equalish(e_2,e_1)
| ~ spl0_27 ),
inference(resolution,[],[f203,f51]) ).
fof(f491,plain,
( $false
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f490,f29]) ).
fof(f492,plain,
~ spl0_27,
inference(avatar_contradiction_clause,[],[f491]) ).
fof(f498,plain,
( equalish(e_1,e_2)
| ~ spl0_28 ),
inference(resolution,[],[f207,f50]) ).
fof(f499,plain,
( $false
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f498,f26]) ).
fof(f500,plain,
~ spl0_28,
inference(avatar_contradiction_clause,[],[f499]) ).
fof(f514,plain,
( ! [X0] :
( ~ product(e_1,e_3,X0)
| product(X0,e_3,e_4) )
| ~ spl0_44 ),
inference(resolution,[],[f290,f43]) ).
fof(f515,plain,
( product(e_4,e_3,e_4)
| ~ spl0_21
| ~ spl0_44 ),
inference(resolution,[],[f514,f178]) ).
fof(f516,plain,
( $false
| ~ spl0_21
| ~ spl0_44
| spl0_53 ),
inference(forward_subsumption_resolution,[],[f515,f336]) ).
fof(f517,plain,
( ~ spl0_21
| ~ spl0_44
| spl0_53 ),
inference(avatar_contradiction_clause,[],[f516]) ).
fof(f523,plain,
( equalish(e_3,e_1)
| ~ spl0_22 ),
inference(resolution,[],[f182,f51]) ).
fof(f524,plain,
( $false
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f523,f32]) ).
fof(f525,plain,
~ spl0_22,
inference(avatar_contradiction_clause,[],[f524]) ).
fof(f537,plain,
( equalish(e_3,e_4)
| ~ spl0_54 ),
inference(resolution,[],[f341,f51]) ).
fof(f538,plain,
( $false
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f537,f34]) ).
fof(f539,plain,
~ spl0_54,
inference(avatar_contradiction_clause,[],[f538]) ).
fof(f547,plain,
( equalish(e_1,e_3)
| ~ spl0_24 ),
inference(resolution,[],[f190,f50]) ).
fof(f548,plain,
( $false
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f547,f27]) ).
fof(f549,plain,
~ spl0_24,
inference(avatar_contradiction_clause,[],[f548]) ).
fof(f559,plain,
( product(e_2,e_3,e_2)
| ~ spl0_45
| ~ spl0_55 ),
inference(resolution,[],[f345,f435]) ).
fof(f563,plain,
( ! [X0] :
( ~ product(e_2,e_4,X0)
| product(X0,e_4,e_3) )
| ~ spl0_55 ),
inference(resolution,[],[f345,f43]) ).
fof(f564,plain,
( $false
| spl0_35
| ~ spl0_45
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f559,f247]) ).
fof(f565,plain,
( spl0_35
| ~ spl0_45
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f564]) ).
fof(f568,plain,
( product(e_3,e_4,e_3)
| ~ spl0_30
| ~ spl0_55 ),
inference(resolution,[],[f563,f227]) ).
fof(f569,plain,
( $false
| ~ spl0_30
| spl0_42
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f568,f281]) ).
fof(f570,plain,
( ~ spl0_30
| spl0_42
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f569]) ).
fof(f576,plain,
( equalish(e_2,e_4)
| ~ spl0_31 ),
inference(resolution,[],[f231,f50]) ).
fof(f577,plain,
( $false
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f576,f31]) ).
fof(f578,plain,
~ spl0_31,
inference(avatar_contradiction_clause,[],[f577]) ).
fof(f585,plain,
( ! [X0] :
( ~ product(e_1,e_2,X0)
| product(X0,e_2,e_4) )
| ~ spl0_32 ),
inference(resolution,[],[f235,f43]) ).
fof(f586,plain,
( product(e_4,e_2,e_4)
| ~ spl0_25
| ~ spl0_32 ),
inference(resolution,[],[f585,f195]) ).
fof(f591,plain,
( equalish(e_2,e_3)
| ~ spl0_47 ),
inference(resolution,[],[f303,f51]) ).
fof(f592,plain,
( $false
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f591,f30]) ).
fof(f593,plain,
~ spl0_47,
inference(avatar_contradiction_clause,[],[f592]) ).
fof(f597,plain,
( ! [X0] :
( ~ product(e_1,e_3,X0)
| product(X0,e_3,e_2) )
| ~ spl0_48 ),
inference(resolution,[],[f307,f43]) ).
fof(f598,plain,
( product(e_2,e_3,e_2)
| ~ spl0_23
| ~ spl0_48 ),
inference(resolution,[],[f597,f186]) ).
fof(f599,plain,
( $false
| ~ spl0_23
| spl0_35
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f598,f247]) ).
fof(f600,plain,
( ~ spl0_23
| spl0_35
| ~ spl0_48 ),
inference(avatar_contradiction_clause,[],[f599]) ).
fof(f625,plain,
( ! [X0] :
( ~ product(e_1,e_4,X0)
| product(X0,e_4,e_3) )
| ~ spl0_56 ),
inference(resolution,[],[f349,f43]) ).
fof(f628,plain,
( product(e_3,e_4,e_3)
| ~ spl0_18
| ~ spl0_56 ),
inference(resolution,[],[f625,f165]) ).
fof(f629,plain,
( $false
| ~ spl0_18
| spl0_42
| ~ spl0_56 ),
inference(forward_subsumption_resolution,[],[f628,f281]) ).
fof(f630,plain,
( ~ spl0_18
| spl0_42
| ~ spl0_56 ),
inference(avatar_contradiction_clause,[],[f629]) ).
fof(f631,plain,
( product(e_2,e_4,e_3)
| ~ spl0_19
| ~ spl0_56 ),
inference(resolution,[],[f169,f625]) ).
fof(f641,plain,
( ! [X0] :
( ~ product(e_3,e_2,X0)
| product(X0,e_2,e_4) )
| ~ spl0_30 ),
inference(resolution,[],[f227,f43]) ).
fof(f647,plain,
( product(e_4,e_2,e_4)
| ~ spl0_30
| ~ spl0_45 ),
inference(resolution,[],[f641,f295]) ).
fof(f654,plain,
( equalish(e_4,e_2)
| ~ spl0_57 ),
inference(resolution,[],[f354,f50]) ).
fof(f655,plain,
( $false
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f654,f36]) ).
fof(f656,plain,
~ spl0_57,
inference(avatar_contradiction_clause,[],[f655]) ).
fof(f659,plain,
( $false
| ~ spl0_25
| ~ spl0_32
| spl0_57 ),
inference(forward_subsumption_resolution,[],[f586,f353]) ).
fof(f660,plain,
( ~ spl0_25
| ~ spl0_32
| spl0_57 ),
inference(avatar_contradiction_clause,[],[f659]) ).
fof(f663,plain,
( $false
| ~ spl0_30
| ~ spl0_45
| spl0_57 ),
inference(forward_subsumption_resolution,[],[f647,f353]) ).
fof(f664,plain,
( ~ spl0_30
| ~ spl0_45
| spl0_57 ),
inference(avatar_contradiction_clause,[],[f663]) ).
fof(f671,plain,
( equalish(e_3,e_2)
| ~ spl0_46 ),
inference(resolution,[],[f299,f50]) ).
fof(f672,plain,
( $false
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f671,f33]) ).
fof(f673,plain,
~ spl0_46,
inference(avatar_contradiction_clause,[],[f672]) ).
fof(f681,plain,
( equalish(e_1,e_4)
| ~ spl0_20 ),
inference(resolution,[],[f173,f50]) ).
fof(f682,plain,
( $false
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f681,f28]) ).
fof(f683,plain,
~ spl0_20,
inference(avatar_contradiction_clause,[],[f682]) ).
fof(f686,plain,
( spl0_30
| ~ spl0_19
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f631,f347,f167,f225]) ).
fof(f722,plain,
( ! [X0] :
( ~ product(e_1,e_3,X0)
| product(X0,e_3,e_2) )
| ~ spl0_48 ),
inference(resolution,[],[f307,f43]) ).
fof(f723,plain,
( product(e_4,e_3,e_2)
| ~ spl0_21
| ~ spl0_48 ),
inference(resolution,[],[f722,f178]) ).
fof(f724,plain,
( $false
| ~ spl0_21
| ~ spl0_48
| spl0_55 ),
inference(forward_subsumption_resolution,[],[f723,f344]) ).
fof(f725,plain,
( ~ spl0_21
| ~ spl0_48
| spl0_55 ),
inference(avatar_contradiction_clause,[],[f724]) ).
cnf(s6,plain,
( spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f174]) ).
cnf(s7,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(sat_conversion,[],[f191]) ).
cnf(s8,plain,
( spl0_25
| spl0_26
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f208]) ).
cnf(s9,plain,
~ spl0_17,
inference(sat_conversion,[],[f215]) ).
cnf(s10,plain,
( spl0_29
| spl0_30
| spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f236]) ).
cnf(s11,plain,
( spl0_33
| spl0_34
| spl0_35
| spl0_36 ),
inference(sat_conversion,[],[f253]) ).
cnf(s13,plain,
( spl0_41
| spl0_42
| spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f291]) ).
cnf(s14,plain,
( spl0_45
| spl0_46
| spl0_47
| spl0_48 ),
inference(sat_conversion,[],[f308]) ).
cnf(s16,plain,
( spl0_53
| spl0_54
| spl0_55
| spl0_56 ),
inference(sat_conversion,[],[f350]) ).
cnf(s19,plain,
~ spl0_29,
inference(sat_conversion,[],[f399]) ).
cnf(s20,plain,
~ spl0_41,
inference(sat_conversion,[],[f418]) ).
cnf(s21,plain,
~ spl0_42,
inference(sat_conversion,[],[f425]) ).
cnf(s22,plain,
~ spl0_53,
inference(sat_conversion,[],[f449]) ).
cnf(s25,plain,
( ~ spl0_33
| ~ spl0_43
| spl0_53 ),
inference(sat_conversion,[],[f453]) ).
cnf(s26,plain,
~ spl0_34,
inference(sat_conversion,[],[f461]) ).
cnf(s27,plain,
~ spl0_35,
inference(sat_conversion,[],[f469]) ).
cnf(s30,plain,
( ~ spl0_26
| ~ spl0_36
| spl0_46 ),
inference(sat_conversion,[],[f484]) ).
cnf(s31,plain,
~ spl0_27,
inference(sat_conversion,[],[f492]) ).
cnf(s32,plain,
~ spl0_28,
inference(sat_conversion,[],[f500]) ).
cnf(s34,plain,
( ~ spl0_21
| ~ spl0_44
| spl0_53 ),
inference(sat_conversion,[],[f517]) ).
cnf(s35,plain,
~ spl0_22,
inference(sat_conversion,[],[f525]) ).
cnf(s36,plain,
~ spl0_54,
inference(sat_conversion,[],[f539]) ).
cnf(s38,plain,
~ spl0_24,
inference(sat_conversion,[],[f549]) ).
cnf(s41,plain,
( spl0_35
| ~ spl0_45
| ~ spl0_55 ),
inference(sat_conversion,[],[f565]) ).
cnf(s43,plain,
( ~ spl0_30
| spl0_42
| ~ spl0_55 ),
inference(sat_conversion,[],[f570]) ).
cnf(s44,plain,
~ spl0_31,
inference(sat_conversion,[],[f578]) ).
cnf(s46,plain,
~ spl0_47,
inference(sat_conversion,[],[f593]) ).
cnf(s47,plain,
( ~ spl0_23
| spl0_35
| ~ spl0_48 ),
inference(sat_conversion,[],[f600]) ).
cnf(s51,plain,
( ~ spl0_18
| spl0_42
| ~ spl0_56 ),
inference(sat_conversion,[],[f630]) ).
cnf(s53,plain,
~ spl0_57,
inference(sat_conversion,[],[f656]) ).
cnf(s56,plain,
( ~ spl0_25
| ~ spl0_32
| spl0_57 ),
inference(sat_conversion,[],[f660]) ).
cnf(s58,plain,
( ~ spl0_30
| ~ spl0_45
| spl0_57 ),
inference(sat_conversion,[],[f664]) ).
cnf(s59,plain,
~ spl0_46,
inference(sat_conversion,[],[f673]) ).
cnf(s61,plain,
~ spl0_20,
inference(sat_conversion,[],[f683]) ).
cnf(s63,plain,
( ~ spl0_19
| spl0_30
| ~ spl0_56 ),
inference(sat_conversion,[],[f686]) ).
cnf(s66,plain,
( ~ spl0_21
| ~ spl0_48
| spl0_55 ),
inference(sat_conversion,[],[f725]) ).
cnf(s67,plain,
( ~ spl0_26
| ~ spl0_36 ),
inference(rat,[],[s30,s59]) ).
cnf(s69,plain,
( spl0_55
| spl0_56 ),
inference(rat,[],[s16,s36,s22]) ).
cnf(s71,plain,
( spl0_45
| spl0_48 ),
inference(rat,[],[s14,s46,s59]) ).
cnf(s72,plain,
( spl0_43
| spl0_44 ),
inference(rat,[],[s13,s21,s20]) ).
cnf(s73,plain,
( spl0_33
| spl0_36 ),
inference(rat,[],[s11,s27,s26]) ).
cnf(s74,plain,
( spl0_30
| spl0_32 ),
inference(rat,[],[s10,s44,s19]) ).
cnf(s75,plain,
( spl0_25
| spl0_26 ),
inference(rat,[],[s8,s32,s31]) ).
cnf(s76,plain,
( spl0_21
| spl0_23 ),
inference(rat,[],[s7,s38,s35]) ).
cnf(s77,plain,
( spl0_18
| spl0_19 ),
inference(rat,[],[s6,s61,s9]) ).
cnf(s78,plain,
( ~ spl0_45
| ~ spl0_19 ),
inference(rat,[],[s69,s63,s41,s58,s27,s53]) ).
cnf(s79,plain,
( ~ spl0_21
| ~ spl0_48 ),
inference(rat,[],[s67,s75,s73,s56,s25,s74,s72,s43,s34,s66,s21,s22,s53]) ).
cnf(s80,plain,
~ spl0_48,
inference(rat,[],[s79,s76,s47,s27]) ).
cnf(s81,plain,
spl0_45,
inference(rat,[],[s71,s80]) ).
cnf(s83,plain,
~ spl0_55,
inference(rat,[],[s41,s27,s81]) ).
cnf(s84,plain,
~ spl0_19,
inference(rat,[],[s78,s81]) ).
cnf(s86,plain,
spl0_56,
inference(rat,[],[s69,s83]) ).
cnf(s87,plain,
spl0_18,
inference(rat,[],[s77,s84]) ).
cnf(s90,plain,
$false,
inference(rat,[],[s51,s21,s86,s87]) ).
fof(f726,plain,
$false,
inference(avatar_sat_refutation,[],[s90]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP127-3.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.37 % Computer : n002.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 09:28:06 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.40 Running first-order model finding
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.47 % (3281302)Will run a generic schedule for satisfiability detection.
% 0.14/0.47 % (3281309)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3229680409:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.14/0.47 % (3281308)% WARNING: option uhcvi not known.
% 0.14/0.47 % (3281308)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1007206292:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.14/0.47 % (3281307)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3298407287_2999 on theBenchmark for (2999ds/0Mi)
% 0.14/0.47 % (3281310)dis+10_1_sil=32000:sp=arity:random_seed=1443624647:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.14/0.47 % (3281311)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1357423324:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.14/0.47 % (3281312)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3884252283:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.14/0.47 % (3281313)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3674171526:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.14/0.47 % Detected minimum model sizes of [1]
% 0.14/0.47 % Detected maximum model sizes of [5]
% 0.14/0.47 % TRYING [1]
% 0.14/0.47 % TRYING [2]
% 0.14/0.47 % TRYING [3]
% 0.14/0.47 % TRYING [4]
% 0.14/0.47 % TRYING [5]
% 0.14/0.47 % (3281312) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3281302-3281312"...
% 0.14/0.47 % (3281307) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3281302-3281307"...
% 0.14/0.47 % (3281312)...printing done.
% 0.14/0.47 % (3281307)...printing done.
% 0.14/0.47 % (3281312)Refutation found. Thanks to Tanya!
% 0.14/0.47 % SZS status Unsatisfiable for theBenchmark
% 0.14/0.47 % SZS output start Proof for theBenchmark
% See solution above
% 0.14/0.47 % (3281312)------------------------------
% 0.14/0.47 % (3281312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.14/0.47 % (3281312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.14/0.47 % (3281312)CaDiCaL version: 2.1.3
% 0.14/0.47 % (3281312)Termination reason: Refutation
% 0.14/0.47 % (3281312)Time elapsed: 0.013 s
% 0.14/0.47 % (3281312)Peak memory usage: 12 MB
% 0.14/0.47 % (3281312)Instructions burned: 17 (million)
% 0.14/0.47 % (3281302)Success in time 0.056 s
% 0.14/0.47 % Vampire exiting
%------------------------------------------------------------------------------