%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP125-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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:12:44 AM UTC 2026
% Result : Unsatisfiable 4.30s 1.20s
% Output : Refutation 4.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 136
% Syntax : Number of formulae : 756 ( 148 unt; 85 def)
% Number of atoms : 1854 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 2089 ( 991 ~;1013 |; 0 &)
% ( 85 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 92 ( 91 usr; 86 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 136 ( 0 sgn 136 !; 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(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(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] :
( ~ group_element(X1)
| ~ group_element(X0)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| product(X0,X1,e_5) ),
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,axiom,
! [X0] : product(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_idempotence) ).
fof(f58,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ product(X1,X0,X3)
| ~ product(X0,X1,X2)
| product(X2,X3,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3) ).
fof(f73,plain,
! [X0,X1] :
( ~ product(X0,X0,X1)
| equalish(X1,X0) ),
inference(resolution,[],[f54,f57]) ).
fof(f75,plain,
! [X0,X1] :
( ~ product(X0,X1,X0)
| equalish(X1,X0) ),
inference(resolution,[],[f55,f57]) ).
fof(f77,plain,
! [X0,X1] :
( ~ product(X0,X1,X1)
| equalish(X0,X1) ),
inference(resolution,[],[f56,f57]) ).
fof(f81,definition,
( spl0_3
<=> ! [X1] :
( ~ next(e_1,X1)
| equalish(e_1,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f82,plain,
( ! [X1] :
( ~ next(e_1,X1)
| equalish(e_1,X1) )
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f81]) ).
fof(f87,plain,
( equalish(e_1,e_2)
| ~ spl0_3 ),
inference(resolution,[],[f82,f2]) ).
fof(f88,plain,
( $false
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f87,f33]) ).
fof(f89,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[],[f88]) ).
fof(f91,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2)
| cycle(e_2,e_3)
| cycle(e_2,e_4) ),
inference(resolution,[],[f22,f29]) ).
fof(f92,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(f93,plain,
( cycle(e_4,e_0)
| cycle(e_4,e_1)
| cycle(e_4,e_2)
| cycle(e_4,e_3)
| cycle(e_4,e_4) ),
inference(resolution,[],[f22,f31]) ).
fof(f96,definition,
( spl0_5
<=> cycle(e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f98,plain,
( cycle(e_4,e_4)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f96]) ).
fof(f100,definition,
( spl0_6
<=> cycle(e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f102,plain,
( cycle(e_4,e_3)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f104,definition,
( spl0_7
<=> cycle(e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f106,plain,
( cycle(e_4,e_2)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f104]) ).
fof(f108,definition,
( spl0_8
<=> cycle(e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f110,plain,
( cycle(e_4,e_1)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f108]) ).
fof(f112,definition,
( spl0_9
<=> cycle(e_4,e_0) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f114,plain,
( cycle(e_4,e_0)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f112]) ).
fof(f115,plain,
( spl0_5
| spl0_6
| spl0_7
| spl0_8
| spl0_9 ),
inference(avatar_split_clause,[],[f93,f112,f108,f104,f100,f96]) ).
fof(f117,definition,
( spl0_10
<=> cycle(e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f119,plain,
( cycle(e_3,e_4)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f117]) ).
fof(f121,definition,
( spl0_11
<=> cycle(e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f123,plain,
( cycle(e_3,e_3)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f125,definition,
( spl0_12
<=> cycle(e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f127,plain,
( cycle(e_3,e_2)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f125]) ).
fof(f129,definition,
( spl0_13
<=> cycle(e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f131,plain,
( cycle(e_3,e_1)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f129]) ).
fof(f133,definition,
( spl0_14
<=> cycle(e_3,e_0) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f135,plain,
( cycle(e_3,e_0)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f133]) ).
fof(f136,plain,
( spl0_10
| spl0_11
| spl0_12
| spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f92,f133,f129,f125,f121,f117]) ).
fof(f138,definition,
( spl0_15
<=> cycle(e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f140,plain,
( cycle(e_2,e_4)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f138]) ).
fof(f142,definition,
( spl0_16
<=> cycle(e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f144,plain,
( cycle(e_2,e_3)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f142]) ).
fof(f146,definition,
( spl0_17
<=> cycle(e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f148,plain,
( cycle(e_2,e_2)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f146]) ).
fof(f150,definition,
( spl0_18
<=> cycle(e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f152,plain,
( cycle(e_2,e_1)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f150]) ).
fof(f154,definition,
( spl0_19
<=> cycle(e_2,e_0) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f156,plain,
( cycle(e_2,e_0)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f157,plain,
( spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_19 ),
inference(avatar_split_clause,[],[f91,f154,f150,f146,f142,f138]) ).
fof(f176,plain,
! [X2,X0,X1] :
( ~ cycle(X0,X1)
| ~ next(X0,e_5)
| ~ greater(X1,e_0)
| ~ next(e_0,X2)
| equalish(X1,X2) ),
inference(resolution,[],[f24,f23]) ).
fof(f197,plain,
( ! [X0] :
( ~ next(e_4,e_5)
| ~ greater(e_4,e_0)
| ~ next(e_0,X0)
| equalish(e_4,X0) )
| ~ spl0_5 ),
inference(resolution,[],[f176,f98]) ).
fof(f199,plain,
( ! [X0] :
( ~ greater(e_4,e_0)
| ~ next(e_0,X0)
| equalish(e_4,X0) )
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f197,f5]) ).
fof(f202,plain,
( ! [X0] :
( ~ next(e_0,X0)
| equalish(e_4,X0) )
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f199,f9]) ).
fof(f204,definition,
( spl0_24
<=> ! [X0] :
( ~ next(e_0,X0)
| equalish(e_4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f205,plain,
( ! [X0] :
( ~ next(e_0,X0)
| equalish(e_4,X0) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f216,plain,
( spl0_24
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f202,f96,f204]) ).
fof(f217,plain,
( equalish(e_4,e_1)
| ~ spl0_24 ),
inference(resolution,[],[f205,f1]) ).
fof(f218,plain,
( $false
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f217,f45]) ).
fof(f219,plain,
~ spl0_24,
inference(avatar_contradiction_clause,[],[f218]) ).
fof(f220,plain,
( ! [X0] :
( ~ next(e_4,e_5)
| ~ greater(e_3,e_0)
| ~ next(e_0,X0)
| equalish(e_3,X0) )
| ~ spl0_6 ),
inference(resolution,[],[f102,f176]) ).
fof(f223,plain,
( ! [X0] :
( ~ greater(e_3,e_0)
| ~ next(e_0,X0)
| equalish(e_3,X0) )
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f220,f5]) ).
fof(f224,plain,
( ! [X0] :
( ~ next(e_0,X0)
| equalish(e_3,X0) )
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f223,f8]) ).
fof(f226,plain,
( equalish(e_3,e_1)
| ~ spl0_6 ),
inference(resolution,[],[f224,f1]) ).
fof(f227,plain,
( $false
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f226,f41]) ).
fof(f228,plain,
~ spl0_6,
inference(avatar_contradiction_clause,[],[f227]) ).
fof(f229,plain,
( ! [X0] :
( ~ next(e_4,e_5)
| ~ greater(e_2,e_0)
| ~ next(e_0,X0)
| equalish(e_2,X0) )
| ~ spl0_7 ),
inference(resolution,[],[f106,f176]) ).
fof(f232,plain,
( ! [X0] :
( ~ greater(e_2,e_0)
| ~ next(e_0,X0)
| equalish(e_2,X0) )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f229,f5]) ).
fof(f233,plain,
( ! [X0] :
( ~ next(e_0,X0)
| equalish(e_2,X0) )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f232,f7]) ).
fof(f235,plain,
( equalish(e_2,e_1)
| ~ spl0_7 ),
inference(resolution,[],[f233,f1]) ).
fof(f236,plain,
( $false
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f235,f37]) ).
fof(f237,plain,
~ spl0_7,
inference(avatar_contradiction_clause,[],[f236]) ).
fof(f239,plain,
( ! [X2,X0,X1] :
( ~ cycle(X0,X1)
| ~ next(X0,e_4)
| ~ greater(X1,e_0)
| ~ next(e_1,X2)
| equalish(X1,X2) )
| ~ spl0_8 ),
inference(resolution,[],[f110,f24]) ).
fof(f309,definition,
( spl0_35
<=> ! [X0] :
( ~ next(e_0,X0)
| equalish(e_3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f310,plain,
( ! [X0] :
( ~ next(e_0,X0)
| equalish(e_3,X0) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f323,plain,
( ! [X0] :
( ~ next(e_3,e_4)
| ~ greater(e_3,e_0)
| ~ next(e_1,X0)
| equalish(e_3,X0) )
| ~ spl0_8
| ~ spl0_11 ),
inference(resolution,[],[f239,f123]) ).
fof(f327,plain,
( ! [X0] :
( ~ greater(e_3,e_0)
| ~ next(e_1,X0)
| equalish(e_3,X0) )
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f323,f4]) ).
fof(f334,plain,
( ! [X0] :
( ~ next(e_1,X0)
| equalish(e_3,X0) )
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f327,f8]) ).
fof(f336,definition,
( spl0_39
<=> ! [X0] :
( ~ next(e_1,X0)
| equalish(e_4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f337,plain,
( ! [X0] :
( ~ next(e_1,X0)
| equalish(e_4,X0) )
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f343,plain,
( equalish(e_3,e_2)
| ~ spl0_8
| ~ spl0_11 ),
inference(resolution,[],[f334,f2]) ).
fof(f344,plain,
( $false
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f343,f42]) ).
fof(f345,plain,
( ~ spl0_8
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f344]) ).
fof(f349,plain,
( ! [X2,X0,X1] :
( ~ cycle(X0,X1)
| ~ next(X0,e_4)
| ~ greater(X1,e_0)
| ~ next(e_0,X2)
| equalish(X1,X2) )
| ~ spl0_9 ),
inference(resolution,[],[f114,f24]) ).
fof(f367,plain,
( ! [X0] :
( ~ next(e_3,e_4)
| ~ greater(e_3,e_0)
| ~ next(e_0,X0)
| equalish(e_3,X0) )
| ~ spl0_9
| ~ spl0_11 ),
inference(resolution,[],[f349,f123]) ).
fof(f370,plain,
( ! [X0] :
( ~ greater(e_3,e_0)
| ~ next(e_0,X0)
| equalish(e_3,X0) )
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f367,f4]) ).
fof(f371,plain,
( ! [X0] :
( ~ next(e_0,X0)
| equalish(e_3,X0) )
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f370,f8]) ).
fof(f372,plain,
( spl0_35
| ~ spl0_9
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f371,f121,f112,f309]) ).
fof(f373,plain,
( equalish(e_3,e_1)
| ~ spl0_35 ),
inference(resolution,[],[f310,f1]) ).
fof(f374,plain,
( $false
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f373,f41]) ).
fof(f375,plain,
~ spl0_35,
inference(avatar_contradiction_clause,[],[f374]) ).
fof(f377,plain,
( ! [X2,X0,X1] :
( ~ cycle(X0,X1)
| ~ next(X0,e_4)
| ~ greater(X1,e_0)
| ~ next(e_1,X2)
| equalish(X1,X2) )
| ~ spl0_8 ),
inference(resolution,[],[f110,f24]) ).
fof(f445,plain,
( ! [X0] :
( ~ next(e_3,e_4)
| ~ greater(e_4,e_0)
| ~ next(e_1,X0)
| equalish(e_4,X0) )
| ~ spl0_8
| ~ spl0_10 ),
inference(resolution,[],[f119,f377]) ).
fof(f446,plain,
( ! [X0] :
( ~ greater(e_4,e_0)
| ~ next(e_1,X0)
| equalish(e_4,X0) )
| ~ spl0_8
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f445,f4]) ).
fof(f447,plain,
( ! [X0] :
( ~ next(e_1,X0)
| equalish(e_4,X0) )
| ~ spl0_8
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f446,f9]) ).
fof(f448,plain,
( spl0_39
| ~ spl0_8
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f447,f117,f108,f336]) ).
fof(f454,plain,
( ! [X0] :
( ~ next(e_3,e_4)
| ~ greater(e_1,e_0)
| ~ next(e_1,X0)
| equalish(e_1,X0) )
| ~ spl0_8
| ~ spl0_13 ),
inference(resolution,[],[f131,f377]) ).
fof(f455,plain,
( ! [X0] :
( ~ greater(e_1,e_0)
| ~ next(e_1,X0)
| equalish(e_1,X0) )
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f454,f4]) ).
fof(f456,plain,
( ! [X0] :
( ~ next(e_1,X0)
| equalish(e_1,X0) )
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f455,f6]) ).
fof(f457,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f456,f129,f108,f81]) ).
fof(f609,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_5) ),
inference(resolution,[],[f53,f28]) ).
fof(f610,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| product(X0,e_2,e_5) ),
inference(resolution,[],[f53,f29]) ).
fof(f611,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| product(X0,e_3,e_5) ),
inference(resolution,[],[f53,f30]) ).
fof(f612,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| product(X0,e_4,e_5) ),
inference(resolution,[],[f53,f31]) ).
fof(f613,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_5) ),
inference(resolution,[],[f53,f32]) ).
fof(f615,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5) ),
inference(resolution,[],[f609,f29]) ).
fof(f616,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5) ),
inference(resolution,[],[f609,f30]) ).
fof(f617,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)
| product(e_4,e_1,e_5) ),
inference(resolution,[],[f609,f31]) ).
fof(f618,plain,
( product(e_5,e_1,e_1)
| product(e_5,e_1,e_2)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_4)
| product(e_5,e_1,e_5) ),
inference(resolution,[],[f609,f32]) ).
fof(f620,definition,
( spl0_54
<=> product(e_5,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f622,plain,
( product(e_5,e_1,e_5)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f624,definition,
( spl0_55
<=> product(e_5,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f626,plain,
( product(e_5,e_1,e_4)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f628,definition,
( spl0_56
<=> product(e_5,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f629,plain,
( ~ product(e_5,e_1,e_3)
| spl0_56 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f630,plain,
( product(e_5,e_1,e_3)
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f632,definition,
( spl0_57
<=> product(e_5,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f634,plain,
( product(e_5,e_1,e_2)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f636,definition,
( spl0_58
<=> product(e_5,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f638,plain,
( product(e_5,e_1,e_1)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f639,plain,
( spl0_54
| spl0_55
| spl0_56
| spl0_57
| spl0_58 ),
inference(avatar_split_clause,[],[f618,f636,f632,f628,f624,f620]) ).
fof(f641,definition,
( spl0_59
<=> product(e_4,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f643,plain,
( product(e_4,e_1,e_5)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f641]) ).
fof(f645,definition,
( spl0_60
<=> product(e_4,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f647,plain,
( product(e_4,e_1,e_4)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f649,definition,
( spl0_61
<=> product(e_4,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f651,plain,
( product(e_4,e_1,e_3)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f649]) ).
fof(f653,definition,
( spl0_62
<=> product(e_4,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f655,plain,
( product(e_4,e_1,e_2)
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f657,definition,
( spl0_63
<=> product(e_4,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f659,plain,
( product(e_4,e_1,e_1)
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f660,plain,
( spl0_59
| spl0_60
| spl0_61
| spl0_62
| spl0_63 ),
inference(avatar_split_clause,[],[f617,f657,f653,f649,f645,f641]) ).
fof(f662,definition,
( spl0_64
<=> product(e_3,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f663,plain,
( ~ product(e_3,e_1,e_5)
| spl0_64 ),
inference(avatar_component_clause,[],[f662]) ).
fof(f664,plain,
( product(e_3,e_1,e_5)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f662]) ).
fof(f666,definition,
( spl0_65
<=> product(e_3,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f668,plain,
( product(e_3,e_1,e_4)
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f670,definition,
( spl0_66
<=> product(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f672,plain,
( product(e_3,e_1,e_3)
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f670]) ).
fof(f674,definition,
( spl0_67
<=> product(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f676,plain,
( product(e_3,e_1,e_2)
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f678,definition,
( spl0_68
<=> product(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f680,plain,
( product(e_3,e_1,e_1)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f681,plain,
( spl0_64
| spl0_65
| spl0_66
| spl0_67
| spl0_68 ),
inference(avatar_split_clause,[],[f616,f678,f674,f670,f666,f662]) ).
fof(f683,definition,
( spl0_69
<=> product(e_2,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f685,plain,
( product(e_2,e_1,e_5)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f687,definition,
( spl0_70
<=> product(e_2,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f689,plain,
( product(e_2,e_1,e_4)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f691,definition,
( spl0_71
<=> product(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f693,plain,
( product(e_2,e_1,e_3)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f695,definition,
( spl0_72
<=> product(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f697,plain,
( product(e_2,e_1,e_2)
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f699,definition,
( spl0_73
<=> product(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f701,plain,
( product(e_2,e_1,e_1)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f702,plain,
( spl0_69
| spl0_70
| spl0_71
| spl0_72
| spl0_73 ),
inference(avatar_split_clause,[],[f615,f699,f695,f691,f687,f683]) ).
fof(f709,plain,
( equalish(e_1,e_5)
| ~ spl0_54 ),
inference(resolution,[],[f622,f75]) ).
fof(f710,plain,
( $false
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f709,f36]) ).
fof(f711,plain,
~ spl0_54,
inference(avatar_contradiction_clause,[],[f710]) ).
fof(f722,plain,
( ! [X0] :
( ~ product(X0,e_1,e_4)
| equalish(X0,e_5) )
| ~ spl0_55 ),
inference(resolution,[],[f626,f56]) ).
fof(f732,plain,
( ~ cycle(e_4,e_0)
| ~ greater(e_5,e_4)
| ~ spl0_59 ),
inference(resolution,[],[f643,f26]) ).
fof(f736,plain,
( ! [X0] :
( ~ product(e_1,e_4,X0)
| product(X0,e_5,e_1) )
| ~ spl0_59 ),
inference(resolution,[],[f643,f58]) ).
fof(f737,plain,
( ~ cycle(e_4,e_0)
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f732,f20]) ).
fof(f742,definition,
( spl0_78
<=> ! [X0] :
( ~ cycle(e_4,X0)
| ~ greater(X0,e_0) ) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f743,plain,
( ! [X0] :
( ~ cycle(e_4,X0)
| ~ greater(X0,e_0) )
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f742]) ).
fof(f745,plain,
( ~ spl0_9
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f737,f641,f112]) ).
fof(f746,plain,
( ! [X0,X1] :
( ~ cycle(e_3,X0)
| ~ greater(X0,e_0)
| ~ next(e_3,X1)
| equalish(e_5,X1) )
| ~ spl0_64 ),
inference(resolution,[],[f664,f27]) ).
fof(f747,plain,
( ~ cycle(e_3,e_0)
| ~ greater(e_5,e_3)
| ~ spl0_64 ),
inference(resolution,[],[f664,f26]) ).
fof(f752,plain,
( ~ greater(e_5,e_3)
| ~ spl0_14
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f747,f135]) ).
fof(f754,definition,
( spl0_79
<=> ! [X1] :
( ~ next(e_3,X1)
| equalish(e_5,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f755,plain,
( ! [X1] :
( ~ next(e_3,X1)
| equalish(e_5,X1) )
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f754]) ).
fof(f757,definition,
( spl0_80
<=> ! [X0] :
( ~ cycle(e_3,X0)
| ~ greater(X0,e_0) ) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f758,plain,
( ! [X0] :
( ~ cycle(e_3,X0)
| ~ greater(X0,e_0) )
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f759,plain,
( spl0_79
| spl0_80
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f746,f662,f757,f754]) ).
fof(f760,plain,
( $false
| ~ spl0_14
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f752,f19]) ).
fof(f761,plain,
( ~ spl0_14
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f760]) ).
fof(f794,plain,
( equalish(e_2,e_1)
| ~ spl0_73 ),
inference(resolution,[],[f701,f77]) ).
fof(f795,plain,
( $false
| ~ spl0_73 ),
inference(forward_subsumption_resolution,[],[f794,f37]) ).
fof(f796,plain,
~ spl0_73,
inference(avatar_contradiction_clause,[],[f795]) ).
fof(f798,definition,
( spl0_81
<=> ! [X0] :
( ~ cycle(e_2,X0)
| ~ greater(X0,e_0) ) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f799,plain,
( ! [X0] :
( ~ cycle(e_2,X0)
| ~ greater(X0,e_0) )
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f798]) ).
fof(f801,plain,
( ! [X0,X1] :
( ~ cycle(e_2,X0)
| ~ greater(X0,e_0)
| ~ next(e_2,X1)
| equalish(e_5,X1) )
| ~ spl0_69 ),
inference(resolution,[],[f685,f27]) ).
fof(f802,plain,
( ~ cycle(e_2,e_0)
| ~ greater(e_5,e_2)
| ~ spl0_69 ),
inference(resolution,[],[f685,f26]) ).
fof(f807,plain,
( ~ cycle(e_2,e_0)
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f802,f17]) ).
fof(f809,definition,
( spl0_82
<=> ! [X1] :
( ~ next(e_2,X1)
| equalish(e_5,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f810,plain,
( ! [X1] :
( ~ next(e_2,X1)
| equalish(e_5,X1) )
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f809]) ).
fof(f811,plain,
( spl0_82
| spl0_81
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f801,f683,f798,f809]) ).
fof(f812,plain,
( ~ spl0_19
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f807,f683,f154]) ).
fof(f813,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5) ),
inference(resolution,[],[f610,f28]) ).
fof(f817,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)
| product(e_5,e_2,e_5) ),
inference(resolution,[],[f610,f32]) ).
fof(f819,definition,
( spl0_83
<=> product(e_5,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f821,plain,
( product(e_5,e_2,e_5)
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f819]) ).
fof(f823,definition,
( spl0_84
<=> product(e_5,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f825,plain,
( product(e_5,e_2,e_4)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f823]) ).
fof(f827,definition,
( spl0_85
<=> product(e_5,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f828,plain,
( ~ product(e_5,e_2,e_3)
| spl0_85 ),
inference(avatar_component_clause,[],[f827]) ).
fof(f829,plain,
( product(e_5,e_2,e_3)
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f827]) ).
fof(f831,definition,
( spl0_86
<=> product(e_5,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f833,plain,
( product(e_5,e_2,e_2)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f831]) ).
fof(f835,definition,
( spl0_87
<=> product(e_5,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f837,plain,
( product(e_5,e_2,e_1)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f835]) ).
fof(f838,plain,
( spl0_83
| spl0_84
| spl0_85
| spl0_86
| spl0_87 ),
inference(avatar_split_clause,[],[f817,f835,f831,f827,f823,f819]) ).
fof(f882,definition,
( spl0_98
<=> product(e_1,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f884,plain,
( product(e_1,e_2,e_5)
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f882]) ).
fof(f886,definition,
( spl0_99
<=> product(e_1,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f887,plain,
( ~ product(e_1,e_2,e_4)
| spl0_99 ),
inference(avatar_component_clause,[],[f886]) ).
fof(f888,plain,
( product(e_1,e_2,e_4)
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f886]) ).
fof(f890,definition,
( spl0_100
<=> product(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f891,plain,
( ~ product(e_1,e_2,e_3)
| spl0_100 ),
inference(avatar_component_clause,[],[f890]) ).
fof(f892,plain,
( product(e_1,e_2,e_3)
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f890]) ).
fof(f894,definition,
( spl0_101
<=> product(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f896,plain,
( product(e_1,e_2,e_2)
| ~ spl0_101 ),
inference(avatar_component_clause,[],[f894]) ).
fof(f898,definition,
( spl0_102
<=> product(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f900,plain,
( product(e_1,e_2,e_1)
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f898]) ).
fof(f901,plain,
( spl0_98
| spl0_99
| spl0_100
| spl0_101
| spl0_102 ),
inference(avatar_split_clause,[],[f813,f898,f894,f890,f886,f882]) ).
fof(f906,plain,
( equalish(e_2,e_5)
| ~ spl0_83 ),
inference(resolution,[],[f821,f75]) ).
fof(f907,plain,
( $false
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f906,f40]) ).
fof(f908,plain,
~ spl0_83,
inference(avatar_contradiction_clause,[],[f907]) ).
fof(f926,plain,
( equalish(e_2,e_1)
| ~ spl0_102 ),
inference(resolution,[],[f900,f75]) ).
fof(f927,plain,
( $false
| ~ spl0_102 ),
inference(forward_subsumption_resolution,[],[f926,f37]) ).
fof(f928,plain,
~ spl0_102,
inference(avatar_contradiction_clause,[],[f927]) ).
fof(f943,plain,
( ! [X0,X1] :
( ~ cycle(e_2,X0)
| ~ greater(X0,e_0)
| ~ next(e_2,X1)
| equalish(e_4,X1) )
| ~ spl0_70 ),
inference(resolution,[],[f689,f27]) ).
fof(f950,definition,
( spl0_103
<=> ! [X1] :
( ~ next(e_2,X1)
| equalish(e_4,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f951,plain,
( ! [X1] :
( ~ next(e_2,X1)
| equalish(e_4,X1) )
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f950]) ).
fof(f952,plain,
( spl0_103
| spl0_81
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f943,f687,f798,f950]) ).
fof(f972,plain,
( ~ greater(e_1,e_0)
| ~ spl0_8
| ~ spl0_78 ),
inference(resolution,[],[f743,f110]) ).
fof(f973,plain,
( $false
| ~ spl0_8
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f972,f6]) ).
fof(f974,plain,
( ~ spl0_8
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f973]) ).
fof(f976,plain,
( ~ greater(e_2,e_0)
| ~ spl0_12
| ~ spl0_80 ),
inference(resolution,[],[f758,f127]) ).
fof(f977,plain,
( $false
| ~ spl0_12
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f976,f7]) ).
fof(f978,plain,
( ~ spl0_12
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f977]) ).
fof(f979,plain,
( ~ greater(e_4,e_0)
| ~ spl0_10
| ~ spl0_80 ),
inference(resolution,[],[f119,f758]) ).
fof(f992,plain,
( $false
| ~ spl0_10
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f979,f9]) ).
fof(f993,plain,
( ~ spl0_10
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f992]) ).
fof(f999,plain,
( ! [X0] :
( ~ product(e_1,e_3,X0)
| product(X0,e_4,e_1) )
| ~ spl0_65 ),
inference(resolution,[],[f668,f58]) ).
fof(f1005,plain,
( equalish(e_4,e_2)
| ~ spl0_39 ),
inference(resolution,[],[f337,f2]) ).
fof(f1006,plain,
( $false
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1005,f46]) ).
fof(f1007,plain,
~ spl0_39,
inference(avatar_contradiction_clause,[],[f1006]) ).
fof(f1023,plain,
( equalish(e_5,e_3)
| ~ spl0_82 ),
inference(resolution,[],[f810,f3]) ).
fof(f1024,plain,
( $false
| ~ spl0_82 ),
inference(forward_subsumption_resolution,[],[f1023,f51]) ).
fof(f1025,plain,
~ spl0_82,
inference(avatar_contradiction_clause,[],[f1024]) ).
fof(f1026,plain,
( equalish(e_4,e_3)
| ~ spl0_103 ),
inference(resolution,[],[f951,f3]) ).
fof(f1027,plain,
( $false
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f1026,f47]) ).
fof(f1028,plain,
~ spl0_103,
inference(avatar_contradiction_clause,[],[f1027]) ).
fof(f1035,plain,
( ! [X0] :
( ~ product(e_1,e_2,X0)
| product(X0,e_3,e_1) )
| ~ spl0_71 ),
inference(resolution,[],[f693,f58]) ).
fof(f1047,plain,
( product(e_5,e_3,e_1)
| ~ spl0_71
| ~ spl0_98 ),
inference(resolution,[],[f1035,f884]) ).
fof(f1060,plain,
( equalish(e_3,e_5)
| ~ spl0_55
| ~ spl0_65 ),
inference(resolution,[],[f722,f668]) ).
fof(f1062,plain,
( $false
| ~ spl0_55
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f1060,f44]) ).
fof(f1063,plain,
( ~ spl0_55
| ~ spl0_65 ),
inference(avatar_contradiction_clause,[],[f1062]) ).
fof(f1075,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_5) ),
inference(resolution,[],[f611,f28]) ).
fof(f1078,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_4)
| product(e_4,e_3,e_5) ),
inference(resolution,[],[f611,f31]) ).
fof(f1081,definition,
( spl0_107
<=> product(e_4,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f1083,plain,
( product(e_4,e_3,e_5)
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f1081]) ).
fof(f1085,definition,
( spl0_108
<=> product(e_4,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f1087,plain,
( product(e_4,e_3,e_4)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f1085]) ).
fof(f1089,definition,
( spl0_109
<=> product(e_4,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f1091,plain,
( product(e_4,e_3,e_3)
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f1089]) ).
fof(f1093,definition,
( spl0_110
<=> product(e_4,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f1095,plain,
( product(e_4,e_3,e_2)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f1093]) ).
fof(f1097,definition,
( spl0_111
<=> product(e_4,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f1099,plain,
( product(e_4,e_3,e_1)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f1097]) ).
fof(f1100,plain,
( spl0_107
| spl0_108
| spl0_109
| spl0_110
| spl0_111 ),
inference(avatar_split_clause,[],[f1078,f1097,f1093,f1089,f1085,f1081]) ).
fof(f1102,definition,
( spl0_112
<=> product(e_2,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f1103,plain,
( ~ product(e_2,e_3,e_5)
| spl0_112 ),
inference(avatar_component_clause,[],[f1102]) ).
fof(f1104,plain,
( product(e_2,e_3,e_5)
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f1102]) ).
fof(f1123,definition,
( spl0_117
<=> product(e_1,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f1125,plain,
( product(e_1,e_3,e_5)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f1123]) ).
fof(f1127,definition,
( spl0_118
<=> product(e_1,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f1129,plain,
( product(e_1,e_3,e_4)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f1127]) ).
fof(f1131,definition,
( spl0_119
<=> product(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f1133,plain,
( product(e_1,e_3,e_3)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f1131]) ).
fof(f1135,definition,
( spl0_120
<=> product(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f1137,plain,
( product(e_1,e_3,e_2)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f1135]) ).
fof(f1139,definition,
( spl0_121
<=> product(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f1141,plain,
( product(e_1,e_3,e_1)
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f1139]) ).
fof(f1142,plain,
( spl0_117
| spl0_118
| spl0_119
| spl0_120
| spl0_121 ),
inference(avatar_split_clause,[],[f1075,f1139,f1135,f1131,f1127,f1123]) ).
fof(f1146,plain,
( ! [X0] :
( ~ product(e_3,e_4,X0)
| product(X0,e_5,e_3) )
| ~ spl0_107 ),
inference(resolution,[],[f1083,f58]) ).
fof(f1191,plain,
( equalish(e_3,e_1)
| ~ spl0_121 ),
inference(resolution,[],[f1141,f75]) ).
fof(f1192,plain,
( $false
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f1191,f41]) ).
fof(f1193,plain,
~ spl0_121,
inference(avatar_contradiction_clause,[],[f1192]) ).
fof(f1196,plain,
( product(e_2,e_4,e_1)
| ~ spl0_65
| ~ spl0_120 ),
inference(resolution,[],[f1137,f999]) ).
fof(f1200,plain,
( ! [X0] :
( ~ product(e_3,e_1,X0)
| product(X0,e_2,e_3) )
| ~ spl0_120 ),
inference(resolution,[],[f1137,f58]) ).
fof(f1222,plain,
( equalish(e_1,e_3)
| ~ spl0_66 ),
inference(resolution,[],[f672,f75]) ).
fof(f1223,plain,
( $false
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f1222,f34]) ).
fof(f1224,plain,
~ spl0_66,
inference(avatar_contradiction_clause,[],[f1223]) ).
fof(f1227,plain,
( product(e_2,e_2,e_3)
| ~ spl0_67
| ~ spl0_120 ),
inference(resolution,[],[f676,f1200]) ).
fof(f1248,plain,
( equalish(e_3,e_1)
| ~ spl0_68 ),
inference(resolution,[],[f680,f77]) ).
fof(f1249,plain,
( $false
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f1248,f41]) ).
fof(f1250,plain,
~ spl0_68,
inference(avatar_contradiction_clause,[],[f1249]) ).
fof(f1273,definition,
( spl0_128
<=> product(e_5,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f1274,plain,
( ~ product(e_5,e_3,e_1)
| spl0_128 ),
inference(avatar_component_clause,[],[f1273]) ).
fof(f1275,plain,
( product(e_5,e_3,e_1)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f1273]) ).
fof(f1291,plain,
( ! [X0] :
( ~ product(e_2,X0,e_1)
| equalish(X0,e_4) )
| ~ spl0_65
| ~ spl0_120 ),
inference(resolution,[],[f1196,f55]) ).
fof(f1323,plain,
( ~ cycle(e_3,e_0)
| ~ greater(e_4,e_3)
| ~ spl0_65 ),
inference(resolution,[],[f668,f26]) ).
fof(f1327,plain,
( ! [X0] :
( ~ product(e_1,e_3,X0)
| product(X0,e_4,e_1) )
| ~ spl0_65 ),
inference(resolution,[],[f668,f58]) ).
fof(f1337,plain,
( equalish(e_1,e_2)
| ~ spl0_72 ),
inference(resolution,[],[f697,f75]) ).
fof(f1338,plain,
( $false
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f1337,f33]) ).
fof(f1339,plain,
~ spl0_72,
inference(avatar_contradiction_clause,[],[f1338]) ).
fof(f1380,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4)
| product(e_1,e_4,e_5) ),
inference(resolution,[],[f612,f28]) ).
fof(f1382,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| product(e_3,e_4,e_4)
| product(e_3,e_4,e_5) ),
inference(resolution,[],[f612,f30]) ).
fof(f1386,definition,
( spl0_130
<=> product(e_3,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f1388,plain,
( product(e_3,e_4,e_5)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f1386]) ).
fof(f1390,definition,
( spl0_131
<=> product(e_3,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f1392,plain,
( product(e_3,e_4,e_4)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f1390]) ).
fof(f1394,definition,
( spl0_132
<=> product(e_3,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f1396,plain,
( product(e_3,e_4,e_3)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f1394]) ).
fof(f1398,definition,
( spl0_133
<=> product(e_3,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f1400,plain,
( product(e_3,e_4,e_2)
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f1398]) ).
fof(f1402,definition,
( spl0_134
<=> product(e_3,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f1404,plain,
( product(e_3,e_4,e_1)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f1402]) ).
fof(f1405,plain,
( spl0_130
| spl0_131
| spl0_132
| spl0_133
| spl0_134 ),
inference(avatar_split_clause,[],[f1382,f1402,f1398,f1394,f1390,f1386]) ).
fof(f1407,definition,
( spl0_135
<=> product(e_1,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f1409,plain,
( product(e_1,e_4,e_5)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f1407]) ).
fof(f1411,definition,
( spl0_136
<=> product(e_1,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f1413,plain,
( product(e_1,e_4,e_4)
| ~ spl0_136 ),
inference(avatar_component_clause,[],[f1411]) ).
fof(f1415,definition,
( spl0_137
<=> product(e_1,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f1417,plain,
( product(e_1,e_4,e_3)
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f1415]) ).
fof(f1419,definition,
( spl0_138
<=> product(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f1421,plain,
( product(e_1,e_4,e_2)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f1419]) ).
fof(f1423,definition,
( spl0_139
<=> product(e_1,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f1425,plain,
( product(e_1,e_4,e_1)
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f1423]) ).
fof(f1426,plain,
( spl0_135
| spl0_136
| spl0_137
| spl0_138
| spl0_139 ),
inference(avatar_split_clause,[],[f1380,f1423,f1419,f1415,f1411,f1407]) ).
fof(f1501,plain,
( ! [X0] :
( ~ product(e_3,e_5,X0)
| product(X0,e_1,e_3) )
| ~ spl0_128 ),
inference(resolution,[],[f1275,f58]) ).
fof(f1502,plain,
( product(e_5,e_5,e_3)
| ~ spl0_107
| ~ spl0_130 ),
inference(resolution,[],[f1388,f1146]) ).
fof(f1508,plain,
( equalish(e_3,e_5)
| ~ spl0_107
| ~ spl0_130 ),
inference(resolution,[],[f1502,f73]) ).
fof(f1514,plain,
( $false
| ~ spl0_107
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f1508,f44]) ).
fof(f1515,plain,
( ~ spl0_107
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f1514]) ).
fof(f1523,plain,
( equalish(e_3,e_4)
| ~ spl0_108 ),
inference(resolution,[],[f1087,f75]) ).
fof(f1524,plain,
( $false
| ~ spl0_108 ),
inference(forward_subsumption_resolution,[],[f1523,f43]) ).
fof(f1525,plain,
~ spl0_108,
inference(avatar_contradiction_clause,[],[f1524]) ).
fof(f1531,plain,
( equalish(e_4,e_3)
| ~ spl0_109 ),
inference(resolution,[],[f1091,f77]) ).
fof(f1532,plain,
( $false
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f1531,f47]) ).
fof(f1533,plain,
~ spl0_109,
inference(avatar_contradiction_clause,[],[f1532]) ).
fof(f1538,plain,
( ! [X0] :
( ~ product(e_3,e_4,X0)
| product(X0,e_2,e_3) )
| ~ spl0_110 ),
inference(resolution,[],[f1095,f58]) ).
fof(f1555,plain,
( product(e_5,e_2,e_3)
| ~ spl0_110
| ~ spl0_130 ),
inference(resolution,[],[f1538,f1388]) ).
fof(f1562,plain,
( product(e_5,e_5,e_1)
| ~ spl0_59
| ~ spl0_135 ),
inference(resolution,[],[f1409,f736]) ).
fof(f1568,plain,
( equalish(e_1,e_5)
| ~ spl0_59
| ~ spl0_135 ),
inference(resolution,[],[f1562,f73]) ).
fof(f1574,plain,
( $false
| ~ spl0_59
| ~ spl0_135 ),
inference(forward_subsumption_resolution,[],[f1568,f36]) ).
fof(f1575,plain,
( ~ spl0_59
| ~ spl0_135 ),
inference(avatar_contradiction_clause,[],[f1574]) ).
fof(f1583,plain,
( equalish(e_1,e_4)
| ~ spl0_136 ),
inference(resolution,[],[f1413,f77]) ).
fof(f1584,plain,
( $false
| ~ spl0_136 ),
inference(forward_subsumption_resolution,[],[f1583,f35]) ).
fof(f1585,plain,
~ spl0_136,
inference(avatar_contradiction_clause,[],[f1584]) ).
fof(f1592,plain,
( equalish(e_4,e_1)
| ~ spl0_139 ),
inference(resolution,[],[f1425,f75]) ).
fof(f1593,plain,
( $false
| ~ spl0_139 ),
inference(forward_subsumption_resolution,[],[f1592,f45]) ).
fof(f1594,plain,
~ spl0_139,
inference(avatar_contradiction_clause,[],[f1593]) ).
fof(f1598,plain,
( product(e_3,e_5,e_1)
| ~ spl0_59
| ~ spl0_137 ),
inference(resolution,[],[f1417,f736]) ).
fof(f1605,plain,
( product(e_2,e_5,e_1)
| ~ spl0_59
| ~ spl0_138 ),
inference(resolution,[],[f1421,f736]) ).
fof(f1612,plain,
( equalish(e_5,e_4)
| ~ spl0_59
| ~ spl0_65
| ~ spl0_120
| ~ spl0_138 ),
inference(resolution,[],[f1605,f1291]) ).
fof(f1620,plain,
( $false
| ~ spl0_59
| ~ spl0_65
| ~ spl0_120
| ~ spl0_138 ),
inference(forward_subsumption_resolution,[],[f1612,f52]) ).
fof(f1621,plain,
( ~ spl0_59
| ~ spl0_65
| ~ spl0_120
| ~ spl0_138 ),
inference(avatar_contradiction_clause,[],[f1620]) ).
fof(f1624,plain,
( product(e_1,e_1,e_3)
| ~ spl0_59
| ~ spl0_128
| ~ spl0_137 ),
inference(resolution,[],[f1598,f1501]) ).
fof(f1634,plain,
( equalish(e_3,e_1)
| ~ spl0_59
| ~ spl0_128
| ~ spl0_137 ),
inference(resolution,[],[f1624,f73]) ).
fof(f1642,plain,
( $false
| ~ spl0_59
| ~ spl0_128
| ~ spl0_137 ),
inference(forward_subsumption_resolution,[],[f1634,f41]) ).
fof(f1643,plain,
( ~ spl0_59
| ~ spl0_128
| ~ spl0_137 ),
inference(avatar_contradiction_clause,[],[f1642]) ).
fof(f1660,plain,
( equalish(e_4,e_1)
| ~ spl0_63 ),
inference(resolution,[],[f659,f77]) ).
fof(f1661,plain,
( $false
| ~ spl0_63 ),
inference(forward_subsumption_resolution,[],[f1660,f45]) ).
fof(f1662,plain,
~ spl0_63,
inference(avatar_contradiction_clause,[],[f1661]) ).
fof(f1670,plain,
( equalish(e_1,e_4)
| ~ spl0_60 ),
inference(resolution,[],[f647,f75]) ).
fof(f1671,plain,
( $false
| ~ spl0_60 ),
inference(forward_subsumption_resolution,[],[f1670,f35]) ).
fof(f1672,plain,
~ spl0_60,
inference(avatar_contradiction_clause,[],[f1671]) ).
fof(f1681,plain,
( product(e_2,e_5,e_1)
| product(e_2,e_5,e_2)
| product(e_2,e_5,e_3)
| product(e_2,e_5,e_4)
| product(e_2,e_5,e_5) ),
inference(resolution,[],[f613,f29]) ).
fof(f1736,definition,
( spl0_157
<=> product(e_1,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1738,plain,
( product(e_1,e_5,e_3)
| ~ spl0_157 ),
inference(avatar_component_clause,[],[f1736]) ).
fof(f1757,plain,
( equalish(e_1,e_2)
| ~ spl0_101 ),
inference(resolution,[],[f896,f77]) ).
fof(f1758,plain,
( $false
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f1757,f33]) ).
fof(f1759,plain,
~ spl0_101,
inference(avatar_contradiction_clause,[],[f1758]) ).
fof(f1786,definition,
( spl0_160
<=> product(e_2,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1788,plain,
( product(e_2,e_5,e_5)
| ~ spl0_160 ),
inference(avatar_component_clause,[],[f1786]) ).
fof(f1790,definition,
( spl0_161
<=> product(e_2,e_5,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1792,plain,
( product(e_2,e_5,e_4)
| ~ spl0_161 ),
inference(avatar_component_clause,[],[f1790]) ).
fof(f1794,definition,
( spl0_162
<=> product(e_2,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1795,plain,
( ~ product(e_2,e_5,e_3)
| spl0_162 ),
inference(avatar_component_clause,[],[f1794]) ).
fof(f1796,plain,
( product(e_2,e_5,e_3)
| ~ spl0_162 ),
inference(avatar_component_clause,[],[f1794]) ).
fof(f1798,definition,
( spl0_163
<=> product(e_2,e_5,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1800,plain,
( product(e_2,e_5,e_2)
| ~ spl0_163 ),
inference(avatar_component_clause,[],[f1798]) ).
fof(f1802,definition,
( spl0_164
<=> product(e_2,e_5,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1804,plain,
( product(e_2,e_5,e_1)
| ~ spl0_164 ),
inference(avatar_component_clause,[],[f1802]) ).
fof(f1805,plain,
( spl0_160
| spl0_161
| spl0_162
| spl0_163
| spl0_164 ),
inference(avatar_split_clause,[],[f1681,f1802,f1798,f1794,f1790,f1786]) ).
fof(f1824,plain,
( ! [X0] :
( ~ product(e_3,e_4,X0)
| product(X0,e_5,e_3) )
| ~ spl0_107 ),
inference(resolution,[],[f1083,f58]) ).
fof(f1853,plain,
( ! [X0,X1] :
( ~ cycle(e_4,X0)
| ~ greater(X0,e_0)
| ~ next(e_4,X1)
| equalish(e_2,X1) )
| ~ spl0_62 ),
inference(resolution,[],[f655,f27]) ).
fof(f1860,definition,
( spl0_165
<=> ! [X1] :
( ~ next(e_4,X1)
| equalish(e_2,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1861,plain,
( ! [X1] :
( ~ next(e_4,X1)
| equalish(e_2,X1) )
| ~ spl0_165 ),
inference(avatar_component_clause,[],[f1860]) ).
fof(f1862,plain,
( spl0_165
| spl0_78
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f1853,f653,f742,f1860]) ).
fof(f1868,plain,
( equalish(e_4,e_3)
| ~ spl0_132 ),
inference(resolution,[],[f1396,f75]) ).
fof(f1869,plain,
( $false
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f1868,f47]) ).
fof(f1870,plain,
~ spl0_132,
inference(avatar_contradiction_clause,[],[f1869]) ).
fof(f1876,plain,
( equalish(e_3,e_4)
| ~ spl0_131 ),
inference(resolution,[],[f1392,f77]) ).
fof(f1877,plain,
( $false
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f1876,f43]) ).
fof(f1878,plain,
~ spl0_131,
inference(avatar_contradiction_clause,[],[f1877]) ).
fof(f1880,plain,
( product(e_2,e_5,e_3)
| ~ spl0_107
| ~ spl0_133 ),
inference(resolution,[],[f1400,f1824]) ).
fof(f1884,plain,
( ! [X0] :
( ~ product(e_4,e_3,X0)
| product(X0,e_2,e_4) )
| ~ spl0_133 ),
inference(resolution,[],[f1400,f58]) ).
fof(f1885,plain,
( spl0_162
| ~ spl0_107
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f1880,f1398,f1081,f1794]) ).
fof(f2111,plain,
( product(e_2,e_2,e_4)
| ~ spl0_110
| ~ spl0_133 ),
inference(resolution,[],[f1095,f1884]) ).
fof(f2115,plain,
( ! [X0] :
( ~ product(e_3,e_4,X0)
| product(X0,e_2,e_3) )
| ~ spl0_110 ),
inference(resolution,[],[f1095,f58]) ).
fof(f2116,plain,
( equalish(e_4,e_2)
| ~ spl0_110
| ~ spl0_133 ),
inference(resolution,[],[f2111,f73]) ).
fof(f2123,plain,
( $false
| ~ spl0_110
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f2116,f46]) ).
fof(f2124,plain,
( ~ spl0_110
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f2123]) ).
fof(f2125,plain,
( product(e_1,e_2,e_3)
| ~ spl0_110
| ~ spl0_134 ),
inference(resolution,[],[f1404,f2115]) ).
fof(f2126,plain,
( product(e_1,e_5,e_3)
| ~ spl0_107
| ~ spl0_134 ),
inference(resolution,[],[f1404,f1824]) ).
fof(f2134,plain,
( spl0_157
| ~ spl0_107
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f2126,f1402,f1081,f1736]) ).
fof(f2153,plain,
( ! [X0] :
( ~ product(e_4,e_3,X0)
| product(X0,e_2,e_4) )
| ~ spl0_133 ),
inference(resolution,[],[f1400,f58]) ).
fof(f2238,plain,
( product(e_4,e_4,e_1)
| ~ spl0_65
| ~ spl0_118 ),
inference(resolution,[],[f1129,f1327]) ).
fof(f2244,plain,
( equalish(e_1,e_4)
| ~ spl0_65
| ~ spl0_118 ),
inference(resolution,[],[f2238,f73]) ).
fof(f2252,plain,
( $false
| ~ spl0_65
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f2244,f35]) ).
fof(f2253,plain,
( ~ spl0_65
| ~ spl0_118 ),
inference(avatar_contradiction_clause,[],[f2252]) ).
fof(f2312,plain,
( equalish(e_5,e_1)
| ~ spl0_58 ),
inference(resolution,[],[f638,f77]) ).
fof(f2313,plain,
( $false
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f2312,f49]) ).
fof(f2314,plain,
~ spl0_58,
inference(avatar_contradiction_clause,[],[f2313]) ).
fof(f2356,plain,
( ! [X0] :
( ~ product(e_5,e_1,X0)
| product(X0,e_3,e_5) )
| ~ spl0_157 ),
inference(resolution,[],[f1738,f58]) ).
fof(f2357,plain,
( product(e_2,e_3,e_5)
| ~ spl0_57
| ~ spl0_157 ),
inference(resolution,[],[f2356,f634]) ).
fof(f2358,plain,
( $false
| ~ spl0_57
| spl0_112
| ~ spl0_157 ),
inference(forward_subsumption_resolution,[],[f2357,f1103]) ).
fof(f2359,plain,
( ~ spl0_57
| spl0_112
| ~ spl0_157 ),
inference(avatar_contradiction_clause,[],[f2358]) ).
fof(f2362,plain,
( ! [X0] :
( ~ product(X0,e_1,e_3)
| equalish(X0,e_5) )
| ~ spl0_56 ),
inference(resolution,[],[f630,f56]) ).
fof(f2376,plain,
( product(e_1,e_2,e_4)
| ~ spl0_111
| ~ spl0_133 ),
inference(resolution,[],[f1099,f2153]) ).
fof(f2380,plain,
( ! [X0] :
( ~ product(e_3,e_4,X0)
| product(X0,e_1,e_3) )
| ~ spl0_111 ),
inference(resolution,[],[f1099,f58]) ).
fof(f2381,plain,
( $false
| spl0_99
| ~ spl0_111
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f2376,f887]) ).
fof(f2382,plain,
( spl0_99
| ~ spl0_111
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f2381]) ).
fof(f2399,plain,
( equalish(e_5,e_4)
| ~ spl0_65
| ~ spl0_120
| ~ spl0_164 ),
inference(resolution,[],[f1804,f1291]) ).
fof(f2404,plain,
( $false
| ~ spl0_65
| ~ spl0_120
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f2399,f52]) ).
fof(f2405,plain,
( ~ spl0_65
| ~ spl0_120
| ~ spl0_164 ),
inference(avatar_contradiction_clause,[],[f2404]) ).
fof(f2414,plain,
( equalish(e_5,e_2)
| ~ spl0_163 ),
inference(resolution,[],[f1800,f75]) ).
fof(f2415,plain,
( $false
| ~ spl0_163 ),
inference(forward_subsumption_resolution,[],[f2414,f50]) ).
fof(f2416,plain,
~ spl0_163,
inference(avatar_contradiction_clause,[],[f2415]) ).
fof(f2425,plain,
( equalish(e_2,e_5)
| ~ spl0_160 ),
inference(resolution,[],[f1788,f77]) ).
fof(f2426,plain,
( $false
| ~ spl0_160 ),
inference(forward_subsumption_resolution,[],[f2425,f40]) ).
fof(f2427,plain,
~ spl0_160,
inference(avatar_contradiction_clause,[],[f2426]) ).
fof(f2444,plain,
( equalish(e_5,e_2)
| ~ spl0_86 ),
inference(resolution,[],[f833,f77]) ).
fof(f2445,plain,
( $false
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f2444,f50]) ).
fof(f2446,plain,
~ spl0_86,
inference(avatar_contradiction_clause,[],[f2445]) ).
fof(f2458,plain,
( equalish(e_3,e_2)
| ~ spl0_67
| ~ spl0_120 ),
inference(resolution,[],[f1227,f73]) ).
fof(f2466,plain,
( $false
| ~ spl0_67
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f2458,f42]) ).
fof(f2467,plain,
( ~ spl0_67
| ~ spl0_120 ),
inference(avatar_contradiction_clause,[],[f2466]) ).
fof(f2471,plain,
( ! [X0] :
( ~ product(e_2,e_5,X0)
| product(X0,e_4,e_2) )
| ~ spl0_84 ),
inference(resolution,[],[f825,f58]) ).
fof(f2472,plain,
( product(e_4,e_4,e_2)
| ~ spl0_84
| ~ spl0_161 ),
inference(resolution,[],[f1792,f2471]) ).
fof(f2476,plain,
( ! [X0] :
( ~ product(e_5,e_2,X0)
| product(X0,e_4,e_5) )
| ~ spl0_161 ),
inference(resolution,[],[f1792,f58]) ).
fof(f2477,plain,
( equalish(e_2,e_4)
| ~ spl0_84
| ~ spl0_161 ),
inference(resolution,[],[f2472,f73]) ).
fof(f2483,plain,
( $false
| ~ spl0_84
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f2477,f39]) ).
fof(f2484,plain,
( ~ spl0_84
| ~ spl0_161 ),
inference(avatar_contradiction_clause,[],[f2483]) ).
fof(f2485,plain,
( product(e_1,e_4,e_5)
| ~ spl0_87
| ~ spl0_161 ),
inference(resolution,[],[f837,f2476]) ).
fof(f2489,plain,
( ! [X0] :
( ~ product(e_2,e_5,X0)
| product(X0,e_1,e_2) )
| ~ spl0_87 ),
inference(resolution,[],[f837,f58]) ).
fof(f2541,plain,
( ! [X0] :
( ~ product(e_2,e_1,X0)
| product(X0,e_3,e_2) )
| ~ spl0_100 ),
inference(resolution,[],[f892,f58]) ).
fof(f2553,plain,
( ~ greater(e_3,e_0)
| ~ spl0_16
| ~ spl0_81 ),
inference(resolution,[],[f799,f144]) ).
fof(f2554,plain,
( $false
| ~ spl0_16
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f2553,f8]) ).
fof(f2555,plain,
( ~ spl0_16
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f2554]) ).
fof(f2556,plain,
( ~ greater(e_4,e_3)
| ~ spl0_14
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f1323,f135]) ).
fof(f2557,plain,
( $false
| ~ spl0_14
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f2556,f18]) ).
fof(f2558,plain,
( ~ spl0_14
| ~ spl0_65 ),
inference(avatar_contradiction_clause,[],[f2557]) ).
fof(f2576,plain,
( ~ greater(e_4,e_0)
| ~ spl0_15
| ~ spl0_81 ),
inference(resolution,[],[f140,f799]) ).
fof(f2586,plain,
( $false
| ~ spl0_15
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f2576,f9]) ).
fof(f2587,plain,
( ~ spl0_15
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f2586]) ).
fof(f2588,plain,
( ~ greater(e_2,e_0)
| ~ spl0_17
| ~ spl0_81 ),
inference(resolution,[],[f148,f799]) ).
fof(f2598,plain,
( $false
| ~ spl0_17
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f2588,f7]) ).
fof(f2599,plain,
( ~ spl0_17
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f2598]) ).
fof(f2600,plain,
( ~ greater(e_1,e_0)
| ~ spl0_18
| ~ spl0_81 ),
inference(resolution,[],[f152,f799]) ).
fof(f2610,plain,
( $false
| ~ spl0_18
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f2600,f6]) ).
fof(f2611,plain,
( ~ spl0_18
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f2610]) ).
fof(f2612,plain,
( $false
| spl0_85
| ~ spl0_110
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f1555,f828]) ).
fof(f2613,plain,
( spl0_85
| ~ spl0_110
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f2612]) ).
fof(f2631,definition,
( spl0_168
<=> product(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f2633,plain,
( product(e_2,e_4,e_3)
| ~ spl0_168 ),
inference(avatar_component_clause,[],[f2631]) ).
fof(f2666,plain,
( ~ cycle(e_2,e_0)
| ~ greater(e_4,e_2)
| ~ spl0_70 ),
inference(resolution,[],[f689,f26]) ).
fof(f2671,plain,
( ~ greater(e_4,e_2)
| ~ spl0_19
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f2666,f156]) ).
fof(f2672,plain,
( $false
| ~ spl0_19
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f2671,f16]) ).
fof(f2673,plain,
( ~ spl0_19
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f2672]) ).
fof(f2674,plain,
( product(e_3,e_3,e_2)
| ~ spl0_71
| ~ spl0_100 ),
inference(resolution,[],[f693,f2541]) ).
fof(f2676,plain,
( ~ cycle(e_2,e_0)
| ~ greater(e_3,e_2)
| ~ spl0_71 ),
inference(resolution,[],[f693,f26]) ).
fof(f2677,plain,
( ! [X0] :
( ~ product(X0,e_1,e_3)
| equalish(X0,e_2) )
| ~ spl0_71 ),
inference(resolution,[],[f693,f56]) ).
fof(f2678,plain,
( ! [X0] :
( ~ product(e_2,X0,e_3)
| equalish(X0,e_1) )
| ~ spl0_71 ),
inference(resolution,[],[f693,f55]) ).
fof(f2681,plain,
( ~ greater(e_3,e_2)
| ~ spl0_19
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f2676,f156]) ).
fof(f2682,plain,
( $false
| ~ spl0_19
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f2681,f15]) ).
fof(f2683,plain,
( ~ spl0_19
| ~ spl0_71 ),
inference(avatar_contradiction_clause,[],[f2682]) ).
fof(f2684,plain,
( equalish(e_2,e_3)
| ~ spl0_71
| ~ spl0_100 ),
inference(resolution,[],[f2674,f73]) ).
fof(f2692,plain,
( $false
| ~ spl0_71
| ~ spl0_100 ),
inference(forward_subsumption_resolution,[],[f2684,f38]) ).
fof(f2693,plain,
( ~ spl0_71
| ~ spl0_100 ),
inference(avatar_contradiction_clause,[],[f2692]) ).
fof(f2694,plain,
( $false
| spl0_100
| ~ spl0_110
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f2125,f891]) ).
fof(f2695,plain,
( spl0_100
| ~ spl0_110
| ~ spl0_134 ),
inference(avatar_contradiction_clause,[],[f2694]) ).
fof(f2709,plain,
( ! [X0] :
( ~ product(e_2,e_5,X0)
| product(X0,e_3,e_2) )
| ~ spl0_85 ),
inference(resolution,[],[f829,f58]) ).
fof(f2712,plain,
( product(e_4,e_3,e_2)
| ~ spl0_85
| ~ spl0_161 ),
inference(resolution,[],[f2709,f1792]) ).
fof(f2722,plain,
( ! [X0] :
( ~ product(X0,e_2,e_4)
| equalish(X0,e_1) )
| ~ spl0_99 ),
inference(resolution,[],[f888,f56]) ).
fof(f2725,plain,
( ! [X0] :
( ~ product(e_2,e_1,X0)
| product(X0,e_4,e_2) )
| ~ spl0_99 ),
inference(resolution,[],[f888,f58]) ).
fof(f2726,plain,
( product(e_3,e_4,e_2)
| ~ spl0_71
| ~ spl0_99 ),
inference(resolution,[],[f2725,f693]) ).
fof(f2758,plain,
( product(e_5,e_1,e_3)
| ~ spl0_111
| ~ spl0_130 ),
inference(resolution,[],[f1388,f2380]) ).
fof(f2770,plain,
( product(e_1,e_1,e_3)
| ~ spl0_111
| ~ spl0_134 ),
inference(resolution,[],[f1404,f2380]) ).
fof(f2777,plain,
( equalish(e_3,e_1)
| ~ spl0_111
| ~ spl0_134 ),
inference(resolution,[],[f2770,f73]) ).
fof(f2785,plain,
( $false
| ~ spl0_111
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f2777,f41]) ).
fof(f2786,plain,
( ~ spl0_111
| ~ spl0_134 ),
inference(avatar_contradiction_clause,[],[f2785]) ).
fof(f2813,plain,
( product(e_1,e_1,e_2)
| ~ spl0_87
| ~ spl0_164 ),
inference(resolution,[],[f1804,f2489]) ).
fof(f2817,plain,
( ! [X0] :
( ~ product(e_5,e_2,X0)
| product(X0,e_1,e_5) )
| ~ spl0_164 ),
inference(resolution,[],[f1804,f58]) ).
fof(f2820,plain,
( equalish(e_2,e_1)
| ~ spl0_87
| ~ spl0_164 ),
inference(resolution,[],[f2813,f73]) ).
fof(f2828,plain,
( $false
| ~ spl0_87
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f2820,f37]) ).
fof(f2829,plain,
( ~ spl0_87
| ~ spl0_164 ),
inference(avatar_contradiction_clause,[],[f2828]) ).
fof(f2833,plain,
( product(e_3,e_1,e_5)
| ~ spl0_85
| ~ spl0_164 ),
inference(resolution,[],[f2817,f829]) ).
fof(f2853,plain,
( equalish(e_5,e_4)
| ~ spl0_79 ),
inference(resolution,[],[f755,f4]) ).
fof(f2854,plain,
( $false
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f2853,f52]) ).
fof(f2855,plain,
~ spl0_79,
inference(avatar_contradiction_clause,[],[f2854]) ).
fof(f2856,plain,
( ~ greater(e_1,e_0)
| ~ spl0_13
| ~ spl0_80 ),
inference(resolution,[],[f758,f131]) ).
fof(f2857,plain,
( $false
| ~ spl0_13
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f2856,f6]) ).
fof(f2858,plain,
( ~ spl0_13
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f2857]) ).
fof(f2863,plain,
( $false
| spl0_64
| ~ spl0_85
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f2833,f663]) ).
fof(f2864,plain,
( spl0_64
| ~ spl0_85
| ~ spl0_164 ),
inference(avatar_contradiction_clause,[],[f2863]) ).
fof(f2919,plain,
( equalish(e_1,e_3)
| ~ spl0_119 ),
inference(resolution,[],[f1133,f77]) ).
fof(f2920,plain,
( $false
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f2919,f34]) ).
fof(f2921,plain,
~ spl0_119,
inference(avatar_contradiction_clause,[],[f2920]) ).
fof(f2957,plain,
( ! [X0] :
( ~ product(e_3,e_1,X0)
| product(X0,e_4,e_3) )
| ~ spl0_118 ),
inference(resolution,[],[f1129,f58]) ).
fof(f2958,plain,
( product(e_2,e_4,e_3)
| ~ spl0_67
| ~ spl0_118 ),
inference(resolution,[],[f2957,f676]) ).
fof(f2959,plain,
( spl0_168
| ~ spl0_67
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f2958,f1127,f674,f2631]) ).
fof(f2997,plain,
( spl0_135
| ~ spl0_87
| ~ spl0_161 ),
inference(avatar_split_clause,[],[f2485,f1790,f835,f1407]) ).
fof(f3018,plain,
( ! [X0] :
( ~ product(e_3,e_1,X0)
| product(X0,e_5,e_3) )
| ~ spl0_117 ),
inference(resolution,[],[f1125,f58]) ).
fof(f3019,plain,
( product(e_2,e_5,e_3)
| ~ spl0_67
| ~ spl0_117 ),
inference(resolution,[],[f3018,f676]) ).
fof(f3020,plain,
( $false
| ~ spl0_67
| ~ spl0_117
| spl0_162 ),
inference(forward_subsumption_resolution,[],[f3019,f1795]) ).
fof(f3021,plain,
( ~ spl0_67
| ~ spl0_117
| spl0_162 ),
inference(avatar_contradiction_clause,[],[f3020]) ).
fof(f3045,plain,
( equalish(e_2,e_5)
| ~ spl0_165 ),
inference(resolution,[],[f1861,f5]) ).
fof(f3046,plain,
( $false
| ~ spl0_165 ),
inference(forward_subsumption_resolution,[],[f3045,f40]) ).
fof(f3047,plain,
~ spl0_165,
inference(avatar_contradiction_clause,[],[f3046]) ).
fof(f3063,plain,
( equalish(e_2,e_5)
| ~ spl0_56
| ~ spl0_71 ),
inference(resolution,[],[f2362,f693]) ).
fof(f3065,plain,
( $false
| ~ spl0_56
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f3063,f40]) ).
fof(f3066,plain,
( ~ spl0_56
| ~ spl0_71 ),
inference(avatar_contradiction_clause,[],[f3065]) ).
fof(f3069,plain,
( $false
| spl0_56
| ~ spl0_111
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f2758,f629]) ).
fof(f3070,plain,
( spl0_56
| ~ spl0_111
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f3069]) ).
fof(f3256,plain,
( ! [X0] :
( ~ product(X0,e_3,e_5)
| equalish(X0,e_2) )
| ~ spl0_112 ),
inference(resolution,[],[f1104,f56]) ).
fof(f3308,plain,
( equalish(e_4,e_2)
| ~ spl0_61
| ~ spl0_71 ),
inference(resolution,[],[f2677,f651]) ).
fof(f3309,plain,
( $false
| ~ spl0_61
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f3308,f46]) ).
fof(f3310,plain,
( ~ spl0_61
| ~ spl0_71 ),
inference(avatar_contradiction_clause,[],[f3309]) ).
fof(f3352,plain,
( equalish(e_5,e_1)
| ~ spl0_71
| ~ spl0_162 ),
inference(resolution,[],[f2678,f1796]) ).
fof(f3353,plain,
( $false
| ~ spl0_71
| ~ spl0_162 ),
inference(forward_subsumption_resolution,[],[f3352,f49]) ).
fof(f3354,plain,
( ~ spl0_71
| ~ spl0_162 ),
inference(avatar_contradiction_clause,[],[f3353]) ).
fof(f3358,plain,
( spl0_164
| ~ spl0_59
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1605,f1419,f641,f1802]) ).
fof(f3361,plain,
( ! [X0] :
( ~ product(X0,e_1,e_2)
| equalish(X0,e_5) )
| ~ spl0_57 ),
inference(resolution,[],[f634,f56]) ).
fof(f3400,plain,
( equalish(e_4,e_1)
| ~ spl0_71
| ~ spl0_168 ),
inference(resolution,[],[f2633,f2678]) ).
fof(f3405,plain,
( $false
| ~ spl0_71
| ~ spl0_168 ),
inference(forward_subsumption_resolution,[],[f3400,f45]) ).
fof(f3406,plain,
( ~ spl0_71
| ~ spl0_168 ),
inference(avatar_contradiction_clause,[],[f3405]) ).
fof(f3450,plain,
( equalish(e_5,e_1)
| ~ spl0_84
| ~ spl0_99 ),
inference(resolution,[],[f2722,f825]) ).
fof(f3451,plain,
( $false
| ~ spl0_84
| ~ spl0_99 ),
inference(forward_subsumption_resolution,[],[f3450,f49]) ).
fof(f3452,plain,
( ~ spl0_84
| ~ spl0_99 ),
inference(avatar_contradiction_clause,[],[f3451]) ).
fof(f3463,plain,
( spl0_110
| ~ spl0_85
| ~ spl0_161 ),
inference(avatar_split_clause,[],[f2712,f1790,f827,f1093]) ).
fof(f3465,plain,
( $false
| ~ spl0_71
| ~ spl0_98
| spl0_128 ),
inference(forward_subsumption_resolution,[],[f1047,f1274]) ).
fof(f3466,plain,
( ~ spl0_71
| ~ spl0_98
| spl0_128 ),
inference(avatar_contradiction_clause,[],[f3465]) ).
fof(f3536,plain,
( equalish(e_1,e_2)
| ~ spl0_112
| ~ spl0_117 ),
inference(resolution,[],[f3256,f1125]) ).
fof(f3538,plain,
( $false
| ~ spl0_112
| ~ spl0_117 ),
inference(forward_subsumption_resolution,[],[f3536,f33]) ).
fof(f3539,plain,
( ~ spl0_112
| ~ spl0_117 ),
inference(avatar_contradiction_clause,[],[f3538]) ).
fof(f3542,plain,
( spl0_133
| ~ spl0_71
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f2726,f886,f691,f1398]) ).
fof(f3578,plain,
( equalish(e_4,e_5)
| ~ spl0_57
| ~ spl0_62 ),
inference(resolution,[],[f3361,f655]) ).
fof(f3580,plain,
( $false
| ~ spl0_57
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f3578,f48]) ).
fof(f3581,plain,
( ~ spl0_57
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f3580]) ).
cnf(s3,plain,
~ spl0_3,
inference(sat_conversion,[],[f89]) ).
cnf(s4,plain,
( spl0_5
| spl0_6
| spl0_7
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f115]) ).
cnf(s5,plain,
( spl0_10
| spl0_11
| spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f136]) ).
cnf(s6,plain,
( spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f157]) ).
cnf(s11,plain,
( ~ spl0_5
| spl0_24 ),
inference(sat_conversion,[],[f216]) ).
cnf(s12,plain,
~ spl0_24,
inference(sat_conversion,[],[f219]) ).
cnf(s13,plain,
~ spl0_6,
inference(sat_conversion,[],[f228]) ).
cnf(s14,plain,
~ spl0_7,
inference(sat_conversion,[],[f237]) ).
cnf(s25,plain,
( ~ spl0_8
| ~ spl0_11 ),
inference(sat_conversion,[],[f345]) ).
cnf(s27,plain,
( ~ spl0_9
| ~ spl0_11
| spl0_35 ),
inference(sat_conversion,[],[f372]) ).
cnf(s28,plain,
~ spl0_35,
inference(sat_conversion,[],[f375]) ).
cnf(s34,plain,
( ~ spl0_8
| ~ spl0_10
| spl0_39 ),
inference(sat_conversion,[],[f448]) ).
cnf(s35,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_13 ),
inference(sat_conversion,[],[f457]) ).
cnf(s45,plain,
( spl0_54
| spl0_55
| spl0_56
| spl0_57
| spl0_58 ),
inference(sat_conversion,[],[f639]) ).
cnf(s46,plain,
( spl0_59
| spl0_60
| spl0_61
| spl0_62
| spl0_63 ),
inference(sat_conversion,[],[f660]) ).
cnf(s47,plain,
( spl0_64
| spl0_65
| spl0_66
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f681]) ).
cnf(s48,plain,
( spl0_69
| spl0_70
| spl0_71
| spl0_72
| spl0_73 ),
inference(sat_conversion,[],[f702]) ).
cnf(s49,plain,
~ spl0_54,
inference(sat_conversion,[],[f711]) ).
cnf(s53,plain,
( ~ spl0_9
| ~ spl0_59 ),
inference(sat_conversion,[],[f745]) ).
cnf(s54,plain,
( ~ spl0_64
| spl0_79
| spl0_80 ),
inference(sat_conversion,[],[f759]) ).
cnf(s55,plain,
( ~ spl0_14
| ~ spl0_64 ),
inference(sat_conversion,[],[f761]) ).
cnf(s56,plain,
~ spl0_73,
inference(sat_conversion,[],[f796]) ).
cnf(s58,plain,
( ~ spl0_69
| spl0_81
| spl0_82 ),
inference(sat_conversion,[],[f811]) ).
cnf(s59,plain,
( ~ spl0_19
| ~ spl0_69 ),
inference(sat_conversion,[],[f812]) ).
cnf(s60,plain,
( spl0_83
| spl0_84
| spl0_85
| spl0_86
| spl0_87 ),
inference(sat_conversion,[],[f838]) ).
cnf(s63,plain,
( spl0_98
| spl0_99
| spl0_100
| spl0_101
| spl0_102 ),
inference(sat_conversion,[],[f901]) ).
cnf(s64,plain,
~ spl0_83,
inference(sat_conversion,[],[f908]) ).
cnf(s65,plain,
~ spl0_102,
inference(sat_conversion,[],[f928]) ).
cnf(s67,plain,
( ~ spl0_70
| spl0_81
| spl0_103 ),
inference(sat_conversion,[],[f952]) ).
cnf(s68,plain,
( ~ spl0_8
| ~ spl0_78 ),
inference(sat_conversion,[],[f974]) ).
cnf(s69,plain,
( ~ spl0_12
| ~ spl0_80 ),
inference(sat_conversion,[],[f978]) ).
cnf(s70,plain,
( ~ spl0_10
| ~ spl0_80 ),
inference(sat_conversion,[],[f993]) ).
cnf(s72,plain,
~ spl0_39,
inference(sat_conversion,[],[f1007]) ).
cnf(s73,plain,
~ spl0_82,
inference(sat_conversion,[],[f1025]) ).
cnf(s74,plain,
~ spl0_103,
inference(sat_conversion,[],[f1028]) ).
cnf(s76,plain,
( ~ spl0_55
| ~ spl0_65 ),
inference(sat_conversion,[],[f1063]) ).
cnf(s78,plain,
( spl0_107
| spl0_108
| spl0_109
| spl0_110
| spl0_111 ),
inference(sat_conversion,[],[f1100]) ).
cnf(s80,plain,
( spl0_117
| spl0_118
| spl0_119
| spl0_120
| spl0_121 ),
inference(sat_conversion,[],[f1142]) ).
cnf(s83,plain,
~ spl0_121,
inference(sat_conversion,[],[f1193]) ).
cnf(s87,plain,
~ spl0_66,
inference(sat_conversion,[],[f1224]) ).
cnf(s92,plain,
~ spl0_68,
inference(sat_conversion,[],[f1250]) ).
cnf(s101,plain,
~ spl0_72,
inference(sat_conversion,[],[f1339]) ).
cnf(s106,plain,
( spl0_130
| spl0_131
| spl0_132
| spl0_133
| spl0_134 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s107,plain,
( spl0_135
| spl0_136
| spl0_137
| spl0_138
| spl0_139 ),
inference(sat_conversion,[],[f1426]) ).
cnf(s112,plain,
( ~ spl0_107
| ~ spl0_130 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s114,plain,
~ spl0_108,
inference(sat_conversion,[],[f1525]) ).
cnf(s115,plain,
~ spl0_109,
inference(sat_conversion,[],[f1533]) ).
cnf(s117,plain,
( ~ spl0_59
| ~ spl0_135 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s119,plain,
~ spl0_136,
inference(sat_conversion,[],[f1585]) ).
cnf(s120,plain,
~ spl0_139,
inference(sat_conversion,[],[f1594]) ).
cnf(s124,plain,
( ~ spl0_59
| ~ spl0_65
| ~ spl0_120
| ~ spl0_138 ),
inference(sat_conversion,[],[f1621]) ).
cnf(s128,plain,
( ~ spl0_59
| ~ spl0_128
| ~ spl0_137 ),
inference(sat_conversion,[],[f1643]) ).
cnf(s131,plain,
~ spl0_63,
inference(sat_conversion,[],[f1662]) ).
cnf(s133,plain,
~ spl0_60,
inference(sat_conversion,[],[f1672]) ).
cnf(s138,plain,
~ spl0_101,
inference(sat_conversion,[],[f1759]) ).
cnf(s143,plain,
( spl0_160
| spl0_161
| spl0_162
| spl0_163
| spl0_164 ),
inference(sat_conversion,[],[f1805]) ).
cnf(s151,plain,
( ~ spl0_62
| spl0_78
| spl0_165 ),
inference(sat_conversion,[],[f1862]) ).
cnf(s152,plain,
~ spl0_132,
inference(sat_conversion,[],[f1870]) ).
cnf(s153,plain,
~ spl0_131,
inference(sat_conversion,[],[f1878]) ).
cnf(s155,plain,
( ~ spl0_107
| ~ spl0_133
| spl0_162 ),
inference(sat_conversion,[],[f1885]) ).
cnf(s186,plain,
( ~ spl0_110
| ~ spl0_133 ),
inference(sat_conversion,[],[f2124]) ).
cnf(s188,plain,
( ~ spl0_107
| ~ spl0_134
| spl0_157 ),
inference(sat_conversion,[],[f2134]) ).
cnf(s204,plain,
( ~ spl0_65
| ~ spl0_118 ),
inference(sat_conversion,[],[f2253]) ).
cnf(s212,plain,
~ spl0_58,
inference(sat_conversion,[],[f2314]) ).
cnf(s217,plain,
( ~ spl0_57
| spl0_112
| ~ spl0_157 ),
inference(sat_conversion,[],[f2359]) ).
cnf(s220,plain,
( spl0_99
| ~ spl0_111
| ~ spl0_133 ),
inference(sat_conversion,[],[f2382]) ).
cnf(s222,plain,
( ~ spl0_65
| ~ spl0_120
| ~ spl0_164 ),
inference(sat_conversion,[],[f2405]) ).
cnf(s224,plain,
~ spl0_163,
inference(sat_conversion,[],[f2416]) ).
cnf(s226,plain,
~ spl0_160,
inference(sat_conversion,[],[f2427]) ).
cnf(s230,plain,
~ spl0_86,
inference(sat_conversion,[],[f2446]) ).
cnf(s233,plain,
( ~ spl0_67
| ~ spl0_120 ),
inference(sat_conversion,[],[f2467]) ).
cnf(s234,plain,
( ~ spl0_84
| ~ spl0_161 ),
inference(sat_conversion,[],[f2484]) ).
cnf(s248,plain,
( ~ spl0_16
| ~ spl0_81 ),
inference(sat_conversion,[],[f2555]) ).
cnf(s249,plain,
( ~ spl0_14
| ~ spl0_65 ),
inference(sat_conversion,[],[f2558]) ).
cnf(s250,plain,
( ~ spl0_15
| ~ spl0_81 ),
inference(sat_conversion,[],[f2587]) ).
cnf(s251,plain,
( ~ spl0_17
| ~ spl0_81 ),
inference(sat_conversion,[],[f2599]) ).
cnf(s252,plain,
( ~ spl0_18
| ~ spl0_81 ),
inference(sat_conversion,[],[f2611]) ).
cnf(s255,plain,
( spl0_85
| ~ spl0_110
| ~ spl0_130 ),
inference(sat_conversion,[],[f2613]) ).
cnf(s264,plain,
( ~ spl0_19
| ~ spl0_70 ),
inference(sat_conversion,[],[f2673]) ).
cnf(s265,plain,
( ~ spl0_19
| ~ spl0_71 ),
inference(sat_conversion,[],[f2683]) ).
cnf(s267,plain,
( ~ spl0_71
| ~ spl0_100 ),
inference(sat_conversion,[],[f2693]) ).
cnf(s268,plain,
( spl0_100
| ~ spl0_110
| ~ spl0_134 ),
inference(sat_conversion,[],[f2695]) ).
cnf(s279,plain,
( ~ spl0_111
| ~ spl0_134 ),
inference(sat_conversion,[],[f2786]) ).
cnf(s282,plain,
( ~ spl0_87
| ~ spl0_164 ),
inference(sat_conversion,[],[f2829]) ).
cnf(s286,plain,
~ spl0_79,
inference(sat_conversion,[],[f2855]) ).
cnf(s287,plain,
( ~ spl0_13
| ~ spl0_80 ),
inference(sat_conversion,[],[f2858]) ).
cnf(s290,plain,
( spl0_64
| ~ spl0_85
| ~ spl0_164 ),
inference(sat_conversion,[],[f2864]) ).
cnf(s298,plain,
~ spl0_119,
inference(sat_conversion,[],[f2921]) ).
cnf(s303,plain,
( ~ spl0_67
| ~ spl0_118
| spl0_168 ),
inference(sat_conversion,[],[f2959]) ).
cnf(s311,plain,
( ~ spl0_87
| spl0_135
| ~ spl0_161 ),
inference(sat_conversion,[],[f2997]) ).
cnf(s312,plain,
( ~ spl0_67
| ~ spl0_117
| spl0_162 ),
inference(sat_conversion,[],[f3021]) ).
cnf(s314,plain,
~ spl0_165,
inference(sat_conversion,[],[f3047]) ).
cnf(s316,plain,
( ~ spl0_56
| ~ spl0_71 ),
inference(sat_conversion,[],[f3066]) ).
cnf(s318,plain,
( spl0_56
| ~ spl0_111
| ~ spl0_130 ),
inference(sat_conversion,[],[f3070]) ).
cnf(s347,plain,
( ~ spl0_61
| ~ spl0_71 ),
inference(sat_conversion,[],[f3310]) ).
cnf(s352,plain,
( ~ spl0_71
| ~ spl0_162 ),
inference(sat_conversion,[],[f3354]) ).
cnf(s357,plain,
( ~ spl0_59
| ~ spl0_138
| spl0_164 ),
inference(sat_conversion,[],[f3358]) ).
cnf(s359,plain,
( ~ spl0_71
| ~ spl0_168 ),
inference(sat_conversion,[],[f3406]) ).
cnf(s361,plain,
( ~ spl0_84
| ~ spl0_99 ),
inference(sat_conversion,[],[f3452]) ).
cnf(s376,plain,
( ~ spl0_85
| spl0_110
| ~ spl0_161 ),
inference(sat_conversion,[],[f3463]) ).
cnf(s378,plain,
( ~ spl0_71
| ~ spl0_98
| spl0_128 ),
inference(sat_conversion,[],[f3466]) ).
cnf(s383,plain,
( ~ spl0_112
| ~ spl0_117 ),
inference(sat_conversion,[],[f3539]) ).
cnf(s387,plain,
( ~ spl0_71
| ~ spl0_99
| spl0_133 ),
inference(sat_conversion,[],[f3542]) ).
cnf(s388,plain,
( ~ spl0_57
| ~ spl0_62 ),
inference(sat_conversion,[],[f3581]) ).
cnf(s392,plain,
( ~ spl0_62
| spl0_78 ),
inference(rat,[],[s151,s314]) ).
cnf(s393,plain,
( spl0_161
| spl0_162
| spl0_164 ),
inference(rat,[],[s143,s224,s226]) ).
cnf(s399,plain,
( spl0_135
| spl0_137
| spl0_138 ),
inference(rat,[],[s107,s120,s119]) ).
cnf(s400,plain,
( spl0_130
| spl0_133
| spl0_134 ),
inference(rat,[],[s106,s152,s153]) ).
cnf(s405,plain,
( spl0_117
| spl0_118
| spl0_120 ),
inference(rat,[],[s80,s83,s298]) ).
cnf(s407,plain,
( spl0_107
| spl0_110
| spl0_111 ),
inference(rat,[],[s78,s115,s114]) ).
cnf(s408,plain,
( ~ spl0_70
| spl0_81 ),
inference(rat,[],[s67,s74]) ).
cnf(s409,plain,
( spl0_98
| spl0_99
| spl0_100 ),
inference(rat,[],[s63,s65,s138]) ).
cnf(s412,plain,
( spl0_84
| spl0_85
| spl0_87 ),
inference(rat,[],[s60,s230,s64]) ).
cnf(s413,plain,
( ~ spl0_69
| spl0_81 ),
inference(rat,[],[s58,s73]) ).
cnf(s414,plain,
( ~ spl0_64
| spl0_80 ),
inference(rat,[],[s54,s286]) ).
cnf(s415,plain,
( spl0_69
| spl0_70
| spl0_71 ),
inference(rat,[],[s48,s56,s101]) ).
cnf(s416,plain,
( spl0_64
| spl0_65
| spl0_67 ),
inference(rat,[],[s47,s92,s87]) ).
cnf(s417,plain,
( spl0_59
| spl0_61
| spl0_62 ),
inference(rat,[],[s46,s131,s133]) ).
cnf(s418,plain,
( spl0_55
| spl0_56
| spl0_57 ),
inference(rat,[],[s45,s212,s49]) ).
cnf(s420,plain,
( ~ spl0_8
| ~ spl0_10 ),
inference(rat,[],[s34,s72]) ).
cnf(s422,plain,
( ~ spl0_9
| ~ spl0_11 ),
inference(rat,[],[s27,s28]) ).
cnf(s426,plain,
~ spl0_5,
inference(rat,[],[s11,s12]) ).
cnf(s429,plain,
( spl0_8
| spl0_9 ),
inference(rat,[],[s4,s14,s13,s426]) ).
cnf(s432,plain,
~ spl0_19,
inference(rat,[],[s415,s59,s264,s265]) ).
cnf(s433,plain,
( ~ spl0_71
| ~ spl0_67 ),
inference(rat,[],[s405,s312,s303,s352,s359,s233]) ).
cnf(s434,plain,
( ~ spl0_81
| spl0_16
| spl0_15 ),
inference(rat,[],[s6,s251,s252,s432]) ).
cnf(s435,plain,
( spl0_81
| spl0_71 ),
inference(rat,[],[s415,s413,s408]) ).
cnf(s436,plain,
( spl0_16
| ~ spl0_81 ),
inference(rat,[],[s250,s434]) ).
cnf(s437,plain,
~ spl0_81,
inference(rat,[],[s436,s248]) ).
cnf(s440,plain,
spl0_71,
inference(rat,[],[s435,s437]) ).
cnf(s442,plain,
~ spl0_162,
inference(rat,[],[s352,s440]) ).
cnf(s443,plain,
~ spl0_61,
inference(rat,[],[s347,s440]) ).
cnf(s444,plain,
~ spl0_56,
inference(rat,[],[s316,s440]) ).
cnf(s445,plain,
~ spl0_100,
inference(rat,[],[s267,s440]) ).
cnf(s447,plain,
~ spl0_67,
inference(rat,[],[s433,s440]) ).
cnf(s448,plain,
~ spl0_9,
inference(rat,[],[s70,s5,s69,s287,s414,s55,s416,s76,s418,s388,s417,s422,s53,s447,s444,s443]) ).
cnf(s449,plain,
spl0_8,
inference(rat,[],[s429,s448]) ).
cnf(s450,plain,
~ spl0_78,
inference(rat,[],[s68,s449]) ).
cnf(s451,plain,
~ spl0_13,
inference(rat,[],[s35,s3,s449]) ).
cnf(s452,plain,
~ spl0_10,
inference(rat,[],[s420,s449]) ).
cnf(s454,plain,
~ spl0_11,
inference(rat,[],[s25,s449]) ).
cnf(s456,plain,
~ spl0_62,
inference(rat,[],[s392,s450]) ).
cnf(s457,plain,
spl0_59,
inference(rat,[],[s417,s443,s456]) ).
cnf(s458,plain,
~ spl0_135,
inference(rat,[],[s117,s457]) ).
cnf(s461,plain,
~ spl0_14,
inference(rat,[],[s416,s55,s249,s447]) ).
cnf(s462,plain,
spl0_12,
inference(rat,[],[s5,s454,s452,s451,s461]) ).
cnf(s463,plain,
~ spl0_80,
inference(rat,[],[s69,s462]) ).
cnf(s467,plain,
~ spl0_64,
inference(rat,[],[s414,s463]) ).
cnf(s468,plain,
spl0_65,
inference(rat,[],[s416,s447,s467]) ).
cnf(s469,plain,
~ spl0_118,
inference(rat,[],[s204,s468]) ).
cnf(s470,plain,
~ spl0_55,
inference(rat,[],[s76,s468]) ).
cnf(s472,plain,
spl0_57,
inference(rat,[],[s418,s444,s470]) ).
cnf(s475,plain,
~ spl0_120,
inference(rat,[],[s387,s186,s409,s376,s378,s412,s128,s311,s234,s399,s393,s124,s222,s440,s445,s457,s458,s442,s468]) ).
cnf(s476,plain,
spl0_117,
inference(rat,[],[s405,s469,s475]) ).
cnf(s477,plain,
~ spl0_112,
inference(rat,[],[s383,s476]) ).
cnf(s479,plain,
~ spl0_157,
inference(rat,[],[s217,s472,s477]) ).
cnf(s486,plain,
~ spl0_85,
inference(rat,[],[s409,s378,s387,s128,s186,s399,s376,s357,s393,s290,s445,s440,s457,s458,s442,s467]) ).
cnf(s487,plain,
~ spl0_87,
inference(rat,[],[s393,s311,s282,s442,s458]) ).
cnf(s488,plain,
spl0_84,
inference(rat,[],[s412,s486,s487]) ).
cnf(s489,plain,
~ spl0_99,
inference(rat,[],[s361,s488]) ).
cnf(s509,plain,
~ spl0_110,
inference(rat,[],[s400,s186,s255,s268,s486,s445]) ).
cnf(s510,plain,
~ spl0_111,
inference(rat,[],[s400,s220,s279,s318,s489,s444]) ).
cnf(s511,plain,
spl0_107,
inference(rat,[],[s407,s509,s510]) ).
cnf(s512,plain,
~ spl0_133,
inference(rat,[],[s155,s442,s511]) ).
cnf(s513,plain,
~ spl0_130,
inference(rat,[],[s112,s511]) ).
cnf(s514,plain,
~ spl0_134,
inference(rat,[],[s188,s479,s511]) ).
cnf(s515,plain,
$false,
inference(rat,[],[s400,s514,s512,s513]) ).
fof(f3582,plain,
$false,
inference(avatar_sat_refutation,[],[s515]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP125-3.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n014.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 09:21:47 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/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
% 3.63/1.20 % (541627)Input is clausal, will run a generic CNF schedule.
% 3.63/1.20 % (541637)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=60424638:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.63/1.20 % (541635)lrs+10_1_sil=8000:sp=occurrence:random_seed=1890566657:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.63/1.20 % (541632)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=412836563:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.63/1.20 % (541633)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2677634951:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.63/1.20 % (541638)dis-21_1_sil=8000:lcm=predicate:random_seed=2454816473:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.63/1.20 % (541634)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3324568809:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.63/1.20 % (541636)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3813246880:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.63/1.20 % (541635)Instruction limit reached!
% 3.63/1.20 % (541635)------------------------------
% 3.63/1.20 % (541635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.63/1.20 % (541635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.20 % (541635)CaDiCaL version: 2.1.3
% 3.63/1.20 % (541635)Termination reason: Instruction limit
% 3.63/1.20 % (541635)Termination phase: Saturation
% 3.63/1.20 % (541635)Time elapsed: 0.060 s
% 3.63/1.20 % (541635)Peak memory usage: 88 MB
% 3.63/1.20 % (541635)Instructions burned: 108 (million)
% 3.63/1.20 % (541636)Instruction limit reached!
% 3.63/1.20 % (541636)------------------------------
% 3.63/1.20 % (541636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.63/1.20 % (541636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.20 % (541636)CaDiCaL version: 2.1.3
% 3.63/1.20 % (541636)Termination reason: Instruction limit
% 3.63/1.20 % (541636)Termination phase: Saturation
% 3.63/1.20 % (541636)Time elapsed: 0.060 s
% 3.63/1.20 % (541636)Peak memory usage: 88 MB
% 3.63/1.20 % (541636)Instructions burned: 114 (million)
% 3.63/1.20 % (541638)Instruction limit reached!
% 3.63/1.20 % (541638)------------------------------
% 3.63/1.20 % (541638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.63/1.20 % (541638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.20 % (541638)CaDiCaL version: 2.1.3
% 3.63/1.20 % (541638)Termination reason: Instruction limit
% 3.63/1.20 % (541638)Termination phase: Saturation
% 3.63/1.20 % (541638)Time elapsed: 0.073 s
% 3.63/1.20 % (541638)Peak memory usage: 89 MB
% 3.63/1.20 % (541638)Instructions burned: 118 (million)
% 3.63/1.20 % (541637)Instruction limit reached!
% 3.63/1.20 % (541637)------------------------------
% 3.63/1.20 % (541637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.63/1.20 % (541637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.20 % (541637)CaDiCaL version: 2.1.3
% 4.30/1.20 % (541637)Termination reason: Instruction limit
% 4.30/1.20 % (541637)Termination phase: Saturation
% 4.30/1.20 % (541637)Time elapsed: 0.110 s
% 4.30/1.20 % (541637)Peak memory usage: 89 MB
% 4.30/1.20 % (541637)Instructions burned: 182 (million)
% 4.30/1.20 % (541646)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=718442147:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 4.30/1.20 % (541647)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=317091402:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 4.30/1.20 % (541647)Refutation not found, incomplete strategy
% 4.30/1.20 % (541647)------------------------------
% 4.30/1.20 % (541647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.30/1.20 % (541647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.20 % (541647)CaDiCaL version: 2.1.3
% 4.30/1.20 % (541647)Termination reason: Refutation not found, incomplete strategy
% 4.30/1.20 % (541647)Time elapsed: 0.002 s
% 4.30/1.20 % (541647)Peak memory usage: 87 MB
% 4.30/1.20 % (541647)Instructions burned: 2 (million)
% 4.30/1.20 % (541648)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1034175519:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.30/1.20 % (541649)lrs+10_64_to=lpo:sil=8000:random_seed=2087901862:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 4.30/1.20 % (541646)Instruction limit reached!
% 4.30/1.20 % (541646)------------------------------
% 4.30/1.20 % (541646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.30/1.20 % (541646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.20 % (541646)CaDiCaL version: 2.1.3
% 4.30/1.20 % (541646)Termination reason: Instruction limit
% 4.30/1.20 % (541646)Termination phase: Saturation
% 4.30/1.20 % (541646)Time elapsed: 0.078 s
% 4.30/1.20 % (541646)Peak memory usage: 88 MB
% 4.30/1.20 % (541646)Instructions burned: 143 (million)
% 4.30/1.20 % (541649)First to succeed.
% 4.30/1.20 % (541649)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-541627"
% 4.30/1.20 % (541648)Instruction limit reached!
% 4.30/1.20 % (541648)------------------------------
% 4.30/1.20 % (541648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.30/1.20 % (541648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.20 % (541648)CaDiCaL version: 2.1.3
% 4.30/1.20 % (541648)Termination reason: Instruction limit
% 4.30/1.20 % (541648)Termination phase: Saturation
% 4.30/1.20 % (541648)Time elapsed: 0.118 s
% 4.30/1.20 % (541648)Peak memory usage: 88 MB
% 4.30/1.20 % (541648)Instructions burned: 220 (million)
% 4.30/1.20 % (541654)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1682492423:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 4.30/1.20 % (541647)------------------------------
% 4.30/1.20 % (541647)------------------------------
% 4.30/1.20 % (541649)Refutation found. Thanks to Tanya!
% 4.30/1.20 % SZS status Unsatisfiable for theBenchmark
% 4.30/1.20 % SZS output start Proof for theBenchmark
% See solution above
% 4.41/1.39 % (541649)------------------------------
% 4.41/1.39 % (541649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.41/1.39 % (541649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.41/1.39 % (541649)CaDiCaL version: 2.1.3
% 4.41/1.39 % (541649)Termination reason: Refutation
% 4.41/1.39 % (541649)Time elapsed: 0.040 s
% 4.41/1.39 % (541649)Peak memory usage: 89 MB
% 4.41/1.39 % (541649)Instructions burned: 101 (million)
% 4.41/1.39 % (541649)------------------------------
% 4.41/1.39 % (541649)------------------------------
% 4.41/1.39 % (541627)Success in time 0.579 s
% 4.41/1.39 % Vampire exiting
%------------------------------------------------------------------------------