%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO040_8 : 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 : n013.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:29:38 PM UTC 2026
% Result : Theorem 0.09s 0.25s
% Output : Refutation 0.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO040_8 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n013.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 17:22:21 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 Running first-order model finding
% 0.09/0.20 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.09/0.25 % (1338319)Will run a generic schedule for satisfiability detection.
% 0.09/0.25 % (1338344)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1189962640:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.09/0.25 % (1338344) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1338319-1338344"...
% 0.09/0.25 % (1338344)...printing done.
% 0.09/0.25 % (1338344)Refutation found. Thanks to Tanya!
% 0.09/0.25 % SZS status Theorem for theBenchmark
% 0.09/0.25 % SZS output start Proof for theBenchmark
% 0.09/0.25 tff(func_def_0, type, h: $o > $i).
% 0.09/0.25 tff(func_def_1, type, bG0: $o).
% 0.09/0.25 tff(func_def_4, type, bG1: $o).
% 0.09/0.25 tff(func_def_5, type, bG2: $o).
% 0.09/0.25 tff(func_def_6, type, bG3: $o).
% 0.09/0.25 tff(func_def_7, type, bG4: $o).
% 0.09/0.25 tff(func_def_8, type, bG5: $o).
% 0.09/0.25 tff(pred_def_1, type, f: $o > $o).
% 0.09/0.25 tff(f1,conjecture,(
% 0.09/0.25 h(f(f(f(x)))) = h(f(x))),
% 0.09/0.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p',2)).
% 0.09/0.25 tff(f2,negated_conjecture,(
% 0.09/0.25 ~ h(f(f(f(x)))) = h(f(x))),
% 0.09/0.25 inference(negated_conjecture,[status(cth)],[f1])).
% 0.09/0.25 tff(f3,plain,(
% 0.09/0.25 ~ h(f(f(f(x)))) = h(f(x))),
% 0.09/0.25 inference(rectify,[],[f2])).
% 0.09/0.25 tff(f4,definition,(
% 0.09/0.25 x <=> (bG0 = $true)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[bG0])],[fool_formula_definition])).
% 0.09/0.25 tff(f5,definition,(
% 0.09/0.25 f(bG0) <=> ($true = bG1)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[bG1])],[fool_formula_definition])).
% 0.09/0.25 tff(f6,definition,(
% 0.09/0.25 f(bG1) <=> ($true = bG2)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[bG2])],[fool_formula_definition])).
% 0.09/0.25 tff(f7,definition,(
% 0.09/0.25 f(bG2) <=> ($true = bG3)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[bG3])],[fool_formula_definition])).
% 0.09/0.25 tff(f8,definition,(
% 0.09/0.25 x <=> ($true = bG4)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[bG4])],[fool_formula_definition])).
% 0.09/0.25 tff(f9,definition,(
% 0.09/0.25 f(bG4) <=> ($true = bG5)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[bG5])],[fool_formula_definition])).
% 0.09/0.25 tff(f10,plain,(
% 0.09/0.25 ~ h(bG3) = h(bG5)),
% 0.09/0.25 inference(fool_elimination,[],[f3,f9,f8,f7,f6,f5,f4])).
% 0.09/0.25 tff(f11,plain,(
% 0.09/0.25 h(bG3) != h(bG5)),
% 0.09/0.25 inference(flattening,[],[f10])).
% 0.09/0.25 tff(f12,plain,(
% 0.09/0.25 (f(bG4) | ($true != bG5)) & (($true = bG5) | ~f(bG4))),
% 0.09/0.25 inference(nnf_transformation,[],[f9])).
% 0.09/0.25 tff(f13,plain,(
% 0.09/0.25 (x | ($true != bG4)) & (($true = bG4) | ~x)),
% 0.09/0.25 inference(nnf_transformation,[],[f8])).
% 0.09/0.25 tff(f14,plain,(
% 0.09/0.25 (f(bG2) | ($true != bG3)) & (($true = bG3) | ~f(bG2))),
% 0.09/0.25 inference(nnf_transformation,[],[f7])).
% 0.09/0.25 tff(f15,plain,(
% 0.09/0.25 (f(bG1) | ($true != bG2)) & (($true = bG2) | ~f(bG1))),
% 0.09/0.25 inference(nnf_transformation,[],[f6])).
% 0.09/0.25 tff(f16,plain,(
% 0.09/0.25 (f(bG0) | ($true != bG1)) & (($true = bG1) | ~f(bG0))),
% 0.09/0.25 inference(nnf_transformation,[],[f5])).
% 0.09/0.25 tff(f17,plain,(
% 0.09/0.25 (x | (bG0 != $true)) & ((bG0 = $true) | ~x)),
% 0.09/0.25 inference(nnf_transformation,[],[f4])).
% 0.09/0.25 tff(f18,plain,(
% 0.09/0.25 ($true = bG5) | ~f(bG4)),
% 0.09/0.25 inference(cnf_transformation,[],[f12])).
% 0.09/0.25 tff(f19,plain,(
% 0.09/0.25 f(bG4) | ($true != bG5)),
% 0.09/0.25 inference(cnf_transformation,[],[f12])).
% 0.09/0.25 tff(f20,plain,(
% 0.09/0.25 ($true = bG4) | ~x),
% 0.09/0.25 inference(cnf_transformation,[],[f13])).
% 0.09/0.25 tff(f21,plain,(
% 0.09/0.25 x | ($true != bG4)),
% 0.09/0.25 inference(cnf_transformation,[],[f13])).
% 0.09/0.25 tff(f22,plain,(
% 0.09/0.25 ($true = bG3) | ~f(bG2)),
% 0.09/0.25 inference(cnf_transformation,[],[f14])).
% 0.09/0.25 tff(f23,plain,(
% 0.09/0.25 f(bG2) | ($true != bG3)),
% 0.09/0.25 inference(cnf_transformation,[],[f14])).
% 0.09/0.25 tff(f24,plain,(
% 0.09/0.25 ($true = bG2) | ~f(bG1)),
% 0.09/0.25 inference(cnf_transformation,[],[f15])).
% 0.09/0.25 tff(f25,plain,(
% 0.09/0.25 f(bG1) | ($true != bG2)),
% 0.09/0.25 inference(cnf_transformation,[],[f15])).
% 0.09/0.25 tff(f26,plain,(
% 0.09/0.25 ($true = bG1) | ~f(bG0)),
% 0.09/0.25 inference(cnf_transformation,[],[f16])).
% 0.09/0.25 tff(f27,plain,(
% 0.09/0.25 f(bG0) | ($true != bG1)),
% 0.09/0.25 inference(cnf_transformation,[],[f16])).
% 0.09/0.25 tff(f28,plain,(
% 0.09/0.25 (bG0 = $true) | ~x),
% 0.09/0.25 inference(cnf_transformation,[],[f17])).
% 0.09/0.25 tff(f29,plain,(
% 0.09/0.25 x | (bG0 != $true)),
% 0.09/0.25 inference(cnf_transformation,[],[f17])).
% 0.09/0.25 tff(f30,plain,(
% 0.09/0.25 h(bG3) != h(bG5)),
% 0.09/0.25 inference(cnf_transformation,[],[f11])).
% 0.09/0.25 tff(f32,definition,(
% 0.09/0.25 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.09/0.25 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.09/0.25 tff(f33,plain,(
% 0.09/0.25 ~f(bG4) | ($true != bG5)),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f19])).
% 0.09/0.25 tff(f34,plain,(
% 0.09/0.25 ($true = bG5) | f(bG4)),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f18])).
% 0.09/0.25 tff(f35,plain,(
% 0.09/0.25 ~x | ($true != bG4)),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f21])).
% 0.09/0.25 tff(f36,plain,(
% 0.09/0.25 ($true = bG4) | x),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f20])).
% 0.09/0.25 tff(f37,plain,(
% 0.09/0.25 ~f(bG2) | ($true != bG3)),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f23])).
% 0.09/0.25 tff(f38,plain,(
% 0.09/0.25 ($true = bG3) | f(bG2)),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f22])).
% 0.09/0.25 tff(f39,plain,(
% 0.09/0.25 ~f(bG1) | ($true != bG2)),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f25])).
% 0.09/0.25 tff(f40,plain,(
% 0.09/0.25 ($true = bG2) | f(bG1)),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f24])).
% 0.09/0.25 tff(f41,plain,(
% 0.09/0.25 ~f(bG0) | ($true != bG1)),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f27])).
% 0.09/0.25 tff(f42,plain,(
% 0.09/0.25 ($true = bG1) | f(bG0)),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f26])).
% 0.09/0.25 tff(f43,plain,(
% 0.09/0.25 ~x | (bG0 != $true)),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f29])).
% 0.09/0.25 tff(f44,plain,(
% 0.09/0.25 (bG0 = $true) | x),
% 0.09/0.25 inference(consistent_polarity_flipping,[],[f28])).
% 0.09/0.25 tff(f46,definition,(
% 0.09/0.25 spl6_1 <=> x),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition])).
% 0.09/0.25 tff(f50,definition,(
% 0.09/0.25 spl6_2 <=> (bG0 = $true)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition])).
% 0.09/0.25 tff(f51,plain,(
% 0.09/0.25 (bG0 != $true) | spl6_2),
% 0.09/0.25 inference(avatar_component_clause,[],[f50])).
% 0.09/0.25 tff(f52,plain,(
% 0.09/0.25 (bG0 = $true) | ~spl6_2),
% 0.09/0.25 inference(avatar_component_clause,[],[f50])).
% 0.09/0.25 tff(f53,plain,(
% 0.09/0.25 spl6_1 | spl6_2),
% 0.09/0.25 inference(avatar_split_clause,[],[f44,f50,f46])).
% 0.09/0.25 tff(f54,plain,(
% 0.09/0.25 ~spl6_2 | ~spl6_1),
% 0.09/0.25 inference(avatar_split_clause,[],[f43,f46,f50])).
% 0.09/0.25 tff(f56,definition,(
% 0.09/0.25 spl6_3 <=> f(bG0)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition])).
% 0.09/0.25 tff(f57,plain,(
% 0.09/0.25 ~f(bG0) | spl6_3),
% 0.09/0.25 inference(avatar_component_clause,[],[f56])).
% 0.09/0.25 tff(f58,plain,(
% 0.09/0.25 f(bG0) | ~spl6_3),
% 0.09/0.25 inference(avatar_component_clause,[],[f56])).
% 0.09/0.25 tff(f60,definition,(
% 0.09/0.25 spl6_4 <=> ($true = bG1)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_4])],[avatar_definition])).
% 0.09/0.25 tff(f61,plain,(
% 0.09/0.25 ($true != bG1) | spl6_4),
% 0.09/0.25 inference(avatar_component_clause,[],[f60])).
% 0.09/0.25 tff(f62,plain,(
% 0.09/0.25 ($true = bG1) | ~spl6_4),
% 0.09/0.25 inference(avatar_component_clause,[],[f60])).
% 0.09/0.25 tff(f63,plain,(
% 0.09/0.25 spl6_3 | spl6_4),
% 0.09/0.25 inference(avatar_split_clause,[],[f42,f60,f56])).
% 0.09/0.25 tff(f64,plain,(
% 0.09/0.25 ~spl6_4 | ~spl6_3),
% 0.09/0.25 inference(avatar_split_clause,[],[f41,f56,f60])).
% 0.09/0.25 tff(f66,definition,(
% 0.09/0.25 spl6_5 <=> f(bG1)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_5])],[avatar_definition])).
% 0.09/0.25 tff(f67,plain,(
% 0.09/0.25 ~f(bG1) | spl6_5),
% 0.09/0.25 inference(avatar_component_clause,[],[f66])).
% 0.09/0.25 tff(f68,plain,(
% 0.09/0.25 f(bG1) | ~spl6_5),
% 0.09/0.25 inference(avatar_component_clause,[],[f66])).
% 0.09/0.25 tff(f70,definition,(
% 0.09/0.25 spl6_6 <=> ($true = bG2)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_6])],[avatar_definition])).
% 0.09/0.25 tff(f71,plain,(
% 0.09/0.25 ($true != bG2) | spl6_6),
% 0.09/0.25 inference(avatar_component_clause,[],[f70])).
% 0.09/0.25 tff(f72,plain,(
% 0.09/0.25 ($true = bG2) | ~spl6_6),
% 0.09/0.25 inference(avatar_component_clause,[],[f70])).
% 0.09/0.25 tff(f73,plain,(
% 0.09/0.25 spl6_5 | spl6_6),
% 0.09/0.25 inference(avatar_split_clause,[],[f40,f70,f66])).
% 0.09/0.25 tff(f74,plain,(
% 0.09/0.25 ~spl6_6 | ~spl6_5),
% 0.09/0.25 inference(avatar_split_clause,[],[f39,f66,f70])).
% 0.09/0.25 tff(f76,definition,(
% 0.09/0.25 spl6_7 <=> f(bG2)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_7])],[avatar_definition])).
% 0.09/0.25 tff(f77,plain,(
% 0.09/0.25 ~f(bG2) | spl6_7),
% 0.09/0.25 inference(avatar_component_clause,[],[f76])).
% 0.09/0.25 tff(f78,plain,(
% 0.09/0.25 f(bG2) | ~spl6_7),
% 0.09/0.25 inference(avatar_component_clause,[],[f76])).
% 0.09/0.25 tff(f80,definition,(
% 0.09/0.25 spl6_8 <=> ($true = bG3)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_8])],[avatar_definition])).
% 0.09/0.25 tff(f81,plain,(
% 0.09/0.25 ($true != bG3) | spl6_8),
% 0.09/0.25 inference(avatar_component_clause,[],[f80])).
% 0.09/0.25 tff(f82,plain,(
% 0.09/0.25 ($true = bG3) | ~spl6_8),
% 0.09/0.25 inference(avatar_component_clause,[],[f80])).
% 0.09/0.25 tff(f83,plain,(
% 0.09/0.25 spl6_7 | spl6_8),
% 0.09/0.25 inference(avatar_split_clause,[],[f38,f80,f76])).
% 0.09/0.25 tff(f84,plain,(
% 0.09/0.25 ~spl6_8 | ~spl6_7),
% 0.09/0.25 inference(avatar_split_clause,[],[f37,f76,f80])).
% 0.09/0.25 tff(f86,definition,(
% 0.09/0.25 spl6_9 <=> ($true = bG4)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_9])],[avatar_definition])).
% 0.09/0.25 tff(f87,plain,(
% 0.09/0.25 ($true != bG4) | spl6_9),
% 0.09/0.25 inference(avatar_component_clause,[],[f86])).
% 0.09/0.25 tff(f88,plain,(
% 0.09/0.25 ($true = bG4) | ~spl6_9),
% 0.09/0.25 inference(avatar_component_clause,[],[f86])).
% 0.09/0.25 tff(f89,plain,(
% 0.09/0.25 spl6_1 | spl6_9),
% 0.09/0.25 inference(avatar_split_clause,[],[f36,f86,f46])).
% 0.09/0.25 tff(f90,plain,(
% 0.09/0.25 ~spl6_9 | ~spl6_1),
% 0.09/0.25 inference(avatar_split_clause,[],[f35,f46,f86])).
% 0.09/0.25 tff(f92,definition,(
% 0.09/0.25 spl6_10 <=> f(bG4)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_10])],[avatar_definition])).
% 0.09/0.25 tff(f93,plain,(
% 0.09/0.25 ~f(bG4) | spl6_10),
% 0.09/0.25 inference(avatar_component_clause,[],[f92])).
% 0.09/0.25 tff(f94,plain,(
% 0.09/0.25 f(bG4) | ~spl6_10),
% 0.09/0.25 inference(avatar_component_clause,[],[f92])).
% 0.09/0.25 tff(f96,definition,(
% 0.09/0.25 spl6_11 <=> ($true = bG5)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_11])],[avatar_definition])).
% 0.09/0.25 tff(f97,plain,(
% 0.09/0.25 ($true != bG5) | spl6_11),
% 0.09/0.25 inference(avatar_component_clause,[],[f96])).
% 0.09/0.25 tff(f98,plain,(
% 0.09/0.25 ($true = bG5) | ~spl6_11),
% 0.09/0.25 inference(avatar_component_clause,[],[f96])).
% 0.09/0.25 tff(f99,plain,(
% 0.09/0.25 spl6_10 | spl6_11),
% 0.09/0.25 inference(avatar_split_clause,[],[f34,f96,f92])).
% 0.09/0.25 tff(f100,plain,(
% 0.09/0.25 ~spl6_11 | ~spl6_10),
% 0.09/0.25 inference(avatar_split_clause,[],[f33,f92,f96])).
% 0.09/0.25 tff(f102,plain,(
% 0.09/0.25 f($true) | (~spl6_9 | ~spl6_10)),
% 0.09/0.25 inference(superposition,[],[f94,f88])).
% 0.09/0.25 tff(f106,plain,(
% 0.09/0.25 f($true) | (bG0 = $false) | ~spl6_3),
% 0.09/0.25 inference(superposition,[],[f58,f32])).
% 0.09/0.25 tff(f107,plain,(
% 0.09/0.25 ($true != $true) | (bG1 = $false) | spl6_4),
% 0.09/0.25 inference(superposition,[],[f61,f32])).
% 0.09/0.25 tff(f109,plain,(
% 0.09/0.25 ($true != $true) | (bG2 = $false) | spl6_6),
% 0.09/0.25 inference(superposition,[],[f71,f32])).
% 0.09/0.25 tff(f110,plain,(
% 0.09/0.25 f($true) | (bG2 = $false) | ~spl6_7),
% 0.09/0.25 inference(superposition,[],[f78,f32])).
% 0.09/0.25 tff(f111,plain,(
% 0.09/0.25 ($true != $true) | (bG3 = $false) | spl6_8),
% 0.09/0.25 inference(superposition,[],[f81,f32])).
% 0.09/0.25 tff(f113,plain,(
% 0.09/0.25 ($true != $true) | (bG5 = $false) | spl6_11),
% 0.09/0.25 inference(superposition,[],[f97,f32])).
% 0.09/0.25 tff(f116,plain,(
% 0.09/0.25 (bG5 = $false) | spl6_11),
% 0.09/0.25 inference(trivial_inequality_removal,[],[f113])).
% 0.09/0.25 tff(f117,plain,(
% 0.09/0.25 (bG3 = $false) | spl6_8),
% 0.09/0.25 inference(trivial_inequality_removal,[],[f111])).
% 0.09/0.25 tff(f118,plain,(
% 0.09/0.25 (bG2 = $false) | spl6_6),
% 0.09/0.25 inference(trivial_inequality_removal,[],[f109])).
% 0.09/0.25 tff(f119,plain,(
% 0.09/0.25 (bG1 = $false) | spl6_4),
% 0.09/0.25 inference(trivial_inequality_removal,[],[f107])).
% 0.09/0.25 tff(f121,definition,(
% 0.09/0.25 spl6_12 <=> (bG5 = $false)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_12])],[avatar_definition])).
% 0.09/0.25 tff(f123,plain,(
% 0.09/0.25 (bG5 = $false) | ~spl6_12),
% 0.09/0.25 inference(avatar_component_clause,[],[f121])).
% 0.09/0.25 tff(f125,definition,(
% 0.09/0.25 spl6_13 <=> h(bG3) = h($true)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_13])],[avatar_definition])).
% 0.09/0.25 tff(f127,plain,(
% 0.09/0.25 h(bG3) != h($true) | spl6_13),
% 0.09/0.25 inference(avatar_component_clause,[],[f125])).
% 0.09/0.25 tff(f129,plain,(
% 0.09/0.25 spl6_12 | spl6_11),
% 0.09/0.25 inference(avatar_split_clause,[],[f116,f96,f121])).
% 0.09/0.25 tff(f131,plain,(
% 0.09/0.25 h($true) != h($true) | (bG3 = $false) | spl6_13),
% 0.09/0.25 inference(superposition,[],[f127,f32])).
% 0.09/0.25 tff(f132,plain,(
% 0.09/0.25 (bG3 = $false) | spl6_13),
% 0.09/0.25 inference(trivial_inequality_removal,[],[f131])).
% 0.09/0.25 tff(f133,plain,(
% 0.09/0.25 ~f($true) | (~spl6_9 | spl6_10)),
% 0.09/0.25 inference(superposition,[],[f93,f88])).
% 0.09/0.25 tff(f136,definition,(
% 0.09/0.25 spl6_14 <=> (bG4 = $false)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_14])],[avatar_definition])).
% 0.09/0.25 tff(f138,plain,(
% 0.09/0.25 (bG4 = $false) | ~spl6_14),
% 0.09/0.25 inference(avatar_component_clause,[],[f136])).
% 0.09/0.25 tff(f140,definition,(
% 0.09/0.25 spl6_15 <=> f($true)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_15])],[avatar_definition])).
% 0.09/0.25 tff(f144,plain,(
% 0.09/0.25 ~spl6_15 | ~spl6_9 | spl6_10),
% 0.09/0.25 inference(avatar_split_clause,[],[f133,f92,f86,f140])).
% 0.09/0.25 tff(f146,plain,(
% 0.09/0.25 h(bG3) != h($true) | ~spl6_11),
% 0.09/0.25 inference(superposition,[],[f30,f98])).
% 0.09/0.25 tff(f151,definition,(
% 0.09/0.25 spl6_16 <=> (bG0 = $false)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_16])],[avatar_definition])).
% 0.09/0.25 tff(f153,plain,(
% 0.09/0.25 (bG0 = $false) | ~spl6_16),
% 0.09/0.25 inference(avatar_component_clause,[],[f151])).
% 0.09/0.25 tff(f154,plain,(
% 0.09/0.25 spl6_16 | spl6_15 | ~spl6_3),
% 0.09/0.25 inference(avatar_split_clause,[],[f106,f56,f140,f151])).
% 0.09/0.25 tff(f156,definition,(
% 0.09/0.25 spl6_17 <=> (bG1 = $false)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_17])],[avatar_definition])).
% 0.09/0.25 tff(f158,plain,(
% 0.09/0.25 (bG1 = $false) | ~spl6_17),
% 0.09/0.25 inference(avatar_component_clause,[],[f156])).
% 0.09/0.25 tff(f163,definition,(
% 0.09/0.25 spl6_18 <=> (bG2 = $false)),
% 0.09/0.25 introduced(definition,[new_symbols(definition,[spl6_18])],[avatar_definition])).
% 0.09/0.25 tff(f165,plain,(
% 0.09/0.25 (bG2 = $false) | ~spl6_18),
% 0.09/0.25 inference(avatar_component_clause,[],[f163])).
% 0.09/0.25 tff(f166,plain,(
% 0.09/0.25 spl6_18 | spl6_15 | ~spl6_7),
% 0.09/0.25 inference(avatar_split_clause,[],[f110,f76,f140,f163])).
% 0.09/0.25 tff(f173,plain,(
% 0.09/0.25 ~f($true) | (bG2 = $false) | spl6_7),
% 0.09/0.25 inference(superposition,[],[f77,f32])).
% 0.09/0.25 tff(f175,plain,(
% 0.09/0.25 ($true != $true) | (bG0 = $false) | spl6_2),
% 0.09/0.25 inference(superposition,[],[f51,f32])).
% 0.09/0.25 tff(f176,plain,(
% 0.09/0.25 (bG0 = $false) | spl6_2),
% 0.09/0.25 inference(trivial_inequality_removal,[],[f175])).
% 0.09/0.25 tff(f177,plain,(
% 0.09/0.25 spl6_16 | spl6_2),
% 0.09/0.25 inference(avatar_split_clause,[],[f176,f50,f151])).
% 0.09/0.25 tff(f178,plain,(
% 0.09/0.25 ~f($true) | (~spl6_4 | spl6_5)),
% 0.09/0.25 inference(superposition,[],[f67,f62])).
% 0.09/0.25 tff(f179,plain,(
% 0.09/0.25 ~f($true) | (~spl6_6 | spl6_7)),
% 0.09/0.25 inference(superposition,[],[f77,f72])).
% 0.09/0.25 tff(f180,plain,(
% 0.09/0.25 ($true = $false) | (~spl6_8 | spl6_13)),
% 0.09/0.25 inference(superposition,[],[f82,f132])).
% 0.09/0.25 tff(f187,plain,(
% 0.09/0.25 $false | (~spl6_8 | spl6_13)),
% 0.09/0.25 inference(trivial_inequality_removal,[],[f180])).
% 0.09/0.25 tff(f188,plain,(
% 0.09/0.25 ~spl6_8 | spl6_13),
% 0.09/0.25 inference(avatar_contradiction_clause,[],[f187])).
% 0.09/0.25 tff(f189,plain,(
% 0.09/0.25 ~spl6_13 | ~spl6_11),
% 0.09/0.25 inference(avatar_split_clause,[],[f146,f96,f125])).
% 0.09/0.25 tff(f191,plain,(
% 0.09/0.25 h(bG3) != h($false) | ~spl6_12),
% 0.09/0.25 inference(superposition,[],[f30,f123])).
% 0.09/0.25 tff(f200,plain,(
% 0.09/0.25 ($true != $true) | (bG4 = $false) | spl6_9),
% 0.09/0.25 inference(superposition,[],[f87,f32])).
% 0.09/0.25 tff(f201,plain,(
% 0.09/0.25 (bG4 = $false) | spl6_9),
% 0.09/0.25 inference(trivial_inequality_removal,[],[f200])).
% 0.09/0.25 tff(f207,plain,(
% 0.09/0.25 f($false) | (~spl6_10 | ~spl6_14)),
% 0.09/0.25 inference(superposition,[],[f94,f138])).
% 0.09/0.25 tff(f211,plain,(
% 0.09/0.25 ~f($false) | (spl6_3 | ~spl6_16)),
% 0.09/0.25 inference(superposition,[],[f57,f153])).
% 0.09/0.25 tff(f217,plain,(
% 0.09/0.25 $false | (spl6_3 | ~spl6_10 | ~spl6_14 | ~spl6_16)),
% 0.09/0.25 inference(resolution,[],[f211,f207])).
% 0.09/0.25 tff(f218,plain,(
% 0.09/0.25 spl6_3 | ~spl6_10 | ~spl6_14 | ~spl6_16),
% 0.09/0.25 inference(avatar_contradiction_clause,[],[f217])).
% 0.09/0.25 tff(f219,plain,(
% 0.09/0.25 spl6_17 | spl6_4),
% 0.09/0.25 inference(avatar_split_clause,[],[f119,f60,f156])).
% 0.09/0.25 tff(f220,plain,(
% 0.09/0.25 spl6_15 | ~spl6_9 | ~spl6_10),
% 0.09/0.25 inference(avatar_split_clause,[],[f102,f92,f86,f140])).
% 0.09/0.25 tff(f221,plain,(
% 0.09/0.25 spl6_14 | spl6_9),
% 0.09/0.25 inference(avatar_split_clause,[],[f201,f86,f136])).
% 0.09/0.25 tff(f224,plain,(
% 0.09/0.25 spl6_18 | ~spl6_15 | spl6_7),
% 0.09/0.25 inference(avatar_split_clause,[],[f173,f76,f140,f163])).
% 0.09/0.25 tff(f225,plain,(
% 0.09/0.25 ~spl6_15 | ~spl6_6 | spl6_7),
% 0.09/0.25 inference(avatar_split_clause,[],[f179,f76,f70,f140])).
% 0.09/0.25 tff(f226,plain,(
% 0.09/0.25 ~spl6_15 | ~spl6_4 | spl6_5),
% 0.09/0.25 inference(avatar_split_clause,[],[f178,f66,f60,f140])).
% 0.09/0.25 tff(f227,plain,(
% 0.09/0.25 spl6_18 | spl6_6),
% 0.09/0.25 inference(avatar_split_clause,[],[f118,f70,f163])).
% 0.09/0.25 tff(f231,plain,(
% 0.09/0.25 ~f($true) | (~spl6_2 | spl6_3)),
% 0.09/0.25 inference(superposition,[],[f57,f52])).
% 0.09/0.25 tff(f232,plain,(
% 0.09/0.25 ~spl6_15 | ~spl6_2 | spl6_3),
% 0.09/0.25 inference(avatar_split_clause,[],[f231,f56,f50,f140])).
% 0.09/0.25 tff(f242,plain,(
% 0.09/0.25 ($true = $false) | (~spl6_2 | ~spl6_16)),
% 0.09/0.25 inference(superposition,[],[f153,f52])).
% 0.09/0.25 tff(f244,plain,(
% 0.09/0.25 f($false) | (~spl6_3 | ~spl6_16)),
% 0.09/0.25 inference(superposition,[],[f58,f153])).
% 0.09/0.25 tff(f249,plain,(
% 0.09/0.25 $false | (~spl6_2 | ~spl6_16)),
% 0.09/0.25 inference(trivial_inequality_removal,[],[f242])).
% 0.09/0.25 tff(f250,plain,(
% 0.09/0.25 ~spl6_2 | ~spl6_16),
% 0.09/0.25 inference(avatar_contradiction_clause,[],[f249])).
% 0.09/0.25 tff(f255,plain,(
% 0.09/0.25 f($false) | (~spl6_5 | ~spl6_17)),
% 0.09/0.25 inference(superposition,[],[f68,f158])).
% 0.09/0.25 tff(f259,plain,(
% 0.09/0.25 ~f($false) | (spl6_7 | ~spl6_18)),
% 0.09/0.25 inference(superposition,[],[f77,f165])).
% 0.09/0.25 tff(f261,plain,(
% 0.09/0.25 $false | (~spl6_5 | spl6_7 | ~spl6_17 | ~spl6_18)),
% 0.09/0.25 inference(resolution,[],[f259,f255])).
% 0.09/0.25 tff(f262,plain,(
% 0.09/0.25 ~spl6_5 | spl6_7 | ~spl6_17 | ~spl6_18),
% 0.09/0.25 inference(avatar_contradiction_clause,[],[f261])).
% 0.09/0.25 tff(f263,plain,(
% 0.09/0.25 ~f($false) | (spl6_5 | ~spl6_17)),
% 0.09/0.25 inference(superposition,[],[f67,f158])).
% 0.09/0.25 tff(f268,plain,(
% 0.09/0.25 ($true = $false) | (~spl6_6 | ~spl6_18)),
% 0.09/0.25 inference(superposition,[],[f72,f165])).
% 0.09/0.25 tff(f273,plain,(
% 0.09/0.25 $false | (~spl6_6 | ~spl6_18)),
% 0.09/0.25 inference(trivial_inequality_removal,[],[f268])).
% 0.09/0.25 tff(f274,plain,(
% 0.09/0.25 ~spl6_6 | ~spl6_18),
% 0.09/0.25 inference(avatar_contradiction_clause,[],[f273])).
% 0.09/0.25 tff(f277,plain,(
% 0.09/0.25 f($false) | (~spl6_7 | ~spl6_18)),
% 0.09/0.25 inference(superposition,[],[f78,f165])).
% 0.09/0.25 tff(f288,plain,(
% 0.09/0.25 h($false) != h($false) | (spl6_8 | ~spl6_12)),
% 0.09/0.25 inference(superposition,[],[f191,f117])).
% 0.09/0.25 tff(f290,plain,(
% 0.09/0.25 $false | (spl6_8 | ~spl6_12)),
% 0.09/0.25 inference(trivial_inequality_removal,[],[f288])).
% 0.09/0.25 tff(f291,plain,(
% 0.09/0.25 spl6_8 | ~spl6_12),
% 0.09/0.25 inference(avatar_contradiction_clause,[],[f290])).
% 0.09/0.25 tff(f303,plain,(
% 0.09/0.25 ~f($false) | (spl6_10 | ~spl6_14)),
% 0.09/0.25 inference(superposition,[],[f93,f138])).
% 0.09/0.25 tff(f310,plain,(
% 0.09/0.25 $false | (~spl6_3 | spl6_10 | ~spl6_14 | ~spl6_16)),
% 0.09/0.25 inference(resolution,[],[f303,f244])).
% 0.09/0.25 tff(f311,plain,(
% 0.09/0.25 ~spl6_3 | spl6_10 | ~spl6_14 | ~spl6_16),
% 0.09/0.25 inference(avatar_contradiction_clause,[],[f310])).
% 0.09/0.25 tff(f315,plain,(
% 0.09/0.25 f($true) | (~spl6_4 | ~spl6_5)),
% 0.09/0.25 inference(superposition,[],[f68,f62])).
% 0.09/0.25 tff(f321,plain,(
% 0.09/0.25 spl6_15 | ~spl6_4 | ~spl6_5),
% 0.09/0.25 inference(avatar_split_clause,[],[f315,f66,f60,f140])).
% 0.09/0.25 tff(f347,plain,(
% 0.09/0.25 $false | (~spl6_3 | spl6_5 | ~spl6_16 | ~spl6_17)),
% 0.09/0.25 inference(resolution,[],[f263,f244])).
% 0.09/0.25 tff(f348,plain,(
% 0.09/0.25 ~spl6_3 | spl6_5 | ~spl6_16 | ~spl6_17),
% 0.09/0.25 inference(avatar_contradiction_clause,[],[f347])).
% 0.09/0.25 tff(f378,plain,(
% 0.09/0.25 $false | (spl6_3 | ~spl6_7 | ~spl6_16 | ~spl6_18)),
% 0.09/0.25 inference(resolution,[],[f277,f211])).
% 0.09/0.25 tff(f379,plain,(
% 0.09/0.25 spl6_3 | ~spl6_7 | ~spl6_16 | ~spl6_18),
% 0.09/0.25 inference(avatar_contradiction_clause,[],[f378])).
% 0.09/0.25 cnf(s1, plain, spl6_1 | spl6_2, inference(sat_conversion,[],[f53])).
% 0.09/0.25 cnf(s2, plain, ~spl6_1 | ~spl6_2, inference(sat_conversion,[],[f54])).
% 0.09/0.25 cnf(s3, plain, spl6_3 | spl6_4, inference(sat_conversion,[],[f63])).
% 0.09/0.25 cnf(s4, plain, ~spl6_3 | ~spl6_4, inference(sat_conversion,[],[f64])).
% 0.09/0.25 cnf(s5, plain, spl6_5 | spl6_6, inference(sat_conversion,[],[f73])).
% 0.09/0.25 cnf(s6, plain, ~spl6_5 | ~spl6_6, inference(sat_conversion,[],[f74])).
% 0.09/0.25 cnf(s7, plain, spl6_7 | spl6_8, inference(sat_conversion,[],[f83])).
% 0.09/0.25 cnf(s8, plain, ~spl6_7 | ~spl6_8, inference(sat_conversion,[],[f84])).
% 0.09/0.25 cnf(s9, plain, spl6_1 | spl6_9, inference(sat_conversion,[],[f89])).
% 0.09/0.25 cnf(s10, plain, ~spl6_1 | ~spl6_9, inference(sat_conversion,[],[f90])).
% 0.09/0.25 cnf(s11, plain, spl6_10 | spl6_11, inference(sat_conversion,[],[f99])).
% 0.09/0.25 cnf(s12, plain, ~spl6_10 | ~spl6_11, inference(sat_conversion,[],[f100])).
% 0.09/0.25 cnf(s14, plain, spl6_11 | spl6_12, inference(sat_conversion,[],[f129])).
% 0.09/0.25 cnf(s16, plain, ~spl6_9 | spl6_10 | ~spl6_15, inference(sat_conversion,[],[f144])).
% 0.09/0.25 cnf(s18, plain, ~spl6_3 | spl6_15 | spl6_16, inference(sat_conversion,[],[f154])).
% 0.09/0.25 cnf(s21, plain, ~spl6_7 | spl6_15 | spl6_18, inference(sat_conversion,[],[f166])).
% 0.09/0.25 cnf(s22, plain, spl6_2 | spl6_16, inference(sat_conversion,[],[f177])).
% 0.09/0.25 cnf(s25, plain, ~spl6_8 | spl6_13, inference(sat_conversion,[],[f188])).
% 0.09/0.25 cnf(s26, plain, ~spl6_11 | ~spl6_13, inference(sat_conversion,[],[f189])).
% 0.09/0.25 cnf(s27, plain, spl6_3 | ~spl6_10 | ~spl6_14 | ~spl6_16, inference(sat_conversion,[],[f218])).
% 0.09/0.25 cnf(s28, plain, spl6_4 | spl6_17, inference(sat_conversion,[],[f219])).
% 0.09/0.25 cnf(s29, plain, ~spl6_9 | ~spl6_10 | spl6_15, inference(sat_conversion,[],[f220])).
% 0.09/0.25 cnf(s31, plain, spl6_9 | spl6_14, inference(sat_conversion,[],[f221])).
% 0.09/0.25 cnf(s35, plain, spl6_7 | ~spl6_15 | spl6_18, inference(sat_conversion,[],[f224])).
% 0.09/0.25 cnf(s36, plain, ~spl6_6 | spl6_7 | ~spl6_15, inference(sat_conversion,[],[f225])).
% 0.09/0.25 cnf(s37, plain, ~spl6_4 | spl6_5 | ~spl6_15, inference(sat_conversion,[],[f226])).
% 0.09/0.25 cnf(s38, plain, spl6_6 | spl6_18, inference(sat_conversion,[],[f227])).
% 0.09/0.25 cnf(s39, plain, ~spl6_2 | spl6_3 | ~spl6_15, inference(sat_conversion,[],[f232])).
% 0.09/0.25 cnf(s42, plain, ~spl6_2 | ~spl6_16, inference(sat_conversion,[],[f250])).
% 0.09/0.25 cnf(s43, plain, ~spl6_5 | spl6_7 | ~spl6_17 | ~spl6_18, inference(sat_conversion,[],[f262])).
% 0.09/0.25 cnf(s48, plain, ~spl6_6 | ~spl6_18, inference(sat_conversion,[],[f274])).
% 0.09/0.25 cnf(s49, plain, spl6_8 | ~spl6_12, inference(sat_conversion,[],[f291])).
% 0.09/0.25 cnf(s50, plain, ~spl6_3 | spl6_10 | ~spl6_14 | ~spl6_16, inference(sat_conversion,[],[f311])).
% 0.09/0.25 cnf(s53, plain, ~spl6_4 | ~spl6_5 | spl6_15, inference(sat_conversion,[],[f321])).
% 0.09/0.25 cnf(s56, plain, ~spl6_3 | spl6_5 | ~spl6_16 | ~spl6_17, inference(sat_conversion,[],[f348])).
% 0.09/0.25 cnf(s61, plain, spl6_3 | ~spl6_7 | ~spl6_16 | ~spl6_18, inference(sat_conversion,[],[f379])).
% 0.09/0.25 cnf(s62, plain, spl6_3 | spl6_1, inference(rat,[],[s7,s21,s25,s48,s26,s5,s11,s53,s29,s3,s39,s9,s1])).
% 0.09/0.25 cnf(s63, plain, spl6_1, inference(rat,[],[s5,s43,s36,s35,s8,s49,s14,s12,s16,s28,s18,s4,s62,s42,s1,s9])).
% 0.09/0.25 cnf(s64, plain, ~spl6_9, inference(rat,[],[s10,s63])).
% 0.09/0.25 cnf(s65, plain, ~spl6_2, inference(rat,[],[s2,s63])).
% 0.09/0.25 cnf(s66, plain, spl6_14, inference(rat,[],[s31,s64])).
% 0.09/0.25 cnf(s67, plain, spl6_16, inference(rat,[],[s22,s65])).
% 0.09/0.25 cnf(s68, plain, spl6_3, inference(rat,[],[s37,s6,s21,s38,s61,s7,s25,s26,s11,s27,s3,s67,s66])).
% 0.09/0.25 cnf(s69, plain, ~spl6_4, inference(rat,[],[s4,s68])).
% 0.09/0.25 cnf(s70, plain, spl6_10, inference(rat,[],[s50,s66,s67,s68])).
% 0.09/0.25 cnf(s71, plain, spl6_17, inference(rat,[],[s28,s69])).
% 0.09/0.25 cnf(s72, plain, ~spl6_11, inference(rat,[],[s12,s70])).
% 0.09/0.25 cnf(s73, plain, spl6_5, inference(rat,[],[s56,s68,s67,s71])).
% 0.09/0.25 cnf(s74, plain, spl6_12, inference(rat,[],[s14,s72])).
% 0.09/0.25 cnf(s75, plain, ~spl6_6, inference(rat,[],[s6,s73])).
% 0.09/0.25 cnf(s76, plain, spl6_8, inference(rat,[],[s49,s74])).
% 0.09/0.25 cnf(s77, plain, spl6_18, inference(rat,[],[s38,s75])).
% 0.09/0.25 cnf(s79, plain, ~spl6_7, inference(rat,[],[s8,s76])).
% 0.09/0.25 cnf(s80, plain, $false, inference(rat,[],[s43,s73,s71,s79,s77])).
% 0.09/0.25 tff(f380,plain,(
% 0.09/0.25 $false),
% 0.09/0.25 inference(avatar_sat_refutation,[],[s80])).
% 0.09/0.25 % SZS output end Proof for theBenchmark
% 0.09/0.25 % (1338344)------------------------------
% 0.09/0.25 % (1338344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.25 % (1338344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.25 % (1338344)CaDiCaL version: 2.1.3
% 0.09/0.25 % (1338344)Termination reason: Refutation
% 0.09/0.25 % (1338344)Time elapsed: 0.005 s
% 0.09/0.25 % (1338344)Peak memory usage: 12 MB
% 0.09/0.25 % (1338344)Instructions burned: 11 (million)
% 0.09/0.25 % (1338319)Success in time 0.037 s
% 0.09/0.25 % Vampire exiting
%------------------------------------------------------------------------------