%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRA117-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.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:00:07 AM UTC 2026
% Result : Unsatisfiable 2.34s 1.18s
% Output : Refutation 2.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 69
% Syntax : Number of formulae : 416 ( 79 unt; 51 def)
% Number of atoms : 1243 ( 22 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1382 ( 555 ~; 776 |; 0 &)
% ( 51 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 54 ( 52 usr; 51 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 75 ( 0 sgn 75 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( r(X1,X0)
| ~ r(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rsym) ).
fof(f2,axiom,
! [X2,X0,X1] :
( X0 = X1
| X0 = X2
| X1 = X2
| ~ r(X0,X1)
| ~ r(X0,X2)
| ~ r(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rno3cl) ).
fof(f3,axiom,
! [X2,X0,X1] :
( X0 = X1
| X0 = X2
| X1 = X2
| r(X0,X1)
| r(X0,X2)
| r(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rno3acl) ).
fof(f4,axiom,
v0 != v1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v0nv1) ).
fof(f5,axiom,
v0 != v2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v0nv2) ).
fof(f6,axiom,
v1 != v2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v1nv2) ).
fof(f7,axiom,
v0 != v3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v0nv3) ).
fof(f8,axiom,
v1 != v3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v1nv3) ).
fof(f9,axiom,
v2 != v3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v2nv3) ).
fof(f10,axiom,
v0 != v4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v0nv4) ).
fof(f11,axiom,
v1 != v4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v1nv4) ).
fof(f12,axiom,
v2 != v4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v2nv4) ).
fof(f13,axiom,
v3 != v4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v3nv4) ).
fof(f14,axiom,
v0 != v5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v0nv5) ).
fof(f15,axiom,
v1 != v5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v1nv5) ).
fof(f16,axiom,
v2 != v5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v2nv5) ).
fof(f17,axiom,
v3 != v5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v3nv5) ).
fof(f18,axiom,
v4 != v5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v4nv5) ).
fof(f19,definition,
! [X0,X1] :
( sQ0_eqProxy(X0,X1)
<=> X0 = X1 ),
introduced(definition,[new_symbols(definition,[sQ0_eqProxy])],[equality_proxy_definition]) ).
fof(f20,plain,
! [X2,X0,X1] :
( sQ0_eqProxy(X1,X2)
| sQ0_eqProxy(X0,X2)
| sQ0_eqProxy(X0,X1)
| ~ r(X0,X1)
| ~ r(X0,X2)
| ~ r(X1,X2) ),
inference(equality_proxy_replacement,[],[f2,f19,f19,f19]) ).
fof(f21,plain,
! [X2,X0,X1] :
( r(X1,X2)
| sQ0_eqProxy(X0,X2)
| sQ0_eqProxy(X1,X2)
| r(X0,X1)
| r(X0,X2)
| sQ0_eqProxy(X0,X1) ),
inference(equality_proxy_replacement,[],[f3,f19,f19,f19]) ).
fof(f22,plain,
~ sQ0_eqProxy(v0,v1),
inference(equality_proxy_replacement,[],[f4,f19]) ).
fof(f23,plain,
~ sQ0_eqProxy(v0,v2),
inference(equality_proxy_replacement,[],[f5,f19]) ).
fof(f24,plain,
~ sQ0_eqProxy(v1,v2),
inference(equality_proxy_replacement,[],[f6,f19]) ).
fof(f25,plain,
~ sQ0_eqProxy(v0,v3),
inference(equality_proxy_replacement,[],[f7,f19]) ).
fof(f26,plain,
~ sQ0_eqProxy(v1,v3),
inference(equality_proxy_replacement,[],[f8,f19]) ).
fof(f27,plain,
~ sQ0_eqProxy(v2,v3),
inference(equality_proxy_replacement,[],[f9,f19]) ).
fof(f28,plain,
~ sQ0_eqProxy(v0,v4),
inference(equality_proxy_replacement,[],[f10,f19]) ).
fof(f29,plain,
~ sQ0_eqProxy(v1,v4),
inference(equality_proxy_replacement,[],[f11,f19]) ).
fof(f30,plain,
~ sQ0_eqProxy(v2,v4),
inference(equality_proxy_replacement,[],[f12,f19]) ).
fof(f31,plain,
~ sQ0_eqProxy(v3,v4),
inference(equality_proxy_replacement,[],[f13,f19]) ).
fof(f32,plain,
~ sQ0_eqProxy(v0,v5),
inference(equality_proxy_replacement,[],[f14,f19]) ).
fof(f33,plain,
~ sQ0_eqProxy(v1,v5),
inference(equality_proxy_replacement,[],[f15,f19]) ).
fof(f34,plain,
~ sQ0_eqProxy(v2,v5),
inference(equality_proxy_replacement,[],[f16,f19]) ).
fof(f35,plain,
~ sQ0_eqProxy(v3,v5),
inference(equality_proxy_replacement,[],[f17,f19]) ).
fof(f36,plain,
~ sQ0_eqProxy(v4,v5),
inference(equality_proxy_replacement,[],[f18,f19]) ).
fof(f38,plain,
! [X0,X1] :
( sQ0_eqProxy(X1,X0)
| ~ sQ0_eqProxy(X0,X1) ),
inference(equality_proxy_axiom,[],[f19]) ).
fof(f47,plain,
~ sQ0_eqProxy(v5,v1),
inference(resolution,[],[f38,f33]) ).
fof(f48,plain,
~ sQ0_eqProxy(v3,v2),
inference(resolution,[],[f38,f27]) ).
fof(f61,plain,
! [X0] :
( sQ0_eqProxy(X0,v2)
| sQ0_eqProxy(X0,v1)
| ~ r(X0,v1)
| ~ r(X0,v2)
| ~ r(v1,v2) ),
inference(resolution,[],[f20,f24]) ).
fof(f62,plain,
! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(X0,v1)
| ~ r(X0,v1)
| ~ r(X0,v3)
| ~ r(v1,v3) ),
inference(resolution,[],[f20,f26]) ).
fof(f63,plain,
! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v1)
| ~ r(X0,v1)
| ~ r(X0,v4)
| ~ r(v1,v4) ),
inference(resolution,[],[f20,f29]) ).
fof(f64,plain,
! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v1)
| ~ r(X0,v1)
| ~ r(X0,v5)
| ~ r(v1,v5) ),
inference(resolution,[],[f20,f33]) ).
fof(f65,plain,
! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(X0,v2)
| ~ r(X0,v2)
| ~ r(X0,v3)
| ~ r(v2,v3) ),
inference(resolution,[],[f20,f27]) ).
fof(f66,plain,
! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v2)
| ~ r(X0,v2)
| ~ r(X0,v4)
| ~ r(v2,v4) ),
inference(resolution,[],[f20,f30]) ).
fof(f67,plain,
! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v2)
| ~ r(X0,v2)
| ~ r(X0,v5)
| ~ r(v2,v5) ),
inference(resolution,[],[f20,f34]) ).
fof(f68,plain,
! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v3)
| ~ r(X0,v3)
| ~ r(X0,v4)
| ~ r(v3,v4) ),
inference(resolution,[],[f20,f31]) ).
fof(f69,plain,
! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v3)
| ~ r(X0,v3)
| ~ r(X0,v5)
| ~ r(v3,v5) ),
inference(resolution,[],[f20,f35]) ).
fof(f70,plain,
! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v4)
| ~ r(X0,v4)
| ~ r(X0,v5)
| ~ r(v4,v5) ),
inference(resolution,[],[f20,f36]) ).
fof(f72,definition,
( spl1_1
<=> r(v4,v5) ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
fof(f73,plain,
( ~ r(v4,v5)
| spl1_1 ),
inference(avatar_component_clause,[],[f72]) ).
fof(f75,definition,
( spl1_2
<=> ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v4)
| sQ0_eqProxy(X0,v4) ) ),
introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition]) ).
fof(f76,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v4)
| sQ0_eqProxy(X0,v4) )
| ~ spl1_2 ),
inference(avatar_component_clause,[],[f75]) ).
fof(f77,plain,
( ~ spl1_1
| spl1_2 ),
inference(avatar_split_clause,[],[f70,f75,f72]) ).
fof(f79,definition,
( spl1_3
<=> r(v3,v5) ),
introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition]) ).
fof(f80,plain,
( ~ r(v3,v5)
| spl1_3 ),
inference(avatar_component_clause,[],[f79]) ).
fof(f82,definition,
( spl1_4
<=> ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v3)
| sQ0_eqProxy(X0,v3) ) ),
introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition]) ).
fof(f83,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v3)
| sQ0_eqProxy(X0,v3) )
| ~ spl1_4 ),
inference(avatar_component_clause,[],[f82]) ).
fof(f84,plain,
( ~ spl1_3
| spl1_4 ),
inference(avatar_split_clause,[],[f69,f82,f79]) ).
fof(f86,definition,
( spl1_5
<=> r(v3,v4) ),
introduced(definition,[new_symbols(definition,[spl1_5])],[avatar_definition]) ).
fof(f87,plain,
( ~ r(v3,v4)
| spl1_5 ),
inference(avatar_component_clause,[],[f86]) ).
fof(f89,definition,
( spl1_6
<=> ! [X0] :
( sQ0_eqProxy(X0,v4)
| ~ r(X0,v4)
| ~ r(X0,v3)
| sQ0_eqProxy(X0,v3) ) ),
introduced(definition,[new_symbols(definition,[spl1_6])],[avatar_definition]) ).
fof(f90,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| ~ r(X0,v4)
| ~ r(X0,v3)
| sQ0_eqProxy(X0,v3) )
| ~ spl1_6 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f91,plain,
( ~ spl1_5
| spl1_6 ),
inference(avatar_split_clause,[],[f68,f89,f86]) ).
fof(f93,definition,
( spl1_7
<=> r(v2,v5) ),
introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition]) ).
fof(f94,plain,
( ~ r(v2,v5)
| spl1_7 ),
inference(avatar_component_clause,[],[f93]) ).
fof(f96,definition,
( spl1_8
<=> ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v2)
| sQ0_eqProxy(X0,v2) ) ),
introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition]) ).
fof(f97,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v2)
| sQ0_eqProxy(X0,v2) )
| ~ spl1_8 ),
inference(avatar_component_clause,[],[f96]) ).
fof(f98,plain,
( ~ spl1_7
| spl1_8 ),
inference(avatar_split_clause,[],[f67,f96,f93]) ).
fof(f100,definition,
( spl1_9
<=> r(v2,v4) ),
introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition]) ).
fof(f101,plain,
( ~ r(v2,v4)
| spl1_9 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f103,definition,
( spl1_10
<=> ! [X0] :
( sQ0_eqProxy(X0,v4)
| ~ r(X0,v4)
| ~ r(X0,v2)
| sQ0_eqProxy(X0,v2) ) ),
introduced(definition,[new_symbols(definition,[spl1_10])],[avatar_definition]) ).
fof(f104,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| ~ r(X0,v4)
| ~ r(X0,v2)
| sQ0_eqProxy(X0,v2) )
| ~ spl1_10 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f105,plain,
( ~ spl1_9
| spl1_10 ),
inference(avatar_split_clause,[],[f66,f103,f100]) ).
fof(f107,definition,
( spl1_11
<=> r(v2,v3) ),
introduced(definition,[new_symbols(definition,[spl1_11])],[avatar_definition]) ).
fof(f108,plain,
( ~ r(v2,v3)
| spl1_11 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f110,definition,
( spl1_12
<=> ! [X0] :
( sQ0_eqProxy(X0,v3)
| ~ r(X0,v3)
| ~ r(X0,v2)
| sQ0_eqProxy(X0,v2) ) ),
introduced(definition,[new_symbols(definition,[spl1_12])],[avatar_definition]) ).
fof(f111,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| ~ r(X0,v3)
| ~ r(X0,v2)
| sQ0_eqProxy(X0,v2) )
| ~ spl1_12 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f112,plain,
( ~ spl1_11
| spl1_12 ),
inference(avatar_split_clause,[],[f65,f110,f107]) ).
fof(f114,definition,
( spl1_13
<=> r(v1,v5) ),
introduced(definition,[new_symbols(definition,[spl1_13])],[avatar_definition]) ).
fof(f115,plain,
( ~ r(v1,v5)
| spl1_13 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f117,definition,
( spl1_14
<=> ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) ) ),
introduced(definition,[new_symbols(definition,[spl1_14])],[avatar_definition]) ).
fof(f118,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) )
| ~ spl1_14 ),
inference(avatar_component_clause,[],[f117]) ).
fof(f119,plain,
( ~ spl1_13
| spl1_14 ),
inference(avatar_split_clause,[],[f64,f117,f114]) ).
fof(f121,definition,
( spl1_15
<=> r(v1,v4) ),
introduced(definition,[new_symbols(definition,[spl1_15])],[avatar_definition]) ).
fof(f122,plain,
( ~ r(v1,v4)
| spl1_15 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f124,definition,
( spl1_16
<=> ! [X0] :
( sQ0_eqProxy(X0,v4)
| ~ r(X0,v4)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) ) ),
introduced(definition,[new_symbols(definition,[spl1_16])],[avatar_definition]) ).
fof(f125,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| ~ r(X0,v4)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) )
| ~ spl1_16 ),
inference(avatar_component_clause,[],[f124]) ).
fof(f126,plain,
( ~ spl1_15
| spl1_16 ),
inference(avatar_split_clause,[],[f63,f124,f121]) ).
fof(f128,definition,
( spl1_17
<=> r(v1,v3) ),
introduced(definition,[new_symbols(definition,[spl1_17])],[avatar_definition]) ).
fof(f129,plain,
( ~ r(v1,v3)
| spl1_17 ),
inference(avatar_component_clause,[],[f128]) ).
fof(f131,definition,
( spl1_18
<=> ! [X0] :
( sQ0_eqProxy(X0,v3)
| ~ r(X0,v3)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) ) ),
introduced(definition,[new_symbols(definition,[spl1_18])],[avatar_definition]) ).
fof(f132,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| ~ r(X0,v3)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) )
| ~ spl1_18 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f133,plain,
( ~ spl1_17
| spl1_18 ),
inference(avatar_split_clause,[],[f62,f131,f128]) ).
fof(f135,definition,
( spl1_19
<=> r(v1,v2) ),
introduced(definition,[new_symbols(definition,[spl1_19])],[avatar_definition]) ).
fof(f138,definition,
( spl1_20
<=> ! [X0] :
( sQ0_eqProxy(X0,v2)
| ~ r(X0,v2)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) ) ),
introduced(definition,[new_symbols(definition,[spl1_20])],[avatar_definition]) ).
fof(f139,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v2)
| ~ r(X0,v2)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) )
| ~ spl1_20 ),
inference(avatar_component_clause,[],[f138]) ).
fof(f140,plain,
( ~ spl1_19
| spl1_20 ),
inference(avatar_split_clause,[],[f61,f138,f135]) ).
fof(f149,definition,
( spl1_23
<=> r(v0,v5) ),
introduced(definition,[new_symbols(definition,[spl1_23])],[avatar_definition]) ).
fof(f156,definition,
( spl1_25
<=> r(v0,v4) ),
introduced(definition,[new_symbols(definition,[spl1_25])],[avatar_definition]) ).
fof(f163,definition,
( spl1_27
<=> r(v0,v3) ),
introduced(definition,[new_symbols(definition,[spl1_27])],[avatar_definition]) ).
fof(f170,definition,
( spl1_29
<=> r(v0,v2) ),
introduced(definition,[new_symbols(definition,[spl1_29])],[avatar_definition]) ).
fof(f177,definition,
( spl1_31
<=> r(v0,v1) ),
introduced(definition,[new_symbols(definition,[spl1_31])],[avatar_definition]) ).
fof(f186,plain,
( ~ r(v5,v1)
| spl1_13 ),
inference(resolution,[],[f115,f1]) ).
fof(f247,definition,
( spl1_33
<=> sQ0_eqProxy(v4,v5) ),
introduced(definition,[new_symbols(definition,[spl1_33])],[avatar_definition]) ).
fof(f248,plain,
( sQ0_eqProxy(v4,v5)
| ~ spl1_33 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f250,definition,
( spl1_34
<=> ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v4)
| r(X0,v5)
| r(X0,v4) ) ),
introduced(definition,[new_symbols(definition,[spl1_34])],[avatar_definition]) ).
fof(f251,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v4)
| r(X0,v5)
| r(X0,v4) )
| ~ spl1_34 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f254,definition,
( spl1_35
<=> sQ0_eqProxy(v3,v5) ),
introduced(definition,[new_symbols(definition,[spl1_35])],[avatar_definition]) ).
fof(f255,plain,
( sQ0_eqProxy(v3,v5)
| ~ spl1_35 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f257,definition,
( spl1_36
<=> ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v3)
| r(X0,v5)
| r(X0,v3) ) ),
introduced(definition,[new_symbols(definition,[spl1_36])],[avatar_definition]) ).
fof(f258,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v3)
| r(X0,v5)
| r(X0,v3) )
| ~ spl1_36 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f261,definition,
( spl1_37
<=> sQ0_eqProxy(v2,v5) ),
introduced(definition,[new_symbols(definition,[spl1_37])],[avatar_definition]) ).
fof(f262,plain,
( sQ0_eqProxy(v2,v5)
| ~ spl1_37 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f264,definition,
( spl1_38
<=> ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v2)
| r(X0,v5)
| r(X0,v2) ) ),
introduced(definition,[new_symbols(definition,[spl1_38])],[avatar_definition]) ).
fof(f265,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v2)
| r(X0,v5)
| r(X0,v2) )
| ~ spl1_38 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f271,definition,
( spl1_40
<=> ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v1)
| r(X0,v5)
| r(X0,v1) ) ),
introduced(definition,[new_symbols(definition,[spl1_40])],[avatar_definition]) ).
fof(f272,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v1)
| r(X0,v5)
| r(X0,v1) )
| ~ spl1_40 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f286,definition,
( spl1_44
<=> sQ0_eqProxy(v3,v4) ),
introduced(definition,[new_symbols(definition,[spl1_44])],[avatar_definition]) ).
fof(f287,plain,
( sQ0_eqProxy(v3,v4)
| ~ spl1_44 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f289,definition,
( spl1_45
<=> ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v3)
| r(X0,v4)
| r(X0,v3) ) ),
introduced(definition,[new_symbols(definition,[spl1_45])],[avatar_definition]) ).
fof(f290,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v3)
| r(X0,v4)
| r(X0,v3) )
| ~ spl1_45 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f293,definition,
( spl1_46
<=> sQ0_eqProxy(v2,v4) ),
introduced(definition,[new_symbols(definition,[spl1_46])],[avatar_definition]) ).
fof(f294,plain,
( sQ0_eqProxy(v2,v4)
| ~ spl1_46 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f296,definition,
( spl1_47
<=> ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v2)
| r(X0,v4)
| r(X0,v2) ) ),
introduced(definition,[new_symbols(definition,[spl1_47])],[avatar_definition]) ).
fof(f297,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v2)
| r(X0,v4)
| r(X0,v2) )
| ~ spl1_47 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f300,definition,
( spl1_48
<=> sQ0_eqProxy(v1,v4) ),
introduced(definition,[new_symbols(definition,[spl1_48])],[avatar_definition]) ).
fof(f301,plain,
( sQ0_eqProxy(v1,v4)
| ~ spl1_48 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f303,definition,
( spl1_49
<=> ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v1)
| r(X0,v4)
| r(X0,v1) ) ),
introduced(definition,[new_symbols(definition,[spl1_49])],[avatar_definition]) ).
fof(f304,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v1)
| r(X0,v4)
| r(X0,v1) )
| ~ spl1_49 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f307,definition,
( spl1_50
<=> sQ0_eqProxy(v0,v4) ),
introduced(definition,[new_symbols(definition,[spl1_50])],[avatar_definition]) ).
fof(f308,plain,
( sQ0_eqProxy(v0,v4)
| ~ spl1_50 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f322,definition,
( spl1_54
<=> sQ0_eqProxy(v2,v3) ),
introduced(definition,[new_symbols(definition,[spl1_54])],[avatar_definition]) ).
fof(f323,plain,
( sQ0_eqProxy(v2,v3)
| ~ spl1_54 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f325,definition,
( spl1_55
<=> ! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(X0,v2)
| r(X0,v3)
| r(X0,v2) ) ),
introduced(definition,[new_symbols(definition,[spl1_55])],[avatar_definition]) ).
fof(f326,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(X0,v2)
| r(X0,v3)
| r(X0,v2) )
| ~ spl1_55 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f329,definition,
( spl1_56
<=> sQ0_eqProxy(v1,v3) ),
introduced(definition,[new_symbols(definition,[spl1_56])],[avatar_definition]) ).
fof(f330,plain,
( sQ0_eqProxy(v1,v3)
| ~ spl1_56 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f332,definition,
( spl1_57
<=> ! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(X0,v1)
| r(X0,v3)
| r(X0,v1) ) ),
introduced(definition,[new_symbols(definition,[spl1_57])],[avatar_definition]) ).
fof(f333,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(X0,v1)
| r(X0,v3)
| r(X0,v1) )
| ~ spl1_57 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f336,definition,
( spl1_58
<=> sQ0_eqProxy(v0,v3) ),
introduced(definition,[new_symbols(definition,[spl1_58])],[avatar_definition]) ).
fof(f337,plain,
( sQ0_eqProxy(v0,v3)
| ~ spl1_58 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f351,definition,
( spl1_62
<=> sQ0_eqProxy(v3,v2) ),
introduced(definition,[new_symbols(definition,[spl1_62])],[avatar_definition]) ).
fof(f352,plain,
( sQ0_eqProxy(v3,v2)
| ~ spl1_62 ),
inference(avatar_component_clause,[],[f351]) ).
fof(f355,definition,
( spl1_63
<=> sQ0_eqProxy(v1,v2) ),
introduced(definition,[new_symbols(definition,[spl1_63])],[avatar_definition]) ).
fof(f356,plain,
( sQ0_eqProxy(v1,v2)
| ~ spl1_63 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f362,definition,
( spl1_65
<=> sQ0_eqProxy(v0,v2) ),
introduced(definition,[new_symbols(definition,[spl1_65])],[avatar_definition]) ).
fof(f363,plain,
( sQ0_eqProxy(v0,v2)
| ~ spl1_65 ),
inference(avatar_component_clause,[],[f362]) ).
fof(f369,definition,
( spl1_67
<=> sQ0_eqProxy(v5,v1) ),
introduced(definition,[new_symbols(definition,[spl1_67])],[avatar_definition]) ).
fof(f370,plain,
( sQ0_eqProxy(v5,v1)
| ~ spl1_67 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f385,definition,
( spl1_71
<=> sQ0_eqProxy(v0,v1) ),
introduced(definition,[new_symbols(definition,[spl1_71])],[avatar_definition]) ).
fof(f386,plain,
( sQ0_eqProxy(v0,v1)
| ~ spl1_71 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f414,plain,
( ~ r(v0,v5)
| ~ r(v0,v4)
| sQ0_eqProxy(v0,v4)
| ~ spl1_2 ),
inference(resolution,[],[f76,f32]) ).
fof(f421,plain,
( spl1_50
| ~ spl1_25
| ~ spl1_23
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f414,f75,f149,f156,f307]) ).
fof(f425,plain,
( ~ r(v0,v5)
| ~ r(v0,v3)
| sQ0_eqProxy(v0,v3)
| ~ spl1_4 ),
inference(resolution,[],[f83,f32]) ).
fof(f426,plain,
( ~ r(v1,v5)
| ~ r(v1,v3)
| sQ0_eqProxy(v1,v3)
| ~ spl1_4 ),
inference(resolution,[],[f83,f33]) ).
fof(f427,plain,
( ~ r(v2,v5)
| ~ r(v2,v3)
| sQ0_eqProxy(v2,v3)
| ~ spl1_4 ),
inference(resolution,[],[f83,f34]) ).
fof(f430,plain,
( spl1_54
| ~ spl1_11
| ~ spl1_7
| ~ spl1_4 ),
inference(avatar_split_clause,[],[f427,f82,f93,f107,f322]) ).
fof(f431,plain,
( spl1_56
| ~ spl1_17
| ~ spl1_13
| ~ spl1_4 ),
inference(avatar_split_clause,[],[f426,f82,f114,f128,f329]) ).
fof(f432,plain,
( spl1_58
| ~ spl1_27
| ~ spl1_23
| ~ spl1_4 ),
inference(avatar_split_clause,[],[f425,f82,f149,f163,f336]) ).
fof(f448,definition,
( spl1_78
<=> r(v3,v2) ),
introduced(definition,[new_symbols(definition,[spl1_78])],[avatar_definition]) ).
fof(f455,plain,
( ~ r(v1,v4)
| ~ r(v1,v2)
| sQ0_eqProxy(v1,v2)
| ~ spl1_10 ),
inference(resolution,[],[f104,f29]) ).
fof(f458,plain,
( spl1_63
| ~ spl1_19
| ~ spl1_15
| ~ spl1_10 ),
inference(avatar_split_clause,[],[f455,f103,f121,f135,f355]) ).
fof(f463,plain,
( ~ r(v0,v3)
| ~ r(v0,v2)
| sQ0_eqProxy(v0,v2)
| ~ spl1_12 ),
inference(resolution,[],[f111,f25]) ).
fof(f464,plain,
( ~ r(v1,v3)
| ~ r(v1,v2)
| sQ0_eqProxy(v1,v2)
| ~ spl1_12 ),
inference(resolution,[],[f111,f26]) ).
fof(f466,plain,
( spl1_63
| ~ spl1_19
| ~ spl1_17
| ~ spl1_12 ),
inference(avatar_split_clause,[],[f464,f110,f128,f135,f355]) ).
fof(f467,plain,
( spl1_65
| ~ spl1_29
| ~ spl1_27
| ~ spl1_12 ),
inference(avatar_split_clause,[],[f463,f110,f163,f170,f362]) ).
fof(f506,plain,
( ~ r(v0,v2)
| ~ r(v0,v1)
| sQ0_eqProxy(v0,v1)
| ~ spl1_20 ),
inference(resolution,[],[f139,f23]) ).
fof(f580,plain,
( ~ r(v1,v5)
| ~ r(v1,v4)
| sQ0_eqProxy(v1,v4)
| ~ spl1_2 ),
inference(resolution,[],[f76,f33]) ).
fof(f581,plain,
( ~ r(v2,v5)
| ~ r(v2,v4)
| sQ0_eqProxy(v2,v4)
| ~ spl1_2 ),
inference(resolution,[],[f76,f34]) ).
fof(f582,plain,
( ~ r(v3,v5)
| ~ r(v3,v4)
| sQ0_eqProxy(v3,v4)
| ~ spl1_2 ),
inference(resolution,[],[f76,f35]) ).
fof(f591,plain,
( $false
| ~ spl1_50 ),
inference(resolution,[],[f308,f28]) ).
fof(f592,plain,
~ spl1_50,
inference(avatar_contradiction_clause,[],[f591]) ).
fof(f593,plain,
( sQ0_eqProxy(v0,v2)
| r(v0,v5)
| r(v0,v2)
| ~ spl1_38 ),
inference(resolution,[],[f265,f32]) ).
fof(f594,plain,
( sQ0_eqProxy(v1,v2)
| r(v1,v5)
| r(v1,v2)
| ~ spl1_38 ),
inference(resolution,[],[f265,f33]) ).
fof(f596,plain,
( sQ0_eqProxy(v3,v2)
| r(v3,v5)
| r(v3,v2)
| ~ spl1_38 ),
inference(resolution,[],[f265,f35]) ).
fof(f604,plain,
( spl1_78
| spl1_3
| spl1_62
| ~ spl1_38 ),
inference(avatar_split_clause,[],[f596,f264,f351,f79,f448]) ).
fof(f642,plain,
( sQ0_eqProxy(v0,v3)
| r(v0,v4)
| r(v0,v3)
| ~ spl1_45 ),
inference(resolution,[],[f290,f28]) ).
fof(f643,plain,
( sQ0_eqProxy(v1,v3)
| r(v1,v4)
| r(v1,v3)
| ~ spl1_45 ),
inference(resolution,[],[f290,f29]) ).
fof(f644,plain,
( sQ0_eqProxy(v2,v3)
| r(v2,v4)
| r(v2,v3)
| ~ spl1_45 ),
inference(resolution,[],[f290,f30]) ).
fof(f652,plain,
( $false
| ~ spl1_44 ),
inference(resolution,[],[f287,f31]) ).
fof(f653,plain,
~ spl1_44,
inference(avatar_contradiction_clause,[],[f652]) ).
fof(f661,plain,
( spl1_48
| ~ spl1_15
| ~ spl1_13
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f580,f75,f114,f121,f300]) ).
fof(f664,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(v2,v5)
| r(X0,v2)
| r(X0,v5)
| sQ0_eqProxy(X0,v2) )
| spl1_7 ),
inference(resolution,[],[f94,f21]) ).
fof(f671,plain,
( $false
| ~ spl1_48 ),
inference(resolution,[],[f301,f29]) ).
fof(f672,plain,
~ spl1_48,
inference(avatar_contradiction_clause,[],[f671]) ).
fof(f681,plain,
( spl1_27
| spl1_25
| spl1_58
| ~ spl1_45 ),
inference(avatar_split_clause,[],[f642,f289,f336,f156,f163]) ).
fof(f682,plain,
( spl1_17
| spl1_15
| spl1_56
| ~ spl1_45 ),
inference(avatar_split_clause,[],[f643,f289,f329,f121,f128]) ).
fof(f683,plain,
( spl1_11
| spl1_9
| spl1_54
| ~ spl1_45 ),
inference(avatar_split_clause,[],[f644,f289,f322,f100,f107]) ).
fof(f684,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(v3,v4)
| r(X0,v3)
| r(X0,v4)
| sQ0_eqProxy(X0,v3) )
| spl1_5 ),
inference(resolution,[],[f87,f21]) ).
fof(f686,plain,
( spl1_44
| spl1_45
| spl1_5 ),
inference(avatar_split_clause,[],[f684,f86,f289,f286]) ).
fof(f687,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(v1,v4)
| r(X0,v1)
| r(X0,v4)
| sQ0_eqProxy(X0,v1) )
| spl1_15 ),
inference(resolution,[],[f122,f21]) ).
fof(f689,plain,
( spl1_48
| spl1_49
| spl1_15 ),
inference(avatar_split_clause,[],[f687,f121,f303,f300]) ).
fof(f690,plain,
( ~ r(v0,v4)
| ~ r(v0,v3)
| sQ0_eqProxy(v0,v3)
| ~ spl1_6 ),
inference(resolution,[],[f90,f28]) ).
fof(f691,plain,
( ~ r(v1,v4)
| ~ r(v1,v3)
| sQ0_eqProxy(v1,v3)
| ~ spl1_6 ),
inference(resolution,[],[f90,f29]) ).
fof(f692,plain,
( ~ r(v2,v4)
| ~ r(v2,v3)
| sQ0_eqProxy(v2,v3)
| ~ spl1_6 ),
inference(resolution,[],[f90,f30]) ).
fof(f694,plain,
( $false
| ~ spl1_56 ),
inference(resolution,[],[f330,f26]) ).
fof(f695,plain,
~ spl1_56,
inference(avatar_contradiction_clause,[],[f694]) ).
fof(f696,plain,
( spl1_37
| spl1_38
| spl1_7 ),
inference(avatar_split_clause,[],[f664,f93,f264,f261]) ).
fof(f706,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v1)
| sQ0_eqProxy(v5,v1)
| r(X0,v5)
| r(X0,v1)
| sQ0_eqProxy(X0,v5) )
| spl1_13 ),
inference(resolution,[],[f186,f21]) ).
fof(f708,plain,
( spl1_67
| spl1_40
| spl1_13 ),
inference(avatar_split_clause,[],[f706,f114,f271,f369]) ).
fof(f709,plain,
( ~ r(v0,v4)
| ~ r(v0,v1)
| sQ0_eqProxy(v0,v1)
| ~ spl1_16 ),
inference(resolution,[],[f125,f28]) ).
fof(f713,plain,
( $false
| ~ spl1_37 ),
inference(resolution,[],[f262,f34]) ).
fof(f714,plain,
~ spl1_37,
inference(avatar_contradiction_clause,[],[f713]) ).
fof(f715,plain,
( spl1_29
| spl1_23
| spl1_65
| ~ spl1_38 ),
inference(avatar_split_clause,[],[f593,f264,f362,f149,f170]) ).
fof(f716,plain,
( spl1_19
| spl1_13
| spl1_63
| ~ spl1_38 ),
inference(avatar_split_clause,[],[f594,f264,f355,f114,f135]) ).
fof(f718,plain,
( ~ r(v0,v3)
| ~ r(v0,v1)
| sQ0_eqProxy(v0,v1)
| ~ spl1_18 ),
inference(resolution,[],[f132,f25]) ).
fof(f726,plain,
( $false
| ~ spl1_58 ),
inference(resolution,[],[f337,f25]) ).
fof(f727,plain,
~ spl1_58,
inference(avatar_contradiction_clause,[],[f726]) ).
fof(f730,plain,
( $false
| ~ spl1_63 ),
inference(resolution,[],[f356,f24]) ).
fof(f731,plain,
~ spl1_63,
inference(avatar_contradiction_clause,[],[f730]) ).
fof(f733,plain,
( spl1_71
| ~ spl1_31
| ~ spl1_29
| ~ spl1_20 ),
inference(avatar_split_clause,[],[f506,f138,f170,f177,f385]) ).
fof(f736,plain,
( spl1_71
| ~ spl1_31
| ~ spl1_27
| ~ spl1_18 ),
inference(avatar_split_clause,[],[f718,f131,f163,f177,f385]) ).
fof(f737,plain,
( spl1_58
| ~ spl1_27
| ~ spl1_25
| ~ spl1_6 ),
inference(avatar_split_clause,[],[f690,f89,f156,f163,f336]) ).
fof(f746,plain,
( spl1_54
| ~ spl1_11
| ~ spl1_9
| ~ spl1_6 ),
inference(avatar_split_clause,[],[f692,f89,f100,f107,f322]) ).
fof(f748,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(v2,v3)
| r(X0,v2)
| r(X0,v3)
| sQ0_eqProxy(X0,v2) )
| spl1_11 ),
inference(resolution,[],[f108,f21]) ).
fof(f750,plain,
( spl1_54
| spl1_55
| spl1_11 ),
inference(avatar_split_clause,[],[f748,f107,f325,f322]) ).
fof(f754,plain,
( ~ r(v0,v4)
| ~ r(v0,v2)
| sQ0_eqProxy(v0,v2)
| ~ spl1_10 ),
inference(resolution,[],[f104,f28]) ).
fof(f757,plain,
( ~ r(v3,v4)
| ~ r(v3,v2)
| sQ0_eqProxy(v3,v2)
| ~ spl1_10 ),
inference(resolution,[],[f104,f31]) ).
fof(f758,plain,
( $false
| ~ spl1_71 ),
inference(resolution,[],[f386,f22]) ).
fof(f759,plain,
~ spl1_71,
inference(avatar_contradiction_clause,[],[f758]) ).
fof(f761,plain,
( spl1_65
| ~ spl1_29
| ~ spl1_25
| ~ spl1_10 ),
inference(avatar_split_clause,[],[f754,f103,f156,f170,f362]) ).
fof(f773,plain,
( $false
| ~ spl1_65 ),
inference(resolution,[],[f363,f23]) ).
fof(f774,plain,
~ spl1_65,
inference(avatar_contradiction_clause,[],[f773]) ).
fof(f784,plain,
( $false
| ~ spl1_46 ),
inference(resolution,[],[f294,f30]) ).
fof(f785,plain,
~ spl1_46,
inference(avatar_contradiction_clause,[],[f784]) ).
fof(f790,plain,
( $false
| ~ spl1_54 ),
inference(resolution,[],[f323,f27]) ).
fof(f791,plain,
~ spl1_54,
inference(avatar_contradiction_clause,[],[f790]) ).
fof(f798,plain,
( ~ r(v0,v5)
| ~ r(v0,v2)
| sQ0_eqProxy(v0,v2)
| ~ spl1_8 ),
inference(resolution,[],[f97,f32]) ).
fof(f799,plain,
( ~ r(v1,v5)
| ~ r(v1,v2)
| sQ0_eqProxy(v1,v2)
| ~ spl1_8 ),
inference(resolution,[],[f97,f33]) ).
fof(f804,plain,
( $false
| ~ spl1_33 ),
inference(resolution,[],[f248,f36]) ).
fof(f805,plain,
~ spl1_33,
inference(avatar_contradiction_clause,[],[f804]) ).
fof(f808,plain,
( spl1_46
| ~ spl1_9
| ~ spl1_7
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f581,f75,f93,f100,f293]) ).
fof(f809,plain,
( spl1_44
| ~ spl1_5
| ~ spl1_3
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f582,f75,f79,f86,f286]) ).
fof(f812,plain,
( spl1_62
| ~ spl1_78
| ~ spl1_5
| ~ spl1_10 ),
inference(avatar_split_clause,[],[f757,f103,f86,f448,f351]) ).
fof(f831,plain,
( $false
| ~ spl1_35 ),
inference(resolution,[],[f255,f35]) ).
fof(f832,plain,
~ spl1_35,
inference(avatar_contradiction_clause,[],[f831]) ).
fof(f870,plain,
( spl1_63
| ~ spl1_19
| ~ spl1_13
| ~ spl1_8 ),
inference(avatar_split_clause,[],[f799,f96,f114,f135,f355]) ).
fof(f872,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(v4,v5)
| r(X0,v4)
| r(X0,v5)
| sQ0_eqProxy(X0,v4) )
| spl1_1 ),
inference(resolution,[],[f73,f21]) ).
fof(f874,plain,
( spl1_33
| spl1_34
| spl1_1 ),
inference(avatar_split_clause,[],[f872,f72,f250,f247]) ).
fof(f881,plain,
( ~ r(v0,v5)
| ~ r(v0,v1)
| sQ0_eqProxy(v0,v1)
| ~ spl1_14 ),
inference(resolution,[],[f118,f32]) ).
fof(f897,plain,
( sQ0_eqProxy(v0,v4)
| r(v0,v5)
| r(v0,v4)
| ~ spl1_34 ),
inference(resolution,[],[f251,f32]) ).
fof(f898,plain,
( sQ0_eqProxy(v1,v4)
| r(v1,v5)
| r(v1,v4)
| ~ spl1_34 ),
inference(resolution,[],[f251,f33]) ).
fof(f899,plain,
( sQ0_eqProxy(v2,v4)
| r(v2,v5)
| r(v2,v4)
| ~ spl1_34 ),
inference(resolution,[],[f251,f34]) ).
fof(f900,plain,
( sQ0_eqProxy(v3,v4)
| r(v3,v5)
| r(v3,v4)
| ~ spl1_34 ),
inference(resolution,[],[f251,f35]) ).
fof(f902,plain,
( spl1_5
| spl1_3
| spl1_44
| ~ spl1_34 ),
inference(avatar_split_clause,[],[f900,f250,f286,f79,f86]) ).
fof(f903,plain,
( spl1_9
| spl1_7
| spl1_46
| ~ spl1_34 ),
inference(avatar_split_clause,[],[f899,f250,f293,f93,f100]) ).
fof(f904,plain,
( spl1_15
| spl1_13
| spl1_48
| ~ spl1_34 ),
inference(avatar_split_clause,[],[f898,f250,f300,f114,f121]) ).
fof(f905,plain,
( spl1_25
| spl1_23
| spl1_50
| ~ spl1_34 ),
inference(avatar_split_clause,[],[f897,f250,f307,f149,f156]) ).
fof(f906,plain,
( sQ0_eqProxy(v0,v1)
| r(v0,v5)
| r(v0,v1)
| ~ spl1_40 ),
inference(resolution,[],[f272,f32]) ).
fof(f914,plain,
( spl1_31
| spl1_23
| spl1_71
| ~ spl1_40 ),
inference(avatar_split_clause,[],[f906,f271,f385,f149,f177]) ).
fof(f925,plain,
( sQ0_eqProxy(v0,v1)
| r(v0,v4)
| r(v0,v1)
| ~ spl1_49 ),
inference(resolution,[],[f304,f28]) ).
fof(f931,plain,
( spl1_31
| spl1_25
| spl1_71
| ~ spl1_49 ),
inference(avatar_split_clause,[],[f925,f303,f385,f156,f177]) ).
fof(f939,plain,
( $false
| ~ spl1_67 ),
inference(resolution,[],[f370,f47]) ).
fof(f940,plain,
~ spl1_67,
inference(avatar_contradiction_clause,[],[f939]) ).
fof(f941,plain,
( sQ0_eqProxy(v0,v2)
| r(v0,v3)
| r(v0,v2)
| ~ spl1_55 ),
inference(resolution,[],[f326,f25]) ).
fof(f942,plain,
( sQ0_eqProxy(v1,v2)
| r(v1,v3)
| r(v1,v2)
| ~ spl1_55 ),
inference(resolution,[],[f326,f26]) ).
fof(f944,plain,
( spl1_19
| spl1_17
| spl1_63
| ~ spl1_55 ),
inference(avatar_split_clause,[],[f942,f325,f355,f128,f135]) ).
fof(f945,plain,
( spl1_29
| spl1_27
| spl1_65
| ~ spl1_55 ),
inference(avatar_split_clause,[],[f941,f325,f362,f163,f170]) ).
fof(f948,plain,
( spl1_71
| ~ spl1_31
| ~ spl1_25
| ~ spl1_16 ),
inference(avatar_split_clause,[],[f709,f124,f156,f177,f385]) ).
fof(f965,plain,
( spl1_65
| ~ spl1_29
| ~ spl1_23
| ~ spl1_8 ),
inference(avatar_split_clause,[],[f798,f96,f149,f170,f362]) ).
fof(f967,plain,
( spl1_71
| ~ spl1_31
| ~ spl1_23
| ~ spl1_14 ),
inference(avatar_split_clause,[],[f881,f117,f149,f177,f385]) ).
fof(f972,plain,
( spl1_56
| ~ spl1_17
| ~ spl1_15
| ~ spl1_6 ),
inference(avatar_split_clause,[],[f691,f89,f121,f128,f329]) ).
fof(f976,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(v3,v5)
| r(X0,v3)
| r(X0,v5)
| sQ0_eqProxy(X0,v3) )
| spl1_3 ),
inference(resolution,[],[f80,f21]) ).
fof(f978,plain,
( spl1_35
| spl1_36
| spl1_3 ),
inference(avatar_split_clause,[],[f976,f79,f257,f254]) ).
fof(f979,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(v2,v4)
| r(X0,v2)
| r(X0,v4)
| sQ0_eqProxy(X0,v2) )
| spl1_9 ),
inference(resolution,[],[f101,f21]) ).
fof(f981,plain,
( spl1_46
| spl1_47
| spl1_9 ),
inference(avatar_split_clause,[],[f979,f100,f296,f293]) ).
fof(f982,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(v1,v3)
| r(X0,v1)
| r(X0,v3)
| sQ0_eqProxy(X0,v1) )
| spl1_17 ),
inference(resolution,[],[f129,f21]) ).
fof(f984,plain,
( spl1_56
| spl1_57
| spl1_17 ),
inference(avatar_split_clause,[],[f982,f128,f332,f329]) ).
fof(f1024,plain,
( sQ0_eqProxy(v0,v3)
| r(v0,v5)
| r(v0,v3)
| ~ spl1_36 ),
inference(resolution,[],[f258,f32]) ).
fof(f1025,plain,
( sQ0_eqProxy(v1,v3)
| r(v1,v5)
| r(v1,v3)
| ~ spl1_36 ),
inference(resolution,[],[f258,f33]) ).
fof(f1026,plain,
( sQ0_eqProxy(v2,v3)
| r(v2,v5)
| r(v2,v3)
| ~ spl1_36 ),
inference(resolution,[],[f258,f34]) ).
fof(f1029,plain,
( spl1_11
| spl1_7
| spl1_54
| ~ spl1_36 ),
inference(avatar_split_clause,[],[f1026,f257,f322,f93,f107]) ).
fof(f1030,plain,
( spl1_17
| spl1_13
| spl1_56
| ~ spl1_36 ),
inference(avatar_split_clause,[],[f1025,f257,f329,f114,f128]) ).
fof(f1031,plain,
( spl1_27
| spl1_23
| spl1_58
| ~ spl1_36 ),
inference(avatar_split_clause,[],[f1024,f257,f336,f149,f163]) ).
fof(f1032,plain,
( sQ0_eqProxy(v0,v2)
| r(v0,v4)
| r(v0,v2)
| ~ spl1_47 ),
inference(resolution,[],[f297,f28]) ).
fof(f1033,plain,
( sQ0_eqProxy(v1,v2)
| r(v1,v4)
| r(v1,v2)
| ~ spl1_47 ),
inference(resolution,[],[f297,f29]) ).
fof(f1037,plain,
( spl1_19
| spl1_15
| spl1_63
| ~ spl1_47 ),
inference(avatar_split_clause,[],[f1033,f296,f355,f121,f135]) ).
fof(f1038,plain,
( spl1_29
| spl1_25
| spl1_65
| ~ spl1_47 ),
inference(avatar_split_clause,[],[f1032,f296,f362,f156,f170]) ).
fof(f1039,plain,
( $false
| ~ spl1_62 ),
inference(resolution,[],[f352,f48]) ).
fof(f1040,plain,
~ spl1_62,
inference(avatar_contradiction_clause,[],[f1039]) ).
fof(f1041,plain,
( sQ0_eqProxy(v0,v1)
| r(v0,v3)
| r(v0,v1)
| ~ spl1_57 ),
inference(resolution,[],[f333,f25]) ).
fof(f1045,plain,
( spl1_31
| spl1_27
| spl1_71
| ~ spl1_57 ),
inference(avatar_split_clause,[],[f1041,f332,f385,f163,f177]) ).
cnf(s1,plain,
( ~ spl1_1
| spl1_2 ),
inference(sat_conversion,[],[f77]) ).
cnf(s2,plain,
( ~ spl1_3
| spl1_4 ),
inference(sat_conversion,[],[f84]) ).
cnf(s3,plain,
( ~ spl1_5
| spl1_6 ),
inference(sat_conversion,[],[f91]) ).
cnf(s4,plain,
( ~ spl1_7
| spl1_8 ),
inference(sat_conversion,[],[f98]) ).
cnf(s5,plain,
( ~ spl1_9
| spl1_10 ),
inference(sat_conversion,[],[f105]) ).
cnf(s6,plain,
( ~ spl1_11
| spl1_12 ),
inference(sat_conversion,[],[f112]) ).
cnf(s7,plain,
( ~ spl1_13
| spl1_14 ),
inference(sat_conversion,[],[f119]) ).
cnf(s8,plain,
( ~ spl1_15
| spl1_16 ),
inference(sat_conversion,[],[f126]) ).
cnf(s9,plain,
( ~ spl1_17
| spl1_18 ),
inference(sat_conversion,[],[f133]) ).
cnf(s10,plain,
( ~ spl1_19
| spl1_20 ),
inference(sat_conversion,[],[f140]) ).
cnf(s53,plain,
( ~ spl1_2
| ~ spl1_23
| ~ spl1_25
| spl1_50 ),
inference(sat_conversion,[],[f421]) ).
cnf(s55,plain,
( ~ spl1_4
| ~ spl1_7
| ~ spl1_11
| spl1_54 ),
inference(sat_conversion,[],[f430]) ).
cnf(s56,plain,
( ~ spl1_4
| ~ spl1_13
| ~ spl1_17
| spl1_56 ),
inference(sat_conversion,[],[f431]) ).
cnf(s57,plain,
( ~ spl1_4
| ~ spl1_23
| ~ spl1_27
| spl1_58 ),
inference(sat_conversion,[],[f432]) ).
cnf(s63,plain,
( ~ spl1_10
| ~ spl1_15
| ~ spl1_19
| spl1_63 ),
inference(sat_conversion,[],[f458]) ).
cnf(s66,plain,
( ~ spl1_12
| ~ spl1_17
| ~ spl1_19
| spl1_63 ),
inference(sat_conversion,[],[f466]) ).
cnf(s67,plain,
( ~ spl1_12
| ~ spl1_27
| ~ spl1_29
| spl1_65 ),
inference(sat_conversion,[],[f467]) ).
cnf(s101,plain,
~ spl1_50,
inference(sat_conversion,[],[f592]) ).
cnf(s103,plain,
( spl1_3
| ~ spl1_38
| spl1_62
| spl1_78 ),
inference(sat_conversion,[],[f604]) ).
cnf(s118,plain,
~ spl1_44,
inference(sat_conversion,[],[f653]) ).
cnf(s125,plain,
( ~ spl1_2
| ~ spl1_13
| ~ spl1_15
| spl1_48 ),
inference(sat_conversion,[],[f661]) ).
cnf(s128,plain,
~ spl1_48,
inference(sat_conversion,[],[f672]) ).
cnf(s134,plain,
( spl1_25
| spl1_27
| ~ spl1_45
| spl1_58 ),
inference(sat_conversion,[],[f681]) ).
cnf(s135,plain,
( spl1_15
| spl1_17
| ~ spl1_45
| spl1_56 ),
inference(sat_conversion,[],[f682]) ).
cnf(s136,plain,
( spl1_9
| spl1_11
| ~ spl1_45
| spl1_54 ),
inference(sat_conversion,[],[f683]) ).
cnf(s138,plain,
( spl1_5
| spl1_44
| spl1_45 ),
inference(sat_conversion,[],[f686]) ).
cnf(s140,plain,
( spl1_15
| spl1_48
| spl1_49 ),
inference(sat_conversion,[],[f689]) ).
cnf(s141,plain,
~ spl1_56,
inference(sat_conversion,[],[f695]) ).
cnf(s142,plain,
( spl1_7
| spl1_37
| spl1_38 ),
inference(sat_conversion,[],[f696]) ).
cnf(s147,plain,
( spl1_13
| spl1_40
| spl1_67 ),
inference(sat_conversion,[],[f708]) ).
cnf(s148,plain,
~ spl1_37,
inference(sat_conversion,[],[f714]) ).
cnf(s149,plain,
( spl1_23
| spl1_29
| ~ spl1_38
| spl1_65 ),
inference(sat_conversion,[],[f715]) ).
cnf(s150,plain,
( spl1_13
| spl1_19
| ~ spl1_38
| spl1_63 ),
inference(sat_conversion,[],[f716]) ).
cnf(s156,plain,
~ spl1_58,
inference(sat_conversion,[],[f727]) ).
cnf(s159,plain,
~ spl1_63,
inference(sat_conversion,[],[f731]) ).
cnf(s163,plain,
( ~ spl1_20
| ~ spl1_29
| ~ spl1_31
| spl1_71 ),
inference(sat_conversion,[],[f733]) ).
cnf(s168,plain,
( ~ spl1_18
| ~ spl1_27
| ~ spl1_31
| spl1_71 ),
inference(sat_conversion,[],[f736]) ).
cnf(s169,plain,
( ~ spl1_6
| ~ spl1_25
| ~ spl1_27
| spl1_58 ),
inference(sat_conversion,[],[f737]) ).
cnf(s177,plain,
( ~ spl1_6
| ~ spl1_9
| ~ spl1_11
| spl1_54 ),
inference(sat_conversion,[],[f746]) ).
cnf(s181,plain,
( spl1_11
| spl1_54
| spl1_55 ),
inference(sat_conversion,[],[f750]) ).
cnf(s184,plain,
~ spl1_71,
inference(sat_conversion,[],[f759]) ).
cnf(s189,plain,
( ~ spl1_10
| ~ spl1_25
| ~ spl1_29
| spl1_65 ),
inference(sat_conversion,[],[f761]) ).
cnf(s196,plain,
~ spl1_65,
inference(sat_conversion,[],[f774]) ).
cnf(s202,plain,
~ spl1_46,
inference(sat_conversion,[],[f785]) ).
cnf(s206,plain,
~ spl1_54,
inference(sat_conversion,[],[f791]) ).
cnf(s210,plain,
~ spl1_33,
inference(sat_conversion,[],[f805]) ).
cnf(s213,plain,
( ~ spl1_2
| ~ spl1_7
| ~ spl1_9
| spl1_46 ),
inference(sat_conversion,[],[f808]) ).
cnf(s214,plain,
( ~ spl1_2
| ~ spl1_3
| ~ spl1_5
| spl1_44 ),
inference(sat_conversion,[],[f809]) ).
cnf(s219,plain,
( ~ spl1_5
| ~ spl1_10
| spl1_62
| ~ spl1_78 ),
inference(sat_conversion,[],[f812]) ).
cnf(s227,plain,
~ spl1_35,
inference(sat_conversion,[],[f832]) ).
cnf(s249,plain,
( ~ spl1_8
| ~ spl1_13
| ~ spl1_19
| spl1_63 ),
inference(sat_conversion,[],[f870]) ).
cnf(s251,plain,
( spl1_1
| spl1_33
| spl1_34 ),
inference(sat_conversion,[],[f874]) ).
cnf(s261,plain,
( spl1_3
| spl1_5
| ~ spl1_34
| spl1_44 ),
inference(sat_conversion,[],[f902]) ).
cnf(s262,plain,
( spl1_7
| spl1_9
| ~ spl1_34
| spl1_46 ),
inference(sat_conversion,[],[f903]) ).
cnf(s263,plain,
( spl1_13
| spl1_15
| ~ spl1_34
| spl1_48 ),
inference(sat_conversion,[],[f904]) ).
cnf(s264,plain,
( spl1_23
| spl1_25
| ~ spl1_34
| spl1_50 ),
inference(sat_conversion,[],[f905]) ).
cnf(s268,plain,
( spl1_23
| spl1_31
| ~ spl1_40
| spl1_71 ),
inference(sat_conversion,[],[f914]) ).
cnf(s274,plain,
( spl1_25
| spl1_31
| ~ spl1_49
| spl1_71 ),
inference(sat_conversion,[],[f931]) ).
cnf(s278,plain,
~ spl1_67,
inference(sat_conversion,[],[f940]) ).
cnf(s279,plain,
( spl1_17
| spl1_19
| ~ spl1_55
| spl1_63 ),
inference(sat_conversion,[],[f944]) ).
cnf(s280,plain,
( spl1_27
| spl1_29
| ~ spl1_55
| spl1_65 ),
inference(sat_conversion,[],[f945]) ).
cnf(s286,plain,
( ~ spl1_16
| ~ spl1_25
| ~ spl1_31
| spl1_71 ),
inference(sat_conversion,[],[f948]) ).
cnf(s301,plain,
( ~ spl1_8
| ~ spl1_23
| ~ spl1_29
| spl1_65 ),
inference(sat_conversion,[],[f965]) ).
cnf(s303,plain,
( ~ spl1_14
| ~ spl1_23
| ~ spl1_31
| spl1_71 ),
inference(sat_conversion,[],[f967]) ).
cnf(s305,plain,
( ~ spl1_6
| ~ spl1_15
| ~ spl1_17
| spl1_56 ),
inference(sat_conversion,[],[f972]) ).
cnf(s318,plain,
( spl1_3
| spl1_35
| spl1_36 ),
inference(sat_conversion,[],[f978]) ).
cnf(s320,plain,
( spl1_9
| spl1_46
| spl1_47 ),
inference(sat_conversion,[],[f981]) ).
cnf(s322,plain,
( spl1_17
| spl1_56
| spl1_57 ),
inference(sat_conversion,[],[f984]) ).
cnf(s332,plain,
( spl1_7
| spl1_11
| ~ spl1_36
| spl1_54 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s333,plain,
( spl1_13
| spl1_17
| ~ spl1_36
| spl1_56 ),
inference(sat_conversion,[],[f1030]) ).
cnf(s334,plain,
( spl1_23
| spl1_27
| ~ spl1_36
| spl1_58 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s336,plain,
( spl1_15
| spl1_19
| ~ spl1_47
| spl1_63 ),
inference(sat_conversion,[],[f1037]) ).
cnf(s337,plain,
( spl1_25
| spl1_29
| ~ spl1_47
| spl1_65 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s338,plain,
~ spl1_62,
inference(sat_conversion,[],[f1040]) ).
cnf(s340,plain,
( spl1_27
| spl1_31
| ~ spl1_57
| spl1_71 ),
inference(sat_conversion,[],[f1045]) ).
cnf(s346,plain,
( ~ spl1_5
| ~ spl1_10
| ~ spl1_78 ),
inference(rat,[],[s219,s338]) ).
cnf(s354,plain,
( ~ spl1_10
| ~ spl1_25
| ~ spl1_29 ),
inference(rat,[],[s189,s196]) ).
cnf(s355,plain,
( spl1_11
| spl1_55 ),
inference(rat,[],[s181,s206]) ).
cnf(s356,plain,
( ~ spl1_6
| ~ spl1_9
| ~ spl1_11 ),
inference(rat,[],[s177,s206]) ).
cnf(s357,plain,
( ~ spl1_18
| ~ spl1_27
| ~ spl1_31 ),
inference(rat,[],[s168,s184]) ).
cnf(s359,plain,
( ~ spl1_20
| ~ spl1_29
| ~ spl1_31 ),
inference(rat,[],[s163,s184]) ).
cnf(s364,plain,
( spl1_13
| spl1_19
| ~ spl1_38 ),
inference(rat,[],[s150,s159]) ).
cnf(s365,plain,
( spl1_23
| spl1_29
| ~ spl1_38 ),
inference(rat,[],[s149,s196]) ).
cnf(s366,plain,
( spl1_13
| spl1_40 ),
inference(rat,[],[s147,s278]) ).
cnf(s368,plain,
( spl1_7
| spl1_38 ),
inference(rat,[],[s142,s148]) ).
cnf(s369,plain,
( spl1_9
| spl1_11
| ~ spl1_45 ),
inference(rat,[],[s136,s206]) ).
cnf(s370,plain,
( spl1_15
| spl1_17
| ~ spl1_45 ),
inference(rat,[],[s135,s141]) ).
cnf(s371,plain,
( spl1_25
| spl1_27
| ~ spl1_45 ),
inference(rat,[],[s134,s156]) ).
cnf(s372,plain,
( ~ spl1_2
| ~ spl1_13
| ~ spl1_15 ),
inference(rat,[],[s125,s128]) ).
cnf(s383,plain,
( spl1_3
| ~ spl1_38
| spl1_78 ),
inference(rat,[],[s103,s338]) ).
cnf(s401,plain,
( ~ spl1_12
| ~ spl1_27
| ~ spl1_29 ),
inference(rat,[],[s67,s196]) ).
cnf(s402,plain,
( ~ spl1_12
| ~ spl1_17
| ~ spl1_19 ),
inference(rat,[],[s66,s159]) ).
cnf(s405,plain,
( ~ spl1_10
| ~ spl1_15
| ~ spl1_19 ),
inference(rat,[],[s63,s159]) ).
cnf(s409,plain,
( ~ spl1_4
| ~ spl1_23
| ~ spl1_27 ),
inference(rat,[],[s57,s156]) ).
cnf(s410,plain,
( ~ spl1_4
| ~ spl1_13
| ~ spl1_17 ),
inference(rat,[],[s56,s141]) ).
cnf(s411,plain,
( ~ spl1_4
| ~ spl1_7
| ~ spl1_11 ),
inference(rat,[],[s55,s206]) ).
cnf(s413,plain,
( ~ spl1_2
| ~ spl1_23
| ~ spl1_25 ),
inference(rat,[],[s53,s101]) ).
cnf(s433,plain,
( spl1_7
| spl1_3
| ~ spl1_34 ),
inference(rat,[],[s356,s262,s332,s318,s3,s261,s202,s206,s118,s227]) ).
cnf(s434,plain,
( spl1_13
| spl1_3
| ~ spl1_34 ),
inference(rat,[],[s305,s263,s333,s318,s3,s261,s141,s128,s118,s227]) ).
cnf(s435,plain,
( ~ spl1_25
| ~ spl1_9
| ~ spl1_6 ),
inference(rat,[],[s280,s169,s354,s5,s355,s356,s196,s156]) ).
cnf(s436,plain,
( ~ spl1_9
| spl1_3
| ~ spl1_34 ),
inference(rat,[],[s303,s264,s274,s435,s140,s305,s279,s355,s356,s3,s261,s249,s4,s433,s7,s434,s184,s101,s128,s141,s159,s118]) ).
cnf(s437,plain,
( ~ spl1_25
| ~ spl1_57
| ~ spl1_16
| ~ spl1_6 ),
inference(rat,[],[s340,s286,s169,s184,s156]) ).
cnf(s438,plain,
( spl1_3
| ~ spl1_34 ),
inference(rat,[],[s301,s264,s337,s437,s322,s8,s305,s336,s320,s436,s249,s434,s4,s433,s3,s261,s118,s202,s159,s141,s101,s196]) ).
cnf(s439,plain,
( spl1_9
| spl1_15
| ~ spl1_34 ),
inference(rat,[],[s249,s4,s336,s262,s320,s263,s159,s202,s128]) ).
cnf(s440,plain,
( spl1_15
| ~ spl1_6
| ~ spl1_34 ),
inference(rat,[],[s303,s274,s264,s435,s439,s7,s263,s140,s184,s101,s128]) ).
cnf(s441,plain,
( ~ spl1_9
| ~ spl1_15
| ~ spl1_6 ),
inference(rat,[],[s279,s355,s405,s356,s5,s305,s159,s141]) ).
cnf(s442,plain,
( ~ spl1_6
| ~ spl1_34 ),
inference(rat,[],[s301,s4,s337,s262,s320,s441,s264,s437,s322,s8,s305,s440,s141,s101,s202,s196]) ).
cnf(s443,plain,
( spl1_15
| ~ spl1_34 ),
inference(rat,[],[s410,s370,s263,s2,s438,s138,s3,s442,s128,s118]) ).
cnf(s444,plain,
( ~ spl1_25
| spl1_13
| ~ spl1_10
| ~ spl1_34 ),
inference(rat,[],[s409,s280,s268,s354,s286,s8,s366,s355,s411,s368,s364,s405,s443,s2,s438,s196,s184]) ).
cnf(s445,plain,
( spl1_25
| ~ spl1_34 ),
inference(rat,[],[s409,s371,s264,s2,s438,s138,s3,s442,s101,s118]) ).
cnf(s446,plain,
( ~ spl1_10
| ~ spl1_34 ),
inference(rat,[],[s368,s365,s411,s409,s355,s340,s279,s322,s410,s444,s354,s405,s2,s438,s286,s445,s8,s443,s184,s159,s141]) ).
cnf(s447,plain,
~ spl1_34,
inference(rat,[],[s411,s369,s262,s5,s446,s138,s3,s442,s2,s438,s202,s118]) ).
cnf(s448,plain,
spl1_1,
inference(rat,[],[s251,s210,s447]) ).
cnf(s449,plain,
spl1_2,
inference(rat,[],[s1,s448]) ).
cnf(s450,plain,
( ~ spl1_25
| ~ spl1_9 ),
inference(rat,[],[s365,s413,s354,s5,s368,s213,s449,s202]) ).
cnf(s451,plain,
( ~ spl1_5
| ~ spl1_9 ),
inference(rat,[],[s383,s346,s214,s5,s368,s213,s449,s118,s202]) ).
cnf(s452,plain,
( spl1_15
| ~ spl1_9 ),
inference(rat,[],[s357,s9,s370,s274,s140,s371,s138,s451,s450,s184,s128,s118]) ).
cnf(s453,plain,
~ spl1_9,
inference(rat,[],[s364,s405,s372,s452,s368,s213,s5,s449,s202]) ).
cnf(s454,plain,
spl1_47,
inference(rat,[],[s320,s202,s453]) ).
cnf(s456,plain,
( ~ spl1_5
| ~ spl1_25 ),
inference(rat,[],[s334,s318,s169,s214,s3,s413,s156,s227,s449,s118]) ).
cnf(s457,plain,
( spl1_15
| ~ spl1_45 ),
inference(rat,[],[s402,s370,s336,s6,s369,s454,s159,s453]) ).
cnf(s458,plain,
~ spl1_25,
inference(rat,[],[s268,s366,s286,s372,s8,s457,s138,s456,s413,s184,s449,s118]) ).
cnf(s461,plain,
spl1_29,
inference(rat,[],[s337,s196,s454,s458]) ).
cnf(s464,plain,
spl1_15,
inference(rat,[],[s359,s10,s274,s336,s140,s461,s458,s184,s454,s159,s128]) ).
cnf(s467,plain,
~ spl1_13,
inference(rat,[],[s372,s449,s464]) ).
cnf(s469,plain,
~ spl1_45,
inference(rat,[],[s6,s401,s369,s371,s461,s453,s458]) ).
cnf(s470,plain,
spl1_5,
inference(rat,[],[s138,s118,s469]) ).
cnf(s472,plain,
spl1_6,
inference(rat,[],[s3,s470]) ).
cnf(s473,plain,
~ spl1_3,
inference(rat,[],[s214,s118,s449,s470]) ).
cnf(s474,plain,
~ spl1_17,
inference(rat,[],[s305,s141,s464,s472]) ).
cnf(s475,plain,
spl1_36,
inference(rat,[],[s318,s227,s473]) ).
cnf(s478,plain,
$false,
inference(rat,[],[s333,s141,s467,s474,s475]) ).
fof(f1046,plain,
$false,
inference(avatar_sat_refutation,[],[s478]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRA117-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n013.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 08:58:36 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.34/1.18 % (4132108)Input is clausal, will run a generic CNF schedule.
% 2.34/1.18 % (4132186)dis-21_1_sil=8000:lcm=predicate:random_seed=1641310677: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)
% 2.34/1.18 % (4132186)First to succeed.
% 2.34/1.18 % (4132186)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4132108"
% 2.34/1.18 % (4132182)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4249542836:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.34/1.18 % (4132180)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=1082077291:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.34/1.18 % (4132181)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3546218702:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.34/1.18 % (4132184)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2310526088:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.34/1.18 % (4132183)lrs+10_1_sil=8000:sp=occurrence:random_seed=1233364307:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.34/1.18 % (4132185)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4117268073:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.34/1.18 % (4132184)Refutation not found, incomplete strategy
% 2.34/1.18 % (4132184)------------------------------
% 2.34/1.18 % (4132184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.34/1.18 % (4132183)Refutation not found, incomplete strategy
% 2.34/1.18 % (4132183)------------------------------
% 2.34/1.18 % (4132183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.34/1.18 % (4132184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.34/1.18 % (4132183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.34/1.18 % (4132184)CaDiCaL version: 2.1.3
% 2.34/1.18 % (4132183)CaDiCaL version: 2.1.3
% 2.34/1.18 % (4132183)Termination reason: Refutation not found, incomplete strategy
% 2.34/1.18 % (4132183)Time elapsed: 0.001 s
% 2.34/1.18 % (4132184)Termination reason: Refutation not found, incomplete strategy
% 2.34/1.18 % (4132184)Time elapsed: 0.001 s
% 2.34/1.18 % (4132184)Peak memory usage: 85 MB
% 2.34/1.18 % (4132183)Peak memory usage: 86 MB
% 2.34/1.18 % (4132185)Instruction limit reached!
% 2.34/1.18 % (4132185)------------------------------
% 2.34/1.18 % (4132185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.34/1.18 % (4132185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.34/1.18 % (4132185)CaDiCaL version: 2.1.3
% 2.34/1.18 % (4132185)Termination reason: Instruction limit
% 2.34/1.18 % (4132185)Termination phase: Saturation
% 2.34/1.18 % (4132185)Time elapsed: 0.071 s
% 2.34/1.18 % (4132185)Peak memory usage: 87 MB
% 2.34/1.18 % (4132185)Instructions burned: 180 (million)
% 2.34/1.18 % (4132186)Refutation found. Thanks to Tanya!
% 2.34/1.18 % SZS status Unsatisfiable for theBenchmark
% 2.34/1.18 % SZS output start Proof for theBenchmark
% See solution above
% 2.85/1.37 % (4132186)------------------------------
% 2.85/1.37 % (4132186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.85/1.37 % (4132186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.85/1.37 % (4132186)CaDiCaL version: 2.1.3
% 2.85/1.37 % (4132186)Termination reason: Refutation
% 2.85/1.37 % (4132186)Time elapsed: 0.011 s
% 2.85/1.37 % (4132186)Peak memory usage: 89 MB
% 2.85/1.37 % (4132186)Instructions burned: 29 (million)
% 2.85/1.37 % (4132186)------------------------------
% 2.85/1.37 % (4132186)------------------------------
% 2.85/1.37 % (4132108)Success in time 0.323 s
% 2.85/1.37 % Vampire exiting
%------------------------------------------------------------------------------