%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV214^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:38:02 AM UTC 2026
% Result : Theorem 0.34s 0.43s
% Output : Refutation 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEV214^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.29 % Computer : n009.cluster.edu
% 0.11/0.29 % Model : x86_64 x86_64
% 0.11/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.29 % Memory : 8046.5625MB
% 0.11/0.29 % OS : Linux 6.8.0-71-generic
% 0.11/0.29 % CPULimit : 300
% 0.11/0.29 % WCLimit : 300
% 0.11/0.29 % DateTime : Tue Sep 29 15:22:00 UTC 2026
% 0.11/0.29 % CPUTime :
% 0.11/0.29 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.29/0.34 Running higher-order theorem proving
% 0.29/0.36 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/0.43 % (4130371)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.34/0.43 % (4130376)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1287909681:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.34/0.43 % (4130382)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.34/0.43 % (4130382)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.34/0.43 % (4130378)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3494985923:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.34/0.43 % (4130377)lrs+10_16_si=on:nwc=1.5:random_seed=1981845187:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.34/0.43 % (4130380)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2921496610:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.34/0.43 % (4130379)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=1044293908:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.34/0.43 % (4130382)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=2148883509:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.34/0.43 % (4130381)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3270328465:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.34/0.43 % (4130378)Instruction limit reached!
% 0.34/0.43 % (4130378)------------------------------
% 0.34/0.43 % (4130378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.34/0.43 % (4130378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.34/0.43 % (4130378)CaDiCaL version: 2.1.3
% 0.34/0.43 % (4130378)Termination reason: Instruction limit
% 0.34/0.43 % (4130378)Termination phase: Saturation
% 0.34/0.43 % (4130378)Time elapsed: 0.004 s
% 0.34/0.43 % (4130378)Peak memory usage: 12 MB
% 0.34/0.43 % (4130378)Instructions burned: 3 (million)
% 0.34/0.43 % (4130376) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4130371-4130376"...
% 0.34/0.43 % (4130381) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4130371-4130381"...
% 0.34/0.43 % (4130382) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4130371-4130382"...
% 0.34/0.43 % (4130376)...printing done.
% 0.34/0.43 % (4130376)Refutation found. Thanks to Tanya!
% 0.34/0.43 % SZS status Theorem for theBenchmark
% 0.34/0.43 % SZS output start Proof for theBenchmark
% 0.34/0.43 thf(type_def_5, type, iS: $tType).
% 0.34/0.43 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.34/0.43 thf(func_def_0, type, c0: iS).
% 0.34/0.43 thf(func_def_1, type, cP: (iS > iS > iS)).
% 0.34/0.43 thf(func_def_5, type, db1: !>[X0: $tType]:(X0)).
% 0.34/0.43 thf(func_def_6, type, db0: !>[X0: $tType]:(X0)).
% 0.34/0.43 thf(func_def_7, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.34/0.43 thf(func_def_8, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.34/0.43 thf(func_def_9, type, vOR: ($o > $o > $o)).
% 0.34/0.43 thf(func_def_10, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.34/0.43 thf(func_def_11, type, sK0: ((iS > $o) > iS)).
% 0.34/0.43 thf(func_def_12, type, sK1: ((iS > $o) > iS)).
% 0.34/0.43 thf(func_def_13, type, vNOT: ($o > $o)).
% 0.34/0.43 thf(func_def_15, type, sK3: iS).
% 0.34/0.43 thf(func_def_16, type, sK4: iS).
% 0.34/0.43 thf(func_def_17, type, sK5: (iS > iS)).
% 0.34/0.43 thf(func_def_18, type, sK6: iS).
% 0.34/0.43 thf(func_def_19, type, sK7: iS).
% 0.34/0.43 thf(f1,conjecture,(
% 0.34/0.43 (! [X4 : (iS > $o)] : ((! [X0 : iS,X1 : iS] : (((X4 @ X0) & (X4 @ X1)) => (X4 @ (cP @ X0 @ X1))) & (X4 @ c0)) => ! [X0 : iS] : (X4 @ X0)) & ! [X0 : iS,X1 : iS] : (((cP @ X0 @ X1)) != c0) & ! [X1 : iS,X0 : iS,X2 : iS,X3 : iS] : ((((cP @ X0 @ X2)) = ((cP @ X1 @ X3))) => ((X0 = X1) & (X2 = X3)))) => (((^[X0 : iS] : (? [X1 : iS] : (c0 = ((cP @ X0 @ X1))) | (X0 = c0))) = (((^[X0 : iS, X1 : iS] : ((X0 = X1))) @ c0))) & ((((^[X0 : iS, X1 : iS] : ((X0 = X1))) @ c0)) = (^[X1 : iS] : (? [X0 : iS] : (c0 = ((cP @ X0 @ X1))) | (X1 = c0)))))),
% 0.34/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cS_T_LR_LEM2_pme)).
% 0.34/0.43 thf(f2,negated_conjecture,(
% 0.34/0.43 ~((! [X4 : (iS > $o)] : ((! [X0 : iS,X1 : iS] : (((X4 @ X0) & (X4 @ X1)) => (X4 @ (cP @ X0 @ X1))) & (X4 @ c0)) => ! [X0 : iS] : (X4 @ X0)) & ! [X0 : iS,X1 : iS] : (((cP @ X0 @ X1)) != c0) & ! [X1 : iS,X0 : iS,X2 : iS,X3 : iS] : ((((cP @ X0 @ X2)) = ((cP @ X1 @ X3))) => ((X0 = X1) & (X2 = X3)))) => (((^[X0 : iS] : (? [X1 : iS] : (c0 = ((cP @ X0 @ X1))) | (X0 = c0))) = (((^[X0 : iS, X1 : iS] : ((X0 = X1))) @ c0))) & ((((^[X0 : iS, X1 : iS] : ((X0 = X1))) @ c0)) = (^[X1 : iS] : (? [X0 : iS] : (c0 = ((cP @ X0 @ X1))) | (X1 = c0))))))),
% 0.34/0.43 inference(negated_conjecture,[status(cth)],[f1])).
% 0.34/0.43 thf(f3,plain,(
% 0.34/0.43 ~((! [X0 : (iS > $o)] : ((! [X1 : iS,X2 : iS] : (((X0 @ X1) & (X0 @ X2)) => (X0 @ (cP @ X1 @ X2))) & (X0 @ c0)) => ! [X3 : iS] : (X0 @ X3)) & ! [X4 : iS,X5 : iS] : (c0 != ((cP @ X4 @ X5))) & ! [X6 : iS,X7 : iS,X8 : iS,X9 : iS] : ((((cP @ X7 @ X8)) = ((cP @ X6 @ X9))) => ((X6 = X7) & (X8 = X9)))) => (((^[X10 : iS] : (? [X11 : iS] : (c0 = ((cP @ X10 @ X11))) | (c0 = X10))) = (((^[X12 : iS, X13 : iS] : ((X12 = X13))) @ c0))) & ((((^[X14 : iS, X15 : iS] : ((X14 = X15))) @ c0)) = (^[X16 : iS] : (? [X17 : iS] : (c0 = ((cP @ X17 @ X16))) | (c0 = X16))))))),
% 0.34/0.43 inference(rectify,[],[f2])).
% 0.34/0.43 thf(f4,plain,(
% 0.34/0.43 ~((! [X0 : (iS > $o)] : (((((X0 @ c0)) = $true) & ! [X1 : iS,X2 : iS] : (((((X0 @ X2)) = $true) & (((X0 @ X1)) = $true)) => (((X0 @ (cP @ X1 @ X2))) = $true))) => ! [X3 : iS] : (((X0 @ X3)) = $true)) & ! [X5 : iS,X4 : iS] : (c0 != ((cP @ X4 @ X5))) & ! [X9 : iS,X8 : iS,X6 : iS,X7 : iS] : ((((cP @ X7 @ X8)) = ((cP @ X6 @ X9))) => ((X6 = X7) & (X8 = X9)))) => (((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) = (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0))) & ((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))) = (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0)))))),
% 0.34/0.43 inference(fool_elimination,[],[f3])).
% 0.34/0.43 thf(f5,plain,(
% 0.34/0.43 (((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) != (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0))) | ((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))) != (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0)))) & (! [X0 : (iS > $o)] : (! [X3 : iS] : (((X0 @ X3)) = $true) | ((((X0 @ c0)) != $true) | ? [X1 : iS,X2 : iS] : ((((X0 @ (cP @ X1 @ X2))) != $true) & ((((X0 @ X2)) = $true) & (((X0 @ X1)) = $true))))) & ! [X5 : iS,X4 : iS] : (c0 != ((cP @ X4 @ X5))) & ! [X7 : iS,X8 : iS,X6 : iS,X9 : iS] : ((((cP @ X7 @ X8)) != ((cP @ X6 @ X9))) | ((X6 = X7) & (X8 = X9))))),
% 0.34/0.43 inference(ennf_transformation,[],[f4])).
% 0.34/0.43 thf(f6,plain,(
% 0.34/0.43 ! [X5 : iS,X4 : iS] : (c0 != ((cP @ X4 @ X5))) & ! [X0 : (iS > $o)] : ((((X0 @ c0)) != $true) | ! [X3 : iS] : (((X0 @ X3)) = $true) | ? [X2 : iS,X1 : iS] : ((((X0 @ X2)) = $true) & (((X0 @ (cP @ X1 @ X2))) != $true) & (((X0 @ X1)) = $true))) & ! [X7 : iS,X8 : iS,X6 : iS,X9 : iS] : ((((cP @ X7 @ X8)) != ((cP @ X6 @ X9))) | ((X6 = X7) & (X8 = X9))) & (((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) != (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0))) | ((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))) != (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0))))),
% 0.34/0.43 inference(flattening,[],[f5])).
% 0.34/0.43 thf(f7,plain,(
% 0.34/0.43 ! [X0 : iS,X1 : iS] : (c0 != ((cP @ X1 @ X0))) & ! [X2 : (iS > $o)] : ((((X2 @ c0)) != $true) | ! [X3 : iS] : (((X2 @ X3)) = $true) | ? [X4 : iS,X5 : iS] : ((((X2 @ X4)) = $true) & (((X2 @ (cP @ X5 @ X4))) != $true) & (((X2 @ X5)) = $true))) & ! [X6 : iS,X7 : iS,X8 : iS,X9 : iS] : ((((cP @ X8 @ X9)) != ((cP @ X6 @ X7))) | ((X6 = X8) & (X7 = X9))) & (((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) != (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0))) | ((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))) != (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0))))),
% 0.34/0.43 inference(rectify,[],[f6])).
% 0.34/0.43 thf(f8,plain,(
% 0.34/0.43 ! [X0 : iS,X1 : iS] : (c0 != ((cP @ X1 @ X0))) & ! [X2 : (iS > $o)] : ((((X2 @ c0)) != $true) | ! [X3 : iS] : (((X2 @ X3)) = $true) | ((((X2 @ (sK0 @ X2))) = $true) & (((X2 @ (cP @ (sK1 @ X2) @ (sK0 @ X2)))) != $true) & (((X2 @ (sK1 @ X2))) = $true))) & ! [X6 : iS,X7 : iS,X8 : iS,X9 : iS] : ((((cP @ X8 @ X9)) != ((cP @ X6 @ X7))) | ((X6 = X8) & (X7 = X9))) & (((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) != (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0))) | ((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))) != (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0))))),
% 0.34/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X5,sK1 @ X2),skolemize(X5,sK1 @ X2)],[f7])).
% 0.34/0.43 thf(f9,plain,(
% 0.34/0.43 ((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) != (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0))) | ((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))) != (((^[Y0 : iS]: ((^[Y1 : iS]: (Y0 = Y1)))) @ c0)))),
% 0.34/0.43 inference(cnf_transformation,[],[f8])).
% 0.34/0.43 thf(f15,plain,(
% 0.34/0.43 ( ! [X0 : iS,X1 : iS] : ((c0 != ((cP @ X1 @ X0)))) )),
% 0.34/0.43 inference(cnf_transformation,[],[f8])).
% 0.34/0.43 thf(f18,plain,(
% 0.34/0.43 (((= @ c0)) != (^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0))))))) | ((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) != ((= @ c0)))),
% 0.34/0.43 inference(beta-eta_normalization,[],[f9])).
% 0.34/0.43 thf(f20,definition,(
% 0.34/0.43 spl2_1 <=> (((= @ c0)) = (^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))))),
% 0.34/0.43 introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition])).
% 0.34/0.43 thf(f22,plain,(
% 0.34/0.43 (((= @ c0)) != (^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0))))))) | spl2_1),
% 0.34/0.43 inference(avatar_component_clause,[],[f20])).
% 0.34/0.43 thf(f24,definition,(
% 0.34/0.43 spl2_2 <=> ((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) = ((= @ c0)))),
% 0.34/0.43 introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition])).
% 0.34/0.43 thf(f26,plain,(
% 0.34/0.43 ((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) != ((= @ c0))) | spl2_2),
% 0.34/0.43 inference(avatar_component_clause,[],[f24])).
% 0.34/0.43 thf(f27,plain,(
% 0.34/0.43 ~spl2_1 | ~spl2_2),
% 0.34/0.43 inference(avatar_split_clause,[],[f18,f24,f20])).
% 0.34/0.43 thf(f798,plain,(
% 0.34/0.43 (((c0 = sK3)) != (((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))) @ sK3))) | spl2_1),
% 0.34/0.43 inference(negative_extensionality,[],[f22])).
% 0.34/0.43 thf(f799,plain,(
% 0.34/0.43 (((c0 = sK3)) = $true) | ($true = (((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))) @ sK3))) | spl2_1),
% 0.34/0.43 inference(xor_proxy_clausification,[],[f798])).
% 0.34/0.43 thf(f800,plain,(
% 0.34/0.43 ($false = (((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))) @ sK3))) | ($false = ((c0 = sK3))) | spl2_1),
% 0.34/0.43 inference(xor_proxy_clausification,[],[f798])).
% 0.34/0.43 thf(f801,plain,(
% 0.34/0.43 ($false = (((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))) @ sK3))) | (c0 != sK3) | spl2_1),
% 0.34/0.43 inference(equality_proxy_clausification,[],[f800])).
% 0.34/0.43 thf(f802,plain,(
% 0.34/0.43 (c0 != sK3) | ((((c0 = sK3) | (?? @ iS @ (^[Y0 : iS]: (c0 = (cP @ Y0 @ sK3)))))) = $false) | spl2_1),
% 0.34/0.43 inference(beta-eta_normalization,[],[f801])).
% 0.34/0.43 thf(f804,plain,(
% 0.34/0.43 ($false = ((c0 = sK3))) | (c0 != sK3) | spl2_1),
% 0.34/0.43 inference(or_proxy_clausification,[],[f802])).
% 0.34/0.43 thf(f805,plain,(
% 0.34/0.43 (c0 != sK3) | (c0 != sK3) | spl2_1),
% 0.34/0.43 inference(equality_proxy_clausification,[],[f804])).
% 0.34/0.43 thf(f806,plain,(
% 0.34/0.43 (c0 != sK3) | spl2_1),
% 0.34/0.43 inference(duplicate_literal_removal,[],[f805])).
% 0.34/0.43 thf(f810,plain,(
% 0.34/0.43 ($true = (((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y1 @ Y0)))))) @ sK3))) | (c0 = sK3) | spl2_1),
% 0.34/0.43 inference(equality_proxy_clausification,[],[f799])).
% 0.34/0.43 thf(f811,plain,(
% 0.34/0.43 ((((c0 = sK3) | (?? @ iS @ (^[Y0 : iS]: (c0 = (cP @ Y0 @ sK3)))))) = $true) | (c0 = sK3) | spl2_1),
% 0.34/0.43 inference(beta-eta_normalization,[],[f810])).
% 0.34/0.43 thf(f812,plain,(
% 0.34/0.43 (((c0 = sK3)) = $true) | (((?? @ iS @ (^[Y0 : iS]: (c0 = (cP @ Y0 @ sK3))))) = $true) | (c0 = sK3) | spl2_1),
% 0.34/0.43 inference(or_proxy_clausification,[],[f811])).
% 0.34/0.43 thf(f813,plain,(
% 0.34/0.43 (((?? @ iS @ (^[Y0 : iS]: (c0 = (cP @ Y0 @ sK3))))) = $true) | (c0 = sK3) | (c0 = sK3) | spl2_1),
% 0.34/0.43 inference(equality_proxy_clausification,[],[f812])).
% 0.34/0.43 thf(f814,plain,(
% 0.34/0.43 (c0 = sK3) | ((((^[Y0 : iS]: (c0 = (cP @ Y0 @ sK3))) @ sK4)) = $true) | (c0 = sK3) | spl2_1),
% 0.34/0.43 inference(sigma_proxy_clausification,[],[f813])).
% 0.34/0.43 thf(f815,plain,(
% 0.34/0.43 (c0 = sK3) | ((((^[Y0 : iS]: (c0 = (cP @ Y0 @ sK3))) @ sK4)) = $true) | spl2_1),
% 0.34/0.43 inference(duplicate_literal_removal,[],[f814])).
% 0.34/0.43 thf(f816,plain,(
% 0.34/0.43 ($true = ((c0 = (cP @ sK4 @ sK3)))) | (c0 = sK3) | spl2_1),
% 0.34/0.43 inference(beta-eta_normalization,[],[f815])).
% 0.34/0.43 thf(f817,plain,(
% 0.34/0.43 (c0 = ((cP @ sK4 @ sK3))) | (c0 = sK3) | spl2_1),
% 0.34/0.43 inference(equality_proxy_clausification,[],[f816])).
% 0.34/0.43 thf(f818,plain,(
% 0.34/0.43 (c0 = sK3) | spl2_1),
% 0.34/0.43 inference(forward_subsumption_resolution,[],[f817,f15])).
% 0.34/0.43 thf(f819,plain,(
% 0.34/0.43 $false | spl2_1),
% 0.34/0.43 inference(forward_subsumption_resolution,[],[f818,f806])).
% 0.34/0.43 thf(f820,plain,(
% 0.34/0.43 spl2_1),
% 0.34/0.43 inference(avatar_contradiction_clause,[],[f819])).
% 0.34/0.43 thf(f1147,plain,(
% 0.34/0.43 ((((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) @ sK6)) != ((c0 = sK6))) | spl2_2),
% 0.34/0.43 inference(negative_extensionality,[],[f26])).
% 0.34/0.43 thf(f1148,plain,(
% 0.34/0.43 ((((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) @ sK6)) = $true) | (((c0 = sK6)) = $true) | spl2_2),
% 0.34/0.43 inference(xor_proxy_clausification,[],[f1147])).
% 0.34/0.43 thf(f1149,plain,(
% 0.34/0.43 ($false = ((c0 = sK6))) | ((((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) @ sK6)) = $false) | spl2_2),
% 0.34/0.43 inference(xor_proxy_clausification,[],[f1147])).
% 0.34/0.43 thf(f1150,plain,(
% 0.34/0.43 ((((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) @ sK6)) = $false) | (c0 != sK6) | spl2_2),
% 0.34/0.43 inference(equality_proxy_clausification,[],[f1149])).
% 0.34/0.43 thf(f1151,plain,(
% 0.34/0.43 (c0 != sK6) | ($false = (((c0 = sK6) | (?? @ iS @ (^[Y0 : iS]: (c0 = (cP @ sK6 @ Y0))))))) | spl2_2),
% 0.34/0.43 inference(beta-eta_normalization,[],[f1150])).
% 0.34/0.43 thf(f1153,plain,(
% 0.34/0.43 (c0 != sK6) | ($false = ((c0 = sK6))) | spl2_2),
% 0.34/0.43 inference(or_proxy_clausification,[],[f1151])).
% 0.34/0.43 thf(f1154,plain,(
% 0.34/0.43 (c0 != sK6) | (c0 != sK6) | spl2_2),
% 0.34/0.43 inference(equality_proxy_clausification,[],[f1153])).
% 0.34/0.43 thf(f1155,plain,(
% 0.34/0.43 (c0 != sK6) | spl2_2),
% 0.34/0.43 inference(duplicate_literal_removal,[],[f1154])).
% 0.34/0.43 thf(f1159,plain,(
% 0.34/0.43 (c0 = sK6) | ((((^[Y0 : iS]: ((c0 = Y0) | (?? @ iS @ (^[Y1 : iS]: (c0 = (cP @ Y0 @ Y1)))))) @ sK6)) = $true) | spl2_2),
% 0.34/0.43 inference(equality_proxy_clausification,[],[f1148])).
% 0.34/0.43 thf(f1160,plain,(
% 0.34/0.43 (c0 = sK6) | ((((c0 = sK6) | (?? @ iS @ (^[Y0 : iS]: (c0 = (cP @ sK6 @ Y0)))))) = $true) | spl2_2),
% 0.34/0.43 inference(beta-eta_normalization,[],[f1159])).
% 0.34/0.43 thf(f1161,plain,(
% 0.34/0.43 (c0 = sK6) | (((?? @ iS @ (^[Y0 : iS]: (c0 = (cP @ sK6 @ Y0))))) = $true) | (((c0 = sK6)) = $true) | spl2_2),
% 0.34/0.43 inference(or_proxy_clausification,[],[f1160])).
% 0.34/0.43 thf(f1162,plain,(
% 0.34/0.43 ((((^[Y0 : iS]: (c0 = (cP @ sK6 @ Y0))) @ sK7)) = $true) | (((c0 = sK6)) = $true) | (c0 = sK6) | spl2_2),
% 0.34/0.43 inference(sigma_proxy_clausification,[],[f1161])).
% 0.34/0.43 thf(f1163,plain,(
% 0.34/0.43 (c0 = sK6) | (c0 = sK6) | ((((^[Y0 : iS]: (c0 = (cP @ sK6 @ Y0))) @ sK7)) = $true) | spl2_2),
% 0.34/0.43 inference(equality_proxy_clausification,[],[f1162])).
% 0.34/0.43 thf(f1164,plain,(
% 0.34/0.43 ((((^[Y0 : iS]: (c0 = (cP @ sK6 @ Y0))) @ sK7)) = $true) | (c0 = sK6) | spl2_2),
% 0.34/0.43 inference(duplicate_literal_removal,[],[f1163])).
% 0.34/0.43 thf(f1165,plain,(
% 0.34/0.43 (c0 = sK6) | (((c0 = (cP @ sK6 @ sK7))) = $true) | spl2_2),
% 0.34/0.43 inference(beta-eta_normalization,[],[f1164])).
% 0.34/0.43 thf(f1166,plain,(
% 0.34/0.43 (c0 = ((cP @ sK6 @ sK7))) | (c0 = sK6) | spl2_2),
% 0.34/0.43 inference(equality_proxy_clausification,[],[f1165])).
% 0.34/0.43 thf(f1167,plain,(
% 0.34/0.43 (c0 = sK6) | spl2_2),
% 0.34/0.43 inference(forward_subsumption_resolution,[],[f1166,f15])).
% 0.34/0.43 thf(f1168,plain,(
% 0.34/0.43 $false | spl2_2),
% 0.34/0.43 inference(forward_subsumption_resolution,[],[f1167,f1155])).
% 0.34/0.43 thf(f1169,plain,(
% 0.34/0.43 spl2_2),
% 0.34/0.43 inference(avatar_contradiction_clause,[],[f1168])).
% 0.34/0.43 cnf(s1, plain, ~spl2_1 | ~spl2_2, inference(sat_conversion,[],[f27])).
% 0.34/0.43 cnf(s7, plain, spl2_1, inference(sat_conversion,[],[f820])).
% 0.34/0.43 cnf(s8, plain, spl2_2, inference(sat_conversion,[],[f1169])).
% 0.34/0.43 cnf(s13, plain, $false, inference(rat,[],[s1,s8,s7])).
% 0.34/0.43 thf(f1170,plain,(
% 0.34/0.43 $false),
% 0.34/0.43 inference(avatar_sat_refutation,[],[s13])).
% 0.34/0.43 % SZS output end Proof for theBenchmark
% 0.34/0.43 % (4130376)------------------------------
% 0.34/0.43 % (4130376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.34/0.43 % (4130376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.34/0.43 % (4130376)CaDiCaL version: 2.1.3
% 0.34/0.43 % (4130376)Termination reason: Refutation
% 0.34/0.43 % (4130376)Time elapsed: 0.024 s
% 0.34/0.43 % (4130376)Peak memory usage: 13 MB
% 0.34/0.43 % (4130376)Instructions burned: 47 (million)
% 0.34/0.43 % (4130371)Success in time 0.056 s
% 0.34/0.43 % Vampire exiting
%------------------------------------------------------------------------------