%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO500_8.007 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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:50 PM UTC 2026
% Result : Theorem 2.90s 0.93s
% Output : Refutation 2.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 94
% Syntax : Number of formulae : 866 ( 18 unt; 0 typ; 92 def)
% Number of atoms : 3394 ( 281 equ)
% Maximal formula atoms : 5 ( 3 avg)
% Number of connectives : 2641 (1099 ~;1419 |; 29 &)
% ( 93 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 990 ( 986 fml; 4 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 103 ( 100 usr; 95 prp; 0-2 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 2 ( 0 sgn 2 !; 0 ?; 2 :)
% 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(func_def_22,type,
bG20: $o ).
tff(func_def_23,type,
bG21: $o ).
tff(func_def_24,type,
bG22: $o ).
tff(func_def_25,type,
bG23: $o ).
tff(func_def_26,type,
bG24: $o ).
tff(func_def_27,type,
bG25: $o ).
tff(func_def_28,type,
bG26: $o ).
tff(func_def_29,type,
bG27: $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(pred_def_7,type,
f5: $o > $o ).
tff(pred_def_8,type,
f6: $o > $o ).
tff(f1,conjecture,
f0(f1(f1(f1(f2(f3(f3(f3(f4(f5(f5(f5(f6(x))))))))))))) = f0(f0(f0(f1(f2(f2(f2(f3(f4(f4(f4(f5(f6(f6(f6(x))))))))))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kaminski7) ).
tff(f2,negated_conjecture,
f0(f1(f1(f1(f2(f3(f3(f3(f4(f5(f5(f5(f6(x))))))))))))) != f0(f0(f0(f1(f2(f2(f2(f3(f4(f4(f4(f5(f6(f6(f6(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,
( f6(bG0)
<=> ( $true = bG1 ) ),
introduced(definition,[new_symbols(definition,[bG1])],[fool_formula_definition]) ).
tff(f5,definition,
( f5(bG1)
<=> ( $true = bG2 ) ),
introduced(definition,[new_symbols(definition,[bG2])],[fool_formula_definition]) ).
tff(f6,definition,
( f5(bG2)
<=> ( $true = bG3 ) ),
introduced(definition,[new_symbols(definition,[bG3])],[fool_formula_definition]) ).
tff(f7,definition,
( f5(bG3)
<=> ( $true = bG4 ) ),
introduced(definition,[new_symbols(definition,[bG4])],[fool_formula_definition]) ).
tff(f8,definition,
( f4(bG4)
<=> ( $true = bG5 ) ),
introduced(definition,[new_symbols(definition,[bG5])],[fool_formula_definition]) ).
tff(f9,definition,
( f3(bG5)
<=> ( $true = bG6 ) ),
introduced(definition,[new_symbols(definition,[bG6])],[fool_formula_definition]) ).
tff(f10,definition,
( f3(bG6)
<=> ( $true = bG7 ) ),
introduced(definition,[new_symbols(definition,[bG7])],[fool_formula_definition]) ).
tff(f11,definition,
( f3(bG7)
<=> ( $true = bG8 ) ),
introduced(definition,[new_symbols(definition,[bG8])],[fool_formula_definition]) ).
tff(f12,definition,
( f2(bG8)
<=> ( $true = bG9 ) ),
introduced(definition,[new_symbols(definition,[bG9])],[fool_formula_definition]) ).
tff(f13,definition,
( f1(bG9)
<=> ( $true = bG10 ) ),
introduced(definition,[new_symbols(definition,[bG10])],[fool_formula_definition]) ).
tff(f14,definition,
( f1(bG10)
<=> ( $true = bG11 ) ),
introduced(definition,[new_symbols(definition,[bG11])],[fool_formula_definition]) ).
tff(f15,definition,
( f1(bG11)
<=> ( $true = bG12 ) ),
introduced(definition,[new_symbols(definition,[bG12])],[fool_formula_definition]) ).
tff(f16,definition,
( x
<=> ( $true = bG13 ) ),
introduced(definition,[new_symbols(definition,[bG13])],[fool_formula_definition]) ).
tff(f17,definition,
( f6(bG13)
<=> ( $true = bG14 ) ),
introduced(definition,[new_symbols(definition,[bG14])],[fool_formula_definition]) ).
tff(f18,definition,
( f6(bG14)
<=> ( $true = bG15 ) ),
introduced(definition,[new_symbols(definition,[bG15])],[fool_formula_definition]) ).
tff(f19,definition,
( f6(bG15)
<=> ( $true = bG16 ) ),
introduced(definition,[new_symbols(definition,[bG16])],[fool_formula_definition]) ).
tff(f20,definition,
( f5(bG16)
<=> ( $true = bG17 ) ),
introduced(definition,[new_symbols(definition,[bG17])],[fool_formula_definition]) ).
tff(f21,definition,
( f4(bG17)
<=> ( $true = bG18 ) ),
introduced(definition,[new_symbols(definition,[bG18])],[fool_formula_definition]) ).
tff(f22,definition,
( f4(bG18)
<=> ( $true = bG19 ) ),
introduced(definition,[new_symbols(definition,[bG19])],[fool_formula_definition]) ).
tff(f23,definition,
( f4(bG19)
<=> ( $true = bG20 ) ),
introduced(definition,[new_symbols(definition,[bG20])],[fool_formula_definition]) ).
tff(f24,definition,
( f3(bG20)
<=> ( $true = bG21 ) ),
introduced(definition,[new_symbols(definition,[bG21])],[fool_formula_definition]) ).
tff(f25,definition,
( f2(bG21)
<=> ( $true = bG22 ) ),
introduced(definition,[new_symbols(definition,[bG22])],[fool_formula_definition]) ).
tff(f26,definition,
( f2(bG22)
<=> ( $true = bG23 ) ),
introduced(definition,[new_symbols(definition,[bG23])],[fool_formula_definition]) ).
tff(f27,definition,
( f2(bG23)
<=> ( $true = bG24 ) ),
introduced(definition,[new_symbols(definition,[bG24])],[fool_formula_definition]) ).
tff(f28,definition,
( f1(bG24)
<=> ( $true = bG25 ) ),
introduced(definition,[new_symbols(definition,[bG25])],[fool_formula_definition]) ).
tff(f29,definition,
( f0(bG25)
<=> ( $true = bG26 ) ),
introduced(definition,[new_symbols(definition,[bG26])],[fool_formula_definition]) ).
tff(f30,definition,
( f0(bG26)
<=> ( $true = bG27 ) ),
introduced(definition,[new_symbols(definition,[bG27])],[fool_formula_definition]) ).
tff(f31,plain,
~ ( f0(bG12)
<=> f0(bG27) ),
inference(fool_elimination,[],[f2,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7,f6,f5,f4,f3]) ).
tff(f32,plain,
( f0(bG12)
<~> f0(bG27) ),
inference(ennf_transformation,[],[f31]) ).
tff(f33,plain,
( ( f0(bG26)
| ( $true != bG27 ) )
& ( ( $true = bG27 )
| ~ f0(bG26) ) ),
inference(nnf_transformation,[],[f30]) ).
tff(f34,plain,
( ( f0(bG25)
| ( $true != bG26 ) )
& ( ( $true = bG26 )
| ~ f0(bG25) ) ),
inference(nnf_transformation,[],[f29]) ).
tff(f35,plain,
( ( f1(bG24)
| ( $true != bG25 ) )
& ( ( $true = bG25 )
| ~ f1(bG24) ) ),
inference(nnf_transformation,[],[f28]) ).
tff(f36,plain,
( ( f2(bG23)
| ( $true != bG24 ) )
& ( ( $true = bG24 )
| ~ f2(bG23) ) ),
inference(nnf_transformation,[],[f27]) ).
tff(f37,plain,
( ( f2(bG22)
| ( $true != bG23 ) )
& ( ( $true = bG23 )
| ~ f2(bG22) ) ),
inference(nnf_transformation,[],[f26]) ).
tff(f38,plain,
( ( f2(bG21)
| ( $true != bG22 ) )
& ( ( $true = bG22 )
| ~ f2(bG21) ) ),
inference(nnf_transformation,[],[f25]) ).
tff(f39,plain,
( ( f3(bG20)
| ( $true != bG21 ) )
& ( ( $true = bG21 )
| ~ f3(bG20) ) ),
inference(nnf_transformation,[],[f24]) ).
tff(f40,plain,
( ( f4(bG19)
| ( $true != bG20 ) )
& ( ( $true = bG20 )
| ~ f4(bG19) ) ),
inference(nnf_transformation,[],[f23]) ).
tff(f41,plain,
( ( f4(bG18)
| ( $true != bG19 ) )
& ( ( $true = bG19 )
| ~ f4(bG18) ) ),
inference(nnf_transformation,[],[f22]) ).
tff(f42,plain,
( ( f4(bG17)
| ( $true != bG18 ) )
& ( ( $true = bG18 )
| ~ f4(bG17) ) ),
inference(nnf_transformation,[],[f21]) ).
tff(f43,plain,
( ( f5(bG16)
| ( $true != bG17 ) )
& ( ( $true = bG17 )
| ~ f5(bG16) ) ),
inference(nnf_transformation,[],[f20]) ).
tff(f44,plain,
( ( f6(bG15)
| ( $true != bG16 ) )
& ( ( $true = bG16 )
| ~ f6(bG15) ) ),
inference(nnf_transformation,[],[f19]) ).
tff(f45,plain,
( ( f6(bG14)
| ( $true != bG15 ) )
& ( ( $true = bG15 )
| ~ f6(bG14) ) ),
inference(nnf_transformation,[],[f18]) ).
tff(f46,plain,
( ( f6(bG13)
| ( $true != bG14 ) )
& ( ( $true = bG14 )
| ~ f6(bG13) ) ),
inference(nnf_transformation,[],[f17]) ).
tff(f47,plain,
( ( x
| ( $true != bG13 ) )
& ( ( $true = bG13 )
| ~ x ) ),
inference(nnf_transformation,[],[f16]) ).
tff(f48,plain,
( ( f1(bG11)
| ( $true != bG12 ) )
& ( ( $true = bG12 )
| ~ f1(bG11) ) ),
inference(nnf_transformation,[],[f15]) ).
tff(f49,plain,
( ( f1(bG10)
| ( $true != bG11 ) )
& ( ( $true = bG11 )
| ~ f1(bG10) ) ),
inference(nnf_transformation,[],[f14]) ).
tff(f50,plain,
( ( f1(bG9)
| ( $true != bG10 ) )
& ( ( $true = bG10 )
| ~ f1(bG9) ) ),
inference(nnf_transformation,[],[f13]) ).
tff(f51,plain,
( ( f2(bG8)
| ( $true != bG9 ) )
& ( ( $true = bG9 )
| ~ f2(bG8) ) ),
inference(nnf_transformation,[],[f12]) ).
tff(f52,plain,
( ( f3(bG7)
| ( $true != bG8 ) )
& ( ( $true = bG8 )
| ~ f3(bG7) ) ),
inference(nnf_transformation,[],[f11]) ).
tff(f53,plain,
( ( f3(bG6)
| ( $true != bG7 ) )
& ( ( $true = bG7 )
| ~ f3(bG6) ) ),
inference(nnf_transformation,[],[f10]) ).
tff(f54,plain,
( ( f3(bG5)
| ( $true != bG6 ) )
& ( ( $true = bG6 )
| ~ f3(bG5) ) ),
inference(nnf_transformation,[],[f9]) ).
tff(f55,plain,
( ( f4(bG4)
| ( $true != bG5 ) )
& ( ( $true = bG5 )
| ~ f4(bG4) ) ),
inference(nnf_transformation,[],[f8]) ).
tff(f56,plain,
( ( f5(bG3)
| ( $true != bG4 ) )
& ( ( $true = bG4 )
| ~ f5(bG3) ) ),
inference(nnf_transformation,[],[f7]) ).
tff(f57,plain,
( ( f5(bG2)
| ( $true != bG3 ) )
& ( ( $true = bG3 )
| ~ f5(bG2) ) ),
inference(nnf_transformation,[],[f6]) ).
tff(f58,plain,
( ( f5(bG1)
| ( $true != bG2 ) )
& ( ( $true = bG2 )
| ~ f5(bG1) ) ),
inference(nnf_transformation,[],[f5]) ).
tff(f59,plain,
( ( f6(bG0)
| ( $true != bG1 ) )
& ( ( $true = bG1 )
| ~ f6(bG0) ) ),
inference(nnf_transformation,[],[f4]) ).
tff(f60,plain,
( ( x
| ( bG0 != $true ) )
& ( ( bG0 = $true )
| ~ x ) ),
inference(nnf_transformation,[],[f3]) ).
tff(f61,plain,
( ( ~ f0(bG27)
| ~ f0(bG12) )
& ( f0(bG27)
| f0(bG12) ) ),
inference(nnf_transformation,[],[f32]) ).
tff(f62,plain,
( ( $true = bG27 )
| ~ f0(bG26) ),
inference(cnf_transformation,[],[f33]) ).
tff(f63,plain,
( f0(bG26)
| ( $true != bG27 ) ),
inference(cnf_transformation,[],[f33]) ).
tff(f64,plain,
( ( $true = bG26 )
| ~ f0(bG25) ),
inference(cnf_transformation,[],[f34]) ).
tff(f65,plain,
( f0(bG25)
| ( $true != bG26 ) ),
inference(cnf_transformation,[],[f34]) ).
tff(f66,plain,
( ( $true = bG25 )
| ~ f1(bG24) ),
inference(cnf_transformation,[],[f35]) ).
tff(f67,plain,
( f1(bG24)
| ( $true != bG25 ) ),
inference(cnf_transformation,[],[f35]) ).
tff(f68,plain,
( ( $true = bG24 )
| ~ f2(bG23) ),
inference(cnf_transformation,[],[f36]) ).
tff(f69,plain,
( f2(bG23)
| ( $true != bG24 ) ),
inference(cnf_transformation,[],[f36]) ).
tff(f70,plain,
( ( $true = bG23 )
| ~ f2(bG22) ),
inference(cnf_transformation,[],[f37]) ).
tff(f71,plain,
( f2(bG22)
| ( $true != bG23 ) ),
inference(cnf_transformation,[],[f37]) ).
tff(f72,plain,
( ( $true = bG22 )
| ~ f2(bG21) ),
inference(cnf_transformation,[],[f38]) ).
tff(f73,plain,
( f2(bG21)
| ( $true != bG22 ) ),
inference(cnf_transformation,[],[f38]) ).
tff(f74,plain,
( ( $true = bG21 )
| ~ f3(bG20) ),
inference(cnf_transformation,[],[f39]) ).
tff(f75,plain,
( f3(bG20)
| ( $true != bG21 ) ),
inference(cnf_transformation,[],[f39]) ).
tff(f76,plain,
( ( $true = bG20 )
| ~ f4(bG19) ),
inference(cnf_transformation,[],[f40]) ).
tff(f77,plain,
( f4(bG19)
| ( $true != bG20 ) ),
inference(cnf_transformation,[],[f40]) ).
tff(f78,plain,
( ( $true = bG19 )
| ~ f4(bG18) ),
inference(cnf_transformation,[],[f41]) ).
tff(f79,plain,
( f4(bG18)
| ( $true != bG19 ) ),
inference(cnf_transformation,[],[f41]) ).
tff(f80,plain,
( ( $true = bG18 )
| ~ f4(bG17) ),
inference(cnf_transformation,[],[f42]) ).
tff(f81,plain,
( f4(bG17)
| ( $true != bG18 ) ),
inference(cnf_transformation,[],[f42]) ).
tff(f82,plain,
( ( $true = bG17 )
| ~ f5(bG16) ),
inference(cnf_transformation,[],[f43]) ).
tff(f83,plain,
( f5(bG16)
| ( $true != bG17 ) ),
inference(cnf_transformation,[],[f43]) ).
tff(f84,plain,
( ( $true = bG16 )
| ~ f6(bG15) ),
inference(cnf_transformation,[],[f44]) ).
tff(f85,plain,
( f6(bG15)
| ( $true != bG16 ) ),
inference(cnf_transformation,[],[f44]) ).
tff(f86,plain,
( ( $true = bG15 )
| ~ f6(bG14) ),
inference(cnf_transformation,[],[f45]) ).
tff(f87,plain,
( f6(bG14)
| ( $true != bG15 ) ),
inference(cnf_transformation,[],[f45]) ).
tff(f88,plain,
( ( $true = bG14 )
| ~ f6(bG13) ),
inference(cnf_transformation,[],[f46]) ).
tff(f89,plain,
( f6(bG13)
| ( $true != bG14 ) ),
inference(cnf_transformation,[],[f46]) ).
tff(f90,plain,
( ( $true = bG13 )
| ~ x ),
inference(cnf_transformation,[],[f47]) ).
tff(f91,plain,
( x
| ( $true != bG13 ) ),
inference(cnf_transformation,[],[f47]) ).
tff(f92,plain,
( ( $true = bG12 )
| ~ f1(bG11) ),
inference(cnf_transformation,[],[f48]) ).
tff(f93,plain,
( f1(bG11)
| ( $true != bG12 ) ),
inference(cnf_transformation,[],[f48]) ).
tff(f94,plain,
( ( $true = bG11 )
| ~ f1(bG10) ),
inference(cnf_transformation,[],[f49]) ).
tff(f95,plain,
( f1(bG10)
| ( $true != bG11 ) ),
inference(cnf_transformation,[],[f49]) ).
tff(f96,plain,
( ( $true = bG10 )
| ~ f1(bG9) ),
inference(cnf_transformation,[],[f50]) ).
tff(f97,plain,
( f1(bG9)
| ( $true != bG10 ) ),
inference(cnf_transformation,[],[f50]) ).
tff(f98,plain,
( ( $true = bG9 )
| ~ f2(bG8) ),
inference(cnf_transformation,[],[f51]) ).
tff(f99,plain,
( f2(bG8)
| ( $true != bG9 ) ),
inference(cnf_transformation,[],[f51]) ).
tff(f100,plain,
( ( $true = bG8 )
| ~ f3(bG7) ),
inference(cnf_transformation,[],[f52]) ).
tff(f101,plain,
( f3(bG7)
| ( $true != bG8 ) ),
inference(cnf_transformation,[],[f52]) ).
tff(f102,plain,
( ( $true = bG7 )
| ~ f3(bG6) ),
inference(cnf_transformation,[],[f53]) ).
tff(f103,plain,
( f3(bG6)
| ( $true != bG7 ) ),
inference(cnf_transformation,[],[f53]) ).
tff(f104,plain,
( ( $true = bG6 )
| ~ f3(bG5) ),
inference(cnf_transformation,[],[f54]) ).
tff(f105,plain,
( f3(bG5)
| ( $true != bG6 ) ),
inference(cnf_transformation,[],[f54]) ).
tff(f106,plain,
( ( $true = bG5 )
| ~ f4(bG4) ),
inference(cnf_transformation,[],[f55]) ).
tff(f107,plain,
( f4(bG4)
| ( $true != bG5 ) ),
inference(cnf_transformation,[],[f55]) ).
tff(f108,plain,
( ( $true = bG4 )
| ~ f5(bG3) ),
inference(cnf_transformation,[],[f56]) ).
tff(f109,plain,
( f5(bG3)
| ( $true != bG4 ) ),
inference(cnf_transformation,[],[f56]) ).
tff(f110,plain,
( ( $true = bG3 )
| ~ f5(bG2) ),
inference(cnf_transformation,[],[f57]) ).
tff(f111,plain,
( f5(bG2)
| ( $true != bG3 ) ),
inference(cnf_transformation,[],[f57]) ).
tff(f112,plain,
( ( $true = bG2 )
| ~ f5(bG1) ),
inference(cnf_transformation,[],[f58]) ).
tff(f113,plain,
( f5(bG1)
| ( $true != bG2 ) ),
inference(cnf_transformation,[],[f58]) ).
tff(f114,plain,
( ( $true = bG1 )
| ~ f6(bG0) ),
inference(cnf_transformation,[],[f59]) ).
tff(f115,plain,
( f6(bG0)
| ( $true != bG1 ) ),
inference(cnf_transformation,[],[f59]) ).
tff(f116,plain,
( ( bG0 = $true )
| ~ x ),
inference(cnf_transformation,[],[f60]) ).
tff(f117,plain,
( x
| ( bG0 != $true ) ),
inference(cnf_transformation,[],[f60]) ).
tff(f118,plain,
( f0(bG27)
| f0(bG12) ),
inference(cnf_transformation,[],[f61]) ).
tff(f119,plain,
( ~ f0(bG27)
| ~ f0(bG12) ),
inference(cnf_transformation,[],[f61]) ).
tff(f121,plain,
! [X0: $o] :
( ( $false = (X0) )
| ( $true = (X0) ) ),
introduced(definition,[],[fool_exhaustiveness_axiom]) ).
tff(f123,definition,
( spl28_1
<=> f0(bG12) ),
introduced(definition,[new_symbols(definition,[spl28_1])],[avatar_definition]) ).
tff(f124,plain,
( ~ f0(bG12)
| spl28_1 ),
inference(avatar_component_clause,[],[f123]) ).
tff(f125,plain,
( f0(bG12)
| ~ spl28_1 ),
inference(avatar_component_clause,[],[f123]) ).
tff(f127,definition,
( spl28_2
<=> f0(bG27) ),
introduced(definition,[new_symbols(definition,[spl28_2])],[avatar_definition]) ).
tff(f128,plain,
( ~ f0(bG27)
| spl28_2 ),
inference(avatar_component_clause,[],[f127]) ).
tff(f129,plain,
( f0(bG27)
| ~ spl28_2 ),
inference(avatar_component_clause,[],[f127]) ).
tff(f130,plain,
( spl28_1
| spl28_2 ),
inference(avatar_split_clause,[],[f118,f127,f123]) ).
tff(f131,plain,
( ~ spl28_1
| ~ spl28_2 ),
inference(avatar_split_clause,[],[f119,f127,f123]) ).
tff(f133,definition,
( spl28_3
<=> x ),
introduced(definition,[new_symbols(definition,[spl28_3])],[avatar_definition]) ).
tff(f137,definition,
( spl28_4
<=> ( bG0 = $true ) ),
introduced(definition,[new_symbols(definition,[spl28_4])],[avatar_definition]) ).
tff(f139,plain,
( ( bG0 = $true )
| ~ spl28_4 ),
inference(avatar_component_clause,[],[f137]) ).
tff(f140,plain,
( ~ spl28_3
| spl28_4 ),
inference(avatar_split_clause,[],[f116,f137,f133]) ).
tff(f141,plain,
( ~ spl28_4
| spl28_3 ),
inference(avatar_split_clause,[],[f117,f133,f137]) ).
tff(f143,definition,
( spl28_5
<=> f6(bG0) ),
introduced(definition,[new_symbols(definition,[spl28_5])],[avatar_definition]) ).
tff(f144,plain,
( f6(bG0)
| ~ spl28_5 ),
inference(avatar_component_clause,[],[f143]) ).
tff(f145,plain,
( ~ f6(bG0)
| spl28_5 ),
inference(avatar_component_clause,[],[f143]) ).
tff(f147,definition,
( spl28_6
<=> ( $true = bG1 ) ),
introduced(definition,[new_symbols(definition,[spl28_6])],[avatar_definition]) ).
tff(f149,plain,
( ( $true = bG1 )
| ~ spl28_6 ),
inference(avatar_component_clause,[],[f147]) ).
tff(f150,plain,
( ~ spl28_5
| spl28_6 ),
inference(avatar_split_clause,[],[f114,f147,f143]) ).
tff(f151,plain,
( ~ spl28_6
| spl28_5 ),
inference(avatar_split_clause,[],[f115,f143,f147]) ).
tff(f153,definition,
( spl28_7
<=> f5(bG1) ),
introduced(definition,[new_symbols(definition,[spl28_7])],[avatar_definition]) ).
tff(f154,plain,
( f5(bG1)
| ~ spl28_7 ),
inference(avatar_component_clause,[],[f153]) ).
tff(f155,plain,
( ~ f5(bG1)
| spl28_7 ),
inference(avatar_component_clause,[],[f153]) ).
tff(f157,definition,
( spl28_8
<=> ( $true = bG2 ) ),
introduced(definition,[new_symbols(definition,[spl28_8])],[avatar_definition]) ).
tff(f159,plain,
( ( $true = bG2 )
| ~ spl28_8 ),
inference(avatar_component_clause,[],[f157]) ).
tff(f160,plain,
( ~ spl28_7
| spl28_8 ),
inference(avatar_split_clause,[],[f112,f157,f153]) ).
tff(f161,plain,
( ~ spl28_8
| spl28_7 ),
inference(avatar_split_clause,[],[f113,f153,f157]) ).
tff(f163,definition,
( spl28_9
<=> f5(bG2) ),
introduced(definition,[new_symbols(definition,[spl28_9])],[avatar_definition]) ).
tff(f164,plain,
( f5(bG2)
| ~ spl28_9 ),
inference(avatar_component_clause,[],[f163]) ).
tff(f165,plain,
( ~ f5(bG2)
| spl28_9 ),
inference(avatar_component_clause,[],[f163]) ).
tff(f167,definition,
( spl28_10
<=> ( $true = bG3 ) ),
introduced(definition,[new_symbols(definition,[spl28_10])],[avatar_definition]) ).
tff(f169,plain,
( ( $true = bG3 )
| ~ spl28_10 ),
inference(avatar_component_clause,[],[f167]) ).
tff(f170,plain,
( ~ spl28_9
| spl28_10 ),
inference(avatar_split_clause,[],[f110,f167,f163]) ).
tff(f171,plain,
( ~ spl28_10
| spl28_9 ),
inference(avatar_split_clause,[],[f111,f163,f167]) ).
tff(f173,definition,
( spl28_11
<=> f5(bG3) ),
introduced(definition,[new_symbols(definition,[spl28_11])],[avatar_definition]) ).
tff(f174,plain,
( f5(bG3)
| ~ spl28_11 ),
inference(avatar_component_clause,[],[f173]) ).
tff(f175,plain,
( ~ f5(bG3)
| spl28_11 ),
inference(avatar_component_clause,[],[f173]) ).
tff(f177,definition,
( spl28_12
<=> ( $true = bG4 ) ),
introduced(definition,[new_symbols(definition,[spl28_12])],[avatar_definition]) ).
tff(f179,plain,
( ( $true = bG4 )
| ~ spl28_12 ),
inference(avatar_component_clause,[],[f177]) ).
tff(f180,plain,
( ~ spl28_11
| spl28_12 ),
inference(avatar_split_clause,[],[f108,f177,f173]) ).
tff(f181,plain,
( ~ spl28_12
| spl28_11 ),
inference(avatar_split_clause,[],[f109,f173,f177]) ).
tff(f183,definition,
( spl28_13
<=> f4(bG4) ),
introduced(definition,[new_symbols(definition,[spl28_13])],[avatar_definition]) ).
tff(f184,plain,
( f4(bG4)
| ~ spl28_13 ),
inference(avatar_component_clause,[],[f183]) ).
tff(f185,plain,
( ~ f4(bG4)
| spl28_13 ),
inference(avatar_component_clause,[],[f183]) ).
tff(f187,definition,
( spl28_14
<=> ( $true = bG5 ) ),
introduced(definition,[new_symbols(definition,[spl28_14])],[avatar_definition]) ).
tff(f189,plain,
( ( $true = bG5 )
| ~ spl28_14 ),
inference(avatar_component_clause,[],[f187]) ).
tff(f190,plain,
( ~ spl28_13
| spl28_14 ),
inference(avatar_split_clause,[],[f106,f187,f183]) ).
tff(f191,plain,
( ~ spl28_14
| spl28_13 ),
inference(avatar_split_clause,[],[f107,f183,f187]) ).
tff(f193,definition,
( spl28_15
<=> f3(bG5) ),
introduced(definition,[new_symbols(definition,[spl28_15])],[avatar_definition]) ).
tff(f194,plain,
( f3(bG5)
| ~ spl28_15 ),
inference(avatar_component_clause,[],[f193]) ).
tff(f195,plain,
( ~ f3(bG5)
| spl28_15 ),
inference(avatar_component_clause,[],[f193]) ).
tff(f197,definition,
( spl28_16
<=> ( $true = bG6 ) ),
introduced(definition,[new_symbols(definition,[spl28_16])],[avatar_definition]) ).
tff(f199,plain,
( ( $true = bG6 )
| ~ spl28_16 ),
inference(avatar_component_clause,[],[f197]) ).
tff(f200,plain,
( ~ spl28_15
| spl28_16 ),
inference(avatar_split_clause,[],[f104,f197,f193]) ).
tff(f201,plain,
( ~ spl28_16
| spl28_15 ),
inference(avatar_split_clause,[],[f105,f193,f197]) ).
tff(f203,definition,
( spl28_17
<=> f3(bG6) ),
introduced(definition,[new_symbols(definition,[spl28_17])],[avatar_definition]) ).
tff(f204,plain,
( f3(bG6)
| ~ spl28_17 ),
inference(avatar_component_clause,[],[f203]) ).
tff(f205,plain,
( ~ f3(bG6)
| spl28_17 ),
inference(avatar_component_clause,[],[f203]) ).
tff(f207,definition,
( spl28_18
<=> ( $true = bG7 ) ),
introduced(definition,[new_symbols(definition,[spl28_18])],[avatar_definition]) ).
tff(f208,plain,
( ( $true != bG7 )
| spl28_18 ),
inference(avatar_component_clause,[],[f207]) ).
tff(f209,plain,
( ( $true = bG7 )
| ~ spl28_18 ),
inference(avatar_component_clause,[],[f207]) ).
tff(f210,plain,
( ~ spl28_17
| spl28_18 ),
inference(avatar_split_clause,[],[f102,f207,f203]) ).
tff(f211,plain,
( ~ spl28_18
| spl28_17 ),
inference(avatar_split_clause,[],[f103,f203,f207]) ).
tff(f213,definition,
( spl28_19
<=> f3(bG7) ),
introduced(definition,[new_symbols(definition,[spl28_19])],[avatar_definition]) ).
tff(f214,plain,
( f3(bG7)
| ~ spl28_19 ),
inference(avatar_component_clause,[],[f213]) ).
tff(f215,plain,
( ~ f3(bG7)
| spl28_19 ),
inference(avatar_component_clause,[],[f213]) ).
tff(f217,definition,
( spl28_20
<=> ( $true = bG8 ) ),
introduced(definition,[new_symbols(definition,[spl28_20])],[avatar_definition]) ).
tff(f219,plain,
( ( $true = bG8 )
| ~ spl28_20 ),
inference(avatar_component_clause,[],[f217]) ).
tff(f220,plain,
( ~ spl28_19
| spl28_20 ),
inference(avatar_split_clause,[],[f100,f217,f213]) ).
tff(f221,plain,
( ~ spl28_20
| spl28_19 ),
inference(avatar_split_clause,[],[f101,f213,f217]) ).
tff(f223,definition,
( spl28_21
<=> f2(bG8) ),
introduced(definition,[new_symbols(definition,[spl28_21])],[avatar_definition]) ).
tff(f224,plain,
( f2(bG8)
| ~ spl28_21 ),
inference(avatar_component_clause,[],[f223]) ).
tff(f225,plain,
( ~ f2(bG8)
| spl28_21 ),
inference(avatar_component_clause,[],[f223]) ).
tff(f227,definition,
( spl28_22
<=> ( $true = bG9 ) ),
introduced(definition,[new_symbols(definition,[spl28_22])],[avatar_definition]) ).
tff(f228,plain,
( ( $true != bG9 )
| spl28_22 ),
inference(avatar_component_clause,[],[f227]) ).
tff(f229,plain,
( ( $true = bG9 )
| ~ spl28_22 ),
inference(avatar_component_clause,[],[f227]) ).
tff(f230,plain,
( ~ spl28_21
| spl28_22 ),
inference(avatar_split_clause,[],[f98,f227,f223]) ).
tff(f231,plain,
( ~ spl28_22
| spl28_21 ),
inference(avatar_split_clause,[],[f99,f223,f227]) ).
tff(f233,definition,
( spl28_23
<=> f1(bG9) ),
introduced(definition,[new_symbols(definition,[spl28_23])],[avatar_definition]) ).
tff(f234,plain,
( f1(bG9)
| ~ spl28_23 ),
inference(avatar_component_clause,[],[f233]) ).
tff(f235,plain,
( ~ f1(bG9)
| spl28_23 ),
inference(avatar_component_clause,[],[f233]) ).
tff(f237,definition,
( spl28_24
<=> ( $true = bG10 ) ),
introduced(definition,[new_symbols(definition,[spl28_24])],[avatar_definition]) ).
tff(f239,plain,
( ( $true = bG10 )
| ~ spl28_24 ),
inference(avatar_component_clause,[],[f237]) ).
tff(f240,plain,
( ~ spl28_23
| spl28_24 ),
inference(avatar_split_clause,[],[f96,f237,f233]) ).
tff(f241,plain,
( ~ spl28_24
| spl28_23 ),
inference(avatar_split_clause,[],[f97,f233,f237]) ).
tff(f243,definition,
( spl28_25
<=> f1(bG10) ),
introduced(definition,[new_symbols(definition,[spl28_25])],[avatar_definition]) ).
tff(f244,plain,
( f1(bG10)
| ~ spl28_25 ),
inference(avatar_component_clause,[],[f243]) ).
tff(f245,plain,
( ~ f1(bG10)
| spl28_25 ),
inference(avatar_component_clause,[],[f243]) ).
tff(f247,definition,
( spl28_26
<=> ( $true = bG11 ) ),
introduced(definition,[new_symbols(definition,[spl28_26])],[avatar_definition]) ).
tff(f249,plain,
( ( $true = bG11 )
| ~ spl28_26 ),
inference(avatar_component_clause,[],[f247]) ).
tff(f250,plain,
( ~ spl28_25
| spl28_26 ),
inference(avatar_split_clause,[],[f94,f247,f243]) ).
tff(f251,plain,
( ~ spl28_26
| spl28_25 ),
inference(avatar_split_clause,[],[f95,f243,f247]) ).
tff(f253,definition,
( spl28_27
<=> f1(bG11) ),
introduced(definition,[new_symbols(definition,[spl28_27])],[avatar_definition]) ).
tff(f254,plain,
( f1(bG11)
| ~ spl28_27 ),
inference(avatar_component_clause,[],[f253]) ).
tff(f255,plain,
( ~ f1(bG11)
| spl28_27 ),
inference(avatar_component_clause,[],[f253]) ).
tff(f257,definition,
( spl28_28
<=> ( $true = bG12 ) ),
introduced(definition,[new_symbols(definition,[spl28_28])],[avatar_definition]) ).
tff(f259,plain,
( ( $true = bG12 )
| ~ spl28_28 ),
inference(avatar_component_clause,[],[f257]) ).
tff(f260,plain,
( ~ spl28_27
| spl28_28 ),
inference(avatar_split_clause,[],[f92,f257,f253]) ).
tff(f261,plain,
( ~ spl28_28
| spl28_27 ),
inference(avatar_split_clause,[],[f93,f253,f257]) ).
tff(f263,definition,
( spl28_29
<=> ( $true = bG13 ) ),
introduced(definition,[new_symbols(definition,[spl28_29])],[avatar_definition]) ).
tff(f265,plain,
( ( $true = bG13 )
| ~ spl28_29 ),
inference(avatar_component_clause,[],[f263]) ).
tff(f266,plain,
( ~ spl28_3
| spl28_29 ),
inference(avatar_split_clause,[],[f90,f263,f133]) ).
tff(f267,plain,
( ~ spl28_29
| spl28_3 ),
inference(avatar_split_clause,[],[f91,f133,f263]) ).
tff(f269,definition,
( spl28_30
<=> f6(bG13) ),
introduced(definition,[new_symbols(definition,[spl28_30])],[avatar_definition]) ).
tff(f270,plain,
( f6(bG13)
| ~ spl28_30 ),
inference(avatar_component_clause,[],[f269]) ).
tff(f271,plain,
( ~ f6(bG13)
| spl28_30 ),
inference(avatar_component_clause,[],[f269]) ).
tff(f273,definition,
( spl28_31
<=> ( $true = bG14 ) ),
introduced(definition,[new_symbols(definition,[spl28_31])],[avatar_definition]) ).
tff(f274,plain,
( ( $true != bG14 )
| spl28_31 ),
inference(avatar_component_clause,[],[f273]) ).
tff(f275,plain,
( ( $true = bG14 )
| ~ spl28_31 ),
inference(avatar_component_clause,[],[f273]) ).
tff(f276,plain,
( ~ spl28_30
| spl28_31 ),
inference(avatar_split_clause,[],[f88,f273,f269]) ).
tff(f277,plain,
( ~ spl28_31
| spl28_30 ),
inference(avatar_split_clause,[],[f89,f269,f273]) ).
tff(f279,definition,
( spl28_32
<=> f6(bG14) ),
introduced(definition,[new_symbols(definition,[spl28_32])],[avatar_definition]) ).
tff(f280,plain,
( f6(bG14)
| ~ spl28_32 ),
inference(avatar_component_clause,[],[f279]) ).
tff(f281,plain,
( ~ f6(bG14)
| spl28_32 ),
inference(avatar_component_clause,[],[f279]) ).
tff(f283,definition,
( spl28_33
<=> ( $true = bG15 ) ),
introduced(definition,[new_symbols(definition,[spl28_33])],[avatar_definition]) ).
tff(f284,plain,
( ( $true != bG15 )
| spl28_33 ),
inference(avatar_component_clause,[],[f283]) ).
tff(f285,plain,
( ( $true = bG15 )
| ~ spl28_33 ),
inference(avatar_component_clause,[],[f283]) ).
tff(f286,plain,
( ~ spl28_32
| spl28_33 ),
inference(avatar_split_clause,[],[f86,f283,f279]) ).
tff(f287,plain,
( ~ spl28_33
| spl28_32 ),
inference(avatar_split_clause,[],[f87,f279,f283]) ).
tff(f289,definition,
( spl28_34
<=> f6(bG15) ),
introduced(definition,[new_symbols(definition,[spl28_34])],[avatar_definition]) ).
tff(f290,plain,
( f6(bG15)
| ~ spl28_34 ),
inference(avatar_component_clause,[],[f289]) ).
tff(f291,plain,
( ~ f6(bG15)
| spl28_34 ),
inference(avatar_component_clause,[],[f289]) ).
tff(f293,definition,
( spl28_35
<=> ( $true = bG16 ) ),
introduced(definition,[new_symbols(definition,[spl28_35])],[avatar_definition]) ).
tff(f294,plain,
( ( $true != bG16 )
| spl28_35 ),
inference(avatar_component_clause,[],[f293]) ).
tff(f295,plain,
( ( $true = bG16 )
| ~ spl28_35 ),
inference(avatar_component_clause,[],[f293]) ).
tff(f296,plain,
( ~ spl28_34
| spl28_35 ),
inference(avatar_split_clause,[],[f84,f293,f289]) ).
tff(f297,plain,
( ~ spl28_35
| spl28_34 ),
inference(avatar_split_clause,[],[f85,f289,f293]) ).
tff(f299,definition,
( spl28_36
<=> f5(bG16) ),
introduced(definition,[new_symbols(definition,[spl28_36])],[avatar_definition]) ).
tff(f300,plain,
( f5(bG16)
| ~ spl28_36 ),
inference(avatar_component_clause,[],[f299]) ).
tff(f301,plain,
( ~ f5(bG16)
| spl28_36 ),
inference(avatar_component_clause,[],[f299]) ).
tff(f303,definition,
( spl28_37
<=> ( $true = bG17 ) ),
introduced(definition,[new_symbols(definition,[spl28_37])],[avatar_definition]) ).
tff(f305,plain,
( ( $true = bG17 )
| ~ spl28_37 ),
inference(avatar_component_clause,[],[f303]) ).
tff(f306,plain,
( ~ spl28_36
| spl28_37 ),
inference(avatar_split_clause,[],[f82,f303,f299]) ).
tff(f307,plain,
( ~ spl28_37
| spl28_36 ),
inference(avatar_split_clause,[],[f83,f299,f303]) ).
tff(f309,definition,
( spl28_38
<=> f4(bG17) ),
introduced(definition,[new_symbols(definition,[spl28_38])],[avatar_definition]) ).
tff(f310,plain,
( f4(bG17)
| ~ spl28_38 ),
inference(avatar_component_clause,[],[f309]) ).
tff(f311,plain,
( ~ f4(bG17)
| spl28_38 ),
inference(avatar_component_clause,[],[f309]) ).
tff(f313,definition,
( spl28_39
<=> ( $true = bG18 ) ),
introduced(definition,[new_symbols(definition,[spl28_39])],[avatar_definition]) ).
tff(f314,plain,
( ( $true != bG18 )
| spl28_39 ),
inference(avatar_component_clause,[],[f313]) ).
tff(f315,plain,
( ( $true = bG18 )
| ~ spl28_39 ),
inference(avatar_component_clause,[],[f313]) ).
tff(f316,plain,
( ~ spl28_38
| spl28_39 ),
inference(avatar_split_clause,[],[f80,f313,f309]) ).
tff(f317,plain,
( ~ spl28_39
| spl28_38 ),
inference(avatar_split_clause,[],[f81,f309,f313]) ).
tff(f319,definition,
( spl28_40
<=> f4(bG18) ),
introduced(definition,[new_symbols(definition,[spl28_40])],[avatar_definition]) ).
tff(f320,plain,
( f4(bG18)
| ~ spl28_40 ),
inference(avatar_component_clause,[],[f319]) ).
tff(f321,plain,
( ~ f4(bG18)
| spl28_40 ),
inference(avatar_component_clause,[],[f319]) ).
tff(f323,definition,
( spl28_41
<=> ( $true = bG19 ) ),
introduced(definition,[new_symbols(definition,[spl28_41])],[avatar_definition]) ).
tff(f324,plain,
( ( $true != bG19 )
| spl28_41 ),
inference(avatar_component_clause,[],[f323]) ).
tff(f325,plain,
( ( $true = bG19 )
| ~ spl28_41 ),
inference(avatar_component_clause,[],[f323]) ).
tff(f326,plain,
( ~ spl28_40
| spl28_41 ),
inference(avatar_split_clause,[],[f78,f323,f319]) ).
tff(f327,plain,
( ~ spl28_41
| spl28_40 ),
inference(avatar_split_clause,[],[f79,f319,f323]) ).
tff(f329,definition,
( spl28_42
<=> f4(bG19) ),
introduced(definition,[new_symbols(definition,[spl28_42])],[avatar_definition]) ).
tff(f330,plain,
( f4(bG19)
| ~ spl28_42 ),
inference(avatar_component_clause,[],[f329]) ).
tff(f331,plain,
( ~ f4(bG19)
| spl28_42 ),
inference(avatar_component_clause,[],[f329]) ).
tff(f333,definition,
( spl28_43
<=> ( $true = bG20 ) ),
introduced(definition,[new_symbols(definition,[spl28_43])],[avatar_definition]) ).
tff(f334,plain,
( ( $true != bG20 )
| spl28_43 ),
inference(avatar_component_clause,[],[f333]) ).
tff(f335,plain,
( ( $true = bG20 )
| ~ spl28_43 ),
inference(avatar_component_clause,[],[f333]) ).
tff(f336,plain,
( ~ spl28_42
| spl28_43 ),
inference(avatar_split_clause,[],[f76,f333,f329]) ).
tff(f337,plain,
( ~ spl28_43
| spl28_42 ),
inference(avatar_split_clause,[],[f77,f329,f333]) ).
tff(f339,definition,
( spl28_44
<=> f3(bG20) ),
introduced(definition,[new_symbols(definition,[spl28_44])],[avatar_definition]) ).
tff(f340,plain,
( f3(bG20)
| ~ spl28_44 ),
inference(avatar_component_clause,[],[f339]) ).
tff(f341,plain,
( ~ f3(bG20)
| spl28_44 ),
inference(avatar_component_clause,[],[f339]) ).
tff(f343,definition,
( spl28_45
<=> ( $true = bG21 ) ),
introduced(definition,[new_symbols(definition,[spl28_45])],[avatar_definition]) ).
tff(f345,plain,
( ( $true = bG21 )
| ~ spl28_45 ),
inference(avatar_component_clause,[],[f343]) ).
tff(f346,plain,
( ~ spl28_44
| spl28_45 ),
inference(avatar_split_clause,[],[f74,f343,f339]) ).
tff(f347,plain,
( ~ spl28_45
| spl28_44 ),
inference(avatar_split_clause,[],[f75,f339,f343]) ).
tff(f349,definition,
( spl28_46
<=> f2(bG21) ),
introduced(definition,[new_symbols(definition,[spl28_46])],[avatar_definition]) ).
tff(f350,plain,
( f2(bG21)
| ~ spl28_46 ),
inference(avatar_component_clause,[],[f349]) ).
tff(f351,plain,
( ~ f2(bG21)
| spl28_46 ),
inference(avatar_component_clause,[],[f349]) ).
tff(f353,definition,
( spl28_47
<=> ( $true = bG22 ) ),
introduced(definition,[new_symbols(definition,[spl28_47])],[avatar_definition]) ).
tff(f355,plain,
( ( $true = bG22 )
| ~ spl28_47 ),
inference(avatar_component_clause,[],[f353]) ).
tff(f356,plain,
( ~ spl28_46
| spl28_47 ),
inference(avatar_split_clause,[],[f72,f353,f349]) ).
tff(f357,plain,
( ~ spl28_47
| spl28_46 ),
inference(avatar_split_clause,[],[f73,f349,f353]) ).
tff(f359,definition,
( spl28_48
<=> f2(bG22) ),
introduced(definition,[new_symbols(definition,[spl28_48])],[avatar_definition]) ).
tff(f360,plain,
( f2(bG22)
| ~ spl28_48 ),
inference(avatar_component_clause,[],[f359]) ).
tff(f361,plain,
( ~ f2(bG22)
| spl28_48 ),
inference(avatar_component_clause,[],[f359]) ).
tff(f363,definition,
( spl28_49
<=> ( $true = bG23 ) ),
introduced(definition,[new_symbols(definition,[spl28_49])],[avatar_definition]) ).
tff(f365,plain,
( ( $true = bG23 )
| ~ spl28_49 ),
inference(avatar_component_clause,[],[f363]) ).
tff(f366,plain,
( ~ spl28_48
| spl28_49 ),
inference(avatar_split_clause,[],[f70,f363,f359]) ).
tff(f367,plain,
( ~ spl28_49
| spl28_48 ),
inference(avatar_split_clause,[],[f71,f359,f363]) ).
tff(f369,definition,
( spl28_50
<=> f2(bG23) ),
introduced(definition,[new_symbols(definition,[spl28_50])],[avatar_definition]) ).
tff(f370,plain,
( f2(bG23)
| ~ spl28_50 ),
inference(avatar_component_clause,[],[f369]) ).
tff(f371,plain,
( ~ f2(bG23)
| spl28_50 ),
inference(avatar_component_clause,[],[f369]) ).
tff(f373,definition,
( spl28_51
<=> ( $true = bG24 ) ),
introduced(definition,[new_symbols(definition,[spl28_51])],[avatar_definition]) ).
tff(f374,plain,
( ( $true != bG24 )
| spl28_51 ),
inference(avatar_component_clause,[],[f373]) ).
tff(f375,plain,
( ( $true = bG24 )
| ~ spl28_51 ),
inference(avatar_component_clause,[],[f373]) ).
tff(f376,plain,
( ~ spl28_50
| spl28_51 ),
inference(avatar_split_clause,[],[f68,f373,f369]) ).
tff(f377,plain,
( ~ spl28_51
| spl28_50 ),
inference(avatar_split_clause,[],[f69,f369,f373]) ).
tff(f379,definition,
( spl28_52
<=> f1(bG24) ),
introduced(definition,[new_symbols(definition,[spl28_52])],[avatar_definition]) ).
tff(f380,plain,
( f1(bG24)
| ~ spl28_52 ),
inference(avatar_component_clause,[],[f379]) ).
tff(f381,plain,
( ~ f1(bG24)
| spl28_52 ),
inference(avatar_component_clause,[],[f379]) ).
tff(f383,definition,
( spl28_53
<=> ( $true = bG25 ) ),
introduced(definition,[new_symbols(definition,[spl28_53])],[avatar_definition]) ).
tff(f385,plain,
( ( $true = bG25 )
| ~ spl28_53 ),
inference(avatar_component_clause,[],[f383]) ).
tff(f386,plain,
( ~ spl28_52
| spl28_53 ),
inference(avatar_split_clause,[],[f66,f383,f379]) ).
tff(f387,plain,
( ~ spl28_53
| spl28_52 ),
inference(avatar_split_clause,[],[f67,f379,f383]) ).
tff(f389,definition,
( spl28_54
<=> f0(bG25) ),
introduced(definition,[new_symbols(definition,[spl28_54])],[avatar_definition]) ).
tff(f390,plain,
( f0(bG25)
| ~ spl28_54 ),
inference(avatar_component_clause,[],[f389]) ).
tff(f391,plain,
( ~ f0(bG25)
| spl28_54 ),
inference(avatar_component_clause,[],[f389]) ).
tff(f393,definition,
( spl28_55
<=> ( $true = bG26 ) ),
introduced(definition,[new_symbols(definition,[spl28_55])],[avatar_definition]) ).
tff(f395,plain,
( ( $true = bG26 )
| ~ spl28_55 ),
inference(avatar_component_clause,[],[f393]) ).
tff(f396,plain,
( ~ spl28_54
| spl28_55 ),
inference(avatar_split_clause,[],[f64,f393,f389]) ).
tff(f397,plain,
( ~ spl28_55
| spl28_54 ),
inference(avatar_split_clause,[],[f65,f389,f393]) ).
tff(f399,definition,
( spl28_56
<=> f0(bG26) ),
introduced(definition,[new_symbols(definition,[spl28_56])],[avatar_definition]) ).
tff(f400,plain,
( f0(bG26)
| ~ spl28_56 ),
inference(avatar_component_clause,[],[f399]) ).
tff(f401,plain,
( ~ f0(bG26)
| spl28_56 ),
inference(avatar_component_clause,[],[f399]) ).
tff(f403,definition,
( spl28_57
<=> ( $true = bG27 ) ),
introduced(definition,[new_symbols(definition,[spl28_57])],[avatar_definition]) ).
tff(f404,plain,
( ( $true != bG27 )
| spl28_57 ),
inference(avatar_component_clause,[],[f403]) ).
tff(f405,plain,
( ( $true = bG27 )
| ~ spl28_57 ),
inference(avatar_component_clause,[],[f403]) ).
tff(f406,plain,
( ~ spl28_56
| spl28_57 ),
inference(avatar_split_clause,[],[f62,f403,f399]) ).
tff(f407,plain,
( ~ spl28_57
| spl28_56 ),
inference(avatar_split_clause,[],[f63,f399,f403]) ).
tff(f424,plain,
( ~ f3($false)
| ( $true = bG7 )
| spl28_19 ),
inference(superposition,[],[f215,f121]) ).
tff(f426,plain,
( ~ f2($false)
| ( $true = bG8 )
| spl28_21 ),
inference(superposition,[],[f225,f121]) ).
tff(f434,plain,
( ~ f0($false)
| ( $true = bG12 )
| spl28_1 ),
inference(superposition,[],[f124,f121]) ).
tff(f438,plain,
( ~ f6($false)
| ( $true = bG14 )
| spl28_32 ),
inference(superposition,[],[f281,f121]) ).
tff(f442,plain,
( ~ f5($false)
| ( $true = bG16 )
| spl28_36 ),
inference(superposition,[],[f301,f121]) ).
tff(f446,plain,
( ~ f4($false)
| ( $true = bG18 )
| spl28_40 ),
inference(superposition,[],[f321,f121]) ).
tff(f450,plain,
( ~ f3($false)
| ( $true = bG20 )
| spl28_44 ),
inference(superposition,[],[f341,f121]) ).
tff(f458,plain,
( ~ f1($false)
| ( $true = bG24 )
| spl28_52 ),
inference(superposition,[],[f381,f121]) ).
tff(f464,plain,
( f0($false)
| ( $true = bG27 )
| ~ spl28_2 ),
inference(superposition,[],[f129,f121]) ).
tff(f466,plain,
( f0($false)
| ~ spl28_2
| spl28_57 ),
inference(forward_subsumption_resolution,[],[f464,f404]) ).
tff(f469,plain,
( ~ f1($false)
| spl28_51
| spl28_52 ),
inference(forward_subsumption_resolution,[],[f458,f374]) ).
tff(f473,plain,
( ~ f3($false)
| spl28_43
| spl28_44 ),
inference(forward_subsumption_resolution,[],[f450,f334]) ).
tff(f475,plain,
( ~ f4($false)
| spl28_39
| spl28_40 ),
inference(forward_subsumption_resolution,[],[f446,f314]) ).
tff(f477,plain,
( ~ f5($false)
| spl28_35
| spl28_36 ),
inference(forward_subsumption_resolution,[],[f442,f294]) ).
tff(f479,plain,
( ~ f6($false)
| spl28_31
| spl28_32 ),
inference(forward_subsumption_resolution,[],[f438,f274]) ).
tff(f486,plain,
( ~ f3($false)
| spl28_18
| spl28_19 ),
inference(forward_subsumption_resolution,[],[f424,f208]) ).
tff(f497,plain,
( ( $true = bG12 )
| spl28_1
| ~ spl28_2
| spl28_57 ),
inference(forward_subsumption_resolution,[],[f434,f466]) ).
tff(f498,plain,
( spl28_28
| spl28_1
| ~ spl28_2
| spl28_57 ),
inference(avatar_split_clause,[],[f497,f403,f127,f123,f257]) ).
tff(f499,plain,
( f1($false)
| ( $true = bG11 )
| ~ spl28_27 ),
inference(superposition,[],[f254,f121]) ).
tff(f513,plain,
( ~ f0($true)
| spl28_1
| ~ spl28_28 ),
inference(superposition,[],[f124,f259]) ).
tff(f517,plain,
( ~ f0($true)
| ~ spl28_55
| spl28_56 ),
inference(superposition,[],[f401,f395]) ).
tff(f526,plain,
( ( $true = bG11 )
| ~ spl28_27
| spl28_51
| spl28_52 ),
inference(forward_subsumption_resolution,[],[f499,f469]) ).
tff(f527,plain,
( spl28_26
| ~ spl28_27
| spl28_51
| spl28_52 ),
inference(avatar_split_clause,[],[f526,f379,f373,f253,f247]) ).
tff(f533,plain,
( f1($false)
| ( $true = bG9 )
| ~ spl28_23 ),
inference(superposition,[],[f234,f121]) ).
tff(f534,plain,
( ( $true = bG9 )
| ~ spl28_23
| spl28_51
| spl28_52 ),
inference(forward_subsumption_resolution,[],[f533,f469]) ).
tff(f535,plain,
( $false
| spl28_22
| ~ spl28_23
| spl28_51
| spl28_52 ),
inference(forward_subsumption_resolution,[],[f534,f228]) ).
tff(f536,plain,
( spl28_22
| ~ spl28_23
| spl28_51
| spl28_52 ),
inference(avatar_contradiction_clause,[],[f535]) ).
tff(f538,definition,
( spl28_58
<=> f1($false) ),
introduced(definition,[new_symbols(definition,[spl28_58])],[avatar_definition]) ).
tff(f544,plain,
( ~ f1($false)
| ( $true = bG9 )
| spl28_23 ),
inference(superposition,[],[f235,f121]) ).
tff(f545,plain,
( ~ f1($false)
| spl28_22
| spl28_23 ),
inference(forward_subsumption_resolution,[],[f544,f228]) ).
tff(f546,plain,
( ~ spl28_58
| spl28_22
| spl28_23 ),
inference(avatar_split_clause,[],[f545,f233,f227,f538]) ).
tff(f549,plain,
( f0($true)
| ~ spl28_55
| ~ spl28_56 ),
inference(forward_demodulation,[],[f400,f395]) ).
tff(f551,definition,
( spl28_59
<=> f0($false) ),
introduced(definition,[new_symbols(definition,[spl28_59])],[avatar_definition]) ).
tff(f552,plain,
( ~ f0($false)
| spl28_59 ),
inference(avatar_component_clause,[],[f551]) ).
tff(f554,plain,
( spl28_57
| spl28_59
| ~ spl28_2 ),
inference(avatar_split_clause,[],[f464,f127,f551,f403]) ).
tff(f573,plain,
( ~ f0($true)
| spl28_2
| ~ spl28_57 ),
inference(superposition,[],[f128,f405]) ).
tff(f575,plain,
( $false
| spl28_2
| ~ spl28_55
| ~ spl28_56
| ~ spl28_57 ),
inference(forward_subsumption_resolution,[],[f573,f549]) ).
tff(f576,plain,
( spl28_2
| ~ spl28_55
| ~ spl28_56
| ~ spl28_57 ),
inference(avatar_contradiction_clause,[],[f575]) ).
tff(f578,plain,
( f0($true)
| ~ spl28_2
| ~ spl28_57 ),
inference(forward_demodulation,[],[f129,f405]) ).
tff(f580,plain,
( ~ f0($false)
| ( $true = bG12 )
| spl28_1 ),
inference(superposition,[],[f124,f121]) ).
tff(f586,plain,
( f0($false)
| ( $true = bG26 )
| ~ spl28_56 ),
inference(superposition,[],[f400,f121]) ).
tff(f610,definition,
( spl28_60
<=> f2($false) ),
introduced(definition,[new_symbols(definition,[spl28_60])],[avatar_definition]) ).
tff(f630,plain,
( f2($true)
| ~ spl28_45
| ~ spl28_46 ),
inference(superposition,[],[f350,f345]) ).
tff(f633,plain,
( f2($true)
| ~ spl28_47
| ~ spl28_48 ),
inference(superposition,[],[f360,f355]) ).
tff(f637,plain,
( f2($true)
| ~ spl28_49
| ~ spl28_50 ),
inference(superposition,[],[f370,f365]) ).
tff(f642,plain,
( f3($false)
| ( $true = bG7 )
| ~ spl28_19 ),
inference(superposition,[],[f214,f121]) ).
tff(f643,plain,
( f3($false)
| spl28_18
| ~ spl28_19 ),
inference(forward_subsumption_resolution,[],[f642,f208]) ).
tff(f645,plain,
( ~ f2($true)
| ~ spl28_20
| spl28_21 ),
inference(superposition,[],[f225,f219]) ).
tff(f647,plain,
( $false
| ~ spl28_20
| spl28_21
| ~ spl28_45
| ~ spl28_46 ),
inference(forward_subsumption_resolution,[],[f645,f630]) ).
tff(f648,plain,
( ~ spl28_20
| spl28_21
| ~ spl28_45
| ~ spl28_46 ),
inference(avatar_contradiction_clause,[],[f647]) ).
tff(f659,plain,
( ~ f2($true)
| ~ spl28_45
| spl28_46 ),
inference(superposition,[],[f351,f345]) ).
tff(f662,plain,
( $false
| ~ spl28_20
| spl28_21
| ~ spl28_49
| ~ spl28_50 ),
inference(forward_subsumption_resolution,[],[f645,f637]) ).
tff(f663,plain,
( ~ spl28_20
| spl28_21
| ~ spl28_49
| ~ spl28_50 ),
inference(avatar_contradiction_clause,[],[f662]) ).
tff(f679,plain,
( ( $true = bG7 )
| ~ spl28_19
| spl28_43
| spl28_44 ),
inference(forward_subsumption_resolution,[],[f642,f473]) ).
tff(f680,plain,
( spl28_18
| ~ spl28_19
| spl28_43
| spl28_44 ),
inference(avatar_split_clause,[],[f679,f339,f333,f213,f207]) ).
tff(f686,definition,
( spl28_61
<=> f3($false) ),
introduced(definition,[new_symbols(definition,[spl28_61])],[avatar_definition]) ).
tff(f701,plain,
( f4($false)
| ( $true = bG19 )
| ~ spl28_42 ),
inference(superposition,[],[f330,f121]) ).
tff(f702,plain,
( f4($false)
| spl28_41
| ~ spl28_42 ),
inference(forward_subsumption_resolution,[],[f701,f324]) ).
tff(f705,plain,
( f3($true)
| ~ spl28_14
| ~ spl28_15 ),
inference(superposition,[],[f194,f189]) ).
tff(f708,plain,
( ~ f3($true)
| ~ spl28_16
| spl28_17 ),
inference(superposition,[],[f205,f199]) ).
tff(f710,plain,
( $false
| ~ spl28_14
| ~ spl28_15
| ~ spl28_16
| spl28_17 ),
inference(forward_subsumption_resolution,[],[f708,f705]) ).
tff(f711,plain,
( ~ spl28_14
| ~ spl28_15
| ~ spl28_16
| spl28_17 ),
inference(avatar_contradiction_clause,[],[f710]) ).
tff(f716,plain,
( ~ f3($true)
| ~ spl28_43
| spl28_44 ),
inference(superposition,[],[f341,f335]) ).
tff(f718,plain,
( spl28_61
| spl28_18
| ~ spl28_19 ),
inference(avatar_split_clause,[],[f643,f213,f207,f686]) ).
tff(f720,plain,
( $false
| spl28_39
| spl28_40
| spl28_41
| ~ spl28_42 ),
inference(forward_subsumption_resolution,[],[f702,f475]) ).
tff(f721,plain,
( spl28_39
| spl28_40
| spl28_41
| ~ spl28_42 ),
inference(avatar_contradiction_clause,[],[f720]) ).
tff(f723,definition,
( spl28_62
<=> f4($false) ),
introduced(definition,[new_symbols(definition,[spl28_62])],[avatar_definition]) ).
tff(f731,plain,
( f5($false)
| ( $true = bG3 )
| ~ spl28_11 ),
inference(superposition,[],[f174,f121]) ).
tff(f732,plain,
( ( $true = bG3 )
| ~ spl28_11
| spl28_35
| spl28_36 ),
inference(forward_subsumption_resolution,[],[f731,f477]) ).
tff(f736,plain,
( f5($false)
| ( $true = bG16 )
| ~ spl28_36 ),
inference(superposition,[],[f300,f121]) ).
tff(f737,plain,
( f5($false)
| spl28_35
| ~ spl28_36 ),
inference(forward_subsumption_resolution,[],[f736,f294]) ).
tff(f742,plain,
( ~ f4($true)
| ~ spl28_12
| spl28_13 ),
inference(superposition,[],[f185,f179]) ).
tff(f745,plain,
( f4($true)
| ~ spl28_37
| ~ spl28_38 ),
inference(superposition,[],[f310,f305]) ).
tff(f747,plain,
( $false
| ~ spl28_12
| spl28_13
| ~ spl28_37
| ~ spl28_38 ),
inference(forward_subsumption_resolution,[],[f745,f742]) ).
tff(f748,plain,
( ~ spl28_12
| spl28_13
| ~ spl28_37
| ~ spl28_38 ),
inference(avatar_contradiction_clause,[],[f747]) ).
tff(f749,plain,
( spl28_10
| ~ spl28_11
| spl28_35
| spl28_36 ),
inference(avatar_split_clause,[],[f732,f299,f293,f173,f167]) ).
tff(f751,definition,
( spl28_63
<=> f5($false) ),
introduced(definition,[new_symbols(definition,[spl28_63])],[avatar_definition]) ).
tff(f753,plain,
( f5($false)
| ~ spl28_63 ),
inference(avatar_component_clause,[],[f751]) ).
tff(f762,plain,
( f6($false)
| ( $true = bG15 )
| ~ spl28_34 ),
inference(superposition,[],[f290,f121]) ).
tff(f763,plain,
( f6($false)
| spl28_33
| ~ spl28_34 ),
inference(forward_subsumption_resolution,[],[f762,f284]) ).
tff(f765,plain,
( f5($true)
| ~ spl28_10
| ~ spl28_11 ),
inference(superposition,[],[f174,f169]) ).
tff(f768,plain,
( ~ f5($true)
| ~ spl28_35
| spl28_36 ),
inference(superposition,[],[f301,f295]) ).
tff(f770,plain,
( $false
| ~ spl28_10
| ~ spl28_11
| ~ spl28_35
| spl28_36 ),
inference(forward_subsumption_resolution,[],[f768,f765]) ).
tff(f771,plain,
( ~ spl28_10
| ~ spl28_11
| ~ spl28_35
| spl28_36 ),
inference(avatar_contradiction_clause,[],[f770]) ).
tff(f785,plain,
( f3($true)
| ~ spl28_16
| ~ spl28_17 ),
inference(forward_demodulation,[],[f204,f199]) ).
tff(f791,plain,
( ~ f5($true)
| ~ spl28_10
| spl28_11 ),
inference(superposition,[],[f175,f169]) ).
tff(f794,plain,
( $false
| ~ spl28_16
| ~ spl28_17
| ~ spl28_43
| spl28_44 ),
inference(forward_subsumption_resolution,[],[f716,f785]) ).
tff(f795,plain,
( ~ spl28_16
| ~ spl28_17
| ~ spl28_43
| spl28_44 ),
inference(avatar_contradiction_clause,[],[f794]) ).
tff(f796,plain,
( f3($true)
| ~ spl28_43
| ~ spl28_44 ),
inference(forward_demodulation,[],[f340,f335]) ).
tff(f799,plain,
( f1($false)
| ( $true = bG9 )
| ~ spl28_23 ),
inference(superposition,[],[f234,f121]) ).
tff(f815,plain,
( f1($true)
| ~ spl28_24
| ~ spl28_25 ),
inference(superposition,[],[f244,f239]) ).
tff(f818,plain,
( ~ f1($true)
| ~ spl28_26
| spl28_27 ),
inference(superposition,[],[f255,f249]) ).
tff(f820,plain,
( $false
| ~ spl28_24
| ~ spl28_25
| ~ spl28_26
| spl28_27 ),
inference(forward_subsumption_resolution,[],[f818,f815]) ).
tff(f821,plain,
( ~ spl28_24
| ~ spl28_25
| ~ spl28_26
| spl28_27 ),
inference(avatar_contradiction_clause,[],[f820]) ).
tff(f822,plain,
( ~ f1($true)
| ~ spl28_24
| spl28_25 ),
inference(forward_demodulation,[],[f245,f239]) ).
tff(f824,plain,
( $false
| spl28_1
| ~ spl28_2
| ~ spl28_28
| ~ spl28_57 ),
inference(forward_subsumption_resolution,[],[f513,f578]) ).
tff(f825,plain,
( spl28_1
| ~ spl28_2
| ~ spl28_28
| ~ spl28_57 ),
inference(avatar_contradiction_clause,[],[f824]) ).
tff(f826,plain,
( ~ f0($true)
| ~ spl28_53
| spl28_54 ),
inference(forward_demodulation,[],[f391,f385]) ).
tff(f827,plain,
( spl28_55
| spl28_59
| ~ spl28_56 ),
inference(avatar_split_clause,[],[f586,f399,f551,f393]) ).
tff(f828,plain,
( spl28_28
| ~ spl28_59
| spl28_1 ),
inference(avatar_split_clause,[],[f580,f123,f551,f257]) ).
tff(f831,plain,
( ~ f0($true)
| spl28_2
| ~ spl28_57 ),
inference(forward_demodulation,[],[f128,f405]) ).
tff(f839,plain,
( f0($true)
| ~ spl28_1
| ~ spl28_28 ),
inference(superposition,[],[f125,f259]) ).
tff(f841,plain,
( $false
| ~ spl28_1
| spl28_2
| ~ spl28_28
| ~ spl28_57 ),
inference(forward_subsumption_resolution,[],[f839,f831]) ).
tff(f842,plain,
( ~ spl28_1
| spl28_2
| ~ spl28_28
| ~ spl28_57 ),
inference(avatar_contradiction_clause,[],[f841]) ).
tff(f843,plain,
( ~ f0($true)
| spl28_1
| ~ spl28_28 ),
inference(forward_demodulation,[],[f124,f259]) ).
tff(f844,plain,
( f0($true)
| ~ spl28_53
| ~ spl28_54 ),
inference(forward_demodulation,[],[f390,f385]) ).
tff(f848,plain,
( ~ f0($false)
| ( $true = bG26 )
| spl28_56 ),
inference(superposition,[],[f401,f121]) ).
tff(f851,plain,
( $false
| spl28_1
| ~ spl28_28
| ~ spl28_53
| ~ spl28_54 ),
inference(forward_subsumption_resolution,[],[f844,f843]) ).
tff(f852,plain,
( spl28_1
| ~ spl28_28
| ~ spl28_53
| ~ spl28_54 ),
inference(avatar_contradiction_clause,[],[f851]) ).
tff(f853,plain,
( ~ f3($true)
| ~ spl28_18
| spl28_19 ),
inference(forward_demodulation,[],[f215,f209]) ).
tff(f854,plain,
( spl28_20
| ~ spl28_60
| spl28_21 ),
inference(avatar_split_clause,[],[f426,f223,f610,f217]) ).
tff(f855,plain,
( $false
| ~ spl28_16
| ~ spl28_17
| ~ spl28_18
| spl28_19 ),
inference(forward_subsumption_resolution,[],[f853,f785]) ).
tff(f856,plain,
( ~ spl28_16
| ~ spl28_17
| ~ spl28_18
| spl28_19 ),
inference(avatar_contradiction_clause,[],[f855]) ).
tff(f857,plain,
( ~ f3($true)
| ~ spl28_14
| spl28_15 ),
inference(forward_demodulation,[],[f195,f189]) ).
tff(f858,plain,
( f0($false)
| ( $true = bG25 )
| ~ spl28_54 ),
inference(superposition,[],[f390,f121]) ).
tff(f872,plain,
( $false
| ~ spl28_18
| spl28_19
| ~ spl28_43
| ~ spl28_44 ),
inference(forward_subsumption_resolution,[],[f853,f796]) ).
tff(f873,plain,
( ~ spl28_18
| spl28_19
| ~ spl28_43
| ~ spl28_44 ),
inference(avatar_contradiction_clause,[],[f872]) ).
tff(f874,plain,
( f3($true)
| ~ spl28_18
| ~ spl28_19 ),
inference(forward_demodulation,[],[f214,f209]) ).
tff(f878,plain,
( $false
| ~ spl28_14
| spl28_15
| ~ spl28_18
| ~ spl28_19 ),
inference(forward_subsumption_resolution,[],[f874,f857]) ).
tff(f879,plain,
( ~ spl28_14
| spl28_15
| ~ spl28_18
| ~ spl28_19 ),
inference(avatar_contradiction_clause,[],[f878]) ).
tff(f882,plain,
( spl28_22
| spl28_58
| ~ spl28_23 ),
inference(avatar_split_clause,[],[f799,f233,f538,f227]) ).
tff(f894,plain,
( f2($false)
| ( $true = bG8 )
| ~ spl28_21 ),
inference(superposition,[],[f224,f121]) ).
tff(f895,plain,
( spl28_20
| spl28_60
| ~ spl28_21 ),
inference(avatar_split_clause,[],[f894,f223,f610,f217]) ).
tff(f903,plain,
( f4($true)
| ~ spl28_12
| ~ spl28_13 ),
inference(superposition,[],[f184,f179]) ).
tff(f912,plain,
( f1($true)
| ~ spl28_22
| ~ spl28_23 ),
inference(superposition,[],[f234,f229]) ).
tff(f914,plain,
( $false
| ~ spl28_22
| ~ spl28_23
| ~ spl28_24
| spl28_25 ),
inference(forward_subsumption_resolution,[],[f912,f822]) ).
tff(f915,plain,
( ~ spl28_22
| ~ spl28_23
| ~ spl28_24
| spl28_25 ),
inference(avatar_contradiction_clause,[],[f914]) ).
tff(f916,plain,
( f1($true)
| ~ spl28_24
| ~ spl28_25 ),
inference(forward_demodulation,[],[f244,f239]) ).
tff(f918,plain,
( f1($true)
| ~ spl28_26
| ~ spl28_27 ),
inference(superposition,[],[f254,f249]) ).
tff(f922,plain,
( f4($true)
| ~ spl28_39
| ~ spl28_40 ),
inference(superposition,[],[f320,f315]) ).
tff(f925,plain,
( f4($true)
| ~ spl28_41
| ~ spl28_42 ),
inference(superposition,[],[f330,f325]) ).
tff(f939,plain,
( ~ f1($true)
| ~ spl28_51
| spl28_52 ),
inference(superposition,[],[f381,f375]) ).
tff(f941,plain,
( $false
| ~ spl28_24
| ~ spl28_25
| ~ spl28_51
| spl28_52 ),
inference(forward_subsumption_resolution,[],[f939,f916]) ).
tff(f942,plain,
( ~ spl28_24
| ~ spl28_25
| ~ spl28_51
| spl28_52 ),
inference(avatar_contradiction_clause,[],[f941]) ).
tff(f943,plain,
( ~ f1($true)
| ~ spl28_22
| spl28_23 ),
inference(forward_demodulation,[],[f235,f229]) ).
tff(f945,plain,
( $false
| ~ spl28_22
| spl28_23
| ~ spl28_26
| ~ spl28_27 ),
inference(forward_subsumption_resolution,[],[f918,f943]) ).
tff(f946,plain,
( ~ spl28_22
| spl28_23
| ~ spl28_26
| ~ spl28_27 ),
inference(avatar_contradiction_clause,[],[f945]) ).
tff(f947,plain,
( f0($true)
| ~ spl28_1
| ~ spl28_28 ),
inference(forward_demodulation,[],[f125,f259]) ).
tff(f949,plain,
( f1($true)
| ~ spl28_51
| ~ spl28_52 ),
inference(forward_demodulation,[],[f380,f375]) ).
tff(f950,plain,
( spl28_53
| spl28_59
| ~ spl28_54 ),
inference(avatar_split_clause,[],[f858,f389,f551,f383]) ).
tff(f952,plain,
( ~ f0($false)
| ( $true = bG27 )
| spl28_2 ),
inference(superposition,[],[f128,f121]) ).
tff(f954,plain,
( $false
| ~ spl28_1
| ~ spl28_28
| ~ spl28_55
| spl28_56 ),
inference(forward_subsumption_resolution,[],[f517,f947]) ).
tff(f955,plain,
( ~ spl28_1
| ~ spl28_28
| ~ spl28_55
| spl28_56 ),
inference(avatar_contradiction_clause,[],[f954]) ).
tff(f956,plain,
( $false
| ~ spl28_1
| ~ spl28_28
| ~ spl28_53
| spl28_54 ),
inference(forward_subsumption_resolution,[],[f826,f947]) ).
tff(f957,plain,
( ~ spl28_1
| ~ spl28_28
| ~ spl28_53
| spl28_54 ),
inference(avatar_contradiction_clause,[],[f956]) ).
tff(f958,plain,
( spl28_55
| ~ spl28_59
| spl28_56 ),
inference(avatar_split_clause,[],[f848,f399,f551,f393]) ).
tff(f959,plain,
( ~ f2($true)
| ~ spl28_49
| spl28_50 ),
inference(forward_demodulation,[],[f371,f365]) ).
tff(f961,plain,
( $false
| ~ spl28_47
| ~ spl28_48
| ~ spl28_49
| spl28_50 ),
inference(forward_subsumption_resolution,[],[f959,f633]) ).
tff(f962,plain,
( ~ spl28_47
| ~ spl28_48
| ~ spl28_49
| spl28_50 ),
inference(avatar_contradiction_clause,[],[f961]) ).
tff(f966,plain,
( ~ f2($true)
| ~ spl28_47
| spl28_48 ),
inference(forward_demodulation,[],[f361,f355]) ).
tff(f968,plain,
( ~ f0($false)
| ( $true = bG25 )
| spl28_54 ),
inference(superposition,[],[f391,f121]) ).
tff(f978,plain,
( $false
| ~ spl28_45
| ~ spl28_46
| ~ spl28_47
| spl28_48 ),
inference(forward_subsumption_resolution,[],[f630,f966]) ).
tff(f979,plain,
( ~ spl28_45
| ~ spl28_46
| ~ spl28_47
| spl28_48 ),
inference(avatar_contradiction_clause,[],[f978]) ).
tff(f980,plain,
( ~ f4($true)
| ~ spl28_41
| spl28_42 ),
inference(forward_demodulation,[],[f331,f325]) ).
tff(f982,plain,
( $false
| ~ spl28_12
| ~ spl28_13
| ~ spl28_41
| spl28_42 ),
inference(forward_subsumption_resolution,[],[f980,f903]) ).
tff(f983,plain,
( ~ spl28_12
| ~ spl28_13
| ~ spl28_41
| spl28_42 ),
inference(avatar_contradiction_clause,[],[f982]) ).
tff(f984,plain,
( ~ f4($true)
| ~ spl28_39
| spl28_40 ),
inference(forward_demodulation,[],[f321,f315]) ).
tff(f987,plain,
( $false
| ~ spl28_12
| ~ spl28_13
| ~ spl28_39
| spl28_40 ),
inference(forward_subsumption_resolution,[],[f984,f903]) ).
tff(f988,plain,
( ~ spl28_12
| ~ spl28_13
| ~ spl28_39
| spl28_40 ),
inference(avatar_contradiction_clause,[],[f987]) ).
tff(f995,plain,
( ~ f4($false)
| ( $true = bG19 )
| spl28_42 ),
inference(superposition,[],[f331,f121]) ).
tff(f996,plain,
( spl28_41
| ~ spl28_62
| spl28_42 ),
inference(avatar_split_clause,[],[f995,f329,f723,f323]) ).
tff(f997,plain,
( ~ f3($false)
| ( $true = bG20 )
| spl28_44 ),
inference(superposition,[],[f341,f121]) ).
tff(f998,plain,
( spl28_43
| ~ spl28_61
| spl28_44 ),
inference(avatar_split_clause,[],[f997,f339,f686,f333]) ).
tff(f1001,plain,
( ~ f2($false)
| ( $true = bG22 )
| spl28_48 ),
inference(superposition,[],[f361,f121]) ).
tff(f1002,plain,
( spl28_47
| ~ spl28_60
| spl28_48 ),
inference(avatar_split_clause,[],[f1001,f359,f610,f353]) ).
tff(f1004,plain,
( f2($true)
| ~ spl28_20
| ~ spl28_21 ),
inference(superposition,[],[f224,f219]) ).
tff(f1022,plain,
( $false
| spl28_31
| spl28_32
| spl28_33
| ~ spl28_34 ),
inference(forward_subsumption_resolution,[],[f763,f479]) ).
tff(f1023,plain,
( spl28_31
| spl28_32
| spl28_33
| ~ spl28_34 ),
inference(avatar_contradiction_clause,[],[f1022]) ).
tff(f1025,definition,
( spl28_64
<=> f6($false) ),
introduced(definition,[new_symbols(definition,[spl28_64])],[avatar_definition]) ).
tff(f1037,plain,
( ~ f6($true)
| ~ spl28_4
| spl28_5 ),
inference(superposition,[],[f145,f139]) ).
tff(f1040,plain,
( ~ f6($true)
| ~ spl28_29
| spl28_30 ),
inference(superposition,[],[f271,f265]) ).
tff(f1044,plain,
( f6($true)
| ~ spl28_33
| ~ spl28_34 ),
inference(superposition,[],[f290,f285]) ).
tff(f1046,plain,
( $false
| ~ spl28_4
| spl28_5
| ~ spl28_33
| ~ spl28_34 ),
inference(forward_subsumption_resolution,[],[f1044,f1037]) ).
tff(f1047,plain,
( ~ spl28_4
| spl28_5
| ~ spl28_33
| ~ spl28_34 ),
inference(avatar_contradiction_clause,[],[f1046]) ).
tff(f1048,plain,
( f6($true)
| ~ spl28_4
| ~ spl28_5 ),
inference(forward_demodulation,[],[f144,f139]) ).
tff(f1050,plain,
( f5($true)
| ~ spl28_6
| ~ spl28_7 ),
inference(superposition,[],[f154,f149]) ).
tff(f1052,plain,
( $false
| ~ spl28_6
| ~ spl28_7
| ~ spl28_35
| spl28_36 ),
inference(forward_subsumption_resolution,[],[f1050,f768]) ).
tff(f1053,plain,
( ~ spl28_6
| ~ spl28_7
| ~ spl28_35
| spl28_36 ),
inference(avatar_contradiction_clause,[],[f1052]) ).
tff(f1054,plain,
( f5($true)
| ~ spl28_35
| ~ spl28_36 ),
inference(forward_demodulation,[],[f300,f295]) ).
tff(f1056,plain,
( ~ f4($true)
| ~ spl28_37
| spl28_38 ),
inference(superposition,[],[f311,f305]) ).
tff(f1058,plain,
( $false
| ~ spl28_12
| ~ spl28_13
| ~ spl28_37
| spl28_38 ),
inference(forward_subsumption_resolution,[],[f1056,f903]) ).
tff(f1059,plain,
( ~ spl28_12
| ~ spl28_13
| ~ spl28_37
| spl28_38 ),
inference(avatar_contradiction_clause,[],[f1058]) ).
tff(f1060,plain,
( f5($true)
| ~ spl28_8
| ~ spl28_9 ),
inference(forward_demodulation,[],[f164,f159]) ).
tff(f1061,plain,
( $false
| ~ spl28_10
| spl28_11
| ~ spl28_35
| ~ spl28_36 ),
inference(forward_subsumption_resolution,[],[f791,f1054]) ).
tff(f1062,plain,
( ~ spl28_10
| spl28_11
| ~ spl28_35
| ~ spl28_36 ),
inference(avatar_contradiction_clause,[],[f1061]) ).
tff(f1064,plain,
( ~ f5($true)
| ~ spl28_8
| spl28_9 ),
inference(forward_demodulation,[],[f165,f159]) ).
tff(f1068,plain,
( $false
| ~ spl28_8
| spl28_9
| ~ spl28_35
| ~ spl28_36 ),
inference(forward_subsumption_resolution,[],[f1064,f1054]) ).
tff(f1069,plain,
( ~ spl28_8
| spl28_9
| ~ spl28_35
| ~ spl28_36 ),
inference(avatar_contradiction_clause,[],[f1068]) ).
tff(f1070,plain,
( ~ f5($true)
| ~ spl28_6
| spl28_7 ),
inference(forward_demodulation,[],[f155,f149]) ).
tff(f1071,plain,
( $false
| ~ spl28_6
| spl28_7
| ~ spl28_35
| ~ spl28_36 ),
inference(forward_subsumption_resolution,[],[f1070,f1054]) ).
tff(f1072,plain,
( ~ spl28_6
| spl28_7
| ~ spl28_35
| ~ spl28_36 ),
inference(avatar_contradiction_clause,[],[f1071]) ).
tff(f1073,plain,
( ~ f6($true)
| ~ spl28_33
| spl28_34 ),
inference(forward_demodulation,[],[f291,f285]) ).
tff(f1074,plain,
( spl28_63
| spl28_35
| ~ spl28_36 ),
inference(avatar_split_clause,[],[f737,f299,f293,f751]) ).
tff(f1075,plain,
( $false
| ~ spl28_4
| ~ spl28_5
| ~ spl28_33
| spl28_34 ),
inference(forward_subsumption_resolution,[],[f1073,f1048]) ).
tff(f1076,plain,
( ~ spl28_4
| ~ spl28_5
| ~ spl28_33
| spl28_34 ),
inference(avatar_contradiction_clause,[],[f1075]) ).
tff(f1079,plain,
( ~ f5($false)
| ( $true = bG2 )
| spl28_9 ),
inference(superposition,[],[f165,f121]) ).
tff(f1080,plain,
( spl28_8
| ~ spl28_63
| spl28_9 ),
inference(avatar_split_clause,[],[f1079,f163,f751,f157]) ).
tff(f1081,plain,
( ~ f5($false)
| ( $true = bG3 )
| spl28_11 ),
inference(superposition,[],[f175,f121]) ).
tff(f1082,plain,
( spl28_10
| ~ spl28_63
| spl28_11 ),
inference(avatar_split_clause,[],[f1081,f173,f751,f167]) ).
tff(f1083,plain,
( f6($false)
| ( $true = bG13 )
| ~ spl28_30 ),
inference(superposition,[],[f270,f121]) ).
tff(f1084,plain,
( ~ f5($false)
| ( $true = bG16 )
| spl28_36 ),
inference(superposition,[],[f301,f121]) ).
tff(f1085,plain,
( spl28_35
| ~ spl28_63
| spl28_36 ),
inference(avatar_split_clause,[],[f1084,f299,f751,f293]) ).
tff(f1093,plain,
( $false
| ~ spl28_39
| ~ spl28_40
| ~ spl28_41
| spl28_42 ),
inference(forward_subsumption_resolution,[],[f922,f980]) ).
tff(f1094,plain,
( ~ spl28_39
| ~ spl28_40
| ~ spl28_41
| spl28_42 ),
inference(avatar_contradiction_clause,[],[f1093]) ).
tff(f1096,plain,
( $false
| ~ spl28_20
| ~ spl28_21
| ~ spl28_45
| spl28_46 ),
inference(forward_subsumption_resolution,[],[f659,f1004]) ).
tff(f1097,plain,
( ~ spl28_20
| ~ spl28_21
| ~ spl28_45
| spl28_46 ),
inference(avatar_contradiction_clause,[],[f1096]) ).
tff(f1099,plain,
( f5($false)
| ( $true = bG2 )
| ~ spl28_9 ),
inference(superposition,[],[f164,f121]) ).
tff(f1100,plain,
( spl28_8
| spl28_63
| ~ spl28_9 ),
inference(avatar_split_clause,[],[f1099,f163,f751,f157]) ).
tff(f1101,plain,
( f5($false)
| ( $true = bG3 )
| ~ spl28_11 ),
inference(superposition,[],[f174,f121]) ).
tff(f1102,plain,
( spl28_10
| spl28_63
| ~ spl28_11 ),
inference(avatar_split_clause,[],[f1101,f173,f751,f167]) ).
tff(f1105,plain,
( f3($false)
| ( $true = bG5 )
| ~ spl28_15 ),
inference(superposition,[],[f194,f121]) ).
tff(f1106,plain,
( spl28_14
| spl28_61
| ~ spl28_15 ),
inference(avatar_split_clause,[],[f1105,f193,f686,f187]) ).
tff(f1131,plain,
( f6($true)
| ~ spl28_31
| ~ spl28_32 ),
inference(superposition,[],[f280,f275]) ).
tff(f1133,plain,
( $false
| ~ spl28_31
| ~ spl28_32
| ~ spl28_33
| spl28_34 ),
inference(forward_subsumption_resolution,[],[f1131,f1073]) ).
tff(f1134,plain,
( ~ spl28_31
| ~ spl28_32
| ~ spl28_33
| spl28_34 ),
inference(avatar_contradiction_clause,[],[f1133]) ).
tff(f1135,plain,
( ~ f6($true)
| ~ spl28_31
| spl28_32 ),
inference(forward_demodulation,[],[f281,f275]) ).
tff(f1143,plain,
( spl28_29
| spl28_64
| ~ spl28_30 ),
inference(avatar_split_clause,[],[f1083,f269,f1025,f263]) ).
tff(f1147,plain,
( $false
| ~ spl28_4
| ~ spl28_5
| ~ spl28_31
| spl28_32 ),
inference(forward_subsumption_resolution,[],[f1135,f1048]) ).
tff(f1148,plain,
( ~ spl28_4
| ~ spl28_5
| ~ spl28_31
| spl28_32 ),
inference(avatar_contradiction_clause,[],[f1147]) ).
tff(f1151,plain,
( ~ f6($false)
| ( bG0 = $true )
| spl28_5 ),
inference(superposition,[],[f145,f121]) ).
tff(f1152,plain,
( spl28_4
| ~ spl28_64
| spl28_5 ),
inference(avatar_split_clause,[],[f1151,f143,f1025,f137]) ).
tff(f1153,plain,
( f5($false)
| ( $true = bG1 )
| ~ spl28_7 ),
inference(superposition,[],[f154,f121]) ).
tff(f1154,plain,
( spl28_6
| spl28_63
| ~ spl28_7 ),
inference(avatar_split_clause,[],[f1153,f153,f751,f147]) ).
tff(f1155,plain,
( f6($false)
| ( $true = bG15 )
| ~ spl28_34 ),
inference(superposition,[],[f290,f121]) ).
tff(f1156,plain,
( spl28_33
| spl28_64
| ~ spl28_34 ),
inference(avatar_split_clause,[],[f1155,f289,f1025,f283]) ).
tff(f1164,plain,
( f6($true)
| ~ spl28_29
| ~ spl28_30 ),
inference(superposition,[],[f270,f265]) ).
tff(f1166,plain,
( $false
| ~ spl28_29
| ~ spl28_30
| ~ spl28_31
| spl28_32 ),
inference(forward_subsumption_resolution,[],[f1164,f1135]) ).
tff(f1167,plain,
( ~ spl28_29
| ~ spl28_30
| ~ spl28_31
| spl28_32 ),
inference(avatar_contradiction_clause,[],[f1166]) ).
tff(f1169,plain,
( ~ f1($true)
| ~ spl28_26
| spl28_27 ),
inference(forward_demodulation,[],[f255,f249]) ).
tff(f1170,plain,
( spl28_53
| ~ spl28_59
| spl28_54 ),
inference(avatar_split_clause,[],[f968,f389,f551,f383]) ).
tff(f1171,plain,
( spl28_57
| ~ spl28_59
| spl28_2 ),
inference(avatar_split_clause,[],[f952,f127,f551,f403]) ).
tff(f1179,plain,
( f6($false)
| ( bG0 = $true )
| ~ spl28_5 ),
inference(superposition,[],[f144,f121]) ).
tff(f1180,plain,
( spl28_4
| spl28_64
| ~ spl28_5 ),
inference(avatar_split_clause,[],[f1179,f143,f1025,f137]) ).
tff(f1182,plain,
( ~ f5($false)
| ( $true = bG1 )
| spl28_7 ),
inference(superposition,[],[f155,f121]) ).
tff(f1183,plain,
( ( $true = bG1 )
| spl28_7
| ~ spl28_63 ),
inference(forward_subsumption_resolution,[],[f1182,f753]) ).
tff(f1184,plain,
( spl28_6
| spl28_7
| ~ spl28_63 ),
inference(avatar_split_clause,[],[f1183,f751,f153,f147]) ).
tff(f1192,plain,
( ~ f3($false)
| ( $true = bG5 )
| spl28_15 ),
inference(superposition,[],[f195,f121]) ).
tff(f1195,plain,
( f2($false)
| ( $true = bG21 )
| ~ spl28_46 ),
inference(superposition,[],[f350,f121]) ).
tff(f1196,plain,
( spl28_45
| spl28_60
| ~ spl28_46 ),
inference(avatar_split_clause,[],[f1195,f349,f610,f343]) ).
tff(f1197,plain,
( f2($false)
| ( $true = bG22 )
| ~ spl28_48 ),
inference(superposition,[],[f360,f121]) ).
tff(f1198,plain,
( spl28_47
| spl28_60
| ~ spl28_48 ),
inference(avatar_split_clause,[],[f1197,f359,f610,f353]) ).
tff(f1199,plain,
( f2($false)
| ( $true = bG23 )
| ~ spl28_50 ),
inference(superposition,[],[f370,f121]) ).
tff(f1200,plain,
( spl28_49
| spl28_60
| ~ spl28_50 ),
inference(avatar_split_clause,[],[f1199,f369,f610,f363]) ).
tff(f1201,plain,
( f1($false)
| ( $true = bG24 )
| ~ spl28_52 ),
inference(superposition,[],[f380,f121]) ).
tff(f1202,plain,
( spl28_51
| spl28_58
| ~ spl28_52 ),
inference(avatar_split_clause,[],[f1201,f379,f538,f373]) ).
tff(f1203,plain,
( $false
| ~ spl28_26
| spl28_27
| ~ spl28_51
| ~ spl28_52 ),
inference(forward_subsumption_resolution,[],[f949,f1169]) ).
tff(f1204,plain,
( ~ spl28_26
| spl28_27
| ~ spl28_51
| ~ spl28_52 ),
inference(avatar_contradiction_clause,[],[f1203]) ).
tff(f1205,plain,
( ~ f1($false)
| ( $true = bG11 )
| spl28_27 ),
inference(superposition,[],[f255,f121]) ).
tff(f1206,plain,
( spl28_26
| ~ spl28_58
| spl28_27 ),
inference(avatar_split_clause,[],[f1205,f253,f538,f247]) ).
tff(f1207,plain,
( ~ f1($false)
| ( $true = bG10 )
| spl28_25 ),
inference(superposition,[],[f245,f121]) ).
tff(f1208,plain,
( spl28_24
| ~ spl28_58
| spl28_25 ),
inference(avatar_split_clause,[],[f1207,f243,f538,f237]) ).
tff(f1209,plain,
( $false
| ~ spl28_22
| spl28_23
| ~ spl28_51
| ~ spl28_52 ),
inference(forward_subsumption_resolution,[],[f949,f943]) ).
tff(f1210,plain,
( ~ spl28_22
| spl28_23
| ~ spl28_51
| ~ spl28_52 ),
inference(avatar_contradiction_clause,[],[f1209]) ).
tff(f1212,plain,
( spl28_14
| ~ spl28_61
| spl28_15 ),
inference(avatar_split_clause,[],[f1192,f193,f686,f187]) ).
tff(f1215,plain,
( f4($false)
| ( $true = bG4 )
| ~ spl28_13 ),
inference(superposition,[],[f184,f121]) ).
tff(f1216,plain,
( spl28_12
| spl28_62
| ~ spl28_13 ),
inference(avatar_split_clause,[],[f1215,f183,f723,f177]) ).
tff(f1217,plain,
( f3($false)
| ( $true = bG6 )
| ~ spl28_17 ),
inference(superposition,[],[f204,f121]) ).
tff(f1218,plain,
( spl28_16
| spl28_61
| ~ spl28_17 ),
inference(avatar_split_clause,[],[f1217,f203,f686,f197]) ).
tff(f1219,plain,
( f1($false)
| ( $true = bG10 )
| ~ spl28_25 ),
inference(superposition,[],[f244,f121]) ).
tff(f1220,plain,
( spl28_24
| spl28_58
| ~ spl28_25 ),
inference(avatar_split_clause,[],[f1219,f243,f538,f237]) ).
tff(f1221,plain,
( ~ f6($false)
| ( $true = bG13 )
| spl28_30 ),
inference(superposition,[],[f271,f121]) ).
tff(f1222,plain,
( spl28_29
| ~ spl28_64
| spl28_30 ),
inference(avatar_split_clause,[],[f1221,f269,f1025,f263]) ).
tff(f1225,plain,
( ~ f6($false)
| ( $true = bG15 )
| spl28_34 ),
inference(superposition,[],[f291,f121]) ).
tff(f1226,plain,
( spl28_33
| ~ spl28_64
| spl28_34 ),
inference(avatar_split_clause,[],[f1225,f289,f1025,f283]) ).
tff(f1228,plain,
( f4($false)
| ( $true = bG18 )
| ~ spl28_40 ),
inference(superposition,[],[f320,f121]) ).
tff(f1229,plain,
( spl28_39
| spl28_62
| ~ spl28_40 ),
inference(avatar_split_clause,[],[f1228,f319,f723,f313]) ).
tff(f1230,plain,
( f3($false)
| ( $true = bG20 )
| ~ spl28_44 ),
inference(superposition,[],[f340,f121]) ).
tff(f1232,plain,
( ~ f2($false)
| ( $true = bG21 )
| spl28_46 ),
inference(superposition,[],[f351,f121]) ).
tff(f1233,plain,
( spl28_45
| ~ spl28_60
| spl28_46 ),
inference(avatar_split_clause,[],[f1232,f349,f610,f343]) ).
tff(f1234,plain,
( ~ f2($false)
| ( $true = bG23 )
| spl28_50 ),
inference(superposition,[],[f371,f121]) ).
tff(f1235,plain,
( spl28_49
| ~ spl28_60
| spl28_50 ),
inference(avatar_split_clause,[],[f1234,f369,f610,f363]) ).
tff(f1239,plain,
( $false
| ~ spl28_8
| ~ spl28_9
| ~ spl28_10
| spl28_11 ),
inference(forward_subsumption_resolution,[],[f791,f1060]) ).
tff(f1240,plain,
( ~ spl28_8
| ~ spl28_9
| ~ spl28_10
| spl28_11 ),
inference(avatar_contradiction_clause,[],[f1239]) ).
tff(f1250,plain,
( $false
| ~ spl28_4
| ~ spl28_5
| ~ spl28_29
| spl28_30 ),
inference(forward_subsumption_resolution,[],[f1040,f1048]) ).
tff(f1251,plain,
( ~ spl28_4
| ~ spl28_5
| ~ spl28_29
| spl28_30 ),
inference(avatar_contradiction_clause,[],[f1250]) ).
tff(f1254,plain,
( ~ spl28_61
| spl28_18
| spl28_19 ),
inference(avatar_split_clause,[],[f486,f213,f207,f686]) ).
tff(f1255,plain,
( spl28_43
| spl28_61
| ~ spl28_44 ),
inference(avatar_split_clause,[],[f1230,f339,f686,f333]) ).
tff(f1257,plain,
( ~ f3($false)
| ( $true = bG6 )
| spl28_17 ),
inference(superposition,[],[f205,f121]) ).
tff(f1258,plain,
( spl28_16
| ~ spl28_61
| spl28_17 ),
inference(avatar_split_clause,[],[f1257,f203,f686,f197]) ).
tff(f1259,plain,
( f6($false)
| ( $true = bG14 )
| ~ spl28_32 ),
inference(superposition,[],[f280,f121]) ).
tff(f1260,plain,
( spl28_31
| spl28_64
| ~ spl28_32 ),
inference(avatar_split_clause,[],[f1259,f279,f1025,f273]) ).
tff(f1261,plain,
( f4($false)
| ( $true = bG17 )
| ~ spl28_38 ),
inference(superposition,[],[f310,f121]) ).
tff(f1262,plain,
( spl28_37
| spl28_62
| ~ spl28_38 ),
inference(avatar_split_clause,[],[f1261,f309,f723,f303]) ).
tff(f1263,plain,
( f4($false)
| ( $true = bG19 )
| ~ spl28_42 ),
inference(superposition,[],[f330,f121]) ).
tff(f1264,plain,
( spl28_41
| spl28_62
| ~ spl28_42 ),
inference(avatar_split_clause,[],[f1263,f329,f723,f323]) ).
tff(f1265,plain,
( $false
| ~ spl28_14
| spl28_15
| ~ spl28_43
| ~ spl28_44 ),
inference(forward_subsumption_resolution,[],[f857,f796]) ).
tff(f1266,plain,
( ~ spl28_14
| spl28_15
| ~ spl28_43
| ~ spl28_44 ),
inference(avatar_contradiction_clause,[],[f1265]) ).
tff(f1268,plain,
( f1($false)
| ( $true = bG11 )
| ~ spl28_27 ),
inference(superposition,[],[f254,f121]) ).
tff(f1269,plain,
( spl28_26
| spl28_58
| ~ spl28_27 ),
inference(avatar_split_clause,[],[f1268,f253,f538,f247]) ).
tff(f1270,plain,
( ! [X0: $o] :
( ~ f0((X0))
| ( $true = (X0) ) )
| spl28_59 ),
inference(superposition,[],[f552,f121]) ).
tff(f1273,plain,
( ( $true = bG12 )
| ~ spl28_1
| spl28_59 ),
inference(resolution,[],[f1270,f125]) ).
tff(f1274,plain,
( spl28_28
| ~ spl28_1
| spl28_59 ),
inference(avatar_split_clause,[],[f1273,f551,f123,f257]) ).
tff(f1278,plain,
( ~ f4($false)
| ( $true = bG4 )
| spl28_13 ),
inference(superposition,[],[f185,f121]) ).
tff(f1279,plain,
( spl28_12
| ~ spl28_62
| spl28_13 ),
inference(avatar_split_clause,[],[f1278,f183,f723,f177]) ).
tff(f1281,plain,
( ~ f4($false)
| ( $true = bG17 )
| spl28_38 ),
inference(superposition,[],[f311,f121]) ).
tff(f1282,plain,
( spl28_37
| ~ spl28_62
| spl28_38 ),
inference(avatar_split_clause,[],[f1281,f309,f723,f303]) ).
tff(f1293,plain,
( $false
| ~ spl28_12
| spl28_13
| ~ spl28_41
| ~ spl28_42 ),
inference(forward_subsumption_resolution,[],[f925,f742]) ).
tff(f1294,plain,
( ~ spl28_12
| spl28_13
| ~ spl28_41
| ~ spl28_42 ),
inference(avatar_contradiction_clause,[],[f1293]) ).
cnf(s1,plain,
( spl28_1
| spl28_2 ),
inference(sat_conversion,[],[f130]) ).
cnf(s2,plain,
( ~ spl28_1
| ~ spl28_2 ),
inference(sat_conversion,[],[f131]) ).
cnf(s3,plain,
( ~ spl28_3
| spl28_4 ),
inference(sat_conversion,[],[f140]) ).
cnf(s4,plain,
( spl28_3
| ~ spl28_4 ),
inference(sat_conversion,[],[f141]) ).
cnf(s5,plain,
( ~ spl28_5
| spl28_6 ),
inference(sat_conversion,[],[f150]) ).
cnf(s6,plain,
( spl28_5
| ~ spl28_6 ),
inference(sat_conversion,[],[f151]) ).
cnf(s7,plain,
( ~ spl28_7
| spl28_8 ),
inference(sat_conversion,[],[f160]) ).
cnf(s8,plain,
( spl28_7
| ~ spl28_8 ),
inference(sat_conversion,[],[f161]) ).
cnf(s9,plain,
( ~ spl28_9
| spl28_10 ),
inference(sat_conversion,[],[f170]) ).
cnf(s10,plain,
( spl28_9
| ~ spl28_10 ),
inference(sat_conversion,[],[f171]) ).
cnf(s11,plain,
( ~ spl28_11
| spl28_12 ),
inference(sat_conversion,[],[f180]) ).
cnf(s12,plain,
( spl28_11
| ~ spl28_12 ),
inference(sat_conversion,[],[f181]) ).
cnf(s13,plain,
( ~ spl28_13
| spl28_14 ),
inference(sat_conversion,[],[f190]) ).
cnf(s14,plain,
( spl28_13
| ~ spl28_14 ),
inference(sat_conversion,[],[f191]) ).
cnf(s15,plain,
( ~ spl28_15
| spl28_16 ),
inference(sat_conversion,[],[f200]) ).
cnf(s16,plain,
( spl28_15
| ~ spl28_16 ),
inference(sat_conversion,[],[f201]) ).
cnf(s17,plain,
( ~ spl28_17
| spl28_18 ),
inference(sat_conversion,[],[f210]) ).
cnf(s18,plain,
( spl28_17
| ~ spl28_18 ),
inference(sat_conversion,[],[f211]) ).
cnf(s19,plain,
( ~ spl28_19
| spl28_20 ),
inference(sat_conversion,[],[f220]) ).
cnf(s20,plain,
( spl28_19
| ~ spl28_20 ),
inference(sat_conversion,[],[f221]) ).
cnf(s21,plain,
( ~ spl28_21
| spl28_22 ),
inference(sat_conversion,[],[f230]) ).
cnf(s22,plain,
( spl28_21
| ~ spl28_22 ),
inference(sat_conversion,[],[f231]) ).
cnf(s23,plain,
( ~ spl28_23
| spl28_24 ),
inference(sat_conversion,[],[f240]) ).
cnf(s24,plain,
( spl28_23
| ~ spl28_24 ),
inference(sat_conversion,[],[f241]) ).
cnf(s25,plain,
( ~ spl28_25
| spl28_26 ),
inference(sat_conversion,[],[f250]) ).
cnf(s26,plain,
( spl28_25
| ~ spl28_26 ),
inference(sat_conversion,[],[f251]) ).
cnf(s27,plain,
( ~ spl28_27
| spl28_28 ),
inference(sat_conversion,[],[f260]) ).
cnf(s28,plain,
( spl28_27
| ~ spl28_28 ),
inference(sat_conversion,[],[f261]) ).
cnf(s29,plain,
( ~ spl28_3
| spl28_29 ),
inference(sat_conversion,[],[f266]) ).
cnf(s30,plain,
( spl28_3
| ~ spl28_29 ),
inference(sat_conversion,[],[f267]) ).
cnf(s31,plain,
( ~ spl28_30
| spl28_31 ),
inference(sat_conversion,[],[f276]) ).
cnf(s32,plain,
( spl28_30
| ~ spl28_31 ),
inference(sat_conversion,[],[f277]) ).
cnf(s33,plain,
( ~ spl28_32
| spl28_33 ),
inference(sat_conversion,[],[f286]) ).
cnf(s34,plain,
( spl28_32
| ~ spl28_33 ),
inference(sat_conversion,[],[f287]) ).
cnf(s35,plain,
( ~ spl28_34
| spl28_35 ),
inference(sat_conversion,[],[f296]) ).
cnf(s36,plain,
( spl28_34
| ~ spl28_35 ),
inference(sat_conversion,[],[f297]) ).
cnf(s37,plain,
( ~ spl28_36
| spl28_37 ),
inference(sat_conversion,[],[f306]) ).
cnf(s38,plain,
( spl28_36
| ~ spl28_37 ),
inference(sat_conversion,[],[f307]) ).
cnf(s39,plain,
( ~ spl28_38
| spl28_39 ),
inference(sat_conversion,[],[f316]) ).
cnf(s40,plain,
( spl28_38
| ~ spl28_39 ),
inference(sat_conversion,[],[f317]) ).
cnf(s41,plain,
( ~ spl28_40
| spl28_41 ),
inference(sat_conversion,[],[f326]) ).
cnf(s42,plain,
( spl28_40
| ~ spl28_41 ),
inference(sat_conversion,[],[f327]) ).
cnf(s43,plain,
( ~ spl28_42
| spl28_43 ),
inference(sat_conversion,[],[f336]) ).
cnf(s44,plain,
( spl28_42
| ~ spl28_43 ),
inference(sat_conversion,[],[f337]) ).
cnf(s45,plain,
( ~ spl28_44
| spl28_45 ),
inference(sat_conversion,[],[f346]) ).
cnf(s46,plain,
( spl28_44
| ~ spl28_45 ),
inference(sat_conversion,[],[f347]) ).
cnf(s47,plain,
( ~ spl28_46
| spl28_47 ),
inference(sat_conversion,[],[f356]) ).
cnf(s48,plain,
( spl28_46
| ~ spl28_47 ),
inference(sat_conversion,[],[f357]) ).
cnf(s49,plain,
( ~ spl28_48
| spl28_49 ),
inference(sat_conversion,[],[f366]) ).
cnf(s50,plain,
( spl28_48
| ~ spl28_49 ),
inference(sat_conversion,[],[f367]) ).
cnf(s51,plain,
( ~ spl28_50
| spl28_51 ),
inference(sat_conversion,[],[f376]) ).
cnf(s52,plain,
( spl28_50
| ~ spl28_51 ),
inference(sat_conversion,[],[f377]) ).
cnf(s53,plain,
( ~ spl28_52
| spl28_53 ),
inference(sat_conversion,[],[f386]) ).
cnf(s54,plain,
( spl28_52
| ~ spl28_53 ),
inference(sat_conversion,[],[f387]) ).
cnf(s55,plain,
( ~ spl28_54
| spl28_55 ),
inference(sat_conversion,[],[f396]) ).
cnf(s56,plain,
( spl28_54
| ~ spl28_55 ),
inference(sat_conversion,[],[f397]) ).
cnf(s57,plain,
( ~ spl28_56
| spl28_57 ),
inference(sat_conversion,[],[f406]) ).
cnf(s58,plain,
( spl28_56
| ~ spl28_57 ),
inference(sat_conversion,[],[f407]) ).
cnf(s60,plain,
( spl28_1
| ~ spl28_2
| spl28_28
| spl28_57 ),
inference(sat_conversion,[],[f498]) ).
cnf(s67,plain,
( spl28_26
| ~ spl28_27
| spl28_51
| spl28_52 ),
inference(sat_conversion,[],[f527]) ).
cnf(s70,plain,
( spl28_22
| ~ spl28_23
| spl28_51
| spl28_52 ),
inference(sat_conversion,[],[f536]) ).
cnf(s74,plain,
( spl28_22
| spl28_23
| ~ spl28_58 ),
inference(sat_conversion,[],[f546]) ).
cnf(s77,plain,
( ~ spl28_2
| spl28_57
| spl28_59 ),
inference(sat_conversion,[],[f554]) ).
cnf(s85,plain,
( spl28_2
| ~ spl28_55
| ~ spl28_56
| ~ spl28_57 ),
inference(sat_conversion,[],[f576]) ).
cnf(s106,plain,
( ~ spl28_20
| spl28_21
| ~ spl28_45
| ~ spl28_46 ),
inference(sat_conversion,[],[f648]) ).
cnf(s110,plain,
( ~ spl28_20
| spl28_21
| ~ spl28_49
| ~ spl28_50 ),
inference(sat_conversion,[],[f663]) ).
cnf(s116,plain,
( spl28_18
| ~ spl28_19
| spl28_43
| spl28_44 ),
inference(sat_conversion,[],[f680]) ).
cnf(s125,plain,
( ~ spl28_14
| ~ spl28_15
| ~ spl28_16
| spl28_17 ),
inference(sat_conversion,[],[f711]) ).
cnf(s126,plain,
( spl28_18
| ~ spl28_19
| spl28_61 ),
inference(sat_conversion,[],[f718]) ).
cnf(s127,plain,
( spl28_39
| spl28_40
| spl28_41
| ~ spl28_42 ),
inference(sat_conversion,[],[f721]) ).
cnf(s135,plain,
( ~ spl28_12
| spl28_13
| ~ spl28_37
| ~ spl28_38 ),
inference(sat_conversion,[],[f748]) ).
cnf(s136,plain,
( spl28_10
| ~ spl28_11
| spl28_35
| spl28_36 ),
inference(sat_conversion,[],[f749]) ).
cnf(s141,plain,
( ~ spl28_10
| ~ spl28_11
| ~ spl28_35
| spl28_36 ),
inference(sat_conversion,[],[f771]) ).
cnf(s156,plain,
( ~ spl28_16
| ~ spl28_17
| ~ spl28_43
| spl28_44 ),
inference(sat_conversion,[],[f795]) ).
cnf(s163,plain,
( ~ spl28_24
| ~ spl28_25
| ~ spl28_26
| spl28_27 ),
inference(sat_conversion,[],[f821]) ).
cnf(s165,plain,
( spl28_1
| ~ spl28_2
| ~ spl28_28
| ~ spl28_57 ),
inference(sat_conversion,[],[f825]) ).
cnf(s166,plain,
( spl28_55
| ~ spl28_56
| spl28_59 ),
inference(sat_conversion,[],[f827]) ).
cnf(s167,plain,
( spl28_1
| spl28_28
| ~ spl28_59 ),
inference(sat_conversion,[],[f828]) ).
cnf(s171,plain,
( ~ spl28_1
| spl28_2
| ~ spl28_28
| ~ spl28_57 ),
inference(sat_conversion,[],[f842]) ).
cnf(s176,plain,
( spl28_1
| ~ spl28_28
| ~ spl28_53
| ~ spl28_54 ),
inference(sat_conversion,[],[f852]) ).
cnf(s178,plain,
( spl28_20
| spl28_21
| ~ spl28_60 ),
inference(sat_conversion,[],[f854]) ).
cnf(s179,plain,
( ~ spl28_16
| ~ spl28_17
| ~ spl28_18
| spl28_19 ),
inference(sat_conversion,[],[f856]) ).
cnf(s184,plain,
( ~ spl28_18
| spl28_19
| ~ spl28_43
| ~ spl28_44 ),
inference(sat_conversion,[],[f873]) ).
cnf(s188,plain,
( ~ spl28_14
| spl28_15
| ~ spl28_18
| ~ spl28_19 ),
inference(sat_conversion,[],[f879]) ).
cnf(s192,plain,
( spl28_22
| ~ spl28_23
| spl28_58 ),
inference(sat_conversion,[],[f882]) ).
cnf(s198,plain,
( spl28_20
| ~ spl28_21
| spl28_60 ),
inference(sat_conversion,[],[f895]) ).
cnf(s200,plain,
( ~ spl28_22
| ~ spl28_23
| ~ spl28_24
| spl28_25 ),
inference(sat_conversion,[],[f915]) ).
cnf(s201,plain,
( ~ spl28_24
| ~ spl28_25
| ~ spl28_51
| spl28_52 ),
inference(sat_conversion,[],[f942]) ).
cnf(s202,plain,
( ~ spl28_22
| spl28_23
| ~ spl28_26
| ~ spl28_27 ),
inference(sat_conversion,[],[f946]) ).
cnf(s203,plain,
( spl28_53
| ~ spl28_54
| spl28_59 ),
inference(sat_conversion,[],[f950]) ).
cnf(s206,plain,
( ~ spl28_1
| ~ spl28_28
| ~ spl28_55
| spl28_56 ),
inference(sat_conversion,[],[f955]) ).
cnf(s207,plain,
( ~ spl28_1
| ~ spl28_28
| ~ spl28_53
| spl28_54 ),
inference(sat_conversion,[],[f957]) ).
cnf(s209,plain,
( spl28_55
| spl28_56
| ~ spl28_59 ),
inference(sat_conversion,[],[f958]) ).
cnf(s213,plain,
( ~ spl28_47
| ~ spl28_48
| ~ spl28_49
| spl28_50 ),
inference(sat_conversion,[],[f962]) ).
cnf(s218,plain,
( ~ spl28_45
| ~ spl28_46
| ~ spl28_47
| spl28_48 ),
inference(sat_conversion,[],[f979]) ).
cnf(s225,plain,
( ~ spl28_12
| ~ spl28_13
| ~ spl28_41
| spl28_42 ),
inference(sat_conversion,[],[f983]) ).
cnf(s227,plain,
( ~ spl28_12
| ~ spl28_13
| ~ spl28_39
| spl28_40 ),
inference(sat_conversion,[],[f988]) ).
cnf(s233,plain,
( spl28_41
| spl28_42
| ~ spl28_62 ),
inference(sat_conversion,[],[f996]) ).
cnf(s234,plain,
( spl28_43
| spl28_44
| ~ spl28_61 ),
inference(sat_conversion,[],[f998]) ).
cnf(s236,plain,
( spl28_47
| spl28_48
| ~ spl28_60 ),
inference(sat_conversion,[],[f1002]) ).
cnf(s237,plain,
( spl28_31
| spl28_32
| spl28_33
| ~ spl28_34 ),
inference(sat_conversion,[],[f1023]) ).
cnf(s244,plain,
( ~ spl28_4
| spl28_5
| ~ spl28_33
| ~ spl28_34 ),
inference(sat_conversion,[],[f1047]) ).
cnf(s245,plain,
( ~ spl28_6
| ~ spl28_7
| ~ spl28_35
| spl28_36 ),
inference(sat_conversion,[],[f1053]) ).
cnf(s246,plain,
( ~ spl28_12
| ~ spl28_13
| ~ spl28_37
| spl28_38 ),
inference(sat_conversion,[],[f1059]) ).
cnf(s247,plain,
( ~ spl28_10
| spl28_11
| ~ spl28_35
| ~ spl28_36 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s251,plain,
( ~ spl28_8
| spl28_9
| ~ spl28_35
| ~ spl28_36 ),
inference(sat_conversion,[],[f1069]) ).
cnf(s253,plain,
( ~ spl28_6
| spl28_7
| ~ spl28_35
| ~ spl28_36 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s254,plain,
( spl28_35
| ~ spl28_36
| spl28_63 ),
inference(sat_conversion,[],[f1074]) ).
cnf(s255,plain,
( ~ spl28_4
| ~ spl28_5
| ~ spl28_33
| spl28_34 ),
inference(sat_conversion,[],[f1076]) ).
cnf(s258,plain,
( spl28_8
| spl28_9
| ~ spl28_63 ),
inference(sat_conversion,[],[f1080]) ).
cnf(s259,plain,
( spl28_10
| spl28_11
| ~ spl28_63 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s260,plain,
( spl28_35
| spl28_36
| ~ spl28_63 ),
inference(sat_conversion,[],[f1085]) ).
cnf(s265,plain,
( ~ spl28_39
| ~ spl28_40
| ~ spl28_41
| spl28_42 ),
inference(sat_conversion,[],[f1094]) ).
cnf(s274,plain,
( ~ spl28_20
| ~ spl28_21
| ~ spl28_45
| spl28_46 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s279,plain,
( spl28_8
| ~ spl28_9
| spl28_63 ),
inference(sat_conversion,[],[f1100]) ).
cnf(s280,plain,
( spl28_10
| ~ spl28_11
| spl28_63 ),
inference(sat_conversion,[],[f1102]) ).
cnf(s282,plain,
( spl28_14
| ~ spl28_15
| spl28_61 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s286,plain,
( ~ spl28_31
| ~ spl28_32
| ~ spl28_33
| spl28_34 ),
inference(sat_conversion,[],[f1134]) ).
cnf(s291,plain,
( spl28_29
| ~ spl28_30
| spl28_64 ),
inference(sat_conversion,[],[f1143]) ).
cnf(s294,plain,
( ~ spl28_4
| ~ spl28_5
| ~ spl28_31
| spl28_32 ),
inference(sat_conversion,[],[f1148]) ).
cnf(s298,plain,
( spl28_4
| spl28_5
| ~ spl28_64 ),
inference(sat_conversion,[],[f1152]) ).
cnf(s299,plain,
( spl28_6
| ~ spl28_7
| spl28_63 ),
inference(sat_conversion,[],[f1154]) ).
cnf(s300,plain,
( spl28_33
| ~ spl28_34
| spl28_64 ),
inference(sat_conversion,[],[f1156]) ).
cnf(s301,plain,
( ~ spl28_29
| ~ spl28_30
| ~ spl28_31
| spl28_32 ),
inference(sat_conversion,[],[f1167]) ).
cnf(s305,plain,
( spl28_53
| spl28_54
| ~ spl28_59 ),
inference(sat_conversion,[],[f1170]) ).
cnf(s306,plain,
( spl28_2
| spl28_57
| ~ spl28_59 ),
inference(sat_conversion,[],[f1171]) ).
cnf(s310,plain,
( spl28_4
| ~ spl28_5
| spl28_64 ),
inference(sat_conversion,[],[f1180]) ).
cnf(s311,plain,
( spl28_6
| spl28_7
| ~ spl28_63 ),
inference(sat_conversion,[],[f1184]) ).
cnf(s313,plain,
( spl28_45
| ~ spl28_46
| spl28_60 ),
inference(sat_conversion,[],[f1196]) ).
cnf(s314,plain,
( spl28_47
| ~ spl28_48
| spl28_60 ),
inference(sat_conversion,[],[f1198]) ).
cnf(s315,plain,
( spl28_49
| ~ spl28_50
| spl28_60 ),
inference(sat_conversion,[],[f1200]) ).
cnf(s316,plain,
( spl28_51
| ~ spl28_52
| spl28_58 ),
inference(sat_conversion,[],[f1202]) ).
cnf(s317,plain,
( ~ spl28_26
| spl28_27
| ~ spl28_51
| ~ spl28_52 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s320,plain,
( spl28_26
| spl28_27
| ~ spl28_58 ),
inference(sat_conversion,[],[f1206]) ).
cnf(s321,plain,
( spl28_24
| spl28_25
| ~ spl28_58 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s322,plain,
( ~ spl28_22
| spl28_23
| ~ spl28_51
| ~ spl28_52 ),
inference(sat_conversion,[],[f1210]) ).
cnf(s328,plain,
( spl28_14
| spl28_15
| ~ spl28_61 ),
inference(sat_conversion,[],[f1212]) ).
cnf(s330,plain,
( spl28_12
| ~ spl28_13
| spl28_62 ),
inference(sat_conversion,[],[f1216]) ).
cnf(s331,plain,
( spl28_16
| ~ spl28_17
| spl28_61 ),
inference(sat_conversion,[],[f1218]) ).
cnf(s332,plain,
( spl28_24
| ~ spl28_25
| spl28_58 ),
inference(sat_conversion,[],[f1220]) ).
cnf(s333,plain,
( spl28_29
| spl28_30
| ~ spl28_64 ),
inference(sat_conversion,[],[f1222]) ).
cnf(s335,plain,
( spl28_33
| spl28_34
| ~ spl28_64 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s336,plain,
( spl28_39
| ~ spl28_40
| spl28_62 ),
inference(sat_conversion,[],[f1229]) ).
cnf(s338,plain,
( spl28_45
| spl28_46
| ~ spl28_60 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s339,plain,
( spl28_49
| spl28_50
| ~ spl28_60 ),
inference(sat_conversion,[],[f1235]) ).
cnf(s340,plain,
( ~ spl28_8
| ~ spl28_9
| ~ spl28_10
| spl28_11 ),
inference(sat_conversion,[],[f1240]) ).
cnf(s342,plain,
( ~ spl28_4
| ~ spl28_5
| ~ spl28_29
| spl28_30 ),
inference(sat_conversion,[],[f1251]) ).
cnf(s345,plain,
( spl28_18
| spl28_19
| ~ spl28_61 ),
inference(sat_conversion,[],[f1254]) ).
cnf(s347,plain,
( spl28_43
| ~ spl28_44
| spl28_61 ),
inference(sat_conversion,[],[f1255]) ).
cnf(s348,plain,
( spl28_16
| spl28_17
| ~ spl28_61 ),
inference(sat_conversion,[],[f1258]) ).
cnf(s349,plain,
( spl28_31
| ~ spl28_32
| spl28_64 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s350,plain,
( spl28_37
| ~ spl28_38
| spl28_62 ),
inference(sat_conversion,[],[f1262]) ).
cnf(s351,plain,
( spl28_41
| ~ spl28_42
| spl28_62 ),
inference(sat_conversion,[],[f1264]) ).
cnf(s352,plain,
( ~ spl28_14
| spl28_15
| ~ spl28_43
| ~ spl28_44 ),
inference(sat_conversion,[],[f1266]) ).
cnf(s360,plain,
( spl28_26
| ~ spl28_27
| spl28_58 ),
inference(sat_conversion,[],[f1269]) ).
cnf(s361,plain,
( ~ spl28_1
| spl28_28
| spl28_59 ),
inference(sat_conversion,[],[f1274]) ).
cnf(s362,plain,
( spl28_12
| spl28_13
| ~ spl28_62 ),
inference(sat_conversion,[],[f1279]) ).
cnf(s363,plain,
( spl28_37
| spl28_38
| ~ spl28_62 ),
inference(sat_conversion,[],[f1282]) ).
cnf(s365,plain,
( ~ spl28_12
| spl28_13
| ~ spl28_41
| ~ spl28_42 ),
inference(sat_conversion,[],[f1294]) ).
cnf(s366,plain,
( spl28_23
| spl28_51
| spl28_22
| spl28_1 ),
inference(rat,[],[s166,s56,s58,s203,s60,s167,s28,s360,s26,s54,s332,s316,s24,s74,s1]) ).
cnf(s367,plain,
( ~ spl28_28
| ~ spl28_53
| spl28_1 ),
inference(rat,[],[s209,s57,s77,s56,s165,s176,s1]) ).
cnf(s368,plain,
( spl28_51
| spl28_22
| spl28_1 ),
inference(rat,[],[s163,s26,s320,s27,s367,s53,s23,s70,s192,s366]) ).
cnf(s369,plain,
( spl28_21
| spl28_20
| spl28_45
| spl28_1 ),
inference(rat,[],[s368,s52,s315,s50,s314,s48,s313,s22,s178]) ).
cnf(s370,plain,
( spl28_50
| ~ spl28_49
| ~ spl28_47 ),
inference(rat,[],[s50,s213]) ).
cnf(s371,plain,
( spl28_50
| ~ spl28_47
| ~ spl28_60 ),
inference(rat,[],[s370,s339]) ).
cnf(s372,plain,
( ~ spl28_23
| ~ spl28_51
| ~ spl28_22
| spl28_1 ),
inference(rat,[],[s367,s27,s53,s317,s201,s25,s200,s23]) ).
cnf(s373,plain,
( spl28_28
| spl28_53
| spl28_1 ),
inference(rat,[],[s166,s56,s58,s203,s60,s167,s1]) ).
cnf(s374,plain,
( ~ spl28_51
| ~ spl28_22
| spl28_1 ),
inference(rat,[],[s321,s360,s25,s202,s28,s373,s54,s24,s322,s372]) ).
cnf(s375,plain,
( spl28_20
| spl28_45
| spl28_1 ),
inference(rat,[],[s374,s51,s371,s47,s338,s21,s198,s369]) ).
cnf(s376,plain,
( spl28_15
| spl28_43
| spl28_14
| spl28_1 ),
inference(rat,[],[s375,s20,s126,s18,s46,s331,s347,s16,s328]) ).
cnf(s377,plain,
( ~ spl28_46
| spl28_50
| ~ spl28_45 ),
inference(rat,[],[s49,s370,s218,s47]) ).
cnf(s378,plain,
( spl28_19
| ~ spl28_16
| ~ spl28_61 ),
inference(rat,[],[s179,s18,s345]) ).
cnf(s379,plain,
( spl28_51
| ~ spl28_20
| ~ spl28_45
| spl28_1 ),
inference(rat,[],[s274,s22,s377,s368,s51]) ).
cnf(s380,plain,
( ~ spl28_20
| ~ spl28_45
| spl28_1 ),
inference(rat,[],[s236,s48,s49,s315,s106,s110,s21,s374,s52,s379]) ).
cnf(s381,plain,
( spl28_43
| spl28_14
| spl28_1 ),
inference(rat,[],[s380,s19,s378,s45,s234,s15,s282,s376]) ).
cnf(s382,plain,
( spl28_13
| spl28_12
| spl28_37
| spl28_1 ),
inference(rat,[],[s381,s44,s351,s42,s336,s40,s350,s14,s362]) ).
cnf(s383,plain,
( spl28_42
| ~ spl28_39
| ~ spl28_62 ),
inference(rat,[],[s265,s42,s233]) ).
cnf(s384,plain,
( spl28_61
| ~ spl28_19
| spl28_44
| ~ spl28_43 ),
inference(rat,[],[s156,s331,s18,s126]) ).
cnf(s385,plain,
( spl28_16
| ~ spl28_61
| ~ spl28_19
| ~ spl28_14 ),
inference(rat,[],[s188,s17,s15,s348]) ).
cnf(s386,plain,
( spl28_45
| ~ spl28_43
| ~ spl28_14
| spl28_1 ),
inference(rat,[],[s156,s125,s16,s385,s384,s20,s375,s45]) ).
cnf(s387,plain,
( ~ spl28_43
| ~ spl28_14
| spl28_1 ),
inference(rat,[],[s17,s125,s184,s15,s19,s352,s380,s46,s386]) ).
cnf(s388,plain,
( spl28_12
| spl28_37
| spl28_1 ),
inference(rat,[],[s387,s43,s383,s39,s363,s330,s13,s382]) ).
cnf(s389,plain,
( spl28_7
| spl28_35
| spl28_6
| spl28_1 ),
inference(rat,[],[s388,s12,s136,s10,s38,s279,s254,s8,s311]) ).
cnf(s390,plain,
( spl28_11
| ~ spl28_63
| ~ spl28_8 ),
inference(rat,[],[s340,s10,s259]) ).
cnf(s391,plain,
( spl28_43
| ~ spl28_12
| ~ spl28_37
| spl28_1 ),
inference(rat,[],[s227,s39,s41,s246,s225,s14,s381,s43]) ).
cnf(s392,plain,
( ~ spl28_12
| ~ spl28_37
| spl28_1 ),
inference(rat,[],[s40,s127,s41,s135,s365,s13,s387,s44,s391]) ).
cnf(s393,plain,
( spl28_35
| spl28_6
| spl28_1 ),
inference(rat,[],[s392,s11,s390,s37,s260,s299,s7,s389]) ).
cnf(s394,plain,
( spl28_5
| spl28_3
| spl28_1 ),
inference(rat,[],[s393,s36,s300,s34,s349,s32,s291,s6,s298,s30,s4]) ).
cnf(s395,plain,
( spl28_34
| ~ spl28_31
| ~ spl28_64 ),
inference(rat,[],[s286,s34,s335]) ).
cnf(s396,plain,
( spl28_12
| spl28_3
| spl28_1 ),
inference(rat,[],[s251,s9,s7,s247,s253,s38,s388,s11,s5,s35,s395,s31,s333,s30,s310,s394,s4]) ).
cnf(s397,plain,
( spl28_3
| spl28_1 ),
inference(rat,[],[s258,s280,s9,s8,s141,s245,s37,s392,s12,s396,s35,s395,s31,s333,s5,s310,s394,s4,s30]) ).
cnf(s398,plain,
( spl28_35
| spl28_1 ),
inference(rat,[],[s294,s33,s31,s255,s342,s6,s393,s35,s29,s3,s397]) ).
cnf(s399,plain,
( spl28_33
| spl28_1 ),
inference(rat,[],[s301,s32,s237,s33,s29,s397,s36,s398]) ).
cnf(s400,plain,
( spl28_12
| spl28_1 ),
inference(rat,[],[s251,s7,s9,s253,s247,s38,s388,s11,s5,s244,s399,s3,s397,s36,s398]) ).
cnf(s401,plain,
spl28_1,
inference(rat,[],[s258,s280,s9,s8,s141,s245,s37,s392,s12,s400,s5,s244,s399,s36,s398,s3,s397]) ).
cnf(s402,plain,
~ spl28_2,
inference(rat,[],[s2,s401]) ).
cnf(s403,plain,
( ~ spl28_28
| ~ spl28_53 ),
inference(rat,[],[s206,s57,s55,s171,s207,s402,s401]) ).
cnf(s404,plain,
( ~ spl28_23
| spl28_22
| spl28_51 ),
inference(rat,[],[s163,s26,s320,s27,s403,s53,s23,s70,s192]) ).
cnf(s405,plain,
( ~ spl28_59
| spl28_53 ),
inference(rat,[],[s85,s58,s55,s306,s305,s402]) ).
cnf(s406,plain,
( spl28_22
| spl28_51 ),
inference(rat,[],[s405,s361,s28,s67,s26,s54,s332,s316,s24,s74,s404,s401]) ).
cnf(s407,plain,
( spl28_51
| spl28_20
| spl28_45 ),
inference(rat,[],[s47,s371,s338,s198,s22,s406,s51]) ).
cnf(s408,plain,
( spl28_60
| ~ spl28_50
| spl28_45 ),
inference(rat,[],[s314,s50,s48,s315,s313]) ).
cnf(s409,plain,
( ~ spl28_53
| ~ spl28_22
| ~ spl28_51 ),
inference(rat,[],[s25,s200,s317,s23,s27,s322,s403,s54]) ).
cnf(s410,plain,
( ~ spl28_23
| ~ spl28_22
| ~ spl28_51 ),
inference(rat,[],[s201,s200,s23,s53,s409]) ).
cnf(s411,plain,
( ~ spl28_22
| ~ spl28_51 ),
inference(rat,[],[s321,s360,s25,s202,s24,s410,s28,s361,s405,s409,s401]) ).
cnf(s412,plain,
( spl28_20
| spl28_45 ),
inference(rat,[],[s411,s21,s178,s408,s52,s407]) ).
cnf(s413,plain,
( ~ spl28_62
| spl28_42
| spl28_37 ),
inference(rat,[],[s39,s383,s363]) ).
cnf(s414,plain,
( spl28_45
| spl28_14
| spl28_43 ),
inference(rat,[],[s331,s18,s16,s116,s282,s20,s234,s412,s45]) ).
cnf(s415,plain,
( ~ spl28_51
| ~ spl28_20
| ~ spl28_45 ),
inference(rat,[],[s236,s48,s49,s315,s106,s110,s21,s411,s52]) ).
cnf(s416,plain,
( ~ spl28_20
| ~ spl28_45 ),
inference(rat,[],[s274,s22,s377,s406,s51,s415]) ).
cnf(s417,plain,
( spl28_14
| spl28_43 ),
inference(rat,[],[s416,s19,s378,s15,s328,s347,s46,s414]) ).
cnf(s418,plain,
( spl28_43
| spl28_37
| spl28_12 ),
inference(rat,[],[s417,s14,s330,s413,s43]) ).
cnf(s419,plain,
( spl28_62
| ~ spl28_42
| spl28_37 ),
inference(rat,[],[s336,s42,s40,s351,s350]) ).
cnf(s420,plain,
( spl28_45
| ~ spl28_14
| ~ spl28_43 ),
inference(rat,[],[s156,s125,s16,s385,s384,s20,s412,s45]) ).
cnf(s421,plain,
( ~ spl28_14
| ~ spl28_43 ),
inference(rat,[],[s17,s125,s184,s15,s19,s352,s416,s46,s420]) ).
cnf(s422,plain,
( spl28_37
| spl28_12 ),
inference(rat,[],[s421,s13,s362,s419,s44,s418]) ).
cnf(s423,plain,
( spl28_4
| ~ spl28_5
| spl28_34 ),
inference(rat,[],[s31,s395,s333,s30,s310,s3]) ).
cnf(s424,plain,
( ~ spl28_5
| spl28_34 ),
inference(rat,[],[s31,s294,s342,s33,s29,s255,s4,s423]) ).
cnf(s425,plain,
( spl28_35
| spl28_12 ),
inference(rat,[],[s424,s6,s311,s7,s390,s254,s35,s11,s38,s422]) ).
cnf(s426,plain,
( spl28_4
| spl28_12 ),
inference(rat,[],[s349,s34,s32,s300,s291,s30,s298,s3,s36,s5,s253,s7,s251,s9,s247,s11,s425,s38,s422]) ).
cnf(s427,plain,
spl28_12,
inference(rat,[],[s301,s32,s237,s33,s29,s244,s4,s426,s5,s253,s7,s251,s9,s36,s247,s425,s38,s422,s11]) ).
cnf(s428,plain,
spl28_11,
inference(rat,[],[s12,s427]) ).
cnf(s429,plain,
( spl28_35
| spl28_6
| spl28_36 ),
inference(rat,[],[s279,s8,s10,s299,s136,s260,s428]) ).
cnf(s430,plain,
( spl28_4
| ~ spl28_34
| spl28_5 ),
inference(rat,[],[s349,s34,s32,s300,s291,s30,s298,s3]) ).
cnf(s431,plain,
( ~ spl28_34
| spl28_5 ),
inference(rat,[],[s301,s32,s237,s33,s29,s244,s4,s430]) ).
cnf(s432,plain,
( spl28_5
| spl28_36 ),
inference(rat,[],[s431,s36,s429,s6]) ).
cnf(s433,plain,
( ~ spl28_35
| spl28_36
| ~ spl28_6 ),
inference(rat,[],[s258,s280,s9,s8,s141,s245,s428]) ).
cnf(s434,plain,
spl28_36,
inference(rat,[],[s433,s35,s424,s5,s432]) ).
cnf(s435,plain,
spl28_37,
inference(rat,[],[s37,s434]) ).
cnf(s436,plain,
spl28_13,
inference(rat,[],[s127,s41,s365,s44,s417,s40,s14,s135,s427,s435]) ).
cnf(s437,plain,
spl28_14,
inference(rat,[],[s13,s436]) ).
cnf(s438,plain,
spl28_38,
inference(rat,[],[s246,s435,s427,s436]) ).
cnf(s439,plain,
~ spl28_43,
inference(rat,[],[s421,s437]) ).
cnf(s440,plain,
spl28_39,
inference(rat,[],[s39,s438]) ).
cnf(s441,plain,
~ spl28_42,
inference(rat,[],[s43,s439]) ).
cnf(s442,plain,
spl28_40,
inference(rat,[],[s227,s436,s427,s440]) ).
cnf(s444,plain,
~ spl28_41,
inference(rat,[],[s225,s436,s427,s441]) ).
cnf(s445,plain,
$false,
inference(rat,[],[s41,s444,s442]) ).
tff(f1295,plain,
$false,
inference(avatar_sat_refutation,[],[s445]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500_8.007 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.20 % Computer : n006.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Mon Sep 28 17:46:25 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 Running first-order theorem proving
% 0.10/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.90/0.93 % (4192238)Detected formulas, will run a generic FOF schedule.
% 2.90/0.93 % (4192251)dis-21_1_sil=8000:lcm=predicate:random_seed=262479010:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/129Mi)
% 2.90/0.93 % (4192251)Refutation not found, incomplete strategy
% 2.90/0.93 % (4192251)------------------------------
% 2.90/0.93 % (4192251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.90/0.93 % (4192251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.90/0.93 % (4192251)CaDiCaL version: 2.1.3
% 2.90/0.93 % (4192251)Termination reason: Refutation not found, incomplete strategy
% 2.90/0.93 % (4192251)Time elapsed: 0.002 s
% 2.90/0.93 % (4192251)Peak memory usage: 89 MB
% 2.90/0.93 % (4192251)Instructions burned: 4 (million)
% 2.90/0.93 % (4192250)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=898585326:s2a=on:i=139:gtg=position_3000 on theBenchmark for (3000ds/139Mi)
% 2.90/0.93 % (4192248)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2935596513:i=109:sd=1:ins=1:gsp=on:ss=axioms_3000 on theBenchmark for (3000ds/109Mi)
% 2.90/0.93 % (4192245)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=2228621788:i=141193_3000 on theBenchmark for (3000ds/141193Mi)
% 2.90/0.93 % (4192246)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=1039506682:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_3000 on theBenchmark for (3000ds/134677Mi)
% 2.90/0.93 % (4192247)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=184682566:i=141695:sd=1:nm=32:gsp=on:ss=included_3000 on theBenchmark for (3000ds/141695Mi)
% 2.90/0.93 % (4192248)Refutation not found, incomplete strategy
% 2.90/0.93 % (4192248)------------------------------
% 2.90/0.93 % (4192248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.90/0.93 % (4192248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.90/0.93 % (4192248)CaDiCaL version: 2.1.3
% 2.90/0.93 % (4192248)Termination reason: Refutation not found, incomplete strategy
% 2.90/0.93 % (4192248)Time elapsed: 0.002 s
% 2.90/0.93 % (4192248)Peak memory usage: 88 MB
% 2.90/0.93 % (4192248)Instructions burned: 1 (million)
% 2.90/0.93 % (4192250)First to succeed.
% 2.90/0.93 % (4192250)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4192238"
% 2.90/0.93 % (4192249)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=888523750:i=119:av=off:ss=axioms_3000 on theBenchmark for (3000ds/119Mi)
% 2.90/0.93 % (4192249)Instruction limit reached!
% 2.90/0.93 % (4192249)------------------------------
% 2.90/0.93 % (4192249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.90/0.93 % (4192249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.90/0.93 % (4192249)CaDiCaL version: 2.1.3
% 2.90/0.93 % (4192249)Termination reason: Instruction limit
% 2.90/0.93 % (4192249)Termination phase: Saturation
% 2.90/0.93 % (4192249)Time elapsed: 0.056 s
% 2.90/0.93 % (4192249)Peak memory usage: 88 MB
% 2.90/0.93 % (4192249)Instructions burned: 120 (million)
% 2.90/0.93 % (4192251)------------------------------
% 2.90/0.93 % (4192251)------------------------------
% 2.90/0.93 % (4192261)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2095676365:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 2.90/0.93 % (4192261)Instruction limit reached!
% 2.90/0.93 % (4192261)------------------------------
% 2.90/0.93 % (4192261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.90/0.93 % (4192261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.90/0.93 % (4192261)CaDiCaL version: 2.1.3
% 2.90/0.93 % (4192261)Termination reason: Instruction limit
% 2.90/0.93 % (4192261)Termination phase: Saturation
% 2.90/0.93 % (4192261)Time elapsed: 0.036 s
% 2.90/0.93 % (4192261)Peak memory usage: 89 MB
% 2.90/0.93 % (4192261)Instructions burned: 158 (million)
% 2.90/0.93 % (4192248)------------------------------
% 2.90/0.93 % (4192248)------------------------------
% 2.90/0.93 % (4192260)lrs+10_1_sil=8000:sp=occurrence:random_seed=3686353744:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 2.90/0.93 % (4192250)Refutation found. Thanks to Tanya!
% 2.90/0.93 % SZS status Theorem for theBenchmark
% 2.90/0.93 % SZS output start Proof for theBenchmark
% See solution above
% 2.90/1.03 % (4192250)------------------------------
% 2.90/1.03 % (4192250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.90/1.03 % (4192250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.90/1.03 % (4192250)CaDiCaL version: 2.1.3
% 2.90/1.03 % (4192250)Termination reason: Refutation
% 2.90/1.03 % (4192250)Time elapsed: 0.034 s
% 2.90/1.03 % (4192250)Peak memory usage: 90 MB
% 2.90/1.03 % (4192250)Instructions burned: 48 (million)
% 2.90/1.03 % (4192250)------------------------------
% 2.90/1.03 % (4192250)------------------------------
% 2.90/1.03 % (4192238)Success in time 0.411 s
% 2.90/1.03 % Vampire exiting
%------------------------------------------------------------------------------