%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO500_8.005 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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 02:26:43 PM UTC 2026
% Result : Theorem 3.01s 1.14s
% Output : Refutation 3.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 68
% Syntax : Number of formulae : 642 ( 29 unt; 0 typ; 66 def)
% Number of atoms : 2480 ( 210 equ)
% Maximal formula atoms : 5 ( 3 avg)
% Number of connectives : 1906 ( 793 ~;1024 |; 21 &)
% ( 67 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 731 ( 725 fml; 6 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 75 ( 72 usr; 69 prp; 0-2 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 3 ( 0 sgn 3 !; 0 ?; 3 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
bG0: $o ).
tff(func_def_3,type,
bG1: $o ).
tff(func_def_4,type,
bG2: $o ).
tff(func_def_5,type,
bG3: $o ).
tff(func_def_6,type,
bG4: $o ).
tff(func_def_7,type,
bG5: $o ).
tff(func_def_8,type,
bG6: $o ).
tff(func_def_9,type,
bG7: $o ).
tff(func_def_10,type,
bG8: $o ).
tff(func_def_11,type,
bG9: $o ).
tff(func_def_12,type,
bG10: $o ).
tff(func_def_13,type,
bG11: $o ).
tff(func_def_14,type,
bG12: $o ).
tff(func_def_15,type,
bG13: $o ).
tff(func_def_16,type,
bG14: $o ).
tff(func_def_17,type,
bG15: $o ).
tff(func_def_18,type,
bG16: $o ).
tff(func_def_19,type,
bG17: $o ).
tff(func_def_20,type,
bG18: $o ).
tff(func_def_21,type,
bG19: $o ).
tff(pred_def_2,type,
f0: $o > $o ).
tff(pred_def_3,type,
f1: $o > $o ).
tff(pred_def_4,type,
f2: $o > $o ).
tff(pred_def_5,type,
f3: $o > $o ).
tff(pred_def_6,type,
f4: $o > $o ).
tff(f1,conjecture,
f0(f1(f1(f1(f2(f3(f3(f3(f4(x))))))))) = f0(f0(f0(f1(f2(f2(f2(f3(f4(f4(f4(x))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kaminski5) ).
tff(f2,negated_conjecture,
f0(f1(f1(f1(f2(f3(f3(f3(f4(x))))))))) != f0(f0(f0(f1(f2(f2(f2(f3(f4(f4(f4(x))))))))))),
inference(negated_conjecture,[status(cth)],[f1]) ).
tff(f3,definition,
( x
<=> ( bG0 = $true ) ),
introduced(definition,[new_symbols(definition,[bG0])],[fool_formula_definition]) ).
tff(f4,definition,
( f4(bG0)
<=> ( $true = bG1 ) ),
introduced(definition,[new_symbols(definition,[bG1])],[fool_formula_definition]) ).
tff(f5,definition,
( f3(bG1)
<=> ( $true = bG2 ) ),
introduced(definition,[new_symbols(definition,[bG2])],[fool_formula_definition]) ).
tff(f6,definition,
( f3(bG2)
<=> ( $true = bG3 ) ),
introduced(definition,[new_symbols(definition,[bG3])],[fool_formula_definition]) ).
tff(f7,definition,
( f3(bG3)
<=> ( $true = bG4 ) ),
introduced(definition,[new_symbols(definition,[bG4])],[fool_formula_definition]) ).
tff(f8,definition,
( f2(bG4)
<=> ( $true = bG5 ) ),
introduced(definition,[new_symbols(definition,[bG5])],[fool_formula_definition]) ).
tff(f9,definition,
( f1(bG5)
<=> ( $true = bG6 ) ),
introduced(definition,[new_symbols(definition,[bG6])],[fool_formula_definition]) ).
tff(f10,definition,
( f1(bG6)
<=> ( $true = bG7 ) ),
introduced(definition,[new_symbols(definition,[bG7])],[fool_formula_definition]) ).
tff(f11,definition,
( f1(bG7)
<=> ( $true = bG8 ) ),
introduced(definition,[new_symbols(definition,[bG8])],[fool_formula_definition]) ).
tff(f12,definition,
( x
<=> ( $true = bG9 ) ),
introduced(definition,[new_symbols(definition,[bG9])],[fool_formula_definition]) ).
tff(f13,definition,
( f4(bG9)
<=> ( $true = bG10 ) ),
introduced(definition,[new_symbols(definition,[bG10])],[fool_formula_definition]) ).
tff(f14,definition,
( f4(bG10)
<=> ( $true = bG11 ) ),
introduced(definition,[new_symbols(definition,[bG11])],[fool_formula_definition]) ).
tff(f15,definition,
( f4(bG11)
<=> ( $true = bG12 ) ),
introduced(definition,[new_symbols(definition,[bG12])],[fool_formula_definition]) ).
tff(f16,definition,
( f3(bG12)
<=> ( $true = bG13 ) ),
introduced(definition,[new_symbols(definition,[bG13])],[fool_formula_definition]) ).
tff(f17,definition,
( f2(bG13)
<=> ( $true = bG14 ) ),
introduced(definition,[new_symbols(definition,[bG14])],[fool_formula_definition]) ).
tff(f18,definition,
( f2(bG14)
<=> ( $true = bG15 ) ),
introduced(definition,[new_symbols(definition,[bG15])],[fool_formula_definition]) ).
tff(f19,definition,
( f2(bG15)
<=> ( $true = bG16 ) ),
introduced(definition,[new_symbols(definition,[bG16])],[fool_formula_definition]) ).
tff(f20,definition,
( f1(bG16)
<=> ( $true = bG17 ) ),
introduced(definition,[new_symbols(definition,[bG17])],[fool_formula_definition]) ).
tff(f21,definition,
( f0(bG17)
<=> ( $true = bG18 ) ),
introduced(definition,[new_symbols(definition,[bG18])],[fool_formula_definition]) ).
tff(f22,definition,
( f0(bG18)
<=> ( $true = bG19 ) ),
introduced(definition,[new_symbols(definition,[bG19])],[fool_formula_definition]) ).
tff(f23,plain,
~ ( f0(bG8)
<=> f0(bG19) ),
inference(fool_elimination,[],[f2,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7,f6,f5,f4,f3]) ).
tff(f24,plain,
( f0(bG8)
<~> f0(bG19) ),
inference(ennf_transformation,[],[f23]) ).
tff(f25,plain,
( ( f0(bG18)
| ( $true != bG19 ) )
& ( ( $true = bG19 )
| ~ f0(bG18) ) ),
inference(nnf_transformation,[],[f22]) ).
tff(f26,plain,
( ( f0(bG17)
| ( $true != bG18 ) )
& ( ( $true = bG18 )
| ~ f0(bG17) ) ),
inference(nnf_transformation,[],[f21]) ).
tff(f27,plain,
( ( f1(bG16)
| ( $true != bG17 ) )
& ( ( $true = bG17 )
| ~ f1(bG16) ) ),
inference(nnf_transformation,[],[f20]) ).
tff(f28,plain,
( ( f2(bG15)
| ( $true != bG16 ) )
& ( ( $true = bG16 )
| ~ f2(bG15) ) ),
inference(nnf_transformation,[],[f19]) ).
tff(f29,plain,
( ( f2(bG14)
| ( $true != bG15 ) )
& ( ( $true = bG15 )
| ~ f2(bG14) ) ),
inference(nnf_transformation,[],[f18]) ).
tff(f30,plain,
( ( f2(bG13)
| ( $true != bG14 ) )
& ( ( $true = bG14 )
| ~ f2(bG13) ) ),
inference(nnf_transformation,[],[f17]) ).
tff(f31,plain,
( ( f3(bG12)
| ( $true != bG13 ) )
& ( ( $true = bG13 )
| ~ f3(bG12) ) ),
inference(nnf_transformation,[],[f16]) ).
tff(f32,plain,
( ( f4(bG11)
| ( $true != bG12 ) )
& ( ( $true = bG12 )
| ~ f4(bG11) ) ),
inference(nnf_transformation,[],[f15]) ).
tff(f33,plain,
( ( f4(bG10)
| ( $true != bG11 ) )
& ( ( $true = bG11 )
| ~ f4(bG10) ) ),
inference(nnf_transformation,[],[f14]) ).
tff(f34,plain,
( ( f4(bG9)
| ( $true != bG10 ) )
& ( ( $true = bG10 )
| ~ f4(bG9) ) ),
inference(nnf_transformation,[],[f13]) ).
tff(f35,plain,
( ( x
| ( $true != bG9 ) )
& ( ( $true = bG9 )
| ~ x ) ),
inference(nnf_transformation,[],[f12]) ).
tff(f36,plain,
( ( f1(bG7)
| ( $true != bG8 ) )
& ( ( $true = bG8 )
| ~ f1(bG7) ) ),
inference(nnf_transformation,[],[f11]) ).
tff(f37,plain,
( ( f1(bG6)
| ( $true != bG7 ) )
& ( ( $true = bG7 )
| ~ f1(bG6) ) ),
inference(nnf_transformation,[],[f10]) ).
tff(f38,plain,
( ( f1(bG5)
| ( $true != bG6 ) )
& ( ( $true = bG6 )
| ~ f1(bG5) ) ),
inference(nnf_transformation,[],[f9]) ).
tff(f39,plain,
( ( f2(bG4)
| ( $true != bG5 ) )
& ( ( $true = bG5 )
| ~ f2(bG4) ) ),
inference(nnf_transformation,[],[f8]) ).
tff(f40,plain,
( ( f3(bG3)
| ( $true != bG4 ) )
& ( ( $true = bG4 )
| ~ f3(bG3) ) ),
inference(nnf_transformation,[],[f7]) ).
tff(f41,plain,
( ( f3(bG2)
| ( $true != bG3 ) )
& ( ( $true = bG3 )
| ~ f3(bG2) ) ),
inference(nnf_transformation,[],[f6]) ).
tff(f42,plain,
( ( f3(bG1)
| ( $true != bG2 ) )
& ( ( $true = bG2 )
| ~ f3(bG1) ) ),
inference(nnf_transformation,[],[f5]) ).
tff(f43,plain,
( ( f4(bG0)
| ( $true != bG1 ) )
& ( ( $true = bG1 )
| ~ f4(bG0) ) ),
inference(nnf_transformation,[],[f4]) ).
tff(f44,plain,
( ( x
| ( bG0 != $true ) )
& ( ( bG0 = $true )
| ~ x ) ),
inference(nnf_transformation,[],[f3]) ).
tff(f45,plain,
( ( ~ f0(bG19)
| ~ f0(bG8) )
& ( f0(bG19)
| f0(bG8) ) ),
inference(nnf_transformation,[],[f24]) ).
tff(f46,plain,
( ( $true = bG19 )
| ~ f0(bG18) ),
inference(cnf_transformation,[],[f25]) ).
tff(f47,plain,
( f0(bG18)
| ( $true != bG19 ) ),
inference(cnf_transformation,[],[f25]) ).
tff(f48,plain,
( ( $true = bG18 )
| ~ f0(bG17) ),
inference(cnf_transformation,[],[f26]) ).
tff(f49,plain,
( f0(bG17)
| ( $true != bG18 ) ),
inference(cnf_transformation,[],[f26]) ).
tff(f50,plain,
( ( $true = bG17 )
| ~ f1(bG16) ),
inference(cnf_transformation,[],[f27]) ).
tff(f51,plain,
( f1(bG16)
| ( $true != bG17 ) ),
inference(cnf_transformation,[],[f27]) ).
tff(f52,plain,
( ( $true = bG16 )
| ~ f2(bG15) ),
inference(cnf_transformation,[],[f28]) ).
tff(f53,plain,
( f2(bG15)
| ( $true != bG16 ) ),
inference(cnf_transformation,[],[f28]) ).
tff(f54,plain,
( ( $true = bG15 )
| ~ f2(bG14) ),
inference(cnf_transformation,[],[f29]) ).
tff(f55,plain,
( f2(bG14)
| ( $true != bG15 ) ),
inference(cnf_transformation,[],[f29]) ).
tff(f56,plain,
( ( $true = bG14 )
| ~ f2(bG13) ),
inference(cnf_transformation,[],[f30]) ).
tff(f57,plain,
( f2(bG13)
| ( $true != bG14 ) ),
inference(cnf_transformation,[],[f30]) ).
tff(f58,plain,
( ( $true = bG13 )
| ~ f3(bG12) ),
inference(cnf_transformation,[],[f31]) ).
tff(f59,plain,
( f3(bG12)
| ( $true != bG13 ) ),
inference(cnf_transformation,[],[f31]) ).
tff(f60,plain,
( ( $true = bG12 )
| ~ f4(bG11) ),
inference(cnf_transformation,[],[f32]) ).
tff(f61,plain,
( f4(bG11)
| ( $true != bG12 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f62,plain,
( ( $true = bG11 )
| ~ f4(bG10) ),
inference(cnf_transformation,[],[f33]) ).
tff(f63,plain,
( f4(bG10)
| ( $true != bG11 ) ),
inference(cnf_transformation,[],[f33]) ).
tff(f64,plain,
( ( $true = bG10 )
| ~ f4(bG9) ),
inference(cnf_transformation,[],[f34]) ).
tff(f65,plain,
( f4(bG9)
| ( $true != bG10 ) ),
inference(cnf_transformation,[],[f34]) ).
tff(f66,plain,
( ( $true = bG9 )
| ~ x ),
inference(cnf_transformation,[],[f35]) ).
tff(f67,plain,
( x
| ( $true != bG9 ) ),
inference(cnf_transformation,[],[f35]) ).
tff(f68,plain,
( ( $true = bG8 )
| ~ f1(bG7) ),
inference(cnf_transformation,[],[f36]) ).
tff(f69,plain,
( f1(bG7)
| ( $true != bG8 ) ),
inference(cnf_transformation,[],[f36]) ).
tff(f70,plain,
( ( $true = bG7 )
| ~ f1(bG6) ),
inference(cnf_transformation,[],[f37]) ).
tff(f71,plain,
( f1(bG6)
| ( $true != bG7 ) ),
inference(cnf_transformation,[],[f37]) ).
tff(f72,plain,
( ( $true = bG6 )
| ~ f1(bG5) ),
inference(cnf_transformation,[],[f38]) ).
tff(f73,plain,
( f1(bG5)
| ( $true != bG6 ) ),
inference(cnf_transformation,[],[f38]) ).
tff(f74,plain,
( ( $true = bG5 )
| ~ f2(bG4) ),
inference(cnf_transformation,[],[f39]) ).
tff(f75,plain,
( f2(bG4)
| ( $true != bG5 ) ),
inference(cnf_transformation,[],[f39]) ).
tff(f76,plain,
( ( $true = bG4 )
| ~ f3(bG3) ),
inference(cnf_transformation,[],[f40]) ).
tff(f77,plain,
( f3(bG3)
| ( $true != bG4 ) ),
inference(cnf_transformation,[],[f40]) ).
tff(f78,plain,
( ( $true = bG3 )
| ~ f3(bG2) ),
inference(cnf_transformation,[],[f41]) ).
tff(f79,plain,
( f3(bG2)
| ( $true != bG3 ) ),
inference(cnf_transformation,[],[f41]) ).
tff(f80,plain,
( ( $true = bG2 )
| ~ f3(bG1) ),
inference(cnf_transformation,[],[f42]) ).
tff(f81,plain,
( f3(bG1)
| ( $true != bG2 ) ),
inference(cnf_transformation,[],[f42]) ).
tff(f82,plain,
( ( $true = bG1 )
| ~ f4(bG0) ),
inference(cnf_transformation,[],[f43]) ).
tff(f83,plain,
( f4(bG0)
| ( $true != bG1 ) ),
inference(cnf_transformation,[],[f43]) ).
tff(f84,plain,
( ( bG0 = $true )
| ~ x ),
inference(cnf_transformation,[],[f44]) ).
tff(f85,plain,
( x
| ( bG0 != $true ) ),
inference(cnf_transformation,[],[f44]) ).
tff(f86,plain,
( f0(bG19)
| f0(bG8) ),
inference(cnf_transformation,[],[f45]) ).
tff(f87,plain,
( ~ f0(bG19)
| ~ f0(bG8) ),
inference(cnf_transformation,[],[f45]) ).
tff(f89,plain,
! [X0: $o] :
( ( $false = (X0) )
| ( $true = (X0) ) ),
introduced(definition,[],[fool_exhaustiveness_axiom]) ).
tff(f91,definition,
( spl20_1
<=> f0(bG8) ),
introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition]) ).
tff(f92,plain,
( ~ f0(bG8)
| spl20_1 ),
inference(avatar_component_clause,[],[f91]) ).
tff(f93,plain,
( f0(bG8)
| ~ spl20_1 ),
inference(avatar_component_clause,[],[f91]) ).
tff(f95,definition,
( spl20_2
<=> f0(bG19) ),
introduced(definition,[new_symbols(definition,[spl20_2])],[avatar_definition]) ).
tff(f96,plain,
( ~ f0(bG19)
| spl20_2 ),
inference(avatar_component_clause,[],[f95]) ).
tff(f97,plain,
( f0(bG19)
| ~ spl20_2 ),
inference(avatar_component_clause,[],[f95]) ).
tff(f98,plain,
( spl20_1
| spl20_2 ),
inference(avatar_split_clause,[],[f86,f95,f91]) ).
tff(f99,plain,
( ~ spl20_1
| ~ spl20_2 ),
inference(avatar_split_clause,[],[f87,f95,f91]) ).
tff(f101,definition,
( spl20_3
<=> x ),
introduced(definition,[new_symbols(definition,[spl20_3])],[avatar_definition]) ).
tff(f105,definition,
( spl20_4
<=> ( bG0 = $true ) ),
introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition]) ).
tff(f107,plain,
( ( bG0 = $true )
| ~ spl20_4 ),
inference(avatar_component_clause,[],[f105]) ).
tff(f108,plain,
( ~ spl20_3
| spl20_4 ),
inference(avatar_split_clause,[],[f84,f105,f101]) ).
tff(f109,plain,
( ~ spl20_4
| spl20_3 ),
inference(avatar_split_clause,[],[f85,f101,f105]) ).
tff(f111,definition,
( spl20_5
<=> f4(bG0) ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
tff(f112,plain,
( f4(bG0)
| ~ spl20_5 ),
inference(avatar_component_clause,[],[f111]) ).
tff(f113,plain,
( ~ f4(bG0)
| spl20_5 ),
inference(avatar_component_clause,[],[f111]) ).
tff(f115,definition,
( spl20_6
<=> ( $true = bG1 ) ),
introduced(definition,[new_symbols(definition,[spl20_6])],[avatar_definition]) ).
tff(f116,plain,
( ( $true != bG1 )
| spl20_6 ),
inference(avatar_component_clause,[],[f115]) ).
tff(f117,plain,
( ( $true = bG1 )
| ~ spl20_6 ),
inference(avatar_component_clause,[],[f115]) ).
tff(f118,plain,
( ~ spl20_5
| spl20_6 ),
inference(avatar_split_clause,[],[f82,f115,f111]) ).
tff(f119,plain,
( ~ spl20_6
| spl20_5 ),
inference(avatar_split_clause,[],[f83,f111,f115]) ).
tff(f121,definition,
( spl20_7
<=> f3(bG1) ),
introduced(definition,[new_symbols(definition,[spl20_7])],[avatar_definition]) ).
tff(f122,plain,
( f3(bG1)
| ~ spl20_7 ),
inference(avatar_component_clause,[],[f121]) ).
tff(f123,plain,
( ~ f3(bG1)
| spl20_7 ),
inference(avatar_component_clause,[],[f121]) ).
tff(f125,definition,
( spl20_8
<=> ( $true = bG2 ) ),
introduced(definition,[new_symbols(definition,[spl20_8])],[avatar_definition]) ).
tff(f127,plain,
( ( $true = bG2 )
| ~ spl20_8 ),
inference(avatar_component_clause,[],[f125]) ).
tff(f128,plain,
( ~ spl20_7
| spl20_8 ),
inference(avatar_split_clause,[],[f80,f125,f121]) ).
tff(f129,plain,
( ~ spl20_8
| spl20_7 ),
inference(avatar_split_clause,[],[f81,f121,f125]) ).
tff(f131,definition,
( spl20_9
<=> f3(bG2) ),
introduced(definition,[new_symbols(definition,[spl20_9])],[avatar_definition]) ).
tff(f132,plain,
( f3(bG2)
| ~ spl20_9 ),
inference(avatar_component_clause,[],[f131]) ).
tff(f133,plain,
( ~ f3(bG2)
| spl20_9 ),
inference(avatar_component_clause,[],[f131]) ).
tff(f135,definition,
( spl20_10
<=> ( $true = bG3 ) ),
introduced(definition,[new_symbols(definition,[spl20_10])],[avatar_definition]) ).
tff(f137,plain,
( ( $true = bG3 )
| ~ spl20_10 ),
inference(avatar_component_clause,[],[f135]) ).
tff(f138,plain,
( ~ spl20_9
| spl20_10 ),
inference(avatar_split_clause,[],[f78,f135,f131]) ).
tff(f139,plain,
( ~ spl20_10
| spl20_9 ),
inference(avatar_split_clause,[],[f79,f131,f135]) ).
tff(f141,definition,
( spl20_11
<=> f3(bG3) ),
introduced(definition,[new_symbols(definition,[spl20_11])],[avatar_definition]) ).
tff(f142,plain,
( f3(bG3)
| ~ spl20_11 ),
inference(avatar_component_clause,[],[f141]) ).
tff(f143,plain,
( ~ f3(bG3)
| spl20_11 ),
inference(avatar_component_clause,[],[f141]) ).
tff(f145,definition,
( spl20_12
<=> ( $true = bG4 ) ),
introduced(definition,[new_symbols(definition,[spl20_12])],[avatar_definition]) ).
tff(f147,plain,
( ( $true = bG4 )
| ~ spl20_12 ),
inference(avatar_component_clause,[],[f145]) ).
tff(f148,plain,
( ~ spl20_11
| spl20_12 ),
inference(avatar_split_clause,[],[f76,f145,f141]) ).
tff(f149,plain,
( ~ spl20_12
| spl20_11 ),
inference(avatar_split_clause,[],[f77,f141,f145]) ).
tff(f151,definition,
( spl20_13
<=> f2(bG4) ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
tff(f152,plain,
( f2(bG4)
| ~ spl20_13 ),
inference(avatar_component_clause,[],[f151]) ).
tff(f153,plain,
( ~ f2(bG4)
| spl20_13 ),
inference(avatar_component_clause,[],[f151]) ).
tff(f155,definition,
( spl20_14
<=> ( $true = bG5 ) ),
introduced(definition,[new_symbols(definition,[spl20_14])],[avatar_definition]) ).
tff(f157,plain,
( ( $true = bG5 )
| ~ spl20_14 ),
inference(avatar_component_clause,[],[f155]) ).
tff(f158,plain,
( ~ spl20_13
| spl20_14 ),
inference(avatar_split_clause,[],[f74,f155,f151]) ).
tff(f159,plain,
( ~ spl20_14
| spl20_13 ),
inference(avatar_split_clause,[],[f75,f151,f155]) ).
tff(f161,definition,
( spl20_15
<=> f1(bG5) ),
introduced(definition,[new_symbols(definition,[spl20_15])],[avatar_definition]) ).
tff(f162,plain,
( f1(bG5)
| ~ spl20_15 ),
inference(avatar_component_clause,[],[f161]) ).
tff(f163,plain,
( ~ f1(bG5)
| spl20_15 ),
inference(avatar_component_clause,[],[f161]) ).
tff(f165,definition,
( spl20_16
<=> ( $true = bG6 ) ),
introduced(definition,[new_symbols(definition,[spl20_16])],[avatar_definition]) ).
tff(f166,plain,
( ( $true != bG6 )
| spl20_16 ),
inference(avatar_component_clause,[],[f165]) ).
tff(f167,plain,
( ( $true = bG6 )
| ~ spl20_16 ),
inference(avatar_component_clause,[],[f165]) ).
tff(f168,plain,
( ~ spl20_15
| spl20_16 ),
inference(avatar_split_clause,[],[f72,f165,f161]) ).
tff(f169,plain,
( ~ spl20_16
| spl20_15 ),
inference(avatar_split_clause,[],[f73,f161,f165]) ).
tff(f171,definition,
( spl20_17
<=> f1(bG6) ),
introduced(definition,[new_symbols(definition,[spl20_17])],[avatar_definition]) ).
tff(f172,plain,
( f1(bG6)
| ~ spl20_17 ),
inference(avatar_component_clause,[],[f171]) ).
tff(f173,plain,
( ~ f1(bG6)
| spl20_17 ),
inference(avatar_component_clause,[],[f171]) ).
tff(f175,definition,
( spl20_18
<=> ( $true = bG7 ) ),
introduced(definition,[new_symbols(definition,[spl20_18])],[avatar_definition]) ).
tff(f177,plain,
( ( $true = bG7 )
| ~ spl20_18 ),
inference(avatar_component_clause,[],[f175]) ).
tff(f178,plain,
( ~ spl20_17
| spl20_18 ),
inference(avatar_split_clause,[],[f70,f175,f171]) ).
tff(f179,plain,
( ~ spl20_18
| spl20_17 ),
inference(avatar_split_clause,[],[f71,f171,f175]) ).
tff(f181,definition,
( spl20_19
<=> f1(bG7) ),
introduced(definition,[new_symbols(definition,[spl20_19])],[avatar_definition]) ).
tff(f182,plain,
( f1(bG7)
| ~ spl20_19 ),
inference(avatar_component_clause,[],[f181]) ).
tff(f183,plain,
( ~ f1(bG7)
| spl20_19 ),
inference(avatar_component_clause,[],[f181]) ).
tff(f185,definition,
( spl20_20
<=> ( $true = bG8 ) ),
introduced(definition,[new_symbols(definition,[spl20_20])],[avatar_definition]) ).
tff(f187,plain,
( ( $true = bG8 )
| ~ spl20_20 ),
inference(avatar_component_clause,[],[f185]) ).
tff(f188,plain,
( ~ spl20_19
| spl20_20 ),
inference(avatar_split_clause,[],[f68,f185,f181]) ).
tff(f189,plain,
( ~ spl20_20
| spl20_19 ),
inference(avatar_split_clause,[],[f69,f181,f185]) ).
tff(f191,definition,
( spl20_21
<=> ( $true = bG9 ) ),
introduced(definition,[new_symbols(definition,[spl20_21])],[avatar_definition]) ).
tff(f193,plain,
( ( $true = bG9 )
| ~ spl20_21 ),
inference(avatar_component_clause,[],[f191]) ).
tff(f194,plain,
( ~ spl20_3
| spl20_21 ),
inference(avatar_split_clause,[],[f66,f191,f101]) ).
tff(f195,plain,
( ~ spl20_21
| spl20_3 ),
inference(avatar_split_clause,[],[f67,f101,f191]) ).
tff(f197,definition,
( spl20_22
<=> f4(bG9) ),
introduced(definition,[new_symbols(definition,[spl20_22])],[avatar_definition]) ).
tff(f198,plain,
( f4(bG9)
| ~ spl20_22 ),
inference(avatar_component_clause,[],[f197]) ).
tff(f199,plain,
( ~ f4(bG9)
| spl20_22 ),
inference(avatar_component_clause,[],[f197]) ).
tff(f201,definition,
( spl20_23
<=> ( $true = bG10 ) ),
introduced(definition,[new_symbols(definition,[spl20_23])],[avatar_definition]) ).
tff(f202,plain,
( ( $true != bG10 )
| spl20_23 ),
inference(avatar_component_clause,[],[f201]) ).
tff(f203,plain,
( ( $true = bG10 )
| ~ spl20_23 ),
inference(avatar_component_clause,[],[f201]) ).
tff(f204,plain,
( ~ spl20_22
| spl20_23 ),
inference(avatar_split_clause,[],[f64,f201,f197]) ).
tff(f205,plain,
( ~ spl20_23
| spl20_22 ),
inference(avatar_split_clause,[],[f65,f197,f201]) ).
tff(f207,definition,
( spl20_24
<=> f4(bG10) ),
introduced(definition,[new_symbols(definition,[spl20_24])],[avatar_definition]) ).
tff(f208,plain,
( f4(bG10)
| ~ spl20_24 ),
inference(avatar_component_clause,[],[f207]) ).
tff(f209,plain,
( ~ f4(bG10)
| spl20_24 ),
inference(avatar_component_clause,[],[f207]) ).
tff(f211,definition,
( spl20_25
<=> ( $true = bG11 ) ),
introduced(definition,[new_symbols(definition,[spl20_25])],[avatar_definition]) ).
tff(f212,plain,
( ( $true != bG11 )
| spl20_25 ),
inference(avatar_component_clause,[],[f211]) ).
tff(f213,plain,
( ( $true = bG11 )
| ~ spl20_25 ),
inference(avatar_component_clause,[],[f211]) ).
tff(f214,plain,
( ~ spl20_24
| spl20_25 ),
inference(avatar_split_clause,[],[f62,f211,f207]) ).
tff(f215,plain,
( ~ spl20_25
| spl20_24 ),
inference(avatar_split_clause,[],[f63,f207,f211]) ).
tff(f217,definition,
( spl20_26
<=> f4(bG11) ),
introduced(definition,[new_symbols(definition,[spl20_26])],[avatar_definition]) ).
tff(f218,plain,
( f4(bG11)
| ~ spl20_26 ),
inference(avatar_component_clause,[],[f217]) ).
tff(f219,plain,
( ~ f4(bG11)
| spl20_26 ),
inference(avatar_component_clause,[],[f217]) ).
tff(f221,definition,
( spl20_27
<=> ( $true = bG12 ) ),
introduced(definition,[new_symbols(definition,[spl20_27])],[avatar_definition]) ).
tff(f222,plain,
( ( $true != bG12 )
| spl20_27 ),
inference(avatar_component_clause,[],[f221]) ).
tff(f223,plain,
( ( $true = bG12 )
| ~ spl20_27 ),
inference(avatar_component_clause,[],[f221]) ).
tff(f224,plain,
( ~ spl20_26
| spl20_27 ),
inference(avatar_split_clause,[],[f60,f221,f217]) ).
tff(f225,plain,
( ~ spl20_27
| spl20_26 ),
inference(avatar_split_clause,[],[f61,f217,f221]) ).
tff(f227,definition,
( spl20_28
<=> f3(bG12) ),
introduced(definition,[new_symbols(definition,[spl20_28])],[avatar_definition]) ).
tff(f228,plain,
( f3(bG12)
| ~ spl20_28 ),
inference(avatar_component_clause,[],[f227]) ).
tff(f229,plain,
( ~ f3(bG12)
| spl20_28 ),
inference(avatar_component_clause,[],[f227]) ).
tff(f231,definition,
( spl20_29
<=> ( $true = bG13 ) ),
introduced(definition,[new_symbols(definition,[spl20_29])],[avatar_definition]) ).
tff(f232,plain,
( ( $true != bG13 )
| spl20_29 ),
inference(avatar_component_clause,[],[f231]) ).
tff(f233,plain,
( ( $true = bG13 )
| ~ spl20_29 ),
inference(avatar_component_clause,[],[f231]) ).
tff(f234,plain,
( ~ spl20_28
| spl20_29 ),
inference(avatar_split_clause,[],[f58,f231,f227]) ).
tff(f235,plain,
( ~ spl20_29
| spl20_28 ),
inference(avatar_split_clause,[],[f59,f227,f231]) ).
tff(f237,definition,
( spl20_30
<=> f2(bG13) ),
introduced(definition,[new_symbols(definition,[spl20_30])],[avatar_definition]) ).
tff(f238,plain,
( f2(bG13)
| ~ spl20_30 ),
inference(avatar_component_clause,[],[f237]) ).
tff(f239,plain,
( ~ f2(bG13)
| spl20_30 ),
inference(avatar_component_clause,[],[f237]) ).
tff(f241,definition,
( spl20_31
<=> ( $true = bG14 ) ),
introduced(definition,[new_symbols(definition,[spl20_31])],[avatar_definition]) ).
tff(f242,plain,
( ( $true != bG14 )
| spl20_31 ),
inference(avatar_component_clause,[],[f241]) ).
tff(f243,plain,
( ( $true = bG14 )
| ~ spl20_31 ),
inference(avatar_component_clause,[],[f241]) ).
tff(f244,plain,
( ~ spl20_30
| spl20_31 ),
inference(avatar_split_clause,[],[f56,f241,f237]) ).
tff(f245,plain,
( ~ spl20_31
| spl20_30 ),
inference(avatar_split_clause,[],[f57,f237,f241]) ).
tff(f247,definition,
( spl20_32
<=> f2(bG14) ),
introduced(definition,[new_symbols(definition,[spl20_32])],[avatar_definition]) ).
tff(f248,plain,
( f2(bG14)
| ~ spl20_32 ),
inference(avatar_component_clause,[],[f247]) ).
tff(f249,plain,
( ~ f2(bG14)
| spl20_32 ),
inference(avatar_component_clause,[],[f247]) ).
tff(f251,definition,
( spl20_33
<=> ( $true = bG15 ) ),
introduced(definition,[new_symbols(definition,[spl20_33])],[avatar_definition]) ).
tff(f252,plain,
( ( $true != bG15 )
| spl20_33 ),
inference(avatar_component_clause,[],[f251]) ).
tff(f253,plain,
( ( $true = bG15 )
| ~ spl20_33 ),
inference(avatar_component_clause,[],[f251]) ).
tff(f254,plain,
( ~ spl20_32
| spl20_33 ),
inference(avatar_split_clause,[],[f54,f251,f247]) ).
tff(f255,plain,
( ~ spl20_33
| spl20_32 ),
inference(avatar_split_clause,[],[f55,f247,f251]) ).
tff(f257,definition,
( spl20_34
<=> f2(bG15) ),
introduced(definition,[new_symbols(definition,[spl20_34])],[avatar_definition]) ).
tff(f258,plain,
( f2(bG15)
| ~ spl20_34 ),
inference(avatar_component_clause,[],[f257]) ).
tff(f259,plain,
( ~ f2(bG15)
| spl20_34 ),
inference(avatar_component_clause,[],[f257]) ).
tff(f261,definition,
( spl20_35
<=> ( $true = bG16 ) ),
introduced(definition,[new_symbols(definition,[spl20_35])],[avatar_definition]) ).
tff(f262,plain,
( ( $true != bG16 )
| spl20_35 ),
inference(avatar_component_clause,[],[f261]) ).
tff(f263,plain,
( ( $true = bG16 )
| ~ spl20_35 ),
inference(avatar_component_clause,[],[f261]) ).
tff(f264,plain,
( ~ spl20_34
| spl20_35 ),
inference(avatar_split_clause,[],[f52,f261,f257]) ).
tff(f265,plain,
( ~ spl20_35
| spl20_34 ),
inference(avatar_split_clause,[],[f53,f257,f261]) ).
tff(f267,definition,
( spl20_36
<=> f1(bG16) ),
introduced(definition,[new_symbols(definition,[spl20_36])],[avatar_definition]) ).
tff(f268,plain,
( f1(bG16)
| ~ spl20_36 ),
inference(avatar_component_clause,[],[f267]) ).
tff(f269,plain,
( ~ f1(bG16)
| spl20_36 ),
inference(avatar_component_clause,[],[f267]) ).
tff(f271,definition,
( spl20_37
<=> ( $true = bG17 ) ),
introduced(definition,[new_symbols(definition,[spl20_37])],[avatar_definition]) ).
tff(f273,plain,
( ( $true = bG17 )
| ~ spl20_37 ),
inference(avatar_component_clause,[],[f271]) ).
tff(f274,plain,
( ~ spl20_36
| spl20_37 ),
inference(avatar_split_clause,[],[f50,f271,f267]) ).
tff(f275,plain,
( ~ spl20_37
| spl20_36 ),
inference(avatar_split_clause,[],[f51,f267,f271]) ).
tff(f277,definition,
( spl20_38
<=> f0(bG17) ),
introduced(definition,[new_symbols(definition,[spl20_38])],[avatar_definition]) ).
tff(f278,plain,
( f0(bG17)
| ~ spl20_38 ),
inference(avatar_component_clause,[],[f277]) ).
tff(f279,plain,
( ~ f0(bG17)
| spl20_38 ),
inference(avatar_component_clause,[],[f277]) ).
tff(f281,definition,
( spl20_39
<=> ( $true = bG18 ) ),
introduced(definition,[new_symbols(definition,[spl20_39])],[avatar_definition]) ).
tff(f282,plain,
( ( $true != bG18 )
| spl20_39 ),
inference(avatar_component_clause,[],[f281]) ).
tff(f283,plain,
( ( $true = bG18 )
| ~ spl20_39 ),
inference(avatar_component_clause,[],[f281]) ).
tff(f284,plain,
( ~ spl20_38
| spl20_39 ),
inference(avatar_split_clause,[],[f48,f281,f277]) ).
tff(f285,plain,
( ~ spl20_39
| spl20_38 ),
inference(avatar_split_clause,[],[f49,f277,f281]) ).
tff(f287,definition,
( spl20_40
<=> f0(bG18) ),
introduced(definition,[new_symbols(definition,[spl20_40])],[avatar_definition]) ).
tff(f288,plain,
( f0(bG18)
| ~ spl20_40 ),
inference(avatar_component_clause,[],[f287]) ).
tff(f289,plain,
( ~ f0(bG18)
| spl20_40 ),
inference(avatar_component_clause,[],[f287]) ).
tff(f291,definition,
( spl20_41
<=> ( $true = bG19 ) ),
introduced(definition,[new_symbols(definition,[spl20_41])],[avatar_definition]) ).
tff(f292,plain,
( ( $true != bG19 )
| spl20_41 ),
inference(avatar_component_clause,[],[f291]) ).
tff(f293,plain,
( ( $true = bG19 )
| ~ spl20_41 ),
inference(avatar_component_clause,[],[f291]) ).
tff(f294,plain,
( ~ spl20_40
| spl20_41 ),
inference(avatar_split_clause,[],[f46,f291,f287]) ).
tff(f295,plain,
( ~ spl20_41
| spl20_40 ),
inference(avatar_split_clause,[],[f47,f287,f291]) ).
tff(f298,plain,
( ~ f4($false)
| ( bG0 = $true )
| spl20_5 ),
inference(superposition,[],[f113,f89]) ).
tff(f300,plain,
( ~ f3($false)
| ( $true = bG1 )
| spl20_7 ),
inference(superposition,[],[f123,f89]) ).
tff(f308,plain,
( ~ f1($false)
| ( $true = bG5 )
| spl20_15 ),
inference(superposition,[],[f163,f89]) ).
tff(f314,plain,
( ~ f0($false)
| ( $true = bG8 )
| spl20_1 ),
inference(superposition,[],[f92,f89]) ).
tff(f318,plain,
( ~ f4($false)
| ( $true = bG10 )
| spl20_24 ),
inference(superposition,[],[f209,f89]) ).
tff(f322,plain,
( ~ f3($false)
| ( $true = bG12 )
| spl20_28 ),
inference(superposition,[],[f229,f89]) ).
tff(f326,plain,
( ~ f2($false)
| ( $true = bG14 )
| spl20_32 ),
inference(superposition,[],[f249,f89]) ).
tff(f330,plain,
( ~ f1($false)
| ( $true = bG16 )
| spl20_36 ),
inference(superposition,[],[f269,f89]) ).
tff(f334,plain,
( ~ f0($false)
| ( $true = bG18 )
| spl20_40 ),
inference(superposition,[],[f289,f89]) ).
tff(f336,plain,
( f0($false)
| ( $true = bG19 )
| ~ spl20_2 ),
inference(superposition,[],[f97,f89]) ).
tff(f338,plain,
( f0($false)
| ~ spl20_2
| spl20_41 ),
inference(forward_subsumption_resolution,[],[f336,f292]) ).
tff(f339,plain,
( ~ f0($false)
| spl20_39
| spl20_40 ),
inference(forward_subsumption_resolution,[],[f334,f282]) ).
tff(f341,plain,
( ~ f1($false)
| spl20_35
| spl20_36 ),
inference(forward_subsumption_resolution,[],[f330,f262]) ).
tff(f343,plain,
( ~ f2($false)
| spl20_31
| spl20_32 ),
inference(forward_subsumption_resolution,[],[f326,f242]) ).
tff(f345,plain,
( ~ f3($false)
| spl20_27
| spl20_28 ),
inference(forward_subsumption_resolution,[],[f322,f222]) ).
tff(f347,plain,
( ~ f4($false)
| spl20_23
| spl20_24 ),
inference(forward_subsumption_resolution,[],[f318,f202]) ).
tff(f356,plain,
( ~ f3($false)
| spl20_6
| spl20_7 ),
inference(forward_subsumption_resolution,[],[f300,f116]) ).
tff(f361,plain,
( ( $true = bG8 )
| spl20_1
| ~ spl20_2
| spl20_41 ),
inference(forward_subsumption_resolution,[],[f314,f338]) ).
tff(f362,plain,
( spl20_20
| spl20_1
| ~ spl20_2
| spl20_41 ),
inference(avatar_split_clause,[],[f361,f291,f95,f91,f185]) ).
tff(f363,plain,
( f1($false)
| ( $true = bG7 )
| ~ spl20_19 ),
inference(superposition,[],[f182,f89]) ).
tff(f377,plain,
( ~ f0($true)
| spl20_1
| ~ spl20_20 ),
inference(superposition,[],[f92,f187]) ).
tff(f381,plain,
( ~ f0($true)
| ~ spl20_39
| spl20_40 ),
inference(superposition,[],[f289,f283]) ).
tff(f388,plain,
( ( $true = bG7 )
| ~ spl20_19
| spl20_35
| spl20_36 ),
inference(forward_subsumption_resolution,[],[f363,f341]) ).
tff(f389,plain,
( spl20_18
| ~ spl20_19
| spl20_35
| spl20_36 ),
inference(avatar_split_clause,[],[f388,f267,f261,f181,f175]) ).
tff(f390,plain,
( f1($false)
| ( $true = bG6 )
| ~ spl20_17 ),
inference(superposition,[],[f172,f89]) ).
tff(f391,plain,
( ( $true = bG6 )
| ~ spl20_17
| spl20_35
| spl20_36 ),
inference(forward_subsumption_resolution,[],[f390,f341]) ).
tff(f392,plain,
( $false
| spl20_16
| ~ spl20_17
| spl20_35
| spl20_36 ),
inference(forward_subsumption_resolution,[],[f391,f166]) ).
tff(f393,plain,
( spl20_16
| ~ spl20_17
| spl20_35
| spl20_36 ),
inference(avatar_contradiction_clause,[],[f392]) ).
tff(f395,definition,
( spl20_42
<=> f1($false) ),
introduced(definition,[new_symbols(definition,[spl20_42])],[avatar_definition]) ).
tff(f397,plain,
( ~ f1($false)
| spl20_42 ),
inference(avatar_component_clause,[],[f395]) ).
tff(f401,plain,
( spl20_14
| ~ spl20_42
| spl20_15 ),
inference(avatar_split_clause,[],[f308,f161,f395,f155]) ).
tff(f404,plain,
( ~ f1($false)
| ( $true = bG6 )
| spl20_17 ),
inference(superposition,[],[f173,f89]) ).
tff(f405,plain,
( ~ f1($false)
| spl20_16
| spl20_17 ),
inference(forward_subsumption_resolution,[],[f404,f166]) ).
tff(f406,plain,
( ~ spl20_42
| spl20_16
| spl20_17 ),
inference(avatar_split_clause,[],[f405,f171,f165,f395]) ).
tff(f411,definition,
( spl20_43
<=> f0($false) ),
introduced(definition,[new_symbols(definition,[spl20_43])],[avatar_definition]) ).
tff(f412,plain,
( ~ f0($false)
| spl20_43 ),
inference(avatar_component_clause,[],[f411]) ).
tff(f415,plain,
( ~ f0($false)
| ( $true = bG19 )
| spl20_2 ),
inference(superposition,[],[f96,f89]) ).
tff(f418,plain,
( f0($true)
| ~ spl20_39
| ~ spl20_40 ),
inference(forward_demodulation,[],[f288,f283]) ).
tff(f419,plain,
( spl20_41
| ~ spl20_43
| spl20_2 ),
inference(avatar_split_clause,[],[f415,f95,f411,f291]) ).
tff(f421,plain,
( ~ f1($false)
| ( $true = bG7 )
| spl20_19 ),
inference(superposition,[],[f183,f89]) ).
tff(f422,plain,
( spl20_18
| ~ spl20_42
| spl20_19 ),
inference(avatar_split_clause,[],[f421,f181,f395,f175]) ).
tff(f424,plain,
( f2($false)
| ( $true = bG15 )
| ~ spl20_34 ),
inference(superposition,[],[f258,f89]) ).
tff(f425,plain,
( f2($false)
| spl20_33
| ~ spl20_34 ),
inference(forward_subsumption_resolution,[],[f424,f252]) ).
tff(f429,plain,
( ~ f0($true)
| spl20_2
| ~ spl20_41 ),
inference(superposition,[],[f96,f293]) ).
tff(f431,plain,
( $false
| spl20_2
| ~ spl20_39
| ~ spl20_40
| ~ spl20_41 ),
inference(forward_subsumption_resolution,[],[f429,f418]) ).
tff(f432,plain,
( spl20_2
| ~ spl20_39
| ~ spl20_40
| ~ spl20_41 ),
inference(avatar_contradiction_clause,[],[f431]) ).
tff(f437,plain,
( ~ f0($false)
| ( $true = bG17 )
| spl20_38 ),
inference(superposition,[],[f279,f89]) ).
tff(f440,plain,
( f0($false)
| ( $true = bG18 )
| ~ spl20_40 ),
inference(superposition,[],[f288,f89]) ).
tff(f445,plain,
( ~ f1($true)
| ~ spl20_14
| spl20_15 ),
inference(superposition,[],[f163,f157]) ).
tff(f449,plain,
( f1($true)
| ~ spl20_35
| ~ spl20_36 ),
inference(superposition,[],[f268,f263]) ).
tff(f451,plain,
( $false
| ~ spl20_14
| spl20_15
| ~ spl20_35
| ~ spl20_36 ),
inference(forward_subsumption_resolution,[],[f449,f445]) ).
tff(f452,plain,
( ~ spl20_14
| spl20_15
| ~ spl20_35
| ~ spl20_36 ),
inference(avatar_contradiction_clause,[],[f451]) ).
tff(f453,plain,
( ~ f2($false)
| ( $true = bG4 )
| spl20_13 ),
inference(superposition,[],[f153,f89]) ).
tff(f456,plain,
( ~ f0($true)
| ~ spl20_37
| spl20_38 ),
inference(superposition,[],[f279,f273]) ).
tff(f459,plain,
( $false
| spl20_31
| spl20_32
| spl20_33
| ~ spl20_34 ),
inference(forward_subsumption_resolution,[],[f425,f343]) ).
tff(f460,plain,
( spl20_31
| spl20_32
| spl20_33
| ~ spl20_34 ),
inference(avatar_contradiction_clause,[],[f459]) ).
tff(f462,definition,
( spl20_44
<=> f2($false) ),
introduced(definition,[new_symbols(definition,[spl20_44])],[avatar_definition]) ).
tff(f469,plain,
( spl20_12
| ~ spl20_44
| spl20_13 ),
inference(avatar_split_clause,[],[f453,f151,f462,f145]) ).
tff(f470,plain,
( f3($false)
| ( $true = bG3 )
| ~ spl20_11 ),
inference(superposition,[],[f142,f89]) ).
tff(f471,plain,
( ( $true = bG3 )
| ~ spl20_11
| spl20_27
| spl20_28 ),
inference(forward_subsumption_resolution,[],[f470,f345]) ).
tff(f474,plain,
( spl20_10
| ~ spl20_11
| spl20_27
| spl20_28 ),
inference(avatar_split_clause,[],[f471,f227,f221,f141,f135]) ).
tff(f480,definition,
( spl20_45
<=> f3($false) ),
introduced(definition,[new_symbols(definition,[spl20_45])],[avatar_definition]) ).
tff(f483,plain,
( spl20_10
| spl20_45
| ~ spl20_11 ),
inference(avatar_split_clause,[],[f470,f141,f480,f135]) ).
tff(f492,plain,
( f3($true)
| ~ spl20_10
| ~ spl20_11 ),
inference(superposition,[],[f142,f137]) ).
tff(f495,plain,
( ~ f2($true)
| ~ spl20_12
| spl20_13 ),
inference(superposition,[],[f153,f147]) ).
tff(f498,plain,
( f2($true)
| ~ spl20_29
| ~ spl20_30 ),
inference(superposition,[],[f238,f233]) ).
tff(f500,plain,
( $false
| ~ spl20_12
| spl20_13
| ~ spl20_29
| ~ spl20_30 ),
inference(forward_subsumption_resolution,[],[f498,f495]) ).
tff(f501,plain,
( ~ spl20_12
| spl20_13
| ~ spl20_29
| ~ spl20_30 ),
inference(avatar_contradiction_clause,[],[f500]) ).
tff(f502,plain,
( ~ f2($true)
| ~ spl20_29
| spl20_30 ),
inference(forward_demodulation,[],[f239,f233]) ).
tff(f507,plain,
( ~ spl20_45
| spl20_6
| spl20_7 ),
inference(avatar_split_clause,[],[f356,f121,f115,f480]) ).
tff(f509,plain,
( f3($false)
| ( $true = bG1 )
| ~ spl20_7 ),
inference(superposition,[],[f122,f89]) ).
tff(f510,plain,
( f3($false)
| spl20_6
| ~ spl20_7 ),
inference(forward_subsumption_resolution,[],[f509,f116]) ).
tff(f511,plain,
( spl20_45
| spl20_6
| ~ spl20_7 ),
inference(avatar_split_clause,[],[f510,f121,f115,f480]) ).
tff(f514,plain,
( f3($true)
| ~ spl20_8
| ~ spl20_9 ),
inference(superposition,[],[f132,f127]) ).
tff(f518,plain,
( f2($true)
| ~ spl20_33
| ~ spl20_34 ),
inference(superposition,[],[f258,f253]) ).
tff(f520,plain,
( $false
| ~ spl20_12
| spl20_13
| ~ spl20_33
| ~ spl20_34 ),
inference(forward_subsumption_resolution,[],[f518,f495]) ).
tff(f521,plain,
( ~ spl20_12
| spl20_13
| ~ spl20_33
| ~ spl20_34 ),
inference(avatar_contradiction_clause,[],[f520]) ).
tff(f522,plain,
( f2($true)
| ~ spl20_12
| ~ spl20_13 ),
inference(forward_demodulation,[],[f152,f147]) ).
tff(f523,plain,
( f1($false)
| ( $true = bG5 )
| ~ spl20_15 ),
inference(superposition,[],[f162,f89]) ).
tff(f524,plain,
( ( $true = bG5 )
| ~ spl20_15
| spl20_42 ),
inference(forward_subsumption_resolution,[],[f523,f397]) ).
tff(f525,plain,
( spl20_14
| ~ spl20_15
| spl20_42 ),
inference(avatar_split_clause,[],[f524,f395,f161,f155]) ).
tff(f526,plain,
( $false
| ~ spl20_12
| ~ spl20_13
| ~ spl20_29
| spl20_30 ),
inference(forward_subsumption_resolution,[],[f522,f502]) ).
tff(f527,plain,
( ~ spl20_12
| ~ spl20_13
| ~ spl20_29
| spl20_30 ),
inference(avatar_contradiction_clause,[],[f526]) ).
tff(f532,plain,
( f4($false)
| ( $true = bG11 )
| ~ spl20_26 ),
inference(superposition,[],[f218,f89]) ).
tff(f533,plain,
( f4($false)
| spl20_25
| ~ spl20_26 ),
inference(forward_subsumption_resolution,[],[f532,f212]) ).
tff(f539,plain,
( f1($true)
| ~ spl20_14
| ~ spl20_15 ),
inference(superposition,[],[f162,f157]) ).
tff(f546,plain,
( f1($true)
| ~ spl20_16
| ~ spl20_17 ),
inference(forward_demodulation,[],[f172,f167]) ).
tff(f549,plain,
( ~ f1($true)
| ~ spl20_18
| spl20_19 ),
inference(superposition,[],[f183,f177]) ).
tff(f551,plain,
( $false
| ~ spl20_18
| spl20_19
| ~ spl20_35
| ~ spl20_36 ),
inference(forward_subsumption_resolution,[],[f549,f449]) ).
tff(f552,plain,
( ~ spl20_18
| spl20_19
| ~ spl20_35
| ~ spl20_36 ),
inference(avatar_contradiction_clause,[],[f551]) ).
tff(f553,plain,
( ~ f1($true)
| ~ spl20_16
| spl20_17 ),
inference(forward_demodulation,[],[f173,f167]) ).
tff(f555,plain,
( ~ f1($true)
| ~ spl20_35
| spl20_36 ),
inference(forward_demodulation,[],[f269,f263]) ).
tff(f556,plain,
( spl20_37
| ~ spl20_43
| spl20_38 ),
inference(avatar_split_clause,[],[f437,f277,f411,f271]) ).
tff(f557,plain,
( f0($false)
| spl20_39
| ~ spl20_40 ),
inference(forward_subsumption_resolution,[],[f440,f282]) ).
tff(f558,plain,
( spl20_43
| spl20_39
| ~ spl20_40 ),
inference(avatar_split_clause,[],[f557,f287,f281,f411]) ).
tff(f559,plain,
( ~ spl20_43
| spl20_39
| spl20_40 ),
inference(avatar_split_clause,[],[f339,f287,f281,f411]) ).
tff(f560,plain,
( ! [X0: $o] :
( ~ f0((X0))
| ( $true = (X0) ) )
| spl20_43 ),
inference(superposition,[],[f412,f89]) ).
tff(f561,plain,
( f1($false)
| ( $true = bG7 )
| ~ spl20_19 ),
inference(superposition,[],[f182,f89]) ).
tff(f562,plain,
( spl20_18
| spl20_42
| ~ spl20_19 ),
inference(avatar_split_clause,[],[f561,f181,f395,f175]) ).
tff(f563,plain,
( ( $true = bG8 )
| ~ spl20_1
| spl20_43 ),
inference(resolution,[],[f560,f93]) ).
tff(f564,plain,
( spl20_20
| ~ spl20_1
| spl20_43 ),
inference(avatar_split_clause,[],[f563,f411,f91,f185]) ).
tff(f567,plain,
( f0($true)
| ~ spl20_1
| ~ spl20_20 ),
inference(superposition,[],[f93,f187]) ).
tff(f572,plain,
( $false
| ~ spl20_14
| ~ spl20_15
| ~ spl20_16
| spl20_17 ),
inference(forward_subsumption_resolution,[],[f539,f553]) ).
tff(f573,plain,
( ~ spl20_14
| ~ spl20_15
| ~ spl20_16
| spl20_17 ),
inference(avatar_contradiction_clause,[],[f572]) ).
tff(f578,plain,
( $false
| ~ spl20_1
| ~ spl20_20
| ~ spl20_37
| spl20_38 ),
inference(forward_subsumption_resolution,[],[f456,f567]) ).
tff(f579,plain,
( ~ spl20_1
| ~ spl20_20
| ~ spl20_37
| spl20_38 ),
inference(avatar_contradiction_clause,[],[f578]) ).
tff(f580,plain,
( $false
| ~ spl20_1
| ~ spl20_20
| ~ spl20_39
| spl20_40 ),
inference(forward_subsumption_resolution,[],[f381,f567]) ).
tff(f581,plain,
( ~ spl20_1
| ~ spl20_20
| ~ spl20_39
| spl20_40 ),
inference(avatar_contradiction_clause,[],[f580]) ).
tff(f582,plain,
( ~ f2($true)
| ~ spl20_33
| spl20_34 ),
inference(forward_demodulation,[],[f259,f253]) ).
tff(f584,plain,
( $false
| ~ spl20_12
| ~ spl20_13
| ~ spl20_33
| spl20_34 ),
inference(forward_subsumption_resolution,[],[f582,f522]) ).
tff(f585,plain,
( ~ spl20_12
| ~ spl20_13
| ~ spl20_33
| spl20_34 ),
inference(avatar_contradiction_clause,[],[f584]) ).
tff(f600,plain,
( f1($true)
| ~ spl20_18
| ~ spl20_19 ),
inference(superposition,[],[f182,f177]) ).
tff(f610,plain,
( ~ f2($true)
| ~ spl20_31
| spl20_32 ),
inference(superposition,[],[f249,f243]) ).
tff(f612,plain,
( $false
| ~ spl20_12
| ~ spl20_13
| ~ spl20_31
| spl20_32 ),
inference(forward_subsumption_resolution,[],[f610,f522]) ).
tff(f613,plain,
( ~ spl20_12
| ~ spl20_13
| ~ spl20_31
| spl20_32 ),
inference(avatar_contradiction_clause,[],[f612]) ).
tff(f614,plain,
( ~ f3($true)
| ~ spl20_27
| spl20_28 ),
inference(forward_demodulation,[],[f229,f223]) ).
tff(f617,plain,
( $false
| ~ spl20_10
| ~ spl20_11
| ~ spl20_27
| spl20_28 ),
inference(forward_subsumption_resolution,[],[f614,f492]) ).
tff(f618,plain,
( ~ spl20_10
| ~ spl20_11
| ~ spl20_27
| spl20_28 ),
inference(avatar_contradiction_clause,[],[f617]) ).
tff(f619,plain,
( ~ f3($true)
| ~ spl20_8
| spl20_9 ),
inference(forward_demodulation,[],[f133,f127]) ).
tff(f620,plain,
( ~ f2($false)
| ( $true = bG13 )
| spl20_30 ),
inference(superposition,[],[f239,f89]) ).
tff(f621,plain,
( spl20_29
| ~ spl20_44
| spl20_30 ),
inference(avatar_split_clause,[],[f620,f237,f462,f231]) ).
tff(f625,plain,
( $false
| spl20_23
| spl20_24
| spl20_25
| ~ spl20_26 ),
inference(forward_subsumption_resolution,[],[f533,f347]) ).
tff(f626,plain,
( spl20_23
| spl20_24
| spl20_25
| ~ spl20_26 ),
inference(avatar_contradiction_clause,[],[f625]) ).
tff(f628,definition,
( spl20_46
<=> f4($false) ),
introduced(definition,[new_symbols(definition,[spl20_46])],[avatar_definition]) ).
tff(f644,plain,
( spl20_4
| ~ spl20_46
| spl20_5 ),
inference(avatar_split_clause,[],[f298,f111,f628,f105]) ).
tff(f646,plain,
( ~ f4($true)
| ~ spl20_4
| spl20_5 ),
inference(superposition,[],[f113,f107]) ).
tff(f654,plain,
( f4($true)
| ~ spl20_25
| ~ spl20_26 ),
inference(superposition,[],[f218,f213]) ).
tff(f656,plain,
( $false
| ~ spl20_4
| spl20_5
| ~ spl20_25
| ~ spl20_26 ),
inference(forward_subsumption_resolution,[],[f654,f646]) ).
tff(f657,plain,
( ~ spl20_4
| spl20_5
| ~ spl20_25
| ~ spl20_26 ),
inference(avatar_contradiction_clause,[],[f656]) ).
tff(f658,plain,
( f4($true)
| ~ spl20_21
| ~ spl20_22 ),
inference(forward_demodulation,[],[f198,f193]) ).
tff(f659,plain,
( $false
| ~ spl20_4
| spl20_5
| ~ spl20_21
| ~ spl20_22 ),
inference(forward_subsumption_resolution,[],[f658,f646]) ).
tff(f660,plain,
( ~ spl20_4
| spl20_5
| ~ spl20_21
| ~ spl20_22 ),
inference(avatar_contradiction_clause,[],[f659]) ).
tff(f661,plain,
( f4($true)
| ~ spl20_4
| ~ spl20_5 ),
inference(forward_demodulation,[],[f112,f107]) ).
tff(f666,plain,
( f3($true)
| ~ spl20_6
| ~ spl20_7 ),
inference(superposition,[],[f122,f117]) ).
tff(f668,plain,
( $false
| ~ spl20_6
| ~ spl20_7
| ~ spl20_27
| spl20_28 ),
inference(forward_subsumption_resolution,[],[f666,f614]) ).
tff(f669,plain,
( ~ spl20_6
| ~ spl20_7
| ~ spl20_27
| spl20_28 ),
inference(avatar_contradiction_clause,[],[f668]) ).
tff(f670,plain,
( ~ f3($true)
| ~ spl20_6
| spl20_7 ),
inference(forward_demodulation,[],[f123,f117]) ).
tff(f679,plain,
( ~ f3($false)
| ( $true = bG2 )
| spl20_9 ),
inference(superposition,[],[f133,f89]) ).
tff(f680,plain,
( spl20_8
| ~ spl20_45
| spl20_9 ),
inference(avatar_split_clause,[],[f679,f131,f480,f125]) ).
tff(f681,plain,
( ~ f3($false)
| ( $true = bG3 )
| spl20_11 ),
inference(superposition,[],[f143,f89]) ).
tff(f683,plain,
( f2($false)
| ( $true = bG4 )
| ~ spl20_13 ),
inference(superposition,[],[f152,f89]) ).
tff(f684,plain,
( spl20_12
| spl20_44
| ~ spl20_13 ),
inference(avatar_split_clause,[],[f683,f151,f462,f145]) ).
tff(f685,plain,
( f1($false)
| ( $true = bG6 )
| ~ spl20_17 ),
inference(superposition,[],[f172,f89]) ).
tff(f688,plain,
( spl20_16
| spl20_42
| ~ spl20_17 ),
inference(avatar_split_clause,[],[f685,f171,f395,f165]) ).
tff(f689,plain,
( f2($false)
| ( $true = bG13 )
| ~ spl20_30 ),
inference(superposition,[],[f238,f89]) ).
tff(f690,plain,
( f2($false)
| spl20_29
| ~ spl20_30 ),
inference(forward_subsumption_resolution,[],[f689,f232]) ).
tff(f691,plain,
( spl20_44
| spl20_29
| ~ spl20_30 ),
inference(avatar_split_clause,[],[f690,f237,f231,f462]) ).
tff(f692,plain,
( f2($false)
| ( $true = bG15 )
| ~ spl20_34 ),
inference(superposition,[],[f258,f89]) ).
tff(f693,plain,
( spl20_33
| spl20_44
| ~ spl20_34 ),
inference(avatar_split_clause,[],[f692,f257,f462,f251]) ).
tff(f696,plain,
( $false
| ~ spl20_18
| ~ spl20_19
| ~ spl20_35
| spl20_36 ),
inference(forward_subsumption_resolution,[],[f600,f555]) ).
tff(f697,plain,
( ~ spl20_18
| ~ spl20_19
| ~ spl20_35
| spl20_36 ),
inference(avatar_contradiction_clause,[],[f696]) ).
tff(f699,plain,
( ~ f1($true)
| ~ spl20_18
| spl20_19 ),
inference(forward_demodulation,[],[f183,f177]) ).
tff(f702,plain,
( ~ f0($false)
| ( $true = bG8 )
| spl20_1 ),
inference(superposition,[],[f92,f89]) ).
tff(f703,plain,
( spl20_20
| ~ spl20_43
| spl20_1 ),
inference(avatar_split_clause,[],[f702,f91,f411,f185]) ).
tff(f706,plain,
( f0($false)
| ( $true = bG17 )
| ~ spl20_38 ),
inference(superposition,[],[f278,f89]) ).
tff(f707,plain,
( spl20_37
| spl20_43
| ~ spl20_38 ),
inference(avatar_split_clause,[],[f706,f277,f411,f271]) ).
tff(f708,plain,
( ! [X0: $o] :
( ~ f0((X0))
| ( $true = (X0) ) )
| spl20_43 ),
inference(superposition,[],[f412,f89]) ).
tff(f711,plain,
( ( $true = bG19 )
| ~ spl20_2
| spl20_43 ),
inference(resolution,[],[f708,f97]) ).
tff(f714,plain,
( spl20_41
| ~ spl20_2
| spl20_43 ),
inference(avatar_split_clause,[],[f711,f411,f95,f291]) ).
tff(f717,plain,
( f2($false)
| ( $true = bG14 )
| ~ spl20_32 ),
inference(superposition,[],[f248,f89]) ).
tff(f718,plain,
( spl20_31
| spl20_44
| ~ spl20_32 ),
inference(avatar_split_clause,[],[f717,f247,f462,f241]) ).
tff(f722,plain,
( ~ f2($false)
| ( $true = bG15 )
| spl20_34 ),
inference(superposition,[],[f259,f89]) ).
tff(f723,plain,
( spl20_33
| ~ spl20_44
| spl20_34 ),
inference(avatar_split_clause,[],[f722,f257,f462,f251]) ).
tff(f725,plain,
( f0($true)
| ~ spl20_2
| ~ spl20_41 ),
inference(superposition,[],[f97,f293]) ).
tff(f727,plain,
( f1($false)
| ( $true = bG16 )
| ~ spl20_36 ),
inference(superposition,[],[f268,f89]) ).
tff(f728,plain,
( spl20_35
| spl20_42
| ~ spl20_36 ),
inference(avatar_split_clause,[],[f727,f267,f395,f261]) ).
tff(f729,plain,
( $false
| ~ spl20_16
| ~ spl20_17
| ~ spl20_18
| spl20_19 ),
inference(forward_subsumption_resolution,[],[f546,f699]) ).
tff(f730,plain,
( ~ spl20_16
| ~ spl20_17
| ~ spl20_18
| spl20_19 ),
inference(avatar_contradiction_clause,[],[f729]) ).
tff(f734,plain,
( ~ f4($true)
| ~ spl20_23
| spl20_24 ),
inference(superposition,[],[f209,f203]) ).
tff(f736,plain,
( $false
| ~ spl20_21
| ~ spl20_22
| ~ spl20_23
| spl20_24 ),
inference(forward_subsumption_resolution,[],[f734,f658]) ).
tff(f737,plain,
( ~ spl20_21
| ~ spl20_22
| ~ spl20_23
| spl20_24 ),
inference(avatar_contradiction_clause,[],[f736]) ).
tff(f738,plain,
( f4($true)
| ~ spl20_23
| ~ spl20_24 ),
inference(forward_demodulation,[],[f208,f203]) ).
tff(f745,plain,
( f2($true)
| ~ spl20_31
| ~ spl20_32 ),
inference(superposition,[],[f248,f243]) ).
tff(f747,plain,
( $false
| ~ spl20_31
| ~ spl20_32
| ~ spl20_33
| spl20_34 ),
inference(forward_subsumption_resolution,[],[f745,f582]) ).
tff(f748,plain,
( ~ spl20_31
| ~ spl20_32
| ~ spl20_33
| spl20_34 ),
inference(avatar_contradiction_clause,[],[f747]) ).
tff(f749,plain,
( f3($true)
| ~ spl20_27
| ~ spl20_28 ),
inference(forward_demodulation,[],[f228,f223]) ).
tff(f752,plain,
( $false
| ~ spl20_6
| spl20_7
| ~ spl20_27
| ~ spl20_28 ),
inference(forward_subsumption_resolution,[],[f749,f670]) ).
tff(f753,plain,
( ~ spl20_6
| spl20_7
| ~ spl20_27
| ~ spl20_28 ),
inference(avatar_contradiction_clause,[],[f752]) ).
tff(f755,plain,
( $false
| ~ spl20_8
| spl20_9
| ~ spl20_27
| ~ spl20_28 ),
inference(forward_subsumption_resolution,[],[f749,f619]) ).
tff(f756,plain,
( ~ spl20_8
| spl20_9
| ~ spl20_27
| ~ spl20_28 ),
inference(avatar_contradiction_clause,[],[f755]) ).
tff(f757,plain,
( spl20_10
| ~ spl20_45
| spl20_11 ),
inference(avatar_split_clause,[],[f681,f141,f480,f135]) ).
tff(f758,plain,
( f3($false)
| ( $true = bG2 )
| ~ spl20_9 ),
inference(superposition,[],[f132,f89]) ).
tff(f759,plain,
( spl20_8
| spl20_45
| ~ spl20_9 ),
inference(avatar_split_clause,[],[f758,f131,f480,f125]) ).
tff(f764,plain,
( ~ f3($true)
| ~ spl20_10
| spl20_11 ),
inference(superposition,[],[f143,f137]) ).
tff(f766,plain,
( $false
| ~ spl20_10
| spl20_11
| ~ spl20_27
| ~ spl20_28 ),
inference(forward_subsumption_resolution,[],[f764,f749]) ).
tff(f767,plain,
( ~ spl20_10
| spl20_11
| ~ spl20_27
| ~ spl20_28 ),
inference(avatar_contradiction_clause,[],[f766]) ).
tff(f768,plain,
( ~ f4($true)
| ~ spl20_25
| spl20_26 ),
inference(forward_demodulation,[],[f219,f213]) ).
tff(f771,plain,
( ~ f4($true)
| ~ spl20_21
| spl20_22 ),
inference(forward_demodulation,[],[f199,f193]) ).
tff(f773,plain,
( f3($false)
| ( $true = bG12 )
| ~ spl20_28 ),
inference(superposition,[],[f228,f89]) ).
tff(f774,plain,
( spl20_27
| spl20_45
| ~ spl20_28 ),
inference(avatar_split_clause,[],[f773,f227,f480,f221]) ).
tff(f775,plain,
( $false
| ~ spl20_4
| ~ spl20_5
| ~ spl20_25
| spl20_26 ),
inference(forward_subsumption_resolution,[],[f768,f661]) ).
tff(f776,plain,
( ~ spl20_4
| ~ spl20_5
| ~ spl20_25
| spl20_26 ),
inference(avatar_contradiction_clause,[],[f775]) ).
tff(f779,plain,
( f4($false)
| ( bG0 = $true )
| ~ spl20_5 ),
inference(superposition,[],[f112,f89]) ).
tff(f782,plain,
( ~ f4($false)
| ( $true = bG11 )
| spl20_26 ),
inference(superposition,[],[f219,f89]) ).
tff(f785,plain,
( $false
| ~ spl20_23
| ~ spl20_24
| ~ spl20_25
| spl20_26 ),
inference(forward_subsumption_resolution,[],[f768,f738]) ).
tff(f786,plain,
( ~ spl20_23
| ~ spl20_24
| ~ spl20_25
| spl20_26 ),
inference(avatar_contradiction_clause,[],[f785]) ).
tff(f788,plain,
( spl20_4
| spl20_46
| ~ spl20_5 ),
inference(avatar_split_clause,[],[f779,f111,f628,f105]) ).
tff(f789,plain,
( spl20_25
| ~ spl20_46
| spl20_26 ),
inference(avatar_split_clause,[],[f782,f217,f628,f211]) ).
tff(f790,plain,
( ~ f4($false)
| ( $true = bG9 )
| spl20_22 ),
inference(superposition,[],[f199,f89]) ).
tff(f791,plain,
( spl20_21
| ~ spl20_46
| spl20_22 ),
inference(avatar_split_clause,[],[f790,f197,f628,f191]) ).
tff(f794,plain,
( $false
| ~ spl20_4
| ~ spl20_5
| ~ spl20_21
| spl20_22 ),
inference(forward_subsumption_resolution,[],[f771,f661]) ).
tff(f795,plain,
( ~ spl20_4
| ~ spl20_5
| ~ spl20_21
| spl20_22 ),
inference(avatar_contradiction_clause,[],[f794]) ).
tff(f807,plain,
( f4($false)
| ( $true = bG9 )
| ~ spl20_22 ),
inference(superposition,[],[f198,f89]) ).
tff(f808,plain,
( spl20_21
| spl20_46
| ~ spl20_22 ),
inference(avatar_split_clause,[],[f807,f197,f628,f191]) ).
tff(f810,plain,
( f4($false)
| ( $true = bG10 )
| ~ spl20_24 ),
inference(superposition,[],[f208,f89]) ).
tff(f811,plain,
( spl20_23
| spl20_46
| ~ spl20_24 ),
inference(avatar_split_clause,[],[f810,f207,f628,f201]) ).
tff(f812,plain,
( f4($false)
| ( $true = bG11 )
| ~ spl20_26 ),
inference(superposition,[],[f218,f89]) ).
tff(f813,plain,
( spl20_25
| spl20_46
| ~ spl20_26 ),
inference(avatar_split_clause,[],[f812,f217,f628,f211]) ).
tff(f814,plain,
( ~ f3($false)
| ( $true = bG12 )
| spl20_28 ),
inference(superposition,[],[f229,f89]) ).
tff(f815,plain,
( spl20_27
| ~ spl20_45
| spl20_28 ),
inference(avatar_split_clause,[],[f814,f227,f480,f221]) ).
tff(f850,plain,
( f0($true)
| ~ spl20_37
| ~ spl20_38 ),
inference(superposition,[],[f278,f273]) ).
tff(f852,plain,
( $false
| spl20_1
| ~ spl20_20
| ~ spl20_37
| ~ spl20_38 ),
inference(forward_subsumption_resolution,[],[f850,f377]) ).
tff(f853,plain,
( spl20_1
| ~ spl20_20
| ~ spl20_37
| ~ spl20_38 ),
inference(avatar_contradiction_clause,[],[f852]) ).
tff(f855,plain,
( $false
| spl20_1
| ~ spl20_2
| ~ spl20_20
| ~ spl20_41 ),
inference(forward_subsumption_resolution,[],[f725,f377]) ).
tff(f856,plain,
( spl20_1
| ~ spl20_2
| ~ spl20_20
| ~ spl20_41 ),
inference(avatar_contradiction_clause,[],[f855]) ).
tff(f874,plain,
( ~ f1($false)
| ( $true = bG16 )
| spl20_36 ),
inference(superposition,[],[f269,f89]) ).
tff(f875,plain,
( spl20_35
| ~ spl20_42
| spl20_36 ),
inference(avatar_split_clause,[],[f874,f267,f395,f261]) ).
tff(f883,plain,
( $false
| ~ spl20_8
| ~ spl20_9
| ~ spl20_10
| spl20_11 ),
inference(forward_subsumption_resolution,[],[f764,f514]) ).
tff(f884,plain,
( ~ spl20_8
| ~ spl20_9
| ~ spl20_10
| spl20_11 ),
inference(avatar_contradiction_clause,[],[f883]) ).
cnf(s1,plain,
( spl20_1
| spl20_2 ),
inference(sat_conversion,[],[f98]) ).
cnf(s2,plain,
( ~ spl20_1
| ~ spl20_2 ),
inference(sat_conversion,[],[f99]) ).
cnf(s3,plain,
( ~ spl20_3
| spl20_4 ),
inference(sat_conversion,[],[f108]) ).
cnf(s4,plain,
( spl20_3
| ~ spl20_4 ),
inference(sat_conversion,[],[f109]) ).
cnf(s5,plain,
( ~ spl20_5
| spl20_6 ),
inference(sat_conversion,[],[f118]) ).
cnf(s6,plain,
( spl20_5
| ~ spl20_6 ),
inference(sat_conversion,[],[f119]) ).
cnf(s7,plain,
( ~ spl20_7
| spl20_8 ),
inference(sat_conversion,[],[f128]) ).
cnf(s8,plain,
( spl20_7
| ~ spl20_8 ),
inference(sat_conversion,[],[f129]) ).
cnf(s9,plain,
( ~ spl20_9
| spl20_10 ),
inference(sat_conversion,[],[f138]) ).
cnf(s10,plain,
( spl20_9
| ~ spl20_10 ),
inference(sat_conversion,[],[f139]) ).
cnf(s11,plain,
( ~ spl20_11
| spl20_12 ),
inference(sat_conversion,[],[f148]) ).
cnf(s12,plain,
( spl20_11
| ~ spl20_12 ),
inference(sat_conversion,[],[f149]) ).
cnf(s13,plain,
( ~ spl20_13
| spl20_14 ),
inference(sat_conversion,[],[f158]) ).
cnf(s14,plain,
( spl20_13
| ~ spl20_14 ),
inference(sat_conversion,[],[f159]) ).
cnf(s15,plain,
( ~ spl20_15
| spl20_16 ),
inference(sat_conversion,[],[f168]) ).
cnf(s16,plain,
( spl20_15
| ~ spl20_16 ),
inference(sat_conversion,[],[f169]) ).
cnf(s17,plain,
( ~ spl20_17
| spl20_18 ),
inference(sat_conversion,[],[f178]) ).
cnf(s18,plain,
( spl20_17
| ~ spl20_18 ),
inference(sat_conversion,[],[f179]) ).
cnf(s19,plain,
( ~ spl20_19
| spl20_20 ),
inference(sat_conversion,[],[f188]) ).
cnf(s20,plain,
( spl20_19
| ~ spl20_20 ),
inference(sat_conversion,[],[f189]) ).
cnf(s21,plain,
( ~ spl20_3
| spl20_21 ),
inference(sat_conversion,[],[f194]) ).
cnf(s22,plain,
( spl20_3
| ~ spl20_21 ),
inference(sat_conversion,[],[f195]) ).
cnf(s23,plain,
( ~ spl20_22
| spl20_23 ),
inference(sat_conversion,[],[f204]) ).
cnf(s24,plain,
( spl20_22
| ~ spl20_23 ),
inference(sat_conversion,[],[f205]) ).
cnf(s25,plain,
( ~ spl20_24
| spl20_25 ),
inference(sat_conversion,[],[f214]) ).
cnf(s26,plain,
( spl20_24
| ~ spl20_25 ),
inference(sat_conversion,[],[f215]) ).
cnf(s27,plain,
( ~ spl20_26
| spl20_27 ),
inference(sat_conversion,[],[f224]) ).
cnf(s28,plain,
( spl20_26
| ~ spl20_27 ),
inference(sat_conversion,[],[f225]) ).
cnf(s29,plain,
( ~ spl20_28
| spl20_29 ),
inference(sat_conversion,[],[f234]) ).
cnf(s30,plain,
( spl20_28
| ~ spl20_29 ),
inference(sat_conversion,[],[f235]) ).
cnf(s31,plain,
( ~ spl20_30
| spl20_31 ),
inference(sat_conversion,[],[f244]) ).
cnf(s32,plain,
( spl20_30
| ~ spl20_31 ),
inference(sat_conversion,[],[f245]) ).
cnf(s33,plain,
( ~ spl20_32
| spl20_33 ),
inference(sat_conversion,[],[f254]) ).
cnf(s34,plain,
( spl20_32
| ~ spl20_33 ),
inference(sat_conversion,[],[f255]) ).
cnf(s35,plain,
( ~ spl20_34
| spl20_35 ),
inference(sat_conversion,[],[f264]) ).
cnf(s36,plain,
( spl20_34
| ~ spl20_35 ),
inference(sat_conversion,[],[f265]) ).
cnf(s37,plain,
( ~ spl20_36
| spl20_37 ),
inference(sat_conversion,[],[f274]) ).
cnf(s38,plain,
( spl20_36
| ~ spl20_37 ),
inference(sat_conversion,[],[f275]) ).
cnf(s39,plain,
( ~ spl20_38
| spl20_39 ),
inference(sat_conversion,[],[f284]) ).
cnf(s40,plain,
( spl20_38
| ~ spl20_39 ),
inference(sat_conversion,[],[f285]) ).
cnf(s41,plain,
( ~ spl20_40
| spl20_41 ),
inference(sat_conversion,[],[f294]) ).
cnf(s42,plain,
( spl20_40
| ~ spl20_41 ),
inference(sat_conversion,[],[f295]) ).
cnf(s44,plain,
( spl20_1
| ~ spl20_2
| spl20_20
| spl20_41 ),
inference(sat_conversion,[],[f362]) ).
cnf(s51,plain,
( spl20_18
| ~ spl20_19
| spl20_35
| spl20_36 ),
inference(sat_conversion,[],[f389]) ).
cnf(s52,plain,
( spl20_16
| ~ spl20_17
| spl20_35
| spl20_36 ),
inference(sat_conversion,[],[f393]) ).
cnf(s56,plain,
( spl20_14
| spl20_15
| ~ spl20_42 ),
inference(sat_conversion,[],[f401]) ).
cnf(s57,plain,
( spl20_16
| spl20_17
| ~ spl20_42 ),
inference(sat_conversion,[],[f406]) ).
cnf(s61,plain,
( spl20_2
| spl20_41
| ~ spl20_43 ),
inference(sat_conversion,[],[f419]) ).
cnf(s62,plain,
( spl20_18
| spl20_19
| ~ spl20_42 ),
inference(sat_conversion,[],[f422]) ).
cnf(s64,plain,
( spl20_2
| ~ spl20_39
| ~ spl20_40
| ~ spl20_41 ),
inference(sat_conversion,[],[f432]) ).
cnf(s69,plain,
( ~ spl20_14
| spl20_15
| ~ spl20_35
| ~ spl20_36 ),
inference(sat_conversion,[],[f452]) ).
cnf(s72,plain,
( spl20_31
| spl20_32
| spl20_33
| ~ spl20_34 ),
inference(sat_conversion,[],[f460]) ).
cnf(s77,plain,
( spl20_12
| spl20_13
| ~ spl20_44 ),
inference(sat_conversion,[],[f469]) ).
cnf(s79,plain,
( spl20_10
| ~ spl20_11
| spl20_27
| spl20_28 ),
inference(sat_conversion,[],[f474]) ).
cnf(s81,plain,
( spl20_10
| ~ spl20_11
| spl20_45 ),
inference(sat_conversion,[],[f483]) ).
cnf(s85,plain,
( ~ spl20_12
| spl20_13
| ~ spl20_29
| ~ spl20_30 ),
inference(sat_conversion,[],[f501]) ).
cnf(s88,plain,
( spl20_6
| spl20_7
| ~ spl20_45 ),
inference(sat_conversion,[],[f507]) ).
cnf(s90,plain,
( spl20_6
| ~ spl20_7
| spl20_45 ),
inference(sat_conversion,[],[f511]) ).
cnf(s91,plain,
( ~ spl20_12
| spl20_13
| ~ spl20_33
| ~ spl20_34 ),
inference(sat_conversion,[],[f521]) ).
cnf(s92,plain,
( spl20_14
| ~ spl20_15
| spl20_42 ),
inference(sat_conversion,[],[f525]) ).
cnf(s93,plain,
( ~ spl20_12
| ~ spl20_13
| ~ spl20_29
| spl20_30 ),
inference(sat_conversion,[],[f527]) ).
cnf(s98,plain,
( ~ spl20_18
| spl20_19
| ~ spl20_35
| ~ spl20_36 ),
inference(sat_conversion,[],[f552]) ).
cnf(s101,plain,
( spl20_37
| spl20_38
| ~ spl20_43 ),
inference(sat_conversion,[],[f556]) ).
cnf(s102,plain,
( spl20_39
| ~ spl20_40
| spl20_43 ),
inference(sat_conversion,[],[f558]) ).
cnf(s103,plain,
( spl20_39
| spl20_40
| ~ spl20_43 ),
inference(sat_conversion,[],[f559]) ).
cnf(s105,plain,
( spl20_18
| ~ spl20_19
| spl20_42 ),
inference(sat_conversion,[],[f562]) ).
cnf(s106,plain,
( ~ spl20_1
| spl20_20
| spl20_43 ),
inference(sat_conversion,[],[f564]) ).
cnf(s107,plain,
( ~ spl20_14
| ~ spl20_15
| ~ spl20_16
| spl20_17 ),
inference(sat_conversion,[],[f573]) ).
cnf(s109,plain,
( ~ spl20_1
| ~ spl20_20
| ~ spl20_37
| spl20_38 ),
inference(sat_conversion,[],[f579]) ).
cnf(s110,plain,
( ~ spl20_1
| ~ spl20_20
| ~ spl20_39
| spl20_40 ),
inference(sat_conversion,[],[f581]) ).
cnf(s113,plain,
( ~ spl20_12
| ~ spl20_13
| ~ spl20_33
| spl20_34 ),
inference(sat_conversion,[],[f585]) ).
cnf(s120,plain,
( ~ spl20_12
| ~ spl20_13
| ~ spl20_31
| spl20_32 ),
inference(sat_conversion,[],[f613]) ).
cnf(s123,plain,
( ~ spl20_10
| ~ spl20_11
| ~ spl20_27
| spl20_28 ),
inference(sat_conversion,[],[f618]) ).
cnf(s124,plain,
( spl20_29
| spl20_30
| ~ spl20_44 ),
inference(sat_conversion,[],[f621]) ).
cnf(s125,plain,
( spl20_23
| spl20_24
| spl20_25
| ~ spl20_26 ),
inference(sat_conversion,[],[f626]) ).
cnf(s135,plain,
( spl20_4
| spl20_5
| ~ spl20_46 ),
inference(sat_conversion,[],[f644]) ).
cnf(s136,plain,
( ~ spl20_4
| spl20_5
| ~ spl20_25
| ~ spl20_26 ),
inference(sat_conversion,[],[f657]) ).
cnf(s137,plain,
( ~ spl20_4
| spl20_5
| ~ spl20_21
| ~ spl20_22 ),
inference(sat_conversion,[],[f660]) ).
cnf(s139,plain,
( ~ spl20_6
| ~ spl20_7
| ~ spl20_27
| spl20_28 ),
inference(sat_conversion,[],[f669]) ).
cnf(s146,plain,
( spl20_8
| spl20_9
| ~ spl20_45 ),
inference(sat_conversion,[],[f680]) ).
cnf(s148,plain,
( spl20_12
| ~ spl20_13
| spl20_44 ),
inference(sat_conversion,[],[f684]) ).
cnf(s150,plain,
( spl20_16
| ~ spl20_17
| spl20_42 ),
inference(sat_conversion,[],[f688]) ).
cnf(s151,plain,
( spl20_29
| ~ spl20_30
| spl20_44 ),
inference(sat_conversion,[],[f691]) ).
cnf(s152,plain,
( spl20_33
| ~ spl20_34
| spl20_44 ),
inference(sat_conversion,[],[f693]) ).
cnf(s153,plain,
( ~ spl20_18
| ~ spl20_19
| ~ spl20_35
| spl20_36 ),
inference(sat_conversion,[],[f697]) ).
cnf(s156,plain,
( spl20_1
| spl20_20
| ~ spl20_43 ),
inference(sat_conversion,[],[f703]) ).
cnf(s158,plain,
( spl20_37
| ~ spl20_38
| spl20_43 ),
inference(sat_conversion,[],[f707]) ).
cnf(s162,plain,
( ~ spl20_2
| spl20_41
| spl20_43 ),
inference(sat_conversion,[],[f714]) ).
cnf(s163,plain,
( spl20_31
| ~ spl20_32
| spl20_44 ),
inference(sat_conversion,[],[f718]) ).
cnf(s164,plain,
( spl20_33
| spl20_34
| ~ spl20_44 ),
inference(sat_conversion,[],[f723]) ).
cnf(s165,plain,
( spl20_35
| ~ spl20_36
| spl20_42 ),
inference(sat_conversion,[],[f728]) ).
cnf(s166,plain,
( ~ spl20_16
| ~ spl20_17
| ~ spl20_18
| spl20_19 ),
inference(sat_conversion,[],[f730]) ).
cnf(s167,plain,
( ~ spl20_21
| ~ spl20_22
| ~ spl20_23
| spl20_24 ),
inference(sat_conversion,[],[f737]) ).
cnf(s168,plain,
( ~ spl20_31
| ~ spl20_32
| ~ spl20_33
| spl20_34 ),
inference(sat_conversion,[],[f748]) ).
cnf(s170,plain,
( ~ spl20_6
| spl20_7
| ~ spl20_27
| ~ spl20_28 ),
inference(sat_conversion,[],[f753]) ).
cnf(s171,plain,
( ~ spl20_8
| spl20_9
| ~ spl20_27
| ~ spl20_28 ),
inference(sat_conversion,[],[f756]) ).
cnf(s172,plain,
( spl20_10
| spl20_11
| ~ spl20_45 ),
inference(sat_conversion,[],[f757]) ).
cnf(s173,plain,
( spl20_8
| ~ spl20_9
| spl20_45 ),
inference(sat_conversion,[],[f759]) ).
cnf(s174,plain,
( ~ spl20_10
| spl20_11
| ~ spl20_27
| ~ spl20_28 ),
inference(sat_conversion,[],[f767]) ).
cnf(s177,plain,
( spl20_27
| ~ spl20_28
| spl20_45 ),
inference(sat_conversion,[],[f774]) ).
cnf(s178,plain,
( ~ spl20_4
| ~ spl20_5
| ~ spl20_25
| spl20_26 ),
inference(sat_conversion,[],[f776]) ).
cnf(s181,plain,
( ~ spl20_23
| ~ spl20_24
| ~ spl20_25
| spl20_26 ),
inference(sat_conversion,[],[f786]) ).
cnf(s187,plain,
( spl20_4
| ~ spl20_5
| spl20_46 ),
inference(sat_conversion,[],[f788]) ).
cnf(s188,plain,
( spl20_25
| spl20_26
| ~ spl20_46 ),
inference(sat_conversion,[],[f789]) ).
cnf(s189,plain,
( spl20_21
| spl20_22
| ~ spl20_46 ),
inference(sat_conversion,[],[f791]) ).
cnf(s191,plain,
( ~ spl20_4
| ~ spl20_5
| ~ spl20_21
| spl20_22 ),
inference(sat_conversion,[],[f795]) ).
cnf(s197,plain,
( spl20_21
| ~ spl20_22
| spl20_46 ),
inference(sat_conversion,[],[f808]) ).
cnf(s198,plain,
( spl20_23
| ~ spl20_24
| spl20_46 ),
inference(sat_conversion,[],[f811]) ).
cnf(s199,plain,
( spl20_25
| ~ spl20_26
| spl20_46 ),
inference(sat_conversion,[],[f813]) ).
cnf(s200,plain,
( spl20_27
| spl20_28
| ~ spl20_45 ),
inference(sat_conversion,[],[f815]) ).
cnf(s201,plain,
( spl20_1
| ~ spl20_20
| ~ spl20_37
| ~ spl20_38 ),
inference(sat_conversion,[],[f853]) ).
cnf(s202,plain,
( spl20_1
| ~ spl20_2
| ~ spl20_20
| ~ spl20_41 ),
inference(sat_conversion,[],[f856]) ).
cnf(s209,plain,
( spl20_35
| spl20_36
| ~ spl20_42 ),
inference(sat_conversion,[],[f875]) ).
cnf(s210,plain,
( ~ spl20_8
| ~ spl20_9
| ~ spl20_10
| spl20_11 ),
inference(sat_conversion,[],[f884]) ).
cnf(s211,plain,
( spl20_15
| spl20_35
| spl20_14
| spl20_1 ),
inference(rat,[],[s102,s40,s42,s158,s44,s156,s20,s105,s18,s38,s150,s165,s16,s56,s1]) ).
cnf(s212,plain,
( ~ spl20_20
| ~ spl20_37
| spl20_1 ),
inference(rat,[],[s103,s41,s162,s40,s202,s201,s1]) ).
cnf(s213,plain,
( spl20_35
| spl20_14
| spl20_1 ),
inference(rat,[],[s166,s18,s62,s19,s212,s37,s209,s15,s92,s211]) ).
cnf(s214,plain,
( spl20_13
| spl20_12
| spl20_29
| spl20_1 ),
inference(rat,[],[s213,s36,s152,s34,s163,s32,s151,s14,s77]) ).
cnf(s215,plain,
( spl20_34
| ~ spl20_31
| ~ spl20_44 ),
inference(rat,[],[s168,s34,s164]) ).
cnf(s216,plain,
( ~ spl20_16
| spl20_17
| ~ spl20_14 ),
inference(rat,[],[s107,s16]) ).
cnf(s217,plain,
( spl20_18
| ~ spl20_35
| ~ spl20_14
| spl20_1 ),
inference(rat,[],[s102,s40,s42,s158,s44,s156,s38,s20,s69,s105,s15,s57,s216,s17,s1]) ).
cnf(s218,plain,
( ~ spl20_19
| ~ spl20_18
| ~ spl20_35
| spl20_1 ),
inference(rat,[],[s37,s212,s153,s19]) ).
cnf(s219,plain,
( spl20_7
| spl20_27
| spl20_6
| spl20_1 ),
inference(rat,[],[s102,s40,s42,s158,s38,s44,s156,s98,s20,s218,s217,s35,s215,s31,s124,s13,s148,s214,s12,s79,s10,s30,s173,s177,s8,s88,s1]) ).
cnf(s221,plain,
( ~ spl20_12
| ~ spl20_13
| spl20_34
| ~ spl20_29 ),
inference(rat,[],[s120,s31,s33,s93,s113]) ).
cnf(s222,plain,
( spl20_11
| ~ spl20_8
| ~ spl20_45 ),
inference(rat,[],[s210,s10,s172]) ).
cnf(s223,plain,
( spl20_35
| ~ spl20_12
| ~ spl20_29
| spl20_1 ),
inference(rat,[],[s14,s221,s213,s35]) ).
cnf(s224,plain,
( spl20_13
| ~ spl20_34
| ~ spl20_12
| ~ spl20_29 ),
inference(rat,[],[s32,s72,s33,s85,s91]) ).
cnf(s225,plain,
( spl20_5
| spl20_3
| spl20_1 ),
inference(rat,[],[s102,s40,s42,s158,s38,s44,s156,s98,s20,s218,s217,s13,s224,s36,s223,s11,s222,s29,s200,s7,s90,s219,s28,s199,s26,s198,s24,s197,s6,s135,s1,s22,s4]) ).
cnf(s226,plain,
( spl20_26
| ~ spl20_23
| ~ spl20_46 ),
inference(rat,[],[s181,s26,s188]) ).
cnf(s227,plain,
( spl20_12
| ~ spl20_13
| spl20_34
| ~ spl20_27
| ~ spl20_6 ),
inference(rat,[],[s171,s9,s7,s174,s170,s30,s124,s31,s215,s148,s11]) ).
cnf(s228,plain,
( spl20_35
| spl20_3
| spl20_1 ),
inference(rat,[],[s146,s81,s9,s8,s123,s139,s29,s223,s12,s227,s14,s213,s35,s5,s27,s226,s23,s189,s22,s187,s225,s4]) ).
cnf(s229,plain,
( spl20_12
| spl20_13
| spl20_3
| spl20_1 ),
inference(rat,[],[s171,s9,s7,s174,s170,s30,s214,s11,s5,s27,s226,s23,s189,s22,s187,s225,s4]) ).
cnf(s230,plain,
( spl20_13
| spl20_3
| spl20_1 ),
inference(rat,[],[s146,s81,s9,s8,s123,s139,s29,s224,s12,s229,s5,s27,s226,s23,s189,s22,s187,s225,s4,s36,s228]) ).
cnf(s231,plain,
( spl20_3
| spl20_1 ),
inference(rat,[],[s102,s40,s42,s158,s38,s44,s156,s98,s20,s218,s217,s13,s230,s228,s1]) ).
cnf(s232,plain,
( spl20_27
| ~ spl20_28
| spl20_11
| ~ spl20_3 ),
inference(rat,[],[s167,s25,s23,s178,s191,s6,s88,s7,s222,s177,s27,s21,s3]) ).
cnf(s233,plain,
( spl20_12
| spl20_13
| spl20_1 ),
inference(rat,[],[s125,s25,s24,s136,s137,s5,s170,s7,s171,s9,s174,s28,s232,s30,s214,s11,s21,s3,s231]) ).
cnf(s234,plain,
( spl20_27
| spl20_28
| ~ spl20_11
| ~ spl20_3 ),
inference(rat,[],[s167,s25,s23,s178,s191,s6,s90,s8,s173,s10,s79,s200,s27,s21,s3]) ).
cnf(s235,plain,
( spl20_13
| spl20_1 ),
inference(rat,[],[s125,s25,s24,s136,s137,s5,s139,s8,s146,s81,s9,s123,s28,s234,s29,s224,s12,s233,s36,s213,s14,s21,s3,s231]) ).
cnf(s236,plain,
( ~ spl20_35
| spl20_1 ),
inference(rat,[],[s102,s40,s42,s158,s38,s44,s156,s98,s20,s218,s217,s1,s13,s235]) ).
cnf(s237,plain,
( spl20_12
| spl20_1 ),
inference(rat,[],[s125,s25,s24,s136,s137,s5,s227,s28,s232,s30,s124,s31,s215,s148,s11,s21,s3,s231,s235,s35,s236]) ).
cnf(s238,plain,
spl20_1,
inference(rat,[],[s125,s25,s24,s136,s137,s5,s139,s8,s146,s81,s9,s123,s28,s234,s29,s223,s12,s237,s236,s3,s21,s231]) ).
cnf(s239,plain,
~ spl20_2,
inference(rat,[],[s2,s238]) ).
cnf(s240,plain,
( ~ spl20_39
| ~ spl20_20 ),
inference(rat,[],[s64,s41,s110,s238,s239]) ).
cnf(s241,plain,
( ~ spl20_20
| ~ spl20_37 ),
inference(rat,[],[s240,s39,s109,s238]) ).
cnf(s242,plain,
( ~ spl20_19
| spl20_18
| spl20_35 ),
inference(rat,[],[s241,s37,s19,s51]) ).
cnf(s243,plain,
( spl20_18
| spl20_35 ),
inference(rat,[],[s64,s39,s42,s101,s61,s38,s106,s165,s20,s62,s242,s238,s239]) ).
cnf(s244,plain,
( spl20_36
| spl20_35
| spl20_14 ),
inference(rat,[],[s16,s92,s52,s209,s18,s243]) ).
cnf(s245,plain,
( spl20_35
| spl20_14 ),
inference(rat,[],[s166,s15,s19,s56,s241,s165,s37,s244,s18,s243]) ).
cnf(s246,plain,
( spl20_27
| ~ spl20_28
| spl20_11 ),
inference(rat,[],[s23,s226,s189,s187,s6,s88,s7,s4,s22,s222,s232,s177,s27]) ).
cnf(s247,plain,
( spl20_3
| spl20_5
| ~ spl20_26 ),
inference(rat,[],[s198,s26,s24,s199,s197,s135,s4,s22]) ).
cnf(s248,plain,
( spl20_5
| ~ spl20_26 ),
inference(rat,[],[s125,s25,s24,s136,s137,s3,s21,s247]) ).
cnf(s249,plain,
( ~ spl20_28
| spl20_11 ),
inference(rat,[],[s248,s5,s170,s7,s171,s9,s174,s28,s246]) ).
cnf(s250,plain,
( spl20_12
| spl20_13 ),
inference(rat,[],[s249,s30,s151,s32,s163,s34,s152,s77,s11,s36,s245,s14]) ).
cnf(s251,plain,
( ~ spl20_27
| spl20_13 ),
inference(rat,[],[s8,s139,s146,s5,s81,s9,s248,s123,s28,s12,s29,s224,s250,s36,s245,s14]) ).
cnf(s252,plain,
spl20_13,
inference(rat,[],[s23,s226,s189,s187,s6,s90,s8,s173,s4,s22,s10,s234,s79,s200,s27,s251,s29,s224,s12,s250,s36,s245,s14]) ).
cnf(s253,plain,
spl20_14,
inference(rat,[],[s13,s252]) ).
cnf(s254,plain,
( spl20_36
| ~ spl20_19
| ~ spl20_35 ),
inference(rat,[],[s57,s216,s105,s17,s153,s253]) ).
cnf(s255,plain,
( ~ spl20_20
| ~ spl20_35 ),
inference(rat,[],[s254,s37,s241,s20]) ).
cnf(s256,plain,
~ spl20_35,
inference(rat,[],[s107,s17,s15,s98,s69,s38,s101,s39,s64,s42,s61,s106,s19,s255,s253,s239,s238]) ).
cnf(s257,plain,
~ spl20_34,
inference(rat,[],[s35,s256]) ).
cnf(s260,plain,
spl20_12,
inference(rat,[],[s124,s31,s30,s215,s249,s148,s11,s257,s252]) ).
cnf(s261,plain,
spl20_11,
inference(rat,[],[s12,s260]) ).
cnf(s262,plain,
~ spl20_29,
inference(rat,[],[s221,s252,s257,s260]) ).
cnf(s264,plain,
~ spl20_28,
inference(rat,[],[s29,s262]) ).
cnf(s269,plain,
~ spl20_27,
inference(rat,[],[s8,s139,s146,s5,s81,s9,s248,s123,s28,s264,s261]) ).
cnf(s270,plain,
~ spl20_26,
inference(rat,[],[s27,s269]) ).
cnf(s271,plain,
~ spl20_45,
inference(rat,[],[s200,s264,s269]) ).
cnf(s272,plain,
spl20_10,
inference(rat,[],[s79,s261,s264,s269]) ).
cnf(s273,plain,
~ spl20_3,
inference(rat,[],[s234,s264,s261,s269]) ).
cnf(s274,plain,
spl20_9,
inference(rat,[],[s10,s272]) ).
cnf(s275,plain,
~ spl20_21,
inference(rat,[],[s22,s273]) ).
cnf(s276,plain,
~ spl20_4,
inference(rat,[],[s4,s273]) ).
cnf(s277,plain,
spl20_8,
inference(rat,[],[s173,s271,s274]) ).
cnf(s278,plain,
spl20_7,
inference(rat,[],[s8,s277]) ).
cnf(s279,plain,
spl20_6,
inference(rat,[],[s90,s271,s278]) ).
cnf(s280,plain,
spl20_5,
inference(rat,[],[s6,s279]) ).
cnf(s281,plain,
spl20_46,
inference(rat,[],[s187,s276,s280]) ).
cnf(s282,plain,
spl20_22,
inference(rat,[],[s189,s275,s281]) ).
cnf(s284,plain,
~ spl20_23,
inference(rat,[],[s226,s270,s281]) ).
cnf(s285,plain,
$false,
inference(rat,[],[s23,s284,s282]) ).
tff(f885,plain,
$false,
inference(avatar_sat_refutation,[],[s285]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500_8.005 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n006.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 17:46:25 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running first-order theorem proving
% 0.07/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.01/1.14 % (4192092)Detected formulas, will run a generic FOF schedule.
% 3.01/1.14 % (4192168)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=3310725334:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.01/1.14 % (4192167)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=185898149:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.01/1.14 % (4192165)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=572261221:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.01/1.14 % (4192172)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2375192203:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.01/1.14 % (4192171)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1716753713:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.01/1.14 % (4192174)dis-21_1_sil=8000:lcm=predicate:random_seed=2367344997: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)
% 3.01/1.14 % (4192174)Refutation not found, incomplete strategy
% 3.01/1.14 % (4192174)------------------------------
% 3.01/1.14 % (4192174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.01/1.14 % (4192174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.01/1.14 % (4192174)CaDiCaL version: 2.1.3
% 3.01/1.14 % (4192174)Termination reason: Refutation not found, incomplete strategy
% 3.01/1.14 % (4192174)Time elapsed: 0.003 s
% 3.01/1.14 % (4192174)Peak memory usage: 89 MB
% 3.01/1.14 % (4192174)Instructions burned: 3 (million)
% 3.01/1.14 % (4192169)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1231225062:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.01/1.14 % (4192169)Refutation not found, incomplete strategy
% 3.01/1.14 % (4192169)------------------------------
% 3.01/1.14 % (4192169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.01/1.14 % (4192169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.01/1.14 % (4192169)CaDiCaL version: 2.1.3
% 3.01/1.14 % (4192169)Termination reason: Refutation not found, incomplete strategy
% 3.01/1.14 % (4192169)Time elapsed: 0.002 s
% 3.01/1.14 % (4192169)Peak memory usage: 88 MB
% 3.01/1.14 % (4192169)Instructions burned: 1 (million)
% 3.01/1.14 % (4192172)First to succeed.
% 3.01/1.14 % (4192172)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4192092"
% 3.01/1.14 % (4192171)Instruction limit reached!
% 3.01/1.14 % (4192171)------------------------------
% 3.01/1.14 % (4192171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.01/1.14 % (4192171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.01/1.14 % (4192171)CaDiCaL version: 2.1.3
% 3.01/1.14 % (4192171)Termination reason: Instruction limit
% 3.01/1.14 % (4192171)Termination phase: Saturation
% 3.01/1.14 % (4192171)Time elapsed: 0.056 s
% 3.01/1.14 % (4192171)Peak memory usage: 88 MB
% 3.01/1.14 % (4192171)Instructions burned: 119 (million)
% 3.01/1.14 % (4192174)------------------------------
% 3.01/1.14 % (4192174)------------------------------
% 3.01/1.14 % (4192169)------------------------------
% 3.01/1.14 % (4192169)------------------------------
% 3.01/1.14 % (4192172)Refutation found. Thanks to Tanya!
% 3.01/1.14 % SZS status Theorem for theBenchmark
% 3.01/1.14 % SZS output start Proof for theBenchmark
% See solution above
% 3.81/1.39 % (4192172)------------------------------
% 3.81/1.39 % (4192172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.81/1.39 % (4192172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.81/1.39 % (4192172)CaDiCaL version: 2.1.3
% 3.81/1.39 % (4192172)Termination reason: Refutation
% 3.81/1.39 % (4192172)Time elapsed: 0.022 s
% 3.81/1.39 % (4192172)Peak memory usage: 90 MB
% 3.81/1.39 % (4192172)Instructions burned: 31 (million)
% 3.81/1.39 % (4192172)------------------------------
% 3.81/1.39 % (4192172)------------------------------
% 3.81/1.39 % (4192092)Success in time 0.452 s
% 3.81/1.39 % Vampire exiting
%------------------------------------------------------------------------------