%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO500_8.002 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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:31:20 PM UTC 2026
% Result : Theorem 0.28s 0.36s
% Output : Refutation 0.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SYO500_8.002 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.26 % Computer : n020.cluster.edu
% 0.10/0.26 % Model : x86_64 x86_64
% 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.26 % Memory : 8046.5625MB
% 0.10/0.26 % OS : Linux 6.8.0-71-generic
% 0.10/0.26 % CPULimit : 300
% 0.10/0.26 % WCLimit : 300
% 0.10/0.26 % DateTime : Mon Sep 28 17:47:19 UTC 2026
% 0.10/0.27 % CPUTime :
% 0.10/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.28/0.31 Running first-order model finding
% 0.28/0.31 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.28/0.36 % (370476)Will run a generic schedule for satisfiability detection.
% 0.28/0.36 % (370484)dis+10_1_sil=32000:sp=arity:random_seed=82991163:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 0.28/0.36 % (370482)% WARNING: option uhcvi not known.
% 0.28/0.36 % (370484) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-370476-370484"...
% 0.28/0.36 % (370484)...printing done.
% 0.28/0.36 % (370487)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1586037339:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 0.28/0.36 % (370481)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=594576636_3000 on theBenchmark for (3000ds/0Mi)
% 0.28/0.36 % (370482)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2016499202:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 0.28/0.36 % (370483)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4063760537:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 0.28/0.36 % (370485)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=268658558:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 0.28/0.36 % (370486)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4255693023:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 0.28/0.36 % Detected minimum model sizes of [1]
% 0.28/0.36 % Detected maximum model sizes of [10]
% 0.28/0.36 % TRYING [1]
% 0.28/0.36 % (370482) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-370476-370482"...
% 0.28/0.36 % (370484)Refutation found. Thanks to Tanya!
% 0.28/0.36 % SZS status Theorem for theBenchmark
% 0.28/0.36 % SZS output start Proof for theBenchmark
% 0.28/0.36 tff(func_def_0, type, bG0: $o).
% 0.28/0.36 tff(func_def_3, type, bG1: $o).
% 0.28/0.36 tff(func_def_4, type, bG2: $o).
% 0.28/0.36 tff(func_def_5, type, bG3: $o).
% 0.28/0.36 tff(func_def_6, type, bG4: $o).
% 0.28/0.36 tff(func_def_7, type, bG5: $o).
% 0.28/0.36 tff(func_def_8, type, bG6: $o).
% 0.28/0.36 tff(func_def_9, type, bG7: $o).
% 0.28/0.36 tff(pred_def_2, type, f0: $o > $o).
% 0.28/0.36 tff(pred_def_3, type, f1: $o > $o).
% 0.28/0.36 tff(f1,conjecture,(
% 0.28/0.36 (f0(f0(f0(f1(x)))) = f0(f1(f1(f1(x)))))),
% 0.28/0.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',kaminski2)).
% 0.28/0.36 tff(f2,negated_conjecture,(
% 0.28/0.36 ~ (f0(f0(f0(f1(x)))) = f0(f1(f1(f1(x)))))),
% 0.28/0.36 inference(negated_conjecture,[status(cth)],[f1])).
% 0.28/0.36 tff(f3,definition,(
% 0.28/0.36 x <=> (bG0 = $true)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[bG0])],[fool_formula_definition])).
% 0.28/0.36 tff(f4,definition,(
% 0.28/0.36 f1(bG0) <=> ($true = bG1)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[bG1])],[fool_formula_definition])).
% 0.28/0.36 tff(f5,definition,(
% 0.28/0.36 f0(bG1) <=> ($true = bG2)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[bG2])],[fool_formula_definition])).
% 0.28/0.36 tff(f6,definition,(
% 0.28/0.36 f0(bG2) <=> ($true = bG3)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[bG3])],[fool_formula_definition])).
% 0.28/0.36 tff(f7,definition,(
% 0.28/0.36 x <=> ($true = bG4)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[bG4])],[fool_formula_definition])).
% 0.28/0.36 tff(f8,definition,(
% 0.28/0.36 f1(bG4) <=> ($true = bG5)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[bG5])],[fool_formula_definition])).
% 0.28/0.36 tff(f9,definition,(
% 0.28/0.36 f1(bG5) <=> ($true = bG6)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[bG6])],[fool_formula_definition])).
% 0.28/0.36 tff(f10,definition,(
% 0.28/0.36 f1(bG6) <=> ($true = bG7)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[bG7])],[fool_formula_definition])).
% 0.28/0.36 tff(f11,plain,(
% 0.28/0.36 ~(f0(bG3) <=> f0(bG7))),
% 0.28/0.36 inference(fool_elimination,[],[f2,f10,f9,f8,f7,f6,f5,f4,f3])).
% 0.28/0.36 tff(f12,plain,(
% 0.28/0.36 f0(bG3) <~> f0(bG7)),
% 0.28/0.36 inference(ennf_transformation,[],[f11])).
% 0.28/0.36 tff(f13,plain,(
% 0.28/0.36 (f1(bG6) | ($true != bG7)) & (($true = bG7) | ~f1(bG6))),
% 0.28/0.36 inference(nnf_transformation,[],[f10])).
% 0.28/0.36 tff(f14,plain,(
% 0.28/0.36 (f1(bG5) | ($true != bG6)) & (($true = bG6) | ~f1(bG5))),
% 0.28/0.36 inference(nnf_transformation,[],[f9])).
% 0.28/0.36 tff(f15,plain,(
% 0.28/0.36 (f1(bG4) | ($true != bG5)) & (($true = bG5) | ~f1(bG4))),
% 0.28/0.36 inference(nnf_transformation,[],[f8])).
% 0.28/0.36 tff(f16,plain,(
% 0.28/0.36 (x | ($true != bG4)) & (($true = bG4) | ~x)),
% 0.28/0.36 inference(nnf_transformation,[],[f7])).
% 0.28/0.36 tff(f17,plain,(
% 0.28/0.36 (f0(bG2) | ($true != bG3)) & (($true = bG3) | ~f0(bG2))),
% 0.28/0.36 inference(nnf_transformation,[],[f6])).
% 0.28/0.36 tff(f18,plain,(
% 0.28/0.36 (f0(bG1) | ($true != bG2)) & (($true = bG2) | ~f0(bG1))),
% 0.28/0.36 inference(nnf_transformation,[],[f5])).
% 0.28/0.36 tff(f19,plain,(
% 0.28/0.36 (f1(bG0) | ($true != bG1)) & (($true = bG1) | ~f1(bG0))),
% 0.28/0.36 inference(nnf_transformation,[],[f4])).
% 0.28/0.36 tff(f20,plain,(
% 0.28/0.36 (x | (bG0 != $true)) & ((bG0 = $true) | ~x)),
% 0.28/0.36 inference(nnf_transformation,[],[f3])).
% 0.28/0.36 tff(f21,plain,(
% 0.28/0.36 (~f0(bG7) | ~f0(bG3)) & (f0(bG7) | f0(bG3))),
% 0.28/0.36 inference(nnf_transformation,[],[f12])).
% 0.28/0.36 tff(f22,plain,(
% 0.28/0.36 ($true = bG7) | ~f1(bG6)),
% 0.28/0.36 inference(cnf_transformation,[],[f13])).
% 0.28/0.36 tff(f23,plain,(
% 0.28/0.36 f1(bG6) | ($true != bG7)),
% 0.28/0.36 inference(cnf_transformation,[],[f13])).
% 0.28/0.36 tff(f24,plain,(
% 0.28/0.36 ($true = bG6) | ~f1(bG5)),
% 0.28/0.36 inference(cnf_transformation,[],[f14])).
% 0.28/0.36 tff(f25,plain,(
% 0.28/0.36 f1(bG5) | ($true != bG6)),
% 0.28/0.36 inference(cnf_transformation,[],[f14])).
% 0.28/0.36 tff(f26,plain,(
% 0.28/0.36 ($true = bG5) | ~f1(bG4)),
% 0.28/0.36 inference(cnf_transformation,[],[f15])).
% 0.28/0.36 tff(f27,plain,(
% 0.28/0.36 f1(bG4) | ($true != bG5)),
% 0.28/0.36 inference(cnf_transformation,[],[f15])).
% 0.28/0.36 tff(f28,plain,(
% 0.28/0.36 ($true = bG4) | ~x),
% 0.28/0.36 inference(cnf_transformation,[],[f16])).
% 0.28/0.36 tff(f29,plain,(
% 0.28/0.36 x | ($true != bG4)),
% 0.28/0.36 inference(cnf_transformation,[],[f16])).
% 0.28/0.36 tff(f30,plain,(
% 0.28/0.36 ($true = bG3) | ~f0(bG2)),
% 0.28/0.36 inference(cnf_transformation,[],[f17])).
% 0.28/0.36 tff(f31,plain,(
% 0.28/0.36 f0(bG2) | ($true != bG3)),
% 0.28/0.36 inference(cnf_transformation,[],[f17])).
% 0.28/0.36 tff(f32,plain,(
% 0.28/0.36 ($true = bG2) | ~f0(bG1)),
% 0.28/0.36 inference(cnf_transformation,[],[f18])).
% 0.28/0.36 tff(f33,plain,(
% 0.28/0.36 f0(bG1) | ($true != bG2)),
% 0.28/0.36 inference(cnf_transformation,[],[f18])).
% 0.28/0.36 tff(f34,plain,(
% 0.28/0.36 ($true = bG1) | ~f1(bG0)),
% 0.28/0.36 inference(cnf_transformation,[],[f19])).
% 0.28/0.36 tff(f35,plain,(
% 0.28/0.36 f1(bG0) | ($true != bG1)),
% 0.28/0.36 inference(cnf_transformation,[],[f19])).
% 0.28/0.36 tff(f36,plain,(
% 0.28/0.36 (bG0 = $true) | ~x),
% 0.28/0.36 inference(cnf_transformation,[],[f20])).
% 0.28/0.36 tff(f37,plain,(
% 0.28/0.36 x | (bG0 != $true)),
% 0.28/0.36 inference(cnf_transformation,[],[f20])).
% 0.28/0.36 tff(f38,plain,(
% 0.28/0.36 f0(bG7) | f0(bG3)),
% 0.28/0.36 inference(cnf_transformation,[],[f21])).
% 0.28/0.36 tff(f39,plain,(
% 0.28/0.36 ~f0(bG7) | ~f0(bG3)),
% 0.28/0.36 inference(cnf_transformation,[],[f21])).
% 0.28/0.36 tff(f41,definition,(
% 0.28/0.36 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.28/0.36 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.28/0.36 tff(f43,definition,(
% 0.28/0.36 spl8_1 <=> f0(bG3)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition])).
% 0.28/0.36 tff(f44,plain,(
% 0.28/0.36 ~f0(bG3) | spl8_1),
% 0.28/0.36 inference(avatar_component_clause,[],[f43])).
% 0.28/0.36 tff(f45,plain,(
% 0.28/0.36 f0(bG3) | ~spl8_1),
% 0.28/0.36 inference(avatar_component_clause,[],[f43])).
% 0.28/0.36 tff(f47,definition,(
% 0.28/0.36 spl8_2 <=> f0(bG7)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition])).
% 0.28/0.36 tff(f48,plain,(
% 0.28/0.36 ~f0(bG7) | spl8_2),
% 0.28/0.36 inference(avatar_component_clause,[],[f47])).
% 0.28/0.36 tff(f49,plain,(
% 0.28/0.36 f0(bG7) | ~spl8_2),
% 0.28/0.36 inference(avatar_component_clause,[],[f47])).
% 0.28/0.36 tff(f50,plain,(
% 0.28/0.36 spl8_1 | spl8_2),
% 0.28/0.36 inference(avatar_split_clause,[],[f38,f47,f43])).
% 0.28/0.36 tff(f51,plain,(
% 0.28/0.36 ~spl8_1 | ~spl8_2),
% 0.28/0.36 inference(avatar_split_clause,[],[f39,f47,f43])).
% 0.28/0.36 tff(f53,definition,(
% 0.28/0.36 spl8_3 <=> x),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition])).
% 0.28/0.36 tff(f57,definition,(
% 0.28/0.36 spl8_4 <=> (bG0 = $true)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_4])],[avatar_definition])).
% 0.28/0.36 tff(f58,plain,(
% 0.28/0.36 (bG0 != $true) | spl8_4),
% 0.28/0.36 inference(avatar_component_clause,[],[f57])).
% 0.28/0.36 tff(f59,plain,(
% 0.28/0.36 (bG0 = $true) | ~spl8_4),
% 0.28/0.36 inference(avatar_component_clause,[],[f57])).
% 0.28/0.36 tff(f60,plain,(
% 0.28/0.36 ~spl8_3 | spl8_4),
% 0.28/0.36 inference(avatar_split_clause,[],[f36,f57,f53])).
% 0.28/0.36 tff(f61,plain,(
% 0.28/0.36 ~spl8_4 | spl8_3),
% 0.28/0.36 inference(avatar_split_clause,[],[f37,f53,f57])).
% 0.28/0.36 tff(f63,definition,(
% 0.28/0.36 spl8_5 <=> f1(bG0)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition])).
% 0.28/0.36 tff(f64,plain,(
% 0.28/0.36 f1(bG0) | ~spl8_5),
% 0.28/0.36 inference(avatar_component_clause,[],[f63])).
% 0.28/0.36 tff(f65,plain,(
% 0.28/0.36 ~f1(bG0) | spl8_5),
% 0.28/0.36 inference(avatar_component_clause,[],[f63])).
% 0.28/0.36 tff(f67,definition,(
% 0.28/0.36 spl8_6 <=> ($true = bG1)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition])).
% 0.28/0.36 tff(f68,plain,(
% 0.28/0.36 ($true != bG1) | spl8_6),
% 0.28/0.36 inference(avatar_component_clause,[],[f67])).
% 0.28/0.36 tff(f69,plain,(
% 0.28/0.36 ($true = bG1) | ~spl8_6),
% 0.28/0.36 inference(avatar_component_clause,[],[f67])).
% 0.28/0.36 tff(f70,plain,(
% 0.28/0.36 ~spl8_5 | spl8_6),
% 0.28/0.36 inference(avatar_split_clause,[],[f34,f67,f63])).
% 0.28/0.36 tff(f71,plain,(
% 0.28/0.36 ~spl8_6 | spl8_5),
% 0.28/0.36 inference(avatar_split_clause,[],[f35,f63,f67])).
% 0.28/0.36 tff(f73,definition,(
% 0.28/0.36 spl8_7 <=> f0(bG1)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_7])],[avatar_definition])).
% 0.28/0.36 tff(f74,plain,(
% 0.28/0.36 f0(bG1) | ~spl8_7),
% 0.28/0.36 inference(avatar_component_clause,[],[f73])).
% 0.28/0.36 tff(f75,plain,(
% 0.28/0.36 ~f0(bG1) | spl8_7),
% 0.28/0.36 inference(avatar_component_clause,[],[f73])).
% 0.28/0.36 tff(f77,definition,(
% 0.28/0.36 spl8_8 <=> ($true = bG2)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_8])],[avatar_definition])).
% 0.28/0.36 tff(f78,plain,(
% 0.28/0.36 ($true != bG2) | spl8_8),
% 0.28/0.36 inference(avatar_component_clause,[],[f77])).
% 0.28/0.36 tff(f79,plain,(
% 0.28/0.36 ($true = bG2) | ~spl8_8),
% 0.28/0.36 inference(avatar_component_clause,[],[f77])).
% 0.28/0.36 tff(f80,plain,(
% 0.28/0.36 ~spl8_7 | spl8_8),
% 0.28/0.36 inference(avatar_split_clause,[],[f32,f77,f73])).
% 0.28/0.36 tff(f81,plain,(
% 0.28/0.36 ~spl8_8 | spl8_7),
% 0.28/0.36 inference(avatar_split_clause,[],[f33,f73,f77])).
% 0.28/0.36 tff(f83,definition,(
% 0.28/0.36 spl8_9 <=> f0(bG2)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_9])],[avatar_definition])).
% 0.28/0.36 tff(f84,plain,(
% 0.28/0.36 f0(bG2) | ~spl8_9),
% 0.28/0.36 inference(avatar_component_clause,[],[f83])).
% 0.28/0.36 tff(f85,plain,(
% 0.28/0.36 ~f0(bG2) | spl8_9),
% 0.28/0.36 inference(avatar_component_clause,[],[f83])).
% 0.28/0.36 tff(f87,definition,(
% 0.28/0.36 spl8_10 <=> ($true = bG3)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_10])],[avatar_definition])).
% 0.28/0.36 tff(f88,plain,(
% 0.28/0.36 ($true != bG3) | spl8_10),
% 0.28/0.36 inference(avatar_component_clause,[],[f87])).
% 0.28/0.36 tff(f89,plain,(
% 0.28/0.36 ($true = bG3) | ~spl8_10),
% 0.28/0.36 inference(avatar_component_clause,[],[f87])).
% 0.28/0.36 tff(f90,plain,(
% 0.28/0.36 ~spl8_9 | spl8_10),
% 0.28/0.36 inference(avatar_split_clause,[],[f30,f87,f83])).
% 0.28/0.36 tff(f91,plain,(
% 0.28/0.36 ~spl8_10 | spl8_9),
% 0.28/0.36 inference(avatar_split_clause,[],[f31,f83,f87])).
% 0.28/0.36 tff(f93,definition,(
% 0.28/0.36 spl8_11 <=> ($true = bG4)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_11])],[avatar_definition])).
% 0.28/0.36 tff(f94,plain,(
% 0.28/0.36 ($true != bG4) | spl8_11),
% 0.28/0.36 inference(avatar_component_clause,[],[f93])).
% 0.28/0.36 tff(f95,plain,(
% 0.28/0.36 ($true = bG4) | ~spl8_11),
% 0.28/0.36 inference(avatar_component_clause,[],[f93])).
% 0.28/0.36 tff(f96,plain,(
% 0.28/0.36 ~spl8_3 | spl8_11),
% 0.28/0.36 inference(avatar_split_clause,[],[f28,f93,f53])).
% 0.28/0.36 tff(f97,plain,(
% 0.28/0.36 ~spl8_11 | spl8_3),
% 0.28/0.36 inference(avatar_split_clause,[],[f29,f53,f93])).
% 0.28/0.36 tff(f99,definition,(
% 0.28/0.36 spl8_12 <=> f1(bG4)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_12])],[avatar_definition])).
% 0.28/0.36 tff(f100,plain,(
% 0.28/0.36 f1(bG4) | ~spl8_12),
% 0.28/0.36 inference(avatar_component_clause,[],[f99])).
% 0.28/0.36 tff(f101,plain,(
% 0.28/0.36 ~f1(bG4) | spl8_12),
% 0.28/0.36 inference(avatar_component_clause,[],[f99])).
% 0.28/0.36 tff(f103,definition,(
% 0.28/0.36 spl8_13 <=> ($true = bG5)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_13])],[avatar_definition])).
% 0.28/0.36 tff(f104,plain,(
% 0.28/0.36 ($true != bG5) | spl8_13),
% 0.28/0.36 inference(avatar_component_clause,[],[f103])).
% 0.28/0.36 tff(f105,plain,(
% 0.28/0.36 ($true = bG5) | ~spl8_13),
% 0.28/0.36 inference(avatar_component_clause,[],[f103])).
% 0.28/0.36 tff(f106,plain,(
% 0.28/0.36 ~spl8_12 | spl8_13),
% 0.28/0.36 inference(avatar_split_clause,[],[f26,f103,f99])).
% 0.28/0.36 tff(f107,plain,(
% 0.28/0.36 ~spl8_13 | spl8_12),
% 0.28/0.36 inference(avatar_split_clause,[],[f27,f99,f103])).
% 0.28/0.36 tff(f109,definition,(
% 0.28/0.36 spl8_14 <=> f1(bG5)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_14])],[avatar_definition])).
% 0.28/0.36 tff(f110,plain,(
% 0.28/0.36 f1(bG5) | ~spl8_14),
% 0.28/0.36 inference(avatar_component_clause,[],[f109])).
% 0.28/0.36 tff(f111,plain,(
% 0.28/0.36 ~f1(bG5) | spl8_14),
% 0.28/0.36 inference(avatar_component_clause,[],[f109])).
% 0.28/0.36 tff(f113,definition,(
% 0.28/0.36 spl8_15 <=> ($true = bG6)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_15])],[avatar_definition])).
% 0.28/0.36 tff(f114,plain,(
% 0.28/0.36 ($true != bG6) | spl8_15),
% 0.28/0.36 inference(avatar_component_clause,[],[f113])).
% 0.28/0.36 tff(f115,plain,(
% 0.28/0.36 ($true = bG6) | ~spl8_15),
% 0.28/0.36 inference(avatar_component_clause,[],[f113])).
% 0.28/0.36 tff(f116,plain,(
% 0.28/0.36 ~spl8_14 | spl8_15),
% 0.28/0.36 inference(avatar_split_clause,[],[f24,f113,f109])).
% 0.28/0.36 tff(f117,plain,(
% 0.28/0.36 ~spl8_15 | spl8_14),
% 0.28/0.36 inference(avatar_split_clause,[],[f25,f109,f113])).
% 0.28/0.36 tff(f119,definition,(
% 0.28/0.36 spl8_16 <=> f1(bG6)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_16])],[avatar_definition])).
% 0.28/0.36 tff(f120,plain,(
% 0.28/0.36 f1(bG6) | ~spl8_16),
% 0.28/0.36 inference(avatar_component_clause,[],[f119])).
% 0.28/0.36 tff(f121,plain,(
% 0.28/0.36 ~f1(bG6) | spl8_16),
% 0.28/0.36 inference(avatar_component_clause,[],[f119])).
% 0.28/0.36 tff(f123,definition,(
% 0.28/0.36 spl8_17 <=> ($true = bG7)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_17])],[avatar_definition])).
% 0.28/0.36 tff(f124,plain,(
% 0.28/0.36 ($true != bG7) | spl8_17),
% 0.28/0.36 inference(avatar_component_clause,[],[f123])).
% 0.28/0.36 tff(f125,plain,(
% 0.28/0.36 ($true = bG7) | ~spl8_17),
% 0.28/0.36 inference(avatar_component_clause,[],[f123])).
% 0.28/0.36 tff(f126,plain,(
% 0.28/0.36 ~spl8_16 | spl8_17),
% 0.28/0.36 inference(avatar_split_clause,[],[f22,f123,f119])).
% 0.28/0.36 tff(f127,plain,(
% 0.28/0.36 ~spl8_17 | spl8_16),
% 0.28/0.36 inference(avatar_split_clause,[],[f23,f119,f123])).
% 0.28/0.36 tff(f130,plain,(
% 0.28/0.36 ($true != $true) | (bG0 = $false) | spl8_4),
% 0.28/0.36 inference(superposition,[],[f58,f41])).
% 0.28/0.36 tff(f132,plain,(
% 0.28/0.36 ($true != $true) | (bG1 = $false) | spl8_6),
% 0.28/0.36 inference(superposition,[],[f68,f41])).
% 0.28/0.36 tff(f134,plain,(
% 0.28/0.36 ($true != $true) | (bG2 = $false) | spl8_8),
% 0.28/0.36 inference(superposition,[],[f78,f41])).
% 0.28/0.36 tff(f136,plain,(
% 0.28/0.36 ($true != $true) | (bG3 = $false) | spl8_10),
% 0.28/0.36 inference(superposition,[],[f88,f41])).
% 0.28/0.36 tff(f138,plain,(
% 0.28/0.36 ($true != $true) | (bG4 = $false) | spl8_11),
% 0.28/0.36 inference(superposition,[],[f94,f41])).
% 0.28/0.36 tff(f140,plain,(
% 0.28/0.36 ($true != $true) | (bG5 = $false) | spl8_13),
% 0.28/0.36 inference(superposition,[],[f104,f41])).
% 0.28/0.36 tff(f142,plain,(
% 0.28/0.36 ($true != $true) | (bG6 = $false) | spl8_15),
% 0.28/0.36 inference(superposition,[],[f114,f41])).
% 0.28/0.36 tff(f143,plain,(
% 0.28/0.36 ~f1($true) | (bG6 = $false) | spl8_16),
% 0.28/0.36 inference(superposition,[],[f121,f41])).
% 0.28/0.36 tff(f144,plain,(
% 0.28/0.36 ($true != $true) | (bG7 = $false) | spl8_17),
% 0.28/0.36 inference(superposition,[],[f124,f41])).
% 0.28/0.36 tff(f147,plain,(
% 0.28/0.36 (bG7 = $false) | spl8_17),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f144])).
% 0.28/0.36 tff(f148,plain,(
% 0.28/0.36 (bG6 = $false) | spl8_15),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f142])).
% 0.28/0.36 tff(f149,plain,(
% 0.28/0.36 (bG5 = $false) | spl8_13),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f140])).
% 0.28/0.36 tff(f150,plain,(
% 0.28/0.36 (bG4 = $false) | spl8_11),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f138])).
% 0.28/0.36 tff(f151,plain,(
% 0.28/0.36 (bG3 = $false) | spl8_10),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f136])).
% 0.28/0.36 tff(f152,plain,(
% 0.28/0.36 (bG2 = $false) | spl8_8),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f134])).
% 0.28/0.36 tff(f153,plain,(
% 0.28/0.36 (bG1 = $false) | spl8_6),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f132])).
% 0.28/0.36 tff(f154,plain,(
% 0.28/0.36 (bG0 = $false) | spl8_4),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f130])).
% 0.28/0.36 tff(f156,definition,(
% 0.28/0.36 spl8_18 <=> (bG7 = $false)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_18])],[avatar_definition])).
% 0.28/0.36 tff(f158,plain,(
% 0.28/0.36 (bG7 = $false) | ~spl8_18),
% 0.28/0.36 inference(avatar_component_clause,[],[f156])).
% 0.28/0.36 tff(f160,definition,(
% 0.28/0.36 spl8_19 <=> f0($true)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_19])],[avatar_definition])).
% 0.28/0.36 tff(f161,plain,(
% 0.28/0.36 ~f0($true) | spl8_19),
% 0.28/0.36 inference(avatar_component_clause,[],[f160])).
% 0.28/0.36 tff(f162,plain,(
% 0.28/0.36 f0($true) | ~spl8_19),
% 0.28/0.36 inference(avatar_component_clause,[],[f160])).
% 0.28/0.36 tff(f164,plain,(
% 0.28/0.36 spl8_18 | spl8_17),
% 0.28/0.36 inference(avatar_split_clause,[],[f147,f123,f156])).
% 0.28/0.36 tff(f166,definition,(
% 0.28/0.36 spl8_20 <=> (bG6 = $false)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_20])],[avatar_definition])).
% 0.28/0.36 tff(f168,plain,(
% 0.28/0.36 (bG6 = $false) | ~spl8_20),
% 0.28/0.36 inference(avatar_component_clause,[],[f166])).
% 0.28/0.36 tff(f170,definition,(
% 0.28/0.36 spl8_21 <=> f1($true)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_21])],[avatar_definition])).
% 0.28/0.36 tff(f173,plain,(
% 0.28/0.36 spl8_20 | ~spl8_21 | spl8_16),
% 0.28/0.36 inference(avatar_split_clause,[],[f143,f119,f170,f166])).
% 0.28/0.36 tff(f174,plain,(
% 0.28/0.36 spl8_20 | spl8_15),
% 0.28/0.36 inference(avatar_split_clause,[],[f148,f113,f166])).
% 0.28/0.36 tff(f176,definition,(
% 0.28/0.36 spl8_22 <=> (bG5 = $false)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_22])],[avatar_definition])).
% 0.28/0.36 tff(f178,plain,(
% 0.28/0.36 (bG5 = $false) | ~spl8_22),
% 0.28/0.36 inference(avatar_component_clause,[],[f176])).
% 0.28/0.36 tff(f180,plain,(
% 0.28/0.36 spl8_22 | spl8_13),
% 0.28/0.36 inference(avatar_split_clause,[],[f149,f103,f176])).
% 0.28/0.36 tff(f182,definition,(
% 0.28/0.36 spl8_23 <=> (bG4 = $false)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_23])],[avatar_definition])).
% 0.28/0.36 tff(f184,plain,(
% 0.28/0.36 (bG4 = $false) | ~spl8_23),
% 0.28/0.36 inference(avatar_component_clause,[],[f182])).
% 0.28/0.36 tff(f186,plain,(
% 0.28/0.36 spl8_23 | spl8_11),
% 0.28/0.36 inference(avatar_split_clause,[],[f150,f93,f182])).
% 0.28/0.36 tff(f188,definition,(
% 0.28/0.36 spl8_24 <=> (bG3 = $false)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_24])],[avatar_definition])).
% 0.28/0.36 tff(f190,plain,(
% 0.28/0.36 (bG3 = $false) | ~spl8_24),
% 0.28/0.36 inference(avatar_component_clause,[],[f188])).
% 0.28/0.36 tff(f192,plain,(
% 0.28/0.36 spl8_24 | spl8_10),
% 0.28/0.36 inference(avatar_split_clause,[],[f151,f87,f188])).
% 0.28/0.36 tff(f194,definition,(
% 0.28/0.36 spl8_25 <=> (bG2 = $false)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_25])],[avatar_definition])).
% 0.28/0.36 tff(f196,plain,(
% 0.28/0.36 (bG2 = $false) | ~spl8_25),
% 0.28/0.36 inference(avatar_component_clause,[],[f194])).
% 0.28/0.36 tff(f198,plain,(
% 0.28/0.36 spl8_25 | spl8_8),
% 0.28/0.36 inference(avatar_split_clause,[],[f152,f77,f194])).
% 0.28/0.36 tff(f200,definition,(
% 0.28/0.36 spl8_26 <=> (bG1 = $false)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_26])],[avatar_definition])).
% 0.28/0.36 tff(f202,plain,(
% 0.28/0.36 (bG1 = $false) | ~spl8_26),
% 0.28/0.36 inference(avatar_component_clause,[],[f200])).
% 0.28/0.36 tff(f204,plain,(
% 0.28/0.36 spl8_26 | spl8_6),
% 0.28/0.36 inference(avatar_split_clause,[],[f153,f67,f200])).
% 0.28/0.36 tff(f206,definition,(
% 0.28/0.36 spl8_27 <=> (bG0 = $false)),
% 0.28/0.36 introduced(definition,[new_symbols(definition,[spl8_27])],[avatar_definition])).
% 0.28/0.36 tff(f208,plain,(
% 0.28/0.36 (bG0 = $false) | ~spl8_27),
% 0.28/0.36 inference(avatar_component_clause,[],[f206])).
% 0.28/0.36 tff(f210,plain,(
% 0.28/0.36 spl8_27 | spl8_4),
% 0.28/0.36 inference(avatar_split_clause,[],[f154,f57,f206])).
% 0.28/0.36 tff(f213,plain,(
% 0.28/0.36 ~f0($true) | (bG3 = $false) | spl8_1),
% 0.28/0.36 inference(superposition,[],[f44,f41])).
% 0.28/0.36 tff(f214,plain,(
% 0.28/0.36 spl8_24 | ~spl8_19 | spl8_1),
% 0.28/0.36 inference(avatar_split_clause,[],[f213,f43,f160,f188])).
% 0.28/0.36 tff(f219,plain,(
% 0.28/0.36 f0($false) | (~spl8_2 | ~spl8_18)),
% 0.28/0.36 inference(superposition,[],[f49,f158])).
% 0.28/0.36 tff(f221,plain,(
% 0.28/0.36 f0($true) | (bG1 = $false) | ~spl8_7),
% 0.28/0.36 inference(superposition,[],[f74,f41])).
% 0.28/0.36 tff(f227,plain,(
% 0.28/0.36 spl8_26 | spl8_19 | ~spl8_7),
% 0.28/0.36 inference(avatar_split_clause,[],[f221,f73,f160,f200])).
% 0.28/0.36 tff(f230,plain,(
% 0.28/0.36 f1($true) | (bG4 = $false) | ~spl8_12),
% 0.28/0.36 inference(superposition,[],[f100,f41])).
% 0.28/0.36 tff(f231,plain,(
% 0.28/0.36 spl8_23 | spl8_21 | ~spl8_12),
% 0.28/0.36 inference(avatar_split_clause,[],[f230,f99,f170,f182])).
% 0.28/0.36 tff(f233,plain,(
% 0.28/0.36 ~f0($false) | (spl8_1 | ~spl8_24)),
% 0.28/0.36 inference(superposition,[],[f44,f190])).
% 0.28/0.36 tff(f235,plain,(
% 0.28/0.36 $false | (spl8_1 | ~spl8_2 | ~spl8_18 | ~spl8_24)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f233,f219])).
% 0.28/0.36 tff(f236,plain,(
% 0.28/0.36 spl8_1 | ~spl8_2 | ~spl8_18 | ~spl8_24),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f235])).
% 0.28/0.36 tff(f237,plain,(
% 0.28/0.36 f1($true) | (bG5 = $false) | ~spl8_14),
% 0.28/0.36 inference(superposition,[],[f110,f41])).
% 0.28/0.36 tff(f238,plain,(
% 0.28/0.36 spl8_22 | spl8_21 | ~spl8_14),
% 0.28/0.36 inference(avatar_split_clause,[],[f237,f109,f170,f176])).
% 0.28/0.36 tff(f239,plain,(
% 0.28/0.36 f1($true) | (bG6 = $false) | ~spl8_16),
% 0.28/0.36 inference(superposition,[],[f120,f41])).
% 0.28/0.36 tff(f240,plain,(
% 0.28/0.36 spl8_20 | spl8_21 | ~spl8_16),
% 0.28/0.36 inference(avatar_split_clause,[],[f239,f119,f170,f166])).
% 0.28/0.36 tff(f242,plain,(
% 0.28/0.36 ~f1($true) | (~spl8_4 | spl8_5)),
% 0.28/0.36 inference(superposition,[],[f65,f59])).
% 0.28/0.36 tff(f243,plain,(
% 0.28/0.36 ~spl8_21 | ~spl8_4 | spl8_5),
% 0.28/0.36 inference(avatar_split_clause,[],[f242,f63,f57,f170])).
% 0.28/0.36 tff(f250,plain,(
% 0.28/0.36 ($true = $false) | (~spl8_10 | ~spl8_24)),
% 0.28/0.36 inference(forward_demodulation,[],[f89,f190])).
% 0.28/0.36 tff(f251,plain,(
% 0.28/0.36 $false | (~spl8_10 | ~spl8_24)),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f250])).
% 0.28/0.36 tff(f252,plain,(
% 0.28/0.36 ~spl8_10 | ~spl8_24),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f251])).
% 0.28/0.36 tff(f253,plain,(
% 0.28/0.36 ~f0($true) | (~spl8_8 | spl8_9)),
% 0.28/0.36 inference(forward_demodulation,[],[f85,f79])).
% 0.28/0.36 tff(f255,plain,(
% 0.28/0.36 $false | (~spl8_8 | spl8_9 | ~spl8_19)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f253,f162])).
% 0.28/0.36 tff(f256,plain,(
% 0.28/0.36 ~spl8_8 | spl8_9 | ~spl8_19),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f255])).
% 0.28/0.36 tff(f269,plain,(
% 0.28/0.36 f1($true) | (~spl8_13 | ~spl8_14)),
% 0.28/0.36 inference(superposition,[],[f110,f105])).
% 0.28/0.36 tff(f270,plain,(
% 0.28/0.36 f1($true) | (~spl8_15 | ~spl8_16)),
% 0.28/0.36 inference(superposition,[],[f120,f115])).
% 0.28/0.36 tff(f272,plain,(
% 0.28/0.36 f0($true) | (~spl8_2 | ~spl8_17)),
% 0.28/0.36 inference(superposition,[],[f49,f125])).
% 0.28/0.36 tff(f275,plain,(
% 0.28/0.36 f1($false) | (~spl8_12 | ~spl8_23)),
% 0.28/0.36 inference(superposition,[],[f100,f184])).
% 0.28/0.36 tff(f279,plain,(
% 0.28/0.36 ~f0($false) | (spl8_9 | ~spl8_25)),
% 0.28/0.36 inference(superposition,[],[f85,f196])).
% 0.28/0.36 tff(f282,plain,(
% 0.28/0.36 ~f0($false) | (spl8_7 | ~spl8_26)),
% 0.28/0.36 inference(superposition,[],[f75,f202])).
% 0.28/0.36 tff(f287,plain,(
% 0.28/0.36 ~f1($false) | (spl8_5 | ~spl8_27)),
% 0.28/0.36 inference(superposition,[],[f65,f208])).
% 0.28/0.36 tff(f289,plain,(
% 0.28/0.36 $false | (spl8_5 | ~spl8_12 | ~spl8_23 | ~spl8_27)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f287,f275])).
% 0.28/0.36 tff(f290,plain,(
% 0.28/0.36 spl8_5 | ~spl8_12 | ~spl8_23 | ~spl8_27),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f289])).
% 0.28/0.36 tff(f291,plain,(
% 0.28/0.36 ~f1($false) | (spl8_12 | ~spl8_23)),
% 0.28/0.36 inference(forward_demodulation,[],[f101,f184])).
% 0.28/0.36 tff(f296,plain,(
% 0.28/0.36 f1($false) | (~spl8_14 | ~spl8_22)),
% 0.28/0.36 inference(superposition,[],[f110,f178])).
% 0.28/0.36 tff(f298,plain,(
% 0.28/0.36 $false | (spl8_12 | ~spl8_14 | ~spl8_22 | ~spl8_23)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f296,f291])).
% 0.28/0.36 tff(f299,plain,(
% 0.28/0.36 spl8_12 | ~spl8_14 | ~spl8_22 | ~spl8_23),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f298])).
% 0.28/0.36 tff(f300,plain,(
% 0.28/0.36 f1($false) | (~spl8_5 | ~spl8_27)),
% 0.28/0.36 inference(forward_demodulation,[],[f64,f208])).
% 0.28/0.36 tff(f301,plain,(
% 0.28/0.36 ($true = $false) | (~spl8_6 | ~spl8_26)),
% 0.28/0.36 inference(forward_demodulation,[],[f69,f202])).
% 0.28/0.36 tff(f302,plain,(
% 0.28/0.36 $false | (~spl8_6 | ~spl8_26)),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f301])).
% 0.28/0.36 tff(f303,plain,(
% 0.28/0.36 ~spl8_6 | ~spl8_26),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f302])).
% 0.28/0.36 tff(f305,plain,(
% 0.28/0.36 f0($false) | (~spl8_1 | ~spl8_24)),
% 0.28/0.36 inference(forward_demodulation,[],[f45,f190])).
% 0.28/0.36 tff(f306,plain,(
% 0.28/0.36 ~f0($true) | (spl8_2 | ~spl8_17)),
% 0.28/0.36 inference(forward_demodulation,[],[f48,f125])).
% 0.28/0.36 tff(f308,plain,(
% 0.28/0.36 ~spl8_19 | spl8_2 | ~spl8_17),
% 0.28/0.36 inference(avatar_split_clause,[],[f306,f123,f47,f160])).
% 0.28/0.36 tff(f309,plain,(
% 0.28/0.36 ( ! [X0 : $o] : (~f0(X0) | ($false = X0)) ) | spl8_19),
% 0.28/0.36 inference(superposition,[],[f161,f41])).
% 0.28/0.36 tff(f313,plain,(
% 0.28/0.36 $false | (~spl8_1 | spl8_9 | ~spl8_24 | ~spl8_25)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f279,f305])).
% 0.28/0.36 tff(f314,plain,(
% 0.28/0.36 ~spl8_1 | spl8_9 | ~spl8_24 | ~spl8_25),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f313])).
% 0.28/0.36 tff(f315,plain,(
% 0.28/0.36 ($true = $false) | (~spl8_11 | ~spl8_23)),
% 0.28/0.36 inference(forward_demodulation,[],[f95,f184])).
% 0.28/0.36 tff(f316,plain,(
% 0.28/0.36 $false | (~spl8_11 | ~spl8_23)),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f315])).
% 0.28/0.36 tff(f317,plain,(
% 0.28/0.36 ~spl8_11 | ~spl8_23),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f316])).
% 0.28/0.36 tff(f318,plain,(
% 0.28/0.36 ~f1($true) | (~spl8_13 | spl8_14)),
% 0.28/0.36 inference(forward_demodulation,[],[f111,f105])).
% 0.28/0.36 tff(f319,plain,(
% 0.28/0.36 ~spl8_21 | ~spl8_13 | spl8_14),
% 0.28/0.36 inference(avatar_split_clause,[],[f318,f109,f103,f170])).
% 0.28/0.36 tff(f322,plain,(
% 0.28/0.36 ~f1($true) | (bG0 = $false) | spl8_5),
% 0.28/0.36 inference(superposition,[],[f65,f41])).
% 0.28/0.36 tff(f323,plain,(
% 0.28/0.36 spl8_27 | ~spl8_21 | spl8_5),
% 0.28/0.36 inference(avatar_split_clause,[],[f322,f63,f170,f206])).
% 0.28/0.36 tff(f345,plain,(
% 0.28/0.36 ~f1($false) | (spl8_16 | ~spl8_20)),
% 0.28/0.36 inference(forward_demodulation,[],[f121,f168])).
% 0.28/0.36 tff(f348,plain,(
% 0.28/0.36 ~f0($false) | (spl8_2 | ~spl8_18)),
% 0.28/0.36 inference(superposition,[],[f48,f158])).
% 0.28/0.36 tff(f350,plain,(
% 0.28/0.36 $false | (~spl8_1 | spl8_2 | ~spl8_18 | ~spl8_24)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f348,f305])).
% 0.28/0.36 tff(f351,plain,(
% 0.28/0.36 ~spl8_1 | spl8_2 | ~spl8_18 | ~spl8_24),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f350])).
% 0.28/0.36 tff(f352,plain,(
% 0.28/0.36 f1($false) | (~spl8_16 | ~spl8_20)),
% 0.28/0.36 inference(forward_demodulation,[],[f120,f168])).
% 0.28/0.36 tff(f356,plain,(
% 0.28/0.36 $false | (spl8_5 | ~spl8_16 | ~spl8_20 | ~spl8_27)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f287,f352])).
% 0.28/0.36 tff(f357,plain,(
% 0.28/0.36 spl8_5 | ~spl8_16 | ~spl8_20 | ~spl8_27),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f356])).
% 0.28/0.36 tff(f358,plain,(
% 0.28/0.36 f0($true) | (~spl8_8 | ~spl8_9)),
% 0.28/0.36 inference(forward_demodulation,[],[f84,f79])).
% 0.28/0.36 tff(f362,plain,(
% 0.28/0.36 $false | (~spl8_8 | ~spl8_9 | spl8_19)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f358,f161])).
% 0.28/0.36 tff(f363,plain,(
% 0.28/0.36 ~spl8_8 | ~spl8_9 | spl8_19),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f362])).
% 0.28/0.36 tff(f365,plain,(
% 0.28/0.36 (bG7 = $false) | (~spl8_2 | spl8_19)),
% 0.28/0.36 inference(resolution,[],[f49,f309])).
% 0.28/0.36 tff(f368,plain,(
% 0.28/0.36 spl8_18 | ~spl8_2 | spl8_19),
% 0.28/0.36 inference(avatar_split_clause,[],[f365,f160,f47,f156])).
% 0.28/0.36 tff(f378,plain,(
% 0.28/0.36 $false | (~spl8_2 | spl8_7 | ~spl8_18 | ~spl8_26)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f282,f219])).
% 0.28/0.36 tff(f379,plain,(
% 0.28/0.36 ~spl8_2 | spl8_7 | ~spl8_18 | ~spl8_26),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f378])).
% 0.28/0.36 tff(f380,plain,(
% 0.28/0.36 f1($true) | (~spl8_4 | ~spl8_5)),
% 0.28/0.36 inference(forward_demodulation,[],[f64,f59])).
% 0.28/0.36 tff(f381,plain,(
% 0.28/0.36 $false | (~spl8_5 | spl8_16 | ~spl8_20 | ~spl8_27)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f300,f345])).
% 0.28/0.36 tff(f382,plain,(
% 0.28/0.36 ~spl8_5 | spl8_16 | ~spl8_20 | ~spl8_27),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f381])).
% 0.28/0.36 tff(f385,plain,(
% 0.28/0.36 spl8_21 | ~spl8_13 | ~spl8_14),
% 0.28/0.36 inference(avatar_split_clause,[],[f269,f109,f103,f170])).
% 0.28/0.36 tff(f386,plain,(
% 0.28/0.36 ($true = $false) | (~spl8_15 | ~spl8_20)),
% 0.28/0.36 inference(forward_demodulation,[],[f115,f168])).
% 0.28/0.36 tff(f387,plain,(
% 0.28/0.36 $false | (~spl8_15 | ~spl8_20)),
% 0.28/0.36 inference(trivial_inequality_removal,[],[f386])).
% 0.28/0.36 tff(f388,plain,(
% 0.28/0.36 ~spl8_15 | ~spl8_20),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f387])).
% 0.28/0.36 tff(f389,plain,(
% 0.28/0.36 spl8_21 | ~spl8_15 | ~spl8_16),
% 0.28/0.36 inference(avatar_split_clause,[],[f270,f119,f113,f170])).
% 0.28/0.36 tff(f394,plain,(
% 0.28/0.36 $false | (~spl8_2 | ~spl8_17 | spl8_19)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f272,f161])).
% 0.28/0.36 tff(f395,plain,(
% 0.28/0.36 ~spl8_2 | ~spl8_17 | spl8_19),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f394])).
% 0.28/0.36 tff(f396,plain,(
% 0.28/0.36 spl8_21 | ~spl8_4 | ~spl8_5),
% 0.28/0.36 inference(avatar_split_clause,[],[f380,f63,f57,f170])).
% 0.28/0.36 tff(f401,plain,(
% 0.28/0.36 f0($true) | (bG3 = $false) | ~spl8_1),
% 0.28/0.36 inference(superposition,[],[f45,f41])).
% 0.28/0.36 tff(f404,plain,(
% 0.28/0.36 ~f0($true) | (bG7 = $false) | spl8_2),
% 0.28/0.36 inference(superposition,[],[f48,f41])).
% 0.28/0.36 tff(f414,plain,(
% 0.28/0.36 ~f1($true) | (bG4 = $false) | spl8_12),
% 0.28/0.36 inference(superposition,[],[f101,f41])).
% 0.28/0.36 tff(f415,plain,(
% 0.28/0.36 spl8_23 | ~spl8_21 | spl8_12),
% 0.28/0.36 inference(avatar_split_clause,[],[f414,f99,f170,f182])).
% 0.28/0.36 tff(f430,plain,(
% 0.28/0.36 ~f1($false) | (spl8_14 | ~spl8_22)),
% 0.28/0.36 inference(superposition,[],[f111,f178])).
% 0.28/0.36 tff(f432,plain,(
% 0.28/0.36 $false | (spl8_14 | ~spl8_16 | ~spl8_20 | ~spl8_22)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f430,f352])).
% 0.28/0.36 tff(f433,plain,(
% 0.28/0.36 spl8_14 | ~spl8_16 | ~spl8_20 | ~spl8_22),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f432])).
% 0.28/0.36 tff(f435,plain,(
% 0.28/0.36 spl8_24 | spl8_19 | ~spl8_1),
% 0.28/0.36 inference(avatar_split_clause,[],[f401,f43,f160,f188])).
% 0.28/0.36 tff(f436,plain,(
% 0.28/0.36 spl8_18 | ~spl8_19 | spl8_2),
% 0.28/0.36 inference(avatar_split_clause,[],[f404,f47,f160,f156])).
% 0.28/0.36 tff(f437,plain,(
% 0.28/0.36 ~f0($true) | (bG1 = $false) | spl8_7),
% 0.28/0.36 inference(superposition,[],[f75,f41])).
% 0.28/0.36 tff(f438,plain,(
% 0.28/0.36 spl8_26 | ~spl8_19 | spl8_7),
% 0.28/0.36 inference(avatar_split_clause,[],[f437,f73,f160,f200])).
% 0.28/0.36 tff(f456,plain,(
% 0.28/0.36 f0($false) | (~spl8_9 | ~spl8_25)),
% 0.28/0.36 inference(superposition,[],[f84,f196])).
% 0.28/0.36 tff(f458,plain,(
% 0.28/0.36 $false | (spl8_2 | ~spl8_9 | ~spl8_18 | ~spl8_25)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f456,f348])).
% 0.28/0.36 tff(f459,plain,(
% 0.28/0.36 spl8_2 | ~spl8_9 | ~spl8_18 | ~spl8_25),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f458])).
% 0.28/0.36 tff(f464,plain,(
% 0.28/0.36 f0($false) | (~spl8_7 | ~spl8_26)),
% 0.28/0.36 inference(superposition,[],[f74,f202])).
% 0.28/0.36 tff(f467,plain,(
% 0.28/0.36 $false | (spl8_2 | ~spl8_7 | ~spl8_18 | ~spl8_26)),
% 0.28/0.36 inference(forward_subsumption_resolution,[],[f464,f348])).
% 0.28/0.36 tff(f468,plain,(
% 0.28/0.36 spl8_2 | ~spl8_7 | ~spl8_18 | ~spl8_26),
% 0.28/0.36 inference(avatar_contradiction_clause,[],[f467])).
% 0.28/0.36 cnf(s1, plain, spl8_1 | spl8_2, inference(sat_conversion,[],[f50])).
% 0.28/0.36 cnf(s2, plain, ~spl8_1 | ~spl8_2, inference(sat_conversion,[],[f51])).
% 0.28/0.36 cnf(s3, plain, ~spl8_3 | spl8_4, inference(sat_conversion,[],[f60])).
% 0.28/0.36 cnf(s4, plain, spl8_3 | ~spl8_4, inference(sat_conversion,[],[f61])).
% 0.28/0.36 cnf(s5, plain, ~spl8_5 | spl8_6, inference(sat_conversion,[],[f70])).
% 0.28/0.36 cnf(s6, plain, spl8_5 | ~spl8_6, inference(sat_conversion,[],[f71])).
% 0.28/0.36 cnf(s7, plain, ~spl8_7 | spl8_8, inference(sat_conversion,[],[f80])).
% 0.28/0.36 cnf(s8, plain, spl8_7 | ~spl8_8, inference(sat_conversion,[],[f81])).
% 0.28/0.36 cnf(s9, plain, ~spl8_9 | spl8_10, inference(sat_conversion,[],[f90])).
% 0.28/0.36 cnf(s10, plain, spl8_9 | ~spl8_10, inference(sat_conversion,[],[f91])).
% 0.28/0.36 cnf(s11, plain, ~spl8_3 | spl8_11, inference(sat_conversion,[],[f96])).
% 0.28/0.37 cnf(s12, plain, spl8_3 | ~spl8_11, inference(sat_conversion,[],[f97])).
% 0.28/0.37 cnf(s13, plain, ~spl8_12 | spl8_13, inference(sat_conversion,[],[f106])).
% 0.28/0.37 cnf(s14, plain, spl8_12 | ~spl8_13, inference(sat_conversion,[],[f107])).
% 0.28/0.37 cnf(s15, plain, ~spl8_14 | spl8_15, inference(sat_conversion,[],[f116])).
% 0.28/0.37 cnf(s16, plain, spl8_14 | ~spl8_15, inference(sat_conversion,[],[f117])).
% 0.28/0.37 cnf(s17, plain, ~spl8_16 | spl8_17, inference(sat_conversion,[],[f126])).
% 0.28/0.37 cnf(s18, plain, spl8_16 | ~spl8_17, inference(sat_conversion,[],[f127])).
% 0.28/0.37 cnf(s20, plain, spl8_17 | spl8_18, inference(sat_conversion,[],[f164])).
% 0.28/0.37 cnf(s21, plain, spl8_16 | spl8_20 | ~spl8_21, inference(sat_conversion,[],[f173])).
% 0.28/0.37 cnf(s22, plain, spl8_15 | spl8_20, inference(sat_conversion,[],[f174])).
% 0.28/0.37 cnf(s24, plain, spl8_13 | spl8_22, inference(sat_conversion,[],[f180])).
% 0.28/0.37 cnf(s26, plain, spl8_11 | spl8_23, inference(sat_conversion,[],[f186])).
% 0.28/0.37 cnf(s28, plain, spl8_10 | spl8_24, inference(sat_conversion,[],[f192])).
% 0.28/0.37 cnf(s30, plain, spl8_8 | spl8_25, inference(sat_conversion,[],[f198])).
% 0.28/0.37 cnf(s32, plain, spl8_6 | spl8_26, inference(sat_conversion,[],[f204])).
% 0.28/0.37 cnf(s34, plain, spl8_4 | spl8_27, inference(sat_conversion,[],[f210])).
% 0.28/0.37 cnf(s36, plain, spl8_1 | ~spl8_19 | spl8_24, inference(sat_conversion,[],[f214])).
% 0.28/0.37 cnf(s40, plain, ~spl8_7 | spl8_19 | spl8_26, inference(sat_conversion,[],[f227])).
% 0.28/0.37 cnf(s42, plain, ~spl8_12 | spl8_21 | spl8_23, inference(sat_conversion,[],[f231])).
% 0.28/0.37 cnf(s43, plain, spl8_1 | ~spl8_2 | ~spl8_18 | ~spl8_24, inference(sat_conversion,[],[f236])).
% 0.28/0.37 cnf(s44, plain, ~spl8_14 | spl8_21 | spl8_22, inference(sat_conversion,[],[f238])).
% 0.28/0.37 cnf(s45, plain, ~spl8_16 | spl8_20 | spl8_21, inference(sat_conversion,[],[f240])).
% 0.28/0.37 cnf(s46, plain, ~spl8_4 | spl8_5 | ~spl8_21, inference(sat_conversion,[],[f243])).
% 0.28/0.37 cnf(s50, plain, ~spl8_10 | ~spl8_24, inference(sat_conversion,[],[f252])).
% 0.28/0.37 cnf(s51, plain, ~spl8_8 | spl8_9 | ~spl8_19, inference(sat_conversion,[],[f256])).
% 0.28/0.37 cnf(s59, plain, spl8_5 | ~spl8_12 | ~spl8_23 | ~spl8_27, inference(sat_conversion,[],[f290])).
% 0.28/0.37 cnf(s62, plain, spl8_12 | ~spl8_14 | ~spl8_22 | ~spl8_23, inference(sat_conversion,[],[f299])).
% 0.28/0.37 cnf(s63, plain, ~spl8_6 | ~spl8_26, inference(sat_conversion,[],[f303])).
% 0.28/0.37 cnf(s65, plain, spl8_2 | ~spl8_17 | ~spl8_19, inference(sat_conversion,[],[f308])).
% 0.28/0.37 cnf(s66, plain, ~spl8_1 | spl8_9 | ~spl8_24 | ~spl8_25, inference(sat_conversion,[],[f314])).
% 0.28/0.37 cnf(s69, plain, ~spl8_11 | ~spl8_23, inference(sat_conversion,[],[f317])).
% 0.28/0.37 cnf(s71, plain, ~spl8_13 | spl8_14 | ~spl8_21, inference(sat_conversion,[],[f319])).
% 0.28/0.37 cnf(s76, plain, spl8_5 | ~spl8_21 | spl8_27, inference(sat_conversion,[],[f323])).
% 0.28/0.37 cnf(s86, plain, ~spl8_1 | spl8_2 | ~spl8_18 | ~spl8_24, inference(sat_conversion,[],[f351])).
% 0.28/0.37 cnf(s87, plain, spl8_5 | ~spl8_16 | ~spl8_20 | ~spl8_27, inference(sat_conversion,[],[f357])).
% 0.28/0.37 cnf(s90, plain, ~spl8_8 | ~spl8_9 | spl8_19, inference(sat_conversion,[],[f363])).
% 0.28/0.37 cnf(s93, plain, ~spl8_2 | spl8_18 | spl8_19, inference(sat_conversion,[],[f368])).
% 0.28/0.37 cnf(s97, plain, ~spl8_2 | spl8_7 | ~spl8_18 | ~spl8_26, inference(sat_conversion,[],[f379])).
% 0.28/0.37 cnf(s98, plain, ~spl8_5 | spl8_16 | ~spl8_20 | ~spl8_27, inference(sat_conversion,[],[f382])).
% 0.28/0.37 cnf(s100, plain, ~spl8_13 | ~spl8_14 | spl8_21, inference(sat_conversion,[],[f385])).
% 0.28/0.37 cnf(s102, plain, ~spl8_15 | ~spl8_20, inference(sat_conversion,[],[f388])).
% 0.28/0.37 cnf(s103, plain, ~spl8_15 | ~spl8_16 | spl8_21, inference(sat_conversion,[],[f389])).
% 0.28/0.37 cnf(s105, plain, ~spl8_2 | ~spl8_17 | spl8_19, inference(sat_conversion,[],[f395])).
% 0.28/0.37 cnf(s106, plain, ~spl8_4 | ~spl8_5 | spl8_21, inference(sat_conversion,[],[f396])).
% 0.28/0.37 cnf(s120, plain, spl8_12 | ~spl8_21 | spl8_23, inference(sat_conversion,[],[f415])).
% 0.28/0.37 cnf(s124, plain, spl8_14 | ~spl8_16 | ~spl8_20 | ~spl8_22, inference(sat_conversion,[],[f433])).
% 0.28/0.37 cnf(s128, plain, ~spl8_1 | spl8_19 | spl8_24, inference(sat_conversion,[],[f435])).
% 0.28/0.37 cnf(s129, plain, spl8_2 | spl8_18 | ~spl8_19, inference(sat_conversion,[],[f436])).
% 0.28/0.37 cnf(s130, plain, spl8_7 | ~spl8_19 | spl8_26, inference(sat_conversion,[],[f438])).
% 0.28/0.37 cnf(s133, plain, spl8_2 | ~spl8_9 | ~spl8_18 | ~spl8_25, inference(sat_conversion,[],[f459])).
% 0.28/0.37 cnf(s134, plain, spl8_2 | ~spl8_7 | ~spl8_18 | ~spl8_26, inference(sat_conversion,[],[f468])).
% 0.28/0.37 cnf(s135, plain, spl8_5 | spl8_3 | spl8_1, inference(rat,[],[s90,s10,s7,s36,s28,s97,s43,s20,s18,s87,s22,s16,s62,s24,s14,s32,s59,s6,s1,s26,s12,s34,s4])).
% 0.28/0.37 cnf(s136, plain, ~spl8_7 | spl8_26 | spl8_1, inference(rat,[],[s50,s9,s36,s51,s40,s7])).
% 0.28/0.37 cnf(s137, plain, spl8_3 | spl8_1, inference(rat,[],[s62,s13,s44,s100,s16,s21,s22,s98,s17,s105,s130,s136,s63,s5,s135,s34,s26,s4,s12,s1])).
% 0.28/0.37 cnf(s138, plain, ~spl8_5 | spl8_1, inference(rat,[],[s21,s17,s102,s105,s15,s130,s71,s136,s13,s63,s120,s5,s106,s1,s3,s69,s11,s137])).
% 0.28/0.37 cnf(s139, plain, ~spl8_19 | ~spl8_8 | spl8_1, inference(rat,[],[s50,s9,s36,s51])).
% 0.28/0.37 cnf(s140, plain, ~spl8_8 | spl8_1, inference(rat,[],[s28,s10,s43,s90,s93,s139,s1])).
% 0.28/0.37 cnf(s141, plain, spl8_1, inference(rat,[],[s124,s15,s45,s103,s18,s20,s97,s7,s140,s24,s14,s42,s32,s46,s6,s138,s69,s3,s11,s137,s1])).
% 0.28/0.37 cnf(s142, plain, ~spl8_2, inference(rat,[],[s2,s141])).
% 0.28/0.37 cnf(s143, plain, spl8_23 | spl8_12 | ~spl8_5, inference(rat,[],[s3,s106,s12,s120,s26])).
% 0.28/0.37 cnf(s144, plain, spl8_12 | ~spl8_5 | spl8_16, inference(rat,[],[s98,s34,s22,s4,s16,s11,s62,s69,s143,s24,s14])).
% 0.28/0.37 cnf(s145, plain, ~spl8_14 | ~spl8_13 | spl8_16, inference(rat,[],[s102,s21,s15,s100])).
% 0.28/0.37 cnf(s146, plain, ~spl8_5 | spl8_16, inference(rat,[],[s98,s34,s22,s106,s16,s71,s145,s13,s144])).
% 0.28/0.37 cnf(s147, plain, ~spl8_19 | ~spl8_7, inference(rat,[],[s146,s6,s32,s17,s134,s65,s129,s142])).
% 0.28/0.37 cnf(s148, plain, ~spl8_14 | spl8_12 | ~spl8_16, inference(rat,[],[s120,s103,s62,s15,s24,s14])).
% 0.28/0.37 cnf(s149, plain, spl8_12 | ~spl8_16, inference(rat,[],[s22,s124,s16,s148,s24,s14])).
% 0.28/0.37 cnf(s150, plain, ~spl8_21 | ~spl8_7, inference(rat,[],[s12,s26,s3,s59,s46,s76,s5,s63,s40,s149,s18,s20,s86,s128,s147,s142,s141])).
% 0.28/0.37 cnf(s151, plain, ~spl8_7, inference(rat,[],[s4,s34,s11,s59,s69,s42,s150,s149,s18,s5,s20,s63,s86,s40,s128,s147,s141,s142])).
% 0.28/0.37 cnf(s152, plain, ~spl8_8, inference(rat,[],[s8,s151])).
% 0.28/0.37 cnf(s153, plain, spl8_25, inference(rat,[],[s30,s152])).
% 0.28/0.37 cnf(s154, plain, ~spl8_18, inference(rat,[],[s10,s28,s133,s86,s142,s153,s141])).
% 0.28/0.37 cnf(s156, plain, ~spl8_19, inference(rat,[],[s129,s142,s154])).
% 0.28/0.37 cnf(s158, plain, spl8_24, inference(rat,[],[s128,s141,s156])).
% 0.28/0.37 cnf(s160, plain, ~spl8_10, inference(rat,[],[s50,s158])).
% 0.28/0.37 cnf(s161, plain, spl8_9, inference(rat,[],[s66,s153,s141,s158])).
% 0.28/0.37 cnf(s163, plain, $false, inference(rat,[],[s9,s160,s161])).
% 0.28/0.37 tff(f469,plain,(
% 0.28/0.37 $false),
% 0.28/0.37 inference(avatar_sat_refutation,[],[s163])).
% 0.28/0.37 % SZS output end Proof for theBenchmark
% 0.28/0.37 % (370484)------------------------------
% 0.28/0.37 % (370484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/0.37 % (370484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/0.37 % (370484)CaDiCaL version: 2.1.3
% 0.28/0.37 % (370484)Termination reason: Refutation
% 0.28/0.37 % (370484)Time elapsed: 0.010 s
% 0.28/0.37 % (370484)Peak memory usage: 12 MB
% 0.28/0.37 % (370484)Instructions burned: 15 (million)
% 0.28/0.37 % (370476)Success in time 0.036 s
% 0.28/0.37 % Vampire exiting
%------------------------------------------------------------------------------