%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP124-8.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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:16:46 AM UTC 2026
% Result : Unsatisfiable 0.16s 0.48s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 59
% Syntax : Number of formulae : 301 ( 74 unt; 36 def)
% Number of atoms : 647 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 635 ( 289 ~; 310 |; 0 &)
% ( 36 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 41 ( 40 usr; 37 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 41 ( 0 sgn 41 !; 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)
| product1(X0,X1,e_1)
| product1(X0,X1,e_2)
| product1(X0,X1,e_3)
| product1(X0,X1,e_4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_total_function1) ).
fof(f40,axiom,
! [X2,X3,X0,X1] :
( ~ product1(X0,X1,X2)
| ~ product1(X0,X3,X2)
| equalish(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_right_cancellation) ).
fof(f41,axiom,
! [X2,X3,X0,X1] :
( ~ product1(X0,X1,X2)
| ~ product1(X3,X1,X2)
| equalish(X0,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_left_cancellation) ).
fof(f42,axiom,
! [X0] : product1(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_idempotence) ).
fof(f44,axiom,
! [X2,X3,X0,X1] :
( ~ product2(X0,X1,X2)
| ~ product2(X0,X1,X3)
| equalish(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_total_function2) ).
fof(f47,axiom,
! [X0] : product2(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_idempotence) ).
fof(f48,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ product1(X0,X1,X2)
| ~ product1(X2,X0,X3)
| product2(X3,X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg2a) ).
fof(f54,plain,
! [X0,X1] :
( ~ product1(X0,X1,X0)
| equalish(X0,X1) ),
inference(resolution,[],[f40,f42]) ).
fof(f56,plain,
! [X0,X1] :
( ~ product1(X0,X1,X1)
| equalish(X1,X0) ),
inference(resolution,[],[f41,f42]) ).
fof(f57,plain,
! [X0,X1] :
( ~ product2(X0,X0,X1)
| equalish(X0,X1) ),
inference(resolution,[],[f44,f47]) ).
fof(f140,plain,
! [X0] :
( ~ group_element(X0)
| product1(e_1,X0,e_1)
| product1(e_1,X0,e_2)
| product1(e_1,X0,e_3)
| product1(e_1,X0,e_4) ),
inference(resolution,[],[f38,f22]) ).
fof(f141,plain,
! [X0] :
( ~ group_element(X0)
| product1(e_2,X0,e_1)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_3)
| product1(e_2,X0,e_4) ),
inference(resolution,[],[f38,f23]) ).
fof(f142,plain,
! [X0] :
( ~ group_element(X0)
| product1(e_3,X0,e_1)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_4) ),
inference(resolution,[],[f38,f24]) ).
fof(f163,plain,
( product1(e_1,e_2,e_1)
| product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(resolution,[],[f140,f23]) ).
fof(f164,plain,
( product1(e_1,e_3,e_1)
| product1(e_1,e_3,e_2)
| product1(e_1,e_3,e_3)
| product1(e_1,e_3,e_4) ),
inference(resolution,[],[f140,f24]) ).
fof(f165,plain,
( product1(e_1,e_4,e_1)
| product1(e_1,e_4,e_2)
| product1(e_1,e_4,e_3)
| product1(e_1,e_4,e_4) ),
inference(resolution,[],[f140,f25]) ).
fof(f167,definition,
( spl0_17
<=> product1(e_1,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f169,plain,
( product1(e_1,e_4,e_4)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f171,definition,
( spl0_18
<=> product1(e_1,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f173,plain,
( product1(e_1,e_4,e_3)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f171]) ).
fof(f175,definition,
( spl0_19
<=> product1(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f177,plain,
( product1(e_1,e_4,e_2)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f179,definition,
( spl0_20
<=> product1(e_1,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f181,plain,
( product1(e_1,e_4,e_1)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f182,plain,
( spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f165,f179,f175,f171,f167]) ).
fof(f184,definition,
( spl0_21
<=> product1(e_1,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f186,plain,
( product1(e_1,e_3,e_4)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f188,definition,
( spl0_22
<=> product1(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f190,plain,
( product1(e_1,e_3,e_3)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f192,definition,
( spl0_23
<=> product1(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f194,plain,
( product1(e_1,e_3,e_2)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f196,definition,
( spl0_24
<=> product1(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f198,plain,
( product1(e_1,e_3,e_1)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f199,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(avatar_split_clause,[],[f164,f196,f192,f188,f184]) ).
fof(f201,definition,
( spl0_25
<=> product1(e_1,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f203,plain,
( product1(e_1,e_2,e_4)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f205,definition,
( spl0_26
<=> product1(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f207,plain,
( product1(e_1,e_2,e_3)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f209,definition,
( spl0_27
<=> product1(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f211,plain,
( product1(e_1,e_2,e_2)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f213,definition,
( spl0_28
<=> product1(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f215,plain,
( product1(e_1,e_2,e_1)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f216,plain,
( spl0_25
| spl0_26
| spl0_27
| spl0_28 ),
inference(avatar_split_clause,[],[f163,f213,f209,f205,f201]) ).
fof(f221,plain,
( equalish(e_4,e_1)
| ~ spl0_17 ),
inference(resolution,[],[f169,f56]) ).
fof(f222,plain,
( $false
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f221,f35]) ).
fof(f223,plain,
~ spl0_17,
inference(avatar_contradiction_clause,[],[f222]) ).
fof(f224,plain,
( product1(e_2,e_1,e_1)
| product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4) ),
inference(resolution,[],[f141,f22]) ).
fof(f226,plain,
( product1(e_2,e_3,e_1)
| product1(e_2,e_3,e_2)
| product1(e_2,e_3,e_3)
| product1(e_2,e_3,e_4) ),
inference(resolution,[],[f141,f24]) ).
fof(f227,plain,
( product1(e_2,e_4,e_1)
| product1(e_2,e_4,e_2)
| product1(e_2,e_4,e_3)
| product1(e_2,e_4,e_4) ),
inference(resolution,[],[f141,f25]) ).
fof(f229,definition,
( spl0_29
<=> product1(e_2,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f231,plain,
( product1(e_2,e_4,e_4)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f233,definition,
( spl0_30
<=> product1(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f235,plain,
( product1(e_2,e_4,e_3)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f237,definition,
( spl0_31
<=> product1(e_2,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f239,plain,
( product1(e_2,e_4,e_2)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f241,definition,
( spl0_32
<=> product1(e_2,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f243,plain,
( product1(e_2,e_4,e_1)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f244,plain,
( spl0_29
| spl0_30
| spl0_31
| spl0_32 ),
inference(avatar_split_clause,[],[f227,f241,f237,f233,f229]) ).
fof(f246,definition,
( spl0_33
<=> product1(e_2,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f248,plain,
( product1(e_2,e_3,e_4)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f250,definition,
( spl0_34
<=> product1(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f252,plain,
( product1(e_2,e_3,e_3)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f254,definition,
( spl0_35
<=> product1(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f256,plain,
( product1(e_2,e_3,e_2)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f258,definition,
( spl0_36
<=> product1(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f260,plain,
( product1(e_2,e_3,e_1)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f261,plain,
( spl0_33
| spl0_34
| spl0_35
| spl0_36 ),
inference(avatar_split_clause,[],[f226,f258,f254,f250,f246]) ).
fof(f263,definition,
( spl0_37
<=> product1(e_2,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f265,plain,
( product1(e_2,e_1,e_4)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f267,definition,
( spl0_38
<=> product1(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f269,plain,
( product1(e_2,e_1,e_3)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f271,definition,
( spl0_39
<=> product1(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f273,plain,
( product1(e_2,e_1,e_2)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f275,definition,
( spl0_40
<=> product1(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f277,plain,
( product1(e_2,e_1,e_1)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f278,plain,
( spl0_37
| spl0_38
| spl0_39
| spl0_40 ),
inference(avatar_split_clause,[],[f224,f275,f271,f267,f263]) ).
fof(f279,plain,
( product1(e_3,e_1,e_1)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_4) ),
inference(resolution,[],[f142,f22]) ).
fof(f280,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_4) ),
inference(resolution,[],[f142,f23]) ).
fof(f282,plain,
( product1(e_3,e_4,e_1)
| product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_3)
| product1(e_3,e_4,e_4) ),
inference(resolution,[],[f142,f25]) ).
fof(f284,definition,
( spl0_41
<=> product1(e_3,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f286,plain,
( product1(e_3,e_4,e_4)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f288,definition,
( spl0_42
<=> product1(e_3,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f290,plain,
( product1(e_3,e_4,e_3)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f292,definition,
( spl0_43
<=> product1(e_3,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f294,plain,
( product1(e_3,e_4,e_2)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f296,definition,
( spl0_44
<=> product1(e_3,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f298,plain,
( product1(e_3,e_4,e_1)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f299,plain,
( spl0_41
| spl0_42
| spl0_43
| spl0_44 ),
inference(avatar_split_clause,[],[f282,f296,f292,f288,f284]) ).
fof(f301,definition,
( spl0_45
<=> product1(e_3,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f303,plain,
( product1(e_3,e_2,e_4)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f305,definition,
( spl0_46
<=> product1(e_3,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f307,plain,
( product1(e_3,e_2,e_3)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f309,definition,
( spl0_47
<=> product1(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f311,plain,
( product1(e_3,e_2,e_2)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f313,definition,
( spl0_48
<=> product1(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f315,plain,
( product1(e_3,e_2,e_1)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f313]) ).
fof(f316,plain,
( spl0_45
| spl0_46
| spl0_47
| spl0_48 ),
inference(avatar_split_clause,[],[f280,f313,f309,f305,f301]) ).
fof(f318,definition,
( spl0_49
<=> product1(e_3,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f320,plain,
( product1(e_3,e_1,e_4)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f322,definition,
( spl0_50
<=> product1(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f324,plain,
( product1(e_3,e_1,e_3)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f326,definition,
( spl0_51
<=> product1(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f328,plain,
( product1(e_3,e_1,e_2)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f330,definition,
( spl0_52
<=> product1(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f332,plain,
( product1(e_3,e_1,e_1)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f333,plain,
( spl0_49
| spl0_50
| spl0_51
| spl0_52 ),
inference(avatar_split_clause,[],[f279,f330,f326,f322,f318]) ).
fof(f337,plain,
( ! [X0] :
( ~ product1(e_3,e_1,X0)
| product2(X0,e_4,e_1) )
| ~ spl0_18 ),
inference(resolution,[],[f173,f48]) ).
fof(f625,plain,
( equalish(e_4,e_2)
| ~ spl0_29 ),
inference(resolution,[],[f231,f56]) ).
fof(f626,plain,
( $false
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f625,f36]) ).
fof(f627,plain,
~ spl0_29,
inference(avatar_contradiction_clause,[],[f626]) ).
fof(f631,plain,
( ! [X0] :
( ~ product1(e_3,e_2,X0)
| product2(X0,e_4,e_2) )
| ~ spl0_30 ),
inference(resolution,[],[f235,f48]) ).
fof(f644,plain,
( equalish(e_4,e_3)
| ~ spl0_41 ),
inference(resolution,[],[f286,f56]) ).
fof(f645,plain,
( $false
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f644,f37]) ).
fof(f646,plain,
~ spl0_41,
inference(avatar_contradiction_clause,[],[f645]) ).
fof(f651,plain,
( equalish(e_3,e_4)
| ~ spl0_42 ),
inference(resolution,[],[f290,f54]) ).
fof(f652,plain,
( $false
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f651,f34]) ).
fof(f653,plain,
~ spl0_42,
inference(avatar_contradiction_clause,[],[f652]) ).
fof(f657,plain,
( ! [X0] :
( ~ product1(e_2,e_3,X0)
| product2(X0,e_4,e_3) )
| ~ spl0_43 ),
inference(resolution,[],[f294,f48]) ).
fof(f658,plain,
( product2(e_4,e_4,e_3)
| ~ spl0_33
| ~ spl0_43 ),
inference(resolution,[],[f657,f248]) ).
fof(f659,plain,
( product2(e_4,e_4,e_2)
| ~ spl0_30
| ~ spl0_45 ),
inference(resolution,[],[f303,f631]) ).
fof(f667,plain,
( equalish(e_4,e_3)
| ~ spl0_33
| ~ spl0_43 ),
inference(resolution,[],[f658,f57]) ).
fof(f668,plain,
( $false
| ~ spl0_33
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f667,f37]) ).
fof(f669,plain,
( ~ spl0_33
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f668]) ).
fof(f673,plain,
( equalish(e_4,e_2)
| ~ spl0_30
| ~ spl0_45 ),
inference(resolution,[],[f659,f57]) ).
fof(f674,plain,
( $false
| ~ spl0_30
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f673,f36]) ).
fof(f675,plain,
( ~ spl0_30
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f674]) ).
fof(f680,plain,
( equalish(e_2,e_4)
| ~ spl0_31 ),
inference(resolution,[],[f239,f54]) ).
fof(f681,plain,
( $false
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f680,f31]) ).
fof(f682,plain,
~ spl0_31,
inference(avatar_contradiction_clause,[],[f681]) ).
fof(f686,plain,
( ! [X0] :
( ~ product1(e_1,e_2,X0)
| product2(X0,e_4,e_2) )
| ~ spl0_32 ),
inference(resolution,[],[f243,f48]) ).
fof(f687,plain,
( product2(e_4,e_4,e_2)
| ~ spl0_25
| ~ spl0_32 ),
inference(resolution,[],[f686,f203]) ).
fof(f693,plain,
( equalish(e_3,e_2)
| ~ spl0_34 ),
inference(resolution,[],[f252,f56]) ).
fof(f694,plain,
( $false
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f693,f33]) ).
fof(f695,plain,
~ spl0_34,
inference(avatar_contradiction_clause,[],[f694]) ).
fof(f700,plain,
( equalish(e_4,e_2)
| ~ spl0_25
| ~ spl0_32 ),
inference(resolution,[],[f687,f57]) ).
fof(f701,plain,
( $false
| ~ spl0_25
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f700,f36]) ).
fof(f702,plain,
( ~ spl0_25
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f701]) ).
fof(f714,plain,
( equalish(e_2,e_1)
| ~ spl0_27 ),
inference(resolution,[],[f211,f56]) ).
fof(f715,plain,
( $false
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f714,f29]) ).
fof(f716,plain,
~ spl0_27,
inference(avatar_contradiction_clause,[],[f715]) ).
fof(f723,plain,
( equalish(e_1,e_2)
| ~ spl0_28 ),
inference(resolution,[],[f215,f54]) ).
fof(f724,plain,
( $false
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f723,f26]) ).
fof(f725,plain,
~ spl0_28,
inference(avatar_contradiction_clause,[],[f724]) ).
fof(f740,plain,
( equalish(e_2,e_3)
| ~ spl0_35 ),
inference(resolution,[],[f256,f54]) ).
fof(f741,plain,
( $false
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f740,f30]) ).
fof(f742,plain,
~ spl0_35,
inference(avatar_contradiction_clause,[],[f741]) ).
fof(f757,plain,
( ! [X0] :
( ~ product1(e_1,e_3,X0)
| product2(X0,e_4,e_3) )
| ~ spl0_44 ),
inference(resolution,[],[f298,f48]) ).
fof(f758,plain,
( product2(e_4,e_4,e_3)
| ~ spl0_21
| ~ spl0_44 ),
inference(resolution,[],[f757,f186]) ).
fof(f764,plain,
( equalish(e_3,e_2)
| ~ spl0_46 ),
inference(resolution,[],[f307,f54]) ).
fof(f765,plain,
( $false
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f764,f33]) ).
fof(f766,plain,
~ spl0_46,
inference(avatar_contradiction_clause,[],[f765]) ).
fof(f771,plain,
( equalish(e_4,e_3)
| ~ spl0_21
| ~ spl0_44 ),
inference(resolution,[],[f758,f57]) ).
fof(f772,plain,
( $false
| ~ spl0_21
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f771,f37]) ).
fof(f773,plain,
( ~ spl0_21
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f772]) ).
fof(f779,plain,
( equalish(e_3,e_1)
| ~ spl0_22 ),
inference(resolution,[],[f190,f56]) ).
fof(f780,plain,
( $false
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f779,f32]) ).
fof(f781,plain,
~ spl0_22,
inference(avatar_contradiction_clause,[],[f780]) ).
fof(f794,plain,
( equalish(e_1,e_3)
| ~ spl0_24 ),
inference(resolution,[],[f198,f54]) ).
fof(f795,plain,
( $false
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f794,f27]) ).
fof(f796,plain,
~ spl0_24,
inference(avatar_contradiction_clause,[],[f795]) ).
fof(f802,plain,
( ! [X0] :
( ~ product1(e_2,e_1,X0)
| product2(X0,e_3,e_1) )
| ~ spl0_23 ),
inference(resolution,[],[f194,f48]) ).
fof(f810,plain,
( equalish(e_2,e_3)
| ~ spl0_47 ),
inference(resolution,[],[f311,f56]) ).
fof(f811,plain,
( $false
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f810,f30]) ).
fof(f812,plain,
~ spl0_47,
inference(avatar_contradiction_clause,[],[f811]) ).
fof(f818,plain,
( ! [X0] :
( ~ product1(e_1,e_3,X0)
| product2(X0,e_2,e_3) )
| ~ spl0_48 ),
inference(resolution,[],[f315,f48]) ).
fof(f820,plain,
( product2(e_2,e_2,e_3)
| ~ spl0_23
| ~ spl0_48 ),
inference(resolution,[],[f818,f194]) ).
fof(f821,plain,
( product2(e_4,e_4,e_1)
| ~ spl0_18
| ~ spl0_49 ),
inference(resolution,[],[f320,f337]) ).
fof(f829,plain,
( equalish(e_2,e_3)
| ~ spl0_23
| ~ spl0_48 ),
inference(resolution,[],[f820,f57]) ).
fof(f830,plain,
( $false
| ~ spl0_23
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f829,f30]) ).
fof(f831,plain,
( ~ spl0_23
| ~ spl0_48 ),
inference(avatar_contradiction_clause,[],[f830]) ).
fof(f835,plain,
( equalish(e_4,e_1)
| ~ spl0_18
| ~ spl0_49 ),
inference(resolution,[],[f821,f57]) ).
fof(f836,plain,
( $false
| ~ spl0_18
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f835,f35]) ).
fof(f837,plain,
( ~ spl0_18
| ~ spl0_49 ),
inference(avatar_contradiction_clause,[],[f836]) ).
fof(f841,plain,
( ! [X0] :
( ~ product1(e_2,e_1,X0)
| product2(X0,e_4,e_1) )
| ~ spl0_19 ),
inference(resolution,[],[f177,f48]) ).
fof(f842,plain,
( product2(e_4,e_4,e_1)
| ~ spl0_19
| ~ spl0_37 ),
inference(resolution,[],[f841,f265]) ).
fof(f846,plain,
( ! [X0] :
( ~ product1(e_3,e_1,X0)
| product2(X0,e_2,e_1) )
| ~ spl0_26 ),
inference(resolution,[],[f207,f48]) ).
fof(f850,plain,
( equalish(e_4,e_1)
| ~ spl0_19
| ~ spl0_37 ),
inference(resolution,[],[f842,f57]) ).
fof(f851,plain,
( $false
| ~ spl0_19
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f850,f35]) ).
fof(f852,plain,
( ~ spl0_19
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f851]) ).
fof(f866,plain,
( equalish(e_1,e_2)
| ~ spl0_40 ),
inference(resolution,[],[f277,f56]) ).
fof(f867,plain,
( $false
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f866,f26]) ).
fof(f868,plain,
~ spl0_40,
inference(avatar_contradiction_clause,[],[f867]) ).
fof(f872,plain,
( product2(e_3,e_3,e_1)
| ~ spl0_23
| ~ spl0_38 ),
inference(resolution,[],[f269,f802]) ).
fof(f881,plain,
( equalish(e_3,e_1)
| ~ spl0_23
| ~ spl0_38 ),
inference(resolution,[],[f872,f57]) ).
fof(f882,plain,
( $false
| ~ spl0_23
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f881,f32]) ).
fof(f883,plain,
( ~ spl0_23
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f882]) ).
fof(f903,plain,
( equalish(e_3,e_1)
| ~ spl0_50 ),
inference(resolution,[],[f324,f54]) ).
fof(f904,plain,
( $false
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f903,f32]) ).
fof(f905,plain,
~ spl0_50,
inference(avatar_contradiction_clause,[],[f904]) ).
fof(f918,plain,
( equalish(e_2,e_1)
| ~ spl0_39 ),
inference(resolution,[],[f273,f54]) ).
fof(f919,plain,
( $false
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f918,f29]) ).
fof(f920,plain,
~ spl0_39,
inference(avatar_contradiction_clause,[],[f919]) ).
fof(f933,plain,
( product2(e_2,e_2,e_1)
| ~ spl0_26
| ~ spl0_51 ),
inference(resolution,[],[f328,f846]) ).
fof(f942,plain,
( equalish(e_2,e_1)
| ~ spl0_26
| ~ spl0_51 ),
inference(resolution,[],[f933,f57]) ).
fof(f943,plain,
( $false
| ~ spl0_26
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f942,f29]) ).
fof(f944,plain,
( ~ spl0_26
| ~ spl0_51 ),
inference(avatar_contradiction_clause,[],[f943]) ).
fof(f949,plain,
( equalish(e_1,e_4)
| ~ spl0_20 ),
inference(resolution,[],[f181,f54]) ).
fof(f950,plain,
( $false
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f949,f28]) ).
fof(f951,plain,
~ spl0_20,
inference(avatar_contradiction_clause,[],[f950]) ).
fof(f962,plain,
( equalish(e_1,e_3)
| ~ spl0_52 ),
inference(resolution,[],[f332,f56]) ).
fof(f963,plain,
( $false
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f962,f27]) ).
fof(f964,plain,
~ spl0_52,
inference(avatar_contradiction_clause,[],[f963]) ).
fof(f978,plain,
( ! [X0] :
( ~ product1(e_1,e_2,X0)
| product2(X0,e_3,e_2) )
| ~ spl0_36 ),
inference(resolution,[],[f260,f48]) ).
fof(f979,plain,
( product2(e_3,e_3,e_2)
| ~ spl0_26
| ~ spl0_36 ),
inference(resolution,[],[f978,f207]) ).
fof(f984,plain,
( ! [X0] :
( ~ product1(e_3,e_2,X0)
| product2(X0,e_1,e_2) )
| ~ spl0_38 ),
inference(resolution,[],[f269,f48]) ).
fof(f988,plain,
( equalish(e_3,e_2)
| ~ spl0_26
| ~ spl0_36 ),
inference(resolution,[],[f979,f57]) ).
fof(f989,plain,
( $false
| ~ spl0_26
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f988,f33]) ).
fof(f990,plain,
( ~ spl0_26
| ~ spl0_36 ),
inference(avatar_contradiction_clause,[],[f989]) ).
fof(f1007,plain,
( product2(e_1,e_1,e_2)
| ~ spl0_38
| ~ spl0_48 ),
inference(resolution,[],[f315,f984]) ).
fof(f1019,plain,
( equalish(e_1,e_2)
| ~ spl0_38
| ~ spl0_48 ),
inference(resolution,[],[f1007,f57]) ).
fof(f1020,plain,
( $false
| ~ spl0_38
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f1019,f26]) ).
fof(f1021,plain,
( ~ spl0_38
| ~ spl0_48 ),
inference(avatar_contradiction_clause,[],[f1020]) ).
fof(f1036,plain,
( ! [X0] :
( ~ product1(e_2,e_3,X0)
| product2(X0,e_1,e_3) )
| ~ spl0_51 ),
inference(resolution,[],[f328,f48]) ).
fof(f1037,plain,
( product2(e_1,e_1,e_3)
| ~ spl0_36
| ~ spl0_51 ),
inference(resolution,[],[f1036,f260]) ).
fof(f1041,plain,
( equalish(e_1,e_3)
| ~ spl0_36
| ~ spl0_51 ),
inference(resolution,[],[f1037,f57]) ).
fof(f1042,plain,
( $false
| ~ spl0_36
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f1041,f27]) ).
fof(f1043,plain,
( ~ spl0_36
| ~ spl0_51 ),
inference(avatar_contradiction_clause,[],[f1042]) ).
cnf(s6,plain,
( spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f182]) ).
cnf(s7,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(sat_conversion,[],[f199]) ).
cnf(s8,plain,
( spl0_25
| spl0_26
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f216]) ).
cnf(s9,plain,
~ spl0_17,
inference(sat_conversion,[],[f223]) ).
cnf(s10,plain,
( spl0_29
| spl0_30
| spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f244]) ).
cnf(s11,plain,
( spl0_33
| spl0_34
| spl0_35
| spl0_36 ),
inference(sat_conversion,[],[f261]) ).
cnf(s12,plain,
( spl0_37
| spl0_38
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f278]) ).
cnf(s13,plain,
( spl0_41
| spl0_42
| spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f299]) ).
cnf(s14,plain,
( spl0_45
| spl0_46
| spl0_47
| spl0_48 ),
inference(sat_conversion,[],[f316]) ).
cnf(s15,plain,
( spl0_49
| spl0_50
| spl0_51
| spl0_52 ),
inference(sat_conversion,[],[f333]) ).
cnf(s31,plain,
~ spl0_29,
inference(sat_conversion,[],[f627]) ).
cnf(s32,plain,
~ spl0_41,
inference(sat_conversion,[],[f646]) ).
cnf(s33,plain,
~ spl0_42,
inference(sat_conversion,[],[f653]) ).
cnf(s34,plain,
( ~ spl0_33
| ~ spl0_43 ),
inference(sat_conversion,[],[f669]) ).
cnf(s35,plain,
( ~ spl0_30
| ~ spl0_45 ),
inference(sat_conversion,[],[f675]) ).
cnf(s36,plain,
~ spl0_31,
inference(sat_conversion,[],[f682]) ).
cnf(s37,plain,
~ spl0_34,
inference(sat_conversion,[],[f695]) ).
cnf(s39,plain,
( ~ spl0_25
| ~ spl0_32 ),
inference(sat_conversion,[],[f702]) ).
cnf(s41,plain,
~ spl0_27,
inference(sat_conversion,[],[f716]) ).
cnf(s43,plain,
~ spl0_28,
inference(sat_conversion,[],[f725]) ).
cnf(s45,plain,
~ spl0_35,
inference(sat_conversion,[],[f742]) ).
cnf(s48,plain,
~ spl0_46,
inference(sat_conversion,[],[f766]) ).
cnf(s50,plain,
( ~ spl0_21
| ~ spl0_44 ),
inference(sat_conversion,[],[f773]) ).
cnf(s51,plain,
~ spl0_22,
inference(sat_conversion,[],[f781]) ).
cnf(s54,plain,
~ spl0_24,
inference(sat_conversion,[],[f796]) ).
cnf(s58,plain,
~ spl0_47,
inference(sat_conversion,[],[f812]) ).
cnf(s61,plain,
( ~ spl0_23
| ~ spl0_48 ),
inference(sat_conversion,[],[f831]) ).
cnf(s63,plain,
( ~ spl0_18
| ~ spl0_49 ),
inference(sat_conversion,[],[f837]) ).
cnf(s64,plain,
( ~ spl0_19
| ~ spl0_37 ),
inference(sat_conversion,[],[f852]) ).
cnf(s66,plain,
~ spl0_40,
inference(sat_conversion,[],[f868]) ).
cnf(s70,plain,
( ~ spl0_23
| ~ spl0_38 ),
inference(sat_conversion,[],[f883]) ).
cnf(s71,plain,
~ spl0_50,
inference(sat_conversion,[],[f905]) ).
cnf(s74,plain,
~ spl0_39,
inference(sat_conversion,[],[f920]) ).
cnf(s78,plain,
( ~ spl0_26
| ~ spl0_51 ),
inference(sat_conversion,[],[f944]) ).
cnf(s79,plain,
~ spl0_20,
inference(sat_conversion,[],[f951]) ).
cnf(s80,plain,
~ spl0_52,
inference(sat_conversion,[],[f964]) ).
cnf(s85,plain,
( ~ spl0_26
| ~ spl0_36 ),
inference(sat_conversion,[],[f990]) ).
cnf(s87,plain,
( ~ spl0_38
| ~ spl0_48 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s90,plain,
( ~ spl0_36
| ~ spl0_51 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s91,plain,
( spl0_49
| spl0_51 ),
inference(rat,[],[s15,s80,s71]) ).
cnf(s92,plain,
( spl0_45
| spl0_48 ),
inference(rat,[],[s14,s58,s48]) ).
cnf(s93,plain,
( spl0_43
| spl0_44 ),
inference(rat,[],[s13,s33,s32]) ).
cnf(s94,plain,
( spl0_37
| spl0_38 ),
inference(rat,[],[s12,s66,s74]) ).
cnf(s95,plain,
( spl0_33
| spl0_36 ),
inference(rat,[],[s11,s45,s37]) ).
cnf(s96,plain,
( spl0_30
| spl0_32 ),
inference(rat,[],[s10,s36,s31]) ).
cnf(s97,plain,
( spl0_25
| spl0_26 ),
inference(rat,[],[s8,s43,s41]) ).
cnf(s98,plain,
( spl0_21
| spl0_23 ),
inference(rat,[],[s7,s54,s51]) ).
cnf(s99,plain,
( spl0_18
| spl0_19 ),
inference(rat,[],[s6,s79,s9]) ).
cnf(s100,plain,
~ spl0_38,
inference(rat,[],[s85,s95,s97,s34,s39,s93,s96,s50,s35,s98,s92,s70,s87]) ).
cnf(s101,plain,
spl0_37,
inference(rat,[],[s94,s100]) ).
cnf(s102,plain,
~ spl0_19,
inference(rat,[],[s64,s101]) ).
cnf(s103,plain,
spl0_18,
inference(rat,[],[s99,s102]) ).
cnf(s104,plain,
~ spl0_49,
inference(rat,[],[s63,s103]) ).
cnf(s105,plain,
spl0_51,
inference(rat,[],[s91,s104]) ).
cnf(s106,plain,
~ spl0_36,
inference(rat,[],[s90,s105]) ).
cnf(s107,plain,
~ spl0_26,
inference(rat,[],[s78,s105]) ).
cnf(s109,plain,
spl0_33,
inference(rat,[],[s95,s106]) ).
cnf(s110,plain,
spl0_25,
inference(rat,[],[s97,s107]) ).
cnf(s111,plain,
~ spl0_43,
inference(rat,[],[s34,s109]) ).
cnf(s112,plain,
~ spl0_32,
inference(rat,[],[s39,s110]) ).
cnf(s113,plain,
spl0_44,
inference(rat,[],[s93,s111]) ).
cnf(s114,plain,
spl0_30,
inference(rat,[],[s96,s112]) ).
cnf(s115,plain,
~ spl0_21,
inference(rat,[],[s50,s113]) ).
cnf(s116,plain,
~ spl0_45,
inference(rat,[],[s35,s114]) ).
cnf(s117,plain,
spl0_23,
inference(rat,[],[s98,s115]) ).
cnf(s118,plain,
spl0_48,
inference(rat,[],[s92,s116]) ).
cnf(s119,plain,
$false,
inference(rat,[],[s61,s118,s117]) ).
fof(f1044,plain,
$false,
inference(avatar_sat_refutation,[],[s119]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP124-8.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n009.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:21:15 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43 Running first-order model finding
% 0.11/0.43 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.16/0.48 % (1765608)Will run a generic schedule for satisfiability detection.
% 0.16/0.48 % (1765618)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=317174635:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.16/0.48 % (1765614)% WARNING: option uhcvi not known.
% 0.16/0.48 % (1765616)dis+10_1_sil=32000:sp=arity:random_seed=2819492842:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.16/0.48 % (1765613)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2916284090_2999 on theBenchmark for (2999ds/0Mi)
% 0.16/0.48 % (1765619)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1576249348:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.16/0.48 % (1765614)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4031837831:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.16/0.48 % (1765615)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=59370446:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.16/0.48 % (1765617)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1878506490:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.16/0.48 % (1765618) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1765608-1765618"...
% 0.16/0.48 % Detected minimum model sizes of [1]
% 0.16/0.48 % Detected maximum model sizes of [5]
% 0.16/0.48 % TRYING [1]
% 0.16/0.48 % TRYING [2]
% 0.16/0.48 % TRYING [3]
% 0.16/0.48 % (1765618)...printing done.
% 0.16/0.48 % (1765618)Refutation found. Thanks to Tanya!
% 0.16/0.48 % SZS status Unsatisfiable for theBenchmark
% 0.16/0.48 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/0.48 % (1765618)------------------------------
% 0.16/0.48 % (1765618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.16/0.48 % (1765618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/0.48 % (1765618)CaDiCaL version: 2.1.3
% 0.16/0.48 % (1765618)Termination reason: Refutation
% 0.16/0.48 % (1765618)Time elapsed: 0.009 s
% 0.16/0.48 % (1765618)Peak memory usage: 12 MB
% 0.16/0.48 % (1765618)Instructions burned: 23 (million)
% 0.16/0.48 % (1765608)Success in time 0.044 s
% 0.16/0.48 % Vampire exiting
%------------------------------------------------------------------------------