%------------------------------------------------------------------------------
% 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 : n020.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.82s 1.30s
% Output : Refutation 3.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 69
% Syntax : Number of formulae : 434 ( 94 unt; 51 def)
% Number of atoms : 1272 ( 43 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1412 ( 574 ~; 787 |; 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 : 83 ( 0 sgn 83 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ r(X0,X1)
| r(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rsym) ).
fof(f2,axiom,
! [X0,X1,X2] :
( 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,
! [X0,X1,X2] :
( 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,plain,
! [X0,X1] :
( r(X1,X0)
| ~ r(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f20,plain,
! [X2,X0,X1] :
( X0 = X1
| X0 = X2
| X1 = X2
| ~ r(X0,X1)
| ~ r(X0,X2)
| ~ r(X1,X2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f21,plain,
! [X2,X0,X1] :
( X0 = X1
| X0 = X2
| X1 = X2
| r(X0,X1)
| r(X0,X2)
| r(X1,X2) ),
inference(cnf_transformation,[],[f3]) ).
fof(f22,plain,
v0 != v1,
inference(cnf_transformation,[],[f4]) ).
fof(f23,plain,
v0 != v2,
inference(cnf_transformation,[],[f5]) ).
fof(f24,plain,
v1 != v2,
inference(cnf_transformation,[],[f6]) ).
fof(f25,plain,
v0 != v3,
inference(cnf_transformation,[],[f7]) ).
fof(f26,plain,
v1 != v3,
inference(cnf_transformation,[],[f8]) ).
fof(f27,plain,
v2 != v3,
inference(cnf_transformation,[],[f9]) ).
fof(f28,plain,
v0 != v4,
inference(cnf_transformation,[],[f10]) ).
fof(f29,plain,
v1 != v4,
inference(cnf_transformation,[],[f11]) ).
fof(f30,plain,
v2 != v4,
inference(cnf_transformation,[],[f12]) ).
fof(f31,plain,
v3 != v4,
inference(cnf_transformation,[],[f13]) ).
fof(f32,plain,
v0 != v5,
inference(cnf_transformation,[],[f14]) ).
fof(f33,plain,
v1 != v5,
inference(cnf_transformation,[],[f15]) ).
fof(f34,plain,
v2 != v5,
inference(cnf_transformation,[],[f16]) ).
fof(f35,plain,
v3 != v5,
inference(cnf_transformation,[],[f17]) ).
fof(f36,plain,
v4 != v5,
inference(cnf_transformation,[],[f18]) ).
fof(f37,definition,
! [X0,X1] :
( sQ0_eqProxy(X0,X1)
<=> X0 = X1 ),
introduced(definition,[new_symbols(definition,[sQ0_eqProxy])],[equality_proxy_definition]) ).
fof(f38,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,[],[f20,f37,f37,f37]) ).
fof(f39,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,[],[f21,f37,f37,f37]) ).
fof(f40,plain,
~ sQ0_eqProxy(v0,v1),
inference(equality_proxy_replacement,[],[f22,f37]) ).
fof(f41,plain,
~ sQ0_eqProxy(v0,v2),
inference(equality_proxy_replacement,[],[f23,f37]) ).
fof(f42,plain,
~ sQ0_eqProxy(v1,v2),
inference(equality_proxy_replacement,[],[f24,f37]) ).
fof(f43,plain,
~ sQ0_eqProxy(v0,v3),
inference(equality_proxy_replacement,[],[f25,f37]) ).
fof(f44,plain,
~ sQ0_eqProxy(v1,v3),
inference(equality_proxy_replacement,[],[f26,f37]) ).
fof(f45,plain,
~ sQ0_eqProxy(v2,v3),
inference(equality_proxy_replacement,[],[f27,f37]) ).
fof(f46,plain,
~ sQ0_eqProxy(v0,v4),
inference(equality_proxy_replacement,[],[f28,f37]) ).
fof(f47,plain,
~ sQ0_eqProxy(v1,v4),
inference(equality_proxy_replacement,[],[f29,f37]) ).
fof(f48,plain,
~ sQ0_eqProxy(v2,v4),
inference(equality_proxy_replacement,[],[f30,f37]) ).
fof(f49,plain,
~ sQ0_eqProxy(v3,v4),
inference(equality_proxy_replacement,[],[f31,f37]) ).
fof(f50,plain,
~ sQ0_eqProxy(v0,v5),
inference(equality_proxy_replacement,[],[f32,f37]) ).
fof(f51,plain,
~ sQ0_eqProxy(v1,v5),
inference(equality_proxy_replacement,[],[f33,f37]) ).
fof(f52,plain,
~ sQ0_eqProxy(v2,v5),
inference(equality_proxy_replacement,[],[f34,f37]) ).
fof(f53,plain,
~ sQ0_eqProxy(v3,v5),
inference(equality_proxy_replacement,[],[f35,f37]) ).
fof(f54,plain,
~ sQ0_eqProxy(v4,v5),
inference(equality_proxy_replacement,[],[f36,f37]) ).
fof(f56,plain,
! [X0,X1] :
( sQ0_eqProxy(X1,X0)
| ~ sQ0_eqProxy(X0,X1) ),
inference(equality_proxy_axiom,[],[f37]) ).
fof(f65,plain,
~ sQ0_eqProxy(v5,v1),
inference(resolution,[],[f56,f51]) ).
fof(f66,plain,
~ sQ0_eqProxy(v3,v2),
inference(resolution,[],[f56,f45]) ).
fof(f79,plain,
! [X0] :
( sQ0_eqProxy(X0,v2)
| sQ0_eqProxy(X0,v1)
| ~ r(X0,v1)
| ~ r(X0,v2)
| ~ r(v1,v2) ),
inference(resolution,[],[f38,f42]) ).
fof(f80,plain,
! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(X0,v1)
| ~ r(X0,v1)
| ~ r(X0,v3)
| ~ r(v1,v3) ),
inference(resolution,[],[f38,f44]) ).
fof(f81,plain,
! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v1)
| ~ r(X0,v1)
| ~ r(X0,v4)
| ~ r(v1,v4) ),
inference(resolution,[],[f38,f47]) ).
fof(f82,plain,
! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v1)
| ~ r(X0,v1)
| ~ r(X0,v5)
| ~ r(v1,v5) ),
inference(resolution,[],[f38,f51]) ).
fof(f83,plain,
! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(X0,v2)
| ~ r(X0,v2)
| ~ r(X0,v3)
| ~ r(v2,v3) ),
inference(resolution,[],[f38,f45]) ).
fof(f84,plain,
! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v2)
| ~ r(X0,v2)
| ~ r(X0,v4)
| ~ r(v2,v4) ),
inference(resolution,[],[f38,f48]) ).
fof(f85,plain,
! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v2)
| ~ r(X0,v2)
| ~ r(X0,v5)
| ~ r(v2,v5) ),
inference(resolution,[],[f38,f52]) ).
fof(f86,plain,
! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v3)
| ~ r(X0,v3)
| ~ r(X0,v4)
| ~ r(v3,v4) ),
inference(resolution,[],[f38,f49]) ).
fof(f87,plain,
! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v3)
| ~ r(X0,v3)
| ~ r(X0,v5)
| ~ r(v3,v5) ),
inference(resolution,[],[f38,f53]) ).
fof(f88,plain,
! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v4)
| ~ r(X0,v4)
| ~ r(X0,v5)
| ~ r(v4,v5) ),
inference(resolution,[],[f38,f54]) ).
fof(f90,definition,
( spl1_1
<=> r(v4,v5) ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
fof(f91,plain,
( ~ r(v4,v5)
| spl1_1 ),
inference(avatar_component_clause,[],[f90]) ).
fof(f93,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(f94,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v4)
| sQ0_eqProxy(X0,v4) )
| ~ spl1_2 ),
inference(avatar_component_clause,[],[f93]) ).
fof(f95,plain,
( ~ spl1_1
| spl1_2 ),
inference(avatar_split_clause,[],[f88,f93,f90]) ).
fof(f97,definition,
( spl1_3
<=> r(v3,v5) ),
introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition]) ).
fof(f98,plain,
( ~ r(v3,v5)
| spl1_3 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,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(f101,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v3)
| sQ0_eqProxy(X0,v3) )
| ~ spl1_4 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f102,plain,
( ~ spl1_3
| spl1_4 ),
inference(avatar_split_clause,[],[f87,f100,f97]) ).
fof(f104,definition,
( spl1_5
<=> r(v3,v4) ),
introduced(definition,[new_symbols(definition,[spl1_5])],[avatar_definition]) ).
fof(f105,plain,
( ~ r(v3,v4)
| spl1_5 ),
inference(avatar_component_clause,[],[f104]) ).
fof(f107,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(f108,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| ~ r(X0,v4)
| ~ r(X0,v3)
| sQ0_eqProxy(X0,v3) )
| ~ spl1_6 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f109,plain,
( ~ spl1_5
| spl1_6 ),
inference(avatar_split_clause,[],[f86,f107,f104]) ).
fof(f111,definition,
( spl1_7
<=> r(v2,v5) ),
introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition]) ).
fof(f112,plain,
( ~ r(v2,v5)
| spl1_7 ),
inference(avatar_component_clause,[],[f111]) ).
fof(f114,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(f115,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v2)
| sQ0_eqProxy(X0,v2) )
| ~ spl1_8 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f116,plain,
( ~ spl1_7
| spl1_8 ),
inference(avatar_split_clause,[],[f85,f114,f111]) ).
fof(f118,definition,
( spl1_9
<=> r(v2,v4) ),
introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition]) ).
fof(f119,plain,
( ~ r(v2,v4)
| spl1_9 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f121,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(f122,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| ~ r(X0,v4)
| ~ r(X0,v2)
| sQ0_eqProxy(X0,v2) )
| ~ spl1_10 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f123,plain,
( ~ spl1_9
| spl1_10 ),
inference(avatar_split_clause,[],[f84,f121,f118]) ).
fof(f125,definition,
( spl1_11
<=> r(v2,v3) ),
introduced(definition,[new_symbols(definition,[spl1_11])],[avatar_definition]) ).
fof(f126,plain,
( ~ r(v2,v3)
| spl1_11 ),
inference(avatar_component_clause,[],[f125]) ).
fof(f128,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(f129,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| ~ r(X0,v3)
| ~ r(X0,v2)
| sQ0_eqProxy(X0,v2) )
| ~ spl1_12 ),
inference(avatar_component_clause,[],[f128]) ).
fof(f130,plain,
( ~ spl1_11
| spl1_12 ),
inference(avatar_split_clause,[],[f83,f128,f125]) ).
fof(f132,definition,
( spl1_13
<=> r(v1,v5) ),
introduced(definition,[new_symbols(definition,[spl1_13])],[avatar_definition]) ).
fof(f133,plain,
( ~ r(v1,v5)
| spl1_13 ),
inference(avatar_component_clause,[],[f132]) ).
fof(f135,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(f136,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| ~ r(X0,v5)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) )
| ~ spl1_14 ),
inference(avatar_component_clause,[],[f135]) ).
fof(f137,plain,
( ~ spl1_13
| spl1_14 ),
inference(avatar_split_clause,[],[f82,f135,f132]) ).
fof(f139,definition,
( spl1_15
<=> r(v1,v4) ),
introduced(definition,[new_symbols(definition,[spl1_15])],[avatar_definition]) ).
fof(f140,plain,
( ~ r(v1,v4)
| spl1_15 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f142,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(f143,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| ~ r(X0,v4)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) )
| ~ spl1_16 ),
inference(avatar_component_clause,[],[f142]) ).
fof(f144,plain,
( ~ spl1_15
| spl1_16 ),
inference(avatar_split_clause,[],[f81,f142,f139]) ).
fof(f146,definition,
( spl1_17
<=> r(v1,v3) ),
introduced(definition,[new_symbols(definition,[spl1_17])],[avatar_definition]) ).
fof(f147,plain,
( ~ r(v1,v3)
| spl1_17 ),
inference(avatar_component_clause,[],[f146]) ).
fof(f149,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(f150,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| ~ r(X0,v3)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) )
| ~ spl1_18 ),
inference(avatar_component_clause,[],[f149]) ).
fof(f151,plain,
( ~ spl1_17
| spl1_18 ),
inference(avatar_split_clause,[],[f80,f149,f146]) ).
fof(f153,definition,
( spl1_19
<=> r(v1,v2) ),
introduced(definition,[new_symbols(definition,[spl1_19])],[avatar_definition]) ).
fof(f156,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(f157,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v2)
| ~ r(X0,v2)
| ~ r(X0,v1)
| sQ0_eqProxy(X0,v1) )
| ~ spl1_20 ),
inference(avatar_component_clause,[],[f156]) ).
fof(f158,plain,
( ~ spl1_19
| spl1_20 ),
inference(avatar_split_clause,[],[f79,f156,f153]) ).
fof(f167,definition,
( spl1_23
<=> r(v0,v5) ),
introduced(definition,[new_symbols(definition,[spl1_23])],[avatar_definition]) ).
fof(f174,definition,
( spl1_25
<=> r(v0,v4) ),
introduced(definition,[new_symbols(definition,[spl1_25])],[avatar_definition]) ).
fof(f181,definition,
( spl1_27
<=> r(v0,v3) ),
introduced(definition,[new_symbols(definition,[spl1_27])],[avatar_definition]) ).
fof(f188,definition,
( spl1_29
<=> r(v0,v2) ),
introduced(definition,[new_symbols(definition,[spl1_29])],[avatar_definition]) ).
fof(f195,definition,
( spl1_31
<=> r(v0,v1) ),
introduced(definition,[new_symbols(definition,[spl1_31])],[avatar_definition]) ).
fof(f204,plain,
( ~ r(v5,v1)
| spl1_13 ),
inference(resolution,[],[f133,f19]) ).
fof(f265,definition,
( spl1_33
<=> sQ0_eqProxy(v4,v5) ),
introduced(definition,[new_symbols(definition,[spl1_33])],[avatar_definition]) ).
fof(f266,plain,
( sQ0_eqProxy(v4,v5)
| ~ spl1_33 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,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(f269,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v4)
| r(X0,v5)
| r(X0,v4) )
| ~ spl1_34 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f272,definition,
( spl1_35
<=> sQ0_eqProxy(v3,v5) ),
introduced(definition,[new_symbols(definition,[spl1_35])],[avatar_definition]) ).
fof(f273,plain,
( sQ0_eqProxy(v3,v5)
| ~ spl1_35 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f275,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(f276,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v3)
| r(X0,v5)
| r(X0,v3) )
| ~ spl1_36 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f279,definition,
( spl1_37
<=> sQ0_eqProxy(v2,v5) ),
introduced(definition,[new_symbols(definition,[spl1_37])],[avatar_definition]) ).
fof(f280,plain,
( sQ0_eqProxy(v2,v5)
| ~ spl1_37 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f282,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(f283,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v2)
| r(X0,v5)
| r(X0,v2) )
| ~ spl1_38 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f289,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(f290,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(X0,v1)
| r(X0,v5)
| r(X0,v1) )
| ~ spl1_40 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f304,definition,
( spl1_44
<=> sQ0_eqProxy(v3,v4) ),
introduced(definition,[new_symbols(definition,[spl1_44])],[avatar_definition]) ).
fof(f305,plain,
( sQ0_eqProxy(v3,v4)
| ~ spl1_44 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f307,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(f308,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v3)
| r(X0,v4)
| r(X0,v3) )
| ~ spl1_45 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f311,definition,
( spl1_46
<=> sQ0_eqProxy(v2,v4) ),
introduced(definition,[new_symbols(definition,[spl1_46])],[avatar_definition]) ).
fof(f312,plain,
( sQ0_eqProxy(v2,v4)
| ~ spl1_46 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f314,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(f315,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v2)
| r(X0,v4)
| r(X0,v2) )
| ~ spl1_47 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f318,definition,
( spl1_48
<=> sQ0_eqProxy(v1,v4) ),
introduced(definition,[new_symbols(definition,[spl1_48])],[avatar_definition]) ).
fof(f319,plain,
( sQ0_eqProxy(v1,v4)
| ~ spl1_48 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f321,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(f322,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(X0,v1)
| r(X0,v4)
| r(X0,v1) )
| ~ spl1_49 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f325,definition,
( spl1_50
<=> sQ0_eqProxy(v0,v4) ),
introduced(definition,[new_symbols(definition,[spl1_50])],[avatar_definition]) ).
fof(f326,plain,
( sQ0_eqProxy(v0,v4)
| ~ spl1_50 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f340,definition,
( spl1_54
<=> sQ0_eqProxy(v2,v3) ),
introduced(definition,[new_symbols(definition,[spl1_54])],[avatar_definition]) ).
fof(f341,plain,
( sQ0_eqProxy(v2,v3)
| ~ spl1_54 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f343,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(f344,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(X0,v2)
| r(X0,v3)
| r(X0,v2) )
| ~ spl1_55 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f347,definition,
( spl1_56
<=> sQ0_eqProxy(v1,v3) ),
introduced(definition,[new_symbols(definition,[spl1_56])],[avatar_definition]) ).
fof(f348,plain,
( sQ0_eqProxy(v1,v3)
| ~ spl1_56 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f350,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(f351,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(X0,v1)
| r(X0,v3)
| r(X0,v1) )
| ~ spl1_57 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f354,definition,
( spl1_58
<=> sQ0_eqProxy(v0,v3) ),
introduced(definition,[new_symbols(definition,[spl1_58])],[avatar_definition]) ).
fof(f355,plain,
( sQ0_eqProxy(v0,v3)
| ~ spl1_58 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f369,definition,
( spl1_62
<=> sQ0_eqProxy(v3,v2) ),
introduced(definition,[new_symbols(definition,[spl1_62])],[avatar_definition]) ).
fof(f370,plain,
( sQ0_eqProxy(v3,v2)
| ~ spl1_62 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f373,definition,
( spl1_63
<=> sQ0_eqProxy(v1,v2) ),
introduced(definition,[new_symbols(definition,[spl1_63])],[avatar_definition]) ).
fof(f374,plain,
( sQ0_eqProxy(v1,v2)
| ~ spl1_63 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f380,definition,
( spl1_65
<=> sQ0_eqProxy(v0,v2) ),
introduced(definition,[new_symbols(definition,[spl1_65])],[avatar_definition]) ).
fof(f381,plain,
( sQ0_eqProxy(v0,v2)
| ~ spl1_65 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f387,definition,
( spl1_67
<=> sQ0_eqProxy(v5,v1) ),
introduced(definition,[new_symbols(definition,[spl1_67])],[avatar_definition]) ).
fof(f388,plain,
( sQ0_eqProxy(v5,v1)
| ~ spl1_67 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f403,definition,
( spl1_71
<=> sQ0_eqProxy(v0,v1) ),
introduced(definition,[new_symbols(definition,[spl1_71])],[avatar_definition]) ).
fof(f404,plain,
( sQ0_eqProxy(v0,v1)
| ~ spl1_71 ),
inference(avatar_component_clause,[],[f403]) ).
fof(f432,plain,
( ~ r(v0,v5)
| ~ r(v0,v4)
| sQ0_eqProxy(v0,v4)
| ~ spl1_2 ),
inference(resolution,[],[f94,f50]) ).
fof(f439,plain,
( spl1_50
| ~ spl1_25
| ~ spl1_23
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f432,f93,f167,f174,f325]) ).
fof(f443,plain,
( ~ r(v0,v5)
| ~ r(v0,v3)
| sQ0_eqProxy(v0,v3)
| ~ spl1_4 ),
inference(resolution,[],[f101,f50]) ).
fof(f444,plain,
( ~ r(v1,v5)
| ~ r(v1,v3)
| sQ0_eqProxy(v1,v3)
| ~ spl1_4 ),
inference(resolution,[],[f101,f51]) ).
fof(f445,plain,
( ~ r(v2,v5)
| ~ r(v2,v3)
| sQ0_eqProxy(v2,v3)
| ~ spl1_4 ),
inference(resolution,[],[f101,f52]) ).
fof(f448,plain,
( spl1_54
| ~ spl1_11
| ~ spl1_7
| ~ spl1_4 ),
inference(avatar_split_clause,[],[f445,f100,f111,f125,f340]) ).
fof(f449,plain,
( spl1_56
| ~ spl1_17
| ~ spl1_13
| ~ spl1_4 ),
inference(avatar_split_clause,[],[f444,f100,f132,f146,f347]) ).
fof(f450,plain,
( spl1_58
| ~ spl1_27
| ~ spl1_23
| ~ spl1_4 ),
inference(avatar_split_clause,[],[f443,f100,f167,f181,f354]) ).
fof(f466,definition,
( spl1_78
<=> r(v3,v2) ),
introduced(definition,[new_symbols(definition,[spl1_78])],[avatar_definition]) ).
fof(f473,plain,
( ~ r(v1,v4)
| ~ r(v1,v2)
| sQ0_eqProxy(v1,v2)
| ~ spl1_10 ),
inference(resolution,[],[f122,f47]) ).
fof(f476,plain,
( spl1_63
| ~ spl1_19
| ~ spl1_15
| ~ spl1_10 ),
inference(avatar_split_clause,[],[f473,f121,f139,f153,f373]) ).
fof(f481,plain,
( ~ r(v0,v3)
| ~ r(v0,v2)
| sQ0_eqProxy(v0,v2)
| ~ spl1_12 ),
inference(resolution,[],[f129,f43]) ).
fof(f482,plain,
( ~ r(v1,v3)
| ~ r(v1,v2)
| sQ0_eqProxy(v1,v2)
| ~ spl1_12 ),
inference(resolution,[],[f129,f44]) ).
fof(f484,plain,
( spl1_63
| ~ spl1_19
| ~ spl1_17
| ~ spl1_12 ),
inference(avatar_split_clause,[],[f482,f128,f146,f153,f373]) ).
fof(f485,plain,
( spl1_65
| ~ spl1_29
| ~ spl1_27
| ~ spl1_12 ),
inference(avatar_split_clause,[],[f481,f128,f181,f188,f380]) ).
fof(f524,plain,
( ~ r(v0,v2)
| ~ r(v0,v1)
| sQ0_eqProxy(v0,v1)
| ~ spl1_20 ),
inference(resolution,[],[f157,f41]) ).
fof(f598,plain,
( ~ r(v1,v5)
| ~ r(v1,v4)
| sQ0_eqProxy(v1,v4)
| ~ spl1_2 ),
inference(resolution,[],[f94,f51]) ).
fof(f599,plain,
( ~ r(v2,v5)
| ~ r(v2,v4)
| sQ0_eqProxy(v2,v4)
| ~ spl1_2 ),
inference(resolution,[],[f94,f52]) ).
fof(f600,plain,
( ~ r(v3,v5)
| ~ r(v3,v4)
| sQ0_eqProxy(v3,v4)
| ~ spl1_2 ),
inference(resolution,[],[f94,f53]) ).
fof(f609,plain,
( $false
| ~ spl1_50 ),
inference(resolution,[],[f326,f46]) ).
fof(f610,plain,
~ spl1_50,
inference(avatar_contradiction_clause,[],[f609]) ).
fof(f611,plain,
( sQ0_eqProxy(v0,v2)
| r(v0,v5)
| r(v0,v2)
| ~ spl1_38 ),
inference(resolution,[],[f283,f50]) ).
fof(f612,plain,
( sQ0_eqProxy(v1,v2)
| r(v1,v5)
| r(v1,v2)
| ~ spl1_38 ),
inference(resolution,[],[f283,f51]) ).
fof(f614,plain,
( sQ0_eqProxy(v3,v2)
| r(v3,v5)
| r(v3,v2)
| ~ spl1_38 ),
inference(resolution,[],[f283,f53]) ).
fof(f622,plain,
( spl1_78
| spl1_3
| spl1_62
| ~ spl1_38 ),
inference(avatar_split_clause,[],[f614,f282,f369,f97,f466]) ).
fof(f660,plain,
( sQ0_eqProxy(v0,v3)
| r(v0,v4)
| r(v0,v3)
| ~ spl1_45 ),
inference(resolution,[],[f308,f46]) ).
fof(f661,plain,
( sQ0_eqProxy(v1,v3)
| r(v1,v4)
| r(v1,v3)
| ~ spl1_45 ),
inference(resolution,[],[f308,f47]) ).
fof(f662,plain,
( sQ0_eqProxy(v2,v3)
| r(v2,v4)
| r(v2,v3)
| ~ spl1_45 ),
inference(resolution,[],[f308,f48]) ).
fof(f670,plain,
( $false
| ~ spl1_44 ),
inference(resolution,[],[f305,f49]) ).
fof(f671,plain,
~ spl1_44,
inference(avatar_contradiction_clause,[],[f670]) ).
fof(f679,plain,
( spl1_48
| ~ spl1_15
| ~ spl1_13
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f598,f93,f132,f139,f318]) ).
fof(f682,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(v2,v5)
| r(X0,v2)
| r(X0,v5)
| sQ0_eqProxy(X0,v2) )
| spl1_7 ),
inference(resolution,[],[f112,f39]) ).
fof(f689,plain,
( $false
| ~ spl1_48 ),
inference(resolution,[],[f319,f47]) ).
fof(f690,plain,
~ spl1_48,
inference(avatar_contradiction_clause,[],[f689]) ).
fof(f699,plain,
( spl1_27
| spl1_25
| spl1_58
| ~ spl1_45 ),
inference(avatar_split_clause,[],[f660,f307,f354,f174,f181]) ).
fof(f700,plain,
( spl1_17
| spl1_15
| spl1_56
| ~ spl1_45 ),
inference(avatar_split_clause,[],[f661,f307,f347,f139,f146]) ).
fof(f701,plain,
( spl1_11
| spl1_9
| spl1_54
| ~ spl1_45 ),
inference(avatar_split_clause,[],[f662,f307,f340,f118,f125]) ).
fof(f702,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(v3,v4)
| r(X0,v3)
| r(X0,v4)
| sQ0_eqProxy(X0,v3) )
| spl1_5 ),
inference(resolution,[],[f105,f39]) ).
fof(f704,plain,
( spl1_44
| spl1_45
| spl1_5 ),
inference(avatar_split_clause,[],[f702,f104,f307,f304]) ).
fof(f705,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(v1,v4)
| r(X0,v1)
| r(X0,v4)
| sQ0_eqProxy(X0,v1) )
| spl1_15 ),
inference(resolution,[],[f140,f39]) ).
fof(f707,plain,
( spl1_48
| spl1_49
| spl1_15 ),
inference(avatar_split_clause,[],[f705,f139,f321,f318]) ).
fof(f708,plain,
( ~ r(v0,v4)
| ~ r(v0,v3)
| sQ0_eqProxy(v0,v3)
| ~ spl1_6 ),
inference(resolution,[],[f108,f46]) ).
fof(f709,plain,
( ~ r(v1,v4)
| ~ r(v1,v3)
| sQ0_eqProxy(v1,v3)
| ~ spl1_6 ),
inference(resolution,[],[f108,f47]) ).
fof(f710,plain,
( ~ r(v2,v4)
| ~ r(v2,v3)
| sQ0_eqProxy(v2,v3)
| ~ spl1_6 ),
inference(resolution,[],[f108,f48]) ).
fof(f712,plain,
( $false
| ~ spl1_56 ),
inference(resolution,[],[f348,f44]) ).
fof(f713,plain,
~ spl1_56,
inference(avatar_contradiction_clause,[],[f712]) ).
fof(f714,plain,
( spl1_37
| spl1_38
| spl1_7 ),
inference(avatar_split_clause,[],[f682,f111,f282,f279]) ).
fof(f724,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v1)
| sQ0_eqProxy(v5,v1)
| r(X0,v5)
| r(X0,v1)
| sQ0_eqProxy(X0,v5) )
| spl1_13 ),
inference(resolution,[],[f204,f39]) ).
fof(f726,plain,
( spl1_67
| spl1_40
| spl1_13 ),
inference(avatar_split_clause,[],[f724,f132,f289,f387]) ).
fof(f727,plain,
( ~ r(v0,v4)
| ~ r(v0,v1)
| sQ0_eqProxy(v0,v1)
| ~ spl1_16 ),
inference(resolution,[],[f143,f46]) ).
fof(f731,plain,
( $false
| ~ spl1_37 ),
inference(resolution,[],[f280,f52]) ).
fof(f732,plain,
~ spl1_37,
inference(avatar_contradiction_clause,[],[f731]) ).
fof(f733,plain,
( spl1_29
| spl1_23
| spl1_65
| ~ spl1_38 ),
inference(avatar_split_clause,[],[f611,f282,f380,f167,f188]) ).
fof(f734,plain,
( spl1_19
| spl1_13
| spl1_63
| ~ spl1_38 ),
inference(avatar_split_clause,[],[f612,f282,f373,f132,f153]) ).
fof(f736,plain,
( ~ r(v0,v3)
| ~ r(v0,v1)
| sQ0_eqProxy(v0,v1)
| ~ spl1_18 ),
inference(resolution,[],[f150,f43]) ).
fof(f744,plain,
( $false
| ~ spl1_58 ),
inference(resolution,[],[f355,f43]) ).
fof(f745,plain,
~ spl1_58,
inference(avatar_contradiction_clause,[],[f744]) ).
fof(f748,plain,
( $false
| ~ spl1_63 ),
inference(resolution,[],[f374,f42]) ).
fof(f749,plain,
~ spl1_63,
inference(avatar_contradiction_clause,[],[f748]) ).
fof(f751,plain,
( spl1_71
| ~ spl1_31
| ~ spl1_29
| ~ spl1_20 ),
inference(avatar_split_clause,[],[f524,f156,f188,f195,f403]) ).
fof(f754,plain,
( spl1_71
| ~ spl1_31
| ~ spl1_27
| ~ spl1_18 ),
inference(avatar_split_clause,[],[f736,f149,f181,f195,f403]) ).
fof(f755,plain,
( spl1_58
| ~ spl1_27
| ~ spl1_25
| ~ spl1_6 ),
inference(avatar_split_clause,[],[f708,f107,f174,f181,f354]) ).
fof(f764,plain,
( spl1_54
| ~ spl1_11
| ~ spl1_9
| ~ spl1_6 ),
inference(avatar_split_clause,[],[f710,f107,f118,f125,f340]) ).
fof(f766,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(v2,v3)
| r(X0,v2)
| r(X0,v3)
| sQ0_eqProxy(X0,v2) )
| spl1_11 ),
inference(resolution,[],[f126,f39]) ).
fof(f768,plain,
( spl1_54
| spl1_55
| spl1_11 ),
inference(avatar_split_clause,[],[f766,f125,f343,f340]) ).
fof(f772,plain,
( ~ r(v0,v4)
| ~ r(v0,v2)
| sQ0_eqProxy(v0,v2)
| ~ spl1_10 ),
inference(resolution,[],[f122,f46]) ).
fof(f775,plain,
( ~ r(v3,v4)
| ~ r(v3,v2)
| sQ0_eqProxy(v3,v2)
| ~ spl1_10 ),
inference(resolution,[],[f122,f49]) ).
fof(f776,plain,
( $false
| ~ spl1_71 ),
inference(resolution,[],[f404,f40]) ).
fof(f777,plain,
~ spl1_71,
inference(avatar_contradiction_clause,[],[f776]) ).
fof(f779,plain,
( spl1_65
| ~ spl1_29
| ~ spl1_25
| ~ spl1_10 ),
inference(avatar_split_clause,[],[f772,f121,f174,f188,f380]) ).
fof(f791,plain,
( $false
| ~ spl1_65 ),
inference(resolution,[],[f381,f41]) ).
fof(f792,plain,
~ spl1_65,
inference(avatar_contradiction_clause,[],[f791]) ).
fof(f802,plain,
( $false
| ~ spl1_46 ),
inference(resolution,[],[f312,f48]) ).
fof(f803,plain,
~ spl1_46,
inference(avatar_contradiction_clause,[],[f802]) ).
fof(f808,plain,
( $false
| ~ spl1_54 ),
inference(resolution,[],[f341,f45]) ).
fof(f809,plain,
~ spl1_54,
inference(avatar_contradiction_clause,[],[f808]) ).
fof(f816,plain,
( ~ r(v0,v5)
| ~ r(v0,v2)
| sQ0_eqProxy(v0,v2)
| ~ spl1_8 ),
inference(resolution,[],[f115,f50]) ).
fof(f817,plain,
( ~ r(v1,v5)
| ~ r(v1,v2)
| sQ0_eqProxy(v1,v2)
| ~ spl1_8 ),
inference(resolution,[],[f115,f51]) ).
fof(f822,plain,
( $false
| ~ spl1_33 ),
inference(resolution,[],[f266,f54]) ).
fof(f823,plain,
~ spl1_33,
inference(avatar_contradiction_clause,[],[f822]) ).
fof(f826,plain,
( spl1_46
| ~ spl1_9
| ~ spl1_7
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f599,f93,f111,f118,f311]) ).
fof(f827,plain,
( spl1_44
| ~ spl1_5
| ~ spl1_3
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f600,f93,f97,f104,f304]) ).
fof(f830,plain,
( spl1_62
| ~ spl1_78
| ~ spl1_5
| ~ spl1_10 ),
inference(avatar_split_clause,[],[f775,f121,f104,f466,f369]) ).
fof(f849,plain,
( $false
| ~ spl1_35 ),
inference(resolution,[],[f273,f53]) ).
fof(f850,plain,
~ spl1_35,
inference(avatar_contradiction_clause,[],[f849]) ).
fof(f888,plain,
( spl1_63
| ~ spl1_19
| ~ spl1_13
| ~ spl1_8 ),
inference(avatar_split_clause,[],[f817,f114,f132,f153,f373]) ).
fof(f890,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(v4,v5)
| r(X0,v4)
| r(X0,v5)
| sQ0_eqProxy(X0,v4) )
| spl1_1 ),
inference(resolution,[],[f91,f39]) ).
fof(f892,plain,
( spl1_33
| spl1_34
| spl1_1 ),
inference(avatar_split_clause,[],[f890,f90,f268,f265]) ).
fof(f899,plain,
( ~ r(v0,v5)
| ~ r(v0,v1)
| sQ0_eqProxy(v0,v1)
| ~ spl1_14 ),
inference(resolution,[],[f136,f50]) ).
fof(f915,plain,
( sQ0_eqProxy(v0,v4)
| r(v0,v5)
| r(v0,v4)
| ~ spl1_34 ),
inference(resolution,[],[f269,f50]) ).
fof(f916,plain,
( sQ0_eqProxy(v1,v4)
| r(v1,v5)
| r(v1,v4)
| ~ spl1_34 ),
inference(resolution,[],[f269,f51]) ).
fof(f917,plain,
( sQ0_eqProxy(v2,v4)
| r(v2,v5)
| r(v2,v4)
| ~ spl1_34 ),
inference(resolution,[],[f269,f52]) ).
fof(f918,plain,
( sQ0_eqProxy(v3,v4)
| r(v3,v5)
| r(v3,v4)
| ~ spl1_34 ),
inference(resolution,[],[f269,f53]) ).
fof(f920,plain,
( spl1_5
| spl1_3
| spl1_44
| ~ spl1_34 ),
inference(avatar_split_clause,[],[f918,f268,f304,f97,f104]) ).
fof(f921,plain,
( spl1_9
| spl1_7
| spl1_46
| ~ spl1_34 ),
inference(avatar_split_clause,[],[f917,f268,f311,f111,f118]) ).
fof(f922,plain,
( spl1_15
| spl1_13
| spl1_48
| ~ spl1_34 ),
inference(avatar_split_clause,[],[f916,f268,f318,f132,f139]) ).
fof(f923,plain,
( spl1_25
| spl1_23
| spl1_50
| ~ spl1_34 ),
inference(avatar_split_clause,[],[f915,f268,f325,f167,f174]) ).
fof(f924,plain,
( sQ0_eqProxy(v0,v1)
| r(v0,v5)
| r(v0,v1)
| ~ spl1_40 ),
inference(resolution,[],[f290,f50]) ).
fof(f932,plain,
( spl1_31
| spl1_23
| spl1_71
| ~ spl1_40 ),
inference(avatar_split_clause,[],[f924,f289,f403,f167,f195]) ).
fof(f943,plain,
( sQ0_eqProxy(v0,v1)
| r(v0,v4)
| r(v0,v1)
| ~ spl1_49 ),
inference(resolution,[],[f322,f46]) ).
fof(f949,plain,
( spl1_31
| spl1_25
| spl1_71
| ~ spl1_49 ),
inference(avatar_split_clause,[],[f943,f321,f403,f174,f195]) ).
fof(f957,plain,
( $false
| ~ spl1_67 ),
inference(resolution,[],[f388,f65]) ).
fof(f958,plain,
~ spl1_67,
inference(avatar_contradiction_clause,[],[f957]) ).
fof(f959,plain,
( sQ0_eqProxy(v0,v2)
| r(v0,v3)
| r(v0,v2)
| ~ spl1_55 ),
inference(resolution,[],[f344,f43]) ).
fof(f960,plain,
( sQ0_eqProxy(v1,v2)
| r(v1,v3)
| r(v1,v2)
| ~ spl1_55 ),
inference(resolution,[],[f344,f44]) ).
fof(f962,plain,
( spl1_19
| spl1_17
| spl1_63
| ~ spl1_55 ),
inference(avatar_split_clause,[],[f960,f343,f373,f146,f153]) ).
fof(f963,plain,
( spl1_29
| spl1_27
| spl1_65
| ~ spl1_55 ),
inference(avatar_split_clause,[],[f959,f343,f380,f181,f188]) ).
fof(f966,plain,
( spl1_71
| ~ spl1_31
| ~ spl1_25
| ~ spl1_16 ),
inference(avatar_split_clause,[],[f727,f142,f174,f195,f403]) ).
fof(f983,plain,
( spl1_65
| ~ spl1_29
| ~ spl1_23
| ~ spl1_8 ),
inference(avatar_split_clause,[],[f816,f114,f167,f188,f380]) ).
fof(f985,plain,
( spl1_71
| ~ spl1_31
| ~ spl1_23
| ~ spl1_14 ),
inference(avatar_split_clause,[],[f899,f135,f167,f195,f403]) ).
fof(f990,plain,
( spl1_56
| ~ spl1_17
| ~ spl1_15
| ~ spl1_6 ),
inference(avatar_split_clause,[],[f709,f107,f139,f146,f347]) ).
fof(f994,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v5)
| sQ0_eqProxy(v3,v5)
| r(X0,v3)
| r(X0,v5)
| sQ0_eqProxy(X0,v3) )
| spl1_3 ),
inference(resolution,[],[f98,f39]) ).
fof(f996,plain,
( spl1_35
| spl1_36
| spl1_3 ),
inference(avatar_split_clause,[],[f994,f97,f275,f272]) ).
fof(f997,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v4)
| sQ0_eqProxy(v2,v4)
| r(X0,v2)
| r(X0,v4)
| sQ0_eqProxy(X0,v2) )
| spl1_9 ),
inference(resolution,[],[f119,f39]) ).
fof(f999,plain,
( spl1_46
| spl1_47
| spl1_9 ),
inference(avatar_split_clause,[],[f997,f118,f314,f311]) ).
fof(f1000,plain,
( ! [X0] :
( sQ0_eqProxy(X0,v3)
| sQ0_eqProxy(v1,v3)
| r(X0,v1)
| r(X0,v3)
| sQ0_eqProxy(X0,v1) )
| spl1_17 ),
inference(resolution,[],[f147,f39]) ).
fof(f1002,plain,
( spl1_56
| spl1_57
| spl1_17 ),
inference(avatar_split_clause,[],[f1000,f146,f350,f347]) ).
fof(f1042,plain,
( sQ0_eqProxy(v0,v3)
| r(v0,v5)
| r(v0,v3)
| ~ spl1_36 ),
inference(resolution,[],[f276,f50]) ).
fof(f1043,plain,
( sQ0_eqProxy(v1,v3)
| r(v1,v5)
| r(v1,v3)
| ~ spl1_36 ),
inference(resolution,[],[f276,f51]) ).
fof(f1044,plain,
( sQ0_eqProxy(v2,v3)
| r(v2,v5)
| r(v2,v3)
| ~ spl1_36 ),
inference(resolution,[],[f276,f52]) ).
fof(f1047,plain,
( spl1_11
| spl1_7
| spl1_54
| ~ spl1_36 ),
inference(avatar_split_clause,[],[f1044,f275,f340,f111,f125]) ).
fof(f1048,plain,
( spl1_17
| spl1_13
| spl1_56
| ~ spl1_36 ),
inference(avatar_split_clause,[],[f1043,f275,f347,f132,f146]) ).
fof(f1049,plain,
( spl1_27
| spl1_23
| spl1_58
| ~ spl1_36 ),
inference(avatar_split_clause,[],[f1042,f275,f354,f167,f181]) ).
fof(f1050,plain,
( sQ0_eqProxy(v0,v2)
| r(v0,v4)
| r(v0,v2)
| ~ spl1_47 ),
inference(resolution,[],[f315,f46]) ).
fof(f1051,plain,
( sQ0_eqProxy(v1,v2)
| r(v1,v4)
| r(v1,v2)
| ~ spl1_47 ),
inference(resolution,[],[f315,f47]) ).
fof(f1055,plain,
( spl1_19
| spl1_15
| spl1_63
| ~ spl1_47 ),
inference(avatar_split_clause,[],[f1051,f314,f373,f139,f153]) ).
fof(f1056,plain,
( spl1_29
| spl1_25
| spl1_65
| ~ spl1_47 ),
inference(avatar_split_clause,[],[f1050,f314,f380,f174,f188]) ).
fof(f1057,plain,
( $false
| ~ spl1_62 ),
inference(resolution,[],[f370,f66]) ).
fof(f1058,plain,
~ spl1_62,
inference(avatar_contradiction_clause,[],[f1057]) ).
fof(f1059,plain,
( sQ0_eqProxy(v0,v1)
| r(v0,v3)
| r(v0,v1)
| ~ spl1_57 ),
inference(resolution,[],[f351,f43]) ).
fof(f1063,plain,
( spl1_31
| spl1_27
| spl1_71
| ~ spl1_57 ),
inference(avatar_split_clause,[],[f1059,f350,f403,f181,f195]) ).
cnf(s1,plain,
( ~ spl1_1
| spl1_2 ),
inference(sat_conversion,[],[f95]) ).
cnf(s2,plain,
( ~ spl1_3
| spl1_4 ),
inference(sat_conversion,[],[f102]) ).
cnf(s3,plain,
( ~ spl1_5
| spl1_6 ),
inference(sat_conversion,[],[f109]) ).
cnf(s4,plain,
( ~ spl1_7
| spl1_8 ),
inference(sat_conversion,[],[f116]) ).
cnf(s5,plain,
( ~ spl1_9
| spl1_10 ),
inference(sat_conversion,[],[f123]) ).
cnf(s6,plain,
( ~ spl1_11
| spl1_12 ),
inference(sat_conversion,[],[f130]) ).
cnf(s7,plain,
( ~ spl1_13
| spl1_14 ),
inference(sat_conversion,[],[f137]) ).
cnf(s8,plain,
( ~ spl1_15
| spl1_16 ),
inference(sat_conversion,[],[f144]) ).
cnf(s9,plain,
( ~ spl1_17
| spl1_18 ),
inference(sat_conversion,[],[f151]) ).
cnf(s10,plain,
( ~ spl1_19
| spl1_20 ),
inference(sat_conversion,[],[f158]) ).
cnf(s53,plain,
( ~ spl1_2
| ~ spl1_23
| ~ spl1_25
| spl1_50 ),
inference(sat_conversion,[],[f439]) ).
cnf(s55,plain,
( ~ spl1_4
| ~ spl1_7
| ~ spl1_11
| spl1_54 ),
inference(sat_conversion,[],[f448]) ).
cnf(s56,plain,
( ~ spl1_4
| ~ spl1_13
| ~ spl1_17
| spl1_56 ),
inference(sat_conversion,[],[f449]) ).
cnf(s57,plain,
( ~ spl1_4
| ~ spl1_23
| ~ spl1_27
| spl1_58 ),
inference(sat_conversion,[],[f450]) ).
cnf(s63,plain,
( ~ spl1_10
| ~ spl1_15
| ~ spl1_19
| spl1_63 ),
inference(sat_conversion,[],[f476]) ).
cnf(s66,plain,
( ~ spl1_12
| ~ spl1_17
| ~ spl1_19
| spl1_63 ),
inference(sat_conversion,[],[f484]) ).
cnf(s67,plain,
( ~ spl1_12
| ~ spl1_27
| ~ spl1_29
| spl1_65 ),
inference(sat_conversion,[],[f485]) ).
cnf(s101,plain,
~ spl1_50,
inference(sat_conversion,[],[f610]) ).
cnf(s103,plain,
( spl1_3
| ~ spl1_38
| spl1_62
| spl1_78 ),
inference(sat_conversion,[],[f622]) ).
cnf(s118,plain,
~ spl1_44,
inference(sat_conversion,[],[f671]) ).
cnf(s125,plain,
( ~ spl1_2
| ~ spl1_13
| ~ spl1_15
| spl1_48 ),
inference(sat_conversion,[],[f679]) ).
cnf(s128,plain,
~ spl1_48,
inference(sat_conversion,[],[f690]) ).
cnf(s134,plain,
( spl1_25
| spl1_27
| ~ spl1_45
| spl1_58 ),
inference(sat_conversion,[],[f699]) ).
cnf(s135,plain,
( spl1_15
| spl1_17
| ~ spl1_45
| spl1_56 ),
inference(sat_conversion,[],[f700]) ).
cnf(s136,plain,
( spl1_9
| spl1_11
| ~ spl1_45
| spl1_54 ),
inference(sat_conversion,[],[f701]) ).
cnf(s138,plain,
( spl1_5
| spl1_44
| spl1_45 ),
inference(sat_conversion,[],[f704]) ).
cnf(s140,plain,
( spl1_15
| spl1_48
| spl1_49 ),
inference(sat_conversion,[],[f707]) ).
cnf(s141,plain,
~ spl1_56,
inference(sat_conversion,[],[f713]) ).
cnf(s142,plain,
( spl1_7
| spl1_37
| spl1_38 ),
inference(sat_conversion,[],[f714]) ).
cnf(s147,plain,
( spl1_13
| spl1_40
| spl1_67 ),
inference(sat_conversion,[],[f726]) ).
cnf(s148,plain,
~ spl1_37,
inference(sat_conversion,[],[f732]) ).
cnf(s149,plain,
( spl1_23
| spl1_29
| ~ spl1_38
| spl1_65 ),
inference(sat_conversion,[],[f733]) ).
cnf(s150,plain,
( spl1_13
| spl1_19
| ~ spl1_38
| spl1_63 ),
inference(sat_conversion,[],[f734]) ).
cnf(s156,plain,
~ spl1_58,
inference(sat_conversion,[],[f745]) ).
cnf(s159,plain,
~ spl1_63,
inference(sat_conversion,[],[f749]) ).
cnf(s163,plain,
( ~ spl1_20
| ~ spl1_29
| ~ spl1_31
| spl1_71 ),
inference(sat_conversion,[],[f751]) ).
cnf(s168,plain,
( ~ spl1_18
| ~ spl1_27
| ~ spl1_31
| spl1_71 ),
inference(sat_conversion,[],[f754]) ).
cnf(s169,plain,
( ~ spl1_6
| ~ spl1_25
| ~ spl1_27
| spl1_58 ),
inference(sat_conversion,[],[f755]) ).
cnf(s177,plain,
( ~ spl1_6
| ~ spl1_9
| ~ spl1_11
| spl1_54 ),
inference(sat_conversion,[],[f764]) ).
cnf(s181,plain,
( spl1_11
| spl1_54
| spl1_55 ),
inference(sat_conversion,[],[f768]) ).
cnf(s184,plain,
~ spl1_71,
inference(sat_conversion,[],[f777]) ).
cnf(s189,plain,
( ~ spl1_10
| ~ spl1_25
| ~ spl1_29
| spl1_65 ),
inference(sat_conversion,[],[f779]) ).
cnf(s196,plain,
~ spl1_65,
inference(sat_conversion,[],[f792]) ).
cnf(s202,plain,
~ spl1_46,
inference(sat_conversion,[],[f803]) ).
cnf(s206,plain,
~ spl1_54,
inference(sat_conversion,[],[f809]) ).
cnf(s210,plain,
~ spl1_33,
inference(sat_conversion,[],[f823]) ).
cnf(s213,plain,
( ~ spl1_2
| ~ spl1_7
| ~ spl1_9
| spl1_46 ),
inference(sat_conversion,[],[f826]) ).
cnf(s214,plain,
( ~ spl1_2
| ~ spl1_3
| ~ spl1_5
| spl1_44 ),
inference(sat_conversion,[],[f827]) ).
cnf(s219,plain,
( ~ spl1_5
| ~ spl1_10
| spl1_62
| ~ spl1_78 ),
inference(sat_conversion,[],[f830]) ).
cnf(s227,plain,
~ spl1_35,
inference(sat_conversion,[],[f850]) ).
cnf(s249,plain,
( ~ spl1_8
| ~ spl1_13
| ~ spl1_19
| spl1_63 ),
inference(sat_conversion,[],[f888]) ).
cnf(s251,plain,
( spl1_1
| spl1_33
| spl1_34 ),
inference(sat_conversion,[],[f892]) ).
cnf(s261,plain,
( spl1_3
| spl1_5
| ~ spl1_34
| spl1_44 ),
inference(sat_conversion,[],[f920]) ).
cnf(s262,plain,
( spl1_7
| spl1_9
| ~ spl1_34
| spl1_46 ),
inference(sat_conversion,[],[f921]) ).
cnf(s263,plain,
( spl1_13
| spl1_15
| ~ spl1_34
| spl1_48 ),
inference(sat_conversion,[],[f922]) ).
cnf(s264,plain,
( spl1_23
| spl1_25
| ~ spl1_34
| spl1_50 ),
inference(sat_conversion,[],[f923]) ).
cnf(s268,plain,
( spl1_23
| spl1_31
| ~ spl1_40
| spl1_71 ),
inference(sat_conversion,[],[f932]) ).
cnf(s274,plain,
( spl1_25
| spl1_31
| ~ spl1_49
| spl1_71 ),
inference(sat_conversion,[],[f949]) ).
cnf(s278,plain,
~ spl1_67,
inference(sat_conversion,[],[f958]) ).
cnf(s279,plain,
( spl1_17
| spl1_19
| ~ spl1_55
| spl1_63 ),
inference(sat_conversion,[],[f962]) ).
cnf(s280,plain,
( spl1_27
| spl1_29
| ~ spl1_55
| spl1_65 ),
inference(sat_conversion,[],[f963]) ).
cnf(s286,plain,
( ~ spl1_16
| ~ spl1_25
| ~ spl1_31
| spl1_71 ),
inference(sat_conversion,[],[f966]) ).
cnf(s301,plain,
( ~ spl1_8
| ~ spl1_23
| ~ spl1_29
| spl1_65 ),
inference(sat_conversion,[],[f983]) ).
cnf(s303,plain,
( ~ spl1_14
| ~ spl1_23
| ~ spl1_31
| spl1_71 ),
inference(sat_conversion,[],[f985]) ).
cnf(s305,plain,
( ~ spl1_6
| ~ spl1_15
| ~ spl1_17
| spl1_56 ),
inference(sat_conversion,[],[f990]) ).
cnf(s318,plain,
( spl1_3
| spl1_35
| spl1_36 ),
inference(sat_conversion,[],[f996]) ).
cnf(s320,plain,
( spl1_9
| spl1_46
| spl1_47 ),
inference(sat_conversion,[],[f999]) ).
cnf(s322,plain,
( spl1_17
| spl1_56
| spl1_57 ),
inference(sat_conversion,[],[f1002]) ).
cnf(s332,plain,
( spl1_7
| spl1_11
| ~ spl1_36
| spl1_54 ),
inference(sat_conversion,[],[f1047]) ).
cnf(s333,plain,
( spl1_13
| spl1_17
| ~ spl1_36
| spl1_56 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s334,plain,
( spl1_23
| spl1_27
| ~ spl1_36
| spl1_58 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s336,plain,
( spl1_15
| spl1_19
| ~ spl1_47
| spl1_63 ),
inference(sat_conversion,[],[f1055]) ).
cnf(s337,plain,
( spl1_25
| spl1_29
| ~ spl1_47
| spl1_65 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s338,plain,
~ spl1_62,
inference(sat_conversion,[],[f1058]) ).
cnf(s340,plain,
( spl1_27
| spl1_31
| ~ spl1_57
| spl1_71 ),
inference(sat_conversion,[],[f1063]) ).
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(f1064,plain,
$false,
inference(avatar_sat_refutation,[],[s478]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % 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.08/0.36 % Computer : n020.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 27 09:00:04 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.40 Running first-order theorem proving
% 0.08/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.82/1.30 % (3110663)Detected formulas, will run a generic FOF schedule.
% 2.82/1.30 % (3110670)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2609483161:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.82/1.30 % (3110672)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=738806291:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.82/1.30 % (3110671)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2462309227:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.82/1.30 % (3110668)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=3278123468:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.82/1.30 % (3110669)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2477921295:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.82/1.30 % (3110674)dis-21_1_sil=8000:lcm=predicate:random_seed=2286366567:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.82/1.30 % (3110673)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=16031653:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.82/1.30 % (3110672)Refutation not found, incomplete strategy
% 2.82/1.30 % (3110672)------------------------------
% 2.82/1.30 % (3110672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.82/1.30 % (3110672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/1.30 % (3110671)Refutation not found, incomplete strategy
% 2.82/1.30 % (3110671)------------------------------
% 2.82/1.30 % (3110671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.82/1.30 % (3110672)CaDiCaL version: 2.1.3
% 2.82/1.30 % (3110672)Termination reason: Refutation not found, incomplete strategy
% 2.82/1.30 % (3110672)Time elapsed: 0.0000 s
% 2.82/1.30 % (3110671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/1.30 % (3110672)Peak memory usage: 86 MB
% 2.82/1.30 % (3110671)CaDiCaL version: 2.1.3
% 2.82/1.30 % (3110671)Termination reason: Refutation not found, incomplete strategy
% 2.82/1.30 % (3110671)Time elapsed: 0.0000 s
% 2.82/1.30 % (3110671)Peak memory usage: 86 MB
% 2.82/1.30 % (3110674)First to succeed.
% 2.82/1.30 % (3110674)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3110663"
% 2.82/1.30 % (3110673)Instruction limit reached!
% 2.82/1.30 % (3110673)------------------------------
% 2.82/1.30 % (3110673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.82/1.30 % (3110673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/1.30 % (3110673)CaDiCaL version: 2.1.3
% 2.82/1.30 % (3110673)Termination reason: Instruction limit
% 2.82/1.30 % (3110673)Termination phase: Saturation
% 2.82/1.30 % (3110673)Time elapsed: 0.057 s
% 2.82/1.30 % (3110673)Peak memory usage: 87 MB
% 2.82/1.30 % (3110673)Instructions burned: 140 (million)
% 2.82/1.30 % (3110682)lrs+10_1_sil=8000:sp=occurrence:random_seed=511897071:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 2.82/1.30 % (3110682)Refutation not found, incomplete strategy
% 2.82/1.30 % (3110682)------------------------------
% 2.82/1.30 % (3110682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.82/1.30 % (3110682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/1.30 % (3110682)CaDiCaL version: 2.1.3
% 2.82/1.30 % (3110682)Termination reason: Refutation not found, incomplete strategy
% 2.82/1.30 % (3110682)Time elapsed: 0.001 s
% 2.82/1.30 % (3110682)Peak memory usage: 86 MB
% 2.82/1.30 % (3110672)------------------------------
% 2.82/1.30 % (3110672)------------------------------
% 2.82/1.30 % (3110671)------------------------------
% 2.82/1.30 % (3110671)------------------------------
% 2.82/1.30 % (3110670)Refutation not found, incomplete strategy
% 2.82/1.30 % (3110670)------------------------------
% 2.82/1.30 % (3110670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.82/1.30 % (3110670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/1.30 % (3110670)CaDiCaL version: 2.1.3
% 2.82/1.30 % (3110670)Termination reason: Refutation not found, incomplete strategy
% 2.82/1.30 % (3110670)Time elapsed: 0.320 s
% 2.82/1.30 % (3110670)Peak memory usage: 127 MB
% 2.82/1.30 % (3110670)Instructions burned: 824 (million)
% 2.82/1.30 % (3110674)Refutation found. Thanks to Tanya!
% 2.82/1.30 % SZS status Unsatisfiable for theBenchmark
% 2.82/1.30 % SZS output start Proof for theBenchmark
% See solution above
% 3.77/1.49 % (3110674)------------------------------
% 3.77/1.49 % (3110674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.49 % (3110674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.49 % (3110674)CaDiCaL version: 2.1.3
% 3.77/1.49 % (3110674)Termination reason: Refutation
% 3.77/1.49 % (3110674)Time elapsed: 0.019 s
% 3.77/1.49 % (3110674)Peak memory usage: 89 MB
% 3.77/1.49 % (3110674)Instructions burned: 29 (million)
% 3.77/1.49 % (3110674)------------------------------
% 3.77/1.49 % (3110674)------------------------------
% 3.77/1.49 % (3110663)Success in time 0.456 s
% 3.77/1.49 % Vampire exiting
%------------------------------------------------------------------------------