%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP128-2.006 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:57 AM UTC 2026
% Result : Unsatisfiable 8.67s 2.04s
% Output : Refutation 8.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 104
% Syntax : Number of formulae : 513 ( 82 unt; 51 def)
% Number of atoms : 1685 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 1839 ( 667 ~;1121 |; 0 &)
% ( 51 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 57 ( 56 usr; 52 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 73 ( 0 sgn 73 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_then_e_2) ).
fof(f2,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_then_e_3) ).
fof(f3,axiom,
next(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_then_e_4) ).
fof(f4,axiom,
next(e_4,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_then_e_5) ).
fof(f11,axiom,
greater(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_greater_e_2) ).
fof(f12,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_2) ).
fof(f13,axiom,
greater(e_5,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_greater_e_2) ).
fof(f14,axiom,
greater(e_6,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_6_greater_e_2) ).
fof(f15,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_3) ).
fof(f16,axiom,
greater(e_5,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_greater_e_3) ).
fof(f17,axiom,
greater(e_6,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_6_greater_e_3) ).
fof(f18,axiom,
greater(e_5,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_greater_e_4) ).
fof(f19,axiom,
greater(e_6,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_6_greater_e_4) ).
fof(f20,axiom,
greater(e_6,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_6_greater_e_5) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ product(X0,e_1,X1)
| ~ next(X0,X2)
| ~ greater(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_redundancy) ).
fof(f22,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
fof(f23,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
fof(f24,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
fof(f25,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
fof(f26,axiom,
group_element(e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_5) ).
fof(f27,axiom,
group_element(e_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_6) ).
fof(f28,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f29,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f30,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f31,axiom,
~ equalish(e_1,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_5) ).
fof(f32,axiom,
~ equalish(e_1,e_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_6) ).
fof(f33,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
fof(f34,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f35,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f36,axiom,
~ equalish(e_2,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_5) ).
fof(f37,axiom,
~ equalish(e_2,e_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_6) ).
fof(f38,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
fof(f39,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
fof(f41,axiom,
~ equalish(e_3,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_5) ).
fof(f42,axiom,
~ equalish(e_3,e_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_6) ).
fof(f43,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
fof(f44,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
fof(f45,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
fof(f46,axiom,
~ equalish(e_4,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_5) ).
fof(f47,axiom,
~ equalish(e_4,e_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_6) ).
fof(f50,axiom,
~ equalish(e_5,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_3) ).
fof(f51,axiom,
~ equalish(e_5,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_4) ).
fof(f52,axiom,
~ equalish(e_5,e_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_6) ).
fof(f53,axiom,
~ equalish(e_6,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_6_is_not_e_1) ).
fof(f54,axiom,
~ equalish(e_6,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_6_is_not_e_2) ).
fof(f55,axiom,
~ equalish(e_6,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_6_is_not_e_3) ).
fof(f56,axiom,
~ equalish(e_6,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_6_is_not_e_4) ).
fof(f57,axiom,
~ equalish(e_6,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_6_is_not_e_5) ).
fof(f58,axiom,
! [X0,X1] :
( product(X0,X1,e_6)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| product(X0,X1,e_5)
| ~ group_element(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
fof(f59,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
fof(f60,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f61,axiom,
! [X2,X3,X0,X1] :
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
fof(f62,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ product(X2,X1,X3)
| ~ product(X0,X1,X2)
| product(X0,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
fof(f63,plain,
~ product(e_1,e_1,e_3),
inference(unit_resulting_resolution,[],[f21,f11,f1]) ).
fof(f64,plain,
~ product(e_1,e_1,e_4),
inference(unit_resulting_resolution,[],[f21,f12,f1]) ).
fof(f65,plain,
~ product(e_1,e_1,e_5),
inference(unit_resulting_resolution,[],[f21,f13,f1]) ).
fof(f66,plain,
~ product(e_1,e_1,e_6),
inference(unit_resulting_resolution,[],[f21,f14,f1]) ).
fof(f67,plain,
~ product(e_2,e_1,e_4),
inference(unit_resulting_resolution,[],[f21,f15,f2]) ).
fof(f68,plain,
~ product(e_2,e_1,e_5),
inference(unit_resulting_resolution,[],[f21,f16,f2]) ).
fof(f69,plain,
~ product(e_2,e_1,e_6),
inference(unit_resulting_resolution,[],[f21,f17,f2]) ).
fof(f70,plain,
~ product(e_3,e_1,e_5),
inference(unit_resulting_resolution,[],[f21,f18,f3]) ).
fof(f71,plain,
~ product(e_3,e_1,e_6),
inference(unit_resulting_resolution,[],[f21,f19,f3]) ).
fof(f72,plain,
~ product(e_4,e_1,e_6),
inference(unit_resulting_resolution,[],[f21,f20,f4]) ).
fof(f73,plain,
! [X2,X0,X1] :
( ~ product(X2,X0,e_6)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| product(X1,X0,e_5)
| ~ group_element(X1)
| ~ group_element(X0)
| equalish(X2,X1) ),
inference(resolution,[],[f58,f61]) ).
fof(f74,plain,
! [X2,X0,X1] :
( ~ product(X1,X2,e_6)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| product(X1,X0,e_5)
| ~ group_element(X1)
| ~ group_element(X0)
| equalish(X2,X0) ),
inference(resolution,[],[f58,f60]) ).
fof(f76,plain,
! [X2,X0,X1] :
( ~ product(X2,X0,X1)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| product(X1,X0,e_5)
| ~ group_element(X1)
| ~ group_element(X0)
| product(X2,X1,e_6) ),
inference(resolution,[],[f58,f62]) ).
fof(f77,plain,
! [X0,X1] :
( ~ group_element(e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_5)
| ~ group_element(X0)
| ~ next(X0,X1)
| ~ greater(e_6,X1) ),
inference(resolution,[],[f58,f21]) ).
fof(f78,plain,
! [X0,X1] :
( product(X0,e_1,e_5)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_1)
| ~ group_element(X0)
| ~ next(X0,X1)
| ~ greater(e_6,X1) ),
inference(forward_subsumption_resolution,[],[f77,f22]) ).
fof(f79,plain,
! [X0,X1] :
( product(e_6,X0,e_1)
| product(e_6,X0,e_2)
| product(e_6,X0,e_3)
| product(e_6,X0,e_4)
| product(e_6,X0,e_5)
| ~ group_element(e_6)
| ~ group_element(X0)
| product(X1,e_6,e_6)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| product(X1,X0,e_5)
| ~ group_element(X1) ),
inference(resolution,[],[f76,f58]) ).
fof(f80,plain,
! [X0,X1] :
( product(e_6,X0,e_1)
| product(e_6,X0,e_2)
| product(e_6,X0,e_3)
| product(e_6,X0,e_4)
| product(e_6,X0,e_5)
| ~ group_element(e_6)
| ~ group_element(X0)
| product(X1,e_6,e_6)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| product(X1,X0,e_5)
| ~ group_element(X1) ),
inference(duplicate_literal_removal,[],[f79]) ).
fof(f81,plain,
! [X0,X1] :
( product(e_6,X0,e_5)
| product(X1,e_6,e_6)
| product(X1,X0,e_5)
| product(e_6,X0,e_4)
| product(e_6,X0,e_3)
| ~ group_element(X0)
| product(e_6,X0,e_2)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| product(e_6,X0,e_1)
| ~ group_element(X1) ),
inference(forward_subsumption_resolution,[],[f80,f27]) ).
fof(f82,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)
| product(e_1,e_1,e_4)
| product(e_1,e_1,e_5)
| ~ group_element(e_1) ),
inference(resolution,[],[f66,f58]) ).
fof(f83,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)
| product(e_1,e_1,e_4)
| product(e_1,e_1,e_5) ),
inference(duplicate_literal_removal,[],[f82]) ).
fof(f84,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_4)
| product(e_1,e_1,e_5) ),
inference(forward_subsumption_resolution,[],[f83,f22]) ).
fof(f85,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_4)
| product(e_1,e_1,e_5) ),
inference(forward_subsumption_resolution,[],[f84,f63]) ).
fof(f86,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_5) ),
inference(forward_subsumption_resolution,[],[f85,f64]) ).
fof(f87,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(forward_subsumption_resolution,[],[f86,f65]) ).
fof(f89,definition,
( spl0_1
<=> product(e_1,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f91,plain,
( product(e_1,e_1,e_2)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f93,definition,
( spl0_2
<=> product(e_1,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f95,plain,
( product(e_1,e_1,e_1)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f93]) ).
fof(f96,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f87,f93,f89]) ).
fof(f97,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)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5)
| ~ group_element(e_2) ),
inference(resolution,[],[f69,f58]) ).
fof(f98,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5)
| ~ group_element(e_2) ),
inference(forward_subsumption_resolution,[],[f97,f22]) ).
fof(f99,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| ~ group_element(e_2) ),
inference(forward_subsumption_resolution,[],[f98,f67]) ).
fof(f100,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,[],[f99,f68]) ).
fof(f101,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,[],[f100,f23]) ).
fof(f103,definition,
( spl0_3
<=> product(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f104,plain,
( ~ product(e_2,e_1,e_3)
| spl0_3 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f105,plain,
( product(e_2,e_1,e_3)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f107,definition,
( spl0_4
<=> product(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f108,plain,
( ~ product(e_2,e_1,e_2)
| spl0_4 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f109,plain,
( product(e_2,e_1,e_2)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f111,definition,
( spl0_5
<=> product(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f114,plain,
( spl0_3
| spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f101,f111,f107,f103]) ).
fof(f115,plain,
( ~ group_element(e_1)
| product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5)
| ~ group_element(e_3) ),
inference(resolution,[],[f71,f58]) ).
fof(f116,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5)
| ~ group_element(e_3) ),
inference(forward_subsumption_resolution,[],[f115,f22]) ).
fof(f117,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| ~ group_element(e_3) ),
inference(forward_subsumption_resolution,[],[f116,f70]) ).
fof(f118,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4) ),
inference(forward_subsumption_resolution,[],[f117,f24]) ).
fof(f120,definition,
( spl0_6
<=> product(e_3,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f121,plain,
( ~ product(e_3,e_1,e_4)
| spl0_6 ),
inference(avatar_component_clause,[],[f120]) ).
fof(f122,plain,
( product(e_3,e_1,e_4)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f120]) ).
fof(f124,definition,
( spl0_7
<=> product(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f125,plain,
( ~ product(e_3,e_1,e_3)
| spl0_7 ),
inference(avatar_component_clause,[],[f124]) ).
fof(f128,definition,
( spl0_8
<=> product(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f129,plain,
( ~ product(e_3,e_1,e_2)
| spl0_8 ),
inference(avatar_component_clause,[],[f128]) ).
fof(f130,plain,
( product(e_3,e_1,e_2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f128]) ).
fof(f132,definition,
( spl0_9
<=> product(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f135,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9 ),
inference(avatar_split_clause,[],[f118,f132,f128,f124,f120]) ).
fof(f140,definition,
( spl0_10
<=> product(e_4,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f141,plain,
( ~ product(e_4,e_1,e_5)
| spl0_10 ),
inference(avatar_component_clause,[],[f140]) ).
fof(f142,plain,
( product(e_4,e_1,e_5)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f140]) ).
fof(f144,definition,
( spl0_11
<=> product(e_4,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f145,plain,
( ~ product(e_4,e_1,e_4)
| spl0_11 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f146,plain,
( product(e_4,e_1,e_4)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f148,definition,
( spl0_12
<=> product(e_4,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f149,plain,
( ~ product(e_4,e_1,e_3)
| spl0_12 ),
inference(avatar_component_clause,[],[f148]) ).
fof(f152,definition,
( spl0_13
<=> product(e_4,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f153,plain,
( ~ product(e_4,e_1,e_2)
| spl0_13 ),
inference(avatar_component_clause,[],[f152]) ).
fof(f154,plain,
( product(e_4,e_1,e_2)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f152]) ).
fof(f156,definition,
( spl0_14
<=> product(e_4,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f157,plain,
( ~ product(e_4,e_1,e_1)
| spl0_14 ),
inference(avatar_component_clause,[],[f156]) ).
fof(f185,plain,
( ~ product(e_2,e_1,e_1)
| ~ spl0_2 ),
inference(unit_resulting_resolution,[],[f61,f28,f95]) ).
fof(f186,plain,
( ~ product(e_3,e_1,e_1)
| ~ spl0_2 ),
inference(unit_resulting_resolution,[],[f61,f29,f95]) ).
fof(f187,plain,
( ~ product(e_4,e_1,e_1)
| ~ spl0_2 ),
inference(unit_resulting_resolution,[],[f61,f30,f95]) ).
fof(f189,plain,
( ~ product(e_6,e_1,e_1)
| ~ spl0_2 ),
inference(unit_resulting_resolution,[],[f61,f32,f95]) ).
fof(f211,plain,
( ~ spl0_5
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f185,f93,f111]) ).
fof(f212,plain,
( ~ spl0_9
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f186,f93,f132]) ).
fof(f213,plain,
( ~ spl0_14
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f187,f93,f156]) ).
fof(f219,plain,
! [X2,X0,X1] :
( ~ product(X2,e_1,X0)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_1)
| ~ group_element(X0)
| ~ next(X0,X1)
| ~ greater(e_6,X1)
| product(X0,e_1,e_2)
| product(X2,X0,e_5) ),
inference(resolution,[],[f78,f62]) ).
fof(f221,plain,
! [X0] :
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_1)
| ~ group_element(e_2)
| ~ next(e_2,X0)
| ~ greater(e_6,X0) ),
inference(resolution,[],[f78,f68]) ).
fof(f222,plain,
! [X0] :
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_1)
| ~ group_element(e_3)
| ~ next(e_3,X0)
| ~ greater(e_6,X0) ),
inference(resolution,[],[f78,f70]) ).
fof(f227,definition,
( spl0_15
<=> product(e_5,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f228,plain,
( ~ product(e_5,e_1,e_5)
| spl0_15 ),
inference(avatar_component_clause,[],[f227]) ).
fof(f229,plain,
( product(e_5,e_1,e_5)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f227]) ).
fof(f231,definition,
( spl0_16
<=> product(e_5,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f232,plain,
( ~ product(e_5,e_1,e_4)
| spl0_16 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f233,plain,
( product(e_5,e_1,e_4)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f235,definition,
( spl0_17
<=> product(e_5,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f236,plain,
( ~ product(e_5,e_1,e_3)
| spl0_17 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f237,plain,
( product(e_5,e_1,e_3)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f239,definition,
( spl0_18
<=> product(e_5,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f240,plain,
( ~ product(e_5,e_1,e_2)
| spl0_18 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f241,plain,
( product(e_5,e_1,e_2)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f249,definition,
( spl0_20
<=> product(e_5,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f250,plain,
( ~ product(e_5,e_1,e_1)
| spl0_20 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f251,plain,
( product(e_5,e_1,e_1)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f273,plain,
( ~ product(e_5,e_5,e_5)
| ~ spl0_15 ),
inference(unit_resulting_resolution,[],[f60,f31,f229]) ).
fof(f295,plain,
( product(e_5,e_5,e_5)
| ~ spl0_15 ),
inference(unit_resulting_resolution,[],[f62,f229,f229]) ).
fof(f312,plain,
( $false
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f295,f273]) ).
fof(f313,plain,
~ spl0_15,
inference(avatar_contradiction_clause,[],[f312]) ).
fof(f314,plain,
! [X2,X0,X1] :
( product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| product(X0,X1,e_5)
| ~ group_element(X0)
| ~ group_element(X1)
| equalish(X2,X0)
| ~ group_element(X1)
| product(X2,X1,e_1)
| product(X2,X1,e_2)
| product(X2,X1,e_3)
| product(X2,X1,e_4)
| product(X2,X1,e_5)
| ~ group_element(X2) ),
inference(resolution,[],[f73,f58]) ).
fof(f315,plain,
! [X2,X0,X1] :
( product(X2,X1,e_5)
| product(X0,X1,e_5)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| product(X0,X1,e_2)
| ~ group_element(X0)
| ~ group_element(X1)
| equalish(X2,X0)
| product(X2,X1,e_1)
| product(X2,X1,e_2)
| product(X2,X1,e_3)
| product(X2,X1,e_4)
| product(X0,X1,e_1)
| ~ group_element(X2) ),
inference(duplicate_literal_removal,[],[f314]) ).
fof(f317,plain,
! [X2,X0,X1] :
( product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| product(X0,X1,e_5)
| ~ group_element(X0)
| ~ group_element(X1)
| equalish(X2,X1)
| ~ group_element(X2)
| product(X0,X2,e_1)
| product(X0,X2,e_2)
| product(X0,X2,e_3)
| product(X0,X2,e_4)
| product(X0,X2,e_5)
| ~ group_element(X0) ),
inference(resolution,[],[f74,f58]) ).
fof(f318,plain,
! [X2,X0,X1] :
( product(X0,X2,e_5)
| product(X0,X1,e_5)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| product(X0,X1,e_2)
| ~ group_element(X0)
| ~ group_element(X1)
| equalish(X2,X1)
| ~ group_element(X2)
| product(X0,X2,e_1)
| product(X0,X2,e_2)
| product(X0,X2,e_3)
| product(X0,X2,e_4)
| product(X0,X1,e_1) ),
inference(duplicate_literal_removal,[],[f317]) ).
fof(f355,plain,
( ~ product(e_3,e_1,e_4)
| ~ spl0_16 ),
inference(unit_resulting_resolution,[],[f61,f41,f233]) ).
fof(f371,plain,
( $false
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f355,f122]) ).
fof(f372,plain,
( ~ spl0_6
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f371]) ).
fof(f397,definition,
( spl0_23
<=> product(e_5,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f398,plain,
( ~ product(e_5,e_4,e_5)
| spl0_23 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f399,plain,
( product(e_5,e_4,e_5)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f408,definition,
( spl0_26
<=> product(e_6,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f409,plain,
( ~ product(e_6,e_1,e_2)
| spl0_26 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f410,plain,
( product(e_6,e_1,e_2)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f415,definition,
( spl0_28
<=> product(e_6,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f416,plain,
( ~ product(e_6,e_1,e_1)
| spl0_28 ),
inference(avatar_component_clause,[],[f415]) ).
fof(f417,plain,
( product(e_6,e_1,e_1)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f415]) ).
fof(f419,definition,
( spl0_29
<=> product(e_6,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f420,plain,
( ~ product(e_6,e_1,e_3)
| spl0_29 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f426,definition,
( spl0_30
<=> product(e_6,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f427,plain,
( ~ product(e_6,e_1,e_4)
| spl0_30 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f464,plain,
( ~ product(e_2,e_1,e_3)
| ~ spl0_17 ),
inference(unit_resulting_resolution,[],[f61,f36,f237]) ).
fof(f484,plain,
( $false
| ~ spl0_3
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f464,f105]) ).
fof(f485,plain,
( ~ spl0_3
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f484]) ).
fof(f517,plain,
( ~ product(e_4,e_1,e_2)
| ~ spl0_18 ),
inference(unit_resulting_resolution,[],[f61,f51,f241]) ).
fof(f518,plain,
( ~ product(e_6,e_1,e_2)
| ~ spl0_18 ),
inference(unit_resulting_resolution,[],[f61,f52,f241]) ).
fof(f520,plain,
( ~ product(e_1,e_1,e_2)
| ~ spl0_18 ),
inference(unit_resulting_resolution,[],[f61,f31,f241]) ).
fof(f539,plain,
( ~ spl0_13
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f517,f239,f152]) ).
fof(f540,plain,
( ~ spl0_26
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f518,f239,f408]) ).
fof(f541,plain,
( $false
| ~ spl0_1
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f520,f91]) ).
fof(f542,plain,
( ~ spl0_1
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f541]) ).
fof(f565,plain,
( ~ product(e_5,e_3,e_6)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20 ),
inference(unit_resulting_resolution,[],[f74,f38,f22,f26,f228,f232,f236,f250,f240]) ).
fof(f566,plain,
( ~ product(e_5,e_4,e_6)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20 ),
inference(unit_resulting_resolution,[],[f74,f43,f22,f26,f228,f232,f236,f250,f240]) ).
fof(f574,plain,
( product(e_5,e_1,e_6)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20 ),
inference(unit_resulting_resolution,[],[f58,f26,f22,f228,f232,f236,f250,f240]) ).
fof(f589,definition,
( spl0_31
<=> product(e_6,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f590,plain,
( ~ product(e_6,e_5,e_5)
| spl0_31 ),
inference(avatar_component_clause,[],[f589]) ).
fof(f591,plain,
( product(e_6,e_5,e_5)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f589]) ).
fof(f593,definition,
( spl0_32
<=> product(e_6,e_5,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f594,plain,
( ~ product(e_6,e_5,e_4)
| spl0_32 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f595,plain,
( product(e_6,e_5,e_4)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f597,definition,
( spl0_33
<=> product(e_6,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f598,plain,
( ~ product(e_6,e_5,e_3)
| spl0_33 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f599,plain,
( product(e_6,e_5,e_3)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f601,definition,
( spl0_34
<=> product(e_6,e_5,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f602,plain,
( ~ product(e_6,e_5,e_2)
| spl0_34 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f603,plain,
( product(e_6,e_5,e_2)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f605,definition,
( spl0_35
<=> product(e_6,e_5,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f606,plain,
( ~ product(e_6,e_5,e_1)
| spl0_35 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f607,plain,
( product(e_6,e_5,e_1)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f643,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_20 ),
inference(unit_resulting_resolution,[],[f61,f31,f251]) ).
fof(f649,plain,
( ~ product(e_1,e_1,e_2)
| spl0_18
| ~ spl0_20 ),
inference(unit_resulting_resolution,[],[f62,f240,f251]) ).
fof(f664,plain,
( $false
| ~ spl0_1
| spl0_18
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f649,f91]) ).
fof(f665,plain,
( ~ spl0_1
| spl0_18
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f664]) ).
fof(f666,plain,
( ~ spl0_28
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f189,f93,f415]) ).
fof(f679,plain,
( $false
| ~ spl0_2
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f643,f95]) ).
fof(f680,plain,
( ~ spl0_2
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f679]) ).
fof(f764,plain,
( ~ product(e_3,e_1,e_2)
| ~ spl0_1 ),
inference(unit_resulting_resolution,[],[f61,f38,f91]) ).
fof(f767,plain,
( ~ product(e_6,e_1,e_2)
| ~ spl0_1 ),
inference(unit_resulting_resolution,[],[f61,f53,f91]) ).
fof(f777,plain,
( ! [X0] :
( ~ product(X0,e_1,e_1)
| product(X0,e_1,e_2) )
| ~ spl0_1 ),
inference(resolution,[],[f91,f62]) ).
fof(f815,plain,
( ~ product(e_6,e_1,e_3)
| ~ spl0_3 ),
inference(unit_resulting_resolution,[],[f61,f37,f105]) ).
fof(f818,plain,
( ~ product(e_3,e_1,e_3)
| ~ spl0_3 ),
inference(unit_resulting_resolution,[],[f61,f39,f105]) ).
fof(f819,plain,
( ~ product(e_4,e_1,e_3)
| ~ spl0_3 ),
inference(unit_resulting_resolution,[],[f61,f44,f105]) ).
fof(f838,plain,
( ~ spl0_29
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f815,f103,f419]) ).
fof(f843,plain,
( ! [X0] :
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| ~ group_element(e_2)
| ~ next(e_2,X0)
| ~ greater(e_6,X0) )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f221,f777]) ).
fof(f845,plain,
( ! [X0] :
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| ~ group_element(e_2)
| ~ next(e_2,X0)
| ~ greater(e_6,X0) )
| ~ spl0_1
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f843,f108]) ).
fof(f847,plain,
( ! [X0] :
( product(e_2,e_1,e_4)
| ~ group_element(e_2)
| ~ next(e_2,X0)
| ~ greater(e_6,X0) )
| ~ spl0_1
| spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f845,f104]) ).
fof(f849,plain,
( ! [X0] :
( ~ group_element(e_2)
| ~ next(e_2,X0)
| ~ greater(e_6,X0) )
| ~ spl0_1
| spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f847,f67]) ).
fof(f851,plain,
( ! [X0] :
( ~ greater(e_6,X0)
| ~ next(e_2,X0) )
| ~ spl0_1
| spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f849,f23]) ).
fof(f857,plain,
( ~ next(e_2,e_3)
| ~ spl0_1
| spl0_3
| spl0_4 ),
inference(unit_resulting_resolution,[],[f851,f17]) ).
fof(f871,plain,
( $false
| ~ spl0_1
| spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f857,f2]) ).
fof(f872,plain,
( ~ spl0_1
| spl0_3
| spl0_4 ),
inference(avatar_contradiction_clause,[],[f871]) ).
fof(f877,plain,
( ~ spl0_12
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f819,f103,f148]) ).
fof(f878,plain,
( ~ spl0_7
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f818,f103,f124]) ).
fof(f888,plain,
( $false
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f764,f130]) ).
fof(f889,plain,
( ~ spl0_1
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[],[f888]) ).
fof(f890,plain,
( ! [X0] :
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| ~ group_element(e_3)
| ~ next(e_3,X0)
| ~ greater(e_6,X0) )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f222,f777]) ).
fof(f891,plain,
( ! [X0] :
( product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| ~ group_element(e_3)
| ~ next(e_3,X0)
| ~ greater(e_6,X0) )
| ~ spl0_1
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f890,f129]) ).
fof(f892,plain,
( ! [X0] :
( product(e_3,e_1,e_4)
| ~ group_element(e_3)
| ~ next(e_3,X0)
| ~ greater(e_6,X0) )
| ~ spl0_1
| spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f891,f125]) ).
fof(f893,plain,
( ! [X0] :
( ~ group_element(e_3)
| ~ next(e_3,X0)
| ~ greater(e_6,X0) )
| ~ spl0_1
| spl0_6
| spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f892,f121]) ).
fof(f894,plain,
( ! [X0] :
( ~ greater(e_6,X0)
| ~ next(e_3,X0) )
| ~ spl0_1
| spl0_6
| spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f893,f24]) ).
fof(f899,plain,
( ~ next(e_3,e_4)
| ~ spl0_1
| spl0_6
| spl0_7
| spl0_8 ),
inference(unit_resulting_resolution,[],[f894,f19]) ).
fof(f912,plain,
( $false
| ~ spl0_1
| spl0_6
| spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f899,f3]) ).
fof(f913,plain,
( ~ spl0_1
| spl0_6
| spl0_7
| spl0_8 ),
inference(avatar_contradiction_clause,[],[f912]) ).
fof(f1047,plain,
( ~ product(e_4,e_1,e_4)
| ~ spl0_6 ),
inference(unit_resulting_resolution,[],[f61,f45,f122]) ).
fof(f1049,plain,
( ~ product(e_6,e_1,e_4)
| ~ spl0_6 ),
inference(unit_resulting_resolution,[],[f61,f55,f122]) ).
fof(f1051,plain,
( product(e_2,e_3,e_4)
| ~ spl0_3
| ~ spl0_6 ),
inference(unit_resulting_resolution,[],[f62,f105,f122]) ).
fof(f1071,definition,
( spl0_37
<=> product(e_3,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f1073,plain,
( product(e_3,e_4,e_5)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f1071]) ).
fof(f1092,plain,
( ~ product(e_5,e_5,e_5)
| ~ spl0_23 ),
inference(unit_resulting_resolution,[],[f60,f46,f399]) ).
fof(f1114,plain,
( product(e_5,e_5,e_5)
| ~ spl0_23 ),
inference(unit_resulting_resolution,[],[f62,f399,f399]) ).
fof(f1124,plain,
( $false
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1114,f1092]) ).
fof(f1125,plain,
~ spl0_23,
inference(avatar_contradiction_clause,[],[f1124]) ).
fof(f1163,plain,
( ~ product(e_6,e_1,e_5)
| ~ spl0_10 ),
inference(unit_resulting_resolution,[],[f61,f47,f142]) ).
fof(f1196,plain,
( ~ product(e_6,e_1,e_1)
| ~ spl0_1
| spl0_26 ),
inference(unit_resulting_resolution,[],[f62,f91,f409]) ).
fof(f1207,plain,
( $false
| ~ spl0_6
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1047,f146]) ).
fof(f1208,plain,
( ~ spl0_6
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f1207]) ).
fof(f1269,definition,
( spl0_38
<=> product(e_5,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f1270,plain,
( ~ product(e_5,e_2,e_5)
| spl0_38 ),
inference(avatar_component_clause,[],[f1269]) ).
fof(f1271,plain,
( product(e_5,e_2,e_5)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f1269]) ).
fof(f1273,definition,
( spl0_39
<=> product(e_5,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f1274,plain,
( ~ product(e_5,e_2,e_4)
| spl0_39 ),
inference(avatar_component_clause,[],[f1273]) ).
fof(f1275,plain,
( product(e_5,e_2,e_4)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f1273]) ).
fof(f1277,definition,
( spl0_40
<=> product(e_5,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f1278,plain,
( ~ product(e_5,e_2,e_3)
| spl0_40 ),
inference(avatar_component_clause,[],[f1277]) ).
fof(f1279,plain,
( product(e_5,e_2,e_3)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f1277]) ).
fof(f1281,definition,
( spl0_41
<=> product(e_5,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f1282,plain,
( ~ product(e_5,e_2,e_2)
| spl0_41 ),
inference(avatar_component_clause,[],[f1281]) ).
fof(f1283,plain,
( product(e_5,e_2,e_2)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f1281]) ).
fof(f1285,definition,
( spl0_42
<=> product(e_5,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f1287,plain,
( product(e_5,e_2,e_1)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f1285]) ).
fof(f1290,plain,
( ~ group_element(e_3)
| product(e_5,e_3,e_1)
| product(e_5,e_3,e_2)
| product(e_5,e_3,e_3)
| product(e_5,e_3,e_4)
| product(e_5,e_3,e_5)
| ~ group_element(e_5)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20 ),
inference(resolution,[],[f565,f58]) ).
fof(f1291,plain,
( product(e_5,e_3,e_1)
| product(e_5,e_3,e_2)
| product(e_5,e_3,e_3)
| product(e_5,e_3,e_4)
| product(e_5,e_3,e_5)
| ~ group_element(e_5)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1290,f24]) ).
fof(f1292,plain,
( product(e_5,e_3,e_1)
| product(e_5,e_3,e_2)
| product(e_5,e_3,e_3)
| product(e_5,e_3,e_4)
| product(e_5,e_3,e_5)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1291,f26]) ).
fof(f1294,definition,
( spl0_43
<=> product(e_5,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f1295,plain,
( ~ product(e_5,e_3,e_5)
| spl0_43 ),
inference(avatar_component_clause,[],[f1294]) ).
fof(f1296,plain,
( product(e_5,e_3,e_5)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f1294]) ).
fof(f1298,definition,
( spl0_44
<=> product(e_5,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f1299,plain,
( ~ product(e_5,e_3,e_4)
| spl0_44 ),
inference(avatar_component_clause,[],[f1298]) ).
fof(f1302,definition,
( spl0_45
<=> product(e_5,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f1304,plain,
( product(e_5,e_3,e_3)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f1302]) ).
fof(f1306,definition,
( spl0_46
<=> product(e_5,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f1307,plain,
( ~ product(e_5,e_3,e_2)
| spl0_46 ),
inference(avatar_component_clause,[],[f1306]) ).
fof(f1308,plain,
( product(e_5,e_3,e_2)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f1306]) ).
fof(f1310,definition,
( spl0_47
<=> product(e_5,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f1311,plain,
( ~ product(e_5,e_3,e_1)
| spl0_47 ),
inference(avatar_component_clause,[],[f1310]) ).
fof(f1312,plain,
( product(e_5,e_3,e_1)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f1310]) ).
fof(f1313,plain,
( spl0_43
| spl0_44
| spl0_45
| spl0_46
| spl0_47
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20 ),
inference(avatar_split_clause,[],[f1292,f249,f239,f235,f231,f227,f1310,f1306,f1302,f1298,f1294]) ).
fof(f1315,plain,
( product(e_3,e_4,e_5)
| ~ spl0_6
| spl0_11
| spl0_12
| spl0_13
| spl0_14 ),
inference(unit_resulting_resolution,[],[f219,f25,f4,f20,f122,f153,f145,f149,f157]) ).
fof(f1319,plain,
( ~ group_element(e_4)
| product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_4)
| product(e_5,e_4,e_5)
| ~ group_element(e_5)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20 ),
inference(resolution,[],[f566,f58]) ).
fof(f1320,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_4)
| product(e_5,e_4,e_5)
| ~ group_element(e_5)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1319,f25]) ).
fof(f1321,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_4)
| ~ group_element(e_5)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_23 ),
inference(forward_subsumption_resolution,[],[f1320,f398]) ).
fof(f1322,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_4)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_23 ),
inference(forward_subsumption_resolution,[],[f1321,f26]) ).
fof(f1324,definition,
( spl0_48
<=> product(e_5,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f1326,plain,
( product(e_5,e_4,e_4)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f1324]) ).
fof(f1328,definition,
( spl0_49
<=> product(e_5,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f1330,plain,
( product(e_5,e_4,e_3)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f1328]) ).
fof(f1332,definition,
( spl0_50
<=> product(e_5,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f1334,plain,
( product(e_5,e_4,e_2)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f1332]) ).
fof(f1336,definition,
( spl0_51
<=> product(e_5,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f1338,plain,
( product(e_5,e_4,e_1)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f1336]) ).
fof(f1339,plain,
( spl0_48
| spl0_49
| spl0_50
| spl0_51
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_23 ),
inference(avatar_split_clause,[],[f1322,f397,f249,f239,f235,f231,f227,f1336,f1332,f1328,f1324]) ).
fof(f1362,plain,
! [X0] :
( product(e_6,X0,e_5)
| product(e_6,e_6,e_6)
| product(e_6,X0,e_4)
| product(e_6,X0,e_3)
| ~ group_element(X0)
| product(e_6,X0,e_2)
| product(e_6,X0,e_1)
| product(e_6,X0,e_2)
| product(e_6,X0,e_3)
| product(e_6,X0,e_4)
| product(e_6,X0,e_1)
| ~ group_element(e_6) ),
inference(factoring,[],[f81]) ).
fof(f1363,plain,
! [X0] :
( product(e_6,X0,e_5)
| product(e_6,e_6,e_6)
| product(e_6,X0,e_4)
| product(e_6,X0,e_3)
| ~ group_element(X0)
| product(e_6,X0,e_2)
| product(e_6,X0,e_1)
| ~ group_element(e_6) ),
inference(duplicate_literal_removal,[],[f1362]) ).
fof(f1371,plain,
! [X0] :
( product(e_6,X0,e_5)
| product(e_6,e_6,e_6)
| product(e_6,X0,e_4)
| product(e_6,X0,e_3)
| ~ group_element(X0)
| product(e_6,X0,e_2)
| product(e_6,X0,e_1) ),
inference(forward_subsumption_resolution,[],[f1363,f27]) ).
fof(f1378,definition,
( spl0_52
<=> product(e_6,e_6,e_6) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f1380,plain,
( product(e_6,e_6,e_6)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f1378]) ).
fof(f1382,definition,
( spl0_53
<=> ! [X0] :
( product(e_6,X0,e_5)
| product(e_6,X0,e_1)
| product(e_6,X0,e_2)
| ~ group_element(X0)
| product(e_6,X0,e_3)
| product(e_6,X0,e_4) ) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f1383,plain,
( ! [X0] :
( product(e_6,X0,e_5)
| product(e_6,X0,e_1)
| product(e_6,X0,e_2)
| ~ group_element(X0)
| product(e_6,X0,e_3)
| product(e_6,X0,e_4) )
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f1382]) ).
fof(f1384,plain,
( spl0_52
| spl0_53 ),
inference(avatar_split_clause,[],[f1371,f1382,f1378]) ).
fof(f1388,definition,
( spl0_54
<=> product(e_6,e_5,e_6) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f1389,plain,
( ~ product(e_6,e_5,e_6)
| spl0_54 ),
inference(avatar_component_clause,[],[f1388]) ).
fof(f1390,plain,
( product(e_6,e_5,e_6)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f1388]) ).
fof(f1462,definition,
( spl0_58
<=> product(e_5,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f1552,plain,
( product(e_6,e_1,e_5)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_26
| spl0_28
| spl0_29
| spl0_30 ),
inference(unit_resulting_resolution,[],[f315,f26,f22,f27,f52,f416,f409,f427,f420,f232,f236,f240,f250,f228]) ).
fof(f1619,plain,
( $false
| ~ spl0_10
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_26
| spl0_28
| spl0_29
| spl0_30 ),
inference(forward_subsumption_resolution,[],[f1552,f1163]) ).
fof(f1620,plain,
( ~ spl0_10
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_26
| spl0_28
| spl0_29
| spl0_30 ),
inference(avatar_contradiction_clause,[],[f1619]) ).
fof(f1655,plain,
( $false
| ~ spl0_1
| spl0_26
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f1196,f417]) ).
fof(f1656,plain,
( ~ spl0_1
| spl0_26
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f1655]) ).
fof(f1659,plain,
( $false
| ~ spl0_1
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f767,f410]) ).
fof(f1660,plain,
( ~ spl0_1
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f1659]) ).
fof(f1782,plain,
( ~ product(e_4,e_1,e_2)
| ~ spl0_26 ),
inference(unit_resulting_resolution,[],[f61,f47,f410]) ).
fof(f1785,plain,
( product(e_6,e_2,e_3)
| ~ spl0_3
| ~ spl0_26 ),
inference(unit_resulting_resolution,[],[f62,f105,f410]) ).
fof(f1946,definition,
( spl0_71
<=> product(e_5,e_6,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f1947,plain,
( ~ product(e_5,e_6,e_2)
| spl0_71 ),
inference(avatar_component_clause,[],[f1946]) ).
fof(f1948,plain,
( product(e_5,e_6,e_2)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f1946]) ).
fof(f2010,plain,
( product(e_5,e_6,e_2)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| ~ spl0_26 ),
inference(unit_resulting_resolution,[],[f62,f410,f574]) ).
fof(f2035,plain,
( ~ product(e_6,e_5,e_6)
| ~ spl0_31 ),
inference(unit_resulting_resolution,[],[f59,f57,f591]) ).
fof(f2074,plain,
( $false
| ~ spl0_31
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f2035,f1390]) ).
fof(f2075,plain,
( ~ spl0_31
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[],[f2074]) ).
fof(f2092,plain,
( ~ product(e_6,e_5,e_6)
| ~ spl0_32 ),
inference(unit_resulting_resolution,[],[f59,f56,f595]) ).
fof(f2129,plain,
( $false
| ~ spl0_32
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f2092,f1390]) ).
fof(f2130,plain,
( ~ spl0_32
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[],[f2129]) ).
fof(f2183,plain,
( ~ product(e_5,e_3,e_4)
| ~ spl0_3
| ~ spl0_6 ),
inference(unit_resulting_resolution,[],[f61,f36,f1051]) ).
fof(f2199,plain,
( ~ spl0_44
| ~ spl0_3
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f2183,f120,f103,f1298]) ).
fof(f2235,plain,
( ~ product(e_3,e_3,e_5)
| ~ spl0_37 ),
inference(unit_resulting_resolution,[],[f60,f45,f1073]) ).
fof(f2324,plain,
( ~ product(e_6,e_1,e_5)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_54 ),
inference(unit_resulting_resolution,[],[f62,f574,f1389]) ).
fof(f2341,plain,
( ~ product(e_5,e_4,e_4)
| ~ spl0_39 ),
inference(unit_resulting_resolution,[],[f60,f35,f1275]) ).
fof(f2376,plain,
( $false
| ~ spl0_39
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f2341,f1326]) ).
fof(f2377,plain,
( ~ spl0_39
| ~ spl0_48 ),
inference(avatar_contradiction_clause,[],[f2376]) ).
fof(f2458,plain,
( product(e_6,e_5,e_1)
| product(e_6,e_5,e_2)
| ~ group_element(e_5)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_4)
| spl0_31
| ~ spl0_53 ),
inference(resolution,[],[f1383,f590]) ).
fof(f2488,plain,
( ~ product(e_5,e_3,e_1)
| ~ spl0_42 ),
inference(unit_resulting_resolution,[],[f60,f34,f1287]) ).
fof(f2526,plain,
( ~ spl0_47
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f2488,f1285,f1310]) ).
fof(f2625,plain,
( ~ product(e_5,e_5,e_5)
| ~ spl0_38 ),
inference(unit_resulting_resolution,[],[f60,f36,f1271]) ).
fof(f2647,plain,
( product(e_5,e_5,e_5)
| ~ spl0_38 ),
inference(unit_resulting_resolution,[],[f62,f1271,f1271]) ).
fof(f2660,plain,
( ~ spl0_58
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f2625,f1269,f1462]) ).
fof(f2662,plain,
( spl0_58
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f2647,f1269,f1462]) ).
fof(f2751,plain,
( ~ product(e_6,e_2,e_3)
| ~ spl0_40 ),
inference(unit_resulting_resolution,[],[f61,f57,f1279]) ).
fof(f2773,plain,
( $false
| ~ spl0_3
| ~ spl0_26
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f2751,f1785]) ).
fof(f2774,plain,
( ~ spl0_3
| ~ spl0_26
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f2773]) ).
fof(f2839,plain,
( product(e_5,e_2,e_1)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_38
| spl0_39
| spl0_40
| spl0_41 ),
inference(unit_resulting_resolution,[],[f318,f26,f23,f22,f33,f250,f240,f232,f236,f228,f1274,f1278,f1270,f1282]) ).
fof(f2917,plain,
( ~ product(e_3,e_3,e_3)
| ~ spl0_45 ),
inference(unit_resulting_resolution,[],[f61,f50,f1304]) ).
fof(f2928,plain,
( ~ product(e_3,e_3,e_4)
| spl0_44
| ~ spl0_45 ),
inference(unit_resulting_resolution,[],[f62,f1299,f1304]) ).
fof(f2931,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_4)
| product(e_3,e_3,e_5)
| ~ group_element(e_3)
| ~ group_element(e_3)
| product(e_5,e_3,e_6)
| ~ spl0_45 ),
inference(resolution,[],[f1304,f76]) ).
fof(f2936,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_4)
| product(e_3,e_3,e_5)
| ~ group_element(e_3)
| product(e_5,e_3,e_6)
| ~ spl0_45 ),
inference(duplicate_literal_removal,[],[f2931]) ).
fof(f2951,definition,
( spl0_87
<=> product(e_3,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f2952,plain,
( ~ product(e_3,e_3,e_2)
| spl0_87 ),
inference(avatar_component_clause,[],[f2951]) ).
fof(f2953,plain,
( product(e_3,e_3,e_2)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f2951]) ).
fof(f2955,definition,
( spl0_88
<=> product(e_3,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f2957,plain,
( product(e_3,e_3,e_1)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f2955]) ).
fof(f2967,plain,
( ~ product(e_3,e_3,e_2)
| ~ spl0_45
| spl0_46 ),
inference(unit_resulting_resolution,[],[f62,f1304,f1307]) ).
fof(f2968,plain,
( $false
| ~ spl0_45
| spl0_46
| ~ spl0_87 ),
inference(forward_subsumption_resolution,[],[f2967,f2953]) ).
fof(f2969,plain,
( ~ spl0_45
| spl0_46
| ~ spl0_87 ),
inference(avatar_contradiction_clause,[],[f2968]) ).
fof(f2974,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_4)
| product(e_3,e_3,e_5)
| ~ group_element(e_3)
| product(e_5,e_3,e_6)
| ~ spl0_45
| spl0_87 ),
inference(forward_subsumption_resolution,[],[f2936,f2952]) ).
fof(f2975,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_4)
| product(e_3,e_3,e_5)
| ~ group_element(e_3)
| product(e_5,e_3,e_6)
| ~ spl0_45
| spl0_87 ),
inference(forward_subsumption_resolution,[],[f2974,f2917]) ).
fof(f2976,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_5)
| ~ group_element(e_3)
| product(e_5,e_3,e_6)
| spl0_44
| ~ spl0_45
| spl0_87 ),
inference(forward_subsumption_resolution,[],[f2975,f2928]) ).
fof(f2977,plain,
( product(e_3,e_3,e_1)
| ~ group_element(e_3)
| product(e_5,e_3,e_6)
| ~ spl0_37
| spl0_44
| ~ spl0_45
| spl0_87 ),
inference(forward_subsumption_resolution,[],[f2976,f2235]) ).
fof(f2978,plain,
( product(e_3,e_3,e_1)
| product(e_5,e_3,e_6)
| ~ spl0_37
| spl0_44
| ~ spl0_45
| spl0_87 ),
inference(forward_subsumption_resolution,[],[f2977,f24]) ).
fof(f2979,plain,
( product(e_3,e_3,e_1)
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| ~ spl0_37
| spl0_44
| ~ spl0_45
| spl0_87 ),
inference(forward_subsumption_resolution,[],[f2978,f565]) ).
fof(f2980,plain,
( spl0_88
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| ~ spl0_37
| spl0_44
| ~ spl0_45
| spl0_87 ),
inference(avatar_split_clause,[],[f2979,f2951,f1302,f1298,f1071,f249,f239,f235,f231,f227,f2955]) ).
fof(f3100,plain,
( ~ product(e_3,e_3,e_1)
| ~ spl0_45
| spl0_47 ),
inference(unit_resulting_resolution,[],[f62,f1304,f1311]) ).
fof(f3101,plain,
( $false
| ~ spl0_45
| spl0_47
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f3100,f2957]) ).
fof(f3102,plain,
( ~ spl0_45
| spl0_47
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f3101]) ).
fof(f3132,plain,
( ~ product(e_5,e_6,e_2)
| ~ spl0_41 ),
inference(unit_resulting_resolution,[],[f60,f54,f1283]) ).
fof(f3179,plain,
( spl0_42
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_38
| spl0_39
| spl0_40
| spl0_41 ),
inference(avatar_split_clause,[],[f2839,f1281,f1277,f1273,f1269,f249,f239,f235,f231,f227,f1285]) ).
fof(f3366,plain,
( ~ product(e_5,e_5,e_5)
| ~ spl0_43 ),
inference(unit_resulting_resolution,[],[f60,f41,f1296]) ).
fof(f3388,plain,
( product(e_5,e_5,e_5)
| ~ spl0_43 ),
inference(unit_resulting_resolution,[],[f62,f1296,f1296]) ).
fof(f3398,plain,
( ~ spl0_58
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f3366,f1294,f1462]) ).
fof(f3400,plain,
( spl0_58
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f3388,f1294,f1462]) ).
fof(f3401,plain,
( ~ spl0_71
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f3132,f1281,f1946]) ).
fof(f3403,plain,
( $false
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| ~ spl0_26
| spl0_71 ),
inference(forward_subsumption_resolution,[],[f2010,f1947]) ).
fof(f3404,plain,
( spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| ~ spl0_26
| spl0_71 ),
inference(avatar_contradiction_clause,[],[f3403]) ).
fof(f3414,plain,
( product(e_6,e_5,e_2)
| ~ group_element(e_5)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_4)
| spl0_31
| spl0_35
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f2458,f606]) ).
fof(f3420,plain,
( ~ group_element(e_5)
| product(e_6,e_5,e_3)
| product(e_6,e_5,e_4)
| spl0_31
| spl0_34
| spl0_35
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f3414,f602]) ).
fof(f3424,plain,
( product(e_6,e_5,e_3)
| product(e_6,e_5,e_4)
| spl0_31
| spl0_34
| spl0_35
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f3420,f26]) ).
fof(f3428,plain,
( product(e_6,e_5,e_4)
| spl0_31
| spl0_33
| spl0_34
| spl0_35
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f3424,f598]) ).
fof(f3432,plain,
( $false
| spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f3428,f594]) ).
fof(f3433,plain,
( spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f3432]) ).
fof(f3446,plain,
( ~ product(e_6,e_5,e_6)
| ~ spl0_33 ),
inference(unit_resulting_resolution,[],[f59,f42,f599]) ).
fof(f3521,plain,
( ~ product(e_6,e_5,e_6)
| ~ spl0_35 ),
inference(unit_resulting_resolution,[],[f59,f53,f607]) ).
fof(f3607,plain,
( $false
| ~ spl0_13
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f1782,f154]) ).
fof(f3608,plain,
( ~ spl0_13
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f3607]) ).
fof(f3696,plain,
( ~ product(e_5,e_4,e_3)
| ~ spl0_37
| spl0_43 ),
inference(unit_resulting_resolution,[],[f62,f1073,f1295]) ).
fof(f3729,plain,
( ~ product(e_5,e_4,e_1)
| ~ spl0_47 ),
inference(unit_resulting_resolution,[],[f60,f45,f1312]) ).
fof(f3789,plain,
( ~ product(e_5,e_6,e_2)
| ~ spl0_50 ),
inference(unit_resulting_resolution,[],[f60,f56,f1334]) ).
fof(f3823,plain,
( $false
| ~ spl0_50
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f3789,f1948]) ).
fof(f3824,plain,
( ~ spl0_50
| ~ spl0_71 ),
inference(avatar_contradiction_clause,[],[f3823]) ).
fof(f3837,plain,
( $false
| ~ spl0_37
| spl0_43
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f3696,f1330]) ).
fof(f3838,plain,
( ~ spl0_37
| spl0_43
| ~ spl0_49 ),
inference(avatar_contradiction_clause,[],[f3837]) ).
fof(f3841,plain,
( $false
| ~ spl0_47
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f3729,f1338]) ).
fof(f3842,plain,
( ~ spl0_47
| ~ spl0_51 ),
inference(avatar_contradiction_clause,[],[f3841]) ).
fof(f3865,plain,
( ~ product(e_5,e_6,e_2)
| ~ spl0_46 ),
inference(unit_resulting_resolution,[],[f60,f55,f1308]) ).
fof(f3898,plain,
( $false
| ~ spl0_46
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f3865,f1948]) ).
fof(f3899,plain,
( ~ spl0_46
| ~ spl0_71 ),
inference(avatar_contradiction_clause,[],[f3898]) ).
fof(f3914,plain,
( $false
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_26
| spl0_28
| spl0_29
| spl0_30
| spl0_54 ),
inference(forward_subsumption_resolution,[],[f2324,f1552]) ).
fof(f3915,plain,
( spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_26
| spl0_28
| spl0_29
| spl0_30
| spl0_54 ),
inference(avatar_contradiction_clause,[],[f3914]) ).
fof(f3953,plain,
( product(e_4,e_1,e_2)
| spl0_10
| spl0_11
| spl0_12
| spl0_14 ),
inference(unit_resulting_resolution,[],[f58,f25,f22,f72,f145,f149,f157,f141]) ).
fof(f4048,plain,
( ~ product(e_6,e_5,e_6)
| ~ spl0_34 ),
inference(unit_resulting_resolution,[],[f59,f54,f603]) ).
fof(f4083,plain,
( $false
| ~ spl0_34
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f4048,f1390]) ).
fof(f4084,plain,
( ~ spl0_34
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[],[f4083]) ).
fof(f4149,plain,
( ~ product(e_6,e_6,e_6)
| spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35 ),
inference(unit_resulting_resolution,[],[f74,f57,f26,f27,f590,f594,f598,f602,f606]) ).
fof(f4167,plain,
( $false
| spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f4149,f1380]) ).
fof(f4168,plain,
( spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35
| ~ spl0_52 ),
inference(avatar_contradiction_clause,[],[f4167]) ).
fof(f4171,plain,
( $false
| ~ spl0_33
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f3446,f1390]) ).
fof(f4172,plain,
( ~ spl0_33
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[],[f4171]) ).
fof(f4175,plain,
( ~ spl0_54
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f3521,f605,f1388]) ).
fof(f4261,plain,
( ~ product(e_2,e_2,e_2)
| ~ spl0_4 ),
inference(unit_resulting_resolution,[],[f60,f28,f109]) ).
fof(f4287,plain,
( product(e_2,e_2,e_2)
| ~ spl0_4 ),
inference(unit_resulting_resolution,[],[f62,f109,f109]) ).
fof(f4300,plain,
( $false
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f4287,f4261]) ).
fof(f4301,plain,
~ spl0_4,
inference(avatar_contradiction_clause,[],[f4300]) ).
fof(f4303,plain,
( spl0_13
| spl0_10
| spl0_11
| spl0_12
| spl0_14 ),
inference(avatar_split_clause,[],[f3953,f156,f148,f144,f140,f152]) ).
fof(f4486,plain,
( product(e_3,e_2,e_3)
| ~ spl0_3
| ~ spl0_8 ),
inference(unit_resulting_resolution,[],[f62,f105,f130]) ).
fof(f4773,plain,
( ~ product(e_3,e_3,e_3)
| ~ spl0_3
| ~ spl0_8 ),
inference(unit_resulting_resolution,[],[f60,f34,f4486]) ).
fof(f4797,plain,
( product(e_3,e_3,e_3)
| ~ spl0_3
| ~ spl0_8 ),
inference(unit_resulting_resolution,[],[f62,f4486,f4486]) ).
fof(f4844,plain,
( $false
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f4797,f4773]) ).
fof(f4845,plain,
( ~ spl0_3
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[],[f4844]) ).
fof(f4877,plain,
( ~ spl0_30
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f1049,f120,f426]) ).
fof(f4880,plain,
( spl0_37
| ~ spl0_6
| spl0_11
| spl0_12
| spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f1315,f156,f152,f148,f144,f120,f1071]) ).
fof(f5465,plain,
( product(e_6,e_1,e_5)
| spl0_26
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_53 ),
inference(unit_resulting_resolution,[],[f1383,f22,f427,f420,f409,f416]) ).
fof(f5486,plain,
( $false
| ~ spl0_10
| spl0_26
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f5465,f1163]) ).
fof(f5487,plain,
( ~ spl0_10
| spl0_26
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f5486]) ).
fof(f5500,plain,
( product(e_6,e_1,e_5)
| spl0_26
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_52 ),
inference(unit_resulting_resolution,[],[f74,f27,f22,f53,f427,f420,f409,f416,f1380]) ).
fof(f5551,plain,
( $false
| ~ spl0_10
| spl0_26
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f5500,f1163]) ).
fof(f5552,plain,
( ~ spl0_10
| spl0_26
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_52 ),
inference(avatar_contradiction_clause,[],[f5551]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f96]) ).
cnf(s2,plain,
( spl0_3
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f114]) ).
cnf(s3,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f135]) ).
cnf(s7,plain,
( ~ spl0_2
| ~ spl0_5 ),
inference(sat_conversion,[],[f211]) ).
cnf(s8,plain,
( ~ spl0_2
| ~ spl0_9 ),
inference(sat_conversion,[],[f212]) ).
cnf(s9,plain,
( ~ spl0_2
| ~ spl0_14 ),
inference(sat_conversion,[],[f213]) ).
cnf(s26,plain,
~ spl0_15,
inference(sat_conversion,[],[f313]) ).
cnf(s35,plain,
( ~ spl0_6
| ~ spl0_16 ),
inference(sat_conversion,[],[f372]) ).
cnf(s45,plain,
( ~ spl0_3
| ~ spl0_17 ),
inference(sat_conversion,[],[f485]) ).
cnf(s52,plain,
( ~ spl0_13
| ~ spl0_18 ),
inference(sat_conversion,[],[f539]) ).
cnf(s53,plain,
( ~ spl0_18
| ~ spl0_26 ),
inference(sat_conversion,[],[f540]) ).
cnf(s54,plain,
( ~ spl0_1
| ~ spl0_18 ),
inference(sat_conversion,[],[f542]) ).
cnf(s62,plain,
( ~ spl0_1
| spl0_18
| ~ spl0_20 ),
inference(sat_conversion,[],[f665]) ).
cnf(s63,plain,
( ~ spl0_2
| ~ spl0_28 ),
inference(sat_conversion,[],[f666]) ).
cnf(s72,plain,
( ~ spl0_2
| ~ spl0_20 ),
inference(sat_conversion,[],[f680]) ).
cnf(s80,plain,
( ~ spl0_3
| ~ spl0_29 ),
inference(sat_conversion,[],[f838]) ).
cnf(s87,plain,
( ~ spl0_1
| spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f872]) ).
cnf(s91,plain,
( ~ spl0_3
| ~ spl0_12 ),
inference(sat_conversion,[],[f877]) ).
cnf(s92,plain,
( ~ spl0_3
| ~ spl0_7 ),
inference(sat_conversion,[],[f878]) ).
cnf(s101,plain,
( ~ spl0_1
| ~ spl0_8 ),
inference(sat_conversion,[],[f889]) ).
cnf(s105,plain,
( ~ spl0_1
| spl0_6
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f913]) ).
cnf(s112,plain,
~ spl0_23,
inference(sat_conversion,[],[f1125]) ).
cnf(s118,plain,
( ~ spl0_6
| ~ spl0_11 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s123,plain,
( spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_43
| spl0_44
| spl0_45
| spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f1313]) ).
cnf(s124,plain,
( spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_23
| spl0_48
| spl0_49
| spl0_50
| spl0_51 ),
inference(sat_conversion,[],[f1339]) ).
cnf(s125,plain,
( spl0_52
| spl0_53 ),
inference(sat_conversion,[],[f1384]) ).
cnf(s131,plain,
( ~ spl0_10
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_26
| spl0_28
| spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f1620]) ).
cnf(s134,plain,
( ~ spl0_1
| spl0_26
| ~ spl0_28 ),
inference(sat_conversion,[],[f1656]) ).
cnf(s136,plain,
( ~ spl0_1
| ~ spl0_26 ),
inference(sat_conversion,[],[f1660]) ).
cnf(s154,plain,
( ~ spl0_31
| ~ spl0_54 ),
inference(sat_conversion,[],[f2075]) ).
cnf(s162,plain,
( ~ spl0_32
| ~ spl0_54 ),
inference(sat_conversion,[],[f2130]) ).
cnf(s166,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_44 ),
inference(sat_conversion,[],[f2199]) ).
cnf(s184,plain,
( ~ spl0_39
| ~ spl0_48 ),
inference(sat_conversion,[],[f2377]) ).
cnf(s201,plain,
( ~ spl0_42
| ~ spl0_47 ),
inference(sat_conversion,[],[f2526]) ).
cnf(s224,plain,
( ~ spl0_38
| ~ spl0_58 ),
inference(sat_conversion,[],[f2660]) ).
cnf(s229,plain,
( ~ spl0_38
| spl0_58 ),
inference(sat_conversion,[],[f2662]) ).
cnf(s244,plain,
( ~ spl0_3
| ~ spl0_26
| ~ spl0_40 ),
inference(sat_conversion,[],[f2774]) ).
cnf(s269,plain,
( ~ spl0_45
| spl0_46
| ~ spl0_87 ),
inference(sat_conversion,[],[f2969]) ).
cnf(s272,plain,
( spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| ~ spl0_37
| spl0_44
| ~ spl0_45
| spl0_87
| spl0_88 ),
inference(sat_conversion,[],[f2980]) ).
cnf(s275,plain,
( ~ spl0_45
| spl0_47
| ~ spl0_88 ),
inference(sat_conversion,[],[f3102]) ).
cnf(s298,plain,
( spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_38
| spl0_39
| spl0_40
| spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f3179]) ).
cnf(s311,plain,
( ~ spl0_43
| ~ spl0_58 ),
inference(sat_conversion,[],[f3398]) ).
cnf(s315,plain,
( ~ spl0_43
| spl0_58 ),
inference(sat_conversion,[],[f3400]) ).
cnf(s321,plain,
( ~ spl0_41
| ~ spl0_71 ),
inference(sat_conversion,[],[f3401]) ).
cnf(s329,plain,
( spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| ~ spl0_26
| spl0_71 ),
inference(sat_conversion,[],[f3404]) ).
cnf(s334,plain,
( spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35
| ~ spl0_53 ),
inference(sat_conversion,[],[f3433]) ).
cnf(s355,plain,
( ~ spl0_13
| ~ spl0_26 ),
inference(sat_conversion,[],[f3608]) ).
cnf(s363,plain,
( ~ spl0_50
| ~ spl0_71 ),
inference(sat_conversion,[],[f3824]) ).
cnf(s368,plain,
( ~ spl0_37
| spl0_43
| ~ spl0_49 ),
inference(sat_conversion,[],[f3838]) ).
cnf(s370,plain,
( ~ spl0_47
| ~ spl0_51 ),
inference(sat_conversion,[],[f3842]) ).
cnf(s374,plain,
( ~ spl0_46
| ~ spl0_71 ),
inference(sat_conversion,[],[f3899]) ).
cnf(s384,plain,
( spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_20
| spl0_26
| spl0_28
| spl0_29
| spl0_30
| spl0_54 ),
inference(sat_conversion,[],[f3915]) ).
cnf(s417,plain,
( ~ spl0_34
| ~ spl0_54 ),
inference(sat_conversion,[],[f4084]) ).
cnf(s428,plain,
( spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35
| ~ spl0_52 ),
inference(sat_conversion,[],[f4168]) ).
cnf(s430,plain,
( ~ spl0_33
| ~ spl0_54 ),
inference(sat_conversion,[],[f4172]) ).
cnf(s433,plain,
( ~ spl0_35
| ~ spl0_54 ),
inference(sat_conversion,[],[f4175]) ).
cnf(s443,plain,
~ spl0_4,
inference(sat_conversion,[],[f4301]) ).
cnf(s465,plain,
( spl0_10
| spl0_11
| spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f4303]) ).
cnf(s522,plain,
( ~ spl0_3
| ~ spl0_8 ),
inference(sat_conversion,[],[f4845]) ).
cnf(s530,plain,
( ~ spl0_6
| ~ spl0_30 ),
inference(sat_conversion,[],[f4877]) ).
cnf(s538,plain,
( ~ spl0_6
| spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_37 ),
inference(sat_conversion,[],[f4880]) ).
cnf(s588,plain,
( ~ spl0_10
| spl0_26
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_53 ),
inference(sat_conversion,[],[f5487]) ).
cnf(s590,plain,
( ~ spl0_10
| spl0_26
| spl0_28
| spl0_29
| spl0_30
| ~ spl0_52 ),
inference(sat_conversion,[],[f5552]) ).
cnf(s600,plain,
( ~ spl0_1
| spl0_3 ),
inference(rat,[],[s87,s443]) ).
cnf(s607,plain,
( spl0_3
| spl0_5 ),
inference(rat,[],[s2,s443]) ).
cnf(s608,plain,
( spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35 ),
inference(rat,[],[s125,s334,s428]) ).
cnf(s609,plain,
~ spl0_54,
inference(rat,[],[s608,s154,s162,s417,s430,s433]) ).
cnf(s611,plain,
( ~ spl0_13
| ~ spl0_2 ),
inference(rat,[],[s384,s52,s355,s72,s63,s80,s45,s530,s35,s3,s92,s522,s607,s7,s8,s26,s609]) ).
cnf(s612,plain,
( ~ spl0_45
| spl0_47
| ~ spl0_26
| ~ spl0_2 ),
inference(rat,[],[s272,s269,s275,s166,s538,s611,s91,s118,s9,s374,s329,s53,s72,s45,s35,s3,s92,s522,s607,s7,s8,s26]) ).
cnf(s613,plain,
~ spl0_43,
inference(rat,[],[s311,s315]) ).
cnf(s614,plain,
( spl0_47
| spl0_18
| ~ spl0_2 ),
inference(rat,[],[s123,s612,s166,s374,s329,s131,s465,s611,s9,s91,s118,s63,s80,s530,s72,s45,s35,s3,s92,s522,s607,s7,s8,s26,s613]) ).
cnf(s615,plain,
~ spl0_38,
inference(rat,[],[s224,s229]) ).
cnf(s616,plain,
( spl0_18
| ~ spl0_2 ),
inference(rat,[],[s184,s298,s124,s321,s363,s201,s370,s329,s244,s614,s131,s72,s63,s80,s45,s530,s35,s465,s368,s538,s611,s91,s118,s3,s92,s522,s607,s7,s8,s9,s26,s615,s112,s613]) ).
cnf(s617,plain,
( spl0_26
| spl0_30
| ~ spl0_10
| spl0_29
| spl0_28 ),
inference(rat,[],[s125,s590,s588]) ).
cnf(s618,plain,
~ spl0_2,
inference(rat,[],[s617,s53,s616,s465,s611,s118,s530,s3,s80,s91,s92,s522,s607,s7,s8,s9,s63]) ).
cnf(s619,plain,
spl0_1,
inference(rat,[],[s1,s618]) ).
cnf(s620,plain,
~ spl0_26,
inference(rat,[],[s136,s619]) ).
cnf(s622,plain,
~ spl0_8,
inference(rat,[],[s101,s619]) ).
cnf(s623,plain,
spl0_3,
inference(rat,[],[s600,s619]) ).
cnf(s624,plain,
~ spl0_18,
inference(rat,[],[s54,s619]) ).
cnf(s626,plain,
~ spl0_20,
inference(rat,[],[s62,s624,s619]) ).
cnf(s627,plain,
~ spl0_28,
inference(rat,[],[s134,s619,s620]) ).
cnf(s629,plain,
~ spl0_7,
inference(rat,[],[s92,s623]) ).
cnf(s631,plain,
~ spl0_29,
inference(rat,[],[s80,s623]) ).
cnf(s632,plain,
~ spl0_17,
inference(rat,[],[s45,s623]) ).
cnf(s633,plain,
spl0_6,
inference(rat,[],[s105,s622,s619,s629]) ).
cnf(s635,plain,
~ spl0_30,
inference(rat,[],[s530,s633]) ).
cnf(s639,plain,
~ spl0_16,
inference(rat,[],[s35,s633]) ).
cnf(s642,plain,
$false,
inference(rat,[],[s384,s624,s632,s620,s627,s626,s609,s631,s26,s639,s635]) ).
fof(f5560,plain,
$false,
inference(avatar_sat_refutation,[],[s642]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP128-2.006 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n010.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 09:26:32 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.44/1.97 % (687924)Input is clausal, will run a generic CNF schedule.
% 6.44/1.97 % (688002)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=974925375:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.44/1.97 % (688001)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=2814003132:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.44/1.97 % (688007)dis-21_1_sil=8000:lcm=predicate:random_seed=2210532823: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)
% 6.44/1.97 % (688003)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4112547511:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.44/1.97 % (688006)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2510332727:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.44/1.97 % (688005)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1829543847:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.44/1.97 % (688004)lrs+10_1_sil=8000:sp=occurrence:random_seed=726571486:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.44/1.97 % (688004)Instruction limit reached!
% 6.44/1.97 % (688004)------------------------------
% 6.44/1.97 % (688004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.44/1.97 % (688004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.97 % (688004)CaDiCaL version: 2.1.3
% 6.44/1.97 % (688004)Termination reason: Instruction limit
% 6.44/1.97 % (688004)Termination phase: Saturation
% 6.44/1.97 % (688004)Time elapsed: 0.052 s
% 6.44/1.97 % (688004)Peak memory usage: 88 MB
% 6.44/1.97 % (688004)Instructions burned: 109 (million)
% 6.44/1.97 % (688005)Instruction limit reached!
% 6.44/1.97 % (688005)------------------------------
% 6.44/1.97 % (688005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.44/1.97 % (688005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.97 % (688005)CaDiCaL version: 2.1.3
% 6.44/1.97 % (688005)Termination reason: Instruction limit
% 6.44/1.97 % (688005)Termination phase: Saturation
% 6.44/1.97 % (688005)Time elapsed: 0.059 s
% 6.44/1.97 % (688005)Peak memory usage: 88 MB
% 6.44/1.97 % (688005)Instructions burned: 114 (million)
% 6.44/1.97 % (688007)Instruction limit reached!
% 6.44/1.97 % (688007)------------------------------
% 6.44/1.97 % (688007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.44/1.97 % (688007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.97 % (688007)CaDiCaL version: 2.1.3
% 6.44/1.97 % (688007)Termination reason: Instruction limit
% 6.44/1.97 % (688007)Termination phase: Saturation
% 6.44/1.97 % (688007)Time elapsed: 0.067 s
% 6.44/1.97 % (688007)Peak memory usage: 88 MB
% 6.44/1.97 % (688007)Instructions burned: 117 (million)
% 6.44/1.97 % (688006)Instruction limit reached!
% 6.44/1.97 % (688006)------------------------------
% 6.44/1.97 % (688006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.44/1.97 % (688006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.97 % (688006)CaDiCaL version: 2.1.3
% 6.44/1.97 % (688006)Termination reason: Instruction limit
% 6.44/1.97 % (688006)Termination phase: Saturation
% 6.44/1.97 % (688006)Time elapsed: 0.110 s
% 6.44/1.97 % (688006)Peak memory usage: 89 MB
% 6.44/1.97 % (688006)Instructions burned: 181 (million)
% 6.44/1.97 % (688015)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=2746210021:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 6.44/1.97 % (688016)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3445407077: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)
% 6.44/1.97 % (688016)Refutation not found, incomplete strategy
% 6.44/1.97 % (688016)------------------------------
% 6.44/1.97 % (688016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.44/1.97 % (688016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.97 % (688016)CaDiCaL version: 2.1.3
% 6.44/1.97 % (688016)Termination reason: Refutation not found, incomplete strategy
% 8.67/2.04 % (688016)Time elapsed: 0.002 s
% 8.67/2.04 % (688016)Peak memory usage: 87 MB
% 8.67/2.04 % (688016)Instructions burned: 2 (million)
% 8.67/2.04 % (688017)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4207259813:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 8.67/2.04 % (688018)lrs+10_64_to=lpo:sil=8000:random_seed=1324425440:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 8.67/2.04 % (688015)Instruction limit reached!
% 8.67/2.04 % (688015)------------------------------
% 8.67/2.04 % (688015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.04 % (688015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.04 % (688015)CaDiCaL version: 2.1.3
% 8.67/2.04 % (688015)Termination reason: Instruction limit
% 8.67/2.04 % (688015)Termination phase: Saturation
% 8.67/2.04 % (688015)Time elapsed: 0.080 s
% 8.67/2.04 % (688015)Peak memory usage: 89 MB
% 8.67/2.04 % (688015)Instructions burned: 144 (million)
% 8.67/2.04 % (688002)Refutation not found, incomplete strategy
% 8.67/2.04 % (688002)------------------------------
% 8.67/2.04 % (688002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.04 % (688002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.04 % (688002)CaDiCaL version: 2.1.3
% 8.67/2.04 % (688002)Termination reason: Refutation not found, incomplete strategy
% 8.67/2.04 % (688002)Time elapsed: 0.359 s
% 8.67/2.04 % (688002)Peak memory usage: 127 MB
% 8.67/2.04 % (688002)Instructions burned: 911 (million)
% 8.67/2.04 % (688018)Instruction limit reached!
% 8.67/2.04 % (688018)------------------------------
% 8.67/2.04 % (688018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.04 % (688018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.04 % (688018)CaDiCaL version: 2.1.3
% 8.67/2.04 % (688018)Termination reason: Instruction limit
% 8.67/2.04 % (688018)Termination phase: Saturation
% 8.67/2.04 % (688018)Time elapsed: 0.074 s
% 8.67/2.04 % (688018)Peak memory usage: 88 MB
% 8.67/2.04 % (688018)Instructions burned: 126 (million)
% 8.67/2.04 % (688017)Instruction limit reached!
% 8.67/2.04 % (688017)------------------------------
% 8.67/2.04 % (688017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.04 % (688017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.04 % (688017)CaDiCaL version: 2.1.3
% 8.67/2.04 % (688017)Termination reason: Instruction limit
% 8.67/2.04 % (688017)Termination phase: Saturation
% 8.67/2.04 % (688017)Time elapsed: 0.117 s
% 8.67/2.04 % (688017)Peak memory usage: 88 MB
% 8.67/2.04 % (688017)Instructions burned: 219 (million)
% 8.67/2.04 % (688023)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2236804379:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 8.67/2.04 % (688016)------------------------------
% 8.67/2.04 % (688016)------------------------------
% 8.67/2.04 % (688024)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1844288430:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 8.67/2.04 % (688002)------------------------------
% 8.67/2.04 % (688002)------------------------------
% 8.67/2.04 % (688025)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3968583394:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 8.67/2.04 % (688023)Instruction limit reached!
% 8.67/2.04 % (688023)------------------------------
% 8.67/2.04 % (688023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.04 % (688023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.04 % (688023)CaDiCaL version: 2.1.3
% 8.67/2.04 % (688023)Termination reason: Instruction limit
% 8.67/2.04 % (688023)Termination phase: Saturation
% 8.67/2.04 % (688023)Time elapsed: 0.073 s
% 8.67/2.04 % (688023)Peak memory usage: 87 MB
% 8.67/2.04 % (688023)Instructions burned: 196 (million)
% 8.67/2.04 % (688024)Instruction limit reached!
% 8.67/2.04 % (688024)------------------------------
% 8.67/2.04 % (688024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.04 % (688024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.04 % (688024)CaDiCaL version: 2.1.3
% 8.67/2.04 % (688024)Termination reason: Instruction limit
% 8.67/2.04 % (688024)Termination phase: Saturation
% 8.67/2.04 % (688024)Time elapsed: 0.078 s
% 8.67/2.04 % (688024)Peak memory usage: 89 MB
% 8.67/2.04 % (688024)Instructions burned: 157 (million)
% 8.67/2.04 % (688030)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2131937571:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 8.67/2.04 % (688027)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2043215896:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 8.67/2.04 % (688027)Refutation not found, incomplete strategy
% 8.67/2.04 % (688027)------------------------------
% 8.67/2.04 % (688027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.04 % (688027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.04 % (688027)CaDiCaL version: 2.1.3
% 8.67/2.04 % (688027)Termination reason: Refutation not found, incomplete strategy
% 8.67/2.04 % (688027)Time elapsed: 0.002 s
% 8.67/2.04 % (688027)Peak memory usage: 87 MB
% 8.67/2.04 % (688027)Instructions burned: 3 (million)
% 8.67/2.04 % (688030)Instruction limit reached!
% 8.67/2.04 % (688030)------------------------------
% 8.67/2.04 % (688030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.04 % (688030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.04 % (688030)CaDiCaL version: 2.1.3
% 8.67/2.04 % (688030)Termination reason: Instruction limit
% 8.67/2.04 % (688030)Termination phase: Saturation
% 8.67/2.04 % (688030)Time elapsed: 0.036 s
% 8.67/2.04 % (688030)Peak memory usage: 88 MB
% 8.67/2.04 % (688030)Instructions burned: 109 (million)
% 8.67/2.04 % (688031)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3712357769:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 8.67/2.04 % (688032)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1530270961:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 8.67/2.04 % (688035)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3188182492:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 8.67/2.04 % (688035)Instruction limit reached!
% 8.67/2.04 % (688035)------------------------------
% 8.67/2.04 % (688035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.04 % (688035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.04 % (688035)CaDiCaL version: 2.1.3
% 8.67/2.04 % (688035)Termination reason: Instruction limit
% 8.67/2.04 % (688035)Termination phase: Saturation
% 8.67/2.04 % (688035)Time elapsed: 0.028 s
% 8.67/2.04 % (688035)Peak memory usage: 88 MB
% 8.67/2.04 % (688035)Instructions burned: 139 (million)
% 8.67/2.04 % (688031)Instruction limit reached!
% 8.67/2.04 % (688031)------------------------------
% 8.67/2.04 % (688031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.04 % (688031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.04 % (688031)CaDiCaL version: 2.1.3
% 8.67/2.04 % (688031)Termination reason: Instruction limit
% 8.67/2.04 % (688031)Termination phase: Saturation
% 8.67/2.04 % (688031)Time elapsed: 0.121 s
% 8.67/2.04 % (688031)Peak memory usage: 88 MB
% 8.67/2.04 % (688031)Instructions burned: 242 (million)
% 8.67/2.04 % (688039)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=811422695:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 8.67/2.04 % (688027)------------------------------
% 8.67/2.04 % (688027)------------------------------
% 8.67/2.04 % (688040)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2256294322:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi)
% 8.67/2.04 % (688039)First to succeed.
% 8.67/2.04 % (688039)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-687924"
% 8.67/2.04 % (688042)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3471411406:i=264:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/264Mi)
% 8.67/2.04 % (688040)Instruction limit reached!
% 8.67/2.04 % (688040)------------------------------
% 8.67/2.04 % (688040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.04 % (688040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.04 % (688040)CaDiCaL version: 2.1.3
% 8.67/2.04 % (688040)Termination reason: Instruction limit
% 8.67/2.04 % (688040)Termination phase: Saturation
% 8.67/2.04 % (688040)Time elapsed: 0.114 s
% 8.67/2.04 % (688040)Peak memory usage: 89 MB
% 8.67/2.04 % (688040)Instructions burned: 191 (million)
% 8.67/2.04 % (688039)Refutation found. Thanks to Tanya!
% 8.67/2.04 % SZS status Unsatisfiable for theBenchmark
% 8.67/2.04 % SZS output start Proof for theBenchmark
% See solution above
% 8.98/2.24 % (688039)------------------------------
% 8.98/2.24 % (688039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.98/2.24 % (688039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.98/2.24 % (688039)CaDiCaL version: 2.1.3
% 8.98/2.24 % (688039)Termination reason: Refutation
% 8.98/2.24 % (688039)Time elapsed: 0.089 s
% 8.98/2.24 % (688039)Peak memory usage: 91 MB
% 8.98/2.24 % (688039)Instructions burned: 309 (million)
% 8.98/2.24 % (688039)------------------------------
% 8.98/2.24 % (688039)------------------------------
% 8.98/2.24 % (687924)Success in time 1.176 s
% 8.98/2.24 % Vampire exiting
%------------------------------------------------------------------------------