%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP128-3.005 : 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 : n003.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 14.51s 2.73s
% Output : Refutation 15.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 117
% Syntax : Number of formulae : 729 ( 82 unt; 62 def)
% Number of atoms : 2210 ( 0 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 2555 (1074 ~;1419 |; 0 &)
% ( 62 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 69 ( 68 usr; 63 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 63 ( 0 sgn 63 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
next(e_0,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_0_then_e_1) ).
fof(f2,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_then_e_2) ).
fof(f3,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_then_e_3) ).
fof(f4,axiom,
next(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_then_e_4) ).
fof(f5,axiom,
next(e_4,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_then_e_5) ).
fof(f6,axiom,
greater(e_1,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_greater_e_0) ).
fof(f7,axiom,
greater(e_2,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_greater_e_0) ).
fof(f8,axiom,
greater(e_3,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_0) ).
fof(f9,axiom,
greater(e_4,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_0) ).
fof(f11,axiom,
greater(e_2,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_greater_e_1) ).
fof(f12,axiom,
greater(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_1) ).
fof(f13,axiom,
greater(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_1) ).
fof(f14,axiom,
greater(e_5,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_greater_e_1) ).
fof(f15,axiom,
greater(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_2) ).
fof(f16,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_2) ).
fof(f17,axiom,
greater(e_5,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_greater_e_2) ).
fof(f18,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_3) ).
fof(f19,axiom,
greater(e_5,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_greater_e_3) ).
fof(f20,axiom,
greater(e_5,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_greater_e_4) ).
fof(f22,axiom,
! [X0] :
( ~ group_element(X0)
| cycle(X0,e_0)
| cycle(X0,e_1)
| cycle(X0,e_2)
| cycle(X0,e_3)
| cycle(X0,e_4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle2) ).
fof(f23,axiom,
cycle(e_5,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle3) ).
fof(f24,axiom,
! [X2,X3,X0,X1,X4] :
( ~ cycle(X2,X3)
| ~ cycle(X0,X1)
| ~ next(X0,X2)
| ~ greater(X1,e_0)
| ~ next(X3,X4)
| equalish(X1,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle4) ).
fof(f25,axiom,
! [X2,X3,X0,X1,X4] :
( ~ cycle(X3,X4)
| ~ cycle(X2,e_0)
| ~ cycle(X0,X1)
| ~ next(X2,X3)
| ~ greater(X2,X0)
| ~ greater(X1,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle5) ).
fof(f26,axiom,
! [X0,X1] :
( ~ product(X0,e_1,X1)
| ~ cycle(X0,e_0)
| ~ greater(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle6) ).
fof(f27,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,e_1,X2)
| ~ cycle(X0,X1)
| ~ greater(X1,e_0)
| ~ next(X0,X3)
| equalish(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle7) ).
fof(f28,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
fof(f29,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
fof(f30,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
fof(f31,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
fof(f32,axiom,
group_element(e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_5) ).
fof(f33,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f34,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f35,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f36,axiom,
~ equalish(e_1,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_5) ).
fof(f37,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
fof(f38,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f39,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f40,axiom,
~ equalish(e_2,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_5) ).
fof(f41,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
fof(f42,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
fof(f43,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f44,axiom,
~ equalish(e_3,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_5) ).
fof(f45,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
fof(f46,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
fof(f47,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
fof(f48,axiom,
~ equalish(e_4,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_5) ).
fof(f49,axiom,
~ equalish(e_5,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_1) ).
fof(f50,axiom,
~ equalish(e_5,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_2) ).
fof(f51,axiom,
~ equalish(e_5,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_3) ).
fof(f52,axiom,
~ equalish(e_5,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_4) ).
fof(f53,axiom,
! [X0,X1] :
( product(X0,X1,e_5)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ group_element(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
fof(f54,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function2) ).
fof(f55,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f56,axiom,
! [X2,X3,X0,X1] :
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_left_cancellation) ).
fof(f57,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ product(X2,X1,X3)
| ~ product(X0,X1,X2)
| product(X0,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3) ).
fof(f64,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_2)
| cycle(e_3,e_3)
| cycle(e_3,e_4) ),
inference(resolution,[],[f22,f30]) ).
fof(f68,definition,
( spl0_1
<=> cycle(e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f69,plain,
( ~ cycle(e_4,e_4)
| spl0_1 ),
inference(avatar_component_clause,[],[f68]) ).
fof(f72,definition,
( spl0_2
<=> cycle(e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f73,plain,
( ~ cycle(e_4,e_3)
| spl0_2 ),
inference(avatar_component_clause,[],[f72]) ).
fof(f74,plain,
( cycle(e_4,e_3)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f72]) ).
fof(f76,definition,
( spl0_3
<=> cycle(e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f77,plain,
( ~ cycle(e_4,e_2)
| spl0_3 ),
inference(avatar_component_clause,[],[f76]) ).
fof(f80,definition,
( spl0_4
<=> cycle(e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f81,plain,
( ~ cycle(e_4,e_1)
| spl0_4 ),
inference(avatar_component_clause,[],[f80]) ).
fof(f82,plain,
( cycle(e_4,e_1)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f80]) ).
fof(f84,definition,
( spl0_5
<=> cycle(e_4,e_0) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f86,plain,
( cycle(e_4,e_0)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f84]) ).
fof(f89,definition,
( spl0_6
<=> cycle(e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f91,plain,
( cycle(e_3,e_4)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f93,definition,
( spl0_7
<=> cycle(e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f97,definition,
( spl0_8
<=> cycle(e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f99,plain,
( cycle(e_3,e_2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f101,definition,
( spl0_9
<=> cycle(e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f105,definition,
( spl0_10
<=> cycle(e_3,e_0) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f107,plain,
( cycle(e_3,e_0)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f105]) ).
fof(f108,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f64,f105,f101,f97,f93,f89]) ).
fof(f110,definition,
( spl0_11
<=> cycle(e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f111,plain,
( ~ cycle(e_2,e_4)
| spl0_11 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f112,plain,
( cycle(e_2,e_4)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f114,definition,
( spl0_12
<=> cycle(e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f115,plain,
( ~ cycle(e_2,e_3)
| spl0_12 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f116,plain,
( cycle(e_2,e_3)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f118,definition,
( spl0_13
<=> cycle(e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f119,plain,
( ~ cycle(e_2,e_2)
| spl0_13 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f120,plain,
( cycle(e_2,e_2)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f122,definition,
( spl0_14
<=> cycle(e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f123,plain,
( ~ cycle(e_2,e_1)
| spl0_14 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f124,plain,
( cycle(e_2,e_1)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f126,definition,
( spl0_15
<=> cycle(e_2,e_0) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f128,plain,
( cycle(e_2,e_0)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f131,definition,
( spl0_16
<=> cycle(e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f132,plain,
( ~ cycle(e_1,e_4)
| spl0_16 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f133,plain,
( cycle(e_1,e_4)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f135,definition,
( spl0_17
<=> cycle(e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f136,plain,
( ~ cycle(e_1,e_3)
| spl0_17 ),
inference(avatar_component_clause,[],[f135]) ).
fof(f137,plain,
( cycle(e_1,e_3)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f135]) ).
fof(f139,definition,
( spl0_18
<=> cycle(e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f140,plain,
( ~ cycle(e_1,e_2)
| spl0_18 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f141,plain,
( cycle(e_1,e_2)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f143,definition,
( spl0_19
<=> cycle(e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f144,plain,
( ~ cycle(e_1,e_1)
| spl0_19 ),
inference(avatar_component_clause,[],[f143]) ).
fof(f145,plain,
( cycle(e_1,e_1)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f143]) ).
fof(f147,definition,
( spl0_20
<=> cycle(e_1,e_0) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f149,plain,
( cycle(e_1,e_0)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f147]) ).
fof(f151,plain,
~ cycle(e_4,e_2),
inference(unit_resulting_resolution,[],[f24,f5,f23,f1,f37,f7]) ).
fof(f152,plain,
~ cycle(e_4,e_3),
inference(unit_resulting_resolution,[],[f24,f5,f23,f1,f41,f8]) ).
fof(f153,plain,
~ cycle(e_4,e_4),
inference(unit_resulting_resolution,[],[f24,f5,f23,f1,f45,f9]) ).
fof(f156,plain,
~ spl0_3,
inference(avatar_split_clause,[],[f151,f76]) ).
fof(f157,plain,
( $false
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f152,f74]) ).
fof(f158,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f157]) ).
fof(f159,plain,
~ spl0_1,
inference(avatar_split_clause,[],[f153,f68]) ).
fof(f161,plain,
! [X2,X0,X1] :
( ~ product(X2,X0,e_5)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ group_element(X1)
| ~ group_element(X0)
| equalish(X2,X1) ),
inference(resolution,[],[f53,f56]) ).
fof(f162,plain,
! [X2,X0,X1] :
( ~ product(X1,X2,e_5)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ group_element(X1)
| ~ group_element(X0)
| equalish(X2,X0) ),
inference(resolution,[],[f53,f55]) ).
fof(f164,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)
| ~ group_element(X1)
| ~ group_element(X0)
| product(X2,X1,e_5) ),
inference(resolution,[],[f53,f57]) ).
fof(f166,plain,
! [X0] :
( ~ 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)
| ~ group_element(X0)
| ~ cycle(X0,e_0)
| ~ greater(e_5,X0) ),
inference(resolution,[],[f53,f26]) ).
fof(f167,plain,
! [X0] :
( product(X0,e_1,e_4)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_1)
| ~ group_element(X0)
| ~ cycle(X0,e_0)
| ~ greater(e_5,X0) ),
inference(forward_subsumption_resolution,[],[f166,f28]) ).
fof(f169,plain,
! [X0,X1] :
( product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| ~ group_element(e_5)
| ~ group_element(X0)
| product(X1,e_5,e_5)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ group_element(X1) ),
inference(resolution,[],[f164,f53]) ).
fof(f170,plain,
! [X0,X1] :
( product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| ~ group_element(e_5)
| ~ group_element(X0)
| product(X1,e_5,e_5)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ group_element(X1) ),
inference(duplicate_literal_removal,[],[f169]) ).
fof(f171,plain,
! [X0,X1] :
( product(e_5,X0,e_4)
| product(X1,e_5,e_5)
| product(X1,X0,e_4)
| product(e_5,X0,e_3)
| ~ group_element(X0)
| product(e_5,X0,e_2)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(e_5,X0,e_1)
| ~ group_element(X1) ),
inference(forward_subsumption_resolution,[],[f170,f32]) ).
fof(f177,plain,
( ~ cycle(e_1,e_1)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f25,f6,f13,f23,f5,f86]) ).
fof(f178,plain,
( ~ cycle(e_1,e_2)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f25,f7,f13,f23,f5,f86]) ).
fof(f179,plain,
( ~ cycle(e_1,e_3)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f25,f8,f13,f23,f5,f86]) ).
fof(f180,plain,
( ~ cycle(e_1,e_4)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f25,f9,f13,f23,f5,f86]) ).
fof(f182,plain,
( ~ cycle(e_2,e_1)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f25,f6,f16,f23,f5,f86]) ).
fof(f183,plain,
( ~ cycle(e_2,e_2)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f25,f7,f16,f23,f5,f86]) ).
fof(f184,plain,
( ~ cycle(e_2,e_3)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f25,f8,f16,f23,f5,f86]) ).
fof(f185,plain,
( ~ cycle(e_2,e_4)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f25,f9,f16,f23,f5,f86]) ).
fof(f187,plain,
( ~ cycle(e_3,e_1)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f25,f6,f18,f23,f5,f86]) ).
fof(f188,plain,
( ~ cycle(e_3,e_2)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f25,f7,f18,f23,f5,f86]) ).
fof(f189,plain,
( ~ cycle(e_3,e_3)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f25,f8,f18,f23,f5,f86]) ).
fof(f197,plain,
( ~ cycle(e_3,e_4)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f24,f45,f1,f9,f4,f86]) ).
fof(f202,plain,
( ~ spl0_19
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f177,f84,f143]) ).
fof(f203,plain,
( ~ spl0_18
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f178,f84,f139]) ).
fof(f204,plain,
( ~ spl0_17
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f179,f84,f135]) ).
fof(f207,plain,
( ~ spl0_14
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f182,f84,f122]) ).
fof(f208,plain,
( ~ spl0_13
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f183,f84,f118]) ).
fof(f209,plain,
( ~ spl0_12
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f184,f84,f114]) ).
fof(f212,plain,
( ~ spl0_9
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f187,f84,f101]) ).
fof(f213,plain,
( ~ spl0_8
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f188,f84,f97]) ).
fof(f214,plain,
( ~ spl0_7
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f189,f84,f93]) ).
fof(f240,plain,
( ~ cycle(e_3,e_1)
| ~ spl0_4 ),
inference(unit_resulting_resolution,[],[f24,f33,f2,f6,f4,f82]) ).
fof(f241,plain,
( ~ cycle(e_3,e_3)
| ~ spl0_4 ),
inference(unit_resulting_resolution,[],[f24,f42,f2,f8,f4,f82]) ).
fof(f242,plain,
( ~ cycle(e_3,e_4)
| ~ spl0_4 ),
inference(unit_resulting_resolution,[],[f24,f46,f2,f9,f4,f82]) ).
fof(f252,plain,
( ~ spl0_9
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f240,f80,f101]) ).
fof(f253,plain,
( ~ spl0_7
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f241,f80,f93]) ).
fof(f254,plain,
( $false
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f242,f91]) ).
fof(f255,plain,
( ~ spl0_4
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[],[f254]) ).
fof(f256,plain,
( ~ spl0_6
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f197,f84,f89]) ).
fof(f257,plain,
( ~ spl0_11
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f185,f84,f110]) ).
fof(f258,plain,
( ~ spl0_16
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f180,f84,f131]) ).
fof(f259,plain,
( cycle(e_4,e_0)
| spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(unit_resulting_resolution,[],[f22,f31,f69,f73,f77,f81]) ).
fof(f280,plain,
( ~ product(e_4,e_1,e_5)
| ~ spl0_5 ),
inference(unit_resulting_resolution,[],[f26,f20,f86]) ).
fof(f306,plain,
( ~ product(e_3,e_1,e_4)
| ~ spl0_10 ),
inference(unit_resulting_resolution,[],[f26,f18,f107]) ).
fof(f315,plain,
( ! [X2,X0,X1] :
( ~ cycle(X1,X2)
| ~ cycle(X0,e_0)
| ~ next(X0,e_3)
| ~ greater(X0,X1)
| ~ greater(X2,e_0) )
| ~ spl0_10 ),
inference(resolution,[],[f107,f25]) ).
fof(f318,plain,
( cycle(e_2,e_0)
| spl0_11
| spl0_12
| spl0_13
| spl0_14 ),
inference(unit_resulting_resolution,[],[f22,f29,f111,f115,f119,f123]) ).
fof(f329,plain,
( ~ product(e_2,e_1,e_3)
| ~ spl0_15 ),
inference(unit_resulting_resolution,[],[f26,f15,f128]) ).
fof(f330,plain,
( ~ product(e_2,e_1,e_4)
| ~ spl0_15 ),
inference(unit_resulting_resolution,[],[f26,f16,f128]) ).
fof(f331,plain,
( ~ product(e_2,e_1,e_5)
| ~ spl0_15 ),
inference(unit_resulting_resolution,[],[f26,f17,f128]) ).
fof(f343,plain,
( cycle(e_1,e_0)
| spl0_16
| spl0_17
| spl0_18
| spl0_19 ),
inference(unit_resulting_resolution,[],[f22,f28,f132,f136,f140,f144]) ).
fof(f349,plain,
( ~ product(e_1,e_1,e_2)
| ~ spl0_20 ),
inference(unit_resulting_resolution,[],[f26,f11,f149]) ).
fof(f350,plain,
( ~ product(e_1,e_1,e_3)
| ~ spl0_20 ),
inference(unit_resulting_resolution,[],[f26,f12,f149]) ).
fof(f351,plain,
( ~ product(e_1,e_1,e_4)
| ~ spl0_20 ),
inference(unit_resulting_resolution,[],[f26,f13,f149]) ).
fof(f413,definition,
( spl0_21
<=> product(e_4,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f414,plain,
( ~ product(e_4,e_1,e_4)
| spl0_21 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f415,plain,
( product(e_4,e_1,e_4)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f417,definition,
( spl0_22
<=> product(e_4,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f418,plain,
( ~ product(e_4,e_1,e_3)
| spl0_22 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f419,plain,
( product(e_4,e_1,e_3)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f421,definition,
( spl0_23
<=> product(e_4,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f422,plain,
( ~ product(e_4,e_1,e_2)
| spl0_23 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f423,plain,
( product(e_4,e_1,e_2)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f425,definition,
( spl0_24
<=> product(e_4,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f426,plain,
( ~ product(e_4,e_1,e_1)
| spl0_24 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f427,plain,
( product(e_4,e_1,e_1)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f448,definition,
( spl0_28
<=> product(e_5,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f449,plain,
( ~ product(e_5,e_4,e_2)
| spl0_28 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f450,plain,
( product(e_5,e_4,e_2)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f452,definition,
( spl0_29
<=> product(e_5,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f453,plain,
( ~ product(e_5,e_4,e_1)
| spl0_29 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f454,plain,
( product(e_5,e_4,e_1)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f550,definition,
( spl0_37
<=> product(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f551,plain,
( ~ product(e_3,e_1,e_3)
| spl0_37 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f552,plain,
( product(e_3,e_1,e_3)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f554,definition,
( spl0_38
<=> product(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f555,plain,
( ~ product(e_3,e_1,e_2)
| spl0_38 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f556,plain,
( product(e_3,e_1,e_2)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f558,definition,
( spl0_39
<=> product(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f559,plain,
( ~ product(e_3,e_1,e_1)
| spl0_39 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f560,plain,
( product(e_3,e_1,e_1)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f601,definition,
( spl0_42
<=> product(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f602,plain,
( ~ product(e_2,e_1,e_2)
| spl0_42 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f603,plain,
( product(e_2,e_1,e_2)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f605,definition,
( spl0_43
<=> product(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f606,plain,
( ~ product(e_2,e_1,e_1)
| spl0_43 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f607,plain,
( product(e_2,e_1,e_1)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f756,definition,
( spl0_58
<=> product(e_5,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f757,plain,
( ~ product(e_5,e_1,e_2)
| spl0_58 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f758,plain,
( product(e_5,e_1,e_2)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f766,definition,
( spl0_61
<=> product(e_5,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f767,plain,
( ~ product(e_5,e_1,e_3)
| spl0_61 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f768,plain,
( product(e_5,e_1,e_3)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f786,definition,
( spl0_65
<=> product(e_5,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f787,plain,
( ~ product(e_5,e_1,e_1)
| spl0_65 ),
inference(avatar_component_clause,[],[f786]) ).
fof(f788,plain,
( product(e_5,e_1,e_1)
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f786]) ).
fof(f824,plain,
( ~ product(e_3,e_1,e_3)
| ~ spl0_22 ),
inference(unit_resulting_resolution,[],[f56,f47,f419]) ).
fof(f853,plain,
( ~ spl0_37
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f824,f417,f550]) ).
fof(f862,definition,
( spl0_68
<=> product(e_4,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f863,plain,
( ~ product(e_4,e_3,e_4)
| spl0_68 ),
inference(avatar_component_clause,[],[f862]) ).
fof(f864,plain,
( product(e_4,e_3,e_4)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f862]) ).
fof(f869,definition,
( spl0_69
<=> product(e_4,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f870,plain,
( ~ product(e_4,e_3,e_5)
| spl0_69 ),
inference(avatar_component_clause,[],[f869]) ).
fof(f902,plain,
( ~ product(e_2,e_1,e_2)
| ~ spl0_23 ),
inference(unit_resulting_resolution,[],[f56,f46,f423]) ).
fof(f929,plain,
( ~ spl0_42
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f902,f421,f601]) ).
fof(f942,definition,
( spl0_71
<=> product(e_4,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f944,plain,
( product(e_4,e_2,e_4)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f942]) ).
fof(f949,definition,
( spl0_72
<=> product(e_4,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f950,plain,
( ~ product(e_4,e_2,e_5)
| spl0_72 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f982,plain,
! [X0] :
( product(e_5,X0,e_4)
| product(e_5,e_5,e_5)
| product(e_5,X0,e_3)
| ~ group_element(X0)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_1)
| ~ group_element(e_5) ),
inference(factoring,[],[f171]) ).
fof(f983,plain,
! [X0] :
( product(e_5,X0,e_4)
| product(e_5,e_5,e_5)
| product(e_5,X0,e_3)
| ~ group_element(X0)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| ~ group_element(e_5) ),
inference(duplicate_literal_removal,[],[f982]) ).
fof(f991,plain,
! [X0] :
( product(e_5,X0,e_4)
| product(e_5,e_5,e_5)
| product(e_5,X0,e_3)
| ~ group_element(X0)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1) ),
inference(forward_subsumption_resolution,[],[f983,f32]) ).
fof(f998,definition,
( spl0_73
<=> product(e_5,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f999,plain,
( ~ product(e_5,e_5,e_5)
| spl0_73 ),
inference(avatar_component_clause,[],[f998]) ).
fof(f1000,plain,
( product(e_5,e_5,e_5)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f998]) ).
fof(f1002,definition,
( spl0_74
<=> ! [X0] :
( product(e_5,X0,e_4)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| ~ group_element(X0)
| product(e_5,X0,e_3) ) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f1003,plain,
( ! [X0] :
( product(e_5,X0,e_4)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| ~ group_element(X0)
| product(e_5,X0,e_3) )
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f1002]) ).
fof(f1004,plain,
( spl0_73
| spl0_74 ),
inference(avatar_split_clause,[],[f991,f1002,f998]) ).
fof(f1008,definition,
( spl0_75
<=> product(e_5,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f1009,plain,
( ~ product(e_5,e_4,e_5)
| spl0_75 ),
inference(avatar_component_clause,[],[f1008]) ).
fof(f1010,plain,
( product(e_5,e_4,e_5)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f1008]) ).
fof(f1029,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)
| product(e_4,e_1,e_4)
| ~ group_element(e_4)
| ~ spl0_5 ),
inference(resolution,[],[f280,f53]) ).
fof(f1031,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_1)
| ~ group_element(e_3)
| ~ cycle(e_3,e_0)
| ~ greater(e_5,e_3)
| ~ spl0_10 ),
inference(resolution,[],[f306,f167]) ).
fof(f1032,plain,
( product(e_3,e_1,e_3)
| product(e_3,e_1,e_1)
| ~ group_element(e_3)
| ~ cycle(e_3,e_0)
| ~ greater(e_5,e_3)
| ~ spl0_10
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f1031,f555]) ).
fof(f1034,plain,
( product(e_3,e_1,e_3)
| ~ group_element(e_3)
| ~ cycle(e_3,e_0)
| ~ greater(e_5,e_3)
| ~ spl0_10
| spl0_38
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f1032,f559]) ).
fof(f1036,plain,
( product(e_3,e_1,e_3)
| ~ cycle(e_3,e_0)
| ~ greater(e_5,e_3)
| ~ spl0_10
| spl0_38
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f1034,f30]) ).
fof(f1038,plain,
( product(e_3,e_1,e_3)
| ~ greater(e_5,e_3)
| ~ spl0_10
| spl0_38
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f1036,f107]) ).
fof(f1040,plain,
( product(e_3,e_1,e_3)
| ~ spl0_10
| spl0_38
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f1038,f19]) ).
fof(f1041,plain,
( spl0_37
| ~ spl0_10
| spl0_38
| spl0_39 ),
inference(avatar_split_clause,[],[f1040,f558,f554,f105,f550]) ).
fof(f1048,plain,
( product(e_1,e_1,e_1)
| ~ spl0_20 ),
inference(unit_resulting_resolution,[],[f167,f28,f14,f149,f350,f349,f351]) ).
fof(f1063,plain,
( ~ product(e_5,e_2,e_5)
| ~ spl0_73 ),
inference(unit_resulting_resolution,[],[f55,f50,f1000]) ).
fof(f1065,plain,
( ~ product(e_5,e_4,e_5)
| ~ spl0_73 ),
inference(unit_resulting_resolution,[],[f55,f52,f1000]) ).
fof(f1096,plain,
( $false
| ~ spl0_73
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f1065,f1010]) ).
fof(f1097,plain,
( ~ spl0_73
| ~ spl0_75 ),
inference(avatar_contradiction_clause,[],[f1096]) ).
fof(f1152,plain,
( product(e_5,e_5,e_5)
| ~ spl0_75 ),
inference(unit_resulting_resolution,[],[f57,f1010,f1010]) ).
fof(f1175,plain,
( $false
| spl0_73
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f1152,f999]) ).
fof(f1176,plain,
( spl0_73
| ~ spl0_75 ),
inference(avatar_contradiction_clause,[],[f1175]) ).
fof(f1217,plain,
( ~ cycle(e_1,e_1)
| ~ spl0_10
| ~ spl0_15 ),
inference(unit_resulting_resolution,[],[f315,f6,f11,f3,f128]) ).
fof(f1261,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_39 ),
inference(unit_resulting_resolution,[],[f56,f34,f560]) ).
fof(f1292,plain,
( $false
| ~ spl0_20
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1261,f1048]) ).
fof(f1293,plain,
( ~ spl0_20
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f1292]) ).
fof(f1487,plain,
( ~ product(e_2,e_1,e_2)
| ~ spl0_38 ),
inference(unit_resulting_resolution,[],[f56,f38,f556]) ).
fof(f1489,plain,
( ~ product(e_5,e_1,e_2)
| ~ spl0_38 ),
inference(unit_resulting_resolution,[],[f56,f51,f556]) ).
fof(f1565,plain,
( product(e_2,e_1,e_1)
| ~ spl0_15
| spl0_42 ),
inference(unit_resulting_resolution,[],[f53,f29,f28,f330,f329,f331,f602]) ).
fof(f1587,plain,
( ~ cycle(e_2,e_1)
| ~ spl0_43 ),
inference(unit_resulting_resolution,[],[f27,f34,f3,f6,f607]) ).
fof(f1614,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_43 ),
inference(unit_resulting_resolution,[],[f56,f37,f607]) ).
fof(f1619,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_43 ),
inference(unit_resulting_resolution,[],[f56,f33,f607]) ).
fof(f1625,plain,
( ~ product(e_1,e_1,e_3)
| ~ spl0_15
| ~ spl0_43 ),
inference(unit_resulting_resolution,[],[f57,f329,f607]) ).
fof(f1652,plain,
( $false
| ~ spl0_20
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f1619,f1048]) ).
fof(f1653,plain,
( ~ spl0_20
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f1652]) ).
fof(f1729,plain,
( $false
| ~ spl0_38
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f1487,f603]) ).
fof(f1730,plain,
( ~ spl0_38
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f1729]) ).
fof(f1791,plain,
( ~ product(e_4,e_4,e_4)
| ~ spl0_21 ),
inference(unit_resulting_resolution,[],[f55,f35,f415]) ).
fof(f1810,plain,
( product(e_4,e_4,e_4)
| ~ spl0_21 ),
inference(unit_resulting_resolution,[],[f57,f415,f415]) ).
fof(f1832,plain,
( $false
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1810,f1791]) ).
fof(f1833,plain,
~ spl0_21,
inference(avatar_contradiction_clause,[],[f1832]) ).
fof(f1842,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4)
| ~ group_element(e_4)
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f1029,f28]) ).
fof(f1843,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4)
| ~ group_element(e_4)
| ~ spl0_5
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1842,f426]) ).
fof(f1844,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_4)
| ~ group_element(e_4)
| ~ spl0_5
| spl0_23
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1843,f422]) ).
fof(f1845,plain,
( product(e_4,e_1,e_4)
| ~ group_element(e_4)
| ~ spl0_5
| spl0_22
| spl0_23
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1844,f418]) ).
fof(f1846,plain,
( ~ group_element(e_4)
| ~ spl0_5
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1845,f414]) ).
fof(f1847,plain,
( $false
| ~ spl0_5
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1846,f31]) ).
fof(f1848,plain,
( ~ spl0_5
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(avatar_contradiction_clause,[],[f1847]) ).
fof(f1884,plain,
( ~ cycle(e_1,e_2)
| ~ spl0_4
| ~ spl0_10 ),
inference(unit_resulting_resolution,[],[f25,f11,f12,f4,f107,f82]) ).
fof(f1885,plain,
( ~ cycle(e_1,e_3)
| ~ spl0_4
| ~ spl0_10 ),
inference(unit_resulting_resolution,[],[f25,f12,f12,f4,f107,f82]) ).
fof(f1886,plain,
( ~ cycle(e_1,e_4)
| ~ spl0_4
| ~ spl0_10 ),
inference(unit_resulting_resolution,[],[f25,f13,f12,f4,f107,f82]) ).
fof(f1889,plain,
( ~ cycle(e_2,e_2)
| ~ spl0_4
| ~ spl0_10 ),
inference(unit_resulting_resolution,[],[f25,f11,f15,f4,f107,f82]) ).
fof(f1890,plain,
( ~ cycle(e_2,e_3)
| ~ spl0_4
| ~ spl0_10 ),
inference(unit_resulting_resolution,[],[f25,f12,f15,f4,f107,f82]) ).
fof(f1891,plain,
( ~ cycle(e_2,e_4)
| ~ spl0_4
| ~ spl0_10 ),
inference(unit_resulting_resolution,[],[f25,f13,f15,f4,f107,f82]) ).
fof(f1894,plain,
( ~ product(e_4,e_1,e_1)
| ~ spl0_4 ),
inference(unit_resulting_resolution,[],[f27,f36,f5,f6,f82]) ).
fof(f1967,plain,
( ~ product(e_4,e_2,e_5)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(unit_resulting_resolution,[],[f162,f37,f28,f31,f414,f422,f426,f418]) ).
fof(f1968,plain,
( ~ product(e_4,e_3,e_5)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(unit_resulting_resolution,[],[f162,f41,f28,f31,f414,f422,f426,f418]) ).
fof(f1970,plain,
( ~ product(e_4,e_5,e_5)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(unit_resulting_resolution,[],[f162,f49,f28,f31,f414,f422,f426,f418]) ).
fof(f1971,plain,
( ~ product(e_1,e_1,e_5)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(unit_resulting_resolution,[],[f161,f35,f28,f31,f414,f422,f426,f418]) ).
fof(f1972,plain,
( ~ product(e_2,e_1,e_5)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(unit_resulting_resolution,[],[f161,f39,f28,f31,f414,f422,f426,f418]) ).
fof(f1974,plain,
( ~ product(e_5,e_1,e_5)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(unit_resulting_resolution,[],[f161,f52,f28,f31,f414,f422,f426,f418]) ).
fof(f1975,plain,
( ~ product(e_5,e_1,e_4)
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_75 ),
inference(unit_resulting_resolution,[],[f164,f31,f28,f1009,f414,f422,f426,f418]) ).
fof(f1976,plain,
( product(e_4,e_1,e_5)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(unit_resulting_resolution,[],[f53,f31,f28,f414,f422,f426,f418]) ).
fof(f1987,plain,
( ~ spl0_72
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(avatar_split_clause,[],[f1967,f425,f421,f417,f413,f949]) ).
fof(f1988,plain,
( ~ spl0_69
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(avatar_split_clause,[],[f1968,f425,f421,f417,f413,f869]) ).
fof(f1994,definition,
( spl0_94
<=> product(e_4,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f1995,plain,
( ~ product(e_4,e_3,e_3)
| spl0_94 ),
inference(avatar_component_clause,[],[f1994]) ).
fof(f1996,plain,
( product(e_4,e_3,e_3)
| ~ spl0_94 ),
inference(avatar_component_clause,[],[f1994]) ).
fof(f1998,definition,
( spl0_95
<=> product(e_4,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f1999,plain,
( ~ product(e_4,e_3,e_2)
| spl0_95 ),
inference(avatar_component_clause,[],[f1998]) ).
fof(f2000,plain,
( product(e_4,e_3,e_2)
| ~ spl0_95 ),
inference(avatar_component_clause,[],[f1998]) ).
fof(f2002,definition,
( spl0_96
<=> product(e_4,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f2003,plain,
( ~ product(e_4,e_3,e_1)
| spl0_96 ),
inference(avatar_component_clause,[],[f2002]) ).
fof(f2004,plain,
( product(e_4,e_3,e_1)
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f2002]) ).
fof(f2006,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)
| product(e_4,e_2,e_4)
| ~ group_element(e_4)
| spl0_72 ),
inference(resolution,[],[f950,f53]) ).
fof(f2007,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_4)
| ~ group_element(e_4)
| spl0_72 ),
inference(forward_subsumption_resolution,[],[f2006,f29]) ).
fof(f2008,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_4)
| spl0_72 ),
inference(forward_subsumption_resolution,[],[f2007,f31]) ).
fof(f2010,definition,
( spl0_97
<=> product(e_4,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f2012,plain,
( product(e_4,e_2,e_3)
| ~ spl0_97 ),
inference(avatar_component_clause,[],[f2010]) ).
fof(f2014,definition,
( spl0_98
<=> product(e_4,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f2016,plain,
( product(e_4,e_2,e_2)
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f2014]) ).
fof(f2018,definition,
( spl0_99
<=> product(e_4,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f2020,plain,
( product(e_4,e_2,e_1)
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f2018]) ).
fof(f2021,plain,
( spl0_71
| spl0_97
| spl0_98
| spl0_99
| spl0_72 ),
inference(avatar_split_clause,[],[f2008,f949,f2018,f2014,f2010,f942]) ).
fof(f2033,definition,
( spl0_100
<=> product(e_4,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f2034,plain,
( ~ product(e_4,e_4,e_4)
| spl0_100 ),
inference(avatar_component_clause,[],[f2033]) ).
fof(f2035,plain,
( product(e_4,e_4,e_4)
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f2033]) ).
fof(f2050,plain,
( product(e_5,e_1,e_4)
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_58
| spl0_61
| spl0_65 ),
inference(unit_resulting_resolution,[],[f171,f31,f28,f787,f418,f422,f426,f757,f767,f414,f1970]) ).
fof(f2055,plain,
( $false
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_58
| spl0_61
| spl0_65
| spl0_75 ),
inference(forward_subsumption_resolution,[],[f2050,f1975]) ).
fof(f2056,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_58
| spl0_61
| spl0_65
| spl0_75 ),
inference(avatar_contradiction_clause,[],[f2055]) ).
fof(f2063,definition,
( spl0_105
<=> product(e_4,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f2067,definition,
( spl0_106
<=> product(e_4,e_5,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f2069,plain,
( product(e_4,e_5,e_2)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f2067]) ).
fof(f2086,plain,
( ~ product(e_5,e_2,e_3)
| ~ spl0_61 ),
inference(unit_resulting_resolution,[],[f55,f33,f768]) ).
fof(f2097,plain,
( ~ product(e_2,e_1,e_3)
| ~ spl0_61 ),
inference(unit_resulting_resolution,[],[f56,f50,f768]) ).
fof(f2098,plain,
( ~ product(e_3,e_1,e_3)
| ~ spl0_61 ),
inference(unit_resulting_resolution,[],[f56,f51,f768]) ).
fof(f2120,plain,
( $false
| ~ spl0_37
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f2098,f552]) ).
fof(f2121,plain,
( ~ spl0_37
| ~ spl0_61 ),
inference(avatar_contradiction_clause,[],[f2120]) ).
fof(f2150,plain,
( ~ product(e_1,e_1,e_2)
| ~ spl0_58 ),
inference(unit_resulting_resolution,[],[f56,f36,f758]) ).
fof(f2151,plain,
( ~ product(e_2,e_1,e_2)
| ~ spl0_58 ),
inference(unit_resulting_resolution,[],[f56,f40,f758]) ).
fof(f2171,plain,
( $false
| ~ spl0_42
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f2151,f603]) ).
fof(f2172,plain,
( ~ spl0_42
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f2171]) ).
fof(f2275,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_65 ),
inference(unit_resulting_resolution,[],[f56,f49,f788]) ).
fof(f2280,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_65 ),
inference(unit_resulting_resolution,[],[f56,f36,f788]) ).
fof(f2285,plain,
( ~ product(e_1,e_1,e_2)
| spl0_58
| ~ spl0_65 ),
inference(unit_resulting_resolution,[],[f57,f757,f788]) ).
fof(f2286,plain,
( ~ product(e_1,e_1,e_3)
| spl0_61
| ~ spl0_65 ),
inference(unit_resulting_resolution,[],[f57,f767,f788]) ).
fof(f2294,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)
| ~ group_element(e_1)
| ~ group_element(e_1)
| product(e_5,e_1,e_5)
| ~ spl0_65 ),
inference(resolution,[],[f788,f164]) ).
fof(f2299,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)
| ~ group_element(e_1)
| product(e_5,e_1,e_5)
| ~ spl0_65 ),
inference(duplicate_literal_removal,[],[f2294]) ).
fof(f2301,plain,
( $false
| ~ spl0_20
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f2275,f1048]) ).
fof(f2302,plain,
( ~ spl0_20
| ~ spl0_65 ),
inference(avatar_contradiction_clause,[],[f2301]) ).
fof(f2303,plain,
( $false
| ~ spl0_20
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f2280,f1048]) ).
fof(f2304,plain,
( ~ spl0_20
| ~ spl0_65 ),
inference(avatar_contradiction_clause,[],[f2303]) ).
fof(f2374,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_5,e_1,e_5)
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f2299,f28]) ).
fof(f2377,plain,
( $false
| ~ spl0_10
| ~ spl0_15
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1217,f145]) ).
fof(f2378,plain,
( ~ spl0_10
| ~ spl0_15
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2377]) ).
fof(f2380,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_4)
| product(e_5,e_1,e_5)
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f2374,f2275]) ).
fof(f2381,plain,
( product(e_1,e_1,e_3)
| product(e_1,e_1,e_4)
| product(e_5,e_1,e_5)
| spl0_58
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f2380,f2285]) ).
fof(f2382,plain,
( product(e_1,e_1,e_4)
| product(e_5,e_1,e_5)
| spl0_58
| spl0_61
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f2381,f2286]) ).
fof(f2383,plain,
( product(e_1,e_1,e_4)
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_58
| spl0_61
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f2382,f1974]) ).
fof(f2392,plain,
( $false
| ~ spl0_4
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1886,f133]) ).
fof(f2393,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2392]) ).
fof(f2402,plain,
( $false
| ~ spl0_4
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1885,f137]) ).
fof(f2403,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2402]) ).
fof(f2412,plain,
( $false
| ~ spl0_4
| ~ spl0_10
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1884,f141]) ).
fof(f2413,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2412]) ).
fof(f2418,plain,
( $false
| ~ spl0_4
| ~ spl0_10
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f1890,f116]) ).
fof(f2419,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f2418]) ).
fof(f2424,plain,
( $false
| ~ spl0_4
| ~ spl0_10
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f1889,f120]) ).
fof(f2425,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f2424]) ).
fof(f2449,plain,
( ~ cycle(e_1,e_1)
| ~ spl0_14 ),
inference(unit_resulting_resolution,[],[f24,f33,f2,f6,f2,f124]) ).
fof(f2450,plain,
( ~ cycle(e_1,e_3)
| ~ spl0_14 ),
inference(unit_resulting_resolution,[],[f24,f42,f2,f8,f2,f124]) ).
fof(f2461,plain,
( ~ product(e_2,e_1,e_2)
| ~ spl0_14 ),
inference(unit_resulting_resolution,[],[f27,f38,f3,f6,f124]) ).
fof(f2488,plain,
( $false
| ~ spl0_14
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f2461,f603]) ).
fof(f2489,plain,
( ~ spl0_14
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f2488]) ).
fof(f2496,plain,
( $false
| ~ spl0_4
| ~ spl0_10
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1891,f112]) ).
fof(f2497,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f2496]) ).
fof(f2498,plain,
( ~ spl0_19
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f2449,f122,f143]) ).
fof(f2499,plain,
( spl0_20
| spl0_16
| spl0_17
| spl0_18
| spl0_19 ),
inference(avatar_split_clause,[],[f343,f143,f139,f135,f131,f147]) ).
fof(f2537,plain,
( ~ product(e_2,e_1,e_4)
| ~ spl0_14 ),
inference(unit_resulting_resolution,[],[f27,f47,f3,f6,f124]) ).
fof(f2607,definition,
( spl0_128
<=> product(e_5,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f2608,plain,
( ~ product(e_5,e_2,e_4)
| spl0_128 ),
inference(avatar_component_clause,[],[f2607]) ).
fof(f2611,definition,
( spl0_129
<=> product(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f2612,plain,
( ~ product(e_2,e_1,e_3)
| spl0_129 ),
inference(avatar_component_clause,[],[f2611]) ).
fof(f2613,plain,
( product(e_2,e_1,e_3)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f2611]) ).
fof(f2617,definition,
( spl0_130
<=> product(e_5,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f2618,plain,
( ~ product(e_5,e_2,e_5)
| spl0_130 ),
inference(avatar_component_clause,[],[f2617]) ).
fof(f2622,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)
| ~ group_element(e_1)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(resolution,[],[f1971,f53]) ).
fof(f2623,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)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(duplicate_literal_removal,[],[f2622]) ).
fof(f2624,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)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f2623,f28]) ).
fof(f2625,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_4)
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f2624,f2150]) ).
fof(f2627,definition,
( spl0_131
<=> product(e_1,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f2628,plain,
( ~ product(e_1,e_1,e_4)
| spl0_131 ),
inference(avatar_component_clause,[],[f2627]) ).
fof(f2629,plain,
( product(e_1,e_1,e_4)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f2627]) ).
fof(f2631,definition,
( spl0_132
<=> product(e_1,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f2632,plain,
( ~ product(e_1,e_1,e_3)
| spl0_132 ),
inference(avatar_component_clause,[],[f2631]) ).
fof(f2633,plain,
( product(e_1,e_1,e_3)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f2631]) ).
fof(f2635,definition,
( spl0_133
<=> product(e_1,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f2636,plain,
( ~ product(e_1,e_1,e_1)
| spl0_133 ),
inference(avatar_component_clause,[],[f2635]) ).
fof(f2637,plain,
( product(e_1,e_1,e_1)
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f2635]) ).
fof(f2638,plain,
( spl0_131
| spl0_132
| spl0_133
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f2625,f756,f425,f421,f417,f413,f2635,f2631,f2627]) ).
fof(f2639,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)
| ~ group_element(e_2)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(resolution,[],[f1972,f53]) ).
fof(f2640,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)
| ~ group_element(e_2)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f2639,f28]) ).
fof(f2641,plain,
( 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)
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f2640,f606]) ).
fof(f2642,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| ~ group_element(e_2)
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f2641,f602]) ).
fof(f2643,plain,
( product(e_2,e_1,e_3)
| ~ group_element(e_2)
| ~ spl0_14
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f2642,f2537]) ).
fof(f2644,plain,
( product(e_2,e_1,e_3)
| ~ spl0_14
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f2643,f29]) ).
fof(f2645,plain,
( spl0_129
| ~ spl0_14
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_42
| spl0_43 ),
inference(avatar_split_clause,[],[f2644,f605,f601,f425,f421,f417,f413,f122,f2611]) ).
fof(f2652,plain,
( ~ product(e_1,e_1,e_2)
| ~ spl0_20 ),
inference(unit_resulting_resolution,[],[f26,f11,f149]) ).
fof(f2653,plain,
( ~ product(e_1,e_1,e_3)
| ~ spl0_20 ),
inference(unit_resulting_resolution,[],[f26,f12,f149]) ).
fof(f2654,plain,
( ~ product(e_1,e_1,e_4)
| ~ spl0_20 ),
inference(unit_resulting_resolution,[],[f26,f13,f149]) ).
fof(f2655,plain,
( ~ product(e_1,e_1,e_5)
| ~ spl0_20 ),
inference(unit_resulting_resolution,[],[f26,f14,f149]) ).
fof(f2673,plain,
( $false
| ~ spl0_20
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f2653,f2633]) ).
fof(f2674,plain,
( ~ spl0_20
| ~ spl0_132 ),
inference(avatar_contradiction_clause,[],[f2673]) ).
fof(f2675,plain,
( ~ spl0_131
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f2654,f147,f2627]) ).
fof(f2721,plain,
( product(e_4,e_5,e_2)
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| ~ spl0_58 ),
inference(unit_resulting_resolution,[],[f57,f758,f1976]) ).
fof(f2741,plain,
( spl0_106
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f2721,f756,f425,f421,f417,f413,f2067]) ).
fof(f2761,plain,
( ~ product(e_4,e_2,e_1)
| ~ spl0_96 ),
inference(unit_resulting_resolution,[],[f55,f42,f2004]) ).
fof(f2784,plain,
( ~ product(e_5,e_3,e_4)
| spl0_29
| ~ spl0_96 ),
inference(unit_resulting_resolution,[],[f57,f453,f2004]) ).
fof(f2794,plain,
( ~ spl0_99
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f2761,f2002,f2018]) ).
fof(f2822,plain,
( ~ product(e_3,e_3,e_3)
| ~ spl0_94 ),
inference(unit_resulting_resolution,[],[f56,f47,f1996]) ).
fof(f2832,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)
| ~ group_element(e_3)
| ~ group_element(e_3)
| product(e_4,e_3,e_5)
| ~ spl0_94 ),
inference(resolution,[],[f1996,f164]) ).
fof(f2837,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)
| ~ group_element(e_3)
| product(e_4,e_3,e_5)
| ~ spl0_94 ),
inference(duplicate_literal_removal,[],[f2832]) ).
fof(f2838,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_4,e_3,e_5)
| ~ spl0_94 ),
inference(forward_subsumption_resolution,[],[f2837,f30]) ).
fof(f2846,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_4)
| product(e_4,e_3,e_5)
| ~ spl0_94 ),
inference(forward_subsumption_resolution,[],[f2838,f2822]) ).
fof(f2847,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_4)
| spl0_69
| ~ spl0_94 ),
inference(forward_subsumption_resolution,[],[f2846,f870]) ).
fof(f2849,definition,
( spl0_134
<=> product(e_3,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f2853,definition,
( spl0_135
<=> product(e_3,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f2855,plain,
( product(e_3,e_3,e_2)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f2853]) ).
fof(f2857,definition,
( spl0_136
<=> product(e_3,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f2859,plain,
( product(e_3,e_3,e_1)
| ~ spl0_136 ),
inference(avatar_component_clause,[],[f2857]) ).
fof(f2860,plain,
( spl0_134
| spl0_135
| spl0_136
| spl0_69
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f2847,f1994,f869,f2857,f2853,f2849]) ).
fof(f2879,plain,
( ~ product(e_4,e_4,e_4)
| ~ spl0_68 ),
inference(unit_resulting_resolution,[],[f55,f43,f864]) ).
fof(f2898,plain,
( product(e_4,e_4,e_4)
| ~ spl0_68 ),
inference(unit_resulting_resolution,[],[f57,f864,f864]) ).
fof(f2911,plain,
( ~ spl0_100
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f2879,f862,f2033]) ).
fof(f2914,plain,
( spl0_100
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f2898,f862,f2033]) ).
fof(f2931,plain,
( ~ product(e_4,e_2,e_2)
| ~ spl0_95 ),
inference(unit_resulting_resolution,[],[f55,f38,f2000]) ).
fof(f2933,plain,
( ~ product(e_4,e_5,e_2)
| ~ spl0_95 ),
inference(unit_resulting_resolution,[],[f55,f51,f2000]) ).
fof(f2946,plain,
( ~ product(e_5,e_3,e_4)
| spl0_28
| ~ spl0_95 ),
inference(unit_resulting_resolution,[],[f57,f449,f2000]) ).
fof(f2959,plain,
( $false
| ~ spl0_95
| ~ spl0_98 ),
inference(forward_subsumption_resolution,[],[f2931,f2016]) ).
fof(f2960,plain,
( ~ spl0_95
| ~ spl0_98 ),
inference(avatar_contradiction_clause,[],[f2959]) ).
fof(f3061,plain,
( ~ product(e_5,e_2,e_1)
| ~ spl0_29 ),
inference(unit_resulting_resolution,[],[f55,f46,f454]) ).
fof(f3101,plain,
( product(e_4,e_3,e_1)
| spl0_68
| spl0_69
| spl0_94
| spl0_95 ),
inference(unit_resulting_resolution,[],[f53,f31,f30,f863,f1995,f870,f1999]) ).
fof(f3185,plain,
( ~ product(e_4,e_5,e_2)
| ~ spl0_98 ),
inference(unit_resulting_resolution,[],[f55,f50,f2016]) ).
fof(f3190,plain,
( ~ product(e_5,e_2,e_2)
| ~ spl0_98 ),
inference(unit_resulting_resolution,[],[f56,f48,f2016]) ).
fof(f3198,plain,
( ~ product(e_5,e_2,e_4)
| spl0_28
| ~ spl0_98 ),
inference(unit_resulting_resolution,[],[f57,f449,f2016]) ).
fof(f3211,plain,
( $false
| ~ spl0_98
| ~ spl0_106 ),
inference(forward_subsumption_resolution,[],[f3185,f2069]) ).
fof(f3212,plain,
( ~ spl0_98
| ~ spl0_106 ),
inference(avatar_contradiction_clause,[],[f3211]) ).
fof(f3276,plain,
( ~ product(e_4,e_5,e_3)
| ~ spl0_97 ),
inference(unit_resulting_resolution,[],[f55,f50,f2012]) ).
fof(f3281,plain,
( ~ product(e_5,e_2,e_3)
| ~ spl0_97 ),
inference(unit_resulting_resolution,[],[f56,f48,f2012]) ).
fof(f3368,plain,
( product(e_4,e_4,e_4)
| ~ spl0_71 ),
inference(unit_resulting_resolution,[],[f57,f944,f944]) ).
fof(f3382,plain,
( $false
| ~ spl0_71
| spl0_100 ),
inference(forward_subsumption_resolution,[],[f3368,f2034]) ).
fof(f3383,plain,
( ~ spl0_71
| spl0_100 ),
inference(avatar_contradiction_clause,[],[f3382]) ).
fof(f3532,plain,
( ~ product(e_3,e_3,e_2)
| ~ spl0_94
| spl0_95 ),
inference(unit_resulting_resolution,[],[f57,f1999,f1996]) ).
fof(f3533,plain,
( ~ product(e_3,e_3,e_4)
| spl0_68
| ~ spl0_94 ),
inference(unit_resulting_resolution,[],[f57,f863,f1996]) ).
fof(f3543,plain,
( $false
| ~ spl0_94
| spl0_95
| ~ spl0_135 ),
inference(forward_subsumption_resolution,[],[f3532,f2855]) ).
fof(f3544,plain,
( ~ spl0_94
| spl0_95
| ~ spl0_135 ),
inference(avatar_contradiction_clause,[],[f3543]) ).
fof(f3545,plain,
( ~ spl0_134
| spl0_68
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f3533,f1994,f862,f2849]) ).
fof(f3627,plain,
( ~ product(e_3,e_3,e_1)
| ~ spl0_94
| spl0_96 ),
inference(unit_resulting_resolution,[],[f57,f1996,f2003]) ).
fof(f3628,plain,
( $false
| ~ spl0_94
| spl0_96
| ~ spl0_136 ),
inference(forward_subsumption_resolution,[],[f3627,f2859]) ).
fof(f3629,plain,
( ~ spl0_94
| spl0_96
| ~ spl0_136 ),
inference(avatar_contradiction_clause,[],[f3628]) ).
fof(f3632,plain,
( ~ spl0_58
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f1489,f554,f756]) ).
fof(f3637,plain,
( $false
| ~ spl0_61
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f2097,f2613]) ).
fof(f3638,plain,
( ~ spl0_61
| ~ spl0_129 ),
inference(avatar_contradiction_clause,[],[f3637]) ).
fof(f3639,plain,
( ~ spl0_106
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f2933,f1998,f2067]) ).
fof(f3646,plain,
( $false
| ~ spl0_4
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1894,f427]) ).
fof(f3647,plain,
( ~ spl0_4
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f3646]) ).
fof(f3648,plain,
( spl0_5
| spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f259,f80,f76,f72,f68,f84]) ).
fof(f3650,plain,
( spl0_15
| spl0_11
| spl0_12
| spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f318,f122,f118,f114,f110,f126]) ).
fof(f3816,plain,
( ~ product(e_1,e_1,e_1)
| ~ spl0_24 ),
inference(unit_resulting_resolution,[],[f56,f35,f427]) ).
fof(f3852,plain,
( $false
| ~ spl0_24
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f3816,f2637]) ).
fof(f3853,plain,
( ~ spl0_24
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f3852]) ).
fof(f3926,definition,
( spl0_151
<=> product(e_3,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f3927,plain,
( ~ product(e_3,e_1,e_4)
| spl0_151 ),
inference(avatar_component_clause,[],[f3926]) ).
fof(f3928,plain,
( product(e_3,e_1,e_4)
| ~ spl0_151 ),
inference(avatar_component_clause,[],[f3926]) ).
fof(f3967,plain,
( ~ product(e_4,e_1,e_2)
| ~ spl0_4 ),
inference(unit_resulting_resolution,[],[f27,f40,f5,f6,f82]) ).
fof(f3968,plain,
( ~ product(e_4,e_1,e_3)
| ~ spl0_4 ),
inference(unit_resulting_resolution,[],[f27,f44,f5,f6,f82]) ).
fof(f4059,plain,
( ~ product(e_3,e_1,e_1)
| ~ spl0_8 ),
inference(unit_resulting_resolution,[],[f27,f35,f4,f7,f99]) ).
fof(f4060,plain,
( ~ product(e_3,e_1,e_2)
| ~ spl0_8 ),
inference(unit_resulting_resolution,[],[f27,f39,f4,f7,f99]) ).
fof(f4061,plain,
( ~ product(e_3,e_1,e_3)
| ~ spl0_8 ),
inference(unit_resulting_resolution,[],[f27,f43,f4,f7,f99]) ).
fof(f4062,plain,
( ~ product(e_3,e_1,e_5)
| ~ spl0_8 ),
inference(unit_resulting_resolution,[],[f27,f52,f4,f7,f99]) ).
fof(f4069,plain,
( ! [X2,X0,X1] :
( ~ cycle(X0,X1)
| ~ next(X0,e_3)
| ~ greater(X1,e_0)
| ~ next(e_2,X2)
| equalish(X1,X2) )
| ~ spl0_8 ),
inference(resolution,[],[f99,f24]) ).
fof(f4103,plain,
( ~ product(e_5,e_4,e_1)
| ~ spl0_28 ),
inference(unit_resulting_resolution,[],[f54,f33,f450]) ).
fof(f4109,plain,
( ~ product(e_5,e_2,e_2)
| ~ spl0_28 ),
inference(unit_resulting_resolution,[],[f55,f46,f450]) ).
fof(f4238,plain,
( product(e_4,e_5,e_3)
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| ~ spl0_61 ),
inference(unit_resulting_resolution,[],[f57,f768,f1976]) ).
fof(f4302,plain,
( product(e_5,e_3,e_4)
| ~ spl0_61
| ~ spl0_151 ),
inference(unit_resulting_resolution,[],[f57,f768,f3928]) ).
fof(f4445,plain,
( ~ product(e_5,e_2,e_1)
| ~ spl0_99 ),
inference(unit_resulting_resolution,[],[f56,f48,f2020]) ).
fof(f4456,plain,
( ~ product(e_5,e_2,e_4)
| spl0_29
| ~ spl0_99 ),
inference(unit_resulting_resolution,[],[f57,f453,f2020]) ).
fof(f4559,plain,
( ~ product(e_4,e_2,e_4)
| ~ spl0_100 ),
inference(unit_resulting_resolution,[],[f55,f39,f2035]) ).
fof(f4589,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)
| ~ group_element(e_1)
| ~ spl0_20 ),
inference(resolution,[],[f2655,f53]) ).
fof(f4590,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)
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f4589]) ).
fof(f4591,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)
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f4590,f28]) ).
fof(f4592,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_4)
| ~ spl0_20
| spl0_133 ),
inference(forward_subsumption_resolution,[],[f4591,f2636]) ).
fof(f4593,plain,
( product(e_1,e_1,e_3)
| product(e_1,e_1,e_4)
| ~ spl0_20
| spl0_133 ),
inference(forward_subsumption_resolution,[],[f4592,f2652]) ).
fof(f4594,plain,
( product(e_1,e_1,e_4)
| ~ spl0_20
| spl0_132
| spl0_133 ),
inference(forward_subsumption_resolution,[],[f4593,f2632]) ).
fof(f4595,plain,
( $false
| ~ spl0_20
| spl0_131
| spl0_132
| spl0_133 ),
inference(forward_subsumption_resolution,[],[f4594,f2628]) ).
fof(f4596,plain,
( ~ spl0_20
| spl0_131
| spl0_132
| spl0_133 ),
inference(avatar_contradiction_clause,[],[f4595]) ).
fof(f4778,plain,
( ~ cycle(e_2,e_1)
| ~ spl0_8 ),
inference(unit_resulting_resolution,[],[f4069,f34,f3,f6,f3]) ).
fof(f4779,plain,
( ~ cycle(e_2,e_2)
| ~ spl0_8 ),
inference(unit_resulting_resolution,[],[f4069,f38,f3,f7,f3]) ).
fof(f4780,plain,
( ~ cycle(e_2,e_4)
| ~ spl0_8 ),
inference(unit_resulting_resolution,[],[f4069,f47,f3,f9,f3]) ).
fof(f5427,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_2)
| ~ group_element(e_2)
| product(e_5,e_2,e_3)
| ~ spl0_74
| spl0_128 ),
inference(resolution,[],[f2608,f1003]) ).
fof(f5436,plain,
( product(e_5,e_2,e_2)
| ~ group_element(e_2)
| product(e_5,e_2,e_3)
| ~ spl0_74
| ~ spl0_99
| spl0_128 ),
inference(forward_subsumption_resolution,[],[f5427,f4445]) ).
fof(f5440,plain,
( ~ group_element(e_2)
| product(e_5,e_2,e_3)
| ~ spl0_28
| ~ spl0_74
| ~ spl0_99
| spl0_128 ),
inference(forward_subsumption_resolution,[],[f5436,f4109]) ).
fof(f5444,plain,
( product(e_5,e_2,e_3)
| ~ spl0_28
| ~ spl0_74
| ~ spl0_99
| spl0_128 ),
inference(forward_subsumption_resolution,[],[f5440,f29]) ).
fof(f5448,plain,
( $false
| ~ spl0_28
| ~ spl0_61
| ~ spl0_74
| ~ spl0_99
| spl0_128 ),
inference(forward_subsumption_resolution,[],[f5444,f2086]) ).
fof(f5449,plain,
( ~ spl0_28
| ~ spl0_61
| ~ spl0_74
| ~ spl0_99
| spl0_128 ),
inference(avatar_contradiction_clause,[],[f5448]) ).
fof(f5453,plain,
( $false
| spl0_28
| ~ spl0_61
| ~ spl0_95
| ~ spl0_151 ),
inference(forward_subsumption_resolution,[],[f2946,f4302]) ).
fof(f5454,plain,
( spl0_28
| ~ spl0_61
| ~ spl0_95
| ~ spl0_151 ),
inference(avatar_contradiction_clause,[],[f5453]) ).
fof(f5465,definition,
( spl0_174
<=> product(e_5,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f5466,plain,
( ~ product(e_5,e_2,e_2)
| spl0_174 ),
inference(avatar_component_clause,[],[f5465]) ).
fof(f5467,plain,
( product(e_5,e_2,e_2)
| ~ spl0_174 ),
inference(avatar_component_clause,[],[f5465]) ).
fof(f5482,plain,
( ~ spl0_174
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f4109,f448,f5465]) ).
fof(f5494,plain,
( ~ spl0_130
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1063,f998,f2617]) ).
fof(f5500,plain,
( ~ spl0_29
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f4103,f448,f452]) ).
fof(f5501,plain,
( ~ spl0_128
| spl0_29
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f4456,f2018,f452,f2607]) ).
fof(f5883,plain,
( ~ group_element(e_2)
| product(e_5,e_2,e_1)
| product(e_5,e_2,e_2)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_4)
| ~ group_element(e_5)
| spl0_130 ),
inference(resolution,[],[f2618,f53]) ).
fof(f5884,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_2)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_4)
| ~ group_element(e_5)
| spl0_130 ),
inference(forward_subsumption_resolution,[],[f5883,f29]) ).
fof(f5885,plain,
( product(e_5,e_2,e_2)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_4)
| ~ group_element(e_5)
| ~ spl0_99
| spl0_130 ),
inference(forward_subsumption_resolution,[],[f5884,f4445]) ).
fof(f5886,plain,
( product(e_5,e_2,e_3)
| product(e_5,e_2,e_4)
| ~ group_element(e_5)
| ~ spl0_99
| spl0_130
| spl0_174 ),
inference(forward_subsumption_resolution,[],[f5885,f5466]) ).
fof(f5887,plain,
( product(e_5,e_2,e_4)
| ~ group_element(e_5)
| ~ spl0_61
| ~ spl0_99
| spl0_130
| spl0_174 ),
inference(forward_subsumption_resolution,[],[f5886,f2086]) ).
fof(f5888,plain,
( ~ group_element(e_5)
| ~ spl0_61
| ~ spl0_99
| spl0_128
| spl0_130
| spl0_174 ),
inference(forward_subsumption_resolution,[],[f5887,f2608]) ).
fof(f5889,plain,
( $false
| ~ spl0_61
| ~ spl0_99
| spl0_128
| spl0_130
| spl0_174 ),
inference(forward_subsumption_resolution,[],[f5888,f32]) ).
fof(f5890,plain,
( ~ spl0_61
| ~ spl0_99
| spl0_128
| spl0_130
| spl0_174 ),
inference(avatar_contradiction_clause,[],[f5889]) ).
fof(f5898,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_4)
| ~ group_element(e_5)
| spl0_130
| spl0_174 ),
inference(forward_subsumption_resolution,[],[f5884,f5466]) ).
fof(f5901,plain,
( $false
| ~ spl0_71
| ~ spl0_100 ),
inference(forward_subsumption_resolution,[],[f4559,f944]) ).
fof(f5902,plain,
( ~ spl0_71
| ~ spl0_100 ),
inference(avatar_contradiction_clause,[],[f5901]) ).
fof(f5903,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_4)
| ~ group_element(e_5)
| ~ spl0_61
| spl0_130
| spl0_174 ),
inference(forward_subsumption_resolution,[],[f5898,f2086]) ).
fof(f5904,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_4)
| ~ spl0_61
| spl0_130
| spl0_174 ),
inference(forward_subsumption_resolution,[],[f5903,f32]) ).
fof(f5906,definition,
( spl0_184
<=> product(e_5,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_184])],[avatar_definition]) ).
fof(f5907,plain,
( ~ product(e_5,e_2,e_1)
| spl0_184 ),
inference(avatar_component_clause,[],[f5906]) ).
fof(f5909,plain,
( spl0_128
| spl0_184
| ~ spl0_61
| spl0_130
| spl0_174 ),
inference(avatar_split_clause,[],[f5904,f5465,f2617,f766,f5906,f2607]) ).
fof(f5915,plain,
( ~ spl0_105
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f3276,f2010,f2063]) ).
fof(f5926,plain,
( $false
| ~ spl0_4
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f3967,f423]) ).
fof(f5927,plain,
( ~ spl0_4
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f5926]) ).
fof(f5949,plain,
( $false
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f4780,f112]) ).
fof(f5950,plain,
( ~ spl0_8
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f5949]) ).
fof(f5969,plain,
( spl0_105
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f4238,f766,f425,f421,f417,f413,f2063]) ).
fof(f5970,plain,
( spl0_96
| spl0_68
| spl0_69
| spl0_94
| spl0_95 ),
inference(avatar_split_clause,[],[f3101,f1998,f1994,f869,f862,f2002]) ).
fof(f5971,plain,
( $false
| spl0_29
| ~ spl0_61
| ~ spl0_96
| ~ spl0_151 ),
inference(forward_subsumption_resolution,[],[f2784,f4302]) ).
fof(f5972,plain,
( spl0_29
| ~ spl0_61
| ~ spl0_96
| ~ spl0_151 ),
inference(avatar_contradiction_clause,[],[f5971]) ).
fof(f5986,plain,
( ~ spl0_128
| spl0_28
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f3198,f2014,f448,f2607]) ).
fof(f5991,plain,
( $false
| ~ spl0_98
| ~ spl0_174 ),
inference(forward_subsumption_resolution,[],[f3190,f5467]) ).
fof(f5992,plain,
( ~ spl0_98
| ~ spl0_174 ),
inference(avatar_contradiction_clause,[],[f5991]) ).
fof(f5993,plain,
( product(e_5,e_2,e_2)
| ~ group_element(e_2)
| product(e_5,e_2,e_3)
| ~ spl0_74
| spl0_128
| spl0_184 ),
inference(forward_subsumption_resolution,[],[f5427,f5907]) ).
fof(f5994,plain,
( ~ group_element(e_2)
| product(e_5,e_2,e_3)
| ~ spl0_74
| spl0_128
| spl0_174
| spl0_184 ),
inference(forward_subsumption_resolution,[],[f5993,f5466]) ).
fof(f5995,plain,
( product(e_5,e_2,e_3)
| ~ spl0_74
| spl0_128
| spl0_174
| spl0_184 ),
inference(forward_subsumption_resolution,[],[f5994,f29]) ).
fof(f5996,plain,
( $false
| ~ spl0_61
| ~ spl0_74
| spl0_128
| spl0_174
| spl0_184 ),
inference(forward_subsumption_resolution,[],[f5995,f2086]) ).
fof(f5997,plain,
( ~ spl0_61
| ~ spl0_74
| spl0_128
| spl0_174
| spl0_184 ),
inference(avatar_contradiction_clause,[],[f5996]) ).
fof(f6011,plain,
( $false
| ~ spl0_8
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f4059,f560]) ).
fof(f6012,plain,
( ~ spl0_8
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f6011]) ).
fof(f6017,plain,
( $false
| ~ spl0_8
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f4060,f556]) ).
fof(f6018,plain,
( ~ spl0_8
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f6017]) ).
fof(f6061,plain,
( ~ cycle(e_1,e_1)
| ~ spl0_12 ),
inference(unit_resulting_resolution,[],[f24,f35,f4,f6,f2,f116]) ).
fof(f6063,plain,
( ~ cycle(e_1,e_3)
| ~ spl0_12 ),
inference(unit_resulting_resolution,[],[f24,f43,f4,f8,f2,f116]) ).
fof(f6113,plain,
( $false
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f4779,f120]) ).
fof(f6114,plain,
( ~ spl0_8
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f6113]) ).
fof(f6116,plain,
( ~ spl0_17
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f6063,f114,f135]) ).
fof(f6117,plain,
( ~ spl0_19
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f6061,f114,f143]) ).
fof(f6144,plain,
( ~ cycle(e_1,e_2)
| ~ spl0_12 ),
inference(unit_resulting_resolution,[],[f24,f39,f4,f7,f2,f116]) ).
fof(f6154,plain,
( ~ product(e_2,e_1,e_4)
| ~ spl0_12 ),
inference(unit_resulting_resolution,[],[f27,f47,f3,f8,f116]) ).
fof(f6255,plain,
( ~ product(e_1,e_1,e_3)
| ~ spl0_16 ),
inference(unit_resulting_resolution,[],[f27,f42,f2,f9,f133]) ).
fof(f6283,plain,
( $false
| ~ spl0_16
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f6255,f2633]) ).
fof(f6284,plain,
( ~ spl0_16
| ~ spl0_132 ),
inference(avatar_contradiction_clause,[],[f6283]) ).
fof(f6289,plain,
( $false
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f6144,f141]) ).
fof(f6290,plain,
( ~ spl0_12
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f6289]) ).
fof(f6446,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)
| ~ group_element(e_2)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(resolution,[],[f1972,f53]) ).
fof(f6447,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)
| ~ group_element(e_2)
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f6446,f28]) ).
fof(f6448,plain,
( 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)
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f6447,f606]) ).
fof(f6449,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| ~ group_element(e_2)
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_42
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f6448,f602]) ).
fof(f6450,plain,
( product(e_2,e_1,e_4)
| ~ group_element(e_2)
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_42
| spl0_43
| spl0_129 ),
inference(forward_subsumption_resolution,[],[f6449,f2612]) ).
fof(f6451,plain,
( ~ group_element(e_2)
| ~ spl0_12
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_42
| spl0_43
| spl0_129 ),
inference(forward_subsumption_resolution,[],[f6450,f6154]) ).
fof(f6452,plain,
( $false
| ~ spl0_12
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_42
| spl0_43
| spl0_129 ),
inference(forward_subsumption_resolution,[],[f6451,f29]) ).
fof(f6453,plain,
( ~ spl0_12
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_42
| spl0_43
| spl0_129 ),
inference(avatar_contradiction_clause,[],[f6452]) ).
fof(f6454,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)
| ~ group_element(e_3)
| ~ spl0_8 ),
inference(resolution,[],[f4062,f53]) ).
fof(f6455,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)
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f6454,f28]) ).
fof(f6456,plain,
( 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)
| ~ spl0_8
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f6455,f559]) ).
fof(f6457,plain,
( product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| ~ group_element(e_3)
| ~ spl0_8
| spl0_38
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f6456,f555]) ).
fof(f6458,plain,
( product(e_3,e_1,e_4)
| ~ group_element(e_3)
| ~ spl0_8
| spl0_37
| spl0_38
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f6457,f551]) ).
fof(f6459,plain,
( ~ group_element(e_3)
| ~ spl0_8
| spl0_37
| spl0_38
| spl0_39
| spl0_151 ),
inference(forward_subsumption_resolution,[],[f6458,f3927]) ).
fof(f6460,plain,
( $false
| ~ spl0_8
| spl0_37
| spl0_38
| spl0_39
| spl0_151 ),
inference(forward_subsumption_resolution,[],[f6459,f30]) ).
fof(f6461,plain,
( ~ spl0_8
| spl0_37
| spl0_38
| spl0_39
| spl0_151 ),
inference(avatar_contradiction_clause,[],[f6460]) ).
fof(f6464,plain,
( ~ spl0_184
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f3061,f452,f5906]) ).
fof(f6721,plain,
( ~ product(e_1,e_1,e_4)
| ~ spl0_151 ),
inference(unit_resulting_resolution,[],[f56,f34,f3928]) ).
fof(f7453,plain,
( product(e_5,e_2,e_3)
| ~ spl0_58
| ~ spl0_129 ),
inference(unit_resulting_resolution,[],[f57,f758,f2613]) ).
fof(f7473,plain,
( $false
| ~ spl0_58
| ~ spl0_97
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f7453,f3281]) ).
fof(f7474,plain,
( ~ spl0_58
| ~ spl0_97
| ~ spl0_129 ),
inference(avatar_contradiction_clause,[],[f7473]) ).
fof(f7475,plain,
( spl0_43
| ~ spl0_15
| spl0_42 ),
inference(avatar_split_clause,[],[f1565,f601,f126,f605]) ).
fof(f7478,plain,
( $false
| ~ spl0_43
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f1614,f2637]) ).
fof(f7479,plain,
( ~ spl0_43
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f7478]) ).
fof(f7496,plain,
( $false
| ~ spl0_131
| ~ spl0_151 ),
inference(forward_subsumption_resolution,[],[f6721,f2629]) ).
fof(f7497,plain,
( ~ spl0_131
| ~ spl0_151 ),
inference(avatar_contradiction_clause,[],[f7496]) ).
fof(f7500,plain,
( $false
| ~ spl0_15
| ~ spl0_43
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f1625,f2633]) ).
fof(f7501,plain,
( ~ spl0_15
| ~ spl0_43
| ~ spl0_132 ),
inference(avatar_contradiction_clause,[],[f7500]) ).
fof(f7502,plain,
( spl0_131
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_58
| spl0_61
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f2383,f786,f766,f756,f425,f421,f417,f413,f2627]) ).
fof(f7520,plain,
( $false
| ~ spl0_8
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f4061,f552]) ).
fof(f7521,plain,
( ~ spl0_8
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f7520]) ).
fof(f7526,plain,
( ~ spl0_17
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f2450,f122,f135]) ).
fof(f7531,plain,
( $false
| ~ spl0_14
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f1587,f124]) ).
fof(f7532,plain,
( ~ spl0_14
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f7531]) ).
fof(f7536,plain,
( $false
| ~ spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f4778,f124]) ).
fof(f7537,plain,
( ~ spl0_8
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f7536]) ).
fof(f7546,plain,
( $false
| ~ spl0_4
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f3968,f419]) ).
fof(f7547,plain,
( ~ spl0_4
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f7546]) ).
cnf(s2,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f108]) ).
cnf(s5,plain,
~ spl0_3,
inference(sat_conversion,[],[f156]) ).
cnf(s6,plain,
~ spl0_2,
inference(sat_conversion,[],[f158]) ).
cnf(s7,plain,
~ spl0_1,
inference(sat_conversion,[],[f159]) ).
cnf(s8,plain,
( ~ spl0_5
| ~ spl0_19 ),
inference(sat_conversion,[],[f202]) ).
cnf(s9,plain,
( ~ spl0_5
| ~ spl0_18 ),
inference(sat_conversion,[],[f203]) ).
cnf(s10,plain,
( ~ spl0_5
| ~ spl0_17 ),
inference(sat_conversion,[],[f204]) ).
cnf(s12,plain,
( ~ spl0_5
| ~ spl0_14 ),
inference(sat_conversion,[],[f207]) ).
cnf(s13,plain,
( ~ spl0_5
| ~ spl0_13 ),
inference(sat_conversion,[],[f208]) ).
cnf(s14,plain,
( ~ spl0_5
| ~ spl0_12 ),
inference(sat_conversion,[],[f209]) ).
cnf(s16,plain,
( ~ spl0_5
| ~ spl0_9 ),
inference(sat_conversion,[],[f212]) ).
cnf(s17,plain,
( ~ spl0_5
| ~ spl0_8 ),
inference(sat_conversion,[],[f213]) ).
cnf(s18,plain,
( ~ spl0_5
| ~ spl0_7 ),
inference(sat_conversion,[],[f214]) ).
cnf(s23,plain,
( ~ spl0_4
| ~ spl0_9 ),
inference(sat_conversion,[],[f252]) ).
cnf(s24,plain,
( ~ spl0_4
| ~ spl0_7 ),
inference(sat_conversion,[],[f253]) ).
cnf(s25,plain,
( ~ spl0_4
| ~ spl0_6 ),
inference(sat_conversion,[],[f255]) ).
cnf(s26,plain,
( ~ spl0_5
| ~ spl0_6 ),
inference(sat_conversion,[],[f256]) ).
cnf(s33,plain,
( ~ spl0_5
| ~ spl0_11 ),
inference(sat_conversion,[],[f257]) ).
cnf(s37,plain,
( ~ spl0_5
| ~ spl0_16 ),
inference(sat_conversion,[],[f258]) ).
cnf(s72,plain,
( ~ spl0_22
| ~ spl0_37 ),
inference(sat_conversion,[],[f853]) ).
cnf(s85,plain,
( ~ spl0_23
| ~ spl0_42 ),
inference(sat_conversion,[],[f929]) ).
cnf(s96,plain,
( spl0_73
| spl0_74 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s101,plain,
( ~ spl0_10
| spl0_37
| spl0_38
| spl0_39 ),
inference(sat_conversion,[],[f1041]) ).
cnf(s102,plain,
( ~ spl0_73
| ~ spl0_75 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s118,plain,
( spl0_73
| ~ spl0_75 ),
inference(sat_conversion,[],[f1176]) ).
cnf(s125,plain,
( ~ spl0_20
| ~ spl0_39 ),
inference(sat_conversion,[],[f1293]) ).
cnf(s142,plain,
( ~ spl0_20
| ~ spl0_43 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s158,plain,
( ~ spl0_38
| ~ spl0_42 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s172,plain,
~ spl0_21,
inference(sat_conversion,[],[f1833]) ).
cnf(s177,plain,
( ~ spl0_5
| spl0_21
| spl0_22
| spl0_23
| spl0_24 ),
inference(sat_conversion,[],[f1848]) ).
cnf(s188,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| ~ spl0_72 ),
inference(sat_conversion,[],[f1987]) ).
cnf(s189,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| ~ spl0_69 ),
inference(sat_conversion,[],[f1988]) ).
cnf(s191,plain,
( spl0_71
| spl0_72
| spl0_97
| spl0_98
| spl0_99 ),
inference(sat_conversion,[],[f2021]) ).
cnf(s193,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_58
| spl0_61
| spl0_65
| spl0_75 ),
inference(sat_conversion,[],[f2056]) ).
cnf(s197,plain,
( ~ spl0_37
| ~ spl0_61 ),
inference(sat_conversion,[],[f2121]) ).
cnf(s202,plain,
( ~ spl0_42
| ~ spl0_58 ),
inference(sat_conversion,[],[f2172]) ).
cnf(s212,plain,
( ~ spl0_20
| ~ spl0_65 ),
inference(sat_conversion,[],[f2302]) ).
cnf(s213,plain,
( ~ spl0_20
| ~ spl0_65 ),
inference(sat_conversion,[],[f2304]) ).
cnf(s229,plain,
( ~ spl0_10
| ~ spl0_15
| ~ spl0_19 ),
inference(sat_conversion,[],[f2378]) ).
cnf(s235,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_16 ),
inference(sat_conversion,[],[f2393]) ).
cnf(s240,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_17 ),
inference(sat_conversion,[],[f2403]) ).
cnf(s245,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_18 ),
inference(sat_conversion,[],[f2413]) ).
cnf(s248,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_12 ),
inference(sat_conversion,[],[f2419]) ).
cnf(s251,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_13 ),
inference(sat_conversion,[],[f2425]) ).
cnf(s257,plain,
( ~ spl0_14
| ~ spl0_42 ),
inference(sat_conversion,[],[f2489]) ).
cnf(s264,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_11 ),
inference(sat_conversion,[],[f2497]) ).
cnf(s269,plain,
( ~ spl0_14
| ~ spl0_19 ),
inference(sat_conversion,[],[f2498]) ).
cnf(s272,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f2499]) ).
cnf(s277,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| ~ spl0_58
| spl0_131
| spl0_132
| spl0_133 ),
inference(sat_conversion,[],[f2638]) ).
cnf(s278,plain,
( ~ spl0_14
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_42
| spl0_43
| spl0_129 ),
inference(sat_conversion,[],[f2645]) ).
cnf(s279,plain,
( ~ spl0_20
| ~ spl0_132 ),
inference(sat_conversion,[],[f2674]) ).
cnf(s280,plain,
( ~ spl0_20
| ~ spl0_131 ),
inference(sat_conversion,[],[f2675]) ).
cnf(s281,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| ~ spl0_58
| spl0_106 ),
inference(sat_conversion,[],[f2741]) ).
cnf(s288,plain,
( ~ spl0_96
| ~ spl0_99 ),
inference(sat_conversion,[],[f2794]) ).
cnf(s302,plain,
( spl0_69
| ~ spl0_94
| spl0_134
| spl0_135
| spl0_136 ),
inference(sat_conversion,[],[f2860]) ).
cnf(s306,plain,
( ~ spl0_68
| ~ spl0_100 ),
inference(sat_conversion,[],[f2911]) ).
cnf(s313,plain,
( ~ spl0_68
| spl0_100 ),
inference(sat_conversion,[],[f2914]) ).
cnf(s318,plain,
( ~ spl0_95
| ~ spl0_98 ),
inference(sat_conversion,[],[f2960]) ).
cnf(s349,plain,
( ~ spl0_98
| ~ spl0_106 ),
inference(sat_conversion,[],[f3212]) ).
cnf(s367,plain,
( ~ spl0_71
| spl0_100 ),
inference(sat_conversion,[],[f3383]) ).
cnf(s378,plain,
( ~ spl0_94
| spl0_95
| ~ spl0_135 ),
inference(sat_conversion,[],[f3544]) ).
cnf(s379,plain,
( spl0_68
| ~ spl0_94
| ~ spl0_134 ),
inference(sat_conversion,[],[f3545]) ).
cnf(s380,plain,
( ~ spl0_94
| spl0_96
| ~ spl0_136 ),
inference(sat_conversion,[],[f3629]) ).
cnf(s388,plain,
( ~ spl0_38
| ~ spl0_58 ),
inference(sat_conversion,[],[f3632]) ).
cnf(s392,plain,
( ~ spl0_61
| ~ spl0_129 ),
inference(sat_conversion,[],[f3638]) ).
cnf(s393,plain,
( ~ spl0_95
| ~ spl0_106 ),
inference(sat_conversion,[],[f3639]) ).
cnf(s400,plain,
( ~ spl0_4
| ~ spl0_24 ),
inference(sat_conversion,[],[f3647]) ).
cnf(s401,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f3648]) ).
cnf(s407,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f3650]) ).
cnf(s417,plain,
( ~ spl0_24
| ~ spl0_133 ),
inference(sat_conversion,[],[f3853]) ).
cnf(s450,plain,
( ~ spl0_20
| spl0_131
| spl0_132
| spl0_133 ),
inference(sat_conversion,[],[f4596]) ).
cnf(s517,plain,
( ~ spl0_28
| ~ spl0_61
| ~ spl0_74
| ~ spl0_99
| spl0_128 ),
inference(sat_conversion,[],[f5449]) ).
cnf(s518,plain,
( spl0_28
| ~ spl0_61
| ~ spl0_95
| ~ spl0_151 ),
inference(sat_conversion,[],[f5454]) ).
cnf(s524,plain,
( ~ spl0_28
| ~ spl0_174 ),
inference(sat_conversion,[],[f5482]) ).
cnf(s532,plain,
( ~ spl0_73
| ~ spl0_130 ),
inference(sat_conversion,[],[f5494]) ).
cnf(s537,plain,
( ~ spl0_28
| ~ spl0_29 ),
inference(sat_conversion,[],[f5500]) ).
cnf(s539,plain,
( spl0_29
| ~ spl0_99
| ~ spl0_128 ),
inference(sat_conversion,[],[f5501]) ).
cnf(s542,plain,
( ~ spl0_61
| ~ spl0_99
| spl0_128
| spl0_130
| spl0_174 ),
inference(sat_conversion,[],[f5890]) ).
cnf(s553,plain,
( ~ spl0_71
| ~ spl0_100 ),
inference(sat_conversion,[],[f5902]) ).
cnf(s554,plain,
( ~ spl0_61
| spl0_128
| spl0_130
| spl0_174
| spl0_184 ),
inference(sat_conversion,[],[f5909]) ).
cnf(s561,plain,
( ~ spl0_97
| ~ spl0_105 ),
inference(sat_conversion,[],[f5915]) ).
cnf(s566,plain,
( ~ spl0_4
| ~ spl0_23 ),
inference(sat_conversion,[],[f5927]) ).
cnf(s575,plain,
( ~ spl0_8
| ~ spl0_11 ),
inference(sat_conversion,[],[f5950]) ).
cnf(s583,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| ~ spl0_61
| spl0_105 ),
inference(sat_conversion,[],[f5969]) ).
cnf(s584,plain,
( spl0_68
| spl0_69
| spl0_94
| spl0_95
| spl0_96 ),
inference(sat_conversion,[],[f5970]) ).
cnf(s585,plain,
( spl0_29
| ~ spl0_61
| ~ spl0_96
| ~ spl0_151 ),
inference(sat_conversion,[],[f5972]) ).
cnf(s593,plain,
( spl0_28
| ~ spl0_98
| ~ spl0_128 ),
inference(sat_conversion,[],[f5986]) ).
cnf(s596,plain,
( ~ spl0_98
| ~ spl0_174 ),
inference(sat_conversion,[],[f5992]) ).
cnf(s597,plain,
( ~ spl0_61
| ~ spl0_74
| spl0_128
| spl0_174
| spl0_184 ),
inference(sat_conversion,[],[f5997]) ).
cnf(s617,plain,
( ~ spl0_8
| ~ spl0_39 ),
inference(sat_conversion,[],[f6012]) ).
cnf(s623,plain,
( ~ spl0_8
| ~ spl0_38 ),
inference(sat_conversion,[],[f6018]) ).
cnf(s654,plain,
( ~ spl0_8
| ~ spl0_13 ),
inference(sat_conversion,[],[f6114]) ).
cnf(s658,plain,
( ~ spl0_12
| ~ spl0_17 ),
inference(sat_conversion,[],[f6116]) ).
cnf(s659,plain,
( ~ spl0_12
| ~ spl0_19 ),
inference(sat_conversion,[],[f6117]) ).
cnf(s666,plain,
( ~ spl0_16
| ~ spl0_132 ),
inference(sat_conversion,[],[f6284]) ).
cnf(s669,plain,
( ~ spl0_12
| ~ spl0_18 ),
inference(sat_conversion,[],[f6290]) ).
cnf(s672,plain,
( ~ spl0_12
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_42
| spl0_43
| spl0_129 ),
inference(sat_conversion,[],[f6453]) ).
cnf(s673,plain,
( ~ spl0_8
| spl0_37
| spl0_38
| spl0_39
| spl0_151 ),
inference(sat_conversion,[],[f6461]) ).
cnf(s676,plain,
( ~ spl0_29
| ~ spl0_184 ),
inference(sat_conversion,[],[f6464]) ).
cnf(s706,plain,
( ~ spl0_58
| ~ spl0_97
| ~ spl0_129 ),
inference(sat_conversion,[],[f7474]) ).
cnf(s709,plain,
( ~ spl0_15
| spl0_42
| spl0_43 ),
inference(sat_conversion,[],[f7475]) ).
cnf(s713,plain,
( ~ spl0_43
| ~ spl0_133 ),
inference(sat_conversion,[],[f7479]) ).
cnf(s724,plain,
( ~ spl0_131
| ~ spl0_151 ),
inference(sat_conversion,[],[f7497]) ).
cnf(s726,plain,
( ~ spl0_15
| ~ spl0_43
| ~ spl0_132 ),
inference(sat_conversion,[],[f7501]) ).
cnf(s727,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_58
| spl0_61
| ~ spl0_65
| spl0_131 ),
inference(sat_conversion,[],[f7502]) ).
cnf(s744,plain,
( ~ spl0_8
| ~ spl0_37 ),
inference(sat_conversion,[],[f7521]) ).
cnf(s745,plain,
( ~ spl0_14
| ~ spl0_17 ),
inference(sat_conversion,[],[f7526]) ).
cnf(s755,plain,
( ~ spl0_14
| ~ spl0_43 ),
inference(sat_conversion,[],[f7532]) ).
cnf(s781,plain,
( ~ spl0_8
| ~ spl0_14 ),
inference(sat_conversion,[],[f7537]) ).
cnf(s800,plain,
( ~ spl0_4
| ~ spl0_22 ),
inference(sat_conversion,[],[f7547]) ).
cnf(s813,plain,
~ spl0_5,
inference(rat,[],[s72,s177,s101,s85,s158,s417,s709,s450,s125,s142,s279,s280,s272,s2,s407,s8,s9,s10,s12,s13,s14,s16,s17,s18,s26,s33,s37,s172]) ).
cnf(s814,plain,
spl0_4,
inference(rat,[],[s401,s5,s6,s7,s813]) ).
cnf(s815,plain,
~ spl0_22,
inference(rat,[],[s800,s814]) ).
cnf(s816,plain,
~ spl0_23,
inference(rat,[],[s566,s814]) ).
cnf(s818,plain,
~ spl0_24,
inference(rat,[],[s400,s814]) ).
cnf(s820,plain,
~ spl0_6,
inference(rat,[],[s25,s814]) ).
cnf(s821,plain,
~ spl0_7,
inference(rat,[],[s24,s814]) ).
cnf(s822,plain,
~ spl0_9,
inference(rat,[],[s23,s814]) ).
cnf(s826,plain,
~ spl0_72,
inference(rat,[],[s188,s818,s815,s172,s816]) ).
cnf(s827,plain,
~ spl0_69,
inference(rat,[],[s189,s818,s815,s172,s816]) ).
cnf(s832,plain,
~ spl0_75,
inference(rat,[],[s102,s118]) ).
cnf(s834,plain,
( ~ spl0_15
| ~ spl0_10 ),
inference(rat,[],[s197,s101,s193,s158,s202,s709,s125,s142,s213,s272,s229,s245,s240,s235,s172,s818,s815,s816,s832,s814]) ).
cnf(s835,plain,
( spl0_96
| spl0_68
| spl0_95 ),
inference(rat,[],[s302,s378,s379,s380,s584,s827]) ).
cnf(s836,plain,
~ spl0_71,
inference(rat,[],[s367,s553]) ).
cnf(s837,plain,
~ spl0_68,
inference(rat,[],[s306,s313]) ).
cnf(s838,plain,
( ~ spl0_14
| ~ spl0_58 ),
inference(rat,[],[s278,s755,s202,s706,s191,s288,s835,s393,s349,s281,s172,s816,s818,s815,s836,s826,s837]) ).
cnf(s839,plain,
( ~ spl0_10
| spl0_14 ),
inference(rat,[],[s407,s834,s248,s251,s264,s814]) ).
cnf(s840,plain,
( ~ spl0_15
| ~ spl0_58 ),
inference(rat,[],[s277,s713,s726,s709,s202,s724,s673,s744,s617,s2,s839,s838,s388,s172,s818,s815,s816,s821,s822,s820]) ).
cnf(s841,plain,
~ spl0_58,
inference(rat,[],[s666,s272,s277,s142,s713,s672,s658,s659,s669,s407,s840,s724,s673,s575,s617,s654,s744,s2,s839,s838,s706,s191,s288,s835,s349,s393,s281,s202,s388,s172,s818,s815,s816,s820,s822,s821,s826,s836,s837]) ).
cnf(s842,plain,
~ spl0_14,
inference(rat,[],[s212,s193,s272,s392,s235,s245,s278,s2,s257,s269,s745,s755,s781,s172,s818,s815,s816,s841,s832,s814,s820,s822,s821]) ).
cnf(s843,plain,
~ spl0_10,
inference(rat,[],[s839,s842]) ).
cnf(s844,plain,
spl0_8,
inference(rat,[],[s2,s821,s822,s820,s843]) ).
cnf(s845,plain,
~ spl0_37,
inference(rat,[],[s744,s844]) ).
cnf(s847,plain,
~ spl0_38,
inference(rat,[],[s623,s844]) ).
cnf(s848,plain,
~ spl0_39,
inference(rat,[],[s617,s844]) ).
cnf(s850,plain,
spl0_151,
inference(rat,[],[s673,s847,s848,s844,s845]) ).
cnf(s851,plain,
~ spl0_131,
inference(rat,[],[s724,s850]) ).
cnf(s856,plain,
( spl0_128
| spl0_184
| ~ spl0_61
| spl0_174 ),
inference(rat,[],[s96,s532,s597,s554]) ).
cnf(s857,plain,
( ~ spl0_96
| ~ spl0_61 ),
inference(rat,[],[s856,s593,s596,s537,s676,s191,s585,s288,s561,s583,s826,s836,s850,s816,s815,s818,s172]) ).
cnf(s858,plain,
~ spl0_61,
inference(rat,[],[s96,s532,s517,s542,s539,s524,s537,s191,s518,s318,s835,s857,s561,s583,s826,s836,s850,s837,s172,s818,s815,s816]) ).
cnf(s859,plain,
spl0_65,
inference(rat,[],[s193,s832,s841,s816,s815,s818,s172,s858]) ).
cnf(s860,plain,
$false,
inference(rat,[],[s727,s851,s841,s816,s815,s818,s172,s858,s859]) ).
fof(f7570,plain,
$false,
inference(avatar_sat_refutation,[],[s860]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP128-3.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n003.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 09:27:55 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 11.50/2.33 % (245461)Input is clausal, will run a generic CNF schedule.
% 11.50/2.33 % (245519)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4211125017:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.50/2.33 % (245517)lrs+10_1_sil=8000:sp=occurrence:random_seed=2979029623:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.50/2.33 % (245515)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3774227573:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.50/2.33 % (245521)dis-21_1_sil=8000:lcm=predicate:random_seed=3860381155: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)
% 11.50/2.33 % (245514)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=1609135400:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.50/2.33 % (245516)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1559989094:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.50/2.33 % (245520)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=144251915:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.50/2.33 % (245517)Instruction limit reached!
% 11.50/2.33 % (245517)------------------------------
% 11.50/2.33 % (245517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/2.33 % (245517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/2.33 % (245517)CaDiCaL version: 2.1.3
% 11.50/2.33 % (245517)Termination reason: Instruction limit
% 11.50/2.33 % (245517)Termination phase: Saturation
% 11.50/2.33 % (245517)Time elapsed: 0.061 s
% 11.50/2.33 % (245517)Peak memory usage: 88 MB
% 11.50/2.33 % (245517)Instructions burned: 108 (million)
% 11.50/2.33 % (245519)Instruction limit reached!
% 11.50/2.33 % (245519)------------------------------
% 11.50/2.33 % (245519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/2.33 % (245519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/2.33 % (245519)CaDiCaL version: 2.1.3
% 11.50/2.33 % (245519)Termination reason: Instruction limit
% 11.50/2.33 % (245519)Termination phase: Saturation
% 11.50/2.33 % (245519)Time elapsed: 0.065 s
% 11.50/2.33 % (245519)Peak memory usage: 88 MB
% 11.50/2.33 % (245519)Instructions burned: 115 (million)
% 11.50/2.33 % (245521)Instruction limit reached!
% 11.50/2.33 % (245521)------------------------------
% 11.50/2.33 % (245521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/2.33 % (245521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/2.33 % (245521)CaDiCaL version: 2.1.3
% 11.50/2.33 % (245521)Termination reason: Instruction limit
% 11.50/2.33 % (245521)Termination phase: Saturation
% 11.50/2.33 % (245521)Time elapsed: 0.072 s
% 11.50/2.33 % (245521)Peak memory usage: 88 MB
% 11.50/2.33 % (245521)Instructions burned: 117 (million)
% 11.50/2.33 % (245520)Instruction limit reached!
% 11.50/2.33 % (245520)------------------------------
% 11.50/2.33 % (245520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/2.33 % (245520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/2.33 % (245520)CaDiCaL version: 2.1.3
% 11.50/2.33 % (245520)Termination reason: Instruction limit
% 11.50/2.33 % (245520)Termination phase: Saturation
% 11.50/2.33 % (245520)Time elapsed: 0.126 s
% 11.50/2.33 % (245520)Peak memory usage: 89 MB
% 11.50/2.33 % (245520)Instructions burned: 180 (million)
% 11.50/2.33 % (245581)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=726581366:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.50/2.33 % (245582)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=66553662: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)
% 11.50/2.33 % (245583)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3530759799:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.50/2.33 % (245581)Instruction limit reached!
% 11.50/2.33 % (245581)------------------------------
% 11.50/2.33 % (245581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/2.33 % (245581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245581)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245581)Termination reason: Instruction limit
% 14.51/2.73 % (245581)Termination phase: Saturation
% 14.51/2.73 % (245581)Time elapsed: 0.046 s
% 14.51/2.73 % (245581)Peak memory usage: 89 MB
% 14.51/2.73 % (245581)Instructions burned: 144 (million)
% 14.51/2.73 % (245582)Refutation not found, incomplete strategy
% 14.51/2.73 % (245582)------------------------------
% 14.51/2.73 % (245582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245582)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245582)Termination reason: Refutation not found, incomplete strategy
% 14.51/2.73 % (245582)Time elapsed: 0.002 s
% 14.51/2.73 % (245582)Peak memory usage: 87 MB
% 14.51/2.73 % (245582)Instructions burned: 2 (million)
% 14.51/2.73 % (245584)lrs+10_64_to=lpo:sil=8000:random_seed=3432697736:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 14.51/2.73 % (245583)Instruction limit reached!
% 14.51/2.73 % (245583)------------------------------
% 14.51/2.73 % (245583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245583)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245583)Termination reason: Instruction limit
% 14.51/2.73 % (245583)Termination phase: Saturation
% 14.51/2.73 % (245583)Time elapsed: 0.123 s
% 14.51/2.73 % (245583)Peak memory usage: 88 MB
% 14.51/2.73 % (245583)Instructions burned: 220 (million)
% 14.51/2.73 % (245584)Instruction limit reached!
% 14.51/2.73 % (245584)------------------------------
% 14.51/2.73 % (245584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245584)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245584)Termination reason: Instruction limit
% 14.51/2.73 % (245584)Termination phase: Saturation
% 14.51/2.73 % (245584)Time elapsed: 0.042 s
% 14.51/2.73 % (245584)Peak memory usage: 88 MB
% 14.51/2.73 % (245584)Instructions burned: 130 (million)
% 14.51/2.73 % (245588)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=564797865:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 14.51/2.73 % (245603)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3463323098:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 14.51/2.73 % (245582)------------------------------
% 14.51/2.73 % (245582)------------------------------
% 14.51/2.73 % (245604)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1404466528:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 14.51/2.73 % (245603)Instruction limit reached!
% 14.51/2.73 % (245603)------------------------------
% 14.51/2.73 % (245603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245603)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245603)Termination reason: Instruction limit
% 14.51/2.73 % (245603)Termination phase: Saturation
% 14.51/2.73 % (245603)Time elapsed: 0.047 s
% 14.51/2.73 % (245603)Peak memory usage: 89 MB
% 14.51/2.73 % (245603)Instructions burned: 160 (million)
% 14.51/2.73 % (245588)Instruction limit reached!
% 14.51/2.73 % (245588)------------------------------
% 14.51/2.73 % (245588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245588)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245588)Termination reason: Instruction limit
% 14.51/2.73 % (245588)Termination phase: Saturation
% 14.51/2.73 % (245588)Time elapsed: 0.127 s
% 14.51/2.73 % (245588)Peak memory usage: 88 MB
% 14.51/2.73 % (245588)Instructions burned: 196 (million)
% 14.51/2.73 % (245515)Refutation not found, incomplete strategy
% 14.51/2.73 % (245515)------------------------------
% 14.51/2.73 % (245515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245515)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245515)Termination reason: Refutation not found, incomplete strategy
% 14.51/2.73 % (245515)Time elapsed: 0.600 s
% 14.51/2.73 % (245515)Peak memory usage: 127 MB
% 14.51/2.73 % (245515)Instructions burned: 904 (million)
% 14.51/2.73 % (245607)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=4057022381:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 14.51/2.73 % (245607)Refutation not found, incomplete strategy
% 14.51/2.73 % (245607)------------------------------
% 14.51/2.73 % (245607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245607)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245607)Termination reason: Refutation not found, incomplete strategy
% 14.51/2.73 % (245607)Time elapsed: 0.003 s
% 14.51/2.73 % (245607)Peak memory usage: 88 MB
% 14.51/2.73 % (245607)Instructions burned: 3 (million)
% 14.51/2.73 % (245609)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=36990259:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 14.51/2.73 % (245609)Instruction limit reached!
% 14.51/2.73 % (245609)------------------------------
% 14.51/2.73 % (245609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245609)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245609)Termination reason: Instruction limit
% 14.51/2.73 % (245609)Termination phase: Saturation
% 14.51/2.73 % (245609)Time elapsed: 0.036 s
% 14.51/2.73 % (245609)Peak memory usage: 88 MB
% 14.51/2.73 % (245609)Instructions burned: 110 (million)
% 14.51/2.73 % (245610)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3234133257:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 14.51/2.73 % (245613)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2937573572:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 14.51/2.73 % (245515)------------------------------
% 14.51/2.73 % (245515)------------------------------
% 14.51/2.73 % (245610)Instruction limit reached!
% 14.51/2.73 % (245610)------------------------------
% 14.51/2.73 % (245610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245610)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245610)Termination reason: Instruction limit
% 14.51/2.73 % (245610)Termination phase: Saturation
% 14.51/2.73 % (245610)Time elapsed: 0.126 s
% 14.51/2.73 % (245610)Peak memory usage: 89 MB
% 14.51/2.73 % (245610)Instructions burned: 242 (million)
% 14.51/2.73 % (245607)------------------------------
% 14.51/2.73 % (245607)------------------------------
% 14.51/2.73 % (245617)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1499629241:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 14.51/2.73 % (245616)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1471048080:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 14.51/2.73 % (245625)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2634566506:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 14.51/2.73 % (245616)Instruction limit reached!
% 14.51/2.73 % (245616)------------------------------
% 14.51/2.73 % (245616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245616)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245616)Termination reason: Instruction limit
% 14.51/2.73 % (245616)Termination phase: Saturation
% 14.51/2.73 % (245616)Time elapsed: 0.078 s
% 14.51/2.73 % (245616)Peak memory usage: 87 MB
% 14.51/2.73 % (245616)Instructions burned: 134 (million)
% 14.51/2.73 % (245625)Instruction limit reached!
% 14.51/2.73 % (245625)------------------------------
% 14.51/2.73 % (245625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245625)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245625)Termination reason: Instruction limit
% 14.51/2.73 % (245625)Termination phase: Saturation
% 14.51/2.73 % (245625)Time elapsed: 0.198 s
% 14.51/2.73 % (245625)Peak memory usage: 89 MB
% 14.51/2.73 % (245625)Instructions burned: 191 (million)
% 14.51/2.73 % (245640)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2547929034:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 14.51/2.73 % (245617)First to succeed.
% 14.51/2.73 % (245617)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-245461"
% 14.51/2.73 % (245644)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1981741037:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 14.51/2.73 % (245640)Instruction limit reached!
% 14.51/2.73 % (245640)------------------------------
% 14.51/2.73 % (245640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245640)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245640)Termination reason: Instruction limit
% 14.51/2.73 % (245640)Termination phase: Saturation
% 14.51/2.73 % (245640)Time elapsed: 0.247 s
% 14.51/2.73 % (245640)Peak memory usage: 89 MB
% 14.51/2.73 % (245640)Instructions burned: 264 (million)
% 14.51/2.73 % (245644)Instruction limit reached!
% 14.51/2.73 % (245644)------------------------------
% 14.51/2.73 % (245644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.51/2.73 % (245644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.73 % (245644)CaDiCaL version: 2.1.3
% 14.51/2.73 % (245644)Termination reason: Instruction limit
% 14.51/2.73 % (245644)Termination phase: Saturation
% 14.51/2.73 % (245644)Time elapsed: 0.138 s
% 14.51/2.73 % (245644)Peak memory usage: 88 MB
% 14.51/2.73 % (245644)Instructions burned: 157 (million)
% 14.51/2.73 % (245617)Refutation found. Thanks to Tanya!
% 14.51/2.73 % SZS status Unsatisfiable for theBenchmark
% 14.51/2.73 % SZS output start Proof for theBenchmark
% See solution above
% 15.17/2.93 % (245617)------------------------------
% 15.17/2.93 % (245617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/2.93 % (245617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/2.93 % (245617)CaDiCaL version: 2.1.3
% 15.17/2.93 % (245617)Termination reason: Refutation
% 15.17/2.93 % (245617)Time elapsed: 0.419 s
% 15.17/2.93 % (245617)Peak memory usage: 91 MB
% 15.17/2.93 % (245617)Instructions burned: 462 (million)
% 15.17/2.93 % (245617)------------------------------
% 15.17/2.93 % (245617)------------------------------
% 15.17/2.93 % (245461)Success in time 2.092 s
% 15.17/2.93 % Vampire exiting
%------------------------------------------------------------------------------