Vampire-SAT---5.0.1.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : SWX178^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 : n015.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.65s 0.42s
% Output   : Refutation 0.65s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWX178^1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21  % Computer : n015.cluster.edu
% 0.09/0.21  % Model    : x86_64 x86_64
% 0.09/0.21  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21  % Memory   : 8046.5625MB
% 0.09/0.21  % OS       : Linux 6.8.0-71-generic
% 0.09/0.21  % CPULimit : 300
% 0.09/0.21  % WCLimit  : 300
% 0.09/0.21  % DateTime : Tue Sep 29 16:13:34 UTC 2026
% 0.09/0.21  % CPUTime  : 
% 0.09/0.21  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24  Running first-order model finding
% 0.09/0.24  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.65/0.42  % (3716975)Will run a generic schedule for satisfiability detection.
% 0.65/0.42  % (3716981)% WARNING: option uhcvi not known.
% 0.65/0.42  % (3716982)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3173812588:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.65/0.42  % (3716981)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=951267877:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.65/0.42  % (3716981)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.65/0.42  % (3716981)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.65/0.42  % (3716983)dis+10_1_sil=32000:sp=arity:random_seed=662708890:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.65/0.42  % (3716986)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2382373969:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.65/0.42  % (3716980)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4046539128_2999 on theBenchmark for (2999ds/0Mi)
% 0.65/0.42  % (3716984)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2927048591:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.65/0.42  % (3716985)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=553534899:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.65/0.42  % (3716984)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.65/0.42  % Exception at run slice level
% 0.65/0.42  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.65/0.42  % (3716983)Instruction limit reached! 
% 0.65/0.42  % (3716983)------------------------------
% 0.65/0.42  % (3716983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.65/0.42  % (3716983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.42  % (3716983)CaDiCaL version: 2.1.3
% 0.65/0.42  % (3716983)Termination reason: Instruction limit
% 0.65/0.42  % (3716983)Termination phase: Saturation
% 0.65/0.42  % (3716983)Time elapsed: 0.034 s
% 0.65/0.42  % (3716983)Peak memory usage: 12 MB
% 0.65/0.42  % (3716983)Instructions burned: 104 (million)
% 0.65/0.42  % (3716994)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2038947362:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.65/0.42  % Exception at run slice level
% 0.65/0.42  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.65/0.42  % (3716997)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2808062543:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.65/0.42  % (3716997)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.65/0.42  % (3716997)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.65/0.42  % (3716995)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1380045267:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.65/0.42  % (3716985)Instruction limit reached! 
% 0.65/0.42  % (3716985)------------------------------
% 0.65/0.42  % (3716985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.65/0.42  % (3716985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.42  % (3716985)CaDiCaL version: 2.1.3
% 0.65/0.42  % (3716985)Termination reason: Instruction limit
% 0.65/0.42  % (3716985)Termination phase: Saturation
% 0.65/0.42  % (3716985)Time elapsed: 0.055 s
% 0.65/0.42  % (3716985)Peak memory usage: 12 MB
% 0.65/0.42  % (3716985)Instructions burned: 133 (million)
% 0.65/0.42  % (3716986) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3716975-3716986"...
% 0.65/0.42  % (3716997) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3716975-3716997"...
% 0.65/0.42  % (3717000)ott-21_1_sil=16000:fs=off:random_seed=3150203013:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.65/0.42  % (3716997)...printing done.
% 0.65/0.42  % (3716997)Refutation found. Thanks to Tanya!
% 0.65/0.42  % SZS status Theorem for theBenchmark
% 0.65/0.42  % SZS output start Proof for theBenchmark
% 0.65/0.42  thf(type_def_5, type, unsorted: $tType).
% 0.65/0.42  thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.65/0.42  thf(type_def_7, type, d_unsorted: $tType).
% 0.65/0.42  thf(func_def_0, type, irel: ($i > $i > $o)).
% 0.65/0.42  thf(func_def_1, type, mnot: (($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_2, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_3, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_4, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_5, type, mbox_s4: (($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_6, type, iatom: (($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_7, type, inot: (($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_8, type, itrue: ($i > $o)).
% 0.65/0.42  thf(func_def_9, type, ifalse: ($i > $o)).
% 0.65/0.42  thf(func_def_10, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_11, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_12, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_13, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_14, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_15, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.65/0.42  thf(func_def_16, type, ivalid: (($i > $o) > $o)).
% 0.65/0.42  thf(func_def_17, type, isatisfiable: (($i > $o) > $o)).
% 0.65/0.42  thf(func_def_18, type, icountersatisfiable: (($i > $o) > $o)).
% 0.65/0.42  thf(func_def_19, type, iinvalid: (($i > $o) > $o)).
% 0.65/0.42  thf(func_def_20, type, d2unsorted: (d_unsorted > $i)).
% 0.65/0.42  thf(func_def_21, type, d_unsorted_0: d_unsorted).
% 0.65/0.42  thf(func_def_23, type, vNOT: ($o > $o)).
% 0.65/0.42  thf(func_def_24, type, db1: !>[X0: $tType]:(X0)).
% 0.65/0.42  thf(func_def_25, type, db0: !>[X0: $tType]:(X0)).
% 0.65/0.42  thf(func_def_26, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.65/0.42  thf(func_def_27, type, vOR: ($o > $o > $o)).
% 0.65/0.42  thf(func_def_28, type, db2: !>[X0: $tType]:(X0)).
% 0.65/0.42  thf(func_def_29, type, vAND: ($o > $o > $o)).
% 0.65/0.42  thf(func_def_30, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.65/0.42  thf(func_def_31, type, db3: !>[X0: $tType]:(X0)).
% 0.65/0.42  thf(func_def_32, type, db5: !>[X0: $tType]:(X0)).
% 0.65/0.42  thf(func_def_33, type, db4: !>[X0: $tType]:(X0)).
% 0.65/0.42  thf(func_def_34, type, db8: !>[X0: $tType]:(X0)).
% 0.65/0.42  thf(func_def_35, type, db6: !>[X0: $tType]:(X0)).
% 0.65/0.42  thf(func_def_36, type, db7: !>[X0: $tType]:(X0)).
% 0.65/0.42  thf(func_def_39, type, sK0: ($i > d_unsorted)).
% 0.65/0.42  thf(func_def_40, type, sK1: ($i > $o)).
% 0.65/0.42  thf(func_def_41, type, sK2: ($i > $o)).
% 0.65/0.42  thf(func_def_55, type, sK16: ($i > $i)).
% 0.65/0.42  thf(func_def_56, type, sK17: ($i > $i)).
% 0.65/0.42  thf(func_def_57, type, sK18: ($i > $i)).
% 0.65/0.42  thf(func_def_58, type, sK19: ($i > $i)).
% 0.65/0.42  thf(func_def_59, type, sK20: ($i > $i)).
% 0.65/0.42  thf(func_def_60, type, sK21: ($i > $i)).
% 0.65/0.42  thf(func_def_61, type, sK22: ($i > $i)).
% 0.65/0.42  thf(func_def_62, type, sK23: ($i > $i)).
% 0.65/0.42  thf(func_def_63, type, sK24: ($i > $i)).
% 0.65/0.42  thf(func_def_64, type, sK25: ($i > $i)).
% 0.65/0.42  thf(func_def_65, type, sK26: ($i > $i)).
% 0.65/0.42  thf(func_def_66, type, sK27: ($i > $i)).
% 0.65/0.42  thf(f1,axiom,(
% 0.65/0.42    ~(ifalse @ (d2unsorted @ d_unsorted_0)) & (itrue @ (d2unsorted @ d_unsorted_0)) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) & (iinvalid = (^[X18 : ($i > $o)] : (! [X19 : $i] : ~(X18 @ X19)))) & (icountersatisfiable = (^[X18 : ($i > $o)] : (~ ! [X19 : $i] : (X18 @ X19)))) & (isatisfiable = (^[X18 : ($i > $o)] : (~ ! [X19 : $i] : ~(X18 @ X19)))) & (ivalid = (^[X18 : ($i > $o)] : (! [X19 : $i] : (X18 @ X19)))) & (ixor = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (~ ! [X5 : $i,X14 : $i,X15 : $i,X16 : $i,X17 : $i] : ((((X8 @ X17) | ~(irel @ X16 @ X17) | ~ ! [X13 : $i] : ((X9 @ X13) | ~(irel @ X16 @ X13)) | ~(irel @ X5 @ X16)) & ((X9 @ X15) | ~(irel @ X14 @ X15) | ~ ! [X11 : $i] : ((X8 @ X11) | ~(irel @ X14 @ X11)) | ~(irel @ X5 @ X14))) | ~(irel @ X7 @ X5))))) & (iequiv = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i,X12 : $i] : ((X8 @ X12) | ~(irel @ X5 @ X12) | ~ ! [X13 : $i] : ((X9 @ X13) | ~(irel @ X5 @ X13)) | ~(irel @ X7 @ X5)) & ! [X5 : $i,X10 : $i] : ((X9 @ X10) | ~(irel @ X5 @ X10) | ~ ! [X11 : $i] : ((X8 @ X11) | ~(irel @ X5 @ X11)) | ~(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] : (! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) & ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5))))) & (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.65/0.42    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lcl696_1)).
% 0.65/0.42  thf(f2,conjecture,(
% 0.65/0.42    (iequiv = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((iand @ (iimplies @ X0 @ X1) @ (iimplies @ X1 @ X0)))))),
% 0.65/0.42    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iequiv)).
% 0.65/0.42  thf(f3,negated_conjecture,(
% 0.65/0.42    ~ (iequiv = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((iand @ (iimplies @ X0 @ X1) @ (iimplies @ X1 @ X0)))))),
% 0.65/0.42    inference(negated_conjecture,[status(cth)],[f2])).
% 0.65/0.42  thf(f4,plain,(
% 0.65/0.42    ~(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,X14 : $i,X15 : $i] : ((((X8 @ X15) | ~(irel @ X14 @ X15) | ~ ! [X16 : $i] : ((X9 @ X16) | ~(irel @ X14 @ X16)) | ~(irel @ X11 @ X14)) & ((X9 @ X13) | ~(irel @ X12 @ X13) | ~ ! [X17 : $i] : ((X8 @ X17) | ~(irel @ X12 @ X17)) | ~(irel @ X11 @ X12))) | ~(irel @ X10 @ X11))))) & (iequiv = (^[X18 : ($i > $o), X19 : ($i > $o), X20 : $i] : (! [X21 : $i,X22 : $i] : ((X18 @ X22) | ~(irel @ X21 @ X22) | ~ ! [X23 : $i] : ((X19 @ X23) | ~(irel @ X21 @ X23)) | ~(irel @ X20 @ X21)) & ! [X24 : $i,X25 : $i] : ((X19 @ X25) | ~(irel @ X24 @ X25) | ~ ! [X26 : $i] : ((X18 @ X26) | ~(irel @ X24 @ X26)) | ~(irel @ X20 @ X24))))) & (iimplied = (^[X27 : ($i > $o), X28 : ($i > $o), X29 : $i] : (! [X30 : $i] : ((X27 @ X30) | ~(irel @ X29 @ X30)) | ~ ! [X31 : $i] : ((X28 @ X31) | ~(irel @ X29 @ X31))))) & (iimplies = (^[X32 : ($i > $o), X33 : ($i > $o), X34 : $i] : (! [X35 : $i] : ((X33 @ X35) | ~(irel @ X34 @ X35)) | ~ ! [X36 : $i] : ((X32 @ X36) | ~(irel @ X34 @ X36))))) & (ior = (^[X37 : ($i > $o), X38 : ($i > $o), X39 : $i] : (! [X40 : $i] : ((X38 @ X40) | ~(irel @ X39 @ X40)) | ! [X41 : $i] : ((X37 @ X41) | ~(irel @ X39 @ X41))))) & (iand = (^[X42 : ($i > $o), X43 : ($i > $o), X44 : $i] : (! [X45 : $i] : ((X43 @ X45) | ~(irel @ X44 @ X45)) & ! [X46 : $i] : ((X42 @ X46) | ~(irel @ X44 @ X46))))) & (inot = (^[X47 : ($i > $o), X48 : $i] : (~ ! [X49 : $i] : ((X47 @ X49) | ~(irel @ X48 @ X49))))) & (iatom = (^[X50 : ($i > $o), X51 : $i] : ((X50 @ X51)))) & (mbox_s4 = (^[X52 : ($i > $o), X53 : $i] : (! [X54 : $i] : ((X52 @ X54) | ~(irel @ X53 @ X54))))) & (mimplies = (^[X55 : ($i > $o), X56 : ($i > $o), X57 : $i] : ((X56 @ X57) | ~(X55 @ X57)))) & (mand = (^[X58 : ($i > $o), X59 : ($i > $o), X60 : $i] : ((X59 @ X60) & (X58 @ X60)))) & (mor = (^[X61 : ($i > $o), X62 : ($i > $o), X63 : $i] : ((X62 @ X63) | (X61 @ X63)))) & (mnot = (^[X64 : ($i > $o), X65 : $i] : (~(X64 @ X65)))) & ! [X66 : d_unsorted,X67 : d_unsorted] : ((((d2unsorted @ X66)) = ((d2unsorted @ X67))) => (X66 = X67)) & ! [X68 : d_unsorted] : (d_unsorted_0 = X68) & ! [X69 : $i] : ? [X70 : d_unsorted] : (((d2unsorted @ X70)) = X69)),
% 0.65/0.42    inference(rectify,[],[f1])).
% 0.65/0.42  thf(f5,plain,(
% 0.65/0.42    ~ (((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]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y2 @ Y7)) | (((((~ (irel @ Y7 @ Y6)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8)))))) | (~ (irel @ Y6 @ Y5))) | (Y1 @ Y5)) & ((((~ (irel @ Y7 @ Y4)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y1 @ Y8)))))) | (~ (irel @ Y4 @ Y3))) | (Y0 @ Y3))))))))))))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y1 @ Y5)))))) | (~ (irel @ Y4 @ 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]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (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)))))) & ! [X66 : d_unsorted,X67 : d_unsorted] : ((((d2unsorted @ X66)) = ((d2unsorted @ X67))) => (X66 = X67)) & ! [X68 : d_unsorted] : (d_unsorted_0 = X68) & ! [X69 : $i] : ? [X70 : d_unsorted] : (((d2unsorted @ X70)) = X69)),
% 0.65/0.42    inference(fool_elimination,[],[f4])).
% 0.65/0.42  thf(f6,plain,(
% 0.65/0.42    ~ (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (iand @ (iimplies @ Y0 @ Y1) @ (iimplies @ Y1 @ Y0))))))),
% 0.65/0.42    inference(fool_elimination,[],[f3])).
% 0.65/0.42  thf(f7,plain,(
% 0.65/0.42    ~ (((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]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y2 @ Y7)) | (((((~ (irel @ Y7 @ Y6)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8)))))) | (~ (irel @ Y6 @ Y5))) | (Y1 @ Y5)) & ((((~ (irel @ Y7 @ Y4)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y1 @ Y8)))))) | (~ (irel @ Y4 @ Y3))) | (Y0 @ Y3))))))))))))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y1 @ Y5)))))) | (~ (irel @ Y4 @ 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]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (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.65/0.42    inference(rectify,[],[f5])).
% 0.65/0.42  thf(f8,plain,(
% 0.65/0.42    (((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]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y2 @ Y7)) | (((((~ (irel @ Y7 @ Y6)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8)))))) | (~ (irel @ Y6 @ Y5))) | (Y1 @ Y5)) & ((((~ (irel @ Y7 @ Y4)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y1 @ Y8)))))) | (~ (irel @ Y4 @ Y3))) | (Y0 @ Y3))))))))))))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y1 @ Y5)))))) | (~ (irel @ Y4 @ 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]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (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.65/0.42    inference(flattening,[],[f7])).
% 0.65/0.42  thf(f9,plain,(
% 0.65/0.42    (iequiv != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (iand @ (iimplies @ Y0 @ Y1) @ (iimplies @ Y1 @ Y0))))))),
% 0.65/0.42    inference(flattening,[],[f6])).
% 0.65/0.42  thf(f10,plain,(
% 0.65/0.42    (((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]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y2 @ Y7)) | (((((~ (irel @ Y7 @ Y6)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8)))))) | (~ (irel @ Y6 @ Y5))) | (Y1 @ Y5)) & ((((~ (irel @ Y7 @ Y4)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y1 @ Y8)))))) | (~ (irel @ Y4 @ Y3))) | (Y0 @ Y3))))))))))))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y1 @ Y5)))))) | (~ (irel @ Y4 @ 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]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (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.65/0.42    inference(ennf_transformation,[],[f8])).
% 0.65/0.42  thf(f11,plain,(
% 0.65/0.42    (((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]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y2 @ Y7)) | (((((~ (irel @ Y7 @ Y6)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8)))))) | (~ (irel @ Y6 @ Y5))) | (Y1 @ Y5)) & ((((~ (irel @ Y7 @ Y4)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y1 @ Y8)))))) | (~ (irel @ Y4 @ Y3))) | (Y0 @ Y3))))))))))))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y1 @ Y5)))))) | (~ (irel @ Y4 @ 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]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (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.65/0.42    inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X4,sK0 @ X3)],[f10])).
% 0.65/0.42  thf(f12,plain,(
% 0.65/0.42    ( ! [X3 : $i] : ((((d2unsorted @ (sK0 @ X3))) = X3)) )),
% 0.65/0.42    inference(cnf_transformation,[],[f11])).
% 0.65/0.42  thf(f13,plain,(
% 0.65/0.42    ( ! [X2 : d_unsorted] : ((d_unsorted_0 = X2)) )),
% 0.65/0.42    inference(cnf_transformation,[],[f11])).
% 0.65/0.42  thf(f22,plain,(
% 0.65/0.42    (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))),
% 0.65/0.42    inference(cnf_transformation,[],[f11])).
% 0.65/0.42  thf(f24,plain,(
% 0.65/0.42    (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)))))))))))),
% 0.65/0.42    inference(cnf_transformation,[],[f11])).
% 0.65/0.42  thf(f26,plain,(
% 0.65/0.42    (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y1 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y0 @ Y3)))))))))))))),
% 0.65/0.42    inference(cnf_transformation,[],[f11])).
% 0.65/0.42  thf(f32,plain,(
% 0.65/0.42    (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true)),
% 0.65/0.42    inference(cnf_transformation,[],[f11])).
% 0.65/0.42  thf(f35,plain,(
% 0.65/0.42    (iequiv != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (iand @ (iimplies @ Y0 @ Y1) @ (iimplies @ Y1 @ Y0))))))),
% 0.65/0.42    inference(cnf_transformation,[],[f9])).
% 0.65/0.42  thf(f38,plain,(
% 0.65/0.42    ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y1 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y0 @ Y3)))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y2 @ Y5)))) & (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y3 @ Y5)))))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y2 @ Y5))))) | (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y3 @ Y5)))))))))) @ Y0 @ Y1) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y2 @ Y5))))) | (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y3 @ Y5)))))))))) @ Y1 @ Y0))))))),
% 0.65/0.42    inference(definition_unfolding,[],[f35,f26,f22,f24,f24])).
% 0.65/0.42  thf(f39,plain,(
% 0.65/0.42    ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y1 @ Y5)))))) | (~ (irel @ Y4 @ 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 @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | ((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y1 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4)))))))))))))))),
% 0.65/0.42    inference(beta-eta_normalization,[],[f38])).
% 0.65/0.42  thf(f47,plain,(
% 0.65/0.42    ( ! [X0 : d_unsorted,X1 : d_unsorted] : ((X0 = X1)) )),
% 0.65/0.42    inference(constrained_superposition,[],[f13,f13])).
% 0.65/0.42  thf(f48,plain,(
% 0.65/0.42    ( ! [X0 : d_unsorted,X1 : $i] : ((((d2unsorted @ X0)) = X1)) )),
% 0.65/0.42    inference(constrained_superposition,[],[f12,f47])).
% 0.65/0.42  thf(f50,plain,(
% 0.65/0.42    ( ! [X2 : $i,X0 : $i] : ((X0 = X2)) )),
% 0.65/0.42    inference(constrained_superposition,[],[f48,f48])).
% 0.65/0.42  thf(f69,plain,(
% 0.65/0.42    ( ! [X0 : $i] : (($true = ((irel @ X0 @ X0)))) )),
% 0.65/0.42    inference(constrained_superposition,[],[f32,f50])).
% 0.65/0.42  thf(f71,plain,(
% 0.65/0.42    ((((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y1 @ Y5)))))) | (~ (irel @ Y4 @ 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 @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | ((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y1 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4)))))))))))))) @ sK1)))),
% 0.65/0.42    inference(negative_extensionality,[],[f39])).
% 0.65/0.42  thf(f72,plain,(
% 0.65/0.42    ((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK1 @ Y4)))))) | (~ (irel @ Y3 @ Y2))) | (Y0 @ Y2)))))) & (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4)))))) | (~ (irel @ Y3 @ 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 @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3)))))))))))))),
% 0.65/0.42    inference(beta-eta_normalization,[],[f71])).
% 0.65/0.42  thf(f73,plain,(
% 0.65/0.42    ((((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK1 @ Y4)))))) | (~ (irel @ Y3 @ Y2))) | (Y0 @ Y2)))))) & (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4)))))) | (~ (irel @ Y3 @ 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 @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3)))))))))))) @ sK2)))),
% 0.65/0.42    inference(negative_extensionality,[],[f72])).
% 0.65/0.42  thf(f74,plain,(
% 0.65/0.42    ((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ 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 @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))))))))),
% 0.65/0.42    inference(beta-eta_normalization,[],[f73])).
% 0.65/0.42  thf(f75,plain,(
% 0.65/0.42    ((((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ 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 @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))))))) @ sK3)))),
% 0.65/0.42    inference(negative_extensionality,[],[f74])).
% 0.65/0.42  thf(f76,plain,(
% 0.65/0.42    ($true = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ 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 @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))))))) @ sK3)))),
% 0.65/0.42    inference(xor_proxy_clausification,[],[f75])).
% 0.65/0.42  thf(f77,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ 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 @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))))))) @ sK3)))),
% 0.65/0.42    inference(xor_proxy_clausification,[],[f75])).
% 0.65/0.42  thf(f78,plain,(
% 0.65/0.42    ($false = (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)))))) & (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ 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 @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))))))))),
% 0.65/0.42    inference(beta-eta_normalization,[],[f77])).
% 0.65/0.42  thf(f79,plain,(
% 0.65/0.42    ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ 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 @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(and_proxy_clausification,[],[f78])).
% 0.65/0.42  thf(f80,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK1 @ Y0))))) @ sK4))) | ($false = (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))))) & (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f79])).
% 0.65/0.42  thf(f81,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK1 @ Y0))))) @ sK4))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))))))))),
% 0.65/0.42    inference(and_proxy_clausification,[],[f80])).
% 0.65/0.42  thf(f82,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK1 @ Y0))))) @ sK4))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))) @ sK5))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))))))))),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f81])).
% 0.65/0.42  thf(f83,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK1 @ Y0))))) @ sK4))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))) @ sK5))) | ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))) @ sK6))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))))))))),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f82])).
% 0.65/0.42  thf(f84,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK1 @ Y0))))) @ sK4))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))) @ sK5))) | ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))) @ sK6))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))))) @ sK7)))),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f83])).
% 0.65/0.42  thf(f85,plain,(
% 0.65/0.42    ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4)))))) | ($false = (((~ (irel @ sK3 @ sK5)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0)))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6)))))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(beta-eta_normalization,[],[f84])).
% 0.65/0.42  thf(f86,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($false = (((~ (irel @ sK3 @ sK5)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0)))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6)))))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f85])).
% 0.65/0.42  thf(f87,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6)))))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f86])).
% 0.65/0.42  thf(f88,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($false = ((~ (irel @ sK3 @ sK5)))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6)))))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f86])).
% 0.65/0.42  thf(f89,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = ((irel @ sK3 @ sK5))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6)))))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(not_proxy_clausification,[],[f88])).
% 0.65/0.42  thf(f90,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK9))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f89])).
% 0.65/0.42  thf(f91,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK9))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0)))))))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f90])).
% 0.65/0.42  thf(f169,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK9))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0)))))))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f91])).
% 0.65/0.42  thf(f170,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK9))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))))),
% 0.65/0.42    inference(not_proxy_clausification,[],[f169])).
% 0.65/0.42  thf(f171,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK9))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))) @ X1)))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f170])).
% 0.65/0.42  thf(f172,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = (((((~ (irel @ sK3 @ sK8)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK8 @ sK4))) | (sK1 @ sK4)))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(beta-eta_normalization,[],[f171])).
% 0.65/0.42  thf(f173,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f172])).
% 0.65/0.42  thf(f174,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((((~ (irel @ sK3 @ sK8)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK8 @ sK4))))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f172])).
% 0.65/0.42  thf(f175,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((~ (irel @ sK8 @ sK4)))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f174])).
% 0.65/0.42  thf(f176,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = (((~ (irel @ sK3 @ sK8)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0)))))))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f174])).
% 0.65/0.42  thf(f177,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))))))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f176])).
% 0.65/0.42  thf(f201,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0)))))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f177])).
% 0.65/0.42  thf(f202,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f201])).
% 0.65/0.42  thf(f204,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($false = ((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f202])).
% 0.65/0.42  thf(f205,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($false = ((~ (irel @ sK9 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f204])).
% 0.65/0.42  thf(f206,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f204])).
% 0.65/0.42  thf(f207,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f206])).
% 0.65/0.42  thf(f215,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f207])).
% 0.65/0.42  thf(f216,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))) @ X3))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f215])).
% 0.65/0.42  thf(f217,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))) @ X3))) | ($true = ((sK1 @ X1))) | ($true = ((~ (irel @ sK7 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f216])).
% 0.65/0.42  thf(f218,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))) @ X3))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f217])).
% 0.65/0.42  thf(f219,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((~ (irel @ sK8 @ X2)) | (sK2 @ X2)))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((~ (irel @ sK9 @ X3)) | (sK1 @ X3)))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1)))) )),
% 0.65/0.42    inference(beta-eta_normalization,[],[f218])).
% 0.65/0.42  thf(f220,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((sK2 @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((~ (irel @ sK9 @ X3)) | (sK1 @ X3)))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1))) | ($true = ((~ (irel @ sK8 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f219])).
% 0.65/0.42  thf(f221,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((sK2 @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((sK1 @ X3))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1))) | ($true = ((~ (irel @ sK8 @ X2)))) | ($true = ((~ (irel @ sK9 @ X3))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f220])).
% 0.65/0.42  thf(f222,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((sK2 @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((sK1 @ X3))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1))) | ($false = ((irel @ sK8 @ X2))) | ($true = ((~ (irel @ sK9 @ X3))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f221])).
% 0.65/0.42  thf(f223,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((sK2 @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((sK1 @ X3))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1))) | ($false = ((irel @ sK8 @ X2))) | ($false = ((irel @ sK9 @ X3)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f222])).
% 0.65/0.42  thf(f224,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f205])).
% 0.65/0.42  thf(f225,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = ((sK1 @ X1))) | ($true = ((~ (irel @ sK7 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f224])).
% 0.65/0.42  thf(f226,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f225])).
% 0.65/0.42  thf(f227,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = (((~ (irel @ sK8 @ X2)) | (sK2 @ X2)))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1)))) )),
% 0.65/0.42    inference(beta-eta_normalization,[],[f226])).
% 0.65/0.42  thf(f228,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((sK2 @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1))) | ($true = ((~ (irel @ sK8 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f227])).
% 0.65/0.42  thf(f229,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((sK2 @ X2))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1))) | ($false = ((irel @ sK8 @ X2)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f228])).
% 0.65/0.42  thf(f235,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f175])).
% 0.65/0.42  thf(f237,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($false = ((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f235])).
% 0.65/0.42  thf(f238,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($false = ((~ (irel @ sK9 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f237])).
% 0.65/0.42  thf(f239,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f237])).
% 0.65/0.42  thf(f240,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f239])).
% 0.65/0.42  thf(f245,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f240])).
% 0.65/0.42  thf(f246,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))) @ X2))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f245])).
% 0.65/0.42  thf(f247,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))) @ X2))) | ($true = ((sK1 @ X1))) | ($true = ((~ (irel @ sK7 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f246])).
% 0.65/0.42  thf(f248,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))) @ X2))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f247])).
% 0.65/0.42  thf(f249,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((~ (irel @ sK9 @ X2)) | (sK1 @ X2)))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1)))) )),
% 0.65/0.42    inference(beta-eta_normalization,[],[f248])).
% 0.65/0.42  thf(f250,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((sK1 @ X2))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1))) | ($true = ((~ (irel @ sK9 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f249])).
% 0.65/0.42  thf(f251,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((sK1 @ X2))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1))) | ($false = ((irel @ sK9 @ X2)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f250])).
% 0.65/0.42  thf(f252,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f238])).
% 0.65/0.42  thf(f253,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = ((sK1 @ X1))) | ($true = ((~ (irel @ sK7 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f252])).
% 0.65/0.42  thf(f254,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f253])).
% 0.65/0.42  thf(f258,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($false = ((((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK9 @ sK6))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f173])).
% 0.65/0.42  thf(f259,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($false = ((~ (irel @ sK9 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f258])).
% 0.65/0.42  thf(f260,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($false = (((~ (irel @ sK3 @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f258])).
% 0.65/0.42  thf(f261,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f260])).
% 0.65/0.42  thf(f266,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0)))))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f261])).
% 0.65/0.42  thf(f267,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))) @ X2))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f266])).
% 0.65/0.42  thf(f268,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))) @ X2))) | ($true = ((sK1 @ X1))) | ($true = ((~ (irel @ sK7 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f267])).
% 0.65/0.42  thf(f269,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK9 @ Y0)) | (sK1 @ Y0))) @ X2))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f268])).
% 0.65/0.42  thf(f270,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = (((~ (irel @ sK9 @ X2)) | (sK1 @ X2)))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1)))) )),
% 0.65/0.42    inference(beta-eta_normalization,[],[f269])).
% 0.65/0.42  thf(f271,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((sK1 @ X2))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1))) | ($true = ((~ (irel @ sK9 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f270])).
% 0.65/0.42  thf(f272,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((sK1 @ X2))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1))) | ($false = ((irel @ sK9 @ X2)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f271])).
% 0.65/0.42  thf(f273,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = (((~ (irel @ sK7 @ X1)) | (sK1 @ X1))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f259])).
% 0.65/0.42  thf(f274,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = ((sK1 @ X1))) | ($true = ((~ (irel @ sK7 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f273])).
% 0.65/0.42  thf(f275,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((irel @ sK3 @ sK5))) | ($true = ((irel @ sK9 @ sK6))) | ($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f274])).
% 0.65/0.42  thf(f424,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0)))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6)))))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f87])).
% 0.65/0.42  thf(f425,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK2 @ Y0))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6)))))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f87])).
% 0.65/0.42  thf(f426,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK2 @ Y0)))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6)))))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(not_proxy_clausification,[],[f425])).
% 0.65/0.42  thf(f427,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK2 @ Y0))) @ X1))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6)))))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f426])).
% 0.65/0.42  thf(f428,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK2 @ Y0))) @ X1))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK11))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f427])).
% 0.65/0.42  thf(f429,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK2 @ Y0))) @ X1))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK11))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0)))))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f428])).
% 0.65/0.42  thf(f527,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK2 @ Y0))) @ X1))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK11))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0)))))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f429])).
% 0.65/0.42  thf(f528,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK2 @ Y0))) @ X1))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK11))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f527])).
% 0.65/0.42  thf(f529,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK2 @ Y0))) @ X1))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK11))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))) @ X2)))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f528])).
% 0.65/0.42  thf(f530,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = (((((~ (irel @ sK3 @ sK8)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK8 @ sK4))) | (sK1 @ sK4)))) | ($true = (((~ (irel @ sK5 @ X1)) | (sK2 @ X1)))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2))))) )),
% 0.65/0.42    inference(beta-eta_normalization,[],[f529])).
% 0.65/0.42  thf(f531,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = (((~ (irel @ sK5 @ X1)) | (sK2 @ X1)))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f530])).
% 0.65/0.42  thf(f532,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((((~ (irel @ sK3 @ sK8)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK8 @ sK4))))) | ($true = (((~ (irel @ sK5 @ X1)) | (sK2 @ X1)))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f530])).
% 0.65/0.42  thf(f533,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((~ (irel @ sK8 @ sK4)))) | ($true = (((~ (irel @ sK5 @ X1)) | (sK2 @ X1)))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f532])).
% 0.65/0.42  thf(f534,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = (((~ (irel @ sK3 @ sK8)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0)))))))) | ($true = (((~ (irel @ sK5 @ X1)) | (sK2 @ X1)))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f532])).
% 0.65/0.42  thf(f535,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))))))) | ($true = (((~ (irel @ sK5 @ X1)) | (sK2 @ X1)))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f534])).
% 0.65/0.42  thf(f564,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0)))))) | ($true = (((~ (irel @ sK5 @ X1)) | (sK2 @ X1)))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f535])).
% 0.65/0.42  thf(f565,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = (((~ (irel @ sK5 @ X1)) | (sK2 @ X1)))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2))))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f564])).
% 0.65/0.42  thf(f566,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f565])).
% 0.65/0.42  thf(f568,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($false = ((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f566])).
% 0.65/0.42  thf(f570,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($false = (((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f568])).
% 0.65/0.42  thf(f571,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f570])).
% 0.65/0.42  thf(f580,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f571])).
% 0.65/0.42  thf(f581,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X4))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f580])).
% 0.65/0.42  thf(f582,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X4))) | ($true = ((sK1 @ X2))) | ($true = ((~ (irel @ sK5 @ X1)))) | ($true = ((~ (irel @ sK7 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f581])).
% 0.65/0.42  thf(f583,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X4))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($true = ((~ (irel @ sK7 @ X2))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f582])).
% 0.65/0.42  thf(f584,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0))) @ X3))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X4))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f583])).
% 0.65/0.42  thf(f585,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((~ (irel @ sK8 @ X3)) | (sK2 @ X3)))) | ($true = ((sK2 @ X1))) | ($true = (((~ (irel @ sK11 @ X4)) | (sK1 @ X4)))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2)))) )),
% 0.65/0.42    inference(beta-eta_normalization,[],[f584])).
% 0.65/0.42  thf(f586,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = (((~ (irel @ sK11 @ X4)) | (sK1 @ X4)))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2))) | ($true = ((~ (irel @ sK8 @ X3))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f585])).
% 0.65/0.42  thf(f587,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X4))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2))) | ($true = ((~ (irel @ sK8 @ X3)))) | ($true = ((~ (irel @ sK11 @ X4))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f586])).
% 0.65/0.42  thf(f588,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X4))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2))) | ($false = ((irel @ sK8 @ X3))) | ($true = ((~ (irel @ sK11 @ X4))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f587])).
% 0.65/0.42  thf(f589,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X3))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X4))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2))) | ($false = ((irel @ sK8 @ X3))) | ($false = ((irel @ sK11 @ X4)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f588])).
% 0.65/0.42  thf(f603,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = (((~ (irel @ sK5 @ X1)) | (sK2 @ X1)))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f533])).
% 0.65/0.42  thf(f604,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f603])).
% 0.65/0.42  thf(f606,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($false = ((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f604])).
% 0.65/0.42  thf(f608,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($false = (((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f606])).
% 0.65/0.42  thf(f609,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f608])).
% 0.65/0.42  thf(f615,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f609])).
% 0.65/0.42  thf(f616,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X3))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f615])).
% 0.65/0.42  thf(f617,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X3))) | ($true = ((sK1 @ X2))) | ($true = ((~ (irel @ sK5 @ X1)))) | ($true = ((~ (irel @ sK7 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f616])).
% 0.65/0.42  thf(f618,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X3))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($true = ((~ (irel @ sK7 @ X2))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f617])).
% 0.65/0.42  thf(f619,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X3))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f618])).
% 0.65/0.42  thf(f620,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = (((~ (irel @ sK11 @ X3)) | (sK1 @ X3)))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2)))) )),
% 0.65/0.42    inference(beta-eta_normalization,[],[f619])).
% 0.65/0.42  thf(f621,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X3))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2))) | ($true = ((~ (irel @ sK11 @ X3))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f620])).
% 0.65/0.42  thf(f622,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((irel @ sK8 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X3))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2))) | ($false = ((irel @ sK11 @ X3)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f621])).
% 0.65/0.42  thf(f630,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($false = (((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))) | (sK2 @ sK6)))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f531])).
% 0.65/0.42  thf(f632,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($false = ((((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK11 @ sK6))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f630])).
% 0.65/0.42  thf(f634,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($false = (((~ (irel @ sK3 @ sK11)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f632])).
% 0.65/0.42  thf(f635,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f634])).
% 0.65/0.42  thf(f641,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0)))))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f635])).
% 0.65/0.42  thf(f642,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X3))) | ($true = (((~ (irel @ sK7 @ X2)) | (sK1 @ X2)))) | ($true = ((~ (irel @ sK5 @ X1))))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f641])).
% 0.65/0.42  thf(f643,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X3))) | ($true = ((sK1 @ X2))) | ($true = ((~ (irel @ sK5 @ X1)))) | ($true = ((~ (irel @ sK7 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f642])).
% 0.65/0.42  thf(f644,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X3))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($true = ((~ (irel @ sK7 @ X2))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f643])).
% 0.65/0.42  thf(f645,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK11 @ Y0)) | (sK1 @ Y0))) @ X3))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f644])).
% 0.65/0.42  thf(f646,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = (((~ (irel @ sK11 @ X3)) | (sK1 @ X3)))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2)))) )),
% 0.65/0.42    inference(beta-eta_normalization,[],[f645])).
% 0.65/0.42  thf(f647,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X3))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2))) | ($true = ((~ (irel @ sK11 @ X3))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f646])).
% 0.65/0.42  thf(f648,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((sK1 @ sK4))) | ($true = ((sK2 @ X1))) | ($true = ((sK1 @ X3))) | ($true = ((sK1 @ X2))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((irel @ sK7 @ X2))) | ($false = ((irel @ sK11 @ X3)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f647])).
% 0.65/0.42  thf(f838,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))) @ sK13))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6)))))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f424])).
% 0.65/0.42  thf(f839,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))) @ sK13))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK14))) | ($false = (((~ (irel @ sK3 @ sK7)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))))),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f838])).
% 0.65/0.42  thf(f840,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))) @ sK13))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK14))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0)))))))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f839])).
% 0.65/0.42  thf(f992,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))) @ sK13))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK14))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))))))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f840])).
% 0.65/0.42  thf(f1209,plain,(
% 0.65/0.42    ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK4))) | (sK1 @ sK4))) @ sK8))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))) @ sK13))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ sK6))) | (sK2 @ sK6))) @ sK14))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK7 @ Y0)) | (sK2 @ Y0))) @ sK15)))),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f992])).
% 0.65/0.42  thf(f1210,plain,(
% 0.65/0.42    ($false = (((((~ (irel @ sK3 @ sK8)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK8 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK8 @ sK4))) | (sK1 @ sK4)))) | ($false = (((~ (irel @ sK5 @ sK13)) | (sK1 @ sK13)))) | ($false = (((((~ (irel @ sK3 @ sK14)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK14 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK14 @ sK6))) | (sK2 @ sK6)))) | ($false = (((~ (irel @ sK7 @ sK15)) | (sK2 @ sK15))))),
% 0.65/0.42    inference(beta-eta_normalization,[],[f1209])).
% 0.65/0.42  thf(f1211,plain,(
% 0.65/0.42    ($false = ((sK1 @ sK4))) | ($false = (((~ (irel @ sK5 @ sK13)) | (sK1 @ sK13)))) | ($false = (((((~ (irel @ sK3 @ sK14)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK14 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK14 @ sK6))) | (sK2 @ sK6)))) | ($false = (((~ (irel @ sK7 @ sK15)) | (sK2 @ sK15))))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f1210])).
% 0.65/0.42  thf(f1442,plain,(
% 0.65/0.42    ($false = ((sK1 @ sK4))) | ($false = ((sK1 @ sK13))) | ($false = (((((~ (irel @ sK3 @ sK14)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK14 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK14 @ sK6))) | (sK2 @ sK6)))) | ($false = (((~ (irel @ sK7 @ sK15)) | (sK2 @ sK15))))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f1211])).
% 0.65/0.42  thf(f1473,plain,(
% 0.65/0.42    ($false = ((sK1 @ sK4))) | ($false = ((sK1 @ sK13))) | ($false = ((sK2 @ sK6))) | ($false = (((~ (irel @ sK7 @ sK15)) | (sK2 @ sK15))))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f1442])).
% 0.65/0.42  thf(f1498,plain,(
% 0.65/0.42    ($false = ((sK1 @ sK4))) | ($false = ((sK1 @ sK13))) | ($false = ((sK2 @ sK6))) | ($false = ((sK2 @ sK15)))),
% 0.65/0.42    inference(or_proxy_clausification,[],[f1473])).
% 0.65/0.42  thf(f1501,plain,(
% 0.65/0.42    ($true = (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)))))) & (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ 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 @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))))))))),
% 0.65/0.42    inference(beta-eta_normalization,[],[f76])).
% 0.65/0.42  thf(f1502,plain,(
% 0.65/0.42    ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ 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 @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))))))))),
% 0.65/0.42    inference(and_proxy_clausification,[],[f1501])).
% 0.65/0.42  thf(f1503,plain,(
% 0.65/0.42    ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ 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 @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))))))))),
% 0.65/0.42    inference(and_proxy_clausification,[],[f1501])).
% 0.65/0.42  thf(f1504,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ 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 @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))))))))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f1503])).
% 0.65/0.42  thf(f1506,plain,(
% 0.65/0.42    ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ 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))))))))))) )),
% 0.65/0.42    inference(and_proxy_clausification,[],[f1504])).
% 0.65/0.42  thf(f1507,plain,(
% 0.65/0.42    ( ! [X2 : $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))))) @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))))) @ X2)))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f1506])).
% 0.65/0.42  thf(f1508,plain,(
% 0.65/0.42    ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1)))))) | ($true = (((~ (irel @ sK3 @ X2)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.65/0.42    inference(beta-eta_normalization,[],[f1507])).
% 0.65/0.42  thf(f1509,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1))) @ X3))) | ($true = (((~ (irel @ sK3 @ X2)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.65/0.42    inference(pi_proxy_clausification,[],[f1508])).
% 0.65/0.42  thf(f1510,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1))) @ X3))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))))) | ($true = ((~ (irel @ sK3 @ X2))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f1509])).
% 0.65/0.42  thf(f1511,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ 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.65/0.42    inference(or_proxy_clausification,[],[f1510])).
% 0.65/0.42  thf(f1512,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ 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.65/0.42    inference(pi_proxy_clausification,[],[f1511])).
% 0.65/0.42  thf(f1513,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ 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.65/0.42    inference(not_proxy_clausification,[],[f1512])).
% 0.65/0.42  thf(f1514,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ 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.65/0.42    inference(not_proxy_clausification,[],[f1513])).
% 0.65/0.42  thf(f1515,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1))) @ X3))) | ($true = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))) @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))) @ (sK16 @ X2))))) )),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f1514])).
% 0.65/0.42  thf(f1516,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1)))) | ($true = (((~ (irel @ X2 @ X4)) | (sK2 @ X4)))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK16 @ X2))) | (sK1 @ (sK16 @ X2)))))) )),
% 0.65/0.42    inference(beta-eta_normalization,[],[f1515])).
% 0.65/0.42  thf(f1517,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = (((~ (irel @ X2 @ X4)) | (sK2 @ X4)))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK16 @ X2))) | (sK1 @ (sK16 @ X2))))) | ($true = ((((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ X3 @ X1)))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f1516])).
% 0.65/0.42  thf(f1518,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK16 @ X2))) | (sK1 @ (sK16 @ X2))))) | ($true = ((((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ X3 @ X1))))) | ($true = ((~ (irel @ X2 @ X4))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f1517])).
% 0.65/0.42  thf(f1519,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK16 @ X2)))) | ($true = ((((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ X3 @ X1))))) | ($true = ((~ (irel @ X2 @ X4))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f1518])).
% 0.65/0.42  thf(f1533,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK16 @ X2)))) | ($true = ((~ (irel @ X3 @ X1)))) | ($true = ((~ (irel @ X2 @ X4)))) | ($true = (((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK1 @ Y0))))))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f1519])).
% 0.65/0.42  thf(f1534,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK16 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($true = ((~ (irel @ X2 @ X4)))) | ($true = (((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK1 @ Y0))))))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f1533])).
% 0.65/0.42  thf(f1535,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK16 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($true = (((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK1 @ Y0))))))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f1534])).
% 0.65/0.42  thf(f1536,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK16 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK1 @ Y0))))))) | ($true = ((~ (irel @ sK3 @ X3))))) )),
% 0.65/0.42    inference(or_proxy_clausification,[],[f1535])).
% 0.65/0.42  thf(f1537,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK16 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK1 @ Y0)))))) | ($true = ((~ (irel @ sK3 @ X3))))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f1536])).
% 0.65/0.42  thf(f1538,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK16 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK1 @ Y0))) @ (sK18 @ X3)))) | ($true = ((~ (irel @ sK3 @ X3))))) )),
% 0.65/0.42    inference(sigma_proxy_clausification,[],[f1537])).
% 0.65/0.42  thf(f1539,plain,(
% 0.65/0.42    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK16 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK1 @ Y0))) @ (sK18 @ X3)))) | ($false = ((irel @ sK3 @ X3)))) )),
% 0.65/0.42    inference(not_proxy_clausification,[],[f1538])).
% 0.65/0.43  thf(f1540,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK16 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($false = (((~ (irel @ X3 @ (sK18 @ X3))) | (sK1 @ (sK18 @ X3))))) | ($false = ((irel @ sK3 @ X3)))) )),
% 0.65/0.43    inference(beta-eta_normalization,[],[f1539])).
% 0.65/0.43  thf(f1541,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK1 @ (sK16 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($false = ((sK1 @ (sK18 @ X3)))) | ($false = ((irel @ sK3 @ X3)))) )),
% 0.65/0.43    inference(or_proxy_clausification,[],[f1540])).
% 0.65/0.43  thf(f1581,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ 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 @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1)))))))))))) )),
% 0.65/0.43    inference(pi_proxy_clausification,[],[f1502])).
% 0.65/0.43  thf(f1582,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK1 @ Y0))))) @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))))))) )),
% 0.65/0.43    inference(and_proxy_clausification,[],[f1581])).
% 0.65/0.43  thf(f1621,plain,(
% 0.65/0.43    ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK3 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK1 @ Y0))))) @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))))) @ X2)))) )),
% 0.65/0.43    inference(pi_proxy_clausification,[],[f1582])).
% 0.65/0.43  thf(f1622,plain,(
% 0.65/0.43    ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1)))))) | ($true = (((~ (irel @ sK3 @ X2)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))))))) )),
% 0.65/0.43    inference(beta-eta_normalization,[],[f1621])).
% 0.65/0.43  thf(f1623,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ X1))) | (sK1 @ X1))) @ X3))) | ($true = (((~ (irel @ sK3 @ X2)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))))))) )),
% 0.65/0.43    inference(pi_proxy_clausification,[],[f1622])).
% 0.65/0.43  thf(f1624,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ 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.65/0.43    inference(or_proxy_clausification,[],[f1623])).
% 0.65/0.43  thf(f1625,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ 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.65/0.43    inference(or_proxy_clausification,[],[f1624])).
% 0.65/0.43  thf(f1626,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ 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.65/0.43    inference(pi_proxy_clausification,[],[f1625])).
% 0.65/0.43  thf(f1627,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ 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.65/0.43    inference(not_proxy_clausification,[],[f1626])).
% 0.65/0.43  thf(f1628,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ 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.65/0.43    inference(not_proxy_clausification,[],[f1627])).
% 0.65/0.43  thf(f1629,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((((~ (irel @ sK3 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ 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))) @ (sK25 @ X2))))) )),
% 0.65/0.43    inference(sigma_proxy_clausification,[],[f1628])).
% 0.65/0.43  thf(f1630,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X3 @ X1))) | (sK1 @ X1)))) | ($true = (((~ (irel @ X2 @ X4)) | (sK1 @ X4)))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK25 @ X2))) | (sK2 @ (sK25 @ X2)))))) )),
% 0.65/0.43    inference(beta-eta_normalization,[],[f1629])).
% 0.65/0.43  thf(f1631,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = (((~ (irel @ X2 @ X4)) | (sK1 @ X4)))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK25 @ X2))) | (sK2 @ (sK25 @ X2))))) | ($true = ((((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X3 @ X1)))))) )),
% 0.65/0.43    inference(or_proxy_clausification,[],[f1630])).
% 0.65/0.43  thf(f1632,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = (((~ (irel @ X2 @ (sK25 @ X2))) | (sK2 @ (sK25 @ X2))))) | ($true = ((((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X3 @ X1))))) | ($true = ((~ (irel @ X2 @ X4))))) )),
% 0.65/0.43    inference(or_proxy_clausification,[],[f1631])).
% 0.65/0.43  thf(f1633,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK25 @ X2)))) | ($true = ((((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X3 @ X1))))) | ($true = ((~ (irel @ X2 @ X4))))) )),
% 0.65/0.43    inference(or_proxy_clausification,[],[f1632])).
% 0.65/0.43  thf(f1647,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK25 @ X2)))) | ($true = ((~ (irel @ X3 @ X1)))) | ($true = ((~ (irel @ X2 @ X4)))) | ($true = (((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.65/0.43    inference(or_proxy_clausification,[],[f1633])).
% 0.65/0.43  thf(f1648,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK25 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($true = ((~ (irel @ X2 @ X4)))) | ($true = (((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.65/0.43    inference(not_proxy_clausification,[],[f1647])).
% 0.65/0.43  thf(f1649,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK25 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($true = (((~ (irel @ sK3 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.65/0.43    inference(not_proxy_clausification,[],[f1648])).
% 0.65/0.43  thf(f1650,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK25 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK2 @ Y0))))))) | ($true = ((~ (irel @ sK3 @ X3))))) )),
% 0.65/0.43    inference(or_proxy_clausification,[],[f1649])).
% 0.65/0.43  thf(f1651,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK25 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK2 @ Y0)))))) | ($true = ((~ (irel @ sK3 @ X3))))) )),
% 0.65/0.43    inference(not_proxy_clausification,[],[f1650])).
% 0.65/0.43  thf(f1652,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK25 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK2 @ Y0))) @ (sK27 @ X3)))) | ($true = ((~ (irel @ sK3 @ X3))))) )),
% 0.65/0.43    inference(sigma_proxy_clausification,[],[f1651])).
% 0.65/0.43  thf(f1653,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK25 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK2 @ Y0))) @ (sK27 @ X3)))) | ($false = ((irel @ sK3 @ X3)))) )),
% 0.65/0.43    inference(not_proxy_clausification,[],[f1652])).
% 0.65/0.43  thf(f1654,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK25 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($false = (((~ (irel @ X3 @ (sK27 @ X3))) | (sK2 @ (sK27 @ X3))))) | ($false = ((irel @ sK3 @ X3)))) )),
% 0.65/0.43    inference(beta-eta_normalization,[],[f1653])).
% 0.65/0.43  thf(f1655,plain,(
% 0.65/0.43    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK1 @ X1))) | ($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((sK2 @ (sK25 @ X2)))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X2 @ X4))) | ($false = ((sK2 @ (sK27 @ X3)))) | ($false = ((irel @ sK3 @ X3)))) )),
% 0.65/0.43    inference(or_proxy_clausification,[],[f1654])).
% 0.65/0.43  thf(f1659,definition,(
% 0.65/0.43    spl28_1 <=> ($true = ((irel @ sK3 @ sK7)))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_1])],[avatar_definition])).
% 0.65/0.43  thf(f1660,plain,(
% 0.65/0.43    ($true != ((irel @ sK3 @ sK7))) | spl28_1),
% 0.65/0.43    inference(avatar_component_clause,[],[f1659])).
% 0.65/0.43  thf(f1661,plain,(
% 0.65/0.43    ($true = ((irel @ sK3 @ sK7))) | ~spl28_1),
% 0.65/0.43    inference(avatar_component_clause,[],[f1659])).
% 0.65/0.43  thf(f1667,definition,(
% 0.65/0.43    spl28_3 <=> ($true = ((irel @ sK3 @ sK5)))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_3])],[avatar_definition])).
% 0.65/0.43  thf(f1669,plain,(
% 0.65/0.43    ($true = ((irel @ sK3 @ sK5))) | ~spl28_3),
% 0.65/0.43    inference(avatar_component_clause,[],[f1667])).
% 0.65/0.43  thf(f1676,definition,(
% 0.65/0.43    spl28_5 <=> ! [X1 : $i] : (($true = ((sK1 @ X1))) | ($false = ((irel @ sK9 @ X1))))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_5])],[avatar_definition])).
% 0.65/0.43  thf(f1677,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($true = ((sK1 @ X1))) | ($false = ((irel @ sK9 @ X1)))) ) | ~spl28_5),
% 0.65/0.43    inference(avatar_component_clause,[],[f1676])).
% 0.65/0.43  thf(f1680,definition,(
% 0.65/0.43    spl28_6 <=> ($true = ((irel @ sK9 @ sK6)))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_6])],[avatar_definition])).
% 0.65/0.43  thf(f1681,plain,(
% 0.65/0.43    ($true != ((irel @ sK9 @ sK6))) | spl28_6),
% 0.65/0.43    inference(avatar_component_clause,[],[f1680])).
% 0.65/0.43  thf(f1682,plain,(
% 0.65/0.43    ($true = ((irel @ sK9 @ sK6))) | ~spl28_6),
% 0.65/0.43    inference(avatar_component_clause,[],[f1680])).
% 0.65/0.43  thf(f1685,definition,(
% 0.65/0.43    spl28_7 <=> ($false = ((sK2 @ sK6)))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_7])],[avatar_definition])).
% 0.65/0.43  thf(f1686,plain,(
% 0.65/0.43    ($false != ((sK2 @ sK6))) | spl28_7),
% 0.65/0.43    inference(avatar_component_clause,[],[f1685])).
% 0.65/0.43  thf(f1687,plain,(
% 0.65/0.43    ($false = ((sK2 @ sK6))) | ~spl28_7),
% 0.65/0.43    inference(avatar_component_clause,[],[f1685])).
% 0.65/0.43  thf(f1690,definition,(
% 0.65/0.43    spl28_8 <=> ! [X1 : $i] : (($true = ((sK2 @ X1))) | ($false = ((irel @ sK8 @ X1))))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_8])],[avatar_definition])).
% 0.65/0.43  thf(f1691,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($true = ((sK2 @ X1))) | ($false = ((irel @ sK8 @ X1)))) ) | ~spl28_8),
% 0.65/0.43    inference(avatar_component_clause,[],[f1690])).
% 0.65/0.43  thf(f1697,definition,(
% 0.65/0.43    spl28_9 <=> ($true = ((irel @ sK8 @ sK4)))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_9])],[avatar_definition])).
% 0.65/0.43  thf(f1699,plain,(
% 0.65/0.43    ($true = ((irel @ sK8 @ sK4))) | ~spl28_9),
% 0.65/0.43    inference(avatar_component_clause,[],[f1697])).
% 0.65/0.43  thf(f1705,definition,(
% 0.65/0.43    spl28_10 <=> ($false = ((sK1 @ sK4)))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_10])],[avatar_definition])).
% 0.65/0.43  thf(f1707,plain,(
% 0.65/0.43    ($false = ((sK1 @ sK4))) | ~spl28_10),
% 0.65/0.43    inference(avatar_component_clause,[],[f1705])).
% 0.65/0.43  thf(f1713,definition,(
% 0.65/0.43    spl28_11 <=> ! [X1 : $i] : (($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1))))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_11])],[avatar_definition])).
% 0.65/0.43  thf(f1714,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($true = ((sK1 @ X1))) | ($false = ((irel @ sK7 @ X1)))) ) | ~spl28_11),
% 0.65/0.43    inference(avatar_component_clause,[],[f1713])).
% 0.65/0.43  thf(f1720,plain,(
% 0.65/0.43    spl28_11 | spl28_5 | spl28_3 | spl28_8),
% 0.65/0.43    inference(avatar_split_clause,[],[f223,f1690,f1667,f1676,f1713])).
% 0.65/0.43  thf(f1721,plain,(
% 0.65/0.43    spl28_11 | spl28_6 | spl28_3 | spl28_8),
% 0.65/0.43    inference(avatar_split_clause,[],[f229,f1690,f1667,f1680,f1713])).
% 0.65/0.43  thf(f1724,plain,(
% 0.65/0.43    spl28_11 | spl28_5 | spl28_3 | spl28_9),
% 0.65/0.43    inference(avatar_split_clause,[],[f251,f1697,f1667,f1676,f1713])).
% 0.65/0.43  thf(f1725,plain,(
% 0.65/0.43    spl28_11 | spl28_6 | spl28_3 | spl28_9),
% 0.65/0.43    inference(avatar_split_clause,[],[f254,f1697,f1667,f1680,f1713])).
% 0.65/0.43  thf(f1728,plain,(
% 0.65/0.43    spl28_11 | spl28_5 | spl28_3 | spl28_10),
% 0.65/0.43    inference(avatar_split_clause,[],[f272,f1705,f1667,f1676,f1713])).
% 0.65/0.43  thf(f1729,plain,(
% 0.65/0.43    spl28_11 | spl28_6 | spl28_3 | spl28_10),
% 0.65/0.43    inference(avatar_split_clause,[],[f275,f1705,f1667,f1680,f1713])).
% 0.65/0.43  thf(f1776,definition,(
% 0.65/0.43    spl28_15 <=> ! [X1 : $i] : (($true = ((sK2 @ X1))) | ($false = ((irel @ sK5 @ X1))))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_15])],[avatar_definition])).
% 0.65/0.43  thf(f1777,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($true = ((sK2 @ X1))) | ($false = ((irel @ sK5 @ X1)))) ) | ~spl28_15),
% 0.65/0.43    inference(avatar_component_clause,[],[f1776])).
% 0.65/0.43  thf(f1780,definition,(
% 0.65/0.43    spl28_16 <=> ! [X2 : $i] : (($true = ((sK1 @ X2))) | ($false = ((irel @ sK11 @ X2))))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_16])],[avatar_definition])).
% 0.65/0.43  thf(f1781,plain,(
% 0.65/0.43    ( ! [X2 : $i] : (($true = ((sK1 @ X2))) | ($false = ((irel @ sK11 @ X2)))) ) | ~spl28_16),
% 0.65/0.43    inference(avatar_component_clause,[],[f1780])).
% 0.65/0.43  thf(f1806,plain,(
% 0.65/0.43    spl28_11 | spl28_16 | spl28_15 | spl28_8),
% 0.65/0.43    inference(avatar_split_clause,[],[f589,f1690,f1776,f1780,f1713])).
% 0.65/0.43  thf(f1810,plain,(
% 0.65/0.43    spl28_11 | spl28_16 | spl28_15 | spl28_9),
% 0.65/0.43    inference(avatar_split_clause,[],[f622,f1697,f1776,f1780,f1713])).
% 0.65/0.43  thf(f1814,plain,(
% 0.65/0.43    spl28_11 | spl28_16 | spl28_15 | spl28_10),
% 0.65/0.43    inference(avatar_split_clause,[],[f648,f1705,f1776,f1780,f1713])).
% 0.65/0.43  thf(f1877,definition,(
% 0.65/0.43    spl28_24 <=> ($false = ((sK1 @ sK13)))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_24])],[avatar_definition])).
% 0.65/0.43  thf(f1878,plain,(
% 0.65/0.43    ($false != ((sK1 @ sK13))) | spl28_24),
% 0.65/0.43    inference(avatar_component_clause,[],[f1877])).
% 0.65/0.43  thf(f1879,plain,(
% 0.65/0.43    ($false = ((sK1 @ sK13))) | ~spl28_24),
% 0.65/0.43    inference(avatar_component_clause,[],[f1877])).
% 0.65/0.43  thf(f1946,definition,(
% 0.65/0.43    spl28_26 <=> ($false = ((sK2 @ sK15)))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_26])],[avatar_definition])).
% 0.65/0.43  thf(f1947,plain,(
% 0.65/0.43    ($false != ((sK2 @ sK15))) | spl28_26),
% 0.65/0.43    inference(avatar_component_clause,[],[f1946])).
% 0.65/0.43  thf(f1948,plain,(
% 0.65/0.43    ($false = ((sK2 @ sK15))) | ~spl28_26),
% 0.65/0.43    inference(avatar_component_clause,[],[f1946])).
% 0.65/0.43  thf(f2011,plain,(
% 0.65/0.43    spl28_26 | spl28_7 | spl28_24 | spl28_10),
% 0.65/0.43    inference(avatar_split_clause,[],[f1498,f1705,f1877,f1685,f1946])).
% 0.65/0.43  thf(f2024,definition,(
% 0.65/0.43    spl28_30 <=> ! [X4 : $i,X2 : $i] : (($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4))) | ($false = ((sK1 @ (sK16 @ X2)))))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_30])],[avatar_definition])).
% 0.65/0.43  thf(f2025,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4))) | ($false = ((sK1 @ (sK16 @ X2))))) ) | ~spl28_30),
% 0.65/0.43    inference(avatar_component_clause,[],[f2024])).
% 0.65/0.43  thf(f2031,definition,(
% 0.65/0.43    spl28_32 <=> ! [X1 : $i,X3 : $i] : (($true = ((sK2 @ X1))) | ($false = ((irel @ sK3 @ X3))) | ($false = ((sK1 @ (sK18 @ X3)))) | ($false = ((irel @ X3 @ X1))))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_32])],[avatar_definition])).
% 0.65/0.43  thf(f2032,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($true = ((sK2 @ X1))) | ($false = ((irel @ sK3 @ X3))) | ($false = ((sK1 @ (sK18 @ X3)))) | ($false = ((irel @ X3 @ X1)))) ) | ~spl28_32),
% 0.65/0.43    inference(avatar_component_clause,[],[f2031])).
% 0.65/0.43  thf(f2033,plain,(
% 0.65/0.43    spl28_30 | spl28_32),
% 0.65/0.43    inference(avatar_split_clause,[],[f1541,f2031,f2024])).
% 0.65/0.43  thf(f2090,definition,(
% 0.65/0.43    spl28_48 <=> ! [X4 : $i,X2 : $i] : (($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4))) | ($false = ((sK2 @ (sK25 @ X2)))))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_48])],[avatar_definition])).
% 0.65/0.43  thf(f2091,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4))) | ($false = ((sK2 @ (sK25 @ X2))))) ) | ~spl28_48),
% 0.65/0.43    inference(avatar_component_clause,[],[f2090])).
% 0.65/0.43  thf(f2097,definition,(
% 0.65/0.43    spl28_50 <=> ! [X1 : $i,X3 : $i] : (($true = ((sK1 @ X1))) | ($false = ((irel @ sK3 @ X3))) | ($false = ((sK2 @ (sK27 @ X3)))) | ($false = ((irel @ X3 @ X1))))),
% 0.65/0.43    introduced(definition,[new_symbols(definition,[spl28_50])],[avatar_definition])).
% 0.65/0.43  thf(f2098,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($true = ((sK1 @ X1))) | ($false = ((irel @ sK3 @ X3))) | ($false = ((sK2 @ (sK27 @ X3)))) | ($false = ((irel @ X3 @ X1)))) ) | ~spl28_50),
% 0.65/0.43    inference(avatar_component_clause,[],[f2097])).
% 0.65/0.43  thf(f2099,plain,(
% 0.65/0.43    spl28_48 | spl28_50),
% 0.65/0.43    inference(avatar_split_clause,[],[f1655,f2097,f2090])).
% 0.65/0.43  thf(f2100,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($false = ((sK1 @ X0)))) ) | ~spl28_24),
% 0.65/0.43    inference(constrained_superposition,[],[f1879,f50])).
% 0.65/0.43  thf(f2106,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($true = ((irel @ sK3 @ X0)))) ) | ~spl28_1),
% 0.65/0.43    inference(constrained_superposition,[],[f1661,f50])).
% 0.65/0.43  thf(f2110,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($true = ((irel @ sK3 @ X0)))) ) | ~spl28_3),
% 0.65/0.43    inference(constrained_superposition,[],[f1669,f50])).
% 0.65/0.43  thf(f2114,plain,(
% 0.65/0.43    ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X0 @ X1)))) ) | ~spl28_1),
% 0.65/0.43    inference(constrained_superposition,[],[f2106,f50])).
% 0.65/0.43  thf(f2124,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($true = $false) | ($false = ((irel @ sK7 @ X1)))) ) | (~spl28_11 | ~spl28_24)),
% 0.65/0.43    inference(forward_demodulation,[],[f1714,f2100])).
% 0.65/0.43  thf(f2125,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($false = ((irel @ sK7 @ X1)))) ) | (~spl28_11 | ~spl28_24)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2124])).
% 0.65/0.43  thf(f2126,plain,(
% 0.65/0.43    ($true = $false) | (~spl28_1 | ~spl28_11 | ~spl28_24)),
% 0.65/0.43    inference(forward_demodulation,[],[f2125,f2114])).
% 0.65/0.43  thf(f2127,plain,(
% 0.65/0.43    $false | (~spl28_1 | ~spl28_11 | ~spl28_24)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2126])).
% 0.65/0.43  thf(f2128,plain,(
% 0.65/0.43    ~spl28_1 | ~spl28_11 | ~spl28_24),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2127])).
% 0.65/0.43  thf(f2131,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($false != ((sK1 @ X0)))) ) | spl28_24),
% 0.65/0.43    inference(constrained_superposition,[],[f1878,f50])).
% 0.65/0.43  thf(f2135,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($false = ((sK2 @ X0)))) ) | ~spl28_26),
% 0.65/0.43    inference(constrained_superposition,[],[f1948,f50])).
% 0.65/0.43  thf(f2141,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($true = ((sK2 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4)))) ) | (spl28_24 | ~spl28_30)),
% 0.65/0.43    inference(forward_subsumption_resolution,[],[f2025,f2131])).
% 0.65/0.43  thf(f2142,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($true = $false) | ($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4)))) ) | (spl28_24 | ~spl28_26 | ~spl28_30)),
% 0.65/0.43    inference(forward_demodulation,[],[f2141,f2135])).
% 0.65/0.43  thf(f2143,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4)))) ) | (spl28_24 | ~spl28_26 | ~spl28_30)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2142])).
% 0.65/0.43  thf(f2144,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($true = $false) | ($false = ((irel @ X2 @ X4)))) ) | (~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_30)),
% 0.65/0.43    inference(forward_demodulation,[],[f2143,f2114])).
% 0.65/0.43  thf(f2145,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($false = ((irel @ X2 @ X4)))) ) | (~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_30)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2144])).
% 0.65/0.43  thf(f2148,plain,(
% 0.65/0.43    ($true = $false) | (~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_30)),
% 0.65/0.43    inference(constrained_superposition,[],[f2145,f2114])).
% 0.65/0.43  thf(f2152,plain,(
% 0.65/0.43    $false | (~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_30)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2148])).
% 0.65/0.43  thf(f2153,plain,(
% 0.65/0.43    ~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_30),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2152])).
% 0.65/0.43  thf(f2155,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($true = ((sK2 @ X1))) | ($false = ((irel @ sK3 @ X3))) | ($false = ((irel @ X3 @ X1)))) ) | (spl28_24 | ~spl28_32)),
% 0.65/0.43    inference(forward_subsumption_resolution,[],[f2032,f2131])).
% 0.65/0.43  thf(f2156,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK3 @ X3))) | ($false = ((irel @ X3 @ X1)))) ) | (spl28_24 | ~spl28_26 | ~spl28_32)),
% 0.65/0.43    inference(forward_demodulation,[],[f2155,f2135])).
% 0.65/0.43  thf(f2157,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X3))) | ($false = ((irel @ X3 @ X1)))) ) | (spl28_24 | ~spl28_26 | ~spl28_32)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2156])).
% 0.65/0.43  thf(f2158,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ X3 @ X1)))) ) | (~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_32)),
% 0.65/0.43    inference(forward_demodulation,[],[f2157,f2114])).
% 0.65/0.43  thf(f2159,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($false = ((irel @ X3 @ X1)))) ) | (~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_32)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2158])).
% 0.65/0.43  thf(f2161,plain,(
% 0.65/0.43    ($true = $false) | (~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_32)),
% 0.65/0.43    inference(constrained_superposition,[],[f2159,f2114])).
% 0.65/0.43  thf(f2165,plain,(
% 0.65/0.43    $false | (~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_32)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2161])).
% 0.65/0.43  thf(f2166,plain,(
% 0.65/0.43    ~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_32),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2165])).
% 0.65/0.43  thf(f2168,plain,(
% 0.65/0.43    $false | (~spl28_10 | spl28_24)),
% 0.65/0.43    inference(forward_subsumption_resolution,[],[f1707,f2131])).
% 0.65/0.43  thf(f2169,plain,(
% 0.65/0.43    ~spl28_10 | spl28_24),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2168])).
% 0.65/0.43  thf(f2173,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($false = ((sK1 @ X0)))) ) | ~spl28_10),
% 0.65/0.43    inference(constrained_superposition,[],[f1707,f50])).
% 0.65/0.43  thf(f2179,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($true = ((irel @ sK8 @ X0)))) ) | ~spl28_9),
% 0.65/0.43    inference(constrained_superposition,[],[f1699,f50])).
% 0.65/0.43  thf(f2187,plain,(
% 0.65/0.43    ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X0 @ X1)))) ) | ~spl28_9),
% 0.65/0.43    inference(constrained_superposition,[],[f2179,f50])).
% 0.65/0.43  thf(f2195,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($true = $false) | ($true = ((sK2 @ X1)))) ) | (~spl28_8 | ~spl28_9)),
% 0.65/0.43    inference(forward_demodulation,[],[f1691,f2187])).
% 0.65/0.43  thf(f2196,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($true = ((sK2 @ X1)))) ) | (~spl28_8 | ~spl28_9)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2195])).
% 0.65/0.43  thf(f2239,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK3 @ X3))) | ($false = ((sK2 @ (sK27 @ X3)))) | ($false = ((irel @ X3 @ X1)))) ) | (~spl28_10 | ~spl28_50)),
% 0.65/0.43    inference(forward_demodulation,[],[f2098,f2173])).
% 0.65/0.43  thf(f2240,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X3))) | ($false = ((sK2 @ (sK27 @ X3)))) | ($false = ((irel @ X3 @ X1)))) ) | (~spl28_10 | ~spl28_50)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2239])).
% 0.65/0.43  thf(f2241,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($true = $false) | ($false = ((sK2 @ (sK27 @ X3)))) | ($false = ((irel @ X3 @ X1)))) ) | (~spl28_9 | ~spl28_10 | ~spl28_50)),
% 0.65/0.43    inference(forward_demodulation,[],[f2240,f2187])).
% 0.65/0.43  thf(f2242,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($false = ((sK2 @ (sK27 @ X3)))) | ($false = ((irel @ X3 @ X1)))) ) | (~spl28_9 | ~spl28_10 | ~spl28_50)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2241])).
% 0.65/0.43  thf(f2243,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ X3 @ X1)))) ) | (~spl28_8 | ~spl28_9 | ~spl28_10 | ~spl28_50)),
% 0.65/0.43    inference(forward_demodulation,[],[f2242,f2196])).
% 0.65/0.43  thf(f2244,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($false = ((irel @ X3 @ X1)))) ) | (~spl28_8 | ~spl28_9 | ~spl28_10 | ~spl28_50)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2243])).
% 0.65/0.43  thf(f2246,plain,(
% 0.65/0.43    ($true = $false) | (~spl28_8 | ~spl28_9 | ~spl28_10 | ~spl28_50)),
% 0.65/0.43    inference(constrained_superposition,[],[f2244,f2187])).
% 0.65/0.43  thf(f2250,plain,(
% 0.65/0.43    $false | (~spl28_8 | ~spl28_9 | ~spl28_10 | ~spl28_50)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2246])).
% 0.65/0.43  thf(f2251,plain,(
% 0.65/0.43    ~spl28_8 | ~spl28_9 | ~spl28_10 | ~spl28_50),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2250])).
% 0.65/0.43  thf(f2253,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($true = $false) | ($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4))) | ($false = ((sK2 @ (sK25 @ X2))))) ) | (~spl28_10 | ~spl28_48)),
% 0.65/0.43    inference(forward_demodulation,[],[f2091,f2173])).
% 0.65/0.43  thf(f2254,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4))) | ($false = ((sK2 @ (sK25 @ X2))))) ) | (~spl28_10 | ~spl28_48)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2253])).
% 0.65/0.43  thf(f2255,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($true = $false) | ($false = ((irel @ X2 @ X4))) | ($false = ((sK2 @ (sK25 @ X2))))) ) | (~spl28_9 | ~spl28_10 | ~spl28_48)),
% 0.65/0.43    inference(forward_demodulation,[],[f2254,f2187])).
% 0.65/0.43  thf(f2256,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($false = ((irel @ X2 @ X4))) | ($false = ((sK2 @ (sK25 @ X2))))) ) | (~spl28_9 | ~spl28_10 | ~spl28_48)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2255])).
% 0.65/0.43  thf(f2257,plain,(
% 0.65/0.43    ( ! [X2 : $i] : (($true = $false) | ($false = ((sK2 @ (sK25 @ X2))))) ) | (~spl28_9 | ~spl28_10 | ~spl28_48)),
% 0.65/0.43    inference(forward_demodulation,[],[f2256,f2187])).
% 0.65/0.43  thf(f2258,plain,(
% 0.65/0.43    ( ! [X2 : $i] : (($false = ((sK2 @ (sK25 @ X2))))) ) | (~spl28_9 | ~spl28_10 | ~spl28_48)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2257])).
% 0.65/0.43  thf(f2259,plain,(
% 0.65/0.43    ($true = $false) | (~spl28_8 | ~spl28_9 | ~spl28_10 | ~spl28_48)),
% 0.65/0.43    inference(forward_demodulation,[],[f2258,f2196])).
% 0.65/0.43  thf(f2260,plain,(
% 0.65/0.43    $false | (~spl28_8 | ~spl28_9 | ~spl28_10 | ~spl28_48)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2259])).
% 0.65/0.43  thf(f2261,plain,(
% 0.65/0.43    ~spl28_8 | ~spl28_9 | ~spl28_10 | ~spl28_48),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2260])).
% 0.65/0.43  thf(f2262,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($false = ((sK2 @ X0)))) ) | ~spl28_7),
% 0.65/0.43    inference(constrained_superposition,[],[f1687,f50])).
% 0.65/0.43  thf(f2272,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($true != ((irel @ sK3 @ X0)))) ) | spl28_1),
% 0.65/0.43    inference(constrained_superposition,[],[f1660,f50])).
% 0.65/0.43  thf(f2291,plain,(
% 0.65/0.43    $false | (~spl28_7 | spl28_26)),
% 0.65/0.43    inference(forward_subsumption_resolution,[],[f1947,f2262])).
% 0.65/0.43  thf(f2292,plain,(
% 0.65/0.43    ~spl28_7 | spl28_26),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2291])).
% 0.65/0.43  thf(f2299,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($true = ((irel @ sK9 @ X0)))) ) | ~spl28_6),
% 0.65/0.43    inference(constrained_superposition,[],[f1682,f50])).
% 0.65/0.43  thf(f2319,plain,(
% 0.65/0.43    ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X0 @ X1)))) ) | ~spl28_6),
% 0.65/0.43    inference(constrained_superposition,[],[f2299,f50])).
% 0.65/0.43  thf(f2326,plain,(
% 0.65/0.43    ($true != $true) | spl28_1),
% 0.65/0.43    inference(constrained_superposition,[],[f2272,f69])).
% 0.65/0.43  thf(f2333,plain,(
% 0.65/0.43    $false | spl28_1),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2326])).
% 0.65/0.43  thf(f2334,plain,(
% 0.65/0.43    spl28_1),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2333])).
% 0.65/0.43  thf(f2344,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($true = $false) | ($false = ((irel @ sK9 @ X1)))) ) | (~spl28_5 | ~spl28_24)),
% 0.65/0.43    inference(forward_demodulation,[],[f1677,f2100])).
% 0.65/0.43  thf(f2345,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($false = ((irel @ sK9 @ X1)))) ) | (~spl28_5 | ~spl28_24)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2344])).
% 0.65/0.43  thf(f2346,plain,(
% 0.65/0.43    ($true = $false) | (~spl28_5 | ~spl28_6 | ~spl28_24)),
% 0.65/0.43    inference(forward_demodulation,[],[f2345,f2319])).
% 0.65/0.43  thf(f2347,plain,(
% 0.65/0.43    $false | (~spl28_5 | ~spl28_6 | ~spl28_24)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2346])).
% 0.65/0.43  thf(f2348,plain,(
% 0.65/0.43    ~spl28_5 | ~spl28_6 | ~spl28_24),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2347])).
% 0.65/0.43  thf(f2349,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($true = $false) | ($false = ((irel @ sK5 @ X1)))) ) | (~spl28_7 | ~spl28_15)),
% 0.65/0.43    inference(forward_demodulation,[],[f1777,f2262])).
% 0.65/0.43  thf(f2350,plain,(
% 0.65/0.43    ( ! [X1 : $i] : (($false = ((irel @ sK5 @ X1)))) ) | (~spl28_7 | ~spl28_15)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2349])).
% 0.65/0.43  thf(f2351,plain,(
% 0.65/0.43    ($true = $false) | (~spl28_6 | ~spl28_7 | ~spl28_15)),
% 0.65/0.43    inference(forward_demodulation,[],[f2350,f2319])).
% 0.65/0.43  thf(f2352,plain,(
% 0.65/0.43    $false | (~spl28_6 | ~spl28_7 | ~spl28_15)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2351])).
% 0.65/0.43  thf(f2353,plain,(
% 0.65/0.43    ~spl28_6 | ~spl28_7 | ~spl28_15),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2352])).
% 0.65/0.43  thf(f2356,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($true != ((irel @ X0 @ sK6)))) ) | spl28_6),
% 0.65/0.43    inference(constrained_superposition,[],[f1681,f50])).
% 0.65/0.43  thf(f2382,plain,(
% 0.65/0.43    ( ! [X0 : $i] : (($false != ((sK2 @ X0)))) ) | spl28_7),
% 0.65/0.43    inference(constrained_superposition,[],[f1686,f50])).
% 0.65/0.43  thf(f2388,plain,(
% 0.65/0.43    ( ! [X2 : $i] : (($true = $false) | ($false = ((irel @ sK11 @ X2)))) ) | (~spl28_16 | ~spl28_24)),
% 0.65/0.43    inference(forward_demodulation,[],[f1781,f2100])).
% 0.65/0.43  thf(f2389,plain,(
% 0.65/0.43    ( ! [X2 : $i] : (($false = ((irel @ sK11 @ X2)))) ) | (~spl28_16 | ~spl28_24)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2388])).
% 0.65/0.43  thf(f2418,plain,(
% 0.65/0.43    ($true = $false) | (~spl28_6 | ~spl28_16 | ~spl28_24)),
% 0.65/0.43    inference(forward_demodulation,[],[f2389,f2319])).
% 0.65/0.43  thf(f2419,plain,(
% 0.65/0.43    $false | (~spl28_6 | ~spl28_16 | ~spl28_24)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2418])).
% 0.65/0.43  thf(f2420,plain,(
% 0.65/0.43    ~spl28_6 | ~spl28_16 | ~spl28_24),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2419])).
% 0.65/0.43  thf(f2468,plain,(
% 0.65/0.43    ($true != $true) | (~spl28_3 | spl28_6)),
% 0.65/0.43    inference(constrained_superposition,[],[f2356,f2110])).
% 0.65/0.43  thf(f2469,plain,(
% 0.65/0.43    $false | (~spl28_3 | spl28_6)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2468])).
% 0.65/0.43  thf(f2470,plain,(
% 0.65/0.43    ~spl28_3 | spl28_6),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2469])).
% 0.65/0.43  thf(f2485,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK3 @ X3))) | ($false = ((sK2 @ (sK27 @ X3)))) | ($false = ((irel @ X3 @ X1)))) ) | (~spl28_24 | ~spl28_50)),
% 0.65/0.43    inference(forward_demodulation,[],[f2098,f2100])).
% 0.65/0.43  thf(f2486,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X3))) | ($false = ((sK2 @ (sK27 @ X3)))) | ($false = ((irel @ X3 @ X1)))) ) | (~spl28_24 | ~spl28_50)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2485])).
% 0.65/0.43  thf(f2493,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($true = $false) | ($false = ((sK2 @ (sK27 @ X3)))) | ($false = ((irel @ X3 @ X1)))) ) | (~spl28_3 | ~spl28_24 | ~spl28_50)),
% 0.65/0.43    inference(forward_demodulation,[],[f2486,f2110])).
% 0.65/0.43  thf(f2494,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($false = ((sK2 @ (sK27 @ X3)))) | ($false = ((irel @ X3 @ X1)))) ) | (~spl28_3 | ~spl28_24 | ~spl28_50)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2493])).
% 0.65/0.43  thf(f2541,plain,(
% 0.65/0.43    ( ! [X3 : $i,X1 : $i] : (($false = ((irel @ X3 @ X1)))) ) | (~spl28_3 | spl28_7 | ~spl28_24 | ~spl28_50)),
% 0.65/0.43    inference(forward_subsumption_resolution,[],[f2494,f2382])).
% 0.65/0.43  thf(f2543,plain,(
% 0.65/0.43    ($true = $false) | (~spl28_3 | ~spl28_6 | spl28_7 | ~spl28_24 | ~spl28_50)),
% 0.65/0.43    inference(constrained_superposition,[],[f2541,f2319])).
% 0.65/0.43  thf(f2547,plain,(
% 0.65/0.43    $false | (~spl28_3 | ~spl28_6 | spl28_7 | ~spl28_24 | ~spl28_50)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2543])).
% 0.65/0.43  thf(f2548,plain,(
% 0.65/0.43    ~spl28_3 | ~spl28_6 | spl28_7 | ~spl28_24 | ~spl28_50),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2547])).
% 0.65/0.43  thf(f2550,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($true = ((sK1 @ X4))) | ($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4)))) ) | (spl28_7 | ~spl28_48)),
% 0.65/0.43    inference(forward_subsumption_resolution,[],[f2091,f2382])).
% 0.65/0.43  thf(f2551,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($true = $false) | ($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4)))) ) | (spl28_7 | ~spl28_24 | ~spl28_48)),
% 0.65/0.43    inference(forward_demodulation,[],[f2550,f2100])).
% 0.65/0.43  thf(f2552,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($false = ((irel @ sK3 @ X2))) | ($false = ((irel @ X2 @ X4)))) ) | (spl28_7 | ~spl28_24 | ~spl28_48)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2551])).
% 0.65/0.43  thf(f2553,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($true = $false) | ($false = ((irel @ X2 @ X4)))) ) | (~spl28_6 | spl28_7 | ~spl28_24 | ~spl28_48)),
% 0.65/0.43    inference(forward_demodulation,[],[f2552,f2319])).
% 0.65/0.43  thf(f2554,plain,(
% 0.65/0.43    ( ! [X2 : $i,X4 : $i] : (($false = ((irel @ X2 @ X4)))) ) | (~spl28_6 | spl28_7 | ~spl28_24 | ~spl28_48)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2553])).
% 0.65/0.43  thf(f2556,plain,(
% 0.65/0.43    ($true = $false) | (~spl28_6 | spl28_7 | ~spl28_24 | ~spl28_48)),
% 0.65/0.43    inference(constrained_superposition,[],[f2554,f2319])).
% 0.65/0.43  thf(f2560,plain,(
% 0.65/0.43    $false | (~spl28_6 | spl28_7 | ~spl28_24 | ~spl28_48)),
% 0.65/0.43    inference(trivial_inequality_removal,[],[f2556])).
% 0.65/0.43  thf(f2561,plain,(
% 0.65/0.43    ~spl28_6 | spl28_7 | ~spl28_24 | ~spl28_48),
% 0.65/0.43    inference(avatar_contradiction_clause,[],[f2560])).
% 0.65/0.43  cnf(s22, plain, spl28_3 | spl28_5 | spl28_8 | spl28_11, inference(sat_conversion,[],[f1720])).
% 0.65/0.43  cnf(s23, plain, spl28_3 | spl28_6 | spl28_8 | spl28_11, inference(sat_conversion,[],[f1721])).
% 0.65/0.43  cnf(s26, plain, spl28_3 | spl28_5 | spl28_9 | spl28_11, inference(sat_conversion,[],[f1724])).
% 0.65/0.43  cnf(s27, plain, spl28_3 | spl28_6 | spl28_9 | spl28_11, inference(sat_conversion,[],[f1725])).
% 0.65/0.43  cnf(s30, plain, spl28_3 | spl28_5 | spl28_10 | spl28_11, inference(sat_conversion,[],[f1728])).
% 0.65/0.43  cnf(s31, plain, spl28_3 | spl28_6 | spl28_10 | spl28_11, inference(sat_conversion,[],[f1729])).
% 0.65/0.43  cnf(s86, plain, spl28_8 | spl28_11 | spl28_15 | spl28_16, inference(sat_conversion,[],[f1806])).
% 0.65/0.43  cnf(s90, plain, spl28_9 | spl28_11 | spl28_15 | spl28_16, inference(sat_conversion,[],[f1810])).
% 0.65/0.43  cnf(s94, plain, spl28_10 | spl28_11 | spl28_15 | spl28_16, inference(sat_conversion,[],[f1814])).
% 0.65/0.43  cnf(s256, plain, spl28_7 | spl28_10 | spl28_24 | spl28_26, inference(sat_conversion,[],[f2011])).
% 0.65/0.43  cnf(s260, plain, spl28_30 | spl28_32, inference(sat_conversion,[],[f2033])).
% 0.65/0.43  cnf(s272, plain, spl28_48 | spl28_50, inference(sat_conversion,[],[f2099])).
% 0.65/0.43  cnf(s273, plain, ~spl28_1 | ~spl28_11 | ~spl28_24, inference(sat_conversion,[],[f2128])).
% 0.65/0.43  cnf(s275, plain, ~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_30, inference(sat_conversion,[],[f2153])).
% 0.65/0.43  cnf(s277, plain, ~spl28_1 | spl28_24 | ~spl28_26 | ~spl28_32, inference(sat_conversion,[],[f2166])).
% 0.65/0.43  cnf(s278, plain, ~spl28_10 | spl28_24, inference(sat_conversion,[],[f2169])).
% 0.65/0.43  cnf(s286, plain, ~spl28_8 | ~spl28_9 | ~spl28_10 | ~spl28_50, inference(sat_conversion,[],[f2251])).
% 0.65/0.43  cnf(s287, plain, ~spl28_8 | ~spl28_9 | ~spl28_10 | ~spl28_48, inference(sat_conversion,[],[f2261])).
% 0.65/0.43  cnf(s289, plain, ~spl28_7 | spl28_26, inference(sat_conversion,[],[f2292])).
% 0.65/0.43  cnf(s292, plain, spl28_1, inference(sat_conversion,[],[f2334])).
% 0.65/0.43  cnf(s293, plain, ~spl28_5 | ~spl28_6 | ~spl28_24, inference(sat_conversion,[],[f2348])).
% 0.65/0.43  cnf(s294, plain, ~spl28_6 | ~spl28_7 | ~spl28_15, inference(sat_conversion,[],[f2353])).
% 0.65/0.43  cnf(s297, plain, ~spl28_6 | ~spl28_16 | ~spl28_24, inference(sat_conversion,[],[f2420])).
% 0.65/0.43  cnf(s298, plain, ~spl28_3 | spl28_6, inference(sat_conversion,[],[f2470])).
% 0.65/0.43  cnf(s307, plain, ~spl28_3 | ~spl28_6 | spl28_7 | ~spl28_24 | ~spl28_50, inference(sat_conversion,[],[f2548])).
% 0.65/0.43  cnf(s309, plain, ~spl28_6 | spl28_7 | ~spl28_24 | ~spl28_48, inference(sat_conversion,[],[f2561])).
% 0.65/0.43  cnf(s310, plain, spl28_24 | ~spl28_26 | ~spl28_32, inference(rat,[],[s277,s292])).
% 0.65/0.43  cnf(s312, plain, spl28_24 | ~spl28_26 | ~spl28_30, inference(rat,[],[s275,s292])).
% 0.65/0.43  cnf(s314, plain, ~spl28_11 | ~spl28_24, inference(rat,[],[s273,s292])).
% 0.65/0.43  cnf(s315, plain, ~spl28_26 | spl28_24, inference(rat,[],[s260,s310,s312])).
% 0.65/0.43  cnf(s316, plain, spl28_24, inference(rat,[],[s256,s289,s315,s278])).
% 0.65/0.43  cnf(s317, plain, ~spl28_11, inference(rat,[],[s314,s316])).
% 0.65/0.43  cnf(s318, plain, ~spl28_8 | ~spl28_9 | ~spl28_10, inference(rat,[],[s272,s286,s287])).
% 0.65/0.43  cnf(s320, plain, spl28_7 | ~spl28_3, inference(rat,[],[s272,s307,s309,s298,s316])).
% 0.65/0.43  cnf(s321, plain, spl28_15 | spl28_16, inference(rat,[],[s318,s86,s90,s94,s317])).
% 0.65/0.43  cnf(s322, plain, ~spl28_3, inference(rat,[],[s321,s294,s320,s297,s298,s316])).
% 0.65/0.43  cnf(s324, plain, spl28_8, inference(rat,[],[s293,s22,s23,s316,s322,s317])).
% 0.65/0.43  cnf(s325, plain, spl28_9, inference(rat,[],[s293,s26,s27,s316,s322,s317])).
% 0.65/0.43  cnf(s326, plain, ~spl28_10, inference(rat,[],[s318,s324,s325])).
% 0.65/0.43  cnf(s328, plain, spl28_6, inference(rat,[],[s31,s317,s322,s326])).
% 0.65/0.43  cnf(s329, plain, spl28_5, inference(rat,[],[s30,s317,s322,s326])).
% 0.65/0.43  cnf(s334, plain, $false, inference(rat,[],[s293,s316,s328,s329])).
% 0.65/0.43  thf(f2563,plain,(
% 0.65/0.43    $false),
% 0.65/0.43    inference(avatar_sat_refutation,[],[s334])).
% 0.65/0.43  % SZS output end Proof for theBenchmark
% 0.65/0.43  % (3716997)------------------------------
% 0.65/0.43  % (3716997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.65/0.43  % (3716997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.43  % (3716997)CaDiCaL version: 2.1.3
% 0.65/0.43  % (3716997)Termination reason: Refutation
% 0.65/0.43  % (3716997)Time elapsed: 0.044 s
% 0.65/0.43  % (3716997)Peak memory usage: 14 MB
% 0.65/0.43  % (3716997)Instructions burned: 147 (million)
% 0.65/0.43  % (3716975)Success in time 0.168 s
% 0.65/0.43  % Vampire exiting
%------------------------------------------------------------------------------