%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP124-9.004 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:12:43 AM UTC 2026
% Result : Unsatisfiable 3.10s 1.05s
% Output : Refutation 3.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 61
% Syntax : Number of formulae : 332 ( 79 unt; 44 def)
% Number of atoms : 832 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 923 ( 423 ~; 456 |; 0 &)
% ( 44 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 49 ( 48 usr; 45 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 72 ( 0 sgn 72 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
fof(f4,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
fof(f5,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
fof(f6,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
fof(f7,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f8,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f9,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f11,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f12,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f15,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f19,axiom,
! [X0,X1] :
( product1(X0,X1,e_4)
| ~ group_element(X1)
| product1(X0,X1,e_1)
| product1(X0,X1,e_2)
| product1(X0,X1,e_3)
| ~ group_element(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_total_function1) ).
fof(f21,axiom,
! [X2,X3,X0,X1] :
( equalish(X1,X3)
| ~ product1(X0,X3,X2)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_right_cancellation) ).
fof(f22,axiom,
! [X2,X3,X0,X1] :
( equalish(X0,X3)
| ~ product1(X3,X1,X2)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_left_cancellation) ).
fof(f23,axiom,
! [X0] : product1(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_idempotence) ).
fof(f25,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ product2(X0,X1,X3)
| ~ product2(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_total_function2) ).
fof(f28,axiom,
! [X0] : product2(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_idempotence) ).
fof(f29,negated_conjecture,
! [X2,X3,X0,X1] :
( product2(X3,X1,X0)
| ~ product1(X2,X0,X3)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg2a) ).
fof(f43,plain,
! [X0,X1] :
( ~ product1(X0,e_2,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f21,f7]) ).
fof(f44,plain,
! [X0,X1] :
( ~ product1(X0,e_3,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f21,f8]) ).
fof(f45,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f21,f9]) ).
fof(f47,plain,
! [X0,X1] :
( ~ product1(X0,e_3,X1)
| ~ product1(X0,e_2,X1) ),
inference(resolution,[],[f21,f11]) ).
fof(f48,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_2,X1) ),
inference(resolution,[],[f21,f12]) ).
fof(f51,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_3,X1) ),
inference(resolution,[],[f21,f15]) ).
fof(f55,plain,
! [X0,X1] :
( ~ product1(e_2,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f22,f7]) ).
fof(f56,plain,
! [X0,X1] :
( ~ product1(e_3,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f22,f8]) ).
fof(f57,plain,
! [X0,X1] :
( ~ product1(e_4,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f22,f9]) ).
fof(f59,plain,
! [X0,X1] :
( ~ product1(e_3,X0,X1)
| ~ product1(e_2,X0,X1) ),
inference(resolution,[],[f22,f11]) ).
fof(f60,plain,
! [X0,X1] :
( ~ product1(e_4,X0,X1)
| ~ product1(e_2,X0,X1) ),
inference(resolution,[],[f22,f12]) ).
fof(f68,plain,
! [X0,X1] :
( ~ product2(X0,X1,e_2)
| ~ product2(X0,X1,e_1) ),
inference(resolution,[],[f25,f7]) ).
fof(f69,plain,
! [X0,X1] :
( ~ product2(X0,X1,e_3)
| ~ product2(X0,X1,e_1) ),
inference(resolution,[],[f25,f8]) ).
fof(f111,plain,
~ product1(e_2,e_1,e_2),
inference(resolution,[],[f43,f23]) ).
fof(f112,plain,
! [X0] :
( ~ product1(X0,e_1,e_4)
| ~ group_element(e_2)
| product1(X0,e_2,e_1)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f43,f19]) ).
fof(f114,definition,
( spl0_1
<=> group_element(e_2) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f115,plain,
( ~ group_element(e_2)
| spl0_1 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f117,definition,
( spl0_2
<=> ! [X0] :
( ~ product1(X0,e_1,e_4)
| ~ group_element(X0)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f118,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product1(X0,e_1,e_4)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f117]) ).
fof(f119,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f112,f117,f114]) ).
fof(f120,plain,
( $false
| spl0_1 ),
inference(resolution,[],[f115,f4]) ).
fof(f121,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f120]) ).
fof(f124,plain,
( ~ product1(e_3,e_1,e_4)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_1)
| ~ spl0_2 ),
inference(resolution,[],[f118,f5]) ).
fof(f140,definition,
( spl0_7
<=> product1(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f141,plain,
( product1(e_3,e_2,e_1)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f140]) ).
fof(f143,definition,
( spl0_8
<=> product1(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f144,plain,
( product1(e_3,e_2,e_2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f143]) ).
fof(f146,definition,
( spl0_9
<=> product1(e_3,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f147,plain,
( product1(e_3,e_2,e_3)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f146]) ).
fof(f149,definition,
( spl0_10
<=> product1(e_3,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f150,plain,
( ~ product1(e_3,e_1,e_4)
| spl0_10 ),
inference(avatar_component_clause,[],[f149]) ).
fof(f151,plain,
( spl0_7
| spl0_8
| spl0_9
| ~ spl0_10
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f124,f117,f149,f146,f143,f140]) ).
fof(f153,definition,
( spl0_11
<=> product1(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f154,plain,
( product1(e_1,e_2,e_1)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f156,definition,
( spl0_12
<=> product1(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f157,plain,
( product1(e_1,e_2,e_2)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f156]) ).
fof(f159,definition,
( spl0_13
<=> product1(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f160,plain,
( product1(e_1,e_2,e_3)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f159]) ).
fof(f167,definition,
( spl0_15
<=> group_element(e_4) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f168,plain,
( ~ group_element(e_4)
| spl0_15 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f179,definition,
( spl0_19
<=> group_element(e_1) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f180,plain,
( ~ group_element(e_1)
| spl0_19 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f184,definition,
( spl0_20
<=> group_element(e_3) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f185,plain,
( ~ group_element(e_3)
| spl0_20 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f187,definition,
( spl0_21
<=> product1(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f188,plain,
( product1(e_3,e_1,e_3)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f190,definition,
( spl0_22
<=> product1(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f191,plain,
( product1(e_3,e_1,e_2)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f190]) ).
fof(f193,definition,
( spl0_23
<=> product1(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f194,plain,
( product1(e_3,e_1,e_1)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f193]) ).
fof(f196,plain,
( $false
| spl0_15 ),
inference(resolution,[],[f168,f6]) ).
fof(f197,plain,
spl0_15,
inference(avatar_contradiction_clause,[],[f196]) ).
fof(f200,plain,
( $false
| spl0_19 ),
inference(resolution,[],[f180,f3]) ).
fof(f201,plain,
spl0_19,
inference(avatar_contradiction_clause,[],[f200]) ).
fof(f205,plain,
( $false
| spl0_20 ),
inference(resolution,[],[f185,f5]) ).
fof(f206,plain,
spl0_20,
inference(avatar_contradiction_clause,[],[f205]) ).
fof(f207,plain,
( ~ product1(e_3,e_1,e_1)
| ~ spl0_7 ),
inference(resolution,[],[f141,f43]) ).
fof(f208,plain,
~ product1(e_3,e_1,e_3),
inference(resolution,[],[f44,f23]) ).
fof(f209,plain,
! [X0] :
( ~ product1(X0,e_1,e_4)
| ~ group_element(e_3)
| product1(X0,e_3,e_1)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f44,f19]) ).
fof(f211,definition,
( spl0_24
<=> ! [X0] :
( ~ product1(X0,e_1,e_4)
| ~ group_element(X0)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f212,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product1(X0,e_1,e_4)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_1) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f211]) ).
fof(f213,plain,
( ~ spl0_20
| spl0_24 ),
inference(avatar_split_clause,[],[f209,f211,f184]) ).
fof(f215,plain,
( ~ product1(e_2,e_1,e_4)
| product1(e_2,e_3,e_3)
| product1(e_2,e_3,e_2)
| product1(e_2,e_3,e_1)
| ~ spl0_24 ),
inference(resolution,[],[f212,f4]) ).
fof(f229,definition,
( spl0_28
<=> product1(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f230,plain,
( product1(e_2,e_3,e_1)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f232,definition,
( spl0_29
<=> product1(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f233,plain,
( product1(e_2,e_3,e_2)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f235,definition,
( spl0_30
<=> product1(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f236,plain,
( product1(e_2,e_3,e_3)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f238,definition,
( spl0_31
<=> product1(e_2,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f239,plain,
( ~ product1(e_2,e_1,e_4)
| spl0_31 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f240,plain,
( spl0_28
| spl0_29
| spl0_30
| ~ spl0_31
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f215,f211,f238,f235,f232,f229]) ).
fof(f245,definition,
( spl0_32
<=> product1(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f246,plain,
( product1(e_2,e_1,e_3)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f248,definition,
( spl0_33
<=> product1(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f249,plain,
( product1(e_2,e_1,e_2)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f251,definition,
( spl0_34
<=> product1(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f252,plain,
( product1(e_2,e_1,e_1)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f254,plain,
( ~ product1(e_2,e_1,e_1)
| ~ spl0_28 ),
inference(resolution,[],[f230,f44]) ).
fof(f271,definition,
( spl0_36
<=> product1(e_3,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f272,plain,
( product1(e_3,e_4,e_1)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f274,definition,
( spl0_37
<=> product1(e_3,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f275,plain,
( product1(e_3,e_4,e_2)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f277,definition,
( spl0_38
<=> product1(e_3,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f278,plain,
( product1(e_3,e_4,e_3)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f281,definition,
( spl0_39
<=> product1(e_2,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f282,plain,
( product1(e_2,e_4,e_1)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f284,definition,
( spl0_40
<=> product1(e_2,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f285,plain,
( product1(e_2,e_4,e_2)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f287,definition,
( spl0_41
<=> product1(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f288,plain,
( product1(e_2,e_4,e_3)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f294,plain,
( $false
| ~ spl0_21 ),
inference(resolution,[],[f188,f208]) ).
fof(f297,plain,
~ spl0_21,
inference(avatar_contradiction_clause,[],[f294]) ).
fof(f301,plain,
~ product1(e_3,e_2,e_3),
inference(resolution,[],[f47,f23]) ).
fof(f317,definition,
( spl0_44
<=> product1(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f318,plain,
( product1(e_1,e_3,e_1)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f317]) ).
fof(f320,definition,
( spl0_45
<=> product1(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f321,plain,
( product1(e_1,e_3,e_2)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f323,definition,
( spl0_46
<=> product1(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f324,plain,
( product1(e_1,e_3,e_3)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f326,definition,
( spl0_47
<=> product1(e_1,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f327,plain,
( ~ product1(e_1,e_2,e_4)
| spl0_47 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f332,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_11 ),
inference(resolution,[],[f154,f43]) ).
fof(f333,plain,
( $false
| ~ spl0_11 ),
inference(resolution,[],[f332,f23]) ).
fof(f334,plain,
~ spl0_11,
inference(avatar_contradiction_clause,[],[f333]) ).
fof(f338,plain,
! [X0] :
( ~ product1(X0,e_2,e_4)
| ~ group_element(e_4)
| product1(X0,e_4,e_1)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f48,f19]) ).
fof(f340,definition,
( spl0_48
<=> ! [X0] :
( ~ product1(X0,e_2,e_4)
| ~ group_element(X0)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f341,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product1(X0,e_2,e_4)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_1) )
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f342,plain,
( ~ spl0_15
| spl0_48 ),
inference(avatar_split_clause,[],[f338,f340,f167]) ).
fof(f345,plain,
( ~ product1(e_3,e_2,e_4)
| product1(e_3,e_4,e_3)
| product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1)
| ~ spl0_48 ),
inference(resolution,[],[f341,f5]) ).
fof(f348,definition,
( spl0_49
<=> product1(e_3,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f349,plain,
( ~ product1(e_3,e_2,e_4)
| spl0_49 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f350,plain,
( spl0_36
| spl0_37
| spl0_38
| ~ spl0_49
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f345,f340,f348,f277,f274,f271]) ).
fof(f355,plain,
( ~ group_element(e_2)
| product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_3)
| ~ group_element(e_3)
| spl0_49 ),
inference(resolution,[],[f349,f19]) ).
fof(f390,definition,
( spl0_58
<=> product1(e_1,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f391,plain,
( product1(e_1,e_4,e_1)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f393,definition,
( spl0_59
<=> product1(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f394,plain,
( product1(e_1,e_4,e_2)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f396,definition,
( spl0_60
<=> product1(e_1,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f397,plain,
( product1(e_1,e_4,e_3)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f399,definition,
( spl0_61
<=> product1(e_1,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f400,plain,
( ~ product1(e_1,e_3,e_4)
| spl0_61 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f409,plain,
( ~ group_element(e_3)
| product1(e_1,e_3,e_1)
| product1(e_1,e_3,e_2)
| product1(e_1,e_3,e_3)
| ~ group_element(e_1)
| spl0_61 ),
inference(resolution,[],[f400,f19]) ).
fof(f410,plain,
( ~ spl0_19
| spl0_46
| spl0_45
| spl0_44
| ~ spl0_20
| spl0_61 ),
inference(avatar_split_clause,[],[f409,f399,f184,f317,f320,f323,f179]) ).
fof(f412,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_44 ),
inference(resolution,[],[f318,f44]) ).
fof(f413,plain,
( $false
| ~ spl0_44 ),
inference(resolution,[],[f412,f23]) ).
fof(f414,plain,
~ spl0_44,
inference(avatar_contradiction_clause,[],[f413]) ).
fof(f415,plain,
( ~ product1(e_1,e_2,e_2)
| ~ spl0_45 ),
inference(resolution,[],[f321,f47]) ).
fof(f418,plain,
( $false
| ~ spl0_12
| ~ spl0_45 ),
inference(resolution,[],[f415,f157]) ).
fof(f419,plain,
( ~ spl0_12
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f418]) ).
fof(f426,plain,
! [X0] :
( ~ product1(e_1,X0,e_4)
| ~ group_element(X0)
| product1(e_2,X0,e_1)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_3)
| ~ group_element(e_2) ),
inference(resolution,[],[f55,f19]) ).
fof(f428,definition,
( spl0_62
<=> ! [X0] :
( ~ product1(e_1,X0,e_4)
| product1(e_2,X0,e_3)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_1)
| ~ group_element(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f429,plain,
( ! [X0] :
( ~ group_element(X0)
| product1(e_2,X0,e_3)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_1)
| ~ product1(e_1,X0,e_4) )
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f428]) ).
fof(f430,plain,
( ~ spl0_1
| spl0_62 ),
inference(avatar_split_clause,[],[f426,f428,f114]) ).
fof(f433,plain,
( product1(e_2,e_3,e_3)
| product1(e_2,e_3,e_2)
| product1(e_2,e_3,e_1)
| ~ product1(e_1,e_3,e_4)
| ~ spl0_62 ),
inference(resolution,[],[f429,f5]) ).
fof(f436,definition,
( spl0_63
<=> product1(e_1,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f437,plain,
( ~ product1(e_1,e_4,e_4)
| spl0_63 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f439,plain,
( ~ group_element(e_4)
| product1(e_1,e_4,e_1)
| product1(e_1,e_4,e_2)
| product1(e_1,e_4,e_3)
| ~ group_element(e_1)
| spl0_63 ),
inference(resolution,[],[f437,f19]) ).
fof(f440,plain,
( ~ spl0_19
| spl0_60
| spl0_59
| spl0_58
| ~ spl0_15
| spl0_63 ),
inference(avatar_split_clause,[],[f439,f436,f167,f390,f393,f396,f179]) ).
fof(f443,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_58 ),
inference(resolution,[],[f391,f45]) ).
fof(f446,plain,
~ product1(e_1,e_3,e_3),
inference(resolution,[],[f56,f23]) ).
fof(f447,plain,
! [X0] :
( ~ product1(e_1,X0,e_4)
| ~ group_element(X0)
| product1(e_3,X0,e_1)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_3)
| ~ group_element(e_3) ),
inference(resolution,[],[f56,f19]) ).
fof(f449,definition,
( spl0_64
<=> ! [X0] :
( ~ product1(e_1,X0,e_4)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_1)
| ~ group_element(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f450,plain,
( ! [X0] :
( ~ group_element(X0)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_1)
| ~ product1(e_1,X0,e_4) )
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f451,plain,
( ~ spl0_20
| spl0_64 ),
inference(avatar_split_clause,[],[f447,f449,f184]) ).
fof(f453,plain,
( product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_1)
| ~ product1(e_1,e_2,e_4)
| ~ spl0_64 ),
inference(resolution,[],[f450,f4]) ).
fof(f456,plain,
( $false
| ~ spl0_58 ),
inference(resolution,[],[f443,f23]) ).
fof(f457,plain,
~ spl0_58,
inference(avatar_contradiction_clause,[],[f456]) ).
fof(f458,plain,
( ~ product1(e_1,e_3,e_2)
| ~ spl0_59 ),
inference(resolution,[],[f394,f51]) ).
fof(f459,plain,
( ~ product1(e_1,e_2,e_2)
| ~ spl0_59 ),
inference(resolution,[],[f394,f48]) ).
fof(f462,plain,
( $false
| ~ spl0_45
| ~ spl0_59 ),
inference(resolution,[],[f458,f321]) ).
fof(f463,plain,
( ~ spl0_45
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f462]) ).
fof(f472,plain,
( $false
| ~ spl0_12
| ~ spl0_59 ),
inference(resolution,[],[f459,f157]) ).
fof(f473,plain,
( ~ spl0_12
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f472]) ).
fof(f477,plain,
~ product1(e_1,e_4,e_4),
inference(resolution,[],[f57,f23]) ).
fof(f487,plain,
( $false
| ~ spl0_46 ),
inference(resolution,[],[f446,f324]) ).
fof(f488,plain,
~ spl0_46,
inference(avatar_contradiction_clause,[],[f487]) ).
fof(f494,plain,
( ~ product1(e_1,e_2,e_3)
| ~ spl0_60 ),
inference(resolution,[],[f397,f48]) ).
fof(f500,plain,
~ product1(e_2,e_3,e_3),
inference(resolution,[],[f59,f23]) ).
fof(f501,plain,
! [X0] :
( ~ product1(e_2,X0,e_4)
| ~ group_element(X0)
| product1(e_3,X0,e_1)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_3)
| ~ group_element(e_3) ),
inference(resolution,[],[f59,f19]) ).
fof(f503,definition,
( spl0_66
<=> ! [X0] :
( ~ product1(e_2,X0,e_4)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_1)
| ~ group_element(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f504,plain,
( ! [X0] :
( ~ group_element(X0)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_1)
| ~ product1(e_2,X0,e_4) )
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f505,plain,
( ~ spl0_20
| spl0_66 ),
inference(avatar_split_clause,[],[f501,f503,f184]) ).
fof(f506,plain,
( product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_1)
| ~ product1(e_2,e_1,e_4)
| ~ spl0_66 ),
inference(resolution,[],[f504,f3]) ).
fof(f511,definition,
( spl0_67
<=> product1(e_2,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f512,plain,
( ~ product1(e_2,e_4,e_4)
| spl0_67 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f514,plain,
( ~ group_element(e_4)
| product1(e_2,e_4,e_1)
| product1(e_2,e_4,e_2)
| product1(e_2,e_4,e_3)
| ~ group_element(e_2)
| spl0_67 ),
inference(resolution,[],[f512,f19]) ).
fof(f515,plain,
( ~ spl0_1
| spl0_41
| spl0_40
| spl0_39
| ~ spl0_15
| spl0_67 ),
inference(avatar_split_clause,[],[f514,f511,f167,f281,f284,f287,f114]) ).
fof(f517,plain,
( ~ product1(e_2,e_3,e_1)
| ~ spl0_39 ),
inference(resolution,[],[f282,f51]) ).
fof(f519,plain,
( ~ product1(e_2,e_1,e_1)
| ~ spl0_39 ),
inference(resolution,[],[f282,f45]) ).
fof(f520,plain,
( $false
| ~ spl0_28
| ~ spl0_39 ),
inference(resolution,[],[f517,f230]) ).
fof(f521,plain,
( ~ spl0_28
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f520]) ).
fof(f524,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_29 ),
inference(resolution,[],[f233,f47]) ).
fof(f536,plain,
( $false
| ~ spl0_33 ),
inference(resolution,[],[f249,f111]) ).
fof(f539,plain,
~ spl0_33,
inference(avatar_contradiction_clause,[],[f536]) ).
fof(f543,plain,
~ product1(e_2,e_4,e_4),
inference(resolution,[],[f60,f23]) ).
fof(f553,plain,
( $false
| ~ spl0_30 ),
inference(resolution,[],[f500,f236]) ).
fof(f554,plain,
~ spl0_30,
inference(avatar_contradiction_clause,[],[f553]) ).
fof(f560,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_40 ),
inference(resolution,[],[f285,f48]) ).
fof(f570,plain,
( $false
| ~ spl0_40 ),
inference(resolution,[],[f560,f23]) ).
fof(f571,plain,
~ spl0_40,
inference(avatar_contradiction_clause,[],[f570]) ).
fof(f572,plain,
( ~ product1(e_1,e_4,e_3)
| ~ spl0_41 ),
inference(resolution,[],[f288,f55]) ).
fof(f586,plain,
( $false
| ~ spl0_41
| ~ spl0_60 ),
inference(resolution,[],[f572,f397]) ).
fof(f587,plain,
( ~ spl0_41
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f586]) ).
fof(f627,plain,
( ~ product1(e_3,e_1,e_1)
| ~ spl0_36 ),
inference(resolution,[],[f272,f45]) ).
fof(f631,plain,
( ~ product1(e_1,e_4,e_2)
| ~ spl0_37 ),
inference(resolution,[],[f275,f56]) ).
fof(f638,plain,
( $false
| ~ spl0_7
| ~ spl0_23 ),
inference(resolution,[],[f194,f207]) ).
fof(f641,plain,
( ~ spl0_7
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f638]) ).
fof(f642,plain,
! [X2,X0,X1] :
( ~ product2(X0,X1,e_1)
| ~ product1(X2,e_2,X0)
| ~ product1(e_2,X1,X2) ),
inference(resolution,[],[f68,f29]) ).
fof(f644,plain,
! [X2,X0,X1] :
( ~ product2(X0,X1,e_1)
| ~ product1(X2,e_3,X0)
| ~ product1(e_3,X1,X2) ),
inference(resolution,[],[f69,f29]) ).
fof(f647,plain,
! [X0] :
( ~ product1(X0,e_2,e_1)
| ~ product1(e_2,e_1,X0) ),
inference(resolution,[],[f642,f28]) ).
fof(f651,plain,
( ~ product1(e_2,e_1,e_3)
| ~ spl0_7 ),
inference(resolution,[],[f647,f141]) ).
fof(f652,plain,
( $false
| ~ spl0_7
| ~ spl0_32 ),
inference(resolution,[],[f651,f246]) ).
fof(f653,plain,
( ~ spl0_7
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f652]) ).
fof(f654,plain,
( $false
| ~ spl0_34
| ~ spl0_39 ),
inference(resolution,[],[f252,f519]) ).
fof(f657,plain,
( ~ spl0_34
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f654]) ).
fof(f658,plain,
( ~ spl0_61
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f433,f428,f235,f232,f229,f399]) ).
fof(f659,plain,
( ~ spl0_31
| spl0_23
| spl0_22
| spl0_21
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f506,f503,f187,f190,f193,f238]) ).
fof(f660,plain,
( ~ spl0_20
| spl0_9
| spl0_8
| spl0_7
| ~ spl0_1
| spl0_49 ),
inference(avatar_split_clause,[],[f355,f348,f114,f140,f143,f146,f184]) ).
fof(f661,plain,
( ~ spl0_47
| spl0_7
| spl0_8
| spl0_9
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f453,f449,f146,f143,f140,f326]) ).
fof(f662,plain,
( $false
| ~ spl0_9 ),
inference(resolution,[],[f147,f301]) ).
fof(f668,plain,
~ spl0_9,
inference(avatar_contradiction_clause,[],[f662]) ).
fof(f670,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_8 ),
inference(resolution,[],[f144,f59]) ).
fof(f681,plain,
( ~ product1(e_2,e_4,e_3)
| ~ spl0_38 ),
inference(resolution,[],[f278,f59]) ).
fof(f691,plain,
( $false
| ~ spl0_29 ),
inference(resolution,[],[f524,f23]) ).
fof(f692,plain,
~ spl0_29,
inference(avatar_contradiction_clause,[],[f691]) ).
fof(f702,plain,
( $false
| ~ spl0_8 ),
inference(resolution,[],[f670,f23]) ).
fof(f703,plain,
~ spl0_8,
inference(avatar_contradiction_clause,[],[f702]) ).
fof(f704,plain,
( ~ group_element(e_1)
| product1(e_3,e_1,e_1)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| ~ group_element(e_3)
| spl0_10 ),
inference(resolution,[],[f150,f19]) ).
fof(f719,plain,
! [X0] :
( ~ product1(X0,e_3,e_1)
| ~ product1(e_3,e_1,X0) ),
inference(resolution,[],[f644,f28]) ).
fof(f720,plain,
( ~ group_element(e_2)
| product1(e_1,e_2,e_1)
| product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| ~ group_element(e_1)
| spl0_47 ),
inference(resolution,[],[f327,f19]) ).
fof(f728,plain,
( $false
| ~ spl0_13
| ~ spl0_60 ),
inference(resolution,[],[f494,f160]) ).
fof(f729,plain,
( ~ spl0_13
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f728]) ).
fof(f730,plain,
~ spl0_67,
inference(avatar_split_clause,[],[f543,f511]) ).
fof(f733,plain,
( ~ spl0_19
| spl0_13
| spl0_12
| spl0_11
| ~ spl0_1
| spl0_47 ),
inference(avatar_split_clause,[],[f720,f326,f114,f153,f156,f159,f179]) ).
fof(f734,plain,
~ spl0_63,
inference(avatar_split_clause,[],[f477,f436]) ).
fof(f765,plain,
( $false
| ~ spl0_38
| ~ spl0_41 ),
inference(resolution,[],[f681,f288]) ).
fof(f766,plain,
( ~ spl0_38
| ~ spl0_41 ),
inference(avatar_contradiction_clause,[],[f765]) ).
fof(f773,plain,
( $false
| ~ spl0_23
| ~ spl0_36 ),
inference(resolution,[],[f627,f194]) ).
fof(f774,plain,
( ~ spl0_23
| ~ spl0_36 ),
inference(avatar_contradiction_clause,[],[f773]) ).
fof(f781,plain,
( $false
| ~ spl0_37
| ~ spl0_59 ),
inference(resolution,[],[f631,f394]) ).
fof(f782,plain,
( ~ spl0_37
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f781]) ).
fof(f783,plain,
( ~ spl0_20
| spl0_21
| spl0_22
| spl0_23
| ~ spl0_19
| spl0_10 ),
inference(avatar_split_clause,[],[f704,f149,f179,f193,f190,f187,f184]) ).
fof(f789,plain,
( ~ product1(e_2,e_3,e_1)
| ~ spl0_22 ),
inference(resolution,[],[f191,f719]) ).
fof(f793,plain,
( $false
| ~ spl0_22
| ~ spl0_28 ),
inference(resolution,[],[f789,f230]) ).
fof(f794,plain,
( ~ spl0_22
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f793]) ).
fof(f799,plain,
( ~ group_element(e_1)
| product1(e_2,e_1,e_1)
| product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| ~ group_element(e_2)
| spl0_31 ),
inference(resolution,[],[f239,f19]) ).
fof(f800,plain,
( ~ spl0_1
| spl0_32
| spl0_33
| spl0_34
| ~ spl0_19
| spl0_31 ),
inference(avatar_split_clause,[],[f799,f238,f179,f251,f248,f245,f114]) ).
fof(f801,plain,
( $false
| ~ spl0_28
| ~ spl0_34 ),
inference(resolution,[],[f252,f254]) ).
fof(f804,plain,
( ~ spl0_28
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f801]) ).
cnf(s1,plain,
( ~ spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f119]) ).
cnf(s2,plain,
spl0_1,
inference(sat_conversion,[],[f121]) ).
cnf(s4,plain,
( ~ spl0_2
| spl0_7
| spl0_8
| spl0_9
| ~ spl0_10 ),
inference(sat_conversion,[],[f151]) ).
cnf(s8,plain,
spl0_15,
inference(sat_conversion,[],[f197]) ).
cnf(s9,plain,
spl0_19,
inference(sat_conversion,[],[f201]) ).
cnf(s10,plain,
spl0_20,
inference(sat_conversion,[],[f206]) ).
cnf(s11,plain,
( ~ spl0_20
| spl0_24 ),
inference(sat_conversion,[],[f213]) ).
cnf(s13,plain,
( ~ spl0_24
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_31 ),
inference(sat_conversion,[],[f240]) ).
cnf(s22,plain,
~ spl0_21,
inference(sat_conversion,[],[f297]) ).
cnf(s27,plain,
~ spl0_11,
inference(sat_conversion,[],[f334]) ).
cnf(s28,plain,
( ~ spl0_15
| spl0_48 ),
inference(sat_conversion,[],[f342]) ).
cnf(s29,plain,
( spl0_36
| spl0_37
| spl0_38
| ~ spl0_48
| ~ spl0_49 ),
inference(sat_conversion,[],[f350]) ).
cnf(s37,plain,
( ~ spl0_19
| ~ spl0_20
| spl0_44
| spl0_45
| spl0_46
| spl0_61 ),
inference(sat_conversion,[],[f410]) ).
cnf(s38,plain,
~ spl0_44,
inference(sat_conversion,[],[f414]) ).
cnf(s39,plain,
( ~ spl0_12
| ~ spl0_45 ),
inference(sat_conversion,[],[f419]) ).
cnf(s40,plain,
( ~ spl0_1
| spl0_62 ),
inference(sat_conversion,[],[f430]) ).
cnf(s42,plain,
( ~ spl0_15
| ~ spl0_19
| spl0_58
| spl0_59
| spl0_60
| spl0_63 ),
inference(sat_conversion,[],[f440]) ).
cnf(s43,plain,
( ~ spl0_20
| spl0_64 ),
inference(sat_conversion,[],[f451]) ).
cnf(s44,plain,
~ spl0_58,
inference(sat_conversion,[],[f457]) ).
cnf(s45,plain,
( ~ spl0_45
| ~ spl0_59 ),
inference(sat_conversion,[],[f463]) ).
cnf(s47,plain,
( ~ spl0_12
| ~ spl0_59 ),
inference(sat_conversion,[],[f473]) ).
cnf(s49,plain,
~ spl0_46,
inference(sat_conversion,[],[f488]) ).
cnf(s51,plain,
( ~ spl0_20
| spl0_66 ),
inference(sat_conversion,[],[f505]) ).
cnf(s53,plain,
( ~ spl0_1
| ~ spl0_15
| spl0_39
| spl0_40
| spl0_41
| spl0_67 ),
inference(sat_conversion,[],[f515]) ).
cnf(s54,plain,
( ~ spl0_28
| ~ spl0_39 ),
inference(sat_conversion,[],[f521]) ).
cnf(s58,plain,
~ spl0_33,
inference(sat_conversion,[],[f539]) ).
cnf(s60,plain,
~ spl0_30,
inference(sat_conversion,[],[f554]) ).
cnf(s62,plain,
~ spl0_40,
inference(sat_conversion,[],[f571]) ).
cnf(s64,plain,
( ~ spl0_41
| ~ spl0_60 ),
inference(sat_conversion,[],[f587]) ).
cnf(s73,plain,
( ~ spl0_7
| ~ spl0_23 ),
inference(sat_conversion,[],[f641]) ).
cnf(s74,plain,
( ~ spl0_7
| ~ spl0_32 ),
inference(sat_conversion,[],[f653]) ).
cnf(s75,plain,
( ~ spl0_34
| ~ spl0_39 ),
inference(sat_conversion,[],[f657]) ).
cnf(s76,plain,
( spl0_28
| spl0_29
| spl0_30
| ~ spl0_61
| ~ spl0_62 ),
inference(sat_conversion,[],[f658]) ).
cnf(s77,plain,
( spl0_21
| spl0_22
| spl0_23
| ~ spl0_31
| ~ spl0_66 ),
inference(sat_conversion,[],[f659]) ).
cnf(s78,plain,
( ~ spl0_1
| spl0_7
| spl0_8
| spl0_9
| ~ spl0_20
| spl0_49 ),
inference(sat_conversion,[],[f660]) ).
cnf(s79,plain,
( spl0_7
| spl0_8
| spl0_9
| ~ spl0_47
| ~ spl0_64 ),
inference(sat_conversion,[],[f661]) ).
cnf(s80,plain,
~ spl0_9,
inference(sat_conversion,[],[f668]) ).
cnf(s82,plain,
~ spl0_29,
inference(sat_conversion,[],[f692]) ).
cnf(s84,plain,
~ spl0_8,
inference(sat_conversion,[],[f703]) ).
cnf(s90,plain,
( ~ spl0_13
| ~ spl0_60 ),
inference(sat_conversion,[],[f729]) ).
cnf(s91,plain,
~ spl0_67,
inference(sat_conversion,[],[f730]) ).
cnf(s94,plain,
( ~ spl0_1
| spl0_11
| spl0_12
| spl0_13
| ~ spl0_19
| spl0_47 ),
inference(sat_conversion,[],[f733]) ).
cnf(s95,plain,
~ spl0_63,
inference(sat_conversion,[],[f734]) ).
cnf(s98,plain,
( ~ spl0_38
| ~ spl0_41 ),
inference(sat_conversion,[],[f766]) ).
cnf(s99,plain,
( ~ spl0_23
| ~ spl0_36 ),
inference(sat_conversion,[],[f774]) ).
cnf(s100,plain,
( ~ spl0_37
| ~ spl0_59 ),
inference(sat_conversion,[],[f782]) ).
cnf(s101,plain,
( spl0_10
| ~ spl0_19
| ~ spl0_20
| spl0_21
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f783]) ).
cnf(s102,plain,
( ~ spl0_22
| ~ spl0_28 ),
inference(sat_conversion,[],[f794]) ).
cnf(s103,plain,
( ~ spl0_1
| ~ spl0_19
| spl0_31
| spl0_32
| spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f800]) ).
cnf(s104,plain,
( ~ spl0_28
| ~ spl0_34 ),
inference(sat_conversion,[],[f804]) ).
cnf(s105,plain,
( spl0_7
| ~ spl0_47
| ~ spl0_64 ),
inference(rat,[],[s79,s80,s84]) ).
cnf(s106,plain,
( ~ spl0_1
| spl0_7
| ~ spl0_20
| spl0_49 ),
inference(rat,[],[s78,s80,s84]) ).
cnf(s107,plain,
( spl0_28
| spl0_30
| ~ spl0_61
| ~ spl0_62 ),
inference(rat,[],[s76,s82]) ).
cnf(s109,plain,
( ~ spl0_1
| ~ spl0_15
| spl0_39
| spl0_41 ),
inference(rat,[],[s53,s91,s62]) ).
cnf(s110,plain,
( ~ spl0_15
| ~ spl0_19
| spl0_59
| spl0_60 ),
inference(rat,[],[s42,s95,s44]) ).
cnf(s111,plain,
( ~ spl0_19
| ~ spl0_20
| spl0_45
| spl0_61 ),
inference(rat,[],[s37,s49,s38]) ).
cnf(s121,plain,
( ~ spl0_24
| spl0_28
| ~ spl0_31 ),
inference(rat,[],[s13,s60,s82]) ).
cnf(s122,plain,
spl0_66,
inference(rat,[],[s51,s10]) ).
cnf(s123,plain,
spl0_64,
inference(rat,[],[s43,s10]) ).
cnf(s125,plain,
spl0_24,
inference(rat,[],[s11,s10]) ).
cnf(s130,plain,
spl0_48,
inference(rat,[],[s28,s8]) ).
cnf(s135,plain,
( ~ spl0_2
| spl0_7
| ~ spl0_10 ),
inference(rat,[],[s4,s80,s84]) ).
cnf(s136,plain,
spl0_62,
inference(rat,[],[s40,s2]) ).
cnf(s137,plain,
spl0_2,
inference(rat,[],[s1,s2]) ).
cnf(s138,plain,
( spl0_28
| spl0_32 ),
inference(rat,[],[s64,s109,s110,s75,s45,s103,s111,s121,s107,s8,s2,s9,s58,s10,s125,s60,s136]) ).
cnf(s139,plain,
~ spl0_7,
inference(rat,[],[s77,s103,s102,s104,s138,s73,s74,s22,s122,s9,s2,s58]) ).
cnf(s140,plain,
~ spl0_47,
inference(rat,[],[s105,s123,s139]) ).
cnf(s141,plain,
spl0_49,
inference(rat,[],[s106,s2,s10,s139]) ).
cnf(s142,plain,
~ spl0_10,
inference(rat,[],[s135,s137,s139]) ).
cnf(s143,plain,
~ spl0_12,
inference(rat,[],[s54,s109,s107,s64,s111,s110,s39,s47,s8,s2,s60,s136,s10,s9]) ).
cnf(s144,plain,
spl0_13,
inference(rat,[],[s94,s140,s9,s2,s27,s143]) ).
cnf(s145,plain,
~ spl0_60,
inference(rat,[],[s90,s144]) ).
cnf(s147,plain,
spl0_59,
inference(rat,[],[s110,s8,s9,s145]) ).
cnf(s148,plain,
~ spl0_37,
inference(rat,[],[s100,s147]) ).
cnf(s149,plain,
~ spl0_45,
inference(rat,[],[s45,s147]) ).
cnf(s150,plain,
spl0_61,
inference(rat,[],[s111,s9,s10,s149]) ).
cnf(s151,plain,
spl0_28,
inference(rat,[],[s107,s136,s60,s150]) ).
cnf(s153,plain,
~ spl0_22,
inference(rat,[],[s102,s151]) ).
cnf(s155,plain,
~ spl0_39,
inference(rat,[],[s54,s151]) ).
cnf(s156,plain,
spl0_23,
inference(rat,[],[s101,s142,s9,s22,s10,s153]) ).
cnf(s157,plain,
spl0_41,
inference(rat,[],[s109,s2,s8,s155]) ).
cnf(s158,plain,
~ spl0_36,
inference(rat,[],[s99,s156]) ).
cnf(s159,plain,
~ spl0_38,
inference(rat,[],[s98,s157]) ).
cnf(s162,plain,
$false,
inference(rat,[],[s29,s141,s130,s148,s159,s158]) ).
fof(f805,plain,
$false,
inference(avatar_sat_refutation,[],[s162]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP124-9.004 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n008.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 09:24:39 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.10/1.05 % (969441)Input is clausal, will run a generic CNF schedule.
% 3.10/1.05 % (969451)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3558450670:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.10/1.05 % (969447)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4032708017:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.10/1.05 % (969448)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1958136034:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.10/1.05 % (969446)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=3639850559:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.10/1.05 % (969449)lrs+10_1_sil=8000:sp=occurrence:random_seed=1950938367:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.10/1.05 % (969452)dis-21_1_sil=8000:lcm=predicate:random_seed=2359396598:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.10/1.05 % (969450)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3925054923:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.10/1.05 % (969452)First to succeed.
% 3.10/1.05 % (969451)Also succeeded, but the first one will report.
% 3.10/1.05 % (969452)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-969441"
% 3.10/1.05 % (969449)Instruction limit reached!
% 3.10/1.05 % (969449)------------------------------
% 3.10/1.05 % (969449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.05 % (969449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.05 % (969449)CaDiCaL version: 2.1.3
% 3.10/1.05 % (969449)Termination reason: Instruction limit
% 3.10/1.05 % (969449)Termination phase: Saturation
% 3.10/1.05 % (969449)Time elapsed: 0.061 s
% 3.10/1.05 % (969449)Peak memory usage: 88 MB
% 3.10/1.05 % (969449)Instructions burned: 108 (million)
% 3.10/1.05 % (969450)Instruction limit reached!
% 3.10/1.05 % (969450)------------------------------
% 3.10/1.05 % (969450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.05 % (969450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.05 % (969450)CaDiCaL version: 2.1.3
% 3.10/1.05 % (969450)Termination reason: Instruction limit
% 3.10/1.05 % (969450)Termination phase: Saturation
% 3.10/1.05 % (969450)Time elapsed: 0.061 s
% 3.10/1.05 % (969450)Peak memory usage: 88 MB
% 3.10/1.05 % (969450)Instructions burned: 114 (million)
% 3.10/1.05 % (969460)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=4192745644:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 3.10/1.05 % (969461)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1710716591:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 3.10/1.05 % (969461)Refutation not found, incomplete strategy
% 3.10/1.05 % (969461)------------------------------
% 3.10/1.05 % (969461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.05 % (969461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.05 % (969461)CaDiCaL version: 2.1.3
% 3.10/1.05 % (969461)Termination reason: Refutation not found, incomplete strategy
% 3.10/1.05 % (969461)Time elapsed: 0.002 s
% 3.10/1.05 % (969461)Peak memory usage: 87 MB
% 3.10/1.05 % (969461)Instructions burned: 1 (million)
% 3.10/1.05 % (969452)Refutation found. Thanks to Tanya!
% 3.10/1.05 % SZS status Unsatisfiable for theBenchmark
% 3.10/1.05 % SZS output start Proof for theBenchmark
% See solution above
% 3.39/1.15 % (969452)------------------------------
% 3.39/1.15 % (969452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.39/1.15 % (969452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.39/1.15 % (969452)CaDiCaL version: 2.1.3
% 3.39/1.15 % (969452)Termination reason: Refutation
% 3.39/1.15 % (969452)Time elapsed: 0.015 s
% 3.39/1.15 % (969452)Peak memory usage: 89 MB
% 3.39/1.15 % (969452)Instructions burned: 22 (million)
% 3.39/1.15 % (969452)------------------------------
% 3.39/1.15 % (969452)------------------------------
% 3.39/1.15 % (969441)Success in time 0.431 s
% 3.39/1.15 % Vampire exiting
%------------------------------------------------------------------------------