%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO041_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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:29:38 PM UTC 2026
% Result : Theorem 0.08s 0.25s
% Output : Refutation 0.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO041_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.08/0.18 % Computer : n003.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 17:24:43 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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.08/0.25 % (1763509)Will run a generic schedule for satisfiability detection.
% 0.08/0.25 % (1763516)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3148182733:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.08/0.25 % (1763515)% WARNING: option uhcvi not known.
% 0.08/0.25 % (1763516) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1763509-1763516"...
% 0.08/0.25 % (1763514)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1186270999_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.25 % (1763517)dis+10_1_sil=32000:sp=arity:random_seed=2785491512:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.08/0.25 % (1763515)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=792354502:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.08/0.25 % (1763519)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3895185867:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.08/0.25 % (1763518)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4171911839:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.08/0.25 % (1763520)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4124028980:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.08/0.25 % (1763516)...printing done.
% 0.08/0.25 % Detected minimum model sizes of [1]
% 0.08/0.25 % Detected maximum model sizes of [9]
% 0.08/0.25 % TRYING [1]
% 0.08/0.25 % TRYING [2]
% 0.08/0.25 % (1763515) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1763509-1763515"...
% 0.08/0.25 % (1763516)Refutation found. Thanks to Tanya!
% 0.08/0.25 % SZS status Theorem for theBenchmark
% 0.08/0.25 % SZS output start Proof for theBenchmark
% 0.08/0.25 tff(func_def_0, type, bG0: $o).
% 0.08/0.25 tff(func_def_3, type, bG1: $o).
% 0.08/0.25 tff(func_def_4, type, bG2: $o).
% 0.08/0.25 tff(func_def_5, type, bG3: $o).
% 0.08/0.25 tff(func_def_6, type, bG4: $o).
% 0.08/0.25 tff(func_def_7, type, bG5: $o).
% 0.08/0.25 tff(func_def_8, type, bG6: $o).
% 0.08/0.25 tff(pred_def_2, type, f: $o > $o).
% 0.08/0.25 tff(pred_def_3, type, g: $o > $o).
% 0.08/0.25 tff(f1,conjecture,(
% 0.08/0.25 ~((x != y) & (g(x) = y) & (g(y) = x) & (f(f(f(x))) = g(f(x))))),
% 0.08/0.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p',3)).
% 0.08/0.25 tff(f2,negated_conjecture,(
% 0.08/0.25 ~ ~((x != y) & (g(x) = y) & (g(y) = x) & (f(f(f(x))) = g(f(x))))),
% 0.08/0.25 inference(negated_conjecture,[status(cth)],[f1])).
% 0.08/0.25 tff(f3,definition,(
% 0.08/0.25 x <=> (bG0 = $true)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[bG0])],[fool_formula_definition])).
% 0.08/0.25 tff(f4,definition,(
% 0.08/0.25 f(bG0) <=> ($true = bG1)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[bG1])],[fool_formula_definition])).
% 0.08/0.25 tff(f5,definition,(
% 0.08/0.25 f(bG1) <=> ($true = bG2)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[bG2])],[fool_formula_definition])).
% 0.08/0.25 tff(f6,definition,(
% 0.08/0.25 x <=> ($true = bG3)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[bG3])],[fool_formula_definition])).
% 0.08/0.25 tff(f7,definition,(
% 0.08/0.25 f(bG3) <=> ($true = bG4)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[bG4])],[fool_formula_definition])).
% 0.08/0.25 tff(f8,definition,(
% 0.08/0.25 y <=> ($true = bG5)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[bG5])],[fool_formula_definition])).
% 0.08/0.25 tff(f9,definition,(
% 0.08/0.25 x <=> ($true = bG6)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[bG6])],[fool_formula_definition])).
% 0.08/0.25 tff(f10,plain,(
% 0.08/0.25 ~ ~((x <~> y) & (g(bG6) <=> y) & (g(bG5) <=> x) & (f(bG2) <=> g(bG4)))),
% 0.08/0.25 inference(fool_elimination,[],[f2,f9,f8,f7,f6,f5,f4,f3])).
% 0.08/0.25 tff(f11,plain,(
% 0.08/0.25 (x <~> y) & (g(bG6) <=> y) & (g(bG5) <=> x) & (f(bG2) <=> g(bG4))),
% 0.08/0.25 inference(flattening,[],[f10])).
% 0.08/0.25 tff(f12,plain,(
% 0.08/0.25 (x | ($true != bG6)) & (($true = bG6) | ~x)),
% 0.08/0.25 inference(nnf_transformation,[],[f9])).
% 0.08/0.25 tff(f13,plain,(
% 0.08/0.25 (y | ($true != bG5)) & (($true = bG5) | ~y)),
% 0.08/0.25 inference(nnf_transformation,[],[f8])).
% 0.08/0.25 tff(f14,plain,(
% 0.08/0.25 (f(bG3) | ($true != bG4)) & (($true = bG4) | ~f(bG3))),
% 0.08/0.25 inference(nnf_transformation,[],[f7])).
% 0.08/0.25 tff(f15,plain,(
% 0.08/0.25 (x | ($true != bG3)) & (($true = bG3) | ~x)),
% 0.08/0.25 inference(nnf_transformation,[],[f6])).
% 0.08/0.25 tff(f16,plain,(
% 0.08/0.25 (f(bG1) | ($true != bG2)) & (($true = bG2) | ~f(bG1))),
% 0.08/0.25 inference(nnf_transformation,[],[f5])).
% 0.08/0.25 tff(f17,plain,(
% 0.08/0.25 (f(bG0) | ($true != bG1)) & (($true = bG1) | ~f(bG0))),
% 0.08/0.25 inference(nnf_transformation,[],[f4])).
% 0.08/0.25 tff(f18,plain,(
% 0.08/0.25 (x | (bG0 != $true)) & ((bG0 = $true) | ~x)),
% 0.08/0.25 inference(nnf_transformation,[],[f3])).
% 0.08/0.25 tff(f19,plain,(
% 0.08/0.25 ((~y | ~x) & (y | x)) & ((g(bG6) | ~y) & (y | ~g(bG6))) & ((g(bG5) | ~x) & (x | ~g(bG5))) & ((f(bG2) | ~g(bG4)) & (g(bG4) | ~f(bG2)))),
% 0.08/0.25 inference(nnf_transformation,[],[f11])).
% 0.08/0.25 tff(f20,plain,(
% 0.08/0.25 (~y | ~x) & (y | x) & (g(bG6) | ~y) & (y | ~g(bG6)) & (g(bG5) | ~x) & (x | ~g(bG5)) & (f(bG2) | ~g(bG4)) & (g(bG4) | ~f(bG2))),
% 0.08/0.25 inference(flattening,[],[f19])).
% 0.08/0.25 tff(f21,plain,(
% 0.08/0.25 ($true = bG6) | ~x),
% 0.08/0.25 inference(cnf_transformation,[],[f12])).
% 0.08/0.25 tff(f22,plain,(
% 0.08/0.25 x | ($true != bG6)),
% 0.08/0.25 inference(cnf_transformation,[],[f12])).
% 0.08/0.25 tff(f24,plain,(
% 0.08/0.25 y | ($true != bG5)),
% 0.08/0.25 inference(cnf_transformation,[],[f13])).
% 0.08/0.25 tff(f25,plain,(
% 0.08/0.25 ($true = bG4) | ~f(bG3)),
% 0.08/0.25 inference(cnf_transformation,[],[f14])).
% 0.08/0.25 tff(f26,plain,(
% 0.08/0.25 f(bG3) | ($true != bG4)),
% 0.08/0.25 inference(cnf_transformation,[],[f14])).
% 0.08/0.25 tff(f27,plain,(
% 0.08/0.25 ($true = bG3) | ~x),
% 0.08/0.25 inference(cnf_transformation,[],[f15])).
% 0.08/0.25 tff(f28,plain,(
% 0.08/0.25 x | ($true != bG3)),
% 0.08/0.25 inference(cnf_transformation,[],[f15])).
% 0.08/0.25 tff(f29,plain,(
% 0.08/0.25 ($true = bG2) | ~f(bG1)),
% 0.08/0.25 inference(cnf_transformation,[],[f16])).
% 0.08/0.25 tff(f30,plain,(
% 0.08/0.25 f(bG1) | ($true != bG2)),
% 0.08/0.25 inference(cnf_transformation,[],[f16])).
% 0.08/0.25 tff(f31,plain,(
% 0.08/0.25 ($true = bG1) | ~f(bG0)),
% 0.08/0.25 inference(cnf_transformation,[],[f17])).
% 0.08/0.25 tff(f32,plain,(
% 0.08/0.25 f(bG0) | ($true != bG1)),
% 0.08/0.25 inference(cnf_transformation,[],[f17])).
% 0.08/0.25 tff(f33,plain,(
% 0.08/0.25 (bG0 = $true) | ~x),
% 0.08/0.25 inference(cnf_transformation,[],[f18])).
% 0.08/0.25 tff(f34,plain,(
% 0.08/0.25 x | (bG0 != $true)),
% 0.08/0.25 inference(cnf_transformation,[],[f18])).
% 0.08/0.25 tff(f35,plain,(
% 0.08/0.25 g(bG4) | ~f(bG2)),
% 0.08/0.25 inference(cnf_transformation,[],[f20])).
% 0.08/0.25 tff(f36,plain,(
% 0.08/0.25 f(bG2) | ~g(bG4)),
% 0.08/0.25 inference(cnf_transformation,[],[f20])).
% 0.08/0.25 tff(f37,plain,(
% 0.08/0.25 x | ~g(bG5)),
% 0.08/0.25 inference(cnf_transformation,[],[f20])).
% 0.08/0.25 tff(f38,plain,(
% 0.08/0.25 g(bG5) | ~x),
% 0.08/0.25 inference(cnf_transformation,[],[f20])).
% 0.08/0.25 tff(f39,plain,(
% 0.08/0.25 y | ~g(bG6)),
% 0.08/0.25 inference(cnf_transformation,[],[f20])).
% 0.08/0.25 tff(f40,plain,(
% 0.08/0.25 g(bG6) | ~y),
% 0.08/0.25 inference(cnf_transformation,[],[f20])).
% 0.08/0.25 tff(f41,plain,(
% 0.08/0.25 y | x),
% 0.08/0.25 inference(cnf_transformation,[],[f20])).
% 0.08/0.25 tff(f42,plain,(
% 0.08/0.25 ~y | ~x),
% 0.08/0.25 inference(cnf_transformation,[],[f20])).
% 0.08/0.25 tff(f44,definition,(
% 0.08/0.25 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.08/0.25 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.08/0.25 tff(f46,definition,(
% 0.08/0.25 spl7_1 <=> x),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[spl7_1])],[avatar_definition])).
% 0.08/0.25 tff(f47,plain,(
% 0.08/0.25 x | ~spl7_1),
% 0.08/0.25 inference(avatar_component_clause,[],[f46])).
% 0.08/0.25 tff(f48,plain,(
% 0.08/0.25 ~x | spl7_1),
% 0.08/0.25 inference(avatar_component_clause,[],[f46])).
% 0.08/0.25 tff(f50,definition,(
% 0.08/0.25 spl7_2 <=> y),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition])).
% 0.08/0.25 tff(f51,plain,(
% 0.08/0.25 y | ~spl7_2),
% 0.08/0.25 inference(avatar_component_clause,[],[f50])).
% 0.08/0.25 tff(f52,plain,(
% 0.08/0.25 ~y | spl7_2),
% 0.08/0.25 inference(avatar_component_clause,[],[f50])).
% 0.08/0.25 tff(f53,plain,(
% 0.08/0.25 ~spl7_1 | ~spl7_2),
% 0.08/0.25 inference(avatar_split_clause,[],[f42,f50,f46])).
% 0.08/0.25 tff(f54,plain,(
% 0.08/0.25 y | spl7_1),
% 0.08/0.25 inference(forward_subsumption_resolution,[],[f41,f48])).
% 0.08/0.25 tff(f55,plain,(
% 0.08/0.25 spl7_2 | spl7_1),
% 0.08/0.25 inference(avatar_split_clause,[],[f54,f46,f50])).
% 0.08/0.25 tff(f56,plain,(
% 0.08/0.25 g(bG5) | ~spl7_1),
% 0.08/0.25 inference(forward_subsumption_resolution,[],[f38,f47])).
% 0.08/0.25 tff(f59,definition,(
% 0.08/0.25 spl7_3 <=> f(bG2)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition])).
% 0.08/0.25 tff(f60,plain,(
% 0.08/0.25 f(bG2) | ~spl7_3),
% 0.08/0.25 inference(avatar_component_clause,[],[f59])).
% 0.08/0.25 tff(f61,plain,(
% 0.08/0.25 ~f(bG2) | spl7_3),
% 0.08/0.25 inference(avatar_component_clause,[],[f59])).
% 0.08/0.25 tff(f63,definition,(
% 0.08/0.25 spl7_4 <=> g(bG4)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[spl7_4])],[avatar_definition])).
% 0.08/0.25 tff(f64,plain,(
% 0.08/0.25 ~g(bG4) | spl7_4),
% 0.08/0.25 inference(avatar_component_clause,[],[f63])).
% 0.08/0.25 tff(f65,plain,(
% 0.08/0.25 g(bG4) | ~spl7_4),
% 0.08/0.25 inference(avatar_component_clause,[],[f63])).
% 0.08/0.25 tff(f66,plain,(
% 0.08/0.25 ~spl7_3 | spl7_4),
% 0.08/0.25 inference(avatar_split_clause,[],[f35,f63,f59])).
% 0.08/0.25 tff(f67,plain,(
% 0.08/0.25 ~g(bG4) | spl7_3),
% 0.08/0.25 inference(forward_subsumption_resolution,[],[f36,f61])).
% 0.08/0.25 tff(f69,plain,(
% 0.08/0.25 ~spl7_4 | spl7_3),
% 0.08/0.25 inference(avatar_split_clause,[],[f67,f59,f63])).
% 0.08/0.25 tff(f71,plain,(
% 0.08/0.25 ($true != bG5) | spl7_2),
% 0.08/0.25 inference(forward_subsumption_resolution,[],[f24,f52])).
% 0.08/0.25 tff(f72,plain,(
% 0.08/0.25 ($true = bG3) | ~spl7_1),
% 0.08/0.25 inference(forward_subsumption_resolution,[],[f27,f47])).
% 0.08/0.25 tff(f74,plain,(
% 0.08/0.25 ~f($true) | ($true = bG4) | ~spl7_1),
% 0.08/0.25 inference(forward_demodulation,[],[f25,f72])).
% 0.08/0.25 tff(f76,definition,(
% 0.08/0.25 spl7_5 <=> ($true = bG4)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[spl7_5])],[avatar_definition])).
% 0.08/0.25 tff(f77,plain,(
% 0.08/0.25 ($true != bG4) | spl7_5),
% 0.08/0.25 inference(avatar_component_clause,[],[f76])).
% 0.08/0.25 tff(f78,plain,(
% 0.08/0.25 ($true = bG4) | ~spl7_5),
% 0.08/0.25 inference(avatar_component_clause,[],[f76])).
% 0.08/0.25 tff(f80,definition,(
% 0.08/0.25 spl7_6 <=> f($true)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[spl7_6])],[avatar_definition])).
% 0.08/0.25 tff(f81,plain,(
% 0.08/0.25 f($true) | ~spl7_6),
% 0.08/0.25 inference(avatar_component_clause,[],[f80])).
% 0.08/0.25 tff(f82,plain,(
% 0.08/0.25 ~f($true) | spl7_6),
% 0.08/0.25 inference(avatar_component_clause,[],[f80])).
% 0.08/0.25 tff(f83,plain,(
% 0.08/0.25 spl7_5 | ~spl7_6 | ~spl7_1),
% 0.08/0.25 inference(avatar_split_clause,[],[f74,f46,f80,f76])).
% 0.08/0.25 tff(f85,plain,(
% 0.08/0.25 f(bG3) | ~spl7_5),
% 0.08/0.25 inference(forward_subsumption_resolution,[],[f26,f78])).
% 0.08/0.25 tff(f86,plain,(
% 0.08/0.25 f($true) | (~spl7_1 | ~spl7_5)),
% 0.08/0.25 inference(forward_demodulation,[],[f85,f72])).
% 0.08/0.25 tff(f87,plain,(
% 0.08/0.25 spl7_6 | ~spl7_1 | ~spl7_5),
% 0.08/0.25 inference(avatar_split_clause,[],[f86,f76,f46,f80])).
% 0.08/0.25 tff(f90,definition,(
% 0.08/0.25 spl7_7 <=> f(bG1)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[spl7_7])],[avatar_definition])).
% 0.08/0.25 tff(f91,plain,(
% 0.08/0.25 f(bG1) | ~spl7_7),
% 0.08/0.25 inference(avatar_component_clause,[],[f90])).
% 0.08/0.25 tff(f92,plain,(
% 0.08/0.25 ~f(bG1) | spl7_7),
% 0.08/0.25 inference(avatar_component_clause,[],[f90])).
% 0.08/0.25 tff(f94,definition,(
% 0.08/0.25 spl7_8 <=> ($true = bG2)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[spl7_8])],[avatar_definition])).
% 0.08/0.25 tff(f95,plain,(
% 0.08/0.25 ($true != bG2) | spl7_8),
% 0.08/0.25 inference(avatar_component_clause,[],[f94])).
% 0.08/0.25 tff(f96,plain,(
% 0.08/0.25 ($true = bG2) | ~spl7_8),
% 0.08/0.25 inference(avatar_component_clause,[],[f94])).
% 0.08/0.25 tff(f97,plain,(
% 0.08/0.25 ~spl7_7 | spl7_8),
% 0.08/0.25 inference(avatar_split_clause,[],[f29,f94,f90])).
% 0.08/0.25 tff(f98,plain,(
% 0.08/0.25 ($true != bG2) | spl7_7),
% 0.08/0.25 inference(forward_subsumption_resolution,[],[f30,f92])).
% 0.08/0.25 tff(f99,plain,(
% 0.08/0.25 ~spl7_8 | spl7_7),
% 0.08/0.25 inference(avatar_split_clause,[],[f98,f90,f94])).
% 0.08/0.25 tff(f100,plain,(
% 0.08/0.25 ~f($true) | (spl7_3 | ~spl7_8)),
% 0.08/0.25 inference(superposition,[],[f61,f96])).
% 0.08/0.25 tff(f117,plain,(
% 0.08/0.25 ($true != $true) | (bG4 = $false) | spl7_5),
% 0.08/0.25 inference(superposition,[],[f77,f44])).
% 0.08/0.25 tff(f119,plain,(
% 0.08/0.25 ($true != $true) | (bG5 = $false) | spl7_2),
% 0.08/0.25 inference(superposition,[],[f71,f44])).
% 0.08/0.25 tff(f123,plain,(
% 0.08/0.25 (bG5 = $false) | spl7_2),
% 0.08/0.25 inference(trivial_inequality_removal,[],[f119])).
% 0.08/0.25 tff(f124,plain,(
% 0.08/0.25 (bG4 = $false) | spl7_5),
% 0.08/0.25 inference(trivial_inequality_removal,[],[f117])).
% 0.08/0.25 tff(f130,plain,(
% 0.08/0.25 g($false) | (~spl7_1 | spl7_2)),
% 0.08/0.25 inference(superposition,[],[f56,f123])).
% 0.08/0.25 tff(f134,plain,(
% 0.08/0.25 ~g($false) | (spl7_4 | spl7_5)),
% 0.08/0.25 inference(superposition,[],[f64,f124])).
% 0.08/0.25 tff(f136,plain,(
% 0.08/0.25 $false | (~spl7_1 | spl7_2 | spl7_4 | spl7_5)),
% 0.08/0.25 inference(forward_subsumption_resolution,[],[f134,f130])).
% 0.08/0.25 tff(f137,plain,(
% 0.08/0.25 ~spl7_1 | spl7_2 | spl7_4 | spl7_5),
% 0.08/0.25 inference(avatar_contradiction_clause,[],[f136])).
% 0.08/0.25 tff(f140,plain,(
% 0.08/0.25 ~spl7_6 | spl7_3 | ~spl7_8),
% 0.08/0.25 inference(avatar_split_clause,[],[f100,f94,f59,f80])).
% 0.08/0.25 tff(f142,plain,(
% 0.08/0.25 ~g(bG5) | spl7_1),
% 0.08/0.25 inference(forward_subsumption_resolution,[],[f37,f48])).
% 0.08/0.25 tff(f143,plain,(
% 0.08/0.25 ~g($true) | (bG5 = $false) | spl7_1),
% 0.08/0.25 inference(superposition,[],[f142,f44])).
% 0.08/0.25 tff(f144,plain,(
% 0.08/0.25 g(bG6) | ~spl7_2),
% 0.08/0.25 inference(forward_subsumption_resolution,[],[f40,f51])).
% 0.08/0.25 tff(f145,plain,(
% 0.08/0.25 g($true) | (bG6 = $false) | ~spl7_2),
% 0.08/0.25 inference(superposition,[],[f144,f44])).
% 0.08/0.25 tff(f147,definition,(
% 0.08/0.25 spl7_11 <=> (bG4 = $false)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[spl7_11])],[avatar_definition])).
% 0.08/0.25 tff(f148,plain,(
% 0.08/0.25 (bG4 != $false) | spl7_11),
% 0.08/0.25 inference(avatar_component_clause,[],[f147])).
% 0.08/0.25 tff(f149,plain,(
% 0.08/0.25 (bG4 = $false) | ~spl7_11),
% 0.08/0.25 inference(avatar_component_clause,[],[f147])).
% 0.08/0.25 tff(f151,definition,(
% 0.08/0.25 spl7_12 <=> g($true)),
% 0.08/0.25 introduced(definition,[new_symbols(definition,[spl7_12])],[avatar_definition])).
% 0.08/0.25 tff(f152,plain,(
% 0.08/0.25 g($true) | ~spl7_12),
% 0.08/0.25 inference(avatar_component_clause,[],[f151])).
% 0.08/0.26 tff(f153,plain,(
% 0.08/0.26 ~g($true) | spl7_12),
% 0.08/0.26 inference(avatar_component_clause,[],[f151])).
% 0.08/0.26 tff(f156,plain,(
% 0.08/0.26 ~g($false) | (spl7_4 | ~spl7_11)),
% 0.08/0.26 inference(superposition,[],[f64,f149])).
% 0.08/0.26 tff(f169,definition,(
% 0.08/0.26 spl7_14 <=> (bG5 = $false)),
% 0.08/0.26 introduced(definition,[new_symbols(definition,[spl7_14])],[avatar_definition])).
% 0.08/0.26 tff(f171,plain,(
% 0.08/0.26 (bG5 = $false) | ~spl7_14),
% 0.08/0.26 inference(avatar_component_clause,[],[f169])).
% 0.08/0.26 tff(f172,plain,(
% 0.08/0.26 spl7_14 | ~spl7_12 | spl7_1),
% 0.08/0.26 inference(avatar_split_clause,[],[f143,f46,f151,f169])).
% 0.08/0.26 tff(f174,plain,(
% 0.08/0.26 (bG6 = $false) | (~spl7_2 | spl7_12)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f145,f153])).
% 0.08/0.26 tff(f176,plain,(
% 0.08/0.26 g($false) | (~spl7_2 | spl7_12)),
% 0.08/0.26 inference(superposition,[],[f144,f174])).
% 0.08/0.26 tff(f178,plain,(
% 0.08/0.26 $false | (~spl7_2 | spl7_4 | ~spl7_11 | spl7_12)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f176,f156])).
% 0.08/0.26 tff(f179,plain,(
% 0.08/0.26 ~spl7_2 | spl7_4 | ~spl7_11 | spl7_12),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f178])).
% 0.08/0.26 tff(f182,plain,(
% 0.08/0.26 ~g($false) | (spl7_1 | ~spl7_14)),
% 0.08/0.26 inference(superposition,[],[f142,f171])).
% 0.08/0.26 tff(f250,plain,(
% 0.08/0.26 ($true != bG6) | spl7_1),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f22,f48])).
% 0.08/0.26 tff(f251,plain,(
% 0.08/0.26 ($true != $true) | (bG6 = $false) | spl7_1),
% 0.08/0.26 inference(superposition,[],[f250,f44])).
% 0.08/0.26 tff(f252,plain,(
% 0.08/0.26 (bG6 = $false) | spl7_1),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f251])).
% 0.08/0.26 tff(f255,plain,(
% 0.08/0.26 g($false) | (spl7_1 | ~spl7_2)),
% 0.08/0.26 inference(superposition,[],[f144,f252])).
% 0.08/0.26 tff(f261,plain,(
% 0.08/0.26 $false | (spl7_1 | ~spl7_2 | ~spl7_14)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f255,f182])).
% 0.08/0.26 tff(f262,plain,(
% 0.08/0.26 spl7_1 | ~spl7_2 | ~spl7_14),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f261])).
% 0.08/0.26 tff(f276,plain,(
% 0.08/0.26 ($true != bG3) | spl7_1),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f28,f48])).
% 0.08/0.26 tff(f277,plain,(
% 0.08/0.26 ($true != $true) | (bG3 = $false) | spl7_1),
% 0.08/0.26 inference(superposition,[],[f276,f44])).
% 0.08/0.26 tff(f278,plain,(
% 0.08/0.26 (bG3 = $false) | spl7_1),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f277])).
% 0.08/0.26 tff(f288,plain,(
% 0.08/0.26 ~f($false) | ($true = bG4) | spl7_1),
% 0.08/0.26 inference(forward_demodulation,[],[f25,f278])).
% 0.08/0.26 tff(f292,plain,(
% 0.08/0.26 ($true != $true) | (bG2 = $false) | spl7_8),
% 0.08/0.26 inference(superposition,[],[f95,f44])).
% 0.08/0.26 tff(f293,plain,(
% 0.08/0.26 (bG2 = $false) | spl7_8),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f292])).
% 0.08/0.26 tff(f295,definition,(
% 0.08/0.26 spl7_17 <=> f($false)),
% 0.08/0.26 introduced(definition,[new_symbols(definition,[spl7_17])],[avatar_definition])).
% 0.08/0.26 tff(f296,plain,(
% 0.08/0.26 f($false) | ~spl7_17),
% 0.08/0.26 inference(avatar_component_clause,[],[f295])).
% 0.08/0.26 tff(f297,plain,(
% 0.08/0.26 ~f($false) | spl7_17),
% 0.08/0.26 inference(avatar_component_clause,[],[f295])).
% 0.08/0.26 tff(f298,plain,(
% 0.08/0.26 spl7_5 | ~spl7_17 | spl7_1),
% 0.08/0.26 inference(avatar_split_clause,[],[f288,f46,f295,f76])).
% 0.08/0.26 tff(f303,plain,(
% 0.08/0.26 f($false) | ($true != bG4) | spl7_1),
% 0.08/0.26 inference(forward_demodulation,[],[f26,f278])).
% 0.08/0.26 tff(f304,plain,(
% 0.08/0.26 ($true != bG4) | (spl7_1 | spl7_17)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f303,f297])).
% 0.08/0.26 tff(f305,plain,(
% 0.08/0.26 ~spl7_5 | spl7_1 | spl7_17),
% 0.08/0.26 inference(avatar_split_clause,[],[f304,f295,f46,f76])).
% 0.08/0.26 tff(f306,plain,(
% 0.08/0.26 ($true != $true) | (bG4 = $false) | spl7_5),
% 0.08/0.26 inference(superposition,[],[f77,f44])).
% 0.08/0.26 tff(f307,plain,(
% 0.08/0.26 (bG4 = $false) | spl7_5),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f306])).
% 0.08/0.26 tff(f308,plain,(
% 0.08/0.26 $false | (spl7_5 | spl7_11)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f307,f148])).
% 0.08/0.26 tff(f309,plain,(
% 0.08/0.26 spl7_5 | spl7_11),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f308])).
% 0.08/0.26 tff(f310,plain,(
% 0.08/0.26 f($false) | (~spl7_3 | spl7_8)),
% 0.08/0.26 inference(forward_demodulation,[],[f60,f293])).
% 0.08/0.26 tff(f312,plain,(
% 0.08/0.26 $false | (~spl7_3 | spl7_8 | spl7_17)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f310,f297])).
% 0.08/0.26 tff(f313,plain,(
% 0.08/0.26 ~spl7_3 | spl7_8 | spl7_17),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f312])).
% 0.08/0.26 tff(f318,plain,(
% 0.08/0.26 f($true) | (bG2 = $false) | ~spl7_3),
% 0.08/0.26 inference(superposition,[],[f60,f44])).
% 0.08/0.26 tff(f319,plain,(
% 0.08/0.26 (bG2 = $false) | (~spl7_3 | spl7_6)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f318,f82])).
% 0.08/0.26 tff(f341,plain,(
% 0.08/0.26 f($false) | (~spl7_3 | spl7_6)),
% 0.08/0.26 inference(superposition,[],[f60,f319])).
% 0.08/0.26 tff(f343,plain,(
% 0.08/0.26 $false | (~spl7_3 | spl7_6 | spl7_17)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f341,f297])).
% 0.08/0.26 tff(f344,plain,(
% 0.08/0.26 ~spl7_3 | spl7_6 | spl7_17),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f343])).
% 0.08/0.26 tff(f364,plain,(
% 0.08/0.26 ($true = $false) | (~spl7_3 | spl7_6 | ~spl7_8)),
% 0.08/0.26 inference(forward_demodulation,[],[f96,f319])).
% 0.08/0.26 tff(f365,plain,(
% 0.08/0.26 $false | (~spl7_3 | spl7_6 | ~spl7_8)),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f364])).
% 0.08/0.26 tff(f366,plain,(
% 0.08/0.26 ~spl7_3 | spl7_6 | ~spl7_8),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f365])).
% 0.08/0.26 tff(f381,plain,(
% 0.08/0.26 (bG0 = $true) | ~spl7_1),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f33,f47])).
% 0.08/0.26 tff(f385,plain,(
% 0.08/0.26 f($true) | ($true != bG1) | ~spl7_1),
% 0.08/0.26 inference(forward_demodulation,[],[f32,f381])).
% 0.08/0.26 tff(f386,plain,(
% 0.08/0.26 ($true != bG1) | (~spl7_1 | spl7_6)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f385,f82])).
% 0.08/0.26 tff(f387,plain,(
% 0.08/0.26 ($true != $true) | (bG1 = $false) | (~spl7_1 | spl7_6)),
% 0.08/0.26 inference(superposition,[],[f386,f44])).
% 0.08/0.26 tff(f388,plain,(
% 0.08/0.26 (bG1 = $false) | (~spl7_1 | spl7_6)),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f387])).
% 0.08/0.26 tff(f391,plain,(
% 0.08/0.26 ~f($false) | (~spl7_1 | spl7_6 | spl7_7)),
% 0.08/0.26 inference(superposition,[],[f92,f388])).
% 0.08/0.26 tff(f393,plain,(
% 0.08/0.26 $false | (~spl7_1 | spl7_6 | spl7_7 | ~spl7_17)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f391,f296])).
% 0.08/0.26 tff(f394,plain,(
% 0.08/0.26 ~spl7_1 | spl7_6 | spl7_7 | ~spl7_17),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f393])).
% 0.08/0.26 tff(f399,plain,(
% 0.08/0.26 ($true != $true) | (bG2 = $false) | spl7_8),
% 0.08/0.26 inference(superposition,[],[f95,f44])).
% 0.08/0.26 tff(f400,plain,(
% 0.08/0.26 (bG2 = $false) | spl7_8),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f399])).
% 0.08/0.26 tff(f415,plain,(
% 0.08/0.26 ~f($false) | (spl7_3 | spl7_8)),
% 0.08/0.26 inference(superposition,[],[f61,f400])).
% 0.08/0.26 tff(f417,plain,(
% 0.08/0.26 $false | (spl7_3 | spl7_8 | ~spl7_17)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f415,f296])).
% 0.08/0.26 tff(f418,plain,(
% 0.08/0.26 spl7_3 | spl7_8 | ~spl7_17),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f417])).
% 0.08/0.26 tff(f420,plain,(
% 0.08/0.26 f($true) | (bG1 = $false) | ~spl7_7),
% 0.08/0.26 inference(superposition,[],[f91,f44])).
% 0.08/0.26 tff(f421,plain,(
% 0.08/0.26 (bG1 = $false) | (spl7_6 | ~spl7_7)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f420,f82])).
% 0.08/0.26 tff(f437,plain,(
% 0.08/0.26 (bG0 != $true) | spl7_1),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f34,f48])).
% 0.08/0.26 tff(f438,plain,(
% 0.08/0.26 ($true != $true) | (bG0 = $false) | spl7_1),
% 0.08/0.26 inference(superposition,[],[f437,f44])).
% 0.08/0.26 tff(f439,plain,(
% 0.08/0.26 (bG0 = $false) | spl7_1),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f438])).
% 0.08/0.26 tff(f445,plain,(
% 0.08/0.26 ($true = $false) | ~f(bG0) | (spl7_6 | ~spl7_7)),
% 0.08/0.26 inference(forward_demodulation,[],[f31,f421])).
% 0.08/0.26 tff(f446,plain,(
% 0.08/0.26 ~f(bG0) | (spl7_6 | ~spl7_7)),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f445])).
% 0.08/0.26 tff(f447,plain,(
% 0.08/0.26 ~f($false) | (spl7_1 | spl7_6 | ~spl7_7)),
% 0.08/0.26 inference(forward_demodulation,[],[f446,f439])).
% 0.08/0.26 tff(f448,plain,(
% 0.08/0.26 $false | (spl7_1 | spl7_6 | ~spl7_7 | ~spl7_17)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f447,f296])).
% 0.08/0.26 tff(f449,plain,(
% 0.08/0.26 spl7_1 | spl7_6 | ~spl7_7 | ~spl7_17),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f448])).
% 0.08/0.26 tff(f450,plain,(
% 0.08/0.26 g($true) | (~spl7_4 | ~spl7_5)),
% 0.08/0.26 inference(forward_demodulation,[],[f65,f78])).
% 0.08/0.26 tff(f453,plain,(
% 0.08/0.26 $false | (~spl7_4 | ~spl7_5 | spl7_12)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f450,f153])).
% 0.08/0.26 tff(f454,plain,(
% 0.08/0.26 ~spl7_4 | ~spl7_5 | spl7_12),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f453])).
% 0.08/0.26 tff(f477,plain,(
% 0.08/0.26 f($false) | ($true != bG1) | spl7_1),
% 0.08/0.26 inference(forward_demodulation,[],[f32,f439])).
% 0.08/0.26 tff(f478,plain,(
% 0.08/0.26 ($true != bG1) | (spl7_1 | spl7_17)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f477,f297])).
% 0.08/0.26 tff(f479,plain,(
% 0.08/0.26 ($true != $true) | (bG1 = $false) | (spl7_1 | spl7_17)),
% 0.08/0.26 inference(superposition,[],[f478,f44])).
% 0.08/0.26 tff(f480,plain,(
% 0.08/0.26 (bG1 = $false) | (spl7_1 | spl7_17)),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f479])).
% 0.08/0.26 tff(f483,plain,(
% 0.08/0.26 f($false) | (spl7_1 | ~spl7_7 | spl7_17)),
% 0.08/0.26 inference(superposition,[],[f91,f480])).
% 0.08/0.26 tff(f485,plain,(
% 0.08/0.26 $false | (spl7_1 | ~spl7_7 | spl7_17)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f483,f297])).
% 0.08/0.26 tff(f486,plain,(
% 0.08/0.26 spl7_1 | ~spl7_7 | spl7_17),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f485])).
% 0.08/0.26 tff(f491,plain,(
% 0.08/0.26 ~g(bG6) | spl7_2),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f39,f52])).
% 0.08/0.26 tff(f492,plain,(
% 0.08/0.26 ~g($true) | (bG6 = $false) | spl7_2),
% 0.08/0.26 inference(superposition,[],[f491,f44])).
% 0.08/0.26 tff(f493,plain,(
% 0.08/0.26 (bG6 = $false) | (spl7_2 | ~spl7_12)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f492,f152])).
% 0.08/0.26 tff(f501,plain,(
% 0.08/0.26 ($true = bG6) | ~spl7_1),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f21,f47])).
% 0.08/0.26 tff(f502,plain,(
% 0.08/0.26 ($true = $false) | (~spl7_1 | spl7_2 | ~spl7_12)),
% 0.08/0.26 inference(forward_demodulation,[],[f501,f493])).
% 0.08/0.26 tff(f503,plain,(
% 0.08/0.26 $false | (~spl7_1 | spl7_2 | ~spl7_12)),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f502])).
% 0.08/0.26 tff(f504,plain,(
% 0.08/0.26 ~spl7_1 | spl7_2 | ~spl7_12),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f503])).
% 0.08/0.26 tff(f513,plain,(
% 0.08/0.26 ~f($true) | (bG1 = $false) | spl7_7),
% 0.08/0.26 inference(superposition,[],[f92,f44])).
% 0.08/0.26 tff(f514,plain,(
% 0.08/0.26 (bG1 = $false) | (~spl7_6 | spl7_7)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f513,f81])).
% 0.08/0.26 tff(f533,plain,(
% 0.08/0.26 (bG0 = $true) | ~spl7_1),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f33,f47])).
% 0.08/0.26 tff(f536,plain,(
% 0.08/0.26 ($true = $false) | ~f(bG0) | (~spl7_6 | spl7_7)),
% 0.08/0.26 inference(forward_demodulation,[],[f31,f514])).
% 0.08/0.26 tff(f537,plain,(
% 0.08/0.26 ~f(bG0) | (~spl7_6 | spl7_7)),
% 0.08/0.26 inference(trivial_inequality_removal,[],[f536])).
% 0.08/0.26 tff(f538,plain,(
% 0.08/0.26 ~f($true) | (~spl7_1 | ~spl7_6 | spl7_7)),
% 0.08/0.26 inference(forward_demodulation,[],[f537,f533])).
% 0.08/0.26 tff(f539,plain,(
% 0.08/0.26 $false | (~spl7_1 | ~spl7_6 | spl7_7)),
% 0.08/0.26 inference(forward_subsumption_resolution,[],[f538,f81])).
% 0.08/0.26 tff(f540,plain,(
% 0.08/0.26 ~spl7_1 | ~spl7_6 | spl7_7),
% 0.08/0.26 inference(avatar_contradiction_clause,[],[f539])).
% 0.08/0.26 cnf(s26, plain, ~spl7_1 | ~spl7_2, inference(sat_conversion,[],[f53])).
% 0.08/0.26 cnf(s32, plain, spl7_1 | spl7_2, inference(sat_conversion,[],[f55])).
% 0.08/0.26 cnf(s43, plain, ~spl7_3 | spl7_4, inference(sat_conversion,[],[f66])).
% 0.08/0.26 cnf(s49, plain, spl7_3 | ~spl7_4, inference(sat_conversion,[],[f69])).
% 0.08/0.26 cnf(s63, plain, ~spl7_1 | spl7_5 | ~spl7_6, inference(sat_conversion,[],[f83])).
% 0.08/0.26 cnf(s68, plain, ~spl7_1 | ~spl7_5 | spl7_6, inference(sat_conversion,[],[f87])).
% 0.08/0.26 cnf(s75, plain, ~spl7_7 | spl7_8, inference(sat_conversion,[],[f97])).
% 0.08/0.26 cnf(s80, plain, spl7_7 | ~spl7_8, inference(sat_conversion,[],[f99])).
% 0.08/0.26 cnf(s103, plain, ~spl7_1 | spl7_2 | spl7_4 | spl7_5, inference(sat_conversion,[],[f137])).
% 0.08/0.26 cnf(s113, plain, spl7_3 | ~spl7_6 | ~spl7_8, inference(sat_conversion,[],[f140])).
% 0.08/0.26 cnf(s160, plain, spl7_1 | ~spl7_12 | spl7_14, inference(sat_conversion,[],[f172])).
% 0.08/0.26 cnf(s166, plain, ~spl7_2 | spl7_4 | ~spl7_11 | spl7_12, inference(sat_conversion,[],[f179])).
% 0.08/0.26 cnf(s217, plain, spl7_1 | ~spl7_2 | ~spl7_14, inference(sat_conversion,[],[f262])).
% 0.08/0.26 cnf(s248, plain, spl7_1 | spl7_5 | ~spl7_17, inference(sat_conversion,[],[f298])).
% 0.08/0.26 cnf(s254, plain, spl7_1 | ~spl7_5 | spl7_17, inference(sat_conversion,[],[f305])).
% 0.08/0.26 cnf(s257, plain, spl7_5 | spl7_11, inference(sat_conversion,[],[f309])).
% 0.08/0.26 cnf(s261, plain, ~spl7_3 | spl7_8 | spl7_17, inference(sat_conversion,[],[f313])).
% 0.08/0.26 cnf(s308, plain, ~spl7_3 | spl7_6 | spl7_17, inference(sat_conversion,[],[f344])).
% 0.08/0.26 cnf(s326, plain, ~spl7_3 | spl7_6 | ~spl7_8, inference(sat_conversion,[],[f366])).
% 0.08/0.26 cnf(s344, plain, ~spl7_1 | spl7_6 | spl7_7 | ~spl7_17, inference(sat_conversion,[],[f394])).
% 0.08/0.26 cnf(s391, plain, spl7_3 | spl7_8 | ~spl7_17, inference(sat_conversion,[],[f418])).
% 0.08/0.26 cnf(s410, plain, spl7_1 | spl7_6 | ~spl7_7 | ~spl7_17, inference(sat_conversion,[],[f449])).
% 0.08/0.26 cnf(s415, plain, ~spl7_4 | ~spl7_5 | spl7_12, inference(sat_conversion,[],[f454])).
% 0.08/0.26 cnf(s449, plain, spl7_1 | ~spl7_7 | spl7_17, inference(sat_conversion,[],[f486])).
% 0.08/0.26 cnf(s488, plain, ~spl7_1 | spl7_2 | ~spl7_12, inference(sat_conversion,[],[f504])).
% 0.08/0.26 cnf(s523, plain, ~spl7_1 | ~spl7_6 | spl7_7, inference(sat_conversion,[],[f540])).
% 0.08/0.26 cnf(s524, plain, spl7_3 | spl7_1, inference(rat,[],[s410,s113,s80,s391,s254,s257,s166,s49,s160,s217,s32])).
% 0.08/0.26 cnf(s525, plain, spl7_14 | spl7_1, inference(rat,[],[s80,s261,s449,s248,s415,s43,s524,s160])).
% 0.08/0.26 cnf(s526, plain, spl7_1 | ~spl7_2, inference(rat,[],[s525,s217])).
% 0.08/0.26 cnf(s527, plain, spl7_1, inference(rat,[],[s526,s32])).
% 0.08/0.26 cnf(s529, plain, ~spl7_2, inference(rat,[],[s26,s527])).
% 0.08/0.26 cnf(s530, plain, ~spl7_12, inference(rat,[],[s488,s527,s529])).
% 0.08/0.26 cnf(s533, plain, spl7_3, inference(rat,[],[s75,s113,s523,s68,s103,s49,s527,s529])).
% 0.08/0.26 cnf(s534, plain, spl7_4, inference(rat,[],[s43,s533])).
% 0.08/0.26 cnf(s535, plain, ~spl7_5, inference(rat,[],[s415,s530,s534])).
% 0.08/0.26 cnf(s537, plain, ~spl7_6, inference(rat,[],[s63,s527,s535])).
% 0.08/0.26 cnf(s538, plain, ~spl7_8, inference(rat,[],[s326,s533,s537])).
% 0.08/0.26 cnf(s539, plain, spl7_17, inference(rat,[],[s308,s533,s537])).
% 0.08/0.26 cnf(s540, plain, ~spl7_7, inference(rat,[],[s75,s538])).
% 0.08/0.26 cnf(s541, plain, $false, inference(rat,[],[s344,s537,s527,s540,s539])).
% 0.08/0.26 tff(f541,plain,(
% 0.08/0.26 $false),
% 0.08/0.26 inference(avatar_sat_refutation,[],[s541])).
% 0.08/0.26 % SZS output end Proof for theBenchmark
% 0.08/0.26 % (1763516)------------------------------
% 0.08/0.26 % (1763516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.26 % (1763516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.26 % (1763516)CaDiCaL version: 2.1.3
% 0.08/0.26 % (1763516)Termination reason: Refutation
% 0.08/0.26 % (1763516)Time elapsed: 0.008 s
% 0.08/0.26 % (1763516)Peak memory usage: 12 MB
% 0.08/0.26 % (1763516)Instructions burned: 18 (million)
% 0.08/0.26 % (1763509)Success in time 0.034 s
% 0.08/0.26 % Vampire exiting
%------------------------------------------------------------------------------