%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO545^1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:48:23 AM UTC 2026
% Result : Theorem 0.21s 0.30s
% Output : Refutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO545^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n011.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 17:14:16 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.30 % (382523)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.30 % (382551)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2427016577:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.30 % (382551)Refutation not found, incomplete strategy
% 0.21/0.30 % (382551)------------------------------
% 0.21/0.30 % (382551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (382551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (382551)CaDiCaL version: 2.1.3
% 0.21/0.30 % (382551)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.30 % (382551)Time elapsed: 0.002 s
% 0.21/0.30 % (382551)Peak memory usage: 12 MB
% 0.21/0.30 % (382551)Instructions burned: 7 (million)
% 0.21/0.30 % (382551)------------------------------
% 0.21/0.30 % (382551)------------------------------
% 0.21/0.30 % (382557)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.30 % (382557)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.21/0.30 % (382553)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=822314284:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.30 % (382552)lrs+10_16_si=on:nwc=1.5:random_seed=3795908030:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.30 % (382555)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3266869626:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.30 % (382557)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=4239470889:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.30 % (382554)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=20016568: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.21/0.30 % (382556)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2328157347:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.30 % (382553)Instruction limit reached!
% 0.21/0.30 % (382553)------------------------------
% 0.21/0.30 % (382553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (382553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (382553)CaDiCaL version: 2.1.3
% 0.21/0.30 % (382553)Termination reason: Instruction limit
% 0.21/0.30 % (382553)Termination phase: Saturation
% 0.21/0.30 % (382553)Time elapsed: 0.002 s
% 0.21/0.30 % (382553)Peak memory usage: 11 MB
% 0.21/0.30 % (382553)Instructions burned: 3 (million)
% 0.21/0.30 % (382568)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2193116236:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.30 % (382568)Instruction limit reached!
% 0.21/0.30 % (382568)------------------------------
% 0.21/0.30 % (382568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (382568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (382568)CaDiCaL version: 2.1.3
% 0.21/0.30 % (382568)Termination reason: Instruction limit
% 0.21/0.30 % (382568)Termination phase: Saturation
% 0.21/0.30 % (382568)Time elapsed: 0.001 s
% 0.21/0.30 % (382568)Peak memory usage: 11 MB
% 0.21/0.30 % (382568)Instructions burned: 3 (million)
% 0.21/0.30 % (382552)Instruction limit reached!
% 0.21/0.30 % (382552)------------------------------
% 0.21/0.30 % (382552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (382552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (382552)CaDiCaL version: 2.1.3
% 0.21/0.30 % (382552)Termination reason: Instruction limit
% 0.21/0.30 % (382552)Termination phase: Saturation
% 0.21/0.30 % (382552)Time elapsed: 0.011 s
% 0.21/0.30 % (382552)Peak memory usage: 12 MB
% 0.21/0.30 % (382552)Instructions burned: 19 (million)
% 0.21/0.30 % (382557) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-382523-382557"...
% 0.21/0.30 % (382555)Instruction limit reached!
% 0.21/0.30 % (382555)------------------------------
% 0.21/0.30 % (382555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (382555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (382555)CaDiCaL version: 2.1.3
% 0.21/0.30 % (382555)Termination reason: Instruction limit
% 0.21/0.30 % (382555)Termination phase: Saturation
% 0.21/0.30 % (382555)Time elapsed: 0.013 s
% 0.21/0.30 % (382555)Peak memory usage: 12 MB
% 0.21/0.30 % (382555)Instructions burned: 24 (million)
% 0.21/0.30 % (382579)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.30 % (382579)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3069237419:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.21/0.30 % (382557)...printing done.
% 0.21/0.30 % (382579)Instruction limit reached!
% 0.21/0.30 % (382579)------------------------------
% 0.21/0.30 % (382579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (382579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (382579)CaDiCaL version: 2.1.3
% 0.21/0.30 % (382579)Termination reason: Instruction limit
% 0.21/0.30 % (382579)Termination phase: Saturation
% 0.21/0.30 % (382579)Time elapsed: 0.002 s
% 0.21/0.30 % (382579)Peak memory usage: 12 MB
% 0.21/0.30 % (382579)Instructions burned: 9 (million)
% 0.21/0.30 % (382557)Refutation found. Thanks to Tanya!
% 0.21/0.30 % SZS status Theorem for theBenchmark
% 0.21/0.30 % SZS output start Proof for theBenchmark
% 0.21/0.30 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.21/0.30 thf(func_def_0, type, eps: (($i > $o) > $i)).
% 0.21/0.30 thf(func_def_2, type, case: (($o > $o) > $i > $i > $i > $i > $i)).
% 0.21/0.30 thf(func_def_3, type, vNOT: ($o > $o)).
% 0.21/0.30 thf(func_def_4, type, f: ($o > $o)).
% 0.21/0.30 thf(func_def_5, type, vOR: ($o > $o > $o)).
% 0.21/0.30 thf(func_def_6, type, vAND: ($o > $o > $o)).
% 0.21/0.30 thf(func_def_7, type, db5: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_10, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.21/0.30 thf(func_def_11, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.21/0.30 thf(func_def_12, type, db4: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_13, type, db0: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_14, type, db3: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_15, type, db1: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_16, type, db2: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_23, type, sK6: $o).
% 0.21/0.30 thf(func_def_24, type, sK7: $o).
% 0.21/0.30 thf(func_def_25, type, sK8: $o).
% 0.21/0.30 thf(func_def_26, type, sK9: $o).
% 0.21/0.30 thf(func_def_27, type, sK10: $o).
% 0.21/0.30 thf(func_def_28, type, sK11: $o).
% 0.21/0.30 thf(func_def_29, type, sK12: $o).
% 0.21/0.30 thf(func_def_30, type, sK13: $o).
% 0.21/0.30 thf(f1,axiom,(
% 0.21/0.30 ! [X0 : ($i > $o)] : (? [X1 : $i] : (X0 @ X1) => (X0 @ (eps @ X0)))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',choiceax)).
% 0.21/0.30 thf(f2,axiom,(
% 0.21/0.30 (case = (^[X0 : ($o > $o), X1 : $i, X2 : $i, X3 : $i, X4 : $i] : ((eps @ (^[X5 : $i] : (((X5 = X3) & (X0 = (^[X6 : $o] : (X6)))) | (((^[X6 : $o] : ($true)) = X0) & (X5 = X4)) | ((X5 = X2) & (X0 = ~)) | ((X5 = X1) & (X0 = (^[X6 : $o] : ($false))))))))))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',caseood)).
% 0.21/0.30 thf(f3,conjecture,(
% 0.21/0.30 ! [X2 : $i,X1 : $i,X3 : $i,X0 : $i] : ((((case @ f @ X0 @ X1 @ X2 @ X3)) = X0) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X2) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X3) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X1))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 0.21/0.30 thf(f4,negated_conjecture,(
% 0.21/0.30 ~ ! [X2 : $i,X1 : $i,X3 : $i,X0 : $i] : ((((case @ f @ X0 @ X1 @ X2 @ X3)) = X0) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X2) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X3) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X1))),
% 0.21/0.30 inference(negated_conjecture,[status(cth)],[f3])).
% 0.21/0.30 thf(f5,plain,(
% 0.21/0.30 (case = (^[X0 : ($o > $o), X1 : $i, X2 : $i, X3 : $i, X4 : $i] : ((eps @ (^[X5 : $i] : (((X5 = X3) & (X0 = (^[X6 : $o] : (X6)))) | (((^[X7 : $o] : ($true)) = X0) & (X5 = X4)) | ((X5 = X2) & (X0 = ~)) | ((X5 = X1) & (X0 = (^[X8 : $o] : ($false))))))))))),
% 0.21/0.30 inference(rectify,[],[f2])).
% 0.21/0.30 thf(f6,plain,(
% 0.21/0.30 (case = (^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y4 = Y5) & ((^[Y6 : $o]: ($true)) = Y0))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5)))))))))))))))),
% 0.21/0.30 inference(fool_elimination,[],[f5])).
% 0.21/0.30 thf(f7,plain,(
% 0.21/0.30 ! [X0 : ($i > $o)] : (? [X1 : $i] : (X0 @ X1) => (X0 @ (eps @ X0)))),
% 0.21/0.30 inference(rectify,[],[f1])).
% 0.21/0.30 thf(f8,plain,(
% 0.21/0.30 ! [X0 : ($i > $o)] : (? [X1 : $i] : (((X0 @ X1)) = $true) => (((X0 @ (eps @ X0))) = $true))),
% 0.21/0.30 inference(fool_elimination,[],[f7])).
% 0.21/0.30 thf(f9,plain,(
% 0.21/0.30 ~ ! [X0 : $i,X3 : $i,X1 : $i,X2 : $i] : ((((case @ f @ X3 @ X1 @ X0 @ X2)) = X0) | (((case @ f @ X3 @ X1 @ X0 @ X2)) = X3) | (((case @ f @ X3 @ X1 @ X0 @ X2)) = X1) | (((case @ f @ X3 @ X1 @ X0 @ X2)) = X2))),
% 0.21/0.30 inference(rectify,[],[f4])).
% 0.21/0.30 thf(f10,plain,(
% 0.21/0.30 ! [X0 : ($i > $o)] : ((((X0 @ (eps @ X0))) = $true) | ! [X1 : $i] : (((X0 @ X1)) != $true))),
% 0.21/0.30 inference(ennf_transformation,[],[f8])).
% 0.21/0.30 thf(f11,plain,(
% 0.21/0.30 ? [X3 : $i,X0 : $i,X2 : $i,X1 : $i] : ((((case @ f @ X3 @ X1 @ X0 @ X2)) != X0) & (((case @ f @ X3 @ X1 @ X0 @ X2)) != X2) & (((case @ f @ X3 @ X1 @ X0 @ X2)) != X3) & (((case @ f @ X3 @ X1 @ X0 @ X2)) != X1))),
% 0.21/0.30 inference(ennf_transformation,[],[f9])).
% 0.21/0.30 thf(f12,plain,(
% 0.21/0.30 ? [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : ((((case @ f @ X0 @ X3 @ X1 @ X2)) != X1) & (((case @ f @ X0 @ X3 @ X1 @ X2)) != X2) & (((case @ f @ X0 @ X3 @ X1 @ X2)) != X0) & (((case @ f @ X0 @ X3 @ X1 @ X2)) != X3))),
% 0.21/0.30 inference(rectify,[],[f11])).
% 0.21/0.30 thf(f13,plain,(
% 0.21/0.30 (sK1 != ((case @ f @ sK0 @ sK3 @ sK1 @ sK2))) & (((case @ f @ sK0 @ sK3 @ sK1 @ sK2)) != sK2) & (((case @ f @ sK0 @ sK3 @ sK1 @ sK2)) != sK0) & (sK3 != ((case @ f @ sK0 @ sK3 @ sK1 @ sK2)))),
% 0.21/0.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f12])).
% 0.21/0.30 thf(f14,plain,(
% 0.21/0.30 (sK3 != ((case @ f @ sK0 @ sK3 @ sK1 @ sK2)))),
% 0.21/0.30 inference(cnf_transformation,[],[f13])).
% 0.21/0.30 thf(f15,plain,(
% 0.21/0.30 (((case @ f @ sK0 @ sK3 @ sK1 @ sK2)) != sK0)),
% 0.21/0.30 inference(cnf_transformation,[],[f13])).
% 0.21/0.30 thf(f16,plain,(
% 0.21/0.30 (((case @ f @ sK0 @ sK3 @ sK1 @ sK2)) != sK2)),
% 0.21/0.30 inference(cnf_transformation,[],[f13])).
% 0.21/0.30 thf(f17,plain,(
% 0.21/0.30 (sK1 != ((case @ f @ sK0 @ sK3 @ sK1 @ sK2)))),
% 0.21/0.30 inference(cnf_transformation,[],[f13])).
% 0.21/0.30 thf(f18,plain,(
% 0.21/0.30 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ (eps @ X0))) = $true) | (((X0 @ X1)) != $true)) )),
% 0.21/0.30 inference(cnf_transformation,[],[f10])).
% 0.21/0.30 thf(f19,plain,(
% 0.21/0.30 (case = (^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y4 = Y5) & ((^[Y6 : $o]: ($true)) = Y0))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5)))))))))))))))),
% 0.21/0.30 inference(cnf_transformation,[],[f6])).
% 0.21/0.30 thf(f21,definition,(
% 0.21/0.30 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.21/0.30 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.21/0.30 thf(f22,plain,(
% 0.21/0.30 (sK1 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y4 = Y5) & ((^[Y6 : $o]: ($true)) = Y0))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5)))))))))))))) @ f @ sK0 @ sK3 @ sK1 @ sK2)))),
% 0.21/0.30 inference(definition_unfolding,[],[f17,f19])).
% 0.21/0.30 thf(f23,plain,(
% 0.21/0.30 (sK2 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y4 = Y5) & ((^[Y6 : $o]: ($true)) = Y0))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5)))))))))))))) @ f @ sK0 @ sK3 @ sK1 @ sK2)))),
% 0.21/0.30 inference(definition_unfolding,[],[f16,f19])).
% 0.21/0.30 thf(f24,plain,(
% 0.21/0.30 (sK0 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y4 = Y5) & ((^[Y6 : $o]: ($true)) = Y0))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5)))))))))))))) @ f @ sK0 @ sK3 @ sK1 @ sK2)))),
% 0.21/0.30 inference(definition_unfolding,[],[f15,f19])).
% 0.21/0.30 thf(f25,plain,(
% 0.21/0.30 (sK3 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y4 = Y5) & ((^[Y6 : $o]: ($true)) = Y0))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5)))))))))))))) @ f @ sK0 @ sK3 @ sK1 @ sK2)))),
% 0.21/0.30 inference(definition_unfolding,[],[f14,f19])).
% 0.21/0.30 thf(f26,definition,(
% 0.21/0.30 (sF4 = (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y4 = Y5) & ((^[Y6 : $o]: ($true)) = Y0))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5)))))))))))))) @ f @ sK0 @ sK3 @ sK1 @ sK2)))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 0.21/0.30 thf(f27,plain,(
% 0.21/0.30 (sK1 != sF4)),
% 0.21/0.30 inference(definition_folding,[],[f22,f26])).
% 0.21/0.30 thf(f28,plain,(
% 0.21/0.30 (sF4 != sK2)),
% 0.21/0.30 inference(definition_folding,[],[f23,f26])).
% 0.21/0.30 thf(f29,plain,(
% 0.21/0.30 (sF4 != sK0)),
% 0.21/0.30 inference(definition_folding,[],[f24,f26])).
% 0.21/0.30 thf(f30,plain,(
% 0.21/0.30 (sF4 != sK3)),
% 0.21/0.30 inference(definition_folding,[],[f25,f26])).
% 0.21/0.30 thf(f31,plain,(
% 0.21/0.30 (((eps @ (^[Y0 : $i]: (((((f = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((~ = f) & (sK3 = Y0))) | ((sK2 = Y0) & ((^[Y1 : $o]: ($true)) = f))) | ((f = (^[Y1 : $o]: (Y1))) & (sK1 = Y0)))))) = sF4)),
% 0.21/0.30 inference(beta-eta_normalization,[],[f26])).
% 0.21/0.30 thf(f39,plain,(
% 0.21/0.30 ( ! [X0 : $i] : (((((^[Y0 : $i]: (((((f = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((~ = f) & (sK3 = Y0))) | ((sK2 = Y0) & ((^[Y1 : $o]: ($true)) = f))) | ((f = (^[Y1 : $o]: (Y1))) & (sK1 = Y0)))) @ X0)) != $true) | ((((^[Y0 : $i]: (((((f = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((~ = f) & (sK3 = Y0))) | ((sK2 = Y0) & ((^[Y1 : $o]: ($true)) = f))) | ((f = (^[Y1 : $o]: (Y1))) & (sK1 = Y0)))) @ sF4)) = $true)) )),
% 0.21/0.30 inference(constrained_superposition,[],[f18,f31])).
% 0.21/0.30 thf(f40,plain,(
% 0.21/0.30 ( ! [X0 : $i] : (($true != ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK3 = X0))) | ((sK2 = X0) & ((^[Y0 : $o]: ($true)) = f))) | ((f = (^[Y0 : $o]: (Y0))) & (sK1 = X0))))) | ($true = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))) | ((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4)))))) )),
% 0.21/0.30 inference(beta-eta_normalization,[],[f39])).
% 0.21/0.30 thf(f41,plain,(
% 0.21/0.30 ( ! [X0 : $i] : (($true = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))) | ((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))))) | ($false = (((f = (^[Y0 : $o]: (Y0))) & (sK1 = X0))))) )),
% 0.21/0.30 inference(or_proxy_clausification,[],[f40])).
% 0.21/0.30 thf(f42,plain,(
% 0.21/0.30 ( ! [X0 : $i] : (($false = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK3 = X0))) | ((sK2 = X0) & ((^[Y0 : $o]: ($true)) = f))))) | ($true = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))) | ((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4)))))) )),
% 0.21/0.30 inference(or_proxy_clausification,[],[f40])).
% 0.21/0.30 thf(f43,plain,(
% 0.21/0.30 ( ! [X0 : $i] : (($false = (((sK2 = X0) & ((^[Y0 : $o]: ($true)) = f)))) | ($true = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))) | ((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4)))))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f42])).
% 0.21/0.31 thf(f44,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))) | ((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))))) | ($false = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK3 = X0)))))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f42])).
% 0.21/0.31 thf(f45,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = (((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4)))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))))) | ($false = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK3 = X0)))))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f44])).
% 0.21/0.31 thf(f46,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))))) | ($false = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK3 = X0))))) | ($true = ((sK1 = sF4)))) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f45])).
% 0.21/0.31 thf(f147,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = (((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f)))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))))) | ($true = ((sK1 = sF4))) | ($false = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK3 = X0)))))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f46])).
% 0.21/0.31 thf(f149,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((sK1 = sF4))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))))) | ($false = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK3 = X0))))) | ($true = ((sK2 = sF4)))) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f147])).
% 0.21/0.31 thf(f150,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($false = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK3 = X0))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))))) | ($true = ((sK2 = sF4))) | (sK1 = sF4)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f149])).
% 0.21/0.31 thf(f151,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((sK2 = sF4))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))))) | ((((~ = f) & (sK3 = X0))) = $false) | (sK1 = sF4)) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f150])).
% 0.21/0.31 thf(f152,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 = sF4) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))))) | ($false = (((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)))) | ($true = ((sK2 = sF4)))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f150])).
% 0.21/0.31 thf(f153,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 = sF4) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | ($false = (((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)))) | ($true = (((~ = f) & (sK3 = sF4)))) | ($true = ((sK2 = sF4)))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f152])).
% 0.21/0.31 thf(f154,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 = sF4) | ($true = (((~ = f) & (sK3 = sF4)))) | ($false = (((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)))) | ($true = ((sK2 = sF4))) | ($true = ((sK0 = sF4)))) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f153])).
% 0.21/0.31 thf(f170,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((sK2 = sF4))) | ($true = ((sK3 = sF4))) | (sK1 = sF4) | ($true = ((sK0 = sF4))) | ($false = (((f = (^[Y0 : $o]: ($false))) & (sK0 = X0))))) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f154])).
% 0.21/0.31 thf(f178,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((sK3 = sF4))) | ($false = (((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)))) | ($true = ((sK0 = sF4))) | (sF4 = sK2) | (sK1 = sF4)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f170])).
% 0.21/0.31 thf(f179,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK2) | ($false = (((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)))) | (sF4 = sK3) | ($true = ((sK0 = sF4))) | (sK1 = sF4)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f178])).
% 0.21/0.31 thf(f180,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK2) | (((f = (^[Y0 : $o]: ($false)))) = $false) | (((sK0 = X0)) = $false) | ($true = ((sK0 = sF4))) | (sF4 = sK3) | (sK1 = sF4)) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f179])).
% 0.21/0.31 thf(f181,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK2) | (sF4 = sK3) | (f != (^[Y0 : $o]: ($false))) | (((sK0 = X0)) = $false) | ($true = ((sK0 = sF4))) | (sK1 = sF4)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f180])).
% 0.21/0.31 thf(f182,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((sK0 = sF4))) | (sK0 != X0) | (sF4 = sK2) | (sK1 = sF4) | (f != (^[Y0 : $o]: ($false))) | (sF4 = sK3)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f181])).
% 0.21/0.31 thf(f183,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK3) | (f != (^[Y0 : $o]: ($false))) | (sK0 != X0) | (sF4 = sK0) | (sF4 = sK2) | (sK1 = sF4)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f182])).
% 0.21/0.31 thf(f184,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK2) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))))) | (sK1 = sF4) | ((((~ = f) & (sK3 = X0))) = $false)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f151])).
% 0.21/0.31 thf(f185,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = (((~ = f) & (sK3 = sF4)))) | (sF4 = sK2) | (sK1 = sF4) | ((((~ = f) & (sK3 = X0))) = $false) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f184])).
% 0.21/0.31 thf(f186,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((sK3 = sF4))) | (sF4 = sK2) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | ((((~ = f) & (sK3 = X0))) = $false) | (sK1 = sF4)) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f185])).
% 0.21/0.31 thf(f198,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (((((~ = f) & (sK3 = X0))) = $false) | (sF4 = sK3) | (sK1 = sF4) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | (sF4 = sK2)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f186])).
% 0.21/0.31 thf(f199,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 = sF4) | ($false = ((sK3 = X0))) | (sF4 = sK2) | ($false = ((~ = f))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | (sF4 = sK3)) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f198])).
% 0.21/0.31 thf(f200,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($false = ((~ = f))) | (sF4 = sK2) | (sF4 = sK3) | (sK1 = sF4) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | (sK3 != X0)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f199])).
% 0.21/0.31 thf(f201,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK3) | (sK1 = sF4) | (sF4 = sK2) | (~ != f) | (sK3 != X0) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f200])).
% 0.21/0.31 thf(f202,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK3 != X0) | (sK1 = sF4) | (sF4 = sK3) | (sF4 = sK2) | ($true = ((sK0 = sF4))) | (~ != f)) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f201])).
% 0.21/0.31 thf(f205,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK3 != X0) | (~ != f) | (sF4 = sK3) | (sF4 = sK2) | (sF4 = sK0) | (sK1 = sF4)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f202])).
% 0.21/0.31 thf(f264,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($false = ((sK2 = X0))) | ($false = (((^[Y0 : $o]: ($true)) = f))) | ($true = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))) | ((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4)))))) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f43])).
% 0.21/0.31 thf(f265,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))) | ((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))))) | ($false = (((^[Y0 : $o]: ($true)) = f))) | (sK2 != X0)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f264])).
% 0.21/0.31 thf(f266,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))))) | ($false = (((^[Y0 : $o]: ($true)) = f))) | (sK2 != X0) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f265])).
% 0.21/0.31 thf(f267,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($false = (((^[Y0 : $o]: ($true)) = f))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))))) | ($true = (((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f)))) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4)))) | (sK2 != X0)) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f266])).
% 0.21/0.31 thf(f268,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: ($true))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))))) | ($true = (((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f)))) | (sK2 != X0) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))))) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f267])).
% 0.21/0.31 thf(f269,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = (((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4)))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | (f != (^[Y0 : $o]: ($true))) | (sK2 != X0) | ($true = (((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f)))) | ($true = (((~ = f) & (sK3 = sF4))))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f268])).
% 0.21/0.31 thf(f270,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = (((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f)))) | ($true = (((~ = f) & (sK3 = sF4)))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | ($true = ((sK1 = sF4))) | (sK2 != X0) | (f != (^[Y0 : $o]: ($true)))) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f269])).
% 0.21/0.31 thf(f308,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((sK1 = sF4))) | ($true = ((sK2 = sF4))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | (f != (^[Y0 : $o]: ($true))) | (sK2 != X0) | ($true = (((~ = f) & (sK3 = sF4))))) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f270])).
% 0.21/0.31 thf(f309,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: ($true))) | (sK2 != X0) | ($true = (((~ = f) & (sK3 = sF4)))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | ($true = ((sK2 = sF4))) | (sK1 = sF4)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f308])).
% 0.21/0.31 thf(f310,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((sK2 = sF4))) | (f != (^[Y0 : $o]: ($true))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | ($true = ((sK3 = sF4))) | (sK1 = sF4) | (sK2 != X0)) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f309])).
% 0.21/0.31 thf(f318,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK2 != X0) | (sF4 = sK2) | (sK1 = sF4) | ($true = ((sK3 = sF4))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | (f != (^[Y0 : $o]: ($true)))) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f310])).
% 0.21/0.31 thf(f319,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | (sF4 = sK3) | (f != (^[Y0 : $o]: ($true))) | (sF4 = sK2) | (sK2 != X0) | (sK1 = sF4)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f318])).
% 0.21/0.31 thf(f320,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: ($true))) | (sK1 = sF4) | ($true = ((sK0 = sF4))) | (sF4 = sK2) | (sF4 = sK3) | (sK2 != X0)) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f319])).
% 0.21/0.31 thf(f323,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 = sF4) | (sF4 = sK2) | (sF4 = sK3) | (f != (^[Y0 : $o]: ($true))) | (sK2 != X0) | (sF4 = sK0)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f320])).
% 0.21/0.31 thf(f341,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($false = (((f = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))))) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f41])).
% 0.21/0.31 thf(f342,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = (((f = (^[Y0 : $o]: (Y0))) & (sK1 = sF4)))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))))) | ($false = ((f = (^[Y0 : $o]: (Y0))))) | ($false = ((sK1 = X0)))) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f341])).
% 0.21/0.31 thf(f343,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((sK1 = sF4))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))))) | ($false = ((f = (^[Y0 : $o]: (Y0))))) | ($false = ((sK1 = X0)))) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f342])).
% 0.21/0.31 thf(f384,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 = sF4) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))) | ((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))))) | ($false = ((sK1 = X0))) | ($false = ((f = (^[Y0 : $o]: (Y0)))))) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f343])).
% 0.21/0.31 thf(f385,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($false = ((sK1 = X0))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))))) | ($true = (((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f)))) | (sK1 = sF4) | ($false = ((f = (^[Y0 : $o]: (Y0)))))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f384])).
% 0.21/0.31 thf(f386,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($false = ((f = (^[Y0 : $o]: (Y0))))) | (sK1 = sF4) | (sK1 != X0) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))))) | ($true = (((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f))))) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f385])).
% 0.21/0.31 thf(f387,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 = sF4) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK3 = sF4))))) | ($true = (((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f)))) | (f != (^[Y0 : $o]: (Y0))) | (sK1 != X0)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f386])).
% 0.21/0.31 thf(f388,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = (((sK2 = sF4) & ((^[Y0 : $o]: ($true)) = f)))) | (f != (^[Y0 : $o]: (Y0))) | (sK1 != X0) | (sK1 = sF4) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | ($true = (((~ = f) & (sK3 = sF4))))) )),
% 0.21/0.31 inference(or_proxy_clausification,[],[f387])).
% 0.21/0.31 thf(f390,plain,(
% 0.21/0.31 ( ! [X0 : $i] : (($true = ((sK2 = sF4))) | ($true = (((~ = f) & (sK3 = sF4)))) | (sK1 = sF4) | (f != (^[Y0 : $o]: (Y0))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | (sK1 != X0)) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f388])).
% 0.21/0.31 thf(f391,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 = sF4) | (sK1 != X0) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)))) | ($true = (((~ = f) & (sK3 = sF4)))) | (sF4 = sK2) | (f != (^[Y0 : $o]: (Y0)))) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f390])).
% 0.21/0.31 thf(f392,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK2) | (sK1 != X0) | (sK1 = sF4) | ($true = ((sK0 = sF4))) | (f != (^[Y0 : $o]: (Y0))) | ($true = (((~ = f) & (sK3 = sF4))))) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f391])).
% 0.21/0.31 thf(f399,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: (Y0))) | (sK1 != X0) | (sF4 = sK0) | ($true = (((~ = f) & (sK3 = sF4)))) | (sF4 = sK2) | (sK1 = sF4)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f392])).
% 0.21/0.31 thf(f400,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: (Y0))) | (sF4 = sK0) | (sF4 = sK2) | ($true = ((sK3 = sF4))) | (sK1 != X0) | (sK1 = sF4)) )),
% 0.21/0.31 inference(and_proxy_clausification,[],[f399])).
% 0.21/0.31 thf(f403,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 != X0) | (sF4 = sK0) | (sK1 = sF4) | (f != (^[Y0 : $o]: (Y0))) | (sF4 = sK3) | (sF4 = sK2)) )),
% 0.21/0.31 inference(equality_proxy_clausification,[],[f400])).
% 0.21/0.31 thf(f426,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 = sF4) | (sF4 = sK2) | (sK0 != X0) | (f != (^[Y0 : $o]: ($false))) | (sF4 = sK0)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f183,f30])).
% 0.21/0.31 thf(f428,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK2) | (sF4 = sK0) | (~ != f) | (sK1 = sF4) | (sK3 != X0)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f205,f30])).
% 0.21/0.31 thf(f440,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK2 != X0) | (sF4 = sK0) | (f != (^[Y0 : $o]: ($true))) | (sF4 = sK2) | (sF4 = sK3)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f323,f27])).
% 0.21/0.31 thf(f444,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK2) | (sK1 != X0) | (sK1 = sF4) | (f != (^[Y0 : $o]: (Y0))) | (sF4 = sK3)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f403,f29])).
% 0.21/0.31 thf(f452,definition,(
% 0.21/0.31 spl5_1 <=> ! [X0 : $i] : (sK0 != X0)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition])).
% 0.21/0.31 thf(f453,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK0 != X0)) ) | ~spl5_1),
% 0.21/0.31 inference(avatar_component_clause,[],[f452])).
% 0.21/0.31 thf(f455,definition,(
% 0.21/0.31 spl5_2 <=> (f = (^[Y0 : $o]: ($false)))),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition])).
% 0.21/0.31 thf(f457,plain,(
% 0.21/0.31 (f != (^[Y0 : $o]: ($false))) | spl5_2),
% 0.21/0.31 inference(avatar_component_clause,[],[f455])).
% 0.21/0.31 thf(f459,definition,(
% 0.21/0.31 spl5_3 <=> (f = (^[Y0 : $o]: (Y0)))),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition])).
% 0.21/0.31 thf(f460,plain,(
% 0.21/0.31 (f != (^[Y0 : $o]: (Y0))) | spl5_3),
% 0.21/0.31 inference(avatar_component_clause,[],[f459])).
% 0.21/0.31 thf(f463,definition,(
% 0.21/0.31 spl5_4 <=> (f = (^[Y0 : $o]: ($true)))),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition])).
% 0.21/0.31 thf(f464,plain,(
% 0.21/0.31 (f != (^[Y0 : $o]: ($true))) | spl5_4),
% 0.21/0.31 inference(avatar_component_clause,[],[f463])).
% 0.21/0.31 thf(f467,definition,(
% 0.21/0.31 spl5_5 <=> (~ = f)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition])).
% 0.21/0.31 thf(f468,plain,(
% 0.21/0.31 (~ != f) | spl5_5),
% 0.21/0.31 inference(avatar_component_clause,[],[f467])).
% 0.21/0.31 thf(f475,definition,(
% 0.21/0.31 spl5_6 <=> ! [X0 : $i] : (sK3 != X0)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition])).
% 0.21/0.31 thf(f476,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK3 != X0)) ) | ~spl5_6),
% 0.21/0.31 inference(avatar_component_clause,[],[f475])).
% 0.21/0.31 thf(f480,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK0) | (f != (^[Y0 : $o]: ($false))) | (sF4 = sK2) | (sK0 != X0)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f426,f27])).
% 0.21/0.31 thf(f482,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 = sF4) | (sF4 = sK0) | (sK3 != X0) | (~ != f)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f428,f28])).
% 0.21/0.31 thf(f488,definition,(
% 0.21/0.31 spl5_7 <=> ! [X0 : $i] : (sK2 != X0)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition])).
% 0.21/0.31 thf(f489,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK2 != X0)) ) | ~spl5_7),
% 0.21/0.31 inference(avatar_component_clause,[],[f488])).
% 0.21/0.31 thf(f497,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK2) | (sF4 = sK3) | (sK2 != X0) | (f != (^[Y0 : $o]: ($true)))) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f440,f29])).
% 0.21/0.31 thf(f501,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sF4 = sK3) | (sK1 = sF4) | (sK1 != X0) | (f != (^[Y0 : $o]: (Y0)))) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f444,f28])).
% 0.21/0.31 thf(f503,definition,(
% 0.21/0.31 spl5_8 <=> ! [X0 : $i] : (sK1 != X0)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition])).
% 0.21/0.31 thf(f504,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 != X0)) ) | ~spl5_8),
% 0.21/0.31 inference(avatar_component_clause,[],[f503])).
% 0.21/0.31 thf(f516,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: ($false))) | (sF4 = sK2)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f480,f29])).
% 0.21/0.31 thf(f518,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((~ != f) | (sK3 != X0) | (sF4 = sK0)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f482,f27])).
% 0.21/0.31 thf(f529,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK2 != X0) | (f != (^[Y0 : $o]: ($true))) | (sF4 = sK3)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f497,f28])).
% 0.21/0.31 thf(f533,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 = sF4) | (sK1 != X0) | (f != (^[Y0 : $o]: (Y0)))) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f501,f30])).
% 0.21/0.31 thf(f540,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: ($false))) | (sK0 != X0)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f516,f28])).
% 0.21/0.31 thf(f542,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((~ != f) | (sK3 != X0)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f518,f29])).
% 0.21/0.31 thf(f548,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((f != (^[Y0 : $o]: ($true))) | (sK2 != X0)) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f529,f30])).
% 0.21/0.31 thf(f551,plain,(
% 0.21/0.31 ( ! [X0 : $i] : ((sK1 != X0) | (f != (^[Y0 : $o]: (Y0)))) )),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f533,f27])).
% 0.21/0.31 thf(f553,plain,(
% 0.21/0.31 spl5_1 | ~spl5_2),
% 0.21/0.31 inference(avatar_split_clause,[],[f540,f455,f452])).
% 0.21/0.31 thf(f554,plain,(
% 0.21/0.31 spl5_6 | ~spl5_5),
% 0.21/0.31 inference(avatar_split_clause,[],[f542,f467,f475])).
% 0.21/0.31 thf(f555,plain,(
% 0.21/0.31 ~spl5_4 | spl5_7),
% 0.21/0.31 inference(avatar_split_clause,[],[f548,f488,f463])).
% 0.21/0.31 thf(f556,plain,(
% 0.21/0.31 spl5_8 | ~spl5_3),
% 0.21/0.31 inference(avatar_split_clause,[],[f551,f459,f503])).
% 0.21/0.31 thf(f557,plain,(
% 0.21/0.31 (((~ sK6)) != ((f @ sK6))) | spl5_5),
% 0.21/0.31 inference(negative_extensionality,[],[f468])).
% 0.21/0.31 thf(f558,plain,(
% 0.21/0.31 ($true = ((f @ sK6))) | (((~ sK6)) = $true) | spl5_5),
% 0.21/0.31 inference(xor_proxy_clausification,[],[f557])).
% 0.21/0.31 thf(f559,plain,(
% 0.21/0.31 ($false = ((f @ sK6))) | ($false = ((~ sK6))) | spl5_5),
% 0.21/0.31 inference(xor_proxy_clausification,[],[f557])).
% 0.21/0.31 thf(f560,plain,(
% 0.21/0.31 ($true = sK6) | ($false = ((f @ sK6))) | spl5_5),
% 0.21/0.31 inference(not_proxy_clausification,[],[f559])).
% 0.21/0.31 thf(f561,plain,(
% 0.21/0.31 ($true = ((f @ sK6))) | ($false = sK6) | spl5_5),
% 0.21/0.31 inference(not_proxy_clausification,[],[f558])).
% 0.21/0.31 thf(f563,definition,(
% 0.21/0.31 spl5_9 <=> ($false = ((f @ sK6)))),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition])).
% 0.21/0.31 thf(f564,plain,(
% 0.21/0.31 ($false != ((f @ sK6))) | spl5_9),
% 0.21/0.31 inference(avatar_component_clause,[],[f563])).
% 0.21/0.31 thf(f565,plain,(
% 0.21/0.31 ($false = ((f @ sK6))) | ~spl5_9),
% 0.21/0.31 inference(avatar_component_clause,[],[f563])).
% 0.21/0.31 thf(f567,definition,(
% 0.21/0.31 spl5_10 <=> ($true = sK6)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition])).
% 0.21/0.31 thf(f569,plain,(
% 0.21/0.31 ($true = sK6) | ~spl5_10),
% 0.21/0.31 inference(avatar_component_clause,[],[f567])).
% 0.21/0.31 thf(f570,plain,(
% 0.21/0.31 spl5_9 | spl5_10 | spl5_5),
% 0.21/0.31 inference(avatar_split_clause,[],[f560,f467,f567,f563])).
% 0.21/0.31 thf(f572,definition,(
% 0.21/0.31 spl5_11 <=> ($false = sK6)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition])).
% 0.21/0.31 thf(f574,plain,(
% 0.21/0.31 ($false = sK6) | ~spl5_11),
% 0.21/0.31 inference(avatar_component_clause,[],[f572])).
% 0.21/0.31 thf(f576,definition,(
% 0.21/0.31 spl5_12 <=> ($true = ((f @ sK6)))),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition])).
% 0.21/0.31 thf(f578,plain,(
% 0.21/0.31 ($true = ((f @ sK6))) | ~spl5_12),
% 0.21/0.31 inference(avatar_component_clause,[],[f576])).
% 0.21/0.31 thf(f579,plain,(
% 0.21/0.31 spl5_11 | spl5_12 | spl5_5),
% 0.21/0.31 inference(avatar_split_clause,[],[f561,f467,f576,f572])).
% 0.21/0.31 thf(f588,plain,(
% 0.21/0.31 (((f @ $false)) = $false) | (~spl5_9 | ~spl5_11)),
% 0.21/0.31 inference(forward_demodulation,[],[f565,f574])).
% 0.21/0.31 thf(f591,definition,(
% 0.21/0.31 spl5_13 <=> (((f @ $true)) = $true)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_13])],[avatar_definition])).
% 0.21/0.31 thf(f593,plain,(
% 0.21/0.31 (((f @ $true)) = $true) | ~spl5_13),
% 0.21/0.31 inference(avatar_component_clause,[],[f591])).
% 0.21/0.31 thf(f600,plain,(
% 0.21/0.31 $false | ~spl5_1),
% 0.21/0.31 inference(equality_resolution,[],[f453])).
% 0.21/0.31 thf(f603,plain,(
% 0.21/0.31 ~spl5_1),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f600])).
% 0.21/0.31 thf(f610,plain,(
% 0.21/0.31 (((f @ sK8)) != (((^[Y0 : $o]: ($false)) @ sK8))) | spl5_2),
% 0.21/0.31 inference(negative_extensionality,[],[f457])).
% 0.21/0.31 thf(f611,plain,(
% 0.21/0.31 ($true = (((^[Y0 : $o]: ($false)) @ sK8))) | ($true = ((f @ sK8))) | spl5_2),
% 0.21/0.31 inference(xor_proxy_clausification,[],[f610])).
% 0.21/0.31 thf(f614,plain,(
% 0.21/0.31 ($false = $true) | ($true = ((f @ sK8))) | spl5_2),
% 0.21/0.31 inference(beta-eta_normalization,[],[f611])).
% 0.21/0.31 thf(f615,plain,(
% 0.21/0.31 ($true = ((f @ sK8))) | spl5_2),
% 0.21/0.31 inference(trivial_inequality_removal,[],[f614])).
% 0.21/0.31 thf(f616,plain,(
% 0.21/0.31 (((f @ $true)) = $true) | ($false = sK8) | spl5_2),
% 0.21/0.31 inference(constrained_superposition,[],[f615,f21])).
% 0.21/0.31 thf(f623,plain,(
% 0.21/0.31 ((((^[Y0 : $o]: (Y0)) @ sK10)) != ((f @ sK10))) | spl5_3),
% 0.21/0.31 inference(negative_extensionality,[],[f460])).
% 0.21/0.31 thf(f624,plain,(
% 0.21/0.31 ($true = (((^[Y0 : $o]: (Y0)) @ sK10))) | ($true = ((f @ sK10))) | spl5_3),
% 0.21/0.31 inference(xor_proxy_clausification,[],[f623])).
% 0.21/0.31 thf(f625,plain,(
% 0.21/0.31 ($false = ((f @ sK10))) | ($false = (((^[Y0 : $o]: (Y0)) @ sK10))) | spl5_3),
% 0.21/0.31 inference(xor_proxy_clausification,[],[f623])).
% 0.21/0.31 thf(f626,plain,(
% 0.21/0.31 (sK10 = $false) | ($false = ((f @ sK10))) | spl5_3),
% 0.21/0.31 inference(beta-eta_normalization,[],[f625])).
% 0.21/0.31 thf(f627,plain,(
% 0.21/0.31 (sK10 = $true) | ($true = ((f @ sK10))) | spl5_3),
% 0.21/0.31 inference(beta-eta_normalization,[],[f624])).
% 0.21/0.31 thf(f629,definition,(
% 0.21/0.31 spl5_15 <=> ($false = ((f @ sK10)))),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_15])],[avatar_definition])).
% 0.21/0.31 thf(f630,plain,(
% 0.21/0.31 ($false != ((f @ sK10))) | spl5_15),
% 0.21/0.31 inference(avatar_component_clause,[],[f629])).
% 0.21/0.31 thf(f631,plain,(
% 0.21/0.31 ($false = ((f @ sK10))) | ~spl5_15),
% 0.21/0.31 inference(avatar_component_clause,[],[f629])).
% 0.21/0.31 thf(f633,definition,(
% 0.21/0.31 spl5_16 <=> (sK10 = $false)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_16])],[avatar_definition])).
% 0.21/0.31 thf(f635,plain,(
% 0.21/0.31 (sK10 = $false) | ~spl5_16),
% 0.21/0.31 inference(avatar_component_clause,[],[f633])).
% 0.21/0.31 thf(f636,plain,(
% 0.21/0.31 spl5_15 | spl5_16 | spl5_3),
% 0.21/0.31 inference(avatar_split_clause,[],[f626,f459,f633,f629])).
% 0.21/0.31 thf(f638,definition,(
% 0.21/0.31 spl5_17 <=> ($true = ((f @ sK10)))),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_17])],[avatar_definition])).
% 0.21/0.31 thf(f640,plain,(
% 0.21/0.31 ($true = ((f @ sK10))) | ~spl5_17),
% 0.21/0.31 inference(avatar_component_clause,[],[f638])).
% 0.21/0.31 thf(f642,definition,(
% 0.21/0.31 spl5_18 <=> (sK10 = $true)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_18])],[avatar_definition])).
% 0.21/0.31 thf(f644,plain,(
% 0.21/0.31 (sK10 = $true) | ~spl5_18),
% 0.21/0.31 inference(avatar_component_clause,[],[f642])).
% 0.21/0.31 thf(f645,plain,(
% 0.21/0.31 spl5_17 | spl5_18 | spl5_3),
% 0.21/0.31 inference(avatar_split_clause,[],[f627,f459,f642,f638])).
% 0.21/0.31 thf(f647,plain,(
% 0.21/0.31 $false | ~spl5_8),
% 0.21/0.31 inference(equality_resolution,[],[f504])).
% 0.21/0.31 thf(f650,plain,(
% 0.21/0.31 ~spl5_8),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f647])).
% 0.21/0.31 thf(f666,definition,(
% 0.21/0.31 spl5_19 <=> ($false = sK8)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_19])],[avatar_definition])).
% 0.21/0.31 thf(f668,plain,(
% 0.21/0.31 ($false = sK8) | ~spl5_19),
% 0.21/0.31 inference(avatar_component_clause,[],[f666])).
% 0.21/0.31 thf(f669,plain,(
% 0.21/0.31 spl5_19 | spl5_13 | spl5_2),
% 0.21/0.31 inference(avatar_split_clause,[],[f616,f455,f591,f666])).
% 0.21/0.31 thf(f671,definition,(
% 0.21/0.31 spl5_20 <=> (((f @ $true)) = $false)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_20])],[avatar_definition])).
% 0.21/0.31 thf(f673,plain,(
% 0.21/0.31 (((f @ $true)) = $false) | ~spl5_20),
% 0.21/0.31 inference(avatar_component_clause,[],[f671])).
% 0.21/0.31 thf(f680,plain,(
% 0.21/0.31 (sK2 != sK2) | ~spl5_7),
% 0.21/0.31 inference(imitation,[],[f489])).
% 0.21/0.31 thf(f683,plain,(
% 0.21/0.31 $false | ~spl5_7),
% 0.21/0.31 inference(trivial_inequality_removal,[],[f680])).
% 0.21/0.31 thf(f684,plain,(
% 0.21/0.31 ~spl5_7),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f683])).
% 0.21/0.31 thf(f692,plain,(
% 0.21/0.31 ((((^[Y0 : $o]: ($true)) @ sK11)) != ((f @ sK11))) | spl5_4),
% 0.21/0.31 inference(negative_extensionality,[],[f464])).
% 0.21/0.31 thf(f694,plain,(
% 0.21/0.31 ($false = ((f @ sK11))) | ($false = (((^[Y0 : $o]: ($true)) @ sK11))) | spl5_4),
% 0.21/0.31 inference(xor_proxy_clausification,[],[f692])).
% 0.21/0.31 thf(f695,plain,(
% 0.21/0.31 ($false = $true) | ($false = ((f @ sK11))) | spl5_4),
% 0.21/0.31 inference(beta-eta_normalization,[],[f694])).
% 0.21/0.31 thf(f696,plain,(
% 0.21/0.31 ($false = ((f @ sK11))) | spl5_4),
% 0.21/0.31 inference(trivial_inequality_removal,[],[f695])).
% 0.21/0.31 thf(f698,plain,(
% 0.21/0.31 ($false = $true) | (~spl5_15 | ~spl5_17)),
% 0.21/0.31 inference(forward_demodulation,[],[f640,f631])).
% 0.21/0.31 thf(f699,plain,(
% 0.21/0.31 $false | (~spl5_15 | ~spl5_17)),
% 0.21/0.31 inference(trivial_inequality_removal,[],[f698])).
% 0.21/0.31 thf(f700,plain,(
% 0.21/0.31 ~spl5_15 | ~spl5_17),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f699])).
% 0.21/0.31 thf(f707,plain,(
% 0.21/0.31 (((f @ $true)) = $false) | (~spl5_15 | ~spl5_18)),
% 0.21/0.31 inference(constrained_superposition,[],[f631,f644])).
% 0.21/0.31 thf(f708,plain,(
% 0.21/0.31 spl5_20 | ~spl5_15 | ~spl5_18),
% 0.21/0.31 inference(avatar_split_clause,[],[f707,f642,f629,f671])).
% 0.21/0.31 thf(f710,plain,(
% 0.21/0.31 (((f @ $false)) = $true) | (spl5_2 | ~spl5_19)),
% 0.21/0.31 inference(constrained_superposition,[],[f615,f668])).
% 0.21/0.31 thf(f712,plain,(
% 0.21/0.31 ($false = $true) | (spl5_2 | ~spl5_9 | ~spl5_11 | ~spl5_19)),
% 0.21/0.31 inference(forward_demodulation,[],[f710,f588])).
% 0.21/0.31 thf(f713,plain,(
% 0.21/0.31 $false | (spl5_2 | ~spl5_9 | ~spl5_11 | ~spl5_19)),
% 0.21/0.31 inference(trivial_inequality_removal,[],[f712])).
% 0.21/0.31 thf(f714,plain,(
% 0.21/0.31 spl5_2 | ~spl5_9 | ~spl5_11 | ~spl5_19),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f713])).
% 0.21/0.31 thf(f720,plain,(
% 0.21/0.31 $false | ~spl5_6),
% 0.21/0.31 inference(equality_resolution,[],[f476])).
% 0.21/0.31 thf(f723,plain,(
% 0.21/0.31 ~spl5_6),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f720])).
% 0.21/0.31 thf(f780,plain,(
% 0.21/0.31 ($false = $true) | (~spl5_9 | ~spl5_12)),
% 0.21/0.31 inference(forward_demodulation,[],[f578,f565])).
% 0.21/0.31 thf(f781,plain,(
% 0.21/0.31 $false | (~spl5_9 | ~spl5_12)),
% 0.21/0.31 inference(trivial_inequality_removal,[],[f780])).
% 0.21/0.31 thf(f782,plain,(
% 0.21/0.31 ~spl5_9 | ~spl5_12),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f781])).
% 0.21/0.31 thf(f796,plain,(
% 0.21/0.31 (((f @ $false)) != $false) | (spl5_15 | ~spl5_16)),
% 0.21/0.31 inference(forward_demodulation,[],[f630,f635])).
% 0.21/0.31 thf(f798,plain,(
% 0.21/0.31 ($false = sK11) | (((f @ $true)) = $false) | spl5_4),
% 0.21/0.31 inference(constrained_superposition,[],[f696,f21])).
% 0.21/0.31 thf(f802,definition,(
% 0.21/0.31 spl5_30 <=> ($false = sK11)),
% 0.21/0.31 introduced(definition,[new_symbols(definition,[spl5_30])],[avatar_definition])).
% 0.21/0.31 thf(f804,plain,(
% 0.21/0.31 ($false = sK11) | ~spl5_30),
% 0.21/0.31 inference(avatar_component_clause,[],[f802])).
% 0.21/0.31 thf(f805,plain,(
% 0.21/0.31 spl5_20 | spl5_30 | spl5_4),
% 0.21/0.31 inference(avatar_split_clause,[],[f798,f463,f802,f671])).
% 0.21/0.31 thf(f820,plain,(
% 0.21/0.31 (((f @ $false)) = $false) | (spl5_4 | ~spl5_30)),
% 0.21/0.31 inference(constrained_superposition,[],[f696,f804])).
% 0.21/0.31 thf(f822,plain,(
% 0.21/0.31 $false | (spl5_4 | spl5_15 | ~spl5_16 | ~spl5_30)),
% 0.21/0.31 inference(forward_subsumption_resolution,[],[f820,f796])).
% 0.21/0.31 thf(f823,plain,(
% 0.21/0.31 spl5_4 | spl5_15 | ~spl5_16 | ~spl5_30),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f822])).
% 0.21/0.31 thf(f833,plain,(
% 0.21/0.31 ($false = $true) | (~spl5_13 | ~spl5_20)),
% 0.21/0.31 inference(forward_demodulation,[],[f673,f593])).
% 0.21/0.31 thf(f834,plain,(
% 0.21/0.31 $false | (~spl5_13 | ~spl5_20)),
% 0.21/0.31 inference(trivial_inequality_removal,[],[f833])).
% 0.21/0.31 thf(f835,plain,(
% 0.21/0.31 ~spl5_13 | ~spl5_20),
% 0.21/0.31 inference(avatar_contradiction_clause,[],[f834])).
% 0.21/0.31 thf(f848,plain,(
% 0.21/0.31 (((f @ $true)) != $false) | (spl5_9 | ~spl5_10)),
% 0.21/0.31 inference(forward_demodulation,[],[f564,f569])).
% 0.21/0.31 thf(f849,plain,(
% 0.21/0.31 ~spl5_20 | spl5_9 | ~spl5_10),
% 0.21/0.31 inference(avatar_split_clause,[],[f848,f567,f563,f671])).
% 0.21/0.31 cnf(s29, plain, spl5_1 | ~spl5_2, inference(sat_conversion,[],[f553])).
% 0.21/0.31 cnf(s30, plain, ~spl5_5 | spl5_6, inference(sat_conversion,[],[f554])).
% 0.21/0.31 cnf(s31, plain, ~spl5_4 | spl5_7, inference(sat_conversion,[],[f555])).
% 0.21/0.31 cnf(s32, plain, ~spl5_3 | spl5_8, inference(sat_conversion,[],[f556])).
% 0.21/0.31 cnf(s33, plain, spl5_5 | spl5_9 | spl5_10, inference(sat_conversion,[],[f570])).
% 0.21/0.31 cnf(s34, plain, spl5_5 | spl5_11 | spl5_12, inference(sat_conversion,[],[f579])).
% 0.21/0.31 cnf(s37, plain, ~spl5_1, inference(sat_conversion,[],[f603])).
% 0.21/0.31 cnf(s38, plain, spl5_3 | spl5_15 | spl5_16, inference(sat_conversion,[],[f636])).
% 0.21/0.31 cnf(s39, plain, spl5_3 | spl5_17 | spl5_18, inference(sat_conversion,[],[f645])).
% 0.21/0.31 cnf(s41, plain, ~spl5_8, inference(sat_conversion,[],[f650])).
% 0.21/0.31 cnf(s43, plain, spl5_2 | spl5_13 | spl5_19, inference(sat_conversion,[],[f669])).
% 0.21/0.31 cnf(s47, plain, ~spl5_7, inference(sat_conversion,[],[f684])).
% 0.21/0.31 cnf(s48, plain, ~spl5_15 | ~spl5_17, inference(sat_conversion,[],[f700])).
% 0.21/0.31 cnf(s50, plain, ~spl5_15 | ~spl5_18 | spl5_20, inference(sat_conversion,[],[f708])).
% 0.21/0.31 cnf(s51, plain, spl5_2 | ~spl5_9 | ~spl5_11 | ~spl5_19, inference(sat_conversion,[],[f714])).
% 0.21/0.31 cnf(s54, plain, ~spl5_6, inference(sat_conversion,[],[f723])).
% 0.21/0.31 cnf(s60, plain, ~spl5_9 | ~spl5_12, inference(sat_conversion,[],[f782])).
% 0.21/0.31 cnf(s63, plain, spl5_4 | spl5_20 | spl5_30, inference(sat_conversion,[],[f805])).
% 0.21/0.31 cnf(s67, plain, spl5_4 | spl5_15 | ~spl5_16 | ~spl5_30, inference(sat_conversion,[],[f823])).
% 0.21/0.31 cnf(s70, plain, ~spl5_13 | ~spl5_20, inference(sat_conversion,[],[f835])).
% 0.21/0.31 cnf(s72, plain, spl5_9 | ~spl5_10 | ~spl5_20, inference(sat_conversion,[],[f849])).
% 0.21/0.31 cnf(s73, plain, ~spl5_3, inference(rat,[],[s32,s41])).
% 0.21/0.31 cnf(s74, plain, ~spl5_4, inference(rat,[],[s31,s47])).
% 0.21/0.31 cnf(s75, plain, ~spl5_5, inference(rat,[],[s30,s54])).
% 0.21/0.31 cnf(s76, plain, ~spl5_2, inference(rat,[],[s29,s37])).
% 0.21/0.31 cnf(s77, plain, spl5_15 | ~spl5_30, inference(rat,[],[s38,s67,s74,s73])).
% 0.21/0.31 cnf(s78, plain, ~spl5_15 | spl5_20, inference(rat,[],[s39,s48,s50,s73])).
% 0.21/0.31 cnf(s79, plain, spl5_20, inference(rat,[],[s78,s77,s63,s74])).
% 0.21/0.31 cnf(s80, plain, ~spl5_13, inference(rat,[],[s70,s79])).
% 0.21/0.31 cnf(s81, plain, spl5_19, inference(rat,[],[s43,s76,s80])).
% 0.21/0.31 cnf(s83, plain, spl5_9, inference(rat,[],[s72,s33,s79,s75])).
% 0.21/0.31 cnf(s84, plain, ~spl5_12, inference(rat,[],[s60,s83])).
% 0.21/0.31 cnf(s85, plain, ~spl5_11, inference(rat,[],[s51,s81,s76,s83])).
% 0.21/0.31 cnf(s86, plain, $false, inference(rat,[],[s34,s75,s84,s85])).
% 0.21/0.31 thf(f850,plain,(
% 0.21/0.31 $false),
% 0.21/0.31 inference(avatar_sat_refutation,[],[s86])).
% 0.21/0.31 % SZS output end Proof for theBenchmark
% 0.21/0.31 % (382557)------------------------------
% 0.21/0.31 % (382557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.31 % (382557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.31 % (382557)CaDiCaL version: 2.1.3
% 0.21/0.31 % (382557)Termination reason: Refutation
% 0.21/0.31 % (382557)Time elapsed: 0.018 s
% 0.21/0.31 % (382557)Peak memory usage: 13 MB
% 0.21/0.31 % (382557)Instructions burned: 32 (million)
% 0.21/0.31 % (382523)Success in time 0.068 s
% 0.21/0.31 % Vampire exiting
%------------------------------------------------------------------------------