%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV089^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:37:37 AM UTC 2026
% Result : Theorem 0.23s 0.35s
% Output : Refutation 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV089^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n009.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.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 15:07:15 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.08/0.25 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.23/0.35 % (4116373)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.23/0.35 % (4116384)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.23/0.35 % (4116384)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.23/0.35 % (4116383)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1336895847:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.23/0.35 % (4116382)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1736409382:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.23/0.35 % (4116380)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=622377707:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.23/0.35 % (4116379)lrs+10_16_si=on:nwc=1.5:random_seed=4160968730:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.23/0.35 % (4116381)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=1124084797: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.23/0.35 % (4116378)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3737662415:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.23/0.35 % (4116384)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=2481291141:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.23/0.35 % (4116380)Instruction limit reached!
% 0.23/0.35 % (4116380)------------------------------
% 0.23/0.35 % (4116380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.35 % (4116380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.35 % (4116380)CaDiCaL version: 2.1.3
% 0.23/0.35 % (4116380)Termination reason: Instruction limit
% 0.23/0.35 % (4116380)Termination phase: Saturation
% 0.23/0.35 % (4116380)Time elapsed: 0.003 s
% 0.23/0.35 % (4116380)Peak memory usage: 12 MB
% 0.23/0.35 % (4116380)Instructions burned: 4 (million)
% 0.23/0.35 % (4116379)Instruction limit reached!
% 0.23/0.35 % (4116379)------------------------------
% 0.23/0.35 % (4116379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.35 % (4116379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.35 % (4116379)CaDiCaL version: 2.1.3
% 0.23/0.35 % (4116379)Termination reason: Instruction limit
% 0.23/0.35 % (4116379)Termination phase: Saturation
% 0.23/0.35 % (4116379)Time elapsed: 0.012 s
% 0.23/0.35 % (4116379)Peak memory usage: 12 MB
% 0.23/0.35 % (4116379)Instructions burned: 20 (million)
% 0.23/0.35 % (4116382)Instruction limit reached!
% 0.23/0.35 % (4116382)------------------------------
% 0.23/0.35 % (4116382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.35 % (4116382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.35 % (4116382)CaDiCaL version: 2.1.3
% 0.23/0.35 % (4116382)Termination reason: Instruction limit
% 0.23/0.35 % (4116382)Termination phase: Saturation
% 0.23/0.35 % (4116382)Time elapsed: 0.014 s
% 0.23/0.35 % (4116382)Peak memory usage: 11 MB
% 0.23/0.35 % (4116382)Instructions burned: 24 (million)
% 0.23/0.35 % (4116392)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2975350838:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.23/0.35 % (4116392)Instruction limit reached!
% 0.23/0.35 % (4116392)------------------------------
% 0.23/0.35 % (4116392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.35 % (4116392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.35 % (4116392)CaDiCaL version: 2.1.3
% 0.23/0.35 % (4116392)Termination reason: Instruction limit
% 0.23/0.35 % (4116392)Termination phase: Saturation
% 0.23/0.35 % (4116392)Time elapsed: 0.003 s
% 0.23/0.35 % (4116392)Peak memory usage: 12 MB
% 0.23/0.35 % (4116392)Instructions burned: 5 (million)
% 0.23/0.35 % (4116394)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.23/0.35 % (4116393)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=384158017:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.23/0.35 % (4116394)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4098833352:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.23/0.35 % (4116393)Instruction limit reached!
% 0.23/0.35 % (4116393)------------------------------
% 0.23/0.35 % (4116393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.35 % (4116393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.35 % (4116393)CaDiCaL version: 2.1.3
% 0.23/0.35 % (4116393)Termination reason: Instruction limit
% 0.23/0.35 % (4116393)Termination phase: Saturation
% 0.23/0.35 % (4116393)Time elapsed: 0.004 s
% 0.23/0.35 % (4116393)Peak memory usage: 12 MB
% 0.23/0.35 % (4116393)Instructions burned: 6 (million)
% 0.23/0.35 % (4116394)Instruction limit reached!
% 0.23/0.35 % (4116394)------------------------------
% 0.23/0.35 % (4116394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.35 % (4116394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.35 % (4116394)CaDiCaL version: 2.1.3
% 0.23/0.35 % (4116394)Termination reason: Instruction limit
% 0.23/0.35 % (4116394)Termination phase: Saturation
% 0.23/0.35 % (4116394)Time elapsed: 0.004 s
% 0.23/0.35 % (4116394)Peak memory usage: 12 MB
% 0.23/0.35 % (4116394)Instructions burned: 8 (million)
% 0.23/0.35 % (4116383)Instruction limit reached!
% 0.23/0.35 % (4116383)------------------------------
% 0.23/0.35 % (4116383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.35 % (4116383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.35 % (4116383)CaDiCaL version: 2.1.3
% 0.23/0.35 % (4116383)Termination reason: Instruction limit
% 0.23/0.35 % (4116383)Termination phase: Saturation
% 0.23/0.35 % (4116383)Time elapsed: 0.039 s
% 0.23/0.35 % (4116383)Peak memory usage: 12 MB
% 0.23/0.35 % (4116383)Instructions burned: 76 (million)
% 0.23/0.35 % (4116378) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4116373-4116378"...
% 0.23/0.35 % (4116396)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2341055589:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.23/0.35 % (4116399)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.23/0.35 % (4116399)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.23/0.35 % (4116378)...printing done.
% 0.23/0.35 % (4116396)Instruction limit reached!
% 0.23/0.35 % (4116396)------------------------------
% 0.23/0.35 % (4116396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.35 % (4116396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.35 % (4116396)CaDiCaL version: 2.1.3
% 0.23/0.35 % (4116396)Termination reason: Instruction limit
% 0.23/0.35 % (4116396)Termination phase: Saturation
% 0.23/0.35 % (4116396)Time elapsed: 0.008 s
% 0.23/0.35 % (4116396)Peak memory usage: 12 MB
% 0.23/0.35 % (4116396)Instructions burned: 14 (million)
% 0.23/0.35 % (4116378)Refutation found. Thanks to Tanya!
% 0.23/0.35 % SZS status Theorem for theBenchmark
% 0.23/0.35 % SZS output start Proof for theBenchmark
% 0.23/0.35 thf(type_def_5, type, a: $tType).
% 0.23/0.35 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.23/0.35 thf(func_def_3, type, vAND: ($o > $o > $o)).
% 0.23/0.35 thf(func_def_4, type, db0: !>[X0: $tType]:(X0)).
% 0.23/0.35 thf(func_def_5, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.23/0.35 thf(func_def_6, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.23/0.35 thf(func_def_7, type, db1: !>[X0: $tType]:(X0)).
% 0.23/0.35 thf(func_def_8, type, sK0: (a > $o)).
% 0.23/0.35 thf(func_def_9, type, sK1: (a > $o)).
% 0.23/0.35 thf(func_def_10, type, sK2: ((a > a) > a)).
% 0.23/0.35 thf(func_def_11, type, sK3: ((a > a) > a)).
% 0.23/0.35 thf(func_def_12, type, sK4: (a > a)).
% 0.23/0.35 thf(func_def_13, type, sK5: (a > a)).
% 0.23/0.35 thf(func_def_14, type, sK6: (a > (a > a) > a)).
% 0.23/0.35 thf(func_def_15, type, sK7: (a > (a > a) > a)).
% 0.23/0.35 thf(f1,conjecture,(
% 0.23/0.35 ! [X1 : (a > $o),X0 : (a > $o)] : (? [X2 : (a > a)] : (! [X4 : a] : ((X1 @ X4) => ? [X5 : a] : ((^[X3 : a] : ((X4 = ((X2 @ X3))) & (X0 @ X3))) = (((^[X0 : a, X1 : a] : ((X0 = X1))) @ X5)))) & ! [X3 : a] : ((X0 @ X3) => (X1 @ (X2 @ X3)))) => ? [X2 : (a > a)] : (! [X4 : a] : ((X0 @ X4) => ? [X6 : a] : ((^[X3 : a] : ((X1 @ X3) & (X4 = ((X2 @ X3))))) = (((^[X0 : a, X1 : a] : ((X0 = X1))) @ X6)))) & ! [X3 : a] : ((X1 @ X3) => (X0 @ (X2 @ X3)))))),
% 0.23/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cEQP_1B_pme)).
% 0.23/0.35 thf(f2,negated_conjecture,(
% 0.23/0.35 ~ ! [X1 : (a > $o),X0 : (a > $o)] : (? [X2 : (a > a)] : (! [X4 : a] : ((X1 @ X4) => ? [X5 : a] : ((^[X3 : a] : ((X4 = ((X2 @ X3))) & (X0 @ X3))) = (((^[X0 : a, X1 : a] : ((X0 = X1))) @ X5)))) & ! [X3 : a] : ((X0 @ X3) => (X1 @ (X2 @ X3)))) => ? [X2 : (a > a)] : (! [X4 : a] : ((X0 @ X4) => ? [X6 : a] : ((^[X3 : a] : ((X1 @ X3) & (X4 = ((X2 @ X3))))) = (((^[X0 : a, X1 : a] : ((X0 = X1))) @ X6)))) & ! [X3 : a] : ((X1 @ X3) => (X0 @ (X2 @ X3)))))),
% 0.23/0.35 inference(negated_conjecture,[status(cth)],[f1])).
% 0.23/0.35 thf(f3,plain,(
% 0.23/0.35 ~ ! [X0 : (a > $o),X1 : (a > $o)] : (? [X2 : (a > a)] : (! [X3 : a] : ((X0 @ X3) => ? [X4 : a] : ((^[X5 : a] : ((((X2 @ X5)) = X3) & (X1 @ X5))) = (((^[X6 : a, X7 : a] : ((X6 = X7))) @ X4)))) & ! [X8 : a] : ((X1 @ X8) => (X0 @ (X2 @ X8)))) => ? [X9 : (a > a)] : (! [X10 : a] : ((X1 @ X10) => ? [X11 : a] : ((^[X12 : a] : ((X0 @ X12) & (((X9 @ X12)) = X10))) = (((^[X13 : a, X14 : a] : ((X13 = X14))) @ X11)))) & ! [X15 : a] : ((X0 @ X15) => (X1 @ (X9 @ X15)))))),
% 0.23/0.35 inference(rectify,[],[f2])).
% 0.23/0.35 thf(f4,plain,(
% 0.23/0.35 ~ ! [X0 : (a > $o),X1 : (a > $o)] : (? [X2 : (a > a)] : (! [X3 : a] : ((((X0 @ X3)) = $true) => ? [X4 : a] : ((^[Y0 : a]: ((X1 @ Y0) & ((X2 @ Y0) = X3))) = (((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ X4)))) & ! [X8 : a] : ((((X1 @ X8)) = $true) => (((X0 @ (X2 @ X8))) = $true))) => ? [X9 : (a > a)] : (! [X10 : a] : ((((X1 @ X10)) = $true) => ? [X11 : a] : ((^[Y0 : a]: (((X9 @ Y0) = X10) & (X0 @ Y0))) = (((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ X11)))) & ! [X15 : a] : ((((X0 @ X15)) = $true) => (((X1 @ (X9 @ X15))) = $true))))),
% 0.23/0.35 inference(fool_elimination,[],[f3])).
% 0.23/0.35 thf(f5,plain,(
% 0.23/0.35 ~ ! [X1 : (a > $o),X0 : (a > $o)] : (? [X2 : (a > a)] : (! [X3 : a] : ((((X0 @ X3)) = $true) => ? [X4 : a] : ((^[Y0 : a]: ((X1 @ Y0) & ((X2 @ Y0) = X3))) = (((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ X4)))) & ! [X5 : a] : ((((X1 @ X5)) = $true) => (((X0 @ (X2 @ X5))) = $true))) => ? [X6 : (a > a)] : (! [X7 : a] : (($true = ((X1 @ X7))) => ? [X8 : a] : ((^[Y0 : a]: (((X6 @ Y0) = X7) & (X0 @ Y0))) = (((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ X8)))) & ! [X9 : a] : (($true = ((X0 @ X9))) => ($true = ((X1 @ (X6 @ X9)))))))),
% 0.23/0.35 inference(rectify,[],[f4])).
% 0.23/0.35 thf(f6,plain,(
% 0.23/0.35 ? [X0 : (a > $o),X1 : (a > $o)] : (! [X6 : (a > a)] : (? [X7 : a] : (! [X8 : a] : ((^[Y0 : a]: (((X6 @ Y0) = X7) & (X0 @ Y0))) != (((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ X8))) & ($true = ((X1 @ X7)))) | ? [X9 : a] : (($true != ((X1 @ (X6 @ X9)))) & ($true = ((X0 @ X9))))) & ? [X2 : (a > a)] : (! [X3 : a] : (? [X4 : a] : ((^[Y0 : a]: ((X1 @ Y0) & ((X2 @ Y0) = X3))) = (((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ X4))) | (((X0 @ X3)) != $true)) & ! [X5 : a] : ((((X1 @ X5)) != $true) | (((X0 @ (X2 @ X5))) = $true))))),
% 0.23/0.35 inference(ennf_transformation,[],[f5])).
% 0.23/0.35 thf(f7,plain,(
% 0.23/0.35 ? [X0 : (a > $o),X1 : (a > $o)] : (! [X2 : (a > a)] : (? [X3 : a] : (! [X4 : a] : ((^[Y0 : a]: (((X2 @ Y0) = X3) & (X0 @ Y0))) != (((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ X4))) & (((X1 @ X3)) = $true)) | ? [X5 : a] : ((((X1 @ (X2 @ X5))) != $true) & ($true = ((X0 @ X5))))) & ? [X6 : (a > a)] : (! [X7 : a] : (? [X8 : a] : ((((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ X8)) = (^[Y0 : a]: ((X1 @ Y0) & ((X6 @ Y0) = X7)))) | ($true != ((X0 @ X7)))) & ! [X9 : a] : ((((X1 @ X9)) != $true) | (((X0 @ (X6 @ X9))) = $true))))),
% 0.23/0.35 inference(rectify,[],[f6])).
% 0.23/0.35 thf(f8,plain,(
% 0.23/0.35 ! [X2 : (a > a)] : ((! [X4 : a] : ((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) != (((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ X4))) & ($true = ((sK1 @ (sK2 @ X2))))) | ((((sK1 @ (X2 @ (sK3 @ X2)))) != $true) & (((sK0 @ (sK3 @ X2))) = $true))) & (! [X7 : a] : (((((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ (sK5 @ X7))) = (^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = X7)))) | (((sK0 @ X7)) != $true)) & ! [X9 : a] : ((((sK1 @ X9)) != $true) | ($true = ((sK0 @ (sK4 @ X9))))))),
% 0.23/0.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,vAPP,vAPP,sK4,vAPP]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X8,sK5 @ X7),skolemize(X8,sK5 @ X7),skolemize(X6,sK4),skolemize(X8,sK5 @ X7)],[f7])).
% 0.23/0.35 thf(f9,plain,(
% 0.23/0.35 ( ! [X9 : a] : ((((sK1 @ X9)) != $true) | ($true = ((sK0 @ (sK4 @ X9))))) )),
% 0.23/0.35 inference(cnf_transformation,[],[f8])).
% 0.23/0.35 thf(f10,plain,(
% 0.23/0.35 ( ! [X7 : a] : (((((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ (sK5 @ X7))) = (^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = X7)))) | (((sK0 @ X7)) != $true)) )),
% 0.23/0.35 inference(cnf_transformation,[],[f8])).
% 0.23/0.35 thf(f11,plain,(
% 0.23/0.35 ( ! [X2 : (a > a)] : (($true = ((sK1 @ (sK2 @ X2)))) | (((sK0 @ (sK3 @ X2))) = $true)) )),
% 0.23/0.35 inference(cnf_transformation,[],[f8])).
% 0.23/0.35 thf(f12,plain,(
% 0.23/0.35 ( ! [X2 : (a > a)] : ((((sK1 @ (X2 @ (sK3 @ X2)))) != $true) | ($true = ((sK1 @ (sK2 @ X2))))) )),
% 0.23/0.35 inference(cnf_transformation,[],[f8])).
% 0.23/0.35 thf(f13,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : (((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) != (((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ X4))) | (((sK0 @ (sK3 @ X2))) = $true)) )),
% 0.23/0.35 inference(cnf_transformation,[],[f8])).
% 0.23/0.35 thf(f14,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK1 @ (X2 @ (sK3 @ X2)))) != $true) | ((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) != (((^[Y0 : a]: ((^[Y1 : a]: (Y0 = Y1)))) @ X4)))) )),
% 0.23/0.35 inference(cnf_transformation,[],[f8])).
% 0.23/0.35 thf(f17,plain,(
% 0.23/0.35 ( ! [X7 : a] : ((((sK0 @ X7)) != $true) | (((= @ (sK5 @ X7))) = (^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = X7))))) )),
% 0.23/0.35 inference(beta-eta_normalization,[],[f10])).
% 0.23/0.35 thf(f18,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : (((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) != ((= @ X4))) | (((sK0 @ (sK3 @ X2))) = $true)) )),
% 0.23/0.35 inference(beta-eta_normalization,[],[f13])).
% 0.23/0.35 thf(f19,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : (((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) != ((= @ X4))) | (((sK1 @ (X2 @ (sK3 @ X2)))) != $true)) )),
% 0.23/0.35 inference(beta-eta_normalization,[],[f14])).
% 0.23/0.35 thf(f20,plain,(
% 0.23/0.35 ( ! [X0 : (a > a)] : (($true != $true) | (((sK0 @ (sK4 @ (sK2 @ X0)))) = $true) | ($true = ((sK0 @ (sK3 @ X0))))) )),
% 0.23/0.35 inference(constrained_superposition,[],[f9,f11])).
% 0.23/0.35 thf(f21,plain,(
% 0.23/0.35 ( ! [X0 : (a > a)] : ((((sK0 @ (sK4 @ (sK2 @ X0)))) = $true) | ($true = ((sK0 @ (sK3 @ X0))))) )),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f20])).
% 0.23/0.35 thf(f22,plain,(
% 0.23/0.35 ( ! [X0 : (a > a)] : (($true != $true) | ($true = ((sK0 @ (sK3 @ X0)))) | ((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK4 @ (sK2 @ X0))))) = ((= @ (sK5 @ (sK4 @ (sK2 @ X0))))))) )),
% 0.23/0.35 inference(constrained_superposition,[],[f17,f21])).
% 0.23/0.35 thf(f23,plain,(
% 0.23/0.35 ( ! [X0 : (a > a)] : (((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK4 @ (sK2 @ X0))))) = ((= @ (sK5 @ (sK4 @ (sK2 @ X0)))))) | ($true = ((sK0 @ (sK3 @ X0))))) )),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f22])).
% 0.23/0.35 thf(f24,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK0 @ (sK3 @ X2))) = $true) | (((X4 = (sK6 @ X4 @ X2))) != (((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) @ (sK6 @ X4 @ X2))))) )),
% 0.23/0.35 inference(negative_extensionality,[],[f18])).
% 0.23/0.35 thf(f25,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK0 @ (sK3 @ X2))) = $true) | ((((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) @ (sK6 @ X4 @ X2))) = $true) | (((X4 = (sK6 @ X4 @ X2))) = $true)) )),
% 0.23/0.35 inference(xor_proxy_clausification,[],[f24])).
% 0.23/0.35 thf(f26,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((X4 = (sK6 @ X4 @ X2))) = $false) | ((((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) @ (sK6 @ X4 @ X2))) = $false) | (((sK0 @ (sK3 @ X2))) = $true)) )),
% 0.23/0.35 inference(xor_proxy_clausification,[],[f24])).
% 0.23/0.35 thf(f27,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : (((((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) @ (sK6 @ X4 @ X2))) = $false) | (((sK0 @ (sK3 @ X2))) = $true) | (((sK6 @ X4 @ X2)) != X4)) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f26])).
% 0.23/0.35 thf(f28,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK6 @ X4 @ X2)) != X4) | (((sK0 @ (sK3 @ X2))) = $true) | (((((X2 @ (sK6 @ X4 @ X2)) = (sK2 @ X2)) & (sK0 @ (sK6 @ X4 @ X2)))) = $false)) )),
% 0.23/0.35 inference(beta-eta_normalization,[],[f27])).
% 0.23/0.35 thf(f29,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK0 @ (sK3 @ X2))) = $true) | (((sK0 @ (sK6 @ X4 @ X2))) = $false) | ($false = (((X2 @ (sK6 @ X4 @ X2)) = (sK2 @ X2)))) | (((sK6 @ X4 @ X2)) != X4)) )),
% 0.23/0.35 inference(and_proxy_clausification,[],[f28])).
% 0.23/0.35 thf(f30,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((X2 @ (sK6 @ X4 @ X2))) != ((sK2 @ X2))) | (((sK0 @ (sK6 @ X4 @ X2))) = $false) | (((sK0 @ (sK3 @ X2))) = $true) | (((sK6 @ X4 @ X2)) != X4)) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f29])).
% 0.23/0.35 thf(f31,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK0 @ (sK3 @ X2))) = $true) | (((sK6 @ X4 @ X2)) = X4) | ((((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) @ (sK6 @ X4 @ X2))) = $true)) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f25])).
% 0.23/0.35 thf(f32,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((((X2 @ (sK6 @ X4 @ X2)) = (sK2 @ X2)) & (sK0 @ (sK6 @ X4 @ X2)))) = $true) | (((sK0 @ (sK3 @ X2))) = $true) | (((sK6 @ X4 @ X2)) = X4)) )),
% 0.23/0.35 inference(beta-eta_normalization,[],[f31])).
% 0.23/0.35 thf(f33,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK0 @ (sK6 @ X4 @ X2))) = $true) | (((sK6 @ X4 @ X2)) = X4) | (((sK0 @ (sK3 @ X2))) = $true)) )),
% 0.23/0.35 inference(and_proxy_clausification,[],[f32])).
% 0.23/0.35 thf(f34,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK6 @ X4 @ X2)) = X4) | ($true = (((X2 @ (sK6 @ X4 @ X2)) = (sK2 @ X2)))) | (((sK0 @ (sK3 @ X2))) = $true)) )),
% 0.23/0.35 inference(and_proxy_clausification,[],[f32])).
% 0.23/0.35 thf(f35,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((X2 @ (sK6 @ X4 @ X2))) = ((sK2 @ X2))) | (((sK6 @ X4 @ X2)) = X4) | (((sK0 @ (sK3 @ X2))) = $true)) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f34])).
% 0.23/0.35 thf(f36,plain,(
% 0.23/0.35 ( ! [X0 : a,X1 : (a > a)] : (($true != $true) | ($true = ((sK0 @ (sK3 @ X1)))) | ((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK6 @ X0 @ X1)))) = ((= @ (sK5 @ (sK6 @ X0 @ X1))))) | (((sK6 @ X0 @ X1)) = X0)) )),
% 0.23/0.35 inference(constrained_superposition,[],[f17,f33])).
% 0.23/0.35 thf(f37,plain,(
% 0.23/0.35 ( ! [X0 : a,X1 : (a > a)] : (((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK6 @ X0 @ X1)))) = ((= @ (sK5 @ (sK6 @ X0 @ X1))))) | ($true = ((sK0 @ (sK3 @ X1)))) | (((sK6 @ X0 @ X1)) = X0)) )),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f36])).
% 0.23/0.35 thf(f38,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : (((((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) @ (sK7 @ X4 @ X2))) != ((X4 = (sK7 @ X4 @ X2)))) | (((sK1 @ (X2 @ (sK3 @ X2)))) != $true)) )),
% 0.23/0.35 inference(negative_extensionality,[],[f19])).
% 0.23/0.35 thf(f39,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((X4 = (sK7 @ X4 @ X2))) = $true) | ((((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) @ (sK7 @ X4 @ X2))) = $true) | (((sK1 @ (X2 @ (sK3 @ X2)))) != $true)) )),
% 0.23/0.35 inference(xor_proxy_clausification,[],[f38])).
% 0.23/0.35 thf(f40,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : (((((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) @ (sK7 @ X4 @ X2))) = $false) | (((sK1 @ (X2 @ (sK3 @ X2)))) != $true) | (((X4 = (sK7 @ X4 @ X2))) = $false)) )),
% 0.23/0.35 inference(xor_proxy_clausification,[],[f38])).
% 0.23/0.35 thf(f41,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK7 @ X4 @ X2)) != X4) | (((sK1 @ (X2 @ (sK3 @ X2)))) != $true) | ((((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) @ (sK7 @ X4 @ X2))) = $false)) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f40])).
% 0.23/0.35 thf(f42,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK7 @ X4 @ X2)) != X4) | ($false = ((((X2 @ (sK7 @ X4 @ X2)) = (sK2 @ X2)) & (sK0 @ (sK7 @ X4 @ X2))))) | (((sK1 @ (X2 @ (sK3 @ X2)))) != $true)) )),
% 0.23/0.35 inference(beta-eta_normalization,[],[f41])).
% 0.23/0.35 thf(f43,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK1 @ (X2 @ (sK3 @ X2)))) != $true) | ((((X2 @ (sK7 @ X4 @ X2)) = (sK2 @ X2))) = $false) | ($false = ((sK0 @ (sK7 @ X4 @ X2)))) | (((sK7 @ X4 @ X2)) != X4)) )),
% 0.23/0.35 inference(and_proxy_clausification,[],[f42])).
% 0.23/0.35 thf(f44,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK2 @ X2)) != ((X2 @ (sK7 @ X4 @ X2)))) | (((sK7 @ X4 @ X2)) != X4) | (((sK1 @ (X2 @ (sK3 @ X2)))) != $true) | ($false = ((sK0 @ (sK7 @ X4 @ X2))))) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f43])).
% 0.23/0.35 thf(f45,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : (((((^[Y0 : a]: (((X2 @ Y0) = (sK2 @ X2)) & (sK0 @ Y0))) @ (sK7 @ X4 @ X2))) = $true) | (((sK7 @ X4 @ X2)) = X4) | (((sK1 @ (X2 @ (sK3 @ X2)))) != $true)) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f39])).
% 0.23/0.35 thf(f46,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK1 @ (X2 @ (sK3 @ X2)))) != $true) | (((sK7 @ X4 @ X2)) = X4) | ($true = ((((X2 @ (sK7 @ X4 @ X2)) = (sK2 @ X2)) & (sK0 @ (sK7 @ X4 @ X2)))))) )),
% 0.23/0.35 inference(beta-eta_normalization,[],[f45])).
% 0.23/0.35 thf(f47,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK1 @ (X2 @ (sK3 @ X2)))) != $true) | (((sK7 @ X4 @ X2)) = X4) | (((sK0 @ (sK7 @ X4 @ X2))) = $true)) )),
% 0.23/0.35 inference(and_proxy_clausification,[],[f46])).
% 0.23/0.35 thf(f48,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK7 @ X4 @ X2)) = X4) | (((sK1 @ (X2 @ (sK3 @ X2)))) != $true) | ((((X2 @ (sK7 @ X4 @ X2)) = (sK2 @ X2))) = $true)) )),
% 0.23/0.35 inference(and_proxy_clausification,[],[f46])).
% 0.23/0.35 thf(f49,plain,(
% 0.23/0.35 ( ! [X2 : (a > a),X4 : a] : ((((sK1 @ (X2 @ (sK3 @ X2)))) != $true) | (((sK2 @ X2)) = ((X2 @ (sK7 @ X4 @ X2)))) | (((sK7 @ X4 @ X2)) = X4)) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f48])).
% 0.23/0.35 thf(f56,plain,(
% 0.23/0.35 ( ! [X0 : (a > a),X1 : a] : (($true = ((sK0 @ (sK3 @ X0)))) | ((((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK4 @ (sK2 @ X0))))) @ X1)) = (((sK5 @ (sK4 @ (sK2 @ X0))) = X1)))) )),
% 0.23/0.35 inference(argument_congruence,[],[f23])).
% 0.23/0.35 thf(f58,plain,(
% 0.23/0.35 ( ! [X0 : (a > a),X1 : a] : (((((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK4 @ (sK2 @ X0))))) @ X1)) = $false) | ($true = (((sK5 @ (sK4 @ (sK2 @ X0))) = X1))) | ($true = ((sK0 @ (sK3 @ X0))))) )),
% 0.23/0.35 inference(iff_proxy_clausification,[],[f56])).
% 0.23/0.35 thf(f59,plain,(
% 0.23/0.35 ( ! [X0 : (a > a),X1 : a] : (((((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK4 @ (sK2 @ X0))))) @ X1)) = $false) | ($true = ((sK0 @ (sK3 @ X0)))) | (((sK5 @ (sK4 @ (sK2 @ X0)))) = X1)) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f58])).
% 0.23/0.35 thf(f60,plain,(
% 0.23/0.35 ( ! [X0 : (a > a),X1 : a] : ((((sK5 @ (sK4 @ (sK2 @ X0)))) = X1) | ((((sK1 @ X1) & ((sK4 @ X1) = (sK4 @ (sK2 @ X0))))) = $false) | ($true = ((sK0 @ (sK3 @ X0))))) )),
% 0.23/0.35 inference(beta-eta_normalization,[],[f59])).
% 0.23/0.35 thf(f61,plain,(
% 0.23/0.35 ( ! [X0 : (a > a),X1 : a] : (($false = ((sK1 @ X1))) | ($false = (((sK4 @ X1) = (sK4 @ (sK2 @ X0))))) | ($true = ((sK0 @ (sK3 @ X0)))) | (((sK5 @ (sK4 @ (sK2 @ X0)))) = X1)) )),
% 0.23/0.35 inference(and_proxy_clausification,[],[f60])).
% 0.23/0.35 thf(f62,plain,(
% 0.23/0.35 ( ! [X0 : (a > a),X1 : a] : ((((sK4 @ X1)) != ((sK4 @ (sK2 @ X0)))) | ($true = ((sK0 @ (sK3 @ X0)))) | (((sK5 @ (sK4 @ (sK2 @ X0)))) = X1) | ($false = ((sK1 @ X1)))) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f61])).
% 0.23/0.35 thf(f80,plain,(
% 0.23/0.35 ( ! [X0 : (a > a)] : ((((sK5 @ (sK4 @ (sK2 @ X0)))) = ((sK2 @ X0))) | ($true = ((sK0 @ (sK3 @ X0)))) | (((sK1 @ (sK2 @ X0))) = $false)) )),
% 0.23/0.35 inference(equality_resolution,[],[f62])).
% 0.23/0.35 thf(f222,plain,(
% 0.23/0.35 ( ! [X2 : a,X0 : a,X1 : (a > a)] : (((((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK6 @ X0 @ X1)))) @ X2)) = (((sK5 @ (sK6 @ X0 @ X1)) = X2))) | (((sK6 @ X0 @ X1)) = X0) | ($true = ((sK0 @ (sK3 @ X1))))) )),
% 0.23/0.35 inference(argument_congruence,[],[f37])).
% 0.23/0.35 thf(f223,plain,(
% 0.23/0.35 ( ! [X2 : a,X0 : a,X1 : (a > a)] : (((((sK5 @ (sK6 @ X0 @ X1)) = X2)) = $false) | ($true = ((sK0 @ (sK3 @ X1)))) | (((sK6 @ X0 @ X1)) = X0) | ((((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK6 @ X0 @ X1)))) @ X2)) = $true)) )),
% 0.23/0.35 inference(iff_proxy_clausification,[],[f222])).
% 0.23/0.35 thf(f229,plain,(
% 0.23/0.35 ( ! [X2 : a,X0 : a,X1 : (a > a)] : ((((sK5 @ (sK6 @ X0 @ X1))) != X2) | ($true = ((sK0 @ (sK3 @ X1)))) | ((((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK6 @ X0 @ X1)))) @ X2)) = $true) | (((sK6 @ X0 @ X1)) = X0)) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f223])).
% 0.23/0.35 thf(f230,plain,(
% 0.23/0.35 ( ! [X2 : a,X0 : a,X1 : (a > a)] : (((((sK1 @ X2) & ((sK4 @ X2) = (sK6 @ X0 @ X1)))) = $true) | (((sK6 @ X0 @ X1)) = X0) | ($true = ((sK0 @ (sK3 @ X1)))) | (((sK5 @ (sK6 @ X0 @ X1))) != X2)) )),
% 0.23/0.35 inference(beta-eta_normalization,[],[f229])).
% 0.23/0.35 thf(f231,plain,(
% 0.23/0.35 ( ! [X2 : a,X0 : a,X1 : (a > a)] : ((((sK5 @ (sK6 @ X0 @ X1))) != X2) | (((sK6 @ X0 @ X1)) = X0) | ($true = ((sK0 @ (sK3 @ X1)))) | ((((sK4 @ X2) = (sK6 @ X0 @ X1))) = $true)) )),
% 0.23/0.35 inference(and_proxy_clausification,[],[f230])).
% 0.23/0.35 thf(f233,plain,(
% 0.23/0.35 ( ! [X2 : a,X0 : a,X1 : (a > a)] : ((((sK5 @ (sK6 @ X0 @ X1))) != X2) | (((sK6 @ X0 @ X1)) = ((sK4 @ X2))) | (((sK6 @ X0 @ X1)) = X0) | ($true = ((sK0 @ (sK3 @ X1))))) )),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f231])).
% 0.23/0.35 thf(f242,definition,(
% 0.23/0.35 spl8_5 <=> (((sK0 @ (sK3 @ sK5))) = $true)),
% 0.23/0.35 introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition])).
% 0.23/0.35 thf(f243,plain,(
% 0.23/0.35 (((sK0 @ (sK3 @ sK5))) != $true) | spl8_5),
% 0.23/0.35 inference(avatar_component_clause,[],[f242])).
% 0.23/0.35 thf(f244,plain,(
% 0.23/0.35 (((sK0 @ (sK3 @ sK5))) = $true) | ~spl8_5),
% 0.23/0.35 inference(avatar_component_clause,[],[f242])).
% 0.23/0.35 thf(f246,definition,(
% 0.23/0.35 spl8_6 <=> ! [X0 : a] : (((sK6 @ X0 @ sK5)) = X0)),
% 0.23/0.35 introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition])).
% 0.23/0.35 thf(f247,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK6 @ X0 @ sK5)) = X0)) ) | ~spl8_6),
% 0.23/0.35 inference(avatar_component_clause,[],[f246])).
% 0.23/0.35 thf(f344,plain,(
% 0.23/0.35 (((= @ (sK5 @ (sK3 @ sK5)))) = (^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK3 @ sK5))))) | ($true != $true) | ~spl8_5),
% 0.23/0.35 inference(constrained_superposition,[],[f17,f244])).
% 0.23/0.35 thf(f345,plain,(
% 0.23/0.35 (((= @ (sK5 @ (sK3 @ sK5)))) = (^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK3 @ sK5))))) | ~spl8_5),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f344])).
% 0.23/0.35 thf(f346,plain,(
% 0.23/0.35 ( ! [X1 : a] : (((((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK3 @ sK5)))) @ X1)) = (((sK5 @ (sK3 @ sK5)) = X1)))) ) | ~spl8_5),
% 0.23/0.35 inference(argument_congruence,[],[f345])).
% 0.23/0.35 thf(f347,plain,(
% 0.23/0.35 ( ! [X1 : a] : (((((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK3 @ sK5)))) @ X1)) = $true) | ($false = (((sK5 @ (sK3 @ sK5)) = X1)))) ) | ~spl8_5),
% 0.23/0.35 inference(iff_proxy_clausification,[],[f346])).
% 0.23/0.35 thf(f353,plain,(
% 0.23/0.35 ( ! [X1 : a] : (((((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK3 @ sK5)))) @ X1)) = $true) | (((sK5 @ (sK3 @ sK5))) != X1)) ) | ~spl8_5),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f347])).
% 0.23/0.35 thf(f354,plain,(
% 0.23/0.35 ( ! [X1 : a] : (((((sK1 @ X1) & ((sK4 @ X1) = (sK3 @ sK5)))) = $true) | (((sK5 @ (sK3 @ sK5))) != X1)) ) | ~spl8_5),
% 0.23/0.35 inference(beta-eta_normalization,[],[f353])).
% 0.23/0.35 thf(f356,plain,(
% 0.23/0.35 ( ! [X1 : a] : ((((sK5 @ (sK3 @ sK5))) != X1) | ($true = ((sK1 @ X1)))) ) | ~spl8_5),
% 0.23/0.35 inference(and_proxy_clausification,[],[f354])).
% 0.23/0.35 thf(f359,plain,(
% 0.23/0.35 ($true = ((sK1 @ (sK5 @ (sK3 @ sK5))))) | ~spl8_5),
% 0.23/0.35 inference(equality_resolution,[],[f356])).
% 0.23/0.35 thf(f361,plain,(
% 0.23/0.35 ( ! [X0 : a] : (($true != $true) | (((sK7 @ X0 @ sK5)) = X0) | (((sK2 @ sK5)) = ((sK5 @ (sK7 @ X0 @ sK5))))) ) | ~spl8_5),
% 0.23/0.35 inference(constrained_superposition,[],[f49,f359])).
% 0.23/0.35 thf(f362,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK0 @ (sK7 @ X0 @ sK5))) = $true) | (((sK7 @ X0 @ sK5)) = X0) | ($true != $true)) ) | ~spl8_5),
% 0.23/0.35 inference(constrained_superposition,[],[f47,f359])).
% 0.23/0.35 thf(f363,plain,(
% 0.23/0.35 ($true = ((sK1 @ (sK2 @ sK5)))) | ($true != $true) | ~spl8_5),
% 0.23/0.35 inference(constrained_superposition,[],[f12,f359])).
% 0.23/0.35 thf(f364,plain,(
% 0.23/0.35 ($true = ((sK1 @ (sK2 @ sK5)))) | ~spl8_5),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f363])).
% 0.23/0.35 thf(f365,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK2 @ sK5)) = ((sK5 @ (sK7 @ X0 @ sK5)))) | (((sK7 @ X0 @ sK5)) = X0)) ) | ~spl8_5),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f361])).
% 0.23/0.35 thf(f367,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK0 @ (sK7 @ X0 @ sK5))) = $true) | (((sK7 @ X0 @ sK5)) = X0)) ) | ~spl8_5),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f362])).
% 0.23/0.35 thf(f368,plain,(
% 0.23/0.35 ($true != $true) | (((sK0 @ (sK4 @ (sK2 @ sK5)))) = $true) | ~spl8_5),
% 0.23/0.35 inference(constrained_superposition,[],[f9,f364])).
% 0.23/0.35 thf(f369,plain,(
% 0.23/0.35 (((sK0 @ (sK4 @ (sK2 @ sK5)))) = $true) | ~spl8_5),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f368])).
% 0.23/0.35 thf(f370,plain,(
% 0.23/0.35 ($true != $true) | (((= @ (sK5 @ (sK4 @ (sK2 @ sK5))))) = (^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK4 @ (sK2 @ sK5)))))) | ~spl8_5),
% 0.23/0.35 inference(constrained_superposition,[],[f17,f369])).
% 0.23/0.35 thf(f371,plain,(
% 0.23/0.35 (((= @ (sK5 @ (sK4 @ (sK2 @ sK5))))) = (^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK4 @ (sK2 @ sK5)))))) | ~spl8_5),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f370])).
% 0.23/0.35 thf(f396,plain,(
% 0.23/0.35 ( ! [X0 : a] : (($true != $true) | (((= @ (sK5 @ (sK7 @ X0 @ sK5)))) = (^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK7 @ X0 @ sK5))))) | (((sK7 @ X0 @ sK5)) = X0)) ) | ~spl8_5),
% 0.23/0.35 inference(constrained_superposition,[],[f17,f367])).
% 0.23/0.35 thf(f397,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((= @ (sK5 @ (sK7 @ X0 @ sK5)))) = (^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK7 @ X0 @ sK5))))) | (((sK7 @ X0 @ sK5)) = X0)) ) | ~spl8_5),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f396])).
% 0.23/0.35 thf(f399,plain,(
% 0.23/0.35 ( ! [X1 : a] : (((((sK5 @ (sK4 @ (sK2 @ sK5))) = X1)) = (((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK4 @ (sK2 @ sK5))))) @ X1)))) ) | ~spl8_5),
% 0.23/0.35 inference(argument_congruence,[],[f371])).
% 0.23/0.35 thf(f400,plain,(
% 0.23/0.35 ( ! [X1 : a] : (((((sK5 @ (sK4 @ (sK2 @ sK5))) = X1)) = $true) | ((((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK4 @ (sK2 @ sK5))))) @ X1)) = $false)) ) | ~spl8_5),
% 0.23/0.35 inference(iff_proxy_clausification,[],[f399])).
% 0.23/0.35 thf(f407,plain,(
% 0.23/0.35 ( ! [X1 : a] : (((((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK4 @ (sK2 @ sK5))))) @ X1)) = $false) | (((sK5 @ (sK4 @ (sK2 @ sK5)))) = X1)) ) | ~spl8_5),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f400])).
% 0.23/0.35 thf(f408,plain,(
% 0.23/0.35 ( ! [X1 : a] : ((((sK5 @ (sK4 @ (sK2 @ sK5)))) = X1) | ($false = (((sK1 @ X1) & ((sK4 @ X1) = (sK4 @ (sK2 @ sK5))))))) ) | ~spl8_5),
% 0.23/0.35 inference(beta-eta_normalization,[],[f407])).
% 0.23/0.35 thf(f409,plain,(
% 0.23/0.35 ( ! [X1 : a] : (((((sK4 @ X1) = (sK4 @ (sK2 @ sK5)))) = $false) | ($false = ((sK1 @ X1))) | (((sK5 @ (sK4 @ (sK2 @ sK5)))) = X1)) ) | ~spl8_5),
% 0.23/0.35 inference(and_proxy_clausification,[],[f408])).
% 0.23/0.35 thf(f410,plain,(
% 0.23/0.35 ( ! [X1 : a] : ((((sK4 @ X1)) != ((sK4 @ (sK2 @ sK5)))) | ($false = ((sK1 @ X1))) | (((sK5 @ (sK4 @ (sK2 @ sK5)))) = X1)) ) | ~spl8_5),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f409])).
% 0.23/0.35 thf(f457,plain,(
% 0.23/0.35 ($false = ((sK1 @ (sK2 @ sK5)))) | (((sK2 @ sK5)) = ((sK5 @ (sK4 @ (sK2 @ sK5))))) | ~spl8_5),
% 0.23/0.35 inference(equality_resolution,[],[f410])).
% 0.23/0.35 thf(f458,plain,(
% 0.23/0.35 ($false = $true) | (((sK2 @ sK5)) = ((sK5 @ (sK4 @ (sK2 @ sK5))))) | ~spl8_5),
% 0.23/0.35 inference(forward_demodulation,[],[f457,f364])).
% 0.23/0.35 thf(f459,plain,(
% 0.23/0.35 (((sK2 @ sK5)) = ((sK5 @ (sK4 @ (sK2 @ sK5))))) | ~spl8_5),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f458])).
% 0.23/0.35 thf(f486,plain,(
% 0.23/0.35 ( ! [X0 : a,X1 : (a > a)] : ((((sK6 @ X0 @ X1)) = ((sK4 @ (sK5 @ (sK6 @ X0 @ X1))))) | (((sK6 @ X0 @ X1)) = X0) | ($true = ((sK0 @ (sK3 @ X1))))) )),
% 0.23/0.35 inference(equality_resolution,[],[f233])).
% 0.23/0.35 thf(f488,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK6 @ X0 @ sK5)) = ((sK4 @ (sK2 @ sK5)))) | (((sK6 @ X0 @ sK5)) = X0) | (((sK0 @ (sK3 @ sK5))) = $true) | (((sK6 @ X0 @ sK5)) = X0) | (((sK0 @ (sK3 @ sK5))) = $true)) )),
% 0.23/0.35 inference(constrained_superposition,[],[f486,f35])).
% 0.23/0.35 thf(f495,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK6 @ X0 @ sK5)) = X0) | (((sK6 @ X0 @ sK5)) = ((sK4 @ (sK2 @ sK5)))) | (((sK0 @ (sK3 @ sK5))) = $true)) )),
% 0.23/0.35 inference(duplicate_literal_removal,[],[f488])).
% 0.23/0.35 thf(f557,plain,(
% 0.23/0.35 ( ! [X0 : a,X1 : a] : (((((sK5 @ (sK7 @ X0 @ sK5)) = X1)) = (((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK7 @ X0 @ sK5)))) @ X1))) | (((sK7 @ X0 @ sK5)) = X0)) ) | ~spl8_5),
% 0.23/0.35 inference(argument_congruence,[],[f397])).
% 0.23/0.35 thf(f559,plain,(
% 0.23/0.35 ( ! [X0 : a,X1 : a] : ((((sK7 @ X0 @ sK5)) = X0) | ($false = (((sK5 @ (sK7 @ X0 @ sK5)) = X1))) | ($true = (((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK7 @ X0 @ sK5)))) @ X1)))) ) | ~spl8_5),
% 0.23/0.35 inference(iff_proxy_clausification,[],[f557])).
% 0.23/0.35 thf(f560,plain,(
% 0.23/0.35 ( ! [X0 : a,X1 : a] : ((((sK5 @ (sK7 @ X0 @ sK5))) != X1) | (((sK7 @ X0 @ sK5)) = X0) | ($true = (((^[Y0 : a]: ((sK1 @ Y0) & ((sK4 @ Y0) = (sK7 @ X0 @ sK5)))) @ X1)))) ) | ~spl8_5),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f559])).
% 0.23/0.35 thf(f561,plain,(
% 0.23/0.35 ( ! [X0 : a,X1 : a] : ((((sK5 @ (sK7 @ X0 @ sK5))) != X1) | (((sK7 @ X0 @ sK5)) = X0) | ((((sK1 @ X1) & ((sK4 @ X1) = (sK7 @ X0 @ sK5)))) = $true)) ) | ~spl8_5),
% 0.23/0.35 inference(beta-eta_normalization,[],[f560])).
% 0.23/0.35 thf(f562,plain,(
% 0.23/0.35 ( ! [X0 : a,X1 : a] : ((((sK5 @ (sK7 @ X0 @ sK5))) != X1) | (((sK7 @ X0 @ sK5)) = X0) | ($true = (((sK4 @ X1) = (sK7 @ X0 @ sK5))))) ) | ~spl8_5),
% 0.23/0.35 inference(and_proxy_clausification,[],[f561])).
% 0.23/0.35 thf(f564,plain,(
% 0.23/0.35 ( ! [X0 : a,X1 : a] : ((((sK5 @ (sK7 @ X0 @ sK5))) != X1) | (((sK7 @ X0 @ sK5)) = X0) | (((sK4 @ X1)) = ((sK7 @ X0 @ sK5)))) ) | ~spl8_5),
% 0.23/0.35 inference(equality_proxy_clausification,[],[f562])).
% 0.23/0.35 thf(f582,plain,(
% 0.23/0.35 ( ! [X0 : a,X1 : a] : ((((sK7 @ X0 @ sK5)) = X0) | (((sK4 @ X1)) = ((sK7 @ X0 @ sK5))) | (((sK2 @ sK5)) != X1) | (((sK7 @ X0 @ sK5)) = X0)) ) | ~spl8_5),
% 0.23/0.35 inference(constrained_superposition,[],[f564,f365])).
% 0.23/0.35 thf(f584,plain,(
% 0.23/0.35 ( ! [X0 : a,X1 : a] : ((((sK2 @ sK5)) != X1) | (((sK7 @ X0 @ sK5)) = X0) | (((sK4 @ X1)) = ((sK7 @ X0 @ sK5)))) ) | ~spl8_5),
% 0.23/0.35 inference(duplicate_literal_removal,[],[f582])).
% 0.23/0.35 thf(f586,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK7 @ X0 @ sK5)) = ((sK4 @ (sK2 @ sK5)))) | (((sK7 @ X0 @ sK5)) = X0)) ) | ~spl8_5),
% 0.23/0.35 inference(equality_resolution,[],[f584])).
% 0.23/0.35 thf(f595,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK4 @ (sK2 @ sK5))) != X0) | (((sK7 @ X0 @ sK5)) = X0)) ) | ~spl8_5),
% 0.23/0.35 inference(equality_factoring,[],[f586])).
% 0.23/0.35 thf(f600,plain,(
% 0.23/0.35 (((sK4 @ (sK2 @ sK5))) = ((sK7 @ (sK4 @ (sK2 @ sK5)) @ sK5))) | ~spl8_5),
% 0.23/0.35 inference(equality_resolution,[],[f595])).
% 0.23/0.35 thf(f601,plain,(
% 0.23/0.35 ($true != ((sK1 @ (sK5 @ (sK3 @ sK5))))) | (((sK4 @ (sK2 @ sK5))) != ((sK4 @ (sK2 @ sK5)))) | ($false = ((sK0 @ (sK4 @ (sK2 @ sK5))))) | (((sK2 @ sK5)) != ((sK5 @ (sK4 @ (sK2 @ sK5))))) | ~spl8_5),
% 0.23/0.35 inference(constrained_superposition,[],[f44,f600])).
% 0.23/0.35 thf(f602,plain,(
% 0.23/0.35 ($true != ((sK1 @ (sK5 @ (sK3 @ sK5))))) | ($false = ((sK0 @ (sK4 @ (sK2 @ sK5))))) | (((sK2 @ sK5)) != ((sK5 @ (sK4 @ (sK2 @ sK5))))) | ~spl8_5),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f601])).
% 0.23/0.35 thf(f603,plain,(
% 0.23/0.35 ($false = ((sK0 @ (sK4 @ (sK2 @ sK5))))) | (((sK2 @ sK5)) != ((sK5 @ (sK4 @ (sK2 @ sK5))))) | ~spl8_5),
% 0.23/0.35 inference(forward_subsumption_resolution,[],[f602,f359])).
% 0.23/0.35 thf(f604,plain,(
% 0.23/0.35 ($false = ((sK0 @ (sK4 @ (sK2 @ sK5))))) | ~spl8_5),
% 0.23/0.35 inference(forward_subsumption_resolution,[],[f603,f459])).
% 0.23/0.35 thf(f605,plain,(
% 0.23/0.35 ($false = $true) | ~spl8_5),
% 0.23/0.35 inference(forward_demodulation,[],[f604,f369])).
% 0.23/0.35 thf(f606,plain,(
% 0.23/0.35 $false | ~spl8_5),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f605])).
% 0.23/0.35 thf(f607,plain,(
% 0.23/0.35 ~spl8_5),
% 0.23/0.35 inference(avatar_contradiction_clause,[],[f606])).
% 0.23/0.35 thf(f613,definition,(
% 0.23/0.35 spl8_15 <=> ! [X0 : a] : ((((sK6 @ X0 @ sK5)) = X0) | (((sK6 @ X0 @ sK5)) = ((sK4 @ (sK2 @ sK5)))))),
% 0.23/0.35 introduced(definition,[new_symbols(definition,[spl8_15])],[avatar_definition])).
% 0.23/0.35 thf(f614,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK6 @ X0 @ sK5)) = ((sK4 @ (sK2 @ sK5)))) | (((sK6 @ X0 @ sK5)) = X0)) ) | ~spl8_15),
% 0.23/0.35 inference(avatar_component_clause,[],[f613])).
% 0.23/0.35 thf(f615,plain,(
% 0.23/0.35 spl8_15 | spl8_5),
% 0.23/0.35 inference(avatar_split_clause,[],[f495,f242,f613])).
% 0.23/0.35 thf(f622,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK0 @ (sK3 @ sK5))) = $true) | (((sK6 @ X0 @ sK5)) = X0) | (((sK2 @ sK5)) = ((sK5 @ (sK4 @ (sK2 @ sK5))))) | (((sK4 @ (sK2 @ sK5))) = X0)) ) | ~spl8_15),
% 0.23/0.35 inference(constrained_superposition,[],[f35,f614])).
% 0.23/0.35 thf(f630,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK4 @ (sK2 @ sK5))) != X0) | (((sK6 @ X0 @ sK5)) = X0)) ) | ~spl8_15),
% 0.23/0.35 inference(equality_factoring,[],[f614])).
% 0.23/0.35 thf(f631,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK4 @ (sK2 @ sK5))) != X0) | (((sK6 @ X0 @ sK5)) = ((sK4 @ (sK2 @ sK5))))) ) | ~spl8_15),
% 0.23/0.35 inference(equality_factoring,[],[f614])).
% 0.23/0.35 thf(f634,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK0 @ (sK3 @ sK5))) = $true) | (((sK6 @ X0 @ sK5)) = X0) | (((sK2 @ sK5)) = ((sK5 @ (sK4 @ (sK2 @ sK5)))))) ) | ~spl8_15),
% 0.23/0.35 inference(forward_subsumption_resolution,[],[f622,f630])).
% 0.23/0.35 thf(f635,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK6 @ X0 @ sK5)) = X0) | (((sK2 @ sK5)) = ((sK5 @ (sK4 @ (sK2 @ sK5)))))) ) | (spl8_5 | ~spl8_15)),
% 0.23/0.35 inference(forward_subsumption_resolution,[],[f634,f243])).
% 0.23/0.35 thf(f637,definition,(
% 0.23/0.35 spl8_16 <=> (((sK2 @ sK5)) = ((sK5 @ (sK4 @ (sK2 @ sK5)))))),
% 0.23/0.35 introduced(definition,[new_symbols(definition,[spl8_16])],[avatar_definition])).
% 0.23/0.35 thf(f639,plain,(
% 0.23/0.35 (((sK2 @ sK5)) = ((sK5 @ (sK4 @ (sK2 @ sK5))))) | ~spl8_16),
% 0.23/0.35 inference(avatar_component_clause,[],[f637])).
% 0.23/0.35 thf(f640,plain,(
% 0.23/0.35 spl8_6 | spl8_16 | spl8_5 | ~spl8_15),
% 0.23/0.35 inference(avatar_split_clause,[],[f635,f613,f242,f637,f246])).
% 0.23/0.35 thf(f642,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK0 @ X0)) = $false) | (((sK2 @ sK5)) != ((sK5 @ X0))) | (X0 != X0) | (((sK0 @ (sK3 @ sK5))) = $true)) ) | ~spl8_6),
% 0.23/0.35 inference(constrained_superposition,[],[f30,f247])).
% 0.23/0.35 thf(f643,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK0 @ (sK3 @ sK5))) = $true) | (((sK0 @ X0)) = $false) | (((sK2 @ sK5)) != ((sK5 @ X0)))) ) | ~spl8_6),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f642])).
% 0.23/0.35 thf(f644,plain,(
% 0.23/0.35 ( ! [X0 : a] : ((((sK2 @ sK5)) != ((sK5 @ X0))) | (((sK0 @ X0)) = $false)) ) | (spl8_5 | ~spl8_6)),
% 0.23/0.35 inference(forward_subsumption_resolution,[],[f643,f243])).
% 0.23/0.35 thf(f646,plain,(
% 0.23/0.35 ( ! [X0 : (a > a)] : ((((sK2 @ X0)) != ((sK2 @ sK5))) | ($false = ((sK0 @ (sK4 @ (sK2 @ X0))))) | ($true = ((sK0 @ (sK3 @ X0)))) | (((sK1 @ (sK2 @ X0))) = $false)) ) | (spl8_5 | ~spl8_6)),
% 0.23/0.35 inference(constrained_superposition,[],[f644,f80])).
% 0.23/0.35 thf(f652,plain,(
% 0.23/0.35 (((sK6 @ (sK4 @ (sK2 @ sK5)) @ sK5)) = ((sK4 @ (sK2 @ sK5)))) | ~spl8_15),
% 0.23/0.35 inference(equality_resolution,[],[f631])).
% 0.23/0.35 thf(f659,plain,(
% 0.23/0.35 ($false = ((sK1 @ (sK2 @ sK5)))) | ($false = ((sK0 @ (sK4 @ (sK2 @ sK5))))) | (((sK0 @ (sK3 @ sK5))) = $true) | (spl8_5 | ~spl8_6)),
% 0.23/0.35 inference(equality_resolution,[],[f646])).
% 0.23/0.35 thf(f660,plain,(
% 0.23/0.35 ($false = ((sK0 @ (sK4 @ (sK2 @ sK5))))) | ($false = ((sK1 @ (sK2 @ sK5)))) | (spl8_5 | ~spl8_6)),
% 0.23/0.35 inference(forward_subsumption_resolution,[],[f659,f243])).
% 0.23/0.35 thf(f667,definition,(
% 0.23/0.35 spl8_17 <=> ($false = ((sK0 @ (sK4 @ (sK2 @ sK5)))))),
% 0.23/0.35 introduced(definition,[new_symbols(definition,[spl8_17])],[avatar_definition])).
% 0.23/0.35 thf(f669,plain,(
% 0.23/0.35 ($false = ((sK0 @ (sK4 @ (sK2 @ sK5))))) | ~spl8_17),
% 0.23/0.35 inference(avatar_component_clause,[],[f667])).
% 0.23/0.35 thf(f671,definition,(
% 0.23/0.35 spl8_18 <=> ($false = ((sK1 @ (sK2 @ sK5))))),
% 0.23/0.35 introduced(definition,[new_symbols(definition,[spl8_18])],[avatar_definition])).
% 0.23/0.35 thf(f673,plain,(
% 0.23/0.35 ($false = ((sK1 @ (sK2 @ sK5)))) | ~spl8_18),
% 0.23/0.35 inference(avatar_component_clause,[],[f671])).
% 0.23/0.35 thf(f674,plain,(
% 0.23/0.35 spl8_17 | spl8_18 | spl8_5 | ~spl8_6),
% 0.23/0.35 inference(avatar_split_clause,[],[f660,f246,f242,f671,f667])).
% 0.23/0.35 thf(f698,plain,(
% 0.23/0.35 (((sK4 @ (sK2 @ sK5))) != ((sK4 @ (sK2 @ sK5)))) | ($false = ((sK0 @ (sK4 @ (sK2 @ sK5))))) | (((sK0 @ (sK3 @ sK5))) = $true) | (((sK2 @ sK5)) != ((sK5 @ (sK4 @ (sK2 @ sK5))))) | ~spl8_15),
% 0.23/0.35 inference(constrained_superposition,[],[f30,f652])).
% 0.23/0.35 thf(f699,plain,(
% 0.23/0.35 (((sK0 @ (sK3 @ sK5))) = $true) | ($false = ((sK0 @ (sK4 @ (sK2 @ sK5))))) | (((sK2 @ sK5)) != ((sK5 @ (sK4 @ (sK2 @ sK5))))) | ~spl8_15),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f698])).
% 0.23/0.35 thf(f700,plain,(
% 0.23/0.35 ($false = ((sK0 @ (sK4 @ (sK2 @ sK5))))) | (((sK0 @ (sK3 @ sK5))) = $true) | (~spl8_15 | ~spl8_16)),
% 0.23/0.35 inference(forward_subsumption_resolution,[],[f699,f639])).
% 0.23/0.35 thf(f701,plain,(
% 0.23/0.35 ($false = ((sK0 @ (sK4 @ (sK2 @ sK5))))) | (spl8_5 | ~spl8_15 | ~spl8_16)),
% 0.23/0.35 inference(forward_subsumption_resolution,[],[f700,f243])).
% 0.23/0.35 thf(f705,plain,(
% 0.23/0.35 spl8_17 | spl8_5 | ~spl8_15 | ~spl8_16),
% 0.23/0.35 inference(avatar_split_clause,[],[f701,f637,f613,f242,f667])).
% 0.23/0.35 thf(f713,plain,(
% 0.23/0.35 (((sK0 @ (sK3 @ sK5))) = $true) | ($false = $true) | ~spl8_17),
% 0.23/0.35 inference(constrained_superposition,[],[f669,f21])).
% 0.23/0.35 thf(f717,plain,(
% 0.23/0.35 (((sK0 @ (sK3 @ sK5))) = $true) | ~spl8_17),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f713])).
% 0.23/0.35 thf(f720,plain,(
% 0.23/0.35 $false | (spl8_5 | ~spl8_17)),
% 0.23/0.35 inference(forward_subsumption_resolution,[],[f717,f243])).
% 0.23/0.35 thf(f721,plain,(
% 0.23/0.35 spl8_5 | ~spl8_17),
% 0.23/0.35 inference(avatar_contradiction_clause,[],[f720])).
% 0.23/0.35 thf(f724,plain,(
% 0.23/0.35 ($false = $true) | (((sK0 @ (sK3 @ sK5))) = $true) | ~spl8_18),
% 0.23/0.35 inference(constrained_superposition,[],[f11,f673])).
% 0.23/0.35 thf(f726,plain,(
% 0.23/0.35 (((sK0 @ (sK3 @ sK5))) = $true) | ~spl8_18),
% 0.23/0.35 inference(trivial_inequality_removal,[],[f724])).
% 0.23/0.35 thf(f729,plain,(
% 0.23/0.35 $false | (spl8_5 | ~spl8_18)),
% 0.23/0.35 inference(forward_subsumption_resolution,[],[f726,f243])).
% 0.23/0.35 thf(f730,plain,(
% 0.23/0.35 spl8_5 | ~spl8_18),
% 0.23/0.35 inference(avatar_contradiction_clause,[],[f729])).
% 0.23/0.35 cnf(s11, plain, ~spl8_5, inference(sat_conversion,[],[f607])).
% 0.23/0.35 cnf(s13, plain, spl8_5 | spl8_15, inference(sat_conversion,[],[f615])).
% 0.23/0.35 cnf(s14, plain, spl8_5 | spl8_6 | ~spl8_15 | spl8_16, inference(sat_conversion,[],[f640])).
% 0.23/0.35 cnf(s16, plain, spl8_5 | ~spl8_6 | spl8_17 | spl8_18, inference(sat_conversion,[],[f674])).
% 0.23/0.35 cnf(s18, plain, spl8_5 | ~spl8_15 | ~spl8_16 | spl8_17, inference(sat_conversion,[],[f705])).
% 0.23/0.35 cnf(s21, plain, spl8_5 | ~spl8_17, inference(sat_conversion,[],[f721])).
% 0.23/0.35 cnf(s23, plain, spl8_5 | ~spl8_18, inference(sat_conversion,[],[f730])).
% 0.23/0.35 cnf(s24, plain, ~spl8_18, inference(rat,[],[s23,s11])).
% 0.23/0.35 cnf(s25, plain, ~spl8_17, inference(rat,[],[s21,s11])).
% 0.23/0.35 cnf(s26, plain, ~spl8_6, inference(rat,[],[s16,s24,s25,s11])).
% 0.23/0.35 cnf(s27, plain, spl8_15, inference(rat,[],[s13,s11])).
% 0.23/0.35 cnf(s29, plain, ~spl8_16, inference(rat,[],[s18,s25,s11,s27])).
% 0.23/0.35 cnf(s30, plain, $false, inference(rat,[],[s14,s26,s11,s29,s27])).
% 0.23/0.35 thf(f731,plain,(
% 0.23/0.35 $false),
% 0.23/0.35 inference(avatar_sat_refutation,[],[s30])).
% 0.23/0.35 % SZS output end Proof for theBenchmark
% 0.23/0.35 % (4116378)------------------------------
% 0.23/0.35 % (4116378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.35 % (4116378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.35 % (4116378)CaDiCaL version: 2.1.3
% 0.23/0.35 % (4116378)Termination reason: Refutation
% 0.23/0.35 % (4116378)Time elapsed: 0.052 s
% 0.23/0.35 % (4116378)Peak memory usage: 13 MB
% 0.23/0.35 % (4116378)Instructions burned: 76 (million)
% 0.23/0.35 % (4116373)Success in time 0.095 s
% 0.23/0.35 % Vampire exiting
%------------------------------------------------------------------------------