%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV300^5 : TPTP v9.3.1. Bugfixed v6.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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 : Wed Sep 30 08:39:17 AM UTC 2026
% Result : Theorem 0.35s 0.42s
% Output : Refutation 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEV300^5 : TPTP v9.3.1. Bugfixed v6.2.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.27 % Computer : n007.cluster.edu
% 0.12/0.27 % Model : x86_64 x86_64
% 0.12/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.27 % Memory : 8046.5625MB
% 0.12/0.27 % OS : Linux 6.8.0-71-generic
% 0.12/0.28 % CPULimit : 300
% 0.12/0.28 % WCLimit : 300
% 0.12/0.28 % DateTime : Tue Sep 29 15:30:26 UTC 2026
% 0.12/0.28 % CPUTime :
% 0.12/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.28/0.33 Running first-order model finding
% 0.28/0.33 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.35/0.42 % (3509972)Will run a generic schedule for satisfiability detection.
% 0.35/0.42 % (3509980)dis+10_1_sil=32000:sp=arity:random_seed=780765057:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.35/0.42 % (3509978)% WARNING: option uhcvi not known.
% 0.35/0.42 % (3509977)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=174777492_2999 on theBenchmark for (2999ds/0Mi)
% 0.35/0.42 % (3509979)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3660437003:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.35/0.42 % (3509978)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4198920635:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.35/0.42 % (3509981)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=704052388:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.35/0.42 % (3509983)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1972548079:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.35/0.42 % (3509978)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.35/0.42 % (3509981)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.35/0.42 % (3509982)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=606526808:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.35/0.42 % Exception at run slice level
% 0.35/0.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.35/0.42 % (3509978)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.35/0.42 % (3509979) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3509972-3509979"...
% 0.35/0.42 % (3509979)...printing done.
% 0.35/0.42 % (3509980)Instruction limit reached!
% 0.35/0.42 % (3509980)------------------------------
% 0.35/0.42 % (3509980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.35/0.42 % (3509980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/0.42 % (3509980)CaDiCaL version: 2.1.3
% 0.35/0.42 % (3509980)Termination reason: Instruction limit
% 0.35/0.42 % (3509980)Termination phase: Saturation
% 0.35/0.42 % (3509980)Time elapsed: 0.042 s
% 0.35/0.42 % (3509980)Peak memory usage: 11 MB
% 0.35/0.42 % (3509980)Instructions burned: 105 (million)
% 0.35/0.42 % (3509979)Refutation found. Thanks to Tanya!
% 0.35/0.42 % SZS status Theorem for theBenchmark
% 0.35/0.42 % SZS output start Proof for theBenchmark
% 0.35/0.42 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.35/0.42 thf(func_def_0, type, cONE: (($i > $o) > $o)).
% 0.35/0.42 thf(func_def_1, type, cSUCC: ((($i > $o) > $o) > ($i > $o) > $o)).
% 0.35/0.42 thf(func_def_2, type, cZERO: (($i > $o) > $o)).
% 0.35/0.42 thf(func_def_4, type, vNOT: ($o > $o)).
% 0.35/0.42 thf(func_def_5, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.35/0.42 thf(func_def_6, type, db1: !>[X0: $tType]:(X0)).
% 0.35/0.42 thf(func_def_7, type, db0: !>[X0: $tType]:(X0)).
% 0.35/0.42 thf(func_def_8, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.35/0.42 thf(func_def_9, type, vAND: ($o > $o > $o)).
% 0.35/0.42 thf(func_def_10, type, db2: !>[X0: $tType]:(X0)).
% 0.35/0.42 thf(func_def_11, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.35/0.42 thf(func_def_12, type, sK0: (($i > $i) > ($i > $i) > $i)).
% 0.35/0.42 thf(func_def_15, type, db3: !>[X0: $tType]:(X0)).
% 0.35/0.42 thf(func_def_16, type, sK1: ($i > $o)).
% 0.35/0.42 thf(func_def_17, type, sK2: ($i > $i)).
% 0.35/0.42 thf(func_def_22, type, sK7: ($i > $i)).
% 0.35/0.42 thf(func_def_24, type, sK9: ($i > $i)).
% 0.35/0.42 thf(f1,axiom,(
% 0.35/0.42 (cZERO = (^[X0 : ($i > $o)] : (~ ? [X1 : $i] : (X0 @ X1))))),
% 0.35/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cZERO_def)).
% 0.35/0.42 thf(f2,axiom,(
% 0.35/0.42 (cSUCC = (^[X0 : (($i > $o) > $o), X1 : ($i > $o)] : (? [X2 : $i] : ((X0 @ (^[X3 : $i] : ((X1 @ X3) & (X3 != X2)))) & (X1 @ X2)))))),
% 0.35/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cSUCC_def)).
% 0.35/0.42 thf(f3,axiom,(
% 0.35/0.42 (cONE = ((cSUCC @ cZERO)))),
% 0.35/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cONE_def)).
% 0.35/0.42 thf(f4,conjecture,(
% 0.35/0.42 ! [X0 : ($i > $i),X1 : ($i > $i)] : (! [X2 : $i] : (((X0 @ X2)) = ((X1 @ X2))) => (X0 = X1)) => (cONE = (^[X3 : ($i > $o)] : (? [X4 : $i] : (X3 = (((^[X2 : $i, X4 : $i] : ((X2 = X4))) @ X4))))))),
% 0.35/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cX6101_EXT_pme)).
% 0.35/0.42 thf(f5,negated_conjecture,(
% 0.35/0.42 ~(! [X0 : ($i > $i),X1 : ($i > $i)] : (! [X2 : $i] : (((X0 @ X2)) = ((X1 @ X2))) => (X0 = X1)) => (cONE = (^[X3 : ($i > $o)] : (? [X4 : $i] : (X3 = (((^[X2 : $i, X4 : $i] : ((X2 = X4))) @ X4)))))))),
% 0.35/0.42 inference(negated_conjecture,[status(cth)],[f4])).
% 0.35/0.42 thf(f6,plain,(
% 0.35/0.42 (cZERO = (^[X0 : ($i > $o)] : (~ ? [X1 : $i] : (X0 @ X1))))),
% 0.35/0.42 inference(rectify,[],[f1])).
% 0.35/0.42 thf(f7,plain,(
% 0.35/0.42 (cZERO = (^[Y0 : $i > $o]: (~ (?? @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))))),
% 0.35/0.42 inference(fool_elimination,[],[f6])).
% 0.35/0.42 thf(f8,plain,(
% 0.35/0.42 (cSUCC = (^[X0 : (($i > $o) > $o), X1 : ($i > $o)] : (? [X2 : $i] : ((X0 @ (^[X3 : $i] : ((X1 @ X3) & (X3 != X2)))) & (X1 @ X2)))))),
% 0.35/0.42 inference(rectify,[],[f2])).
% 0.35/0.42 thf(f9,plain,(
% 0.35/0.42 (cSUCC = (^[Y0 : ($i > $o) > $o]: ((^[Y1 : $i > $o]: (?? @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ (^[Y3 : $i]: ((~ (Y2 = Y3)) & (Y1 @ Y3)))))))))))),
% 0.35/0.42 inference(fool_elimination,[],[f8])).
% 0.35/0.42 thf(f10,plain,(
% 0.35/0.42 ~(! [X0 : ($i > $i),X1 : ($i > $i)] : (! [X2 : $i] : (((X0 @ X2)) = ((X1 @ X2))) => (X0 = X1)) => (cONE = (^[X3 : ($i > $o)] : (? [X4 : $i] : (X3 = (((^[X5 : $i, X6 : $i] : ((X5 = X6))) @ X4)))))))),
% 0.35/0.42 inference(rectify,[],[f5])).
% 0.35/0.42 thf(f11,plain,(
% 0.35/0.42 ~(! [X0 : ($i > $i),X1 : ($i > $i)] : (! [X2 : $i] : (((X0 @ X2)) = ((X1 @ X2))) => (X0 = X1)) => (cONE = (^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: (Y0 = ((^[Y2 : $i]: ((^[Y3 : $i]: (Y2 = Y3)))) @ Y1)))))))),
% 0.35/0.42 inference(fool_elimination,[],[f10])).
% 0.35/0.42 thf(f12,plain,(
% 0.35/0.42 (cONE != (^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: (Y0 = ((^[Y2 : $i]: ((^[Y3 : $i]: (Y2 = Y3)))) @ Y1)))))) & ! [X0 : ($i > $i),X1 : ($i > $i)] : ((X0 = X1) | ? [X2 : $i] : (((X0 @ X2)) != ((X1 @ X2))))),
% 0.35/0.42 inference(ennf_transformation,[],[f11])).
% 0.35/0.42 thf(f13,plain,(
% 0.35/0.42 (cONE != (^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: (Y0 = ((^[Y2 : $i]: ((^[Y3 : $i]: (Y2 = Y3)))) @ Y1)))))) & ! [X0 : ($i > $i),X1 : ($i > $i)] : ((X0 = X1) | (((X0 @ (sK0 @ X1 @ X0))) != ((X1 @ (sK0 @ X1 @ X0)))))),
% 0.35/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X2,sK0 @ X1 @ X0)],[f12])).
% 0.35/0.42 thf(f14,plain,(
% 0.35/0.42 (cZERO = (^[Y0 : $i > $o]: (~ (?? @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))))),
% 0.35/0.42 inference(cnf_transformation,[],[f7])).
% 0.35/0.42 thf(f15,plain,(
% 0.35/0.42 (cSUCC = (^[Y0 : ($i > $o) > $o]: ((^[Y1 : $i > $o]: (?? @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ (^[Y3 : $i]: ((~ (Y2 = Y3)) & (Y1 @ Y3)))))))))))),
% 0.35/0.42 inference(cnf_transformation,[],[f9])).
% 0.35/0.42 thf(f16,plain,(
% 0.35/0.42 (cONE = ((cSUCC @ cZERO)))),
% 0.35/0.42 inference(cnf_transformation,[],[f3])).
% 0.35/0.42 thf(f18,plain,(
% 0.35/0.42 (cONE != (^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: (Y0 = ((^[Y2 : $i]: ((^[Y3 : $i]: (Y2 = Y3)))) @ Y1))))))),
% 0.35/0.42 inference(cnf_transformation,[],[f13])).
% 0.35/0.42 thf(f21,plain,(
% 0.35/0.42 (cONE = (((^[Y0 : ($i > $o) > $o]: ((^[Y1 : $i > $o]: (?? @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ (^[Y3 : $i]: ((~ (Y2 = Y3)) & (Y1 @ Y3)))))))))) @ (^[Y0 : $i > $o]: (~ (?? @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))))))),
% 0.35/0.42 inference(definition_unfolding,[],[f16,f15,f14])).
% 0.35/0.42 thf(f22,plain,(
% 0.35/0.42 ((^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: (Y0 = ((^[Y2 : $i]: ((^[Y3 : $i]: (Y2 = Y3)))) @ Y1))))) != (((^[Y0 : ($i > $o) > $o]: ((^[Y1 : $i > $o]: (?? @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ (^[Y3 : $i]: ((~ (Y2 = Y3)) & (Y1 @ Y3)))))))))) @ (^[Y0 : $i > $o]: (~ (?? @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))))))),
% 0.35/0.42 inference(definition_unfolding,[],[f18,f21])).
% 0.35/0.42 thf(f23,plain,(
% 0.35/0.42 ((^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: (Y0 = (= @ Y1))))) != (^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (~ (?? @ $i @ (^[Y2 : $i]: ((~ (Y1 = Y2)) & (Y0 @ Y2))))))))))),
% 0.35/0.42 inference(beta-eta_normalization,[],[f22])).
% 0.35/0.42 thf(f24,plain,(
% 0.35/0.42 ((((^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: (Y0 = (= @ Y1))))) @ sK1)) != (((^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (~ (?? @ $i @ (^[Y2 : $i]: ((~ (Y1 = Y2)) & (Y0 @ Y2))))))))) @ sK1)))),
% 0.35/0.42 inference(negative_extensionality,[],[f23])).
% 0.35/0.42 thf(f25,plain,(
% 0.35/0.42 ($true = (((^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: (Y0 = (= @ Y1))))) @ sK1))) | ($true = (((^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (~ (?? @ $i @ (^[Y2 : $i]: ((~ (Y1 = Y2)) & (Y0 @ Y2))))))))) @ sK1)))),
% 0.35/0.42 inference(xor_proxy_clausification,[],[f24])).
% 0.35/0.42 thf(f26,plain,(
% 0.35/0.42 ($false = (((^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: (Y0 = (= @ Y1))))) @ sK1))) | ($false = (((^[Y0 : $i > $o]: (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (~ (?? @ $i @ (^[Y2 : $i]: ((~ (Y1 = Y2)) & (Y0 @ Y2))))))))) @ sK1)))),
% 0.35/0.42 inference(xor_proxy_clausification,[],[f24])).
% 0.35/0.42 thf(f27,plain,(
% 0.35/0.42 ($false = ((?? @ $i @ (^[Y0 : $i]: (sK1 = (= @ Y0)))))) | ($false = ((?? @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) & (~ (?? @ $i @ (^[Y1 : $i]: ((~ (Y0 = Y1)) & (sK1 @ Y1))))))))))),
% 0.35/0.42 inference(beta-eta_normalization,[],[f26])).
% 0.35/0.42 thf(f28,plain,(
% 0.35/0.42 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (sK1 = (= @ Y0))) @ X1))) | ($false = ((?? @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) & (~ (?? @ $i @ (^[Y1 : $i]: ((~ (Y0 = Y1)) & (sK1 @ Y1))))))))))) )),
% 0.35/0.42 inference(pi_proxy_clausification,[],[f27])).
% 0.35/0.42 thf(f29,plain,(
% 0.35/0.42 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: (sK1 = (= @ Y0))) @ X1))) | ($false = (((^[Y0 : $i]: ((sK1 @ Y0) & (~ (?? @ $i @ (^[Y1 : $i]: ((~ (Y0 = Y1)) & (sK1 @ Y1))))))) @ X2)))) )),
% 0.35/0.42 inference(pi_proxy_clausification,[],[f28])).
% 0.35/0.42 thf(f30,plain,(
% 0.35/0.42 ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 = (= @ X1)))) | ($false = (((sK1 @ X2) & (~ (?? @ $i @ (^[Y0 : $i]: ((~ (X2 = Y0)) & (sK1 @ Y0))))))))) )),
% 0.35/0.42 inference(beta-eta_normalization,[],[f29])).
% 0.35/0.42 thf(f31,plain,(
% 0.35/0.42 ( ! [X2 : $i,X1 : $i] : ((sK1 != ((= @ X1))) | ($false = (((sK1 @ X2) & (~ (?? @ $i @ (^[Y0 : $i]: ((~ (X2 = Y0)) & (sK1 @ Y0))))))))) )),
% 0.35/0.42 inference(equality_proxy_clausification,[],[f30])).
% 0.35/0.42 thf(f32,plain,(
% 0.35/0.42 ( ! [X2 : $i,X1 : $i] : ((sK1 != ((= @ X1))) | ($false = ((~ (?? @ $i @ (^[Y0 : $i]: ((~ (X2 = Y0)) & (sK1 @ Y0))))))) | ($false = ((sK1 @ X2)))) )),
% 0.35/0.42 inference(and_proxy_clausification,[],[f31])).
% 0.35/0.42 thf(f33,plain,(
% 0.35/0.42 ( ! [X2 : $i,X1 : $i] : ((sK1 != ((= @ X1))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((~ (X2 = Y0)) & (sK1 @ Y0)))))) | ($false = ((sK1 @ X2)))) )),
% 0.35/0.42 inference(not_proxy_clausification,[],[f32])).
% 0.35/0.42 thf(f34,plain,(
% 0.35/0.42 ( ! [X2 : $i,X1 : $i] : ((sK1 != ((= @ X1))) | ($true = (((^[Y0 : $i]: ((~ (X2 = Y0)) & (sK1 @ Y0))) @ (sK2 @ X2)))) | ($false = ((sK1 @ X2)))) )),
% 0.35/0.42 inference(sigma_proxy_clausification,[],[f33])).
% 0.35/0.42 thf(f35,plain,(
% 0.35/0.42 ( ! [X2 : $i,X1 : $i] : ((sK1 != ((= @ X1))) | ($true = (((~ (X2 = (sK2 @ X2))) & (sK1 @ (sK2 @ X2))))) | ($false = ((sK1 @ X2)))) )),
% 0.35/0.42 inference(beta-eta_normalization,[],[f34])).
% 0.35/0.42 thf(f36,plain,(
% 0.35/0.42 ( ! [X2 : $i,X1 : $i] : ((sK1 != ((= @ X1))) | ($true = ((sK1 @ (sK2 @ X2)))) | ($false = ((sK1 @ X2)))) )),
% 0.35/0.42 inference(and_proxy_clausification,[],[f35])).
% 0.35/0.42 thf(f37,plain,(
% 0.35/0.42 ( ! [X2 : $i,X1 : $i] : ((sK1 != ((= @ X1))) | ($true = ((~ (X2 = (sK2 @ X2))))) | ($false = ((sK1 @ X2)))) )),
% 0.35/0.42 inference(and_proxy_clausification,[],[f35])).
% 0.35/0.42 thf(f38,plain,(
% 0.35/0.42 ( ! [X2 : $i,X1 : $i] : ((sK1 != ((= @ X1))) | ($false = ((X2 = (sK2 @ X2)))) | ($false = ((sK1 @ X2)))) )),
% 0.35/0.42 inference(not_proxy_clausification,[],[f37])).
% 0.35/0.42 thf(f39,plain,(
% 0.35/0.42 ( ! [X2 : $i,X1 : $i] : ((sK1 != ((= @ X1))) | (((sK2 @ X2)) != X2) | ($false = ((sK1 @ X2)))) )),
% 0.35/0.42 inference(equality_proxy_clausification,[],[f38])).
% 0.35/0.42 thf(f40,plain,(
% 0.35/0.42 ($true = ((?? @ $i @ (^[Y0 : $i]: (sK1 = (= @ Y0)))))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) & (~ (?? @ $i @ (^[Y1 : $i]: ((~ (Y0 = Y1)) & (sK1 @ Y1))))))))))),
% 0.35/0.43 inference(beta-eta_normalization,[],[f25])).
% 0.35/0.43 thf(f41,plain,(
% 0.35/0.43 ($true = (((^[Y0 : $i]: (sK1 = (= @ Y0))) @ sK3))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) & (~ (?? @ $i @ (^[Y1 : $i]: ((~ (Y0 = Y1)) & (sK1 @ Y1))))))))))),
% 0.35/0.43 inference(sigma_proxy_clausification,[],[f40])).
% 0.35/0.43 thf(f42,plain,(
% 0.35/0.43 ($true = (((^[Y0 : $i]: (sK1 = (= @ Y0))) @ sK3))) | ($true = (((^[Y0 : $i]: ((sK1 @ Y0) & (~ (?? @ $i @ (^[Y1 : $i]: ((~ (Y0 = Y1)) & (sK1 @ Y1))))))) @ sK4)))),
% 0.35/0.43 inference(sigma_proxy_clausification,[],[f41])).
% 0.35/0.43 thf(f43,plain,(
% 0.35/0.43 ($true = ((sK1 = (= @ sK3)))) | ($true = (((sK1 @ sK4) & (~ (?? @ $i @ (^[Y0 : $i]: ((~ (sK4 = Y0)) & (sK1 @ Y0))))))))),
% 0.35/0.43 inference(beta-eta_normalization,[],[f42])).
% 0.35/0.43 thf(f44,plain,(
% 0.35/0.43 (sK1 = ((= @ sK3))) | ($true = (((sK1 @ sK4) & (~ (?? @ $i @ (^[Y0 : $i]: ((~ (sK4 = Y0)) & (sK1 @ Y0))))))))),
% 0.35/0.43 inference(equality_proxy_clausification,[],[f43])).
% 0.35/0.43 thf(f45,plain,(
% 0.35/0.43 (sK1 = ((= @ sK3))) | ($true = ((~ (?? @ $i @ (^[Y0 : $i]: ((~ (sK4 = Y0)) & (sK1 @ Y0)))))))),
% 0.35/0.43 inference(and_proxy_clausification,[],[f44])).
% 0.35/0.43 thf(f46,plain,(
% 0.35/0.43 (sK1 = ((= @ sK3))) | ($true = ((sK1 @ sK4)))),
% 0.35/0.43 inference(and_proxy_clausification,[],[f44])).
% 0.35/0.43 thf(f47,plain,(
% 0.35/0.43 (sK1 = ((= @ sK3))) | ($false = ((?? @ $i @ (^[Y0 : $i]: ((~ (sK4 = Y0)) & (sK1 @ Y0))))))),
% 0.35/0.43 inference(not_proxy_clausification,[],[f45])).
% 0.35/0.43 thf(f48,plain,(
% 0.35/0.43 ( ! [X1 : $i] : ((sK1 = ((= @ sK3))) | ($false = (((^[Y0 : $i]: ((~ (sK4 = Y0)) & (sK1 @ Y0))) @ X1)))) )),
% 0.35/0.43 inference(pi_proxy_clausification,[],[f47])).
% 0.35/0.43 thf(f49,plain,(
% 0.35/0.43 ( ! [X1 : $i] : ((sK1 = ((= @ sK3))) | ($false = (((~ (sK4 = X1)) & (sK1 @ X1))))) )),
% 0.35/0.43 inference(beta-eta_normalization,[],[f48])).
% 0.35/0.43 thf(f50,plain,(
% 0.35/0.43 ( ! [X1 : $i] : ((sK1 = ((= @ sK3))) | ($false = ((sK1 @ X1))) | ($false = ((~ (sK4 = X1))))) )),
% 0.35/0.43 inference(and_proxy_clausification,[],[f49])).
% 0.35/0.43 thf(f51,plain,(
% 0.35/0.43 ( ! [X1 : $i] : ((sK1 = ((= @ sK3))) | ($false = ((sK1 @ X1))) | ($true = ((sK4 = X1)))) )),
% 0.35/0.43 inference(not_proxy_clausification,[],[f50])).
% 0.35/0.43 thf(f52,plain,(
% 0.35/0.43 ( ! [X1 : $i] : ((sK1 = ((= @ sK3))) | ($false = ((sK1 @ X1))) | (sK4 = X1)) )),
% 0.35/0.43 inference(equality_proxy_clausification,[],[f51])).
% 0.35/0.43 thf(f54,definition,(
% 0.35/0.43 spl5_1 <=> ($true = ((sK1 @ sK4)))),
% 0.35/0.43 introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition])).
% 0.35/0.43 thf(f56,plain,(
% 0.35/0.43 ($true = ((sK1 @ sK4))) | ~spl5_1),
% 0.35/0.43 inference(avatar_component_clause,[],[f54])).
% 0.35/0.43 thf(f58,definition,(
% 0.35/0.43 spl5_2 <=> (sK1 = ((= @ sK3)))),
% 0.35/0.43 introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition])).
% 0.35/0.43 thf(f60,plain,(
% 0.35/0.43 (sK1 = ((= @ sK3))) | ~spl5_2),
% 0.35/0.43 inference(avatar_component_clause,[],[f58])).
% 0.35/0.43 thf(f61,plain,(
% 0.35/0.43 spl5_1 | spl5_2),
% 0.35/0.43 inference(avatar_split_clause,[],[f46,f58,f54])).
% 0.35/0.43 thf(f69,definition,(
% 0.35/0.43 spl5_5 <=> ! [X1 : $i] : (($false = ((sK1 @ X1))) | (sK4 = X1))),
% 0.35/0.43 introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition])).
% 0.35/0.43 thf(f70,plain,(
% 0.35/0.43 ( ! [X1 : $i] : (($false = ((sK1 @ X1))) | (sK4 = X1)) ) | ~spl5_5),
% 0.35/0.43 inference(avatar_component_clause,[],[f69])).
% 0.35/0.43 thf(f71,plain,(
% 0.35/0.43 spl5_5 | spl5_2),
% 0.35/0.43 inference(avatar_split_clause,[],[f52,f58,f69])).
% 0.35/0.43 thf(f118,plain,(
% 0.35/0.43 ( ! [X1 : $i] : ((((sK1 @ X1)) = ((sK3 = X1)))) ) | ~spl5_2),
% 0.35/0.43 inference(argument_congruence,[],[f60])).
% 0.35/0.43 thf(f121,plain,(
% 0.35/0.43 ( ! [X1 : $i] : (($true = ((sK1 @ X1))) | ($false = ((sK3 = X1)))) ) | ~spl5_2),
% 0.35/0.43 inference(iff_proxy_clausification,[],[f118])).
% 0.35/0.43 thf(f122,plain,(
% 0.35/0.43 ( ! [X1 : $i] : (($false = ((sK1 @ X1))) | ($true = ((sK3 = X1)))) ) | ~spl5_2),
% 0.35/0.43 inference(iff_proxy_clausification,[],[f118])).
% 0.35/0.43 thf(f123,plain,(
% 0.35/0.43 ( ! [X1 : $i] : (($false = ((sK1 @ X1))) | (sK3 = X1)) ) | ~spl5_2),
% 0.35/0.43 inference(equality_proxy_clausification,[],[f122])).
% 0.35/0.43 thf(f124,plain,(
% 0.35/0.43 ( ! [X1 : $i] : ((sK3 != X1) | ($true = ((sK1 @ X1)))) ) | ~spl5_2),
% 0.35/0.43 inference(equality_proxy_clausification,[],[f121])).
% 0.35/0.43 thf(f160,plain,(
% 0.35/0.43 ($true = ((sK1 @ sK3))) | ~spl5_2),
% 0.35/0.43 inference(equality_resolution,[],[f124])).
% 0.35/0.43 thf(f185,definition,(
% 0.35/0.43 spl5_10 <=> ! [X2 : $i] : ((((sK2 @ X2)) != X2) | ($false = ((sK1 @ X2))))),
% 0.35/0.43 introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition])).
% 0.35/0.43 thf(f186,plain,(
% 0.35/0.43 ( ! [X2 : $i] : ((((sK2 @ X2)) != X2) | ($false = ((sK1 @ X2)))) ) | ~spl5_10),
% 0.35/0.43 inference(avatar_component_clause,[],[f185])).
% 0.35/0.43 thf(f188,definition,(
% 0.35/0.43 spl5_11 <=> ! [X1 : $i] : (sK1 != ((= @ X1)))),
% 0.35/0.43 introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition])).
% 0.35/0.43 thf(f189,plain,(
% 0.35/0.43 ( ! [X1 : $i] : ((sK1 != ((= @ X1)))) ) | ~spl5_11),
% 0.35/0.43 inference(avatar_component_clause,[],[f188])).
% 0.35/0.43 thf(f190,plain,(
% 0.35/0.43 spl5_10 | spl5_11),
% 0.35/0.43 inference(avatar_split_clause,[],[f39,f188,f185])).
% 0.35/0.43 thf(f195,definition,(
% 0.35/0.43 spl5_13 <=> ! [X2 : $i] : (($true = ((sK1 @ (sK2 @ X2)))) | ($false = ((sK1 @ X2))))),
% 0.35/0.43 introduced(definition,[new_symbols(definition,[spl5_13])],[avatar_definition])).
% 0.35/0.43 thf(f196,plain,(
% 0.35/0.43 ( ! [X2 : $i] : (($true = ((sK1 @ (sK2 @ X2)))) | ($false = ((sK1 @ X2)))) ) | ~spl5_13),
% 0.35/0.43 inference(avatar_component_clause,[],[f195])).
% 0.35/0.43 thf(f197,plain,(
% 0.35/0.43 spl5_13 | spl5_11),
% 0.35/0.43 inference(avatar_split_clause,[],[f36,f188,f195])).
% 0.35/0.43 thf(f199,plain,(
% 0.35/0.43 (sK1 != sK1) | (~spl5_2 | ~spl5_11)),
% 0.35/0.43 inference(constrained_superposition,[],[f189,f60])).
% 0.35/0.43 thf(f200,plain,(
% 0.35/0.43 $false | (~spl5_2 | ~spl5_11)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f199])).
% 0.35/0.43 thf(f201,plain,(
% 0.35/0.43 ~spl5_2 | ~spl5_11),
% 0.35/0.43 inference(avatar_contradiction_clause,[],[f200])).
% 0.35/0.43 thf(f214,plain,(
% 0.35/0.43 ( ! [X0 : $i] : (($true = $false) | (sK3 = ((sK2 @ X0))) | ($false = ((sK1 @ X0)))) ) | (~spl5_2 | ~spl5_13)),
% 0.35/0.43 inference(constrained_superposition,[],[f123,f196])).
% 0.35/0.43 thf(f215,plain,(
% 0.35/0.43 ( ! [X0 : $i] : (($false = ((sK1 @ X0))) | (sK3 = ((sK2 @ X0)))) ) | (~spl5_2 | ~spl5_13)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f214])).
% 0.35/0.43 thf(f223,plain,(
% 0.35/0.43 ($true = $false) | (sK3 = ((sK2 @ sK3))) | (~spl5_2 | ~spl5_13)),
% 0.35/0.43 inference(constrained_superposition,[],[f160,f215])).
% 0.35/0.43 thf(f225,plain,(
% 0.35/0.43 (sK3 = ((sK2 @ sK3))) | (~spl5_2 | ~spl5_13)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f223])).
% 0.35/0.43 thf(f238,plain,(
% 0.35/0.43 (sK3 != sK3) | ($false = ((sK1 @ sK3))) | (~spl5_2 | ~spl5_10 | ~spl5_13)),
% 0.35/0.43 inference(constrained_superposition,[],[f186,f225])).
% 0.35/0.43 thf(f239,plain,(
% 0.35/0.43 ($false = ((sK1 @ sK3))) | (~spl5_2 | ~spl5_10 | ~spl5_13)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f238])).
% 0.35/0.43 thf(f240,plain,(
% 0.35/0.43 ($true = $false) | (~spl5_2 | ~spl5_10 | ~spl5_13)),
% 0.35/0.43 inference(constrained_superposition,[],[f239,f160])).
% 0.35/0.43 thf(f244,plain,(
% 0.35/0.43 $false | (~spl5_2 | ~spl5_10 | ~spl5_13)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f240])).
% 0.35/0.43 thf(f245,plain,(
% 0.35/0.43 ~spl5_2 | ~spl5_10 | ~spl5_13),
% 0.35/0.43 inference(avatar_contradiction_clause,[],[f244])).
% 0.35/0.43 thf(f252,plain,(
% 0.35/0.43 ( ! [X0 : $i] : (($true = $false) | ($false = ((sK1 @ X0))) | (sK4 = ((sK2 @ X0)))) ) | (~spl5_5 | ~spl5_13)),
% 0.35/0.43 inference(constrained_superposition,[],[f196,f70])).
% 0.35/0.43 thf(f253,plain,(
% 0.35/0.43 ( ! [X0 : $i] : (($false = ((sK1 @ X0))) | (sK4 = ((sK2 @ X0)))) ) | (~spl5_5 | ~spl5_13)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f252])).
% 0.35/0.43 thf(f278,plain,(
% 0.35/0.43 ($true = $false) | (sK4 = ((sK2 @ sK4))) | (~spl5_1 | ~spl5_5 | ~spl5_13)),
% 0.35/0.43 inference(constrained_superposition,[],[f56,f253])).
% 0.35/0.43 thf(f281,plain,(
% 0.35/0.43 (sK4 = ((sK2 @ sK4))) | (~spl5_1 | ~spl5_5 | ~spl5_13)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f278])).
% 0.35/0.43 thf(f292,plain,(
% 0.35/0.43 (sK4 != sK4) | ($false = ((sK1 @ sK4))) | (~spl5_1 | ~spl5_5 | ~spl5_10 | ~spl5_13)),
% 0.35/0.43 inference(constrained_superposition,[],[f186,f281])).
% 0.35/0.43 thf(f294,plain,(
% 0.35/0.43 ($false = ((sK1 @ sK4))) | (~spl5_1 | ~spl5_5 | ~spl5_10 | ~spl5_13)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f292])).
% 0.35/0.43 thf(f295,plain,(
% 0.35/0.43 ($true = $false) | (~spl5_1 | ~spl5_5 | ~spl5_10 | ~spl5_13)),
% 0.35/0.43 inference(constrained_superposition,[],[f294,f56])).
% 0.35/0.43 thf(f299,plain,(
% 0.35/0.43 $false | (~spl5_1 | ~spl5_5 | ~spl5_10 | ~spl5_13)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f295])).
% 0.35/0.43 thf(f300,plain,(
% 0.35/0.43 ~spl5_1 | ~spl5_5 | ~spl5_10 | ~spl5_13),
% 0.35/0.43 inference(avatar_contradiction_clause,[],[f299])).
% 0.35/0.43 thf(f301,plain,(
% 0.35/0.43 ( ! [X1 : $i] : ((((sK1 @ (sK9 @ X1))) != ((X1 = (sK9 @ X1))))) ) | ~spl5_11),
% 0.35/0.43 inference(negative_extensionality,[],[f189])).
% 0.35/0.43 thf(f302,plain,(
% 0.35/0.43 ( ! [X1 : $i] : (($true = ((sK1 @ (sK9 @ X1)))) | ($true = ((X1 = (sK9 @ X1))))) ) | ~spl5_11),
% 0.35/0.43 inference(xor_proxy_clausification,[],[f301])).
% 0.35/0.43 thf(f303,plain,(
% 0.35/0.43 ( ! [X1 : $i] : (($false = ((sK1 @ (sK9 @ X1)))) | ($false = ((X1 = (sK9 @ X1))))) ) | ~spl5_11),
% 0.35/0.43 inference(xor_proxy_clausification,[],[f301])).
% 0.35/0.43 thf(f304,plain,(
% 0.35/0.43 ( ! [X1 : $i] : ((((sK9 @ X1)) != X1) | ($false = ((sK1 @ (sK9 @ X1))))) ) | ~spl5_11),
% 0.35/0.43 inference(equality_proxy_clausification,[],[f303])).
% 0.35/0.43 thf(f305,plain,(
% 0.35/0.43 ( ! [X1 : $i] : (($true = ((sK1 @ (sK9 @ X1)))) | (((sK9 @ X1)) = X1)) ) | ~spl5_11),
% 0.35/0.43 inference(equality_proxy_clausification,[],[f302])).
% 0.35/0.43 thf(f329,plain,(
% 0.35/0.43 ( ! [X0 : $i] : (($true = $false) | (sK4 = ((sK9 @ X0))) | (((sK9 @ X0)) = X0)) ) | (~spl5_5 | ~spl5_11)),
% 0.35/0.43 inference(constrained_superposition,[],[f70,f305])).
% 0.35/0.43 thf(f330,plain,(
% 0.35/0.43 ( ! [X0 : $i] : ((sK4 = ((sK9 @ X0))) | (((sK9 @ X0)) = X0)) ) | (~spl5_5 | ~spl5_11)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f329])).
% 0.35/0.43 thf(f352,plain,(
% 0.35/0.43 ( ! [X0 : $i] : ((sK4 != X0) | (((sK9 @ X0)) = X0)) ) | (~spl5_5 | ~spl5_11)),
% 0.35/0.43 inference(equality_factoring,[],[f330])).
% 0.35/0.43 thf(f367,plain,(
% 0.35/0.43 (sK4 = ((sK9 @ sK4))) | (~spl5_5 | ~spl5_11)),
% 0.35/0.43 inference(equality_resolution,[],[f352])).
% 0.35/0.43 thf(f370,plain,(
% 0.35/0.43 (sK4 != sK4) | ($false = ((sK1 @ sK4))) | (~spl5_5 | ~spl5_11)),
% 0.35/0.43 inference(constrained_superposition,[],[f304,f367])).
% 0.35/0.43 thf(f371,plain,(
% 0.35/0.43 ($false = ((sK1 @ sK4))) | (~spl5_5 | ~spl5_11)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f370])).
% 0.35/0.43 thf(f372,plain,(
% 0.35/0.43 ($true = $false) | (~spl5_1 | ~spl5_5 | ~spl5_11)),
% 0.35/0.43 inference(constrained_superposition,[],[f371,f56])).
% 0.35/0.43 thf(f376,plain,(
% 0.35/0.43 $false | (~spl5_1 | ~spl5_5 | ~spl5_11)),
% 0.35/0.43 inference(trivial_inequality_removal,[],[f372])).
% 0.35/0.43 thf(f377,plain,(
% 0.35/0.43 ~spl5_1 | ~spl5_5 | ~spl5_11),
% 0.35/0.43 inference(avatar_contradiction_clause,[],[f376])).
% 0.35/0.43 cnf(s12, plain, spl5_1 | spl5_2, inference(sat_conversion,[],[f61])).
% 0.35/0.43 cnf(s16, plain, spl5_2 | spl5_5, inference(sat_conversion,[],[f71])).
% 0.35/0.43 cnf(s97, plain, spl5_10 | spl5_11, inference(sat_conversion,[],[f190])).
% 0.35/0.43 cnf(s102, plain, spl5_11 | spl5_13, inference(sat_conversion,[],[f197])).
% 0.35/0.43 cnf(s106, plain, ~spl5_2 | ~spl5_11, inference(sat_conversion,[],[f201])).
% 0.35/0.43 cnf(s141, plain, ~spl5_2 | ~spl5_10 | ~spl5_13, inference(sat_conversion,[],[f245])).
% 0.35/0.43 cnf(s181, plain, ~spl5_1 | ~spl5_5 | ~spl5_10 | ~spl5_13, inference(sat_conversion,[],[f300])).
% 0.35/0.43 cnf(s234, plain, ~spl5_1 | ~spl5_5 | ~spl5_11, inference(sat_conversion,[],[f377])).
% 0.35/0.43 cnf(s235, plain, ~spl5_2, inference(rat,[],[s141,s97,s102,s106])).
% 0.35/0.43 cnf(s236, plain, spl5_5, inference(rat,[],[s16,s235])).
% 0.35/0.43 cnf(s237, plain, spl5_1, inference(rat,[],[s12,s235])).
% 0.35/0.43 cnf(s239, plain, ~spl5_11, inference(rat,[],[s234,s236,s237])).
% 0.35/0.43 cnf(s241, plain, spl5_13, inference(rat,[],[s102,s239])).
% 0.35/0.43 cnf(s242, plain, spl5_10, inference(rat,[],[s97,s239])).
% 0.35/0.43 cnf(s243, plain, $false, inference(rat,[],[s181,s237,s236,s241,s242])).
% 0.35/0.43 thf(f378,plain,(
% 0.35/0.43 $false),
% 0.35/0.43 inference(avatar_sat_refutation,[],[s243])).
% 0.35/0.43 % SZS output end Proof for theBenchmark
% 0.35/0.43 % (3509979)------------------------------
% 0.35/0.43 % (3509979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.35/0.43 % (3509979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/0.43 % (3509979)CaDiCaL version: 2.1.3
% 0.35/0.43 % (3509979)Termination reason: Refutation
% 0.35/0.43 % (3509979)Time elapsed: 0.026 s
% 0.35/0.43 % (3509979)Peak memory usage: 13 MB
% 0.35/0.43 % (3509979)Instructions burned: 21 (million)
% 0.35/0.43 % (3509972)Success in time 0.08 s
% 0.35/0.43 % Vampire exiting
%------------------------------------------------------------------------------