%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX174^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 : n006.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.21s 0.30s
% Output : Refutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX174^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.08/0.18 % Computer : n006.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:09:25 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.30 % (920880)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.30 % (920887)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1874196021:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.30 % (920887)Instruction limit reached!
% 0.21/0.30 % (920887)------------------------------
% 0.21/0.30 % (920887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (920887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (920887)CaDiCaL version: 2.1.3
% 0.21/0.30 % (920887)Termination reason: Instruction limit
% 0.21/0.30 % (920887)Termination phase: Preprocessing 3
% 0.21/0.30 % (920887)Time elapsed: 0.001 s
% 0.21/0.30 % (920887)Peak memory usage: 10 MB
% 0.21/0.30 % (920887)Instructions burned: 3 (million)
% 0.21/0.30 % (920891)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.30 % (920891)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.21/0.30 % (920885)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3280539776:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.30 % (920888)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=27152847:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.21/0.30 % (920886)lrs+10_16_si=on:nwc=1.5:random_seed=449875510:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.30 % (920889)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3185952509:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.30 % (920890)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2442154628:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.30 % (920891)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=3201323785:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.30 % (920893)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2003557989:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.30 % (920893)Instruction limit reached!
% 0.21/0.30 % (920893)------------------------------
% 0.21/0.30 % (920893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (920893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (920893)CaDiCaL version: 2.1.3
% 0.21/0.30 % (920893)Termination reason: Instruction limit
% 0.21/0.30 % (920893)Termination phase: Property scanning
% 0.21/0.30 % (920893)Time elapsed: 0.001 s
% 0.21/0.30 % (920893)Peak memory usage: 10 MB
% 0.21/0.30 % (920893)Instructions burned: 4 (million)
% 0.21/0.30 % (920891) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-920880-920891"...
% 0.21/0.30 % (920886)Instruction limit reached!
% 0.21/0.30 % (920886)------------------------------
% 0.21/0.30 % (920886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (920886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (920886)CaDiCaL version: 2.1.3
% 0.21/0.30 % (920886)Termination reason: Instruction limit
% 0.21/0.30 % (920886)Termination phase: Saturation
% 0.21/0.30 % (920886)Time elapsed: 0.010 s
% 0.21/0.30 % (920886)Peak memory usage: 12 MB
% 0.21/0.30 % (920886)Instructions burned: 19 (million)
% 0.21/0.30 % (920885) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-920880-920885"...
% 0.21/0.30 % (920890) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-920880-920890"...
% 0.21/0.30 % (920889)Instruction limit reached!
% 0.21/0.30 % (920889)------------------------------
% 0.21/0.30 % (920889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (920889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (920889)CaDiCaL version: 2.1.3
% 0.21/0.30 % (920889)Termination reason: Instruction limit
% 0.21/0.30 % (920889)Termination phase: Saturation
% 0.21/0.30 % (920889)Time elapsed: 0.014 s
% 0.21/0.30 % (920889)Peak memory usage: 12 MB
% 0.21/0.30 % (920889)Instructions burned: 25 (million)
% 0.21/0.30 % (920901)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1348894117:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.21/0.30 % (920891)...printing done.
% 0.21/0.30 % (920885)...printing done.
% 0.21/0.30 % (920901)Instruction limit reached!
% 0.21/0.30 % (920901)------------------------------
% 0.21/0.30 % (920901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (920901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (920901)CaDiCaL version: 2.1.3
% 0.21/0.30 % (920901)Termination reason: Instruction limit
% 0.21/0.30 % (920901)Termination phase: Saturation
% 0.21/0.30 % (920901)Time elapsed: 0.002 s
% 0.21/0.30 % (920901)Peak memory usage: 12 MB
% 0.21/0.30 % (920901)Instructions burned: 7 (million)
% 0.21/0.30 % (920891)Refutation found. Thanks to Tanya!
% 0.21/0.30 % SZS status Theorem for theBenchmark
% 0.21/0.30 % SZS output start Proof for theBenchmark
% 0.21/0.30 thf(type_def_5, type, unsorted: $tType).
% 0.21/0.30 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.21/0.30 thf(type_def_7, type, d_unsorted: $tType).
% 0.21/0.30 thf(func_def_0, type, irel: ($i > $i > $o)).
% 0.21/0.30 thf(func_def_1, type, mnot: (($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_2, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_3, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_4, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_5, type, mbox_s4: (($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_6, type, iatom: (($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_7, type, inot: (($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_8, type, itrue: ($i > $o)).
% 0.21/0.30 thf(func_def_9, type, ifalse: ($i > $o)).
% 0.21/0.30 thf(func_def_10, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_11, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_12, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_13, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_14, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_15, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.30 thf(func_def_16, type, ivalid: (($i > $o) > $o)).
% 0.21/0.30 thf(func_def_17, type, isatisfiable: (($i > $o) > $o)).
% 0.21/0.30 thf(func_def_18, type, icountersatisfiable: (($i > $o) > $o)).
% 0.21/0.30 thf(func_def_19, type, iinvalid: (($i > $o) > $o)).
% 0.21/0.30 thf(func_def_20, type, d2unsorted: (d_unsorted > $i)).
% 0.21/0.30 thf(func_def_21, type, d_unsorted_0: d_unsorted).
% 0.21/0.30 thf(func_def_23, type, db1: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_24, type, db0: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_25, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.21/0.30 thf(func_def_28, type, vAND: ($o > $o > $o)).
% 0.21/0.30 thf(func_def_29, type, db2: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_30, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.21/0.30 thf(func_def_31, type, vOR: ($o > $o > $o)).
% 0.21/0.30 thf(func_def_32, type, vNOT: ($o > $o)).
% 0.21/0.30 thf(func_def_33, type, db3: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_34, type, db5: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_35, type, db6: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_36, type, db4: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_37, type, sK0: ($i > d_unsorted)).
% 0.21/0.30 thf(func_def_38, type, sK1: ($i > $o)).
% 0.21/0.30 thf(func_def_39, type, sK2: ($i > $o)).
% 0.21/0.30 thf(f1,axiom,(
% 0.21/0.30 ((^[X14 : ($i > $o)] : (~ ! [X15 : $i] : (X14 @ X15))) = icountersatisfiable) & (mand = (^[X4 : ($i > $o), X5 : ($i > $o), X0 : $i] : ((X5 @ X0) & (X4 @ X0)))) & ~(ifalse @ (d2unsorted @ d_unsorted_0)) & ! [X1 : d_unsorted] : (X1 = d_unsorted_0) & ((^[X0 : ($i > $o), X6 : ($i > $o), X7 : $i] : ((X6 @ X7) | ~(X0 @ X7))) = mimplies) & ! [X0 : $i] : ? [X1 : d_unsorted] : (X0 = ((d2unsorted @ X1))) & ! [X3 : d_unsorted,X2 : d_unsorted] : ((((d2unsorted @ X2)) = ((d2unsorted @ X3))) => (X2 = X3)) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5)) | ! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)))) = ior) & (ixor = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (~ ! [X11 : $i,X10 : $i,X5 : $i] : (~(irel @ X7 @ X5) | ((~(irel @ X5 @ X10) | (X9 @ X10) | ~ ! [X12 : $i] : ((X8 @ X12) | ~(irel @ X5 @ X12))) & (~ ! [X13 : $i] : (~(irel @ X5 @ X13) | (X9 @ X13)) | (X8 @ X11) | ~(irel @ X5 @ X11))))))) & (mor = (^[X4 : ($i > $o), X5 : ($i > $o), X0 : $i] : ((X4 @ X0) | (X5 @ X0)))) & ((^[X8 : ($i > $o), X7 : $i] : ((X8 @ X7))) = iatom) & ((^[X4 : ($i > $o), X0 : $i] : (~(X4 @ X0))) = mnot) & (inot = (^[X8 : ($i > $o), X7 : $i] : (~ ! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5))))) & (iinvalid = (^[X14 : ($i > $o)] : (! [X15 : $i] : ~(X14 @ X15)))) & (isatisfiable = (^[X14 : ($i > $o)] : (~ ! [X15 : $i] : ~(X14 @ X15)))) & (iimplies = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : (~(irel @ X7 @ X5) | (X9 @ X5)) | ~ ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5))))) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5)) | ~ ! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)))) = iimplied) & (ivalid = (^[X14 : ($i > $o)] : (! [X15 : $i] : (X14 @ X15)))) & (itrue @ (d2unsorted @ d_unsorted_0)) & (iequiv = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : ((! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ~ ! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5))) & (! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)) | ~ ! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)))))) & ((^[X8 : ($i > $o), X4 : $i] : (! [X5 : $i] : ((X8 @ X5) | ~(irel @ X4 @ X5)))) = mbox_s4) & (iand = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : ((X9 @ X7) & (X8 @ X7)))) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lcl695_1)).
% 0.21/0.30 thf(f2,conjecture,(
% 0.21/0.30 ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((mimplies @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))) = iimplies)),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iimplies)).
% 0.21/0.30 thf(f3,negated_conjecture,(
% 0.21/0.30 ~ ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((mimplies @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))) = iimplies)),
% 0.21/0.30 inference(negated_conjecture,[status(cth)],[f2])).
% 0.21/0.30 thf(f4,plain,(
% 0.21/0.30 ~ (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 0.21/0.30 inference(fool_elimination,[],[f3])).
% 0.21/0.30 thf(f5,plain,(
% 0.21/0.30 ((^[X0 : ($i > $o)] : (~ ! [X1 : $i] : (X0 @ X1))) = icountersatisfiable) & (mand = (^[X2 : ($i > $o), X3 : ($i > $o), X4 : $i] : ((X3 @ X4) & (X2 @ X4)))) & ~(ifalse @ (d2unsorted @ d_unsorted_0)) & ! [X5 : d_unsorted] : (d_unsorted_0 = X5) & ((^[X6 : ($i > $o), X7 : ($i > $o), X8 : $i] : ((X7 @ X8) | ~(X6 @ X8))) = mimplies) & ! [X9 : $i] : ? [X10 : d_unsorted] : (((d2unsorted @ X10)) = X9) & ! [X11 : d_unsorted,X12 : d_unsorted] : ((((d2unsorted @ X11)) = ((d2unsorted @ X12))) => (X11 = X12)) & ((^[X13 : ($i > $o), X14 : ($i > $o), X15 : $i] : (! [X16 : $i] : (~(irel @ X15 @ X16) | (X13 @ X16)) | ! [X17 : $i] : ((X14 @ X17) | ~(irel @ X15 @ X17)))) = ior) & (ixor = (^[X18 : ($i > $o), X19 : ($i > $o), X20 : $i] : (~ ! [X21 : $i,X22 : $i,X23 : $i] : (~(irel @ X20 @ X23) | ((~(irel @ X23 @ X22) | (X19 @ X22) | ~ ! [X24 : $i] : ((X18 @ X24) | ~(irel @ X23 @ X24))) & (~ ! [X25 : $i] : (~(irel @ X23 @ X25) | (X19 @ X25)) | (X18 @ X21) | ~(irel @ X23 @ X21))))))) & (mor = (^[X26 : ($i > $o), X27 : ($i > $o), X28 : $i] : ((X26 @ X28) | (X27 @ X28)))) & ((^[X29 : ($i > $o), X30 : $i] : ((X29 @ X30))) = iatom) & ((^[X31 : ($i > $o), X32 : $i] : (~(X31 @ X32))) = mnot) & (inot = (^[X33 : ($i > $o), X34 : $i] : (~ ! [X35 : $i] : (~(irel @ X34 @ X35) | (X33 @ X35))))) & (iinvalid = (^[X36 : ($i > $o)] : (! [X37 : $i] : ~(X36 @ X37)))) & (isatisfiable = (^[X38 : ($i > $o)] : (~ ! [X39 : $i] : ~(X38 @ X39)))) & (iimplies = (^[X40 : ($i > $o), X41 : ($i > $o), X42 : $i] : (! [X43 : $i] : (~(irel @ X42 @ X43) | (X41 @ X43)) | ~ ! [X44 : $i] : ((X40 @ X44) | ~(irel @ X42 @ X44))))) & ((^[X45 : ($i > $o), X46 : ($i > $o), X47 : $i] : (! [X48 : $i] : (~(irel @ X47 @ X48) | (X45 @ X48)) | ~ ! [X49 : $i] : ((X46 @ X49) | ~(irel @ X47 @ X49)))) = iimplied) & (ivalid = (^[X50 : ($i > $o)] : (! [X51 : $i] : (X50 @ X51)))) & (itrue @ (d2unsorted @ d_unsorted_0)) & (iequiv = (^[X52 : ($i > $o), X53 : ($i > $o), X54 : $i] : ((! [X55 : $i] : ((X53 @ X55) | ~(irel @ X54 @ X55)) | ~ ! [X56 : $i] : (~(irel @ X54 @ X56) | (X52 @ X56))) & (! [X57 : $i] : ((X52 @ X57) | ~(irel @ X54 @ X57)) | ~ ! [X58 : $i] : ((X53 @ X58) | ~(irel @ X54 @ X58)))))) & ((^[X59 : ($i > $o), X60 : $i] : (! [X61 : $i] : ((X59 @ X61) | ~(irel @ X60 @ X61)))) = mbox_s4) & (iand = (^[X62 : ($i > $o), X63 : ($i > $o), X64 : $i] : ((X63 @ X64) & (X62 @ X64)))) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))),
% 0.21/0.30 inference(rectify,[],[f1])).
% 0.21/0.30 thf(f6,plain,(
% 0.21/0.30 (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & ~ (((ifalse @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X5 : d_unsorted] : (d_unsorted_0 = X5) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & ! [X9 : $i] : ? [X10 : d_unsorted] : (((d2unsorted @ X10)) = X9) & ! [X11 : d_unsorted,X12 : d_unsorted] : ((((d2unsorted @ X11)) = ((d2unsorted @ X12))) => (X11 = X12)) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y3 @ Y6)) | (Y0 @ Y6))))) | (Y1 @ Y4)) | (~ (irel @ Y3 @ Y4)))) | (~ (irel @ Y2 @ Y3)))))))))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true)),
% 0.21/0.30 inference(fool_elimination,[],[f5])).
% 0.21/0.30 thf(f7,plain,(
% 0.21/0.30 (iimplies != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 0.21/0.30 inference(flattening,[],[f4])).
% 0.21/0.30 thf(f8,plain,(
% 0.21/0.30 (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & ~ (((ifalse @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & ! [X1 : $i] : ? [X2 : d_unsorted] : (((d2unsorted @ X2)) = X1) & ! [X3 : d_unsorted,X4 : d_unsorted] : ((((d2unsorted @ X3)) = ((d2unsorted @ X4))) => (X3 = X4)) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y3 @ Y6)) | (Y0 @ Y6))))) | (Y1 @ Y4)) | (~ (irel @ Y3 @ Y4)))) | (~ (irel @ Y2 @ Y3)))))))))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true)),
% 0.21/0.30 inference(rectify,[],[f6])).
% 0.21/0.30 thf(f9,plain,(
% 0.21/0.30 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & ! [X3 : d_unsorted,X4 : d_unsorted] : ((((d2unsorted @ X3)) = ((d2unsorted @ X4))) => (X3 = X4)) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y3 @ Y6)) | (Y0 @ Y6))))) | (Y1 @ Y4)) | (~ (irel @ Y3 @ Y4)))) | (~ (irel @ Y2 @ Y3)))))))))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & ! [X1 : $i] : ? [X2 : d_unsorted] : (((d2unsorted @ X2)) = X1) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0)),
% 0.21/0.30 inference(flattening,[],[f8])).
% 0.21/0.30 thf(f10,plain,(
% 0.21/0.30 (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (mor = (^[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)))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ! [X1 : $i] : ? [X2 : d_unsorted] : (((d2unsorted @ X2)) = X1) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y3 @ Y6)) | (Y0 @ Y6))))) | (Y1 @ Y4)) | (~ (irel @ Y3 @ Y4)))) | (~ (irel @ Y2 @ Y3)))))))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X3 : d_unsorted,X4 : d_unsorted] : ((X3 = X4) | (((d2unsorted @ X3)) != ((d2unsorted @ X4)))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0)),
% 0.21/0.30 inference(ennf_transformation,[],[f9])).
% 0.21/0.30 thf(f11,plain,(
% 0.21/0.30 (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (mor = (^[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)))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ! [X0 : $i] : ? [X1 : d_unsorted] : (((d2unsorted @ X1)) = X0) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y3 @ Y6)) | (Y0 @ Y6))))) | (Y1 @ Y4)) | (~ (irel @ Y3 @ Y4)))) | (~ (irel @ Y2 @ Y3)))))))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((X2 = X3) | (((d2unsorted @ X2)) != ((d2unsorted @ X3)))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4)),
% 0.21/0.30 inference(rectify,[],[f10])).
% 0.21/0.30 thf(f12,plain,(
% 0.21/0.30 (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (mor = (^[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)))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ! [X0 : $i] : (((d2unsorted @ (sK0 @ X0))) = X0) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y3 @ Y6)) | (Y0 @ Y6))))) | (Y1 @ Y4)) | (~ (irel @ Y3 @ Y4)))) | (~ (irel @ Y2 @ Y3)))))))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((X2 = X3) | (((d2unsorted @ X2)) != ((d2unsorted @ X3)))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4)),
% 0.21/0.30 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X1,sK0 @ X0)],[f11])).
% 0.21/0.30 thf(f13,plain,(
% 0.21/0.30 (iimplies != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 0.21/0.30 inference(cnf_transformation,[],[f7])).
% 0.21/0.30 thf(f14,plain,(
% 0.21/0.30 ( ! [X4 : d_unsorted] : ((d_unsorted_0 = X4)) )),
% 0.21/0.30 inference(cnf_transformation,[],[f12])).
% 0.21/0.30 thf(f15,plain,(
% 0.21/0.30 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))))),
% 0.21/0.30 inference(cnf_transformation,[],[f12])).
% 0.21/0.30 thf(f24,plain,(
% 0.21/0.30 ( ! [X0 : $i] : ((((d2unsorted @ (sK0 @ X0))) = X0)) )),
% 0.21/0.30 inference(cnf_transformation,[],[f12])).
% 0.21/0.30 thf(f28,plain,(
% 0.21/0.30 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2))))))))),
% 0.21/0.30 inference(cnf_transformation,[],[f12])).
% 0.21/0.30 thf(f33,plain,(
% 0.21/0.30 (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true)),
% 0.21/0.30 inference(cnf_transformation,[],[f12])).
% 0.21/0.30 thf(f35,plain,(
% 0.21/0.30 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2))))))))),
% 0.21/0.30 inference(cnf_transformation,[],[f12])).
% 0.21/0.30 thf(f39,plain,(
% 0.21/0.30 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((~ (Y2 @ Y4)) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y2 @ Y4))))))) @ Y1))))))),
% 0.21/0.30 inference(definition_unfolding,[],[f13,f15,f28,f35,f35])).
% 0.21/0.30 thf(f40,plain,(
% 0.21/0.30 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))),
% 0.21/0.30 inference(beta-eta_normalization,[],[f39])).
% 0.21/0.30 thf(f51,plain,(
% 0.21/0.30 ( ! [X0 : $i] : ((((d2unsorted @ d_unsorted_0)) = X0)) )),
% 0.21/0.30 inference(forward_demodulation,[],[f24,f14])).
% 0.21/0.30 thf(f55,plain,(
% 0.21/0.30 ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) )),
% 0.21/0.30 inference(constrained_superposition,[],[f51,f51])).
% 0.21/0.30 thf(f81,plain,(
% 0.21/0.30 ( ! [X0 : $i] : (($true = ((irel @ X0 @ X0)))) )),
% 0.21/0.30 inference(constrained_superposition,[],[f33,f51])).
% 0.21/0.30 thf(f84,plain,(
% 0.21/0.30 ((((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) @ sK1)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))) @ sK1)))),
% 0.21/0.30 inference(negative_extensionality,[],[f40])).
% 0.21/0.30 thf(f85,plain,(
% 0.21/0.30 ((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i]: ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))))),
% 0.21/0.30 inference(beta-eta_normalization,[],[f84])).
% 0.21/0.30 thf(f86,plain,(
% 0.21/0.30 ((((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) @ sK2)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))))))) @ sK2)))),
% 0.21/0.30 inference(negative_extensionality,[],[f85])).
% 0.21/0.30 thf(f87,plain,(
% 0.21/0.30 ((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) != (^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))))))),
% 0.21/0.30 inference(beta-eta_normalization,[],[f86])).
% 0.21/0.30 thf(f88,plain,(
% 0.21/0.30 ((((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))))) @ sK3)) != (((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) @ sK3)))),
% 0.21/0.30 inference(negative_extensionality,[],[f87])).
% 0.21/0.30 thf(f89,plain,(
% 0.21/0.30 ((((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) @ sK3)) = $true) | ((((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))))) @ sK3)) = $true)),
% 0.21/0.30 inference(xor_proxy_clausification,[],[f88])).
% 0.21/0.30 thf(f90,plain,(
% 0.21/0.30 ((((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) @ sK3)) = $false) | ((((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))))) @ sK3)) = $false)),
% 0.21/0.30 inference(xor_proxy_clausification,[],[f88])).
% 0.21/0.30 thf(f91,plain,(
% 0.21/0.30 ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0))))))) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))))) = $false)),
% 0.21/0.30 inference(beta-eta_normalization,[],[f90])).
% 0.21/0.30 thf(f92,plain,(
% 0.21/0.30 ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0))))) = $false)),
% 0.21/0.30 inference(or_proxy_clausification,[],[f91])).
% 0.21/0.30 thf(f93,plain,(
% 0.21/0.30 (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) = $false) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))))) = $false)),
% 0.21/0.30 inference(or_proxy_clausification,[],[f91])).
% 0.21/0.30 thf(f94,plain,(
% 0.21/0.30 ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))))) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))))),
% 0.21/0.30 inference(not_proxy_clausification,[],[f93])).
% 0.21/0.30 thf(f96,plain,(
% 0.21/0.30 ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) | (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) = $false)),
% 0.21/0.30 inference(or_proxy_clausification,[],[f94])).
% 0.21/0.30 thf(f97,plain,(
% 0.21/0.30 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ X1)) = $true) | (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) = $false)) )),
% 0.21/0.30 inference(pi_proxy_clausification,[],[f96])).
% 0.21/0.30 thf(f98,plain,(
% 0.21/0.30 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ X1)) = $true) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))))) )),
% 0.21/0.30 inference(not_proxy_clausification,[],[f97])).
% 0.21/0.30 thf(f99,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ X2)) = $true) | ((((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ X1)) = $true)) )),
% 0.21/0.30 inference(pi_proxy_clausification,[],[f98])).
% 0.21/0.30 thf(f100,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (((((~ (irel @ sK3 @ X2)) | (sK1 @ X2))) = $true) | ($true = (((~ (irel @ sK3 @ X1)) | (sK1 @ X1))))) )),
% 0.21/0.30 inference(beta-eta_normalization,[],[f99])).
% 0.21/0.30 thf(f101,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (($true = (((~ (irel @ sK3 @ X1)) | (sK1 @ X1)))) | ($true = ((sK1 @ X2))) | ($true = ((~ (irel @ sK3 @ X2))))) )),
% 0.21/0.30 inference(or_proxy_clausification,[],[f100])).
% 0.21/0.30 thf(f102,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (($true = ((~ (irel @ sK3 @ X2)))) | ($true = ((~ (irel @ sK3 @ X1)))) | ($true = ((sK1 @ X2))) | ($true = ((sK1 @ X1)))) )),
% 0.21/0.30 inference(or_proxy_clausification,[],[f101])).
% 0.21/0.30 thf(f103,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (($true = ((sK1 @ X1))) | ($true = ((~ (irel @ sK3 @ X1)))) | (((irel @ sK3 @ X2)) = $false) | ($true = ((sK1 @ X2)))) )),
% 0.21/0.30 inference(not_proxy_clausification,[],[f102])).
% 0.21/0.30 thf(f104,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ sK3 @ X1))) | ($true = ((sK1 @ X2))) | ($true = ((sK1 @ X1)))) )),
% 0.21/0.30 inference(not_proxy_clausification,[],[f103])).
% 0.21/0.30 thf(f115,plain,(
% 0.21/0.30 (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0))))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $false)),
% 0.21/0.30 inference(or_proxy_clausification,[],[f92])).
% 0.21/0.30 thf(f128,plain,(
% 0.21/0.30 (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $false) | ((((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0))) @ sK6)) = $false)),
% 0.21/0.30 inference(sigma_proxy_clausification,[],[f115])).
% 0.21/0.30 thf(f129,plain,(
% 0.21/0.30 ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ sK7)) = $false) | ((((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0))) @ sK6)) = $false)),
% 0.21/0.30 inference(sigma_proxy_clausification,[],[f128])).
% 0.21/0.30 thf(f130,plain,(
% 0.21/0.30 ($false = (((~ (irel @ sK3 @ sK6)) | (sK2 @ sK6)))) | ($false = (((sK2 @ sK7) | (~ (irel @ sK3 @ sK7)))))),
% 0.21/0.30 inference(beta-eta_normalization,[],[f129])).
% 0.21/0.30 thf(f131,plain,(
% 0.21/0.30 (((sK2 @ sK6)) = $false) | ($false = (((sK2 @ sK7) | (~ (irel @ sK3 @ sK7)))))),
% 0.21/0.30 inference(or_proxy_clausification,[],[f130])).
% 0.21/0.30 thf(f139,plain,(
% 0.21/0.30 (((sK2 @ sK6)) = $false) | (((sK2 @ sK7)) = $false)),
% 0.21/0.30 inference(or_proxy_clausification,[],[f131])).
% 0.21/0.30 thf(f141,plain,(
% 0.21/0.30 ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0)))))))),
% 0.21/0.30 inference(beta-eta_normalization,[],[f89])).
% 0.21/0.30 thf(f142,plain,(
% 0.21/0.30 ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0))))))) | (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) = $true) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))))),
% 0.21/0.30 inference(or_proxy_clausification,[],[f141])).
% 0.21/0.30 thf(f143,plain,(
% 0.21/0.30 (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) = $true) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0)))))) | (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) = $true)),
% 0.21/0.30 inference(or_proxy_clausification,[],[f142])).
% 0.21/0.30 thf(f144,plain,(
% 0.21/0.30 ($true = ((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0)))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))))),
% 0.21/0.30 inference(not_proxy_clausification,[],[f143])).
% 0.21/0.30 thf(f145,plain,(
% 0.21/0.30 ( ! [X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0)))))) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X1)) = $true)) )),
% 0.21/0.30 inference(pi_proxy_clausification,[],[f144])).
% 0.21/0.30 thf(f146,plain,(
% 0.21/0.30 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ sK8))) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X1)) = $true) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ sK8))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0))))))) )),
% 0.21/0.30 inference(sigma_proxy_clausification,[],[f145])).
% 0.21/0.30 thf(f147,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X1)) = $true) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ sK8))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ sK8)))) )),
% 0.21/0.30 inference(pi_proxy_clausification,[],[f146])).
% 0.21/0.30 thf(f148,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK2 @ Y0))) @ X2))) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X1)) = $true) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ sK8)))) )),
% 0.21/0.30 inference(duplicate_literal_removal,[],[f147])).
% 0.21/0.30 thf(f149,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (($true = (((~ (irel @ sK3 @ X2)) | (sK2 @ X2)))) | ($true = (((sK2 @ X1) | (~ (irel @ sK3 @ X1))))) | ((((~ (irel @ sK3 @ sK8)) | (sK1 @ sK8))) = $false)) )),
% 0.21/0.30 inference(beta-eta_normalization,[],[f148])).
% 0.21/0.30 thf(f150,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (((((~ (irel @ sK3 @ sK8)) | (sK1 @ sK8))) = $false) | ($true = ((~ (irel @ sK3 @ X2)))) | ($true = (((sK2 @ X1) | (~ (irel @ sK3 @ X1))))) | ($true = ((sK2 @ X2)))) )),
% 0.21/0.30 inference(or_proxy_clausification,[],[f149])).
% 0.21/0.30 thf(f151,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (($true = (((sK2 @ X1) | (~ (irel @ sK3 @ X1))))) | ($true = ((~ (irel @ sK3 @ X2)))) | (((sK1 @ sK8)) = $false) | ($true = ((sK2 @ X2)))) )),
% 0.21/0.30 inference(or_proxy_clausification,[],[f150])).
% 0.21/0.30 thf(f152,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (($true = ((sK2 @ X2))) | ($true = ((~ (irel @ sK3 @ X2)))) | ($true = (((sK2 @ X1) | (~ (irel @ sK3 @ X1))))) | (((~ (irel @ sK3 @ sK8))) = $false)) )),
% 0.21/0.30 inference(or_proxy_clausification,[],[f150])).
% 0.21/0.30 thf(f153,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK3 @ X2)) = $false) | ($true = (((sK2 @ X1) | (~ (irel @ sK3 @ X1))))) | (((~ (irel @ sK3 @ sK8))) = $false) | ($true = ((sK2 @ X2)))) )),
% 0.21/0.30 inference(not_proxy_clausification,[],[f152])).
% 0.21/0.30 thf(f154,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (($true = ((sK2 @ X2))) | (((irel @ sK3 @ X2)) = $false) | ($true = ((~ (irel @ sK3 @ X1)))) | ($true = ((sK2 @ X1))) | (((~ (irel @ sK3 @ sK8))) = $false)) )),
% 0.21/0.30 inference(or_proxy_clausification,[],[f153])).
% 0.21/0.30 thf(f155,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK3 @ X2)) = $false) | (((~ (irel @ sK3 @ sK8))) = $false) | ($true = ((sK2 @ X2))) | ($true = ((sK2 @ X1))) | ($false = ((irel @ sK3 @ X1)))) )),
% 0.21/0.30 inference(not_proxy_clausification,[],[f154])).
% 0.21/0.30 thf(f156,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ sK3 @ sK8)) = $true) | ($true = ((sK2 @ X2))) | (((irel @ sK3 @ X2)) = $false) | ($true = ((sK2 @ X1)))) )),
% 0.21/0.30 inference(not_proxy_clausification,[],[f155])).
% 0.21/0.30 thf(f157,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (($true = ((~ (irel @ sK3 @ X2)))) | (((sK1 @ sK8)) = $false) | ($true = ((sK2 @ X1))) | ($true = ((~ (irel @ sK3 @ X1)))) | ($true = ((sK2 @ X2)))) )),
% 0.21/0.30 inference(or_proxy_clausification,[],[f151])).
% 0.21/0.30 thf(f158,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : (($true = ((~ (irel @ sK3 @ X1)))) | ($true = ((sK2 @ X2))) | ($true = ((sK2 @ X1))) | (((sK1 @ sK8)) = $false) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.21/0.30 inference(not_proxy_clausification,[],[f157])).
% 0.21/0.30 thf(f159,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ sK3 @ X1))) | ($true = ((sK2 @ X1))) | ($true = ((sK2 @ X2))) | (((sK1 @ sK8)) = $false)) )),
% 0.21/0.30 inference(not_proxy_clausification,[],[f158])).
% 0.21/0.30 thf(f161,definition,(
% 0.21/0.30 spl9_1 <=> ! [X1 : $i] : (($false = ((irel @ sK3 @ X1))) | ($true = ((sK1 @ X1))))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition])).
% 0.21/0.30 thf(f162,plain,(
% 0.21/0.30 ( ! [X1 : $i] : (($false = ((irel @ sK3 @ X1))) | ($true = ((sK1 @ X1)))) ) | ~spl9_1),
% 0.21/0.30 inference(avatar_component_clause,[],[f161])).
% 0.21/0.30 thf(f163,plain,(
% 0.21/0.30 spl9_1 | spl9_1),
% 0.21/0.30 inference(avatar_split_clause,[],[f104,f161,f161])).
% 0.21/0.30 thf(f185,definition,(
% 0.21/0.30 spl9_6 <=> (((sK2 @ sK7)) = $false)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl9_6])],[avatar_definition])).
% 0.21/0.30 thf(f187,plain,(
% 0.21/0.30 (((sK2 @ sK7)) = $false) | ~spl9_6),
% 0.21/0.30 inference(avatar_component_clause,[],[f185])).
% 0.21/0.30 thf(f199,definition,(
% 0.21/0.30 spl9_9 <=> (((sK2 @ sK6)) = $false)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl9_9])],[avatar_definition])).
% 0.21/0.30 thf(f201,plain,(
% 0.21/0.30 (((sK2 @ sK6)) = $false) | ~spl9_9),
% 0.21/0.30 inference(avatar_component_clause,[],[f199])).
% 0.21/0.30 thf(f202,plain,(
% 0.21/0.30 spl9_6 | spl9_9),
% 0.21/0.30 inference(avatar_split_clause,[],[f139,f199,f185])).
% 0.21/0.30 thf(f205,definition,(
% 0.21/0.30 spl9_10 <=> (((irel @ sK3 @ sK8)) = $true)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl9_10])],[avatar_definition])).
% 0.21/0.30 thf(f207,plain,(
% 0.21/0.30 (((irel @ sK3 @ sK8)) = $true) | ~spl9_10),
% 0.21/0.30 inference(avatar_component_clause,[],[f205])).
% 0.21/0.30 thf(f209,definition,(
% 0.21/0.30 spl9_11 <=> ! [X2 : $i] : (($true = ((sK2 @ X2))) | (((irel @ sK3 @ X2)) = $false))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl9_11])],[avatar_definition])).
% 0.21/0.30 thf(f210,plain,(
% 0.21/0.30 ( ! [X2 : $i] : ((((irel @ sK3 @ X2)) = $false) | ($true = ((sK2 @ X2)))) ) | ~spl9_11),
% 0.21/0.30 inference(avatar_component_clause,[],[f209])).
% 0.21/0.30 thf(f211,plain,(
% 0.21/0.30 spl9_10 | spl9_11 | spl9_11),
% 0.21/0.30 inference(avatar_split_clause,[],[f156,f209,f209,f205])).
% 0.21/0.30 thf(f213,definition,(
% 0.21/0.30 spl9_12 <=> (((sK1 @ sK8)) = $false)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl9_12])],[avatar_definition])).
% 0.21/0.30 thf(f215,plain,(
% 0.21/0.30 (((sK1 @ sK8)) = $false) | ~spl9_12),
% 0.21/0.30 inference(avatar_component_clause,[],[f213])).
% 0.21/0.30 thf(f216,plain,(
% 0.21/0.30 spl9_12 | spl9_11 | spl9_11),
% 0.21/0.30 inference(avatar_split_clause,[],[f159,f209,f209,f213])).
% 0.21/0.30 thf(f219,plain,(
% 0.21/0.30 ($true = $false) | (((sK2 @ sK3)) = $true) | ~spl9_11),
% 0.21/0.30 inference(constrained_superposition,[],[f210,f81])).
% 0.21/0.30 thf(f223,plain,(
% 0.21/0.30 (((sK2 @ sK3)) = $true) | ~spl9_11),
% 0.21/0.30 inference(trivial_inequality_removal,[],[f219])).
% 0.21/0.30 thf(f225,plain,(
% 0.21/0.30 ( ! [X0 : $i] : (($true = ((sK2 @ X0)))) ) | ~spl9_11),
% 0.21/0.30 inference(constrained_superposition,[],[f223,f55])).
% 0.21/0.30 thf(f227,plain,(
% 0.21/0.30 ($true = $false) | (~spl9_6 | ~spl9_11)),
% 0.21/0.30 inference(forward_demodulation,[],[f187,f225])).
% 0.21/0.30 thf(f228,plain,(
% 0.21/0.30 $false | (~spl9_6 | ~spl9_11)),
% 0.21/0.30 inference(trivial_inequality_removal,[],[f227])).
% 0.21/0.30 thf(f229,plain,(
% 0.21/0.30 ~spl9_6 | ~spl9_11),
% 0.21/0.30 inference(avatar_contradiction_clause,[],[f228])).
% 0.21/0.30 thf(f231,plain,(
% 0.21/0.30 ($true = $false) | (~spl9_9 | ~spl9_11)),
% 0.21/0.30 inference(forward_demodulation,[],[f201,f225])).
% 0.21/0.30 thf(f232,plain,(
% 0.21/0.30 $false | (~spl9_9 | ~spl9_11)),
% 0.21/0.30 inference(trivial_inequality_removal,[],[f231])).
% 0.21/0.30 thf(f233,plain,(
% 0.21/0.30 ~spl9_9 | ~spl9_11),
% 0.21/0.30 inference(avatar_contradiction_clause,[],[f232])).
% 0.21/0.30 thf(f234,plain,(
% 0.21/0.30 ( ! [X0 : $i] : ((((sK1 @ X0)) = $false)) ) | ~spl9_12),
% 0.21/0.30 inference(constrained_superposition,[],[f215,f55])).
% 0.21/0.30 thf(f240,plain,(
% 0.21/0.30 ( ! [X0 : $i] : (($true = ((irel @ sK3 @ X0)))) ) | ~spl9_10),
% 0.21/0.30 inference(constrained_superposition,[],[f207,f55])).
% 0.21/0.30 thf(f250,plain,(
% 0.21/0.30 ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X0 @ X1)))) ) | ~spl9_10),
% 0.21/0.30 inference(constrained_superposition,[],[f240,f55])).
% 0.21/0.30 thf(f254,plain,(
% 0.21/0.30 ( ! [X1 : $i] : (($true = ((sK1 @ X1))) | ($true = $false)) ) | (~spl9_1 | ~spl9_10)),
% 0.21/0.30 inference(forward_demodulation,[],[f162,f250])).
% 0.21/0.30 thf(f255,plain,(
% 0.21/0.30 ( ! [X1 : $i] : (($true = ((sK1 @ X1)))) ) | (~spl9_1 | ~spl9_10)),
% 0.21/0.30 inference(trivial_inequality_removal,[],[f254])).
% 0.21/0.30 thf(f256,plain,(
% 0.21/0.30 ($true = $false) | (~spl9_1 | ~spl9_10 | ~spl9_12)),
% 0.21/0.30 inference(forward_demodulation,[],[f255,f234])).
% 0.21/0.30 thf(f257,plain,(
% 0.21/0.30 $false | (~spl9_1 | ~spl9_10 | ~spl9_12)),
% 0.21/0.30 inference(trivial_inequality_removal,[],[f256])).
% 0.21/0.30 thf(f258,plain,(
% 0.21/0.30 ~spl9_1 | ~spl9_10 | ~spl9_12),
% 0.21/0.30 inference(avatar_contradiction_clause,[],[f257])).
% 0.21/0.30 cnf(s1, plain, spl9_1 | spl9_1, inference(sat_conversion,[],[f163])).
% 0.21/0.30 cnf(s2, plain, spl9_1, inference(rat,[],[s1])).
% 0.21/0.30 cnf(s9, plain, spl9_6 | spl9_9, inference(sat_conversion,[],[f202])).
% 0.21/0.30 cnf(s11, plain, spl9_11 | spl9_10 | spl9_11, inference(sat_conversion,[],[f211])).
% 0.21/0.30 cnf(s12, plain, spl9_10 | spl9_11, inference(rat,[],[s11])).
% 0.21/0.30 cnf(s13, plain, spl9_11 | spl9_11 | spl9_12, inference(sat_conversion,[],[f216])).
% 0.21/0.30 cnf(s14, plain, spl9_11 | spl9_12, inference(rat,[],[s13])).
% 0.21/0.30 cnf(s15, plain, ~spl9_6 | ~spl9_11, inference(sat_conversion,[],[f229])).
% 0.21/0.30 cnf(s16, plain, ~spl9_9 | ~spl9_11, inference(sat_conversion,[],[f233])).
% 0.21/0.30 cnf(s17, plain, ~spl9_1 | ~spl9_10 | ~spl9_12, inference(sat_conversion,[],[f258])).
% 0.21/0.30 cnf(s18, plain, spl9_11, inference(rat,[],[s17,s12,s14,s2])).
% 0.21/0.30 cnf(s19, plain, ~spl9_9, inference(rat,[],[s16,s18])).
% 0.21/0.30 cnf(s20, plain, ~spl9_6, inference(rat,[],[s15,s18])).
% 0.21/0.30 cnf(s22, plain, $false, inference(rat,[],[s9,s19,s20])).
% 0.21/0.30 thf(f259,plain,(
% 0.21/0.30 $false),
% 0.21/0.30 inference(avatar_sat_refutation,[],[s22])).
% 0.21/0.30 % SZS output end Proof for theBenchmark
% 0.21/0.30 % (920891)------------------------------
% 0.21/0.30 % (920891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (920891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (920891)CaDiCaL version: 2.1.3
% 0.21/0.30 % (920891)Termination reason: Refutation
% 0.21/0.30 % (920891)Time elapsed: 0.016 s
% 0.21/0.30 % (920891)Peak memory usage: 13 MB
% 0.21/0.30 % (920891)Instructions burned: 31 (million)
% 0.21/0.30 % (920880)Success in time 0.054 s
% 0.21/0.30 % Vampire exiting
%------------------------------------------------------------------------------