%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO546^1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:48:23 AM UTC 2026
% Result : Theorem 0.20s 0.30s
% Output : Refutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO546^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n010.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 17:14:33 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.08/0.24 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.20/0.30 % (3155792)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.20/0.30 % (3155803)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.20/0.30 % (3155803)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.20/0.30 % (3155801)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1600565212:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.20/0.30 % (3155800)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=795765858: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.20/0.30 % (3155797)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2904730786:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.20/0.30 % (3155799)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2512065766:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.20/0.30 % (3155798)lrs+10_16_si=on:nwc=1.5:random_seed=1730117640:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.20/0.30 % (3155802)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3134527878:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.20/0.30 % (3155803)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=2794901836:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.20/0.30 % (3155799)Refutation not found, incomplete strategy
% 0.20/0.30 % (3155799)------------------------------
% 0.20/0.30 % (3155799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.30 % (3155799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.30 % (3155799)CaDiCaL version: 2.1.3
% 0.20/0.30 % (3155799)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.30 % (3155799)Time elapsed: 0.002 s
% 0.20/0.30 % (3155799)Peak memory usage: 12 MB
% 0.20/0.30 % (3155799)Instructions burned: 2 (million)
% 0.20/0.30 % (3155799)------------------------------
% 0.20/0.30 % (3155799)------------------------------
% 0.20/0.30 % (3155797)Refutation not found, incomplete strategy
% 0.20/0.30 % (3155797)------------------------------
% 0.20/0.30 % (3155797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.30 % (3155797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.30 % (3155797)CaDiCaL version: 2.1.3
% 0.20/0.30 % (3155797)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.30 % (3155797)Time elapsed: 0.003 s
% 0.20/0.30 % (3155797)Peak memory usage: 12 MB
% 0.20/0.30 % (3155797)Instructions burned: 4 (million)
% 0.20/0.30 % (3155797)------------------------------
% 0.20/0.30 % (3155797)------------------------------
% 0.20/0.30 % (3155803) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3155792-3155803"...
% 0.20/0.30 % (3155798)Instruction limit reached!
% 0.20/0.30 % (3155798)------------------------------
% 0.20/0.30 % (3155798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.30 % (3155798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.30 % (3155798)CaDiCaL version: 2.1.3
% 0.20/0.30 % (3155798)Termination reason: Instruction limit
% 0.20/0.30 % (3155798)Termination phase: Saturation
% 0.20/0.30 % (3155798)Time elapsed: 0.011 s
% 0.20/0.30 % (3155798)Peak memory usage: 12 MB
% 0.20/0.30 % (3155798)Instructions burned: 19 (million)
% 0.20/0.30 % (3155801)Instruction limit reached!
% 0.20/0.30 % (3155801)------------------------------
% 0.20/0.30 % (3155801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.30 % (3155801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.30 % (3155801)CaDiCaL version: 2.1.3
% 0.20/0.30 % (3155801)Termination reason: Instruction limit
% 0.20/0.30 % (3155801)Termination phase: Saturation
% 0.20/0.30 % (3155801)Time elapsed: 0.014 s
% 0.20/0.30 % (3155801)Peak memory usage: 11 MB
% 0.20/0.30 % (3155801)Instructions burned: 25 (million)
% 0.20/0.30 % (3155803)...printing done.
% 0.20/0.30 % (3155803)Refutation found. Thanks to Tanya!
% 0.20/0.30 % SZS status Theorem for theBenchmark
% 0.20/0.30 % SZS output start Proof for theBenchmark
% 0.20/0.30 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.20/0.30 thf(func_def_0, type, eps: (($i > $o) > $i)).
% 0.20/0.30 thf(func_def_2, type, case: (($o > $o) > $i > $i > $i > $i > $i)).
% 0.20/0.30 thf(func_def_3, type, vNOT: ($o > $o)).
% 0.20/0.30 thf(func_def_4, type, f: ($o > $o)).
% 0.20/0.30 thf(func_def_7, type, vOR: ($o > $o > $o)).
% 0.20/0.30 thf(func_def_8, type, vAND: ($o > $o > $o)).
% 0.20/0.30 thf(func_def_9, type, db1: !>[X0: $tType]:(X0)).
% 0.20/0.30 thf(func_def_10, type, db0: !>[X0: $tType]:(X0)).
% 0.20/0.30 thf(func_def_11, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.20/0.30 thf(func_def_12, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.20/0.30 thf(func_def_13, type, db5: !>[X0: $tType]:(X0)).
% 0.20/0.30 thf(func_def_14, type, db3: !>[X0: $tType]:(X0)).
% 0.20/0.30 thf(func_def_15, type, db2: !>[X0: $tType]:(X0)).
% 0.20/0.30 thf(func_def_16, type, db4: !>[X0: $tType]:(X0)).
% 0.20/0.30 thf(func_def_20, type, sK3: $o).
% 0.20/0.30 thf(func_def_21, type, sK4: $o).
% 0.20/0.30 thf(func_def_22, type, sK5: $o).
% 0.20/0.30 thf(func_def_23, type, sK6: $o).
% 0.20/0.30 thf(func_def_24, type, sK7: $o).
% 0.20/0.30 thf(f1,axiom,(
% 0.20/0.30 ! [X0 : ($i > $o)] : (? [X1 : $i] : (X0 @ X1) => (X0 @ (eps @ X0)))),
% 0.20/0.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',choiceax)).
% 0.20/0.30 thf(f2,axiom,(
% 0.20/0.30 ((^[X0 : ($o > $o), X1 : $i, X2 : $i, X3 : $i, X4 : $i] : ((eps @ (^[X5 : $i] : (((X5 = X1) & ((^[X6 : $o] : ($false)) = X0)) | (((^[X6 : $o] : (X6)) = X0) & (X5 = X3)) | ((X5 = X2) & (X0 = ~)) | (((^[X6 : $o] : ($true)) = X0) & (X5 = X4))))))) = case)),
% 0.20/0.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',caseood)).
% 0.20/0.30 thf(f3,conjecture,(
% 0.20/0.30 ! [X0 : $i] : (((case @ f @ X0 @ X0 @ X0 @ X0)) = X0)),
% 0.20/0.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 0.20/0.30 thf(f4,negated_conjecture,(
% 0.20/0.30 ~ ! [X0 : $i] : (((case @ f @ X0 @ X0 @ X0 @ X0)) = X0)),
% 0.20/0.30 inference(negated_conjecture,[status(cth)],[f3])).
% 0.20/0.30 thf(f5,plain,(
% 0.20/0.30 ! [X0 : ($i > $o)] : (? [X1 : $i] : (X0 @ X1) => (X0 @ (eps @ X0)))),
% 0.20/0.30 inference(rectify,[],[f1])).
% 0.20/0.30 thf(f6,plain,(
% 0.20/0.30 ! [X0 : ($i > $o)] : (? [X1 : $i] : (((X0 @ X1)) = $true) => (((X0 @ (eps @ X0))) = $true))),
% 0.20/0.30 inference(fool_elimination,[],[f5])).
% 0.20/0.30 thf(f7,plain,(
% 0.20/0.30 ((^[X0 : ($o > $o), X1 : $i, X2 : $i, X3 : $i, X4 : $i] : ((eps @ (^[X5 : $i] : (((X5 = X1) & ((^[X6 : $o] : ($false)) = X0)) | (((^[X7 : $o] : (X7)) = X0) & (X5 = X3)) | ((X5 = X2) & (X0 = ~)) | (((^[X8 : $o] : ($true)) = X0) & (X5 = X4))))))) = case)),
% 0.20/0.30 inference(rectify,[],[f2])).
% 0.20/0.30 thf(f8,plain,(
% 0.20/0.30 (case = (^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y4 = Y5) & ((^[Y6 : $o]: ($true)) = Y0)) | ((~ = Y0) & (Y2 = Y5))) | ((Y3 = Y5) & ((^[Y6 : $o]: (Y6)) = Y0))) | (((^[Y6 : $o]: ($false)) = Y0) & (Y1 = Y5)))))))))))))))),
% 0.20/0.30 inference(fool_elimination,[],[f7])).
% 0.20/0.30 thf(f9,plain,(
% 0.20/0.30 ! [X0 : ($i > $o)] : ((((X0 @ (eps @ X0))) = $true) | ! [X1 : $i] : (((X0 @ X1)) != $true))),
% 0.20/0.30 inference(ennf_transformation,[],[f6])).
% 0.20/0.30 thf(f10,plain,(
% 0.20/0.30 ? [X0 : $i] : (((case @ f @ X0 @ X0 @ X0 @ X0)) != X0)),
% 0.20/0.30 inference(ennf_transformation,[],[f4])).
% 0.20/0.30 thf(f11,plain,(
% 0.20/0.30 (sK0 != ((case @ f @ sK0 @ sK0 @ sK0 @ sK0)))),
% 0.20/0.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f10])).
% 0.20/0.30 thf(f12,plain,(
% 0.20/0.30 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ (eps @ X0))) = $true) | (((X0 @ X1)) != $true)) )),
% 0.20/0.30 inference(cnf_transformation,[],[f9])).
% 0.20/0.30 thf(f13,plain,(
% 0.20/0.30 (case = (^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y4 = Y5) & ((^[Y6 : $o]: ($true)) = Y0)) | ((~ = Y0) & (Y2 = Y5))) | ((Y3 = Y5) & ((^[Y6 : $o]: (Y6)) = Y0))) | (((^[Y6 : $o]: ($false)) = Y0) & (Y1 = Y5)))))))))))))))),
% 0.20/0.30 inference(cnf_transformation,[],[f8])).
% 0.20/0.30 thf(f14,plain,(
% 0.20/0.30 (sK0 != ((case @ f @ sK0 @ sK0 @ sK0 @ sK0)))),
% 0.20/0.30 inference(cnf_transformation,[],[f11])).
% 0.20/0.30 thf(f16,definition,(
% 0.20/0.30 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.20/0.30 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.20/0.30 thf(f17,plain,(
% 0.20/0.30 (sK0 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y4 = Y5) & ((^[Y6 : $o]: ($true)) = Y0)) | ((~ = Y0) & (Y2 = Y5))) | ((Y3 = Y5) & ((^[Y6 : $o]: (Y6)) = Y0))) | (((^[Y6 : $o]: ($false)) = Y0) & (Y1 = Y5)))))))))))))) @ f @ sK0 @ sK0 @ sK0 @ sK0)))),
% 0.20/0.30 inference(definition_unfolding,[],[f14,f13])).
% 0.20/0.30 thf(f18,definition,(
% 0.20/0.30 (sF1 = (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y4 = Y5) & ((^[Y6 : $o]: ($true)) = Y0)) | ((~ = Y0) & (Y2 = Y5))) | ((Y3 = Y5) & ((^[Y6 : $o]: (Y6)) = Y0))) | (((^[Y6 : $o]: ($false)) = Y0) & (Y1 = Y5)))))))))))))) @ f @ sK0 @ sK0 @ sK0 @ sK0)))),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 0.20/0.30 thf(f19,plain,(
% 0.20/0.30 (sK0 != sF1)),
% 0.20/0.30 inference(definition_folding,[],[f17,f18])).
% 0.20/0.30 thf(f20,plain,(
% 0.20/0.30 (sF1 = ((eps @ (^[Y0 : $i]: (((((sK0 = Y0) & ((^[Y1 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = Y0))) | ((sK0 = Y0) & ((^[Y1 : $o]: (Y1)) = f))) | (((^[Y1 : $o]: ($false)) = f) & (sK0 = Y0)))))))),
% 0.20/0.30 inference(beta-eta_normalization,[],[f18])).
% 0.20/0.30 thf(f28,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true != (((^[Y0 : $i]: (((((sK0 = Y0) & ((^[Y1 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = Y0))) | ((sK0 = Y0) & ((^[Y1 : $o]: (Y1)) = f))) | (((^[Y1 : $o]: ($false)) = f) & (sK0 = Y0)))) @ X0))) | ($true = (((^[Y0 : $i]: (((((sK0 = Y0) & ((^[Y1 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = Y0))) | ((sK0 = Y0) & ((^[Y1 : $o]: (Y1)) = f))) | (((^[Y1 : $o]: ($false)) = f) & (sK0 = Y0)))) @ sF1)))) )),
% 0.20/0.30 inference(constrained_superposition,[],[f12,f20])).
% 0.20/0.30 thf(f29,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true != ((((((sK0 = X0) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = X0))) | ((sK0 = X0) & ((^[Y0 : $o]: (Y0)) = f))) | (((^[Y0 : $o]: ($false)) = f) & (sK0 = X0))))) | ($true = ((((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f))) | (((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))))) )),
% 0.20/0.30 inference(beta-eta_normalization,[],[f28])).
% 0.20/0.30 thf(f30,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($false = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = X0)))) | ($true = ((((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f))) | (((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f29])).
% 0.20/0.30 thf(f31,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = ((((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f))) | (((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1))))) | ($false = (((((sK0 = X0) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = X0))) | ((sK0 = X0) & ((^[Y0 : $o]: (Y0)) = f)))))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f29])).
% 0.20/0.30 thf(f32,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($false = (((((sK0 = X0) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = X0))) | ((sK0 = X0) & ((^[Y0 : $o]: (Y0)) = f))))) | ($true = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))) | ($true = (((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f)))))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f31])).
% 0.20/0.30 thf(f33,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($false = (((sK0 = X0) & ((^[Y0 : $o]: (Y0)) = f)))) | ($true = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))) | ($true = (((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f)))))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f32])).
% 0.20/0.30 thf(f34,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = (((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f))))) | ($true = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))) | ($false = ((((sK0 = X0) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = X0)))))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f32])).
% 0.20/0.30 thf(f35,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = (((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f)))) | ($true = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))) | (((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1)))) = $true) | ($false = ((((sK0 = X0) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = X0)))))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f34])).
% 0.20/0.30 thf(f36,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1)))) = $true) | ($false = ((((sK0 = X0) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = X0))))) | ($true = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))) | ($true = (((^[Y0 : $o]: (Y0)) = f)))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f35])).
% 0.20/0.30 thf(f132,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))) | ($true = (((~ = f) & (sK0 = sF1)))) | ($true = (((^[Y0 : $o]: (Y0)) = f))) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)))) | ($false = ((((sK0 = X0) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = X0)))))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f36])).
% 0.20/0.30 thf(f133,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = (((^[Y0 : $o]: (Y0)) = f))) | ($true = ((sK0 = sF1))) | ($true = (((~ = f) & (sK0 = sF1)))) | ($false = ((((sK0 = X0) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = X0))))) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f))))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f132])).
% 0.20/0.30 thf(f186,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((f = (^[Y0 : $o]: (Y0))) | ($false = ((((sK0 = X0) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = X0))))) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)))) | ($true = ((sK0 = sF1))) | ($true = (((~ = f) & (sK0 = sF1))))) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f133])).
% 0.20/0.30 thf(f187,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((f = (^[Y0 : $o]: (Y0))) | ($false = (((~ = f) & (sK0 = X0)))) | ($true = (((~ = f) & (sK0 = sF1)))) | ($true = ((sK0 = sF1))) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f))))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f186])).
% 0.20/0.30 thf(f188,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((f = (^[Y0 : $o]: (Y0))) | ($false = (((sK0 = X0) & ((^[Y0 : $o]: ($true)) = f)))) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)))) | ($true = (((~ = f) & (sK0 = sF1)))) | ($true = ((sK0 = sF1)))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f186])).
% 0.20/0.30 thf(f189,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)))) | ($false = ((sK0 = X0))) | ($true = ((sK0 = sF1))) | (f = (^[Y0 : $o]: (Y0))) | ($false = (((^[Y0 : $o]: ($true)) = f))) | ($true = (((~ = f) & (sK0 = sF1))))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f188])).
% 0.20/0.30 thf(f191,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($false = ((sK0 = X0))) | ($false = (((^[Y0 : $o]: ($true)) = f))) | ($true = ((sK0 = sF1))) | ($true = ((sK0 = sF1))) | (f = (^[Y0 : $o]: (Y0))) | ($true = (((~ = f) & (sK0 = sF1))))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f189])).
% 0.20/0.30 thf(f192,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 != X0) | ($true = ((sK0 = sF1))) | (f = (^[Y0 : $o]: (Y0))) | ($true = (((~ = f) & (sK0 = sF1)))) | ($false = (((^[Y0 : $o]: ($true)) = f))) | ($true = ((sK0 = sF1)))) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f191])).
% 0.20/0.30 thf(f193,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 != X0) | (sK0 = sF1) | ($false = (((^[Y0 : $o]: ($true)) = f))) | (sK0 = sF1) | ($true = (((~ = f) & (sK0 = sF1)))) | (f = (^[Y0 : $o]: (Y0)))) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f192])).
% 0.20/0.30 thf(f194,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: ($true))) | (sK0 = sF1) | ($true = (((~ = f) & (sK0 = sF1)))) | (f = (^[Y0 : $o]: (Y0))) | (sK0 = sF1)) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f193])).
% 0.20/0.30 thf(f195,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($true))) | ($true = ((sK0 = sF1))) | (f = (^[Y0 : $o]: (Y0)))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f194])).
% 0.20/0.30 thf(f199,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 = sF1) | (f != (^[Y0 : $o]: ($true))) | (sK0 = sF1) | (sK0 != X0) | (f = (^[Y0 : $o]: (Y0))) | (sK0 = sF1)) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f195])).
% 0.20/0.30 thf(f200,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((f = (^[Y0 : $o]: (Y0))) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($true)))) )),
% 0.20/0.30 inference(duplicate_literal_removal,[],[f199])).
% 0.20/0.30 thf(f211,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = ((sK0 = sF1))) | ($false = ((sK0 = X0))) | (f = (^[Y0 : $o]: (Y0))) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)))) | ($false = ((~ = f))) | ($true = (((~ = f) & (sK0 = sF1))))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f187])).
% 0.20/0.30 thf(f212,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)))) | ($false = ((~ = f))) | (f = (^[Y0 : $o]: (Y0))) | ($true = (((~ = f) & (sK0 = sF1)))) | (sK0 = sF1) | ($false = ((sK0 = X0)))) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f211])).
% 0.20/0.30 thf(f214,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = ((~ = f))) | ($true = ((sK0 = sF1))) | ($true = (((~ = f) & (sK0 = sF1)))) | (f = (^[Y0 : $o]: (Y0))) | ($false = ((sK0 = X0)))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f212])).
% 0.20/0.30 thf(f215,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((~ != f) | (f = (^[Y0 : $o]: (Y0))) | ($true = (((~ = f) & (sK0 = sF1)))) | ($true = ((sK0 = sF1))) | ($false = ((sK0 = X0))) | (sK0 = sF1)) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f214])).
% 0.20/0.30 thf(f216,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = ((sK0 = sF1))) | ($true = ((sK0 = sF1))) | (f = (^[Y0 : $o]: (Y0))) | ($false = ((sK0 = X0))) | (~ != f) | (sK0 = sF1)) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f215])).
% 0.20/0.30 thf(f222,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = ((sK0 = X0))) | (sK0 = sF1) | (sK0 = sF1) | (~ != f) | (f = (^[Y0 : $o]: (Y0)))) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f216])).
% 0.20/0.30 thf(f223,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 = sF1) | (f = (^[Y0 : $o]: (Y0))) | (~ != f) | (sK0 = sF1) | (sK0 = sF1) | (sK0 != X0)) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f222])).
% 0.20/0.30 thf(f224,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((~ != f) | (sK0 = sF1) | (f = (^[Y0 : $o]: (Y0))) | (sK0 != X0)) )),
% 0.20/0.30 inference(duplicate_literal_removal,[],[f223])).
% 0.20/0.30 thf(f233,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = (((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f))))) | ($false = (((^[Y0 : $o]: (Y0)) = f))) | ($true = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))) | ($false = ((sK0 = X0)))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f33])).
% 0.20/0.30 thf(f234,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = (((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f)))) | ($false = ((sK0 = X0))) | ($false = (((^[Y0 : $o]: (Y0)) = f))) | (((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1)))) = $true) | ($true = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1))))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f233])).
% 0.20/0.30 thf(f236,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1)))) = $true) | ($false = (((^[Y0 : $o]: (Y0)) = f))) | ($false = ((sK0 = X0))) | ($true = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))) | ($true = ((sK0 = sF1)))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f234])).
% 0.20/0.30 thf(f237,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))) | ($true = ((sK0 = sF1))) | ($false = ((sK0 = X0))) | ($false = (((^[Y0 : $o]: (Y0)) = f))) | ($true = (((~ = f) & (sK0 = sF1)))) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f))))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f236])).
% 0.20/0.30 thf(f238,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = (((~ = f) & (sK0 = sF1)))) | ($true = ((sK0 = sF1))) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)))) | ($true = ((sK0 = sF1))) | ($false = ((sK0 = X0))) | ($false = (((^[Y0 : $o]: (Y0)) = f)))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f237])).
% 0.20/0.30 thf(f264,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = ((sK0 = sF1))) | ($false = (((^[Y0 : $o]: (Y0)) = f))) | ($true = ((sK0 = sF1))) | ($false = ((sK0 = X0))) | ($true = ((sK0 = sF1))) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f))))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f238])).
% 0.20/0.30 thf(f277,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($false = ((sK0 = X0))) | (sK0 = sF1) | ($false = (((^[Y0 : $o]: (Y0)) = f))) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)))) | (sK0 = sF1) | (sK0 = sF1)) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f264])).
% 0.20/0.30 thf(f278,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = (((^[Y0 : $o]: (Y0)) = f))) | (sK0 = sF1) | (sK0 = sF1) | (sK0 != X0) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f))))) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f277])).
% 0.20/0.30 thf(f279,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 = sF1) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)))) | (f != (^[Y0 : $o]: (Y0))) | (sK0 = sF1) | (sK0 != X0) | (sK0 = sF1)) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f278])).
% 0.20/0.30 thf(f281,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: (Y0))) | (sK0 = sF1) | (sK0 = sF1) | ($true = ((sK0 = sF1))) | (sK0 = sF1)) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f279])).
% 0.20/0.30 thf(f282,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 = sF1) | (sK0 != X0) | (f != (^[Y0 : $o]: (Y0))) | (sK0 = sF1) | (sK0 = sF1)) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f281])).
% 0.20/0.30 thf(f283,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: (Y0))) | (sK0 = sF1)) )),
% 0.20/0.30 inference(duplicate_literal_removal,[],[f282])).
% 0.20/0.30 thf(f326,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($false = (((^[Y0 : $o]: ($false)) = f))) | ($true = ((((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f))) | (((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1))))) | ($false = ((sK0 = X0)))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f30])).
% 0.20/0.30 thf(f327,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = ((((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f))) | (((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1))))) | (f != (^[Y0 : $o]: ($false))) | ($false = ((sK0 = X0)))) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f326])).
% 0.20/0.30 thf(f328,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = ((((^[Y0 : $o]: ($false)) = f) & (sK0 = sF1)))) | ($false = ((sK0 = X0))) | ($true = (((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f))))) | (f != (^[Y0 : $o]: ($false)))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f327])).
% 0.20/0.30 thf(f329,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($false = ((sK0 = X0))) | ($true = ((sK0 = sF1))) | (f != (^[Y0 : $o]: ($false))) | ($true = (((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f)))))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f328])).
% 0.20/0.30 thf(f376,plain,(
% 0.20/0.30 ( ! [X0 : $i] : (($true = ((sK0 = sF1))) | (f != (^[Y0 : $o]: ($false))) | (sK0 != X0) | ($true = (((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f)))))) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f329])).
% 0.20/0.30 thf(f377,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: ($false))) | ($true = (((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1))) | ((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f))))) | (sK0 = sF1) | (sK0 != X0)) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f376])).
% 0.20/0.30 thf(f378,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 = sF1) | (f != (^[Y0 : $o]: ($false))) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: (Y0)) = f)))) | (((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1)))) = $true) | (sK0 != X0)) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f377])).
% 0.20/0.30 thf(f380,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((((((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)) | ((~ = f) & (sK0 = sF1)))) = $true) | (sK0 != X0) | (f != (^[Y0 : $o]: ($false))) | ($true = ((sK0 = sF1))) | (sK0 = sF1)) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f378])).
% 0.20/0.30 thf(f381,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: ($false))) | ($true = ((sK0 = sF1))) | (sK0 = sF1) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)))) | ($true = (((~ = f) & (sK0 = sF1))))) )),
% 0.20/0.30 inference(or_proxy_clausification,[],[f380])).
% 0.20/0.30 thf(f382,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 != X0) | ($true = (((~ = f) & (sK0 = sF1)))) | (f != (^[Y0 : $o]: ($false))) | (sK0 = sF1) | (sK0 = sF1) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f))))) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f381])).
% 0.20/0.30 thf(f383,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: ($false))) | (sK0 = sF1) | (sK0 = sF1) | ($true = (((sK0 = sF1) & ((^[Y0 : $o]: ($true)) = f)))) | ($true = ((sK0 = sF1))) | (sK0 != X0)) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f382])).
% 0.20/0.30 thf(f393,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: ($false))) | (sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | ($true = ((sK0 = sF1))) | ($true = ((sK0 = sF1)))) )),
% 0.20/0.30 inference(and_proxy_clausification,[],[f383])).
% 0.20/0.30 thf(f394,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: ($false))) | (sK0 = sF1) | (sK0 = sF1) | (sK0 = sF1) | (sK0 = sF1)) )),
% 0.20/0.30 inference(equality_proxy_clausification,[],[f393])).
% 0.20/0.30 thf(f395,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: ($false))) | (sK0 = sF1)) )),
% 0.20/0.30 inference(duplicate_literal_removal,[],[f394])).
% 0.20/0.30 thf(f429,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: ($true))) | (sK0 != X0) | (f = (^[Y0 : $o]: (Y0)))) )),
% 0.20/0.30 inference(forward_subsumption_resolution,[],[f200,f19])).
% 0.20/0.30 thf(f430,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((f = (^[Y0 : $o]: (Y0))) | (sK0 != X0) | (~ != f)) )),
% 0.20/0.30 inference(forward_subsumption_resolution,[],[f224,f19])).
% 0.20/0.30 thf(f438,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: (Y0))) | (sK0 != X0)) )),
% 0.20/0.30 inference(forward_subsumption_resolution,[],[f283,f19])).
% 0.20/0.30 thf(f442,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: ($false))) | (sK0 != X0)) )),
% 0.20/0.30 inference(forward_subsumption_resolution,[],[f395,f19])).
% 0.20/0.30 thf(f449,definition,(
% 0.20/0.30 spl2_1 <=> (~ = f)),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition])).
% 0.20/0.30 thf(f450,plain,(
% 0.20/0.30 (~ != f) | spl2_1),
% 0.20/0.30 inference(avatar_component_clause,[],[f449])).
% 0.20/0.30 thf(f453,definition,(
% 0.20/0.30 spl2_2 <=> (f = (^[Y0 : $o]: ($false)))),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition])).
% 0.20/0.30 thf(f454,plain,(
% 0.20/0.30 (f != (^[Y0 : $o]: ($false))) | spl2_2),
% 0.20/0.30 inference(avatar_component_clause,[],[f453])).
% 0.20/0.30 thf(f457,definition,(
% 0.20/0.30 spl2_3 <=> ! [X0 : $i] : (sK0 != X0)),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition])).
% 0.20/0.30 thf(f458,plain,(
% 0.20/0.30 ( ! [X0 : $i] : ((sK0 != X0)) ) | ~spl2_3),
% 0.20/0.30 inference(avatar_component_clause,[],[f457])).
% 0.20/0.30 thf(f460,definition,(
% 0.20/0.30 spl2_4 <=> (f = (^[Y0 : $o]: ($true)))),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition])).
% 0.20/0.30 thf(f462,plain,(
% 0.20/0.30 (f != (^[Y0 : $o]: ($true))) | spl2_4),
% 0.20/0.30 inference(avatar_component_clause,[],[f460])).
% 0.20/0.30 thf(f472,definition,(
% 0.20/0.30 spl2_5 <=> (f = (^[Y0 : $o]: (Y0)))),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition])).
% 0.20/0.30 thf(f473,plain,(
% 0.20/0.30 (f != (^[Y0 : $o]: (Y0))) | spl2_5),
% 0.20/0.30 inference(avatar_component_clause,[],[f472])).
% 0.20/0.30 thf(f480,plain,(
% 0.20/0.30 spl2_5 | ~spl2_4 | spl2_3),
% 0.20/0.30 inference(avatar_split_clause,[],[f429,f457,f460,f472])).
% 0.20/0.30 thf(f481,plain,(
% 0.20/0.30 spl2_3 | ~spl2_1 | spl2_5),
% 0.20/0.30 inference(avatar_split_clause,[],[f430,f472,f449,f457])).
% 0.20/0.30 thf(f489,plain,(
% 0.20/0.30 ~spl2_5 | spl2_3),
% 0.20/0.30 inference(avatar_split_clause,[],[f438,f457,f472])).
% 0.20/0.30 thf(f493,plain,(
% 0.20/0.30 spl2_3 | ~spl2_2),
% 0.20/0.30 inference(avatar_split_clause,[],[f442,f453,f457])).
% 0.20/0.30 thf(f522,plain,(
% 0.20/0.30 (sK0 != sK0) | ~spl2_3),
% 0.20/0.30 inference(imitation,[],[f458])).
% 0.20/0.30 thf(f525,plain,(
% 0.20/0.30 $false | ~spl2_3),
% 0.20/0.30 inference(trivial_inequality_removal,[],[f522])).
% 0.20/0.30 thf(f526,plain,(
% 0.20/0.30 ~spl2_3),
% 0.20/0.30 inference(avatar_contradiction_clause,[],[f525])).
% 0.20/0.30 thf(f527,plain,(
% 0.20/0.30 (((~ sK4)) != ((f @ sK4))) | spl2_1),
% 0.20/0.30 inference(negative_extensionality,[],[f450])).
% 0.20/0.30 thf(f528,plain,(
% 0.20/0.30 ($true = ((f @ sK4))) | ($true = ((~ sK4))) | spl2_1),
% 0.20/0.30 inference(xor_proxy_clausification,[],[f527])).
% 0.20/0.30 thf(f529,plain,(
% 0.20/0.30 ($false = ((f @ sK4))) | ($false = ((~ sK4))) | spl2_1),
% 0.20/0.30 inference(xor_proxy_clausification,[],[f527])).
% 0.20/0.30 thf(f530,plain,(
% 0.20/0.30 ($true = sK4) | ($false = ((f @ sK4))) | spl2_1),
% 0.20/0.30 inference(not_proxy_clausification,[],[f529])).
% 0.20/0.30 thf(f531,plain,(
% 0.20/0.30 ($false = sK4) | ($true = ((f @ sK4))) | spl2_1),
% 0.20/0.30 inference(not_proxy_clausification,[],[f528])).
% 0.20/0.30 thf(f533,definition,(
% 0.20/0.30 spl2_10 <=> ($false = ((f @ sK4)))),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition])).
% 0.20/0.30 thf(f534,plain,(
% 0.20/0.30 ($false != ((f @ sK4))) | spl2_10),
% 0.20/0.30 inference(avatar_component_clause,[],[f533])).
% 0.20/0.30 thf(f535,plain,(
% 0.20/0.30 ($false = ((f @ sK4))) | ~spl2_10),
% 0.20/0.30 inference(avatar_component_clause,[],[f533])).
% 0.20/0.30 thf(f537,definition,(
% 0.20/0.30 spl2_11 <=> ($true = sK4)),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition])).
% 0.20/0.30 thf(f539,plain,(
% 0.20/0.30 ($true = sK4) | ~spl2_11),
% 0.20/0.30 inference(avatar_component_clause,[],[f537])).
% 0.20/0.30 thf(f540,plain,(
% 0.20/0.30 spl2_10 | spl2_11 | spl2_1),
% 0.20/0.30 inference(avatar_split_clause,[],[f530,f449,f537,f533])).
% 0.20/0.30 thf(f542,definition,(
% 0.20/0.30 spl2_12 <=> ($true = ((f @ sK4)))),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition])).
% 0.20/0.30 thf(f543,plain,(
% 0.20/0.30 ($true != ((f @ sK4))) | spl2_12),
% 0.20/0.30 inference(avatar_component_clause,[],[f542])).
% 0.20/0.30 thf(f544,plain,(
% 0.20/0.30 ($true = ((f @ sK4))) | ~spl2_12),
% 0.20/0.30 inference(avatar_component_clause,[],[f542])).
% 0.20/0.30 thf(f546,definition,(
% 0.20/0.30 spl2_13 <=> ($false = sK4)),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_13])],[avatar_definition])).
% 0.20/0.30 thf(f548,plain,(
% 0.20/0.30 ($false = sK4) | ~spl2_13),
% 0.20/0.30 inference(avatar_component_clause,[],[f546])).
% 0.20/0.30 thf(f549,plain,(
% 0.20/0.30 spl2_12 | spl2_13 | spl2_1),
% 0.20/0.30 inference(avatar_split_clause,[],[f531,f449,f546,f542])).
% 0.20/0.30 thf(f554,definition,(
% 0.20/0.30 spl2_14 <=> ($false = ((f @ $true)))),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_14])],[avatar_definition])).
% 0.20/0.30 thf(f556,plain,(
% 0.20/0.30 ($false = ((f @ $true))) | ~spl2_14),
% 0.20/0.30 inference(avatar_component_clause,[],[f554])).
% 0.20/0.30 thf(f561,plain,(
% 0.20/0.30 (((f @ sK5)) != (((^[Y0 : $o]: ($false)) @ sK5))) | spl2_2),
% 0.20/0.30 inference(negative_extensionality,[],[f454])).
% 0.20/0.30 thf(f562,plain,(
% 0.20/0.30 (((f @ sK5)) = $true) | ($true = (((^[Y0 : $o]: ($false)) @ sK5))) | spl2_2),
% 0.20/0.30 inference(xor_proxy_clausification,[],[f561])).
% 0.20/0.30 thf(f565,plain,(
% 0.20/0.30 (((f @ sK5)) = $true) | ($true = $false) | spl2_2),
% 0.20/0.30 inference(beta-eta_normalization,[],[f562])).
% 0.20/0.30 thf(f566,plain,(
% 0.20/0.30 (((f @ sK5)) = $true) | spl2_2),
% 0.20/0.30 inference(trivial_inequality_removal,[],[f565])).
% 0.20/0.30 thf(f586,plain,(
% 0.20/0.30 ($true = $false) | (~spl2_10 | ~spl2_12)),
% 0.20/0.30 inference(forward_demodulation,[],[f544,f535])).
% 0.20/0.30 thf(f587,plain,(
% 0.20/0.30 $false | (~spl2_10 | ~spl2_12)),
% 0.20/0.30 inference(trivial_inequality_removal,[],[f586])).
% 0.20/0.30 thf(f588,plain,(
% 0.20/0.30 ~spl2_10 | ~spl2_12),
% 0.20/0.30 inference(avatar_contradiction_clause,[],[f587])).
% 0.20/0.30 thf(f595,plain,(
% 0.20/0.30 ($true != ((f @ $false))) | (spl2_12 | ~spl2_13)),
% 0.20/0.30 inference(forward_demodulation,[],[f543,f548])).
% 0.20/0.30 thf(f597,plain,(
% 0.20/0.30 ((((^[Y0 : $o]: ($true)) @ sK6)) != ((f @ sK6))) | spl2_4),
% 0.20/0.30 inference(negative_extensionality,[],[f462])).
% 0.20/0.30 thf(f599,plain,(
% 0.20/0.30 ($false = (((^[Y0 : $o]: ($true)) @ sK6))) | ($false = ((f @ sK6))) | spl2_4),
% 0.20/0.30 inference(xor_proxy_clausification,[],[f597])).
% 0.20/0.30 thf(f600,plain,(
% 0.20/0.30 ($false = ((f @ sK6))) | ($true = $false) | spl2_4),
% 0.20/0.30 inference(beta-eta_normalization,[],[f599])).
% 0.20/0.30 thf(f601,plain,(
% 0.20/0.30 ($false = ((f @ sK6))) | spl2_4),
% 0.20/0.30 inference(trivial_inequality_removal,[],[f600])).
% 0.20/0.30 thf(f603,plain,(
% 0.20/0.30 ($false = sK5) | ($true = ((f @ $true))) | spl2_2),
% 0.20/0.30 inference(constrained_superposition,[],[f566,f16])).
% 0.20/0.30 thf(f605,definition,(
% 0.20/0.30 spl2_15 <=> ($true = ((f @ $true)))),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_15])],[avatar_definition])).
% 0.20/0.30 thf(f607,plain,(
% 0.20/0.30 ($true = ((f @ $true))) | ~spl2_15),
% 0.20/0.30 inference(avatar_component_clause,[],[f605])).
% 0.20/0.30 thf(f609,definition,(
% 0.20/0.30 spl2_16 <=> ($false = sK5)),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_16])],[avatar_definition])).
% 0.20/0.30 thf(f611,plain,(
% 0.20/0.30 ($false = sK5) | ~spl2_16),
% 0.20/0.30 inference(avatar_component_clause,[],[f609])).
% 0.20/0.30 thf(f612,plain,(
% 0.20/0.30 spl2_15 | spl2_16 | spl2_2),
% 0.20/0.30 inference(avatar_split_clause,[],[f603,f453,f609,f605])).
% 0.20/0.30 thf(f619,plain,(
% 0.20/0.30 ($false = ((f @ $true))) | ($false = sK6) | spl2_4),
% 0.20/0.30 inference(constrained_superposition,[],[f601,f16])).
% 0.20/0.30 thf(f623,definition,(
% 0.20/0.30 spl2_17 <=> ($false = sK6)),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition])).
% 0.20/0.30 thf(f625,plain,(
% 0.20/0.30 ($false = sK6) | ~spl2_17),
% 0.20/0.30 inference(avatar_component_clause,[],[f623])).
% 0.20/0.30 thf(f626,plain,(
% 0.20/0.30 spl2_17 | spl2_14 | spl2_4),
% 0.20/0.30 inference(avatar_split_clause,[],[f619,f460,f554,f623])).
% 0.20/0.30 thf(f628,plain,(
% 0.20/0.30 ($false = ((f @ $false))) | (spl2_4 | ~spl2_17)),
% 0.20/0.30 inference(constrained_superposition,[],[f601,f625])).
% 0.20/0.30 thf(f637,plain,(
% 0.20/0.30 ((((^[Y0 : $o]: (Y0)) @ sK7)) != ((f @ sK7))) | spl2_5),
% 0.20/0.30 inference(negative_extensionality,[],[f473])).
% 0.20/0.30 thf(f638,plain,(
% 0.20/0.30 ($true = ((f @ sK7))) | ((((^[Y0 : $o]: (Y0)) @ sK7)) = $true) | spl2_5),
% 0.20/0.30 inference(xor_proxy_clausification,[],[f637])).
% 0.20/0.30 thf(f639,plain,(
% 0.20/0.30 ($false = ((f @ sK7))) | ((((^[Y0 : $o]: (Y0)) @ sK7)) = $false) | spl2_5),
% 0.20/0.30 inference(xor_proxy_clausification,[],[f637])).
% 0.20/0.30 thf(f640,plain,(
% 0.20/0.30 ($false = sK7) | ($false = ((f @ sK7))) | spl2_5),
% 0.20/0.30 inference(beta-eta_normalization,[],[f639])).
% 0.20/0.30 thf(f641,plain,(
% 0.20/0.30 ($true = sK7) | ($true = ((f @ sK7))) | spl2_5),
% 0.20/0.30 inference(beta-eta_normalization,[],[f638])).
% 0.20/0.30 thf(f643,definition,(
% 0.20/0.30 spl2_18 <=> ($false = ((f @ sK7)))),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition])).
% 0.20/0.30 thf(f645,plain,(
% 0.20/0.30 ($false = ((f @ sK7))) | ~spl2_18),
% 0.20/0.30 inference(avatar_component_clause,[],[f643])).
% 0.20/0.30 thf(f647,definition,(
% 0.20/0.30 spl2_19 <=> ($false = sK7)),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition])).
% 0.20/0.30 thf(f649,plain,(
% 0.20/0.30 ($false = sK7) | ~spl2_19),
% 0.20/0.30 inference(avatar_component_clause,[],[f647])).
% 0.20/0.30 thf(f650,plain,(
% 0.20/0.30 spl2_18 | spl2_19 | spl2_5),
% 0.20/0.30 inference(avatar_split_clause,[],[f640,f472,f647,f643])).
% 0.20/0.30 thf(f652,definition,(
% 0.20/0.30 spl2_20 <=> ($true = sK7)),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_20])],[avatar_definition])).
% 0.20/0.30 thf(f653,plain,(
% 0.20/0.30 ($true != sK7) | spl2_20),
% 0.20/0.30 inference(avatar_component_clause,[],[f652])).
% 0.20/0.30 thf(f654,plain,(
% 0.20/0.30 ($true = sK7) | ~spl2_20),
% 0.20/0.30 inference(avatar_component_clause,[],[f652])).
% 0.20/0.30 thf(f656,definition,(
% 0.20/0.30 spl2_21 <=> ($true = ((f @ sK7)))),
% 0.20/0.30 introduced(definition,[new_symbols(definition,[spl2_21])],[avatar_definition])).
% 0.20/0.30 thf(f658,plain,(
% 0.20/0.30 ($true = ((f @ sK7))) | ~spl2_21),
% 0.20/0.30 inference(avatar_component_clause,[],[f656])).
% 0.20/0.30 thf(f659,plain,(
% 0.20/0.30 spl2_20 | spl2_21 | spl2_5),
% 0.20/0.30 inference(avatar_split_clause,[],[f641,f472,f656,f652])).
% 0.20/0.30 thf(f660,plain,(
% 0.20/0.30 ($false = ((f @ $true))) | (~spl2_18 | ~spl2_20)),
% 0.20/0.30 inference(forward_demodulation,[],[f645,f654])).
% 0.20/0.30 thf(f666,plain,(
% 0.20/0.30 ($true = $false) | (~spl2_14 | ~spl2_15)),
% 0.20/0.30 inference(forward_demodulation,[],[f556,f607])).
% 0.20/0.30 thf(f667,plain,(
% 0.20/0.30 $false | (~spl2_14 | ~spl2_15)),
% 0.20/0.30 inference(trivial_inequality_removal,[],[f666])).
% 0.20/0.30 thf(f668,plain,(
% 0.20/0.30 ~spl2_14 | ~spl2_15),
% 0.20/0.30 inference(avatar_contradiction_clause,[],[f667])).
% 0.20/0.30 thf(f669,plain,(
% 0.20/0.30 spl2_14 | ~spl2_18 | ~spl2_20),
% 0.20/0.30 inference(avatar_split_clause,[],[f660,f652,f643,f554])).
% 0.20/0.30 thf(f677,plain,(
% 0.20/0.30 ($true = ((f @ $false))) | (spl2_2 | ~spl2_16)),
% 0.20/0.30 inference(constrained_superposition,[],[f566,f611])).
% 0.20/0.30 thf(f679,plain,(
% 0.20/0.30 $false | (spl2_2 | spl2_12 | ~spl2_13 | ~spl2_16)),
% 0.20/0.30 inference(forward_subsumption_resolution,[],[f677,f595])).
% 0.20/0.30 thf(f680,plain,(
% 0.20/0.30 spl2_2 | spl2_12 | ~spl2_13 | ~spl2_16),
% 0.20/0.30 inference(avatar_contradiction_clause,[],[f679])).
% 0.20/0.30 thf(f684,plain,(
% 0.20/0.30 ($false != ((f @ $true))) | (spl2_10 | ~spl2_11)),
% 0.20/0.30 inference(forward_demodulation,[],[f534,f539])).
% 0.20/0.30 thf(f685,plain,(
% 0.20/0.30 ~spl2_14 | spl2_10 | ~spl2_11),
% 0.20/0.30 inference(avatar_split_clause,[],[f684,f537,f533,f554])).
% 0.20/0.30 thf(f686,plain,(
% 0.20/0.30 ($true = $false) | (~spl2_19 | ~spl2_20)),
% 0.20/0.30 inference(forward_demodulation,[],[f649,f654])).
% 0.20/0.30 thf(f687,plain,(
% 0.20/0.30 $false | (~spl2_19 | ~spl2_20)),
% 0.20/0.30 inference(trivial_inequality_removal,[],[f686])).
% 0.20/0.30 thf(f688,plain,(
% 0.20/0.30 ~spl2_19 | ~spl2_20),
% 0.20/0.30 inference(avatar_contradiction_clause,[],[f687])).
% 0.20/0.30 thf(f691,plain,(
% 0.20/0.30 ($false = sK7) | ($true != $true) | spl2_20),
% 0.20/0.30 inference(constrained_superposition,[],[f653,f16])).
% 0.20/0.30 thf(f692,plain,(
% 0.20/0.30 ($false = sK7) | spl2_20),
% 0.20/0.30 inference(trivial_inequality_removal,[],[f691])).
% 0.20/0.30 thf(f693,plain,(
% 0.20/0.30 spl2_19 | spl2_20),
% 0.20/0.30 inference(avatar_split_clause,[],[f692,f652,f647])).
% 0.20/0.30 thf(f700,plain,(
% 0.20/0.30 ($true = ((f @ $false))) | (~spl2_19 | ~spl2_21)),
% 0.20/0.30 inference(forward_demodulation,[],[f658,f649])).
% 0.20/0.30 thf(f724,plain,(
% 0.20/0.30 ($true = $false) | (spl2_4 | ~spl2_17 | ~spl2_19 | ~spl2_21)),
% 0.20/0.30 inference(forward_demodulation,[],[f628,f700])).
% 0.20/0.30 thf(f725,plain,(
% 0.20/0.30 $false | (spl2_4 | ~spl2_17 | ~spl2_19 | ~spl2_21)),
% 0.20/0.30 inference(trivial_inequality_removal,[],[f724])).
% 0.20/0.30 thf(f726,plain,(
% 0.20/0.30 spl2_4 | ~spl2_17 | ~spl2_19 | ~spl2_21),
% 0.20/0.30 inference(avatar_contradiction_clause,[],[f725])).
% 0.20/0.30 cnf(s14, plain, spl2_3 | ~spl2_4 | spl2_5, inference(sat_conversion,[],[f480])).
% 0.20/0.30 cnf(s15, plain, ~spl2_1 | spl2_3 | spl2_5, inference(sat_conversion,[],[f481])).
% 0.20/0.30 cnf(s23, plain, spl2_3 | ~spl2_5, inference(sat_conversion,[],[f489])).
% 0.20/0.30 cnf(s27, plain, ~spl2_2 | spl2_3, inference(sat_conversion,[],[f493])).
% 0.20/0.30 cnf(s36, plain, ~spl2_3, inference(sat_conversion,[],[f526])).
% 0.20/0.30 cnf(s37, plain, spl2_1 | spl2_10 | spl2_11, inference(sat_conversion,[],[f540])).
% 0.20/0.30 cnf(s38, plain, spl2_1 | spl2_12 | spl2_13, inference(sat_conversion,[],[f549])).
% 0.20/0.30 cnf(s44, plain, ~spl2_10 | ~spl2_12, inference(sat_conversion,[],[f588])).
% 0.20/0.30 cnf(s46, plain, spl2_2 | spl2_15 | spl2_16, inference(sat_conversion,[],[f612])).
% 0.20/0.30 cnf(s48, plain, spl2_4 | spl2_14 | spl2_17, inference(sat_conversion,[],[f626])).
% 0.20/0.30 cnf(s49, plain, spl2_5 | spl2_18 | spl2_19, inference(sat_conversion,[],[f650])).
% 0.20/0.30 cnf(s50, plain, spl2_5 | spl2_20 | spl2_21, inference(sat_conversion,[],[f659])).
% 0.20/0.30 cnf(s53, plain, ~spl2_14 | ~spl2_15, inference(sat_conversion,[],[f668])).
% 0.20/0.30 cnf(s54, plain, spl2_14 | ~spl2_18 | ~spl2_20, inference(sat_conversion,[],[f669])).
% 0.20/0.30 cnf(s56, plain, spl2_2 | spl2_12 | ~spl2_13 | ~spl2_16, inference(sat_conversion,[],[f680])).
% 0.20/0.30 cnf(s57, plain, spl2_10 | ~spl2_11 | ~spl2_14, inference(sat_conversion,[],[f685])).
% 0.20/0.30 cnf(s58, plain, ~spl2_19 | ~spl2_20, inference(sat_conversion,[],[f688])).
% 0.20/0.30 cnf(s60, plain, spl2_19 | spl2_20, inference(sat_conversion,[],[f693])).
% 0.20/0.30 cnf(s66, plain, spl2_4 | ~spl2_17 | ~spl2_19 | ~spl2_21, inference(sat_conversion,[],[f726])).
% 0.20/0.30 cnf(s72, plain, ~spl2_2, inference(rat,[],[s27,s36])).
% 0.20/0.30 cnf(s74, plain, ~spl2_5, inference(rat,[],[s23,s36])).
% 0.20/0.30 cnf(s76, plain, ~spl2_1, inference(rat,[],[s15,s74,s36])).
% 0.20/0.30 cnf(s77, plain, ~spl2_4, inference(rat,[],[s14,s74,s36])).
% 0.20/0.30 cnf(s78, plain, ~spl2_19 | ~spl2_17, inference(rat,[],[s50,s66,s58,s74,s77])).
% 0.20/0.30 cnf(s79, plain, spl2_14, inference(rat,[],[s54,s49,s60,s78,s48,s74,s77])).
% 0.20/0.30 cnf(s80, plain, ~spl2_15, inference(rat,[],[s53,s79])).
% 0.20/0.30 cnf(s81, plain, spl2_16, inference(rat,[],[s46,s72,s80])).
% 0.20/0.30 cnf(s86, plain, spl2_10, inference(rat,[],[s37,s57,s76,s79])).
% 0.20/0.30 cnf(s87, plain, ~spl2_12, inference(rat,[],[s44,s86])).
% 0.20/0.30 cnf(s88, plain, spl2_13, inference(rat,[],[s38,s76,s87])).
% 0.20/0.30 cnf(s89, plain, $false, inference(rat,[],[s56,s81,s72,s87,s88])).
% 0.20/0.30 thf(f727,plain,(
% 0.20/0.30 $false),
% 0.20/0.30 inference(avatar_sat_refutation,[],[s89])).
% 0.20/0.30 % SZS output end Proof for theBenchmark
% 0.20/0.30 % (3155803)------------------------------
% 0.20/0.30 % (3155803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.30 % (3155803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.30 % (3155803)CaDiCaL version: 2.1.3
% 0.20/0.30 % (3155803)Termination reason: Refutation
% 0.20/0.30 % (3155803)Time elapsed: 0.014 s
% 0.20/0.30 % (3155803)Peak memory usage: 13 MB
% 0.20/0.30 % (3155803)Instructions burned: 25 (million)
% 0.20/0.30 % (3155792)Success in time 0.051 s
% 0.20/0.30 % Vampire exiting
%------------------------------------------------------------------------------