%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX180^1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:40:39 AM UTC 2026
% Result : Theorem 0.23s 0.29s
% Output : Refutation 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX180^1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n026.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 16:12:42 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/0.24 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.29 % (796895)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.23/0.29 % (796903)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=799244077: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.29 % (796906)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.29 % (796906)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.29 % (796900)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2802559684:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.23/0.29 % (796901)lrs+10_16_si=on:nwc=1.5:random_seed=1506117357:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.23/0.29 % (796902)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=76523335:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.23/0.29 % (796904)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1516567969:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.23/0.29 % (796905)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=136028631:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.23/0.29 % (796906)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=3745509785:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.23/0.29 % (796902)Instruction limit reached!
% 0.23/0.29 % (796902)------------------------------
% 0.23/0.29 % (796902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.29 % (796902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.29 % (796902)CaDiCaL version: 2.1.3
% 0.23/0.29 % (796902)Termination reason: Instruction limit
% 0.23/0.29 % (796902)Termination phase: Property scanning
% 0.23/0.29 % (796902)Time elapsed: 0.002 s
% 0.23/0.29 % (796902)Peak memory usage: 10 MB
% 0.23/0.29 % (796902)Instructions burned: 4 (million)
% 0.23/0.29 % (796901) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-796895-796901"...
% 0.23/0.29 % (796900) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-796895-796900"...
% 0.23/0.29 % (796906) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-796895-796906"...
% 0.23/0.29 % (796905) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-796895-796905"...
% 0.23/0.29 % (796901)...printing done.
% 0.23/0.29 % (796901)Refutation found. Thanks to Tanya!
% 0.23/0.29 % SZS status Theorem for theBenchmark
% 0.23/0.29 % SZS output start Proof for theBenchmark
% 0.23/0.29 thf(type_def_5, type, unsorted: $tType).
% 0.23/0.29 thf(type_def_6, type, mu: $tType).
% 0.23/0.29 thf(type_def_7, type, sTfun: ($tType * $tType) > $tType).
% 0.23/0.29 thf(type_def_8, type, d_unsorted: $tType).
% 0.23/0.29 thf(type_def_9, type, d_mu: $tType).
% 0.23/0.29 thf(func_def_0, type, meq_ind: (mu > mu > $i > $o)).
% 0.23/0.29 thf(func_def_1, type, meq_prop: (($i > $o) > ($i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_2, type, mnot: (($i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_3, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_4, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_5, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_6, type, mimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_7, type, mequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_8, type, mxor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_9, type, mforall_ind: ((mu > $i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_10, type, mforall_prop: ((($i > $o) > $i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_11, type, mexists_ind: ((mu > $i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_12, type, mexists_prop: ((($i > $o) > $i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_13, type, mtrue: ($i > $o)).
% 0.23/0.29 thf(func_def_14, type, mfalse: ($i > $o)).
% 0.23/0.29 thf(func_def_15, type, mbox: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_16, type, mdia: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 0.23/0.29 thf(func_def_17, type, mreflexive: (($i > $i > $o) > $o)).
% 0.23/0.29 thf(func_def_18, type, msymmetric: (($i > $i > $o) > $o)).
% 0.23/0.29 thf(func_def_19, type, mserial: (($i > $i > $o) > $o)).
% 0.23/0.29 thf(func_def_20, type, mtransitive: (($i > $i > $o) > $o)).
% 0.23/0.29 thf(func_def_21, type, meuclidean: (($i > $i > $o) > $o)).
% 0.23/0.29 thf(func_def_22, type, mpartially_functional: (($i > $i > $o) > $o)).
% 0.23/0.29 thf(func_def_23, type, mfunctional: (($i > $i > $o) > $o)).
% 0.23/0.29 thf(func_def_24, type, mweakly_dense: (($i > $i > $o) > $o)).
% 0.23/0.29 thf(func_def_25, type, mweakly_connected: (($i > $i > $o) > $o)).
% 0.23/0.29 thf(func_def_26, type, mweakly_directed: (($i > $i > $o) > $o)).
% 0.23/0.29 thf(func_def_27, type, mvalid: (($i > $o) > $o)).
% 0.23/0.29 thf(func_def_28, type, minvalid: (($i > $o) > $o)).
% 0.23/0.29 thf(func_def_29, type, msatisfiable: (($i > $o) > $o)).
% 0.23/0.29 thf(func_def_30, type, mcountersatisfiable: (($i > $o) > $o)).
% 0.23/0.29 thf(func_def_31, type, d2unsorted: (d_unsorted > $i)).
% 0.23/0.29 thf(func_def_32, type, d2mu: (d_mu > mu)).
% 0.23/0.29 thf(func_def_33, type, d_unsorted_0: d_unsorted).
% 0.23/0.29 thf(func_def_34, type, d_mu_0: d_mu).
% 0.23/0.29 thf(func_def_36, type, db1: !>[X0: $tType]:(X0)).
% 0.23/0.29 thf(func_def_37, type, db0: !>[X0: $tType]:(X0)).
% 0.23/0.29 thf(func_def_38, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.23/0.29 thf(func_def_39, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.23/0.29 thf(func_def_40, type, vOR: ($o > $o > $o)).
% 0.23/0.29 thf(func_def_41, type, db3: !>[X0: $tType]:(X0)).
% 0.23/0.29 thf(func_def_42, type, vNOT: ($o > $o)).
% 0.23/0.29 thf(func_def_43, type, db2: !>[X0: $tType]:(X0)).
% 0.23/0.29 thf(func_def_44, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.23/0.29 thf(func_def_47, type, db4: !>[X0: $tType]:(X0)).
% 0.23/0.29 thf(func_def_48, type, sK0: (mu > d_mu)).
% 0.23/0.29 thf(func_def_49, type, sK1: ($i > d_unsorted)).
% 0.23/0.29 thf(f1,axiom,(
% 0.23/0.29 ((^[X11 : (($i > $o) > $i > $o), X13 : $i] : (~ ! [X14 : ($i > $o)] : ~(X11 @ X14 @ X13))) = mexists_prop) & (mor = (^[X11 : ($i > $o), X12 : ($i > $o), X10 : $i] : ((X11 @ X10) | (X12 @ X10)))) & (meq_prop = (^[X8 : ($i > $o), X9 : ($i > $o), X10 : $i] : ((((X8 @ X10)) = ((X9 @ X10)))))) & ! [X1 : d_unsorted] : (X1 = d_unsorted_0) & (mimplies = (^[X11 : ($i > $o), X12 : ($i > $o), X13 : $i] : (~(X11 @ X13) | (X12 @ X13)))) & ((^[X15 : ($i > $i > $o)] : (! [X18 : $i,X0 : $i,X17 : $i] : (~(X15 @ X17 @ X0) | ~(X15 @ X17 @ X18) | ~ ! [X16 : $i] : (~(X15 @ X0 @ X16) | ~(X15 @ X18 @ X16))))) = mweakly_directed) & (mand = (^[X11 : ($i > $o), X12 : ($i > $o), X13 : $i] : (~(~(X12 @ X13) | ~(X11 @ X13))))) & (meuclidean = (^[X15 : ($i > $i > $o)] : (! [X0 : $i,X17 : $i,X18 : $i] : ((X15 @ X18 @ X0) | ~(X15 @ X17 @ X18) | ~(X15 @ X17 @ X0))))) & (mtrue @ (d2unsorted @ d_unsorted_0)) & (msatisfiable = (^[X11 : ($i > $o)] : (~ ! [X10 : $i] : ~(X11 @ X10)))) & (meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0)) & ! [X0 : $i] : ? [X1 : d_unsorted] : (X0 = ((d2unsorted @ X1))) & ((^[X11 : ($i > $o), X12 : ($i > $o), X13 : $i] : (~((X12 @ X13) | ~(X11 @ X13)) | ~(~(X12 @ X13) | (X11 @ X13)))) = mxor) & ((^[X15 : ($i > $i > $o)] : (! [X17 : $i,X18 : $i] : (~ ! [X19 : $i] : (~(X15 @ X17 @ X19) | ~(X15 @ X19 @ X18)) | ~(X15 @ X17 @ X18)))) = mweakly_dense) & ((^[X15 : ($i > $i > $o)] : (! [X0 : $i,X18 : $i,X17 : $i] : ((X18 = X0) | (X15 @ X18 @ X0) | (X15 @ X0 @ X18) | ~(X15 @ X17 @ X18) | ~(X15 @ X17 @ X0)))) = mweakly_connected) & ! [X5 : d_mu] : (X5 = d_mu_0) & ((^[X15 : ($i > $i > $o)] : (! [X17 : $i] : (X15 @ X17 @ X17))) = mreflexive) & ! [X6 : d_mu,X7 : d_mu] : ((((d2mu @ X6)) = ((d2mu @ X7))) => (X6 = X7)) & ((^[X11 : ($i > $o), X12 : ($i > $o), X13 : $i] : (~(~(~(X12 @ X13) | (X11 @ X13)) | ~(~(X11 @ X13) | (X12 @ X13))))) = mequiv) & ((^[X11 : ($i > $o)] : (~ ! [X10 : $i] : (X11 @ X10))) = mcountersatisfiable) & ((^[X11 : ($i > $o)] : (! [X10 : $i] : ~(X11 @ X10))) = minvalid) & (mdia = (^[X15 : ($i > $i > $o), X11 : ($i > $o), X13 : $i] : (~ ! [X16 : $i] : (~(X15 @ X13 @ X16) | ~(X11 @ X16))))) & (mforall_ind = (^[X11 : (mu > $i > $o), X10 : $i] : (! [X8 : mu] : (X11 @ X8 @ X10)))) & (mimplied = (^[X11 : ($i > $o), X12 : ($i > $o), X13 : $i] : (~(X12 @ X13) | (X11 @ X13)))) & ((^[X15 : ($i > $i > $o), X11 : ($i > $o), X10 : $i] : (! [X16 : $i] : (~(X15 @ X10 @ X16) | (X11 @ X16)))) = mbox) & ! [X4 : mu] : ? [X5 : d_mu] : (X4 = ((d2mu @ X5))) & ((^[X15 : ($i > $i > $o)] : (! [X17 : $i] : ~ ! [X18 : $i] : ~(X15 @ X17 @ X18))) = mserial) & ((^[X11 : (($i > $o) > $i > $o), X10 : $i] : (! [X14 : ($i > $o)] : (X11 @ X14 @ X10))) = mforall_prop) & ~(mfalse @ (d2unsorted @ d_unsorted_0)) & (mnot = (^[X11 : ($i > $o), X10 : $i] : (~(X11 @ X10)))) & (mpartially_functional = (^[X15 : ($i > $i > $o)] : (! [X0 : $i,X17 : $i,X18 : $i] : (~(X15 @ X17 @ X0) | ~(X15 @ X17 @ X18) | (X18 = X0))))) & ((^[X15 : ($i > $i > $o)] : (! [X17 : $i] : ~ ! [X18 : $i] : (~(X15 @ X17 @ X18) | ~ ! [X0 : $i] : ((X18 = X0) | ~(X15 @ X17 @ X0))))) = mfunctional) & (mexists_ind = (^[X11 : (mu > $i > $o), X13 : $i] : (~ ! [X8 : mu] : ~(X11 @ X8 @ X13)))) & ((^[X11 : ($i > $o)] : (! [X10 : $i] : (X11 @ X10))) = mvalid) & ((^[X15 : ($i > $i > $o)] : (! [X17 : $i,X18 : $i] : ((X15 @ X18 @ X17) | ~(X15 @ X17 @ X18)))) = msymmetric) & ((^[X15 : ($i > $i > $o)] : (! [X17 : $i,X0 : $i,X18 : $i] : (~(X15 @ X17 @ X18) | ~(X15 @ X18 @ X0) | (X15 @ X17 @ X0)))) = mtransitive) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((((d2unsorted @ X2)) = ((d2unsorted @ X3))) => (X2 = X3))),
% 0.23/0.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lcl698_1)).
% 0.23/0.29 thf(f2,conjecture,(
% 0.23/0.29 ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((mand @ (mimplies @ X0 @ X1) @ (mimplies @ X1 @ X0)))) = mequiv)),
% 0.23/0.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mequiv)).
% 0.23/0.29 thf(f3,negated_conjecture,(
% 0.23/0.29 ~ ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((mand @ (mimplies @ X0 @ X1) @ (mimplies @ X1 @ X0)))) = mequiv)),
% 0.23/0.29 inference(negated_conjecture,[status(cth)],[f2])).
% 0.23/0.29 thf(f4,plain,(
% 0.23/0.29 ~ (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ (mimplies @ Y0 @ Y1) @ (mimplies @ Y1 @ Y0))))))),
% 0.23/0.29 inference(fool_elimination,[],[f3])).
% 0.23/0.29 thf(f5,plain,(
% 0.23/0.29 ((^[X0 : (($i > $o) > $i > $o), X1 : $i] : (~ ! [X2 : ($i > $o)] : ~(X0 @ X2 @ X1))) = mexists_prop) & (mor = (^[X3 : ($i > $o), X4 : ($i > $o), X5 : $i] : ((X3 @ X5) | (X4 @ X5)))) & (meq_prop = (^[X6 : ($i > $o), X7 : ($i > $o), X8 : $i] : ((((X7 @ X8)) = ((X6 @ X8)))))) & ! [X9 : d_unsorted] : (d_unsorted_0 = X9) & (mimplies = (^[X10 : ($i > $o), X11 : ($i > $o), X12 : $i] : (~(X10 @ X12) | (X11 @ X12)))) & ((^[X13 : ($i > $i > $o)] : (! [X14 : $i,X15 : $i,X16 : $i] : (~(X13 @ X16 @ X15) | ~(X13 @ X16 @ X14) | ~ ! [X17 : $i] : (~(X13 @ X15 @ X17) | ~(X13 @ X14 @ X17))))) = mweakly_directed) & (mand = (^[X18 : ($i > $o), X19 : ($i > $o), X20 : $i] : (~(~(X19 @ X20) | ~(X18 @ X20))))) & (meuclidean = (^[X21 : ($i > $i > $o)] : (! [X22 : $i,X23 : $i,X24 : $i] : ((X21 @ X24 @ X22) | ~(X21 @ X23 @ X24) | ~(X21 @ X23 @ X22))))) & (mtrue @ (d2unsorted @ d_unsorted_0)) & (msatisfiable = (^[X25 : ($i > $o)] : (~ ! [X26 : $i] : ~(X25 @ X26)))) & (meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0)) & ! [X27 : $i] : ? [X28 : d_unsorted] : (((d2unsorted @ X28)) = X27) & ((^[X29 : ($i > $o), X30 : ($i > $o), X31 : $i] : (~((X30 @ X31) | ~(X29 @ X31)) | ~(~(X30 @ X31) | (X29 @ X31)))) = mxor) & ((^[X32 : ($i > $i > $o)] : (! [X33 : $i,X34 : $i] : (~ ! [X35 : $i] : (~(X32 @ X33 @ X35) | ~(X32 @ X35 @ X34)) | ~(X32 @ X33 @ X34)))) = mweakly_dense) & ((^[X36 : ($i > $i > $o)] : (! [X37 : $i,X38 : $i,X39 : $i] : ((X37 = X38) | (X36 @ X38 @ X37) | (X36 @ X37 @ X38) | ~(X36 @ X39 @ X38) | ~(X36 @ X39 @ X37)))) = mweakly_connected) & ! [X40 : d_mu] : (d_mu_0 = X40) & ((^[X41 : ($i > $i > $o)] : (! [X42 : $i] : (X41 @ X42 @ X42))) = mreflexive) & ! [X43 : d_mu,X44 : d_mu] : ((((d2mu @ X43)) = ((d2mu @ X44))) => (X43 = X44)) & ((^[X45 : ($i > $o), X46 : ($i > $o), X47 : $i] : (~(~(~(X46 @ X47) | (X45 @ X47)) | ~(~(X45 @ X47) | (X46 @ X47))))) = mequiv) & ((^[X48 : ($i > $o)] : (~ ! [X49 : $i] : (X48 @ X49))) = mcountersatisfiable) & ((^[X50 : ($i > $o)] : (! [X51 : $i] : ~(X50 @ X51))) = minvalid) & (mdia = (^[X52 : ($i > $i > $o), X53 : ($i > $o), X54 : $i] : (~ ! [X55 : $i] : (~(X52 @ X54 @ X55) | ~(X53 @ X55))))) & (mforall_ind = (^[X56 : (mu > $i > $o), X57 : $i] : (! [X58 : mu] : (X56 @ X58 @ X57)))) & (mimplied = (^[X59 : ($i > $o), X60 : ($i > $o), X61 : $i] : (~(X60 @ X61) | (X59 @ X61)))) & ((^[X62 : ($i > $i > $o), X63 : ($i > $o), X64 : $i] : (! [X65 : $i] : (~(X62 @ X64 @ X65) | (X63 @ X65)))) = mbox) & ! [X66 : mu] : ? [X67 : d_mu] : (((d2mu @ X67)) = X66) & ((^[X68 : ($i > $i > $o)] : (! [X69 : $i] : ~ ! [X70 : $i] : ~(X68 @ X69 @ X70))) = mserial) & ((^[X71 : (($i > $o) > $i > $o), X72 : $i] : (! [X73 : ($i > $o)] : (X71 @ X73 @ X72))) = mforall_prop) & ~(mfalse @ (d2unsorted @ d_unsorted_0)) & (mnot = (^[X74 : ($i > $o), X75 : $i] : (~(X74 @ X75)))) & (mpartially_functional = (^[X76 : ($i > $i > $o)] : (! [X77 : $i,X78 : $i,X79 : $i] : (~(X76 @ X78 @ X77) | ~(X76 @ X78 @ X79) | (X77 = X79))))) & ((^[X80 : ($i > $i > $o)] : (! [X81 : $i] : ~ ! [X82 : $i] : (~(X80 @ X81 @ X82) | ~ ! [X83 : $i] : ((X82 = X83) | ~(X80 @ X81 @ X83))))) = mfunctional) & (mexists_ind = (^[X84 : (mu > $i > $o), X85 : $i] : (~ ! [X86 : mu] : ~(X84 @ X86 @ X85)))) & ((^[X87 : ($i > $o)] : (! [X88 : $i] : (X87 @ X88))) = mvalid) & ((^[X89 : ($i > $i > $o)] : (! [X90 : $i,X91 : $i] : ((X89 @ X91 @ X90) | ~(X89 @ X90 @ X91)))) = msymmetric) & ((^[X92 : ($i > $i > $o)] : (! [X93 : $i,X94 : $i,X95 : $i] : (~(X92 @ X93 @ X95) | ~(X92 @ X95 @ X94) | (X92 @ X93 @ X94)))) = mtransitive) & ! [X96 : d_unsorted,X97 : d_unsorted] : ((((d2unsorted @ X97)) = ((d2unsorted @ X96))) => (X96 = X97))),
% 0.23/0.29 inference(rectify,[],[f1])).
% 0.23/0.29 thf(f6,plain,(
% 0.23/0.29 (mexists_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (~ (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (~ (Y0 @ Y2 @ Y1))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (meq_prop = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) = (Y0 @ Y2)))))))) & ! [X9 : d_unsorted] : (d_unsorted_0 = X9) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (mweakly_directed = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y0 @ Y3 @ Y4)) | (~ (Y0 @ Y2 @ Y4)))))) | (~ (Y0 @ Y1 @ Y3))) | (~ (Y0 @ Y1 @ Y2))))))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2)))))))))) & (meuclidean = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y2 @ Y3)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y1 @ Y3)))))))))) & (((mtrue @ (d2unsorted @ d_unsorted_0))) = $true) & (msatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (((meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X27 : $i] : ? [X28 : d_unsorted] : (((d2unsorted @ X28)) = X27) & (mxor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))) | (~ ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))))) & (mweakly_dense = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y3 @ Y1)) | (~ (Y0 @ Y2 @ Y3))))))))))))) & (mweakly_connected = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((~ (Y0 @ Y1 @ Y3)) | (~ (Y0 @ Y1 @ Y2))) | (Y0 @ Y3 @ Y2)) | (Y0 @ Y2 @ Y3)) | (Y3 = Y2)))))))))) & ! [X40 : d_mu] : (d_mu_0 = X40) & (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & ! [X43 : d_mu,X44 : d_mu] : ((((d2mu @ X43)) = ((d2mu @ X44))) => (X43 = X44)) & (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((Y1 @ Y2) | (~ (Y0 @ Y2)))) | (~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))))))))))) & (mcountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (minvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y1 @ Y3)) | (~ (Y0 @ Y2 @ Y3)))))))))))) & (mforall_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (!! @ mu @ (^[Y2 : mu]: (Y0 @ Y2 @ Y1))))))) & (mimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (~ (Y1 @ Y2))))))))) & (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3))))))))))) & ! [X66 : mu] : ? [X67 : d_mu] : (((d2mu @ X67)) = X66) & (mserial = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2))))))))) & (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1))))))) & ~ (((mfalse @ (d2unsorted @ d_unsorted_0))) = $true) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mpartially_functional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y3 = Y1) | (~ (Y0 @ Y2 @ Y1))) | (~ (Y0 @ Y2 @ Y3))))))))))) & (mfunctional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y1 @ Y3)) | (Y2 = Y3))))) | (~ (Y0 @ Y1 @ Y2)))))))))) & (mexists_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (~ (!! @ mu @ (^[Y2 : mu]: (~ (Y0 @ Y2 @ Y1))))))))) & (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y0 @ Y3 @ Y2) | (~ (Y0 @ Y1 @ Y2))) | (~ (Y0 @ Y3 @ Y1))))))))))) & ! [X96 : d_unsorted,X97 : d_unsorted] : ((((d2unsorted @ X97)) = ((d2unsorted @ X96))) => (X96 = X97))),
% 0.23/0.29 inference(fool_elimination,[],[f5])).
% 0.23/0.29 thf(f7,plain,(
% 0.23/0.29 (mequiv != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ (mimplies @ Y0 @ Y1) @ (mimplies @ Y1 @ Y0))))))),
% 0.23/0.29 inference(flattening,[],[f4])).
% 0.23/0.29 thf(f8,plain,(
% 0.23/0.29 (mexists_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (~ (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (~ (Y0 @ Y2 @ Y1))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (meq_prop = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) = (Y0 @ Y2)))))))) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (mweakly_directed = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y0 @ Y3 @ Y4)) | (~ (Y0 @ Y2 @ Y4)))))) | (~ (Y0 @ Y1 @ Y3))) | (~ (Y0 @ Y1 @ Y2))))))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2)))))))))) & (meuclidean = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y2 @ Y3)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y1 @ Y3)))))))))) & (((mtrue @ (d2unsorted @ d_unsorted_0))) = $true) & (msatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (((meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X1 : $i] : ? [X2 : d_unsorted] : (((d2unsorted @ X2)) = X1) & (mxor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))) | (~ ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))))) & (mweakly_dense = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y3 @ Y1)) | (~ (Y0 @ Y2 @ Y3))))))))))))) & (mweakly_connected = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((~ (Y0 @ Y1 @ Y3)) | (~ (Y0 @ Y1 @ Y2))) | (Y0 @ Y3 @ Y2)) | (Y0 @ Y2 @ Y3)) | (Y3 = Y2)))))))))) & ! [X3 : d_mu] : (d_mu_0 = X3) & (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & ! [X4 : d_mu,X5 : d_mu] : ((((d2mu @ X5)) = ((d2mu @ X4))) => (X4 = X5)) & (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((Y1 @ Y2) | (~ (Y0 @ Y2)))) | (~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))))))))))) & (mcountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (minvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y1 @ Y3)) | (~ (Y0 @ Y2 @ Y3)))))))))))) & (mforall_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (!! @ mu @ (^[Y2 : mu]: (Y0 @ Y2 @ Y1))))))) & (mimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (~ (Y1 @ Y2))))))))) & (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3))))))))))) & ! [X6 : mu] : ? [X7 : d_mu] : (((d2mu @ X7)) = X6) & (mserial = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2))))))))) & (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1))))))) & ~ (((mfalse @ (d2unsorted @ d_unsorted_0))) = $true) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mpartially_functional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y3 = Y1) | (~ (Y0 @ Y2 @ Y1))) | (~ (Y0 @ Y2 @ Y3))))))))))) & (mfunctional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y1 @ Y3)) | (Y2 = Y3))))) | (~ (Y0 @ Y1 @ Y2)))))))))) & (mexists_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (~ (!! @ mu @ (^[Y2 : mu]: (~ (Y0 @ Y2 @ Y1))))))))) & (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y0 @ Y3 @ Y2) | (~ (Y0 @ Y1 @ Y2))) | (~ (Y0 @ Y3 @ Y1))))))))))) & ! [X8 : d_unsorted,X9 : d_unsorted] : ((((d2unsorted @ X9)) = ((d2unsorted @ X8))) => (X8 = X9))),
% 0.23/0.29 inference(rectify,[],[f6])).
% 0.23/0.29 thf(f9,plain,(
% 0.23/0.29 (mweakly_dense = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y3 @ Y1)) | (~ (Y0 @ Y2 @ Y3))))))))))))) & ! [X8 : d_unsorted,X9 : d_unsorted] : ((((d2unsorted @ X9)) = ((d2unsorted @ X8))) => (X8 = X9)) & (msatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (mimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (~ (Y1 @ Y2))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mforall_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (!! @ mu @ (^[Y2 : mu]: (Y0 @ Y2 @ Y1))))))) & (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((Y1 @ Y2) | (~ (Y0 @ Y2)))) | (~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))))))))))) & (meq_prop = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) = (Y0 @ Y2)))))))) & (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (minvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y0 @ Y3 @ Y2) | (~ (Y0 @ Y1 @ Y2))) | (~ (Y0 @ Y3 @ Y1))))))))))) & (mcountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (((mtrue @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X3 : d_mu] : (d_mu_0 = X3) & (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y1 @ Y3)) | (~ (Y0 @ Y2 @ Y3)))))))))))) & (mserial = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2))))))))) & ! [X1 : $i] : ? [X2 : d_unsorted] : (((d2unsorted @ X2)) = X1) & ! [X6 : mu] : ? [X7 : d_mu] : (((d2mu @ X7)) = X6) & ! [X4 : d_mu,X5 : d_mu] : ((((d2mu @ X5)) = ((d2mu @ X4))) => (X4 = X5)) & (((meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (((mfalse @ (d2unsorted @ d_unsorted_0))) != $true) & (meuclidean = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y2 @ Y3)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y1 @ Y3)))))))))) & (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3))))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (mexists_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (~ (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (~ (Y0 @ Y2 @ Y1))))))))) & (mexists_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (~ (!! @ mu @ (^[Y2 : mu]: (~ (Y0 @ Y2 @ Y1))))))))) & (mweakly_directed = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y0 @ Y3 @ Y4)) | (~ (Y0 @ Y2 @ Y4)))))) | (~ (Y0 @ Y1 @ Y3))) | (~ (Y0 @ Y1 @ Y2))))))))))) & (mpartially_functional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y3 = Y1) | (~ (Y0 @ Y2 @ Y1))) | (~ (Y0 @ Y2 @ Y3))))))))))) & (mxor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))) | (~ ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))))) & (mfunctional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y1 @ Y3)) | (Y2 = Y3))))) | (~ (Y0 @ Y1 @ Y2)))))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2)))))))))) & (mweakly_connected = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((~ (Y0 @ Y1 @ Y3)) | (~ (Y0 @ Y1 @ Y2))) | (Y0 @ Y3 @ Y2)) | (Y0 @ Y2 @ Y3)) | (Y3 = Y2)))))))))) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0) & (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 0.23/0.29 inference(flattening,[],[f8])).
% 0.23/0.29 thf(f10,plain,(
% 0.23/0.29 (((mfalse @ (d2unsorted @ d_unsorted_0))) != $true) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((Y1 @ Y2) | (~ (Y0 @ Y2)))) | (~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))))))))))) & (mfunctional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y1 @ Y3)) | (Y2 = Y3))))) | (~ (Y0 @ Y1 @ Y2)))))))))) & (mimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (~ (Y1 @ Y2))))))))) & (mxor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))) | (~ ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))))) & (mweakly_directed = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y0 @ Y3 @ Y4)) | (~ (Y0 @ Y2 @ Y4)))))) | (~ (Y0 @ Y1 @ Y3))) | (~ (Y0 @ Y1 @ Y2))))))))))) & (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1))))))) & (((meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2)))))))))) & ! [X6 : mu] : ? [X7 : d_mu] : (((d2mu @ X7)) = X6) & ! [X3 : d_mu] : (d_mu_0 = X3) & (mweakly_dense = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y3 @ Y1)) | (~ (Y0 @ Y2 @ Y3))))))))))))) & (minvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((mtrue @ (d2unsorted @ d_unsorted_0))) = $true) & (mserial = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2))))))))) & (mforall_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (!! @ mu @ (^[Y2 : mu]: (Y0 @ Y2 @ Y1))))))) & (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y1 @ Y3)) | (~ (Y0 @ Y2 @ Y3)))))))))))) & (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0) & (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mexists_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (~ (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (~ (Y0 @ Y2 @ Y1))))))))) & (mcountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y0 @ Y3 @ Y2) | (~ (Y0 @ Y1 @ Y2))) | (~ (Y0 @ Y3 @ Y1))))))))))) & (mexists_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (~ (!! @ mu @ (^[Y2 : mu]: (~ (Y0 @ Y2 @ Y1))))))))) & ! [X9 : d_unsorted,X8 : d_unsorted] : ((X8 = X9) | (((d2unsorted @ X9)) != ((d2unsorted @ X8)))) & (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3))))))))))) & (mpartially_functional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y3 = Y1) | (~ (Y0 @ Y2 @ Y1))) | (~ (Y0 @ Y2 @ Y3))))))))))) & (mweakly_connected = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((~ (Y0 @ Y1 @ Y3)) | (~ (Y0 @ Y1 @ Y2))) | (Y0 @ Y3 @ Y2)) | (Y0 @ Y2 @ Y3)) | (Y3 = Y2)))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & ! [X1 : $i] : ? [X2 : d_unsorted] : (((d2unsorted @ X2)) = X1) & (meq_prop = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) = (Y0 @ Y2)))))))) & (msatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & ! [X5 : d_mu,X4 : d_mu] : ((((d2mu @ X5)) != ((d2mu @ X4))) | (X4 = X5)) & (meuclidean = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y2 @ Y3)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y1 @ Y3))))))))))),
% 0.23/0.29 inference(ennf_transformation,[],[f9])).
% 0.23/0.29 thf(f11,plain,(
% 0.23/0.29 (((mfalse @ (d2unsorted @ d_unsorted_0))) != $true) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((Y1 @ Y2) | (~ (Y0 @ Y2)))) | (~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))))))))))) & (mfunctional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y1 @ Y3)) | (Y2 = Y3))))) | (~ (Y0 @ Y1 @ Y2)))))))))) & (mimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (~ (Y1 @ Y2))))))))) & (mxor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))) | (~ ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))))) & (mweakly_directed = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y0 @ Y3 @ Y4)) | (~ (Y0 @ Y2 @ Y4)))))) | (~ (Y0 @ Y1 @ Y3))) | (~ (Y0 @ Y1 @ Y2))))))))))) & (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1))))))) & (((meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2)))))))))) & ! [X0 : mu] : ? [X1 : d_mu] : (((d2mu @ X1)) = X0) & ! [X2 : d_mu] : (d_mu_0 = X2) & (mweakly_dense = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y3 @ Y1)) | (~ (Y0 @ Y2 @ Y3))))))))))))) & (minvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((mtrue @ (d2unsorted @ d_unsorted_0))) = $true) & (mserial = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2))))))))) & (mforall_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (!! @ mu @ (^[Y2 : mu]: (Y0 @ Y2 @ Y1))))))) & (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y1 @ Y3)) | (~ (Y0 @ Y2 @ Y3)))))))))))) & (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & ! [X3 : d_unsorted] : (d_unsorted_0 = X3) & (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mexists_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (~ (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (~ (Y0 @ Y2 @ Y1))))))))) & (mcountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y0 @ Y3 @ Y2) | (~ (Y0 @ Y1 @ Y2))) | (~ (Y0 @ Y3 @ Y1))))))))))) & (mexists_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (~ (!! @ mu @ (^[Y2 : mu]: (~ (Y0 @ Y2 @ Y1))))))))) & ! [X4 : d_unsorted,X5 : d_unsorted] : ((X4 = X5) | (((d2unsorted @ X5)) != ((d2unsorted @ X4)))) & (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3))))))))))) & (mpartially_functional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y3 = Y1) | (~ (Y0 @ Y2 @ Y1))) | (~ (Y0 @ Y2 @ Y3))))))))))) & (mweakly_connected = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((~ (Y0 @ Y1 @ Y3)) | (~ (Y0 @ Y1 @ Y2))) | (Y0 @ Y3 @ Y2)) | (Y0 @ Y2 @ Y3)) | (Y3 = Y2)))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & ! [X6 : $i] : ? [X7 : d_unsorted] : (((d2unsorted @ X7)) = X6) & (meq_prop = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) = (Y0 @ Y2)))))))) & (msatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & ! [X8 : d_mu,X9 : d_mu] : ((((d2mu @ X9)) != ((d2mu @ X8))) | (X8 = X9)) & (meuclidean = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y2 @ Y3)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y1 @ Y3))))))))))),
% 0.23/0.29 inference(rectify,[],[f10])).
% 0.23/0.29 thf(f12,plain,(
% 0.23/0.29 (((mfalse @ (d2unsorted @ d_unsorted_0))) != $true) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((Y1 @ Y2) | (~ (Y0 @ Y2)))) | (~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))))))))))) & (mfunctional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y1 @ Y3)) | (Y2 = Y3))))) | (~ (Y0 @ Y1 @ Y2)))))))))) & (mimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (~ (Y1 @ Y2))))))))) & (mxor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ ((Y0 @ Y2) | (~ (Y1 @ Y2)))) | (~ ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))))) & (mweakly_directed = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y0 @ Y3 @ Y4)) | (~ (Y0 @ Y2 @ Y4)))))) | (~ (Y0 @ Y1 @ Y3))) | (~ (Y0 @ Y1 @ Y2))))))))))) & (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1))))))) & (((meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2)))))))))) & ! [X0 : mu] : (((d2mu @ (sK0 @ X0))) = X0) & ! [X2 : d_mu] : (d_mu_0 = X2) & (mweakly_dense = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y3 @ Y1)) | (~ (Y0 @ Y2 @ Y3))))))))))))) & (minvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((mtrue @ (d2unsorted @ d_unsorted_0))) = $true) & (mserial = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2))))))))) & (mforall_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (!! @ mu @ (^[Y2 : mu]: (Y0 @ Y2 @ Y1))))))) & (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y1 @ Y3)) | (~ (Y0 @ Y2 @ Y3)))))))))))) & (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & ! [X3 : d_unsorted] : (d_unsorted_0 = X3) & (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mexists_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (~ (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (~ (Y0 @ Y2 @ Y1))))))))) & (mcountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y0 @ Y3 @ Y2) | (~ (Y0 @ Y1 @ Y2))) | (~ (Y0 @ Y3 @ Y1))))))))))) & (mexists_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (~ (!! @ mu @ (^[Y2 : mu]: (~ (Y0 @ Y2 @ Y1))))))))) & ! [X4 : d_unsorted,X5 : d_unsorted] : ((X4 = X5) | (((d2unsorted @ X5)) != ((d2unsorted @ X4)))) & (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3))))))))))) & (mpartially_functional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y3 = Y1) | (~ (Y0 @ Y2 @ Y1))) | (~ (Y0 @ Y2 @ Y3))))))))))) & (mweakly_connected = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((~ (Y0 @ Y1 @ Y3)) | (~ (Y0 @ Y1 @ Y2))) | (Y0 @ Y3 @ Y2)) | (Y0 @ Y2 @ Y3)) | (Y3 = Y2)))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & ! [X6 : $i] : (((d2unsorted @ (sK1 @ X6))) = X6) & (meq_prop = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) = (Y0 @ Y2)))))))) & (msatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & ! [X8 : d_mu,X9 : d_mu] : ((((d2mu @ X9)) != ((d2mu @ X8))) | (X8 = X9)) & (meuclidean = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y2 @ Y3)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y1 @ Y3))))))))))),
% 0.23/0.29 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X7,sK1 @ X6),skolemize(X7,sK1 @ X6)],[f11])).
% 0.23/0.29 thf(f18,plain,(
% 0.23/0.29 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2)))))))))),
% 0.23/0.29 inference(cnf_transformation,[],[f12])).
% 0.23/0.29 thf(f40,plain,(
% 0.23/0.29 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2))))))))))),
% 0.23/0.29 inference(cnf_transformation,[],[f12])).
% 0.23/0.29 thf(f47,plain,(
% 0.23/0.29 (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((Y1 @ Y2) | (~ (Y0 @ Y2)))) | (~ ((Y0 @ Y2) | (~ (Y1 @ Y2))))))))))))),
% 0.23/0.29 inference(cnf_transformation,[],[f12])).
% 0.23/0.29 thf(f50,plain,(
% 0.23/0.29 (mequiv != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ (mimplies @ Y0 @ Y1) @ (mimplies @ Y1 @ Y0))))))),
% 0.23/0.29 inference(cnf_transformation,[],[f7])).
% 0.23/0.29 thf(f53,plain,(
% 0.23/0.29 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((Y1 @ Y2) | (~ (Y0 @ Y2)))) | (~ ((Y0 @ Y2) | (~ (Y1 @ Y2))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ ((~ (Y2 @ Y4)) | (~ (Y3 @ Y4))))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y3 @ Y4) | (~ (Y2 @ Y4)))))))) @ Y0 @ Y1) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y3 @ Y4) | (~ (Y2 @ Y4)))))))) @ Y1 @ Y0))))))),
% 0.23/0.29 inference(definition_unfolding,[],[f50,f47,f40,f18,f18])).
% 0.23/0.29 thf(f54,plain,(
% 0.23/0.29 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((Y1 @ Y2) | (~ (Y0 @ Y2)))) | (~ ((Y0 @ Y2) | (~ (Y1 @ Y2))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((Y1 @ Y2) | (~ (Y0 @ Y2)))) | (~ ((Y0 @ Y2) | (~ (Y1 @ Y2))))))))))))),
% 0.23/0.29 inference(beta-eta_normalization,[],[f53])).
% 0.23/0.29 thf(f55,plain,(
% 0.23/0.29 $false),
% 0.23/0.29 inference(trivial_inequality_removal,[],[f54])).
% 0.23/0.29 % SZS output end Proof for theBenchmark
% 0.23/0.29 % (796901)------------------------------
% 0.23/0.29 % (796901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.29 % (796901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.29 % (796901)CaDiCaL version: 2.1.3
% 0.23/0.29 % (796901)Termination reason: Refutation
% 0.23/0.29 % (796901)Time elapsed: 0.011 s
% 0.23/0.29 % (796901)Peak memory usage: 12 MB
% 0.23/0.29 % (796901)Instructions burned: 23 (million)
% 0.23/0.29 % (796895)Success in time 0.046 s
% 0.23/0.29 % Vampire exiting
%------------------------------------------------------------------------------