%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO500_8.003 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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 1.80s 0.73s
% Output : Refutation 2.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 42
% Syntax : Number of formulae : 384 ( 20 unt; 0 typ; 40 def)
% Number of atoms : 1452 ( 122 equ)
% Maximal formula atoms : 5 ( 3 avg)
% Number of connectives : 1108 ( 467 ~; 586 |; 13 &)
% ( 41 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 429 ( 427 fml; 2 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 47 ( 44 usr; 43 prp; 0-2 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 1 ( 0 sgn 1 !; 0 ?; 1 :)
% 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(pred_def_2,type,
f0: $o > $o ).
tff(pred_def_3,type,
f1: $o > $o ).
tff(pred_def_4,type,
f2: $o > $o ).
tff(f1,conjecture,
f0(f1(f1(f1(f2(x))))) = f0(f0(f0(f1(f2(f2(f2(x))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kaminski3) ).
tff(f2,negated_conjecture,
f0(f1(f1(f1(f2(x))))) != f0(f0(f0(f1(f2(f2(f2(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,
( f2(bG0)
<=> ( $true = bG1 ) ),
introduced(definition,[new_symbols(definition,[bG1])],[fool_formula_definition]) ).
tff(f5,definition,
( f1(bG1)
<=> ( $true = bG2 ) ),
introduced(definition,[new_symbols(definition,[bG2])],[fool_formula_definition]) ).
tff(f6,definition,
( f1(bG2)
<=> ( $true = bG3 ) ),
introduced(definition,[new_symbols(definition,[bG3])],[fool_formula_definition]) ).
tff(f7,definition,
( f1(bG3)
<=> ( $true = bG4 ) ),
introduced(definition,[new_symbols(definition,[bG4])],[fool_formula_definition]) ).
tff(f8,definition,
( x
<=> ( $true = bG5 ) ),
introduced(definition,[new_symbols(definition,[bG5])],[fool_formula_definition]) ).
tff(f9,definition,
( f2(bG5)
<=> ( $true = bG6 ) ),
introduced(definition,[new_symbols(definition,[bG6])],[fool_formula_definition]) ).
tff(f10,definition,
( f2(bG6)
<=> ( $true = bG7 ) ),
introduced(definition,[new_symbols(definition,[bG7])],[fool_formula_definition]) ).
tff(f11,definition,
( f2(bG7)
<=> ( $true = bG8 ) ),
introduced(definition,[new_symbols(definition,[bG8])],[fool_formula_definition]) ).
tff(f12,definition,
( f1(bG8)
<=> ( $true = bG9 ) ),
introduced(definition,[new_symbols(definition,[bG9])],[fool_formula_definition]) ).
tff(f13,definition,
( f0(bG9)
<=> ( $true = bG10 ) ),
introduced(definition,[new_symbols(definition,[bG10])],[fool_formula_definition]) ).
tff(f14,definition,
( f0(bG10)
<=> ( $true = bG11 ) ),
introduced(definition,[new_symbols(definition,[bG11])],[fool_formula_definition]) ).
tff(f15,plain,
~ ( f0(bG4)
<=> f0(bG11) ),
inference(fool_elimination,[],[f2,f14,f13,f12,f11,f10,f9,f8,f7,f6,f5,f4,f3]) ).
tff(f16,plain,
( f0(bG4)
<~> f0(bG11) ),
inference(ennf_transformation,[],[f15]) ).
tff(f17,plain,
( ( f0(bG10)
| ( $true != bG11 ) )
& ( ( $true = bG11 )
| ~ f0(bG10) ) ),
inference(nnf_transformation,[],[f14]) ).
tff(f18,plain,
( ( f0(bG9)
| ( $true != bG10 ) )
& ( ( $true = bG10 )
| ~ f0(bG9) ) ),
inference(nnf_transformation,[],[f13]) ).
tff(f19,plain,
( ( f1(bG8)
| ( $true != bG9 ) )
& ( ( $true = bG9 )
| ~ f1(bG8) ) ),
inference(nnf_transformation,[],[f12]) ).
tff(f20,plain,
( ( f2(bG7)
| ( $true != bG8 ) )
& ( ( $true = bG8 )
| ~ f2(bG7) ) ),
inference(nnf_transformation,[],[f11]) ).
tff(f21,plain,
( ( f2(bG6)
| ( $true != bG7 ) )
& ( ( $true = bG7 )
| ~ f2(bG6) ) ),
inference(nnf_transformation,[],[f10]) ).
tff(f22,plain,
( ( f2(bG5)
| ( $true != bG6 ) )
& ( ( $true = bG6 )
| ~ f2(bG5) ) ),
inference(nnf_transformation,[],[f9]) ).
tff(f23,plain,
( ( x
| ( $true != bG5 ) )
& ( ( $true = bG5 )
| ~ x ) ),
inference(nnf_transformation,[],[f8]) ).
tff(f24,plain,
( ( f1(bG3)
| ( $true != bG4 ) )
& ( ( $true = bG4 )
| ~ f1(bG3) ) ),
inference(nnf_transformation,[],[f7]) ).
tff(f25,plain,
( ( f1(bG2)
| ( $true != bG3 ) )
& ( ( $true = bG3 )
| ~ f1(bG2) ) ),
inference(nnf_transformation,[],[f6]) ).
tff(f26,plain,
( ( f1(bG1)
| ( $true != bG2 ) )
& ( ( $true = bG2 )
| ~ f1(bG1) ) ),
inference(nnf_transformation,[],[f5]) ).
tff(f27,plain,
( ( f2(bG0)
| ( $true != bG1 ) )
& ( ( $true = bG1 )
| ~ f2(bG0) ) ),
inference(nnf_transformation,[],[f4]) ).
tff(f28,plain,
( ( x
| ( bG0 != $true ) )
& ( ( bG0 = $true )
| ~ x ) ),
inference(nnf_transformation,[],[f3]) ).
tff(f29,plain,
( ( ~ f0(bG11)
| ~ f0(bG4) )
& ( f0(bG11)
| f0(bG4) ) ),
inference(nnf_transformation,[],[f16]) ).
tff(f30,plain,
( ( $true = bG11 )
| ~ f0(bG10) ),
inference(cnf_transformation,[],[f17]) ).
tff(f31,plain,
( f0(bG10)
| ( $true != bG11 ) ),
inference(cnf_transformation,[],[f17]) ).
tff(f32,plain,
( ( $true = bG10 )
| ~ f0(bG9) ),
inference(cnf_transformation,[],[f18]) ).
tff(f33,plain,
( f0(bG9)
| ( $true != bG10 ) ),
inference(cnf_transformation,[],[f18]) ).
tff(f34,plain,
( ( $true = bG9 )
| ~ f1(bG8) ),
inference(cnf_transformation,[],[f19]) ).
tff(f35,plain,
( f1(bG8)
| ( $true != bG9 ) ),
inference(cnf_transformation,[],[f19]) ).
tff(f36,plain,
( ( $true = bG8 )
| ~ f2(bG7) ),
inference(cnf_transformation,[],[f20]) ).
tff(f37,plain,
( f2(bG7)
| ( $true != bG8 ) ),
inference(cnf_transformation,[],[f20]) ).
tff(f38,plain,
( ( $true = bG7 )
| ~ f2(bG6) ),
inference(cnf_transformation,[],[f21]) ).
tff(f39,plain,
( f2(bG6)
| ( $true != bG7 ) ),
inference(cnf_transformation,[],[f21]) ).
tff(f40,plain,
( ( $true = bG6 )
| ~ f2(bG5) ),
inference(cnf_transformation,[],[f22]) ).
tff(f41,plain,
( f2(bG5)
| ( $true != bG6 ) ),
inference(cnf_transformation,[],[f22]) ).
tff(f42,plain,
( ( $true = bG5 )
| ~ x ),
inference(cnf_transformation,[],[f23]) ).
tff(f43,plain,
( x
| ( $true != bG5 ) ),
inference(cnf_transformation,[],[f23]) ).
tff(f44,plain,
( ( $true = bG4 )
| ~ f1(bG3) ),
inference(cnf_transformation,[],[f24]) ).
tff(f45,plain,
( f1(bG3)
| ( $true != bG4 ) ),
inference(cnf_transformation,[],[f24]) ).
tff(f46,plain,
( ( $true = bG3 )
| ~ f1(bG2) ),
inference(cnf_transformation,[],[f25]) ).
tff(f47,plain,
( f1(bG2)
| ( $true != bG3 ) ),
inference(cnf_transformation,[],[f25]) ).
tff(f48,plain,
( ( $true = bG2 )
| ~ f1(bG1) ),
inference(cnf_transformation,[],[f26]) ).
tff(f49,plain,
( f1(bG1)
| ( $true != bG2 ) ),
inference(cnf_transformation,[],[f26]) ).
tff(f50,plain,
( ( $true = bG1 )
| ~ f2(bG0) ),
inference(cnf_transformation,[],[f27]) ).
tff(f51,plain,
( f2(bG0)
| ( $true != bG1 ) ),
inference(cnf_transformation,[],[f27]) ).
tff(f52,plain,
( ( bG0 = $true )
| ~ x ),
inference(cnf_transformation,[],[f28]) ).
tff(f53,plain,
( x
| ( bG0 != $true ) ),
inference(cnf_transformation,[],[f28]) ).
tff(f54,plain,
( f0(bG11)
| f0(bG4) ),
inference(cnf_transformation,[],[f29]) ).
tff(f55,plain,
( ~ f0(bG11)
| ~ f0(bG4) ),
inference(cnf_transformation,[],[f29]) ).
tff(f57,plain,
! [X0: $o] :
( ( $false = (X0) )
| ( $true = (X0) ) ),
introduced(definition,[],[fool_exhaustiveness_axiom]) ).
tff(f59,definition,
( spl12_1
<=> f0(bG4) ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
tff(f60,plain,
( ~ f0(bG4)
| spl12_1 ),
inference(avatar_component_clause,[],[f59]) ).
tff(f61,plain,
( f0(bG4)
| ~ spl12_1 ),
inference(avatar_component_clause,[],[f59]) ).
tff(f63,definition,
( spl12_2
<=> f0(bG11) ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
tff(f64,plain,
( ~ f0(bG11)
| spl12_2 ),
inference(avatar_component_clause,[],[f63]) ).
tff(f65,plain,
( f0(bG11)
| ~ spl12_2 ),
inference(avatar_component_clause,[],[f63]) ).
tff(f66,plain,
( spl12_1
| spl12_2 ),
inference(avatar_split_clause,[],[f54,f63,f59]) ).
tff(f67,plain,
( ~ spl12_1
| ~ spl12_2 ),
inference(avatar_split_clause,[],[f55,f63,f59]) ).
tff(f69,definition,
( spl12_3
<=> x ),
introduced(definition,[new_symbols(definition,[spl12_3])],[avatar_definition]) ).
tff(f73,definition,
( spl12_4
<=> ( bG0 = $true ) ),
introduced(definition,[new_symbols(definition,[spl12_4])],[avatar_definition]) ).
tff(f75,plain,
( ( bG0 = $true )
| ~ spl12_4 ),
inference(avatar_component_clause,[],[f73]) ).
tff(f76,plain,
( ~ spl12_3
| spl12_4 ),
inference(avatar_split_clause,[],[f52,f73,f69]) ).
tff(f77,plain,
( ~ spl12_4
| spl12_3 ),
inference(avatar_split_clause,[],[f53,f69,f73]) ).
tff(f79,definition,
( spl12_5
<=> f2(bG0) ),
introduced(definition,[new_symbols(definition,[spl12_5])],[avatar_definition]) ).
tff(f80,plain,
( f2(bG0)
| ~ spl12_5 ),
inference(avatar_component_clause,[],[f79]) ).
tff(f81,plain,
( ~ f2(bG0)
| spl12_5 ),
inference(avatar_component_clause,[],[f79]) ).
tff(f83,definition,
( spl12_6
<=> ( $true = bG1 ) ),
introduced(definition,[new_symbols(definition,[spl12_6])],[avatar_definition]) ).
tff(f84,plain,
( ( $true != bG1 )
| spl12_6 ),
inference(avatar_component_clause,[],[f83]) ).
tff(f85,plain,
( ( $true = bG1 )
| ~ spl12_6 ),
inference(avatar_component_clause,[],[f83]) ).
tff(f86,plain,
( ~ spl12_5
| spl12_6 ),
inference(avatar_split_clause,[],[f50,f83,f79]) ).
tff(f87,plain,
( ~ spl12_6
| spl12_5 ),
inference(avatar_split_clause,[],[f51,f79,f83]) ).
tff(f89,definition,
( spl12_7
<=> f1(bG1) ),
introduced(definition,[new_symbols(definition,[spl12_7])],[avatar_definition]) ).
tff(f90,plain,
( f1(bG1)
| ~ spl12_7 ),
inference(avatar_component_clause,[],[f89]) ).
tff(f91,plain,
( ~ f1(bG1)
| spl12_7 ),
inference(avatar_component_clause,[],[f89]) ).
tff(f93,definition,
( spl12_8
<=> ( $true = bG2 ) ),
introduced(definition,[new_symbols(definition,[spl12_8])],[avatar_definition]) ).
tff(f95,plain,
( ( $true = bG2 )
| ~ spl12_8 ),
inference(avatar_component_clause,[],[f93]) ).
tff(f96,plain,
( ~ spl12_7
| spl12_8 ),
inference(avatar_split_clause,[],[f48,f93,f89]) ).
tff(f97,plain,
( ~ spl12_8
| spl12_7 ),
inference(avatar_split_clause,[],[f49,f89,f93]) ).
tff(f99,definition,
( spl12_9
<=> f1(bG2) ),
introduced(definition,[new_symbols(definition,[spl12_9])],[avatar_definition]) ).
tff(f100,plain,
( f1(bG2)
| ~ spl12_9 ),
inference(avatar_component_clause,[],[f99]) ).
tff(f101,plain,
( ~ f1(bG2)
| spl12_9 ),
inference(avatar_component_clause,[],[f99]) ).
tff(f103,definition,
( spl12_10
<=> ( $true = bG3 ) ),
introduced(definition,[new_symbols(definition,[spl12_10])],[avatar_definition]) ).
tff(f104,plain,
( ( $true != bG3 )
| spl12_10 ),
inference(avatar_component_clause,[],[f103]) ).
tff(f105,plain,
( ( $true = bG3 )
| ~ spl12_10 ),
inference(avatar_component_clause,[],[f103]) ).
tff(f106,plain,
( ~ spl12_9
| spl12_10 ),
inference(avatar_split_clause,[],[f46,f103,f99]) ).
tff(f107,plain,
( ~ spl12_10
| spl12_9 ),
inference(avatar_split_clause,[],[f47,f99,f103]) ).
tff(f109,definition,
( spl12_11
<=> f1(bG3) ),
introduced(definition,[new_symbols(definition,[spl12_11])],[avatar_definition]) ).
tff(f110,plain,
( f1(bG3)
| ~ spl12_11 ),
inference(avatar_component_clause,[],[f109]) ).
tff(f111,plain,
( ~ f1(bG3)
| spl12_11 ),
inference(avatar_component_clause,[],[f109]) ).
tff(f113,definition,
( spl12_12
<=> ( $true = bG4 ) ),
introduced(definition,[new_symbols(definition,[spl12_12])],[avatar_definition]) ).
tff(f115,plain,
( ( $true = bG4 )
| ~ spl12_12 ),
inference(avatar_component_clause,[],[f113]) ).
tff(f116,plain,
( ~ spl12_11
| spl12_12 ),
inference(avatar_split_clause,[],[f44,f113,f109]) ).
tff(f117,plain,
( ~ spl12_12
| spl12_11 ),
inference(avatar_split_clause,[],[f45,f109,f113]) ).
tff(f119,definition,
( spl12_13
<=> ( $true = bG5 ) ),
introduced(definition,[new_symbols(definition,[spl12_13])],[avatar_definition]) ).
tff(f121,plain,
( ( $true = bG5 )
| ~ spl12_13 ),
inference(avatar_component_clause,[],[f119]) ).
tff(f122,plain,
( ~ spl12_3
| spl12_13 ),
inference(avatar_split_clause,[],[f42,f119,f69]) ).
tff(f123,plain,
( ~ spl12_13
| spl12_3 ),
inference(avatar_split_clause,[],[f43,f69,f119]) ).
tff(f125,definition,
( spl12_14
<=> f2(bG5) ),
introduced(definition,[new_symbols(definition,[spl12_14])],[avatar_definition]) ).
tff(f126,plain,
( f2(bG5)
| ~ spl12_14 ),
inference(avatar_component_clause,[],[f125]) ).
tff(f127,plain,
( ~ f2(bG5)
| spl12_14 ),
inference(avatar_component_clause,[],[f125]) ).
tff(f129,definition,
( spl12_15
<=> ( $true = bG6 ) ),
introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition]) ).
tff(f131,plain,
( ( $true = bG6 )
| ~ spl12_15 ),
inference(avatar_component_clause,[],[f129]) ).
tff(f132,plain,
( ~ spl12_14
| spl12_15 ),
inference(avatar_split_clause,[],[f40,f129,f125]) ).
tff(f133,plain,
( ~ spl12_15
| spl12_14 ),
inference(avatar_split_clause,[],[f41,f125,f129]) ).
tff(f135,definition,
( spl12_16
<=> f2(bG6) ),
introduced(definition,[new_symbols(definition,[spl12_16])],[avatar_definition]) ).
tff(f136,plain,
( f2(bG6)
| ~ spl12_16 ),
inference(avatar_component_clause,[],[f135]) ).
tff(f137,plain,
( ~ f2(bG6)
| spl12_16 ),
inference(avatar_component_clause,[],[f135]) ).
tff(f139,definition,
( spl12_17
<=> ( $true = bG7 ) ),
introduced(definition,[new_symbols(definition,[spl12_17])],[avatar_definition]) ).
tff(f141,plain,
( ( $true = bG7 )
| ~ spl12_17 ),
inference(avatar_component_clause,[],[f139]) ).
tff(f142,plain,
( ~ spl12_16
| spl12_17 ),
inference(avatar_split_clause,[],[f38,f139,f135]) ).
tff(f143,plain,
( ~ spl12_17
| spl12_16 ),
inference(avatar_split_clause,[],[f39,f135,f139]) ).
tff(f145,definition,
( spl12_18
<=> f2(bG7) ),
introduced(definition,[new_symbols(definition,[spl12_18])],[avatar_definition]) ).
tff(f146,plain,
( f2(bG7)
| ~ spl12_18 ),
inference(avatar_component_clause,[],[f145]) ).
tff(f147,plain,
( ~ f2(bG7)
| spl12_18 ),
inference(avatar_component_clause,[],[f145]) ).
tff(f149,definition,
( spl12_19
<=> ( $true = bG8 ) ),
introduced(definition,[new_symbols(definition,[spl12_19])],[avatar_definition]) ).
tff(f150,plain,
( ( $true != bG8 )
| spl12_19 ),
inference(avatar_component_clause,[],[f149]) ).
tff(f151,plain,
( ( $true = bG8 )
| ~ spl12_19 ),
inference(avatar_component_clause,[],[f149]) ).
tff(f152,plain,
( ~ spl12_18
| spl12_19 ),
inference(avatar_split_clause,[],[f36,f149,f145]) ).
tff(f153,plain,
( ~ spl12_19
| spl12_18 ),
inference(avatar_split_clause,[],[f37,f145,f149]) ).
tff(f155,definition,
( spl12_20
<=> f1(bG8) ),
introduced(definition,[new_symbols(definition,[spl12_20])],[avatar_definition]) ).
tff(f156,plain,
( f1(bG8)
| ~ spl12_20 ),
inference(avatar_component_clause,[],[f155]) ).
tff(f157,plain,
( ~ f1(bG8)
| spl12_20 ),
inference(avatar_component_clause,[],[f155]) ).
tff(f159,definition,
( spl12_21
<=> ( $true = bG9 ) ),
introduced(definition,[new_symbols(definition,[spl12_21])],[avatar_definition]) ).
tff(f161,plain,
( ( $true = bG9 )
| ~ spl12_21 ),
inference(avatar_component_clause,[],[f159]) ).
tff(f162,plain,
( ~ spl12_20
| spl12_21 ),
inference(avatar_split_clause,[],[f34,f159,f155]) ).
tff(f163,plain,
( ~ spl12_21
| spl12_20 ),
inference(avatar_split_clause,[],[f35,f155,f159]) ).
tff(f165,definition,
( spl12_22
<=> f0(bG9) ),
introduced(definition,[new_symbols(definition,[spl12_22])],[avatar_definition]) ).
tff(f166,plain,
( f0(bG9)
| ~ spl12_22 ),
inference(avatar_component_clause,[],[f165]) ).
tff(f167,plain,
( ~ f0(bG9)
| spl12_22 ),
inference(avatar_component_clause,[],[f165]) ).
tff(f169,definition,
( spl12_23
<=> ( $true = bG10 ) ),
introduced(definition,[new_symbols(definition,[spl12_23])],[avatar_definition]) ).
tff(f171,plain,
( ( $true = bG10 )
| ~ spl12_23 ),
inference(avatar_component_clause,[],[f169]) ).
tff(f172,plain,
( ~ spl12_22
| spl12_23 ),
inference(avatar_split_clause,[],[f32,f169,f165]) ).
tff(f173,plain,
( ~ spl12_23
| spl12_22 ),
inference(avatar_split_clause,[],[f33,f165,f169]) ).
tff(f175,definition,
( spl12_24
<=> f0(bG10) ),
introduced(definition,[new_symbols(definition,[spl12_24])],[avatar_definition]) ).
tff(f176,plain,
( f0(bG10)
| ~ spl12_24 ),
inference(avatar_component_clause,[],[f175]) ).
tff(f177,plain,
( ~ f0(bG10)
| spl12_24 ),
inference(avatar_component_clause,[],[f175]) ).
tff(f179,definition,
( spl12_25
<=> ( $true = bG11 ) ),
introduced(definition,[new_symbols(definition,[spl12_25])],[avatar_definition]) ).
tff(f180,plain,
( ( $true != bG11 )
| spl12_25 ),
inference(avatar_component_clause,[],[f179]) ).
tff(f181,plain,
( ( $true = bG11 )
| ~ spl12_25 ),
inference(avatar_component_clause,[],[f179]) ).
tff(f182,plain,
( ~ spl12_24
| spl12_25 ),
inference(avatar_split_clause,[],[f30,f179,f175]) ).
tff(f183,plain,
( ~ spl12_25
| spl12_24 ),
inference(avatar_split_clause,[],[f31,f175,f179]) ).
tff(f188,plain,
( ~ f1($false)
| ( $true = bG1 )
| spl12_7 ),
inference(superposition,[],[f91,f57]) ).
tff(f194,plain,
( ~ f0($false)
| ( $true = bG4 )
| spl12_1 ),
inference(superposition,[],[f60,f57]) ).
tff(f202,plain,
( ~ f1($false)
| ( $true = bG8 )
| spl12_20 ),
inference(superposition,[],[f157,f57]) ).
tff(f208,plain,
( f0($false)
| ( $true = bG11 )
| ~ spl12_2 ),
inference(superposition,[],[f65,f57]) ).
tff(f210,plain,
( f0($false)
| ~ spl12_2
| spl12_25 ),
inference(forward_subsumption_resolution,[],[f208,f180]) ).
tff(f213,plain,
( ~ f1($false)
| spl12_19
| spl12_20 ),
inference(forward_subsumption_resolution,[],[f202,f150]) ).
tff(f220,plain,
( ~ f1($false)
| spl12_6
| spl12_7 ),
inference(forward_subsumption_resolution,[],[f188,f84]) ).
tff(f225,plain,
( ( $true = bG4 )
| spl12_1
| ~ spl12_2
| spl12_25 ),
inference(forward_subsumption_resolution,[],[f194,f210]) ).
tff(f226,plain,
( spl12_12
| spl12_1
| ~ spl12_2
| spl12_25 ),
inference(avatar_split_clause,[],[f225,f179,f63,f59,f113]) ).
tff(f227,plain,
( f1($false)
| ( $true = bG3 )
| ~ spl12_11 ),
inference(superposition,[],[f110,f57]) ).
tff(f228,plain,
( f1($false)
| spl12_10
| ~ spl12_11 ),
inference(forward_subsumption_resolution,[],[f227,f104]) ).
tff(f248,plain,
( $false
| spl12_10
| ~ spl12_11
| spl12_19
| spl12_20 ),
inference(forward_subsumption_resolution,[],[f228,f213]) ).
tff(f249,plain,
( spl12_10
| ~ spl12_11
| spl12_19
| spl12_20 ),
inference(avatar_contradiction_clause,[],[f248]) ).
tff(f251,definition,
( spl12_26
<=> f1($false) ),
introduced(definition,[new_symbols(definition,[spl12_26])],[avatar_definition]) ).
tff(f256,plain,
( ~ spl12_26
| spl12_6
| spl12_7 ),
inference(avatar_split_clause,[],[f220,f89,f83,f251]) ).
tff(f259,plain,
( f0($true)
| ~ spl12_23
| ~ spl12_24 ),
inference(forward_demodulation,[],[f176,f171]) ).
tff(f261,definition,
( spl12_27
<=> f0($false) ),
introduced(definition,[new_symbols(definition,[spl12_27])],[avatar_definition]) ).
tff(f263,plain,
( f0($false)
| ~ spl12_27 ),
inference(avatar_component_clause,[],[f261]) ).
tff(f279,plain,
( f0($true)
| ~ spl12_2
| ~ spl12_25 ),
inference(superposition,[],[f65,f181]) ).
tff(f287,plain,
( f1($true)
| ~ spl12_19
| ~ spl12_20 ),
inference(superposition,[],[f156,f151]) ).
tff(f290,plain,
( f0($true)
| ~ spl12_21
| ~ spl12_22 ),
inference(superposition,[],[f166,f161]) ).
tff(f296,definition,
( spl12_28
<=> f2($false) ),
introduced(definition,[new_symbols(definition,[spl12_28])],[avatar_definition]) ).
tff(f303,plain,
( f2($false)
| ( $true = bG5 )
| ~ spl12_14 ),
inference(superposition,[],[f126,f57]) ).
tff(f306,plain,
( spl12_13
| spl12_28
| ~ spl12_14 ),
inference(avatar_split_clause,[],[f303,f125,f296,f119]) ).
tff(f311,plain,
( ~ f2($true)
| ~ spl12_4
| spl12_5 ),
inference(superposition,[],[f81,f75]) ).
tff(f314,plain,
( f2($true)
| ~ spl12_13
| ~ spl12_14 ),
inference(superposition,[],[f126,f121]) ).
tff(f316,plain,
( $false
| ~ spl12_4
| spl12_5
| ~ spl12_13
| ~ spl12_14 ),
inference(forward_subsumption_resolution,[],[f314,f311]) ).
tff(f317,plain,
( ~ spl12_4
| spl12_5
| ~ spl12_13
| ~ spl12_14 ),
inference(avatar_contradiction_clause,[],[f316]) ).
tff(f318,plain,
( f2($true)
| ~ spl12_4
| ~ spl12_5 ),
inference(forward_demodulation,[],[f80,f75]) ).
tff(f320,plain,
( ~ f1($true)
| ~ spl12_6
| spl12_7 ),
inference(superposition,[],[f91,f85]) ).
tff(f322,plain,
( $false
| ~ spl12_6
| spl12_7
| ~ spl12_19
| ~ spl12_20 ),
inference(forward_subsumption_resolution,[],[f320,f287]) ).
tff(f323,plain,
( ~ spl12_6
| spl12_7
| ~ spl12_19
| ~ spl12_20 ),
inference(avatar_contradiction_clause,[],[f322]) ).
tff(f324,plain,
( ~ f1($true)
| ~ spl12_19
| spl12_20 ),
inference(forward_demodulation,[],[f157,f151]) ).
tff(f328,plain,
( f0($false)
| ( $true = bG10 )
| ~ spl12_24 ),
inference(superposition,[],[f176,f57]) ).
tff(f331,plain,
( ~ f0($true)
| spl12_2
| ~ spl12_25 ),
inference(forward_demodulation,[],[f64,f181]) ).
tff(f334,plain,
( spl12_23
| spl12_27
| ~ spl12_24 ),
inference(avatar_split_clause,[],[f328,f175,f261,f169]) ).
tff(f335,plain,
( f1($true)
| ~ spl12_6
| ~ spl12_7 ),
inference(forward_demodulation,[],[f90,f85]) ).
tff(f337,plain,
( f0($false)
| ( $true = bG4 )
| ~ spl12_1 ),
inference(superposition,[],[f61,f57]) ).
tff(f345,plain,
( ~ f1($true)
| ~ spl12_8
| spl12_9 ),
inference(superposition,[],[f101,f95]) ).
tff(f347,plain,
( $false
| ~ spl12_6
| ~ spl12_7
| ~ spl12_8
| spl12_9 ),
inference(forward_subsumption_resolution,[],[f345,f335]) ).
tff(f348,plain,
( ~ spl12_6
| ~ spl12_7
| ~ spl12_8
| spl12_9 ),
inference(avatar_contradiction_clause,[],[f347]) ).
tff(f349,plain,
( f1($true)
| ~ spl12_8
| ~ spl12_9 ),
inference(forward_demodulation,[],[f100,f95]) ).
tff(f351,plain,
( ~ f1($true)
| ~ spl12_10
| spl12_11 ),
inference(superposition,[],[f111,f105]) ).
tff(f353,plain,
( $false
| ~ spl12_6
| ~ spl12_7
| ~ spl12_10
| spl12_11 ),
inference(forward_subsumption_resolution,[],[f351,f335]) ).
tff(f354,plain,
( ~ spl12_6
| ~ spl12_7
| ~ spl12_10
| spl12_11 ),
inference(avatar_contradiction_clause,[],[f353]) ).
tff(f357,plain,
( $false
| spl12_2
| ~ spl12_23
| ~ spl12_24
| ~ spl12_25 ),
inference(forward_subsumption_resolution,[],[f259,f331]) ).
tff(f358,plain,
( spl12_2
| ~ spl12_23
| ~ spl12_24
| ~ spl12_25 ),
inference(avatar_contradiction_clause,[],[f357]) ).
tff(f360,plain,
( ~ f0($false)
| ( $true = bG11 )
| spl12_2 ),
inference(superposition,[],[f64,f57]) ).
tff(f366,plain,
( spl12_25
| ~ spl12_27
| spl12_2 ),
inference(avatar_split_clause,[],[f360,f63,f261,f179]) ).
tff(f367,plain,
( spl12_12
| spl12_27
| ~ spl12_1 ),
inference(avatar_split_clause,[],[f337,f59,f261,f113]) ).
tff(f368,plain,
( f1($false)
| ( $true = bG3 )
| ~ spl12_11 ),
inference(superposition,[],[f110,f57]) ).
tff(f369,plain,
( spl12_10
| spl12_26
| ~ spl12_11 ),
inference(avatar_split_clause,[],[f368,f109,f251,f103]) ).
tff(f377,plain,
( f0($true)
| ~ spl12_1
| ~ spl12_12 ),
inference(superposition,[],[f61,f115]) ).
tff(f381,plain,
( ~ f0($true)
| ~ spl12_23
| spl12_24 ),
inference(superposition,[],[f177,f171]) ).
tff(f383,plain,
( $false
| ~ spl12_1
| ~ spl12_12
| ~ spl12_23
| spl12_24 ),
inference(forward_subsumption_resolution,[],[f381,f377]) ).
tff(f384,plain,
( ~ spl12_1
| ~ spl12_12
| ~ spl12_23
| spl12_24 ),
inference(avatar_contradiction_clause,[],[f383]) ).
tff(f385,plain,
( ~ f0($false)
| ( $true = bG9 )
| spl12_22 ),
inference(superposition,[],[f167,f57]) ).
tff(f387,plain,
( ~ f2($false)
| ( bG0 = $true )
| spl12_5 ),
inference(superposition,[],[f81,f57]) ).
tff(f388,plain,
( spl12_4
| ~ spl12_28
| spl12_5 ),
inference(avatar_split_clause,[],[f387,f79,f296,f73]) ).
tff(f392,plain,
( ~ f1($false)
| ( $true = bG2 )
| spl12_9 ),
inference(superposition,[],[f101,f57]) ).
tff(f393,plain,
( spl12_8
| ~ spl12_26
| spl12_9 ),
inference(avatar_split_clause,[],[f392,f99,f251,f93]) ).
tff(f415,plain,
( ~ f0($true)
| ~ spl12_21
| spl12_22 ),
inference(superposition,[],[f167,f161]) ).
tff(f417,plain,
( $false
| ~ spl12_1
| ~ spl12_12
| ~ spl12_21
| spl12_22 ),
inference(forward_subsumption_resolution,[],[f415,f377]) ).
tff(f418,plain,
( ~ spl12_1
| ~ spl12_12
| ~ spl12_21
| spl12_22 ),
inference(avatar_contradiction_clause,[],[f417]) ).
tff(f422,plain,
( f1($false)
| ( $true = bG2 )
| ~ spl12_9 ),
inference(superposition,[],[f100,f57]) ).
tff(f423,plain,
( spl12_8
| spl12_26
| ~ spl12_9 ),
inference(avatar_split_clause,[],[f422,f99,f251,f93]) ).
tff(f424,plain,
( f2($false)
| ( bG0 = $true )
| ~ spl12_5 ),
inference(superposition,[],[f80,f57]) ).
tff(f447,plain,
( f1($true)
| ~ spl12_10
| ~ spl12_11 ),
inference(superposition,[],[f110,f105]) ).
tff(f450,plain,
( f2($true)
| ~ spl12_15
| ~ spl12_16 ),
inference(superposition,[],[f136,f131]) ).
tff(f453,plain,
( ~ f2($true)
| ~ spl12_17
| spl12_18 ),
inference(superposition,[],[f147,f141]) ).
tff(f456,plain,
( $false
| ~ spl12_15
| ~ spl12_16
| ~ spl12_17
| spl12_18 ),
inference(forward_subsumption_resolution,[],[f453,f450]) ).
tff(f457,plain,
( ~ spl12_15
| ~ spl12_16
| ~ spl12_17
| spl12_18 ),
inference(avatar_contradiction_clause,[],[f456]) ).
tff(f458,plain,
( f2($true)
| ~ spl12_17
| ~ spl12_18 ),
inference(forward_demodulation,[],[f146,f141]) ).
tff(f461,plain,
( $false
| ~ spl12_6
| ~ spl12_7
| ~ spl12_19
| spl12_20 ),
inference(forward_subsumption_resolution,[],[f324,f335]) ).
tff(f462,plain,
( ~ spl12_6
| ~ spl12_7
| ~ spl12_19
| spl12_20 ),
inference(avatar_contradiction_clause,[],[f461]) ).
tff(f469,plain,
( $false
| ~ spl12_10
| ~ spl12_11
| ~ spl12_19
| spl12_20 ),
inference(forward_subsumption_resolution,[],[f447,f324]) ).
tff(f470,plain,
( ~ spl12_10
| ~ spl12_11
| ~ spl12_19
| spl12_20 ),
inference(avatar_contradiction_clause,[],[f469]) ).
tff(f472,plain,
( ~ f2($true)
| ~ spl12_17
| spl12_18 ),
inference(forward_demodulation,[],[f147,f141]) ).
tff(f473,plain,
( ~ f2($false)
| ( $true = bG5 )
| spl12_14 ),
inference(superposition,[],[f127,f57]) ).
tff(f475,plain,
( $false
| ~ spl12_4
| ~ spl12_5
| ~ spl12_17
| spl12_18 ),
inference(forward_subsumption_resolution,[],[f472,f318]) ).
tff(f476,plain,
( ~ spl12_4
| ~ spl12_5
| ~ spl12_17
| spl12_18 ),
inference(avatar_contradiction_clause,[],[f475]) ).
tff(f477,plain,
( spl12_4
| spl12_28
| ~ spl12_5 ),
inference(avatar_split_clause,[],[f424,f79,f296,f73]) ).
tff(f478,plain,
( spl12_13
| ~ spl12_28
| spl12_14 ),
inference(avatar_split_clause,[],[f473,f125,f296,f119]) ).
tff(f479,plain,
( ~ f2($false)
| ( $true = bG6 )
| spl12_16 ),
inference(superposition,[],[f137,f57]) ).
tff(f480,plain,
( spl12_15
| ~ spl12_28
| spl12_16 ),
inference(avatar_split_clause,[],[f479,f135,f296,f129]) ).
tff(f491,plain,
( ~ f2($true)
| ~ spl12_13
| spl12_14 ),
inference(superposition,[],[f127,f121]) ).
tff(f493,plain,
( $false
| ~ spl12_4
| ~ spl12_5
| ~ spl12_13
| spl12_14 ),
inference(forward_subsumption_resolution,[],[f491,f318]) ).
tff(f494,plain,
( ~ spl12_4
| ~ spl12_5
| ~ spl12_13
| spl12_14 ),
inference(avatar_contradiction_clause,[],[f493]) ).
tff(f498,plain,
( ~ f2($true)
| ~ spl12_15
| spl12_16 ),
inference(superposition,[],[f137,f131]) ).
tff(f500,plain,
( $false
| ~ spl12_4
| ~ spl12_5
| ~ spl12_15
| spl12_16 ),
inference(forward_subsumption_resolution,[],[f498,f318]) ).
tff(f501,plain,
( ~ spl12_4
| ~ spl12_5
| ~ spl12_15
| spl12_16 ),
inference(avatar_contradiction_clause,[],[f500]) ).
tff(f502,plain,
( ~ f0($true)
| spl12_1
| ~ spl12_12 ),
inference(forward_demodulation,[],[f60,f115]) ).
tff(f504,plain,
( spl12_21
| ~ spl12_27
| spl12_22 ),
inference(avatar_split_clause,[],[f385,f165,f261,f159]) ).
tff(f505,plain,
( f0($false)
| ( $true = bG11 )
| ~ spl12_2 ),
inference(superposition,[],[f65,f57]) ).
tff(f506,plain,
( spl12_25
| spl12_27
| ~ spl12_2 ),
inference(avatar_split_clause,[],[f505,f63,f261,f179]) ).
tff(f509,plain,
( $false
| spl12_1
| ~ spl12_2
| ~ spl12_12
| ~ spl12_25 ),
inference(forward_subsumption_resolution,[],[f279,f502]) ).
tff(f510,plain,
( spl12_1
| ~ spl12_2
| ~ spl12_12
| ~ spl12_25 ),
inference(avatar_contradiction_clause,[],[f509]) ).
tff(f511,plain,
( $false
| spl12_1
| ~ spl12_12
| ~ spl12_21
| ~ spl12_22 ),
inference(forward_subsumption_resolution,[],[f290,f502]) ).
tff(f512,plain,
( spl12_1
| ~ spl12_12
| ~ spl12_21
| ~ spl12_22 ),
inference(avatar_contradiction_clause,[],[f511]) ).
tff(f513,plain,
( ~ f2($true)
| ~ spl12_4
| spl12_5 ),
inference(forward_demodulation,[],[f81,f75]) ).
tff(f516,plain,
( f0($false)
| ( $true = bG9 )
| ~ spl12_22 ),
inference(superposition,[],[f166,f57]) ).
tff(f517,plain,
( spl12_21
| spl12_27
| ~ spl12_22 ),
inference(avatar_split_clause,[],[f516,f165,f261,f159]) ).
tff(f519,plain,
( ~ f0($false)
| ( $true = bG10 )
| spl12_24 ),
inference(superposition,[],[f177,f57]) ).
tff(f520,plain,
( ( $true = bG10 )
| spl12_24
| ~ spl12_27 ),
inference(forward_subsumption_resolution,[],[f519,f263]) ).
tff(f521,plain,
( spl12_23
| spl12_24
| ~ spl12_27 ),
inference(avatar_split_clause,[],[f520,f261,f175,f169]) ).
tff(f527,plain,
( f1($false)
| ( $true = bG1 )
| ~ spl12_7 ),
inference(superposition,[],[f90,f57]) ).
tff(f528,plain,
( spl12_6
| spl12_26
| ~ spl12_7 ),
inference(avatar_split_clause,[],[f527,f89,f251,f83]) ).
tff(f530,plain,
( f2($false)
| ( $true = bG6 )
| ~ spl12_16 ),
inference(superposition,[],[f136,f57]) ).
tff(f531,plain,
( spl12_15
| spl12_28
| ~ spl12_16 ),
inference(avatar_split_clause,[],[f530,f135,f296,f129]) ).
tff(f532,plain,
( f2($false)
| ( $true = bG7 )
| ~ spl12_18 ),
inference(superposition,[],[f146,f57]) ).
tff(f533,plain,
( spl12_17
| spl12_28
| ~ spl12_18 ),
inference(avatar_split_clause,[],[f532,f145,f296,f139]) ).
tff(f534,plain,
( ~ f1($false)
| ( $true = bG8 )
| spl12_20 ),
inference(superposition,[],[f157,f57]) ).
tff(f535,plain,
( spl12_19
| ~ spl12_26
| spl12_20 ),
inference(avatar_split_clause,[],[f534,f155,f251,f149]) ).
tff(f536,plain,
( $false
| ~ spl12_4
| spl12_5
| ~ spl12_17
| ~ spl12_18 ),
inference(forward_subsumption_resolution,[],[f513,f458]) ).
tff(f537,plain,
( ~ spl12_4
| spl12_5
| ~ spl12_17
| ~ spl12_18 ),
inference(avatar_contradiction_clause,[],[f536]) ).
tff(f540,plain,
( ~ f0($false)
| ( $true = bG4 )
| spl12_1 ),
inference(superposition,[],[f60,f57]) ).
tff(f541,plain,
( spl12_12
| ~ spl12_27
| spl12_1 ),
inference(avatar_split_clause,[],[f540,f59,f261,f113]) ).
tff(f542,plain,
( ~ f1($false)
| ( $true = bG3 )
| spl12_11 ),
inference(superposition,[],[f111,f57]) ).
tff(f543,plain,
( spl12_10
| ~ spl12_26
| spl12_11 ),
inference(avatar_split_clause,[],[f542,f109,f251,f103]) ).
tff(f549,plain,
( ~ f2($false)
| ( $true = bG7 )
| spl12_18 ),
inference(superposition,[],[f147,f57]) ).
tff(f550,plain,
( spl12_17
| ~ spl12_28
| spl12_18 ),
inference(avatar_split_clause,[],[f549,f145,f296,f139]) ).
tff(f554,plain,
( f1($false)
| ( $true = bG8 )
| ~ spl12_20 ),
inference(superposition,[],[f156,f57]) ).
tff(f555,plain,
( spl12_19
| spl12_26
| ~ spl12_20 ),
inference(avatar_split_clause,[],[f554,f155,f251,f149]) ).
tff(f558,plain,
( ~ f1($true)
| ~ spl12_10
| spl12_11 ),
inference(superposition,[],[f111,f105]) ).
tff(f560,plain,
( $false
| ~ spl12_8
| ~ spl12_9
| ~ spl12_10
| spl12_11 ),
inference(forward_subsumption_resolution,[],[f558,f349]) ).
tff(f561,plain,
( ~ spl12_8
| ~ spl12_9
| ~ spl12_10
| spl12_11 ),
inference(avatar_contradiction_clause,[],[f560]) ).
cnf(s1,plain,
( spl12_1
| spl12_2 ),
inference(sat_conversion,[],[f66]) ).
cnf(s2,plain,
( ~ spl12_1
| ~ spl12_2 ),
inference(sat_conversion,[],[f67]) ).
cnf(s3,plain,
( ~ spl12_3
| spl12_4 ),
inference(sat_conversion,[],[f76]) ).
cnf(s4,plain,
( spl12_3
| ~ spl12_4 ),
inference(sat_conversion,[],[f77]) ).
cnf(s5,plain,
( ~ spl12_5
| spl12_6 ),
inference(sat_conversion,[],[f86]) ).
cnf(s6,plain,
( spl12_5
| ~ spl12_6 ),
inference(sat_conversion,[],[f87]) ).
cnf(s7,plain,
( ~ spl12_7
| spl12_8 ),
inference(sat_conversion,[],[f96]) ).
cnf(s8,plain,
( spl12_7
| ~ spl12_8 ),
inference(sat_conversion,[],[f97]) ).
cnf(s9,plain,
( ~ spl12_9
| spl12_10 ),
inference(sat_conversion,[],[f106]) ).
cnf(s10,plain,
( spl12_9
| ~ spl12_10 ),
inference(sat_conversion,[],[f107]) ).
cnf(s11,plain,
( ~ spl12_11
| spl12_12 ),
inference(sat_conversion,[],[f116]) ).
cnf(s12,plain,
( spl12_11
| ~ spl12_12 ),
inference(sat_conversion,[],[f117]) ).
cnf(s13,plain,
( ~ spl12_3
| spl12_13 ),
inference(sat_conversion,[],[f122]) ).
cnf(s14,plain,
( spl12_3
| ~ spl12_13 ),
inference(sat_conversion,[],[f123]) ).
cnf(s15,plain,
( ~ spl12_14
| spl12_15 ),
inference(sat_conversion,[],[f132]) ).
cnf(s16,plain,
( spl12_14
| ~ spl12_15 ),
inference(sat_conversion,[],[f133]) ).
cnf(s17,plain,
( ~ spl12_16
| spl12_17 ),
inference(sat_conversion,[],[f142]) ).
cnf(s18,plain,
( spl12_16
| ~ spl12_17 ),
inference(sat_conversion,[],[f143]) ).
cnf(s19,plain,
( ~ spl12_18
| spl12_19 ),
inference(sat_conversion,[],[f152]) ).
cnf(s20,plain,
( spl12_18
| ~ spl12_19 ),
inference(sat_conversion,[],[f153]) ).
cnf(s21,plain,
( ~ spl12_20
| spl12_21 ),
inference(sat_conversion,[],[f162]) ).
cnf(s22,plain,
( spl12_20
| ~ spl12_21 ),
inference(sat_conversion,[],[f163]) ).
cnf(s23,plain,
( ~ spl12_22
| spl12_23 ),
inference(sat_conversion,[],[f172]) ).
cnf(s24,plain,
( spl12_22
| ~ spl12_23 ),
inference(sat_conversion,[],[f173]) ).
cnf(s25,plain,
( ~ spl12_24
| spl12_25 ),
inference(sat_conversion,[],[f182]) ).
cnf(s26,plain,
( spl12_24
| ~ spl12_25 ),
inference(sat_conversion,[],[f183]) ).
cnf(s28,plain,
( spl12_1
| ~ spl12_2
| spl12_12
| spl12_25 ),
inference(sat_conversion,[],[f226]) ).
cnf(s34,plain,
( spl12_10
| ~ spl12_11
| spl12_19
| spl12_20 ),
inference(sat_conversion,[],[f249]) ).
cnf(s37,plain,
( spl12_6
| spl12_7
| ~ spl12_26 ),
inference(sat_conversion,[],[f256]) ).
cnf(s55,plain,
( spl12_13
| ~ spl12_14
| spl12_28 ),
inference(sat_conversion,[],[f306]) ).
cnf(s58,plain,
( ~ spl12_4
| spl12_5
| ~ spl12_13
| ~ spl12_14 ),
inference(sat_conversion,[],[f317]) ).
cnf(s59,plain,
( ~ spl12_6
| spl12_7
| ~ spl12_19
| ~ spl12_20 ),
inference(sat_conversion,[],[f323]) ).
cnf(s64,plain,
( spl12_23
| ~ spl12_24
| spl12_27 ),
inference(sat_conversion,[],[f334]) ).
cnf(s67,plain,
( ~ spl12_6
| ~ spl12_7
| ~ spl12_8
| spl12_9 ),
inference(sat_conversion,[],[f348]) ).
cnf(s68,plain,
( ~ spl12_6
| ~ spl12_7
| ~ spl12_10
| spl12_11 ),
inference(sat_conversion,[],[f354]) ).
cnf(s69,plain,
( spl12_2
| ~ spl12_23
| ~ spl12_24
| ~ spl12_25 ),
inference(sat_conversion,[],[f358]) ).
cnf(s77,plain,
( spl12_2
| spl12_25
| ~ spl12_27 ),
inference(sat_conversion,[],[f366]) ).
cnf(s78,plain,
( ~ spl12_1
| spl12_12
| spl12_27 ),
inference(sat_conversion,[],[f367]) ).
cnf(s79,plain,
( spl12_10
| ~ spl12_11
| spl12_26 ),
inference(sat_conversion,[],[f369]) ).
cnf(s83,plain,
( ~ spl12_1
| ~ spl12_12
| ~ spl12_23
| spl12_24 ),
inference(sat_conversion,[],[f384]) ).
cnf(s84,plain,
( spl12_4
| spl12_5
| ~ spl12_28 ),
inference(sat_conversion,[],[f388]) ).
cnf(s86,plain,
( spl12_8
| spl12_9
| ~ spl12_26 ),
inference(sat_conversion,[],[f393]) ).
cnf(s91,plain,
( ~ spl12_1
| ~ spl12_12
| ~ spl12_21
| spl12_22 ),
inference(sat_conversion,[],[f418]) ).
cnf(s95,plain,
( spl12_8
| ~ spl12_9
| spl12_26 ),
inference(sat_conversion,[],[f423]) ).
cnf(s103,plain,
( ~ spl12_15
| ~ spl12_16
| ~ spl12_17
| spl12_18 ),
inference(sat_conversion,[],[f457]) ).
cnf(s105,plain,
( ~ spl12_6
| ~ spl12_7
| ~ spl12_19
| spl12_20 ),
inference(sat_conversion,[],[f462]) ).
cnf(s107,plain,
( ~ spl12_10
| ~ spl12_11
| ~ spl12_19
| spl12_20 ),
inference(sat_conversion,[],[f470]) ).
cnf(s111,plain,
( ~ spl12_4
| ~ spl12_5
| ~ spl12_17
| spl12_18 ),
inference(sat_conversion,[],[f476]) ).
cnf(s114,plain,
( spl12_4
| ~ spl12_5
| spl12_28 ),
inference(sat_conversion,[],[f477]) ).
cnf(s115,plain,
( spl12_13
| spl12_14
| ~ spl12_28 ),
inference(sat_conversion,[],[f478]) ).
cnf(s116,plain,
( spl12_15
| spl12_16
| ~ spl12_28 ),
inference(sat_conversion,[],[f480]) ).
cnf(s118,plain,
( ~ spl12_4
| ~ spl12_5
| ~ spl12_13
| spl12_14 ),
inference(sat_conversion,[],[f494]) ).
cnf(s119,plain,
( ~ spl12_4
| ~ spl12_5
| ~ spl12_15
| spl12_16 ),
inference(sat_conversion,[],[f501]) ).
cnf(s120,plain,
( spl12_21
| spl12_22
| ~ spl12_27 ),
inference(sat_conversion,[],[f504]) ).
cnf(s121,plain,
( ~ spl12_2
| spl12_25
| spl12_27 ),
inference(sat_conversion,[],[f506]) ).
cnf(s123,plain,
( spl12_1
| ~ spl12_2
| ~ spl12_12
| ~ spl12_25 ),
inference(sat_conversion,[],[f510]) ).
cnf(s124,plain,
( spl12_1
| ~ spl12_12
| ~ spl12_21
| ~ spl12_22 ),
inference(sat_conversion,[],[f512]) ).
cnf(s130,plain,
( spl12_21
| ~ spl12_22
| spl12_27 ),
inference(sat_conversion,[],[f517]) ).
cnf(s131,plain,
( spl12_23
| spl12_24
| ~ spl12_27 ),
inference(sat_conversion,[],[f521]) ).
cnf(s133,plain,
( spl12_6
| ~ spl12_7
| spl12_26 ),
inference(sat_conversion,[],[f528]) ).
cnf(s134,plain,
( spl12_15
| ~ spl12_16
| spl12_28 ),
inference(sat_conversion,[],[f531]) ).
cnf(s135,plain,
( spl12_17
| ~ spl12_18
| spl12_28 ),
inference(sat_conversion,[],[f533]) ).
cnf(s136,plain,
( spl12_19
| spl12_20
| ~ spl12_26 ),
inference(sat_conversion,[],[f535]) ).
cnf(s137,plain,
( ~ spl12_4
| spl12_5
| ~ spl12_17
| ~ spl12_18 ),
inference(sat_conversion,[],[f537]) ).
cnf(s139,plain,
( spl12_1
| spl12_12
| ~ spl12_27 ),
inference(sat_conversion,[],[f541]) ).
cnf(s140,plain,
( spl12_10
| spl12_11
| ~ spl12_26 ),
inference(sat_conversion,[],[f543]) ).
cnf(s143,plain,
( spl12_17
| spl12_18
| ~ spl12_28 ),
inference(sat_conversion,[],[f550]) ).
cnf(s144,plain,
( spl12_19
| ~ spl12_20
| spl12_26 ),
inference(sat_conversion,[],[f555]) ).
cnf(s145,plain,
( ~ spl12_8
| ~ spl12_9
| ~ spl12_10
| spl12_11 ),
inference(sat_conversion,[],[f561]) ).
cnf(s146,plain,
( spl12_7
| spl12_19
| spl12_6
| spl12_1 ),
inference(rat,[],[s64,s24,s26,s130,s28,s139,s12,s34,s10,s22,s95,s144,s8,s37,s1]) ).
cnf(s147,plain,
( ~ spl12_12
| ~ spl12_21
| spl12_1 ),
inference(rat,[],[s131,s24,s25,s121,s124,s123,s1]) ).
cnf(s148,plain,
( spl12_19
| spl12_6
| spl12_1 ),
inference(rat,[],[s145,s10,s140,s11,s147,s21,s136,s7,s133,s146]) ).
cnf(s149,plain,
( spl12_5
| spl12_3
| spl12_1 ),
inference(rat,[],[s148,s20,s135,s18,s134,s16,s55,s6,s84,s14,s4]) ).
cnf(s150,plain,
( spl12_18
| ~ spl12_15
| ~ spl12_28 ),
inference(rat,[],[s103,s18,s143]) ).
cnf(s151,plain,
( ~ spl12_8
| spl12_9
| ~ spl12_6 ),
inference(rat,[],[s67,s8]) ).
cnf(s152,plain,
( spl12_10
| spl12_3
| spl12_1 ),
inference(rat,[],[s64,s24,s26,s130,s28,s139,s22,s12,s59,s79,s7,s86,s151,s9,s1,s5,s19,s150,s15,s115,s14,s114,s149,s4]) ).
cnf(s153,plain,
( ~ spl12_11
| spl12_3
| spl12_1 ),
inference(rat,[],[s21,s147,s107,s11,s19,s150,s15,s115,s14,s114,s149,s4,s152]) ).
cnf(s154,plain,
( spl12_3
| spl12_1 ),
inference(rat,[],[s24,s130,s64,s22,s26,s59,s28,s139,s68,s12,s153,s152,s19,s150,s15,s115,s114,s5,s149,s4,s14,s1]) ).
cnf(s155,plain,
( spl12_19
| spl12_1 ),
inference(rat,[],[s119,s17,s15,s111,s118,s6,s148,s19,s13,s3,s154]) ).
cnf(s156,plain,
( spl12_5
| spl12_1 ),
inference(rat,[],[s116,s16,s17,s135,s58,s137,s13,s3,s154,s20,s155]) ).
cnf(s157,plain,
( spl12_10
| spl12_1 ),
inference(rat,[],[s64,s24,s26,s130,s28,s139,s22,s12,s59,s79,s7,s86,s151,s9,s1,s155,s5,s156]) ).
cnf(s158,plain,
( ~ spl12_11
| spl12_1 ),
inference(rat,[],[s21,s147,s107,s11,s155,s157]) ).
cnf(s159,plain,
spl12_1,
inference(rat,[],[s24,s130,s64,s22,s26,s59,s28,s139,s68,s12,s158,s157,s5,s156,s155,s1]) ).
cnf(s160,plain,
~ spl12_2,
inference(rat,[],[s2,s159]) ).
cnf(s161,plain,
( ~ spl12_23
| ~ spl12_12 ),
inference(rat,[],[s69,s25,s83,s159,s160]) ).
cnf(s162,plain,
( ~ spl12_21
| ~ spl12_12 ),
inference(rat,[],[s161,s23,s91,s159]) ).
cnf(s163,plain,
( ~ spl12_11
| spl12_10
| spl12_19 ),
inference(rat,[],[s162,s21,s34,s11]) ).
cnf(s164,plain,
( spl12_10
| spl12_19 ),
inference(rat,[],[s69,s23,s26,s120,s77,s22,s78,s144,s12,s140,s163,s159,s160]) ).
cnf(s165,plain,
( spl12_26
| spl12_6
| ~ spl12_9 ),
inference(rat,[],[s8,s95,s133]) ).
cnf(s166,plain,
( spl12_6
| spl12_19 ),
inference(rat,[],[s11,s145,s162,s7,s21,s37,s136,s165,s10,s164]) ).
cnf(s167,plain,
( spl12_3
| spl12_19 ),
inference(rat,[],[s15,s150,s115,s114,s4,s14,s19,s6,s166]) ).
cnf(s168,plain,
spl12_19,
inference(rat,[],[s119,s17,s15,s111,s118,s3,s13,s167,s6,s166,s19]) ).
cnf(s169,plain,
spl12_18,
inference(rat,[],[s20,s168]) ).
cnf(s170,plain,
( ~ spl12_10
| ~ spl12_21 ),
inference(rat,[],[s37,s59,s7,s95,s145,s10,s22,s11,s162,s168]) ).
cnf(s171,plain,
( ~ spl12_6
| ~ spl12_21 ),
inference(rat,[],[s7,s151,s59,s22,s9,s170,s168]) ).
cnf(s172,plain,
( spl12_28
| spl12_13 ),
inference(rat,[],[s134,s18,s16,s135,s55,s169]) ).
cnf(s173,plain,
( spl12_3
| spl12_5 ),
inference(rat,[],[s172,s84,s4,s14]) ).
cnf(s174,plain,
spl12_5,
inference(rat,[],[s116,s16,s17,s135,s58,s137,s3,s13,s173,s169]) ).
cnf(s175,plain,
spl12_6,
inference(rat,[],[s5,s174]) ).
cnf(s176,plain,
~ spl12_21,
inference(rat,[],[s171,s175]) ).
cnf(s177,plain,
~ spl12_20,
inference(rat,[],[s21,s176]) ).
cnf(s178,plain,
~ spl12_7,
inference(rat,[],[s105,s168,s175,s177]) ).
cnf(s179,plain,
~ spl12_8,
inference(rat,[],[s8,s178]) ).
cnf(s180,plain,
~ spl12_27,
inference(rat,[],[s69,s23,s26,s120,s77,s160,s176]) ).
cnf(s181,plain,
spl12_12,
inference(rat,[],[s78,s159,s180]) ).
cnf(s183,plain,
spl12_11,
inference(rat,[],[s12,s181]) ).
cnf(s185,plain,
~ spl12_10,
inference(rat,[],[s107,s177,s168,s183]) ).
cnf(s187,plain,
~ spl12_9,
inference(rat,[],[s9,s185]) ).
cnf(s188,plain,
spl12_26,
inference(rat,[],[s79,s183,s185]) ).
cnf(s190,plain,
$false,
inference(rat,[],[s86,s179,s187,s188]) ).
tff(f562,plain,
$false,
inference(avatar_sat_refutation,[],[s190]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500_8.003 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.19 % Computer : n016.cluster.edu
% 0.13/0.19 % Model : x86_64 x86_64
% 0.13/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.19 % Memory : 8046.5625MB
% 0.13/0.19 % OS : Linux 6.8.0-71-generic
% 0.13/0.19 % CPULimit : 300
% 0.13/0.19 % WCLimit : 300
% 0.13/0.19 % DateTime : Mon Sep 28 17:51:18 UTC 2026
% 0.13/0.20 % CPUTime :
% 0.13/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.23 Running first-order theorem proving
% 0.13/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.80/0.73 % (3834139)Detected formulas, will run a generic FOF schedule.
% 1.80/0.73 % (3834220)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3818407588:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.80/0.73 % (3834220)First to succeed.
% 1.80/0.73 % (3834220)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3834139"
% 1.80/0.73 % (3834216)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=1484498030:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.80/0.73 % (3834217)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1577129437:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.80/0.73 % (3834214)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=1099919991:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.80/0.73 % (3834221)dis-21_1_sil=8000:lcm=predicate:random_seed=1490357814: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)
% 1.80/0.73 % (3834217)Refutation not found, incomplete strategy
% 1.80/0.73 % (3834217)------------------------------
% 1.80/0.73 % (3834217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.80/0.73 % (3834217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.80/0.73 % (3834217)CaDiCaL version: 2.1.3
% 1.80/0.73 % (3834217)Termination reason: Refutation not found, incomplete strategy
% 1.80/0.73 % (3834217)Time elapsed: 0.002 s
% 1.80/0.73 % (3834217)Peak memory usage: 88 MB
% 1.80/0.73 % (3834217)Instructions burned: 1 (million)
% 1.80/0.73 % (3834221)Refutation not found, incomplete strategy
% 1.80/0.73 % (3834221)------------------------------
% 1.80/0.73 % (3834221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.80/0.73 % (3834221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.80/0.73 % (3834221)CaDiCaL version: 2.1.3
% 1.80/0.73 % (3834221)Termination reason: Refutation not found, incomplete strategy
% 1.80/0.73 % (3834221)Time elapsed: 0.002 s
% 1.80/0.73 % (3834221)Peak memory usage: 88 MB
% 1.80/0.73 % (3834221)Instructions burned: 2 (million)
% 1.80/0.73 % (3834215)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=2862417370:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.80/0.73 % (3834219)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1495047380:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.80/0.73 % (3834219)Instruction limit reached!
% 1.80/0.73 % (3834219)------------------------------
% 1.80/0.73 % (3834219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.80/0.73 % (3834219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.80/0.73 % (3834219)CaDiCaL version: 2.1.3
% 1.80/0.73 % (3834219)Termination reason: Instruction limit
% 1.80/0.73 % (3834219)Termination phase: Saturation
% 1.80/0.73 % (3834219)Time elapsed: 0.068 s
% 1.80/0.73 % (3834219)Peak memory usage: 88 MB
% 1.80/0.73 % (3834219)Instructions burned: 120 (million)
% 1.80/0.73 % (3834220)Refutation found. Thanks to Tanya!
% 1.80/0.73 % SZS status Theorem for theBenchmark
% 1.80/0.73 % SZS output start Proof for theBenchmark
% See solution above
% 2.36/0.84 % (3834220)------------------------------
% 2.36/0.84 % (3834220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.36/0.84 % (3834220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.84 % (3834220)CaDiCaL version: 2.1.3
% 2.36/0.84 % (3834220)Termination reason: Refutation
% 2.36/0.84 % (3834220)Time elapsed: 0.008 s
% 2.36/0.84 % (3834220)Peak memory usage: 90 MB
% 2.36/0.84 % (3834220)Instructions burned: 18 (million)
% 2.36/0.84 % (3834220)------------------------------
% 2.36/0.84 % (3834220)------------------------------
% 2.36/0.84 % (3834139)Success in time 0.293 s
% 2.36/0.84 % Vampire exiting
%------------------------------------------------------------------------------