%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO500_8.004 : 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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:26:43 PM UTC 2026
% Result : Theorem 3.00s 1.12s
% Output : Refutation 3.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 55
% Syntax : Number of formulae : 496 ( 16 unt; 0 typ; 53 def)
% Number of atoms : 1925 ( 163 equ)
% Maximal formula atoms : 5 ( 3 avg)
% Number of connectives : 1473 ( 609 ~; 792 |; 17 &)
% ( 54 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 569 ( 565 fml; 4 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 61 ( 58 usr; 56 prp; 0-2 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 2 ( 0 sgn 2 !; 0 ?; 2 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
bG0: $o ).
tff(func_def_3,type,
bG1: $o ).
tff(func_def_4,type,
bG2: $o ).
tff(func_def_5,type,
bG3: $o ).
tff(func_def_6,type,
bG4: $o ).
tff(func_def_7,type,
bG5: $o ).
tff(func_def_8,type,
bG6: $o ).
tff(func_def_9,type,
bG7: $o ).
tff(func_def_10,type,
bG8: $o ).
tff(func_def_11,type,
bG9: $o ).
tff(func_def_12,type,
bG10: $o ).
tff(func_def_13,type,
bG11: $o ).
tff(func_def_14,type,
bG12: $o ).
tff(func_def_15,type,
bG13: $o ).
tff(func_def_16,type,
bG14: $o ).
tff(func_def_17,type,
bG15: $o ).
tff(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(f1,conjecture,
f0(f0(f0(f1(f2(f2(f2(f3(x)))))))) = f0(f1(f1(f1(f2(f3(f3(f3(x)))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kaminski4) ).
tff(f2,negated_conjecture,
f0(f0(f0(f1(f2(f2(f2(f3(x)))))))) != f0(f1(f1(f1(f2(f3(f3(f3(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,
( f3(bG0)
<=> ( $true = bG1 ) ),
introduced(definition,[new_symbols(definition,[bG1])],[fool_formula_definition]) ).
tff(f5,definition,
( f2(bG1)
<=> ( $true = bG2 ) ),
introduced(definition,[new_symbols(definition,[bG2])],[fool_formula_definition]) ).
tff(f6,definition,
( f2(bG2)
<=> ( $true = bG3 ) ),
introduced(definition,[new_symbols(definition,[bG3])],[fool_formula_definition]) ).
tff(f7,definition,
( f2(bG3)
<=> ( $true = bG4 ) ),
introduced(definition,[new_symbols(definition,[bG4])],[fool_formula_definition]) ).
tff(f8,definition,
( f1(bG4)
<=> ( $true = bG5 ) ),
introduced(definition,[new_symbols(definition,[bG5])],[fool_formula_definition]) ).
tff(f9,definition,
( f0(bG5)
<=> ( $true = bG6 ) ),
introduced(definition,[new_symbols(definition,[bG6])],[fool_formula_definition]) ).
tff(f10,definition,
( f0(bG6)
<=> ( $true = bG7 ) ),
introduced(definition,[new_symbols(definition,[bG7])],[fool_formula_definition]) ).
tff(f11,definition,
( x
<=> ( $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,
( f3(bG9)
<=> ( $true = bG10 ) ),
introduced(definition,[new_symbols(definition,[bG10])],[fool_formula_definition]) ).
tff(f14,definition,
( f3(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,
( f1(bG13)
<=> ( $true = bG14 ) ),
introduced(definition,[new_symbols(definition,[bG14])],[fool_formula_definition]) ).
tff(f18,definition,
( f1(bG14)
<=> ( $true = bG15 ) ),
introduced(definition,[new_symbols(definition,[bG15])],[fool_formula_definition]) ).
tff(f19,plain,
~ ( f0(bG7)
<=> f0(bG15) ),
inference(fool_elimination,[],[f2,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7,f6,f5,f4,f3]) ).
tff(f20,plain,
( f0(bG7)
<~> f0(bG15) ),
inference(ennf_transformation,[],[f19]) ).
tff(f21,plain,
( ( f1(bG14)
| ( $true != bG15 ) )
& ( ( $true = bG15 )
| ~ f1(bG14) ) ),
inference(nnf_transformation,[],[f18]) ).
tff(f22,plain,
( ( f1(bG13)
| ( $true != bG14 ) )
& ( ( $true = bG14 )
| ~ f1(bG13) ) ),
inference(nnf_transformation,[],[f17]) ).
tff(f23,plain,
( ( f1(bG12)
| ( $true != bG13 ) )
& ( ( $true = bG13 )
| ~ f1(bG12) ) ),
inference(nnf_transformation,[],[f16]) ).
tff(f24,plain,
( ( f2(bG11)
| ( $true != bG12 ) )
& ( ( $true = bG12 )
| ~ f2(bG11) ) ),
inference(nnf_transformation,[],[f15]) ).
tff(f25,plain,
( ( f3(bG10)
| ( $true != bG11 ) )
& ( ( $true = bG11 )
| ~ f3(bG10) ) ),
inference(nnf_transformation,[],[f14]) ).
tff(f26,plain,
( ( f3(bG9)
| ( $true != bG10 ) )
& ( ( $true = bG10 )
| ~ f3(bG9) ) ),
inference(nnf_transformation,[],[f13]) ).
tff(f27,plain,
( ( f3(bG8)
| ( $true != bG9 ) )
& ( ( $true = bG9 )
| ~ f3(bG8) ) ),
inference(nnf_transformation,[],[f12]) ).
tff(f28,plain,
( ( x
| ( $true != bG8 ) )
& ( ( $true = bG8 )
| ~ x ) ),
inference(nnf_transformation,[],[f11]) ).
tff(f29,plain,
( ( f0(bG6)
| ( $true != bG7 ) )
& ( ( $true = bG7 )
| ~ f0(bG6) ) ),
inference(nnf_transformation,[],[f10]) ).
tff(f30,plain,
( ( f0(bG5)
| ( $true != bG6 ) )
& ( ( $true = bG6 )
| ~ f0(bG5) ) ),
inference(nnf_transformation,[],[f9]) ).
tff(f31,plain,
( ( f1(bG4)
| ( $true != bG5 ) )
& ( ( $true = bG5 )
| ~ f1(bG4) ) ),
inference(nnf_transformation,[],[f8]) ).
tff(f32,plain,
( ( f2(bG3)
| ( $true != bG4 ) )
& ( ( $true = bG4 )
| ~ f2(bG3) ) ),
inference(nnf_transformation,[],[f7]) ).
tff(f33,plain,
( ( f2(bG2)
| ( $true != bG3 ) )
& ( ( $true = bG3 )
| ~ f2(bG2) ) ),
inference(nnf_transformation,[],[f6]) ).
tff(f34,plain,
( ( f2(bG1)
| ( $true != bG2 ) )
& ( ( $true = bG2 )
| ~ f2(bG1) ) ),
inference(nnf_transformation,[],[f5]) ).
tff(f35,plain,
( ( f3(bG0)
| ( $true != bG1 ) )
& ( ( $true = bG1 )
| ~ f3(bG0) ) ),
inference(nnf_transformation,[],[f4]) ).
tff(f36,plain,
( ( x
| ( bG0 != $true ) )
& ( ( bG0 = $true )
| ~ x ) ),
inference(nnf_transformation,[],[f3]) ).
tff(f37,plain,
( ( ~ f0(bG15)
| ~ f0(bG7) )
& ( f0(bG15)
| f0(bG7) ) ),
inference(nnf_transformation,[],[f20]) ).
tff(f38,plain,
( ( $true = bG15 )
| ~ f1(bG14) ),
inference(cnf_transformation,[],[f21]) ).
tff(f39,plain,
( f1(bG14)
| ( $true != bG15 ) ),
inference(cnf_transformation,[],[f21]) ).
tff(f40,plain,
( ( $true = bG14 )
| ~ f1(bG13) ),
inference(cnf_transformation,[],[f22]) ).
tff(f41,plain,
( f1(bG13)
| ( $true != bG14 ) ),
inference(cnf_transformation,[],[f22]) ).
tff(f42,plain,
( ( $true = bG13 )
| ~ f1(bG12) ),
inference(cnf_transformation,[],[f23]) ).
tff(f43,plain,
( f1(bG12)
| ( $true != bG13 ) ),
inference(cnf_transformation,[],[f23]) ).
tff(f44,plain,
( ( $true = bG12 )
| ~ f2(bG11) ),
inference(cnf_transformation,[],[f24]) ).
tff(f45,plain,
( f2(bG11)
| ( $true != bG12 ) ),
inference(cnf_transformation,[],[f24]) ).
tff(f46,plain,
( ( $true = bG11 )
| ~ f3(bG10) ),
inference(cnf_transformation,[],[f25]) ).
tff(f47,plain,
( f3(bG10)
| ( $true != bG11 ) ),
inference(cnf_transformation,[],[f25]) ).
tff(f48,plain,
( ( $true = bG10 )
| ~ f3(bG9) ),
inference(cnf_transformation,[],[f26]) ).
tff(f49,plain,
( f3(bG9)
| ( $true != bG10 ) ),
inference(cnf_transformation,[],[f26]) ).
tff(f50,plain,
( ( $true = bG9 )
| ~ f3(bG8) ),
inference(cnf_transformation,[],[f27]) ).
tff(f51,plain,
( f3(bG8)
| ( $true != bG9 ) ),
inference(cnf_transformation,[],[f27]) ).
tff(f52,plain,
( ( $true = bG8 )
| ~ x ),
inference(cnf_transformation,[],[f28]) ).
tff(f53,plain,
( x
| ( $true != bG8 ) ),
inference(cnf_transformation,[],[f28]) ).
tff(f54,plain,
( ( $true = bG7 )
| ~ f0(bG6) ),
inference(cnf_transformation,[],[f29]) ).
tff(f55,plain,
( f0(bG6)
| ( $true != bG7 ) ),
inference(cnf_transformation,[],[f29]) ).
tff(f56,plain,
( ( $true = bG6 )
| ~ f0(bG5) ),
inference(cnf_transformation,[],[f30]) ).
tff(f57,plain,
( f0(bG5)
| ( $true != bG6 ) ),
inference(cnf_transformation,[],[f30]) ).
tff(f58,plain,
( ( $true = bG5 )
| ~ f1(bG4) ),
inference(cnf_transformation,[],[f31]) ).
tff(f59,plain,
( f1(bG4)
| ( $true != bG5 ) ),
inference(cnf_transformation,[],[f31]) ).
tff(f60,plain,
( ( $true = bG4 )
| ~ f2(bG3) ),
inference(cnf_transformation,[],[f32]) ).
tff(f61,plain,
( f2(bG3)
| ( $true != bG4 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f62,plain,
( ( $true = bG3 )
| ~ f2(bG2) ),
inference(cnf_transformation,[],[f33]) ).
tff(f63,plain,
( f2(bG2)
| ( $true != bG3 ) ),
inference(cnf_transformation,[],[f33]) ).
tff(f64,plain,
( ( $true = bG2 )
| ~ f2(bG1) ),
inference(cnf_transformation,[],[f34]) ).
tff(f65,plain,
( f2(bG1)
| ( $true != bG2 ) ),
inference(cnf_transformation,[],[f34]) ).
tff(f66,plain,
( ( $true = bG1 )
| ~ f3(bG0) ),
inference(cnf_transformation,[],[f35]) ).
tff(f67,plain,
( f3(bG0)
| ( $true != bG1 ) ),
inference(cnf_transformation,[],[f35]) ).
tff(f68,plain,
( ( bG0 = $true )
| ~ x ),
inference(cnf_transformation,[],[f36]) ).
tff(f69,plain,
( x
| ( bG0 != $true ) ),
inference(cnf_transformation,[],[f36]) ).
tff(f70,plain,
( f0(bG15)
| f0(bG7) ),
inference(cnf_transformation,[],[f37]) ).
tff(f71,plain,
( ~ f0(bG15)
| ~ f0(bG7) ),
inference(cnf_transformation,[],[f37]) ).
tff(f73,plain,
! [X0: $o] :
( ( $false = (X0) )
| ( $true = (X0) ) ),
introduced(definition,[],[fool_exhaustiveness_axiom]) ).
tff(f75,definition,
( spl16_1
<=> f0(bG7) ),
introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition]) ).
tff(f76,plain,
( ~ f0(bG7)
| spl16_1 ),
inference(avatar_component_clause,[],[f75]) ).
tff(f77,plain,
( f0(bG7)
| ~ spl16_1 ),
inference(avatar_component_clause,[],[f75]) ).
tff(f79,definition,
( spl16_2
<=> f0(bG15) ),
introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition]) ).
tff(f80,plain,
( ~ f0(bG15)
| spl16_2 ),
inference(avatar_component_clause,[],[f79]) ).
tff(f81,plain,
( f0(bG15)
| ~ spl16_2 ),
inference(avatar_component_clause,[],[f79]) ).
tff(f82,plain,
( spl16_1
| spl16_2 ),
inference(avatar_split_clause,[],[f70,f79,f75]) ).
tff(f83,plain,
( ~ spl16_1
| ~ spl16_2 ),
inference(avatar_split_clause,[],[f71,f79,f75]) ).
tff(f85,definition,
( spl16_3
<=> x ),
introduced(definition,[new_symbols(definition,[spl16_3])],[avatar_definition]) ).
tff(f89,definition,
( spl16_4
<=> ( bG0 = $true ) ),
introduced(definition,[new_symbols(definition,[spl16_4])],[avatar_definition]) ).
tff(f91,plain,
( ( bG0 = $true )
| ~ spl16_4 ),
inference(avatar_component_clause,[],[f89]) ).
tff(f92,plain,
( ~ spl16_3
| spl16_4 ),
inference(avatar_split_clause,[],[f68,f89,f85]) ).
tff(f93,plain,
( ~ spl16_4
| spl16_3 ),
inference(avatar_split_clause,[],[f69,f85,f89]) ).
tff(f95,definition,
( spl16_5
<=> f3(bG0) ),
introduced(definition,[new_symbols(definition,[spl16_5])],[avatar_definition]) ).
tff(f96,plain,
( f3(bG0)
| ~ spl16_5 ),
inference(avatar_component_clause,[],[f95]) ).
tff(f97,plain,
( ~ f3(bG0)
| spl16_5 ),
inference(avatar_component_clause,[],[f95]) ).
tff(f99,definition,
( spl16_6
<=> ( $true = bG1 ) ),
introduced(definition,[new_symbols(definition,[spl16_6])],[avatar_definition]) ).
tff(f100,plain,
( ( $true != bG1 )
| spl16_6 ),
inference(avatar_component_clause,[],[f99]) ).
tff(f101,plain,
( ( $true = bG1 )
| ~ spl16_6 ),
inference(avatar_component_clause,[],[f99]) ).
tff(f102,plain,
( ~ spl16_5
| spl16_6 ),
inference(avatar_split_clause,[],[f66,f99,f95]) ).
tff(f103,plain,
( ~ spl16_6
| spl16_5 ),
inference(avatar_split_clause,[],[f67,f95,f99]) ).
tff(f105,definition,
( spl16_7
<=> f2(bG1) ),
introduced(definition,[new_symbols(definition,[spl16_7])],[avatar_definition]) ).
tff(f106,plain,
( f2(bG1)
| ~ spl16_7 ),
inference(avatar_component_clause,[],[f105]) ).
tff(f107,plain,
( ~ f2(bG1)
| spl16_7 ),
inference(avatar_component_clause,[],[f105]) ).
tff(f109,definition,
( spl16_8
<=> ( $true = bG2 ) ),
introduced(definition,[new_symbols(definition,[spl16_8])],[avatar_definition]) ).
tff(f110,plain,
( ( $true != bG2 )
| spl16_8 ),
inference(avatar_component_clause,[],[f109]) ).
tff(f111,plain,
( ( $true = bG2 )
| ~ spl16_8 ),
inference(avatar_component_clause,[],[f109]) ).
tff(f112,plain,
( ~ spl16_7
| spl16_8 ),
inference(avatar_split_clause,[],[f64,f109,f105]) ).
tff(f113,plain,
( ~ spl16_8
| spl16_7 ),
inference(avatar_split_clause,[],[f65,f105,f109]) ).
tff(f115,definition,
( spl16_9
<=> f2(bG2) ),
introduced(definition,[new_symbols(definition,[spl16_9])],[avatar_definition]) ).
tff(f116,plain,
( f2(bG2)
| ~ spl16_9 ),
inference(avatar_component_clause,[],[f115]) ).
tff(f117,plain,
( ~ f2(bG2)
| spl16_9 ),
inference(avatar_component_clause,[],[f115]) ).
tff(f119,definition,
( spl16_10
<=> ( $true = bG3 ) ),
introduced(definition,[new_symbols(definition,[spl16_10])],[avatar_definition]) ).
tff(f120,plain,
( ( $true != bG3 )
| spl16_10 ),
inference(avatar_component_clause,[],[f119]) ).
tff(f121,plain,
( ( $true = bG3 )
| ~ spl16_10 ),
inference(avatar_component_clause,[],[f119]) ).
tff(f122,plain,
( ~ spl16_9
| spl16_10 ),
inference(avatar_split_clause,[],[f62,f119,f115]) ).
tff(f123,plain,
( ~ spl16_10
| spl16_9 ),
inference(avatar_split_clause,[],[f63,f115,f119]) ).
tff(f125,definition,
( spl16_11
<=> f2(bG3) ),
introduced(definition,[new_symbols(definition,[spl16_11])],[avatar_definition]) ).
tff(f126,plain,
( f2(bG3)
| ~ spl16_11 ),
inference(avatar_component_clause,[],[f125]) ).
tff(f127,plain,
( ~ f2(bG3)
| spl16_11 ),
inference(avatar_component_clause,[],[f125]) ).
tff(f129,definition,
( spl16_12
<=> ( $true = bG4 ) ),
introduced(definition,[new_symbols(definition,[spl16_12])],[avatar_definition]) ).
tff(f130,plain,
( ( $true != bG4 )
| spl16_12 ),
inference(avatar_component_clause,[],[f129]) ).
tff(f131,plain,
( ( $true = bG4 )
| ~ spl16_12 ),
inference(avatar_component_clause,[],[f129]) ).
tff(f132,plain,
( ~ spl16_11
| spl16_12 ),
inference(avatar_split_clause,[],[f60,f129,f125]) ).
tff(f133,plain,
( ~ spl16_12
| spl16_11 ),
inference(avatar_split_clause,[],[f61,f125,f129]) ).
tff(f135,definition,
( spl16_13
<=> f1(bG4) ),
introduced(definition,[new_symbols(definition,[spl16_13])],[avatar_definition]) ).
tff(f136,plain,
( f1(bG4)
| ~ spl16_13 ),
inference(avatar_component_clause,[],[f135]) ).
tff(f137,plain,
( ~ f1(bG4)
| spl16_13 ),
inference(avatar_component_clause,[],[f135]) ).
tff(f139,definition,
( spl16_14
<=> ( $true = bG5 ) ),
introduced(definition,[new_symbols(definition,[spl16_14])],[avatar_definition]) ).
tff(f141,plain,
( ( $true = bG5 )
| ~ spl16_14 ),
inference(avatar_component_clause,[],[f139]) ).
tff(f142,plain,
( ~ spl16_13
| spl16_14 ),
inference(avatar_split_clause,[],[f58,f139,f135]) ).
tff(f143,plain,
( ~ spl16_14
| spl16_13 ),
inference(avatar_split_clause,[],[f59,f135,f139]) ).
tff(f145,definition,
( spl16_15
<=> f0(bG5) ),
introduced(definition,[new_symbols(definition,[spl16_15])],[avatar_definition]) ).
tff(f146,plain,
( f0(bG5)
| ~ spl16_15 ),
inference(avatar_component_clause,[],[f145]) ).
tff(f147,plain,
( ~ f0(bG5)
| spl16_15 ),
inference(avatar_component_clause,[],[f145]) ).
tff(f149,definition,
( spl16_16
<=> ( $true = bG6 ) ),
introduced(definition,[new_symbols(definition,[spl16_16])],[avatar_definition]) ).
tff(f150,plain,
( ( $true != bG6 )
| spl16_16 ),
inference(avatar_component_clause,[],[f149]) ).
tff(f151,plain,
( ( $true = bG6 )
| ~ spl16_16 ),
inference(avatar_component_clause,[],[f149]) ).
tff(f152,plain,
( ~ spl16_15
| spl16_16 ),
inference(avatar_split_clause,[],[f56,f149,f145]) ).
tff(f153,plain,
( ~ spl16_16
| spl16_15 ),
inference(avatar_split_clause,[],[f57,f145,f149]) ).
tff(f155,definition,
( spl16_17
<=> f0(bG6) ),
introduced(definition,[new_symbols(definition,[spl16_17])],[avatar_definition]) ).
tff(f156,plain,
( f0(bG6)
| ~ spl16_17 ),
inference(avatar_component_clause,[],[f155]) ).
tff(f157,plain,
( ~ f0(bG6)
| spl16_17 ),
inference(avatar_component_clause,[],[f155]) ).
tff(f159,definition,
( spl16_18
<=> ( $true = bG7 ) ),
introduced(definition,[new_symbols(definition,[spl16_18])],[avatar_definition]) ).
tff(f161,plain,
( ( $true = bG7 )
| ~ spl16_18 ),
inference(avatar_component_clause,[],[f159]) ).
tff(f162,plain,
( ~ spl16_17
| spl16_18 ),
inference(avatar_split_clause,[],[f54,f159,f155]) ).
tff(f163,plain,
( ~ spl16_18
| spl16_17 ),
inference(avatar_split_clause,[],[f55,f155,f159]) ).
tff(f165,definition,
( spl16_19
<=> ( $true = bG8 ) ),
introduced(definition,[new_symbols(definition,[spl16_19])],[avatar_definition]) ).
tff(f167,plain,
( ( $true = bG8 )
| ~ spl16_19 ),
inference(avatar_component_clause,[],[f165]) ).
tff(f168,plain,
( ~ spl16_3
| spl16_19 ),
inference(avatar_split_clause,[],[f52,f165,f85]) ).
tff(f169,plain,
( ~ spl16_19
| spl16_3 ),
inference(avatar_split_clause,[],[f53,f85,f165]) ).
tff(f171,definition,
( spl16_20
<=> f3(bG8) ),
introduced(definition,[new_symbols(definition,[spl16_20])],[avatar_definition]) ).
tff(f172,plain,
( f3(bG8)
| ~ spl16_20 ),
inference(avatar_component_clause,[],[f171]) ).
tff(f173,plain,
( ~ f3(bG8)
| spl16_20 ),
inference(avatar_component_clause,[],[f171]) ).
tff(f175,definition,
( spl16_21
<=> ( $true = bG9 ) ),
introduced(definition,[new_symbols(definition,[spl16_21])],[avatar_definition]) ).
tff(f177,plain,
( ( $true = bG9 )
| ~ spl16_21 ),
inference(avatar_component_clause,[],[f175]) ).
tff(f178,plain,
( ~ spl16_20
| spl16_21 ),
inference(avatar_split_clause,[],[f50,f175,f171]) ).
tff(f179,plain,
( ~ spl16_21
| spl16_20 ),
inference(avatar_split_clause,[],[f51,f171,f175]) ).
tff(f181,definition,
( spl16_22
<=> f3(bG9) ),
introduced(definition,[new_symbols(definition,[spl16_22])],[avatar_definition]) ).
tff(f182,plain,
( f3(bG9)
| ~ spl16_22 ),
inference(avatar_component_clause,[],[f181]) ).
tff(f183,plain,
( ~ f3(bG9)
| spl16_22 ),
inference(avatar_component_clause,[],[f181]) ).
tff(f185,definition,
( spl16_23
<=> ( $true = bG10 ) ),
introduced(definition,[new_symbols(definition,[spl16_23])],[avatar_definition]) ).
tff(f186,plain,
( ( $true != bG10 )
| spl16_23 ),
inference(avatar_component_clause,[],[f185]) ).
tff(f187,plain,
( ( $true = bG10 )
| ~ spl16_23 ),
inference(avatar_component_clause,[],[f185]) ).
tff(f188,plain,
( ~ spl16_22
| spl16_23 ),
inference(avatar_split_clause,[],[f48,f185,f181]) ).
tff(f189,plain,
( ~ spl16_23
| spl16_22 ),
inference(avatar_split_clause,[],[f49,f181,f185]) ).
tff(f191,definition,
( spl16_24
<=> f3(bG10) ),
introduced(definition,[new_symbols(definition,[spl16_24])],[avatar_definition]) ).
tff(f192,plain,
( f3(bG10)
| ~ spl16_24 ),
inference(avatar_component_clause,[],[f191]) ).
tff(f193,plain,
( ~ f3(bG10)
| spl16_24 ),
inference(avatar_component_clause,[],[f191]) ).
tff(f195,definition,
( spl16_25
<=> ( $true = bG11 ) ),
introduced(definition,[new_symbols(definition,[spl16_25])],[avatar_definition]) ).
tff(f196,plain,
( ( $true != bG11 )
| spl16_25 ),
inference(avatar_component_clause,[],[f195]) ).
tff(f197,plain,
( ( $true = bG11 )
| ~ spl16_25 ),
inference(avatar_component_clause,[],[f195]) ).
tff(f198,plain,
( ~ spl16_24
| spl16_25 ),
inference(avatar_split_clause,[],[f46,f195,f191]) ).
tff(f199,plain,
( ~ spl16_25
| spl16_24 ),
inference(avatar_split_clause,[],[f47,f191,f195]) ).
tff(f201,definition,
( spl16_26
<=> f2(bG11) ),
introduced(definition,[new_symbols(definition,[spl16_26])],[avatar_definition]) ).
tff(f202,plain,
( f2(bG11)
| ~ spl16_26 ),
inference(avatar_component_clause,[],[f201]) ).
tff(f203,plain,
( ~ f2(bG11)
| spl16_26 ),
inference(avatar_component_clause,[],[f201]) ).
tff(f205,definition,
( spl16_27
<=> ( $true = bG12 ) ),
introduced(definition,[new_symbols(definition,[spl16_27])],[avatar_definition]) ).
tff(f207,plain,
( ( $true = bG12 )
| ~ spl16_27 ),
inference(avatar_component_clause,[],[f205]) ).
tff(f208,plain,
( ~ spl16_26
| spl16_27 ),
inference(avatar_split_clause,[],[f44,f205,f201]) ).
tff(f209,plain,
( ~ spl16_27
| spl16_26 ),
inference(avatar_split_clause,[],[f45,f201,f205]) ).
tff(f211,definition,
( spl16_28
<=> f1(bG12) ),
introduced(definition,[new_symbols(definition,[spl16_28])],[avatar_definition]) ).
tff(f212,plain,
( f1(bG12)
| ~ spl16_28 ),
inference(avatar_component_clause,[],[f211]) ).
tff(f213,plain,
( ~ f1(bG12)
| spl16_28 ),
inference(avatar_component_clause,[],[f211]) ).
tff(f215,definition,
( spl16_29
<=> ( $true = bG13 ) ),
introduced(definition,[new_symbols(definition,[spl16_29])],[avatar_definition]) ).
tff(f217,plain,
( ( $true = bG13 )
| ~ spl16_29 ),
inference(avatar_component_clause,[],[f215]) ).
tff(f218,plain,
( ~ spl16_28
| spl16_29 ),
inference(avatar_split_clause,[],[f42,f215,f211]) ).
tff(f219,plain,
( ~ spl16_29
| spl16_28 ),
inference(avatar_split_clause,[],[f43,f211,f215]) ).
tff(f221,definition,
( spl16_30
<=> f1(bG13) ),
introduced(definition,[new_symbols(definition,[spl16_30])],[avatar_definition]) ).
tff(f222,plain,
( f1(bG13)
| ~ spl16_30 ),
inference(avatar_component_clause,[],[f221]) ).
tff(f223,plain,
( ~ f1(bG13)
| spl16_30 ),
inference(avatar_component_clause,[],[f221]) ).
tff(f225,definition,
( spl16_31
<=> ( $true = bG14 ) ),
introduced(definition,[new_symbols(definition,[spl16_31])],[avatar_definition]) ).
tff(f226,plain,
( ( $true != bG14 )
| spl16_31 ),
inference(avatar_component_clause,[],[f225]) ).
tff(f227,plain,
( ( $true = bG14 )
| ~ spl16_31 ),
inference(avatar_component_clause,[],[f225]) ).
tff(f228,plain,
( ~ spl16_30
| spl16_31 ),
inference(avatar_split_clause,[],[f40,f225,f221]) ).
tff(f229,plain,
( ~ spl16_31
| spl16_30 ),
inference(avatar_split_clause,[],[f41,f221,f225]) ).
tff(f231,definition,
( spl16_32
<=> f1(bG14) ),
introduced(definition,[new_symbols(definition,[spl16_32])],[avatar_definition]) ).
tff(f232,plain,
( f1(bG14)
| ~ spl16_32 ),
inference(avatar_component_clause,[],[f231]) ).
tff(f233,plain,
( ~ f1(bG14)
| spl16_32 ),
inference(avatar_component_clause,[],[f231]) ).
tff(f235,definition,
( spl16_33
<=> ( $true = bG15 ) ),
introduced(definition,[new_symbols(definition,[spl16_33])],[avatar_definition]) ).
tff(f236,plain,
( ( $true != bG15 )
| spl16_33 ),
inference(avatar_component_clause,[],[f235]) ).
tff(f237,plain,
( ( $true = bG15 )
| ~ spl16_33 ),
inference(avatar_component_clause,[],[f235]) ).
tff(f238,plain,
( ~ spl16_32
| spl16_33 ),
inference(avatar_split_clause,[],[f38,f235,f231]) ).
tff(f239,plain,
( ~ spl16_33
| spl16_32 ),
inference(avatar_split_clause,[],[f39,f231,f235]) ).
tff(f244,plain,
( ~ f2($false)
| ( $true = bG1 )
| spl16_7 ),
inference(superposition,[],[f107,f73]) ).
tff(f246,plain,
( ~ f2($false)
| ( $true = bG2 )
| spl16_9 ),
inference(superposition,[],[f117,f73]) ).
tff(f250,plain,
( ~ f1($false)
| ( $true = bG4 )
| spl16_13 ),
inference(superposition,[],[f137,f73]) ).
tff(f254,plain,
( ~ f0($false)
| ( $true = bG6 )
| spl16_17 ),
inference(superposition,[],[f157,f73]) ).
tff(f256,plain,
( ~ f0($false)
| ( $true = bG7 )
| spl16_1 ),
inference(superposition,[],[f76,f73]) ).
tff(f262,plain,
( ~ f3($false)
| ( $true = bG10 )
| spl16_24 ),
inference(superposition,[],[f193,f73]) ).
tff(f264,plain,
( ~ f2($false)
| ( $true = bG11 )
| spl16_26 ),
inference(superposition,[],[f203,f73]) ).
tff(f270,plain,
( ~ f1($false)
| ( $true = bG14 )
| spl16_32 ),
inference(superposition,[],[f233,f73]) ).
tff(f272,plain,
( f0($false)
| ( $true = bG15 )
| ~ spl16_2 ),
inference(superposition,[],[f81,f73]) ).
tff(f274,plain,
( f0($false)
| ~ spl16_2
| spl16_33 ),
inference(forward_subsumption_resolution,[],[f272,f236]) ).
tff(f275,plain,
( ~ f1($false)
| spl16_31
| spl16_32 ),
inference(forward_subsumption_resolution,[],[f270,f226]) ).
tff(f278,plain,
( ~ f2($false)
| spl16_25
| spl16_26 ),
inference(forward_subsumption_resolution,[],[f264,f196]) ).
tff(f279,plain,
( ~ f3($false)
| spl16_23
| spl16_24 ),
inference(forward_subsumption_resolution,[],[f262,f186]) ).
tff(f283,plain,
( ~ f0($false)
| spl16_16
| spl16_17 ),
inference(forward_subsumption_resolution,[],[f254,f150]) ).
tff(f285,plain,
( ~ f1($false)
| spl16_12
| spl16_13 ),
inference(forward_subsumption_resolution,[],[f250,f130]) ).
tff(f287,plain,
( ~ f2($false)
| spl16_8
| spl16_9 ),
inference(forward_subsumption_resolution,[],[f246,f110]) ).
tff(f288,plain,
( ~ f2($false)
| spl16_6
| spl16_7 ),
inference(forward_subsumption_resolution,[],[f244,f100]) ).
tff(f290,plain,
( ! [X0: $o] :
( f0((X0))
| ( $true = (X0) ) )
| ~ spl16_2
| spl16_33 ),
inference(superposition,[],[f274,f73]) ).
tff(f293,plain,
( ( $true = bG7 )
| spl16_1
| ~ spl16_2
| spl16_33 ),
inference(forward_subsumption_resolution,[],[f256,f274]) ).
tff(f294,plain,
( spl16_18
| spl16_1
| ~ spl16_2
| spl16_33 ),
inference(avatar_split_clause,[],[f293,f235,f79,f75,f159]) ).
tff(f295,plain,
( f0($false)
| ( $true = bG6 )
| ~ spl16_17 ),
inference(superposition,[],[f156,f73]) ).
tff(f297,plain,
( ( $true = bG5 )
| ~ spl16_2
| spl16_15
| spl16_33 ),
inference(resolution,[],[f290,f147]) ).
tff(f301,plain,
( spl16_14
| ~ spl16_2
| spl16_15
| spl16_33 ),
inference(avatar_split_clause,[],[f297,f235,f145,f79,f139]) ).
tff(f303,plain,
( ~ f0($true)
| spl16_1
| ~ spl16_18 ),
inference(superposition,[],[f76,f161]) ).
tff(f306,plain,
( f1($false)
| ( $true = bG4 )
| ~ spl16_13 ),
inference(superposition,[],[f136,f73]) ).
tff(f307,plain,
( f1($false)
| spl16_12
| ~ spl16_13 ),
inference(forward_subsumption_resolution,[],[f306,f130]) ).
tff(f310,plain,
( ~ f0($true)
| ~ spl16_14
| spl16_15 ),
inference(superposition,[],[f147,f141]) ).
tff(f314,plain,
( $false
| spl16_12
| ~ spl16_13
| spl16_31
| spl16_32 ),
inference(forward_subsumption_resolution,[],[f307,f275]) ).
tff(f315,plain,
( spl16_12
| ~ spl16_13
| spl16_31
| spl16_32 ),
inference(avatar_contradiction_clause,[],[f314]) ).
tff(f317,definition,
( spl16_34
<=> f1($false) ),
introduced(definition,[new_symbols(definition,[spl16_34])],[avatar_definition]) ).
tff(f324,plain,
( f2($false)
| ( $true = bG3 )
| ~ spl16_11 ),
inference(superposition,[],[f126,f73]) ).
tff(f325,plain,
( ( $true = bG3 )
| ~ spl16_11
| spl16_25
| spl16_26 ),
inference(forward_subsumption_resolution,[],[f324,f278]) ).
tff(f326,plain,
( $false
| spl16_10
| ~ spl16_11
| spl16_25
| spl16_26 ),
inference(forward_subsumption_resolution,[],[f325,f120]) ).
tff(f327,plain,
( spl16_10
| ~ spl16_11
| spl16_25
| spl16_26 ),
inference(avatar_contradiction_clause,[],[f326]) ).
tff(f329,definition,
( spl16_35
<=> f2($false) ),
introduced(definition,[new_symbols(definition,[spl16_35])],[avatar_definition]) ).
tff(f333,plain,
( ~ spl16_35
| spl16_8
| spl16_9 ),
inference(avatar_split_clause,[],[f287,f115,f109,f329]) ).
tff(f334,plain,
( ~ spl16_35
| spl16_6
| spl16_7 ),
inference(avatar_split_clause,[],[f288,f105,f99,f329]) ).
tff(f337,plain,
( spl16_10
| spl16_35
| ~ spl16_11 ),
inference(avatar_split_clause,[],[f324,f125,f329,f119]) ).
tff(f346,plain,
( f3($false)
| ( bG0 = $true )
| ~ spl16_5 ),
inference(superposition,[],[f96,f73]) ).
tff(f358,plain,
( f2($true)
| ~ spl16_6
| ~ spl16_7 ),
inference(superposition,[],[f106,f101]) ).
tff(f368,plain,
( f1($true)
| ~ spl16_12
| ~ spl16_13 ),
inference(superposition,[],[f136,f131]) ).
tff(f371,plain,
( f2($true)
| ~ spl16_25
| ~ spl16_26 ),
inference(superposition,[],[f202,f197]) ).
tff(f375,plain,
( ~ f1($true)
| ~ spl16_27
| spl16_28 ),
inference(superposition,[],[f213,f207]) ).
tff(f377,plain,
( $false
| ~ spl16_12
| ~ spl16_13
| ~ spl16_27
| spl16_28 ),
inference(forward_subsumption_resolution,[],[f375,f368]) ).
tff(f378,plain,
( ~ spl16_12
| ~ spl16_13
| ~ spl16_27
| spl16_28 ),
inference(avatar_contradiction_clause,[],[f377]) ).
tff(f379,plain,
( ~ f2($true)
| ~ spl16_10
| spl16_11 ),
inference(forward_demodulation,[],[f127,f121]) ).
tff(f382,plain,
( f2($true)
| ~ spl16_10
| ~ spl16_11 ),
inference(forward_demodulation,[],[f126,f121]) ).
tff(f385,plain,
( f0($true)
| ~ spl16_16
| ~ spl16_17 ),
inference(superposition,[],[f156,f151]) ).
tff(f387,plain,
( $false
| spl16_1
| ~ spl16_16
| ~ spl16_17
| ~ spl16_18 ),
inference(forward_subsumption_resolution,[],[f385,f303]) ).
tff(f388,plain,
( spl16_1
| ~ spl16_16
| ~ spl16_17
| ~ spl16_18 ),
inference(avatar_contradiction_clause,[],[f387]) ).
tff(f389,plain,
( ~ f2($true)
| ~ spl16_25
| spl16_26 ),
inference(forward_demodulation,[],[f203,f197]) ).
tff(f390,plain,
( $false
| ~ spl16_6
| ~ spl16_7
| ~ spl16_25
| spl16_26 ),
inference(forward_subsumption_resolution,[],[f389,f358]) ).
tff(f391,plain,
( ~ spl16_6
| ~ spl16_7
| ~ spl16_25
| spl16_26 ),
inference(avatar_contradiction_clause,[],[f390]) ).
tff(f406,definition,
( spl16_36
<=> f3($false) ),
introduced(definition,[new_symbols(definition,[spl16_36])],[avatar_definition]) ).
tff(f407,plain,
( f3($false)
| ~ spl16_36 ),
inference(avatar_component_clause,[],[f406]) ).
tff(f410,plain,
( ~ spl16_36
| spl16_23
| spl16_24 ),
inference(avatar_split_clause,[],[f279,f191,f185,f406]) ).
tff(f413,plain,
( spl16_4
| spl16_36
| ~ spl16_5 ),
inference(avatar_split_clause,[],[f346,f95,f406,f89]) ).
tff(f414,plain,
( f3($false)
| ( $true = bG8 )
| ~ spl16_20 ),
inference(superposition,[],[f172,f73]) ).
tff(f415,plain,
( spl16_19
| spl16_36
| ~ spl16_20 ),
inference(avatar_split_clause,[],[f414,f171,f406,f165]) ).
tff(f417,plain,
( f3($true)
| ~ spl16_4
| ~ spl16_5 ),
inference(superposition,[],[f96,f91]) ).
tff(f427,plain,
( ~ f3($true)
| ~ spl16_21
| spl16_22 ),
inference(superposition,[],[f183,f177]) ).
tff(f429,plain,
( $false
| ~ spl16_4
| ~ spl16_5
| ~ spl16_21
| spl16_22 ),
inference(forward_subsumption_resolution,[],[f427,f417]) ).
tff(f430,plain,
( ~ spl16_4
| ~ spl16_5
| ~ spl16_21
| spl16_22 ),
inference(avatar_contradiction_clause,[],[f429]) ).
tff(f431,plain,
( ~ f3($true)
| ~ spl16_19
| spl16_20 ),
inference(forward_demodulation,[],[f173,f167]) ).
tff(f432,plain,
( $false
| ~ spl16_4
| ~ spl16_5
| ~ spl16_19
| spl16_20 ),
inference(forward_subsumption_resolution,[],[f431,f417]) ).
tff(f433,plain,
( ~ spl16_4
| ~ spl16_5
| ~ spl16_19
| spl16_20 ),
inference(avatar_contradiction_clause,[],[f432]) ).
tff(f434,plain,
( ~ f3($true)
| ~ spl16_4
| spl16_5 ),
inference(forward_demodulation,[],[f97,f91]) ).
tff(f438,plain,
( f3($false)
| ( $true = bG9 )
| ~ spl16_22 ),
inference(superposition,[],[f182,f73]) ).
tff(f441,plain,
( spl16_21
| spl16_36
| ~ spl16_22 ),
inference(avatar_split_clause,[],[f438,f181,f406,f175]) ).
tff(f442,plain,
( f3($false)
| ( $true = bG10 )
| ~ spl16_24 ),
inference(superposition,[],[f192,f73]) ).
tff(f443,plain,
( spl16_23
| spl16_36
| ~ spl16_24 ),
inference(avatar_split_clause,[],[f442,f191,f406,f185]) ).
tff(f444,plain,
( $false
| ~ spl16_10
| ~ spl16_11
| ~ spl16_25
| spl16_26 ),
inference(forward_subsumption_resolution,[],[f389,f382]) ).
tff(f445,plain,
( ~ spl16_10
| ~ spl16_11
| ~ spl16_25
| spl16_26 ),
inference(avatar_contradiction_clause,[],[f444]) ).
tff(f452,plain,
( f3($true)
| ~ spl16_23
| ~ spl16_24 ),
inference(superposition,[],[f192,f187]) ).
tff(f454,plain,
( $false
| ~ spl16_19
| spl16_20
| ~ spl16_23
| ~ spl16_24 ),
inference(forward_subsumption_resolution,[],[f452,f431]) ).
tff(f455,plain,
( ~ spl16_19
| spl16_20
| ~ spl16_23
| ~ spl16_24 ),
inference(avatar_contradiction_clause,[],[f454]) ).
tff(f458,plain,
( ~ f3($true)
| ~ spl16_23
| spl16_24 ),
inference(forward_demodulation,[],[f193,f187]) ).
tff(f459,plain,
( ~ f3($false)
| ( bG0 = $true )
| spl16_5 ),
inference(superposition,[],[f97,f73]) ).
tff(f460,plain,
( spl16_4
| ~ spl16_36
| spl16_5 ),
inference(avatar_split_clause,[],[f459,f95,f406,f89]) ).
tff(f461,plain,
( ~ f3($false)
| ( $true = bG8 )
| spl16_20 ),
inference(superposition,[],[f173,f73]) ).
tff(f462,plain,
( spl16_19
| ~ spl16_36
| spl16_20 ),
inference(avatar_split_clause,[],[f461,f171,f406,f165]) ).
tff(f472,plain,
( f1($true)
| ~ spl16_27
| ~ spl16_28 ),
inference(superposition,[],[f212,f207]) ).
tff(f475,plain,
( f1($true)
| ~ spl16_29
| ~ spl16_30 ),
inference(superposition,[],[f222,f217]) ).
tff(f478,plain,
( ~ f1($true)
| ~ spl16_31
| spl16_32 ),
inference(superposition,[],[f233,f227]) ).
tff(f480,plain,
( $false
| ~ spl16_12
| ~ spl16_13
| ~ spl16_31
| spl16_32 ),
inference(forward_subsumption_resolution,[],[f478,f368]) ).
tff(f481,plain,
( ~ spl16_12
| ~ spl16_13
| ~ spl16_31
| spl16_32 ),
inference(avatar_contradiction_clause,[],[f480]) ).
tff(f482,plain,
( f1($true)
| ~ spl16_31
| ~ spl16_32 ),
inference(forward_demodulation,[],[f232,f227]) ).
tff(f484,definition,
( spl16_37
<=> f0($false) ),
introduced(definition,[new_symbols(definition,[spl16_37])],[avatar_definition]) ).
tff(f488,plain,
( f0($false)
| spl16_16
| ~ spl16_17 ),
inference(forward_subsumption_resolution,[],[f295,f150]) ).
tff(f489,plain,
( spl16_37
| spl16_16
| ~ spl16_17 ),
inference(avatar_split_clause,[],[f488,f155,f149,f484]) ).
tff(f491,plain,
( f0($true)
| ~ spl16_2
| ~ spl16_33 ),
inference(superposition,[],[f81,f237]) ).
tff(f495,plain,
( ~ spl16_37
| spl16_16
| spl16_17 ),
inference(avatar_split_clause,[],[f283,f155,f149,f484]) ).
tff(f504,plain,
( $false
| ~ spl16_2
| ~ spl16_14
| spl16_15
| ~ spl16_33 ),
inference(forward_subsumption_resolution,[],[f310,f491]) ).
tff(f505,plain,
( ~ spl16_2
| ~ spl16_14
| spl16_15
| ~ spl16_33 ),
inference(avatar_contradiction_clause,[],[f504]) ).
tff(f506,plain,
( f0($true)
| ~ spl16_14
| ~ spl16_15 ),
inference(forward_demodulation,[],[f146,f141]) ).
tff(f508,plain,
( ~ f0($true)
| ~ spl16_16
| spl16_17 ),
inference(superposition,[],[f157,f151]) ).
tff(f510,plain,
( $false
| ~ spl16_2
| ~ spl16_16
| spl16_17
| ~ spl16_33 ),
inference(forward_subsumption_resolution,[],[f508,f491]) ).
tff(f511,plain,
( ~ spl16_2
| ~ spl16_16
| spl16_17
| ~ spl16_33 ),
inference(avatar_contradiction_clause,[],[f510]) ).
tff(f512,plain,
( ~ f0($true)
| spl16_2
| ~ spl16_33 ),
inference(forward_demodulation,[],[f80,f237]) ).
tff(f522,plain,
( $false
| spl16_2
| ~ spl16_14
| ~ spl16_15
| ~ spl16_33 ),
inference(forward_subsumption_resolution,[],[f506,f512]) ).
tff(f523,plain,
( spl16_2
| ~ spl16_14
| ~ spl16_15
| ~ spl16_33 ),
inference(avatar_contradiction_clause,[],[f522]) ).
tff(f531,plain,
( f0($true)
| ~ spl16_1
| ~ spl16_18 ),
inference(superposition,[],[f77,f161]) ).
tff(f533,plain,
( $false
| ~ spl16_1
| spl16_2
| ~ spl16_18
| ~ spl16_33 ),
inference(forward_subsumption_resolution,[],[f531,f512]) ).
tff(f534,plain,
( ~ spl16_1
| spl16_2
| ~ spl16_18
| ~ spl16_33 ),
inference(avatar_contradiction_clause,[],[f533]) ).
tff(f535,plain,
( ~ f1($true)
| ~ spl16_29
| spl16_30 ),
inference(forward_demodulation,[],[f223,f217]) ).
tff(f537,plain,
( $false
| ~ spl16_12
| ~ spl16_13
| ~ spl16_29
| spl16_30 ),
inference(forward_subsumption_resolution,[],[f535,f368]) ).
tff(f538,plain,
( ~ spl16_12
| ~ spl16_13
| ~ spl16_29
| spl16_30 ),
inference(avatar_contradiction_clause,[],[f537]) ).
tff(f539,plain,
( ~ f1($true)
| ~ spl16_12
| spl16_13 ),
inference(forward_demodulation,[],[f137,f131]) ).
tff(f542,plain,
( ~ f2($true)
| ~ spl16_8
| spl16_9 ),
inference(forward_demodulation,[],[f117,f111]) ).
tff(f544,plain,
( f3($true)
| ~ spl16_19
| ~ spl16_20 ),
inference(forward_demodulation,[],[f172,f167]) ).
tff(f561,plain,
( ~ f3($false)
| ( $true = bG9 )
| spl16_22 ),
inference(superposition,[],[f183,f73]) ).
tff(f562,plain,
( ( $true = bG9 )
| spl16_22
| ~ spl16_36 ),
inference(forward_subsumption_resolution,[],[f561,f407]) ).
tff(f563,plain,
( spl16_21
| spl16_22
| ~ spl16_36 ),
inference(avatar_split_clause,[],[f562,f406,f181,f175]) ).
tff(f572,plain,
( $false
| ~ spl16_4
| spl16_5
| ~ spl16_19
| ~ spl16_20 ),
inference(forward_subsumption_resolution,[],[f544,f434]) ).
tff(f573,plain,
( ~ spl16_4
| spl16_5
| ~ spl16_19
| ~ spl16_20 ),
inference(avatar_contradiction_clause,[],[f572]) ).
tff(f597,plain,
( $false
| ~ spl16_6
| ~ spl16_7
| ~ spl16_8
| spl16_9 ),
inference(forward_subsumption_resolution,[],[f358,f542]) ).
tff(f598,plain,
( ~ spl16_6
| ~ spl16_7
| ~ spl16_8
| spl16_9 ),
inference(avatar_contradiction_clause,[],[f597]) ).
tff(f599,plain,
( f2($true)
| ~ spl16_8
| ~ spl16_9 ),
inference(forward_demodulation,[],[f116,f111]) ).
tff(f611,plain,
( $false
| ~ spl16_27
| ~ spl16_28
| ~ spl16_29
| spl16_30 ),
inference(forward_subsumption_resolution,[],[f472,f535]) ).
tff(f612,plain,
( ~ spl16_27
| ~ spl16_28
| ~ spl16_29
| spl16_30 ),
inference(avatar_contradiction_clause,[],[f611]) ).
tff(f615,plain,
( $false
| ~ spl16_12
| spl16_13
| ~ spl16_31
| ~ spl16_32 ),
inference(forward_subsumption_resolution,[],[f539,f482]) ).
tff(f616,plain,
( ~ spl16_12
| spl16_13
| ~ spl16_31
| ~ spl16_32 ),
inference(avatar_contradiction_clause,[],[f615]) ).
tff(f618,plain,
( f0($false)
| ( $true = bG7 )
| ~ spl16_1 ),
inference(superposition,[],[f77,f73]) ).
tff(f620,plain,
( ~ f0($false)
| ( $true = bG15 )
| spl16_2 ),
inference(superposition,[],[f80,f73]) ).
tff(f623,plain,
( f0($false)
| ( $true = bG5 )
| ~ spl16_15 ),
inference(superposition,[],[f146,f73]) ).
tff(f630,plain,
( f3($true)
| ~ spl16_21
| ~ spl16_22 ),
inference(forward_demodulation,[],[f182,f177]) ).
tff(f642,plain,
( ~ f2($false)
| ( $true = bG11 )
| spl16_26 ),
inference(superposition,[],[f203,f73]) ).
tff(f643,plain,
( spl16_25
| ~ spl16_35
| spl16_26 ),
inference(avatar_split_clause,[],[f642,f201,f329,f195]) ).
tff(f647,plain,
( ~ f1($false)
| ( $true = bG12 )
| spl16_28 ),
inference(superposition,[],[f213,f73]) ).
tff(f648,plain,
( spl16_27
| ~ spl16_34
| spl16_28 ),
inference(avatar_split_clause,[],[f647,f211,f317,f205]) ).
tff(f650,plain,
( ~ f1($false)
| ( $true = bG13 )
| spl16_30 ),
inference(superposition,[],[f223,f73]) ).
tff(f651,plain,
( spl16_29
| ~ spl16_34
| spl16_30 ),
inference(avatar_split_clause,[],[f650,f221,f317,f215]) ).
tff(f652,plain,
( $false
| ~ spl16_21
| ~ spl16_22
| ~ spl16_23
| spl16_24 ),
inference(forward_subsumption_resolution,[],[f630,f458]) ).
tff(f653,plain,
( ~ spl16_21
| ~ spl16_22
| ~ spl16_23
| spl16_24 ),
inference(avatar_contradiction_clause,[],[f652]) ).
tff(f654,plain,
( ~ f2($true)
| ~ spl16_6
| spl16_7 ),
inference(forward_demodulation,[],[f107,f101]) ).
tff(f658,plain,
( f1($false)
| ( $true = bG4 )
| ~ spl16_13 ),
inference(superposition,[],[f136,f73]) ).
tff(f659,plain,
( spl16_12
| spl16_34
| ~ spl16_13 ),
inference(avatar_split_clause,[],[f658,f135,f317,f129]) ).
tff(f661,plain,
( f1($false)
| ( $true = bG12 )
| ~ spl16_28 ),
inference(superposition,[],[f212,f73]) ).
tff(f662,plain,
( spl16_27
| spl16_34
| ~ spl16_28 ),
inference(avatar_split_clause,[],[f661,f211,f317,f205]) ).
tff(f663,plain,
( f1($false)
| ( $true = bG13 )
| ~ spl16_30 ),
inference(superposition,[],[f222,f73]) ).
tff(f664,plain,
( spl16_29
| spl16_34
| ~ spl16_30 ),
inference(avatar_split_clause,[],[f663,f221,f317,f215]) ).
tff(f667,plain,
( $false
| ~ spl16_29
| ~ spl16_30
| ~ spl16_31
| spl16_32 ),
inference(forward_subsumption_resolution,[],[f478,f475]) ).
tff(f668,plain,
( ~ spl16_29
| ~ spl16_30
| ~ spl16_31
| spl16_32 ),
inference(avatar_contradiction_clause,[],[f667]) ).
tff(f669,plain,
( ~ spl16_34
| spl16_12
| spl16_13 ),
inference(avatar_split_clause,[],[f285,f135,f129,f317]) ).
tff(f671,plain,
( spl16_18
| spl16_37
| ~ spl16_1 ),
inference(avatar_split_clause,[],[f618,f75,f484,f159]) ).
tff(f672,plain,
( spl16_33
| ~ spl16_37
| spl16_2 ),
inference(avatar_split_clause,[],[f620,f79,f484,f235]) ).
tff(f673,plain,
( spl16_14
| spl16_37
| ~ spl16_15 ),
inference(avatar_split_clause,[],[f623,f145,f484,f139]) ).
tff(f674,plain,
( $false
| ~ spl16_10
| spl16_11
| ~ spl16_25
| ~ spl16_26 ),
inference(forward_subsumption_resolution,[],[f371,f379]) ).
tff(f675,plain,
( ~ spl16_10
| spl16_11
| ~ spl16_25
| ~ spl16_26 ),
inference(avatar_contradiction_clause,[],[f674]) ).
tff(f678,plain,
( f1($false)
| ( $true = bG14 )
| ~ spl16_32 ),
inference(superposition,[],[f232,f73]) ).
tff(f679,plain,
( spl16_31
| spl16_34
| ~ spl16_32 ),
inference(avatar_split_clause,[],[f678,f231,f317,f225]) ).
tff(f685,plain,
( ~ f2($false)
| ( $true = bG3 )
| spl16_11 ),
inference(superposition,[],[f127,f73]) ).
tff(f686,plain,
( spl16_10
| ~ spl16_35
| spl16_11 ),
inference(avatar_split_clause,[],[f685,f125,f329,f119]) ).
tff(f692,plain,
( f2($false)
| ( $true = bG11 )
| ~ spl16_26 ),
inference(superposition,[],[f202,f73]) ).
tff(f693,plain,
( spl16_25
| spl16_35
| ~ spl16_26 ),
inference(avatar_split_clause,[],[f692,f201,f329,f195]) ).
tff(f694,plain,
( $false
| ~ spl16_6
| spl16_7
| ~ spl16_25
| ~ spl16_26 ),
inference(forward_subsumption_resolution,[],[f371,f654]) ).
tff(f695,plain,
( ~ spl16_6
| spl16_7
| ~ spl16_25
| ~ spl16_26 ),
inference(avatar_contradiction_clause,[],[f694]) ).
tff(f698,plain,
( f2($false)
| ( $true = bG1 )
| ~ spl16_7 ),
inference(superposition,[],[f106,f73]) ).
tff(f699,plain,
( spl16_6
| spl16_35
| ~ spl16_7 ),
inference(avatar_split_clause,[],[f698,f105,f329,f99]) ).
tff(f700,plain,
( f2($false)
| ( $true = bG2 )
| ~ spl16_9 ),
inference(superposition,[],[f116,f73]) ).
tff(f701,plain,
( spl16_8
| spl16_35
| ~ spl16_9 ),
inference(avatar_split_clause,[],[f700,f115,f329,f109]) ).
tff(f707,plain,
( $false
| ~ spl16_8
| ~ spl16_9
| ~ spl16_10
| spl16_11 ),
inference(forward_subsumption_resolution,[],[f599,f379]) ).
tff(f708,plain,
( ~ spl16_8
| ~ spl16_9
| ~ spl16_10
| spl16_11 ),
inference(avatar_contradiction_clause,[],[f707]) ).
cnf(s1,plain,
( spl16_1
| spl16_2 ),
inference(sat_conversion,[],[f82]) ).
cnf(s2,plain,
( ~ spl16_1
| ~ spl16_2 ),
inference(sat_conversion,[],[f83]) ).
cnf(s3,plain,
( ~ spl16_3
| spl16_4 ),
inference(sat_conversion,[],[f92]) ).
cnf(s4,plain,
( spl16_3
| ~ spl16_4 ),
inference(sat_conversion,[],[f93]) ).
cnf(s5,plain,
( ~ spl16_5
| spl16_6 ),
inference(sat_conversion,[],[f102]) ).
cnf(s6,plain,
( spl16_5
| ~ spl16_6 ),
inference(sat_conversion,[],[f103]) ).
cnf(s7,plain,
( ~ spl16_7
| spl16_8 ),
inference(sat_conversion,[],[f112]) ).
cnf(s8,plain,
( spl16_7
| ~ spl16_8 ),
inference(sat_conversion,[],[f113]) ).
cnf(s9,plain,
( ~ spl16_9
| spl16_10 ),
inference(sat_conversion,[],[f122]) ).
cnf(s10,plain,
( spl16_9
| ~ spl16_10 ),
inference(sat_conversion,[],[f123]) ).
cnf(s11,plain,
( ~ spl16_11
| spl16_12 ),
inference(sat_conversion,[],[f132]) ).
cnf(s12,plain,
( spl16_11
| ~ spl16_12 ),
inference(sat_conversion,[],[f133]) ).
cnf(s13,plain,
( ~ spl16_13
| spl16_14 ),
inference(sat_conversion,[],[f142]) ).
cnf(s14,plain,
( spl16_13
| ~ spl16_14 ),
inference(sat_conversion,[],[f143]) ).
cnf(s15,plain,
( ~ spl16_15
| spl16_16 ),
inference(sat_conversion,[],[f152]) ).
cnf(s16,plain,
( spl16_15
| ~ spl16_16 ),
inference(sat_conversion,[],[f153]) ).
cnf(s17,plain,
( ~ spl16_17
| spl16_18 ),
inference(sat_conversion,[],[f162]) ).
cnf(s18,plain,
( spl16_17
| ~ spl16_18 ),
inference(sat_conversion,[],[f163]) ).
cnf(s19,plain,
( ~ spl16_3
| spl16_19 ),
inference(sat_conversion,[],[f168]) ).
cnf(s20,plain,
( spl16_3
| ~ spl16_19 ),
inference(sat_conversion,[],[f169]) ).
cnf(s21,plain,
( ~ spl16_20
| spl16_21 ),
inference(sat_conversion,[],[f178]) ).
cnf(s22,plain,
( spl16_20
| ~ spl16_21 ),
inference(sat_conversion,[],[f179]) ).
cnf(s23,plain,
( ~ spl16_22
| spl16_23 ),
inference(sat_conversion,[],[f188]) ).
cnf(s24,plain,
( spl16_22
| ~ spl16_23 ),
inference(sat_conversion,[],[f189]) ).
cnf(s25,plain,
( ~ spl16_24
| spl16_25 ),
inference(sat_conversion,[],[f198]) ).
cnf(s26,plain,
( spl16_24
| ~ spl16_25 ),
inference(sat_conversion,[],[f199]) ).
cnf(s27,plain,
( ~ spl16_26
| spl16_27 ),
inference(sat_conversion,[],[f208]) ).
cnf(s28,plain,
( spl16_26
| ~ spl16_27 ),
inference(sat_conversion,[],[f209]) ).
cnf(s29,plain,
( ~ spl16_28
| spl16_29 ),
inference(sat_conversion,[],[f218]) ).
cnf(s30,plain,
( spl16_28
| ~ spl16_29 ),
inference(sat_conversion,[],[f219]) ).
cnf(s31,plain,
( ~ spl16_30
| spl16_31 ),
inference(sat_conversion,[],[f228]) ).
cnf(s32,plain,
( spl16_30
| ~ spl16_31 ),
inference(sat_conversion,[],[f229]) ).
cnf(s33,plain,
( ~ spl16_32
| spl16_33 ),
inference(sat_conversion,[],[f238]) ).
cnf(s34,plain,
( spl16_32
| ~ spl16_33 ),
inference(sat_conversion,[],[f239]) ).
cnf(s36,plain,
( spl16_1
| ~ spl16_2
| spl16_18
| spl16_33 ),
inference(sat_conversion,[],[f294]) ).
cnf(s39,plain,
( ~ spl16_2
| spl16_14
| spl16_15
| spl16_33 ),
inference(sat_conversion,[],[f301]) ).
cnf(s41,plain,
( spl16_12
| ~ spl16_13
| spl16_31
| spl16_32 ),
inference(sat_conversion,[],[f315]) ).
cnf(s46,plain,
( spl16_10
| ~ spl16_11
| spl16_25
| spl16_26 ),
inference(sat_conversion,[],[f327]) ).
cnf(s48,plain,
( spl16_8
| spl16_9
| ~ spl16_35 ),
inference(sat_conversion,[],[f333]) ).
cnf(s49,plain,
( spl16_6
| spl16_7
| ~ spl16_35 ),
inference(sat_conversion,[],[f334]) ).
cnf(s51,plain,
( spl16_10
| ~ spl16_11
| spl16_35 ),
inference(sat_conversion,[],[f337]) ).
cnf(s59,plain,
( ~ spl16_12
| ~ spl16_13
| ~ spl16_27
| spl16_28 ),
inference(sat_conversion,[],[f378]) ).
cnf(s61,plain,
( spl16_1
| ~ spl16_16
| ~ spl16_17
| ~ spl16_18 ),
inference(sat_conversion,[],[f388]) ).
cnf(s64,plain,
( ~ spl16_6
| ~ spl16_7
| ~ spl16_25
| spl16_26 ),
inference(sat_conversion,[],[f391]) ).
cnf(s69,plain,
( spl16_23
| spl16_24
| ~ spl16_36 ),
inference(sat_conversion,[],[f410]) ).
cnf(s72,plain,
( spl16_4
| ~ spl16_5
| spl16_36 ),
inference(sat_conversion,[],[f413]) ).
cnf(s73,plain,
( spl16_19
| ~ spl16_20
| spl16_36 ),
inference(sat_conversion,[],[f415]) ).
cnf(s74,plain,
( ~ spl16_4
| ~ spl16_5
| ~ spl16_21
| spl16_22 ),
inference(sat_conversion,[],[f430]) ).
cnf(s75,plain,
( ~ spl16_4
| ~ spl16_5
| ~ spl16_19
| spl16_20 ),
inference(sat_conversion,[],[f433]) ).
cnf(s80,plain,
( spl16_21
| ~ spl16_22
| spl16_36 ),
inference(sat_conversion,[],[f441]) ).
cnf(s81,plain,
( spl16_23
| ~ spl16_24
| spl16_36 ),
inference(sat_conversion,[],[f443]) ).
cnf(s82,plain,
( ~ spl16_10
| ~ spl16_11
| ~ spl16_25
| spl16_26 ),
inference(sat_conversion,[],[f445]) ).
cnf(s84,plain,
( ~ spl16_19
| spl16_20
| ~ spl16_23
| ~ spl16_24 ),
inference(sat_conversion,[],[f455]) ).
cnf(s87,plain,
( spl16_4
| spl16_5
| ~ spl16_36 ),
inference(sat_conversion,[],[f460]) ).
cnf(s88,plain,
( spl16_19
| spl16_20
| ~ spl16_36 ),
inference(sat_conversion,[],[f462]) ).
cnf(s89,plain,
( ~ spl16_12
| ~ spl16_13
| ~ spl16_31
| spl16_32 ),
inference(sat_conversion,[],[f481]) ).
cnf(s91,plain,
( spl16_16
| ~ spl16_17
| spl16_37 ),
inference(sat_conversion,[],[f489]) ).
cnf(s93,plain,
( spl16_16
| spl16_17
| ~ spl16_37 ),
inference(sat_conversion,[],[f495]) ).
cnf(s97,plain,
( ~ spl16_2
| ~ spl16_14
| spl16_15
| ~ spl16_33 ),
inference(sat_conversion,[],[f505]) ).
cnf(s98,plain,
( ~ spl16_2
| ~ spl16_16
| spl16_17
| ~ spl16_33 ),
inference(sat_conversion,[],[f511]) ).
cnf(s102,plain,
( spl16_2
| ~ spl16_14
| ~ spl16_15
| ~ spl16_33 ),
inference(sat_conversion,[],[f523]) ).
cnf(s105,plain,
( ~ spl16_1
| spl16_2
| ~ spl16_18
| ~ spl16_33 ),
inference(sat_conversion,[],[f534]) ).
cnf(s107,plain,
( ~ spl16_12
| ~ spl16_13
| ~ spl16_29
| spl16_30 ),
inference(sat_conversion,[],[f538]) ).
cnf(s120,plain,
( spl16_21
| spl16_22
| ~ spl16_36 ),
inference(sat_conversion,[],[f563]) ).
cnf(s124,plain,
( ~ spl16_4
| spl16_5
| ~ spl16_19
| ~ spl16_20 ),
inference(sat_conversion,[],[f573]) ).
cnf(s136,plain,
( ~ spl16_6
| ~ spl16_7
| ~ spl16_8
| spl16_9 ),
inference(sat_conversion,[],[f598]) ).
cnf(s137,plain,
( ~ spl16_27
| ~ spl16_28
| ~ spl16_29
| spl16_30 ),
inference(sat_conversion,[],[f612]) ).
cnf(s139,plain,
( ~ spl16_12
| spl16_13
| ~ spl16_31
| ~ spl16_32 ),
inference(sat_conversion,[],[f616]) ).
cnf(s154,plain,
( spl16_25
| spl16_26
| ~ spl16_35 ),
inference(sat_conversion,[],[f643]) ).
cnf(s155,plain,
( spl16_27
| spl16_28
| ~ spl16_34 ),
inference(sat_conversion,[],[f648]) ).
cnf(s156,plain,
( spl16_29
| spl16_30
| ~ spl16_34 ),
inference(sat_conversion,[],[f651]) ).
cnf(s157,plain,
( ~ spl16_21
| ~ spl16_22
| ~ spl16_23
| spl16_24 ),
inference(sat_conversion,[],[f653]) ).
cnf(s161,plain,
( spl16_12
| ~ spl16_13
| spl16_34 ),
inference(sat_conversion,[],[f659]) ).
cnf(s162,plain,
( spl16_27
| ~ spl16_28
| spl16_34 ),
inference(sat_conversion,[],[f662]) ).
cnf(s163,plain,
( spl16_29
| ~ spl16_30
| spl16_34 ),
inference(sat_conversion,[],[f664]) ).
cnf(s164,plain,
( ~ spl16_29
| ~ spl16_30
| ~ spl16_31
| spl16_32 ),
inference(sat_conversion,[],[f668]) ).
cnf(s165,plain,
( spl16_12
| spl16_13
| ~ spl16_34 ),
inference(sat_conversion,[],[f669]) ).
cnf(s167,plain,
( ~ spl16_1
| spl16_18
| spl16_37 ),
inference(sat_conversion,[],[f671]) ).
cnf(s168,plain,
( spl16_2
| spl16_33
| ~ spl16_37 ),
inference(sat_conversion,[],[f672]) ).
cnf(s169,plain,
( spl16_14
| ~ spl16_15
| spl16_37 ),
inference(sat_conversion,[],[f673]) ).
cnf(s170,plain,
( ~ spl16_10
| spl16_11
| ~ spl16_25
| ~ spl16_26 ),
inference(sat_conversion,[],[f675]) ).
cnf(s173,plain,
( spl16_31
| ~ spl16_32
| spl16_34 ),
inference(sat_conversion,[],[f679]) ).
cnf(s176,plain,
( spl16_10
| spl16_11
| ~ spl16_35 ),
inference(sat_conversion,[],[f686]) ).
cnf(s178,plain,
( spl16_25
| ~ spl16_26
| spl16_35 ),
inference(sat_conversion,[],[f693]) ).
cnf(s179,plain,
( ~ spl16_6
| spl16_7
| ~ spl16_25
| ~ spl16_26 ),
inference(sat_conversion,[],[f695]) ).
cnf(s182,plain,
( spl16_6
| ~ spl16_7
| spl16_35 ),
inference(sat_conversion,[],[f699]) ).
cnf(s183,plain,
( spl16_8
| ~ spl16_9
| spl16_35 ),
inference(sat_conversion,[],[f701]) ).
cnf(s186,plain,
( ~ spl16_8
| ~ spl16_9
| ~ spl16_10
| spl16_11 ),
inference(sat_conversion,[],[f708]) ).
cnf(s187,plain,
( spl16_13
| spl16_12
| spl16_27
| spl16_1 ),
inference(rat,[],[s61,s15,s18,s39,s36,s34,s173,s32,s163,s30,s162,s14,s165,s1]) ).
cnf(s188,plain,
( ~ spl16_17
| ~ spl16_16
| spl16_1 ),
inference(rat,[],[s61,s17]) ).
cnf(s189,plain,
( ~ spl16_16
| spl16_1 ),
inference(rat,[],[s36,s98,s18,s188,s1]) ).
cnf(s190,plain,
( spl16_32
| ~ spl16_31
| ~ spl16_29 ),
inference(rat,[],[s32,s164]) ).
cnf(s191,plain,
( spl16_7
| spl16_25
| spl16_6
| spl16_1 ),
inference(rat,[],[s190,s41,s33,s97,s29,s155,s13,s161,s187,s12,s46,s28,s10,s178,s183,s49,s8,s1,s15,s189]) ).
cnf(s192,plain,
( spl16_11
| ~ spl16_35
| ~ spl16_8 ),
inference(rat,[],[s186,s10,s176]) ).
cnf(s193,plain,
( ~ spl16_13
| spl16_30
| ~ spl16_12
| ~ spl16_27 ),
inference(rat,[],[s29,s107,s59]) ).
cnf(s194,plain,
( spl16_31
| ~ spl16_12
| ~ spl16_27
| spl16_1 ),
inference(rat,[],[s137,s30,s156,s173,s34,s39,s14,s193,s31,s1,s15,s189]) ).
cnf(s195,plain,
( ~ spl16_13
| ~ spl16_31
| ~ spl16_12
| spl16_1 ),
inference(rat,[],[s33,s97,s89,s13,s1,s15,s189]) ).
cnf(s196,plain,
( spl16_5
| spl16_3
| spl16_1 ),
inference(rat,[],[s39,s34,s14,s139,s195,s194,s11,s192,s27,s154,s182,s7,s191,s26,s81,s24,s80,s22,s73,s87,s6,s1,s15,s189,s20,s4]) ).
cnf(s197,plain,
( ~ spl16_13
| spl16_12
| spl16_31
| spl16_1 ),
inference(rat,[],[s33,s97,s41,s13,s1,s15,s189]) ).
cnf(s198,plain,
( spl16_12
| spl16_31
| spl16_1 ),
inference(rat,[],[s34,s173,s39,s165,s14,s197,s1,s15,s189]) ).
cnf(s199,plain,
( spl16_35
| spl16_8
| ~ spl16_11 ),
inference(rat,[],[s10,s183,s51]) ).
cnf(s200,plain,
( spl16_8
| spl16_26
| ~ spl16_11 ),
inference(rat,[],[s82,s9,s154,s48,s199]) ).
cnf(s201,plain,
( spl16_24
| ~ spl16_21
| ~ spl16_36 ),
inference(rat,[],[s157,s24,s69]) ).
cnf(s202,plain,
( spl16_31
| spl16_3
| spl16_1 ),
inference(rat,[],[s8,s64,s200,s27,s194,s12,s198,s5,s25,s201,s21,s88,s20,s72,s196,s4]) ).
cnf(s203,plain,
( spl16_27
| spl16_12
| ~ spl16_31
| spl16_1 ),
inference(rat,[],[s190,s33,s29,s97,s155,s13,s161,s187,s1,s15,s189]) ).
cnf(s204,plain,
( spl16_11
| spl16_3
| spl16_1 ),
inference(rat,[],[s136,s9,s7,s170,s179,s28,s203,s12,s5,s25,s201,s21,s88,s20,s72,s196,s4,s202]) ).
cnf(s205,plain,
( spl16_3
| spl16_1 ),
inference(rat,[],[s39,s34,s14,s139,s195,s11,s204,s202,s1,s15,s189]) ).
cnf(s206,plain,
( spl16_25
| ~ spl16_7
| spl16_26
| ~ spl16_3 ),
inference(rat,[],[s157,s23,s74,s21,s75,s6,s182,s154,s25,s19,s3]) ).
cnf(s207,plain,
( spl16_20
| ~ spl16_24
| ~ spl16_19 ),
inference(rat,[],[s120,s23,s81,s22,s84]) ).
cnf(s208,plain,
( spl16_31
| spl16_1 ),
inference(rat,[],[s207,s124,s5,s64,s26,s206,s8,s200,s27,s194,s12,s198,s19,s3,s205]) ).
cnf(s209,plain,
( spl16_25
| ~ spl16_26
| spl16_11
| ~ spl16_3 ),
inference(rat,[],[s157,s23,s74,s21,s75,s6,s49,s7,s192,s178,s25,s19,s3]) ).
cnf(s210,plain,
( spl16_11
| spl16_1 ),
inference(rat,[],[s136,s7,s179,s5,s124,s9,s207,s170,s26,s209,s28,s203,s12,s19,s3,s205,s208]) ).
cnf(s211,plain,
spl16_1,
inference(rat,[],[s39,s34,s14,s139,s195,s11,s210,s208,s15,s189,s1]) ).
cnf(s212,plain,
~ spl16_2,
inference(rat,[],[s2,s211]) ).
cnf(s213,plain,
( ~ spl16_13
| ~ spl16_15
| spl16_12
| spl16_31 ),
inference(rat,[],[s33,s102,s41,s13,s212]) ).
cnf(s214,plain,
( ~ spl16_15
| spl16_12
| spl16_31 ),
inference(rat,[],[s34,s168,s173,s169,s165,s14,s213,s212]) ).
cnf(s215,plain,
( spl16_18
| spl16_16 ),
inference(rat,[],[s93,s17,s167,s211]) ).
cnf(s216,plain,
spl16_16,
inference(rat,[],[s168,s91,s105,s18,s215,s212,s211]) ).
cnf(s217,plain,
spl16_15,
inference(rat,[],[s16,s216]) ).
cnf(s218,plain,
( spl16_25
| ~ spl16_7
| spl16_26 ),
inference(rat,[],[s21,s201,s88,s72,s6,s4,s20,s182,s206,s154,s25]) ).
cnf(s219,plain,
( spl16_3
| spl16_5
| ~ spl16_24 ),
inference(rat,[],[s80,s24,s22,s81,s73,s87,s4,s20]) ).
cnf(s220,plain,
( spl16_5
| ~ spl16_24 ),
inference(rat,[],[s124,s207,s3,s19,s219]) ).
cnf(s221,plain,
( ~ spl16_7
| spl16_26 ),
inference(rat,[],[s220,s5,s64,s26,s218]) ).
cnf(s222,plain,
( spl16_26
| ~ spl16_11 ),
inference(rat,[],[s221,s8,s200]) ).
cnf(s223,plain,
spl16_31,
inference(rat,[],[s137,s30,s156,s173,s34,s168,s169,s14,s193,s27,s222,s12,s214,s31,s212,s217]) ).
cnf(s224,plain,
spl16_30,
inference(rat,[],[s32,s223]) ).
cnf(s225,plain,
( spl16_29
| spl16_27 ),
inference(rat,[],[s155,s29,s163,s224]) ).
cnf(s226,plain,
( spl16_27
| spl16_12 ),
inference(rat,[],[s13,s102,s165,s33,s162,s190,s30,s225,s212,s217,s223]) ).
cnf(s227,plain,
( spl16_25
| spl16_11 ),
inference(rat,[],[s21,s201,s88,s72,s6,s49,s7,s4,s20,s192,s209,s178,s25,s28,s226,s12]) ).
cnf(s228,plain,
spl16_11,
inference(rat,[],[s136,s7,s179,s5,s9,s220,s170,s26,s227,s28,s226,s12]) ).
cnf(s229,plain,
spl16_12,
inference(rat,[],[s11,s228]) ).
cnf(s234,plain,
spl16_33,
inference(rat,[],[s14,s169,s89,s168,s33,s217,s229,s223,s212]) ).
cnf(s235,plain,
spl16_32,
inference(rat,[],[s34,s234]) ).
cnf(s237,plain,
~ spl16_14,
inference(rat,[],[s102,s217,s212,s234]) ).
cnf(s238,plain,
spl16_13,
inference(rat,[],[s139,s223,s229,s235]) ).
cnf(s241,plain,
$false,
inference(rat,[],[s13,s237,s238]) ).
tff(f709,plain,
$false,
inference(avatar_sat_refutation,[],[s241]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500_8.004 : 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.19 % Computer : n008.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 17:47:09 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.00/1.12 % (2465703)Detected formulas, will run a generic FOF schedule.
% 3.00/1.12 % (2465790)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=802788824:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.00/1.12 % (2465790)Instruction limit reached!
% 3.00/1.12 % (2465790)------------------------------
% 3.00/1.12 % (2465790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.00/1.12 % (2465790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.00/1.12 % (2465790)CaDiCaL version: 2.1.3
% 3.00/1.12 % (2465790)Termination reason: Instruction limit
% 3.00/1.12 % (2465790)Termination phase: Saturation
% 3.00/1.12 % (2465790)Time elapsed: 0.031 s
% 3.00/1.12 % (2465790)Peak memory usage: 88 MB
% 3.00/1.12 % (2465790)Instructions burned: 123 (million)
% 3.00/1.12 % (2465787)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=1742829252:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.00/1.12 % (2465786)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=1829917563:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.00/1.12 % (2465792)dis-21_1_sil=8000:lcm=predicate:random_seed=3717752734:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.00/1.12 % (2465788)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=2780162315:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.00/1.12 % (2465789)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2526173043:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.00/1.12 % (2465791)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4164778991:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.00/1.12 % (2465789)Refutation not found, incomplete strategy
% 3.00/1.12 % (2465789)------------------------------
% 3.00/1.12 % (2465789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.00/1.12 % (2465789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.00/1.12 % (2465789)CaDiCaL version: 2.1.3
% 3.00/1.12 % (2465789)Termination reason: Refutation not found, incomplete strategy
% 3.00/1.12 % (2465789)Time elapsed: 0.002 s
% 3.00/1.12 % (2465789)Peak memory usage: 88 MB
% 3.00/1.12 % (2465789)Instructions burned: 1 (million)
% 3.00/1.12 % (2465792)Refutation not found, incomplete strategy
% 3.00/1.12 % (2465792)------------------------------
% 3.00/1.12 % (2465792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.00/1.12 % (2465792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.00/1.12 % (2465792)CaDiCaL version: 2.1.3
% 3.00/1.12 % (2465792)Termination reason: Refutation not found, incomplete strategy
% 3.00/1.12 % (2465792)Time elapsed: 0.002 s
% 3.00/1.12 % (2465792)Peak memory usage: 88 MB
% 3.00/1.12 % (2465792)Instructions burned: 2 (million)
% 3.00/1.12 % (2465791)First to succeed.
% 3.00/1.12 % (2465791)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2465703"
% 3.00/1.12 % (2465800)lrs+10_1_sil=8000:sp=occurrence:random_seed=3773525933:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.00/1.12 % (2465800)Instruction limit reached!
% 3.00/1.12 % (2465800)------------------------------
% 3.00/1.12 % (2465800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.00/1.12 % (2465800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.00/1.12 % (2465800)CaDiCaL version: 2.1.3
% 3.00/1.12 % (2465800)Termination reason: Instruction limit
% 3.00/1.12 % (2465800)Termination phase: Saturation
% 3.00/1.12 % (2465800)Time elapsed: 0.063 s
% 3.00/1.12 % (2465800)Peak memory usage: 89 MB
% 3.00/1.12 % (2465800)Instructions burned: 289 (million)
% 3.00/1.12 % (2465792)------------------------------
% 3.00/1.12 % (2465792)------------------------------
% 3.00/1.12 % (2465789)------------------------------
% 3.00/1.12 % (2465789)------------------------------
% 3.00/1.12 % (2465791)Refutation found. Thanks to Tanya!
% 3.00/1.12 % SZS status Theorem for theBenchmark
% 3.00/1.12 % SZS output start Proof for theBenchmark
% See solution above
% 3.88/1.32 % (2465791)------------------------------
% 3.88/1.32 % (2465791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.88/1.32 % (2465791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.88/1.32 % (2465791)CaDiCaL version: 2.1.3
% 3.88/1.32 % (2465791)Termination reason: Refutation
% 3.88/1.32 % (2465791)Time elapsed: 0.018 s
% 3.88/1.32 % (2465791)Peak memory usage: 90 MB
% 3.88/1.32 % (2465791)Instructions burned: 24 (million)
% 3.88/1.32 % (2465791)------------------------------
% 3.88/1.32 % (2465791)------------------------------
% 3.88/1.32 % (2465703)Success in time 0.452 s
% 3.88/1.32 % Vampire exiting
%------------------------------------------------------------------------------