%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO500_8.008 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:54 PM UTC 2026
% Result : Theorem 2.65s 0.87s
% Output : Refutation 3.60s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% 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(func_def_30,type,
bG28: $o ).
tff(func_def_31,type,
bG29: $o ).
tff(func_def_32,type,
bG30: $o ).
tff(func_def_33,type,
bG31: $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(pred_def_9,type,
f7: $o > $o ).
tff(f1,conjecture,
f0(f0(f0(f1(f2(f2(f2(f3(f4(f4(f4(f5(f6(f6(f6(f7(x)))))))))))))))) = f0(f1(f1(f1(f2(f3(f3(f3(f4(f5(f5(f5(f6(f7(f7(f7(x)))))))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kaminski8) ).
tff(f2,negated_conjecture,
f0(f0(f0(f1(f2(f2(f2(f3(f4(f4(f4(f5(f6(f6(f6(f7(x)))))))))))))))) != f0(f1(f1(f1(f2(f3(f3(f3(f4(f5(f5(f5(f6(f7(f7(f7(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,
( f7(bG0)
<=> ( $true = bG1 ) ),
introduced(definition,[new_symbols(definition,[bG1])],[fool_formula_definition]) ).
tff(f5,definition,
( f6(bG1)
<=> ( $true = bG2 ) ),
introduced(definition,[new_symbols(definition,[bG2])],[fool_formula_definition]) ).
tff(f6,definition,
( f6(bG2)
<=> ( $true = bG3 ) ),
introduced(definition,[new_symbols(definition,[bG3])],[fool_formula_definition]) ).
tff(f7,definition,
( f6(bG3)
<=> ( $true = bG4 ) ),
introduced(definition,[new_symbols(definition,[bG4])],[fool_formula_definition]) ).
tff(f8,definition,
( f5(bG4)
<=> ( $true = bG5 ) ),
introduced(definition,[new_symbols(definition,[bG5])],[fool_formula_definition]) ).
tff(f9,definition,
( f4(bG5)
<=> ( $true = bG6 ) ),
introduced(definition,[new_symbols(definition,[bG6])],[fool_formula_definition]) ).
tff(f10,definition,
( f4(bG6)
<=> ( $true = bG7 ) ),
introduced(definition,[new_symbols(definition,[bG7])],[fool_formula_definition]) ).
tff(f11,definition,
( f4(bG7)
<=> ( $true = bG8 ) ),
introduced(definition,[new_symbols(definition,[bG8])],[fool_formula_definition]) ).
tff(f12,definition,
( f3(bG8)
<=> ( $true = bG9 ) ),
introduced(definition,[new_symbols(definition,[bG9])],[fool_formula_definition]) ).
tff(f13,definition,
( f2(bG9)
<=> ( $true = bG10 ) ),
introduced(definition,[new_symbols(definition,[bG10])],[fool_formula_definition]) ).
tff(f14,definition,
( f2(bG10)
<=> ( $true = bG11 ) ),
introduced(definition,[new_symbols(definition,[bG11])],[fool_formula_definition]) ).
tff(f15,definition,
( f2(bG11)
<=> ( $true = bG12 ) ),
introduced(definition,[new_symbols(definition,[bG12])],[fool_formula_definition]) ).
tff(f16,definition,
( f1(bG12)
<=> ( $true = bG13 ) ),
introduced(definition,[new_symbols(definition,[bG13])],[fool_formula_definition]) ).
tff(f17,definition,
( f0(bG13)
<=> ( $true = bG14 ) ),
introduced(definition,[new_symbols(definition,[bG14])],[fool_formula_definition]) ).
tff(f18,definition,
( f0(bG14)
<=> ( $true = bG15 ) ),
introduced(definition,[new_symbols(definition,[bG15])],[fool_formula_definition]) ).
tff(f19,definition,
( x
<=> ( $true = bG16 ) ),
introduced(definition,[new_symbols(definition,[bG16])],[fool_formula_definition]) ).
tff(f20,definition,
( f7(bG16)
<=> ( $true = bG17 ) ),
introduced(definition,[new_symbols(definition,[bG17])],[fool_formula_definition]) ).
tff(f21,definition,
( f7(bG17)
<=> ( $true = bG18 ) ),
introduced(definition,[new_symbols(definition,[bG18])],[fool_formula_definition]) ).
tff(f22,definition,
( f7(bG18)
<=> ( $true = bG19 ) ),
introduced(definition,[new_symbols(definition,[bG19])],[fool_formula_definition]) ).
tff(f23,definition,
( f6(bG19)
<=> ( $true = bG20 ) ),
introduced(definition,[new_symbols(definition,[bG20])],[fool_formula_definition]) ).
tff(f24,definition,
( f5(bG20)
<=> ( $true = bG21 ) ),
introduced(definition,[new_symbols(definition,[bG21])],[fool_formula_definition]) ).
tff(f25,definition,
( f5(bG21)
<=> ( $true = bG22 ) ),
introduced(definition,[new_symbols(definition,[bG22])],[fool_formula_definition]) ).
tff(f26,definition,
( f5(bG22)
<=> ( $true = bG23 ) ),
introduced(definition,[new_symbols(definition,[bG23])],[fool_formula_definition]) ).
tff(f27,definition,
( f4(bG23)
<=> ( $true = bG24 ) ),
introduced(definition,[new_symbols(definition,[bG24])],[fool_formula_definition]) ).
tff(f28,definition,
( f3(bG24)
<=> ( $true = bG25 ) ),
introduced(definition,[new_symbols(definition,[bG25])],[fool_formula_definition]) ).
tff(f29,definition,
( f3(bG25)
<=> ( $true = bG26 ) ),
introduced(definition,[new_symbols(definition,[bG26])],[fool_formula_definition]) ).
tff(f30,definition,
( f3(bG26)
<=> ( $true = bG27 ) ),
introduced(definition,[new_symbols(definition,[bG27])],[fool_formula_definition]) ).
tff(f31,definition,
( f2(bG27)
<=> ( $true = bG28 ) ),
introduced(definition,[new_symbols(definition,[bG28])],[fool_formula_definition]) ).
tff(f32,definition,
( f1(bG28)
<=> ( $true = bG29 ) ),
introduced(definition,[new_symbols(definition,[bG29])],[fool_formula_definition]) ).
tff(f33,definition,
( f1(bG29)
<=> ( $true = bG30 ) ),
introduced(definition,[new_symbols(definition,[bG30])],[fool_formula_definition]) ).
tff(f34,definition,
( f1(bG30)
<=> ( $true = bG31 ) ),
introduced(definition,[new_symbols(definition,[bG31])],[fool_formula_definition]) ).
tff(f35,plain,
~ ( f0(bG15)
<=> f0(bG31) ),
inference(fool_elimination,[],[f2,f34,f33,f32,f31,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(f36,plain,
( f0(bG15)
<~> f0(bG31) ),
inference(ennf_transformation,[],[f35]) ).
tff(f37,plain,
( ( f1(bG30)
| ( $true != bG31 ) )
& ( ( $true = bG31 )
| ~ f1(bG30) ) ),
inference(nnf_transformation,[],[f34]) ).
tff(f38,plain,
( ( f1(bG29)
| ( $true != bG30 ) )
& ( ( $true = bG30 )
| ~ f1(bG29) ) ),
inference(nnf_transformation,[],[f33]) ).
tff(f39,plain,
( ( f1(bG28)
| ( $true != bG29 ) )
& ( ( $true = bG29 )
| ~ f1(bG28) ) ),
inference(nnf_transformation,[],[f32]) ).
tff(f40,plain,
( ( f2(bG27)
| ( $true != bG28 ) )
& ( ( $true = bG28 )
| ~ f2(bG27) ) ),
inference(nnf_transformation,[],[f31]) ).
tff(f41,plain,
( ( f3(bG26)
| ( $true != bG27 ) )
& ( ( $true = bG27 )
| ~ f3(bG26) ) ),
inference(nnf_transformation,[],[f30]) ).
tff(f42,plain,
( ( f3(bG25)
| ( $true != bG26 ) )
& ( ( $true = bG26 )
| ~ f3(bG25) ) ),
inference(nnf_transformation,[],[f29]) ).
tff(f43,plain,
( ( f3(bG24)
| ( $true != bG25 ) )
& ( ( $true = bG25 )
| ~ f3(bG24) ) ),
inference(nnf_transformation,[],[f28]) ).
tff(f44,plain,
( ( f4(bG23)
| ( $true != bG24 ) )
& ( ( $true = bG24 )
| ~ f4(bG23) ) ),
inference(nnf_transformation,[],[f27]) ).
tff(f45,plain,
( ( f5(bG22)
| ( $true != bG23 ) )
& ( ( $true = bG23 )
| ~ f5(bG22) ) ),
inference(nnf_transformation,[],[f26]) ).
tff(f46,plain,
( ( f5(bG21)
| ( $true != bG22 ) )
& ( ( $true = bG22 )
| ~ f5(bG21) ) ),
inference(nnf_transformation,[],[f25]) ).
tff(f47,plain,
( ( f5(bG20)
| ( $true != bG21 ) )
& ( ( $true = bG21 )
| ~ f5(bG20) ) ),
inference(nnf_transformation,[],[f24]) ).
tff(f48,plain,
( ( f6(bG19)
| ( $true != bG20 ) )
& ( ( $true = bG20 )
| ~ f6(bG19) ) ),
inference(nnf_transformation,[],[f23]) ).
tff(f49,plain,
( ( f7(bG18)
| ( $true != bG19 ) )
& ( ( $true = bG19 )
| ~ f7(bG18) ) ),
inference(nnf_transformation,[],[f22]) ).
tff(f50,plain,
( ( f7(bG17)
| ( $true != bG18 ) )
& ( ( $true = bG18 )
| ~ f7(bG17) ) ),
inference(nnf_transformation,[],[f21]) ).
tff(f51,plain,
( ( f7(bG16)
| ( $true != bG17 ) )
& ( ( $true = bG17 )
| ~ f7(bG16) ) ),
inference(nnf_transformation,[],[f20]) ).
tff(f52,plain,
( ( x
| ( $true != bG16 ) )
& ( ( $true = bG16 )
| ~ x ) ),
inference(nnf_transformation,[],[f19]) ).
tff(f53,plain,
( ( f0(bG14)
| ( $true != bG15 ) )
& ( ( $true = bG15 )
| ~ f0(bG14) ) ),
inference(nnf_transformation,[],[f18]) ).
tff(f54,plain,
( ( f0(bG13)
| ( $true != bG14 ) )
& ( ( $true = bG14 )
| ~ f0(bG13) ) ),
inference(nnf_transformation,[],[f17]) ).
tff(f55,plain,
( ( f1(bG12)
| ( $true != bG13 ) )
& ( ( $true = bG13 )
| ~ f1(bG12) ) ),
inference(nnf_transformation,[],[f16]) ).
tff(f56,plain,
( ( f2(bG11)
| ( $true != bG12 ) )
& ( ( $true = bG12 )
| ~ f2(bG11) ) ),
inference(nnf_transformation,[],[f15]) ).
tff(f57,plain,
( ( f2(bG10)
| ( $true != bG11 ) )
& ( ( $true = bG11 )
| ~ f2(bG10) ) ),
inference(nnf_transformation,[],[f14]) ).
tff(f58,plain,
( ( f2(bG9)
| ( $true != bG10 ) )
& ( ( $true = bG10 )
| ~ f2(bG9) ) ),
inference(nnf_transformation,[],[f13]) ).
tff(f59,plain,
( ( f3(bG8)
| ( $true != bG9 ) )
& ( ( $true = bG9 )
| ~ f3(bG8) ) ),
inference(nnf_transformation,[],[f12]) ).
tff(f60,plain,
( ( f4(bG7)
| ( $true != bG8 ) )
& ( ( $true = bG8 )
| ~ f4(bG7) ) ),
inference(nnf_transformation,[],[f11]) ).
tff(f61,plain,
( ( f4(bG6)
| ( $true != bG7 ) )
& ( ( $true = bG7 )
| ~ f4(bG6) ) ),
inference(nnf_transformation,[],[f10]) ).
tff(f62,plain,
( ( f4(bG5)
| ( $true != bG6 ) )
& ( ( $true = bG6 )
| ~ f4(bG5) ) ),
inference(nnf_transformation,[],[f9]) ).
tff(f63,plain,
( ( f5(bG4)
| ( $true != bG5 ) )
& ( ( $true = bG5 )
| ~ f5(bG4) ) ),
inference(nnf_transformation,[],[f8]) ).
tff(f64,plain,
( ( f6(bG3)
| ( $true != bG4 ) )
& ( ( $true = bG4 )
| ~ f6(bG3) ) ),
inference(nnf_transformation,[],[f7]) ).
tff(f65,plain,
( ( f6(bG2)
| ( $true != bG3 ) )
& ( ( $true = bG3 )
| ~ f6(bG2) ) ),
inference(nnf_transformation,[],[f6]) ).
tff(f66,plain,
( ( f6(bG1)
| ( $true != bG2 ) )
& ( ( $true = bG2 )
| ~ f6(bG1) ) ),
inference(nnf_transformation,[],[f5]) ).
tff(f67,plain,
( ( f7(bG0)
| ( $true != bG1 ) )
& ( ( $true = bG1 )
| ~ f7(bG0) ) ),
inference(nnf_transformation,[],[f4]) ).
tff(f68,plain,
( ( x
| ( bG0 != $true ) )
& ( ( bG0 = $true )
| ~ x ) ),
inference(nnf_transformation,[],[f3]) ).
tff(f69,plain,
( ( ~ f0(bG31)
| ~ f0(bG15) )
& ( f0(bG31)
| f0(bG15) ) ),
inference(nnf_transformation,[],[f36]) ).
tff(f70,plain,
( ( $true = bG31 )
| ~ f1(bG30) ),
inference(cnf_transformation,[],[f37]) ).
tff(f71,plain,
( f1(bG30)
| ( $true != bG31 ) ),
inference(cnf_transformation,[],[f37]) ).
tff(f72,plain,
( ( $true = bG30 )
| ~ f1(bG29) ),
inference(cnf_transformation,[],[f38]) ).
tff(f73,plain,
( f1(bG29)
| ( $true != bG30 ) ),
inference(cnf_transformation,[],[f38]) ).
tff(f74,plain,
( ( $true = bG29 )
| ~ f1(bG28) ),
inference(cnf_transformation,[],[f39]) ).
tff(f75,plain,
( f1(bG28)
| ( $true != bG29 ) ),
inference(cnf_transformation,[],[f39]) ).
tff(f76,plain,
( ( $true = bG28 )
| ~ f2(bG27) ),
inference(cnf_transformation,[],[f40]) ).
tff(f77,plain,
( f2(bG27)
| ( $true != bG28 ) ),
inference(cnf_transformation,[],[f40]) ).
tff(f78,plain,
( ( $true = bG27 )
| ~ f3(bG26) ),
inference(cnf_transformation,[],[f41]) ).
tff(f79,plain,
( f3(bG26)
| ( $true != bG27 ) ),
inference(cnf_transformation,[],[f41]) ).
tff(f80,plain,
( ( $true = bG26 )
| ~ f3(bG25) ),
inference(cnf_transformation,[],[f42]) ).
tff(f81,plain,
( f3(bG25)
| ( $true != bG26 ) ),
inference(cnf_transformation,[],[f42]) ).
tff(f82,plain,
( ( $true = bG25 )
| ~ f3(bG24) ),
inference(cnf_transformation,[],[f43]) ).
tff(f83,plain,
( f3(bG24)
| ( $true != bG25 ) ),
inference(cnf_transformation,[],[f43]) ).
tff(f84,plain,
( ( $true = bG24 )
| ~ f4(bG23) ),
inference(cnf_transformation,[],[f44]) ).
tff(f85,plain,
( f4(bG23)
| ( $true != bG24 ) ),
inference(cnf_transformation,[],[f44]) ).
tff(f86,plain,
( ( $true = bG23 )
| ~ f5(bG22) ),
inference(cnf_transformation,[],[f45]) ).
tff(f87,plain,
( f5(bG22)
| ( $true != bG23 ) ),
inference(cnf_transformation,[],[f45]) ).
tff(f88,plain,
( ( $true = bG22 )
| ~ f5(bG21) ),
inference(cnf_transformation,[],[f46]) ).
tff(f89,plain,
( f5(bG21)
| ( $true != bG22 ) ),
inference(cnf_transformation,[],[f46]) ).
tff(f90,plain,
( ( $true = bG21 )
| ~ f5(bG20) ),
inference(cnf_transformation,[],[f47]) ).
tff(f91,plain,
( f5(bG20)
| ( $true != bG21 ) ),
inference(cnf_transformation,[],[f47]) ).
tff(f92,plain,
( ( $true = bG20 )
| ~ f6(bG19) ),
inference(cnf_transformation,[],[f48]) ).
tff(f93,plain,
( f6(bG19)
| ( $true != bG20 ) ),
inference(cnf_transformation,[],[f48]) ).
tff(f94,plain,
( ( $true = bG19 )
| ~ f7(bG18) ),
inference(cnf_transformation,[],[f49]) ).
tff(f95,plain,
( f7(bG18)
| ( $true != bG19 ) ),
inference(cnf_transformation,[],[f49]) ).
tff(f96,plain,
( ( $true = bG18 )
| ~ f7(bG17) ),
inference(cnf_transformation,[],[f50]) ).
tff(f97,plain,
( f7(bG17)
| ( $true != bG18 ) ),
inference(cnf_transformation,[],[f50]) ).
tff(f98,plain,
( ( $true = bG17 )
| ~ f7(bG16) ),
inference(cnf_transformation,[],[f51]) ).
tff(f99,plain,
( f7(bG16)
| ( $true != bG17 ) ),
inference(cnf_transformation,[],[f51]) ).
tff(f100,plain,
( ( $true = bG16 )
| ~ x ),
inference(cnf_transformation,[],[f52]) ).
tff(f101,plain,
( x
| ( $true != bG16 ) ),
inference(cnf_transformation,[],[f52]) ).
tff(f102,plain,
( ( $true = bG15 )
| ~ f0(bG14) ),
inference(cnf_transformation,[],[f53]) ).
tff(f103,plain,
( f0(bG14)
| ( $true != bG15 ) ),
inference(cnf_transformation,[],[f53]) ).
tff(f104,plain,
( ( $true = bG14 )
| ~ f0(bG13) ),
inference(cnf_transformation,[],[f54]) ).
tff(f105,plain,
( f0(bG13)
| ( $true != bG14 ) ),
inference(cnf_transformation,[],[f54]) ).
tff(f106,plain,
( ( $true = bG13 )
| ~ f1(bG12) ),
inference(cnf_transformation,[],[f55]) ).
tff(f107,plain,
( f1(bG12)
| ( $true != bG13 ) ),
inference(cnf_transformation,[],[f55]) ).
tff(f108,plain,
( ( $true = bG12 )
| ~ f2(bG11) ),
inference(cnf_transformation,[],[f56]) ).
tff(f109,plain,
( f2(bG11)
| ( $true != bG12 ) ),
inference(cnf_transformation,[],[f56]) ).
tff(f110,plain,
( ( $true = bG11 )
| ~ f2(bG10) ),
inference(cnf_transformation,[],[f57]) ).
tff(f111,plain,
( f2(bG10)
| ( $true != bG11 ) ),
inference(cnf_transformation,[],[f57]) ).
tff(f112,plain,
( ( $true = bG10 )
| ~ f2(bG9) ),
inference(cnf_transformation,[],[f58]) ).
tff(f113,plain,
( f2(bG9)
| ( $true != bG10 ) ),
inference(cnf_transformation,[],[f58]) ).
tff(f114,plain,
( ( $true = bG9 )
| ~ f3(bG8) ),
inference(cnf_transformation,[],[f59]) ).
tff(f115,plain,
( f3(bG8)
| ( $true != bG9 ) ),
inference(cnf_transformation,[],[f59]) ).
tff(f116,plain,
( ( $true = bG8 )
| ~ f4(bG7) ),
inference(cnf_transformation,[],[f60]) ).
tff(f117,plain,
( f4(bG7)
| ( $true != bG8 ) ),
inference(cnf_transformation,[],[f60]) ).
tff(f118,plain,
( ( $true = bG7 )
| ~ f4(bG6) ),
inference(cnf_transformation,[],[f61]) ).
tff(f119,plain,
( f4(bG6)
| ( $true != bG7 ) ),
inference(cnf_transformation,[],[f61]) ).
tff(f120,plain,
( ( $true = bG6 )
| ~ f4(bG5) ),
inference(cnf_transformation,[],[f62]) ).
tff(f121,plain,
( f4(bG5)
| ( $true != bG6 ) ),
inference(cnf_transformation,[],[f62]) ).
tff(f122,plain,
( ( $true = bG5 )
| ~ f5(bG4) ),
inference(cnf_transformation,[],[f63]) ).
tff(f123,plain,
( f5(bG4)
| ( $true != bG5 ) ),
inference(cnf_transformation,[],[f63]) ).
tff(f124,plain,
( ( $true = bG4 )
| ~ f6(bG3) ),
inference(cnf_transformation,[],[f64]) ).
tff(f125,plain,
( f6(bG3)
| ( $true != bG4 ) ),
inference(cnf_transformation,[],[f64]) ).
tff(f126,plain,
( ( $true = bG3 )
| ~ f6(bG2) ),
inference(cnf_transformation,[],[f65]) ).
tff(f127,plain,
( f6(bG2)
| ( $true != bG3 ) ),
inference(cnf_transformation,[],[f65]) ).
tff(f128,plain,
( ( $true = bG2 )
| ~ f6(bG1) ),
inference(cnf_transformation,[],[f66]) ).
tff(f129,plain,
( f6(bG1)
| ( $true != bG2 ) ),
inference(cnf_transformation,[],[f66]) ).
tff(f130,plain,
( ( $true = bG1 )
| ~ f7(bG0) ),
inference(cnf_transformation,[],[f67]) ).
tff(f131,plain,
( f7(bG0)
| ( $true != bG1 ) ),
inference(cnf_transformation,[],[f67]) ).
tff(f132,plain,
( ( bG0 = $true )
| ~ x ),
inference(cnf_transformation,[],[f68]) ).
tff(f133,plain,
( x
| ( bG0 != $true ) ),
inference(cnf_transformation,[],[f68]) ).
tff(f134,plain,
( f0(bG31)
| f0(bG15) ),
inference(cnf_transformation,[],[f69]) ).
tff(f135,plain,
( ~ f0(bG31)
| ~ f0(bG15) ),
inference(cnf_transformation,[],[f69]) ).
tff(f137,plain,
! [X0: $o] :
( ( $false = (X0) )
| ( $true = (X0) ) ),
introduced(definition,[],[fool_exhaustiveness_axiom]) ).
tff(f139,definition,
( spl32_1
<=> f0(bG15) ),
introduced(definition,[new_symbols(definition,[spl32_1])],[avatar_definition]) ).
tff(f140,plain,
( ~ f0(bG15)
| spl32_1 ),
inference(avatar_component_clause,[],[f139]) ).
tff(f141,plain,
( f0(bG15)
| ~ spl32_1 ),
inference(avatar_component_clause,[],[f139]) ).
tff(f143,definition,
( spl32_2
<=> f0(bG31) ),
introduced(definition,[new_symbols(definition,[spl32_2])],[avatar_definition]) ).
tff(f144,plain,
( ~ f0(bG31)
| spl32_2 ),
inference(avatar_component_clause,[],[f143]) ).
tff(f145,plain,
( f0(bG31)
| ~ spl32_2 ),
inference(avatar_component_clause,[],[f143]) ).
tff(f146,plain,
( spl32_1
| spl32_2 ),
inference(avatar_split_clause,[],[f134,f143,f139]) ).
tff(f147,plain,
( ~ spl32_1
| ~ spl32_2 ),
inference(avatar_split_clause,[],[f135,f143,f139]) ).
tff(f149,definition,
( spl32_3
<=> x ),
introduced(definition,[new_symbols(definition,[spl32_3])],[avatar_definition]) ).
tff(f153,definition,
( spl32_4
<=> ( bG0 = $true ) ),
introduced(definition,[new_symbols(definition,[spl32_4])],[avatar_definition]) ).
tff(f155,plain,
( ( bG0 = $true )
| ~ spl32_4 ),
inference(avatar_component_clause,[],[f153]) ).
tff(f156,plain,
( ~ spl32_3
| spl32_4 ),
inference(avatar_split_clause,[],[f132,f153,f149]) ).
tff(f157,plain,
( ~ spl32_4
| spl32_3 ),
inference(avatar_split_clause,[],[f133,f149,f153]) ).
tff(f159,definition,
( spl32_5
<=> f7(bG0) ),
introduced(definition,[new_symbols(definition,[spl32_5])],[avatar_definition]) ).
tff(f160,plain,
( f7(bG0)
| ~ spl32_5 ),
inference(avatar_component_clause,[],[f159]) ).
tff(f161,plain,
( ~ f7(bG0)
| spl32_5 ),
inference(avatar_component_clause,[],[f159]) ).
tff(f163,definition,
( spl32_6
<=> ( $true = bG1 ) ),
introduced(definition,[new_symbols(definition,[spl32_6])],[avatar_definition]) ).
tff(f165,plain,
( ( $true = bG1 )
| ~ spl32_6 ),
inference(avatar_component_clause,[],[f163]) ).
tff(f166,plain,
( ~ spl32_5
| spl32_6 ),
inference(avatar_split_clause,[],[f130,f163,f159]) ).
tff(f167,plain,
( ~ spl32_6
| spl32_5 ),
inference(avatar_split_clause,[],[f131,f159,f163]) ).
tff(f169,definition,
( spl32_7
<=> f6(bG1) ),
introduced(definition,[new_symbols(definition,[spl32_7])],[avatar_definition]) ).
tff(f170,plain,
( f6(bG1)
| ~ spl32_7 ),
inference(avatar_component_clause,[],[f169]) ).
tff(f171,plain,
( ~ f6(bG1)
| spl32_7 ),
inference(avatar_component_clause,[],[f169]) ).
tff(f173,definition,
( spl32_8
<=> ( $true = bG2 ) ),
introduced(definition,[new_symbols(definition,[spl32_8])],[avatar_definition]) ).
tff(f175,plain,
( ( $true = bG2 )
| ~ spl32_8 ),
inference(avatar_component_clause,[],[f173]) ).
tff(f176,plain,
( ~ spl32_7
| spl32_8 ),
inference(avatar_split_clause,[],[f128,f173,f169]) ).
tff(f177,plain,
( ~ spl32_8
| spl32_7 ),
inference(avatar_split_clause,[],[f129,f169,f173]) ).
tff(f179,definition,
( spl32_9
<=> f6(bG2) ),
introduced(definition,[new_symbols(definition,[spl32_9])],[avatar_definition]) ).
tff(f180,plain,
( f6(bG2)
| ~ spl32_9 ),
inference(avatar_component_clause,[],[f179]) ).
tff(f181,plain,
( ~ f6(bG2)
| spl32_9 ),
inference(avatar_component_clause,[],[f179]) ).
tff(f183,definition,
( spl32_10
<=> ( $true = bG3 ) ),
introduced(definition,[new_symbols(definition,[spl32_10])],[avatar_definition]) ).
tff(f184,plain,
( ( $true != bG3 )
| spl32_10 ),
inference(avatar_component_clause,[],[f183]) ).
tff(f185,plain,
( ( $true = bG3 )
| ~ spl32_10 ),
inference(avatar_component_clause,[],[f183]) ).
tff(f186,plain,
( ~ spl32_9
| spl32_10 ),
inference(avatar_split_clause,[],[f126,f183,f179]) ).
tff(f187,plain,
( ~ spl32_10
| spl32_9 ),
inference(avatar_split_clause,[],[f127,f179,f183]) ).
tff(f189,definition,
( spl32_11
<=> f6(bG3) ),
introduced(definition,[new_symbols(definition,[spl32_11])],[avatar_definition]) ).
tff(f190,plain,
( f6(bG3)
| ~ spl32_11 ),
inference(avatar_component_clause,[],[f189]) ).
tff(f191,plain,
( ~ f6(bG3)
| spl32_11 ),
inference(avatar_component_clause,[],[f189]) ).
tff(f193,definition,
( spl32_12
<=> ( $true = bG4 ) ),
introduced(definition,[new_symbols(definition,[spl32_12])],[avatar_definition]) ).
tff(f195,plain,
( ( $true = bG4 )
| ~ spl32_12 ),
inference(avatar_component_clause,[],[f193]) ).
tff(f196,plain,
( ~ spl32_11
| spl32_12 ),
inference(avatar_split_clause,[],[f124,f193,f189]) ).
tff(f197,plain,
( ~ spl32_12
| spl32_11 ),
inference(avatar_split_clause,[],[f125,f189,f193]) ).
tff(f199,definition,
( spl32_13
<=> f5(bG4) ),
introduced(definition,[new_symbols(definition,[spl32_13])],[avatar_definition]) ).
tff(f200,plain,
( f5(bG4)
| ~ spl32_13 ),
inference(avatar_component_clause,[],[f199]) ).
tff(f201,plain,
( ~ f5(bG4)
| spl32_13 ),
inference(avatar_component_clause,[],[f199]) ).
tff(f203,definition,
( spl32_14
<=> ( $true = bG5 ) ),
introduced(definition,[new_symbols(definition,[spl32_14])],[avatar_definition]) ).
tff(f205,plain,
( ( $true = bG5 )
| ~ spl32_14 ),
inference(avatar_component_clause,[],[f203]) ).
tff(f206,plain,
( ~ spl32_13
| spl32_14 ),
inference(avatar_split_clause,[],[f122,f203,f199]) ).
tff(f207,plain,
( ~ spl32_14
| spl32_13 ),
inference(avatar_split_clause,[],[f123,f199,f203]) ).
tff(f209,definition,
( spl32_15
<=> f4(bG5) ),
introduced(definition,[new_symbols(definition,[spl32_15])],[avatar_definition]) ).
tff(f210,plain,
( f4(bG5)
| ~ spl32_15 ),
inference(avatar_component_clause,[],[f209]) ).
tff(f211,plain,
( ~ f4(bG5)
| spl32_15 ),
inference(avatar_component_clause,[],[f209]) ).
tff(f213,definition,
( spl32_16
<=> ( $true = bG6 ) ),
introduced(definition,[new_symbols(definition,[spl32_16])],[avatar_definition]) ).
tff(f215,plain,
( ( $true = bG6 )
| ~ spl32_16 ),
inference(avatar_component_clause,[],[f213]) ).
tff(f216,plain,
( ~ spl32_15
| spl32_16 ),
inference(avatar_split_clause,[],[f120,f213,f209]) ).
tff(f217,plain,
( ~ spl32_16
| spl32_15 ),
inference(avatar_split_clause,[],[f121,f209,f213]) ).
tff(f219,definition,
( spl32_17
<=> f4(bG6) ),
introduced(definition,[new_symbols(definition,[spl32_17])],[avatar_definition]) ).
tff(f220,plain,
( f4(bG6)
| ~ spl32_17 ),
inference(avatar_component_clause,[],[f219]) ).
tff(f221,plain,
( ~ f4(bG6)
| spl32_17 ),
inference(avatar_component_clause,[],[f219]) ).
tff(f223,definition,
( spl32_18
<=> ( $true = bG7 ) ),
introduced(definition,[new_symbols(definition,[spl32_18])],[avatar_definition]) ).
tff(f224,plain,
( ( $true != bG7 )
| spl32_18 ),
inference(avatar_component_clause,[],[f223]) ).
tff(f225,plain,
( ( $true = bG7 )
| ~ spl32_18 ),
inference(avatar_component_clause,[],[f223]) ).
tff(f226,plain,
( ~ spl32_17
| spl32_18 ),
inference(avatar_split_clause,[],[f118,f223,f219]) ).
tff(f227,plain,
( ~ spl32_18
| spl32_17 ),
inference(avatar_split_clause,[],[f119,f219,f223]) ).
tff(f229,definition,
( spl32_19
<=> f4(bG7) ),
introduced(definition,[new_symbols(definition,[spl32_19])],[avatar_definition]) ).
tff(f230,plain,
( f4(bG7)
| ~ spl32_19 ),
inference(avatar_component_clause,[],[f229]) ).
tff(f231,plain,
( ~ f4(bG7)
| spl32_19 ),
inference(avatar_component_clause,[],[f229]) ).
tff(f233,definition,
( spl32_20
<=> ( $true = bG8 ) ),
introduced(definition,[new_symbols(definition,[spl32_20])],[avatar_definition]) ).
tff(f235,plain,
( ( $true = bG8 )
| ~ spl32_20 ),
inference(avatar_component_clause,[],[f233]) ).
tff(f236,plain,
( ~ spl32_19
| spl32_20 ),
inference(avatar_split_clause,[],[f116,f233,f229]) ).
tff(f237,plain,
( ~ spl32_20
| spl32_19 ),
inference(avatar_split_clause,[],[f117,f229,f233]) ).
tff(f239,definition,
( spl32_21
<=> f3(bG8) ),
introduced(definition,[new_symbols(definition,[spl32_21])],[avatar_definition]) ).
tff(f240,plain,
( f3(bG8)
| ~ spl32_21 ),
inference(avatar_component_clause,[],[f239]) ).
tff(f241,plain,
( ~ f3(bG8)
| spl32_21 ),
inference(avatar_component_clause,[],[f239]) ).
tff(f243,definition,
( spl32_22
<=> ( $true = bG9 ) ),
introduced(definition,[new_symbols(definition,[spl32_22])],[avatar_definition]) ).
tff(f244,plain,
( ( $true != bG9 )
| spl32_22 ),
inference(avatar_component_clause,[],[f243]) ).
tff(f245,plain,
( ( $true = bG9 )
| ~ spl32_22 ),
inference(avatar_component_clause,[],[f243]) ).
tff(f246,plain,
( ~ spl32_21
| spl32_22 ),
inference(avatar_split_clause,[],[f114,f243,f239]) ).
tff(f247,plain,
( ~ spl32_22
| spl32_21 ),
inference(avatar_split_clause,[],[f115,f239,f243]) ).
tff(f249,definition,
( spl32_23
<=> f2(bG9) ),
introduced(definition,[new_symbols(definition,[spl32_23])],[avatar_definition]) ).
tff(f250,plain,
( f2(bG9)
| ~ spl32_23 ),
inference(avatar_component_clause,[],[f249]) ).
tff(f251,plain,
( ~ f2(bG9)
| spl32_23 ),
inference(avatar_component_clause,[],[f249]) ).
tff(f253,definition,
( spl32_24
<=> ( $true = bG10 ) ),
introduced(definition,[new_symbols(definition,[spl32_24])],[avatar_definition]) ).
tff(f255,plain,
( ( $true = bG10 )
| ~ spl32_24 ),
inference(avatar_component_clause,[],[f253]) ).
tff(f256,plain,
( ~ spl32_23
| spl32_24 ),
inference(avatar_split_clause,[],[f112,f253,f249]) ).
tff(f257,plain,
( ~ spl32_24
| spl32_23 ),
inference(avatar_split_clause,[],[f113,f249,f253]) ).
tff(f259,definition,
( spl32_25
<=> f2(bG10) ),
introduced(definition,[new_symbols(definition,[spl32_25])],[avatar_definition]) ).
tff(f260,plain,
( f2(bG10)
| ~ spl32_25 ),
inference(avatar_component_clause,[],[f259]) ).
tff(f261,plain,
( ~ f2(bG10)
| spl32_25 ),
inference(avatar_component_clause,[],[f259]) ).
tff(f263,definition,
( spl32_26
<=> ( $true = bG11 ) ),
introduced(definition,[new_symbols(definition,[spl32_26])],[avatar_definition]) ).
tff(f265,plain,
( ( $true = bG11 )
| ~ spl32_26 ),
inference(avatar_component_clause,[],[f263]) ).
tff(f266,plain,
( ~ spl32_25
| spl32_26 ),
inference(avatar_split_clause,[],[f110,f263,f259]) ).
tff(f267,plain,
( ~ spl32_26
| spl32_25 ),
inference(avatar_split_clause,[],[f111,f259,f263]) ).
tff(f269,definition,
( spl32_27
<=> f2(bG11) ),
introduced(definition,[new_symbols(definition,[spl32_27])],[avatar_definition]) ).
tff(f270,plain,
( f2(bG11)
| ~ spl32_27 ),
inference(avatar_component_clause,[],[f269]) ).
tff(f271,plain,
( ~ f2(bG11)
| spl32_27 ),
inference(avatar_component_clause,[],[f269]) ).
tff(f273,definition,
( spl32_28
<=> ( $true = bG12 ) ),
introduced(definition,[new_symbols(definition,[spl32_28])],[avatar_definition]) ).
tff(f275,plain,
( ( $true = bG12 )
| ~ spl32_28 ),
inference(avatar_component_clause,[],[f273]) ).
tff(f276,plain,
( ~ spl32_27
| spl32_28 ),
inference(avatar_split_clause,[],[f108,f273,f269]) ).
tff(f277,plain,
( ~ spl32_28
| spl32_27 ),
inference(avatar_split_clause,[],[f109,f269,f273]) ).
tff(f279,definition,
( spl32_29
<=> f1(bG12) ),
introduced(definition,[new_symbols(definition,[spl32_29])],[avatar_definition]) ).
tff(f280,plain,
( f1(bG12)
| ~ spl32_29 ),
inference(avatar_component_clause,[],[f279]) ).
tff(f281,plain,
( ~ f1(bG12)
| spl32_29 ),
inference(avatar_component_clause,[],[f279]) ).
tff(f283,definition,
( spl32_30
<=> ( $true = bG13 ) ),
introduced(definition,[new_symbols(definition,[spl32_30])],[avatar_definition]) ).
tff(f285,plain,
( ( $true = bG13 )
| ~ spl32_30 ),
inference(avatar_component_clause,[],[f283]) ).
tff(f286,plain,
( ~ spl32_29
| spl32_30 ),
inference(avatar_split_clause,[],[f106,f283,f279]) ).
tff(f287,plain,
( ~ spl32_30
| spl32_29 ),
inference(avatar_split_clause,[],[f107,f279,f283]) ).
tff(f289,definition,
( spl32_31
<=> f0(bG13) ),
introduced(definition,[new_symbols(definition,[spl32_31])],[avatar_definition]) ).
tff(f290,plain,
( f0(bG13)
| ~ spl32_31 ),
inference(avatar_component_clause,[],[f289]) ).
tff(f291,plain,
( ~ f0(bG13)
| spl32_31 ),
inference(avatar_component_clause,[],[f289]) ).
tff(f293,definition,
( spl32_32
<=> ( $true = bG14 ) ),
introduced(definition,[new_symbols(definition,[spl32_32])],[avatar_definition]) ).
tff(f294,plain,
( ( $true != bG14 )
| spl32_32 ),
inference(avatar_component_clause,[],[f293]) ).
tff(f295,plain,
( ( $true = bG14 )
| ~ spl32_32 ),
inference(avatar_component_clause,[],[f293]) ).
tff(f296,plain,
( ~ spl32_31
| spl32_32 ),
inference(avatar_split_clause,[],[f104,f293,f289]) ).
tff(f297,plain,
( ~ spl32_32
| spl32_31 ),
inference(avatar_split_clause,[],[f105,f289,f293]) ).
tff(f299,definition,
( spl32_33
<=> f0(bG14) ),
introduced(definition,[new_symbols(definition,[spl32_33])],[avatar_definition]) ).
tff(f300,plain,
( f0(bG14)
| ~ spl32_33 ),
inference(avatar_component_clause,[],[f299]) ).
tff(f301,plain,
( ~ f0(bG14)
| spl32_33 ),
inference(avatar_component_clause,[],[f299]) ).
tff(f303,definition,
( spl32_34
<=> ( $true = bG15 ) ),
introduced(definition,[new_symbols(definition,[spl32_34])],[avatar_definition]) ).
tff(f305,plain,
( ( $true = bG15 )
| ~ spl32_34 ),
inference(avatar_component_clause,[],[f303]) ).
tff(f306,plain,
( ~ spl32_33
| spl32_34 ),
inference(avatar_split_clause,[],[f102,f303,f299]) ).
tff(f307,plain,
( ~ spl32_34
| spl32_33 ),
inference(avatar_split_clause,[],[f103,f299,f303]) ).
tff(f309,definition,
( spl32_35
<=> ( $true = bG16 ) ),
introduced(definition,[new_symbols(definition,[spl32_35])],[avatar_definition]) ).
tff(f311,plain,
( ( $true = bG16 )
| ~ spl32_35 ),
inference(avatar_component_clause,[],[f309]) ).
tff(f312,plain,
( ~ spl32_3
| spl32_35 ),
inference(avatar_split_clause,[],[f100,f309,f149]) ).
tff(f313,plain,
( ~ spl32_35
| spl32_3 ),
inference(avatar_split_clause,[],[f101,f149,f309]) ).
tff(f315,definition,
( spl32_36
<=> f7(bG16) ),
introduced(definition,[new_symbols(definition,[spl32_36])],[avatar_definition]) ).
tff(f316,plain,
( f7(bG16)
| ~ spl32_36 ),
inference(avatar_component_clause,[],[f315]) ).
tff(f317,plain,
( ~ f7(bG16)
| spl32_36 ),
inference(avatar_component_clause,[],[f315]) ).
tff(f319,definition,
( spl32_37
<=> ( $true = bG17 ) ),
introduced(definition,[new_symbols(definition,[spl32_37])],[avatar_definition]) ).
tff(f320,plain,
( ( $true != bG17 )
| spl32_37 ),
inference(avatar_component_clause,[],[f319]) ).
tff(f321,plain,
( ( $true = bG17 )
| ~ spl32_37 ),
inference(avatar_component_clause,[],[f319]) ).
tff(f322,plain,
( ~ spl32_36
| spl32_37 ),
inference(avatar_split_clause,[],[f98,f319,f315]) ).
tff(f323,plain,
( ~ spl32_37
| spl32_36 ),
inference(avatar_split_clause,[],[f99,f315,f319]) ).
tff(f325,definition,
( spl32_38
<=> f7(bG17) ),
introduced(definition,[new_symbols(definition,[spl32_38])],[avatar_definition]) ).
tff(f326,plain,
( f7(bG17)
| ~ spl32_38 ),
inference(avatar_component_clause,[],[f325]) ).
tff(f327,plain,
( ~ f7(bG17)
| spl32_38 ),
inference(avatar_component_clause,[],[f325]) ).
tff(f329,definition,
( spl32_39
<=> ( $true = bG18 ) ),
introduced(definition,[new_symbols(definition,[spl32_39])],[avatar_definition]) ).
tff(f330,plain,
( ( $true != bG18 )
| spl32_39 ),
inference(avatar_component_clause,[],[f329]) ).
tff(f331,plain,
( ( $true = bG18 )
| ~ spl32_39 ),
inference(avatar_component_clause,[],[f329]) ).
tff(f332,plain,
( ~ spl32_38
| spl32_39 ),
inference(avatar_split_clause,[],[f96,f329,f325]) ).
tff(f333,plain,
( ~ spl32_39
| spl32_38 ),
inference(avatar_split_clause,[],[f97,f325,f329]) ).
tff(f335,definition,
( spl32_40
<=> f7(bG18) ),
introduced(definition,[new_symbols(definition,[spl32_40])],[avatar_definition]) ).
tff(f336,plain,
( f7(bG18)
| ~ spl32_40 ),
inference(avatar_component_clause,[],[f335]) ).
tff(f337,plain,
( ~ f7(bG18)
| spl32_40 ),
inference(avatar_component_clause,[],[f335]) ).
tff(f339,definition,
( spl32_41
<=> ( $true = bG19 ) ),
introduced(definition,[new_symbols(definition,[spl32_41])],[avatar_definition]) ).
tff(f340,plain,
( ( $true != bG19 )
| spl32_41 ),
inference(avatar_component_clause,[],[f339]) ).
tff(f341,plain,
( ( $true = bG19 )
| ~ spl32_41 ),
inference(avatar_component_clause,[],[f339]) ).
tff(f342,plain,
( ~ spl32_40
| spl32_41 ),
inference(avatar_split_clause,[],[f94,f339,f335]) ).
tff(f343,plain,
( ~ spl32_41
| spl32_40 ),
inference(avatar_split_clause,[],[f95,f335,f339]) ).
tff(f345,definition,
( spl32_42
<=> f6(bG19) ),
introduced(definition,[new_symbols(definition,[spl32_42])],[avatar_definition]) ).
tff(f346,plain,
( f6(bG19)
| ~ spl32_42 ),
inference(avatar_component_clause,[],[f345]) ).
tff(f347,plain,
( ~ f6(bG19)
| spl32_42 ),
inference(avatar_component_clause,[],[f345]) ).
tff(f349,definition,
( spl32_43
<=> ( $true = bG20 ) ),
introduced(definition,[new_symbols(definition,[spl32_43])],[avatar_definition]) ).
tff(f350,plain,
( ( $true != bG20 )
| spl32_43 ),
inference(avatar_component_clause,[],[f349]) ).
tff(f351,plain,
( ( $true = bG20 )
| ~ spl32_43 ),
inference(avatar_component_clause,[],[f349]) ).
tff(f352,plain,
( ~ spl32_42
| spl32_43 ),
inference(avatar_split_clause,[],[f92,f349,f345]) ).
tff(f353,plain,
( ~ spl32_43
| spl32_42 ),
inference(avatar_split_clause,[],[f93,f345,f349]) ).
tff(f355,definition,
( spl32_44
<=> f5(bG20) ),
introduced(definition,[new_symbols(definition,[spl32_44])],[avatar_definition]) ).
tff(f356,plain,
( f5(bG20)
| ~ spl32_44 ),
inference(avatar_component_clause,[],[f355]) ).
tff(f357,plain,
( ~ f5(bG20)
| spl32_44 ),
inference(avatar_component_clause,[],[f355]) ).
tff(f359,definition,
( spl32_45
<=> ( $true = bG21 ) ),
introduced(definition,[new_symbols(definition,[spl32_45])],[avatar_definition]) ).
tff(f361,plain,
( ( $true = bG21 )
| ~ spl32_45 ),
inference(avatar_component_clause,[],[f359]) ).
tff(f362,plain,
( ~ spl32_44
| spl32_45 ),
inference(avatar_split_clause,[],[f90,f359,f355]) ).
tff(f363,plain,
( ~ spl32_45
| spl32_44 ),
inference(avatar_split_clause,[],[f91,f355,f359]) ).
tff(f365,definition,
( spl32_46
<=> f5(bG21) ),
introduced(definition,[new_symbols(definition,[spl32_46])],[avatar_definition]) ).
tff(f366,plain,
( f5(bG21)
| ~ spl32_46 ),
inference(avatar_component_clause,[],[f365]) ).
tff(f367,plain,
( ~ f5(bG21)
| spl32_46 ),
inference(avatar_component_clause,[],[f365]) ).
tff(f369,definition,
( spl32_47
<=> ( $true = bG22 ) ),
introduced(definition,[new_symbols(definition,[spl32_47])],[avatar_definition]) ).
tff(f371,plain,
( ( $true = bG22 )
| ~ spl32_47 ),
inference(avatar_component_clause,[],[f369]) ).
tff(f372,plain,
( ~ spl32_46
| spl32_47 ),
inference(avatar_split_clause,[],[f88,f369,f365]) ).
tff(f373,plain,
( ~ spl32_47
| spl32_46 ),
inference(avatar_split_clause,[],[f89,f365,f369]) ).
tff(f375,definition,
( spl32_48
<=> f5(bG22) ),
introduced(definition,[new_symbols(definition,[spl32_48])],[avatar_definition]) ).
tff(f376,plain,
( f5(bG22)
| ~ spl32_48 ),
inference(avatar_component_clause,[],[f375]) ).
tff(f377,plain,
( ~ f5(bG22)
| spl32_48 ),
inference(avatar_component_clause,[],[f375]) ).
tff(f379,definition,
( spl32_49
<=> ( $true = bG23 ) ),
introduced(definition,[new_symbols(definition,[spl32_49])],[avatar_definition]) ).
tff(f380,plain,
( ( $true != bG23 )
| spl32_49 ),
inference(avatar_component_clause,[],[f379]) ).
tff(f381,plain,
( ( $true = bG23 )
| ~ spl32_49 ),
inference(avatar_component_clause,[],[f379]) ).
tff(f382,plain,
( ~ spl32_48
| spl32_49 ),
inference(avatar_split_clause,[],[f86,f379,f375]) ).
tff(f383,plain,
( ~ spl32_49
| spl32_48 ),
inference(avatar_split_clause,[],[f87,f375,f379]) ).
tff(f385,definition,
( spl32_50
<=> f4(bG23) ),
introduced(definition,[new_symbols(definition,[spl32_50])],[avatar_definition]) ).
tff(f386,plain,
( f4(bG23)
| ~ spl32_50 ),
inference(avatar_component_clause,[],[f385]) ).
tff(f387,plain,
( ~ f4(bG23)
| spl32_50 ),
inference(avatar_component_clause,[],[f385]) ).
tff(f389,definition,
( spl32_51
<=> ( $true = bG24 ) ),
introduced(definition,[new_symbols(definition,[spl32_51])],[avatar_definition]) ).
tff(f391,plain,
( ( $true = bG24 )
| ~ spl32_51 ),
inference(avatar_component_clause,[],[f389]) ).
tff(f392,plain,
( ~ spl32_50
| spl32_51 ),
inference(avatar_split_clause,[],[f84,f389,f385]) ).
tff(f393,plain,
( ~ spl32_51
| spl32_50 ),
inference(avatar_split_clause,[],[f85,f385,f389]) ).
tff(f395,definition,
( spl32_52
<=> f3(bG24) ),
introduced(definition,[new_symbols(definition,[spl32_52])],[avatar_definition]) ).
tff(f396,plain,
( f3(bG24)
| ~ spl32_52 ),
inference(avatar_component_clause,[],[f395]) ).
tff(f397,plain,
( ~ f3(bG24)
| spl32_52 ),
inference(avatar_component_clause,[],[f395]) ).
tff(f399,definition,
( spl32_53
<=> ( $true = bG25 ) ),
introduced(definition,[new_symbols(definition,[spl32_53])],[avatar_definition]) ).
tff(f401,plain,
( ( $true = bG25 )
| ~ spl32_53 ),
inference(avatar_component_clause,[],[f399]) ).
tff(f402,plain,
( ~ spl32_52
| spl32_53 ),
inference(avatar_split_clause,[],[f82,f399,f395]) ).
tff(f403,plain,
( ~ spl32_53
| spl32_52 ),
inference(avatar_split_clause,[],[f83,f395,f399]) ).
tff(f405,definition,
( spl32_54
<=> f3(bG25) ),
introduced(definition,[new_symbols(definition,[spl32_54])],[avatar_definition]) ).
tff(f406,plain,
( f3(bG25)
| ~ spl32_54 ),
inference(avatar_component_clause,[],[f405]) ).
tff(f407,plain,
( ~ f3(bG25)
| spl32_54 ),
inference(avatar_component_clause,[],[f405]) ).
tff(f409,definition,
( spl32_55
<=> ( $true = bG26 ) ),
introduced(definition,[new_symbols(definition,[spl32_55])],[avatar_definition]) ).
tff(f411,plain,
( ( $true = bG26 )
| ~ spl32_55 ),
inference(avatar_component_clause,[],[f409]) ).
tff(f412,plain,
( ~ spl32_54
| spl32_55 ),
inference(avatar_split_clause,[],[f80,f409,f405]) ).
tff(f413,plain,
( ~ spl32_55
| spl32_54 ),
inference(avatar_split_clause,[],[f81,f405,f409]) ).
tff(f415,definition,
( spl32_56
<=> f3(bG26) ),
introduced(definition,[new_symbols(definition,[spl32_56])],[avatar_definition]) ).
tff(f416,plain,
( f3(bG26)
| ~ spl32_56 ),
inference(avatar_component_clause,[],[f415]) ).
tff(f417,plain,
( ~ f3(bG26)
| spl32_56 ),
inference(avatar_component_clause,[],[f415]) ).
tff(f419,definition,
( spl32_57
<=> ( $true = bG27 ) ),
introduced(definition,[new_symbols(definition,[spl32_57])],[avatar_definition]) ).
tff(f420,plain,
( ( $true != bG27 )
| spl32_57 ),
inference(avatar_component_clause,[],[f419]) ).
tff(f421,plain,
( ( $true = bG27 )
| ~ spl32_57 ),
inference(avatar_component_clause,[],[f419]) ).
tff(f422,plain,
( ~ spl32_56
| spl32_57 ),
inference(avatar_split_clause,[],[f78,f419,f415]) ).
tff(f423,plain,
( ~ spl32_57
| spl32_56 ),
inference(avatar_split_clause,[],[f79,f415,f419]) ).
tff(f425,definition,
( spl32_58
<=> f2(bG27) ),
introduced(definition,[new_symbols(definition,[spl32_58])],[avatar_definition]) ).
tff(f426,plain,
( f2(bG27)
| ~ spl32_58 ),
inference(avatar_component_clause,[],[f425]) ).
tff(f427,plain,
( ~ f2(bG27)
| spl32_58 ),
inference(avatar_component_clause,[],[f425]) ).
tff(f429,definition,
( spl32_59
<=> ( $true = bG28 ) ),
introduced(definition,[new_symbols(definition,[spl32_59])],[avatar_definition]) ).
tff(f431,plain,
( ( $true = bG28 )
| ~ spl32_59 ),
inference(avatar_component_clause,[],[f429]) ).
tff(f432,plain,
( ~ spl32_58
| spl32_59 ),
inference(avatar_split_clause,[],[f76,f429,f425]) ).
tff(f433,plain,
( ~ spl32_59
| spl32_58 ),
inference(avatar_split_clause,[],[f77,f425,f429]) ).
tff(f435,definition,
( spl32_60
<=> f1(bG28) ),
introduced(definition,[new_symbols(definition,[spl32_60])],[avatar_definition]) ).
tff(f436,plain,
( f1(bG28)
| ~ spl32_60 ),
inference(avatar_component_clause,[],[f435]) ).
tff(f437,plain,
( ~ f1(bG28)
| spl32_60 ),
inference(avatar_component_clause,[],[f435]) ).
tff(f439,definition,
( spl32_61
<=> ( $true = bG29 ) ),
introduced(definition,[new_symbols(definition,[spl32_61])],[avatar_definition]) ).
tff(f440,plain,
( ( $true != bG29 )
| spl32_61 ),
inference(avatar_component_clause,[],[f439]) ).
tff(f441,plain,
( ( $true = bG29 )
| ~ spl32_61 ),
inference(avatar_component_clause,[],[f439]) ).
tff(f442,plain,
( ~ spl32_60
| spl32_61 ),
inference(avatar_split_clause,[],[f74,f439,f435]) ).
tff(f443,plain,
( ~ spl32_61
| spl32_60 ),
inference(avatar_split_clause,[],[f75,f435,f439]) ).
tff(f445,definition,
( spl32_62
<=> f1(bG29) ),
introduced(definition,[new_symbols(definition,[spl32_62])],[avatar_definition]) ).
tff(f446,plain,
( f1(bG29)
| ~ spl32_62 ),
inference(avatar_component_clause,[],[f445]) ).
tff(f447,plain,
( ~ f1(bG29)
| spl32_62 ),
inference(avatar_component_clause,[],[f445]) ).
tff(f449,definition,
( spl32_63
<=> ( $true = bG30 ) ),
introduced(definition,[new_symbols(definition,[spl32_63])],[avatar_definition]) ).
tff(f450,plain,
( ( $true != bG30 )
| spl32_63 ),
inference(avatar_component_clause,[],[f449]) ).
tff(f451,plain,
( ( $true = bG30 )
| ~ spl32_63 ),
inference(avatar_component_clause,[],[f449]) ).
tff(f452,plain,
( ~ spl32_62
| spl32_63 ),
inference(avatar_split_clause,[],[f72,f449,f445]) ).
tff(f453,plain,
( ~ spl32_63
| spl32_62 ),
inference(avatar_split_clause,[],[f73,f445,f449]) ).
tff(f455,definition,
( spl32_64
<=> f1(bG30) ),
introduced(definition,[new_symbols(definition,[spl32_64])],[avatar_definition]) ).
tff(f456,plain,
( f1(bG30)
| ~ spl32_64 ),
inference(avatar_component_clause,[],[f455]) ).
tff(f457,plain,
( ~ f1(bG30)
| spl32_64 ),
inference(avatar_component_clause,[],[f455]) ).
tff(f459,definition,
( spl32_65
<=> ( $true = bG31 ) ),
introduced(definition,[new_symbols(definition,[spl32_65])],[avatar_definition]) ).
tff(f460,plain,
( ( $true != bG31 )
| spl32_65 ),
inference(avatar_component_clause,[],[f459]) ).
tff(f461,plain,
( ( $true = bG31 )
| ~ spl32_65 ),
inference(avatar_component_clause,[],[f459]) ).
tff(f462,plain,
( ~ spl32_64
| spl32_65 ),
inference(avatar_split_clause,[],[f70,f459,f455]) ).
tff(f463,plain,
( ~ spl32_65
| spl32_64 ),
inference(avatar_split_clause,[],[f71,f455,f459]) ).
tff(f494,plain,
( ~ f0($false)
| ( $true = bG14 )
| spl32_33 ),
inference(superposition,[],[f301,f137]) ).
tff(f496,plain,
( ~ f0($false)
| ( $true = bG15 )
| spl32_1 ),
inference(superposition,[],[f140,f137]) ).
tff(f498,plain,
( ~ f7($false)
| ( $true = bG16 )
| spl32_36 ),
inference(superposition,[],[f317,f137]) ).
tff(f500,plain,
( ~ f7($false)
| ( $true = bG17 )
| spl32_38 ),
inference(superposition,[],[f327,f137]) ).
tff(f504,plain,
( ~ f6($false)
| ( $true = bG19 )
| spl32_42 ),
inference(superposition,[],[f347,f137]) ).
tff(f506,plain,
( ~ f5($false)
| ( $true = bG20 )
| spl32_44 ),
inference(superposition,[],[f357,f137]) ).
tff(f512,plain,
( ~ f4($false)
| ( $true = bG23 )
| spl32_50 ),
inference(superposition,[],[f387,f137]) ).
tff(f520,plain,
( ~ f2($false)
| ( $true = bG27 )
| spl32_58 ),
inference(superposition,[],[f427,f137]) ).
tff(f524,plain,
( ~ f1($false)
| ( $true = bG29 )
| spl32_62 ),
inference(superposition,[],[f447,f137]) ).
tff(f526,plain,
( ~ f1($false)
| ( $true = bG30 )
| spl32_64 ),
inference(superposition,[],[f457,f137]) ).
tff(f528,plain,
( f0($false)
| ( $true = bG31 )
| ~ spl32_2 ),
inference(superposition,[],[f145,f137]) ).
tff(f530,plain,
( f0($false)
| ~ spl32_2
| spl32_65 ),
inference(forward_subsumption_resolution,[],[f528,f460]) ).
tff(f531,plain,
( ~ f1($false)
| spl32_63
| spl32_64 ),
inference(forward_subsumption_resolution,[],[f526,f450]) ).
tff(f532,plain,
( ~ f1($false)
| spl32_61
| spl32_62 ),
inference(forward_subsumption_resolution,[],[f524,f440]) ).
tff(f534,plain,
( ~ f2($false)
| spl32_57
| spl32_58 ),
inference(forward_subsumption_resolution,[],[f520,f420]) ).
tff(f538,plain,
( ~ f4($false)
| spl32_49
| spl32_50 ),
inference(forward_subsumption_resolution,[],[f512,f380]) ).
tff(f541,plain,
( ~ f5($false)
| spl32_43
| spl32_44 ),
inference(forward_subsumption_resolution,[],[f506,f350]) ).
tff(f542,plain,
( ~ f6($false)
| spl32_41
| spl32_42 ),
inference(forward_subsumption_resolution,[],[f504,f340]) ).
tff(f544,plain,
( ~ f7($false)
| spl32_37
| spl32_38 ),
inference(forward_subsumption_resolution,[],[f500,f320]) ).
tff(f547,plain,
( ~ f0($false)
| spl32_32
| spl32_33 ),
inference(forward_subsumption_resolution,[],[f494,f294]) ).
tff(f562,plain,
( ! [X0: $o] :
( f0((X0))
| ( $true = (X0) ) )
| ~ spl32_2
| spl32_65 ),
inference(superposition,[],[f530,f137]) ).
tff(f565,plain,
( ( $true = bG15 )
| spl32_1
| ~ spl32_2
| spl32_65 ),
inference(forward_subsumption_resolution,[],[f496,f530]) ).
tff(f566,plain,
( spl32_34
| spl32_1
| ~ spl32_2
| spl32_65 ),
inference(avatar_split_clause,[],[f565,f459,f143,f139,f303]) ).
tff(f569,plain,
( ( $true = bG13 )
| ~ spl32_2
| spl32_31
| spl32_65 ),
inference(resolution,[],[f562,f291]) ).
tff(f573,plain,
( spl32_30
| ~ spl32_2
| spl32_31
| spl32_65 ),
inference(avatar_split_clause,[],[f569,f459,f289,f143,f283]) ).
tff(f575,plain,
( ~ f0($true)
| spl32_1
| ~ spl32_34 ),
inference(superposition,[],[f140,f305]) ).
tff(f578,plain,
( f1($false)
| ( $true = bG12 )
| ~ spl32_29 ),
inference(superposition,[],[f280,f137]) ).
tff(f592,plain,
( ( $true = bG12 )
| ~ spl32_29
| spl32_63
| spl32_64 ),
inference(forward_subsumption_resolution,[],[f578,f531]) ).
tff(f593,plain,
( spl32_28
| ~ spl32_29
| spl32_63
| spl32_64 ),
inference(avatar_split_clause,[],[f592,f455,f449,f279,f273]) ).
tff(f594,plain,
( f2($false)
| ( $true = bG11 )
| ~ spl32_27 ),
inference(superposition,[],[f270,f137]) ).
tff(f595,plain,
( ( $true = bG11 )
| ~ spl32_27
| spl32_57
| spl32_58 ),
inference(forward_subsumption_resolution,[],[f594,f534]) ).
tff(f598,plain,
( spl32_26
| ~ spl32_27
| spl32_57
| spl32_58 ),
inference(avatar_split_clause,[],[f595,f425,f419,f269,f263]) ).
tff(f599,plain,
( f2($false)
| ( $true = bG10 )
| ~ spl32_25 ),
inference(superposition,[],[f260,f137]) ).
tff(f600,plain,
( ( $true = bG10 )
| ~ spl32_25
| spl32_57
| spl32_58 ),
inference(forward_subsumption_resolution,[],[f599,f534]) ).
tff(f603,plain,
( spl32_24
| ~ spl32_25
| spl32_57
| spl32_58 ),
inference(avatar_split_clause,[],[f600,f425,f419,f259,f253]) ).
tff(f604,plain,
( f2($false)
| ( $true = bG9 )
| ~ spl32_23 ),
inference(superposition,[],[f250,f137]) ).
tff(f605,plain,
( ( $true = bG9 )
| ~ spl32_23
| spl32_57
| spl32_58 ),
inference(forward_subsumption_resolution,[],[f604,f534]) ).
tff(f606,plain,
( $false
| spl32_22
| ~ spl32_23
| spl32_57
| spl32_58 ),
inference(forward_subsumption_resolution,[],[f605,f244]) ).
tff(f607,plain,
( spl32_22
| ~ spl32_23
| spl32_57
| spl32_58 ),
inference(avatar_contradiction_clause,[],[f606]) ).
tff(f609,definition,
( spl32_66
<=> f2($false) ),
introduced(definition,[new_symbols(definition,[spl32_66])],[avatar_definition]) ).
tff(f613,plain,
( spl32_26
| spl32_66
| ~ spl32_27 ),
inference(avatar_split_clause,[],[f594,f269,f609,f263]) ).
tff(f624,plain,
( f2($true)
| ~ spl32_22
| ~ spl32_23 ),
inference(superposition,[],[f250,f245]) ).
tff(f627,plain,
( f2($true)
| ~ spl32_24
| ~ spl32_25 ),
inference(superposition,[],[f260,f255]) ).
tff(f630,plain,
( f2($true)
| ~ spl32_26
| ~ spl32_27 ),
inference(superposition,[],[f270,f265]) ).
tff(f635,definition,
( spl32_67
<=> f3($false) ),
introduced(definition,[new_symbols(definition,[spl32_67])],[avatar_definition]) ).
tff(f641,plain,
( f4($false)
| ( $true = bG7 )
| ~ spl32_19 ),
inference(superposition,[],[f230,f137]) ).
tff(f642,plain,
( ( $true = bG7 )
| ~ spl32_19
| spl32_49
| spl32_50 ),
inference(forward_subsumption_resolution,[],[f641,f538]) ).
tff(f643,plain,
( $false
| spl32_18
| ~ spl32_19
| spl32_49
| spl32_50 ),
inference(forward_subsumption_resolution,[],[f642,f224]) ).
tff(f644,plain,
( spl32_18
| ~ spl32_19
| spl32_49
| spl32_50 ),
inference(avatar_contradiction_clause,[],[f643]) ).
tff(f646,definition,
( spl32_68
<=> f4($false) ),
introduced(definition,[new_symbols(definition,[spl32_68])],[avatar_definition]) ).
tff(f649,plain,
( spl32_49
| ~ spl32_68
| spl32_50 ),
inference(avatar_split_clause,[],[f512,f385,f646,f379]) ).
tff(f663,plain,
( f5($false)
| ( $true = bG4 )
| ~ spl32_13 ),
inference(superposition,[],[f200,f137]) ).
tff(f671,plain,
( f4($true)
| ~ spl32_14
| ~ spl32_15 ),
inference(superposition,[],[f210,f205]) ).
tff(f674,plain,
( f4($true)
| ~ spl32_16
| ~ spl32_17 ),
inference(superposition,[],[f220,f215]) ).
tff(f678,plain,
( f4($true)
| ~ spl32_18
| ~ spl32_19 ),
inference(superposition,[],[f230,f225]) ).
tff(f681,plain,
( f3($true)
| ~ spl32_20
| ~ spl32_21 ),
inference(superposition,[],[f240,f235]) ).
tff(f684,plain,
( f1($true)
| ~ spl32_28
| ~ spl32_29 ),
inference(superposition,[],[f280,f275]) ).
tff(f687,plain,
( ~ f4($true)
| ~ spl32_49
| spl32_50 ),
inference(superposition,[],[f387,f381]) ).
tff(f689,plain,
( $false
| ~ spl32_14
| ~ spl32_15
| ~ spl32_49
| spl32_50 ),
inference(forward_subsumption_resolution,[],[f687,f671]) ).
tff(f690,plain,
( ~ spl32_14
| ~ spl32_15
| ~ spl32_49
| spl32_50 ),
inference(avatar_contradiction_clause,[],[f689]) ).
tff(f691,plain,
( ~ f4($true)
| ~ spl32_14
| spl32_15 ),
inference(forward_demodulation,[],[f211,f205]) ).
tff(f703,plain,
( ~ f3($true)
| ~ spl32_53
| spl32_54 ),
inference(superposition,[],[f407,f401]) ).
tff(f706,plain,
( ~ f2($true)
| ~ spl32_57
| spl32_58 ),
inference(superposition,[],[f427,f421]) ).
tff(f708,plain,
( $false
| ~ spl32_22
| ~ spl32_23
| ~ spl32_57
| spl32_58 ),
inference(forward_subsumption_resolution,[],[f706,f624]) ).
tff(f709,plain,
( ~ spl32_22
| ~ spl32_23
| ~ spl32_57
| spl32_58 ),
inference(avatar_contradiction_clause,[],[f708]) ).
tff(f710,plain,
( ~ f2($true)
| ~ spl32_22
| spl32_23 ),
inference(forward_demodulation,[],[f251,f245]) ).
tff(f712,plain,
( $false
| ~ spl32_22
| spl32_23
| ~ spl32_26
| ~ spl32_27 ),
inference(forward_subsumption_resolution,[],[f630,f710]) ).
tff(f713,plain,
( ~ spl32_22
| spl32_23
| ~ spl32_26
| ~ spl32_27 ),
inference(avatar_contradiction_clause,[],[f712]) ).
tff(f715,plain,
( f2($true)
| ~ spl32_22
| ~ spl32_23 ),
inference(forward_demodulation,[],[f250,f245]) ).
tff(f716,plain,
( f2($true)
| ~ spl32_57
| ~ spl32_58 ),
inference(forward_demodulation,[],[f426,f421]) ).
tff(f720,plain,
( ~ f2($true)
| ~ spl32_24
| spl32_25 ),
inference(superposition,[],[f261,f255]) ).
tff(f722,plain,
( $false
| ~ spl32_22
| ~ spl32_23
| ~ spl32_24
| spl32_25 ),
inference(forward_subsumption_resolution,[],[f720,f715]) ).
tff(f723,plain,
( ~ spl32_22
| ~ spl32_23
| ~ spl32_24
| spl32_25 ),
inference(avatar_contradiction_clause,[],[f722]) ).
tff(f732,plain,
( f2($false)
| ( $true = bG9 )
| ~ spl32_23 ),
inference(superposition,[],[f250,f137]) ).
tff(f733,plain,
( spl32_22
| spl32_66
| ~ spl32_23 ),
inference(avatar_split_clause,[],[f732,f249,f609,f243]) ).
tff(f748,plain,
( ~ f1($true)
| ~ spl32_59
| spl32_60 ),
inference(superposition,[],[f437,f431]) ).
tff(f750,plain,
( $false
| ~ spl32_28
| ~ spl32_29
| ~ spl32_59
| spl32_60 ),
inference(forward_subsumption_resolution,[],[f748,f684]) ).
tff(f751,plain,
( ~ spl32_28
| ~ spl32_29
| ~ spl32_59
| spl32_60 ),
inference(avatar_contradiction_clause,[],[f750]) ).
tff(f756,plain,
( ~ f1($true)
| ~ spl32_28
| spl32_29 ),
inference(forward_demodulation,[],[f281,f275]) ).
tff(f760,plain,
( f0($true)
| ~ spl32_32
| ~ spl32_33 ),
inference(superposition,[],[f300,f295]) ).
tff(f762,plain,
( $false
| spl32_1
| ~ spl32_32
| ~ spl32_33
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f760,f575]) ).
tff(f763,plain,
( spl32_1
| ~ spl32_32
| ~ spl32_33
| ~ spl32_34 ),
inference(avatar_contradiction_clause,[],[f762]) ).
tff(f764,plain,
( f1($true)
| ~ spl32_28
| ~ spl32_29 ),
inference(forward_demodulation,[],[f280,f275]) ).
tff(f771,plain,
( f1($false)
| ( $true = bG28 )
| ~ spl32_60 ),
inference(superposition,[],[f436,f137]) ).
tff(f772,plain,
( ( $true = bG28 )
| ~ spl32_60
| spl32_63
| spl32_64 ),
inference(forward_subsumption_resolution,[],[f771,f531]) ).
tff(f773,plain,
( spl32_59
| ~ spl32_60
| spl32_63
| spl32_64 ),
inference(avatar_split_clause,[],[f772,f455,f449,f435,f429]) ).
tff(f780,definition,
( spl32_69
<=> f5($false) ),
introduced(definition,[new_symbols(definition,[spl32_69])],[avatar_definition]) ).
tff(f790,plain,
( ~ f5($true)
| ~ spl32_45
| spl32_46 ),
inference(superposition,[],[f367,f361]) ).
tff(f796,plain,
( f1($true)
| ~ spl32_59
| ~ spl32_60 ),
inference(superposition,[],[f436,f431]) ).
tff(f799,plain,
( ~ f1($true)
| ~ spl32_61
| spl32_62 ),
inference(superposition,[],[f447,f441]) ).
tff(f801,plain,
( $false
| ~ spl32_28
| ~ spl32_29
| ~ spl32_61
| spl32_62 ),
inference(forward_subsumption_resolution,[],[f799,f764]) ).
tff(f802,plain,
( ~ spl32_28
| ~ spl32_29
| ~ spl32_61
| spl32_62 ),
inference(avatar_contradiction_clause,[],[f801]) ).
tff(f803,plain,
( f1($true)
| ~ spl32_61
| ~ spl32_62 ),
inference(forward_demodulation,[],[f446,f441]) ).
tff(f805,definition,
( spl32_70
<=> f1($false) ),
introduced(definition,[new_symbols(definition,[spl32_70])],[avatar_definition]) ).
tff(f810,plain,
( ~ f1($true)
| ~ spl32_63
| spl32_64 ),
inference(superposition,[],[f457,f451]) ).
tff(f812,plain,
( $false
| ~ spl32_28
| ~ spl32_29
| ~ spl32_63
| spl32_64 ),
inference(forward_subsumption_resolution,[],[f810,f764]) ).
tff(f813,plain,
( ~ spl32_28
| ~ spl32_29
| ~ spl32_63
| spl32_64 ),
inference(avatar_contradiction_clause,[],[f812]) ).
tff(f814,plain,
( f1($true)
| ~ spl32_63
| ~ spl32_64 ),
inference(forward_demodulation,[],[f456,f451]) ).
tff(f816,definition,
( spl32_71
<=> f0($false) ),
introduced(definition,[new_symbols(definition,[spl32_71])],[avatar_definition]) ).
tff(f817,plain,
( ~ f0($false)
| spl32_71 ),
inference(avatar_component_clause,[],[f816]) ).
tff(f822,plain,
( f0($true)
| ~ spl32_1
| ~ spl32_34 ),
inference(forward_demodulation,[],[f141,f305]) ).
tff(f823,plain,
( f0($true)
| ~ spl32_30
| ~ spl32_31 ),
inference(forward_demodulation,[],[f290,f285]) ).
tff(f831,plain,
( ~ f0($true)
| spl32_2
| ~ spl32_65 ),
inference(superposition,[],[f144,f461]) ).
tff(f833,plain,
( $false
| ~ spl32_1
| spl32_2
| ~ spl32_34
| ~ spl32_65 ),
inference(forward_subsumption_resolution,[],[f831,f822]) ).
tff(f834,plain,
( ~ spl32_1
| spl32_2
| ~ spl32_34
| ~ spl32_65 ),
inference(avatar_contradiction_clause,[],[f833]) ).
tff(f835,plain,
( ~ f0($true)
| ~ spl32_32
| spl32_33 ),
inference(forward_demodulation,[],[f301,f295]) ).
tff(f836,plain,
( f0($false)
| ( $true = bG15 )
| ~ spl32_1 ),
inference(superposition,[],[f141,f137]) ).
tff(f837,plain,
( spl32_34
| spl32_71
| ~ spl32_1 ),
inference(avatar_split_clause,[],[f836,f139,f816,f303]) ).
tff(f838,plain,
( $false
| spl32_2
| ~ spl32_30
| ~ spl32_31
| ~ spl32_65 ),
inference(forward_subsumption_resolution,[],[f823,f831]) ).
tff(f839,plain,
( spl32_2
| ~ spl32_30
| ~ spl32_31
| ~ spl32_65 ),
inference(avatar_contradiction_clause,[],[f838]) ).
tff(f846,plain,
( $false
| ~ spl32_28
| spl32_29
| ~ spl32_63
| ~ spl32_64 ),
inference(forward_subsumption_resolution,[],[f756,f814]) ).
tff(f847,plain,
( ~ spl32_28
| spl32_29
| ~ spl32_63
| ~ spl32_64 ),
inference(avatar_contradiction_clause,[],[f846]) ).
tff(f852,plain,
( f0($true)
| ~ spl32_2
| ~ spl32_65 ),
inference(forward_demodulation,[],[f145,f461]) ).
tff(f853,plain,
( ~ spl32_71
| spl32_32
| spl32_33 ),
inference(avatar_split_clause,[],[f547,f299,f293,f816]) ).
tff(f863,plain,
( ~ f0($true)
| ~ spl32_30
| spl32_31 ),
inference(superposition,[],[f291,f285]) ).
tff(f865,plain,
( $false
| ~ spl32_2
| ~ spl32_30
| spl32_31
| ~ spl32_65 ),
inference(forward_subsumption_resolution,[],[f863,f852]) ).
tff(f866,plain,
( ~ spl32_2
| ~ spl32_30
| spl32_31
| ~ spl32_65 ),
inference(avatar_contradiction_clause,[],[f865]) ).
tff(f869,plain,
( f1($false)
| ( $true = bG30 )
| ~ spl32_64 ),
inference(superposition,[],[f456,f137]) ).
tff(f870,plain,
( spl32_63
| spl32_70
| ~ spl32_64 ),
inference(avatar_split_clause,[],[f869,f455,f805,f449]) ).
tff(f872,plain,
( $false
| ~ spl32_28
| spl32_29
| ~ spl32_59
| ~ spl32_60 ),
inference(forward_subsumption_resolution,[],[f796,f756]) ).
tff(f873,plain,
( ~ spl32_28
| spl32_29
| ~ spl32_59
| ~ spl32_60 ),
inference(avatar_contradiction_clause,[],[f872]) ).
tff(f875,plain,
( ~ spl32_70
| spl32_61
| spl32_62 ),
inference(avatar_split_clause,[],[f532,f445,f439,f805]) ).
tff(f876,plain,
( f4($true)
| ~ spl32_49
| ~ spl32_50 ),
inference(forward_demodulation,[],[f386,f381]) ).
tff(f877,plain,
( $false
| ~ spl32_14
| spl32_15
| ~ spl32_49
| ~ spl32_50 ),
inference(forward_subsumption_resolution,[],[f876,f691]) ).
tff(f878,plain,
( ~ spl32_14
| spl32_15
| ~ spl32_49
| ~ spl32_50 ),
inference(avatar_contradiction_clause,[],[f877]) ).
tff(f879,plain,
( $false
| ~ spl32_14
| spl32_15
| ~ spl32_18
| ~ spl32_19 ),
inference(forward_subsumption_resolution,[],[f678,f691]) ).
tff(f880,plain,
( ~ spl32_14
| spl32_15
| ~ spl32_18
| ~ spl32_19 ),
inference(avatar_contradiction_clause,[],[f879]) ).
tff(f889,plain,
( f3($false)
| ( $true = bG8 )
| ~ spl32_21 ),
inference(superposition,[],[f240,f137]) ).
tff(f890,plain,
( spl32_20
| spl32_67
| ~ spl32_21 ),
inference(avatar_split_clause,[],[f889,f239,f635,f233]) ).
tff(f893,plain,
( ~ f2($false)
| ( $true = bG11 )
| spl32_27 ),
inference(superposition,[],[f271,f137]) ).
tff(f895,plain,
( ~ f1($false)
| ( $true = bG12 )
| spl32_29 ),
inference(superposition,[],[f281,f137]) ).
tff(f896,plain,
( spl32_28
| ~ spl32_70
| spl32_29 ),
inference(avatar_split_clause,[],[f895,f279,f805,f273]) ).
tff(f914,plain,
( f1($false)
| ( $true = bG28 )
| ~ spl32_60 ),
inference(superposition,[],[f436,f137]) ).
tff(f915,plain,
( spl32_59
| spl32_70
| ~ spl32_60 ),
inference(avatar_split_clause,[],[f914,f435,f805,f429]) ).
tff(f916,plain,
( $false
| ~ spl32_22
| spl32_23
| ~ spl32_57
| ~ spl32_58 ),
inference(forward_subsumption_resolution,[],[f716,f710]) ).
tff(f917,plain,
( ~ spl32_22
| spl32_23
| ~ spl32_57
| ~ spl32_58 ),
inference(avatar_contradiction_clause,[],[f916]) ).
tff(f919,plain,
( $false
| ~ spl32_2
| ~ spl32_32
| spl32_33
| ~ spl32_65 ),
inference(forward_subsumption_resolution,[],[f835,f852]) ).
tff(f920,plain,
( ~ spl32_2
| ~ spl32_32
| spl32_33
| ~ spl32_65 ),
inference(avatar_contradiction_clause,[],[f919]) ).
tff(f928,plain,
( f0($false)
| ( $true = bG14 )
| ~ spl32_33 ),
inference(superposition,[],[f300,f137]) ).
tff(f945,plain,
( ~ f4($true)
| ~ spl32_18
| spl32_19 ),
inference(superposition,[],[f231,f225]) ).
tff(f948,plain,
( $false
| ~ spl32_61
| ~ spl32_62
| ~ spl32_63
| spl32_64 ),
inference(forward_subsumption_resolution,[],[f810,f803]) ).
tff(f949,plain,
( ~ spl32_61
| ~ spl32_62
| ~ spl32_63
| spl32_64 ),
inference(avatar_contradiction_clause,[],[f948]) ).
tff(f951,plain,
( ~ spl32_70
| spl32_63
| spl32_64 ),
inference(avatar_split_clause,[],[f531,f455,f449,f805]) ).
tff(f952,plain,
( spl32_32
| spl32_71
| ~ spl32_33 ),
inference(avatar_split_clause,[],[f928,f299,f816,f293]) ).
tff(f953,plain,
( ~ f0($false)
| ( $true = bG31 )
| spl32_2 ),
inference(superposition,[],[f144,f137]) ).
tff(f954,plain,
( ~ f0($false)
| spl32_2
| spl32_65 ),
inference(forward_subsumption_resolution,[],[f953,f460]) ).
tff(f955,plain,
( ~ spl32_71
| spl32_2
| spl32_65 ),
inference(avatar_split_clause,[],[f954,f459,f143,f816]) ).
tff(f957,plain,
( f0($false)
| ( $true = bG13 )
| ~ spl32_31 ),
inference(superposition,[],[f290,f137]) ).
tff(f958,plain,
( ( $true = bG13 )
| ~ spl32_31
| spl32_71 ),
inference(forward_subsumption_resolution,[],[f957,f817]) ).
tff(f959,plain,
( spl32_30
| ~ spl32_31
| spl32_71 ),
inference(avatar_split_clause,[],[f958,f816,f289,f283]) ).
tff(f960,plain,
( spl32_26
| ~ spl32_66
| spl32_27 ),
inference(avatar_split_clause,[],[f893,f269,f609,f263]) ).
tff(f967,plain,
( f2($false)
| ( $true = bG10 )
| ~ spl32_25 ),
inference(superposition,[],[f260,f137]) ).
tff(f968,plain,
( spl32_24
| spl32_66
| ~ spl32_25 ),
inference(avatar_split_clause,[],[f967,f259,f609,f253]) ).
tff(f969,plain,
( f1($false)
| ( $true = bG12 )
| ~ spl32_29 ),
inference(superposition,[],[f280,f137]) ).
tff(f970,plain,
( spl32_28
| spl32_70
| ~ spl32_29 ),
inference(avatar_split_clause,[],[f969,f279,f805,f273]) ).
tff(f971,plain,
( ~ f3($false)
| ( $true = bG26 )
| spl32_56 ),
inference(superposition,[],[f417,f137]) ).
tff(f972,plain,
( spl32_55
| ~ spl32_67
| spl32_56 ),
inference(avatar_split_clause,[],[f971,f415,f635,f409]) ).
tff(f973,plain,
( f2($false)
| ( $true = bG27 )
| ~ spl32_58 ),
inference(superposition,[],[f426,f137]) ).
tff(f974,plain,
( spl32_57
| spl32_66
| ~ spl32_58 ),
inference(avatar_split_clause,[],[f973,f425,f609,f419]) ).
tff(f975,plain,
( ~ f1($false)
| ( $true = bG28 )
| spl32_60 ),
inference(superposition,[],[f437,f137]) ).
tff(f976,plain,
( spl32_59
| ~ spl32_70
| spl32_60 ),
inference(avatar_split_clause,[],[f975,f435,f805,f429]) ).
tff(f977,plain,
( f1($false)
| ( $true = bG29 )
| ~ spl32_62 ),
inference(superposition,[],[f446,f137]) ).
tff(f978,plain,
( spl32_61
| spl32_70
| ~ spl32_62 ),
inference(avatar_split_clause,[],[f977,f445,f805,f439]) ).
tff(f984,plain,
( ~ f2($true)
| ~ spl32_26
| spl32_27 ),
inference(superposition,[],[f271,f265]) ).
tff(f996,plain,
( f3($true)
| ~ spl32_53
| ~ spl32_54 ),
inference(superposition,[],[f406,f401]) ).
tff(f999,plain,
( ~ f3($true)
| ~ spl32_55
| spl32_56 ),
inference(superposition,[],[f417,f411]) ).
tff(f1001,plain,
( $false
| ~ spl32_53
| ~ spl32_54
| ~ spl32_55
| spl32_56 ),
inference(forward_subsumption_resolution,[],[f999,f996]) ).
tff(f1002,plain,
( ~ spl32_53
| ~ spl32_54
| ~ spl32_55
| spl32_56 ),
inference(avatar_contradiction_clause,[],[f1001]) ).
tff(f1007,plain,
( spl32_12
| spl32_69
| ~ spl32_13 ),
inference(avatar_split_clause,[],[f663,f199,f780,f193]) ).
tff(f1008,plain,
( f6($false)
| ( $true = bG3 )
| ~ spl32_11 ),
inference(superposition,[],[f190,f137]) ).
tff(f1009,plain,
( f6($false)
| spl32_10
| ~ spl32_11 ),
inference(forward_subsumption_resolution,[],[f1008,f184]) ).
tff(f1012,plain,
( ~ f5($false)
| ( $true = bG22 )
| spl32_48 ),
inference(superposition,[],[f377,f137]) ).
tff(f1018,plain,
( f5($true)
| ~ spl32_12
| ~ spl32_13 ),
inference(superposition,[],[f200,f195]) ).
tff(f1020,plain,
( $false
| ~ spl32_12
| ~ spl32_13
| ~ spl32_45
| spl32_46 ),
inference(forward_subsumption_resolution,[],[f1018,f790]) ).
tff(f1021,plain,
( ~ spl32_12
| ~ spl32_13
| ~ spl32_45
| spl32_46 ),
inference(avatar_contradiction_clause,[],[f1020]) ).
tff(f1026,plain,
( ~ f5($true)
| ~ spl32_43
| spl32_44 ),
inference(superposition,[],[f357,f351]) ).
tff(f1030,plain,
( $false
| ~ spl32_12
| ~ spl32_13
| ~ spl32_43
| spl32_44 ),
inference(forward_subsumption_resolution,[],[f1026,f1018]) ).
tff(f1031,plain,
( ~ spl32_12
| ~ spl32_13
| ~ spl32_43
| spl32_44 ),
inference(avatar_contradiction_clause,[],[f1030]) ).
tff(f1032,plain,
( ~ spl32_69
| spl32_43
| spl32_44 ),
inference(avatar_split_clause,[],[f541,f355,f349,f780]) ).
tff(f1038,plain,
( ~ f3($true)
| ~ spl32_51
| spl32_52 ),
inference(superposition,[],[f397,f391]) ).
tff(f1043,plain,
( $false
| spl32_10
| ~ spl32_11
| spl32_41
| spl32_42 ),
inference(forward_subsumption_resolution,[],[f1009,f542]) ).
tff(f1044,plain,
( spl32_10
| ~ spl32_11
| spl32_41
| spl32_42 ),
inference(avatar_contradiction_clause,[],[f1043]) ).
tff(f1046,definition,
( spl32_72
<=> f6($false) ),
introduced(definition,[new_symbols(definition,[spl32_72])],[avatar_definition]) ).
tff(f1054,plain,
( spl32_47
| ~ spl32_69
| spl32_48 ),
inference(avatar_split_clause,[],[f1012,f375,f780,f369]) ).
tff(f1057,plain,
( f7($false)
| ( $true = bG18 )
| ~ spl32_40 ),
inference(superposition,[],[f336,f137]) ).
tff(f1058,plain,
( f7($false)
| spl32_39
| ~ spl32_40 ),
inference(forward_subsumption_resolution,[],[f1057,f330]) ).
tff(f1066,plain,
( f6($true)
| ~ spl32_41
| ~ spl32_42 ),
inference(superposition,[],[f346,f341]) ).
tff(f1073,plain,
( ~ f5($true)
| ~ spl32_47
| spl32_48 ),
inference(superposition,[],[f377,f371]) ).
tff(f1084,plain,
( $false
| spl32_37
| spl32_38
| spl32_39
| ~ spl32_40 ),
inference(forward_subsumption_resolution,[],[f1058,f544]) ).
tff(f1085,plain,
( spl32_37
| spl32_38
| spl32_39
| ~ spl32_40 ),
inference(avatar_contradiction_clause,[],[f1084]) ).
tff(f1087,definition,
( spl32_73
<=> f7($false) ),
introduced(definition,[new_symbols(definition,[spl32_73])],[avatar_definition]) ).
tff(f1089,plain,
( f7($false)
| ~ spl32_73 ),
inference(avatar_component_clause,[],[f1087]) ).
tff(f1090,plain,
( spl32_39
| spl32_73
| ~ spl32_40 ),
inference(avatar_split_clause,[],[f1057,f335,f1087,f329]) ).
tff(f1093,plain,
( f7($false)
| ( $true = bG17 )
| ~ spl32_38 ),
inference(superposition,[],[f326,f137]) ).
tff(f1096,plain,
( spl32_35
| ~ spl32_73
| spl32_36 ),
inference(avatar_split_clause,[],[f498,f315,f1087,f309]) ).
tff(f1100,plain,
( ~ f7($true)
| ~ spl32_4
| spl32_5 ),
inference(superposition,[],[f161,f155]) ).
tff(f1103,plain,
( ~ f7($true)
| ~ spl32_35
| spl32_36 ),
inference(superposition,[],[f317,f311]) ).
tff(f1106,plain,
( f7($true)
| ~ spl32_39
| ~ spl32_40 ),
inference(superposition,[],[f336,f331]) ).
tff(f1108,plain,
( $false
| ~ spl32_4
| spl32_5
| ~ spl32_39
| ~ spl32_40 ),
inference(forward_subsumption_resolution,[],[f1106,f1100]) ).
tff(f1109,plain,
( ~ spl32_4
| spl32_5
| ~ spl32_39
| ~ spl32_40 ),
inference(avatar_contradiction_clause,[],[f1108]) ).
tff(f1110,plain,
( f7($true)
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_demodulation,[],[f160,f155]) ).
tff(f1111,plain,
( $false
| ~ spl32_4
| ~ spl32_5
| ~ spl32_35
| spl32_36 ),
inference(forward_subsumption_resolution,[],[f1103,f1110]) ).
tff(f1112,plain,
( ~ spl32_4
| ~ spl32_5
| ~ spl32_35
| spl32_36 ),
inference(avatar_contradiction_clause,[],[f1111]) ).
tff(f1113,plain,
( spl32_37
| spl32_73
| ~ spl32_38 ),
inference(avatar_split_clause,[],[f1093,f325,f1087,f319]) ).
tff(f1114,plain,
( ~ f7($false)
| ( bG0 = $true )
| spl32_5 ),
inference(superposition,[],[f161,f137]) ).
tff(f1115,plain,
( spl32_4
| ~ spl32_73
| spl32_5 ),
inference(avatar_split_clause,[],[f1114,f159,f1087,f153]) ).
tff(f1116,plain,
( f7($false)
| ( $true = bG16 )
| ~ spl32_36 ),
inference(superposition,[],[f316,f137]) ).
tff(f1117,plain,
( spl32_35
| spl32_73
| ~ spl32_36 ),
inference(avatar_split_clause,[],[f1116,f315,f1087,f309]) ).
tff(f1118,plain,
( f7($false)
| ( bG0 = $true )
| ~ spl32_5 ),
inference(superposition,[],[f160,f137]) ).
tff(f1119,plain,
( spl32_4
| spl32_73
| ~ spl32_5 ),
inference(avatar_split_clause,[],[f1118,f159,f1087,f153]) ).
tff(f1122,plain,
( ~ f6($true)
| ~ spl32_6
| spl32_7 ),
inference(superposition,[],[f171,f165]) ).
tff(f1124,plain,
( $false
| ~ spl32_6
| spl32_7
| ~ spl32_41
| ~ spl32_42 ),
inference(forward_subsumption_resolution,[],[f1122,f1066]) ).
tff(f1125,plain,
( ~ spl32_6
| spl32_7
| ~ spl32_41
| ~ spl32_42 ),
inference(avatar_contradiction_clause,[],[f1124]) ).
tff(f1126,plain,
( ~ f6($true)
| ~ spl32_41
| spl32_42 ),
inference(forward_demodulation,[],[f347,f341]) ).
tff(f1135,plain,
( f5($true)
| ~ spl32_45
| ~ spl32_46 ),
inference(superposition,[],[f366,f361]) ).
tff(f1137,plain,
( $false
| ~ spl32_45
| ~ spl32_46
| ~ spl32_47
| spl32_48 ),
inference(forward_subsumption_resolution,[],[f1135,f1073]) ).
tff(f1138,plain,
( ~ spl32_45
| ~ spl32_46
| ~ spl32_47
| spl32_48 ),
inference(avatar_contradiction_clause,[],[f1137]) ).
tff(f1139,plain,
( f6($true)
| ~ spl32_6
| ~ spl32_7 ),
inference(forward_demodulation,[],[f170,f165]) ).
tff(f1141,plain,
( $false
| ~ spl32_6
| ~ spl32_7
| ~ spl32_41
| spl32_42 ),
inference(forward_subsumption_resolution,[],[f1139,f1126]) ).
tff(f1142,plain,
( ~ spl32_6
| ~ spl32_7
| ~ spl32_41
| spl32_42 ),
inference(avatar_contradiction_clause,[],[f1141]) ).
tff(f1146,plain,
( f6($false)
| ( $true = bG3 )
| ~ spl32_11 ),
inference(superposition,[],[f190,f137]) ).
tff(f1147,plain,
( spl32_10
| spl32_72
| ~ spl32_11 ),
inference(avatar_split_clause,[],[f1146,f189,f1046,f183]) ).
tff(f1154,plain,
( f6($true)
| ~ spl32_10
| ~ spl32_11 ),
inference(superposition,[],[f190,f185]) ).
tff(f1156,plain,
( $false
| ~ spl32_10
| ~ spl32_11
| ~ spl32_41
| spl32_42 ),
inference(forward_subsumption_resolution,[],[f1154,f1126]) ).
tff(f1157,plain,
( ~ spl32_10
| ~ spl32_11
| ~ spl32_41
| spl32_42 ),
inference(avatar_contradiction_clause,[],[f1156]) ).
tff(f1158,plain,
( ~ f6($true)
| ~ spl32_10
| spl32_11 ),
inference(forward_demodulation,[],[f191,f185]) ).
tff(f1160,plain,
( ~ f5($false)
| ( $true = bG4 )
| spl32_13 ),
inference(superposition,[],[f201,f137]) ).
tff(f1161,plain,
( spl32_12
| ~ spl32_69
| spl32_13 ),
inference(avatar_split_clause,[],[f1160,f199,f780,f193]) ).
tff(f1164,plain,
( $false
| ~ spl32_16
| ~ spl32_17
| ~ spl32_18
| spl32_19 ),
inference(forward_subsumption_resolution,[],[f945,f674]) ).
tff(f1165,plain,
( ~ spl32_16
| ~ spl32_17
| ~ spl32_18
| spl32_19 ),
inference(avatar_contradiction_clause,[],[f1164]) ).
tff(f1167,plain,
( $false
| ~ spl32_20
| ~ spl32_21
| ~ spl32_55
| spl32_56 ),
inference(forward_subsumption_resolution,[],[f681,f999]) ).
tff(f1168,plain,
( ~ spl32_20
| ~ spl32_21
| ~ spl32_55
| spl32_56 ),
inference(avatar_contradiction_clause,[],[f1167]) ).
tff(f1172,plain,
( $false
| ~ spl32_20
| ~ spl32_21
| ~ spl32_51
| spl32_52 ),
inference(forward_subsumption_resolution,[],[f1038,f681]) ).
tff(f1173,plain,
( ~ spl32_20
| ~ spl32_21
| ~ spl32_51
| spl32_52 ),
inference(avatar_contradiction_clause,[],[f1172]) ).
tff(f1174,plain,
( f3($true)
| ~ spl32_51
| ~ spl32_52 ),
inference(forward_demodulation,[],[f396,f391]) ).
tff(f1175,plain,
( $false
| ~ spl32_20
| ~ spl32_21
| ~ spl32_53
| spl32_54 ),
inference(forward_subsumption_resolution,[],[f703,f681]) ).
tff(f1176,plain,
( ~ spl32_20
| ~ spl32_21
| ~ spl32_53
| spl32_54 ),
inference(avatar_contradiction_clause,[],[f1175]) ).
tff(f1178,plain,
( ~ f3($true)
| ~ spl32_51
| spl32_52 ),
inference(forward_demodulation,[],[f397,f391]) ).
tff(f1182,plain,
( f6($true)
| ~ spl32_41
| ~ spl32_42 ),
inference(forward_demodulation,[],[f346,f341]) ).
tff(f1186,plain,
( ~ f4($false)
| ( $true = bG6 )
| spl32_17 ),
inference(superposition,[],[f221,f137]) ).
tff(f1187,plain,
( spl32_16
| ~ spl32_68
| spl32_17 ),
inference(avatar_split_clause,[],[f1186,f219,f646,f213]) ).
tff(f1190,plain,
( f5($false)
| ( $true = bG20 )
| ~ spl32_44 ),
inference(superposition,[],[f356,f137]) ).
tff(f1191,plain,
( spl32_43
| spl32_69
| ~ spl32_44 ),
inference(avatar_split_clause,[],[f1190,f355,f780,f349]) ).
tff(f1192,plain,
( f5($false)
| ( $true = bG21 )
| ~ spl32_46 ),
inference(superposition,[],[f366,f137]) ).
tff(f1193,plain,
( spl32_45
| spl32_69
| ~ spl32_46 ),
inference(avatar_split_clause,[],[f1192,f365,f780,f359]) ).
tff(f1194,plain,
( f5($false)
| ( $true = bG22 )
| ~ spl32_48 ),
inference(superposition,[],[f376,f137]) ).
tff(f1195,plain,
( spl32_47
| spl32_69
| ~ spl32_48 ),
inference(avatar_split_clause,[],[f1194,f375,f780,f369]) ).
tff(f1200,plain,
( ~ f7($true)
| ~ spl32_37
| spl32_38 ),
inference(forward_demodulation,[],[f327,f321]) ).
tff(f1203,plain,
( f6($false)
| ( $true = bG1 )
| ~ spl32_7 ),
inference(superposition,[],[f170,f137]) ).
tff(f1204,plain,
( spl32_6
| spl32_72
| ~ spl32_7 ),
inference(avatar_split_clause,[],[f1203,f169,f1046,f163]) ).
tff(f1205,plain,
( $false
| ~ spl32_10
| spl32_11
| ~ spl32_41
| ~ spl32_42 ),
inference(forward_subsumption_resolution,[],[f1182,f1158]) ).
tff(f1206,plain,
( ~ spl32_10
| spl32_11
| ~ spl32_41
| ~ spl32_42 ),
inference(avatar_contradiction_clause,[],[f1205]) ).
tff(f1231,plain,
( ~ f4($true)
| ~ spl32_16
| spl32_17 ),
inference(superposition,[],[f221,f215]) ).
tff(f1233,plain,
( $false
| ~ spl32_16
| spl32_17
| ~ spl32_49
| ~ spl32_50 ),
inference(forward_subsumption_resolution,[],[f1231,f876]) ).
tff(f1234,plain,
( ~ spl32_16
| spl32_17
| ~ spl32_49
| ~ spl32_50 ),
inference(avatar_contradiction_clause,[],[f1233]) ).
tff(f1235,plain,
( ~ f5($true)
| ~ spl32_12
| spl32_13 ),
inference(forward_demodulation,[],[f201,f195]) ).
tff(f1237,plain,
( ~ f5($false)
| ( $true = bG21 )
| spl32_46 ),
inference(superposition,[],[f367,f137]) ).
tff(f1238,plain,
( spl32_45
| ~ spl32_69
| spl32_46 ),
inference(avatar_split_clause,[],[f1237,f365,f780,f359]) ).
tff(f1244,plain,
( f7($true)
| ~ spl32_35
| ~ spl32_36 ),
inference(superposition,[],[f316,f311]) ).
tff(f1246,plain,
( $false
| ~ spl32_35
| ~ spl32_36
| ~ spl32_37
| spl32_38 ),
inference(forward_subsumption_resolution,[],[f1244,f1200]) ).
tff(f1247,plain,
( ~ spl32_35
| ~ spl32_36
| ~ spl32_37
| spl32_38 ),
inference(avatar_contradiction_clause,[],[f1246]) ).
tff(f1257,plain,
( f5($true)
| ~ spl32_43
| ~ spl32_44 ),
inference(superposition,[],[f356,f351]) ).
tff(f1259,plain,
( $false
| ~ spl32_12
| spl32_13
| ~ spl32_43
| ~ spl32_44 ),
inference(forward_subsumption_resolution,[],[f1257,f1235]) ).
tff(f1260,plain,
( ~ spl32_12
| spl32_13
| ~ spl32_43
| ~ spl32_44 ),
inference(avatar_contradiction_clause,[],[f1259]) ).
tff(f1261,plain,
( ~ f6($true)
| ~ spl32_8
| spl32_9 ),
inference(forward_demodulation,[],[f181,f175]) ).
tff(f1264,plain,
( f6($true)
| ~ spl32_8
| ~ spl32_9 ),
inference(forward_demodulation,[],[f180,f175]) ).
tff(f1265,plain,
( f7($true)
| ~ spl32_37
| ~ spl32_38 ),
inference(forward_demodulation,[],[f326,f321]) ).
tff(f1269,plain,
( ~ f6($false)
| ( $true = bG3 )
| spl32_11 ),
inference(superposition,[],[f191,f137]) ).
tff(f1270,plain,
( spl32_10
| ~ spl32_72
| spl32_11 ),
inference(avatar_split_clause,[],[f1269,f189,f1046,f183]) ).
tff(f1272,plain,
( ~ f3($false)
| ( $true = bG8 )
| spl32_21 ),
inference(superposition,[],[f241,f137]) ).
tff(f1275,plain,
( ~ f7($false)
| ( $true = bG18 )
| spl32_40 ),
inference(superposition,[],[f337,f137]) ).
tff(f1276,plain,
( ( $true = bG18 )
| spl32_40
| ~ spl32_73 ),
inference(forward_subsumption_resolution,[],[f1275,f1089]) ).
tff(f1277,plain,
( spl32_39
| spl32_40
| ~ spl32_73 ),
inference(avatar_split_clause,[],[f1276,f1087,f335,f329]) ).
tff(f1283,plain,
( ~ f3($false)
| ( $true = bG25 )
| spl32_54 ),
inference(superposition,[],[f407,f137]) ).
tff(f1284,plain,
( spl32_53
| ~ spl32_67
| spl32_54 ),
inference(avatar_split_clause,[],[f1283,f405,f635,f399]) ).
tff(f1285,plain,
( $false
| ~ spl32_8
| ~ spl32_9
| ~ spl32_10
| spl32_11 ),
inference(forward_subsumption_resolution,[],[f1264,f1158]) ).
tff(f1286,plain,
( ~ spl32_8
| ~ spl32_9
| ~ spl32_10
| spl32_11 ),
inference(avatar_contradiction_clause,[],[f1285]) ).
tff(f1290,plain,
( ~ f6($false)
| ( $true = bG19 )
| spl32_42 ),
inference(superposition,[],[f347,f137]) ).
tff(f1291,plain,
( spl32_41
| ~ spl32_72
| spl32_42 ),
inference(avatar_split_clause,[],[f1290,f345,f1046,f339]) ).
tff(f1292,plain,
( $false
| ~ spl32_6
| ~ spl32_7
| ~ spl32_8
| spl32_9 ),
inference(forward_subsumption_resolution,[],[f1261,f1139]) ).
tff(f1293,plain,
( ~ spl32_6
| ~ spl32_7
| ~ spl32_8
| spl32_9 ),
inference(avatar_contradiction_clause,[],[f1292]) ).
tff(f1296,plain,
( ~ f6($false)
| ( $true = bG1 )
| spl32_7 ),
inference(superposition,[],[f171,f137]) ).
tff(f1297,plain,
( spl32_6
| ~ spl32_72
| spl32_7 ),
inference(avatar_split_clause,[],[f1296,f169,f1046,f163]) ).
tff(f1298,plain,
( ~ f6($false)
| ( $true = bG2 )
| spl32_9 ),
inference(superposition,[],[f181,f137]) ).
tff(f1299,plain,
( spl32_8
| ~ spl32_72
| spl32_9 ),
inference(avatar_split_clause,[],[f1298,f179,f1046,f173]) ).
tff(f1311,plain,
( $false
| ~ spl32_24
| ~ spl32_25
| ~ spl32_26
| spl32_27 ),
inference(forward_subsumption_resolution,[],[f984,f627]) ).
tff(f1312,plain,
( ~ spl32_24
| ~ spl32_25
| ~ spl32_26
| spl32_27 ),
inference(avatar_contradiction_clause,[],[f1311]) ).
tff(f1314,plain,
( spl32_20
| ~ spl32_67
| spl32_21 ),
inference(avatar_split_clause,[],[f1272,f239,f635,f233]) ).
tff(f1315,plain,
( f4($false)
| ( $true = bG5 )
| ~ spl32_15 ),
inference(superposition,[],[f210,f137]) ).
tff(f1316,plain,
( spl32_14
| spl32_68
| ~ spl32_15 ),
inference(avatar_split_clause,[],[f1315,f209,f646,f203]) ).
tff(f1317,plain,
( f4($false)
| ( $true = bG6 )
| ~ spl32_17 ),
inference(superposition,[],[f220,f137]) ).
tff(f1318,plain,
( spl32_16
| spl32_68
| ~ spl32_17 ),
inference(avatar_split_clause,[],[f1317,f219,f646,f213]) ).
tff(f1319,plain,
( f4($false)
| ( $true = bG7 )
| ~ spl32_19 ),
inference(superposition,[],[f230,f137]) ).
tff(f1320,plain,
( spl32_18
| spl32_68
| ~ spl32_19 ),
inference(avatar_split_clause,[],[f1319,f229,f646,f223]) ).
tff(f1321,plain,
( ~ f2($false)
| ( $true = bG9 )
| spl32_23 ),
inference(superposition,[],[f251,f137]) ).
tff(f1322,plain,
( spl32_22
| ~ spl32_66
| spl32_23 ),
inference(avatar_split_clause,[],[f1321,f249,f609,f243]) ).
tff(f1323,plain,
( ~ f2($false)
| ( $true = bG10 )
| spl32_25 ),
inference(superposition,[],[f261,f137]) ).
tff(f1324,plain,
( spl32_24
| ~ spl32_66
| spl32_25 ),
inference(avatar_split_clause,[],[f1323,f259,f609,f253]) ).
tff(f1325,plain,
( f4($false)
| ( $true = bG23 )
| ~ spl32_50 ),
inference(superposition,[],[f386,f137]) ).
tff(f1326,plain,
( spl32_49
| spl32_68
| ~ spl32_50 ),
inference(avatar_split_clause,[],[f1325,f385,f646,f379]) ).
tff(f1327,plain,
( f3($false)
| ( $true = bG24 )
| ~ spl32_52 ),
inference(superposition,[],[f396,f137]) ).
tff(f1328,plain,
( spl32_51
| spl32_67
| ~ spl32_52 ),
inference(avatar_split_clause,[],[f1327,f395,f635,f389]) ).
tff(f1329,plain,
( f3($false)
| ( $true = bG26 )
| ~ spl32_56 ),
inference(superposition,[],[f416,f137]) ).
tff(f1330,plain,
( spl32_55
| spl32_67
| ~ spl32_56 ),
inference(avatar_split_clause,[],[f1329,f415,f635,f409]) ).
tff(f1343,plain,
( f3($false)
| ( $true = bG25 )
| ~ spl32_54 ),
inference(superposition,[],[f406,f137]) ).
tff(f1344,plain,
( spl32_53
| spl32_67
| ~ spl32_54 ),
inference(avatar_split_clause,[],[f1343,f405,f635,f399]) ).
tff(f1346,plain,
( ~ f3($true)
| ~ spl32_20
| spl32_21 ),
inference(superposition,[],[f241,f235]) ).
tff(f1348,plain,
( $false
| ~ spl32_20
| spl32_21
| ~ spl32_51
| ~ spl32_52 ),
inference(forward_subsumption_resolution,[],[f1346,f1174]) ).
tff(f1349,plain,
( ~ spl32_20
| spl32_21
| ~ spl32_51
| ~ spl32_52 ),
inference(avatar_contradiction_clause,[],[f1348]) ).
tff(f1350,plain,
( ~ f3($false)
| ( $true = bG24 )
| spl32_52 ),
inference(superposition,[],[f397,f137]) ).
tff(f1351,plain,
( spl32_51
| ~ spl32_67
| spl32_52 ),
inference(avatar_split_clause,[],[f1350,f395,f635,f389]) ).
tff(f1361,plain,
( ~ f7($true)
| ~ spl32_39
| spl32_40 ),
inference(superposition,[],[f337,f331]) ).
tff(f1379,plain,
( f3($true)
| ~ spl32_55
| ~ spl32_56 ),
inference(superposition,[],[f416,f411]) ).
tff(f1381,plain,
( $false
| ~ spl32_51
| spl32_52
| ~ spl32_55
| ~ spl32_56 ),
inference(forward_subsumption_resolution,[],[f1379,f1178]) ).
tff(f1382,plain,
( ~ spl32_51
| spl32_52
| ~ spl32_55
| ~ spl32_56 ),
inference(avatar_contradiction_clause,[],[f1381]) ).
tff(f1387,plain,
( f6($false)
| ( $true = bG2 )
| ~ spl32_9 ),
inference(superposition,[],[f180,f137]) ).
tff(f1391,plain,
( f6($false)
| ( $true = bG19 )
| ~ spl32_42 ),
inference(superposition,[],[f346,f137]) ).
tff(f1408,plain,
( $false
| ~ spl32_37
| ~ spl32_38
| ~ spl32_39
| spl32_40 ),
inference(forward_subsumption_resolution,[],[f1361,f1265]) ).
tff(f1409,plain,
( ~ spl32_37
| ~ spl32_38
| ~ spl32_39
| spl32_40 ),
inference(avatar_contradiction_clause,[],[f1408]) ).
tff(f1413,plain,
( spl32_41
| spl32_72
| ~ spl32_42 ),
inference(avatar_split_clause,[],[f1391,f345,f1046,f339]) ).
tff(f1414,plain,
( spl32_8
| spl32_72
| ~ spl32_9 ),
inference(avatar_split_clause,[],[f1387,f179,f1046,f173]) ).
tff(f1417,plain,
( ~ f4($false)
| ( $true = bG5 )
| spl32_15 ),
inference(superposition,[],[f211,f137]) ).
tff(f1418,plain,
( spl32_14
| ~ spl32_68
| spl32_15 ),
inference(avatar_split_clause,[],[f1417,f209,f646,f203]) ).
tff(f1421,plain,
( ~ f4($false)
| ( $true = bG7 )
| spl32_19 ),
inference(superposition,[],[f231,f137]) ).
tff(f1422,plain,
( spl32_18
| ~ spl32_68
| spl32_19 ),
inference(avatar_split_clause,[],[f1421,f229,f646,f223]) ).
tff(f1445,plain,
( f5($true)
| ~ spl32_47
| ~ spl32_48 ),
inference(superposition,[],[f376,f371]) ).
tff(f1447,plain,
( $false
| ~ spl32_43
| spl32_44
| ~ spl32_47
| ~ spl32_48 ),
inference(forward_subsumption_resolution,[],[f1445,f1026]) ).
tff(f1448,plain,
( ~ spl32_43
| spl32_44
| ~ spl32_47
| ~ spl32_48 ),
inference(avatar_contradiction_clause,[],[f1447]) ).
cnf(s1,plain,
( spl32_1
| spl32_2 ),
inference(sat_conversion,[],[f146]) ).
cnf(s2,plain,
( ~ spl32_1
| ~ spl32_2 ),
inference(sat_conversion,[],[f147]) ).
cnf(s3,plain,
( ~ spl32_3
| spl32_4 ),
inference(sat_conversion,[],[f156]) ).
cnf(s4,plain,
( spl32_3
| ~ spl32_4 ),
inference(sat_conversion,[],[f157]) ).
cnf(s5,plain,
( ~ spl32_5
| spl32_6 ),
inference(sat_conversion,[],[f166]) ).
cnf(s6,plain,
( spl32_5
| ~ spl32_6 ),
inference(sat_conversion,[],[f167]) ).
cnf(s7,plain,
( ~ spl32_7
| spl32_8 ),
inference(sat_conversion,[],[f176]) ).
cnf(s8,plain,
( spl32_7
| ~ spl32_8 ),
inference(sat_conversion,[],[f177]) ).
cnf(s9,plain,
( ~ spl32_9
| spl32_10 ),
inference(sat_conversion,[],[f186]) ).
cnf(s10,plain,
( spl32_9
| ~ spl32_10 ),
inference(sat_conversion,[],[f187]) ).
cnf(s11,plain,
( ~ spl32_11
| spl32_12 ),
inference(sat_conversion,[],[f196]) ).
cnf(s12,plain,
( spl32_11
| ~ spl32_12 ),
inference(sat_conversion,[],[f197]) ).
cnf(s13,plain,
( ~ spl32_13
| spl32_14 ),
inference(sat_conversion,[],[f206]) ).
cnf(s14,plain,
( spl32_13
| ~ spl32_14 ),
inference(sat_conversion,[],[f207]) ).
cnf(s15,plain,
( ~ spl32_15
| spl32_16 ),
inference(sat_conversion,[],[f216]) ).
cnf(s16,plain,
( spl32_15
| ~ spl32_16 ),
inference(sat_conversion,[],[f217]) ).
cnf(s17,plain,
( ~ spl32_17
| spl32_18 ),
inference(sat_conversion,[],[f226]) ).
cnf(s18,plain,
( spl32_17
| ~ spl32_18 ),
inference(sat_conversion,[],[f227]) ).
cnf(s19,plain,
( ~ spl32_19
| spl32_20 ),
inference(sat_conversion,[],[f236]) ).
cnf(s20,plain,
( spl32_19
| ~ spl32_20 ),
inference(sat_conversion,[],[f237]) ).
cnf(s21,plain,
( ~ spl32_21
| spl32_22 ),
inference(sat_conversion,[],[f246]) ).
cnf(s22,plain,
( spl32_21
| ~ spl32_22 ),
inference(sat_conversion,[],[f247]) ).
cnf(s23,plain,
( ~ spl32_23
| spl32_24 ),
inference(sat_conversion,[],[f256]) ).
cnf(s24,plain,
( spl32_23
| ~ spl32_24 ),
inference(sat_conversion,[],[f257]) ).
cnf(s25,plain,
( ~ spl32_25
| spl32_26 ),
inference(sat_conversion,[],[f266]) ).
cnf(s26,plain,
( spl32_25
| ~ spl32_26 ),
inference(sat_conversion,[],[f267]) ).
cnf(s27,plain,
( ~ spl32_27
| spl32_28 ),
inference(sat_conversion,[],[f276]) ).
cnf(s28,plain,
( spl32_27
| ~ spl32_28 ),
inference(sat_conversion,[],[f277]) ).
cnf(s29,plain,
( ~ spl32_29
| spl32_30 ),
inference(sat_conversion,[],[f286]) ).
cnf(s30,plain,
( spl32_29
| ~ spl32_30 ),
inference(sat_conversion,[],[f287]) ).
cnf(s31,plain,
( ~ spl32_31
| spl32_32 ),
inference(sat_conversion,[],[f296]) ).
cnf(s32,plain,
( spl32_31
| ~ spl32_32 ),
inference(sat_conversion,[],[f297]) ).
cnf(s33,plain,
( ~ spl32_33
| spl32_34 ),
inference(sat_conversion,[],[f306]) ).
cnf(s34,plain,
( spl32_33
| ~ spl32_34 ),
inference(sat_conversion,[],[f307]) ).
cnf(s35,plain,
( ~ spl32_3
| spl32_35 ),
inference(sat_conversion,[],[f312]) ).
cnf(s36,plain,
( spl32_3
| ~ spl32_35 ),
inference(sat_conversion,[],[f313]) ).
cnf(s37,plain,
( ~ spl32_36
| spl32_37 ),
inference(sat_conversion,[],[f322]) ).
cnf(s38,plain,
( spl32_36
| ~ spl32_37 ),
inference(sat_conversion,[],[f323]) ).
cnf(s39,plain,
( ~ spl32_38
| spl32_39 ),
inference(sat_conversion,[],[f332]) ).
cnf(s40,plain,
( spl32_38
| ~ spl32_39 ),
inference(sat_conversion,[],[f333]) ).
cnf(s41,plain,
( ~ spl32_40
| spl32_41 ),
inference(sat_conversion,[],[f342]) ).
cnf(s42,plain,
( spl32_40
| ~ spl32_41 ),
inference(sat_conversion,[],[f343]) ).
cnf(s43,plain,
( ~ spl32_42
| spl32_43 ),
inference(sat_conversion,[],[f352]) ).
cnf(s44,plain,
( spl32_42
| ~ spl32_43 ),
inference(sat_conversion,[],[f353]) ).
cnf(s45,plain,
( ~ spl32_44
| spl32_45 ),
inference(sat_conversion,[],[f362]) ).
cnf(s46,plain,
( spl32_44
| ~ spl32_45 ),
inference(sat_conversion,[],[f363]) ).
cnf(s47,plain,
( ~ spl32_46
| spl32_47 ),
inference(sat_conversion,[],[f372]) ).
cnf(s48,plain,
( spl32_46
| ~ spl32_47 ),
inference(sat_conversion,[],[f373]) ).
cnf(s49,plain,
( ~ spl32_48
| spl32_49 ),
inference(sat_conversion,[],[f382]) ).
cnf(s50,plain,
( spl32_48
| ~ spl32_49 ),
inference(sat_conversion,[],[f383]) ).
cnf(s51,plain,
( ~ spl32_50
| spl32_51 ),
inference(sat_conversion,[],[f392]) ).
cnf(s52,plain,
( spl32_50
| ~ spl32_51 ),
inference(sat_conversion,[],[f393]) ).
cnf(s53,plain,
( ~ spl32_52
| spl32_53 ),
inference(sat_conversion,[],[f402]) ).
cnf(s54,plain,
( spl32_52
| ~ spl32_53 ),
inference(sat_conversion,[],[f403]) ).
cnf(s55,plain,
( ~ spl32_54
| spl32_55 ),
inference(sat_conversion,[],[f412]) ).
cnf(s56,plain,
( spl32_54
| ~ spl32_55 ),
inference(sat_conversion,[],[f413]) ).
cnf(s57,plain,
( ~ spl32_56
| spl32_57 ),
inference(sat_conversion,[],[f422]) ).
cnf(s58,plain,
( spl32_56
| ~ spl32_57 ),
inference(sat_conversion,[],[f423]) ).
cnf(s59,plain,
( ~ spl32_58
| spl32_59 ),
inference(sat_conversion,[],[f432]) ).
cnf(s60,plain,
( spl32_58
| ~ spl32_59 ),
inference(sat_conversion,[],[f433]) ).
cnf(s61,plain,
( ~ spl32_60
| spl32_61 ),
inference(sat_conversion,[],[f442]) ).
cnf(s62,plain,
( spl32_60
| ~ spl32_61 ),
inference(sat_conversion,[],[f443]) ).
cnf(s63,plain,
( ~ spl32_62
| spl32_63 ),
inference(sat_conversion,[],[f452]) ).
cnf(s64,plain,
( spl32_62
| ~ spl32_63 ),
inference(sat_conversion,[],[f453]) ).
cnf(s65,plain,
( ~ spl32_64
| spl32_65 ),
inference(sat_conversion,[],[f462]) ).
cnf(s66,plain,
( spl32_64
| ~ spl32_65 ),
inference(sat_conversion,[],[f463]) ).
cnf(s68,plain,
( spl32_1
| ~ spl32_2
| spl32_34
| spl32_65 ),
inference(sat_conversion,[],[f566]) ).
cnf(s71,plain,
( ~ spl32_2
| spl32_30
| spl32_31
| spl32_65 ),
inference(sat_conversion,[],[f573]) ).
cnf(s74,plain,
( spl32_28
| ~ spl32_29
| spl32_63
| spl32_64 ),
inference(sat_conversion,[],[f593]) ).
cnf(s76,plain,
( spl32_26
| ~ spl32_27
| spl32_57
| spl32_58 ),
inference(sat_conversion,[],[f598]) ).
cnf(s78,plain,
( spl32_24
| ~ spl32_25
| spl32_57
| spl32_58 ),
inference(sat_conversion,[],[f603]) ).
cnf(s79,plain,
( spl32_22
| ~ spl32_23
| spl32_57
| spl32_58 ),
inference(sat_conversion,[],[f607]) ).
cnf(s81,plain,
( spl32_26
| ~ spl32_27
| spl32_66 ),
inference(sat_conversion,[],[f613]) ).
cnf(s89,plain,
( spl32_18
| ~ spl32_19
| spl32_49
| spl32_50 ),
inference(sat_conversion,[],[f644]) ).
cnf(s90,plain,
( spl32_49
| spl32_50
| ~ spl32_68 ),
inference(sat_conversion,[],[f649]) ).
cnf(s100,plain,
( ~ spl32_14
| ~ spl32_15
| ~ spl32_49
| spl32_50 ),
inference(sat_conversion,[],[f690]) ).
cnf(s107,plain,
( ~ spl32_22
| ~ spl32_23
| ~ spl32_57
| spl32_58 ),
inference(sat_conversion,[],[f709]) ).
cnf(s108,plain,
( ~ spl32_22
| spl32_23
| ~ spl32_26
| ~ spl32_27 ),
inference(sat_conversion,[],[f713]) ).
cnf(s111,plain,
( ~ spl32_22
| ~ spl32_23
| ~ spl32_24
| spl32_25 ),
inference(sat_conversion,[],[f723]) ).
cnf(s119,plain,
( spl32_22
| ~ spl32_23
| spl32_66 ),
inference(sat_conversion,[],[f733]) ).
cnf(s123,plain,
( ~ spl32_28
| ~ spl32_29
| ~ spl32_59
| spl32_60 ),
inference(sat_conversion,[],[f751]) ).
cnf(s125,plain,
( spl32_1
| ~ spl32_32
| ~ spl32_33
| ~ spl32_34 ),
inference(sat_conversion,[],[f763]) ).
cnf(s130,plain,
( spl32_59
| ~ spl32_60
| spl32_63
| spl32_64 ),
inference(sat_conversion,[],[f773]) ).
cnf(s136,plain,
( ~ spl32_28
| ~ spl32_29
| ~ spl32_61
| spl32_62 ),
inference(sat_conversion,[],[f802]) ).
cnf(s138,plain,
( ~ spl32_28
| ~ spl32_29
| ~ spl32_63
| spl32_64 ),
inference(sat_conversion,[],[f813]) ).
cnf(s143,plain,
( ~ spl32_1
| spl32_2
| ~ spl32_34
| ~ spl32_65 ),
inference(sat_conversion,[],[f834]) ).
cnf(s144,plain,
( ~ spl32_1
| spl32_34
| spl32_71 ),
inference(sat_conversion,[],[f837]) ).
cnf(s145,plain,
( spl32_2
| ~ spl32_30
| ~ spl32_31
| ~ spl32_65 ),
inference(sat_conversion,[],[f839]) ).
cnf(s146,plain,
( ~ spl32_28
| spl32_29
| ~ spl32_63
| ~ spl32_64 ),
inference(sat_conversion,[],[f847]) ).
cnf(s149,plain,
( spl32_32
| spl32_33
| ~ spl32_71 ),
inference(sat_conversion,[],[f853]) ).
cnf(s152,plain,
( ~ spl32_2
| ~ spl32_30
| spl32_31
| ~ spl32_65 ),
inference(sat_conversion,[],[f866]) ).
cnf(s153,plain,
( spl32_63
| ~ spl32_64
| spl32_70 ),
inference(sat_conversion,[],[f870]) ).
cnf(s154,plain,
( ~ spl32_28
| spl32_29
| ~ spl32_59
| ~ spl32_60 ),
inference(sat_conversion,[],[f873]) ).
cnf(s155,plain,
( spl32_61
| spl32_62
| ~ spl32_70 ),
inference(sat_conversion,[],[f875]) ).
cnf(s156,plain,
( ~ spl32_14
| spl32_15
| ~ spl32_49
| ~ spl32_50 ),
inference(sat_conversion,[],[f878]) ).
cnf(s158,plain,
( ~ spl32_14
| spl32_15
| ~ spl32_18
| ~ spl32_19 ),
inference(sat_conversion,[],[f880]) ).
cnf(s167,plain,
( spl32_20
| ~ spl32_21
| spl32_67 ),
inference(sat_conversion,[],[f890]) ).
cnf(s170,plain,
( spl32_28
| spl32_29
| ~ spl32_70 ),
inference(sat_conversion,[],[f896]) ).
cnf(s180,plain,
( spl32_59
| ~ spl32_60
| spl32_70 ),
inference(sat_conversion,[],[f915]) ).
cnf(s181,plain,
( ~ spl32_22
| spl32_23
| ~ spl32_57
| ~ spl32_58 ),
inference(sat_conversion,[],[f917]) ).
cnf(s183,plain,
( ~ spl32_2
| ~ spl32_32
| spl32_33
| ~ spl32_65 ),
inference(sat_conversion,[],[f920]) ).
cnf(s200,plain,
( ~ spl32_61
| ~ spl32_62
| ~ spl32_63
| spl32_64 ),
inference(sat_conversion,[],[f949]) ).
cnf(s204,plain,
( spl32_63
| spl32_64
| ~ spl32_70 ),
inference(sat_conversion,[],[f951]) ).
cnf(s205,plain,
( spl32_32
| ~ spl32_33
| spl32_71 ),
inference(sat_conversion,[],[f952]) ).
cnf(s206,plain,
( spl32_2
| spl32_65
| ~ spl32_71 ),
inference(sat_conversion,[],[f955]) ).
cnf(s207,plain,
( spl32_30
| ~ spl32_31
| spl32_71 ),
inference(sat_conversion,[],[f959]) ).
cnf(s209,plain,
( spl32_26
| spl32_27
| ~ spl32_66 ),
inference(sat_conversion,[],[f960]) ).
cnf(s212,plain,
( spl32_24
| ~ spl32_25
| spl32_66 ),
inference(sat_conversion,[],[f968]) ).
cnf(s213,plain,
( spl32_28
| ~ spl32_29
| spl32_70 ),
inference(sat_conversion,[],[f970]) ).
cnf(s214,plain,
( spl32_55
| spl32_56
| ~ spl32_67 ),
inference(sat_conversion,[],[f972]) ).
cnf(s215,plain,
( spl32_57
| ~ spl32_58
| spl32_66 ),
inference(sat_conversion,[],[f974]) ).
cnf(s216,plain,
( spl32_59
| spl32_60
| ~ spl32_70 ),
inference(sat_conversion,[],[f976]) ).
cnf(s217,plain,
( spl32_61
| ~ spl32_62
| spl32_70 ),
inference(sat_conversion,[],[f978]) ).
cnf(s218,plain,
( ~ spl32_53
| ~ spl32_54
| ~ spl32_55
| spl32_56 ),
inference(sat_conversion,[],[f1002]) ).
cnf(s222,plain,
( spl32_12
| ~ spl32_13
| spl32_69 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s225,plain,
( ~ spl32_12
| ~ spl32_13
| ~ spl32_45
| spl32_46 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s228,plain,
( ~ spl32_12
| ~ spl32_13
| ~ spl32_43
| spl32_44 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s229,plain,
( spl32_43
| spl32_44
| ~ spl32_69 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s230,plain,
( spl32_10
| ~ spl32_11
| spl32_41
| spl32_42 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s237,plain,
( spl32_47
| spl32_48
| ~ spl32_69 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s241,plain,
( spl32_37
| spl32_38
| spl32_39
| ~ spl32_40 ),
inference(sat_conversion,[],[f1085]) ).
cnf(s242,plain,
( spl32_39
| ~ spl32_40
| spl32_73 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s246,plain,
( spl32_35
| spl32_36
| ~ spl32_73 ),
inference(sat_conversion,[],[f1096]) ).
cnf(s248,plain,
( ~ spl32_4
| spl32_5
| ~ spl32_39
| ~ spl32_40 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s249,plain,
( ~ spl32_4
| ~ spl32_5
| ~ spl32_35
| spl32_36 ),
inference(sat_conversion,[],[f1112]) ).
cnf(s251,plain,
( spl32_37
| ~ spl32_38
| spl32_73 ),
inference(sat_conversion,[],[f1113]) ).
cnf(s252,plain,
( spl32_4
| spl32_5
| ~ spl32_73 ),
inference(sat_conversion,[],[f1115]) ).
cnf(s253,plain,
( spl32_35
| ~ spl32_36
| spl32_73 ),
inference(sat_conversion,[],[f1117]) ).
cnf(s254,plain,
( spl32_4
| ~ spl32_5
| spl32_73 ),
inference(sat_conversion,[],[f1119]) ).
cnf(s255,plain,
( ~ spl32_6
| spl32_7
| ~ spl32_41
| ~ spl32_42 ),
inference(sat_conversion,[],[f1125]) ).
cnf(s256,plain,
( ~ spl32_45
| ~ spl32_46
| ~ spl32_47
| spl32_48 ),
inference(sat_conversion,[],[f1138]) ).
cnf(s263,plain,
( ~ spl32_6
| ~ spl32_7
| ~ spl32_41
| spl32_42 ),
inference(sat_conversion,[],[f1142]) ).
cnf(s265,plain,
( spl32_10
| ~ spl32_11
| spl32_72 ),
inference(sat_conversion,[],[f1147]) ).
cnf(s268,plain,
( ~ spl32_10
| ~ spl32_11
| ~ spl32_41
| spl32_42 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s270,plain,
( spl32_12
| spl32_13
| ~ spl32_69 ),
inference(sat_conversion,[],[f1161]) ).
cnf(s271,plain,
( ~ spl32_16
| ~ spl32_17
| ~ spl32_18
| spl32_19 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s272,plain,
( ~ spl32_20
| ~ spl32_21
| ~ spl32_55
| spl32_56 ),
inference(sat_conversion,[],[f1168]) ).
cnf(s277,plain,
( ~ spl32_20
| ~ spl32_21
| ~ spl32_51
| spl32_52 ),
inference(sat_conversion,[],[f1173]) ).
cnf(s278,plain,
( ~ spl32_20
| ~ spl32_21
| ~ spl32_53
| spl32_54 ),
inference(sat_conversion,[],[f1176]) ).
cnf(s287,plain,
( spl32_16
| spl32_17
| ~ spl32_68 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s289,plain,
( spl32_43
| ~ spl32_44
| spl32_69 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s290,plain,
( spl32_45
| ~ spl32_46
| spl32_69 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s291,plain,
( spl32_47
| ~ spl32_48
| spl32_69 ),
inference(sat_conversion,[],[f1195]) ).
cnf(s295,plain,
( spl32_6
| ~ spl32_7
| spl32_72 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s296,plain,
( ~ spl32_10
| spl32_11
| ~ spl32_41
| ~ spl32_42 ),
inference(sat_conversion,[],[f1206]) ).
cnf(s299,plain,
( ~ spl32_16
| spl32_17
| ~ spl32_49
| ~ spl32_50 ),
inference(sat_conversion,[],[f1234]) ).
cnf(s301,plain,
( spl32_45
| spl32_46
| ~ spl32_69 ),
inference(sat_conversion,[],[f1238]) ).
cnf(s302,plain,
( ~ spl32_35
| ~ spl32_36
| ~ spl32_37
| spl32_38 ),
inference(sat_conversion,[],[f1247]) ).
cnf(s303,plain,
( ~ spl32_12
| spl32_13
| ~ spl32_43
| ~ spl32_44 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s317,plain,
( spl32_10
| spl32_11
| ~ spl32_72 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s319,plain,
( spl32_39
| spl32_40
| ~ spl32_73 ),
inference(sat_conversion,[],[f1277]) ).
cnf(s322,plain,
( spl32_53
| spl32_54
| ~ spl32_67 ),
inference(sat_conversion,[],[f1284]) ).
cnf(s323,plain,
( ~ spl32_8
| ~ spl32_9
| ~ spl32_10
| spl32_11 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s328,plain,
( spl32_41
| spl32_42
| ~ spl32_72 ),
inference(sat_conversion,[],[f1291]) ).
cnf(s329,plain,
( ~ spl32_6
| ~ spl32_7
| ~ spl32_8
| spl32_9 ),
inference(sat_conversion,[],[f1293]) ).
cnf(s333,plain,
( spl32_6
| spl32_7
| ~ spl32_72 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s334,plain,
( spl32_8
| spl32_9
| ~ spl32_72 ),
inference(sat_conversion,[],[f1299]) ).
cnf(s337,plain,
( ~ spl32_24
| ~ spl32_25
| ~ spl32_26
| spl32_27 ),
inference(sat_conversion,[],[f1312]) ).
cnf(s343,plain,
( spl32_20
| spl32_21
| ~ spl32_67 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s344,plain,
( spl32_14
| ~ spl32_15
| spl32_68 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s345,plain,
( spl32_16
| ~ spl32_17
| spl32_68 ),
inference(sat_conversion,[],[f1318]) ).
cnf(s346,plain,
( spl32_18
| ~ spl32_19
| spl32_68 ),
inference(sat_conversion,[],[f1320]) ).
cnf(s347,plain,
( spl32_22
| spl32_23
| ~ spl32_66 ),
inference(sat_conversion,[],[f1322]) ).
cnf(s348,plain,
( spl32_24
| spl32_25
| ~ spl32_66 ),
inference(sat_conversion,[],[f1324]) ).
cnf(s349,plain,
( spl32_49
| ~ spl32_50
| spl32_68 ),
inference(sat_conversion,[],[f1326]) ).
cnf(s350,plain,
( spl32_51
| ~ spl32_52
| spl32_67 ),
inference(sat_conversion,[],[f1328]) ).
cnf(s351,plain,
( spl32_55
| ~ spl32_56
| spl32_67 ),
inference(sat_conversion,[],[f1330]) ).
cnf(s353,plain,
( spl32_53
| ~ spl32_54
| spl32_67 ),
inference(sat_conversion,[],[f1344]) ).
cnf(s354,plain,
( ~ spl32_20
| spl32_21
| ~ spl32_51
| ~ spl32_52 ),
inference(sat_conversion,[],[f1349]) ).
cnf(s355,plain,
( spl32_51
| spl32_52
| ~ spl32_67 ),
inference(sat_conversion,[],[f1351]) ).
cnf(s356,plain,
( ~ spl32_51
| spl32_52
| ~ spl32_55
| ~ spl32_56 ),
inference(sat_conversion,[],[f1382]) ).
cnf(s368,plain,
( ~ spl32_37
| ~ spl32_38
| ~ spl32_39
| spl32_40 ),
inference(sat_conversion,[],[f1409]) ).
cnf(s373,plain,
( spl32_41
| ~ spl32_42
| spl32_72 ),
inference(sat_conversion,[],[f1413]) ).
cnf(s374,plain,
( spl32_8
| ~ spl32_9
| spl32_72 ),
inference(sat_conversion,[],[f1414]) ).
cnf(s376,plain,
( spl32_14
| spl32_15
| ~ spl32_68 ),
inference(sat_conversion,[],[f1418]) ).
cnf(s378,plain,
( spl32_18
| spl32_19
| ~ spl32_68 ),
inference(sat_conversion,[],[f1422]) ).
cnf(s379,plain,
( ~ spl32_43
| spl32_44
| ~ spl32_47
| ~ spl32_48 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s380,plain,
( spl32_29
| spl32_28
| spl32_59
| spl32_1 ),
inference(rat,[],[s125,s31,s34,s71,s68,s66,s153,s64,s217,s62,s180,s30,s170,s1]) ).
cnf(s381,plain,
( ~ spl32_33
| ~ spl32_32
| spl32_1 ),
inference(rat,[],[s125,s33]) ).
cnf(s382,plain,
( ~ spl32_32
| spl32_1 ),
inference(rat,[],[s68,s183,s34,s381,s1]) ).
cnf(s383,plain,
( spl32_23
| spl32_57
| spl32_22
| spl32_1 ),
inference(rat,[],[s200,s64,s204,s65,s152,s61,s216,s29,s213,s380,s28,s81,s26,s60,s212,s215,s24,s347,s1,s31,s382]) ).
cnf(s384,plain,
( ~ spl32_28
| ~ spl32_29
| spl32_64
| ~ spl32_59 ),
inference(rat,[],[s136,s61,s63,s123,s138]) ).
cnf(s385,plain,
( spl32_27
| ~ spl32_24
| ~ spl32_66 ),
inference(rat,[],[s337,s26,s209]) ).
cnf(s386,plain,
( ~ spl32_29
| ~ spl32_28
| ~ spl32_59
| spl32_1 ),
inference(rat,[],[s65,s152,s384,s29,s1,s31,s382]) ).
cnf(s387,plain,
( spl32_21
| spl32_20
| spl32_51
| spl32_1 ),
inference(rat,[],[s155,s153,s63,s146,s66,s71,s62,s30,s154,s386,s27,s385,s59,s23,s79,s119,s383,s58,s351,s56,s353,s54,s350,s22,s343,s1,s31,s382]) ).
cnf(s388,plain,
( spl32_56
| ~ spl32_53
| ~ spl32_67 ),
inference(rat,[],[s218,s56,s214]) ).
cnf(s389,plain,
( ~ spl32_23
| spl32_27
| ~ spl32_22 ),
inference(rat,[],[s337,s25,s111,s23]) ).
cnf(s390,plain,
( ~ spl32_61
| spl32_64
| ~ spl32_63 ),
inference(rat,[],[s64,s200]) ).
cnf(s391,plain,
( spl32_27
| ~ spl32_57
| ~ spl32_22
| spl32_1 ),
inference(rat,[],[s390,s130,s61,s65,s216,s152,s213,s29,s380,s60,s181,s389,s28,s1,s31,s382]) ).
cnf(s392,plain,
( spl32_23
| ~ spl32_27
| ~ spl32_22 ),
inference(rat,[],[s348,s25,s81,s24,s108]) ).
cnf(s393,plain,
( spl32_15
| spl32_49
| spl32_14
| spl32_1 ),
inference(rat,[],[s155,s153,s63,s146,s66,s71,s62,s30,s154,s386,s59,s107,s392,s27,s391,s57,s388,s53,s355,s21,s167,s387,s20,s346,s18,s52,s345,s349,s16,s376,s1,s31,s382]) ).
cnf(s394,plain,
( spl32_22
| spl32_27
| spl32_57
| spl32_1 ),
inference(rat,[],[s385,s23,s119,s383]) ).
cnf(s395,plain,
( spl32_19
| ~ spl32_68
| ~ spl32_16 ),
inference(rat,[],[s271,s18,s378]) ).
cnf(s396,plain,
( ~ spl32_21
| spl32_56
| ~ spl32_20
| ~ spl32_51 ),
inference(rat,[],[s278,s55,s53,s272,s277]) ).
cnf(s397,plain,
( spl32_57
| ~ spl32_20
| ~ spl32_51
| spl32_1 ),
inference(rat,[],[s155,s153,s63,s146,s66,s71,s62,s30,s154,s386,s59,s27,s79,s394,s383,s22,s396,s57,s1,s31,s382]) ).
cnf(s398,plain,
( spl32_52
| ~ spl32_56
| ~ spl32_51 ),
inference(rat,[],[s322,s55,s351,s54,s356]) ).
cnf(s399,plain,
( spl32_13
| spl32_12
| spl32_43
| spl32_1 ),
inference(rat,[],[s155,s153,s63,s146,s66,s71,s62,s30,s154,s386,s59,s107,s392,s27,s391,s21,s354,s398,s58,s397,s19,s395,s51,s90,s344,s15,s393,s50,s291,s48,s290,s46,s289,s14,s270,s1,s31,s382]) ).
cnf(s400,plain,
( spl32_48
| ~ spl32_45
| ~ spl32_69 ),
inference(rat,[],[s256,s48,s237]) ).
cnf(s401,plain,
( spl32_20
| ~ spl32_21
| spl32_56
| ~ spl32_49
| ~ spl32_14 ),
inference(rat,[],[s271,s17,s299,s15,s156,s52,s355,s53,s388,s167,s19]) ).
cnf(s402,plain,
( spl32_15
| ~ spl32_19
| ~ spl32_14 ),
inference(rat,[],[s287,s17,s346,s16,s158]) ).
cnf(s403,plain,
( ~ spl32_20
| spl32_57
| ~ spl32_49
| ~ spl32_14
| spl32_1 ),
inference(rat,[],[s402,s100,s51,s397,s20]) ).
cnf(s404,plain,
( spl32_57
| ~ spl32_49
| ~ spl32_14
| spl32_1 ),
inference(rat,[],[s271,s17,s299,s15,s156,s52,s387,s401,s19,s403,s57]) ).
cnf(s405,plain,
( ~ spl32_22
| ~ spl32_57
| spl32_1 ),
inference(rat,[],[s155,s153,s63,s146,s66,s71,s62,s30,s154,s386,s59,s107,s392,s27,s391,s1,s31,s382]) ).
cnf(s406,plain,
( spl32_20
| ~ spl32_49
| ~ spl32_14
| spl32_1 ),
inference(rat,[],[s271,s17,s299,s15,s156,s52,s387,s19,s21,s405,s404]) ).
cnf(s407,plain,
( ~ spl32_49
| ~ spl32_14
| spl32_1 ),
inference(rat,[],[s354,s398,s51,s100,s402,s20,s406,s21,s405,s58,s404]) ).
cnf(s408,plain,
( spl32_12
| spl32_43
| spl32_1 ),
inference(rat,[],[s407,s49,s400,s45,s229,s222,s13,s399]) ).
cnf(s409,plain,
( spl32_7
| spl32_41
| spl32_6
| spl32_1 ),
inference(rat,[],[s408,s12,s230,s10,s44,s374,s373,s8,s333]) ).
cnf(s412,plain,
( spl32_11
| ~ spl32_72
| ~ spl32_8 ),
inference(rat,[],[s323,s10,s317]) ).
cnf(s413,plain,
( spl32_49
| ~ spl32_50
| spl32_19
| ~ spl32_12
| ~ spl32_43 ),
inference(rat,[],[s256,s47,s225,s45,s228,s14,s376,s15,s395,s349,s49]) ).
cnf(s414,plain,
( spl32_44
| ~ spl32_48
| ~ spl32_43 ),
inference(rat,[],[s301,s47,s291,s46,s379]) ).
cnf(s415,plain,
( ~ spl32_49
| ~ spl32_12
| ~ spl32_43
| spl32_1 ),
inference(rat,[],[s414,s303,s13,s407,s50]) ).
cnf(s417,plain,
( ~ spl32_13
| spl32_48
| ~ spl32_12
| ~ spl32_43 ),
inference(rat,[],[s256,s47,s225,s45,s228]) ).
cnf(s418,plain,
( ~ spl32_20
| ~ spl32_51
| spl32_1 ),
inference(rat,[],[s354,s21,s398,s405,s58,s397]) ).
cnf(s419,plain,
( spl32_14
| spl32_49
| spl32_1 ),
inference(rat,[],[s418,s19,s51,s395,s90,s344,s15,s393]) ).
cnf(s420,plain,
( ~ spl32_12
| ~ spl32_43
| spl32_1 ),
inference(rat,[],[s419,s14,s417,s49,s415]) ).
cnf(s421,plain,
( spl32_41
| spl32_6
| spl32_1 ),
inference(rat,[],[s420,s11,s412,s43,s328,s295,s7,s409]) ).
cnf(s422,plain,
( spl32_5
| spl32_3
| spl32_1 ),
inference(rat,[],[s421,s42,s242,s40,s251,s38,s253,s6,s252,s36,s4]) ).
cnf(s424,plain,
( spl32_40
| ~ spl32_37
| ~ spl32_73 ),
inference(rat,[],[s368,s40,s319]) ).
cnf(s425,plain,
( spl32_43
| spl32_3
| spl32_1 ),
inference(rat,[],[s334,s265,s9,s268,s8,s12,s263,s408,s43,s5,s41,s424,s37,s246,s36,s254,s422,s4]) ).
cnf(s426,plain,
( spl32_3
| spl32_1 ),
inference(rat,[],[s9,s329,s296,s7,s11,s255,s420,s44,s425,s41,s424,s37,s246,s254,s5,s422,s4,s36]) ).
cnf(s427,plain,
( spl32_41
| spl32_1 ),
inference(rat,[],[s368,s39,s302,s37,s249,s6,s421,s41,s35,s3,s426]) ).
cnf(s428,plain,
( spl32_39
| spl32_1 ),
inference(rat,[],[s302,s38,s241,s39,s35,s426,s42,s427]) ).
cnf(s429,plain,
( spl32_43
| spl32_1 ),
inference(rat,[],[s334,s265,s9,s268,s8,s12,s263,s408,s43,s5,s248,s428,s3,s426,s42,s427]) ).
cnf(s430,plain,
spl32_1,
inference(rat,[],[s9,s329,s296,s7,s11,s255,s420,s44,s429,s5,s248,s428,s42,s427,s3,s426]) ).
cnf(s431,plain,
~ spl32_2,
inference(rat,[],[s2,s430]) ).
cnf(s432,plain,
( spl32_64
| spl32_59
| spl32_28 ),
inference(rat,[],[s61,s390,s216,s74,s213,s30,s207,s32,s205,s34,s144,s206,s66,s430,s431]) ).
cnf(s433,plain,
( spl32_59
| spl32_28 ),
inference(rat,[],[s217,s64,s62,s153,s180,s170,s29,s145,s32,s149,s33,s144,s143,s65,s432,s430,s431]) ).
cnf(s434,plain,
( spl32_27
| spl32_22
| spl32_57 ),
inference(rat,[],[s23,s385,s347,s215,s60,s433,s28]) ).
cnf(s435,plain,
( spl32_58
| spl32_22
| spl32_57 ),
inference(rat,[],[s78,s26,s24,s76,s79,s434]) ).
cnf(s436,plain,
( spl32_64
| ~ spl32_59
| ~ spl32_28 ),
inference(rat,[],[s205,s32,s34,s207,s144,s30,s206,s384,s66,s430,s431]) ).
cnf(s437,plain,
( ~ spl32_59
| ~ spl32_28 ),
inference(rat,[],[s155,s153,s63,s62,s146,s154,s29,s145,s32,s149,s33,s144,s143,s65,s436,s430,s431]) ).
cnf(s438,plain,
( spl32_22
| spl32_57 ),
inference(rat,[],[s437,s59,s435,s27,s434]) ).
cnf(s439,plain,
( spl32_57
| spl32_51
| spl32_20 ),
inference(rat,[],[s53,s355,s388,s167,s22,s438,s57]) ).
cnf(s440,plain,
( spl32_67
| ~ spl32_56
| spl32_51 ),
inference(rat,[],[s353,s56,s54,s351,s350]) ).
cnf(s441,plain,
( spl32_59
| ~ spl32_22
| ~ spl32_57 ),
inference(rat,[],[s392,s28,s107,s433,s59]) ).
cnf(s442,plain,
( ~ spl32_22
| ~ spl32_57 ),
inference(rat,[],[s389,s27,s181,s437,s60,s441]) ).
cnf(s443,plain,
( spl32_51
| spl32_20 ),
inference(rat,[],[s442,s21,s343,s440,s58,s439]) ).
cnf(s444,plain,
( spl32_49
| spl32_20
| spl32_12
| spl32_43 ),
inference(rat,[],[s45,s400,s229,s222,s14,s376,s15,s395,s349,s49,s19,s52,s443]) ).
cnf(s445,plain,
( spl32_69
| ~ spl32_48
| spl32_43 ),
inference(rat,[],[s290,s48,s46,s291,s289]) ).
cnf(s446,plain,
( spl32_20
| spl32_12
| spl32_43 ),
inference(rat,[],[s271,s17,s299,s15,s156,s13,s270,s445,s50,s444,s52,s443,s19]) ).
cnf(s447,plain,
( spl32_49
| spl32_50
| spl32_12
| spl32_43 ),
inference(rat,[],[s45,s400,s229,s222,s14,s344,s16,s345,s18,s89,s90,s49,s20,s446]) ).
cnf(s448,plain,
( spl32_50
| spl32_12
| spl32_43 ),
inference(rat,[],[s100,s402,s13,s270,s445,s50,s447,s20,s446]) ).
cnf(s449,plain,
( spl32_57
| ~ spl32_51
| ~ spl32_20 ),
inference(rat,[],[s22,s396,s438,s57]) ).
cnf(s450,plain,
( ~ spl32_51
| ~ spl32_20 ),
inference(rat,[],[s354,s21,s398,s442,s58,s449]) ).
cnf(s451,plain,
( spl32_12
| spl32_43 ),
inference(rat,[],[s450,s51,s448,s446]) ).
cnf(s452,plain,
( spl32_4
| ~ spl32_5
| spl32_40 ),
inference(rat,[],[s37,s424,s246,s36,s254,s3]) ).
cnf(s453,plain,
( ~ spl32_5
| spl32_40 ),
inference(rat,[],[s368,s39,s302,s37,s249,s35,s4,s452]) ).
cnf(s454,plain,
( spl32_43
| spl32_41 ),
inference(rat,[],[s374,s10,s8,s230,s295,s12,s328,s451,s43,s6,s453,s41]) ).
cnf(s455,plain,
( ~ spl32_12
| ~ spl32_50
| ~ spl32_43
| spl32_19 ),
inference(rat,[],[s271,s17,s299,s15,s156,s13,s303,s414,s50,s413]) ).
cnf(s456,plain,
( spl32_20
| spl32_41 ),
inference(rat,[],[s455,s52,s443,s19,s11,s412,s7,s333,s6,s453,s41,s373,s44,s454]) ).
cnf(s457,plain,
( spl32_49
| spl32_41 ),
inference(rat,[],[s16,s344,s345,s14,s18,s417,s89,s90,s49,s11,s412,s7,s333,s6,s453,s41,s373,s44,s454,s20,s51,s450,s456]) ).
cnf(s458,plain,
spl32_41,
inference(rat,[],[s100,s402,s13,s303,s414,s50,s457,s51,s450,s20,s456,s11,s412,s7,s333,s373,s44,s454,s6,s453,s41]) ).
cnf(s459,plain,
spl32_40,
inference(rat,[],[s42,s458]) ).
cnf(s460,plain,
( spl32_73
| spl32_35 ),
inference(rat,[],[s251,s40,s38,s242,s253,s459]) ).
cnf(s461,plain,
( spl32_4
| spl32_5 ),
inference(rat,[],[s460,s36,s252,s3]) ).
cnf(s462,plain,
spl32_5,
inference(rat,[],[s302,s38,s241,s39,s35,s248,s4,s461,s459]) ).
cnf(s463,plain,
spl32_6,
inference(rat,[],[s5,s462]) ).
cnf(s464,plain,
spl32_43,
inference(rat,[],[s334,s265,s9,s268,s8,s12,s263,s451,s43,s458,s463]) ).
cnf(s465,plain,
spl32_42,
inference(rat,[],[s44,s464]) ).
cnf(s466,plain,
spl32_7,
inference(rat,[],[s255,s458,s463,s465]) ).
cnf(s467,plain,
spl32_8,
inference(rat,[],[s7,s466]) ).
cnf(s468,plain,
spl32_9,
inference(rat,[],[s329,s466,s463,s467]) ).
cnf(s469,plain,
spl32_10,
inference(rat,[],[s9,s468]) ).
cnf(s470,plain,
spl32_11,
inference(rat,[],[s296,s465,s458,s469]) ).
cnf(s471,plain,
spl32_12,
inference(rat,[],[s11,s470]) ).
cnf(s472,plain,
spl32_20,
inference(rat,[],[s52,s455,s443,s19,s464,s471]) ).
cnf(s473,plain,
spl32_19,
inference(rat,[],[s20,s472]) ).
cnf(s474,plain,
~ spl32_51,
inference(rat,[],[s450,s472]) ).
cnf(s475,plain,
~ spl32_50,
inference(rat,[],[s51,s474]) ).
cnf(s476,plain,
spl32_49,
inference(rat,[],[s16,s344,s345,s14,s18,s417,s89,s90,s49,s471,s464,s475,s473]) ).
cnf(s477,plain,
spl32_48,
inference(rat,[],[s50,s476]) ).
cnf(s478,plain,
spl32_44,
inference(rat,[],[s414,s464,s477]) ).
cnf(s480,plain,
spl32_13,
inference(rat,[],[s303,s471,s464,s478]) ).
cnf(s482,plain,
spl32_14,
inference(rat,[],[s13,s480]) ).
cnf(s484,plain,
spl32_15,
inference(rat,[],[s402,s473,s482]) ).
cnf(s485,plain,
$false,
inference(rat,[],[s100,s475,s476,s482,s484]) ).
tff(f1449,plain,
$false,
inference(avatar_sat_refutation,[],[s485]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO500_8.008 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n003.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 17:48:27 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.65/0.87 % (1816127)Detected formulas, will run a generic FOF schedule.
% 2.65/0.87 % (1816226)dis-21_1_sil=8000:lcm=predicate:random_seed=519406635:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.65/0.87 % (1816226)Refutation not found, incomplete strategy
% 2.65/0.87 % (1816226)------------------------------
% 2.65/0.87 % (1816226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.65/0.87 % (1816226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.87 % (1816226)CaDiCaL version: 2.1.3
% 2.65/0.87 % (1816226)Termination reason: Refutation not found, incomplete strategy
% 2.65/0.87 % (1816226)Time elapsed: 0.002 s
% 2.65/0.87 % (1816226)Peak memory usage: 89 MB
% 2.65/0.87 % (1816226)Instructions burned: 5 (million)
% 2.65/0.87 % (1816224)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3689617125:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.65/0.87 % (1816223)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3161780146:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.65/0.87 % (1816220)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=2820168035:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.65/0.87 % (1816218)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=2658607544:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.65/0.87 % (1816221)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1958170186:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.65/0.87 % (1816219)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=1017810826:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.65/0.87 % (1816221)Refutation not found, incomplete strategy
% 2.65/0.87 % (1816221)------------------------------
% 2.65/0.87 % (1816221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.65/0.87 % (1816221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.87 % (1816221)CaDiCaL version: 2.1.3
% 2.65/0.87 % (1816221)Termination reason: Refutation not found, incomplete strategy
% 2.65/0.87 % (1816221)Time elapsed: 0.002 s
% 2.65/0.87 % (1816221)Peak memory usage: 88 MB
% 2.65/0.87 % (1816221)Instructions burned: 2 (million)
% 2.65/0.87 % (1816224)First to succeed.
% 2.65/0.87 % (1816224)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1816127"
% 2.65/0.87 % (1816223)Instruction limit reached!
% 2.65/0.87 % (1816223)------------------------------
% 2.65/0.87 % (1816223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.65/0.87 % (1816223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.87 % (1816223)CaDiCaL version: 2.1.3
% 2.65/0.87 % (1816223)Termination reason: Instruction limit
% 2.65/0.87 % (1816223)Termination phase: Saturation
% 2.65/0.87 % (1816223)Time elapsed: 0.056 s
% 2.65/0.87 % (1816223)Peak memory usage: 88 MB
% 2.65/0.87 % (1816223)Instructions burned: 119 (million)
% 2.65/0.87 % (1816226)------------------------------
% 2.65/0.87 % (1816226)------------------------------
% 2.65/0.87 % (1816238)lrs+10_1_sil=8000:sp=occurrence:random_seed=3278885009:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 2.65/0.87 % (1816239)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2791966195:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 2.65/0.87 % (1816221)------------------------------
% 2.65/0.87 % (1816221)------------------------------
% 2.65/0.87 % (1816239)Instruction limit reached!
% 2.65/0.87 % (1816239)------------------------------
% 2.65/0.87 % (1816239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.65/0.87 % (1816239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.87 % (1816239)CaDiCaL version: 2.1.3
% 2.65/0.87 % (1816239)Termination reason: Instruction limit
% 2.65/0.87 % (1816239)Termination phase: Saturation
% 2.65/0.87 % (1816239)Time elapsed: 0.036 s
% 2.65/0.87 % (1816239)Peak memory usage: 89 MB
% 2.65/0.87 % (1816239)Instructions burned: 158 (million)
% 2.65/0.87 % (1816224)Refutation found. Thanks to Tanya!
% 2.65/0.87 % SZS status Theorem for theBenchmark
% 2.65/0.87 % SZS output start Proof for theBenchmark
% See solution above
% 3.60/1.06 % (1816224)------------------------------
% 3.60/1.06 % (1816224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.60/1.06 % (1816224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/1.06 % (1816224)CaDiCaL version: 2.1.3
% 3.60/1.06 % (1816224)Termination reason: Refutation
% 3.60/1.06 % (1816224)Time elapsed: 0.038 s
% 3.60/1.06 % (1816224)Peak memory usage: 90 MB
% 3.60/1.06 % (1816224)Instructions burned: 55 (million)
% 3.60/1.06 % (1816224)------------------------------
% 3.60/1.06 % (1816224)------------------------------
% 3.60/1.06 % (1816127)Success in time 0.458 s
% 3.60/1.06 % Vampire exiting
%------------------------------------------------------------------------------