%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI646_1 : TPTP v9.3.1. Released v6.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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 09:35:01 AM UTC 2026
% Result : Theorem 0.50s 0.41s
% Output : Refutation 0.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ARI646_1 : TPTP v9.3.1. Released v6.3.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.26 % Computer : n011.cluster.edu
% 0.09/0.26 % Model : x86_64 x86_64
% 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.26 % Memory : 8046.5625MB
% 0.09/0.26 % OS : Linux 6.8.0-71-generic
% 0.09/0.26 % CPULimit : 300
% 0.09/0.26 % WCLimit : 300
% 0.09/0.27 % DateTime : Mon Sep 28 20:54:46 UTC 2026
% 0.09/0.27 % CPUTime :
% 0.09/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.32 Running first-order model finding
% 0.25/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.50/0.41 % (3775477)Will run a generic schedule for satisfiability detection.
% 0.50/0.41 % (3775488)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1671636966:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.50/0.41 % (3775483)% WARNING: option uhcvi not known.
% 0.50/0.41 % (3775482)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3273151278_2999 on theBenchmark for (2999ds/0Mi)
% 0.50/0.41 % (3775485)dis+10_1_sil=32000:sp=arity:random_seed=3001890010:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.50/0.41 % (3775483)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3504671707:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.50/0.41 % (3775484)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3139983623:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.50/0.41 % (3775482)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.50/0.41 % (3775482)Terminated due to inappropriate strategy.
% 0.50/0.41 % (3775482)------------------------------
% 0.50/0.41 % (3775482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.41 % (3775482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.41 % (3775487)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1262262054:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.50/0.41 % (3775482)CaDiCaL version: 2.1.3
% 0.50/0.41 % (3775482)Termination reason: Inappropriate
% 0.50/0.41 % (3775482)Time elapsed: 0.001 s
% 0.50/0.41 % (3775482)Peak memory usage: 10 MB
% 0.50/0.41 % (3775486)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1405767038:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.50/0.41 % (3775482)------------------------------
% 0.50/0.41 % (3775482)------------------------------
% 0.50/0.41 % (3775496)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4222537713:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.50/0.41 % (3775496)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.50/0.41 % (3775496)Terminated due to inappropriate strategy.
% 0.50/0.41 % (3775496)------------------------------
% 0.50/0.41 % (3775496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.41 % (3775496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.41 % (3775496)CaDiCaL version: 2.1.3
% 0.50/0.41 % (3775496)Termination reason: Inappropriate
% 0.50/0.41 % (3775496)Time elapsed: 0.001 s
% 0.50/0.41 % (3775496)Peak memory usage: 10 MB
% 0.50/0.41 % (3775496)------------------------------
% 0.50/0.41 % (3775496)------------------------------
% 0.50/0.41 % (3775487) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3775477-3775487"...
% 0.50/0.41 % (3775487)...printing done.
% 0.50/0.41 % (3775487)Refutation found. Thanks to Tanya!
% 0.50/0.41 % SZS status Theorem for theBenchmark
% 0.50/0.41 % SZS output start Proof for theBenchmark
% 0.50/0.41 tff(func_def_0, type, a: $int).
% 0.50/0.41 tff(f1,conjecture,(
% 0.50/0.41 ($greater(10,a) & $lesseq(0,a)) <=> (a = 9 | a = 8 | a = 7 | a = 6 | a = 5 | a = 4 | a = 3 | a = 2 | a = 1 | a = 0)),
% 0.50/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 0.50/0.41 tff(f2,negated_conjecture,(
% 0.50/0.41 ~(($greater(10,a) & $lesseq(0,a)) <=> (a = 9 | a = 8 | a = 7 | a = 6 | a = 5 | a = 4 | a = 3 | a = 2 | a = 1 | a = 0))),
% 0.50/0.41 inference(negated_conjecture,[status(cth)],[f1])).
% 0.50/0.41 tff(f3,plain,(
% 0.50/0.41 ~(($less(a,10) & ~$less(a,0)) <=> (a = 9 | a = 8 | a = 7 | a = 6 | a = 5 | a = 4 | a = 3 | a = 2 | a = 1 | a = 0))),
% 0.50/0.41 inference(theory_normalization,[],[f2])).
% 0.50/0.41 tff(f4,definition,(
% 0.50/0.41 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 0.50/0.41 introduced(theory,[tha_commutativity])).
% 0.50/0.41 tff(f9,definition,(
% 0.50/0.41 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 0.50/0.41 introduced(theory,[tha_non-reflexivity])).
% 0.50/0.41 tff(f11,definition,(
% 0.50/0.41 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | $less(X1,X0) | X0 = X1) )),
% 0.50/0.41 introduced(theory,[tha_order_totality])).
% 0.50/0.41 tff(f12,definition,(
% 0.50/0.41 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,X2),$sum(X1,X2))) )),
% 0.50/0.41 introduced(theory,[tha_order_monotonicity])).
% 0.50/0.41 tff(f15,definition,(
% 0.50/0.41 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,$sum(X0,1))) )),
% 0.50/0.41 introduced(theory,[tha_extra_integer_ordering])).
% 0.50/0.41 tff(f16,plain,(
% 0.50/0.41 ($less(a,10) & ~$less(a,0)) <~> (a = 9 | a = 8 | a = 7 | a = 6 | a = 5 | a = 4 | a = 3 | a = 2 | a = 1 | a = 0)),
% 0.50/0.41 inference(ennf_transformation,[],[f3])).
% 0.50/0.41 tff(f17,definition,(
% 0.50/0.41 sP0 <=> (a = 9 | a = 8 | a = 7 | a = 6 | a = 5 | a = 4 | a = 3 | a = 2 | a = 1 | a = 0)),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction])).
% 0.50/0.41 tff(f18,plain,(
% 0.50/0.41 ($less(a,10) & ~$less(a,0)) <~> sP0),
% 0.50/0.41 inference(definition_folding,[],[f16,f17])).
% 0.50/0.41 tff(f19,plain,(
% 0.50/0.41 (sP0 | (a != 9 & a != 8 & a != 7 & a != 6 & a != 5 & a != 4 & a != 3 & a != 2 & a != 1 & a != 0)) & ((a = 9 | a = 8 | a = 7 | a = 6 | a = 5 | a = 4 | a = 3 | a = 2 | a = 1 | a = 0) | ~sP0)),
% 0.50/0.41 inference(nnf_transformation,[],[f17])).
% 0.50/0.41 tff(f20,plain,(
% 0.50/0.41 (sP0 | (a != 9 & a != 8 & a != 7 & a != 6 & a != 5 & a != 4 & a != 3 & a != 2 & a != 1 & a != 0)) & (a = 9 | a = 8 | a = 7 | a = 6 | a = 5 | a = 4 | a = 3 | a = 2 | a = 1 | a = 0 | ~sP0)),
% 0.50/0.41 inference(flattening,[],[f19])).
% 0.50/0.41 tff(f21,plain,(
% 0.50/0.41 (~sP0 | (~$less(a,10) | $less(a,0))) & (sP0 | ($less(a,10) & ~$less(a,0)))),
% 0.50/0.41 inference(nnf_transformation,[],[f18])).
% 0.50/0.41 tff(f22,plain,(
% 0.50/0.41 (~sP0 | ~$less(a,10) | $less(a,0)) & (sP0 | ($less(a,10) & ~$less(a,0)))),
% 0.50/0.41 inference(flattening,[],[f21])).
% 0.50/0.41 tff(f23,plain,(
% 0.50/0.41 a = 9 | a = 8 | a = 7 | a = 6 | a = 5 | a = 4 | a = 3 | a = 2 | a = 1 | a = 0 | ~sP0),
% 0.50/0.41 inference(cnf_transformation,[],[f20])).
% 0.50/0.41 tff(f24,plain,(
% 0.50/0.41 sP0 | a != 0),
% 0.50/0.41 inference(cnf_transformation,[],[f20])).
% 0.50/0.41 tff(f25,plain,(
% 0.50/0.41 sP0 | a != 1),
% 0.50/0.41 inference(cnf_transformation,[],[f20])).
% 0.50/0.41 tff(f26,plain,(
% 0.50/0.41 sP0 | a != 2),
% 0.50/0.41 inference(cnf_transformation,[],[f20])).
% 0.50/0.41 tff(f27,plain,(
% 0.50/0.41 sP0 | a != 3),
% 0.50/0.41 inference(cnf_transformation,[],[f20])).
% 0.50/0.41 tff(f28,plain,(
% 0.50/0.41 sP0 | a != 4),
% 0.50/0.41 inference(cnf_transformation,[],[f20])).
% 0.50/0.41 tff(f29,plain,(
% 0.50/0.41 sP0 | a != 5),
% 0.50/0.41 inference(cnf_transformation,[],[f20])).
% 0.50/0.41 tff(f30,plain,(
% 0.50/0.41 sP0 | a != 6),
% 0.50/0.41 inference(cnf_transformation,[],[f20])).
% 0.50/0.41 tff(f31,plain,(
% 0.50/0.41 sP0 | a != 7),
% 0.50/0.41 inference(cnf_transformation,[],[f20])).
% 0.50/0.41 tff(f32,plain,(
% 0.50/0.41 sP0 | a != 8),
% 0.50/0.41 inference(cnf_transformation,[],[f20])).
% 0.50/0.41 tff(f33,plain,(
% 0.50/0.41 sP0 | a != 9),
% 0.50/0.41 inference(cnf_transformation,[],[f20])).
% 0.50/0.41 tff(f34,plain,(
% 0.50/0.41 sP0 | ~$less(a,0)),
% 0.50/0.41 inference(cnf_transformation,[],[f22])).
% 0.50/0.41 tff(f35,plain,(
% 0.50/0.41 sP0 | $less(a,10)),
% 0.50/0.41 inference(cnf_transformation,[],[f22])).
% 0.50/0.41 tff(f36,plain,(
% 0.50/0.41 ~sP0 | ~$less(a,10) | $less(a,0)),
% 0.50/0.41 inference(cnf_transformation,[],[f22])).
% 0.50/0.41 tff(f38,definition,(
% 0.50/0.41 spl1_1 <=> $less(a,0)),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition])).
% 0.50/0.41 tff(f39,plain,(
% 0.50/0.41 $less(a,0) | ~spl1_1),
% 0.50/0.41 inference(avatar_component_clause,[],[f38])).
% 0.50/0.41 tff(f40,plain,(
% 0.50/0.41 ~$less(a,0) | spl1_1),
% 0.50/0.41 inference(avatar_component_clause,[],[f38])).
% 0.50/0.41 tff(f42,definition,(
% 0.50/0.41 spl1_2 <=> sP0),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition])).
% 0.50/0.41 tff(f45,plain,(
% 0.50/0.41 ~spl1_1 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f34,f42,f38])).
% 0.50/0.41 tff(f47,definition,(
% 0.50/0.41 spl1_3 <=> $less(a,10)),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition])).
% 0.50/0.41 tff(f48,plain,(
% 0.50/0.41 ~$less(a,10) | spl1_3),
% 0.50/0.41 inference(avatar_component_clause,[],[f47])).
% 0.50/0.41 tff(f49,plain,(
% 0.50/0.41 $less(a,10) | ~spl1_3),
% 0.50/0.41 inference(avatar_component_clause,[],[f47])).
% 0.50/0.41 tff(f50,plain,(
% 0.50/0.41 spl1_3 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f35,f42,f47])).
% 0.50/0.41 tff(f51,plain,(
% 0.50/0.41 spl1_1 | ~spl1_3 | ~spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f36,f42,f47,f38])).
% 0.50/0.41 tff(f53,definition,(
% 0.50/0.41 spl1_4 <=> a = 0),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition])).
% 0.50/0.41 tff(f54,plain,(
% 0.50/0.41 a != 0 | spl1_4),
% 0.50/0.41 inference(avatar_component_clause,[],[f53])).
% 0.50/0.41 tff(f55,plain,(
% 0.50/0.41 a = 0 | ~spl1_4),
% 0.50/0.41 inference(avatar_component_clause,[],[f53])).
% 0.50/0.41 tff(f57,definition,(
% 0.50/0.41 spl1_5 <=> a = 1),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_5])],[avatar_definition])).
% 0.50/0.41 tff(f58,plain,(
% 0.50/0.41 a != 1 | spl1_5),
% 0.50/0.41 inference(avatar_component_clause,[],[f57])).
% 0.50/0.41 tff(f59,plain,(
% 0.50/0.41 a = 1 | ~spl1_5),
% 0.50/0.41 inference(avatar_component_clause,[],[f57])).
% 0.50/0.41 tff(f61,definition,(
% 0.50/0.41 spl1_6 <=> a = 2),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_6])],[avatar_definition])).
% 0.50/0.41 tff(f62,plain,(
% 0.50/0.41 a != 2 | spl1_6),
% 0.50/0.41 inference(avatar_component_clause,[],[f61])).
% 0.50/0.41 tff(f63,plain,(
% 0.50/0.41 a = 2 | ~spl1_6),
% 0.50/0.41 inference(avatar_component_clause,[],[f61])).
% 0.50/0.41 tff(f65,definition,(
% 0.50/0.41 spl1_7 <=> a = 3),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition])).
% 0.50/0.41 tff(f66,plain,(
% 0.50/0.41 a != 3 | spl1_7),
% 0.50/0.41 inference(avatar_component_clause,[],[f65])).
% 0.50/0.41 tff(f67,plain,(
% 0.50/0.41 a = 3 | ~spl1_7),
% 0.50/0.41 inference(avatar_component_clause,[],[f65])).
% 0.50/0.41 tff(f69,definition,(
% 0.50/0.41 spl1_8 <=> a = 4),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition])).
% 0.50/0.41 tff(f70,plain,(
% 0.50/0.41 a != 4 | spl1_8),
% 0.50/0.41 inference(avatar_component_clause,[],[f69])).
% 0.50/0.41 tff(f71,plain,(
% 0.50/0.41 a = 4 | ~spl1_8),
% 0.50/0.41 inference(avatar_component_clause,[],[f69])).
% 0.50/0.41 tff(f73,definition,(
% 0.50/0.41 spl1_9 <=> a = 5),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition])).
% 0.50/0.41 tff(f74,plain,(
% 0.50/0.41 a != 5 | spl1_9),
% 0.50/0.41 inference(avatar_component_clause,[],[f73])).
% 0.50/0.41 tff(f75,plain,(
% 0.50/0.41 a = 5 | ~spl1_9),
% 0.50/0.41 inference(avatar_component_clause,[],[f73])).
% 0.50/0.41 tff(f77,definition,(
% 0.50/0.41 spl1_10 <=> a = 6),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_10])],[avatar_definition])).
% 0.50/0.41 tff(f78,plain,(
% 0.50/0.41 a != 6 | spl1_10),
% 0.50/0.41 inference(avatar_component_clause,[],[f77])).
% 0.50/0.41 tff(f79,plain,(
% 0.50/0.41 a = 6 | ~spl1_10),
% 0.50/0.41 inference(avatar_component_clause,[],[f77])).
% 0.50/0.41 tff(f81,definition,(
% 0.50/0.41 spl1_11 <=> a = 7),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_11])],[avatar_definition])).
% 0.50/0.41 tff(f82,plain,(
% 0.50/0.41 a != 7 | spl1_11),
% 0.50/0.41 inference(avatar_component_clause,[],[f81])).
% 0.50/0.41 tff(f83,plain,(
% 0.50/0.41 a = 7 | ~spl1_11),
% 0.50/0.41 inference(avatar_component_clause,[],[f81])).
% 0.50/0.41 tff(f85,definition,(
% 0.50/0.41 spl1_12 <=> a = 8),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_12])],[avatar_definition])).
% 0.50/0.41 tff(f86,plain,(
% 0.50/0.41 a != 8 | spl1_12),
% 0.50/0.41 inference(avatar_component_clause,[],[f85])).
% 0.50/0.41 tff(f87,plain,(
% 0.50/0.41 a = 8 | ~spl1_12),
% 0.50/0.41 inference(avatar_component_clause,[],[f85])).
% 0.50/0.41 tff(f89,definition,(
% 0.50/0.41 spl1_13 <=> a = 9),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_13])],[avatar_definition])).
% 0.50/0.41 tff(f90,plain,(
% 0.50/0.41 a != 9 | spl1_13),
% 0.50/0.41 inference(avatar_component_clause,[],[f89])).
% 0.50/0.41 tff(f91,plain,(
% 0.50/0.41 a = 9 | ~spl1_13),
% 0.50/0.41 inference(avatar_component_clause,[],[f89])).
% 0.50/0.41 tff(f92,plain,(
% 0.50/0.41 ~spl1_2 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12 | spl1_13),
% 0.50/0.41 inference(avatar_split_clause,[],[f23,f89,f85,f81,f77,f73,f69,f65,f61,f57,f53,f42])).
% 0.50/0.41 tff(f93,plain,(
% 0.50/0.41 ~spl1_4 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f24,f42,f53])).
% 0.50/0.41 tff(f94,plain,(
% 0.50/0.41 ~spl1_5 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f25,f42,f57])).
% 0.50/0.41 tff(f95,plain,(
% 0.50/0.41 ~spl1_6 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f26,f42,f61])).
% 0.50/0.41 tff(f96,plain,(
% 0.50/0.41 ~spl1_7 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f27,f42,f65])).
% 0.50/0.41 tff(f97,plain,(
% 0.50/0.41 ~spl1_8 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f28,f42,f69])).
% 0.50/0.41 tff(f98,plain,(
% 0.50/0.41 ~spl1_9 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f29,f42,f73])).
% 0.50/0.41 tff(f99,plain,(
% 0.50/0.41 ~spl1_10 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f30,f42,f77])).
% 0.50/0.41 tff(f100,plain,(
% 0.50/0.41 ~spl1_11 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f31,f42,f81])).
% 0.50/0.41 tff(f101,plain,(
% 0.50/0.41 ~spl1_12 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f32,f42,f85])).
% 0.50/0.41 tff(f102,plain,(
% 0.50/0.41 ~spl1_13 | spl1_2),
% 0.50/0.41 inference(avatar_split_clause,[],[f33,f42,f89])).
% 0.50/0.41 tff(f127,plain,(
% 0.50/0.41 $less(0,a) | a = 0 | spl1_1),
% 0.50/0.41 inference(resolution,[],[f11,f40])).
% 0.50/0.41 tff(f131,plain,(
% 0.50/0.41 $less(0,a) | (spl1_1 | spl1_4)),
% 0.50/0.41 inference(forward_subsumption_resolution,[],[f127,f54])).
% 0.50/0.41 tff(f134,plain,(
% 0.50/0.41 ~$less(a,$sum(0,1)) | (spl1_1 | spl1_4)),
% 0.50/0.41 inference(resolution,[],[f131,f15])).
% 0.50/0.41 tff(f135,plain,(
% 0.50/0.41 ~$less(a,1) | (spl1_1 | spl1_4)),
% 0.50/0.41 inference(evaluation,[],[f134])).
% 0.50/0.41 tff(f146,plain,(
% 0.50/0.41 $less(1,a) | a = 1 | (spl1_1 | spl1_4)),
% 0.50/0.41 inference(resolution,[],[f135,f11])).
% 0.50/0.41 tff(f149,plain,(
% 0.50/0.41 $less(1,a) | (spl1_1 | spl1_4 | spl1_5)),
% 0.50/0.41 inference(forward_subsumption_resolution,[],[f146,f58])).
% 0.50/0.41 tff(f164,plain,(
% 0.50/0.41 ~$less(a,$sum(1,1)) | (spl1_1 | spl1_4 | spl1_5)),
% 0.50/0.41 inference(resolution,[],[f149,f15])).
% 0.50/0.41 tff(f165,plain,(
% 0.50/0.41 ~$less(a,2) | (spl1_1 | spl1_4 | spl1_5)),
% 0.50/0.41 inference(evaluation,[],[f164])).
% 0.50/0.41 tff(f190,plain,(
% 0.50/0.41 $less(2,a) | a = 2 | (spl1_1 | spl1_4 | spl1_5)),
% 0.50/0.41 inference(resolution,[],[f165,f11])).
% 0.50/0.41 tff(f193,plain,(
% 0.50/0.41 $less(2,a) | (spl1_1 | spl1_4 | spl1_5 | spl1_6)),
% 0.50/0.41 inference(forward_subsumption_resolution,[],[f190,f62])).
% 0.50/0.41 tff(f202,plain,(
% 0.50/0.41 ~$less(a,$sum(2,1)) | (spl1_1 | spl1_4 | spl1_5 | spl1_6)),
% 0.50/0.41 inference(resolution,[],[f193,f15])).
% 0.50/0.41 tff(f203,plain,(
% 0.50/0.41 ~$less(a,3) | (spl1_1 | spl1_4 | spl1_5 | spl1_6)),
% 0.50/0.41 inference(evaluation,[],[f202])).
% 0.50/0.41 tff(f223,plain,(
% 0.50/0.41 $less(3,a) | a = 3 | (spl1_1 | spl1_4 | spl1_5 | spl1_6)),
% 0.50/0.41 inference(resolution,[],[f203,f11])).
% 0.50/0.41 tff(f226,plain,(
% 0.50/0.41 $less(3,a) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7)),
% 0.50/0.41 inference(forward_subsumption_resolution,[],[f223,f66])).
% 0.50/0.41 tff(f263,plain,(
% 0.50/0.41 ~$less(a,$sum(3,1)) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7)),
% 0.50/0.41 inference(resolution,[],[f226,f15])).
% 0.50/0.41 tff(f264,plain,(
% 0.50/0.41 ~$less(a,4) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7)),
% 0.50/0.41 inference(evaluation,[],[f263])).
% 0.50/0.41 tff(f297,plain,(
% 0.50/0.41 $less(4,a) | a = 4 | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7)),
% 0.50/0.41 inference(resolution,[],[f264,f11])).
% 0.50/0.41 tff(f300,plain,(
% 0.50/0.41 $less(4,a) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8)),
% 0.50/0.41 inference(forward_subsumption_resolution,[],[f297,f70])).
% 0.50/0.41 tff(f319,plain,(
% 0.50/0.41 ~$less(a,$sum(4,1)) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8)),
% 0.50/0.41 inference(resolution,[],[f300,f15])).
% 0.50/0.41 tff(f320,plain,(
% 0.50/0.41 ~$less(a,5) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8)),
% 0.50/0.41 inference(evaluation,[],[f319])).
% 0.50/0.41 tff(f350,plain,(
% 0.50/0.41 $less(5,a) | a = 5 | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8)),
% 0.50/0.41 inference(resolution,[],[f320,f11])).
% 0.50/0.41 tff(f353,plain,(
% 0.50/0.41 $less(5,a) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9)),
% 0.50/0.41 inference(forward_subsumption_resolution,[],[f350,f74])).
% 0.50/0.41 tff(f374,plain,(
% 0.50/0.41 ~$less(a,$sum(5,1)) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9)),
% 0.50/0.41 inference(resolution,[],[f353,f15])).
% 0.50/0.41 tff(f375,plain,(
% 0.50/0.41 ~$less(a,6) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9)),
% 0.50/0.41 inference(evaluation,[],[f374])).
% 0.50/0.41 tff(f392,plain,(
% 0.50/0.41 $less(6,a) | a = 6 | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9)),
% 0.50/0.41 inference(resolution,[],[f375,f11])).
% 0.50/0.41 tff(f395,plain,(
% 0.50/0.41 $less(6,a) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10)),
% 0.50/0.41 inference(forward_subsumption_resolution,[],[f392,f78])).
% 0.50/0.41 tff(f411,definition,(
% 0.50/0.41 spl1_14 <=> 10 = $sum(1,a)),
% 0.50/0.41 introduced(definition,[new_symbols(definition,[spl1_14])],[avatar_definition])).
% 0.50/0.41 tff(f412,plain,(
% 0.50/0.41 10 != $sum(1,a) | spl1_14),
% 0.50/0.41 inference(avatar_component_clause,[],[f411])).
% 0.50/0.41 tff(f413,plain,(
% 0.50/0.41 10 = $sum(1,a) | ~spl1_14),
% 0.50/0.41 inference(avatar_component_clause,[],[f411])).
% 0.50/0.41 tff(f422,plain,(
% 0.50/0.41 ~$less(a,$sum(6,1)) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10)),
% 0.50/0.41 inference(resolution,[],[f395,f15])).
% 0.50/0.41 tff(f423,plain,(
% 0.50/0.41 ~$less(a,7) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10)),
% 0.50/0.41 inference(evaluation,[],[f422])).
% 0.50/0.41 tff(f505,plain,(
% 0.50/0.41 $less(7,a) | a = 7 | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10)),
% 0.50/0.41 inference(resolution,[],[f423,f11])).
% 0.50/0.41 tff(f508,plain,(
% 0.50/0.41 $less(7,a) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11)),
% 0.50/0.41 inference(forward_subsumption_resolution,[],[f505,f82])).
% 0.50/0.41 tff(f592,plain,(
% 0.50/0.41 ~$less(a,$sum(7,1)) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11)),
% 0.50/0.41 inference(resolution,[],[f508,f15])).
% 0.50/0.41 tff(f593,plain,(
% 0.50/0.41 ~$less(a,8) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11)),
% 0.50/0.41 inference(evaluation,[],[f592])).
% 0.50/0.41 tff(f709,plain,(
% 0.50/0.41 $less(8,a) | a = 8 | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11)),
% 0.50/0.41 inference(resolution,[],[f593,f11])).
% 0.50/0.41 tff(f712,plain,(
% 0.50/0.41 $less(8,a) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12)),
% 0.50/0.41 inference(forward_subsumption_resolution,[],[f709,f86])).
% 0.50/0.41 tff(f740,plain,(
% 0.50/0.41 ~$less(a,$sum(8,1)) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12)),
% 0.50/0.41 inference(resolution,[],[f712,f15])).
% 0.50/0.41 tff(f741,plain,(
% 0.50/0.41 ~$less(a,9) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12)),
% 0.50/0.41 inference(evaluation,[],[f740])).
% 0.50/0.41 tff(f801,plain,(
% 0.50/0.41 $less(9,a) | a = 9 | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12)),
% 0.50/0.41 inference(resolution,[],[f741,f11])).
% 0.50/0.41 tff(f804,plain,(
% 0.50/0.41 $less(9,a) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12 | spl1_13)),
% 0.50/0.41 inference(forward_subsumption_resolution,[],[f801,f90])).
% 0.50/0.41 tff(f894,plain,(
% 0.50/0.41 ~$less(a,$sum(9,1)) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12 | spl1_13)),
% 0.50/0.41 inference(resolution,[],[f804,f15])).
% 0.50/0.41 tff(f895,plain,(
% 0.50/0.41 ~$less(a,10) | (spl1_1 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12 | spl1_13)),
% 0.50/0.41 inference(evaluation,[],[f894])).
% 0.50/0.41 tff(f896,plain,(
% 0.50/0.41 $false | (spl1_1 | ~spl1_3 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12 | spl1_13)),
% 0.50/0.41 inference(forward_subsumption_resolution,[],[f895,f49])).
% 0.50/0.41 tff(f897,plain,(
% 0.50/0.41 spl1_1 | ~spl1_3 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12 | spl1_13),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f896])).
% 0.50/0.41 tff(f902,plain,(
% 0.50/0.41 ~$less(0,$sum(a,1)) | ~spl1_1),
% 0.50/0.41 inference(resolution,[],[f39,f15])).
% 0.50/0.41 tff(f904,plain,(
% 0.50/0.41 ~$less(0,$sum(1,a)) | ~spl1_1),
% 0.50/0.41 inference(forward_demodulation,[],[f902,f4])).
% 0.50/0.41 tff(f909,plain,(
% 0.50/0.41 ~$less(0,10) | (~spl1_1 | ~spl1_14)),
% 0.50/0.41 inference(forward_demodulation,[],[f904,f413])).
% 0.50/0.41 tff(f910,plain,(
% 0.50/0.41 $false | (~spl1_1 | ~spl1_14)),
% 0.50/0.41 inference(evaluation,[],[f909])).
% 0.50/0.41 tff(f911,plain,(
% 0.50/0.41 ~spl1_1 | ~spl1_14),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f910])).
% 0.50/0.41 tff(f915,plain,(
% 0.50/0.41 ~$less(0,$sum(1,3)) | (~spl1_1 | ~spl1_7)),
% 0.50/0.41 inference(forward_demodulation,[],[f904,f67])).
% 0.50/0.41 tff(f916,plain,(
% 0.50/0.41 $false | (~spl1_1 | ~spl1_7)),
% 0.50/0.41 inference(evaluation,[],[f915])).
% 0.50/0.41 tff(f917,plain,(
% 0.50/0.41 ~spl1_1 | ~spl1_7),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f916])).
% 0.50/0.41 tff(f925,plain,(
% 0.50/0.41 ~$less(3,10) | (spl1_3 | ~spl1_7)),
% 0.50/0.41 inference(forward_demodulation,[],[f48,f67])).
% 0.50/0.41 tff(f926,plain,(
% 0.50/0.41 $false | (spl1_3 | ~spl1_7)),
% 0.50/0.41 inference(evaluation,[],[f925])).
% 0.50/0.41 tff(f927,plain,(
% 0.50/0.41 spl1_3 | ~spl1_7),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f926])).
% 0.50/0.41 tff(f936,plain,(
% 0.50/0.41 ~$less(2,10) | (spl1_3 | ~spl1_6)),
% 0.50/0.41 inference(forward_demodulation,[],[f48,f63])).
% 0.50/0.41 tff(f937,plain,(
% 0.50/0.41 $false | (spl1_3 | ~spl1_6)),
% 0.50/0.41 inference(evaluation,[],[f936])).
% 0.50/0.41 tff(f938,plain,(
% 0.50/0.41 spl1_3 | ~spl1_6),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f937])).
% 0.50/0.41 tff(f947,plain,(
% 0.50/0.41 ~$less(4,10) | (spl1_3 | ~spl1_8)),
% 0.50/0.41 inference(forward_demodulation,[],[f48,f71])).
% 0.50/0.41 tff(f948,plain,(
% 0.50/0.41 $false | (spl1_3 | ~spl1_8)),
% 0.50/0.41 inference(evaluation,[],[f947])).
% 0.50/0.41 tff(f949,plain,(
% 0.50/0.41 spl1_3 | ~spl1_8),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f948])).
% 0.50/0.41 tff(f951,plain,(
% 0.50/0.41 10 != $sum(1,9) | (~spl1_13 | spl1_14)),
% 0.50/0.41 inference(forward_demodulation,[],[f412,f91])).
% 0.50/0.41 tff(f952,plain,(
% 0.50/0.41 $false | (~spl1_13 | spl1_14)),
% 0.50/0.41 inference(evaluation,[],[f951])).
% 0.50/0.41 tff(f953,plain,(
% 0.50/0.41 ~spl1_13 | spl1_14),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f952])).
% 0.50/0.41 tff(f962,plain,(
% 0.50/0.41 ~$less(9,10) | (spl1_3 | ~spl1_13)),
% 0.50/0.41 inference(forward_demodulation,[],[f48,f91])).
% 0.50/0.41 tff(f963,plain,(
% 0.50/0.41 $false | (spl1_3 | ~spl1_13)),
% 0.50/0.41 inference(evaluation,[],[f962])).
% 0.50/0.41 tff(f964,plain,(
% 0.50/0.41 spl1_3 | ~spl1_13),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f963])).
% 0.50/0.41 tff(f970,plain,(
% 0.50/0.41 ~$less(0,10) | (spl1_3 | ~spl1_4)),
% 0.50/0.41 inference(forward_demodulation,[],[f48,f55])).
% 0.50/0.41 tff(f971,plain,(
% 0.50/0.41 $false | (spl1_3 | ~spl1_4)),
% 0.50/0.41 inference(evaluation,[],[f970])).
% 0.50/0.41 tff(f972,plain,(
% 0.50/0.41 spl1_3 | ~spl1_4),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f971])).
% 0.50/0.41 tff(f978,plain,(
% 0.50/0.41 ~$less(8,10) | (spl1_3 | ~spl1_12)),
% 0.50/0.41 inference(forward_demodulation,[],[f48,f87])).
% 0.50/0.41 tff(f979,plain,(
% 0.50/0.41 $false | (spl1_3 | ~spl1_12)),
% 0.50/0.41 inference(evaluation,[],[f978])).
% 0.50/0.41 tff(f980,plain,(
% 0.50/0.41 spl1_3 | ~spl1_12),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f979])).
% 0.50/0.41 tff(f987,plain,(
% 0.50/0.41 ~$less(7,10) | (spl1_3 | ~spl1_11)),
% 0.50/0.41 inference(forward_demodulation,[],[f48,f83])).
% 0.50/0.41 tff(f988,plain,(
% 0.50/0.41 $false | (spl1_3 | ~spl1_11)),
% 0.50/0.41 inference(evaluation,[],[f987])).
% 0.50/0.41 tff(f989,plain,(
% 0.50/0.41 spl1_3 | ~spl1_11),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f988])).
% 0.50/0.41 tff(f997,plain,(
% 0.50/0.41 ~$less(5,10) | (spl1_3 | ~spl1_9)),
% 0.50/0.41 inference(forward_demodulation,[],[f48,f75])).
% 0.50/0.41 tff(f998,plain,(
% 0.50/0.41 $false | (spl1_3 | ~spl1_9)),
% 0.50/0.41 inference(evaluation,[],[f997])).
% 0.50/0.41 tff(f999,plain,(
% 0.50/0.41 spl1_3 | ~spl1_9),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f998])).
% 0.50/0.41 tff(f1008,plain,(
% 0.50/0.41 ~$less(1,10) | (spl1_3 | ~spl1_5)),
% 0.50/0.41 inference(forward_demodulation,[],[f48,f59])).
% 0.50/0.41 tff(f1009,plain,(
% 0.50/0.41 $false | (spl1_3 | ~spl1_5)),
% 0.50/0.41 inference(evaluation,[],[f1008])).
% 0.50/0.41 tff(f1010,plain,(
% 0.50/0.41 spl1_3 | ~spl1_5),
% 0.50/0.41 inference(avatar_contradiction_clause,[],[f1009])).
% 0.50/0.41 tff(f1019,plain,(
% 0.50/0.41 ~$less(6,10) | (spl1_3 | ~spl1_10)),
% 0.50/0.41 inference(forward_demodulation,[],[f48,f79])).
% 0.50/0.42 tff(f1020,plain,(
% 0.50/0.42 $false | (spl1_3 | ~spl1_10)),
% 0.50/0.42 inference(evaluation,[],[f1019])).
% 0.50/0.42 tff(f1021,plain,(
% 0.50/0.42 spl1_3 | ~spl1_10),
% 0.50/0.42 inference(avatar_contradiction_clause,[],[f1020])).
% 0.50/0.42 tff(f1031,plain,(
% 0.50/0.42 ( ! [X0 : $int] : ($less($sum(a,X0),$sum(0,X0))) ) | ~spl1_1),
% 0.50/0.42 inference(resolution,[],[f39,f12])).
% 0.50/0.42 tff(f1033,plain,(
% 0.50/0.42 ~$less(0,$sum(a,1)) | ~spl1_1),
% 0.50/0.42 inference(resolution,[],[f39,f15])).
% 0.50/0.42 tff(f1034,plain,(
% 0.50/0.42 ( ! [X0 : $int] : ($less($sum(a,X0),X0)) ) | ~spl1_1),
% 0.50/0.42 inference(evaluation,[],[f1031])).
% 0.50/0.42 tff(f1035,plain,(
% 0.50/0.42 ~$less(0,$sum(1,a)) | ~spl1_1),
% 0.50/0.42 inference(forward_demodulation,[],[f1033,f4])).
% 0.50/0.42 tff(f1037,plain,(
% 0.50/0.42 ( ! [X0 : $int] : ($less($sum(0,X0),X0)) ) | (~spl1_1 | ~spl1_4)),
% 0.50/0.42 inference(forward_demodulation,[],[f1034,f55])).
% 0.50/0.42 tff(f1038,plain,(
% 0.50/0.42 ( ! [X0 : $int] : ($less(X0,X0)) ) | (~spl1_1 | ~spl1_4)),
% 0.50/0.42 inference(evaluation,[],[f1037])).
% 0.50/0.42 tff(f1044,plain,(
% 0.50/0.42 $false | (~spl1_1 | ~spl1_4)),
% 0.50/0.42 inference(forward_subsumption_resolution,[],[f1038,f9])).
% 0.50/0.42 tff(f1045,plain,(
% 0.50/0.42 ~spl1_1 | ~spl1_4),
% 0.50/0.42 inference(avatar_contradiction_clause,[],[f1044])).
% 0.50/0.42 tff(f1057,plain,(
% 0.50/0.42 ~$less(0,$sum(1,5)) | (~spl1_1 | ~spl1_9)),
% 0.50/0.42 inference(forward_demodulation,[],[f1035,f75])).
% 0.50/0.42 tff(f1058,plain,(
% 0.50/0.42 $false | (~spl1_1 | ~spl1_9)),
% 0.50/0.42 inference(evaluation,[],[f1057])).
% 0.50/0.42 tff(f1059,plain,(
% 0.50/0.42 ~spl1_1 | ~spl1_9),
% 0.50/0.42 inference(avatar_contradiction_clause,[],[f1058])).
% 0.50/0.42 tff(f1070,plain,(
% 0.50/0.42 ~$less(0,$sum(1,7)) | (~spl1_1 | ~spl1_11)),
% 0.50/0.42 inference(forward_demodulation,[],[f1035,f83])).
% 0.50/0.42 tff(f1071,plain,(
% 0.50/0.42 $false | (~spl1_1 | ~spl1_11)),
% 0.50/0.42 inference(evaluation,[],[f1070])).
% 0.50/0.42 tff(f1072,plain,(
% 0.50/0.42 ~spl1_1 | ~spl1_11),
% 0.50/0.42 inference(avatar_contradiction_clause,[],[f1071])).
% 0.50/0.42 tff(f1084,plain,(
% 0.50/0.42 ~$less(0,$sum(1,2)) | (~spl1_1 | ~spl1_6)),
% 0.50/0.42 inference(forward_demodulation,[],[f1035,f63])).
% 0.50/0.42 tff(f1085,plain,(
% 0.50/0.42 $false | (~spl1_1 | ~spl1_6)),
% 0.50/0.42 inference(evaluation,[],[f1084])).
% 0.50/0.42 tff(f1086,plain,(
% 0.50/0.42 ~spl1_1 | ~spl1_6),
% 0.50/0.42 inference(avatar_contradiction_clause,[],[f1085])).
% 0.50/0.42 tff(f1099,plain,(
% 0.50/0.42 ~$less(0,$sum(1,1)) | (~spl1_1 | ~spl1_5)),
% 0.50/0.42 inference(forward_demodulation,[],[f1035,f59])).
% 0.50/0.42 tff(f1100,plain,(
% 0.50/0.42 $false | (~spl1_1 | ~spl1_5)),
% 0.50/0.42 inference(evaluation,[],[f1099])).
% 0.50/0.42 tff(f1101,plain,(
% 0.50/0.42 ~spl1_1 | ~spl1_5),
% 0.50/0.42 inference(avatar_contradiction_clause,[],[f1100])).
% 0.50/0.42 tff(f1113,plain,(
% 0.50/0.42 ~$less(0,$sum(1,8)) | (~spl1_1 | ~spl1_12)),
% 0.50/0.42 inference(forward_demodulation,[],[f1035,f87])).
% 0.50/0.42 tff(f1114,plain,(
% 0.50/0.42 $false | (~spl1_1 | ~spl1_12)),
% 0.50/0.42 inference(evaluation,[],[f1113])).
% 0.50/0.42 tff(f1115,plain,(
% 0.50/0.42 ~spl1_1 | ~spl1_12),
% 0.50/0.42 inference(avatar_contradiction_clause,[],[f1114])).
% 0.50/0.42 tff(f1128,plain,(
% 0.50/0.42 ~$less(0,$sum(1,4)) | (~spl1_1 | ~spl1_8)),
% 0.50/0.42 inference(forward_demodulation,[],[f1035,f71])).
% 0.50/0.42 tff(f1129,plain,(
% 0.50/0.42 $false | (~spl1_1 | ~spl1_8)),
% 0.50/0.42 inference(evaluation,[],[f1128])).
% 0.50/0.42 tff(f1130,plain,(
% 0.50/0.42 ~spl1_1 | ~spl1_8),
% 0.50/0.42 inference(avatar_contradiction_clause,[],[f1129])).
% 0.50/0.42 tff(f1143,plain,(
% 0.50/0.42 ~$less(0,$sum(1,6)) | (~spl1_1 | ~spl1_10)),
% 0.50/0.42 inference(forward_demodulation,[],[f1035,f79])).
% 0.50/0.42 tff(f1144,plain,(
% 0.50/0.42 $false | (~spl1_1 | ~spl1_10)),
% 0.50/0.42 inference(evaluation,[],[f1143])).
% 0.50/0.42 tff(f1145,plain,(
% 0.50/0.42 ~spl1_1 | ~spl1_10),
% 0.50/0.42 inference(avatar_contradiction_clause,[],[f1144])).
% 0.50/0.42 cnf(s1, plain, ~spl1_1 | spl1_2, inference(sat_conversion,[],[f45])).
% 0.50/0.42 cnf(s2, plain, spl1_2 | spl1_3, inference(sat_conversion,[],[f50])).
% 0.50/0.42 cnf(s3, plain, spl1_1 | ~spl1_2 | ~spl1_3, inference(sat_conversion,[],[f51])).
% 0.50/0.42 cnf(s4, plain, ~spl1_2 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12 | spl1_13, inference(sat_conversion,[],[f92])).
% 0.50/0.42 cnf(s5, plain, spl1_2 | ~spl1_4, inference(sat_conversion,[],[f93])).
% 0.50/0.42 cnf(s6, plain, spl1_2 | ~spl1_5, inference(sat_conversion,[],[f94])).
% 0.50/0.42 cnf(s7, plain, spl1_2 | ~spl1_6, inference(sat_conversion,[],[f95])).
% 0.50/0.42 cnf(s8, plain, spl1_2 | ~spl1_7, inference(sat_conversion,[],[f96])).
% 0.50/0.42 cnf(s9, plain, spl1_2 | ~spl1_8, inference(sat_conversion,[],[f97])).
% 0.50/0.42 cnf(s10, plain, spl1_2 | ~spl1_9, inference(sat_conversion,[],[f98])).
% 0.50/0.42 cnf(s11, plain, spl1_2 | ~spl1_10, inference(sat_conversion,[],[f99])).
% 0.50/0.42 cnf(s12, plain, spl1_2 | ~spl1_11, inference(sat_conversion,[],[f100])).
% 0.50/0.42 cnf(s13, plain, spl1_2 | ~spl1_12, inference(sat_conversion,[],[f101])).
% 0.50/0.42 cnf(s14, plain, spl1_2 | ~spl1_13, inference(sat_conversion,[],[f102])).
% 0.50/0.42 cnf(s16, plain, spl1_1 | ~spl1_3 | spl1_4 | spl1_5 | spl1_6 | spl1_7 | spl1_8 | spl1_9 | spl1_10 | spl1_11 | spl1_12 | spl1_13, inference(sat_conversion,[],[f897])).
% 0.50/0.42 cnf(s17, plain, ~spl1_1 | ~spl1_14, inference(sat_conversion,[],[f911])).
% 0.50/0.42 cnf(s18, plain, ~spl1_1 | ~spl1_7, inference(sat_conversion,[],[f917])).
% 0.50/0.42 cnf(s19, plain, spl1_3 | ~spl1_7, inference(sat_conversion,[],[f927])).
% 0.50/0.42 cnf(s20, plain, spl1_3 | ~spl1_6, inference(sat_conversion,[],[f938])).
% 0.50/0.42 cnf(s21, plain, spl1_3 | ~spl1_8, inference(sat_conversion,[],[f949])).
% 0.50/0.42 cnf(s22, plain, ~spl1_13 | spl1_14, inference(sat_conversion,[],[f953])).
% 0.50/0.42 cnf(s24, plain, spl1_3 | ~spl1_13, inference(sat_conversion,[],[f964])).
% 0.50/0.42 cnf(s25, plain, spl1_3 | ~spl1_4, inference(sat_conversion,[],[f972])).
% 0.50/0.42 cnf(s26, plain, spl1_3 | ~spl1_12, inference(sat_conversion,[],[f980])).
% 0.50/0.42 cnf(s27, plain, spl1_3 | ~spl1_11, inference(sat_conversion,[],[f989])).
% 0.50/0.42 cnf(s28, plain, spl1_3 | ~spl1_9, inference(sat_conversion,[],[f999])).
% 0.50/0.42 cnf(s29, plain, spl1_3 | ~spl1_5, inference(sat_conversion,[],[f1010])).
% 0.50/0.42 cnf(s30, plain, spl1_3 | ~spl1_10, inference(sat_conversion,[],[f1021])).
% 0.50/0.42 cnf(s32, plain, ~spl1_1 | ~spl1_4, inference(sat_conversion,[],[f1045])).
% 0.50/0.42 cnf(s33, plain, ~spl1_1 | ~spl1_9, inference(sat_conversion,[],[f1059])).
% 0.50/0.42 cnf(s34, plain, ~spl1_1 | ~spl1_11, inference(sat_conversion,[],[f1072])).
% 0.50/0.42 cnf(s35, plain, ~spl1_1 | ~spl1_6, inference(sat_conversion,[],[f1086])).
% 0.50/0.42 cnf(s36, plain, ~spl1_1 | ~spl1_5, inference(sat_conversion,[],[f1101])).
% 0.50/0.42 cnf(s37, plain, ~spl1_1 | ~spl1_12, inference(sat_conversion,[],[f1115])).
% 0.50/0.42 cnf(s38, plain, ~spl1_1 | ~spl1_8, inference(sat_conversion,[],[f1130])).
% 0.50/0.42 cnf(s39, plain, ~spl1_1 | ~spl1_10, inference(sat_conversion,[],[f1145])).
% 0.50/0.42 cnf(s40, plain, spl1_2 | spl1_1, inference(rat,[],[s16,s2,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14])).
% 0.50/0.42 cnf(s41, plain, ~spl1_2 | spl1_1, inference(rat,[],[s4,s19,s20,s21,s24,s25,s26,s27,s28,s29,s30,s3])).
% 0.50/0.42 cnf(s42, plain, spl1_1, inference(rat,[],[s41,s40])).
% 0.50/0.42 cnf(s43, plain, ~spl1_10, inference(rat,[],[s39,s42])).
% 0.50/0.42 cnf(s44, plain, ~spl1_8, inference(rat,[],[s38,s42])).
% 0.50/0.42 cnf(s45, plain, ~spl1_12, inference(rat,[],[s37,s42])).
% 0.50/0.42 cnf(s46, plain, ~spl1_5, inference(rat,[],[s36,s42])).
% 0.50/0.42 cnf(s47, plain, ~spl1_6, inference(rat,[],[s35,s42])).
% 0.50/0.42 cnf(s48, plain, ~spl1_11, inference(rat,[],[s34,s42])).
% 0.50/0.42 cnf(s49, plain, ~spl1_9, inference(rat,[],[s33,s42])).
% 0.50/0.42 cnf(s50, plain, ~spl1_4, inference(rat,[],[s32,s42])).
% 0.50/0.42 cnf(s51, plain, ~spl1_7, inference(rat,[],[s18,s42])).
% 0.50/0.42 cnf(s52, plain, ~spl1_14, inference(rat,[],[s17,s42])).
% 0.50/0.42 cnf(s53, plain, spl1_2, inference(rat,[],[s1,s42])).
% 0.50/0.42 cnf(s54, plain, spl1_13, inference(rat,[],[s4,s50,s45,s48,s43,s49,s44,s53,s47,s46,s51])).
% 0.50/0.42 cnf(s55, plain, $false, inference(rat,[],[s22,s52,s54])).
% 0.50/0.42 tff(f1147,plain,(
% 0.50/0.42 $false),
% 0.50/0.42 inference(avatar_sat_refutation,[],[s55])).
% 0.50/0.42 % SZS output end Proof for theBenchmark
% 0.50/0.42 % (3775487)------------------------------
% 0.50/0.42 % (3775487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.42 % (3775487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.42 % (3775487)CaDiCaL version: 2.1.3
% 0.50/0.42 % (3775487)Termination reason: Refutation
% 0.50/0.42 % (3775487)Time elapsed: 0.046 s
% 0.50/0.42 % (3775487)Peak memory usage: 13 MB
% 0.50/0.42 % (3775487)Instructions burned: 42 (million)
% 0.50/0.42 % (3775477)Success in time 0.085 s
% 0.50/0.42 % Vampire exiting
%------------------------------------------------------------------------------