%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX175^1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : 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:45 AM UTC 2026
% Result : Theorem 0.19s 0.28s
% Output : Refutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX175^1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19 % Computer : n004.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 16:09:52 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.28 % (1488088)Will run a generic schedule for satisfiability detection.
% 0.19/0.28 % (1488098)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=161467991:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.28 % (1488094)% WARNING: option uhcvi not known.
% 0.19/0.28 % (1488093)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3405332660_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.28 % (1488094)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2777490016:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.28 % (1488095)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3799394359:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.28 % (1488096)dis+10_1_sil=32000:sp=arity:random_seed=1939893896:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.28 % (1488097)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4276690912:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.28 % (1488099)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3182263328:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.28 % (1488094)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.19/0.28 % (1488097)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.19/0.28 % Exception at run slice level
% 0.19/0.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.19/0.28 % (1488094)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.19/0.28 % (1488098) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1488088-1488098"...
% 0.19/0.28 % (1488107)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3714933738:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.19/0.28 % Exception at run slice level
% 0.19/0.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.19/0.28 % (1488098)...printing done.
% 0.19/0.28 % (1488098)Refutation found. Thanks to Tanya!
% 0.19/0.28 % SZS status Theorem for theBenchmark
% 0.19/0.28 % SZS output start Proof for theBenchmark
% 0.19/0.28 thf(type_def_5, type, unsorted: $tType).
% 0.19/0.28 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.19/0.28 thf(type_def_7, type, d_unsorted: $tType).
% 0.19/0.28 thf(func_def_0, type, irel: ($i > $i > $o)).
% 0.19/0.28 thf(func_def_1, type, mnot: (($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_2, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_3, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_4, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_5, type, mbox_s4: (($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_6, type, iatom: (($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_7, type, inot: (($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_8, type, itrue: ($i > $o)).
% 0.19/0.28 thf(func_def_9, type, ifalse: ($i > $o)).
% 0.19/0.28 thf(func_def_10, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_11, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_12, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_13, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_14, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_15, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.19/0.28 thf(func_def_16, type, ivalid: (($i > $o) > $o)).
% 0.19/0.28 thf(func_def_17, type, isatisfiable: (($i > $o) > $o)).
% 0.19/0.28 thf(func_def_18, type, icountersatisfiable: (($i > $o) > $o)).
% 0.19/0.28 thf(func_def_19, type, iinvalid: (($i > $o) > $o)).
% 0.19/0.28 thf(func_def_20, type, d2unsorted: (d_unsorted > $i)).
% 0.19/0.28 thf(func_def_21, type, d_unsorted_0: d_unsorted).
% 0.19/0.28 thf(func_def_23, type, vNOT: ($o > $o)).
% 0.19/0.28 thf(func_def_24, type, db1: !>[X0: $tType]:(X0)).
% 0.19/0.28 thf(func_def_25, type, db0: !>[X0: $tType]:(X0)).
% 0.19/0.28 thf(func_def_26, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.19/0.28 thf(func_def_27, type, vOR: ($o > $o > $o)).
% 0.19/0.28 thf(func_def_28, type, db2: !>[X0: $tType]:(X0)).
% 0.19/0.28 thf(func_def_29, type, vAND: ($o > $o > $o)).
% 0.19/0.28 thf(func_def_30, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.19/0.28 thf(func_def_31, type, db3: !>[X0: $tType]:(X0)).
% 0.19/0.28 thf(func_def_32, type, db6: !>[X0: $tType]:(X0)).
% 0.19/0.28 thf(func_def_33, type, db4: !>[X0: $tType]:(X0)).
% 0.19/0.28 thf(func_def_34, type, db5: !>[X0: $tType]:(X0)).
% 0.19/0.28 thf(func_def_37, type, sK0: ($i > d_unsorted)).
% 0.19/0.28 thf(func_def_38, type, sK1: ($i > $o)).
% 0.19/0.28 thf(func_def_39, type, sK2: ($i > $o)).
% 0.19/0.28 thf(func_def_41, type, sK4: ($i > $i)).
% 0.19/0.28 thf(func_def_42, type, sK5: ($i > $i)).
% 0.19/0.28 thf(func_def_43, type, sK6: ($i > $i)).
% 0.19/0.28 thf(func_def_44, type, sK7: ($i > $i)).
% 0.19/0.28 thf(func_def_45, type, sK8: ($i > $i)).
% 0.19/0.28 thf(func_def_46, type, sK9: ($i > $i)).
% 0.19/0.28 thf(func_def_47, type, sK10: ($i > $i)).
% 0.19/0.28 thf(func_def_48, type, sK11: ($i > $i)).
% 0.19/0.28 thf(func_def_49, type, sK12: ($i > $i)).
% 0.19/0.28 thf(func_def_50, type, sK13: ($i > $i)).
% 0.19/0.28 thf(f1,axiom,(
% 0.19/0.28 ~(ifalse @ (d2unsorted @ d_unsorted_0)) & (itrue @ (d2unsorted @ d_unsorted_0)) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) & (iinvalid = (^[X14 : ($i > $o)] : (! [X15 : $i] : ~(X14 @ X15)))) & (icountersatisfiable = (^[X14 : ($i > $o)] : (~ ! [X15 : $i] : (X14 @ X15)))) & (isatisfiable = (^[X14 : ($i > $o)] : (~ ! [X15 : $i] : ~(X14 @ X15)))) & (ivalid = (^[X14 : ($i > $o)] : (! [X15 : $i] : (X14 @ X15)))) & (ixor = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (~ ! [X5 : $i,X10 : $i,X11 : $i] : ((((X8 @ X11) | ~(irel @ X5 @ X11) | ~ ! [X13 : $i] : ((X9 @ X13) | ~(irel @ X5 @ X13))) & ((X9 @ X10) | ~(irel @ X5 @ X10) | ~ ! [X12 : $i] : ((X8 @ X12) | ~(irel @ X5 @ X12)))) | ~(irel @ X7 @ X5))))) & (iequiv = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : ((! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)) | ~ ! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5))) & (! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ~ ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)))))) & (iimplied = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)) | ~ ! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5))))) & (iimplies = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ~ ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5))))) & (ior = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5))))) & (iand = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : ((X9 @ X7) & (X8 @ X7)))) & (inot = (^[X8 : ($i > $o), X7 : $i] : (~ ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5))))) & (iatom = (^[X8 : ($i > $o), X7 : $i] : ((X8 @ X7)))) & (mbox_s4 = (^[X8 : ($i > $o), X4 : $i] : (! [X5 : $i] : ((X8 @ X5) | ~(irel @ X4 @ X5))))) & (mimplies = (^[X0 : ($i > $o), X6 : ($i > $o), X7 : $i] : ((X6 @ X7) | ~(X0 @ X7)))) & (mand = (^[X4 : ($i > $o), X5 : ($i > $o), X0 : $i] : ((X5 @ X0) & (X4 @ X0)))) & (mor = (^[X4 : ($i > $o), X5 : ($i > $o), X0 : $i] : ((X5 @ X0) | (X4 @ X0)))) & (mnot = (^[X4 : ($i > $o), X0 : $i] : (~(X4 @ X0)))) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((((d2unsorted @ X2)) = ((d2unsorted @ X3))) => (X2 = X3)) & ! [X1 : d_unsorted] : (X1 = d_unsorted_0) & ! [X0 : $i] : ? [X1 : d_unsorted] : (X0 = ((d2unsorted @ X1)))),
% 0.19/0.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lcl695_1)).
% 0.19/0.28 thf(f2,conjecture,(
% 0.19/0.28 (ixor = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((inot @ (iequiv @ X0 @ X1)))))),
% 0.19/0.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ixor)).
% 0.19/0.28 thf(f3,negated_conjecture,(
% 0.19/0.28 ~ (ixor = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((inot @ (iequiv @ X0 @ X1)))))),
% 0.19/0.28 inference(negated_conjecture,[status(cth)],[f2])).
% 0.19/0.28 thf(f4,plain,(
% 0.19/0.28 ~(ifalse @ (d2unsorted @ d_unsorted_0)) & (itrue @ (d2unsorted @ d_unsorted_0)) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) & (iinvalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : ~(X0 @ X1)))) & (icountersatisfiable = (^[X2 : ($i > $o)] : (~ ! [X3 : $i] : (X2 @ X3)))) & (isatisfiable = (^[X4 : ($i > $o)] : (~ ! [X5 : $i] : ~(X4 @ X5)))) & (ivalid = (^[X6 : ($i > $o)] : (! [X7 : $i] : (X6 @ X7)))) & (ixor = (^[X8 : ($i > $o), X9 : ($i > $o), X10 : $i] : (~ ! [X11 : $i,X12 : $i,X13 : $i] : ((((X8 @ X13) | ~(irel @ X11 @ X13) | ~ ! [X14 : $i] : ((X9 @ X14) | ~(irel @ X11 @ X14))) & ((X9 @ X12) | ~(irel @ X11 @ X12) | ~ ! [X15 : $i] : ((X8 @ X15) | ~(irel @ X11 @ X15)))) | ~(irel @ X10 @ X11))))) & (iequiv = (^[X16 : ($i > $o), X17 : ($i > $o), X18 : $i] : ((! [X19 : $i] : ((X16 @ X19) | ~(irel @ X18 @ X19)) | ~ ! [X20 : $i] : ((X17 @ X20) | ~(irel @ X18 @ X20))) & (! [X21 : $i] : ((X17 @ X21) | ~(irel @ X18 @ X21)) | ~ ! [X22 : $i] : ((X16 @ X22) | ~(irel @ X18 @ X22)))))) & (iimplied = (^[X23 : ($i > $o), X24 : ($i > $o), X25 : $i] : (! [X26 : $i] : ((X23 @ X26) | ~(irel @ X25 @ X26)) | ~ ! [X27 : $i] : ((X24 @ X27) | ~(irel @ X25 @ X27))))) & (iimplies = (^[X28 : ($i > $o), X29 : ($i > $o), X30 : $i] : (! [X31 : $i] : ((X29 @ X31) | ~(irel @ X30 @ X31)) | ~ ! [X32 : $i] : ((X28 @ X32) | ~(irel @ X30 @ X32))))) & (ior = (^[X33 : ($i > $o), X34 : ($i > $o), X35 : $i] : (! [X36 : $i] : ((X34 @ X36) | ~(irel @ X35 @ X36)) | ! [X37 : $i] : ((X33 @ X37) | ~(irel @ X35 @ X37))))) & (iand = (^[X38 : ($i > $o), X39 : ($i > $o), X40 : $i] : ((X39 @ X40) & (X38 @ X40)))) & (inot = (^[X41 : ($i > $o), X42 : $i] : (~ ! [X43 : $i] : ((X41 @ X43) | ~(irel @ X42 @ X43))))) & (iatom = (^[X44 : ($i > $o), X45 : $i] : ((X44 @ X45)))) & (mbox_s4 = (^[X46 : ($i > $o), X47 : $i] : (! [X48 : $i] : ((X46 @ X48) | ~(irel @ X47 @ X48))))) & (mimplies = (^[X49 : ($i > $o), X50 : ($i > $o), X51 : $i] : ((X50 @ X51) | ~(X49 @ X51)))) & (mand = (^[X52 : ($i > $o), X53 : ($i > $o), X54 : $i] : ((X53 @ X54) & (X52 @ X54)))) & (mor = (^[X55 : ($i > $o), X56 : ($i > $o), X57 : $i] : ((X56 @ X57) | (X55 @ X57)))) & (mnot = (^[X58 : ($i > $o), X59 : $i] : (~(X58 @ X59)))) & ! [X60 : d_unsorted,X61 : d_unsorted] : ((((d2unsorted @ X60)) = ((d2unsorted @ X61))) => (X60 = X61)) & ! [X62 : d_unsorted] : (d_unsorted_0 = X62) & ! [X63 : $i] : ? [X64 : d_unsorted] : (((d2unsorted @ X64)) = X63)),
% 0.19/0.28 inference(rectify,[],[f1])).
% 0.19/0.28 thf(f5,plain,(
% 0.19/0.28 ~ (((ifalse @ (d2unsorted @ d_unsorted_0))) = $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (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]: ((~ (irel @ Y2 @ Y5)) | ((((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y0 @ Y6))))) | (~ (irel @ Y5 @ Y4))) | (Y1 @ Y4)) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y1 @ Y6))))) | (~ (irel @ Y5 @ Y3))) | (Y0 @ Y3))))))))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iand = (^[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))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X60 : d_unsorted,X61 : d_unsorted] : ((((d2unsorted @ X60)) = ((d2unsorted @ X61))) => (X60 = X61)) & ! [X62 : d_unsorted] : (d_unsorted_0 = X62) & ! [X63 : $i] : ? [X64 : d_unsorted] : (((d2unsorted @ X64)) = X63)),
% 0.19/0.28 inference(fool_elimination,[],[f4])).
% 0.19/0.28 thf(f6,plain,(
% 0.19/0.28 ~ (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (inot @ (iequiv @ Y0 @ Y1))))))),
% 0.19/0.28 inference(fool_elimination,[],[f3])).
% 0.19/0.28 thf(f7,plain,(
% 0.19/0.28 ~ (((ifalse @ (d2unsorted @ d_unsorted_0))) = $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (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]: ((~ (irel @ Y2 @ Y5)) | ((((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y0 @ Y6))))) | (~ (irel @ Y5 @ Y4))) | (Y1 @ Y4)) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y1 @ Y6))))) | (~ (irel @ Y5 @ Y3))) | (Y0 @ Y3))))))))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iand = (^[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))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X0 : d_unsorted,X1 : d_unsorted] : ((((d2unsorted @ X1)) = ((d2unsorted @ X0))) => (X0 = X1)) & ! [X2 : d_unsorted] : (d_unsorted_0 = X2) & ! [X3 : $i] : ? [X4 : d_unsorted] : (((d2unsorted @ X4)) = X3)),
% 0.19/0.28 inference(rectify,[],[f5])).
% 0.19/0.28 thf(f8,plain,(
% 0.19/0.28 (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (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]: ((~ (irel @ Y2 @ Y5)) | ((((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y0 @ Y6))))) | (~ (irel @ Y5 @ Y4))) | (Y1 @ Y4)) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y1 @ Y6))))) | (~ (irel @ Y5 @ Y3))) | (Y0 @ Y3))))))))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iand = (^[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))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X0 : d_unsorted,X1 : d_unsorted] : ((((d2unsorted @ X1)) = ((d2unsorted @ X0))) => (X0 = X1)) & ! [X2 : d_unsorted] : (d_unsorted_0 = X2) & ! [X3 : $i] : ? [X4 : d_unsorted] : (((d2unsorted @ X4)) = X3)),
% 0.19/0.28 inference(flattening,[],[f7])).
% 0.19/0.28 thf(f9,plain,(
% 0.19/0.28 (ixor != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (inot @ (iequiv @ Y0 @ Y1))))))),
% 0.19/0.28 inference(flattening,[],[f6])).
% 0.19/0.28 thf(f10,plain,(
% 0.19/0.28 (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (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]: ((~ (irel @ Y2 @ Y5)) | ((((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y0 @ Y6))))) | (~ (irel @ Y5 @ Y4))) | (Y1 @ Y4)) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y1 @ Y6))))) | (~ (irel @ Y5 @ Y3))) | (Y0 @ Y3))))))))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iand = (^[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))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X0 : d_unsorted,X1 : d_unsorted] : ((X0 = X1) | (((d2unsorted @ X1)) != ((d2unsorted @ X0)))) & ! [X2 : d_unsorted] : (d_unsorted_0 = X2) & ! [X3 : $i] : ? [X4 : d_unsorted] : (((d2unsorted @ X4)) = X3)),
% 0.19/0.28 inference(ennf_transformation,[],[f8])).
% 0.19/0.28 thf(f11,plain,(
% 0.19/0.28 (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (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]: ((~ (irel @ Y2 @ Y5)) | ((((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y0 @ Y6))))) | (~ (irel @ Y5 @ Y4))) | (Y1 @ Y4)) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y1 @ Y6))))) | (~ (irel @ Y5 @ Y3))) | (Y0 @ Y3))))))))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iand = (^[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))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X0 : d_unsorted,X1 : d_unsorted] : ((X0 = X1) | (((d2unsorted @ X1)) != ((d2unsorted @ X0)))) & ! [X2 : d_unsorted] : (d_unsorted_0 = X2) & ! [X3 : $i] : (((d2unsorted @ (sK0 @ X3))) = X3)),
% 0.19/0.28 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X4,sK0 @ X3)],[f10])).
% 0.19/0.28 thf(f12,plain,(
% 0.19/0.28 ( ! [X3 : $i] : ((((d2unsorted @ (sK0 @ X3))) = X3)) )),
% 0.19/0.28 inference(cnf_transformation,[],[f11])).
% 0.19/0.28 thf(f13,plain,(
% 0.19/0.28 ( ! [X2 : d_unsorted] : ((d_unsorted_0 = X2)) )),
% 0.19/0.28 inference(cnf_transformation,[],[f11])).
% 0.19/0.28 thf(f21,plain,(
% 0.19/0.28 (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))))),
% 0.19/0.28 inference(cnf_transformation,[],[f11])).
% 0.19/0.28 thf(f26,plain,(
% 0.19/0.28 (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))))))))))),
% 0.19/0.28 inference(cnf_transformation,[],[f11])).
% 0.19/0.28 thf(f27,plain,(
% 0.19/0.28 (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y2 @ Y5)) | ((((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y0 @ Y6))))) | (~ (irel @ Y5 @ Y4))) | (Y1 @ Y4)) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y1 @ Y6))))) | (~ (irel @ Y5 @ Y3))) | (Y0 @ Y3)))))))))))))))))),
% 0.19/0.28 inference(cnf_transformation,[],[f11])).
% 0.19/0.28 thf(f32,plain,(
% 0.19/0.28 (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true)),
% 0.19/0.28 inference(cnf_transformation,[],[f11])).
% 0.19/0.28 thf(f35,plain,(
% 0.19/0.28 (ixor != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (inot @ (iequiv @ Y0 @ Y1))))))),
% 0.19/0.28 inference(cnf_transformation,[],[f9])).
% 0.19/0.28 thf(f38,plain,(
% 0.19/0.28 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y2 @ Y5)) | ((((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y0 @ Y6))))) | (~ (irel @ Y5 @ Y4))) | (Y1 @ Y4)) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y1 @ Y6))))) | (~ (irel @ Y5 @ Y3))) | (Y0 @ Y3)))))))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y2 @ Y4)))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (((~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y2 @ Y5))))) | (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y3 @ Y5))))) & ((~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y3 @ Y5))))) | (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y2 @ Y5))))))))))) @ Y0 @ Y1))))))),
% 0.19/0.28 inference(definition_unfolding,[],[f35,f27,f21,f26])).
% 0.19/0.28 thf(f39,plain,(
% 0.19/0.28 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y2 @ Y5)) | ((((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y0 @ Y6))))) | (~ (irel @ Y5 @ Y4))) | (Y1 @ Y4)) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y1 @ Y6))))) | (~ (irel @ Y5 @ Y3))) | (Y0 @ Y3)))))))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y1 @ Y4))))) & ((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y1 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4))))))))))))))))),
% 0.19/0.28 inference(beta-eta_normalization,[],[f38])).
% 0.19/0.28 thf(f52,plain,(
% 0.19/0.28 ( ! [X0 : $i] : ((((d2unsorted @ d_unsorted_0)) = X0)) )),
% 0.19/0.28 inference(constrained_superposition,[],[f12,f13])).
% 0.19/0.28 thf(f59,plain,(
% 0.19/0.28 ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) )),
% 0.19/0.28 inference(constrained_superposition,[],[f52,f52])).
% 0.19/0.28 thf(f113,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($true = ((irel @ X0 @ X0)))) )),
% 0.19/0.28 inference(constrained_superposition,[],[f32,f59])).
% 0.19/0.28 thf(f114,plain,(
% 0.19/0.28 ((((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y2 @ Y5)) | ((((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y0 @ Y6))))) | (~ (irel @ Y5 @ Y4))) | (Y1 @ Y4)) & (((~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y1 @ Y6))))) | (~ (irel @ Y5 @ Y3))) | (Y0 @ Y3)))))))))))))))) @ sK1)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y1 @ Y4))))) & ((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y1 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4))))))))))))))) @ sK1)))),
% 0.19/0.28 inference(negative_extensionality,[],[f39])).
% 0.19/0.28 thf(f115,plain,(
% 0.19/0.28 ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y1 @ Y4)) | ((((~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (sK1 @ Y5))))) | (~ (irel @ Y4 @ Y3))) | (Y0 @ Y3)) & (((~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5))))) | (~ (irel @ Y4 @ Y2))) | (sK1 @ Y2)))))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))))))))))))),
% 0.19/0.28 inference(beta-eta_normalization,[],[f114])).
% 0.19/0.28 thf(f134,plain,(
% 0.19/0.28 ((((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y1 @ Y4)) | ((((~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (sK1 @ Y5))))) | (~ (irel @ Y4 @ Y3))) | (Y0 @ Y3)) & (((~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5))))) | (~ (irel @ Y4 @ Y2))) | (sK1 @ Y2)))))))))))))) @ sK2)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))))))))))) @ sK2)))),
% 0.19/0.28 inference(negative_extensionality,[],[f115])).
% 0.19/0.28 thf(f135,plain,(
% 0.19/0.28 ((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y0 @ Y3)) | ((((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK1 @ Y4))))) | (~ (irel @ Y3 @ Y2))) | (sK2 @ Y2)) & (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK2 @ Y4))))) | (~ (irel @ Y3 @ Y1))) | (sK1 @ Y1)))))))))))) != (^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))))))))))),
% 0.19/0.28 inference(beta-eta_normalization,[],[f134])).
% 0.19/0.28 thf(f143,plain,(
% 0.19/0.28 ((((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y0 @ Y3)) | ((((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK1 @ Y4))))) | (~ (irel @ Y3 @ Y2))) | (sK2 @ Y2)) & (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK2 @ Y4))))) | (~ (irel @ Y3 @ Y1))) | (sK1 @ Y1)))))))))))) @ sK3)) != (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))))))))) @ sK3)))),
% 0.19/0.28 inference(negative_extensionality,[],[f135])).
% 0.19/0.28 thf(f144,plain,(
% 0.19/0.28 ($true = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y0 @ Y3)) | ((((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK1 @ Y4))))) | (~ (irel @ Y3 @ Y2))) | (sK2 @ Y2)) & (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK2 @ Y4))))) | (~ (irel @ Y3 @ Y1))) | (sK1 @ Y1)))))))))))) @ sK3))) | ($true = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))))))))) @ sK3)))),
% 0.19/0.28 inference(xor_proxy_clausification,[],[f143])).
% 0.19/0.28 thf(f145,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y0 @ Y3)) | ((((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK1 @ Y4))))) | (~ (irel @ Y3 @ Y2))) | (sK2 @ Y2)) & (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK2 @ Y4))))) | (~ (irel @ Y3 @ Y1))) | (sK1 @ Y1)))))))))))) @ sK3))) | ($false = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))))))))) @ sK3)))),
% 0.19/0.28 inference(xor_proxy_clausification,[],[f143])).
% 0.19/0.28 thf(f146,plain,(
% 0.19/0.28 ($false = ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK3 @ Y2)) | ((((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)) & (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3))))) | (~ (irel @ Y2 @ Y0))) | (sK1 @ Y0))))))))))))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))))))))),
% 0.19/0.28 inference(beta-eta_normalization,[],[f145])).
% 0.19/0.28 thf(f147,plain,(
% 0.19/0.28 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK3 @ Y2)) | ((((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)) & (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3))))) | (~ (irel @ Y2 @ Y0))) | (sK1 @ Y0)))))))))))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))))))))),
% 0.19/0.28 inference(not_proxy_clausification,[],[f146])).
% 0.19/0.28 thf(f148,plain,(
% 0.19/0.28 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK3 @ Y2)) | ((((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)) & (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3))))) | (~ (irel @ Y2 @ Y0))) | (sK1 @ Y0))))))))) @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))))))))) )),
% 0.19/0.28 inference(pi_proxy_clausification,[],[f147])).
% 0.19/0.28 thf(f149,plain,(
% 0.19/0.28 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK3 @ Y2)) | ((((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)) & (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3))))) | (~ (irel @ Y2 @ Y0))) | (sK1 @ Y0))))))))) @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))))))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f148])).
% 0.19/0.28 thf(f150,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK3 @ Y2)) | ((((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)) & (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3))))) | (~ (irel @ Y2 @ Y0))) | (sK1 @ Y0))))))))) @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))))) @ X2)))) )),
% 0.19/0.28 inference(pi_proxy_clausification,[],[f149])).
% 0.19/0.28 thf(f151,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1)))))))))) | ($true = (((~ (irel @ sK3 @ X2)) | (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0)))))))))) )),
% 0.19/0.28 inference(beta-eta_normalization,[],[f150])).
% 0.19/0.28 thf(f152,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = (((~ (irel @ sK3 @ X2)) | (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0)))))))))) )),
% 0.19/0.28 inference(pi_proxy_clausification,[],[f151])).
% 0.19/0.28 thf(f153,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0)))))))) | ($true = ((~ (irel @ sK3 @ X2))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f152])).
% 0.19/0.28 thf(f154,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))))) | ($true = ((~ (irel @ sK3 @ X2))))) )),
% 0.19/0.28 inference(and_proxy_clausification,[],[f153])).
% 0.19/0.28 thf(f155,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))))) | ($true = ((~ (irel @ sK3 @ X2))))) )),
% 0.19/0.28 inference(and_proxy_clausification,[],[f153])).
% 0.19/0.28 thf(f156,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0)))))) | ($true = ((~ (irel @ sK3 @ X2)))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0)))))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f155])).
% 0.19/0.28 thf(f157,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))) @ X4))) | ($true = ((~ (irel @ sK3 @ X2)))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0)))))))) )),
% 0.19/0.28 inference(pi_proxy_clausification,[],[f156])).
% 0.19/0.28 thf(f158,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))) @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0)))))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f157])).
% 0.19/0.28 thf(f159,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))) @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f158])).
% 0.19/0.28 thf(f160,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))) @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))) @ (sK4 @ X2))))) )),
% 0.19/0.28 inference(sigma_proxy_clausification,[],[f159])).
% 0.19/0.28 thf(f161,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1)))))))) | ($true = (((~ (irel @ X2 @ X4)) | (sK2 @ X4)))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK4 @ X2))) | (sK1 @ (sK4 @ X2)))))) )),
% 0.19/0.28 inference(beta-eta_normalization,[],[f160])).
% 0.19/0.28 thf(f162,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1))))) @ X5))) | ($true = (((~ (irel @ X2 @ X4)) | (sK2 @ X4)))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK4 @ X2))) | (sK1 @ (sK4 @ X2)))))) )),
% 0.19/0.28 inference(pi_proxy_clausification,[],[f161])).
% 0.19/0.28 thf(f163,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1))))) @ X5))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK4 @ X2))) | (sK1 @ (sK4 @ X2))))) | ($true = ((~ (irel @ X2 @ X4))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f162])).
% 0.19/0.28 thf(f164,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1))))) @ X5))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($true = ((~ (irel @ X2 @ X4))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f163])).
% 0.19/0.28 thf(f192,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1))))) @ X5))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4)))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f164])).
% 0.19/0.28 thf(f193,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((~ (irel @ sK3 @ X5)) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ X5 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ X5 @ X1))) | (sK1 @ X1)))))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4)))) )),
% 0.19/0.28 inference(beta-eta_normalization,[],[f192])).
% 0.19/0.28 thf(f194,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ X5 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ X5 @ X1))) | (sK1 @ X1))))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($true = ((~ (irel @ sK3 @ X5))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f193])).
% 0.19/0.28 thf(f196,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($true = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ X5 @ X3))) | (sK2 @ X3)))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($true = ((~ (irel @ sK3 @ X5))))) )),
% 0.19/0.28 inference(and_proxy_clausification,[],[f194])).
% 0.19/0.28 thf(f197,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($true = ((~ (irel @ sK3 @ X5)))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ X5 @ X3)))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f196])).
% 0.19/0.28 thf(f198,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ X5 @ X3)))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f197])).
% 0.19/0.28 thf(f199,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($true = ((~ (irel @ X5 @ X3)))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK1 @ Y0)))))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f198])).
% 0.19/0.28 thf(f200,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X3))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK1 @ Y0)))))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f199])).
% 0.19/0.28 thf(f201,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X3))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK1 @ Y0))))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f200])).
% 0.19/0.28 thf(f202,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X3))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK1 @ Y0))) @ (sK7 @ X5))))) )),
% 0.19/0.28 inference(sigma_proxy_clausification,[],[f201])).
% 0.19/0.28 thf(f203,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X3))) | ($false = (((~ (irel @ X5 @ (sK7 @ X5))) | (sK1 @ (sK7 @ X5)))))) )),
% 0.19/0.28 inference(beta-eta_normalization,[],[f202])).
% 0.19/0.28 thf(f204,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X3))) | ($false = ((sK1 @ (sK7 @ X5))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f203])).
% 0.19/0.28 thf(f217,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0)))))) | ($true = ((~ (irel @ sK3 @ X2)))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0)))))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f154])).
% 0.19/0.28 thf(f218,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))) @ X4))) | ($true = ((~ (irel @ sK3 @ X2)))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0)))))))) )),
% 0.19/0.28 inference(pi_proxy_clausification,[],[f217])).
% 0.19/0.28 thf(f219,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))) @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0)))))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f218])).
% 0.19/0.28 thf(f220,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))) @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f219])).
% 0.19/0.28 thf(f221,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ X1))) | (sK1 @ X1))))))) @ X3))) | ($true = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))) @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))) @ (sK9 @ X2))))) )),
% 0.19/0.28 inference(sigma_proxy_clausification,[],[f220])).
% 0.19/0.28 thf(f222,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1)))))))) | ($true = (((~ (irel @ X2 @ X4)) | (sK1 @ X4)))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK9 @ X2))) | (sK2 @ (sK9 @ X2)))))) )),
% 0.19/0.28 inference(beta-eta_normalization,[],[f221])).
% 0.19/0.28 thf(f223,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1))))) @ X5))) | ($true = (((~ (irel @ X2 @ X4)) | (sK1 @ X4)))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK9 @ X2))) | (sK2 @ (sK9 @ X2)))))) )),
% 0.19/0.28 inference(pi_proxy_clausification,[],[f222])).
% 0.19/0.28 thf(f224,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1))))) @ X5))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK9 @ X2))) | (sK2 @ (sK9 @ X2))))) | ($true = ((~ (irel @ X2 @ X4))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f223])).
% 0.19/0.28 thf(f225,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1))))) @ X5))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($true = ((~ (irel @ X2 @ X4))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f224])).
% 0.19/0.28 thf(f253,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1))))) @ X5))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4)))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f225])).
% 0.19/0.28 thf(f254,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((~ (irel @ sK3 @ X5)) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ X5 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ X5 @ X1))) | (sK1 @ X1)))))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4)))) )),
% 0.19/0.28 inference(beta-eta_normalization,[],[f253])).
% 0.19/0.28 thf(f255,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ X5 @ X3))) | (sK2 @ X3)) & (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ X5 @ X1))) | (sK1 @ X1))))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($true = ((~ (irel @ sK3 @ X5))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f254])).
% 0.19/0.28 thf(f256,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ X5 @ X1))) | (sK1 @ X1)))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($true = ((~ (irel @ sK3 @ X5))))) )),
% 0.19/0.28 inference(and_proxy_clausification,[],[f255])).
% 0.19/0.28 thf(f268,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($true = ((~ (irel @ sK3 @ X5)))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ X5 @ X1)))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f256])).
% 0.19/0.28 thf(f269,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ X5 @ X1)))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f268])).
% 0.19/0.28 thf(f270,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($true = ((~ (irel @ X5 @ X1)))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK2 @ Y0)))))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f269])).
% 0.19/0.28 thf(f271,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X1))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK2 @ Y0)))))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f270])).
% 0.19/0.28 thf(f272,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X1))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK2 @ Y0))))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f271])).
% 0.19/0.28 thf(f273,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X1))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X5 @ Y0)) | (sK2 @ Y0))) @ (sK13 @ X5))))) )),
% 0.19/0.28 inference(sigma_proxy_clausification,[],[f272])).
% 0.19/0.28 thf(f274,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X1))) | ($false = (((~ (irel @ X5 @ (sK13 @ X5))) | (sK2 @ (sK13 @ X5)))))) )),
% 0.19/0.28 inference(beta-eta_normalization,[],[f273])).
% 0.19/0.28 thf(f275,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X1))) | ($false = ((sK2 @ (sK13 @ X5))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f274])).
% 0.19/0.28 thf(f278,plain,(
% 0.19/0.28 ($true = ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK3 @ Y2)) | ((((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)) & (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3))))) | (~ (irel @ Y2 @ Y0))) | (sK1 @ Y0))))))))))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))))))))),
% 0.19/0.28 inference(beta-eta_normalization,[],[f144])).
% 0.19/0.28 thf(f279,plain,(
% 0.19/0.28 ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK3 @ Y2)) | ((((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)) & (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3))))) | (~ (irel @ Y2 @ Y0))) | (sK1 @ Y0)))))))))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))))))))),
% 0.19/0.28 inference(not_proxy_clausification,[],[f278])).
% 0.19/0.28 thf(f280,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK3 @ Y2)) | ((((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)) & (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3))))) | (~ (irel @ Y2 @ Y0))) | (sK1 @ Y0))))))))) @ sK14))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))))))))),
% 0.19/0.28 inference(sigma_proxy_clausification,[],[f279])).
% 0.19/0.28 thf(f281,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK3 @ Y2)) | ((((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)) & (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3))))) | (~ (irel @ Y2 @ Y0))) | (sK1 @ Y0))))))))) @ sK14))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))))))))),
% 0.19/0.28 inference(not_proxy_clausification,[],[f280])).
% 0.19/0.28 thf(f282,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK3 @ Y2)) | ((((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)) & (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3))))) | (~ (irel @ Y2 @ Y0))) | (sK1 @ Y0))))))))) @ sK14))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))))) @ sK15)))),
% 0.19/0.28 inference(sigma_proxy_clausification,[],[f281])).
% 0.19/0.28 thf(f283,plain,(
% 0.19/0.28 ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14)))))))))) | ($false = (((~ (irel @ sK3 @ sK15)) | (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0)))))))))),
% 0.19/0.28 inference(beta-eta_normalization,[],[f282])).
% 0.19/0.28 thf(f284,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($false = (((~ (irel @ sK3 @ sK15)) | (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0)))))))))),
% 0.19/0.28 inference(sigma_proxy_clausification,[],[f283])).
% 0.19/0.28 thf(f285,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))))))),
% 0.19/0.28 inference(or_proxy_clausification,[],[f284])).
% 0.19/0.28 thf(f340,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))))),
% 0.19/0.28 inference(and_proxy_clausification,[],[f285])).
% 0.19/0.28 thf(f341,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0)))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))))),
% 0.19/0.28 inference(or_proxy_clausification,[],[f340])).
% 0.19/0.28 thf(f342,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))))),
% 0.19/0.28 inference(or_proxy_clausification,[],[f340])).
% 0.19/0.28 thf(f343,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))))),
% 0.19/0.28 inference(not_proxy_clausification,[],[f342])).
% 0.19/0.28 thf(f344,plain,(
% 0.19/0.28 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))) @ X1))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))))) )),
% 0.19/0.28 inference(pi_proxy_clausification,[],[f343])).
% 0.19/0.28 thf(f346,plain,(
% 0.19/0.28 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))) @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0)))))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f344])).
% 0.19/0.28 thf(f347,plain,(
% 0.19/0.28 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))) @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f346])).
% 0.19/0.28 thf(f348,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))) @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))) @ X2)))) )),
% 0.19/0.28 inference(pi_proxy_clausification,[],[f347])).
% 0.19/0.28 thf(f349,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ sK14))) | (sK1 @ sK14)))))))) | ($true = (((~ (irel @ sK15 @ X1)) | (sK2 @ X1)))) | ($true = (((~ (irel @ sK15 @ X2)) | (sK1 @ X2))))) )),
% 0.19/0.28 inference(beta-eta_normalization,[],[f348])).
% 0.19/0.28 thf(f350,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ sK14))) | (sK1 @ sK14))))) @ sK18))) | ($true = (((~ (irel @ sK15 @ X1)) | (sK2 @ X1)))) | ($true = (((~ (irel @ sK15 @ X2)) | (sK1 @ X2))))) )),
% 0.19/0.28 inference(sigma_proxy_clausification,[],[f349])).
% 0.19/0.28 thf(f351,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ sK14))) | (sK1 @ sK14))))) @ sK18))) | ($true = ((sK2 @ X1))) | ($true = (((~ (irel @ sK15 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK15 @ X1))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f350])).
% 0.19/0.28 thf(f352,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ sK14))) | (sK1 @ sK14))))) @ sK18))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($true = ((~ (irel @ sK15 @ X1)))) | ($true = ((~ (irel @ sK15 @ X2))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f351])).
% 0.19/0.28 thf(f353,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ sK14))) | (sK1 @ sK14))))) @ sK18))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($true = ((~ (irel @ sK15 @ X2))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f352])).
% 0.19/0.28 thf(f354,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ sK14))) | (sK1 @ sK14))))) @ sK18))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2)))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f353])).
% 0.19/0.28 thf(f355,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = (((~ (irel @ sK3 @ sK18)) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK18 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ sK18 @ sK14))) | (sK1 @ sK14)))))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2)))) )),
% 0.19/0.28 inference(beta-eta_normalization,[],[f354])).
% 0.19/0.28 thf(f356,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = (((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK18 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ sK18 @ sK14))) | (sK1 @ sK14))))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2)))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f355])).
% 0.19/0.28 thf(f359,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ sK18 @ sK14))) | (sK1 @ sK14)))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK18 @ sK16))) | (sK2 @ sK16))))) )),
% 0.19/0.28 inference(and_proxy_clausification,[],[f356])).
% 0.19/0.28 thf(f361,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ sK18 @ sK14))))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK18 @ sK16))) | (sK2 @ sK16))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f359])).
% 0.19/0.28 thf(f363,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK2 @ Y0))))))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK18 @ sK16))) | (sK2 @ sK16))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f361])).
% 0.19/0.28 thf(f364,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK2 @ Y0)))))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK18 @ sK16))) | (sK2 @ sK16))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f363])).
% 0.19/0.28 thf(f365,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK18 @ sK16))) | (sK2 @ sK16))))) )),
% 0.19/0.28 inference(pi_proxy_clausification,[],[f364])).
% 0.19/0.28 thf(f367,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK18 @ sK16)))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f365])).
% 0.19/0.28 thf(f369,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK1 @ Y0)))))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f367])).
% 0.19/0.28 thf(f370,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK1 @ Y0))))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f369])).
% 0.19/0.28 thf(f371,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK18 @ Y0)) | (sK1 @ Y0))) @ X4)))) )),
% 0.19/0.28 inference(pi_proxy_clausification,[],[f370])).
% 0.19/0.28 thf(f372,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((~ (irel @ sK18 @ X3)) | (sK2 @ X3)))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($true = (((~ (irel @ sK18 @ X4)) | (sK1 @ X4))))) )),
% 0.19/0.28 inference(beta-eta_normalization,[],[f371])).
% 0.19/0.28 thf(f373,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($true = (((~ (irel @ sK18 @ X4)) | (sK1 @ X4)))) | ($true = ((~ (irel @ sK18 @ X3))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f372])).
% 0.19/0.28 thf(f374,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($true = ((sK1 @ X4))) | ($true = ((~ (irel @ sK18 @ X3)))) | ($true = ((~ (irel @ sK18 @ X4))))) )),
% 0.19/0.28 inference(or_proxy_clausification,[],[f373])).
% 0.19/0.28 thf(f375,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK18 @ X3))) | ($true = ((~ (irel @ sK18 @ X4))))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f374])).
% 0.19/0.28 thf(f376,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X1))) | ($false = ((irel @ sK15 @ X2))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK18 @ X3))) | ($false = ((irel @ sK18 @ X4)))) )),
% 0.19/0.28 inference(not_proxy_clausification,[],[f375])).
% 0.19/0.28 thf(f514,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))) @ sK21))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))))),
% 0.19/0.28 inference(sigma_proxy_clausification,[],[f341])).
% 0.19/0.28 thf(f515,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))) @ sK21))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))))),
% 0.19/0.28 inference(or_proxy_clausification,[],[f514])).
% 0.19/0.28 thf(f628,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK3 @ Y1)) | ((((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)) & (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (~ (irel @ Y1 @ sK14))) | (sK1 @ sK14))))))) @ sK16))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))) @ sK21))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))) @ sK23)))),
% 0.19/0.28 inference(sigma_proxy_clausification,[],[f515])).
% 0.19/0.28 thf(f629,plain,(
% 0.19/0.28 ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ sK14))) | (sK1 @ sK14)))))))) | ($false = (((~ (irel @ sK15 @ sK21)) | (sK1 @ sK21)))) | ($false = (((~ (irel @ sK15 @ sK23)) | (sK2 @ sK23))))),
% 0.19/0.28 inference(beta-eta_normalization,[],[f628])).
% 0.19/0.28 thf(f630,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ sK14))) | (sK1 @ sK14))))) @ sK24))) | ($false = (((~ (irel @ sK15 @ sK21)) | (sK1 @ sK21)))) | ($false = (((~ (irel @ sK15 @ sK23)) | (sK2 @ sK23))))),
% 0.19/0.28 inference(sigma_proxy_clausification,[],[f629])).
% 0.19/0.28 thf(f631,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ sK14))) | (sK1 @ sK14))))) @ sK24))) | ($false = ((sK1 @ sK21))) | ($false = (((~ (irel @ sK15 @ sK23)) | (sK2 @ sK23))))),
% 0.19/0.28 inference(or_proxy_clausification,[],[f630])).
% 0.19/0.28 thf(f737,plain,(
% 0.19/0.28 ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (~ (irel @ Y0 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (~ (irel @ Y0 @ sK14))) | (sK1 @ sK14))))) @ sK24))) | ($false = ((sK1 @ sK21))) | ($false = ((sK2 @ sK23)))),
% 0.19/0.28 inference(or_proxy_clausification,[],[f631])).
% 0.19/0.28 thf(f790,plain,(
% 0.19/0.28 ($false = (((~ (irel @ sK3 @ sK24)) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK24 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ sK24 @ sK14))) | (sK1 @ sK14)))))) | ($false = ((sK1 @ sK21))) | ($false = ((sK2 @ sK23)))),
% 0.19/0.28 inference(beta-eta_normalization,[],[f737])).
% 0.19/0.28 thf(f791,plain,(
% 0.19/0.28 ($false = (((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK24 @ sK16))) | (sK2 @ sK16)) & (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ sK24 @ sK14))) | (sK1 @ sK14))))) | ($false = ((sK1 @ sK21))) | ($false = ((sK2 @ sK23)))),
% 0.19/0.28 inference(or_proxy_clausification,[],[f790])).
% 0.19/0.28 thf(f794,plain,(
% 0.19/0.28 ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK2 @ Y0))))) | (~ (irel @ sK24 @ sK14))) | (sK1 @ sK14)))) | ($false = ((sK1 @ sK21))) | ($false = ((sK2 @ sK23))) | ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK24 @ sK16))) | (sK2 @ sK16))))),
% 0.19/0.28 inference(and_proxy_clausification,[],[f791])).
% 0.19/0.28 thf(f795,plain,(
% 0.19/0.28 ($false = ((sK1 @ sK14))) | ($false = ((sK1 @ sK21))) | ($false = ((sK2 @ sK23))) | ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK1 @ Y0))))) | (~ (irel @ sK24 @ sK16))) | (sK2 @ sK16))))),
% 0.19/0.28 inference(or_proxy_clausification,[],[f794])).
% 0.19/0.28 thf(f830,plain,(
% 0.19/0.28 ($false = ((sK1 @ sK14))) | ($false = ((sK1 @ sK21))) | ($false = ((sK2 @ sK23))) | ($false = ((sK2 @ sK16)))),
% 0.19/0.28 inference(or_proxy_clausification,[],[f795])).
% 0.19/0.28 thf(f845,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((sK1 @ (sK4 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X3))) | ($false = ((sK1 @ (sK7 @ X5))))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f204,f52])).
% 0.19/0.28 thf(f855,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((sK2 @ (sK9 @ X2)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X1))) | ($false = ((sK2 @ (sK13 @ X5))))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f275,f52])).
% 0.19/0.28 thf(f867,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X1))) | ($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK15 @ X2))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK18 @ X3))) | ($false = ((irel @ sK18 @ X4)))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f376,f52])).
% 0.19/0.28 thf(f955,plain,(
% 0.19/0.28 ($false = ((sK1 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((sK1 @ sK21))) | ($false = ((sK2 @ sK23))) | ($false = ((sK2 @ sK16)))),
% 0.19/0.28 inference(forward_demodulation,[],[f830,f52])).
% 0.19/0.28 thf(f961,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($false = ((sK1 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X3))) | ($false = ((sK1 @ (sK7 @ X5))))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f845,f52])).
% 0.19/0.28 thf(f971,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X5))) | ($false = ((irel @ X5 @ X1))) | ($false = ((sK2 @ (sK13 @ X5))))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f855,f52])).
% 0.19/0.28 thf(f983,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X1))) | ($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK18 @ X3))) | ($false = ((irel @ sK18 @ X4)))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f867,f52])).
% 0.19/0.28 thf(f1079,plain,(
% 0.19/0.28 ($false = ((sK1 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((sK1 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((sK2 @ sK23))) | ($false = ((sK2 @ sK16)))),
% 0.19/0.28 inference(forward_demodulation,[],[f955,f52])).
% 0.19/0.28 thf(f1080,plain,(
% 0.19/0.28 ($false = ((sK1 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((sK2 @ sK23))) | ($false = ((sK2 @ sK16)))),
% 0.19/0.28 inference(duplicate_literal_removal,[],[f1079])).
% 0.19/0.28 thf(f1086,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X5))) | ($false = ((sK1 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ X5 @ X3))) | ($false = ((sK1 @ (sK7 @ X5))))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f961,f52])).
% 0.19/0.28 thf(f1096,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X5))) | ($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ X5 @ X1))) | ($false = ((sK2 @ (sK13 @ X5))))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f971,f52])).
% 0.19/0.28 thf(f1100,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X3))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X1))) | ($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK18 @ X4)))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f983,f52])).
% 0.19/0.28 thf(f1143,plain,(
% 0.19/0.28 ($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((sK1 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((sK2 @ sK16)))),
% 0.19/0.28 inference(forward_demodulation,[],[f1080,f52])).
% 0.19/0.28 thf(f1149,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($false = ((sK1 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X5))) | ($false = ((sK1 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ X5 @ X3)))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f1086,f52])).
% 0.19/0.28 thf(f1150,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X4 : $i,X5 : $i] : (($false = ((sK1 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X5))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($true = ((sK2 @ X3))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ X5 @ X3)))) )),
% 0.19/0.28 inference(duplicate_literal_removal,[],[f1149])).
% 0.19/0.28 thf(f1160,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X5))) | ($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ X5 @ X1)))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f1096,f52])).
% 0.19/0.28 thf(f1161,plain,(
% 0.19/0.28 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X5))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ X5 @ X1)))) )),
% 0.19/0.28 inference(duplicate_literal_removal,[],[f1160])).
% 0.19/0.28 thf(f1162,plain,(
% 0.19/0.28 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X4))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X3))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X1))) | ($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X2))) | ($true = ((sK1 @ X4)))) )),
% 0.19/0.28 inference(forward_demodulation,[],[f1100,f52])).
% 0.19/0.28 thf(f1189,plain,(
% 0.19/0.28 ($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((sK1 @ (d2unsorted @ d_unsorted_0))))),
% 0.19/0.28 inference(forward_demodulation,[],[f1143,f52])).
% 0.19/0.28 thf(f1190,plain,(
% 0.19/0.28 ($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | ($false = ((sK1 @ (d2unsorted @ d_unsorted_0))))),
% 0.19/0.28 inference(duplicate_literal_removal,[],[f1189])).
% 0.19/0.28 thf(f1196,definition,(
% 0.19/0.28 spl25_2 <=> ! [X5 : $i,X3 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X5))) | ($false = ((irel @ X5 @ X3))) | ($true = ((sK2 @ X3))))),
% 0.19/0.28 introduced(definition,[new_symbols(definition,[spl25_2])],[avatar_definition])).
% 0.19/0.28 thf(f1197,plain,(
% 0.19/0.28 ( ! [X3 : $i,X5 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X5))) | ($false = ((irel @ X5 @ X3))) | ($true = ((sK2 @ X3)))) ) | ~spl25_2),
% 0.19/0.28 inference(avatar_component_clause,[],[f1196])).
% 0.19/0.28 thf(f1199,definition,(
% 0.19/0.28 spl25_3 <=> ($false = ((sK1 @ (d2unsorted @ d_unsorted_0))))),
% 0.19/0.28 introduced(definition,[new_symbols(definition,[spl25_3])],[avatar_definition])).
% 0.19/0.28 thf(f1201,plain,(
% 0.19/0.28 ($false = ((sK1 @ (d2unsorted @ d_unsorted_0)))) | ~spl25_3),
% 0.19/0.28 inference(avatar_component_clause,[],[f1199])).
% 0.19/0.28 thf(f1208,definition,(
% 0.19/0.28 spl25_5 <=> ! [X5 : $i,X1 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X5))) | ($false = ((irel @ X5 @ X1))) | ($true = ((sK1 @ X1))))),
% 0.19/0.28 introduced(definition,[new_symbols(definition,[spl25_5])],[avatar_definition])).
% 0.19/0.28 thf(f1209,plain,(
% 0.19/0.28 ( ! [X1 : $i,X5 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X5))) | ($false = ((irel @ X5 @ X1))) | ($true = ((sK1 @ X1)))) ) | ~spl25_5),
% 0.19/0.28 inference(avatar_component_clause,[],[f1208])).
% 0.19/0.28 thf(f1211,definition,(
% 0.19/0.28 spl25_6 <=> ($false = ((sK2 @ (d2unsorted @ d_unsorted_0))))),
% 0.19/0.28 introduced(definition,[new_symbols(definition,[spl25_6])],[avatar_definition])).
% 0.19/0.28 thf(f1213,plain,(
% 0.19/0.28 ($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | ~spl25_6),
% 0.19/0.28 inference(avatar_component_clause,[],[f1211])).
% 0.19/0.28 thf(f1216,plain,(
% 0.19/0.28 spl25_2 | spl25_2 | spl25_3),
% 0.19/0.28 inference(avatar_split_clause,[],[f1150,f1199,f1196,f1196])).
% 0.19/0.28 thf(f1226,plain,(
% 0.19/0.28 spl25_5 | spl25_5 | spl25_6),
% 0.19/0.28 inference(avatar_split_clause,[],[f1161,f1211,f1208,f1208])).
% 0.19/0.28 thf(f1228,definition,(
% 0.19/0.28 spl25_7 <=> ! [X1 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X1))) | ($true = ((sK2 @ X1))))),
% 0.19/0.28 introduced(definition,[new_symbols(definition,[spl25_7])],[avatar_definition])).
% 0.19/0.28 thf(f1229,plain,(
% 0.19/0.28 ( ! [X1 : $i] : (($true = ((sK2 @ X1))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X1)))) ) | ~spl25_7),
% 0.19/0.28 inference(avatar_component_clause,[],[f1228])).
% 0.19/0.28 thf(f1231,definition,(
% 0.19/0.28 spl25_8 <=> ! [X2 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2))) | ($true = ((sK1 @ X2))))),
% 0.19/0.28 introduced(definition,[new_symbols(definition,[spl25_8])],[avatar_definition])).
% 0.19/0.28 thf(f1232,plain,(
% 0.19/0.28 ( ! [X2 : $i] : (($true = ((sK1 @ X2))) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X2)))) ) | ~spl25_8),
% 0.19/0.28 inference(avatar_component_clause,[],[f1231])).
% 0.19/0.28 thf(f1233,plain,(
% 0.19/0.28 spl25_7 | spl25_8 | spl25_7 | spl25_8),
% 0.19/0.28 inference(avatar_split_clause,[],[f1162,f1231,f1228,f1231,f1228])).
% 0.19/0.28 thf(f1252,plain,(
% 0.19/0.28 spl25_3 | spl25_6),
% 0.19/0.28 inference(avatar_split_clause,[],[f1190,f1211,f1199])).
% 0.19/0.28 thf(f1260,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($false = ((sK1 @ X0)))) ) | ~spl25_3),
% 0.19/0.28 inference(constrained_superposition,[],[f1201,f59])).
% 0.19/0.28 thf(f1278,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0))) | ($true = ((sK1 @ X0)))) ) | ~spl25_5),
% 0.19/0.28 inference(constrained_superposition,[],[f113,f1209])).
% 0.19/0.28 thf(f1283,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0))) | ($true = ((sK1 @ X0)))) ) | ~spl25_5),
% 0.19/0.28 inference(trivial_inequality_removal,[],[f1278])).
% 0.19/0.28 thf(f1289,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0)))) ) | (~spl25_3 | ~spl25_5)),
% 0.19/0.28 inference(forward_demodulation,[],[f1283,f1260])).
% 0.19/0.28 thf(f1290,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0)))) ) | (~spl25_3 | ~spl25_5)),
% 0.19/0.28 inference(trivial_inequality_removal,[],[f1289])).
% 0.19/0.28 thf(f1318,plain,(
% 0.19/0.28 ($true = $false) | (~spl25_3 | ~spl25_5)),
% 0.19/0.28 inference(constrained_superposition,[],[f1290,f32])).
% 0.19/0.28 thf(f1328,plain,(
% 0.19/0.28 $false | (~spl25_3 | ~spl25_5)),
% 0.19/0.28 inference(trivial_inequality_removal,[],[f1318])).
% 0.19/0.28 thf(f1329,plain,(
% 0.19/0.28 ~spl25_3 | ~spl25_5),
% 0.19/0.28 inference(avatar_contradiction_clause,[],[f1328])).
% 0.19/0.28 thf(f1350,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($false = ((sK2 @ X0)))) ) | ~spl25_6),
% 0.19/0.28 inference(constrained_superposition,[],[f1213,f59])).
% 0.19/0.28 thf(f1368,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0))) | ($true = ((sK2 @ X0)))) ) | ~spl25_2),
% 0.19/0.28 inference(constrained_superposition,[],[f113,f1197])).
% 0.19/0.28 thf(f1373,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0))) | ($true = ((sK2 @ X0)))) ) | ~spl25_2),
% 0.19/0.28 inference(trivial_inequality_removal,[],[f1368])).
% 0.19/0.28 thf(f1398,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0)))) ) | (~spl25_6 | ~spl25_7)),
% 0.19/0.28 inference(constrained_superposition,[],[f1350,f1229])).
% 0.19/0.28 thf(f1399,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0)))) ) | (~spl25_6 | ~spl25_7)),
% 0.19/0.28 inference(trivial_inequality_removal,[],[f1398])).
% 0.19/0.28 thf(f1460,plain,(
% 0.19/0.28 ($true = $false) | (~spl25_6 | ~spl25_7)),
% 0.19/0.28 inference(constrained_superposition,[],[f113,f1399])).
% 0.19/0.28 thf(f1461,plain,(
% 0.19/0.28 $false | (~spl25_6 | ~spl25_7)),
% 0.19/0.28 inference(trivial_inequality_removal,[],[f1460])).
% 0.19/0.28 thf(f1462,plain,(
% 0.19/0.28 ~spl25_6 | ~spl25_7),
% 0.19/0.28 inference(avatar_contradiction_clause,[],[f1461])).
% 0.19/0.28 thf(f1470,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0)))) ) | (~spl25_2 | ~spl25_6)),
% 0.19/0.28 inference(forward_demodulation,[],[f1373,f1350])).
% 0.19/0.28 thf(f1471,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0)))) ) | (~spl25_2 | ~spl25_6)),
% 0.19/0.28 inference(trivial_inequality_removal,[],[f1470])).
% 0.19/0.28 thf(f1521,plain,(
% 0.19/0.28 ($true = $false) | (~spl25_2 | ~spl25_6)),
% 0.19/0.28 inference(constrained_superposition,[],[f113,f1471])).
% 0.19/0.28 thf(f1522,plain,(
% 0.19/0.28 $false | (~spl25_2 | ~spl25_6)),
% 0.19/0.28 inference(trivial_inequality_removal,[],[f1521])).
% 0.19/0.28 thf(f1523,plain,(
% 0.19/0.28 ~spl25_2 | ~spl25_6),
% 0.19/0.28 inference(avatar_contradiction_clause,[],[f1522])).
% 0.19/0.28 thf(f1638,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0)))) ) | (~spl25_3 | ~spl25_8)),
% 0.19/0.28 inference(constrained_superposition,[],[f1260,f1232])).
% 0.19/0.28 thf(f1639,plain,(
% 0.19/0.28 ( ! [X0 : $i] : (($false = ((irel @ (d2unsorted @ d_unsorted_0) @ X0)))) ) | (~spl25_3 | ~spl25_8)),
% 0.19/0.28 inference(trivial_inequality_removal,[],[f1638])).
% 0.19/0.28 thf(f1718,plain,(
% 0.19/0.28 ($true = $false) | (~spl25_3 | ~spl25_8)),
% 0.19/0.28 inference(constrained_superposition,[],[f1639,f32])).
% 0.19/0.28 thf(f1734,plain,(
% 0.19/0.28 $false | (~spl25_3 | ~spl25_8)),
% 0.19/0.28 inference(trivial_inequality_removal,[],[f1718])).
% 0.19/0.28 thf(f1735,plain,(
% 0.19/0.28 ~spl25_3 | ~spl25_8),
% 0.19/0.28 inference(avatar_contradiction_clause,[],[f1734])).
% 0.19/0.28 cnf(s7, plain, spl25_2 | spl25_2 | spl25_3, inference(sat_conversion,[],[f1216])).
% 0.19/0.28 cnf(s8, plain, spl25_2 | spl25_3, inference(rat,[],[s7])).
% 0.19/0.28 cnf(s19, plain, spl25_5 | spl25_5 | spl25_6, inference(sat_conversion,[],[f1226])).
% 0.19/0.28 cnf(s20, plain, spl25_5 | spl25_6, inference(rat,[],[s19])).
% 0.19/0.28 cnf(s21, plain, spl25_7 | spl25_8 | spl25_7 | spl25_8, inference(sat_conversion,[],[f1233])).
% 0.19/0.28 cnf(s22, plain, spl25_7 | spl25_8, inference(rat,[],[s21])).
% 0.19/0.28 cnf(s43, plain, spl25_3 | spl25_6, inference(sat_conversion,[],[f1252])).
% 0.19/0.28 cnf(s47, plain, ~spl25_3 | ~spl25_5, inference(sat_conversion,[],[f1329])).
% 0.19/0.28 cnf(s48, plain, ~spl25_6 | ~spl25_7, inference(sat_conversion,[],[f1462])).
% 0.19/0.28 cnf(s52, plain, ~spl25_2 | ~spl25_6, inference(sat_conversion,[],[f1523])).
% 0.19/0.28 cnf(s59, plain, ~spl25_3 | ~spl25_8, inference(sat_conversion,[],[f1735])).
% 0.19/0.28 cnf(s60, plain, ~spl25_3, inference(rat,[],[s48,s20,s22,s47,s59])).
% 0.19/0.28 cnf(s61, plain, spl25_6, inference(rat,[],[s43,s60])).
% 0.19/0.28 cnf(s63, plain, spl25_2, inference(rat,[],[s8,s60])).
% 0.19/0.28 cnf(s65, plain, $false, inference(rat,[],[s52,s61,s63])).
% 0.19/0.28 thf(f1737,plain,(
% 0.19/0.28 $false),
% 0.19/0.28 inference(avatar_sat_refutation,[],[s65])).
% 0.19/0.28 % SZS output end Proof for theBenchmark
% 0.19/0.28 % (1488098)------------------------------
% 0.19/0.28 % (1488098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.28 % (1488098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.28 % (1488098)CaDiCaL version: 2.1.3
% 0.19/0.28 % (1488098)Termination reason: Refutation
% 0.19/0.28 % (1488098)Time elapsed: 0.034 s
% 0.19/0.28 % (1488098)Peak memory usage: 13 MB
% 0.19/0.28 % (1488098)Instructions burned: 139 (million)
% 0.19/0.28 % (1488088)Success in time 0.05 s
% 0.19/0.28 % Vampire exiting
%------------------------------------------------------------------------------