%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:40:45 AM UTC 2026
% Result : Theorem 0.20s 0.26s
% Output : Refutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX180^1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n011.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 16:10:01 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.26 % (275225)Will run a generic schedule for satisfiability detection.
% 0.20/0.26 % (275234)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=51087912:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.26 % (275234)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.26 % (275234) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-275225-275234"...
% 0.20/0.26 % (275231)% WARNING: option uhcvi not known.
% 0.20/0.26 % (275234)...printing done.
% 0.20/0.26 % (275234)Refutation found. Thanks to Tanya!
% 0.20/0.26 % SZS status Theorem for theBenchmark
% 0.20/0.26 % SZS output start Proof for theBenchmark
% 0.20/0.26 thf(type_def_5, type, unsorted: $tType).
% 0.20/0.26 thf(type_def_6, type, mu: $tType).
% 0.20/0.26 thf(type_def_7, type, sTfun: ($tType * $tType) > $tType).
% 0.20/0.26 thf(type_def_8, type, d_unsorted: $tType).
% 0.20/0.26 thf(type_def_9, type, d_mu: $tType).
% 0.20/0.26 thf(func_def_0, type, meq_ind: (mu > mu > $i > $o)).
% 0.20/0.26 thf(func_def_1, type, meq_prop: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_2, type, mnot: (($i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_3, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_4, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_5, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_6, type, mimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_7, type, mequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_8, type, mxor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_9, type, mforall_ind: ((mu > $i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_10, type, mforall_prop: ((($i > $o) > $i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_11, type, mexists_ind: ((mu > $i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_12, type, mexists_prop: ((($i > $o) > $i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_13, type, mtrue: ($i > $o)).
% 0.20/0.26 thf(func_def_14, type, mfalse: ($i > $o)).
% 0.20/0.26 thf(func_def_15, type, mbox: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_16, type, mdia: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.26 thf(func_def_17, type, mreflexive: (($i > $i > $o) > $o)).
% 0.20/0.26 thf(func_def_18, type, msymmetric: (($i > $i > $o) > $o)).
% 0.20/0.26 thf(func_def_19, type, mserial: (($i > $i > $o) > $o)).
% 0.20/0.26 thf(func_def_20, type, mtransitive: (($i > $i > $o) > $o)).
% 0.20/0.26 thf(func_def_21, type, meuclidean: (($i > $i > $o) > $o)).
% 0.20/0.26 thf(func_def_22, type, mpartially_functional: (($i > $i > $o) > $o)).
% 0.20/0.26 thf(func_def_23, type, mfunctional: (($i > $i > $o) > $o)).
% 0.20/0.26 thf(func_def_24, type, mweakly_dense: (($i > $i > $o) > $o)).
% 0.20/0.26 thf(func_def_25, type, mweakly_connected: (($i > $i > $o) > $o)).
% 0.20/0.26 thf(func_def_26, type, mweakly_directed: (($i > $i > $o) > $o)).
% 0.20/0.26 thf(func_def_27, type, mvalid: (($i > $o) > $o)).
% 0.20/0.26 thf(func_def_28, type, minvalid: (($i > $o) > $o)).
% 0.20/0.26 thf(func_def_29, type, msatisfiable: (($i > $o) > $o)).
% 0.20/0.26 thf(func_def_30, type, mcountersatisfiable: (($i > $o) > $o)).
% 0.20/0.26 thf(func_def_31, type, d2unsorted: (d_unsorted > $i)).
% 0.20/0.26 thf(func_def_32, type, d2mu: (d_mu > mu)).
% 0.20/0.26 thf(func_def_33, type, d_unsorted_0: d_unsorted).
% 0.20/0.26 thf(func_def_34, type, d_mu_0: d_mu).
% 0.20/0.26 thf(func_def_36, type, db2: !>[X0: $tType]:(X0)).
% 0.20/0.26 thf(func_def_37, type, db0: !>[X0: $tType]:(X0)).
% 0.20/0.26 thf(func_def_38, type, db1: !>[X0: $tType]:(X0)).
% 0.20/0.26 thf(func_def_39, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.20/0.26 thf(func_def_40, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.20/0.26 thf(func_def_41, type, vNOT: ($o > $o)).
% 0.20/0.26 thf(func_def_42, type, vOR: ($o > $o > $o)).
% 0.20/0.26 thf(func_def_43, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.20/0.26 thf(func_def_44, type, db3: !>[X0: $tType]:(X0)).
% 0.20/0.26 thf(func_def_45, type, db4: !>[X0: $tType]:(X0)).
% 0.20/0.26 thf(func_def_48, type, sK0: (mu > d_mu)).
% 0.20/0.26 thf(func_def_49, type, sK1: ($i > d_unsorted)).
% 0.20/0.26 thf(f1,axiom,(
% 0.20/0.26 ~(mfalse @ (d2unsorted @ d_unsorted_0)) & (mtrue @ (d2unsorted @ d_unsorted_0)) & (meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0)) & (mcountersatisfiable = (^[X11 : ($i > $o)] : (~ ! [X10 : $i] : (X11 @ X10)))) & (msatisfiable = (^[X11 : ($i > $o)] : (~ ! [X10 : $i] : ~(X11 @ X10)))) & (minvalid = (^[X11 : ($i > $o)] : (! [X10 : $i] : ~(X11 @ X10)))) & (mvalid = (^[X11 : ($i > $o)] : (! [X10 : $i] : (X11 @ X10)))) & (mweakly_directed = (^[X15 : ($i > $i > $o)] : (! [X17 : $i,X18 : $i,X0 : $i] : (~ ! [X16 : $i] : (~(X15 @ X0 @ X16) | ~(X15 @ X18 @ X16)) | ~(X15 @ X17 @ X0) | ~(X15 @ X17 @ X18))))) & (mweakly_connected = (^[X15 : ($i > $i > $o)] : (! [X17 : $i,X18 : $i,X0 : $i] : ((X15 @ X0 @ X18) | (X18 = X0) | (X15 @ X18 @ X0) | ~(X15 @ X17 @ X0) | ~(X15 @ X17 @ X18))))) & (mweakly_dense = (^[X15 : ($i > $i > $o)] : (! [X17 : $i,X18 : $i] : (~ ! [X19 : $i] : (~(X15 @ X19 @ X18) | ~(X15 @ X17 @ X19)) | ~(X15 @ X17 @ X18))))) & (mfunctional = (^[X15 : ($i > $i > $o)] : (! [X17 : $i] : ~ ! [X18 : $i] : (~ ! [X0 : $i] : ((X18 = X0) | ~(X15 @ X17 @ X0)) | ~(X15 @ X17 @ X18))))) & (mpartially_functional = (^[X15 : ($i > $i > $o)] : (! [X17 : $i,X18 : $i,X0 : $i] : ((X18 = X0) | ~(X15 @ X17 @ X0) | ~(X15 @ X17 @ X18))))) & (meuclidean = (^[X15 : ($i > $i > $o)] : (! [X17 : $i,X18 : $i,X0 : $i] : ((X15 @ X18 @ X0) | ~(X15 @ X17 @ X0) | ~(X15 @ X17 @ X18))))) & (mtransitive = (^[X15 : ($i > $i > $o)] : (! [X17 : $i,X18 : $i,X0 : $i] : ((X15 @ X17 @ X0) | ~(X15 @ X18 @ X0) | ~(X15 @ X17 @ X18))))) & (mserial = (^[X15 : ($i > $i > $o)] : (! [X17 : $i] : ~ ! [X18 : $i] : ~(X15 @ X17 @ X18)))) & (msymmetric = (^[X15 : ($i > $i > $o)] : (! [X17 : $i,X18 : $i] : ((X15 @ X18 @ X17) | ~(X15 @ X17 @ X18))))) & (mreflexive = (^[X15 : ($i > $i > $o)] : (! [X17 : $i] : (X15 @ X17 @ X17)))) & (mdia = (^[X15 : ($i > $i > $o), X11 : ($i > $o), X13 : $i] : (~ ! [X16 : $i] : (~(X11 @ X16) | ~(X15 @ X13 @ X16))))) & (mbox = (^[X15 : ($i > $i > $o), X11 : ($i > $o), X10 : $i] : (! [X16 : $i] : ((X11 @ X16) | ~(X15 @ X10 @ X16))))) & (mexists_prop = (^[X11 : (($i > $o) > $i > $o), X13 : $i] : (~ ! [X14 : ($i > $o)] : ~(X11 @ X14 @ X13)))) & (mexists_ind = (^[X11 : (mu > $i > $o), X13 : $i] : (~ ! [X8 : mu] : ~(X11 @ X8 @ X13)))) & (mforall_prop = (^[X11 : (($i > $o) > $i > $o), X10 : $i] : (! [X14 : ($i > $o)] : (X11 @ X14 @ X10)))) & (mforall_ind = (^[X11 : (mu > $i > $o), X10 : $i] : (! [X8 : mu] : (X11 @ X8 @ X10)))) & (mxor = (^[X11 : ($i > $o), X12 : ($i > $o), X13 : $i] : (~((X11 @ X13) | ~(X12 @ X13)) | ~((X12 @ X13) | ~(X11 @ X13))))) & (mequiv = (^[X11 : ($i > $o), X12 : ($i > $o), X13 : $i] : (~(~((X11 @ X13) | ~(X12 @ X13)) | ~((X12 @ X13) | ~(X11 @ X13)))))) & (mimplied = (^[X11 : ($i > $o), X12 : ($i > $o), X13 : $i] : ((X11 @ X13) | ~(X12 @ X13)))) & (mimplies = (^[X11 : ($i > $o), X12 : ($i > $o), X13 : $i] : ((X12 @ X13) | ~(X11 @ X13)))) & (mand = (^[X11 : ($i > $o), X12 : ($i > $o), X13 : $i] : (~(~(X12 @ X13) | ~(X11 @ X13))))) & (mor = (^[X11 : ($i > $o), X12 : ($i > $o), X10 : $i] : ((X12 @ X10) | (X11 @ X10)))) & (mnot = (^[X11 : ($i > $o), X10 : $i] : (~(X11 @ X10)))) & (meq_prop = (^[X8 : ($i > $o), X9 : ($i > $o), X10 : $i] : ((((X8 @ X10)) = ((X9 @ X10)))))) & ! [X6 : d_mu,X7 : d_mu] : ((((d2mu @ X6)) = ((d2mu @ X7))) => (X6 = X7)) & ! [X5 : d_mu] : (X5 = d_mu_0) & ! [X4 : mu] : ? [X5 : d_mu] : (X4 = ((d2mu @ X5))) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((((d2unsorted @ X2)) = ((d2unsorted @ X3))) => (X2 = X3)) & ! [X1 : d_unsorted] : (X1 = d_unsorted_0) & ! [X0 : $i] : ? [X1 : d_unsorted] : (X0 = ((d2unsorted @ X1)))),
% 0.20/0.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lcl698_1)).
% 0.20/0.26 thf(f2,conjecture,(
% 0.20/0.26 (mequiv = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mand @ (mimplies @ X0 @ X1) @ (mimplies @ X1 @ X0)))))),
% 0.20/0.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mequiv)).
% 0.20/0.26 thf(f3,negated_conjecture,(
% 0.20/0.26 ~ (mequiv = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mand @ (mimplies @ X0 @ X1) @ (mimplies @ X1 @ X0)))))),
% 0.20/0.26 inference(negated_conjecture,[status(cth)],[f2])).
% 0.20/0.26 thf(f4,plain,(
% 0.20/0.26 ~(mfalse @ (d2unsorted @ d_unsorted_0)) & (mtrue @ (d2unsorted @ d_unsorted_0)) & (meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0)) & (mcountersatisfiable = (^[X0 : ($i > $o)] : (~ ! [X1 : $i] : (X0 @ X1)))) & (msatisfiable = (^[X2 : ($i > $o)] : (~ ! [X3 : $i] : ~(X2 @ X3)))) & (minvalid = (^[X4 : ($i > $o)] : (! [X5 : $i] : ~(X4 @ X5)))) & (mvalid = (^[X6 : ($i > $o)] : (! [X7 : $i] : (X6 @ X7)))) & (mweakly_directed = (^[X8 : ($i > $i > $o)] : (! [X9 : $i,X10 : $i,X11 : $i] : (~ ! [X12 : $i] : (~(X8 @ X11 @ X12) | ~(X8 @ X10 @ X12)) | ~(X8 @ X9 @ X11) | ~(X8 @ X9 @ X10))))) & (mweakly_connected = (^[X13 : ($i > $i > $o)] : (! [X14 : $i,X15 : $i,X16 : $i] : ((X13 @ X16 @ X15) | (X15 = X16) | (X13 @ X15 @ X16) | ~(X13 @ X14 @ X16) | ~(X13 @ X14 @ X15))))) & (mweakly_dense = (^[X17 : ($i > $i > $o)] : (! [X18 : $i,X19 : $i] : (~ ! [X20 : $i] : (~(X17 @ X20 @ X19) | ~(X17 @ X18 @ X20)) | ~(X17 @ X18 @ X19))))) & (mfunctional = (^[X21 : ($i > $i > $o)] : (! [X22 : $i] : ~ ! [X23 : $i] : (~ ! [X24 : $i] : ((X23 = X24) | ~(X21 @ X22 @ X24)) | ~(X21 @ X22 @ X23))))) & (mpartially_functional = (^[X25 : ($i > $i > $o)] : (! [X26 : $i,X27 : $i,X28 : $i] : ((X27 = X28) | ~(X25 @ X26 @ X28) | ~(X25 @ X26 @ X27))))) & (meuclidean = (^[X29 : ($i > $i > $o)] : (! [X30 : $i,X31 : $i,X32 : $i] : ((X29 @ X31 @ X32) | ~(X29 @ X30 @ X32) | ~(X29 @ X30 @ X31))))) & (mtransitive = (^[X33 : ($i > $i > $o)] : (! [X34 : $i,X35 : $i,X36 : $i] : ((X33 @ X34 @ X36) | ~(X33 @ X35 @ X36) | ~(X33 @ X34 @ X35))))) & (mserial = (^[X37 : ($i > $i > $o)] : (! [X38 : $i] : ~ ! [X39 : $i] : ~(X37 @ X38 @ X39)))) & (msymmetric = (^[X40 : ($i > $i > $o)] : (! [X41 : $i,X42 : $i] : ((X40 @ X42 @ X41) | ~(X40 @ X41 @ X42))))) & (mreflexive = (^[X43 : ($i > $i > $o)] : (! [X44 : $i] : (X43 @ X44 @ X44)))) & (mdia = (^[X45 : ($i > $i > $o), X46 : ($i > $o), X47 : $i] : (~ ! [X48 : $i] : (~(X46 @ X48) | ~(X45 @ X47 @ X48))))) & (mbox = (^[X49 : ($i > $i > $o), X50 : ($i > $o), X51 : $i] : (! [X52 : $i] : ((X50 @ X52) | ~(X49 @ X51 @ X52))))) & (mexists_prop = (^[X53 : (($i > $o) > $i > $o), X54 : $i] : (~ ! [X55 : ($i > $o)] : ~(X53 @ X55 @ X54)))) & (mexists_ind = (^[X56 : (mu > $i > $o), X57 : $i] : (~ ! [X58 : mu] : ~(X56 @ X58 @ X57)))) & (mforall_prop = (^[X59 : (($i > $o) > $i > $o), X60 : $i] : (! [X61 : ($i > $o)] : (X59 @ X61 @ X60)))) & (mforall_ind = (^[X62 : (mu > $i > $o), X63 : $i] : (! [X64 : mu] : (X62 @ X64 @ X63)))) & (mxor = (^[X65 : ($i > $o), X66 : ($i > $o), X67 : $i] : (~((X65 @ X67) | ~(X66 @ X67)) | ~((X66 @ X67) | ~(X65 @ X67))))) & (mequiv = (^[X68 : ($i > $o), X69 : ($i > $o), X70 : $i] : (~(~((X68 @ X70) | ~(X69 @ X70)) | ~((X69 @ X70) | ~(X68 @ X70)))))) & (mimplied = (^[X71 : ($i > $o), X72 : ($i > $o), X73 : $i] : ((X71 @ X73) | ~(X72 @ X73)))) & (mimplies = (^[X74 : ($i > $o), X75 : ($i > $o), X76 : $i] : ((X75 @ X76) | ~(X74 @ X76)))) & (mand = (^[X77 : ($i > $o), X78 : ($i > $o), X79 : $i] : (~(~(X78 @ X79) | ~(X77 @ X79))))) & (mor = (^[X80 : ($i > $o), X81 : ($i > $o), X82 : $i] : ((X81 @ X82) | (X80 @ X82)))) & (mnot = (^[X83 : ($i > $o), X84 : $i] : (~(X83 @ X84)))) & (meq_prop = (^[X85 : ($i > $o), X86 : ($i > $o), X87 : $i] : ((((X85 @ X87)) = ((X86 @ X87)))))) & ! [X88 : d_mu,X89 : d_mu] : ((((d2mu @ X88)) = ((d2mu @ X89))) => (X88 = X89)) & ! [X90 : d_mu] : (d_mu_0 = X90) & ! [X91 : mu] : ? [X92 : d_mu] : (((d2mu @ X92)) = X91) & ! [X93 : d_unsorted,X94 : d_unsorted] : ((((d2unsorted @ X93)) = ((d2unsorted @ X94))) => (X93 = X94)) & ! [X95 : d_unsorted] : (d_unsorted_0 = X95) & ! [X96 : $i] : ? [X97 : d_unsorted] : (((d2unsorted @ X97)) = X96)),
% 0.20/0.26 inference(rectify,[],[f1])).
% 0.20/0.26 thf(f5,plain,(
% 0.20/0.26 ~ (((mfalse @ (d2unsorted @ d_unsorted_0))) = $true) & (((mtrue @ (d2unsorted @ d_unsorted_0))) = $true) & (((meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (mcountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (msatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (minvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (mweakly_directed = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y0 @ Y2 @ Y4)) | (~ (Y0 @ Y1 @ Y4))))))))))))))) & (mweakly_connected = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y0 @ Y2 @ Y1)) | (Y2 = Y1)) | (Y0 @ Y1 @ Y2)))))))))) & (mweakly_dense = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (~ (Y0 @ Y3 @ Y1))))))))))))) & (mfunctional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y1 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y1 @ Y3)) | (Y2 = Y3))))))))))))) & (mpartially_functional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y2 = Y1)))))))))) & (meuclidean = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y0 @ Y2 @ Y1)))))))))) & (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1)))))))))) & (mserial = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2))))))))) & (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (~ (Y1 @ Y3)))))))))))) & (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) & (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))))))))) & (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1))))))) & (mforall_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (!! @ mu @ (^[Y2 : mu]: (Y0 @ Y2 @ Y1))))))) & (mxor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))))) & (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2))))))))))) & (mimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2)))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (meq_prop = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) = (Y1 @ Y2)))))))) & ! [X88 : d_mu,X89 : d_mu] : ((((d2mu @ X88)) = ((d2mu @ X89))) => (X88 = X89)) & ! [X90 : d_mu] : (d_mu_0 = X90) & ! [X91 : mu] : ? [X92 : d_mu] : (((d2mu @ X92)) = X91) & ! [X93 : d_unsorted,X94 : d_unsorted] : ((((d2unsorted @ X93)) = ((d2unsorted @ X94))) => (X93 = X94)) & ! [X95 : d_unsorted] : (d_unsorted_0 = X95) & ! [X96 : $i] : ? [X97 : d_unsorted] : (((d2unsorted @ X97)) = X96)),
% 0.20/0.26 inference(fool_elimination,[],[f4])).
% 0.20/0.26 thf(f6,plain,(
% 0.20/0.26 ~ (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ (mimplies @ Y0 @ Y1) @ (mimplies @ Y1 @ Y0))))))),
% 0.20/0.26 inference(fool_elimination,[],[f3])).
% 0.20/0.26 thf(f7,plain,(
% 0.20/0.26 ~ (((mfalse @ (d2unsorted @ d_unsorted_0))) = $true) & (((mtrue @ (d2unsorted @ d_unsorted_0))) = $true) & (((meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (mcountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (msatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (minvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (mweakly_directed = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y0 @ Y2 @ Y4)) | (~ (Y0 @ Y1 @ Y4))))))))))))))) & (mweakly_connected = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y0 @ Y2 @ Y1)) | (Y2 = Y1)) | (Y0 @ Y1 @ Y2)))))))))) & (mweakly_dense = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (~ (Y0 @ Y3 @ Y1))))))))))))) & (mfunctional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y1 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y1 @ Y3)) | (Y2 = Y3))))))))))))) & (mpartially_functional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y2 = Y1)))))))))) & (meuclidean = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y0 @ Y2 @ Y1)))))))))) & (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1)))))))))) & (mserial = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2))))))))) & (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (~ (Y1 @ Y3)))))))))))) & (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) & (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))))))))) & (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1))))))) & (mforall_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (!! @ mu @ (^[Y2 : mu]: (Y0 @ Y2 @ Y1))))))) & (mxor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))))) & (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2))))))))))) & (mimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2)))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (meq_prop = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) = (Y1 @ Y2)))))))) & ! [X0 : d_mu,X1 : d_mu] : ((((d2mu @ X0)) = ((d2mu @ X1))) => (X0 = X1)) & ! [X2 : d_mu] : (d_mu_0 = X2) & ! [X3 : mu] : ? [X4 : d_mu] : (((d2mu @ X4)) = X3) & ! [X5 : d_unsorted,X6 : d_unsorted] : ((((d2unsorted @ X5)) = ((d2unsorted @ X6))) => (X5 = X6)) & ! [X7 : d_unsorted] : (d_unsorted_0 = X7) & ! [X8 : $i] : ? [X9 : d_unsorted] : (((d2unsorted @ X9)) = X8)),
% 0.20/0.26 inference(rectify,[],[f5])).
% 0.20/0.26 thf(f8,plain,(
% 0.20/0.26 (((mfalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((mtrue @ (d2unsorted @ d_unsorted_0))) = $true) & (((meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (mcountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (msatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (minvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (mweakly_directed = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y0 @ Y2 @ Y4)) | (~ (Y0 @ Y1 @ Y4))))))))))))))) & (mweakly_connected = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y0 @ Y2 @ Y1)) | (Y2 = Y1)) | (Y0 @ Y1 @ Y2)))))))))) & (mweakly_dense = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (~ (Y0 @ Y3 @ Y1))))))))))))) & (mfunctional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y1 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y1 @ Y3)) | (Y2 = Y3))))))))))))) & (mpartially_functional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y2 = Y1)))))))))) & (meuclidean = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y0 @ Y2 @ Y1)))))))))) & (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1)))))))))) & (mserial = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2))))))))) & (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (~ (Y1 @ Y3)))))))))))) & (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) & (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))))))))) & (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1))))))) & (mforall_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (!! @ mu @ (^[Y2 : mu]: (Y0 @ Y2 @ Y1))))))) & (mxor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))))) & (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2))))))))))) & (mimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2)))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (meq_prop = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) = (Y1 @ Y2)))))))) & ! [X0 : d_mu,X1 : d_mu] : ((((d2mu @ X0)) = ((d2mu @ X1))) => (X0 = X1)) & ! [X2 : d_mu] : (d_mu_0 = X2) & ! [X3 : mu] : ? [X4 : d_mu] : (((d2mu @ X4)) = X3) & ! [X5 : d_unsorted,X6 : d_unsorted] : ((((d2unsorted @ X5)) = ((d2unsorted @ X6))) => (X5 = X6)) & ! [X7 : d_unsorted] : (d_unsorted_0 = X7) & ! [X8 : $i] : ? [X9 : d_unsorted] : (((d2unsorted @ X9)) = X8)),
% 0.20/0.26 inference(flattening,[],[f7])).
% 0.20/0.26 thf(f9,plain,(
% 0.20/0.26 (mequiv != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ (mimplies @ Y0 @ Y1) @ (mimplies @ Y1 @ Y0))))))),
% 0.20/0.26 inference(flattening,[],[f6])).
% 0.20/0.26 thf(f10,plain,(
% 0.20/0.26 (((mfalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((mtrue @ (d2unsorted @ d_unsorted_0))) = $true) & (((meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (mcountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (msatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (minvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (mweakly_directed = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y0 @ Y2 @ Y4)) | (~ (Y0 @ Y1 @ Y4))))))))))))))) & (mweakly_connected = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y0 @ Y2 @ Y1)) | (Y2 = Y1)) | (Y0 @ Y1 @ Y2)))))))))) & (mweakly_dense = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (~ (Y0 @ Y3 @ Y1))))))))))))) & (mfunctional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y1 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y1 @ Y3)) | (Y2 = Y3))))))))))))) & (mpartially_functional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y2 = Y1)))))))))) & (meuclidean = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y0 @ Y2 @ Y1)))))))))) & (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1)))))))))) & (mserial = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2))))))))) & (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (~ (Y1 @ Y3)))))))))))) & (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) & (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))))))))) & (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1))))))) & (mforall_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (!! @ mu @ (^[Y2 : mu]: (Y0 @ Y2 @ Y1))))))) & (mxor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))))) & (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2))))))))))) & (mimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2)))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (meq_prop = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) = (Y1 @ Y2)))))))) & ! [X0 : d_mu,X1 : d_mu] : ((X0 = X1) | (((d2mu @ X0)) != ((d2mu @ X1)))) & ! [X2 : d_mu] : (d_mu_0 = X2) & ! [X3 : mu] : ? [X4 : d_mu] : (((d2mu @ X4)) = X3) & ! [X5 : d_unsorted,X6 : d_unsorted] : ((X5 = X6) | (((d2unsorted @ X5)) != ((d2unsorted @ X6)))) & ! [X7 : d_unsorted] : (d_unsorted_0 = X7) & ! [X8 : $i] : ? [X9 : d_unsorted] : (((d2unsorted @ X9)) = X8)),
% 0.20/0.26 inference(ennf_transformation,[],[f8])).
% 0.20/0.26 thf(f11,plain,(
% 0.20/0.26 (((mfalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((mtrue @ (d2unsorted @ d_unsorted_0))) = $true) & (((meq_ind @ (d2mu @ d_mu_0) @ (d2mu @ d_mu_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (mcountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (msatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (minvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (mweakly_directed = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y0 @ Y2 @ Y4)) | (~ (Y0 @ Y1 @ Y4))))))))))))))) & (mweakly_connected = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y0 @ Y2 @ Y1)) | (Y2 = Y1)) | (Y0 @ Y1 @ Y2)))))))))) & (mweakly_dense = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (~ (Y0 @ Y3 @ Y1))))))))))))) & (mfunctional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y1 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y1 @ Y3)) | (Y2 = Y3))))))))))))) & (mpartially_functional = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y2 = Y1)))))))))) & (meuclidean = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y3 @ Y1))) | (Y0 @ Y2 @ Y1)))))))))) & (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1)))))))))) & (mserial = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2))))))))) & (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (~ (Y1 @ Y3)))))))))))) & (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) & (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))))))))) & (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1))))))) & (mforall_ind = (^[Y0 : mu > $i > $o]: ((^[Y1 : $i]: (!! @ mu @ (^[Y2 : mu]: (Y0 @ Y2 @ Y1))))))) & (mxor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))))) & (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2))))))))))) & (mimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2)))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (meq_prop = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) = (Y1 @ Y2)))))))) & ! [X0 : d_mu,X1 : d_mu] : ((X0 = X1) | (((d2mu @ X0)) != ((d2mu @ X1)))) & ! [X2 : d_mu] : (d_mu_0 = X2) & ! [X3 : mu] : (((d2mu @ (sK0 @ X3))) = X3) & ! [X5 : d_unsorted,X6 : d_unsorted] : ((X5 = X6) | (((d2unsorted @ X5)) != ((d2unsorted @ X6)))) & ! [X7 : d_unsorted] : (d_unsorted_0 = X7) & ! [X8 : $i] : (((d2unsorted @ (sK1 @ X8))) = X8)),
% 0.20/0.26 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X9,sK1 @ X8),skolemize(X9,sK1 @ X8)],[f10])).
% 0.20/0.26 thf(f21,plain,(
% 0.20/0.26 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ (Y0 @ Y2)) | (~ (Y1 @ Y2))))))))))),
% 0.20/0.26 inference(cnf_transformation,[],[f11])).
% 0.20/0.26 thf(f22,plain,(
% 0.20/0.26 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2))))))))),
% 0.20/0.26 inference(cnf_transformation,[],[f11])).
% 0.20/0.26 thf(f24,plain,(
% 0.20/0.26 (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))))))),
% 0.20/0.26 inference(cnf_transformation,[],[f11])).
% 0.20/0.26 thf(f49,plain,(
% 0.20/0.26 (mequiv != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ (mimplies @ Y0 @ Y1) @ (mimplies @ Y1 @ Y0))))))),
% 0.20/0.26 inference(cnf_transformation,[],[f9])).
% 0.20/0.26 thf(f52,plain,(
% 0.20/0.26 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ 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]: ((~ (Y2 @ Y4)) | (Y3 @ Y4))))))) @ Y0 @ Y1) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((~ (Y2 @ Y4)) | (Y3 @ Y4))))))) @ Y1 @ Y0))))))),
% 0.20/0.26 inference(definition_unfolding,[],[f49,f24,f21,f22,f22])).
% 0.20/0.26 thf(f53,plain,(
% 0.20/0.26 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ ((~ ((~ (Y0 @ Y2)) | (Y1 @ Y2))) | (~ ((~ (Y1 @ Y2)) | (Y0 @ Y2)))))))))))),
% 0.20/0.26 inference(beta-eta_normalization,[],[f52])).
% 0.20/0.26 thf(f54,plain,(
% 0.20/0.26 $false),
% 0.20/0.26 inference(trivial_inequality_removal,[],[f53])).
% 0.20/0.26 % SZS output end Proof for theBenchmark
% 0.20/0.26 % (275234)------------------------------
% 0.20/0.26 % (275234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.26 % (275234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.26 % (275234)CaDiCaL version: 2.1.3
% 0.20/0.26 % (275234)Termination reason: Refutation
% 0.20/0.26 % (275234)Time elapsed: 0.005 s
% 0.20/0.26 % (275234)Peak memory usage: 11 MB
% 0.20/0.26 % (275234)Instructions burned: 21 (million)
% 0.20/0.26 % (275225)Success in time 0.036 s
% 0.20/0.26 % Vampire exiting
%------------------------------------------------------------------------------