%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP129-2.004 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:58 AM UTC 2026
% Result : Unsatisfiable 3.08s 1.36s
% Output : Refutation 4.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 80
% Syntax : Number of formulae : 612 ( 74 unt; 59 def)
% Number of atoms : 1900 ( 0 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 2096 ( 808 ~;1229 |; 0 &)
% ( 59 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 65 ( 64 usr; 60 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 167 ( 0 sgn 167 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_then_e_2) ).
fof(f2,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_then_e_3) ).
fof(f7,axiom,
greater(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_2) ).
fof(f8,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_2) ).
fof(f9,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_3) ).
fof(f10,axiom,
! [X2,X0,X1] :
( ~ greater(X1,X2)
| ~ next(X0,X2)
| ~ product(X0,e_1,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_redundancy) ).
fof(f11,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
fof(f12,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
fof(f13,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
fof(f14,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
fof(f15,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f16,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f17,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f19,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f20,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f23,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f27,axiom,
! [X0,X1] :
( product(X0,X1,e_4)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| ~ group_element(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
fof(f28,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function2) ).
fof(f29,axiom,
! [X2,X3,X0,X1] :
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f30,axiom,
! [X2,X3,X0,X1] :
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_left_cancellation) ).
fof(f31,negated_conjecture,
! [X2,X3,X0,X1] :
( product(X2,X0,X3)
| ~ product(X1,X2,X3)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3) ).
fof(f35,plain,
! [X0] :
( ~ product(X0,e_1,e_3)
| ~ next(X0,e_2) ),
inference(resolution,[],[f7,f10]) ).
fof(f36,plain,
! [X0] :
( ~ next(X0,e_2)
| ~ product(X0,e_1,e_4) ),
inference(resolution,[],[f8,f10]) ).
fof(f37,plain,
! [X0] :
( ~ next(X0,e_3)
| ~ product(X0,e_1,e_4) ),
inference(resolution,[],[f9,f10]) ).
fof(f38,plain,
! [X0,X1] :
( ~ product(e_2,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[],[f15,f30]) ).
fof(f39,plain,
! [X0,X1] :
( ~ product(X0,e_2,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f15,f29]) ).
fof(f41,plain,
! [X0,X1] :
( ~ product(e_3,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[],[f16,f30]) ).
fof(f42,plain,
! [X0,X1] :
( ~ product(X0,e_3,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f16,f29]) ).
fof(f44,plain,
! [X0,X1] :
( ~ product(e_4,X0,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[],[f17,f30]) ).
fof(f45,plain,
! [X0,X1] :
( ~ product(X0,e_4,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f17,f29]) ).
fof(f50,plain,
! [X0,X1] :
( ~ product(e_3,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(resolution,[],[f19,f30]) ).
fof(f51,plain,
! [X0,X1] :
( ~ product(X0,e_3,X1)
| ~ product(X0,e_2,X1) ),
inference(resolution,[],[f19,f29]) ).
fof(f53,plain,
! [X0,X1] :
( ~ product(e_4,X0,X1)
| ~ product(e_2,X0,X1) ),
inference(resolution,[],[f20,f30]) ).
fof(f54,plain,
! [X0,X1] :
( ~ product(X0,e_4,X1)
| ~ product(X0,e_2,X1) ),
inference(resolution,[],[f20,f29]) ).
fof(f55,plain,
! [X0,X1] :
( ~ product(X0,X1,e_2)
| ~ product(X0,X1,e_4) ),
inference(resolution,[],[f20,f28]) ).
fof(f62,plain,
! [X0,X1] :
( ~ product(e_3,X0,X1)
| ~ product(e_4,X0,X1) ),
inference(resolution,[],[f23,f30]) ).
fof(f63,plain,
! [X0,X1] :
( ~ product(X0,e_4,X1)
| ~ product(X0,e_3,X1) ),
inference(resolution,[],[f23,f29]) ).
fof(f74,plain,
! [X0,X1] :
( ~ next(X0,e_2)
| ~ product(X1,X0,e_3)
| ~ product(e_1,X1,X0) ),
inference(resolution,[],[f35,f31]) ).
fof(f75,plain,
~ product(e_1,e_1,e_4),
inference(resolution,[],[f36,f1]) ).
fof(f76,plain,
! [X0] :
( ~ product(e_1,X0,e_1)
| ~ product(X0,e_1,e_3) ),
inference(resolution,[],[f74,f1]) ).
fof(f77,plain,
~ product(e_2,e_1,e_4),
inference(resolution,[],[f37,f2]) ).
fof(f79,plain,
! [X2,X0,X1] :
( ~ product(X0,X2,e_2)
| ~ product(X2,e_2,X1)
| ~ product(e_1,X0,X1) ),
inference(resolution,[],[f38,f31]) ).
fof(f80,plain,
! [X0] :
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| ~ group_element(e_2) ),
inference(resolution,[],[f38,f27]) ).
fof(f81,plain,
! [X0] :
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f80,f12]) ).
fof(f86,definition,
( spl0_1
<=> product(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f87,plain,
( product(e_1,e_2,e_2)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f86]) ).
fof(f88,plain,
( ~ product(e_1,e_2,e_2)
| spl0_1 ),
inference(avatar_component_clause,[],[f86]) ).
fof(f90,definition,
( spl0_2
<=> product(e_1,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f94,plain,
! [X2,X0,X1] :
( ~ product(e_2,X2,X0)
| ~ product(X2,X0,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f39,f31]) ).
fof(f95,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f39,f27]) ).
fof(f96,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f95,f12]) ).
fof(f97,plain,
( ! [X0] :
( ~ product(e_2,X0,e_1)
| ~ product(X0,e_1,e_2) )
| spl0_1 ),
inference(resolution,[],[f88,f31]) ).
fof(f109,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f42,f27]) ).
fof(f110,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f109,f13]) ).
fof(f117,plain,
! [X2,X0,X1] :
( ~ product(e_1,X0,X1)
| ~ product(X2,e_4,X1)
| ~ product(X0,X2,e_4) ),
inference(resolution,[],[f44,f31]) ).
fof(f118,plain,
! [X0] :
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| ~ group_element(e_4) ),
inference(resolution,[],[f44,f27]) ).
fof(f119,plain,
! [X0] :
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f118,f14]) ).
fof(f125,definition,
( spl0_3
<=> product(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f129,definition,
( spl0_4
<=> product(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f130,plain,
( product(e_3,e_1,e_3)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f129]) ).
fof(f131,plain,
( ~ product(e_3,e_1,e_3)
| spl0_4 ),
inference(avatar_component_clause,[],[f129]) ).
fof(f134,plain,
! [X2,X0,X1] :
( ~ product(e_4,X2,X0)
| ~ product(X2,X0,X1)
| ~ product(X0,e_1,X1) ),
inference(resolution,[],[f45,f31]) ).
fof(f135,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| ~ group_element(e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f45,f27]) ).
fof(f136,plain,
! [X0] :
( ~ product(X0,e_1,e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f135,f14]) ).
fof(f144,plain,
! [X0] :
( ~ product(e_1,e_4,X0)
| ~ product(e_4,e_1,e_4) ),
inference(factoring,[],[f117]) ).
fof(f147,definition,
( spl0_5
<=> product(e_4,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f149,plain,
( ~ product(e_4,e_1,e_4)
| spl0_5 ),
inference(avatar_component_clause,[],[f147]) ).
fof(f151,definition,
( spl0_6
<=> ! [X0] : ~ product(e_1,e_4,X0) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f152,plain,
( ! [X0] : ~ product(e_1,e_4,X0)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f153,plain,
( ~ spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f144,f151,f147]) ).
fof(f160,definition,
( spl0_7
<=> product(e_4,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f162,plain,
( product(e_4,e_1,e_3)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f160]) ).
fof(f164,definition,
( spl0_8
<=> product(e_4,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f166,plain,
( product(e_4,e_1,e_2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f164]) ).
fof(f168,definition,
( spl0_9
<=> product(e_4,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f170,plain,
( product(e_4,e_1,e_1)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f168]) ).
fof(f172,plain,
! [X2,X0,X1] :
( ~ product(e_2,X0,X1)
| ~ product(X2,e_3,X1)
| ~ product(X0,X2,e_3) ),
inference(resolution,[],[f50,f31]) ).
fof(f176,plain,
! [X2,X0,X1] :
( ~ product(e_3,X2,X0)
| ~ product(X2,X0,X1)
| ~ product(X0,e_2,X1) ),
inference(resolution,[],[f51,f31]) ).
fof(f177,plain,
! [X0] :
( ~ product(X0,e_2,e_4)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f51,f27]) ).
fof(f178,plain,
! [X0] :
( ~ product(X0,e_2,e_4)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f177,f13]) ).
fof(f180,plain,
( ~ group_element(e_4)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| ~ spl0_6 ),
inference(resolution,[],[f152,f27]) ).
fof(f181,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ group_element(e_1)
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f180,f14]) ).
fof(f182,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| ~ group_element(e_1)
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f181,f152]) ).
fof(f183,plain,
( product(e_1,e_4,e_1)
| ~ group_element(e_1)
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f182,f152]) ).
fof(f184,plain,
( ~ group_element(e_1)
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f183,f152]) ).
fof(f185,plain,
( $false
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f184,f11]) ).
fof(f186,plain,
~ spl0_6,
inference(avatar_contradiction_clause,[],[f185]) ).
fof(f188,plain,
( ~ group_element(e_1)
| product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| ~ group_element(e_4)
| spl0_5 ),
inference(resolution,[],[f149,f27]) ).
fof(f190,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| ~ group_element(e_4)
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f188,f11]) ).
fof(f191,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f190,f14]) ).
fof(f192,plain,
( spl0_7
| spl0_8
| spl0_9
| spl0_5 ),
inference(avatar_split_clause,[],[f191,f147,f168,f164,f160]) ).
fof(f193,plain,
! [X2,X0,X1] :
( ~ product(e_2,X0,X1)
| ~ product(X2,e_4,X1)
| ~ product(X0,X2,e_4) ),
inference(resolution,[],[f53,f31]) ).
fof(f194,plain,
! [X0] :
( ~ product(e_2,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| ~ group_element(e_4) ),
inference(resolution,[],[f53,f27]) ).
fof(f195,plain,
! [X0] :
( ~ product(e_2,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f194,f14]) ).
fof(f196,plain,
( ~ product(e_2,e_1,e_3)
| ~ spl0_7 ),
inference(resolution,[],[f162,f53]) ).
fof(f205,plain,
! [X2,X0,X1] :
( ~ product(X0,e_2,X1)
| ~ product(X2,X0,X1)
| ~ product(e_4,X2,X0) ),
inference(resolution,[],[f54,f31]) ).
fof(f206,plain,
! [X0] :
( ~ product(X0,e_2,e_4)
| ~ group_element(e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f54,f27]) ).
fof(f207,plain,
! [X0] :
( ~ product(X0,e_2,e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f206,f14]) ).
fof(f208,plain,
! [X2,X0,X1] :
( ~ product(X2,X0,e_2)
| ~ product(X0,X1,e_4)
| ~ product(X1,X2,X0) ),
inference(resolution,[],[f55,f31]) ).
fof(f222,definition,
( spl0_10
<=> product(e_1,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f226,definition,
( spl0_11
<=> product(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f230,definition,
( spl0_12
<=> product(e_1,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f238,plain,
! [X2,X0,X1] :
( ~ product(X0,X2,e_3)
| ~ product(X2,e_3,X1)
| ~ product(e_4,X0,X1) ),
inference(resolution,[],[f62,f31]) ).
fof(f247,definition,
( spl0_14
<=> product(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f251,definition,
( spl0_15
<=> product(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f257,plain,
! [X2,X0,X1] :
( ~ product(e_4,X2,X0)
| ~ product(X2,X0,X1)
| ~ product(X0,e_3,X1) ),
inference(resolution,[],[f63,f31]) ).
fof(f258,plain,
! [X0] :
( ~ product(X0,e_3,e_4)
| ~ group_element(e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f63,f27]) ).
fof(f259,plain,
! [X0] :
( ~ product(X0,e_3,e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0) ),
inference(forward_subsumption_resolution,[],[f258,f14]) ).
fof(f282,definition,
( spl0_16
<=> product(e_3,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f284,plain,
( product(e_3,e_3,e_3)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f286,definition,
( spl0_17
<=> product(e_3,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f288,plain,
( product(e_3,e_3,e_2)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f290,definition,
( spl0_18
<=> product(e_3,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f292,plain,
( product(e_3,e_3,e_1)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f294,definition,
( spl0_19
<=> product(e_1,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f296,plain,
( ~ product(e_1,e_1,e_4)
| spl0_19 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f304,definition,
( spl0_20
<=> product(e_1,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f309,definition,
( spl0_21
<=> product(e_1,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f327,plain,
( ~ product(e_1,e_1,e_2)
| ~ spl0_8 ),
inference(resolution,[],[f166,f44]) ).
fof(f339,plain,
! [X0] :
( ~ product(e_2,e_3,X0)
| ~ product(e_3,e_2,e_3) ),
inference(factoring,[],[f172]) ).
fof(f342,definition,
( spl0_22
<=> product(e_3,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f344,plain,
( ~ product(e_3,e_2,e_3)
| spl0_22 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f346,definition,
( spl0_23
<=> ! [X0] : ~ product(e_2,e_3,X0) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f347,plain,
( ! [X0] : ~ product(e_2,e_3,X0)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f348,plain,
( ~ spl0_22
| spl0_23 ),
inference(avatar_split_clause,[],[f339,f346,f342]) ).
fof(f351,plain,
! [X2,X3,X0,X1] :
( ~ product(X1,e_2,X2)
| ~ product(X0,X1,X2)
| ~ product(X3,e_3,X1)
| ~ product(X0,X3,e_3) ),
inference(resolution,[],[f176,f31]) ).
fof(f356,plain,
( ! [X0] :
( ~ product(e_1,e_1,X0)
| ~ product(e_1,e_1,X0) )
| ~ spl0_9 ),
inference(resolution,[],[f170,f134]) ).
fof(f361,plain,
( ! [X0] : ~ product(e_1,e_1,X0)
| ~ spl0_9 ),
inference(duplicate_literal_removal,[],[f356]) ).
fof(f369,plain,
! [X0] :
( ~ product(e_2,e_4,X0)
| ~ product(e_4,e_2,e_4) ),
inference(factoring,[],[f193]) ).
fof(f372,definition,
( spl0_24
<=> product(e_4,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f374,plain,
( ~ product(e_4,e_2,e_4)
| spl0_24 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f376,definition,
( spl0_25
<=> ! [X0] : ~ product(e_2,e_4,X0) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f377,plain,
( ! [X0] : ~ product(e_2,e_4,X0)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f378,plain,
( ~ spl0_24
| spl0_25 ),
inference(avatar_split_clause,[],[f369,f376,f372]) ).
fof(f385,definition,
( spl0_26
<=> product(e_4,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f387,plain,
( product(e_4,e_2,e_3)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f389,definition,
( spl0_27
<=> product(e_4,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f393,definition,
( spl0_28
<=> product(e_4,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f399,plain,
! [X0] :
( ~ product(e_2,e_2,X0)
| ~ product(e_4,e_2,e_2) ),
inference(factoring,[],[f205]) ).
fof(f402,definition,
( spl0_29
<=> product(e_2,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f403,plain,
( product(e_2,e_4,e_4)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f404,plain,
( ~ product(e_2,e_4,e_4)
| spl0_29 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f407,definition,
( spl0_30
<=> ! [X0] : ~ product(e_2,e_2,X0) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f408,plain,
( ! [X0] : ~ product(e_2,e_2,X0)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f409,plain,
( ~ spl0_27
| spl0_30 ),
inference(avatar_split_clause,[],[f399,f407,f389]) ).
fof(f422,plain,
( ~ group_element(e_4)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| ~ group_element(e_2)
| ~ spl0_25 ),
inference(resolution,[],[f377,f27]) ).
fof(f423,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| ~ group_element(e_2)
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f422,f14]) ).
fof(f424,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| ~ group_element(e_2)
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f423,f377]) ).
fof(f425,plain,
( product(e_2,e_4,e_1)
| ~ group_element(e_2)
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f424,f377]) ).
fof(f426,plain,
( ~ group_element(e_2)
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f425,f377]) ).
fof(f427,plain,
( $false
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f426,f12]) ).
fof(f428,plain,
~ spl0_25,
inference(avatar_contradiction_clause,[],[f427]) ).
fof(f433,plain,
( ~ group_element(e_2)
| product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| ~ group_element(e_4)
| spl0_24 ),
inference(resolution,[],[f374,f27]) ).
fof(f435,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| ~ group_element(e_4)
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f433,f12]) ).
fof(f436,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f435,f14]) ).
fof(f437,plain,
( spl0_26
| spl0_27
| spl0_28
| spl0_24 ),
inference(avatar_split_clause,[],[f436,f372,f393,f389,f385]) ).
fof(f442,plain,
( ~ product(e_4,e_3,e_4)
| ~ product(e_3,e_4,e_4) ),
inference(factoring,[],[f257]) ).
fof(f444,definition,
( spl0_31
<=> product(e_3,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f445,plain,
( product(e_3,e_4,e_4)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f446,plain,
( ~ product(e_3,e_4,e_4)
| spl0_31 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f448,definition,
( spl0_32
<=> product(e_4,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f449,plain,
( product(e_4,e_3,e_4)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f450,plain,
( ~ product(e_4,e_3,e_4)
| spl0_32 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f451,plain,
( ~ spl0_31
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f442,f448,f444]) ).
fof(f458,definition,
( spl0_33
<=> product(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f459,plain,
( ~ product(e_2,e_4,e_3)
| spl0_33 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f460,plain,
( product(e_2,e_4,e_3)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f462,definition,
( spl0_34
<=> product(e_2,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f464,plain,
( product(e_2,e_4,e_2)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f462]) ).
fof(f466,definition,
( spl0_35
<=> product(e_2,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f467,plain,
( ~ product(e_2,e_4,e_1)
| spl0_35 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f468,plain,
( product(e_2,e_4,e_1)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f488,definition,
( spl0_36
<=> product(e_3,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f489,plain,
( ~ product(e_3,e_4,e_3)
| spl0_36 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f490,plain,
( product(e_3,e_4,e_3)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f492,definition,
( spl0_37
<=> product(e_3,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f494,plain,
( product(e_3,e_4,e_2)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f492]) ).
fof(f496,definition,
( spl0_38
<=> product(e_3,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f498,plain,
( product(e_3,e_4,e_1)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f496]) ).
fof(f500,plain,
( ~ group_element(e_1)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ group_element(e_2) ),
inference(resolution,[],[f77,f27]) ).
fof(f501,plain,
! [X0] :
( ~ product(e_1,X0,e_2)
| ~ product(X0,e_2,e_4) ),
inference(resolution,[],[f77,f31]) ).
fof(f502,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ group_element(e_2) ),
inference(forward_subsumption_resolution,[],[f500,f11]) ).
fof(f503,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3) ),
inference(forward_subsumption_resolution,[],[f502,f12]) ).
fof(f505,definition,
( spl0_39
<=> product(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f507,plain,
( product(e_2,e_1,e_3)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f509,definition,
( spl0_40
<=> product(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f510,plain,
( ~ product(e_2,e_1,e_2)
| spl0_40 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f511,plain,
( product(e_2,e_1,e_2)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f513,definition,
( spl0_41
<=> product(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f515,plain,
( product(e_2,e_1,e_1)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f516,plain,
( spl0_39
| spl0_40
| spl0_41 ),
inference(avatar_split_clause,[],[f503,f513,f509,f505]) ).
fof(f519,plain,
( ~ product(e_2,e_4,e_4)
| ~ spl0_31 ),
inference(resolution,[],[f445,f50]) ).
fof(f530,plain,
( ~ spl0_29
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f519,f444,f402]) ).
fof(f531,plain,
! [X0] :
( ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| ~ group_element(e_1) ),
inference(resolution,[],[f81,f27]) ).
fof(f533,plain,
! [X0] :
( ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| ~ group_element(e_1) ),
inference(duplicate_literal_removal,[],[f531]) ).
fof(f534,plain,
! [X0] :
( ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f533,f11]) ).
fof(f540,plain,
! [X0] :
( product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f96,f27]) ).
fof(f542,plain,
! [X0] :
( product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(duplicate_literal_removal,[],[f540]) ).
fof(f543,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(forward_subsumption_resolution,[],[f542,f11]) ).
fof(f549,definition,
( spl0_42
<=> product(e_4,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f550,plain,
( ~ product(e_4,e_3,e_3)
| spl0_42 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f551,plain,
( product(e_4,e_3,e_3)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f553,definition,
( spl0_43
<=> product(e_4,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f554,plain,
( ~ product(e_4,e_3,e_2)
| spl0_43 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f555,plain,
( product(e_4,e_3,e_2)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f557,definition,
( spl0_44
<=> product(e_4,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f558,plain,
( ~ product(e_4,e_3,e_1)
| spl0_44 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f559,plain,
( product(e_4,e_3,e_1)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f570,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f110,f27]) ).
fof(f571,plain,
! [X0,X1] :
( ~ product(X1,X0,e_4)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0)
| product(X0,e_3,e_1)
| ~ product(e_1,X1,X0) ),
inference(resolution,[],[f110,f31]) ).
fof(f572,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(duplicate_literal_removal,[],[f570]) ).
fof(f573,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(forward_subsumption_resolution,[],[f572,f11]) ).
fof(f583,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| ~ group_element(e_1) ),
inference(resolution,[],[f119,f27]) ).
fof(f585,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| ~ group_element(e_1) ),
inference(duplicate_literal_removal,[],[f583]) ).
fof(f586,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f585,f11]) ).
fof(f589,plain,
( ~ product(e_2,e_2,e_3)
| ~ spl0_26 ),
inference(resolution,[],[f387,f53]) ).
fof(f590,plain,
( ~ product(e_1,e_2,e_3)
| ~ spl0_26 ),
inference(resolution,[],[f387,f44]) ).
fof(f601,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f136,f27]) ).
fof(f603,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(duplicate_literal_removal,[],[f601]) ).
fof(f604,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3) ),
inference(forward_subsumption_resolution,[],[f603,f11]) ).
fof(f611,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f178,f27]) ).
fof(f613,plain,
! [X0] :
( product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3) ),
inference(duplicate_literal_removal,[],[f611]) ).
fof(f614,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3) ),
inference(forward_subsumption_resolution,[],[f613,f12]) ).
fof(f622,plain,
( ~ product(e_2,e_1,e_3)
| ~ spl0_33 ),
inference(resolution,[],[f460,f45]) ).
fof(f631,plain,
( ~ spl0_39
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f622,f458,f505]) ).
fof(f633,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| ~ group_element(e_2) ),
inference(resolution,[],[f195,f27]) ).
fof(f635,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| ~ group_element(e_2) ),
inference(duplicate_literal_removal,[],[f633]) ).
fof(f636,plain,
! [X0] :
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3) ),
inference(forward_subsumption_resolution,[],[f635,f12]) ).
fof(f638,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f207,f27]) ).
fof(f640,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3) ),
inference(duplicate_literal_removal,[],[f638]) ).
fof(f641,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3) ),
inference(forward_subsumption_resolution,[],[f640,f12]) ).
fof(f645,plain,
( ~ product(e_1,e_4,e_2)
| ~ spl0_34 ),
inference(resolution,[],[f464,f38]) ).
fof(f646,plain,
( ~ product(e_2,e_3,e_2)
| ~ spl0_34 ),
inference(resolution,[],[f464,f63]) ).
fof(f656,plain,
( ~ spl0_11
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f645,f462,f226]) ).
fof(f665,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f259,f27]) ).
fof(f668,plain,
! [X0] :
( product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| ~ group_element(X0)
| ~ group_element(e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3) ),
inference(duplicate_literal_removal,[],[f665]) ).
fof(f670,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_1)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3) ),
inference(forward_subsumption_resolution,[],[f668,f13]) ).
fof(f672,definition,
( spl0_45
<=> product(e_4,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f673,plain,
( ~ product(e_4,e_4,e_3)
| spl0_45 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f674,plain,
( product(e_4,e_4,e_3)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f676,definition,
( spl0_46
<=> product(e_4,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f677,plain,
( ~ product(e_4,e_4,e_2)
| spl0_46 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f678,plain,
( product(e_4,e_4,e_2)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f680,definition,
( spl0_47
<=> product(e_4,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f681,plain,
( ~ product(e_4,e_4,e_1)
| spl0_47 ),
inference(avatar_component_clause,[],[f680]) ).
fof(f682,plain,
( product(e_4,e_4,e_1)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f680]) ).
fof(f700,plain,
( ! [X0] :
( ~ product(e_4,e_3,X0)
| ~ product(e_4,e_3,X0) )
| ~ spl0_36 ),
inference(resolution,[],[f490,f238]) ).
fof(f706,plain,
( ! [X0] : ~ product(e_4,e_3,X0)
| ~ spl0_36 ),
inference(duplicate_literal_removal,[],[f700]) ).
fof(f731,plain,
( ~ product(e_2,e_4,e_2)
| ~ spl0_37 ),
inference(resolution,[],[f494,f50]) ).
fof(f733,plain,
( ~ product(e_1,e_4,e_2)
| ~ spl0_37 ),
inference(resolution,[],[f494,f41]) ).
fof(f734,plain,
( ~ product(e_3,e_3,e_2)
| ~ spl0_37 ),
inference(resolution,[],[f494,f63]) ).
fof(f735,plain,
( ~ product(e_3,e_2,e_2)
| ~ spl0_37 ),
inference(resolution,[],[f494,f54]) ).
fof(f739,plain,
( ~ product(e_3,e_4,e_4)
| ~ spl0_37 ),
inference(resolution,[],[f494,f55]) ).
fof(f744,plain,
( ~ spl0_17
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f734,f492,f286]) ).
fof(f745,plain,
( ~ spl0_11
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f733,f492,f226]) ).
fof(f749,plain,
( ~ spl0_34
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f731,f492,f462]) ).
fof(f762,plain,
( ~ product(e_4,e_1,e_2)
| spl0_1
| ~ spl0_35 ),
inference(resolution,[],[f468,f97]) ).
fof(f768,plain,
( ~ product(e_2,e_2,e_1)
| ~ spl0_35 ),
inference(resolution,[],[f468,f54]) ).
fof(f792,plain,
( ~ product(e_4,e_2,e_3)
| ~ spl0_42 ),
inference(resolution,[],[f551,f51]) ).
fof(f841,plain,
( ~ product(e_4,e_1,e_2)
| ~ spl0_43 ),
inference(resolution,[],[f555,f42]) ).
fof(f860,definition,
( spl0_53
<=> product(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f861,plain,
( product(e_2,e_3,e_3)
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f862,plain,
( ~ product(e_2,e_3,e_3)
| spl0_53 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f872,plain,
! [X0,X1] :
( ~ product(e_2,e_2,X0)
| ~ product(X1,e_3,e_2)
| ~ product(e_2,X1,e_3) ),
inference(factoring,[],[f351]) ).
fof(f875,definition,
( spl0_55
<=> ! [X1] :
( ~ product(X1,e_3,e_2)
| ~ product(e_2,X1,e_3) ) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f876,plain,
( ! [X1] :
( ~ product(e_2,X1,e_3)
| ~ product(X1,e_3,e_2) )
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f875]) ).
fof(f877,plain,
( spl0_55
| spl0_30 ),
inference(avatar_split_clause,[],[f872,f407,f875]) ).
fof(f880,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ group_element(e_2)
| ~ spl0_30 ),
inference(resolution,[],[f408,f27]) ).
fof(f881,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ spl0_30 ),
inference(duplicate_literal_removal,[],[f880]) ).
fof(f882,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f881,f12]) ).
fof(f883,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f882,f408]) ).
fof(f884,plain,
( product(e_2,e_2,e_1)
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f883,f408]) ).
fof(f885,plain,
( $false
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f884,f408]) ).
fof(f886,plain,
~ spl0_30,
inference(avatar_contradiction_clause,[],[f885]) ).
fof(f946,plain,
( ~ product(e_1,e_4,e_3)
| ~ spl0_45 ),
inference(resolution,[],[f674,f44]) ).
fof(f948,plain,
( ~ product(e_4,e_3,e_3)
| ~ spl0_45 ),
inference(resolution,[],[f674,f63]) ).
fof(f963,plain,
( ~ spl0_10
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f946,f672,f222]) ).
fof(f994,plain,
( ~ spl0_2
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f327,f164,f90]) ).
fof(f995,plain,
~ spl0_19,
inference(avatar_split_clause,[],[f75,f294]) ).
fof(f998,plain,
( ~ spl0_8
| spl0_1
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f762,f466,f86,f164]) ).
fof(f999,plain,
( ~ spl0_8
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f841,f553,f164]) ).
fof(f1001,plain,
( ~ spl0_39
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f196,f160,f505]) ).
fof(f1021,plain,
( ~ group_element(e_4)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| ~ group_element(e_2)
| spl0_29 ),
inference(resolution,[],[f404,f27]) ).
fof(f1024,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| ~ group_element(e_2)
| spl0_29 ),
inference(forward_subsumption_resolution,[],[f1021,f14]) ).
fof(f1103,plain,
( ~ product(e_4,e_4,e_1)
| ~ spl0_38 ),
inference(resolution,[],[f498,f62]) ).
fof(f1106,plain,
( ~ product(e_1,e_4,e_1)
| ~ spl0_38 ),
inference(resolution,[],[f498,f41]) ).
fof(f1107,plain,
( ~ product(e_3,e_3,e_1)
| ~ spl0_38 ),
inference(resolution,[],[f498,f63]) ).
fof(f1108,plain,
( ~ product(e_3,e_2,e_1)
| ~ spl0_38 ),
inference(resolution,[],[f498,f54]) ).
fof(f1113,plain,
( ~ spl0_18
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f1107,f496,f290]) ).
fof(f1114,plain,
( ~ spl0_12
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f1106,f496,f230]) ).
fof(f1115,plain,
( ~ spl0_47
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f1103,f496,f680]) ).
fof(f1130,definition,
( spl0_58
<=> product(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f1134,definition,
( spl0_59
<=> product(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f1136,plain,
( product(e_2,e_3,e_1)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f1134]) ).
fof(f1138,plain,
( ~ group_element(e_3)
| product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| ~ group_element(e_4)
| spl0_32 ),
inference(resolution,[],[f450,f27]) ).
fof(f1140,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| ~ group_element(e_4)
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f1138,f13]) ).
fof(f1147,plain,
( ~ product(e_2,e_3,e_1)
| ~ spl0_44 ),
inference(resolution,[],[f559,f53]) ).
fof(f1148,plain,
( ~ product(e_1,e_3,e_1)
| ~ spl0_44 ),
inference(resolution,[],[f559,f44]) ).
fof(f1150,plain,
( ~ product(e_4,e_2,e_1)
| ~ spl0_44 ),
inference(resolution,[],[f559,f51]) ).
fof(f1157,plain,
( ~ spl0_59
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f1147,f557,f1134]) ).
fof(f1251,definition,
( spl0_63
<=> product(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f1255,definition,
( spl0_64
<=> product(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f1288,definition,
( spl0_66
<=> product(e_2,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f1292,definition,
( spl0_67
<=> product(e_2,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f1296,definition,
( spl0_68
<=> product(e_2,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f1323,plain,
( ~ product(e_4,e_1,e_2)
| ~ spl0_46 ),
inference(resolution,[],[f678,f45]) ).
fof(f1381,plain,
( ~ product(e_2,e_4,e_1)
| ~ spl0_47 ),
inference(resolution,[],[f682,f53]) ).
fof(f1382,plain,
( ~ product(e_1,e_4,e_1)
| ~ spl0_47 ),
inference(resolution,[],[f682,f44]) ).
fof(f1384,plain,
( ~ product(e_4,e_2,e_1)
| ~ spl0_47 ),
inference(resolution,[],[f682,f54]) ).
fof(f1392,plain,
( ~ spl0_12
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1382,f680,f230]) ).
fof(f1393,plain,
( ~ spl0_64
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f1108,f496,f1255]) ).
fof(f1437,plain,
( ~ product(e_1,e_1,e_3)
| ~ spl0_39 ),
inference(resolution,[],[f507,f38]) ).
fof(f1454,plain,
( ~ spl0_21
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f1437,f505,f309]) ).
fof(f1499,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3) ),
inference(resolution,[],[f534,f13]) ).
fof(f1500,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3) ),
inference(resolution,[],[f534,f14]) ).
fof(f1504,definition,
( spl0_70
<=> product(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f1506,plain,
( product(e_1,e_2,e_1)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f1504]) ).
fof(f1511,plain,
( product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_1)
| product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3) ),
inference(resolution,[],[f543,f13]) ).
fof(f1516,definition,
( spl0_71
<=> product(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f1517,plain,
( ~ product(e_3,e_1,e_2)
| spl0_71 ),
inference(avatar_component_clause,[],[f1516]) ).
fof(f1518,plain,
( product(e_3,e_1,e_2)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f1516]) ).
fof(f1520,definition,
( spl0_72
<=> product(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f1521,plain,
( ~ product(e_3,e_1,e_1)
| spl0_72 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1522,plain,
( product(e_3,e_1,e_1)
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1532,plain,
( ~ product(e_2,e_1,e_3)
| ~ spl0_70 ),
inference(resolution,[],[f1506,f76]) ).
fof(f1553,definition,
( spl0_74
<=> product(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f1603,plain,
( ! [X0] :
( ~ product(e_2,X0,e_3)
| ~ product(X0,e_3,e_3) )
| spl0_22 ),
inference(resolution,[],[f344,f31]) ).
fof(f1605,plain,
( ~ group_element(e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| ~ group_element(e_2)
| ~ spl0_23 ),
inference(resolution,[],[f347,f27]) ).
fof(f1606,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| ~ group_element(e_2)
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1605,f13]) ).
fof(f1607,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| ~ group_element(e_2)
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1606,f347]) ).
fof(f1608,plain,
( product(e_2,e_3,e_1)
| ~ group_element(e_2)
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1607,f347]) ).
fof(f1609,plain,
( ~ group_element(e_2)
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1608,f347]) ).
fof(f1610,plain,
( $false
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1609,f12]) ).
fof(f1611,plain,
~ spl0_23,
inference(avatar_contradiction_clause,[],[f1610]) ).
fof(f1614,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_1)
| product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3) ),
inference(resolution,[],[f573,f13]) ).
fof(f1622,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3) ),
inference(resolution,[],[f586,f14]) ).
fof(f1628,plain,
( ~ product(e_4,e_1,e_2)
| ~ spl0_71 ),
inference(resolution,[],[f1518,f62]) ).
fof(f1642,plain,
( product(e_3,e_2,e_2)
| product(e_3,e_2,e_1)
| product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1511,f344]) ).
fof(f1643,plain,
( spl0_4
| spl0_71
| spl0_72
| spl0_18
| spl0_16
| spl0_17 ),
inference(avatar_split_clause,[],[f1614,f286,f282,f290,f1520,f1516,f129]) ).
fof(f1644,plain,
( spl0_4
| spl0_71
| spl0_72
| spl0_64
| spl0_63
| spl0_22 ),
inference(avatar_split_clause,[],[f1642,f342,f1251,f1255,f1520,f1516,f129]) ).
fof(f1647,plain,
( ~ product(e_2,e_1,e_3)
| ~ spl0_4 ),
inference(resolution,[],[f130,f50]) ).
fof(f1668,plain,
( $false
| ~ spl0_4
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1647,f507]) ).
fof(f1669,plain,
( ~ spl0_4
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f1668]) ).
fof(f1673,plain,
( product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| product(e_3,e_4,e_1)
| product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3) ),
inference(resolution,[],[f604,f13]) ).
fof(f1695,plain,
( ~ product(e_2,e_1,e_3)
| ~ spl0_53 ),
inference(resolution,[],[f861,f42]) ).
fof(f1718,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[],[f614,f11]) ).
fof(f1732,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3) ),
inference(resolution,[],[f636,f13]) ).
fof(f1733,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3) ),
inference(resolution,[],[f636,f14]) ).
fof(f1738,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_72 ),
inference(resolution,[],[f1522,f41]) ).
fof(f1743,plain,
( ~ spl0_20
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f1738,f1520,f304]) ).
fof(f1766,plain,
( ~ spl0_68
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f768,f466,f1296]) ).
fof(f1768,plain,
( ~ spl0_31
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f739,f492,f444]) ).
fof(f1769,plain,
( ~ spl0_63
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f735,f492,f1251]) ).
fof(f1799,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[],[f641,f11]) ).
fof(f1848,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3) ),
inference(resolution,[],[f670,f11]) ).
fof(f1851,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_1)
| product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3) ),
inference(resolution,[],[f670,f14]) ).
fof(f1882,plain,
( ~ product(e_4,e_3,e_3)
| ~ spl0_16 ),
inference(resolution,[],[f284,f62]) ).
fof(f1914,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ group_element(e_1)
| spl0_19 ),
inference(resolution,[],[f296,f27]) ).
fof(f1916,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| spl0_19 ),
inference(duplicate_literal_removal,[],[f1914]) ).
fof(f1917,plain,
( ~ product(e_1,e_3,e_2)
| ~ spl0_39
| ~ spl0_55 ),
inference(resolution,[],[f876,f507]) ).
fof(f1919,plain,
( ~ spl0_14
| ~ spl0_39
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f1917,f875,f505,f247]) ).
fof(f1922,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ group_element(e_1)
| ~ spl0_9 ),
inference(resolution,[],[f361,f27]) ).
fof(f1923,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ spl0_9 ),
inference(duplicate_literal_removal,[],[f1922]) ).
fof(f1935,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1916,f11]) ).
fof(f1936,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f1923,f11]) ).
fof(f1946,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f1936,f361]) ).
fof(f1955,plain,
( product(e_1,e_1,e_1)
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f1946,f361]) ).
fof(f1964,plain,
( $false
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f1955,f361]) ).
fof(f1965,plain,
~ spl0_9,
inference(avatar_contradiction_clause,[],[f1964]) ).
fof(f1974,plain,
( ~ spl0_39
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f1532,f1504,f505]) ).
fof(f1985,plain,
( spl0_21
| spl0_2
| spl0_20
| spl0_19 ),
inference(avatar_split_clause,[],[f1935,f294,f304,f90,f309]) ).
fof(f2012,plain,
( ~ spl0_15
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f1148,f557,f251]) ).
fof(f2017,plain,
( product(e_4,e_4,e_3)
| product(e_4,e_4,e_1)
| product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| spl0_46 ),
inference(forward_subsumption_resolution,[],[f1851,f677]) ).
fof(f2040,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| spl0_45
| spl0_46 ),
inference(forward_subsumption_resolution,[],[f2017,f673]) ).
fof(f2059,plain,
( ~ spl0_39
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f1695,f860,f505]) ).
fof(f2083,plain,
( ! [X0] :
( ~ product(e_1,X0,e_2)
| ~ product(X0,e_2,e_2) )
| spl0_40 ),
inference(resolution,[],[f510,f31]) ).
fof(f2090,plain,
( ! [X0] :
( ~ product(e_1,e_1,X0)
| ~ product(e_1,e_1,X0) )
| ~ spl0_41 ),
inference(resolution,[],[f515,f94]) ).
fof(f2095,plain,
( ! [X0] : ~ product(e_1,e_1,X0)
| ~ spl0_41 ),
inference(duplicate_literal_removal,[],[f2090]) ).
fof(f2097,plain,
( spl0_3
| spl0_14
| spl0_15
| spl0_53
| spl0_58
| spl0_59 ),
inference(avatar_split_clause,[],[f1499,f1134,f1130,f860,f251,f247,f125]) ).
fof(f2098,plain,
( spl0_74
| spl0_1
| spl0_70
| spl0_15
| spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f1718,f247,f125,f251,f1504,f86,f1553]) ).
fof(f2099,plain,
( spl0_3
| spl0_14
| spl0_15
| spl0_12
| spl0_10
| spl0_11 ),
inference(avatar_split_clause,[],[f1848,f226,f222,f230,f251,f247,f125]) ).
fof(f2107,plain,
( spl0_74
| spl0_1
| spl0_70
| spl0_12
| spl0_10
| spl0_11 ),
inference(avatar_split_clause,[],[f1799,f226,f222,f230,f1504,f86,f1553]) ).
fof(f2114,plain,
( ~ product(e_2,e_2,e_4)
| ~ spl0_1 ),
inference(resolution,[],[f87,f501]) ).
fof(f2208,plain,
( ~ spl0_58
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f646,f462,f1130]) ).
fof(f2210,plain,
( ~ spl0_35
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1381,f680,f466]) ).
fof(f2213,plain,
( $false
| ~ spl0_8
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f1628,f166]) ).
fof(f2214,plain,
( ~ spl0_8
| ~ spl0_71 ),
inference(avatar_contradiction_clause,[],[f2213]) ).
fof(f2270,plain,
( ! [X0] :
( ~ product(X0,e_1,e_2)
| ~ product(e_2,X0,e_4) )
| ~ spl0_1 ),
inference(resolution,[],[f87,f208]) ).
fof(f2276,plain,
( ! [X0] :
( ~ product(e_4,X0,e_3)
| ~ product(X0,e_3,e_4) )
| spl0_31 ),
inference(resolution,[],[f446,f31]) ).
fof(f2336,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ group_element(e_2)
| ~ spl0_1 ),
inference(resolution,[],[f2114,f27]) ).
fof(f2338,plain,
( ~ group_element(e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ spl0_1 ),
inference(duplicate_literal_removal,[],[f2336]) ).
fof(f2339,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f2338,f12]) ).
fof(f2340,plain,
( spl0_66
| spl0_67
| spl0_68
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f2339,f86,f1296,f1292,f1288]) ).
fof(f2352,plain,
( ~ product(e_3,e_2,e_1)
| ~ spl0_18 ),
inference(resolution,[],[f292,f51]) ).
fof(f2359,plain,
( ~ spl0_64
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f2352,f290,f1255]) ).
fof(f2390,plain,
( ~ spl0_66
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f589,f385,f1288]) ).
fof(f2392,plain,
( ~ spl0_26
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f792,f549,f385]) ).
fof(f2393,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| spl0_45
| spl0_46
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f2040,f681]) ).
fof(f2395,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_3)
| ~ group_element(e_4)
| spl0_32
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1140,f554]) ).
fof(f2399,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1732,f554]) ).
fof(f2400,plain,
( ~ spl0_42
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f1882,f282,f549]) ).
fof(f2406,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_3)
| spl0_43
| spl0_45
| spl0_46
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f2393,f554]) ).
fof(f2407,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_3)
| spl0_32
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f2395,f14]) ).
fof(f2411,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_3)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| spl0_43
| spl0_53 ),
inference(forward_subsumption_resolution,[],[f2399,f862]) ).
fof(f2417,plain,
( spl0_42
| spl0_44
| spl0_43
| spl0_45
| spl0_46
| spl0_47 ),
inference(avatar_split_clause,[],[f2406,f680,f676,f672,f553,f557,f549]) ).
fof(f2418,plain,
( spl0_42
| spl0_44
| spl0_32
| spl0_43 ),
inference(avatar_split_clause,[],[f2407,f553,f448,f557,f549]) ).
fof(f2422,plain,
( spl0_58
| spl0_59
| spl0_42
| spl0_44
| spl0_43
| spl0_53 ),
inference(avatar_split_clause,[],[f2411,f860,f553,f557,f549,f1134,f1130]) ).
fof(f2431,plain,
( ~ spl0_28
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f1150,f557,f393]) ).
fof(f2534,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ group_element(e_1)
| ~ spl0_41 ),
inference(resolution,[],[f2095,f27]) ).
fof(f2535,plain,
( ~ group_element(e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ spl0_41 ),
inference(duplicate_literal_removal,[],[f2534]) ).
fof(f2536,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f2535,f11]) ).
fof(f2537,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f2536,f2095]) ).
fof(f2538,plain,
( product(e_1,e_1,e_1)
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f2537,f2095]) ).
fof(f2539,plain,
( $false
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f2538,f2095]) ).
fof(f2540,plain,
~ spl0_41,
inference(avatar_contradiction_clause,[],[f2539]) ).
fof(f2553,plain,
( product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| ~ group_element(e_2)
| spl0_29
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f1024,f467]) ).
fof(f2554,plain,
( product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f1500,f467]) ).
fof(f2568,plain,
( product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| spl0_29
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f2553,f12]) ).
fof(f2569,plain,
( spl0_10
| spl0_11
| spl0_12
| spl0_33
| spl0_34
| spl0_35 ),
inference(avatar_split_clause,[],[f2554,f466,f462,f458,f230,f226,f222]) ).
fof(f2580,plain,
( spl0_33
| spl0_34
| spl0_29
| spl0_35 ),
inference(avatar_split_clause,[],[f2568,f466,f402,f462,f458]) ).
fof(f2676,plain,
( ~ product(e_3,e_2,e_2)
| ~ spl0_17 ),
inference(resolution,[],[f288,f51]) ).
fof(f2687,plain,
( ~ spl0_63
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f2676,f286,f1251]) ).
fof(f2690,plain,
( ~ product(e_1,e_3,e_3)
| spl0_22
| ~ spl0_39 ),
inference(resolution,[],[f1603,f507]) ).
fof(f2696,plain,
( ~ spl0_3
| spl0_22
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f2690,f505,f342,f125]) ).
fof(f2748,plain,
( ~ group_element(e_3)
| product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| ~ group_element(e_4)
| ~ spl0_36 ),
inference(resolution,[],[f706,f27]) ).
fof(f2760,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| ~ group_element(e_4)
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f2748,f13]) ).
fof(f2764,plain,
( product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| ~ group_element(e_4)
| ~ spl0_36
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f2760,f558]) ).
fof(f2768,plain,
( product(e_4,e_3,e_3)
| ~ group_element(e_4)
| ~ spl0_36
| spl0_43
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f2764,f554]) ).
fof(f2770,plain,
( ~ group_element(e_4)
| ~ spl0_36
| spl0_43
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f2768,f706]) ).
fof(f2771,plain,
( $false
| ~ spl0_36
| spl0_43
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f2770,f14]) ).
fof(f2772,plain,
( ~ spl0_36
| spl0_43
| spl0_44 ),
inference(avatar_contradiction_clause,[],[f2771]) ).
fof(f2815,plain,
( ~ spl0_42
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f948,f672,f549]) ).
fof(f2817,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f1851,f558]) ).
fof(f2818,plain,
( spl0_10
| spl0_11
| spl0_12
| spl0_45
| spl0_46
| spl0_47 ),
inference(avatar_split_clause,[],[f1622,f680,f676,f672,f230,f226,f222]) ).
fof(f2819,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f1733,f467]) ).
fof(f2821,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_1)
| product(e_4,e_3,e_3)
| spl0_43
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f2817,f554]) ).
fof(f2822,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_2,e_4,e_2)
| spl0_33
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f2819,f459]) ).
fof(f2823,plain,
( spl0_42
| spl0_47
| spl0_45
| spl0_46
| spl0_43
| spl0_44 ),
inference(avatar_split_clause,[],[f2821,f557,f553,f676,f672,f680,f549]) ).
fof(f2824,plain,
( spl0_34
| spl0_45
| spl0_46
| spl0_47
| spl0_33
| spl0_35 ),
inference(avatar_split_clause,[],[f2822,f466,f458,f680,f676,f672,f462]) ).
fof(f2826,plain,
( ~ group_element(e_4)
| product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| ~ spl0_29 ),
inference(resolution,[],[f403,f195]) ).
fof(f2849,plain,
( product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| ~ group_element(e_4)
| product(e_4,e_3,e_1)
| ~ product(e_1,e_2,e_4)
| ~ spl0_29 ),
inference(resolution,[],[f403,f571]) ).
fof(f2858,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f2826,f14]) ).
fof(f2863,plain,
( spl0_45
| spl0_46
| spl0_47
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f2858,f402,f680,f676,f672]) ).
fof(f2978,plain,
( ~ product(e_2,e_2,e_2)
| ~ spl0_1
| spl0_40 ),
inference(resolution,[],[f2083,f87]) ).
fof(f2980,plain,
( ~ spl0_67
| ~ spl0_1
| spl0_40 ),
inference(avatar_split_clause,[],[f2978,f509,f86,f1292]) ).
fof(f2988,plain,
( ~ product(e_1,e_3,e_1)
| ~ spl0_59 ),
inference(resolution,[],[f1136,f38]) ).
fof(f2997,plain,
( ~ spl0_15
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f2988,f1134,f251]) ).
fof(f3023,plain,
( ~ product(e_2,e_4,e_4)
| ~ spl0_1
| ~ spl0_8 ),
inference(resolution,[],[f2270,f166]) ).
fof(f3024,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f3023,f403]) ).
fof(f3025,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f3024]) ).
fof(f3026,plain,
( product(e_4,e_3,e_3)
| ~ group_element(e_4)
| product(e_4,e_3,e_1)
| ~ product(e_1,e_2,e_4)
| ~ spl0_29
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f2849,f554]) ).
fof(f3027,plain,
( ~ group_element(e_4)
| product(e_4,e_3,e_1)
| ~ product(e_1,e_2,e_4)
| ~ spl0_29
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f3026,f550]) ).
fof(f3028,plain,
( product(e_4,e_3,e_1)
| ~ product(e_1,e_2,e_4)
| ~ spl0_29
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f3027,f14]) ).
fof(f3029,plain,
( ~ product(e_1,e_2,e_4)
| ~ spl0_29
| spl0_42
| spl0_43
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f3028,f558]) ).
fof(f3036,plain,
( ~ group_element(e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| ~ spl0_29
| spl0_42
| spl0_43
| spl0_44 ),
inference(resolution,[],[f3029,f27]) ).
fof(f3038,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| ~ spl0_29
| spl0_42
| spl0_43
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f3036,f12]) ).
fof(f3066,plain,
( ~ product(e_4,e_3,e_4)
| spl0_31
| ~ spl0_45 ),
inference(resolution,[],[f2276,f674]) ).
fof(f3068,plain,
( $false
| spl0_31
| ~ spl0_32
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f3066,f449]) ).
fof(f3069,plain,
( spl0_31
| ~ spl0_32
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f3068]) ).
fof(f3070,plain,
( ~ spl0_8
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f1323,f676,f164]) ).
fof(f3132,plain,
( ! [X0] :
( ~ product(e_1,e_2,X0)
| ~ product(e_1,e_2,X0) )
| ~ spl0_40 ),
inference(resolution,[],[f511,f79]) ).
fof(f3133,plain,
( ! [X0] : ~ product(e_1,e_2,X0)
| ~ spl0_40 ),
inference(duplicate_literal_removal,[],[f3132]) ).
fof(f3156,plain,
( ~ group_element(e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| ~ spl0_40 ),
inference(resolution,[],[f3133,f27]) ).
fof(f3160,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f3156,f12]) ).
fof(f3166,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| ~ group_element(e_1)
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f3160,f3133]) ).
fof(f3171,plain,
( product(e_1,e_2,e_1)
| ~ group_element(e_1)
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f3166,f3133]) ).
fof(f3174,plain,
( ~ group_element(e_1)
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f3171,f3133]) ).
fof(f3178,plain,
( $false
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f3174,f11]) ).
fof(f3179,plain,
~ spl0_40,
inference(avatar_contradiction_clause,[],[f3178]) ).
fof(f3180,plain,
( ~ spl0_74
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f590,f385,f1553]) ).
fof(f3181,plain,
( ~ spl0_28
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1384,f680,f393]) ).
fof(f3184,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_3)
| ~ group_element(e_1)
| spl0_1
| ~ spl0_29
| spl0_42
| spl0_43
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f3038,f88]) ).
fof(f3188,plain,
( product(e_3,e_4,e_2)
| product(e_3,e_4,e_1)
| product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| spl0_36 ),
inference(forward_subsumption_resolution,[],[f1673,f489]) ).
fof(f3199,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_3)
| spl0_1
| ~ spl0_29
| spl0_42
| spl0_43
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f3184,f11]) ).
fof(f3202,plain,
( product(e_3,e_4,e_2)
| product(e_3,e_4,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| spl0_36
| spl0_72 ),
inference(forward_subsumption_resolution,[],[f3188,f1521]) ).
fof(f3212,plain,
( spl0_74
| spl0_70
| spl0_1
| ~ spl0_29
| spl0_42
| spl0_43
| spl0_44 ),
inference(avatar_split_clause,[],[f3199,f557,f553,f549,f402,f86,f1504,f1553]) ).
fof(f3214,plain,
( product(e_3,e_4,e_2)
| product(e_3,e_4,e_1)
| product(e_3,e_1,e_3)
| spl0_36
| spl0_71
| spl0_72 ),
inference(forward_subsumption_resolution,[],[f3202,f1517]) ).
fof(f3221,plain,
( product(e_3,e_4,e_2)
| product(e_3,e_4,e_1)
| spl0_4
| spl0_36
| spl0_71
| spl0_72 ),
inference(forward_subsumption_resolution,[],[f3214,f131]) ).
fof(f3223,plain,
( spl0_38
| spl0_37
| spl0_4
| spl0_36
| spl0_71
| spl0_72 ),
inference(avatar_split_clause,[],[f3221,f1520,f1516,f488,f129,f492,f496]) ).
cnf(s3,plain,
( ~ spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f153]) ).
cnf(s5,plain,
~ spl0_6,
inference(sat_conversion,[],[f186]) ).
cnf(s6,plain,
( spl0_5
| spl0_7
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f192]) ).
cnf(s19,plain,
( ~ spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f348]) ).
cnf(s22,plain,
( ~ spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f378]) ).
cnf(s25,plain,
( ~ spl0_27
| spl0_30 ),
inference(sat_conversion,[],[f409]) ).
cnf(s27,plain,
~ spl0_25,
inference(sat_conversion,[],[f428]) ).
cnf(s28,plain,
( spl0_24
| spl0_26
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f437]) ).
cnf(s29,plain,
( ~ spl0_31
| ~ spl0_32 ),
inference(sat_conversion,[],[f451]) ).
cnf(s33,plain,
( spl0_39
| spl0_40
| spl0_41 ),
inference(sat_conversion,[],[f516]) ).
cnf(s36,plain,
( ~ spl0_29
| ~ spl0_31 ),
inference(sat_conversion,[],[f530]) ).
cnf(s45,plain,
( ~ spl0_33
| ~ spl0_39 ),
inference(sat_conversion,[],[f631]) ).
cnf(s49,plain,
( ~ spl0_11
| ~ spl0_34 ),
inference(sat_conversion,[],[f656]) ).
cnf(s60,plain,
( ~ spl0_17
| ~ spl0_37 ),
inference(sat_conversion,[],[f744]) ).
cnf(s61,plain,
( ~ spl0_11
| ~ spl0_37 ),
inference(sat_conversion,[],[f745]) ).
cnf(s64,plain,
( ~ spl0_34
| ~ spl0_37 ),
inference(sat_conversion,[],[f749]) ).
cnf(s75,plain,
( spl0_30
| spl0_55 ),
inference(sat_conversion,[],[f877]) ).
cnf(s76,plain,
~ spl0_30,
inference(sat_conversion,[],[f886]) ).
cnf(s85,plain,
( ~ spl0_10
| ~ spl0_45 ),
inference(sat_conversion,[],[f963]) ).
cnf(s90,plain,
( ~ spl0_2
| ~ spl0_8 ),
inference(sat_conversion,[],[f994]) ).
cnf(s91,plain,
~ spl0_19,
inference(sat_conversion,[],[f995]) ).
cnf(s94,plain,
( spl0_1
| ~ spl0_8
| ~ spl0_35 ),
inference(sat_conversion,[],[f998]) ).
cnf(s95,plain,
( ~ spl0_8
| ~ spl0_43 ),
inference(sat_conversion,[],[f999]) ).
cnf(s98,plain,
( ~ spl0_7
| ~ spl0_39 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s124,plain,
( ~ spl0_18
| ~ spl0_38 ),
inference(sat_conversion,[],[f1113]) ).
cnf(s125,plain,
( ~ spl0_12
| ~ spl0_38 ),
inference(sat_conversion,[],[f1114]) ).
cnf(s126,plain,
( ~ spl0_38
| ~ spl0_47 ),
inference(sat_conversion,[],[f1115]) ).
cnf(s130,plain,
( ~ spl0_44
| ~ spl0_59 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s172,plain,
( ~ spl0_12
| ~ spl0_47 ),
inference(sat_conversion,[],[f1392]) ).
cnf(s176,plain,
( ~ spl0_38
| ~ spl0_64 ),
inference(sat_conversion,[],[f1393]) ).
cnf(s183,plain,
( ~ spl0_21
| ~ spl0_39 ),
inference(sat_conversion,[],[f1454]) ).
cnf(s217,plain,
~ spl0_23,
inference(sat_conversion,[],[f1611]) ).
cnf(s223,plain,
( spl0_4
| spl0_16
| spl0_17
| spl0_18
| spl0_71
| spl0_72 ),
inference(sat_conversion,[],[f1643]) ).
cnf(s224,plain,
( spl0_4
| spl0_22
| spl0_63
| spl0_64
| spl0_71
| spl0_72 ),
inference(sat_conversion,[],[f1644]) ).
cnf(s228,plain,
( ~ spl0_4
| ~ spl0_39 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s240,plain,
( ~ spl0_20
| ~ spl0_72 ),
inference(sat_conversion,[],[f1743]) ).
cnf(s248,plain,
( ~ spl0_35
| ~ spl0_68 ),
inference(sat_conversion,[],[f1766]) ).
cnf(s253,plain,
( ~ spl0_31
| ~ spl0_37 ),
inference(sat_conversion,[],[f1768]) ).
cnf(s256,plain,
( ~ spl0_37
| ~ spl0_63 ),
inference(sat_conversion,[],[f1769]) ).
cnf(s283,plain,
( ~ spl0_14
| ~ spl0_39
| ~ spl0_55 ),
inference(sat_conversion,[],[f1919]) ).
cnf(s290,plain,
~ spl0_9,
inference(sat_conversion,[],[f1965]) ).
cnf(s301,plain,
( ~ spl0_39
| ~ spl0_70 ),
inference(sat_conversion,[],[f1974]) ).
cnf(s307,plain,
( spl0_2
| spl0_19
| spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f1985]) ).
cnf(s333,plain,
( ~ spl0_15
| ~ spl0_44 ),
inference(sat_conversion,[],[f2012]) ).
cnf(s358,plain,
( ~ spl0_39
| ~ spl0_53 ),
inference(sat_conversion,[],[f2059]) ).
cnf(s386,plain,
( spl0_3
| spl0_14
| spl0_15
| spl0_53
| spl0_58
| spl0_59 ),
inference(sat_conversion,[],[f2097]) ).
cnf(s387,plain,
( spl0_1
| spl0_3
| spl0_14
| spl0_15
| spl0_70
| spl0_74 ),
inference(sat_conversion,[],[f2098]) ).
cnf(s388,plain,
( spl0_3
| spl0_10
| spl0_11
| spl0_12
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f2099]) ).
cnf(s393,plain,
( spl0_1
| spl0_10
| spl0_11
| spl0_12
| spl0_70
| spl0_74 ),
inference(sat_conversion,[],[f2107]) ).
cnf(s418,plain,
( ~ spl0_34
| ~ spl0_58 ),
inference(sat_conversion,[],[f2208]) ).
cnf(s425,plain,
( ~ spl0_35
| ~ spl0_47 ),
inference(sat_conversion,[],[f2210]) ).
cnf(s428,plain,
( ~ spl0_8
| ~ spl0_71 ),
inference(sat_conversion,[],[f2214]) ).
cnf(s472,plain,
( ~ spl0_1
| spl0_66
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f2340]) ).
cnf(s475,plain,
( ~ spl0_18
| ~ spl0_64 ),
inference(sat_conversion,[],[f2359]) ).
cnf(s482,plain,
( ~ spl0_26
| ~ spl0_66 ),
inference(sat_conversion,[],[f2390]) ).
cnf(s484,plain,
( ~ spl0_26
| ~ spl0_42 ),
inference(sat_conversion,[],[f2392]) ).
cnf(s487,plain,
( ~ spl0_16
| ~ spl0_42 ),
inference(sat_conversion,[],[f2400]) ).
cnf(s490,plain,
( spl0_42
| spl0_43
| spl0_44
| spl0_45
| spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f2417]) ).
cnf(s491,plain,
( spl0_32
| spl0_42
| spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f2418]) ).
cnf(s494,plain,
( spl0_42
| spl0_43
| spl0_44
| spl0_53
| spl0_58
| spl0_59 ),
inference(sat_conversion,[],[f2422]) ).
cnf(s512,plain,
( ~ spl0_28
| ~ spl0_44 ),
inference(sat_conversion,[],[f2431]) ).
cnf(s535,plain,
~ spl0_41,
inference(sat_conversion,[],[f2540]) ).
cnf(s565,plain,
( spl0_10
| spl0_11
| spl0_12
| spl0_33
| spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f2569]) ).
cnf(s574,plain,
( spl0_29
| spl0_33
| spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f2580]) ).
cnf(s591,plain,
( ~ spl0_17
| ~ spl0_63 ),
inference(sat_conversion,[],[f2687]) ).
cnf(s600,plain,
( ~ spl0_3
| spl0_22
| ~ spl0_39 ),
inference(sat_conversion,[],[f2696]) ).
cnf(s617,plain,
( ~ spl0_36
| spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f2772]) ).
cnf(s649,plain,
( ~ spl0_42
| ~ spl0_45 ),
inference(sat_conversion,[],[f2815]) ).
cnf(s652,plain,
( spl0_10
| spl0_11
| spl0_12
| spl0_45
| spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f2818]) ).
cnf(s654,plain,
( spl0_42
| spl0_43
| spl0_44
| spl0_45
| spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f2823]) ).
cnf(s655,plain,
( spl0_33
| spl0_34
| spl0_35
| spl0_45
| spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f2824]) ).
cnf(s659,plain,
( ~ spl0_29
| spl0_45
| spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f2863]) ).
cnf(s679,plain,
( ~ spl0_1
| spl0_40
| ~ spl0_67 ),
inference(sat_conversion,[],[f2980]) ).
cnf(s682,plain,
( ~ spl0_15
| ~ spl0_59 ),
inference(sat_conversion,[],[f2997]) ).
cnf(s688,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_29 ),
inference(sat_conversion,[],[f3025]) ).
cnf(s694,plain,
( spl0_31
| ~ spl0_32
| ~ spl0_45 ),
inference(sat_conversion,[],[f3069]) ).
cnf(s699,plain,
( ~ spl0_8
| ~ spl0_46 ),
inference(sat_conversion,[],[f3070]) ).
cnf(s725,plain,
~ spl0_40,
inference(sat_conversion,[],[f3179]) ).
cnf(s734,plain,
( ~ spl0_26
| ~ spl0_74 ),
inference(sat_conversion,[],[f3180]) ).
cnf(s767,plain,
( ~ spl0_28
| ~ spl0_47 ),
inference(sat_conversion,[],[f3181]) ).
cnf(s784,plain,
( spl0_1
| ~ spl0_29
| spl0_42
| spl0_43
| spl0_44
| spl0_70
| spl0_74 ),
inference(sat_conversion,[],[f3212]) ).
cnf(s791,plain,
( spl0_4
| spl0_36
| spl0_37
| spl0_38
| spl0_71
| spl0_72 ),
inference(sat_conversion,[],[f3223]) ).
cnf(s795,plain,
( ~ spl0_1
| ~ spl0_67 ),
inference(rat,[],[s679,s725]) ).
cnf(s815,plain,
spl0_55,
inference(rat,[],[s75,s76]) ).
cnf(s816,plain,
spl0_39,
inference(rat,[],[s33,s535,s725]) ).
cnf(s817,plain,
~ spl0_53,
inference(rat,[],[s358,s816]) ).
cnf(s818,plain,
~ spl0_70,
inference(rat,[],[s301,s816]) ).
cnf(s819,plain,
~ spl0_14,
inference(rat,[],[s283,s815,s816]) ).
cnf(s820,plain,
~ spl0_4,
inference(rat,[],[s228,s816]) ).
cnf(s821,plain,
~ spl0_21,
inference(rat,[],[s183,s816]) ).
cnf(s822,plain,
~ spl0_7,
inference(rat,[],[s98,s816]) ).
cnf(s823,plain,
~ spl0_33,
inference(rat,[],[s45,s816]) ).
cnf(s825,plain,
~ spl0_27,
inference(rat,[],[s25,s76]) ).
cnf(s827,plain,
~ spl0_24,
inference(rat,[],[s22,s27]) ).
cnf(s829,plain,
~ spl0_22,
inference(rat,[],[s19,s217]) ).
cnf(s830,plain,
~ spl0_3,
inference(rat,[],[s600,s816,s829]) ).
cnf(s834,plain,
( spl0_5
| spl0_8 ),
inference(rat,[],[s6,s290,s822]) ).
cnf(s836,plain,
~ spl0_5,
inference(rat,[],[s3,s5]) ).
cnf(s837,plain,
spl0_8,
inference(rat,[],[s834,s836]) ).
cnf(s838,plain,
~ spl0_46,
inference(rat,[],[s699,s837]) ).
cnf(s839,plain,
~ spl0_71,
inference(rat,[],[s428,s837]) ).
cnf(s840,plain,
~ spl0_43,
inference(rat,[],[s95,s837]) ).
cnf(s841,plain,
~ spl0_2,
inference(rat,[],[s90,s837]) ).
cnf(s842,plain,
spl0_20,
inference(rat,[],[s307,s821,s91,s841]) ).
cnf(s843,plain,
~ spl0_72,
inference(rat,[],[s240,s842]) ).
cnf(s844,plain,
( spl0_12
| spl0_11
| spl0_10
| spl0_1 ),
inference(rat,[],[s652,s649,s767,s494,s28,s333,s682,s418,s734,s388,s565,s393,s94,s838,s840,s817,s825,s827,s830,s819,s823,s818,s837]) ).
cnf(s845,plain,
( spl0_44
| ~ spl0_12
| spl0_35 ),
inference(rat,[],[s491,s694,s649,s655,s64,s253,s791,s617,s172,s125,s840,s823,s838,s820,s839,s843]) ).
cnf(s846,plain,
( ~ spl0_44
| spl0_1 ),
inference(rat,[],[s734,s387,s28,s333,s512,s819,s830,s818,s825,s827]) ).
cnf(s847,plain,
( ~ spl0_11
| spl0_1 ),
inference(rat,[],[s491,s694,s649,s36,s659,s126,s574,s791,s49,s61,s94,s617,s846,s840,s838,s823,s820,s839,s843,s837]) ).
cnf(s848,plain,
( spl0_34
| spl0_1 ),
inference(rat,[],[s784,s484,s734,s28,s767,s655,s574,s85,s844,s847,s845,s846,s94,s840,s818,s825,s827,s823,s838,s837]) ).
cnf(s849,plain,
spl0_1,
inference(rat,[],[s223,s487,s591,s654,s224,s124,s126,s176,s791,s64,s848,s85,s844,s847,s845,s617,s846,s94,s820,s839,s843,s840,s838,s829,s837]) ).
cnf(s850,plain,
~ spl0_29,
inference(rat,[],[s688,s837,s849]) ).
cnf(s851,plain,
~ spl0_67,
inference(rat,[],[s795,s849]) ).
cnf(s854,plain,
( ~ spl0_32
| ~ spl0_45 ),
inference(rat,[],[s29,s694]) ).
cnf(s855,plain,
( spl0_42
| spl0_47
| spl0_44 ),
inference(rat,[],[s854,s491,s490,s838,s840]) ).
cnf(s856,plain,
( spl0_44
| spl0_37 ),
inference(rat,[],[s855,s487,s223,s591,s224,s124,s126,s176,s791,s617,s820,s839,s843,s829,s840]) ).
cnf(s857,plain,
~ spl0_34,
inference(rat,[],[s386,s130,s333,s856,s64,s418,s819,s817,s830]) ).
cnf(s858,plain,
spl0_35,
inference(rat,[],[s574,s850,s823,s857]) ).
cnf(s859,plain,
~ spl0_47,
inference(rat,[],[s425,s858]) ).
cnf(s861,plain,
~ spl0_68,
inference(rat,[],[s248,s858]) ).
cnf(s863,plain,
spl0_66,
inference(rat,[],[s472,s849,s851,s861]) ).
cnf(s864,plain,
~ spl0_26,
inference(rat,[],[s482,s863]) ).
cnf(s865,plain,
spl0_28,
inference(rat,[],[s28,s827,s825,s864]) ).
cnf(s866,plain,
~ spl0_44,
inference(rat,[],[s512,s865]) ).
cnf(s868,plain,
spl0_37,
inference(rat,[],[s856,s866]) ).
cnf(s869,plain,
spl0_42,
inference(rat,[],[s855,s859,s866]) ).
cnf(s870,plain,
~ spl0_63,
inference(rat,[],[s256,s868]) ).
cnf(s873,plain,
~ spl0_17,
inference(rat,[],[s60,s868]) ).
cnf(s876,plain,
~ spl0_16,
inference(rat,[],[s487,s869]) ).
cnf(s879,plain,
spl0_64,
inference(rat,[],[s224,s843,s839,s829,s820,s870]) ).
cnf(s883,plain,
spl0_18,
inference(rat,[],[s223,s843,s839,s873,s820,s876]) ).
cnf(s885,plain,
$false,
inference(rat,[],[s475,s879,s883]) ).
fof(f3225,plain,
$false,
inference(avatar_sat_refutation,[],[s885]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP129-2.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 09:27:46 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 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.08/1.36 % (543645)Input is clausal, will run a generic CNF schedule.
% 3.08/1.36 % (543654)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4264167873:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.08/1.36 % (543654)Instruction limit reached!
% 3.08/1.36 % (543654)------------------------------
% 3.08/1.36 % (543654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.36 % (543654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.36 % (543654)CaDiCaL version: 2.1.3
% 3.08/1.36 % (543654)Termination reason: Instruction limit
% 3.08/1.36 % (543654)Termination phase: Saturation
% 3.08/1.36 % (543654)Time elapsed: 0.034 s
% 3.08/1.36 % (543654)Peak memory usage: 88 MB
% 3.08/1.36 % (543654)Instructions burned: 114 (million)
% 3.08/1.36 % (543651)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1235808775:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.08/1.36 % (543650)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=2679488120:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.08/1.36 % (543652)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3586103443:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.08/1.36 % (543653)lrs+10_1_sil=8000:sp=occurrence:random_seed=3951596957:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.08/1.36 % (543656)dis-21_1_sil=8000:lcm=predicate:random_seed=1946331610: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.08/1.36 % (543655)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3839278354:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.08/1.36 % (543653)Instruction limit reached!
% 3.08/1.36 % (543653)------------------------------
% 3.08/1.36 % (543653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.36 % (543653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.36 % (543653)CaDiCaL version: 2.1.3
% 3.08/1.36 % (543653)Termination reason: Instruction limit
% 3.08/1.36 % (543653)Termination phase: Saturation
% 3.08/1.36 % (543653)Time elapsed: 0.058 s
% 3.08/1.36 % (543653)Peak memory usage: 88 MB
% 3.08/1.36 % (543653)Instructions burned: 108 (million)
% 3.08/1.36 % (543656)Instruction limit reached!
% 3.08/1.36 % (543656)------------------------------
% 3.08/1.36 % (543656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.36 % (543656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.36 % (543656)CaDiCaL version: 2.1.3
% 3.08/1.36 % (543656)Termination reason: Instruction limit
% 3.08/1.36 % (543656)Termination phase: Saturation
% 3.08/1.36 % (543656)Time elapsed: 0.071 s
% 3.08/1.36 % (543656)Peak memory usage: 88 MB
% 3.08/1.36 % (543656)Instructions burned: 117 (million)
% 3.08/1.36 % (543655)First to succeed.
% 3.08/1.36 % (543655)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-543645"
% 3.08/1.36 % (543658)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=1026834189:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.08/1.36 % (543658)Instruction limit reached!
% 3.08/1.36 % (543658)------------------------------
% 3.08/1.36 % (543658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.36 % (543658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.36 % (543658)CaDiCaL version: 2.1.3
% 3.08/1.36 % (543658)Termination reason: Instruction limit
% 3.08/1.36 % (543658)Termination phase: Saturation
% 3.08/1.36 % (543658)Time elapsed: 0.049 s
% 3.08/1.36 % (543658)Peak memory usage: 89 MB
% 3.08/1.36 % (543658)Instructions burned: 146 (million)
% 3.08/1.36 % (543665)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1164707248: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.08/1.36 % (543665)Refutation not found, incomplete strategy
% 3.08/1.36 % (543665)------------------------------
% 3.08/1.36 % (543665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.36 % (543665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.36 % (543665)CaDiCaL version: 2.1.3
% 3.08/1.36 % (543665)Termination reason: Refutation not found, incomplete strategy
% 3.08/1.36 % (543665)Time elapsed: 0.002 s
% 3.08/1.36 % (543665)Peak memory usage: 87 MB
% 3.08/1.36 % (543665)Instructions burned: 1 (million)
% 3.08/1.36 % (543666)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1595351088:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 3.08/1.36 % (543668)lrs+10_64_to=lpo:sil=8000:random_seed=464596783:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 3.08/1.36 % (543668)Also succeeded, but the first one will report.
% 3.08/1.36 % (543655)Refutation found. Thanks to Tanya!
% 3.08/1.36 % SZS status Unsatisfiable for theBenchmark
% 3.08/1.36 % SZS output start Proof for theBenchmark
% See solution above
% 4.23/1.56 % (543655)------------------------------
% 4.23/1.56 % (543655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.23/1.56 % (543655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.23/1.56 % (543655)CaDiCaL version: 2.1.3
% 4.23/1.56 % (543655)Termination reason: Refutation
% 4.23/1.56 % (543655)Time elapsed: 0.088 s
% 4.23/1.56 % (543655)Peak memory usage: 90 MB
% 4.23/1.56 % (543655)Instructions burned: 135 (million)
% 4.23/1.56 % (543655)------------------------------
% 4.23/1.56 % (543655)------------------------------
% 4.23/1.56 % (543645)Success in time 0.514 s
% 4.23/1.56 % Vampire exiting
%------------------------------------------------------------------------------