%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP130-2.003 : 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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:13:00 AM UTC 2026
% Result : Unsatisfiable 2.99s 1.34s
% Output : Refutation 3.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 35
% Syntax : Number of formulae : 231 ( 21 unt; 21 def)
% Number of atoms : 633 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 701 ( 299 ~; 381 |; 0 &)
% ( 21 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 27 ( 26 usr; 22 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 85 ( 0 sgn 85 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_then_e_2) ).
fof(f5,axiom,
greater(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_greater_e_2) ).
fof(f6,axiom,
! [X2,X0,X1] :
( ~ greater(X1,X2)
| ~ next(X0,X2)
| ~ product(X0,e_1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_redundancy) ).
fof(f7,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
fof(f8,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
fof(f9,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
fof(f10,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f11,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f13,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f16,axiom,
! [X0,X1] :
( product(X0,X1,e_3)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| ~ group_element(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
fof(f17,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(f18,axiom,
! [X2,X3,X0,X1] :
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f19,axiom,
! [X2,X3,X0,X1] :
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
fof(f20,negated_conjecture,
! [X2,X3,X0,X1] :
( product(X3,X1,X0)
| ~ product(X0,X2,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
fof(f23,plain,
! [X0] :
( ~ next(X0,e_2)
| ~ product(X0,e_1,e_3) ),
inference(resolution,[],[f5,f6]) ).
fof(f24,plain,
! [X0,X1] :
( ~ product(e_2,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[],[f10,f19]) ).
fof(f25,plain,
! [X0,X1] :
( ~ product(X0,e_2,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f10,f18]) ).
fof(f27,plain,
! [X0,X1] :
( ~ product(e_3,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[],[f11,f19]) ).
fof(f28,plain,
! [X0,X1] :
( ~ product(X0,e_3,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f11,f18]) ).
fof(f33,plain,
! [X0,X1] :
( ~ product(e_3,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(resolution,[],[f13,f19]) ).
fof(f34,plain,
! [X0,X1] :
( ~ product(X0,e_3,X1)
| ~ product(X0,e_2,X1) ),
inference(resolution,[],[f13,f18]) ).
fof(f35,plain,
! [X0,X1] :
( ~ product(X0,X1,e_2)
| ~ product(X0,X1,e_3) ),
inference(resolution,[],[f13,f17]) ).
fof(f42,plain,
~ product(e_1,e_1,e_3),
inference(resolution,[],[f23,f1]) ).
fof(f43,plain,
! [X2,X0,X1] :
( ~ product(X1,X2,e_2)
| ~ product(e_1,X0,X1)
| ~ product(X1,X0,X2) ),
inference(resolution,[],[f24,f20]) ).
fof(f47,plain,
! [X0] :
( ~ product(X0,e_2,e_2)
| ~ product(e_1,e_2,X0) ),
inference(factoring,[],[f43]) ).
fof(f48,plain,
! [X2,X0,X1] :
( ~ product(X1,e_2,X2)
| ~ product(X1,X2,X0)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f25,f20]) ).
fof(f49,plain,
! [X0] :
( ~ product(X0,e_1,e_3)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| ~ group_element(X0) ),
inference(resolution,[],[f25,f16]) ).
fof(f50,plain,
! [X0] :
( ~ product(X0,e_1,e_3)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f49,f8]) ).
fof(f55,plain,
! [X0] :
( ~ product(X0,e_2,e_2)
| ~ product(e_2,e_1,X0) ),
inference(factoring,[],[f48]) ).
fof(f58,plain,
! [X0] :
( ~ product(e_1,X0,e_3)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| ~ group_element(e_3) ),
inference(resolution,[],[f27,f16]) ).
fof(f59,plain,
! [X0] :
( ~ product(e_1,X0,e_3)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2) ),
inference(forward_subsumption_resolution,[],[f58,f9]) ).
fof(f60,plain,
! [X0,X1] :
( ~ product(e_2,e_1,X0)
| ~ product(e_2,X1,X0)
| ~ product(e_2,e_2,X1) ),
inference(resolution,[],[f55,f20]) ).
fof(f62,plain,
! [X0] :
( ~ product(X0,e_1,e_3)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| ~ group_element(X0) ),
inference(resolution,[],[f28,f16]) ).
fof(f63,plain,
! [X0] :
( ~ product(X0,e_1,e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f62,f9]) ).
fof(f67,definition,
( spl0_1
<=> product(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f69,plain,
( ~ product(e_2,e_1,e_2)
| spl0_1 ),
inference(avatar_component_clause,[],[f67]) ).
fof(f81,definition,
( spl0_3
<=> product(e_1,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f83,plain,
( ~ product(e_1,e_1,e_3)
| spl0_3 ),
inference(avatar_component_clause,[],[f81]) ).
fof(f85,definition,
( spl0_4
<=> ! [X0] : ~ product(e_1,X0,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f86,plain,
( ! [X0] : ~ product(e_1,X0,e_1)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f85]) ).
fof(f90,plain,
( ! [X0] :
( ~ product(e_3,X0,e_1)
| ~ product(e_3,e_1,X0) )
| spl0_3 ),
inference(resolution,[],[f83,f20]) ).
fof(f94,definition,
( spl0_5
<=> product(e_1,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f95,plain,
( ~ product(e_1,e_1,e_2)
| spl0_5 ),
inference(avatar_component_clause,[],[f94]) ).
fof(f96,plain,
( product(e_1,e_1,e_2)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f94]) ).
fof(f98,definition,
( spl0_6
<=> product(e_1,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f100,plain,
( product(e_1,e_1,e_1)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f98]) ).
fof(f102,plain,
! [X2,X0,X1] :
( ~ product(e_2,X0,X1)
| ~ product(X1,X2,e_3)
| ~ product(X1,X0,X2) ),
inference(resolution,[],[f33,f20]) ).
fof(f107,plain,
( ! [X0] :
( ~ product(e_1,X0,e_1)
| ~ product(e_1,X0,e_1) )
| ~ spl0_5 ),
inference(resolution,[],[f96,f43]) ).
fof(f108,plain,
( ! [X0] : ~ product(e_1,X0,e_1)
| ~ spl0_5 ),
inference(duplicate_literal_removal,[],[f107]) ).
fof(f109,plain,
( spl0_4
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f108,f94,f85]) ).
fof(f112,plain,
! [X0] :
( ~ product(X0,e_2,e_3)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| ~ group_element(X0) ),
inference(resolution,[],[f34,f16]) ).
fof(f113,plain,
! [X0] :
( ~ product(X0,e_2,e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f112,f9]) ).
fof(f114,plain,
( ! [X0] :
( ~ product(e_2,X0,e_1)
| ~ product(e_2,e_1,X0) )
| spl0_5 ),
inference(resolution,[],[f95,f20]) ).
fof(f115,plain,
! [X2,X0,X1] :
( ~ product(e_2,X2,X0)
| ~ product(X0,X1,e_3)
| ~ product(e_2,X1,X2) ),
inference(resolution,[],[f35,f20]) ).
fof(f120,plain,
( ~ product(e_3,e_1,e_1)
| spl0_3 ),
inference(factoring,[],[f90]) ).
fof(f123,plain,
( ~ product(e_2,e_1,e_1)
| spl0_5 ),
inference(factoring,[],[f114]) ).
fof(f138,definition,
( spl0_7
<=> product(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f140,plain,
( product(e_3,e_1,e_2)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f138]) ).
fof(f150,definition,
( spl0_9
<=> product(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f151,plain,
( product(e_1,e_3,e_1)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f150]) ).
fof(f160,plain,
! [X0] :
( ~ product(e_2,X0,e_2)
| ~ product(e_2,e_2,e_3) ),
inference(factoring,[],[f102]) ).
fof(f162,definition,
( spl0_11
<=> product(e_2,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f163,plain,
( product(e_2,e_2,e_3)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f162]) ).
fof(f164,plain,
( ~ product(e_2,e_2,e_3)
| spl0_11 ),
inference(avatar_component_clause,[],[f162]) ).
fof(f166,definition,
( spl0_12
<=> ! [X0] : ~ product(e_2,X0,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f167,plain,
( ! [X0] : ~ product(e_2,X0,e_2)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f168,plain,
( ~ spl0_11
| spl0_12 ),
inference(avatar_split_clause,[],[f160,f166,f162]) ).
fof(f175,definition,
( spl0_13
<=> product(e_2,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f177,plain,
( product(e_2,e_2,e_2)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f179,definition,
( spl0_14
<=> product(e_2,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f181,plain,
( product(e_2,e_2,e_1)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f188,plain,
( ~ product(e_1,e_2,e_3)
| ~ spl0_11 ),
inference(resolution,[],[f163,f24]) ).
fof(f190,plain,
( ~ product(e_2,e_1,e_3)
| ~ spl0_11 ),
inference(resolution,[],[f163,f25]) ).
fof(f195,plain,
! [X0] :
( ~ product(X0,X0,e_3)
| ~ product(e_2,X0,X0) ),
inference(factoring,[],[f115]) ).
fof(f203,definition,
( spl0_15
<=> product(e_3,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f205,plain,
( product(e_3,e_3,e_2)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f207,definition,
( spl0_16
<=> product(e_3,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f209,plain,
( product(e_3,e_3,e_1)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f214,plain,
( ~ product(e_1,e_1,e_2)
| ~ spl0_7 ),
inference(resolution,[],[f140,f27]) ).
fof(f229,plain,
! [X0] :
( product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| ~ group_element(X0) ),
inference(resolution,[],[f50,f16]) ).
fof(f231,plain,
! [X0] :
( product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2) ),
inference(duplicate_literal_removal,[],[f229]) ).
fof(f232,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2) ),
inference(forward_subsumption_resolution,[],[f231,f7]) ).
fof(f238,definition,
( spl0_17
<=> product(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f239,plain,
( ~ product(e_1,e_2,e_2)
| spl0_17 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f240,plain,
( product(e_1,e_2,e_2)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f242,definition,
( spl0_18
<=> product(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f243,plain,
( ~ product(e_1,e_2,e_1)
| spl0_18 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f244,plain,
( product(e_1,e_2,e_1)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f253,plain,
( ! [X0] :
( ~ product(e_3,e_2,X0)
| ~ product(e_3,X0,e_2) )
| spl0_11 ),
inference(resolution,[],[f164,f20]) ).
fof(f257,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| ~ group_element(e_1) ),
inference(resolution,[],[f59,f16]) ).
fof(f259,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| ~ group_element(e_1) ),
inference(duplicate_literal_removal,[],[f257]) ).
fof(f260,plain,
! [X0] :
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2) ),
inference(forward_subsumption_resolution,[],[f259,f7]) ).
fof(f266,plain,
( ~ product(e_1,e_2,e_2)
| ~ spl0_13 ),
inference(resolution,[],[f177,f47]) ).
fof(f268,plain,
( ~ product(e_2,e_1,e_2)
| ~ spl0_13 ),
inference(resolution,[],[f177,f25]) ).
fof(f273,plain,
( ~ spl0_17
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f266,f175,f238]) ).
fof(f274,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| ~ group_element(X0) ),
inference(resolution,[],[f63,f16]) ).
fof(f276,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2) ),
inference(duplicate_literal_removal,[],[f274]) ).
fof(f277,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2) ),
inference(forward_subsumption_resolution,[],[f276,f7]) ).
fof(f288,definition,
( spl0_19
<=> product(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f290,plain,
( product(e_2,e_3,e_2)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f292,definition,
( spl0_20
<=> product(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f296,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| ~ group_element(X0)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| ~ group_element(X0) ),
inference(resolution,[],[f113,f16]) ).
fof(f298,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| ~ group_element(X0)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2) ),
inference(duplicate_literal_removal,[],[f296]) ).
fof(f299,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2) ),
inference(forward_subsumption_resolution,[],[f298,f8]) ).
fof(f306,definition,
( spl0_21
<=> product(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f307,plain,
( ~ product(e_3,e_2,e_2)
| spl0_21 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f310,definition,
( spl0_22
<=> product(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f312,plain,
( product(e_3,e_2,e_1)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f323,plain,
( ~ product(e_1,e_3,e_2)
| ~ spl0_15 ),
inference(resolution,[],[f205,f27]) ).
fof(f379,plain,
( ~ product(e_3,e_2,e_2)
| spl0_11 ),
inference(factoring,[],[f253]) ).
fof(f393,plain,
( ~ product(e_3,e_1,e_2)
| spl0_3
| ~ spl0_22 ),
inference(resolution,[],[f312,f90]) ).
fof(f455,plain,
( ~ product(e_2,e_2,e_2)
| ~ spl0_11 ),
inference(resolution,[],[f163,f195]) ).
fof(f460,plain,
( ~ spl0_13
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f455,f162,f175]) ).
fof(f475,definition,
( spl0_28
<=> product(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f476,plain,
( ~ product(e_1,e_3,e_2)
| spl0_28 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f540,plain,
( ~ group_element(e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| ~ group_element(e_1)
| ~ spl0_11 ),
inference(resolution,[],[f188,f16]) ).
fof(f542,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| ~ group_element(e_1)
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f540,f8]) ).
fof(f543,plain,
( product(e_1,e_2,e_1)
| ~ group_element(e_1)
| ~ spl0_11
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f542,f239]) ).
fof(f544,plain,
( product(e_1,e_2,e_1)
| ~ spl0_11
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f543,f7]) ).
fof(f555,plain,
( ~ group_element(e_1)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| ~ group_element(e_2)
| ~ spl0_11 ),
inference(resolution,[],[f190,f16]) ).
fof(f557,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| ~ group_element(e_2)
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f555,f7]) ).
fof(f558,plain,
( product(e_2,e_1,e_2)
| ~ group_element(e_2)
| spl0_5
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f557,f123]) ).
fof(f559,plain,
( ~ group_element(e_2)
| spl0_5
| ~ spl0_11
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f558,f167]) ).
fof(f560,plain,
( $false
| spl0_5
| ~ spl0_11
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f559,f8]) ).
fof(f561,plain,
( spl0_5
| ~ spl0_11
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f560]) ).
fof(f562,plain,
( ~ spl0_21
| spl0_11 ),
inference(avatar_split_clause,[],[f379,f162,f306]) ).
fof(f573,plain,
( ~ spl0_7
| spl0_3
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f393,f310,f81,f138]) ).
fof(f574,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| ~ group_element(e_2)
| spl0_11 ),
inference(resolution,[],[f164,f16]) ).
fof(f576,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| spl0_11 ),
inference(duplicate_literal_removal,[],[f574]) ).
fof(f577,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f576,f8]) ).
fof(f647,plain,
( ~ product(e_2,e_3,e_1)
| ~ spl0_16 ),
inference(resolution,[],[f209,f33]) ).
fof(f653,plain,
( ~ product(e_3,e_2,e_1)
| ~ spl0_16 ),
inference(resolution,[],[f209,f34]) ).
fof(f659,plain,
( $false
| ~ spl0_16
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f653,f312]) ).
fof(f660,plain,
( ~ spl0_16
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f659]) ).
fof(f661,plain,
( ~ spl0_20
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f647,f207,f292]) ).
fof(f667,plain,
( ~ spl0_28
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f323,f203,f475]) ).
fof(f674,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_9 ),
inference(resolution,[],[f151,f28]) ).
fof(f688,plain,
( ~ spl0_6
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f674,f150,f98]) ).
fof(f690,plain,
~ spl0_3,
inference(avatar_split_clause,[],[f42,f81]) ).
fof(f703,definition,
( spl0_32
<=> product(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f704,plain,
( ~ product(e_3,e_1,e_1)
| spl0_32 ),
inference(avatar_component_clause,[],[f703]) ).
fof(f711,plain,
( ~ spl0_32
| spl0_3 ),
inference(avatar_split_clause,[],[f120,f81,f703]) ).
fof(f717,plain,
( ~ spl0_1
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f268,f175,f67]) ).
fof(f723,plain,
( spl0_13
| spl0_14
| spl0_11 ),
inference(avatar_split_clause,[],[f577,f162,f179,f175]) ).
fof(f726,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ group_element(e_1)
| spl0_3 ),
inference(resolution,[],[f83,f16]) ).
fof(f728,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| spl0_3 ),
inference(duplicate_literal_removal,[],[f726]) ).
fof(f730,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f728,f7]) ).
fof(f756,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2) ),
inference(resolution,[],[f232,f8]) ).
fof(f806,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2) ),
inference(resolution,[],[f260,f8]) ).
fof(f816,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2) ),
inference(resolution,[],[f277,f8]) ).
fof(f817,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_1)
| product(e_3,e_1,e_1)
| product(e_3,e_1,e_2) ),
inference(resolution,[],[f277,f9]) ).
fof(f848,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2) ),
inference(resolution,[],[f299,f7]) ).
fof(f872,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_18 ),
inference(resolution,[],[f244,f25]) ).
fof(f876,plain,
( $false
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f872,f100]) ).
fof(f877,plain,
( ~ spl0_6
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f876]) ).
fof(f883,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_1,e_2)
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f756,f123]) ).
fof(f884,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_2,e_1,e_2)
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f816,f123]) ).
fof(f886,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_1)
| spl0_1
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f883,f69]) ).
fof(f887,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| spl0_1
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f884,f69]) ).
fof(f889,plain,
( spl0_14
| spl0_13
| spl0_1
| spl0_5 ),
inference(avatar_split_clause,[],[f886,f94,f67,f175,f179]) ).
fof(f890,plain,
( spl0_20
| spl0_19
| spl0_1
| spl0_5 ),
inference(avatar_split_clause,[],[f887,f94,f67,f288,f292]) ).
fof(f925,plain,
( ~ product(e_1,e_1,e_2)
| ~ spl0_17 ),
inference(resolution,[],[f240,f25]) ).
fof(f962,plain,
( ~ product(e_2,e_2,e_2)
| ~ spl0_19 ),
inference(resolution,[],[f290,f34]) ).
fof(f1000,plain,
! [X0] :
( ~ product(e_2,e_1,X0)
| ~ product(e_2,e_2,e_1) ),
inference(factoring,[],[f60]) ).
fof(f1001,plain,
( ! [X0] : ~ product(e_2,e_1,X0)
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1000,f181]) ).
fof(f1003,plain,
( ~ group_element(e_1)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| ~ group_element(e_2)
| ~ spl0_14 ),
inference(resolution,[],[f1001,f16]) ).
fof(f1004,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| ~ group_element(e_2)
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1003,f7]) ).
fof(f1011,plain,
( spl0_5
| spl0_6
| spl0_3 ),
inference(avatar_split_clause,[],[f730,f81,f98,f94]) ).
fof(f1012,plain,
( ~ spl0_5
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f214,f138,f94]) ).
fof(f1013,plain,
( ~ spl0_5
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f925,f238,f94]) ).
fof(f1014,plain,
( product(e_2,e_1,e_1)
| ~ group_element(e_2)
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1004,f1001]) ).
fof(f1017,plain,
( ~ group_element(e_2)
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1014,f1001]) ).
fof(f1020,plain,
( $false
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1017,f8]) ).
fof(f1021,plain,
~ spl0_14,
inference(avatar_contradiction_clause,[],[f1020]) ).
fof(f1024,plain,
( product(e_3,e_2,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f806,f307]) ).
fof(f1027,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f848,f476]) ).
fof(f1043,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_1)
| product(e_3,e_1,e_2)
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f817,f704]) ).
fof(f1046,plain,
( product(e_3,e_2,e_1)
| product(e_1,e_2,e_2)
| spl0_18
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1024,f243]) ).
fof(f1049,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_2,e_2)
| spl0_18
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f1027,f243]) ).
fof(f1067,plain,
( spl0_7
| spl0_16
| spl0_15
| spl0_32 ),
inference(avatar_split_clause,[],[f1043,f703,f203,f207,f138]) ).
fof(f1070,plain,
( spl0_17
| spl0_22
| spl0_18
| spl0_21 ),
inference(avatar_split_clause,[],[f1046,f306,f242,f310,f238]) ).
fof(f1072,plain,
( spl0_17
| spl0_9
| spl0_18
| spl0_28 ),
inference(avatar_split_clause,[],[f1049,f475,f242,f150,f238]) ).
fof(f1086,plain,
( $false
| ~ spl0_4
| ~ spl0_11
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f544,f86]) ).
fof(f1087,plain,
( ~ spl0_4
| ~ spl0_11
| spl0_17 ),
inference(avatar_contradiction_clause,[],[f1086]) ).
fof(f1088,plain,
( $false
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f244,f86]) ).
fof(f1089,plain,
( ~ spl0_4
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1088]) ).
fof(f1091,plain,
( ~ spl0_13
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f962,f288,f175]) ).
fof(f1099,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_2,e_2)
| ~ spl0_4
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f1027,f86]) ).
fof(f1105,plain,
( product(e_1,e_2,e_2)
| ~ spl0_4
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f1099,f86]) ).
fof(f1108,plain,
( spl0_17
| ~ spl0_4
| spl0_28 ),
inference(avatar_split_clause,[],[f1105,f475,f85,f238]) ).
cnf(s4,plain,
( spl0_4
| ~ spl0_5 ),
inference(sat_conversion,[],[f109]) ).
cnf(s8,plain,
( ~ spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f168]) ).
cnf(s15,plain,
( ~ spl0_13
| ~ spl0_17 ),
inference(sat_conversion,[],[f273]) ).
cnf(s32,plain,
( ~ spl0_11
| ~ spl0_13 ),
inference(sat_conversion,[],[f460]) ).
cnf(s43,plain,
( spl0_5
| ~ spl0_11
| ~ spl0_12 ),
inference(sat_conversion,[],[f561]) ).
cnf(s44,plain,
( spl0_11
| ~ spl0_21 ),
inference(sat_conversion,[],[f562]) ).
cnf(s51,plain,
( spl0_3
| ~ spl0_7
| ~ spl0_22 ),
inference(sat_conversion,[],[f573]) ).
cnf(s55,plain,
( ~ spl0_16
| ~ spl0_22 ),
inference(sat_conversion,[],[f660]) ).
cnf(s56,plain,
( ~ spl0_16
| ~ spl0_20 ),
inference(sat_conversion,[],[f661]) ).
cnf(s60,plain,
( ~ spl0_15
| ~ spl0_28 ),
inference(sat_conversion,[],[f667]) ).
cnf(s65,plain,
( ~ spl0_6
| ~ spl0_9 ),
inference(sat_conversion,[],[f688]) ).
cnf(s66,plain,
~ spl0_3,
inference(sat_conversion,[],[f690]) ).
cnf(s71,plain,
( spl0_3
| ~ spl0_32 ),
inference(sat_conversion,[],[f711]) ).
cnf(s77,plain,
( ~ spl0_1
| ~ spl0_13 ),
inference(sat_conversion,[],[f717]) ).
cnf(s86,plain,
( spl0_11
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f723]) ).
cnf(s109,plain,
( ~ spl0_6
| ~ spl0_18 ),
inference(sat_conversion,[],[f877]) ).
cnf(s118,plain,
( spl0_1
| spl0_5
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f889]) ).
cnf(s119,plain,
( spl0_1
| spl0_5
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f890]) ).
cnf(s136,plain,
( spl0_3
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f1011]) ).
cnf(s137,plain,
( ~ spl0_5
| ~ spl0_7 ),
inference(sat_conversion,[],[f1012]) ).
cnf(s140,plain,
( ~ spl0_5
| ~ spl0_17 ),
inference(sat_conversion,[],[f1013]) ).
cnf(s143,plain,
~ spl0_14,
inference(sat_conversion,[],[f1021]) ).
cnf(s175,plain,
( spl0_7
| spl0_15
| spl0_16
| spl0_32 ),
inference(sat_conversion,[],[f1067]) ).
cnf(s176,plain,
( spl0_17
| spl0_18
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f1070]) ).
cnf(s178,plain,
( spl0_9
| spl0_17
| spl0_18
| spl0_28 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s187,plain,
( ~ spl0_4
| ~ spl0_11
| spl0_17 ),
inference(sat_conversion,[],[f1087]) ).
cnf(s190,plain,
( ~ spl0_4
| ~ spl0_18 ),
inference(sat_conversion,[],[f1089]) ).
cnf(s192,plain,
( ~ spl0_13
| ~ spl0_19 ),
inference(sat_conversion,[],[f1091]) ).
cnf(s200,plain,
( ~ spl0_4
| spl0_17
| spl0_28 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s203,plain,
( spl0_1
| spl0_5
| spl0_13 ),
inference(rat,[],[s118,s143]) ).
cnf(s205,plain,
( spl0_11
| spl0_13 ),
inference(rat,[],[s86,s143]) ).
cnf(s208,plain,
~ spl0_32,
inference(rat,[],[s71,s66]) ).
cnf(s210,plain,
( ~ spl0_7
| ~ spl0_22 ),
inference(rat,[],[s51,s66]) ).
cnf(s219,plain,
( spl0_5
| spl0_1 ),
inference(rat,[],[s175,s210,s60,s56,s176,s178,s44,s119,s15,s32,s192,s65,s109,s203,s136,s208,s66]) ).
cnf(s220,plain,
~ spl0_5,
inference(rat,[],[s55,s176,s175,s44,s60,s187,s190,s200,s4,s137,s140,s208]) ).
cnf(s222,plain,
spl0_1,
inference(rat,[],[s219,s220]) ).
cnf(s226,plain,
~ spl0_13,
inference(rat,[],[s77,s222]) ).
cnf(s229,plain,
spl0_11,
inference(rat,[],[s205,s226]) ).
cnf(s234,plain,
spl0_12,
inference(rat,[],[s8,s229]) ).
cnf(s235,plain,
$false,
inference(rat,[],[s43,s220,s229,s234]) ).
fof(f1109,plain,
$false,
inference(avatar_sat_refutation,[],[s235]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP130-2.003 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n005.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:28:17 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
% 2.99/1.34 % (3734625)Input is clausal, will run a generic CNF schedule.
% 2.99/1.34 % (3734634)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2645425536:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.99/1.34 % (3734634)Instruction limit reached!
% 2.99/1.34 % (3734634)------------------------------
% 2.99/1.34 % (3734634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.34 % (3734634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.34 % (3734634)CaDiCaL version: 2.1.3
% 2.99/1.34 % (3734634)Termination reason: Instruction limit
% 2.99/1.34 % (3734634)Termination phase: Saturation
% 2.99/1.34 % (3734634)Time elapsed: 0.033 s
% 2.99/1.34 % (3734634)Peak memory usage: 88 MB
% 2.99/1.34 % (3734634)Instructions burned: 117 (million)
% 2.99/1.34 % (3734630)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=1517098838:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.99/1.34 % (3734631)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2380519660:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.99/1.34 % (3734633)lrs+10_1_sil=8000:sp=occurrence:random_seed=4094122685:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.99/1.34 % (3734632)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3273926431:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.99/1.34 % (3734636)dis-21_1_sil=8000:lcm=predicate:random_seed=3435543984:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 2.99/1.34 % (3734635)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1506273636:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.99/1.34 % (3734635)First to succeed.
% 2.99/1.34 % (3734635)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3734625"
% 2.99/1.34 % (3734636)Also succeeded, but the first one will report.
% 2.99/1.34 % (3734633)Instruction limit reached!
% 2.99/1.34 % (3734633)------------------------------
% 2.99/1.34 % (3734633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.34 % (3734633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.34 % (3734633)CaDiCaL version: 2.1.3
% 2.99/1.34 % (3734633)Termination reason: Instruction limit
% 2.99/1.34 % (3734633)Termination phase: Saturation
% 2.99/1.34 % (3734633)Time elapsed: 0.065 s
% 2.99/1.34 % (3734633)Peak memory usage: 88 MB
% 2.99/1.34 % (3734633)Instructions burned: 108 (million)
% 2.99/1.34 % (3734638)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=3863405460:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 2.99/1.34 % (3734638)Also succeeded, but the first one will report.
% 2.99/1.34 % (3734645)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3791355865:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 2.99/1.34 % (3734645)Refutation not found, incomplete strategy
% 2.99/1.34 % (3734645)------------------------------
% 2.99/1.34 % (3734645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.34 % (3734645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.34 % (3734645)CaDiCaL version: 2.1.3
% 2.99/1.34 % (3734645)Termination reason: Refutation not found, incomplete strategy
% 2.99/1.34 % (3734645)Time elapsed: 0.001 s
% 2.99/1.34 % (3734645)Peak memory usage: 87 MB
% 2.99/1.34 % (3734645)Instructions burned: 1 (million)
% 2.99/1.34 % (3734635)Refutation found. Thanks to Tanya!
% 2.99/1.34 % SZS status Unsatisfiable for theBenchmark
% 2.99/1.34 % SZS output start Proof for theBenchmark
% See solution above
% 3.95/1.54 % (3734635)------------------------------
% 3.95/1.54 % (3734635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.95/1.54 % (3734635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.95/1.54 % (3734635)CaDiCaL version: 2.1.3
% 3.95/1.54 % (3734635)Termination reason: Refutation
% 3.95/1.54 % (3734635)Time elapsed: 0.029 s
% 3.95/1.54 % (3734635)Peak memory usage: 89 MB
% 3.95/1.54 % (3734635)Instructions burned: 41 (million)
% 3.95/1.54 % (3734635)------------------------------
% 3.95/1.54 % (3734635)------------------------------
% 3.95/1.54 % (3734625)Success in time 0.469 s
% 3.95/1.54 % Vampire exiting
%------------------------------------------------------------------------------