%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX177^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 : n004.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.18s 0.28s
% Output : Refutation 0.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX177^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.16 % Computer : n004.cluster.edu
% 0.08/0.16 % Model : x86_64 x86_64
% 0.08/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.16 % Memory : 8046.5625MB
% 0.08/0.16 % OS : Linux 6.8.0-71-generic
% 0.08/0.16 % CPULimit : 300
% 0.08/0.16 % WCLimit : 300
% 0.08/0.16 % DateTime : Tue Sep 29 16:10:07 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 Running higher-order theorem proving
% 0.08/0.21 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.18/0.28 % (1488894)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.18/0.28 % (1488913)lrs+10_16_si=on:nwc=1.5:random_seed=3540638352:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.18/0.28 % (1488918)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.18/0.28 % (1488918)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.18/0.28 % (1488913)Instruction limit reached!
% 0.18/0.28 % (1488913)------------------------------
% 0.18/0.28 % (1488913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.28 % (1488913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.28 % (1488913)CaDiCaL version: 2.1.3
% 0.18/0.28 % (1488913)Termination reason: Instruction limit
% 0.18/0.28 % (1488913)Termination phase: Saturation
% 0.18/0.28 % (1488913)Time elapsed: 0.006 s
% 0.18/0.28 % (1488913)Peak memory usage: 12 MB
% 0.18/0.28 % (1488913)Instructions burned: 18 (million)
% 0.18/0.28 % (1488912)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1769781155:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.18/0.28 % (1488914)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=667941501:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.18/0.28 % (1488916)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=495650995:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.18/0.28 % (1488917)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1048030297:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.18/0.28 % (1488915)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=152019088: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.18/0.28 % (1488918)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=3443225157:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.18/0.28 % (1488914)Instruction limit reached!
% 0.18/0.28 % (1488914)------------------------------
% 0.18/0.28 % (1488914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.28 % (1488914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.28 % (1488914)CaDiCaL version: 2.1.3
% 0.18/0.28 % (1488914)Termination reason: Instruction limit
% 0.18/0.28 % (1488914)Termination phase: Preprocessing 3
% 0.18/0.28 % (1488914)Time elapsed: 0.002 s
% 0.18/0.28 % (1488914)Peak memory usage: 10 MB
% 0.18/0.28 % (1488914)Instructions burned: 4 (million)
% 0.18/0.28 % (1488912) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1488894-1488912"...
% 0.18/0.28 % (1488917) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1488894-1488917"...
% 0.18/0.28 % (1488918) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1488894-1488918"...
% 0.18/0.28 % (1488916)Instruction limit reached!
% 0.18/0.28 % (1488916)------------------------------
% 0.18/0.28 % (1488916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.28 % (1488916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.28 % (1488916)CaDiCaL version: 2.1.3
% 0.18/0.28 % (1488916)Termination reason: Instruction limit
% 0.18/0.28 % (1488916)Termination phase: Saturation
% 0.18/0.28 % (1488916)Time elapsed: 0.014 s
% 0.18/0.28 % (1488916)Peak memory usage: 12 MB
% 0.18/0.28 % (1488916)Instructions burned: 25 (million)
% 0.18/0.28 % (1488912)...printing done.
% 0.18/0.28 % (1488927)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1859365285:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.18/0.28 % (1488912)Refutation found. Thanks to Tanya!
% 0.18/0.28 % SZS status Theorem for theBenchmark
% 0.18/0.28 % SZS output start Proof for theBenchmark
% 0.18/0.28 thf(type_def_5, type, unsorted: $tType).
% 0.18/0.28 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.18/0.28 thf(type_def_7, type, d_unsorted: $tType).
% 0.18/0.28 thf(func_def_0, type, irel: ($i > $i > $o)).
% 0.18/0.28 thf(func_def_1, type, mnot: (($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_2, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_3, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_4, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_5, type, mbox_s4: (($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_6, type, iatom: (($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_7, type, inot: (($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_8, type, itrue: ($i > $o)).
% 0.18/0.28 thf(func_def_9, type, ifalse: ($i > $o)).
% 0.18/0.28 thf(func_def_10, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_11, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_12, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_13, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_14, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_15, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.18/0.28 thf(func_def_16, type, ivalid: (($i > $o) > $o)).
% 0.18/0.28 thf(func_def_17, type, isatisfiable: (($i > $o) > $o)).
% 0.18/0.28 thf(func_def_18, type, icountersatisfiable: (($i > $o) > $o)).
% 0.18/0.28 thf(func_def_19, type, iinvalid: (($i > $o) > $o)).
% 0.18/0.28 thf(func_def_20, type, d2unsorted: (d_unsorted > $i)).
% 0.18/0.28 thf(func_def_21, type, d_unsorted_0: d_unsorted).
% 0.18/0.28 thf(func_def_23, type, db1: !>[X0: $tType]:(X0)).
% 0.18/0.28 thf(func_def_24, type, db0: !>[X0: $tType]:(X0)).
% 0.18/0.28 thf(func_def_25, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.18/0.28 thf(func_def_26, type, vOR: ($o > $o > $o)).
% 0.18/0.28 thf(func_def_27, type, vNOT: ($o > $o)).
% 0.18/0.28 thf(func_def_28, type, db2: !>[X0: $tType]:(X0)).
% 0.18/0.28 thf(func_def_29, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.18/0.28 thf(func_def_32, type, vAND: ($o > $o > $o)).
% 0.18/0.28 thf(func_def_33, type, db8: !>[X0: $tType]:(X0)).
% 0.18/0.28 thf(func_def_34, type, db6: !>[X0: $tType]:(X0)).
% 0.18/0.28 thf(func_def_35, type, db3: !>[X0: $tType]:(X0)).
% 0.18/0.28 thf(func_def_36, type, db7: !>[X0: $tType]:(X0)).
% 0.18/0.28 thf(func_def_37, type, db5: !>[X0: $tType]:(X0)).
% 0.18/0.28 thf(func_def_38, type, db4: !>[X0: $tType]:(X0)).
% 0.18/0.28 thf(func_def_39, type, sK0: ($i > d_unsorted)).
% 0.18/0.28 thf(func_def_40, type, sK1: ($i > $o)).
% 0.18/0.28 thf(func_def_41, type, sK2: ($i > $o)).
% 0.18/0.28 thf(f1,axiom,(
% 0.18/0.28 (ior = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)) | ! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5))))) & (mnot = (^[X4 : ($i > $o), X0 : $i] : (~(X4 @ X0)))) & ((^[X18 : ($i > $o)] : (! [X19 : $i] : ~(X18 @ X19))) = iinvalid) & (itrue @ (d2unsorted @ d_unsorted_0)) & ((^[X8 : ($i > $o), X4 : $i] : (! [X5 : $i] : (~(irel @ X4 @ X5) | (X8 @ X5)))) = mbox_s4) & (iequiv = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i,X10 : $i] : (~(irel @ X7 @ X5) | ~ ! [X11 : $i] : (~(irel @ X5 @ X11) | (X8 @ X11)) | (X9 @ X10) | ~(irel @ X5 @ X10)) & ! [X12 : $i,X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X12) | ~(irel @ X5 @ X12) | ~ ! [X13 : $i] : (~(irel @ X5 @ X13) | (X9 @ X13)))))) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (~ ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)) | ! [X5 : $i] : (~(irel @ X7 @ X5) | (X9 @ X5)))) = iimplies) & ((^[X4 : ($i > $o), X5 : ($i > $o), X0 : $i] : ((X5 @ X0) & (X4 @ X0))) = mand) & ! [X1 : d_unsorted] : (X1 = d_unsorted_0) & (mor = (^[X4 : ($i > $o), X5 : ($i > $o), X0 : $i] : ((X5 @ X0) | (X4 @ X0)))) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)) & ! [X5 : $i] : (~(irel @ X7 @ X5) | (X9 @ X5)))) = iand) & (iatom = (^[X8 : ($i > $o), X7 : $i] : ((X8 @ X7)))) & ~(ifalse @ (d2unsorted @ d_unsorted_0)) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)) | ~ ! [X5 : $i] : (~(irel @ X7 @ X5) | (X9 @ X5)))) = iimplied) & ! [X3 : d_unsorted,X2 : d_unsorted] : ((((d2unsorted @ X2)) = ((d2unsorted @ X3))) => (X2 = X3)) & (ivalid = (^[X18 : ($i > $o)] : (! [X19 : $i] : (X18 @ X19)))) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (~ ! [X15 : $i,X14 : $i,X17 : $i,X5 : $i,X16 : $i] : (~(irel @ X7 @ X5) | ((~(irel @ X16 @ X17) | ~(irel @ X5 @ X16) | (X8 @ X17) | ~ ! [X13 : $i] : (~(irel @ X16 @ X13) | (X9 @ X13))) & (~(irel @ X5 @ X14) | (X9 @ X15) | ~(irel @ X14 @ X15) | ~ ! [X11 : $i] : ((X8 @ X11) | ~(irel @ X14 @ X11))))))) = ixor) & ((^[X18 : ($i > $o)] : (~ ! [X19 : $i] : ~(X18 @ X19))) = isatisfiable) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) & (icountersatisfiable = (^[X18 : ($i > $o)] : (~ ! [X19 : $i] : (X18 @ X19)))) & (inot = (^[X8 : ($i > $o), X7 : $i] : (~ ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5))))) & ! [X0 : $i] : ? [X1 : d_unsorted] : (X0 = ((d2unsorted @ X1))) & ((^[X0 : ($i > $o), X6 : ($i > $o), X7 : $i] : ((X6 @ X7) | ~(X0 @ X7))) = mimplies)),
% 0.18/0.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lcl696_1)).
% 0.18/0.28 thf(f2,conjecture,(
% 0.18/0.28 ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((mimplies @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))) = iimplies)),
% 0.18/0.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iimplies)).
% 0.18/0.28 thf(f3,negated_conjecture,(
% 0.18/0.28 ~ ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((mimplies @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))) = iimplies)),
% 0.18/0.28 inference(negated_conjecture,[status(cth)],[f2])).
% 0.18/0.28 thf(f4,plain,(
% 0.18/0.28 ~ (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 0.18/0.28 inference(fool_elimination,[],[f3])).
% 0.18/0.28 thf(f5,plain,(
% 0.18/0.28 (ior = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : (! [X3 : $i] : ((X0 @ X3) | ~(irel @ X2 @ X3)) | ! [X4 : $i] : ((X1 @ X4) | ~(irel @ X2 @ X4))))) & (mnot = (^[X5 : ($i > $o), X6 : $i] : (~(X5 @ X6)))) & ((^[X7 : ($i > $o)] : (! [X8 : $i] : ~(X7 @ X8))) = iinvalid) & (itrue @ (d2unsorted @ d_unsorted_0)) & ((^[X9 : ($i > $o), X10 : $i] : (! [X11 : $i] : (~(irel @ X10 @ X11) | (X9 @ X11)))) = mbox_s4) & (iequiv = (^[X12 : ($i > $o), X13 : ($i > $o), X14 : $i] : (! [X15 : $i,X16 : $i] : (~(irel @ X14 @ X15) | ~ ! [X17 : $i] : (~(irel @ X15 @ X17) | (X12 @ X17)) | (X13 @ X16) | ~(irel @ X15 @ X16)) & ! [X18 : $i,X19 : $i] : (~(irel @ X14 @ X19) | (X12 @ X18) | ~(irel @ X19 @ X18) | ~ ! [X20 : $i] : (~(irel @ X19 @ X20) | (X13 @ X20)))))) & ((^[X21 : ($i > $o), X22 : ($i > $o), X23 : $i] : (~ ! [X24 : $i] : ((X21 @ X24) | ~(irel @ X23 @ X24)) | ! [X25 : $i] : (~(irel @ X23 @ X25) | (X22 @ X25)))) = iimplies) & ((^[X26 : ($i > $o), X27 : ($i > $o), X28 : $i] : ((X27 @ X28) & (X26 @ X28))) = mand) & ! [X29 : d_unsorted] : (d_unsorted_0 = X29) & (mor = (^[X30 : ($i > $o), X31 : ($i > $o), X32 : $i] : ((X31 @ X32) | (X30 @ X32)))) & ((^[X33 : ($i > $o), X34 : ($i > $o), X35 : $i] : (! [X36 : $i] : ((X33 @ X36) | ~(irel @ X35 @ X36)) & ! [X37 : $i] : (~(irel @ X35 @ X37) | (X34 @ X37)))) = iand) & (iatom = (^[X38 : ($i > $o), X39 : $i] : ((X38 @ X39)))) & ~(ifalse @ (d2unsorted @ d_unsorted_0)) & ((^[X40 : ($i > $o), X41 : ($i > $o), X42 : $i] : (! [X43 : $i] : ((X40 @ X43) | ~(irel @ X42 @ X43)) | ~ ! [X44 : $i] : (~(irel @ X42 @ X44) | (X41 @ X44)))) = iimplied) & ! [X45 : d_unsorted,X46 : d_unsorted] : ((((d2unsorted @ X45)) = ((d2unsorted @ X46))) => (X45 = X46)) & (ivalid = (^[X47 : ($i > $o)] : (! [X48 : $i] : (X47 @ X48)))) & ((^[X49 : ($i > $o), X50 : ($i > $o), X51 : $i] : (~ ! [X52 : $i,X53 : $i,X54 : $i,X55 : $i,X56 : $i] : (~(irel @ X51 @ X55) | ((~(irel @ X56 @ X54) | ~(irel @ X55 @ X56) | (X49 @ X54) | ~ ! [X57 : $i] : (~(irel @ X56 @ X57) | (X50 @ X57))) & (~(irel @ X55 @ X53) | (X50 @ X52) | ~(irel @ X53 @ X52) | ~ ! [X58 : $i] : ((X49 @ X58) | ~(irel @ X53 @ X58))))))) = ixor) & ((^[X59 : ($i > $o)] : (~ ! [X60 : $i] : ~(X59 @ X60))) = isatisfiable) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) & (icountersatisfiable = (^[X61 : ($i > $o)] : (~ ! [X62 : $i] : (X61 @ X62)))) & (inot = (^[X63 : ($i > $o), X64 : $i] : (~ ! [X65 : $i] : ((X63 @ X65) | ~(irel @ X64 @ X65))))) & ! [X66 : $i] : ? [X67 : d_unsorted] : (((d2unsorted @ X67)) = X66) & ((^[X68 : ($i > $o), X69 : ($i > $o), X70 : $i] : ((X69 @ X70) | ~(X68 @ X70))) = mimplies)),
% 0.18/0.28 inference(rectify,[],[f1])).
% 0.18/0.28 thf(f6,plain,(
% 0.18/0.28 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (Y0 @ Y4)) | (~ (irel @ Y2 @ Y3))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (Y1 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y0 @ Y5) | (~ (irel @ Y4 @ Y5))))))) | (~ (irel @ Y2 @ Y4)))))))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & ! [X29 : d_unsorted] : (d_unsorted_0 = X29) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (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]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & ! [X45 : d_unsorted,X46 : d_unsorted] : ((((d2unsorted @ X45)) = ((d2unsorted @ X46))) => (X45 = X46)) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (~ (irel @ Y6 @ Y7))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((Y1 @ Y8) | (~ (irel @ Y3 @ Y8)))))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y3))) | (~ (irel @ Y3 @ Y5)))) | (~ (irel @ Y2 @ Y4)))))))))))))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2))))))))) & ! [X66 : $i] : ? [X67 : d_unsorted] : (((d2unsorted @ X67)) = X66) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2))))))))),
% 0.18/0.28 inference(fool_elimination,[],[f5])).
% 0.18/0.28 thf(f7,plain,(
% 0.18/0.28 (iimplies != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 0.18/0.28 inference(flattening,[],[f4])).
% 0.18/0.28 thf(f8,plain,(
% 0.18/0.28 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (Y0 @ Y4)) | (~ (irel @ Y2 @ Y3))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (Y1 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y0 @ Y5) | (~ (irel @ Y4 @ Y5))))))) | (~ (irel @ Y2 @ Y4)))))))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (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]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & ! [X1 : d_unsorted,X2 : d_unsorted] : ((((d2unsorted @ X1)) = ((d2unsorted @ X2))) => (X1 = X2)) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (~ (irel @ Y6 @ Y7))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((Y1 @ Y8) | (~ (irel @ Y3 @ Y8)))))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y3))) | (~ (irel @ Y3 @ Y5)))) | (~ (irel @ Y2 @ Y4)))))))))))))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2))))))))) & ! [X3 : $i] : ? [X4 : d_unsorted] : (((d2unsorted @ X4)) = X3) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2))))))))),
% 0.18/0.28 inference(rectify,[],[f6])).
% 0.18/0.28 thf(f9,plain,(
% 0.18/0.28 (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (~ (irel @ Y6 @ Y7))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((Y1 @ Y8) | (~ (irel @ Y3 @ Y8)))))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y3))) | (~ (irel @ Y3 @ Y5)))) | (~ (irel @ Y2 @ Y4)))))))))))))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & ! [X1 : d_unsorted,X2 : d_unsorted] : ((((d2unsorted @ X1)) = ((d2unsorted @ X2))) => (X1 = X2)) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (Y0 @ Y4)) | (~ (irel @ Y2 @ Y3))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (Y1 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y0 @ Y5) | (~ (irel @ Y4 @ Y5))))))) | (~ (irel @ Y2 @ Y4)))))))))))))) & ! [X3 : $i] : ? [X4 : d_unsorted] : (((d2unsorted @ X4)) = X3)),
% 0.18/0.28 inference(flattening,[],[f8])).
% 0.18/0.28 thf(f10,plain,(
% 0.18/0.28 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X3 : $i] : ? [X4 : d_unsorted] : (((d2unsorted @ X4)) = X3) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & ! [X2 : d_unsorted,X1 : d_unsorted] : ((((d2unsorted @ X1)) != ((d2unsorted @ X2))) | (X1 = X2)) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (~ (irel @ Y6 @ Y7))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((Y1 @ Y8) | (~ (irel @ Y3 @ Y8)))))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y3))) | (~ (irel @ Y3 @ Y5)))) | (~ (irel @ Y2 @ Y4)))))))))))))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (Y0 @ Y4)) | (~ (irel @ Y2 @ Y3))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (Y1 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y0 @ Y5) | (~ (irel @ Y4 @ Y5))))))) | (~ (irel @ Y2 @ Y4)))))))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))))),
% 0.18/0.28 inference(ennf_transformation,[],[f9])).
% 0.18/0.28 thf(f11,plain,(
% 0.18/0.28 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X1 : $i] : ? [X2 : d_unsorted] : (((d2unsorted @ X2)) = X1) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & ! [X3 : d_unsorted,X4 : d_unsorted] : ((((d2unsorted @ X3)) != ((d2unsorted @ X4))) | (X3 = X4)) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (~ (irel @ Y6 @ Y7))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((Y1 @ Y8) | (~ (irel @ Y3 @ Y8)))))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y3))) | (~ (irel @ Y3 @ Y5)))) | (~ (irel @ Y2 @ Y4)))))))))))))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (Y0 @ Y4)) | (~ (irel @ Y2 @ Y3))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (Y1 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y0 @ Y5) | (~ (irel @ Y4 @ Y5))))))) | (~ (irel @ Y2 @ Y4)))))))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))))),
% 0.18/0.28 inference(rectify,[],[f10])).
% 0.18/0.28 thf(f12,plain,(
% 0.18/0.28 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X1 : $i] : (((d2unsorted @ (sK0 @ X1))) = X1) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & ! [X3 : d_unsorted,X4 : d_unsorted] : ((((d2unsorted @ X3)) != ((d2unsorted @ X4))) | (X3 = X4)) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (~ (irel @ Y6 @ Y7))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((Y1 @ Y8) | (~ (irel @ Y3 @ Y8)))))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y3))) | (~ (irel @ Y3 @ Y5)))) | (~ (irel @ Y2 @ Y4)))))))))))))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (Y0 @ Y4)) | (~ (irel @ Y2 @ Y3))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (Y1 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y0 @ Y5) | (~ (irel @ Y4 @ Y5))))))) | (~ (irel @ Y2 @ Y4)))))))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))))),
% 0.18/0.28 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X2,sK0 @ X1)],[f11])).
% 0.18/0.28 thf(f14,plain,(
% 0.18/0.28 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2))))))))),
% 0.18/0.28 inference(cnf_transformation,[],[f12])).
% 0.18/0.28 thf(f28,plain,(
% 0.18/0.28 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))))),
% 0.18/0.28 inference(cnf_transformation,[],[f12])).
% 0.18/0.28 thf(f29,plain,(
% 0.18/0.28 ( ! [X1 : $i] : ((((d2unsorted @ (sK0 @ X1))) = X1)) )),
% 0.18/0.28 inference(cnf_transformation,[],[f12])).
% 0.18/0.28 thf(f33,plain,(
% 0.18/0.28 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))),
% 0.18/0.28 inference(cnf_transformation,[],[f12])).
% 0.18/0.28 thf(f34,plain,(
% 0.18/0.28 ( ! [X0 : d_unsorted] : ((d_unsorted_0 = X0)) )),
% 0.18/0.28 inference(cnf_transformation,[],[f12])).
% 0.18/0.28 thf(f36,plain,(
% 0.18/0.28 (iimplies != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 0.18/0.28 inference(cnf_transformation,[],[f7])).
% 0.18/0.28 thf(f39,plain,(
% 0.18/0.28 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ 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]: ((Y2 @ Y4) | (~ (irel @ Y3 @ Y4)))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y2 @ Y4) | (~ (irel @ Y3 @ Y4)))))))) @ Y1))))))),
% 0.18/0.28 inference(definition_unfolding,[],[f36,f28,f14,f33,f33])).
% 0.18/0.28 thf(f40,plain,(
% 0.18/0.28 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))))),
% 0.18/0.28 inference(beta-eta_normalization,[],[f39])).
% 0.18/0.28 thf(f41,plain,(
% 0.18/0.28 ( ! [X0 : d_unsorted,X1 : d_unsorted] : ((X0 = X1)) )),
% 0.18/0.28 inference(constrained_superposition,[],[f34,f34])).
% 0.18/0.28 thf(f42,plain,(
% 0.18/0.28 ((((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) @ sK1)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))) @ sK1)))),
% 0.18/0.28 inference(negative_extensionality,[],[f40])).
% 0.18/0.28 thf(f43,plain,(
% 0.18/0.28 ((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))))))))),
% 0.18/0.28 inference(beta-eta_normalization,[],[f42])).
% 0.18/0.28 thf(f52,plain,(
% 0.18/0.28 ( ! [X0 : d_unsorted,X1 : $i] : ((((d2unsorted @ X0)) = X1)) )),
% 0.18/0.28 inference(constrained_superposition,[],[f29,f41])).
% 0.18/0.28 thf(f60,plain,(
% 0.18/0.28 ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) )),
% 0.18/0.28 inference(constrained_superposition,[],[f29,f52])).
% 0.18/0.28 thf(f100,plain,(
% 0.18/0.28 ((((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))))))) @ sK2)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))))))) @ sK2)))),
% 0.18/0.28 inference(negative_extensionality,[],[f43])).
% 0.18/0.28 thf(f101,plain,(
% 0.18/0.28 ((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))) != (^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))))))),
% 0.18/0.28 inference(beta-eta_normalization,[],[f100])).
% 0.18/0.28 thf(f102,plain,(
% 0.18/0.28 ((((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))))) @ sK3)) != (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))) @ sK3)))),
% 0.18/0.28 inference(negative_extensionality,[],[f101])).
% 0.18/0.28 thf(f103,plain,(
% 0.18/0.28 ((((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))) @ sK3)) = $true) | ((((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))))) @ sK3)) = $true)),
% 0.18/0.28 inference(xor_proxy_clausification,[],[f102])).
% 0.18/0.28 thf(f104,plain,(
% 0.18/0.28 ((((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))) @ sK3)) = $false) | ((((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1))))))) @ sK3)) = $false)),
% 0.18/0.28 inference(xor_proxy_clausification,[],[f102])).
% 0.18/0.28 thf(f105,plain,(
% 0.18/0.28 ($false = (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))))))),
% 0.18/0.28 inference(beta-eta_normalization,[],[f104])).
% 0.18/0.28 thf(f106,plain,(
% 0.18/0.28 ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))))),
% 0.18/0.28 inference(or_proxy_clausification,[],[f105])).
% 0.18/0.28 thf(f107,plain,(
% 0.18/0.28 ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))))) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $false)),
% 0.18/0.28 inference(or_proxy_clausification,[],[f105])).
% 0.18/0.28 thf(f108,plain,(
% 0.18/0.28 (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $false)),
% 0.18/0.28 inference(or_proxy_clausification,[],[f107])).
% 0.18/0.28 thf(f120,plain,(
% 0.18/0.28 ($false = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ sK5))) | ($false = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ sK5)))),
% 0.18/0.28 inference(sigma_proxy_clausification,[],[f108])).
% 0.18/0.28 thf(f121,plain,(
% 0.18/0.28 ($false = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ sK5)))),
% 0.18/0.28 inference(duplicate_literal_removal,[],[f120])).
% 0.18/0.28 thf(f122,plain,(
% 0.18/0.28 ($false = (((sK2 @ sK5) | (~ (irel @ sK3 @ sK5)))))),
% 0.18/0.28 inference(beta-eta_normalization,[],[f121])).
% 0.18/0.28 thf(f123,plain,(
% 0.18/0.28 ($false = ((~ (irel @ sK3 @ sK5))))),
% 0.18/0.28 inference(or_proxy_clausification,[],[f122])).
% 0.18/0.28 thf(f124,plain,(
% 0.18/0.28 ($false = ((sK2 @ sK5)))),
% 0.18/0.28 inference(or_proxy_clausification,[],[f122])).
% 0.18/0.28 thf(f125,plain,(
% 0.18/0.28 (((irel @ sK3 @ sK5)) = $true)),
% 0.18/0.28 inference(not_proxy_clausification,[],[f123])).
% 0.18/0.28 thf(f127,plain,(
% 0.18/0.28 ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0))))))))),
% 0.18/0.28 inference(or_proxy_clausification,[],[f106])).
% 0.18/0.28 thf(f128,plain,(
% 0.18/0.28 ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))))),
% 0.18/0.28 inference(not_proxy_clausification,[],[f127])).
% 0.18/0.28 thf(f129,plain,(
% 0.18/0.28 ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) | (((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $true)),
% 0.18/0.28 inference(not_proxy_clausification,[],[f128])).
% 0.18/0.28 thf(f130,plain,(
% 0.18/0.28 ( ! [X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $true) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ X1)))) )),
% 0.18/0.28 inference(pi_proxy_clausification,[],[f129])).
% 0.18/0.28 thf(f131,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X2))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ X1)))) )),
% 0.18/0.28 inference(pi_proxy_clausification,[],[f130])).
% 0.18/0.28 thf(f132,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : (($true = (((sK1 @ X2) | (~ (irel @ sK3 @ X2))))) | ($true = (((~ (irel @ sK3 @ X1)) | (sK1 @ X1))))) )),
% 0.18/0.28 inference(beta-eta_normalization,[],[f131])).
% 0.18/0.28 thf(f133,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : (($true = ((sK1 @ X2))) | (((~ (irel @ sK3 @ X2))) = $true) | ($true = (((~ (irel @ sK3 @ X1)) | (sK1 @ X1))))) )),
% 0.18/0.28 inference(or_proxy_clausification,[],[f132])).
% 0.18/0.28 thf(f134,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK3 @ X2)) = $false) | ($true = (((~ (irel @ sK3 @ X1)) | (sK1 @ X1)))) | ($true = ((sK1 @ X2)))) )),
% 0.18/0.28 inference(not_proxy_clausification,[],[f133])).
% 0.18/0.28 thf(f135,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : ((((~ (irel @ sK3 @ X1))) = $true) | ($true = ((sK1 @ X2))) | (((sK1 @ X1)) = $true) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.18/0.28 inference(or_proxy_clausification,[],[f134])).
% 0.18/0.28 thf(f136,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : (($true = ((sK1 @ X2))) | (((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ sK3 @ X1))) | (((sK1 @ X1)) = $true)) )),
% 0.18/0.28 inference(not_proxy_clausification,[],[f135])).
% 0.18/0.28 thf(f146,plain,(
% 0.18/0.28 ($true = (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))))))),
% 0.18/0.28 inference(beta-eta_normalization,[],[f103])).
% 0.18/0.28 thf(f147,plain,(
% 0.18/0.28 (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $true) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))))))),
% 0.18/0.28 inference(or_proxy_clausification,[],[f146])).
% 0.18/0.28 thf(f148,plain,(
% 0.18/0.28 ( ! [X1 : $i] : (($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))))) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X1))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0))))))))) )),
% 0.18/0.28 inference(pi_proxy_clausification,[],[f147])).
% 0.18/0.28 thf(f149,plain,(
% 0.18/0.28 ( ! [X1 : $i] : (($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X1)))) )),
% 0.18/0.28 inference(not_proxy_clausification,[],[f148])).
% 0.18/0.28 thf(f150,plain,(
% 0.18/0.28 ( ! [X1 : $i] : (($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))))) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X1))) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $true) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))))))) )),
% 0.18/0.28 inference(or_proxy_clausification,[],[f149])).
% 0.18/0.28 thf(f151,plain,(
% 0.18/0.28 ( ! [X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0)))))) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X1))) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $false)) )),
% 0.18/0.28 inference(not_proxy_clausification,[],[f150])).
% 0.18/0.28 thf(f152,plain,(
% 0.18/0.28 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ sK7))) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $false)) )),
% 0.18/0.28 inference(sigma_proxy_clausification,[],[f151])).
% 0.18/0.28 thf(f153,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X1))) | (((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))))) = $false) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ sK7))) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X2)) = $true)) )),
% 0.18/0.28 inference(pi_proxy_clausification,[],[f152])).
% 0.18/0.28 thf(f154,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X2)) = $true) | ($false = (((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ sK8))) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK3 @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (sK1 @ Y0))) @ sK7)))) )),
% 0.18/0.28 inference(sigma_proxy_clausification,[],[f153])).
% 0.18/0.28 thf(f155,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : (($true = (((sK2 @ X1) | (~ (irel @ sK3 @ X1))))) | ($false = (((sK1 @ sK8) | (~ (irel @ sK3 @ sK8))))) | ((((sK2 @ X2) | (~ (irel @ sK3 @ X2)))) = $true) | ((((~ (irel @ sK3 @ sK7)) | (sK1 @ sK7))) = $false)) )),
% 0.18/0.28 inference(beta-eta_normalization,[],[f154])).
% 0.18/0.28 thf(f156,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : (((((sK2 @ X2) | (~ (irel @ sK3 @ X2)))) = $true) | ((((~ (irel @ sK3 @ sK7)) | (sK1 @ sK7))) = $false) | (((sK2 @ X1)) = $true) | (((~ (irel @ sK3 @ X1))) = $true) | ($false = (((sK1 @ sK8) | (~ (irel @ sK3 @ sK8)))))) )),
% 0.18/0.28 inference(or_proxy_clausification,[],[f155])).
% 0.18/0.28 thf(f157,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : (($true = ((sK2 @ X2))) | ((((~ (irel @ sK3 @ sK7)) | (sK1 @ sK7))) = $false) | ($false = (((sK1 @ sK8) | (~ (irel @ sK3 @ sK8))))) | (((~ (irel @ sK3 @ X2))) = $true) | (((sK2 @ X1)) = $true) | (((~ (irel @ sK3 @ X1))) = $true)) )),
% 0.18/0.28 inference(or_proxy_clausification,[],[f156])).
% 0.18/0.28 thf(f158,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : ((((~ (irel @ sK3 @ X2))) = $true) | (((~ (irel @ sK3 @ X1))) = $true) | ($false = (((sK1 @ sK8) | (~ (irel @ sK3 @ sK8))))) | ($true = ((sK2 @ X2))) | (((sK2 @ X1)) = $true) | ($false = ((sK1 @ sK7)))) )),
% 0.18/0.28 inference(or_proxy_clausification,[],[f157])).
% 0.18/0.28 thf(f167,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : (($false = (((sK1 @ sK8) | (~ (irel @ sK3 @ sK8))))) | ($false = ((sK1 @ sK7))) | (((~ (irel @ sK3 @ X1))) = $true) | ($true = ((sK2 @ X2))) | (((irel @ sK3 @ X2)) = $false) | (((sK2 @ X1)) = $true)) )),
% 0.18/0.28 inference(not_proxy_clausification,[],[f158])).
% 0.18/0.28 thf(f169,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK3 @ X2)) = $false) | (((~ (irel @ sK3 @ X1))) = $true) | ($true = ((sK2 @ X2))) | (((sK2 @ X1)) = $true) | ($false = ((sK1 @ sK7))) | ($false = ((sK1 @ sK8)))) )),
% 0.18/0.28 inference(or_proxy_clausification,[],[f167])).
% 0.18/0.28 thf(f170,plain,(
% 0.18/0.28 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((sK1 @ sK7))) | ($false = ((sK1 @ sK8))) | (((sK2 @ X1)) = $true)) )),
% 0.18/0.28 inference(not_proxy_clausification,[],[f169])).
% 0.18/0.28 thf(f178,definition,(
% 0.18/0.28 spl9_2 <=> ! [X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((sK1 @ X1)) = $true))),
% 0.18/0.28 introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition])).
% 0.18/0.28 thf(f179,plain,(
% 0.18/0.28 ( ! [X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((sK1 @ X1)) = $true)) ) | ~spl9_2),
% 0.18/0.28 inference(avatar_component_clause,[],[f178])).
% 0.18/0.28 thf(f186,plain,(
% 0.18/0.28 spl9_2 | spl9_2),
% 0.18/0.28 inference(avatar_split_clause,[],[f136,f178,f178])).
% 0.18/0.28 thf(f198,definition,(
% 0.18/0.28 spl9_6 <=> ! [X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((sK2 @ X1)) = $true))),
% 0.18/0.28 introduced(definition,[new_symbols(definition,[spl9_6])],[avatar_definition])).
% 0.18/0.28 thf(f199,plain,(
% 0.18/0.28 ( ! [X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((sK2 @ X1)) = $true)) ) | ~spl9_6),
% 0.18/0.28 inference(avatar_component_clause,[],[f198])).
% 0.18/0.28 thf(f201,definition,(
% 0.18/0.28 spl9_7 <=> ($false = ((sK1 @ sK8)))),
% 0.18/0.28 introduced(definition,[new_symbols(definition,[spl9_7])],[avatar_definition])).
% 0.18/0.28 thf(f203,plain,(
% 0.18/0.28 ($false = ((sK1 @ sK8))) | ~spl9_7),
% 0.18/0.28 inference(avatar_component_clause,[],[f201])).
% 0.18/0.28 thf(f215,definition,(
% 0.18/0.28 spl9_10 <=> ($false = ((sK1 @ sK7)))),
% 0.18/0.28 introduced(definition,[new_symbols(definition,[spl9_10])],[avatar_definition])).
% 0.18/0.28 thf(f217,plain,(
% 0.18/0.28 ($false = ((sK1 @ sK7))) | ~spl9_10),
% 0.18/0.28 inference(avatar_component_clause,[],[f215])).
% 0.18/0.28 thf(f218,plain,(
% 0.18/0.28 spl9_6 | spl9_6 | spl9_7 | spl9_10),
% 0.18/0.28 inference(avatar_split_clause,[],[f170,f215,f201,f198,f198])).
% 0.18/0.28 thf(f220,plain,(
% 0.18/0.28 ( ! [X0 : $i] : (($false = ((sK2 @ X0)))) )),
% 0.18/0.28 inference(constrained_superposition,[],[f124,f60])).
% 0.18/0.28 thf(f223,plain,(
% 0.18/0.28 ( ! [X0 : $i] : (($true = ((irel @ sK3 @ X0)))) )),
% 0.18/0.28 inference(constrained_superposition,[],[f125,f60])).
% 0.18/0.28 thf(f227,plain,(
% 0.18/0.28 ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X0 @ X1)))) )),
% 0.18/0.28 inference(constrained_superposition,[],[f223,f60])).
% 0.18/0.28 thf(f230,plain,(
% 0.18/0.28 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ X0 @ X1))) | (((sK2 @ X1)) = $true)) ) | ~spl9_6),
% 0.18/0.28 inference(constrained_superposition,[],[f199,f60])).
% 0.18/0.28 thf(f275,plain,(
% 0.18/0.28 ( ! [X1 : $i] : ((((sK2 @ X1)) = $true) | ($false = $true)) ) | ~spl9_6),
% 0.18/0.28 inference(forward_demodulation,[],[f230,f227])).
% 0.18/0.28 thf(f276,plain,(
% 0.18/0.28 ( ! [X1 : $i] : ((((sK2 @ X1)) = $true)) ) | ~spl9_6),
% 0.18/0.28 inference(trivial_inequality_removal,[],[f275])).
% 0.18/0.28 thf(f289,plain,(
% 0.18/0.28 ($false = $true) | ~spl9_6),
% 0.18/0.28 inference(forward_demodulation,[],[f276,f220])).
% 0.18/0.28 thf(f290,plain,(
% 0.18/0.28 $false | ~spl9_6),
% 0.18/0.28 inference(trivial_inequality_removal,[],[f289])).
% 0.18/0.28 thf(f291,plain,(
% 0.18/0.28 ~spl9_6),
% 0.18/0.28 inference(avatar_contradiction_clause,[],[f290])).
% 0.18/0.28 thf(f292,plain,(
% 0.18/0.28 ( ! [X0 : $i] : (($false = ((sK1 @ X0)))) ) | ~spl9_7),
% 0.18/0.28 inference(constrained_superposition,[],[f203,f60])).
% 0.18/0.28 thf(f294,plain,(
% 0.18/0.28 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ X0 @ X1))) | (((sK1 @ X1)) = $true)) ) | ~spl9_2),
% 0.18/0.28 inference(constrained_superposition,[],[f179,f60])).
% 0.18/0.28 thf(f302,plain,(
% 0.18/0.28 ( ! [X0 : $i] : ((((sK1 @ X0)) = $true) | ($false = $true)) ) | ~spl9_2),
% 0.18/0.28 inference(constrained_superposition,[],[f223,f179])).
% 0.18/0.28 thf(f314,plain,(
% 0.18/0.28 ( ! [X0 : $i] : ((((sK1 @ X0)) = $true)) ) | ~spl9_2),
% 0.18/0.28 inference(trivial_inequality_removal,[],[f302])).
% 0.18/0.28 thf(f339,plain,(
% 0.18/0.28 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ X0 @ X1))) | ($false = $true)) ) | (~spl9_2 | ~spl9_7)),
% 0.18/0.28 inference(forward_demodulation,[],[f294,f292])).
% 0.18/0.28 thf(f340,plain,(
% 0.18/0.28 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ X0 @ X1)))) ) | (~spl9_2 | ~spl9_7)),
% 0.18/0.28 inference(trivial_inequality_removal,[],[f339])).
% 0.18/0.28 thf(f353,plain,(
% 0.18/0.28 ($false = $true) | (~spl9_2 | ~spl9_7)),
% 0.18/0.28 inference(forward_demodulation,[],[f340,f227])).
% 0.18/0.28 thf(f354,plain,(
% 0.18/0.28 $false | (~spl9_2 | ~spl9_7)),
% 0.18/0.28 inference(trivial_inequality_removal,[],[f353])).
% 0.18/0.28 thf(f355,plain,(
% 0.18/0.28 ~spl9_2 | ~spl9_7),
% 0.18/0.28 inference(avatar_contradiction_clause,[],[f354])).
% 0.18/0.28 thf(f358,plain,(
% 0.18/0.28 ( ! [X0 : $i] : (($false = ((sK1 @ X0)))) ) | ~spl9_10),
% 0.18/0.28 inference(constrained_superposition,[],[f217,f60])).
% 0.18/0.28 thf(f362,plain,(
% 0.18/0.28 ($false = $true) | (~spl9_2 | ~spl9_10)),
% 0.18/0.28 inference(forward_demodulation,[],[f358,f314])).
% 0.18/0.28 thf(f363,plain,(
% 0.18/0.28 $false | (~spl9_2 | ~spl9_10)),
% 0.18/0.28 inference(trivial_inequality_removal,[],[f362])).
% 0.18/0.28 thf(f364,plain,(
% 0.18/0.28 ~spl9_2 | ~spl9_10),
% 0.18/0.28 inference(avatar_contradiction_clause,[],[f363])).
% 0.18/0.28 cnf(s3, plain, spl9_2 | spl9_2, inference(sat_conversion,[],[f186])).
% 0.18/0.28 cnf(s4, plain, spl9_2, inference(rat,[],[s3])).
% 0.18/0.28 cnf(s11, plain, spl9_6 | spl9_6 | spl9_7 | spl9_10, inference(sat_conversion,[],[f218])).
% 0.18/0.28 cnf(s12, plain, spl9_6 | spl9_7 | spl9_10, inference(rat,[],[s11])).
% 0.18/0.28 cnf(s26, plain, ~spl9_6, inference(sat_conversion,[],[f291])).
% 0.18/0.28 cnf(s38, plain, ~spl9_2 | ~spl9_7, inference(sat_conversion,[],[f355])).
% 0.18/0.28 cnf(s40, plain, ~spl9_2 | ~spl9_10, inference(sat_conversion,[],[f364])).
% 0.18/0.28 cnf(s42, plain, spl9_7 | spl9_10, inference(rat,[],[s12,s26])).
% 0.18/0.28 cnf(s45, plain, ~spl9_10, inference(rat,[],[s40,s4])).
% 0.18/0.28 cnf(s46, plain, ~spl9_7, inference(rat,[],[s38,s4])).
% 0.18/0.28 cnf(s48, plain, $false, inference(rat,[],[s42,s45,s46])).
% 0.18/0.28 thf(f365,plain,(
% 0.18/0.28 $false),
% 0.18/0.28 inference(avatar_sat_refutation,[],[s48])).
% 0.18/0.28 % SZS output end Proof for theBenchmark
% 0.18/0.28 % (1488912)------------------------------
% 0.18/0.28 % (1488912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.28 % (1488912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.28 % (1488912)CaDiCaL version: 2.1.3
% 0.18/0.28 % (1488912)Termination reason: Refutation
% 0.18/0.28 % (1488912)Time elapsed: 0.017 s
% 0.18/0.28 % (1488912)Peak memory usage: 13 MB
% 0.18/0.28 % (1488912)Instructions burned: 34 (million)
% 0.18/0.28 % (1488894)Success in time 0.062 s
% 0.18/0.28 % Vampire exiting
%------------------------------------------------------------------------------