%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW678_1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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 01:40:38 PM UTC 2026
% Result : Theorem 0.21s 0.30s
% Output : Refutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW678_1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n015.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 14:28:17 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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.21/0.30 % (2667804)Will run a generic schedule for satisfiability detection.
% 0.21/0.30 % (2667811)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3242702622:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.30 % (2667810)% WARNING: option uhcvi not known.
% 0.21/0.30 % (2667809)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=503280564_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.30 % (2667810)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3096993092:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.30 % (2667812)dis+10_1_sil=32000:sp=arity:random_seed=2561535782:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.30 % (2667813)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=320754481:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.30 % (2667809)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.21/0.30 % (2667809)Terminated due to inappropriate strategy.
% 0.21/0.30 % (2667809)------------------------------
% 0.21/0.30 % (2667809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (2667809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (2667809)CaDiCaL version: 2.1.3
% 0.21/0.30 % (2667809)Termination reason: Inappropriate
% 0.21/0.30 % (2667809)Time elapsed: 0.001 s
% 0.21/0.30 % (2667809)Peak memory usage: 10 MB
% 0.21/0.30 % (2667809)Instructions burned: 2 (million)
% 0.21/0.30 % (2667809)------------------------------
% 0.21/0.30 % (2667809)------------------------------
% 0.21/0.30 % (2667813) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2667804-2667813"...
% 0.21/0.30 % (2667810) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2667804-2667810"...
% 0.21/0.30 % (2667813)...printing done.
% 0.21/0.30 % (2667810)...printing done.
% 0.21/0.30 % (2667815)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1398716686:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.30 % (2667813)Refutation found. Thanks to Tanya!
% 0.21/0.30 % SZS status Theorem for theBenchmark
% 0.21/0.30 % SZS output start Proof for theBenchmark
% 0.21/0.30 tff(type_def_5, type, 'Tree': $tType).
% 0.21/0.30 tff(func_def_0, type, 'empty:Tree': 'Tree').
% 0.21/0.30 tff(func_def_1, type, 'left:(Tree)>Tree': 'Tree' > 'Tree').
% 0.21/0.30 tff(func_def_2, type, 'val:(Tree)>Int': 'Tree' > $int).
% 0.21/0.30 tff(func_def_3, type, 'node:(Int*Tree*Tree)>Tree': ($int * 'Tree' * 'Tree') > 'Tree').
% 0.21/0.30 tff(func_def_4, type, 'right:(Tree)>Tree': 'Tree' > 'Tree').
% 0.21/0.30 tff(func_def_9, type, sK0: 'Tree' > $int).
% 0.21/0.30 tff(func_def_10, type, sK1: 'Tree' > $int).
% 0.21/0.30 tff(func_def_11, type, sK2: 'Tree').
% 0.21/0.30 tff(func_def_12, type, sK3: $int).
% 0.21/0.30 tff(func_def_13, type, sK4: 'Tree').
% 0.21/0.30 tff(func_def_14, type, sK5: 'Tree').
% 0.21/0.30 tff(pred_def_1, type, searchtree: 'Tree' > $o).
% 0.21/0.30 tff(pred_def_2, type, in: ($int * 'Tree') > $o).
% 0.21/0.30 tff(f6,axiom,(
% 0.21/0.30 ! [X0 : $int,X1 : 'Tree'] : (in(X0,X1) <=> ((X1 = 'empty:Tree' => $false) & (X1 != 'empty:Tree' => (X0 = 'val:(Tree)>Int'(X1) | in(X0,'left:(Tree)>Tree'(X1)) | in(X0,'right:(Tree)>Tree'(X1))))))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_005)).
% 0.21/0.30 tff(f7,axiom,(
% 0.21/0.30 ! [X0 : 'Tree'] : (searchtree(X0) <=> ((X0 = 'empty:Tree' => $true) & (X0 != 'empty:Tree' => (searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (in(X1,'left:(Tree)>Tree'(X0)) => $lesseq(X1,'val:(Tree)>Int'(X0))) & ! [X1 : $int] : (in(X1,'right:(Tree)>Tree'(X0)) => $greater(X1,'val:(Tree)>Int'(X0)))))))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_006)).
% 0.21/0.30 tff(f8,conjecture,(
% 0.21/0.30 ! [X0 : 'Tree',X1 : $int] : (searchtree(X0) => (((X0 = 'empty:Tree' => $false) & (X0 != 'empty:Tree' => ((X1 = 'val:(Tree)>Int'(X0) => $true) & (X1 != 'val:(Tree)>Int'(X0) => (($less(X1,'val:(Tree)>Int'(X0)) => ? [X2 : 'Tree'] : (X2 = 'left:(Tree)>Tree'(X0) & in(X1,X2))) & (~$less(X1,'val:(Tree)>Int'(X0)) => ? [X3 : 'Tree'] : (X3 = 'right:(Tree)>Tree'(X0) & in(X1,X3)))))))) <=> in(X1,X0)))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_007)).
% 0.21/0.30 tff(f9,negated_conjecture,(
% 0.21/0.30 ~ ! [X0 : 'Tree',X1 : $int] : (searchtree(X0) => (((X0 = 'empty:Tree' => $false) & (X0 != 'empty:Tree' => ((X1 = 'val:(Tree)>Int'(X0) => $true) & (X1 != 'val:(Tree)>Int'(X0) => (($less(X1,'val:(Tree)>Int'(X0)) => ? [X2 : 'Tree'] : (X2 = 'left:(Tree)>Tree'(X0) & in(X1,X2))) & (~$less(X1,'val:(Tree)>Int'(X0)) => ? [X3 : 'Tree'] : (X3 = 'right:(Tree)>Tree'(X0) & in(X1,X3)))))))) <=> in(X1,X0)))),
% 0.21/0.30 inference(negated_conjecture,[status(cth)],[f8])).
% 0.21/0.30 tff(f10,plain,(
% 0.21/0.30 ! [X0 : 'Tree'] : (searchtree(X0) <=> ((X0 = 'empty:Tree' => $true) & (X0 != 'empty:Tree' => (searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (in(X1,'left:(Tree)>Tree'(X0)) => ~$less('val:(Tree)>Int'(X0),X1)) & ! [X1 : $int] : (in(X1,'right:(Tree)>Tree'(X0)) => $less('val:(Tree)>Int'(X0),X1))))))),
% 0.21/0.30 inference(theory_normalization,[],[f7])).
% 0.21/0.30 tff(f16,definition,(
% 0.21/0.30 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 0.21/0.30 introduced(theory,[tha_non-reflexivity])).
% 0.21/0.30 tff(f17,definition,(
% 0.21/0.30 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,X2) | $less(X0,X2)) )),
% 0.21/0.30 introduced(theory,[tha_transitivity])).
% 0.21/0.30 tff(f18,definition,(
% 0.21/0.30 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | $less(X1,X0) | X0 = X1) )),
% 0.21/0.30 introduced(theory,[tha_order_totality])).
% 0.21/0.30 tff(f23,plain,(
% 0.21/0.30 ! [X0 : 'Tree'] : (searchtree(X0) <=> ((X0 = 'empty:Tree' => $true) & (X0 != 'empty:Tree' => (searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (in(X1,'left:(Tree)>Tree'(X0)) => ~$less('val:(Tree)>Int'(X0),X1)) & ! [X2 : $int] : (in(X2,'right:(Tree)>Tree'(X0)) => $less('val:(Tree)>Int'(X0),X2))))))),
% 0.21/0.30 inference(rectify,[],[f10])).
% 0.21/0.30 tff(f24,plain,(
% 0.21/0.30 ! [X0 : $int,X1 : 'Tree'] : (in(X0,X1) <=> (($false | 'empty:Tree' != X1) & ((X0 = 'val:(Tree)>Int'(X1) | in(X0,'left:(Tree)>Tree'(X1)) | in(X0,'right:(Tree)>Tree'(X1))) | 'empty:Tree' = X1)))),
% 0.21/0.30 inference(ennf_transformation,[],[f6])).
% 0.21/0.30 tff(f25,plain,(
% 0.21/0.30 ! [X0 : $int,X1 : 'Tree'] : (in(X0,X1) <=> (($false | 'empty:Tree' != X1) & (X0 = 'val:(Tree)>Int'(X1) | in(X0,'left:(Tree)>Tree'(X1)) | in(X0,'right:(Tree)>Tree'(X1)) | 'empty:Tree' = X1)))),
% 0.21/0.30 inference(flattening,[],[f24])).
% 0.21/0.30 tff(f26,plain,(
% 0.21/0.30 ! [X0 : 'Tree'] : (searchtree(X0) <=> (($true | 'empty:Tree' != X0) & ((searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (~$less('val:(Tree)>Int'(X0),X1) | ~in(X1,'left:(Tree)>Tree'(X0))) & ! [X2 : $int] : ($less('val:(Tree)>Int'(X0),X2) | ~in(X2,'right:(Tree)>Tree'(X0)))) | 'empty:Tree' = X0)))),
% 0.21/0.30 inference(ennf_transformation,[],[f23])).
% 0.21/0.30 tff(f27,plain,(
% 0.21/0.30 ? [X0 : 'Tree',X1 : $int] : (((($false | 'empty:Tree' != X0) & ((($true | 'val:(Tree)>Int'(X0) != X1) & (((? [X2 : 'Tree'] : (X2 = 'left:(Tree)>Tree'(X0) & in(X1,X2)) | ~$less(X1,'val:(Tree)>Int'(X0))) & (? [X3 : 'Tree'] : (X3 = 'right:(Tree)>Tree'(X0) & in(X1,X3)) | $less(X1,'val:(Tree)>Int'(X0)))) | 'val:(Tree)>Int'(X0) = X1)) | 'empty:Tree' = X0)) <~> in(X1,X0)) & searchtree(X0))),
% 0.21/0.30 inference(ennf_transformation,[],[f9])).
% 0.21/0.30 tff(f33,plain,(
% 0.21/0.30 ( ! [X0 : $int,X1 : 'Tree'] : ('empty:Tree' != X1 | ~in(X0,X1)) )),
% 0.21/0.30 inference(cnf_transformation,[],[f25])).
% 0.21/0.30 tff(f34,plain,(
% 0.21/0.30 ( ! [X0 : $int,X1 : 'Tree'] : ('val:(Tree)>Int'(X1) != X0 | 'empty:Tree' = X1 | in(X0,X1)) )),
% 0.21/0.30 inference(cnf_transformation,[],[f25])).
% 0.21/0.30 tff(f35,plain,(
% 0.21/0.30 ( ! [X0 : $int,X1 : 'Tree'] : (~in(X0,'left:(Tree)>Tree'(X1)) | 'empty:Tree' = X1 | in(X0,X1)) )),
% 0.21/0.30 inference(cnf_transformation,[],[f25])).
% 0.21/0.30 tff(f36,plain,(
% 0.21/0.30 ( ! [X0 : $int,X1 : 'Tree'] : (~in(X0,'right:(Tree)>Tree'(X1)) | 'empty:Tree' = X1 | in(X0,X1)) )),
% 0.21/0.30 inference(cnf_transformation,[],[f25])).
% 0.21/0.30 tff(f37,plain,(
% 0.21/0.30 ( ! [X0 : $int,X1 : 'Tree'] : (in(X0,'right:(Tree)>Tree'(X1)) | 'empty:Tree' = X1 | in(X0,'left:(Tree)>Tree'(X1)) | 'val:(Tree)>Int'(X1) = X0 | ~in(X0,X1)) )),
% 0.21/0.30 inference(cnf_transformation,[],[f25])).
% 0.21/0.30 tff(f38,plain,(
% 0.21/0.30 ( ! [X0 : 'Tree',X1 : $int] : (~searchtree(X0) | ~in(X1,'left:(Tree)>Tree'(X0)) | ~$less('val:(Tree)>Int'(X0),X1) | 'empty:Tree' = X0) )),
% 0.21/0.30 inference(cnf_transformation,[],[f26])).
% 0.21/0.30 tff(f47,plain,(
% 0.21/0.30 ( ! [X2 : $int,X0 : 'Tree'] : (~searchtree(X0) | ~in(X2,'right:(Tree)>Tree'(X0)) | $less('val:(Tree)>Int'(X0),X2) | 'empty:Tree' = X0) )),
% 0.21/0.30 inference(cnf_transformation,[],[f26])).
% 0.21/0.30 tff(f52,plain,(
% 0.21/0.30 ( ! [X2 : 'Tree'] : (~in(sK3,sK2) | ~$less(sK3,'val:(Tree)>Int'(sK2)) | ~in(sK3,X2) | 'left:(Tree)>Tree'(sK2) != X2 | 'empty:Tree' = sK2) )),
% 0.21/0.30 inference(cnf_transformation,[],[f27])).
% 0.21/0.30 tff(f53,plain,(
% 0.21/0.30 in(sK3,sK2) | 'empty:Tree' = sK2 | sK3 = 'val:(Tree)>Int'(sK2) | ~$less(sK3,'val:(Tree)>Int'(sK2)) | in(sK3,sK5)),
% 0.21/0.30 inference(cnf_transformation,[],[f27])).
% 0.21/0.30 tff(f54,plain,(
% 0.21/0.30 in(sK3,sK2) | 'empty:Tree' = sK2 | sK3 = 'val:(Tree)>Int'(sK2) | ~$less(sK3,'val:(Tree)>Int'(sK2)) | sK5 = 'left:(Tree)>Tree'(sK2)),
% 0.21/0.30 inference(cnf_transformation,[],[f27])).
% 0.21/0.30 tff(f57,plain,(
% 0.21/0.30 in(sK3,sK2) | 'empty:Tree' = sK2 | sK3 = 'val:(Tree)>Int'(sK2) | $less(sK3,'val:(Tree)>Int'(sK2)) | in(sK3,sK4)),
% 0.21/0.30 inference(cnf_transformation,[],[f27])).
% 0.21/0.30 tff(f58,plain,(
% 0.21/0.30 in(sK3,sK2) | 'empty:Tree' = sK2 | sK3 = 'val:(Tree)>Int'(sK2) | $less(sK3,'val:(Tree)>Int'(sK2)) | sK4 = 'right:(Tree)>Tree'(sK2)),
% 0.21/0.30 inference(cnf_transformation,[],[f27])).
% 0.21/0.30 tff(f60,plain,(
% 0.21/0.30 ( ! [X3 : 'Tree'] : (~in(sK3,sK2) | ~in(sK3,X3) | 'right:(Tree)>Tree'(sK2) != X3 | $less(sK3,'val:(Tree)>Int'(sK2)) | 'empty:Tree' = sK2) )),
% 0.21/0.30 inference(cnf_transformation,[],[f27])).
% 0.21/0.30 tff(f61,plain,(
% 0.21/0.30 ~in(sK3,sK2) | sK3 != 'val:(Tree)>Int'(sK2) | 'empty:Tree' = sK2),
% 0.21/0.30 inference(cnf_transformation,[],[f27])).
% 0.21/0.30 tff(f62,plain,(
% 0.21/0.30 in(sK3,sK2) | 'empty:Tree' != sK2),
% 0.21/0.30 inference(cnf_transformation,[],[f27])).
% 0.21/0.30 tff(f63,plain,(
% 0.21/0.30 searchtree(sK2)),
% 0.21/0.30 inference(cnf_transformation,[],[f27])).
% 0.21/0.30 tff(f64,plain,(
% 0.21/0.30 ( ! [X1 : 'Tree'] : (in('val:(Tree)>Int'(X1),X1) | 'empty:Tree' = X1) )),
% 0.21/0.30 inference(equality_resolution,[],[f34])).
% 0.21/0.30 tff(f65,plain,(
% 0.21/0.30 ( ! [X0 : $int] : (~in(X0,'empty:Tree')) )),
% 0.21/0.30 inference(equality_resolution,[],[f33])).
% 0.21/0.30 tff(f67,plain,(
% 0.21/0.30 ~in(sK3,sK2) | ~in(sK3,'right:(Tree)>Tree'(sK2)) | $less(sK3,'val:(Tree)>Int'(sK2)) | 'empty:Tree' = sK2),
% 0.21/0.30 inference(equality_resolution,[],[f60])).
% 0.21/0.30 tff(f73,plain,(
% 0.21/0.30 ~in(sK3,sK2) | ~$less(sK3,'val:(Tree)>Int'(sK2)) | ~in(sK3,'left:(Tree)>Tree'(sK2)) | 'empty:Tree' = sK2),
% 0.21/0.30 inference(equality_resolution,[],[f52])).
% 0.21/0.30 tff(f76,definition,(
% 0.21/0.30 spl6_1 <=> 'empty:Tree' = sK2),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition])).
% 0.21/0.30 tff(f77,plain,(
% 0.21/0.30 'empty:Tree' != sK2 | spl6_1),
% 0.21/0.30 inference(avatar_component_clause,[],[f76])).
% 0.21/0.30 tff(f78,plain,(
% 0.21/0.30 'empty:Tree' = sK2 | ~spl6_1),
% 0.21/0.30 inference(avatar_component_clause,[],[f76])).
% 0.21/0.30 tff(f80,definition,(
% 0.21/0.30 spl6_2 <=> sK3 = 'val:(Tree)>Int'(sK2)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition])).
% 0.21/0.30 tff(f81,plain,(
% 0.21/0.30 sK3 != 'val:(Tree)>Int'(sK2) | spl6_2),
% 0.21/0.30 inference(avatar_component_clause,[],[f80])).
% 0.21/0.30 tff(f82,plain,(
% 0.21/0.30 sK3 = 'val:(Tree)>Int'(sK2) | ~spl6_2),
% 0.21/0.30 inference(avatar_component_clause,[],[f80])).
% 0.21/0.30 tff(f84,definition,(
% 0.21/0.30 spl6_3 <=> in(sK3,'left:(Tree)>Tree'(sK2))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition])).
% 0.21/0.30 tff(f85,plain,(
% 0.21/0.30 in(sK3,'left:(Tree)>Tree'(sK2)) | ~spl6_3),
% 0.21/0.30 inference(avatar_component_clause,[],[f84])).
% 0.21/0.30 tff(f86,plain,(
% 0.21/0.30 ~in(sK3,'left:(Tree)>Tree'(sK2)) | spl6_3),
% 0.21/0.30 inference(avatar_component_clause,[],[f84])).
% 0.21/0.30 tff(f88,definition,(
% 0.21/0.30 spl6_4 <=> $less(sK3,'val:(Tree)>Int'(sK2))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl6_4])],[avatar_definition])).
% 0.21/0.30 tff(f89,plain,(
% 0.21/0.30 $less(sK3,'val:(Tree)>Int'(sK2)) | ~spl6_4),
% 0.21/0.30 inference(avatar_component_clause,[],[f88])).
% 0.21/0.30 tff(f90,plain,(
% 0.21/0.30 ~$less(sK3,'val:(Tree)>Int'(sK2)) | spl6_4),
% 0.21/0.30 inference(avatar_component_clause,[],[f88])).
% 0.21/0.30 tff(f92,definition,(
% 0.21/0.30 spl6_5 <=> in(sK3,sK2)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl6_5])],[avatar_definition])).
% 0.21/0.30 tff(f93,plain,(
% 0.21/0.30 in(sK3,sK2) | ~spl6_5),
% 0.21/0.30 inference(avatar_component_clause,[],[f92])).
% 0.21/0.30 tff(f94,plain,(
% 0.21/0.30 ~in(sK3,sK2) | spl6_5),
% 0.21/0.30 inference(avatar_component_clause,[],[f92])).
% 0.21/0.30 tff(f96,plain,(
% 0.21/0.30 spl6_1 | ~spl6_3 | ~spl6_4 | ~spl6_5),
% 0.21/0.30 inference(avatar_split_clause,[],[f73,f92,f88,f84,f76])).
% 0.21/0.30 tff(f98,definition,(
% 0.21/0.30 spl6_6 <=> in(sK3,sK5)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl6_6])],[avatar_definition])).
% 0.21/0.30 tff(f100,plain,(
% 0.21/0.30 in(sK3,sK5) | ~spl6_6),
% 0.21/0.30 inference(avatar_component_clause,[],[f98])).
% 0.21/0.30 tff(f101,plain,(
% 0.21/0.30 spl6_6 | ~spl6_4 | spl6_2 | spl6_1 | spl6_5),
% 0.21/0.30 inference(avatar_split_clause,[],[f53,f92,f76,f80,f88,f98])).
% 0.21/0.30 tff(f103,definition,(
% 0.21/0.30 spl6_7 <=> sK5 = 'left:(Tree)>Tree'(sK2)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl6_7])],[avatar_definition])).
% 0.21/0.30 tff(f105,plain,(
% 0.21/0.30 sK5 = 'left:(Tree)>Tree'(sK2) | ~spl6_7),
% 0.21/0.30 inference(avatar_component_clause,[],[f103])).
% 0.21/0.30 tff(f106,plain,(
% 0.21/0.30 spl6_7 | ~spl6_4 | spl6_2 | spl6_1 | spl6_5),
% 0.21/0.30 inference(avatar_split_clause,[],[f54,f92,f76,f80,f88,f103])).
% 0.21/0.30 tff(f108,definition,(
% 0.21/0.30 spl6_8 <=> in(sK3,'right:(Tree)>Tree'(sK2))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl6_8])],[avatar_definition])).
% 0.21/0.30 tff(f109,plain,(
% 0.21/0.30 in(sK3,'right:(Tree)>Tree'(sK2)) | ~spl6_8),
% 0.21/0.30 inference(avatar_component_clause,[],[f108])).
% 0.21/0.30 tff(f110,plain,(
% 0.21/0.30 ~in(sK3,'right:(Tree)>Tree'(sK2)) | spl6_8),
% 0.21/0.30 inference(avatar_component_clause,[],[f108])).
% 0.21/0.30 tff(f114,definition,(
% 0.21/0.30 spl6_9 <=> in(sK3,sK4)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl6_9])],[avatar_definition])).
% 0.21/0.30 tff(f116,plain,(
% 0.21/0.30 in(sK3,sK4) | ~spl6_9),
% 0.21/0.30 inference(avatar_component_clause,[],[f114])).
% 0.21/0.30 tff(f117,plain,(
% 0.21/0.30 spl6_9 | spl6_4 | spl6_2 | spl6_1 | spl6_5),
% 0.21/0.30 inference(avatar_split_clause,[],[f57,f92,f76,f80,f88,f114])).
% 0.21/0.30 tff(f119,definition,(
% 0.21/0.30 spl6_10 <=> sK4 = 'right:(Tree)>Tree'(sK2)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl6_10])],[avatar_definition])).
% 0.21/0.30 tff(f121,plain,(
% 0.21/0.30 sK4 = 'right:(Tree)>Tree'(sK2) | ~spl6_10),
% 0.21/0.30 inference(avatar_component_clause,[],[f119])).
% 0.21/0.30 tff(f122,plain,(
% 0.21/0.30 spl6_10 | spl6_4 | spl6_2 | spl6_1 | spl6_5),
% 0.21/0.30 inference(avatar_split_clause,[],[f58,f92,f76,f80,f88,f119])).
% 0.21/0.30 tff(f124,plain,(
% 0.21/0.30 spl6_1 | spl6_4 | ~spl6_8 | ~spl6_5),
% 0.21/0.30 inference(avatar_split_clause,[],[f67,f92,f108,f88,f76])).
% 0.21/0.30 tff(f125,plain,(
% 0.21/0.30 spl6_1 | ~spl6_2 | ~spl6_5),
% 0.21/0.30 inference(avatar_split_clause,[],[f61,f92,f80,f76])).
% 0.21/0.30 tff(f126,plain,(
% 0.21/0.30 ~spl6_1 | spl6_5),
% 0.21/0.30 inference(avatar_split_clause,[],[f62,f92,f76])).
% 0.21/0.30 tff(f134,plain,(
% 0.21/0.30 in(sK3,sK2) | 'empty:Tree' = sK2 | ~spl6_2),
% 0.21/0.30 inference(superposition,[],[f64,f82])).
% 0.21/0.30 tff(f137,plain,(
% 0.21/0.30 'empty:Tree' = sK2 | (~spl6_2 | spl6_5)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f134,f94])).
% 0.21/0.30 tff(f138,plain,(
% 0.21/0.30 $false | (spl6_1 | ~spl6_2 | spl6_5)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f137,f77])).
% 0.21/0.30 tff(f139,plain,(
% 0.21/0.30 spl6_1 | ~spl6_2 | spl6_5),
% 0.21/0.30 inference(avatar_contradiction_clause,[],[f138])).
% 0.21/0.30 tff(f315,plain,(
% 0.21/0.30 ( ! [X0 : $int] : (~in(X0,'left:(Tree)>Tree'(sK2)) | ~$less('val:(Tree)>Int'(sK2),X0) | 'empty:Tree' = sK2) )),
% 0.21/0.30 inference(resolution,[],[f38,f63])).
% 0.21/0.30 tff(f316,plain,(
% 0.21/0.30 ( ! [X0 : $int] : (~in(X0,'left:(Tree)>Tree'(sK2)) | ~$less('val:(Tree)>Int'(sK2),X0)) ) | spl6_1),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f315,f77])).
% 0.21/0.30 tff(f330,plain,(
% 0.21/0.30 ( ! [X0 : $int] : (~in(X0,'right:(Tree)>Tree'(sK2)) | $less('val:(Tree)>Int'(sK2),X0) | 'empty:Tree' = sK2) )),
% 0.21/0.30 inference(resolution,[],[f47,f63])).
% 0.21/0.30 tff(f334,plain,(
% 0.21/0.30 'empty:Tree' = sK2 | in(sK3,'left:(Tree)>Tree'(sK2)) | sK3 = 'val:(Tree)>Int'(sK2) | ~in(sK3,sK2) | spl6_8),
% 0.21/0.30 inference(resolution,[],[f37,f110])).
% 0.21/0.30 tff(f338,plain,(
% 0.21/0.30 in(sK3,'left:(Tree)>Tree'(sK2)) | sK3 = 'val:(Tree)>Int'(sK2) | ~in(sK3,sK2) | (spl6_1 | spl6_8)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f334,f77])).
% 0.21/0.30 tff(f340,plain,(
% 0.21/0.30 sK3 = 'val:(Tree)>Int'(sK2) | ~in(sK3,sK2) | (spl6_1 | spl6_3 | spl6_8)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f338,f86])).
% 0.21/0.30 tff(f342,plain,(
% 0.21/0.30 ~in(sK3,sK2) | (spl6_1 | spl6_2 | spl6_3 | spl6_8)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f340,f81])).
% 0.21/0.30 tff(f343,plain,(
% 0.21/0.30 $false | (spl6_1 | spl6_2 | spl6_3 | ~spl6_5 | spl6_8)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f342,f93])).
% 0.21/0.30 tff(f344,plain,(
% 0.21/0.30 spl6_1 | spl6_2 | spl6_3 | ~spl6_5 | spl6_8),
% 0.21/0.30 inference(avatar_contradiction_clause,[],[f343])).
% 0.21/0.30 tff(f345,plain,(
% 0.21/0.30 ~$less('val:(Tree)>Int'(sK2),sK3) | (spl6_1 | ~spl6_3)),
% 0.21/0.30 inference(resolution,[],[f85,f316])).
% 0.21/0.30 tff(f348,plain,(
% 0.21/0.30 $less(sK3,'val:(Tree)>Int'(sK2)) | sK3 = 'val:(Tree)>Int'(sK2) | (spl6_1 | ~spl6_3)),
% 0.21/0.30 inference(resolution,[],[f345,f18])).
% 0.21/0.30 tff(f352,plain,(
% 0.21/0.30 sK3 = 'val:(Tree)>Int'(sK2) | (spl6_1 | ~spl6_3 | spl6_4)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f348,f90])).
% 0.21/0.30 tff(f355,plain,(
% 0.21/0.30 $false | (spl6_1 | spl6_2 | ~spl6_3 | spl6_4)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f352,f81])).
% 0.21/0.30 tff(f356,plain,(
% 0.21/0.30 spl6_1 | spl6_2 | ~spl6_3 | spl6_4),
% 0.21/0.30 inference(avatar_contradiction_clause,[],[f355])).
% 0.21/0.30 tff(f357,plain,(
% 0.21/0.30 ( ! [X0 : $int] : (~in(X0,sK2)) ) | ~spl6_1),
% 0.21/0.30 inference(superposition,[],[f65,f78])).
% 0.21/0.30 tff(f360,plain,(
% 0.21/0.30 $false | (~spl6_1 | ~spl6_5)),
% 0.21/0.30 inference(resolution,[],[f357,f93])).
% 0.21/0.30 tff(f361,plain,(
% 0.21/0.30 ~spl6_1 | ~spl6_5),
% 0.21/0.30 inference(avatar_contradiction_clause,[],[f360])).
% 0.21/0.30 tff(f363,plain,(
% 0.21/0.30 ( ! [X0 : $int] : (~in(X0,'right:(Tree)>Tree'(sK2)) | $less('val:(Tree)>Int'(sK2),X0)) ) | spl6_1),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f330,f77])).
% 0.21/0.30 tff(f364,plain,(
% 0.21/0.30 ( ! [X0 : $int] : ($less(X0,'val:(Tree)>Int'(sK2)) | ~$less(X0,sK3)) ) | ~spl6_4),
% 0.21/0.30 inference(resolution,[],[f89,f17])).
% 0.21/0.30 tff(f371,plain,(
% 0.21/0.30 ~$less('val:(Tree)>Int'(sK2),sK3) | ~spl6_4),
% 0.21/0.31 inference(resolution,[],[f364,f16])).
% 0.21/0.31 tff(f434,plain,(
% 0.21/0.31 $less('val:(Tree)>Int'(sK2),sK3) | (spl6_1 | ~spl6_8)),
% 0.21/0.31 inference(resolution,[],[f363,f109])).
% 0.21/0.31 tff(f437,plain,(
% 0.21/0.31 $false | (spl6_1 | ~spl6_4 | ~spl6_8)),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f434,f371])).
% 0.21/0.31 tff(f438,plain,(
% 0.21/0.31 spl6_1 | ~spl6_4 | ~spl6_8),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f437])).
% 0.21/0.31 tff(f450,plain,(
% 0.21/0.31 ~in(sK3,sK5) | (spl6_3 | ~spl6_7)),
% 0.21/0.31 inference(superposition,[],[f86,f105])).
% 0.21/0.31 tff(f453,plain,(
% 0.21/0.31 ( ! [X0 : $int] : (~in(X0,sK5) | 'empty:Tree' = sK2 | in(X0,sK2)) ) | ~spl6_7),
% 0.21/0.31 inference(superposition,[],[f35,f105])).
% 0.21/0.31 tff(f456,plain,(
% 0.21/0.31 ( ! [X0 : $int] : (~in(X0,sK5) | in(X0,sK2)) ) | (spl6_1 | ~spl6_7)),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f453,f77])).
% 0.21/0.31 tff(f458,plain,(
% 0.21/0.31 $false | (spl6_3 | ~spl6_6 | ~spl6_7)),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f450,f100])).
% 0.21/0.31 tff(f459,plain,(
% 0.21/0.31 spl6_3 | ~spl6_6 | ~spl6_7),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f458])).
% 0.21/0.31 tff(f483,plain,(
% 0.21/0.31 in(sK3,sK2) | (spl6_1 | ~spl6_6 | ~spl6_7)),
% 0.21/0.31 inference(resolution,[],[f456,f100])).
% 0.21/0.31 tff(f484,plain,(
% 0.21/0.31 $false | (spl6_1 | spl6_5 | ~spl6_6 | ~spl6_7)),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f483,f94])).
% 0.21/0.31 tff(f485,plain,(
% 0.21/0.31 spl6_1 | spl6_5 | ~spl6_6 | ~spl6_7),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f484])).
% 0.21/0.31 tff(f495,plain,(
% 0.21/0.31 ( ! [X0 : $int] : (~in(X0,sK4) | 'empty:Tree' = sK2 | in(X0,sK2)) ) | ~spl6_10),
% 0.21/0.31 inference(superposition,[],[f36,f121])).
% 0.21/0.31 tff(f504,plain,(
% 0.21/0.31 ( ! [X0 : $int] : (~in(X0,sK4) | in(X0,sK2)) ) | (spl6_1 | ~spl6_10)),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f495,f77])).
% 0.21/0.31 tff(f529,plain,(
% 0.21/0.31 in(sK3,sK2) | (spl6_1 | ~spl6_9 | ~spl6_10)),
% 0.21/0.31 inference(resolution,[],[f504,f116])).
% 0.21/0.31 tff(f530,plain,(
% 0.21/0.31 $false | (spl6_1 | spl6_5 | ~spl6_9 | ~spl6_10)),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f529,f94])).
% 0.21/0.31 tff(f531,plain,(
% 0.21/0.31 spl6_1 | spl6_5 | ~spl6_9 | ~spl6_10),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f530])).
% 0.21/0.31 cnf(s2, plain, spl6_1 | ~spl6_3 | ~spl6_4 | ~spl6_5, inference(sat_conversion,[],[f96])).
% 0.21/0.31 cnf(s3, plain, spl6_1 | spl6_2 | ~spl6_4 | spl6_5 | spl6_6, inference(sat_conversion,[],[f101])).
% 0.21/0.31 cnf(s4, plain, spl6_1 | spl6_2 | ~spl6_4 | spl6_5 | spl6_7, inference(sat_conversion,[],[f106])).
% 0.21/0.31 cnf(s7, plain, spl6_1 | spl6_2 | spl6_4 | spl6_5 | spl6_9, inference(sat_conversion,[],[f117])).
% 0.21/0.31 cnf(s8, plain, spl6_1 | spl6_2 | spl6_4 | spl6_5 | spl6_10, inference(sat_conversion,[],[f122])).
% 0.21/0.31 cnf(s10, plain, spl6_1 | spl6_4 | ~spl6_5 | ~spl6_8, inference(sat_conversion,[],[f124])).
% 0.21/0.31 cnf(s11, plain, spl6_1 | ~spl6_2 | ~spl6_5, inference(sat_conversion,[],[f125])).
% 0.21/0.31 cnf(s12, plain, ~spl6_1 | spl6_5, inference(sat_conversion,[],[f126])).
% 0.21/0.31 cnf(s13, plain, spl6_1 | ~spl6_2 | spl6_5, inference(sat_conversion,[],[f139])).
% 0.21/0.31 cnf(s15, plain, spl6_1 | spl6_2 | spl6_3 | ~spl6_5 | spl6_8, inference(sat_conversion,[],[f344])).
% 0.21/0.31 cnf(s17, plain, spl6_1 | spl6_2 | ~spl6_3 | spl6_4, inference(sat_conversion,[],[f356])).
% 0.21/0.31 cnf(s18, plain, ~spl6_1 | ~spl6_5, inference(sat_conversion,[],[f361])).
% 0.21/0.31 cnf(s21, plain, spl6_1 | ~spl6_4 | ~spl6_8, inference(sat_conversion,[],[f438])).
% 0.21/0.31 cnf(s23, plain, spl6_3 | ~spl6_6 | ~spl6_7, inference(sat_conversion,[],[f459])).
% 0.21/0.31 cnf(s27, plain, spl6_1 | spl6_5 | ~spl6_6 | ~spl6_7, inference(sat_conversion,[],[f485])).
% 0.21/0.31 cnf(s33, plain, spl6_1 | spl6_5 | ~spl6_9 | ~spl6_10, inference(sat_conversion,[],[f531])).
% 0.21/0.31 cnf(s34, plain, spl6_5 | spl6_4 | spl6_1 | spl6_2, inference(rat,[],[s33,s7,s8])).
% 0.21/0.31 cnf(s35, plain, spl6_4 | spl6_3 | spl6_2 | spl6_1, inference(rat,[],[s15,s10,s34])).
% 0.21/0.31 cnf(s36, plain, spl6_3 | spl6_2 | spl6_1, inference(rat,[],[s23,s3,s4,s15,s21,s35])).
% 0.21/0.31 cnf(s37, plain, spl6_5 | ~spl6_4 | spl6_1 | spl6_2, inference(rat,[],[s27,s3,s4])).
% 0.21/0.31 cnf(s38, plain, ~spl6_3 | spl6_2 | spl6_1, inference(rat,[],[s37,s2,s17])).
% 0.21/0.31 cnf(s39, plain, spl6_2 | spl6_1, inference(rat,[],[s38,s36])).
% 0.21/0.31 cnf(s40, plain, ~spl6_2 | spl6_1, inference(rat,[],[s11,s13])).
% 0.21/0.31 cnf(s41, plain, spl6_1, inference(rat,[],[s40,s39])).
% 0.21/0.31 cnf(s42, plain, ~spl6_5, inference(rat,[],[s18,s41])).
% 0.21/0.31 cnf(s43, plain, $false, inference(rat,[],[s12,s42,s41])).
% 0.21/0.31 tff(f533,plain,(
% 0.21/0.31 $false),
% 0.21/0.31 inference(avatar_sat_refutation,[],[s43])).
% 0.21/0.31 % SZS output end Proof for theBenchmark
% 0.21/0.31 % (2667813)------------------------------
% 0.21/0.31 % (2667813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.31 % (2667813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.31 % (2667813)CaDiCaL version: 2.1.3
% 0.21/0.31 % (2667813)Termination reason: Refutation
% 0.21/0.31 % (2667813)Time elapsed: 0.016 s
% 0.21/0.31 % (2667813)Peak memory usage: 12 MB
% 0.21/0.31 % (2667813)Instructions burned: 22 (million)
% 0.21/0.31 % (2667804)Success in time 0.06 s
% 0.21/0.31 % Vampire exiting
%------------------------------------------------------------------------------