%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO500_8.003 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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.23s 0.37s
% Output : Refutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYO500_8.003 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.23/0.29 % Computer : n017.cluster.edu
% 0.23/0.29 % Model : x86_64 x86_64
% 0.23/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.29 % Memory : 8046.5625MB
% 0.23/0.29 % OS : Linux 6.8.0-71-generic
% 0.23/0.29 % CPULimit : 300
% 0.23/0.29 % WCLimit : 300
% 0.23/0.29 % DateTime : Mon Sep 28 17:41:51 UTC 2026
% 0.23/0.29 % CPUTime :
% 0.23/0.29 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.23/0.32 Running first-order model finding
% 0.23/0.32 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.23/0.37 % (3817637)Will run a generic schedule for satisfiability detection.
% 0.23/0.37 % (3817647)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1382125019:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 0.23/0.37 % (3817643)% WARNING: option uhcvi not known.
% 0.23/0.37 % (3817647) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3817637-3817647"...
% 0.23/0.37 % (3817644)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2661106700:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 0.23/0.37 % (3817642)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1370301549_3000 on theBenchmark for (3000ds/0Mi)
% 0.23/0.37 % (3817645)dis+10_1_sil=32000:sp=arity:random_seed=3426068307:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 0.23/0.37 % (3817643)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3312936254:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 0.23/0.37 % (3817647)...printing done.
% 0.23/0.37 % (3817647)Refutation found. Thanks to Tanya!
% 0.23/0.37 % SZS status Theorem for theBenchmark
% 0.23/0.37 % SZS output start Proof for theBenchmark
% 0.23/0.37 tff(func_def_0, type, bG0: $o).
% 0.23/0.37 tff(func_def_3, type, bG1: $o).
% 0.23/0.37 tff(func_def_4, type, bG2: $o).
% 0.23/0.37 tff(func_def_5, type, bG3: $o).
% 0.23/0.37 tff(func_def_6, type, bG4: $o).
% 0.23/0.37 tff(func_def_7, type, bG5: $o).
% 0.23/0.37 tff(func_def_8, type, bG6: $o).
% 0.23/0.37 tff(func_def_9, type, bG7: $o).
% 0.23/0.37 tff(func_def_10, type, bG8: $o).
% 0.23/0.37 tff(func_def_11, type, bG9: $o).
% 0.23/0.37 tff(func_def_12, type, bG10: $o).
% 0.23/0.37 tff(func_def_13, type, bG11: $o).
% 0.23/0.37 tff(pred_def_2, type, f0: $o > $o).
% 0.23/0.37 tff(pred_def_3, type, f1: $o > $o).
% 0.23/0.37 tff(pred_def_4, type, f2: $o > $o).
% 0.23/0.37 tff(f1,conjecture,(
% 0.23/0.37 (f0(f1(f1(f1(f2(x))))) = f0(f0(f0(f1(f2(f2(f2(x))))))))),
% 0.23/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p',kaminski3)).
% 0.23/0.37 tff(f2,negated_conjecture,(
% 0.23/0.37 ~ (f0(f1(f1(f1(f2(x))))) = f0(f0(f0(f1(f2(f2(f2(x))))))))),
% 0.23/0.37 inference(negated_conjecture,[status(cth)],[f1])).
% 0.23/0.37 tff(f3,definition,(
% 0.23/0.37 x <=> (bG0 = $true)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG0])],[fool_formula_definition])).
% 0.23/0.37 tff(f4,definition,(
% 0.23/0.37 f2(bG0) <=> ($true = bG1)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG1])],[fool_formula_definition])).
% 0.23/0.37 tff(f5,definition,(
% 0.23/0.37 f1(bG1) <=> ($true = bG2)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG2])],[fool_formula_definition])).
% 0.23/0.37 tff(f6,definition,(
% 0.23/0.37 f1(bG2) <=> ($true = bG3)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG3])],[fool_formula_definition])).
% 0.23/0.37 tff(f7,definition,(
% 0.23/0.37 f1(bG3) <=> ($true = bG4)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG4])],[fool_formula_definition])).
% 0.23/0.37 tff(f8,definition,(
% 0.23/0.37 x <=> ($true = bG5)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG5])],[fool_formula_definition])).
% 0.23/0.37 tff(f9,definition,(
% 0.23/0.37 f2(bG5) <=> ($true = bG6)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG6])],[fool_formula_definition])).
% 0.23/0.37 tff(f10,definition,(
% 0.23/0.37 f2(bG6) <=> ($true = bG7)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG7])],[fool_formula_definition])).
% 0.23/0.37 tff(f11,definition,(
% 0.23/0.37 f2(bG7) <=> ($true = bG8)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG8])],[fool_formula_definition])).
% 0.23/0.37 tff(f12,definition,(
% 0.23/0.37 f1(bG8) <=> ($true = bG9)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG9])],[fool_formula_definition])).
% 0.23/0.37 tff(f13,definition,(
% 0.23/0.37 f0(bG9) <=> ($true = bG10)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG10])],[fool_formula_definition])).
% 0.23/0.37 tff(f14,definition,(
% 0.23/0.37 f0(bG10) <=> ($true = bG11)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[bG11])],[fool_formula_definition])).
% 0.23/0.37 tff(f15,plain,(
% 0.23/0.37 ~(f0(bG4) <=> f0(bG11))),
% 0.23/0.37 inference(fool_elimination,[],[f2,f14,f13,f12,f11,f10,f9,f8,f7,f6,f5,f4,f3])).
% 0.23/0.37 tff(f16,plain,(
% 0.23/0.37 f0(bG4) <~> f0(bG11)),
% 0.23/0.37 inference(ennf_transformation,[],[f15])).
% 0.23/0.37 tff(f17,plain,(
% 0.23/0.37 (f0(bG10) | ($true != bG11)) & (($true = bG11) | ~f0(bG10))),
% 0.23/0.37 inference(nnf_transformation,[],[f14])).
% 0.23/0.37 tff(f18,plain,(
% 0.23/0.37 (f0(bG9) | ($true != bG10)) & (($true = bG10) | ~f0(bG9))),
% 0.23/0.37 inference(nnf_transformation,[],[f13])).
% 0.23/0.37 tff(f19,plain,(
% 0.23/0.37 (f1(bG8) | ($true != bG9)) & (($true = bG9) | ~f1(bG8))),
% 0.23/0.37 inference(nnf_transformation,[],[f12])).
% 0.23/0.37 tff(f20,plain,(
% 0.23/0.37 (f2(bG7) | ($true != bG8)) & (($true = bG8) | ~f2(bG7))),
% 0.23/0.37 inference(nnf_transformation,[],[f11])).
% 0.23/0.37 tff(f21,plain,(
% 0.23/0.37 (f2(bG6) | ($true != bG7)) & (($true = bG7) | ~f2(bG6))),
% 0.23/0.37 inference(nnf_transformation,[],[f10])).
% 0.23/0.37 tff(f22,plain,(
% 0.23/0.37 (f2(bG5) | ($true != bG6)) & (($true = bG6) | ~f2(bG5))),
% 0.23/0.37 inference(nnf_transformation,[],[f9])).
% 0.23/0.37 tff(f23,plain,(
% 0.23/0.37 (x | ($true != bG5)) & (($true = bG5) | ~x)),
% 0.23/0.37 inference(nnf_transformation,[],[f8])).
% 0.23/0.37 tff(f24,plain,(
% 0.23/0.37 (f1(bG3) | ($true != bG4)) & (($true = bG4) | ~f1(bG3))),
% 0.23/0.37 inference(nnf_transformation,[],[f7])).
% 0.23/0.37 tff(f25,plain,(
% 0.23/0.37 (f1(bG2) | ($true != bG3)) & (($true = bG3) | ~f1(bG2))),
% 0.23/0.37 inference(nnf_transformation,[],[f6])).
% 0.23/0.37 tff(f26,plain,(
% 0.23/0.37 (f1(bG1) | ($true != bG2)) & (($true = bG2) | ~f1(bG1))),
% 0.23/0.37 inference(nnf_transformation,[],[f5])).
% 0.23/0.37 tff(f27,plain,(
% 0.23/0.37 (f2(bG0) | ($true != bG1)) & (($true = bG1) | ~f2(bG0))),
% 0.23/0.37 inference(nnf_transformation,[],[f4])).
% 0.23/0.37 tff(f28,plain,(
% 0.23/0.37 (x | (bG0 != $true)) & ((bG0 = $true) | ~x)),
% 0.23/0.37 inference(nnf_transformation,[],[f3])).
% 0.23/0.37 tff(f29,plain,(
% 0.23/0.37 (~f0(bG11) | ~f0(bG4)) & (f0(bG11) | f0(bG4))),
% 0.23/0.37 inference(nnf_transformation,[],[f16])).
% 0.23/0.37 tff(f30,plain,(
% 0.23/0.37 ($true = bG11) | ~f0(bG10)),
% 0.23/0.37 inference(cnf_transformation,[],[f17])).
% 0.23/0.37 tff(f31,plain,(
% 0.23/0.37 f0(bG10) | ($true != bG11)),
% 0.23/0.37 inference(cnf_transformation,[],[f17])).
% 0.23/0.37 tff(f32,plain,(
% 0.23/0.37 ($true = bG10) | ~f0(bG9)),
% 0.23/0.37 inference(cnf_transformation,[],[f18])).
% 0.23/0.37 tff(f33,plain,(
% 0.23/0.37 f0(bG9) | ($true != bG10)),
% 0.23/0.37 inference(cnf_transformation,[],[f18])).
% 0.23/0.37 tff(f34,plain,(
% 0.23/0.37 ($true = bG9) | ~f1(bG8)),
% 0.23/0.37 inference(cnf_transformation,[],[f19])).
% 0.23/0.37 tff(f35,plain,(
% 0.23/0.37 f1(bG8) | ($true != bG9)),
% 0.23/0.37 inference(cnf_transformation,[],[f19])).
% 0.23/0.37 tff(f36,plain,(
% 0.23/0.37 ($true = bG8) | ~f2(bG7)),
% 0.23/0.37 inference(cnf_transformation,[],[f20])).
% 0.23/0.37 tff(f37,plain,(
% 0.23/0.37 f2(bG7) | ($true != bG8)),
% 0.23/0.37 inference(cnf_transformation,[],[f20])).
% 0.23/0.37 tff(f38,plain,(
% 0.23/0.37 ($true = bG7) | ~f2(bG6)),
% 0.23/0.37 inference(cnf_transformation,[],[f21])).
% 0.23/0.37 tff(f39,plain,(
% 0.23/0.37 f2(bG6) | ($true != bG7)),
% 0.23/0.37 inference(cnf_transformation,[],[f21])).
% 0.23/0.37 tff(f40,plain,(
% 0.23/0.37 ($true = bG6) | ~f2(bG5)),
% 0.23/0.37 inference(cnf_transformation,[],[f22])).
% 0.23/0.37 tff(f41,plain,(
% 0.23/0.37 f2(bG5) | ($true != bG6)),
% 0.23/0.37 inference(cnf_transformation,[],[f22])).
% 0.23/0.37 tff(f42,plain,(
% 0.23/0.37 ($true = bG5) | ~x),
% 0.23/0.37 inference(cnf_transformation,[],[f23])).
% 0.23/0.37 tff(f43,plain,(
% 0.23/0.37 x | ($true != bG5)),
% 0.23/0.37 inference(cnf_transformation,[],[f23])).
% 0.23/0.37 tff(f44,plain,(
% 0.23/0.37 ($true = bG4) | ~f1(bG3)),
% 0.23/0.37 inference(cnf_transformation,[],[f24])).
% 0.23/0.37 tff(f45,plain,(
% 0.23/0.37 f1(bG3) | ($true != bG4)),
% 0.23/0.37 inference(cnf_transformation,[],[f24])).
% 0.23/0.37 tff(f46,plain,(
% 0.23/0.37 ($true = bG3) | ~f1(bG2)),
% 0.23/0.37 inference(cnf_transformation,[],[f25])).
% 0.23/0.37 tff(f47,plain,(
% 0.23/0.37 f1(bG2) | ($true != bG3)),
% 0.23/0.37 inference(cnf_transformation,[],[f25])).
% 0.23/0.37 tff(f48,plain,(
% 0.23/0.37 ($true = bG2) | ~f1(bG1)),
% 0.23/0.37 inference(cnf_transformation,[],[f26])).
% 0.23/0.37 tff(f49,plain,(
% 0.23/0.37 f1(bG1) | ($true != bG2)),
% 0.23/0.37 inference(cnf_transformation,[],[f26])).
% 0.23/0.37 tff(f50,plain,(
% 0.23/0.37 ($true = bG1) | ~f2(bG0)),
% 0.23/0.37 inference(cnf_transformation,[],[f27])).
% 0.23/0.37 tff(f51,plain,(
% 0.23/0.37 f2(bG0) | ($true != bG1)),
% 0.23/0.37 inference(cnf_transformation,[],[f27])).
% 0.23/0.37 tff(f52,plain,(
% 0.23/0.37 (bG0 = $true) | ~x),
% 0.23/0.37 inference(cnf_transformation,[],[f28])).
% 0.23/0.37 tff(f53,plain,(
% 0.23/0.37 x | (bG0 != $true)),
% 0.23/0.37 inference(cnf_transformation,[],[f28])).
% 0.23/0.37 tff(f54,plain,(
% 0.23/0.37 f0(bG11) | f0(bG4)),
% 0.23/0.37 inference(cnf_transformation,[],[f29])).
% 0.23/0.37 tff(f55,plain,(
% 0.23/0.37 ~f0(bG11) | ~f0(bG4)),
% 0.23/0.37 inference(cnf_transformation,[],[f29])).
% 0.23/0.37 tff(f57,definition,(
% 0.23/0.37 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.23/0.37 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.23/0.37 tff(f59,definition,(
% 0.23/0.37 spl12_1 <=> f0(bG4)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition])).
% 0.23/0.37 tff(f60,plain,(
% 0.23/0.37 ~f0(bG4) | spl12_1),
% 0.23/0.37 inference(avatar_component_clause,[],[f59])).
% 0.23/0.37 tff(f61,plain,(
% 0.23/0.37 f0(bG4) | ~spl12_1),
% 0.23/0.37 inference(avatar_component_clause,[],[f59])).
% 0.23/0.37 tff(f63,definition,(
% 0.23/0.37 spl12_2 <=> f0(bG11)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition])).
% 0.23/0.37 tff(f64,plain,(
% 0.23/0.37 ~f0(bG11) | spl12_2),
% 0.23/0.37 inference(avatar_component_clause,[],[f63])).
% 0.23/0.37 tff(f65,plain,(
% 0.23/0.37 f0(bG11) | ~spl12_2),
% 0.23/0.37 inference(avatar_component_clause,[],[f63])).
% 0.23/0.37 tff(f66,plain,(
% 0.23/0.37 spl12_1 | spl12_2),
% 0.23/0.37 inference(avatar_split_clause,[],[f54,f63,f59])).
% 0.23/0.37 tff(f67,plain,(
% 0.23/0.37 ~spl12_1 | ~spl12_2),
% 0.23/0.37 inference(avatar_split_clause,[],[f55,f63,f59])).
% 0.23/0.37 tff(f69,definition,(
% 0.23/0.37 spl12_3 <=> x),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_3])],[avatar_definition])).
% 0.23/0.37 tff(f73,definition,(
% 0.23/0.37 spl12_4 <=> (bG0 = $true)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_4])],[avatar_definition])).
% 0.23/0.37 tff(f74,plain,(
% 0.23/0.37 (bG0 != $true) | spl12_4),
% 0.23/0.37 inference(avatar_component_clause,[],[f73])).
% 0.23/0.37 tff(f75,plain,(
% 0.23/0.37 (bG0 = $true) | ~spl12_4),
% 0.23/0.37 inference(avatar_component_clause,[],[f73])).
% 0.23/0.37 tff(f76,plain,(
% 0.23/0.37 ~spl12_3 | spl12_4),
% 0.23/0.37 inference(avatar_split_clause,[],[f52,f73,f69])).
% 0.23/0.37 tff(f77,plain,(
% 0.23/0.37 ~spl12_4 | spl12_3),
% 0.23/0.37 inference(avatar_split_clause,[],[f53,f69,f73])).
% 0.23/0.37 tff(f79,definition,(
% 0.23/0.37 spl12_5 <=> f2(bG0)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_5])],[avatar_definition])).
% 0.23/0.37 tff(f80,plain,(
% 0.23/0.37 f2(bG0) | ~spl12_5),
% 0.23/0.37 inference(avatar_component_clause,[],[f79])).
% 0.23/0.37 tff(f81,plain,(
% 0.23/0.37 ~f2(bG0) | spl12_5),
% 0.23/0.37 inference(avatar_component_clause,[],[f79])).
% 0.23/0.37 tff(f83,definition,(
% 0.23/0.37 spl12_6 <=> ($true = bG1)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_6])],[avatar_definition])).
% 0.23/0.37 tff(f84,plain,(
% 0.23/0.37 ($true != bG1) | spl12_6),
% 0.23/0.37 inference(avatar_component_clause,[],[f83])).
% 0.23/0.37 tff(f85,plain,(
% 0.23/0.37 ($true = bG1) | ~spl12_6),
% 0.23/0.37 inference(avatar_component_clause,[],[f83])).
% 0.23/0.37 tff(f86,plain,(
% 0.23/0.37 ~spl12_5 | spl12_6),
% 0.23/0.37 inference(avatar_split_clause,[],[f50,f83,f79])).
% 0.23/0.37 tff(f87,plain,(
% 0.23/0.37 ~spl12_6 | spl12_5),
% 0.23/0.37 inference(avatar_split_clause,[],[f51,f79,f83])).
% 0.23/0.37 tff(f89,definition,(
% 0.23/0.37 spl12_7 <=> f1(bG1)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_7])],[avatar_definition])).
% 0.23/0.37 tff(f90,plain,(
% 0.23/0.37 f1(bG1) | ~spl12_7),
% 0.23/0.37 inference(avatar_component_clause,[],[f89])).
% 0.23/0.37 tff(f91,plain,(
% 0.23/0.37 ~f1(bG1) | spl12_7),
% 0.23/0.37 inference(avatar_component_clause,[],[f89])).
% 0.23/0.37 tff(f93,definition,(
% 0.23/0.37 spl12_8 <=> ($true = bG2)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_8])],[avatar_definition])).
% 0.23/0.37 tff(f94,plain,(
% 0.23/0.37 ($true != bG2) | spl12_8),
% 0.23/0.37 inference(avatar_component_clause,[],[f93])).
% 0.23/0.37 tff(f95,plain,(
% 0.23/0.37 ($true = bG2) | ~spl12_8),
% 0.23/0.37 inference(avatar_component_clause,[],[f93])).
% 0.23/0.37 tff(f96,plain,(
% 0.23/0.37 ~spl12_7 | spl12_8),
% 0.23/0.37 inference(avatar_split_clause,[],[f48,f93,f89])).
% 0.23/0.37 tff(f97,plain,(
% 0.23/0.37 ~spl12_8 | spl12_7),
% 0.23/0.37 inference(avatar_split_clause,[],[f49,f89,f93])).
% 0.23/0.37 tff(f99,definition,(
% 0.23/0.37 spl12_9 <=> f1(bG2)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_9])],[avatar_definition])).
% 0.23/0.37 tff(f100,plain,(
% 0.23/0.37 f1(bG2) | ~spl12_9),
% 0.23/0.37 inference(avatar_component_clause,[],[f99])).
% 0.23/0.37 tff(f101,plain,(
% 0.23/0.37 ~f1(bG2) | spl12_9),
% 0.23/0.37 inference(avatar_component_clause,[],[f99])).
% 0.23/0.37 tff(f103,definition,(
% 0.23/0.37 spl12_10 <=> ($true = bG3)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_10])],[avatar_definition])).
% 0.23/0.37 tff(f104,plain,(
% 0.23/0.37 ($true != bG3) | spl12_10),
% 0.23/0.37 inference(avatar_component_clause,[],[f103])).
% 0.23/0.37 tff(f105,plain,(
% 0.23/0.37 ($true = bG3) | ~spl12_10),
% 0.23/0.37 inference(avatar_component_clause,[],[f103])).
% 0.23/0.37 tff(f106,plain,(
% 0.23/0.37 ~spl12_9 | spl12_10),
% 0.23/0.37 inference(avatar_split_clause,[],[f46,f103,f99])).
% 0.23/0.37 tff(f107,plain,(
% 0.23/0.37 ~spl12_10 | spl12_9),
% 0.23/0.37 inference(avatar_split_clause,[],[f47,f99,f103])).
% 0.23/0.37 tff(f109,definition,(
% 0.23/0.37 spl12_11 <=> f1(bG3)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_11])],[avatar_definition])).
% 0.23/0.37 tff(f110,plain,(
% 0.23/0.37 f1(bG3) | ~spl12_11),
% 0.23/0.37 inference(avatar_component_clause,[],[f109])).
% 0.23/0.37 tff(f111,plain,(
% 0.23/0.37 ~f1(bG3) | spl12_11),
% 0.23/0.37 inference(avatar_component_clause,[],[f109])).
% 0.23/0.37 tff(f113,definition,(
% 0.23/0.37 spl12_12 <=> ($true = bG4)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_12])],[avatar_definition])).
% 0.23/0.37 tff(f114,plain,(
% 0.23/0.37 ($true != bG4) | spl12_12),
% 0.23/0.37 inference(avatar_component_clause,[],[f113])).
% 0.23/0.37 tff(f115,plain,(
% 0.23/0.37 ($true = bG4) | ~spl12_12),
% 0.23/0.37 inference(avatar_component_clause,[],[f113])).
% 0.23/0.37 tff(f116,plain,(
% 0.23/0.37 ~spl12_11 | spl12_12),
% 0.23/0.37 inference(avatar_split_clause,[],[f44,f113,f109])).
% 0.23/0.37 tff(f117,plain,(
% 0.23/0.37 ~spl12_12 | spl12_11),
% 0.23/0.37 inference(avatar_split_clause,[],[f45,f109,f113])).
% 0.23/0.37 tff(f119,definition,(
% 0.23/0.37 spl12_13 <=> ($true = bG5)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_13])],[avatar_definition])).
% 0.23/0.37 tff(f120,plain,(
% 0.23/0.37 ($true != bG5) | spl12_13),
% 0.23/0.37 inference(avatar_component_clause,[],[f119])).
% 0.23/0.37 tff(f121,plain,(
% 0.23/0.37 ($true = bG5) | ~spl12_13),
% 0.23/0.37 inference(avatar_component_clause,[],[f119])).
% 0.23/0.37 tff(f122,plain,(
% 0.23/0.37 ~spl12_3 | spl12_13),
% 0.23/0.37 inference(avatar_split_clause,[],[f42,f119,f69])).
% 0.23/0.37 tff(f123,plain,(
% 0.23/0.37 ~spl12_13 | spl12_3),
% 0.23/0.37 inference(avatar_split_clause,[],[f43,f69,f119])).
% 0.23/0.37 tff(f125,definition,(
% 0.23/0.37 spl12_14 <=> f2(bG5)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_14])],[avatar_definition])).
% 0.23/0.37 tff(f126,plain,(
% 0.23/0.37 f2(bG5) | ~spl12_14),
% 0.23/0.37 inference(avatar_component_clause,[],[f125])).
% 0.23/0.37 tff(f127,plain,(
% 0.23/0.37 ~f2(bG5) | spl12_14),
% 0.23/0.37 inference(avatar_component_clause,[],[f125])).
% 0.23/0.37 tff(f129,definition,(
% 0.23/0.37 spl12_15 <=> ($true = bG6)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition])).
% 0.23/0.37 tff(f130,plain,(
% 0.23/0.37 ($true != bG6) | spl12_15),
% 0.23/0.37 inference(avatar_component_clause,[],[f129])).
% 0.23/0.37 tff(f131,plain,(
% 0.23/0.37 ($true = bG6) | ~spl12_15),
% 0.23/0.37 inference(avatar_component_clause,[],[f129])).
% 0.23/0.37 tff(f132,plain,(
% 0.23/0.37 ~spl12_14 | spl12_15),
% 0.23/0.37 inference(avatar_split_clause,[],[f40,f129,f125])).
% 0.23/0.37 tff(f133,plain,(
% 0.23/0.37 ~spl12_15 | spl12_14),
% 0.23/0.37 inference(avatar_split_clause,[],[f41,f125,f129])).
% 0.23/0.37 tff(f135,definition,(
% 0.23/0.37 spl12_16 <=> f2(bG6)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_16])],[avatar_definition])).
% 0.23/0.37 tff(f136,plain,(
% 0.23/0.37 f2(bG6) | ~spl12_16),
% 0.23/0.37 inference(avatar_component_clause,[],[f135])).
% 0.23/0.37 tff(f137,plain,(
% 0.23/0.37 ~f2(bG6) | spl12_16),
% 0.23/0.37 inference(avatar_component_clause,[],[f135])).
% 0.23/0.37 tff(f139,definition,(
% 0.23/0.37 spl12_17 <=> ($true = bG7)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_17])],[avatar_definition])).
% 0.23/0.37 tff(f140,plain,(
% 0.23/0.37 ($true != bG7) | spl12_17),
% 0.23/0.37 inference(avatar_component_clause,[],[f139])).
% 0.23/0.37 tff(f141,plain,(
% 0.23/0.37 ($true = bG7) | ~spl12_17),
% 0.23/0.37 inference(avatar_component_clause,[],[f139])).
% 0.23/0.37 tff(f142,plain,(
% 0.23/0.37 ~spl12_16 | spl12_17),
% 0.23/0.37 inference(avatar_split_clause,[],[f38,f139,f135])).
% 0.23/0.37 tff(f143,plain,(
% 0.23/0.37 ~spl12_17 | spl12_16),
% 0.23/0.37 inference(avatar_split_clause,[],[f39,f135,f139])).
% 0.23/0.37 tff(f145,definition,(
% 0.23/0.37 spl12_18 <=> f2(bG7)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_18])],[avatar_definition])).
% 0.23/0.37 tff(f146,plain,(
% 0.23/0.37 f2(bG7) | ~spl12_18),
% 0.23/0.37 inference(avatar_component_clause,[],[f145])).
% 0.23/0.37 tff(f147,plain,(
% 0.23/0.37 ~f2(bG7) | spl12_18),
% 0.23/0.37 inference(avatar_component_clause,[],[f145])).
% 0.23/0.37 tff(f149,definition,(
% 0.23/0.37 spl12_19 <=> ($true = bG8)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_19])],[avatar_definition])).
% 0.23/0.37 tff(f150,plain,(
% 0.23/0.37 ($true != bG8) | spl12_19),
% 0.23/0.37 inference(avatar_component_clause,[],[f149])).
% 0.23/0.37 tff(f151,plain,(
% 0.23/0.37 ($true = bG8) | ~spl12_19),
% 0.23/0.37 inference(avatar_component_clause,[],[f149])).
% 0.23/0.37 tff(f152,plain,(
% 0.23/0.37 ~spl12_18 | spl12_19),
% 0.23/0.37 inference(avatar_split_clause,[],[f36,f149,f145])).
% 0.23/0.37 tff(f153,plain,(
% 0.23/0.37 ~spl12_19 | spl12_18),
% 0.23/0.37 inference(avatar_split_clause,[],[f37,f145,f149])).
% 0.23/0.37 tff(f155,definition,(
% 0.23/0.37 spl12_20 <=> f1(bG8)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_20])],[avatar_definition])).
% 0.23/0.37 tff(f156,plain,(
% 0.23/0.37 f1(bG8) | ~spl12_20),
% 0.23/0.37 inference(avatar_component_clause,[],[f155])).
% 0.23/0.37 tff(f157,plain,(
% 0.23/0.37 ~f1(bG8) | spl12_20),
% 0.23/0.37 inference(avatar_component_clause,[],[f155])).
% 0.23/0.37 tff(f159,definition,(
% 0.23/0.37 spl12_21 <=> ($true = bG9)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_21])],[avatar_definition])).
% 0.23/0.37 tff(f160,plain,(
% 0.23/0.37 ($true != bG9) | spl12_21),
% 0.23/0.37 inference(avatar_component_clause,[],[f159])).
% 0.23/0.37 tff(f161,plain,(
% 0.23/0.37 ($true = bG9) | ~spl12_21),
% 0.23/0.37 inference(avatar_component_clause,[],[f159])).
% 0.23/0.37 tff(f162,plain,(
% 0.23/0.37 ~spl12_20 | spl12_21),
% 0.23/0.37 inference(avatar_split_clause,[],[f34,f159,f155])).
% 0.23/0.37 tff(f163,plain,(
% 0.23/0.37 ~spl12_21 | spl12_20),
% 0.23/0.37 inference(avatar_split_clause,[],[f35,f155,f159])).
% 0.23/0.37 tff(f165,definition,(
% 0.23/0.37 spl12_22 <=> f0(bG9)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_22])],[avatar_definition])).
% 0.23/0.37 tff(f166,plain,(
% 0.23/0.37 f0(bG9) | ~spl12_22),
% 0.23/0.37 inference(avatar_component_clause,[],[f165])).
% 0.23/0.37 tff(f167,plain,(
% 0.23/0.37 ~f0(bG9) | spl12_22),
% 0.23/0.37 inference(avatar_component_clause,[],[f165])).
% 0.23/0.37 tff(f169,definition,(
% 0.23/0.37 spl12_23 <=> ($true = bG10)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_23])],[avatar_definition])).
% 0.23/0.37 tff(f170,plain,(
% 0.23/0.37 ($true != bG10) | spl12_23),
% 0.23/0.37 inference(avatar_component_clause,[],[f169])).
% 0.23/0.37 tff(f171,plain,(
% 0.23/0.37 ($true = bG10) | ~spl12_23),
% 0.23/0.37 inference(avatar_component_clause,[],[f169])).
% 0.23/0.37 tff(f172,plain,(
% 0.23/0.37 ~spl12_22 | spl12_23),
% 0.23/0.37 inference(avatar_split_clause,[],[f32,f169,f165])).
% 0.23/0.37 tff(f173,plain,(
% 0.23/0.37 ~spl12_23 | spl12_22),
% 0.23/0.37 inference(avatar_split_clause,[],[f33,f165,f169])).
% 0.23/0.37 tff(f175,definition,(
% 0.23/0.37 spl12_24 <=> f0(bG10)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_24])],[avatar_definition])).
% 0.23/0.37 tff(f176,plain,(
% 0.23/0.37 f0(bG10) | ~spl12_24),
% 0.23/0.37 inference(avatar_component_clause,[],[f175])).
% 0.23/0.37 tff(f177,plain,(
% 0.23/0.37 ~f0(bG10) | spl12_24),
% 0.23/0.37 inference(avatar_component_clause,[],[f175])).
% 0.23/0.37 tff(f179,definition,(
% 0.23/0.37 spl12_25 <=> ($true = bG11)),
% 0.23/0.37 introduced(definition,[new_symbols(definition,[spl12_25])],[avatar_definition])).
% 0.23/0.37 tff(f180,plain,(
% 0.23/0.37 ($true != bG11) | spl12_25),
% 0.23/0.37 inference(avatar_component_clause,[],[f179])).
% 0.23/0.37 tff(f181,plain,(
% 0.23/0.37 ($true = bG11) | ~spl12_25),
% 0.23/0.37 inference(avatar_component_clause,[],[f179])).
% 0.23/0.37 tff(f182,plain,(
% 0.23/0.37 ~spl12_24 | spl12_25),
% 0.23/0.37 inference(avatar_split_clause,[],[f30,f179,f175])).
% 0.23/0.37 tff(f183,plain,(
% 0.23/0.37 ~spl12_25 | spl12_24),
% 0.23/0.37 inference(avatar_split_clause,[],[f31,f175,f179])).
% 0.23/0.37 tff(f186,plain,(
% 0.23/0.37 ($true != $true) | (bG0 = $false) | spl12_4),
% 0.23/0.37 inference(superposition,[],[f74,f57])).
% 0.23/0.37 tff(f188,plain,(
% 0.23/0.37 ($true != $true) | (bG1 = $false) | spl12_6),
% 0.23/0.37 inference(superposition,[],[f84,f57])).
% 0.23/0.37 tff(f189,plain,(
% 0.23/0.37 ~f1($true) | (bG1 = $false) | spl12_7),
% 0.23/0.37 inference(superposition,[],[f91,f57])).
% 0.23/0.37 tff(f190,plain,(
% 0.23/0.37 ($true != $true) | (bG2 = $false) | spl12_8),
% 0.23/0.37 inference(superposition,[],[f94,f57])).
% 0.23/0.37 tff(f192,plain,(
% 0.23/0.37 ($true != $true) | (bG3 = $false) | spl12_10),
% 0.23/0.37 inference(superposition,[],[f104,f57])).
% 0.23/0.37 tff(f193,plain,(
% 0.23/0.37 ~f1($true) | (bG3 = $false) | spl12_11),
% 0.23/0.37 inference(superposition,[],[f111,f57])).
% 0.23/0.37 tff(f194,plain,(
% 0.23/0.37 ($true != $true) | (bG4 = $false) | spl12_12),
% 0.23/0.37 inference(superposition,[],[f114,f57])).
% 0.23/0.37 tff(f195,plain,(
% 0.23/0.37 ~f0($true) | (bG4 = $false) | spl12_1),
% 0.23/0.37 inference(superposition,[],[f60,f57])).
% 0.23/0.37 tff(f196,plain,(
% 0.23/0.37 ($true != $true) | (bG5 = $false) | spl12_13),
% 0.23/0.37 inference(superposition,[],[f120,f57])).
% 0.23/0.37 tff(f197,plain,(
% 0.23/0.37 ~f2($true) | (bG5 = $false) | spl12_14),
% 0.23/0.37 inference(superposition,[],[f127,f57])).
% 0.23/0.37 tff(f198,plain,(
% 0.23/0.37 ($true != $true) | (bG6 = $false) | spl12_15),
% 0.23/0.37 inference(superposition,[],[f130,f57])).
% 0.23/0.37 tff(f199,plain,(
% 0.23/0.37 ~f2($true) | (bG6 = $false) | spl12_16),
% 0.23/0.37 inference(superposition,[],[f137,f57])).
% 0.23/0.37 tff(f200,plain,(
% 0.23/0.37 ($true != $true) | (bG7 = $false) | spl12_17),
% 0.23/0.37 inference(superposition,[],[f140,f57])).
% 0.23/0.37 tff(f201,plain,(
% 0.23/0.37 ~f2($true) | (bG7 = $false) | spl12_18),
% 0.23/0.37 inference(superposition,[],[f147,f57])).
% 0.23/0.37 tff(f202,plain,(
% 0.23/0.37 ($true != $true) | (bG8 = $false) | spl12_19),
% 0.23/0.37 inference(superposition,[],[f150,f57])).
% 0.23/0.37 tff(f204,plain,(
% 0.23/0.37 ($true != $true) | (bG9 = $false) | spl12_21),
% 0.23/0.37 inference(superposition,[],[f160,f57])).
% 0.23/0.37 tff(f206,plain,(
% 0.23/0.37 ($true != $true) | (bG10 = $false) | spl12_23),
% 0.23/0.37 inference(superposition,[],[f170,f57])).
% 0.23/0.37 tff(f207,plain,(
% 0.23/0.37 ~f0($true) | (bG10 = $false) | spl12_24),
% 0.23/0.37 inference(superposition,[],[f177,f57])).
% 0.23/0.37 tff(f208,plain,(
% 0.23/0.37 ($true != $true) | (bG11 = $false) | spl12_25),
% 0.23/0.37 inference(superposition,[],[f180,f57])).
% 0.23/0.37 tff(f209,plain,(
% 0.23/0.37 f0($true) | (bG11 = $false) | ~spl12_2),
% 0.23/0.37 inference(superposition,[],[f65,f57])).
% 0.23/0.37 tff(f211,plain,(
% 0.23/0.37 (bG11 = $false) | spl12_25),
% 0.23/0.37 inference(trivial_inequality_removal,[],[f208])).
% 0.23/0.37 tff(f212,plain,(
% 0.23/0.37 (bG10 = $false) | spl12_23),
% 0.23/0.37 inference(trivial_inequality_removal,[],[f206])).
% 0.23/0.37 tff(f213,plain,(
% 0.23/0.37 (bG9 = $false) | spl12_21),
% 0.23/0.37 inference(trivial_inequality_removal,[],[f204])).
% 0.23/0.37 tff(f214,plain,(
% 0.23/0.37 (bG8 = $false) | spl12_19),
% 0.23/0.37 inference(trivial_inequality_removal,[],[f202])).
% 0.23/0.37 tff(f215,plain,(
% 0.23/0.37 (bG7 = $false) | spl12_17),
% 0.23/0.37 inference(trivial_inequality_removal,[],[f200])).
% 0.23/0.37 tff(f216,plain,(
% 0.23/0.37 (bG6 = $false) | spl12_15),
% 0.23/0.37 inference(trivial_inequality_removal,[],[f198])).
% 0.54/0.37 tff(f217,plain,(
% 0.54/0.37 (bG5 = $false) | spl12_13),
% 0.54/0.37 inference(trivial_inequality_removal,[],[f196])).
% 0.54/0.37 tff(f218,plain,(
% 0.54/0.37 (bG4 = $false) | spl12_12),
% 0.54/0.37 inference(trivial_inequality_removal,[],[f194])).
% 0.54/0.37 tff(f219,plain,(
% 0.54/0.37 (bG3 = $false) | spl12_10),
% 0.54/0.37 inference(trivial_inequality_removal,[],[f192])).
% 0.54/0.37 tff(f220,plain,(
% 0.54/0.37 (bG2 = $false) | spl12_8),
% 0.54/0.37 inference(trivial_inequality_removal,[],[f190])).
% 0.54/0.37 tff(f221,plain,(
% 0.54/0.37 (bG1 = $false) | spl12_6),
% 0.54/0.37 inference(trivial_inequality_removal,[],[f188])).
% 0.54/0.37 tff(f222,plain,(
% 0.54/0.37 (bG0 = $false) | spl12_4),
% 0.54/0.37 inference(trivial_inequality_removal,[],[f186])).
% 0.54/0.37 tff(f224,definition,(
% 0.54/0.37 spl12_26 <=> (bG11 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_26])],[avatar_definition])).
% 0.54/0.37 tff(f226,plain,(
% 0.54/0.37 (bG11 = $false) | ~spl12_26),
% 0.54/0.37 inference(avatar_component_clause,[],[f224])).
% 0.54/0.37 tff(f228,definition,(
% 0.54/0.37 spl12_27 <=> f0($true)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_27])],[avatar_definition])).
% 0.54/0.37 tff(f229,plain,(
% 0.54/0.37 ~f0($true) | spl12_27),
% 0.54/0.37 inference(avatar_component_clause,[],[f228])).
% 0.54/0.37 tff(f230,plain,(
% 0.54/0.37 f0($true) | ~spl12_27),
% 0.54/0.37 inference(avatar_component_clause,[],[f228])).
% 0.54/0.37 tff(f231,plain,(
% 0.54/0.37 spl12_26 | spl12_27 | ~spl12_2),
% 0.54/0.37 inference(avatar_split_clause,[],[f209,f63,f228,f224])).
% 0.54/0.37 tff(f232,plain,(
% 0.54/0.37 spl12_26 | spl12_25),
% 0.54/0.37 inference(avatar_split_clause,[],[f211,f179,f224])).
% 0.54/0.37 tff(f234,definition,(
% 0.54/0.37 spl12_28 <=> (bG10 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_28])],[avatar_definition])).
% 0.54/0.37 tff(f236,plain,(
% 0.54/0.37 (bG10 = $false) | ~spl12_28),
% 0.54/0.37 inference(avatar_component_clause,[],[f234])).
% 0.54/0.37 tff(f237,plain,(
% 0.54/0.37 spl12_28 | ~spl12_27 | spl12_24),
% 0.54/0.37 inference(avatar_split_clause,[],[f207,f175,f228,f234])).
% 0.54/0.37 tff(f238,plain,(
% 0.54/0.37 spl12_28 | spl12_23),
% 0.54/0.37 inference(avatar_split_clause,[],[f212,f169,f234])).
% 0.54/0.37 tff(f240,definition,(
% 0.54/0.37 spl12_29 <=> (bG9 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_29])],[avatar_definition])).
% 0.54/0.37 tff(f242,plain,(
% 0.54/0.37 (bG9 = $false) | ~spl12_29),
% 0.54/0.37 inference(avatar_component_clause,[],[f240])).
% 0.54/0.37 tff(f244,plain,(
% 0.54/0.37 spl12_29 | spl12_21),
% 0.54/0.37 inference(avatar_split_clause,[],[f213,f159,f240])).
% 0.54/0.37 tff(f246,definition,(
% 0.54/0.37 spl12_30 <=> (bG8 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_30])],[avatar_definition])).
% 0.54/0.37 tff(f248,plain,(
% 0.54/0.37 (bG8 = $false) | ~spl12_30),
% 0.54/0.37 inference(avatar_component_clause,[],[f246])).
% 0.54/0.37 tff(f250,definition,(
% 0.54/0.37 spl12_31 <=> f1($true)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_31])],[avatar_definition])).
% 0.54/0.37 tff(f251,plain,(
% 0.54/0.37 f1($true) | ~spl12_31),
% 0.54/0.37 inference(avatar_component_clause,[],[f250])).
% 0.54/0.37 tff(f252,plain,(
% 0.54/0.37 ~f1($true) | spl12_31),
% 0.54/0.37 inference(avatar_component_clause,[],[f250])).
% 0.54/0.37 tff(f254,plain,(
% 0.54/0.37 spl12_30 | spl12_19),
% 0.54/0.37 inference(avatar_split_clause,[],[f214,f149,f246])).
% 0.54/0.37 tff(f256,definition,(
% 0.54/0.37 spl12_32 <=> (bG7 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_32])],[avatar_definition])).
% 0.54/0.37 tff(f258,plain,(
% 0.54/0.37 (bG7 = $false) | ~spl12_32),
% 0.54/0.37 inference(avatar_component_clause,[],[f256])).
% 0.54/0.37 tff(f260,definition,(
% 0.54/0.37 spl12_33 <=> f2($true)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_33])],[avatar_definition])).
% 0.54/0.37 tff(f261,plain,(
% 0.54/0.37 f2($true) | ~spl12_33),
% 0.54/0.37 inference(avatar_component_clause,[],[f260])).
% 0.54/0.37 tff(f262,plain,(
% 0.54/0.37 ~f2($true) | spl12_33),
% 0.54/0.37 inference(avatar_component_clause,[],[f260])).
% 0.54/0.37 tff(f263,plain,(
% 0.54/0.37 spl12_32 | ~spl12_33 | spl12_18),
% 0.54/0.37 inference(avatar_split_clause,[],[f201,f145,f260,f256])).
% 0.54/0.37 tff(f264,plain,(
% 0.54/0.37 spl12_32 | spl12_17),
% 0.54/0.37 inference(avatar_split_clause,[],[f215,f139,f256])).
% 0.54/0.37 tff(f266,definition,(
% 0.54/0.37 spl12_34 <=> (bG6 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_34])],[avatar_definition])).
% 0.54/0.37 tff(f268,plain,(
% 0.54/0.37 (bG6 = $false) | ~spl12_34),
% 0.54/0.37 inference(avatar_component_clause,[],[f266])).
% 0.54/0.37 tff(f269,plain,(
% 0.54/0.37 spl12_34 | ~spl12_33 | spl12_16),
% 0.54/0.37 inference(avatar_split_clause,[],[f199,f135,f260,f266])).
% 0.54/0.37 tff(f270,plain,(
% 0.54/0.37 spl12_34 | spl12_15),
% 0.54/0.37 inference(avatar_split_clause,[],[f216,f129,f266])).
% 0.54/0.37 tff(f272,definition,(
% 0.54/0.37 spl12_35 <=> (bG5 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_35])],[avatar_definition])).
% 0.54/0.37 tff(f274,plain,(
% 0.54/0.37 (bG5 = $false) | ~spl12_35),
% 0.54/0.37 inference(avatar_component_clause,[],[f272])).
% 0.54/0.37 tff(f275,plain,(
% 0.54/0.37 spl12_35 | ~spl12_33 | spl12_14),
% 0.54/0.37 inference(avatar_split_clause,[],[f197,f125,f260,f272])).
% 0.54/0.37 tff(f276,plain,(
% 0.54/0.37 spl12_35 | spl12_13),
% 0.54/0.37 inference(avatar_split_clause,[],[f217,f119,f272])).
% 0.54/0.37 tff(f278,definition,(
% 0.54/0.37 spl12_36 <=> (bG4 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_36])],[avatar_definition])).
% 0.54/0.37 tff(f280,plain,(
% 0.54/0.37 (bG4 = $false) | ~spl12_36),
% 0.54/0.37 inference(avatar_component_clause,[],[f278])).
% 0.54/0.37 tff(f281,plain,(
% 0.54/0.37 spl12_36 | ~spl12_27 | spl12_1),
% 0.54/0.37 inference(avatar_split_clause,[],[f195,f59,f228,f278])).
% 0.54/0.37 tff(f282,plain,(
% 0.54/0.37 spl12_36 | spl12_12),
% 0.54/0.37 inference(avatar_split_clause,[],[f218,f113,f278])).
% 0.54/0.37 tff(f284,definition,(
% 0.54/0.37 spl12_37 <=> (bG3 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_37])],[avatar_definition])).
% 0.54/0.37 tff(f286,plain,(
% 0.54/0.37 (bG3 = $false) | ~spl12_37),
% 0.54/0.37 inference(avatar_component_clause,[],[f284])).
% 0.54/0.37 tff(f287,plain,(
% 0.54/0.37 spl12_37 | ~spl12_31 | spl12_11),
% 0.54/0.37 inference(avatar_split_clause,[],[f193,f109,f250,f284])).
% 0.54/0.37 tff(f288,plain,(
% 0.54/0.37 spl12_37 | spl12_10),
% 0.54/0.37 inference(avatar_split_clause,[],[f219,f103,f284])).
% 0.54/0.37 tff(f290,definition,(
% 0.54/0.37 spl12_38 <=> (bG2 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_38])],[avatar_definition])).
% 0.54/0.37 tff(f292,plain,(
% 0.54/0.37 (bG2 = $false) | ~spl12_38),
% 0.54/0.37 inference(avatar_component_clause,[],[f290])).
% 0.54/0.37 tff(f294,plain,(
% 0.54/0.37 spl12_38 | spl12_8),
% 0.54/0.37 inference(avatar_split_clause,[],[f220,f93,f290])).
% 0.54/0.37 tff(f296,definition,(
% 0.54/0.37 spl12_39 <=> (bG1 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_39])],[avatar_definition])).
% 0.54/0.37 tff(f298,plain,(
% 0.54/0.37 (bG1 = $false) | ~spl12_39),
% 0.54/0.37 inference(avatar_component_clause,[],[f296])).
% 0.54/0.37 tff(f299,plain,(
% 0.54/0.37 spl12_39 | ~spl12_31 | spl12_7),
% 0.54/0.37 inference(avatar_split_clause,[],[f189,f89,f250,f296])).
% 0.54/0.37 tff(f300,plain,(
% 0.54/0.37 spl12_39 | spl12_6),
% 0.54/0.37 inference(avatar_split_clause,[],[f221,f83,f296])).
% 0.54/0.37 tff(f302,definition,(
% 0.54/0.37 spl12_40 <=> (bG0 = $false)),
% 0.54/0.37 introduced(definition,[new_symbols(definition,[spl12_40])],[avatar_definition])).
% 0.54/0.37 tff(f304,plain,(
% 0.54/0.37 (bG0 = $false) | ~spl12_40),
% 0.54/0.37 inference(avatar_component_clause,[],[f302])).
% 0.54/0.37 tff(f306,plain,(
% 0.54/0.37 spl12_40 | spl12_4),
% 0.54/0.37 inference(avatar_split_clause,[],[f222,f73,f302])).
% 0.54/0.37 tff(f307,plain,(
% 0.54/0.37 f1($true) | (~spl12_8 | ~spl12_9)),
% 0.54/0.37 inference(forward_demodulation,[],[f100,f95])).
% 0.54/0.37 tff(f308,plain,(
% 0.54/0.37 f1($true) | (~spl12_10 | ~spl12_11)),
% 0.54/0.37 inference(forward_demodulation,[],[f110,f105])).
% 0.54/0.37 tff(f309,plain,(
% 0.54/0.37 f2($true) | (~spl12_13 | ~spl12_14)),
% 0.54/0.37 inference(forward_demodulation,[],[f126,f121])).
% 0.54/0.37 tff(f310,plain,(
% 0.54/0.37 f2($true) | (~spl12_15 | ~spl12_16)),
% 0.54/0.37 inference(forward_demodulation,[],[f136,f131])).
% 0.54/0.37 tff(f311,plain,(
% 0.54/0.37 f2($true) | (~spl12_17 | ~spl12_18)),
% 0.54/0.37 inference(forward_demodulation,[],[f146,f141])).
% 0.54/0.37 tff(f312,plain,(
% 0.54/0.37 f1($true) | (~spl12_19 | ~spl12_20)),
% 0.54/0.37 inference(forward_demodulation,[],[f156,f151])).
% 0.54/0.37 tff(f313,plain,(
% 0.54/0.37 f0($true) | (~spl12_21 | ~spl12_22)),
% 0.54/0.37 inference(forward_demodulation,[],[f166,f161])).
% 0.54/0.37 tff(f314,plain,(
% 0.54/0.37 f0($true) | (~spl12_23 | ~spl12_24)),
% 0.54/0.37 inference(forward_demodulation,[],[f176,f171])).
% 0.54/0.37 tff(f325,plain,(
% 0.54/0.37 $false | (~spl12_19 | ~spl12_20 | spl12_31)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f312,f252])).
% 0.54/0.37 tff(f326,plain,(
% 0.54/0.37 ~spl12_19 | ~spl12_20 | spl12_31),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f325])).
% 0.54/0.37 tff(f327,plain,(
% 0.54/0.37 $false | (~spl12_21 | ~spl12_22 | spl12_27)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f313,f229])).
% 0.54/0.37 tff(f328,plain,(
% 0.54/0.37 ~spl12_21 | ~spl12_22 | spl12_27),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f327])).
% 0.54/0.37 tff(f332,plain,(
% 0.54/0.37 ~f2($true) | (~spl12_17 | spl12_18)),
% 0.54/0.37 inference(forward_demodulation,[],[f147,f141])).
% 0.54/0.37 tff(f333,plain,(
% 0.54/0.37 f1($false) | (~spl12_20 | ~spl12_30)),
% 0.54/0.37 inference(forward_demodulation,[],[f156,f248])).
% 0.54/0.37 tff(f334,plain,(
% 0.54/0.37 f2($false) | (~spl12_16 | ~spl12_34)),
% 0.54/0.37 inference(forward_demodulation,[],[f136,f268])).
% 0.54/0.37 tff(f336,plain,(
% 0.54/0.37 ~f0($true) | (bG11 = $false) | spl12_2),
% 0.54/0.37 inference(superposition,[],[f64,f57])).
% 0.54/0.37 tff(f337,plain,(
% 0.54/0.37 (bG11 = $false) | (spl12_2 | ~spl12_27)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f336,f230])).
% 0.54/0.37 tff(f338,plain,(
% 0.54/0.37 spl12_26 | spl12_2 | ~spl12_27),
% 0.54/0.37 inference(avatar_split_clause,[],[f337,f228,f63,f224])).
% 0.54/0.37 tff(f339,plain,(
% 0.54/0.37 ~f0($true) | (~spl12_21 | spl12_22)),
% 0.54/0.37 inference(forward_demodulation,[],[f167,f161])).
% 0.54/0.37 tff(f341,plain,(
% 0.54/0.37 f0($false) | (~spl12_24 | ~spl12_28)),
% 0.54/0.37 inference(forward_demodulation,[],[f176,f236])).
% 0.54/0.37 tff(f346,plain,(
% 0.54/0.37 f0($false) | (~spl12_1 | ~spl12_36)),
% 0.54/0.37 inference(superposition,[],[f61,f280])).
% 0.54/0.37 tff(f353,plain,(
% 0.54/0.37 ($true = $false) | (~spl12_12 | ~spl12_36)),
% 0.54/0.37 inference(superposition,[],[f115,f280])).
% 0.54/0.37 tff(f355,plain,(
% 0.54/0.37 f0($true) | (~spl12_1 | ~spl12_12)),
% 0.54/0.37 inference(superposition,[],[f61,f115])).
% 0.54/0.37 tff(f358,plain,(
% 0.54/0.37 $false | (~spl12_12 | ~spl12_36)),
% 0.54/0.37 inference(trivial_inequality_removal,[],[f353])).
% 0.54/0.37 tff(f359,plain,(
% 0.54/0.37 ~spl12_12 | ~spl12_36),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f358])).
% 0.54/0.37 tff(f362,plain,(
% 0.54/0.37 ~f1($true) | (~spl12_10 | spl12_11)),
% 0.54/0.37 inference(forward_demodulation,[],[f111,f105])).
% 0.54/0.37 tff(f366,plain,(
% 0.54/0.37 ~f1($true) | (~spl12_8 | spl12_9)),
% 0.54/0.37 inference(forward_demodulation,[],[f101,f95])).
% 0.54/0.37 tff(f368,plain,(
% 0.54/0.37 ~f1($false) | (spl12_11 | ~spl12_37)),
% 0.54/0.37 inference(forward_demodulation,[],[f111,f286])).
% 0.54/0.37 tff(f369,plain,(
% 0.54/0.37 $false | (~spl12_8 | spl12_9 | ~spl12_31)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f366,f251])).
% 0.54/0.37 tff(f370,plain,(
% 0.54/0.37 ~spl12_8 | spl12_9 | ~spl12_31),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f369])).
% 0.54/0.37 tff(f371,plain,(
% 0.54/0.37 $false | (spl12_11 | ~spl12_20 | ~spl12_30 | ~spl12_37)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f368,f333])).
% 0.54/0.37 tff(f372,plain,(
% 0.54/0.37 spl12_11 | ~spl12_20 | ~spl12_30 | ~spl12_37),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f371])).
% 0.54/0.37 tff(f373,plain,(
% 0.54/0.37 ~f1($false) | (spl12_20 | ~spl12_30)),
% 0.54/0.37 inference(forward_demodulation,[],[f157,f248])).
% 0.54/0.37 tff(f374,plain,(
% 0.54/0.37 ~f0($false) | (spl12_22 | ~spl12_29)),
% 0.54/0.37 inference(forward_demodulation,[],[f167,f242])).
% 0.54/0.37 tff(f375,plain,(
% 0.54/0.37 $false | (spl12_22 | ~spl12_24 | ~spl12_28 | ~spl12_29)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f374,f341])).
% 0.54/0.37 tff(f376,plain,(
% 0.54/0.37 spl12_22 | ~spl12_24 | ~spl12_28 | ~spl12_29),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f375])).
% 0.54/0.37 tff(f377,plain,(
% 0.54/0.37 ~f2($false) | (spl12_16 | ~spl12_34)),
% 0.54/0.37 inference(forward_demodulation,[],[f137,f268])).
% 0.54/0.37 tff(f378,plain,(
% 0.54/0.37 ~f0($false) | (spl12_24 | ~spl12_28)),
% 0.54/0.37 inference(forward_demodulation,[],[f177,f236])).
% 0.54/0.37 tff(f379,plain,(
% 0.54/0.37 ~f1($true) | (~spl12_19 | spl12_20)),
% 0.54/0.37 inference(forward_demodulation,[],[f157,f151])).
% 0.54/0.37 tff(f380,plain,(
% 0.54/0.37 $false | (~spl12_1 | spl12_22 | ~spl12_29 | ~spl12_36)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f374,f346])).
% 0.54/0.37 tff(f381,plain,(
% 0.54/0.37 ~spl12_1 | spl12_22 | ~spl12_29 | ~spl12_36),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f380])).
% 0.54/0.37 tff(f384,plain,(
% 0.54/0.37 f0($false) | (~spl12_22 | ~spl12_29)),
% 0.54/0.37 inference(forward_demodulation,[],[f166,f242])).
% 0.54/0.37 tff(f386,plain,(
% 0.54/0.37 ~f0($true) | (~spl12_23 | spl12_24)),
% 0.54/0.37 inference(forward_demodulation,[],[f177,f171])).
% 0.54/0.37 tff(f390,plain,(
% 0.54/0.37 ~f0($false) | (spl12_2 | ~spl12_26)),
% 0.54/0.37 inference(superposition,[],[f64,f226])).
% 0.54/0.37 tff(f392,plain,(
% 0.54/0.37 $false | (~spl12_1 | spl12_2 | ~spl12_26 | ~spl12_36)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f390,f346])).
% 0.54/0.37 tff(f393,plain,(
% 0.54/0.37 ~spl12_1 | spl12_2 | ~spl12_26 | ~spl12_36),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f392])).
% 0.54/0.37 tff(f394,plain,(
% 0.54/0.37 f1($false) | (~spl12_11 | ~spl12_37)),
% 0.54/0.37 inference(forward_demodulation,[],[f110,f286])).
% 0.54/0.37 tff(f395,plain,(
% 0.54/0.37 spl12_27 | ~spl12_1 | ~spl12_12),
% 0.54/0.37 inference(avatar_split_clause,[],[f355,f113,f59,f228])).
% 0.54/0.37 tff(f397,plain,(
% 0.54/0.37 spl12_27 | ~spl12_23 | ~spl12_24),
% 0.54/0.37 inference(avatar_split_clause,[],[f314,f175,f169,f228])).
% 0.54/0.37 tff(f398,plain,(
% 0.54/0.37 ($true = $false) | (~spl12_25 | ~spl12_26)),
% 0.54/0.37 inference(forward_demodulation,[],[f181,f226])).
% 0.54/0.37 tff(f399,plain,(
% 0.54/0.37 $false | (~spl12_25 | ~spl12_26)),
% 0.54/0.37 inference(trivial_inequality_removal,[],[f398])).
% 0.54/0.37 tff(f400,plain,(
% 0.54/0.37 ~spl12_25 | ~spl12_26),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f399])).
% 0.54/0.37 tff(f430,plain,(
% 0.54/0.37 f2($false) | (~spl12_18 | ~spl12_32)),
% 0.54/0.37 inference(superposition,[],[f146,f258])).
% 0.54/0.37 tff(f432,plain,(
% 0.54/0.37 $false | (spl12_16 | ~spl12_18 | ~spl12_32 | ~spl12_34)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f430,f377])).
% 0.54/0.37 tff(f433,plain,(
% 0.54/0.37 spl12_16 | ~spl12_18 | ~spl12_32 | ~spl12_34),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f432])).
% 0.54/0.37 tff(f435,plain,(
% 0.54/0.37 ($true = $false) | (~spl12_6 | ~spl12_39)),
% 0.54/0.37 inference(forward_demodulation,[],[f85,f298])).
% 0.54/0.37 tff(f436,plain,(
% 0.54/0.37 $false | (~spl12_6 | ~spl12_39)),
% 0.54/0.37 inference(trivial_inequality_removal,[],[f435])).
% 0.54/0.37 tff(f437,plain,(
% 0.54/0.37 ~spl12_6 | ~spl12_39),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f436])).
% 0.54/0.37 tff(f439,plain,(
% 0.54/0.37 spl12_33 | ~spl12_13 | ~spl12_14),
% 0.54/0.37 inference(avatar_split_clause,[],[f309,f125,f119,f260])).
% 0.54/0.37 tff(f440,plain,(
% 0.54/0.37 spl12_33 | ~spl12_15 | ~spl12_16),
% 0.54/0.37 inference(avatar_split_clause,[],[f310,f135,f129,f260])).
% 0.54/0.37 tff(f445,plain,(
% 0.54/0.37 spl12_33 | ~spl12_17 | ~spl12_18),
% 0.54/0.37 inference(avatar_split_clause,[],[f311,f145,f139,f260])).
% 0.54/0.37 tff(f449,plain,(
% 0.54/0.37 ~f2($true) | (~spl12_4 | spl12_5)),
% 0.54/0.37 inference(forward_demodulation,[],[f81,f75])).
% 0.54/0.37 tff(f452,plain,(
% 0.54/0.37 $false | (~spl12_4 | spl12_5 | ~spl12_33)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f449,f261])).
% 0.54/0.37 tff(f453,plain,(
% 0.54/0.37 ~spl12_4 | spl12_5 | ~spl12_33),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f452])).
% 0.54/0.37 tff(f458,plain,(
% 0.54/0.37 ~f1($false) | (spl12_9 | ~spl12_38)),
% 0.54/0.37 inference(forward_demodulation,[],[f101,f292])).
% 0.54/0.37 tff(f459,plain,(
% 0.54/0.37 $false | (spl12_9 | ~spl12_11 | ~spl12_37 | ~spl12_38)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f458,f394])).
% 0.54/0.37 tff(f460,plain,(
% 0.54/0.37 spl12_9 | ~spl12_11 | ~spl12_37 | ~spl12_38),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f459])).
% 0.54/0.37 tff(f462,plain,(
% 0.54/0.37 ~f2($false) | (spl12_5 | ~spl12_40)),
% 0.54/0.37 inference(forward_demodulation,[],[f81,f304])).
% 0.54/0.37 tff(f465,plain,(
% 0.54/0.37 f2($false) | (~spl12_14 | ~spl12_35)),
% 0.54/0.37 inference(forward_demodulation,[],[f126,f274])).
% 0.54/0.37 tff(f466,plain,(
% 0.54/0.37 $false | (spl12_5 | ~spl12_14 | ~spl12_35 | ~spl12_40)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f465,f462])).
% 0.54/0.37 tff(f467,plain,(
% 0.54/0.37 spl12_5 | ~spl12_14 | ~spl12_35 | ~spl12_40),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f466])).
% 0.54/0.37 tff(f468,plain,(
% 0.54/0.37 ~f2($false) | (spl12_14 | ~spl12_35)),
% 0.54/0.37 inference(forward_demodulation,[],[f127,f274])).
% 0.54/0.37 tff(f471,plain,(
% 0.54/0.37 ~f1($false) | (spl12_20 | ~spl12_30)),
% 0.54/0.37 inference(forward_demodulation,[],[f157,f248])).
% 0.54/0.37 tff(f472,plain,(
% 0.54/0.37 $false | (~spl12_11 | spl12_20 | ~spl12_30 | ~spl12_37)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f471,f394])).
% 0.54/0.37 tff(f473,plain,(
% 0.54/0.37 ~spl12_11 | spl12_20 | ~spl12_30 | ~spl12_37),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f472])).
% 0.54/0.37 tff(f478,plain,(
% 0.54/0.37 $false | (~spl12_21 | spl12_22 | ~spl12_27)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f339,f230])).
% 0.54/0.37 tff(f479,plain,(
% 0.54/0.37 ~spl12_21 | spl12_22 | ~spl12_27),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f478])).
% 0.54/0.37 tff(f486,plain,(
% 0.54/0.37 spl12_31 | ~spl12_8 | ~spl12_9),
% 0.54/0.37 inference(avatar_split_clause,[],[f307,f99,f93,f250])).
% 0.54/0.37 tff(f487,plain,(
% 0.54/0.37 spl12_31 | ~spl12_10 | ~spl12_11),
% 0.54/0.37 inference(avatar_split_clause,[],[f308,f109,f103,f250])).
% 0.54/0.37 tff(f520,plain,(
% 0.54/0.37 ~f2($false) | (spl12_18 | ~spl12_32)),
% 0.54/0.37 inference(superposition,[],[f147,f258])).
% 0.54/0.37 tff(f531,plain,(
% 0.54/0.37 f1($false) | (~spl12_7 | ~spl12_39)),
% 0.54/0.37 inference(superposition,[],[f90,f298])).
% 0.54/0.37 tff(f533,plain,(
% 0.54/0.37 $false | (~spl12_7 | spl12_20 | ~spl12_30 | ~spl12_39)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f531,f373])).
% 0.54/0.37 tff(f534,plain,(
% 0.54/0.37 ~spl12_7 | spl12_20 | ~spl12_30 | ~spl12_39),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f533])).
% 0.54/0.37 tff(f535,plain,(
% 0.54/0.37 ~f1($false) | (spl12_7 | ~spl12_39)),
% 0.54/0.37 inference(forward_demodulation,[],[f91,f298])).
% 0.54/0.37 tff(f539,plain,(
% 0.54/0.37 f0($false) | (~spl12_2 | ~spl12_26)),
% 0.54/0.37 inference(forward_demodulation,[],[f65,f226])).
% 0.54/0.37 tff(f541,plain,(
% 0.54/0.37 $false | (~spl12_2 | spl12_24 | ~spl12_26 | ~spl12_28)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f539,f378])).
% 0.54/0.37 tff(f542,plain,(
% 0.54/0.37 ~spl12_2 | spl12_24 | ~spl12_26 | ~spl12_28),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f541])).
% 0.54/0.37 tff(f544,plain,(
% 0.54/0.37 ~spl12_27 | ~spl12_23 | spl12_24),
% 0.54/0.37 inference(avatar_split_clause,[],[f386,f175,f169,f228])).
% 0.54/0.37 tff(f550,plain,(
% 0.54/0.37 ~f0($false) | (spl12_1 | ~spl12_36)),
% 0.54/0.37 inference(superposition,[],[f60,f280])).
% 0.54/0.37 tff(f552,plain,(
% 0.54/0.37 $false | (spl12_1 | ~spl12_22 | ~spl12_29 | ~spl12_36)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f550,f384])).
% 0.54/0.37 tff(f553,plain,(
% 0.54/0.37 spl12_1 | ~spl12_22 | ~spl12_29 | ~spl12_36),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f552])).
% 0.54/0.37 tff(f555,plain,(
% 0.54/0.37 f1($true) | (~spl12_6 | ~spl12_7)),
% 0.54/0.37 inference(forward_demodulation,[],[f90,f85])).
% 0.54/0.37 tff(f565,plain,(
% 0.54/0.37 ~spl12_33 | ~spl12_17 | spl12_18),
% 0.54/0.37 inference(avatar_split_clause,[],[f332,f145,f139,f260])).
% 0.54/0.37 tff(f567,plain,(
% 0.54/0.37 $false | (spl12_14 | ~spl12_16 | ~spl12_34 | ~spl12_35)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f468,f334])).
% 0.54/0.37 tff(f568,plain,(
% 0.54/0.37 spl12_14 | ~spl12_16 | ~spl12_34 | ~spl12_35),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f567])).
% 0.54/0.37 tff(f571,plain,(
% 0.54/0.37 ~spl12_31 | ~spl12_10 | spl12_11),
% 0.54/0.37 inference(avatar_split_clause,[],[f362,f109,f103,f250])).
% 0.54/0.37 tff(f573,plain,(
% 0.54/0.37 f1($false) | (~spl12_20 | ~spl12_30)),
% 0.54/0.37 inference(forward_demodulation,[],[f156,f248])).
% 0.54/0.37 tff(f583,plain,(
% 0.54/0.37 f1($false) | (~spl12_9 | ~spl12_38)),
% 0.54/0.37 inference(forward_demodulation,[],[f100,f292])).
% 0.54/0.37 tff(f584,plain,(
% 0.54/0.37 $false | (spl12_7 | ~spl12_20 | ~spl12_30 | ~spl12_39)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f573,f535])).
% 0.54/0.37 tff(f585,plain,(
% 0.54/0.37 spl12_7 | ~spl12_20 | ~spl12_30 | ~spl12_39),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f584])).
% 0.54/0.37 tff(f586,plain,(
% 0.54/0.37 $false | (spl12_7 | ~spl12_9 | ~spl12_38 | ~spl12_39)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f583,f535])).
% 0.54/0.37 tff(f587,plain,(
% 0.54/0.37 spl12_7 | ~spl12_9 | ~spl12_38 | ~spl12_39),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f586])).
% 0.54/0.37 tff(f592,plain,(
% 0.54/0.37 f2($true) | (~spl12_4 | ~spl12_5)),
% 0.54/0.37 inference(forward_demodulation,[],[f80,f75])).
% 0.54/0.37 tff(f593,plain,(
% 0.54/0.37 ($true = $false) | (~spl12_13 | ~spl12_35)),
% 0.54/0.37 inference(forward_demodulation,[],[f121,f274])).
% 0.54/0.37 tff(f594,plain,(
% 0.54/0.37 $false | (~spl12_13 | ~spl12_35)),
% 0.54/0.37 inference(trivial_inequality_removal,[],[f593])).
% 0.54/0.37 tff(f595,plain,(
% 0.54/0.37 ~spl12_13 | ~spl12_35),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f594])).
% 0.54/0.37 tff(f598,plain,(
% 0.54/0.37 $false | (~spl12_4 | ~spl12_5 | spl12_33)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f592,f262])).
% 0.54/0.37 tff(f599,plain,(
% 0.54/0.37 ~spl12_4 | ~spl12_5 | spl12_33),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f598])).
% 0.54/0.37 tff(f600,plain,(
% 0.54/0.37 ($true = $false) | (~spl12_15 | ~spl12_34)),
% 0.54/0.37 inference(forward_demodulation,[],[f131,f268])).
% 0.54/0.37 tff(f601,plain,(
% 0.54/0.37 $false | (~spl12_15 | ~spl12_34)),
% 0.54/0.37 inference(trivial_inequality_removal,[],[f600])).
% 0.54/0.37 tff(f602,plain,(
% 0.54/0.37 ~spl12_15 | ~spl12_34),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f601])).
% 0.54/0.37 tff(f604,plain,(
% 0.54/0.37 spl12_31 | ~spl12_6 | ~spl12_7),
% 0.54/0.37 inference(avatar_split_clause,[],[f555,f89,f83,f250])).
% 0.54/0.37 tff(f610,plain,(
% 0.54/0.37 ~spl12_31 | ~spl12_19 | spl12_20),
% 0.54/0.37 inference(avatar_split_clause,[],[f379,f155,f149,f250])).
% 0.54/0.37 tff(f624,plain,(
% 0.54/0.37 f2($false) | (~spl12_5 | ~spl12_40)),
% 0.54/0.37 inference(forward_demodulation,[],[f80,f304])).
% 0.54/0.37 tff(f625,plain,(
% 0.54/0.37 $false | (~spl12_5 | spl12_18 | ~spl12_32 | ~spl12_40)),
% 0.54/0.37 inference(forward_subsumption_resolution,[],[f624,f520])).
% 0.54/0.37 tff(f626,plain,(
% 0.54/0.37 ~spl12_5 | spl12_18 | ~spl12_32 | ~spl12_40),
% 0.54/0.37 inference(avatar_contradiction_clause,[],[f625])).
% 0.54/0.37 cnf(s1, plain, spl12_1 | spl12_2, inference(sat_conversion,[],[f66])).
% 0.54/0.37 cnf(s2, plain, ~spl12_1 | ~spl12_2, inference(sat_conversion,[],[f67])).
% 0.54/0.37 cnf(s3, plain, ~spl12_3 | spl12_4, inference(sat_conversion,[],[f76])).
% 0.54/0.37 cnf(s4, plain, spl12_3 | ~spl12_4, inference(sat_conversion,[],[f77])).
% 0.54/0.37 cnf(s5, plain, ~spl12_5 | spl12_6, inference(sat_conversion,[],[f86])).
% 0.54/0.37 cnf(s6, plain, spl12_5 | ~spl12_6, inference(sat_conversion,[],[f87])).
% 0.54/0.37 cnf(s7, plain, ~spl12_7 | spl12_8, inference(sat_conversion,[],[f96])).
% 0.54/0.37 cnf(s8, plain, spl12_7 | ~spl12_8, inference(sat_conversion,[],[f97])).
% 0.54/0.37 cnf(s9, plain, ~spl12_9 | spl12_10, inference(sat_conversion,[],[f106])).
% 0.54/0.37 cnf(s10, plain, spl12_9 | ~spl12_10, inference(sat_conversion,[],[f107])).
% 0.54/0.37 cnf(s11, plain, ~spl12_11 | spl12_12, inference(sat_conversion,[],[f116])).
% 0.54/0.37 cnf(s12, plain, spl12_11 | ~spl12_12, inference(sat_conversion,[],[f117])).
% 0.54/0.38 cnf(s13, plain, ~spl12_3 | spl12_13, inference(sat_conversion,[],[f122])).
% 0.54/0.38 cnf(s14, plain, spl12_3 | ~spl12_13, inference(sat_conversion,[],[f123])).
% 0.54/0.38 cnf(s15, plain, ~spl12_14 | spl12_15, inference(sat_conversion,[],[f132])).
% 0.54/0.38 cnf(s16, plain, spl12_14 | ~spl12_15, inference(sat_conversion,[],[f133])).
% 0.54/0.38 cnf(s17, plain, ~spl12_16 | spl12_17, inference(sat_conversion,[],[f142])).
% 0.54/0.38 cnf(s18, plain, spl12_16 | ~spl12_17, inference(sat_conversion,[],[f143])).
% 0.54/0.38 cnf(s19, plain, ~spl12_18 | spl12_19, inference(sat_conversion,[],[f152])).
% 0.54/0.38 cnf(s20, plain, spl12_18 | ~spl12_19, inference(sat_conversion,[],[f153])).
% 0.54/0.38 cnf(s21, plain, ~spl12_20 | spl12_21, inference(sat_conversion,[],[f162])).
% 0.54/0.38 cnf(s22, plain, spl12_20 | ~spl12_21, inference(sat_conversion,[],[f163])).
% 0.54/0.38 cnf(s23, plain, ~spl12_22 | spl12_23, inference(sat_conversion,[],[f172])).
% 0.54/0.38 cnf(s24, plain, spl12_22 | ~spl12_23, inference(sat_conversion,[],[f173])).
% 0.54/0.38 cnf(s25, plain, ~spl12_24 | spl12_25, inference(sat_conversion,[],[f182])).
% 0.54/0.38 cnf(s26, plain, spl12_24 | ~spl12_25, inference(sat_conversion,[],[f183])).
% 0.54/0.38 cnf(s27, plain, ~spl12_2 | spl12_26 | spl12_27, inference(sat_conversion,[],[f231])).
% 0.54/0.38 cnf(s28, plain, spl12_25 | spl12_26, inference(sat_conversion,[],[f232])).
% 0.54/0.38 cnf(s29, plain, spl12_24 | ~spl12_27 | spl12_28, inference(sat_conversion,[],[f237])).
% 0.54/0.38 cnf(s30, plain, spl12_23 | spl12_28, inference(sat_conversion,[],[f238])).
% 0.54/0.38 cnf(s32, plain, spl12_21 | spl12_29, inference(sat_conversion,[],[f244])).
% 0.54/0.38 cnf(s34, plain, spl12_19 | spl12_30, inference(sat_conversion,[],[f254])).
% 0.54/0.38 cnf(s35, plain, spl12_18 | spl12_32 | ~spl12_33, inference(sat_conversion,[],[f263])).
% 0.54/0.38 cnf(s36, plain, spl12_17 | spl12_32, inference(sat_conversion,[],[f264])).
% 0.54/0.38 cnf(s37, plain, spl12_16 | ~spl12_33 | spl12_34, inference(sat_conversion,[],[f269])).
% 0.54/0.38 cnf(s38, plain, spl12_15 | spl12_34, inference(sat_conversion,[],[f270])).
% 0.54/0.38 cnf(s39, plain, spl12_14 | ~spl12_33 | spl12_35, inference(sat_conversion,[],[f275])).
% 0.54/0.38 cnf(s40, plain, spl12_13 | spl12_35, inference(sat_conversion,[],[f276])).
% 0.54/0.38 cnf(s41, plain, spl12_1 | ~spl12_27 | spl12_36, inference(sat_conversion,[],[f281])).
% 0.54/0.38 cnf(s42, plain, spl12_12 | spl12_36, inference(sat_conversion,[],[f282])).
% 0.54/0.38 cnf(s43, plain, spl12_11 | ~spl12_31 | spl12_37, inference(sat_conversion,[],[f287])).
% 0.54/0.38 cnf(s44, plain, spl12_10 | spl12_37, inference(sat_conversion,[],[f288])).
% 0.54/0.38 cnf(s46, plain, spl12_8 | spl12_38, inference(sat_conversion,[],[f294])).
% 0.54/0.38 cnf(s47, plain, spl12_7 | ~spl12_31 | spl12_39, inference(sat_conversion,[],[f299])).
% 0.54/0.38 cnf(s48, plain, spl12_6 | spl12_39, inference(sat_conversion,[],[f300])).
% 0.54/0.38 cnf(s50, plain, spl12_4 | spl12_40, inference(sat_conversion,[],[f306])).
% 0.54/0.38 cnf(s56, plain, ~spl12_19 | ~spl12_20 | spl12_31, inference(sat_conversion,[],[f326])).
% 0.54/0.38 cnf(s57, plain, ~spl12_21 | ~spl12_22 | spl12_27, inference(sat_conversion,[],[f328])).
% 0.54/0.38 cnf(s61, plain, spl12_2 | spl12_26 | ~spl12_27, inference(sat_conversion,[],[f338])).
% 0.54/0.38 cnf(s65, plain, ~spl12_12 | ~spl12_36, inference(sat_conversion,[],[f359])).
% 0.54/0.38 cnf(s68, plain, ~spl12_8 | spl12_9 | ~spl12_31, inference(sat_conversion,[],[f370])).
% 0.54/0.38 cnf(s69, plain, spl12_11 | ~spl12_20 | ~spl12_30 | ~spl12_37, inference(sat_conversion,[],[f372])).
% 0.54/0.38 cnf(s71, plain, spl12_22 | ~spl12_24 | ~spl12_28 | ~spl12_29, inference(sat_conversion,[],[f376])).
% 0.54/0.38 cnf(s74, plain, ~spl12_1 | spl12_22 | ~spl12_29 | ~spl12_36, inference(sat_conversion,[],[f381])).
% 0.54/0.38 cnf(s76, plain, ~spl12_1 | spl12_2 | ~spl12_26 | ~spl12_36, inference(sat_conversion,[],[f393])).
% 0.54/0.38 cnf(s77, plain, ~spl12_1 | ~spl12_12 | spl12_27, inference(sat_conversion,[],[f395])).
% 0.54/0.38 cnf(s78, plain, ~spl12_23 | ~spl12_24 | spl12_27, inference(sat_conversion,[],[f397])).
% 0.54/0.38 cnf(s79, plain, ~spl12_25 | ~spl12_26, inference(sat_conversion,[],[f400])).
% 0.54/0.38 cnf(s82, plain, spl12_16 | ~spl12_18 | ~spl12_32 | ~spl12_34, inference(sat_conversion,[],[f433])).
% 0.54/0.38 cnf(s83, plain, ~spl12_6 | ~spl12_39, inference(sat_conversion,[],[f437])).
% 0.54/0.38 cnf(s84, plain, ~spl12_13 | ~spl12_14 | spl12_33, inference(sat_conversion,[],[f439])).
% 0.54/0.38 cnf(s85, plain, ~spl12_15 | ~spl12_16 | spl12_33, inference(sat_conversion,[],[f440])).
% 0.54/0.38 cnf(s87, plain, ~spl12_17 | ~spl12_18 | spl12_33, inference(sat_conversion,[],[f445])).
% 0.54/0.38 cnf(s91, plain, ~spl12_4 | spl12_5 | ~spl12_33, inference(sat_conversion,[],[f453])).
% 0.54/0.38 cnf(s92, plain, spl12_9 | ~spl12_11 | ~spl12_37 | ~spl12_38, inference(sat_conversion,[],[f460])).
% 0.54/0.38 cnf(s95, plain, spl12_5 | ~spl12_14 | ~spl12_35 | ~spl12_40, inference(sat_conversion,[],[f467])).
% 0.54/0.38 cnf(s102, plain, ~spl12_11 | spl12_20 | ~spl12_30 | ~spl12_37, inference(sat_conversion,[],[f473])).
% 0.54/0.38 cnf(s104, plain, ~spl12_21 | spl12_22 | ~spl12_27, inference(sat_conversion,[],[f479])).
% 0.54/0.38 cnf(s107, plain, ~spl12_8 | ~spl12_9 | spl12_31, inference(sat_conversion,[],[f486])).
% 0.54/0.38 cnf(s108, plain, ~spl12_10 | ~spl12_11 | spl12_31, inference(sat_conversion,[],[f487])).
% 0.54/0.38 cnf(s111, plain, ~spl12_7 | spl12_20 | ~spl12_30 | ~spl12_39, inference(sat_conversion,[],[f534])).
% 0.54/0.38 cnf(s116, plain, ~spl12_2 | spl12_24 | ~spl12_26 | ~spl12_28, inference(sat_conversion,[],[f542])).
% 0.54/0.38 cnf(s117, plain, ~spl12_23 | spl12_24 | ~spl12_27, inference(sat_conversion,[],[f544])).
% 0.54/0.38 cnf(s118, plain, spl12_1 | ~spl12_22 | ~spl12_29 | ~spl12_36, inference(sat_conversion,[],[f553])).
% 0.54/0.38 cnf(s120, plain, ~spl12_17 | spl12_18 | ~spl12_33, inference(sat_conversion,[],[f565])).
% 0.54/0.38 cnf(s121, plain, spl12_14 | ~spl12_16 | ~spl12_34 | ~spl12_35, inference(sat_conversion,[],[f568])).
% 0.54/0.38 cnf(s125, plain, ~spl12_10 | spl12_11 | ~spl12_31, inference(sat_conversion,[],[f571])).
% 0.54/0.38 cnf(s135, plain, spl12_7 | ~spl12_20 | ~spl12_30 | ~spl12_39, inference(sat_conversion,[],[f585])).
% 0.54/0.38 cnf(s136, plain, spl12_7 | ~spl12_9 | ~spl12_38 | ~spl12_39, inference(sat_conversion,[],[f587])).
% 0.54/0.38 cnf(s139, plain, ~spl12_13 | ~spl12_35, inference(sat_conversion,[],[f595])).
% 0.54/0.38 cnf(s140, plain, ~spl12_4 | ~spl12_5 | spl12_33, inference(sat_conversion,[],[f599])).
% 0.54/0.38 cnf(s143, plain, ~spl12_15 | ~spl12_34, inference(sat_conversion,[],[f602])).
% 0.54/0.38 cnf(s144, plain, ~spl12_6 | ~spl12_7 | spl12_31, inference(sat_conversion,[],[f604])).
% 0.54/0.38 cnf(s154, plain, ~spl12_19 | spl12_20 | ~spl12_31, inference(sat_conversion,[],[f610])).
% 0.54/0.38 cnf(s167, plain, ~spl12_5 | spl12_18 | ~spl12_32 | ~spl12_40, inference(sat_conversion,[],[f626])).
% 0.54/0.38 cnf(s168, plain, spl12_24 | ~spl12_28 | ~spl12_2, inference(rat,[],[s28,s26,s116])).
% 0.54/0.38 cnf(s169, plain, spl12_7 | ~spl12_30 | ~spl12_39 | spl12_1, inference(rat,[],[s168,s71,s30,s24,s118,s42,s12,s102,s44,s10,s136,s32,s46,s22,s8,s135,s1])).
% 0.54/0.38 cnf(s170, plain, spl12_24 | ~spl12_21 | ~spl12_2, inference(rat,[],[s24,s57,s30,s29,s168])).
% 0.54/0.38 cnf(s171, plain, spl12_5 | spl12_3 | spl12_1, inference(rat,[],[s107,s10,s43,s44,s69,s11,s65,s41,s27,s79,s25,s170,s21,s7,s111,s169,s34,s20,s82,s36,s18,s121,s38,s16,s48,s95,s6,s1,s40,s14,s50,s4])).
% 0.54/0.38 cnf(s172, plain, spl12_18 | ~spl12_5 | ~spl12_40 | ~spl12_35, inference(rat,[],[s121,s15,s38,s85,s18,s36,s35,s167])).
% 0.54/0.38 cnf(s173, plain, spl12_24 | spl12_3 | spl12_1, inference(rat,[],[s92,s46,s9,s44,s8,s108,s144,s154,s12,s42,s118,s24,s21,s32,s30,s170,s168,s1,s5,s19,s172,s171,s50,s4,s40,s14])).
% 0.54/0.38 cnf(s174, plain, ~spl12_31 | spl12_11 | spl12_39, inference(rat,[],[s68,s7,s9,s47,s125])).
% 0.54/0.38 cnf(s175, plain, spl12_3 | spl12_1, inference(rat,[],[s30,s71,s24,s118,s32,s22,s56,s174,s11,s65,s41,s27,s79,s25,s173,s19,s172,s83,s5,s171,s50,s40,s4,s14,s1])).
% 0.54/0.38 cnf(s176, plain, spl12_19 | spl12_11 | ~spl12_20 | ~spl12_3, inference(rat,[],[s37,s143,s17,s15,s120,s39,s140,s6,s48,s136,s7,s46,s107,s10,s43,s44,s69,s19,s34,s3,s139,s13])).
% 0.54/0.38 cnf(s177, plain, ~spl12_20 | spl12_1, inference(rat,[],[s38,s82,s16,s17,s36,s84,s87,s91,s5,s83,s174,s56,s20,s176,s11,s65,s41,s27,s79,s25,s170,s21,s1,s13,s3,s175])).
% 0.54/0.38 cnf(s178, plain, ~spl12_39 | ~spl12_30 | spl12_1, inference(rat,[],[s111,s169,s177])).
% 0.54/0.38 cnf(s179, plain, spl12_19 | spl12_1, inference(rat,[],[s37,s143,s17,s15,s120,s39,s140,s6,s48,s178,s19,s34,s3,s139,s13,s175])).
% 0.54/0.38 cnf(s180, plain, spl12_33 | spl12_1, inference(rat,[],[s38,s82,s16,s17,s36,s84,s87,s13,s175,s20,s179])).
% 0.54/0.38 cnf(s181, plain, spl12_22 | spl12_1, inference(rat,[],[s168,s71,s30,s24,s1,s32,s22,s177])).
% 0.54/0.38 cnf(s182, plain, spl12_1, inference(rat,[],[s92,s9,s44,s108,s12,s42,s118,s181,s46,s8,s144,s5,s91,s180,s154,s179,s32,s22,s177,s3,s175])).
% 0.54/0.38 cnf(s183, plain, ~spl12_2, inference(rat,[],[s2,s182])).
% 0.54/0.38 cnf(s184, plain, ~spl12_36 | ~spl12_29, inference(rat,[],[s26,s78,s23,s28,s61,s74,s76,s183,s182])).
% 0.54/0.38 cnf(s185, plain, spl12_20 | ~spl12_19 | ~spl12_6, inference(rat,[],[s92,s9,s44,s108,s12,s42,s184,s46,s8,s144,s32,s154,s22])).
% 0.54/0.38 cnf(s186, plain, ~spl12_27 | ~spl12_21, inference(rat,[],[s25,s117,s79,s23,s61,s104,s183])).
% 0.54/0.38 cnf(s187, plain, ~spl12_19 | ~spl12_6, inference(rat,[],[s186,s77,s11,s174,s56,s21,s185,s83,s182])).
% 0.54/0.38 cnf(s188, plain, ~spl12_3 | ~spl12_6, inference(rat,[],[s37,s143,s17,s15,s120,s39,s140,s139,s3,s13,s6,s19,s187])).
% 0.54/0.38 cnf(s189, plain, ~spl12_6, inference(rat,[],[s172,s50,s40,s4,s14,s188,s19,s187,s6])).
% 0.54/0.38 cnf(s190, plain, spl12_39, inference(rat,[],[s48,s189])).
% 0.54/0.38 cnf(s191, plain, ~spl12_5, inference(rat,[],[s5,s189])).
% 0.54/0.38 cnf(s192, plain, ~spl12_30 | spl12_20, inference(rat,[],[s136,s10,s46,s44,s8,s102,s111,s12,s42,s184,s32,s22,s190])).
% 0.54/0.38 cnf(s193, plain, ~spl12_3 | ~spl12_18, inference(rat,[],[s38,s82,s16,s17,s36,s84,s87,s91,s3,s13,s191])).
% 0.54/0.38 cnf(s194, plain, ~spl12_18, inference(rat,[],[s36,s82,s18,s121,s38,s16,s95,s50,s40,s4,s14,s193,s191])).
% 0.54/0.38 cnf(s195, plain, ~spl12_19, inference(rat,[],[s20,s194])).
% 0.54/0.38 cnf(s196, plain, spl12_30, inference(rat,[],[s34,s195])).
% 0.54/0.38 cnf(s197, plain, spl12_20, inference(rat,[],[s192,s196])).
% 0.54/0.38 cnf(s198, plain, spl12_21, inference(rat,[],[s21,s197])).
% 0.54/0.38 cnf(s199, plain, spl12_7, inference(rat,[],[s135,s190,s196,s197])).
% 0.54/0.38 cnf(s201, plain, ~spl12_27, inference(rat,[],[s186,s198])).
% 0.54/0.38 cnf(s202, plain, spl12_8, inference(rat,[],[s7,s199])).
% 0.54/0.38 cnf(s204, plain, ~spl12_12, inference(rat,[],[s77,s182,s201])).
% 0.54/0.38 cnf(s207, plain, ~spl12_11, inference(rat,[],[s11,s204])).
% 0.54/0.38 cnf(s211, plain, ~spl12_37, inference(rat,[],[s69,s197,s196,s207])).
% 0.54/0.38 cnf(s216, plain, spl12_10, inference(rat,[],[s44,s211])).
% 0.54/0.38 cnf(s217, plain, ~spl12_31, inference(rat,[],[s43,s207,s211])).
% 0.54/0.38 cnf(s220, plain, spl12_9, inference(rat,[],[s10,s216])).
% 0.54/0.38 cnf(s221, plain, $false, inference(rat,[],[s107,s202,s217,s220])).
% 0.54/0.38 tff(f627,plain,(
% 0.54/0.38 $false),
% 0.54/0.38 inference(avatar_sat_refutation,[],[s221])).
% 0.54/0.38 % SZS output end Proof for theBenchmark
% 0.54/0.38 % (3817647)------------------------------
% 0.54/0.38 % (3817647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.38 % (3817647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.38 % (3817647)CaDiCaL version: 2.1.3
% 0.54/0.38 % (3817647)Termination reason: Refutation
% 0.54/0.38 % (3817647)Time elapsed: 0.011 s
% 0.54/0.38 % (3817647)Peak memory usage: 12 MB
% 0.54/0.38 % (3817647)Instructions burned: 18 (million)
% 0.54/0.38 % (3817637)Success in time 0.035 s
% 0.54/0.38 % Vampire exiting
%------------------------------------------------------------------------------