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

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : SWX179^1 : TPTP v9.3.1. Released v9.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT

% Computer : n016.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.90s 0.39s
% Output   : Refutation 0.90s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SWX179^1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19  % Computer : n016.cluster.edu
% 0.09/0.19  % Model    : x86_64 x86_64
% 0.09/0.19  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19  % Memory   : 8046.5625MB
% 0.09/0.19  % OS       : Linux 6.8.0-71-generic
% 0.09/0.19  % CPULimit : 300
% 0.09/0.19  % WCLimit  : 300
% 0.09/0.19  % DateTime : Tue Sep 29 16:14:49 UTC 2026
% 0.09/0.19  % CPUTime  : 
% 0.09/0.19  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22  Running first-order model finding
% 0.09/0.22  Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.90/0.39  % (540431)Will run a generic schedule for satisfiability detection.
% 0.90/0.39  % (540436)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3053211403_2999 on theBenchmark for (2999ds/0Mi)
% 0.90/0.39  % Exception at run slice level
% 0.90/0.39  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.90/0.39  % (540437)% WARNING: option uhcvi not known.
% 0.90/0.39  % (540437)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2335611841:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.90/0.39  % (540438)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3998643676:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.90/0.39  % (540439)dis+10_1_sil=32000:sp=arity:random_seed=2105383089:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.90/0.39  % (540440)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2674195307:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.90/0.39  % (540437)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.90/0.39  % (540440)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.90/0.39  % (540437)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.90/0.39  % (540444)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1564256090:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.90/0.39  % Exception at run slice level
% 0.90/0.39  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.90/0.39  % (540442)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2261589027:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.90/0.39  % (540441)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3993468259:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.90/0.39  % (540451)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3340513586:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.90/0.39  % (540439)Instruction limit reached! 
% 0.90/0.39  % (540439)------------------------------
% 0.90/0.39  % (540439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.90/0.39  % (540439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.90/0.39  % (540439)CaDiCaL version: 2.1.3
% 0.90/0.39  % (540439)Termination reason: Instruction limit
% 0.90/0.39  % (540439)Termination phase: Saturation
% 0.90/0.39  % (540439)Time elapsed: 0.048 s
% 0.90/0.39  % (540439)Peak memory usage: 12 MB
% 0.90/0.39  % (540439)Instructions burned: 103 (million)
% 0.90/0.39  % (540440)Instruction limit reached! 
% 0.90/0.39  % (540440)------------------------------
% 0.90/0.39  % (540440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.90/0.39  % (540440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.90/0.39  % (540440)CaDiCaL version: 2.1.3
% 0.90/0.39  % (540440)Termination reason: Instruction limit
% 0.90/0.39  % (540440)Termination phase: Saturation
% 0.90/0.39  % (540440)Time elapsed: 0.052 s
% 0.90/0.39  % (540440)Peak memory usage: 13 MB
% 0.90/0.39  % (540440)Instructions burned: 117 (million)
% 0.90/0.39  % (540451)Instruction limit reached! 
% 0.90/0.39  % (540451)------------------------------
% 0.90/0.39  % (540451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.90/0.39  % (540451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.90/0.39  % (540451)CaDiCaL version: 2.1.3
% 0.90/0.39  % (540451)Termination reason: Instruction limit
% 0.90/0.39  % (540451)Termination phase: Saturation
% 0.90/0.39  % (540451)Time elapsed: 0.033 s
% 0.90/0.39  % (540451)Peak memory usage: 13 MB
% 0.90/0.39  % (540451)Instructions burned: 134 (million)
% 0.90/0.39  % (540456)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4138086573:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 0.90/0.39  % (540441)Instruction limit reached! 
% 0.90/0.39  % (540441)------------------------------
% 0.90/0.39  % (540441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.90/0.39  % (540441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.90/0.39  % (540441)CaDiCaL version: 2.1.3
% 0.90/0.39  % (540441)Termination reason: Instruction limit
% 0.90/0.39  % (540441)Termination phase: Saturation
% 0.90/0.39  % (540441)Time elapsed: 0.058 s
% 0.90/0.39  % (540441)Peak memory usage: 12 MB
% 0.90/0.39  % (540441)Instructions burned: 131 (million)
% 0.90/0.39  % (540454)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=4189895841:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.90/0.39  % (540454)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.90/0.39  % (540454)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.90/0.39  % (540455)ott-21_1_sil=16000:fs=off:random_seed=291089575:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.90/0.39  % (540442)Instruction limit reached! 
% 0.90/0.39  % (540442)------------------------------
% 0.90/0.39  % (540442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.90/0.39  % (540442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.90/0.39  % (540442)CaDiCaL version: 2.1.3
% 0.90/0.39  % (540442)Termination reason: Instruction limit
% 0.90/0.39  % (540442)Termination phase: Saturation
% 0.90/0.39  % (540442)Time elapsed: 0.081 s
% 0.90/0.39  % (540442)Peak memory usage: 13 MB
% 0.90/0.39  % (540442)Instructions burned: 160 (million)
% 0.90/0.39  % (540456) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-540431-540456"...
% 0.90/0.39  % (540459)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3262225858:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 0.90/0.39  % (540461)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2347188008:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 0.90/0.39  % Exception at run slice level
% 0.90/0.39  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.90/0.39  % (540454) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-540431-540454"...
% 0.90/0.39  % (540456)...printing done.
% 0.90/0.39  % (540456)Refutation found. Thanks to Tanya!
% 0.90/0.39  % SZS status Theorem for theBenchmark
% 0.90/0.39  % SZS output start Proof for theBenchmark
% 0.90/0.39  thf(type_def_5, type, unsorted: $tType).
% 0.90/0.39  thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.90/0.39  thf(type_def_7, type, d_unsorted: $tType).
% 0.90/0.39  thf(func_def_0, type, irel: ($i > $i > $o)).
% 0.90/0.39  thf(func_def_1, type, mnot: (($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_2, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_3, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_4, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_5, type, mbox_s4: (($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_6, type, iatom: (($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_7, type, inot: (($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_8, type, itrue: ($i > $o)).
% 0.90/0.39  thf(func_def_9, type, ifalse: ($i > $o)).
% 0.90/0.39  thf(func_def_10, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_11, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_12, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_13, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_14, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_15, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.90/0.39  thf(func_def_16, type, ivalid: (($i > $o) > $o)).
% 0.90/0.39  thf(func_def_17, type, isatisfiable: (($i > $o) > $o)).
% 0.90/0.39  thf(func_def_18, type, icountersatisfiable: (($i > $o) > $o)).
% 0.90/0.39  thf(func_def_19, type, iinvalid: (($i > $o) > $o)).
% 0.90/0.39  thf(func_def_20, type, d2unsorted: (d_unsorted > $i)).
% 0.90/0.39  thf(func_def_21, type, d_unsorted_0: d_unsorted).
% 0.90/0.39  thf(func_def_23, type, vNOT: ($o > $o)).
% 0.90/0.39  thf(func_def_24, type, db1: !>[X0: $tType]:(X0)).
% 0.90/0.39  thf(func_def_25, type, db0: !>[X0: $tType]:(X0)).
% 0.90/0.39  thf(func_def_26, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.90/0.39  thf(func_def_27, type, vOR: ($o > $o > $o)).
% 0.90/0.39  thf(func_def_28, type, db2: !>[X0: $tType]:(X0)).
% 0.90/0.39  thf(func_def_29, type, vAND: ($o > $o > $o)).
% 0.90/0.39  thf(func_def_30, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.90/0.39  thf(func_def_31, type, db3: !>[X0: $tType]:(X0)).
% 0.90/0.39  thf(func_def_32, type, db5: !>[X0: $tType]:(X0)).
% 0.90/0.39  thf(func_def_33, type, db4: !>[X0: $tType]:(X0)).
% 0.90/0.39  thf(func_def_34, type, db8: !>[X0: $tType]:(X0)).
% 0.90/0.39  thf(func_def_35, type, db6: !>[X0: $tType]:(X0)).
% 0.90/0.39  thf(func_def_36, type, db7: !>[X0: $tType]:(X0)).
% 0.90/0.39  thf(func_def_39, type, sK0: ($i > d_unsorted)).
% 0.90/0.39  thf(func_def_41, type, sK2: ($i > $o)).
% 0.90/0.39  thf(func_def_42, type, sK3: ($i > $o)).
% 0.90/0.39  thf(func_def_44, type, sK5: ($i > $i)).
% 0.90/0.39  thf(func_def_45, type, sK6: ($i > $i)).
% 0.90/0.39  thf(func_def_46, type, sK7: ($i > $i)).
% 0.90/0.39  thf(func_def_47, type, sK8: ($i > $i)).
% 0.90/0.39  thf(func_def_48, type, sK9: ($i > $i)).
% 0.90/0.39  thf(func_def_49, type, sK10: ($i > $i)).
% 0.90/0.39  thf(func_def_50, type, sK11: ($i > $i)).
% 0.90/0.39  thf(func_def_51, type, sK12: ($i > $i)).
% 0.90/0.39  thf(func_def_52, type, sK13: ($i > $i)).
% 0.90/0.39  thf(func_def_53, type, sK14: ($i > $i)).
% 0.90/0.39  thf(f1,axiom,(
% 0.90/0.39    ~(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.90/0.39    file('/export/starexec/sandbox/benchmark/theBenchmark.p',lcl696_1)).
% 0.90/0.39  thf(f2,conjecture,(
% 0.90/0.39    (ixor = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((inot @ (iequiv @ X0 @ X1)))))),
% 0.90/0.39    file('/export/starexec/sandbox/benchmark/theBenchmark.p',ixor)).
% 0.90/0.39  thf(f3,negated_conjecture,(
% 0.90/0.39    ~ (ixor = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((inot @ (iequiv @ X0 @ X1)))))),
% 0.90/0.39    inference(negated_conjecture,[status(cth)],[f2])).
% 0.90/0.39  thf(f4,plain,(
% 0.90/0.39    ~(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.90/0.39    inference(rectify,[],[f1])).
% 0.90/0.39  thf(f5,plain,(
% 0.90/0.39    ~ (((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.90/0.39    inference(fool_elimination,[],[f4])).
% 0.90/0.39  thf(f6,plain,(
% 0.90/0.39    ~ (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (inot @ (iequiv @ Y0 @ Y1))))))),
% 0.90/0.39    inference(fool_elimination,[],[f3])).
% 0.90/0.39  thf(f7,plain,(
% 0.90/0.39    ~ (((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.90/0.39    inference(rectify,[],[f5])).
% 0.90/0.39  thf(f8,plain,(
% 0.90/0.39    (((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.90/0.39    inference(flattening,[],[f7])).
% 0.90/0.39  thf(f9,plain,(
% 0.90/0.39    (ixor != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (inot @ (iequiv @ Y0 @ Y1))))))),
% 0.90/0.39    inference(flattening,[],[f6])).
% 0.90/0.39  thf(f10,plain,(
% 0.90/0.39    (((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.90/0.39    inference(ennf_transformation,[],[f8])).
% 0.90/0.39  thf(f11,plain,(
% 0.90/0.39    (((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.90/0.39    inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X4,sK0 @ X3)],[f10])).
% 0.90/0.39  thf(f12,plain,(
% 0.90/0.39    ( ! [X3 : $i] : ((((d2unsorted @ (sK0 @ X3))) = X3)) )),
% 0.90/0.39    inference(cnf_transformation,[],[f11])).
% 0.90/0.39  thf(f13,plain,(
% 0.90/0.39    ( ! [X2 : d_unsorted] : ((d_unsorted_0 = X2)) )),
% 0.90/0.39    inference(cnf_transformation,[],[f11])).
% 0.90/0.39  thf(f21,plain,(
% 0.90/0.39    (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))))),
% 0.90/0.39    inference(cnf_transformation,[],[f11])).
% 0.90/0.39  thf(f26,plain,(
% 0.90/0.39    (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.90/0.39    inference(cnf_transformation,[],[f11])).
% 0.90/0.39  thf(f27,plain,(
% 0.90/0.39    (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)))))))))))))))))))))),
% 0.90/0.39    inference(cnf_transformation,[],[f11])).
% 0.90/0.39  thf(f35,plain,(
% 0.90/0.39    (ixor != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (inot @ (iequiv @ Y0 @ Y1))))))),
% 0.90/0.39    inference(cnf_transformation,[],[f9])).
% 0.90/0.39  thf(f38,plain,(
% 0.90/0.39    ((^[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)))))))))))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y2 @ Y4)))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((((~ (irel @ Y4 @ Y6)) | (~ (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y6 @ Y7)) | (Y2 @ Y7)))))) | (~ (irel @ Y6 @ Y5))) | (Y3 @ Y5)))))) & (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((((~ (irel @ Y4 @ Y6)) | (~ (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y6 @ Y7)) | (Y3 @ Y7)))))) | (~ (irel @ Y6 @ Y5))) | (Y2 @ Y5)))))))))))) @ Y0 @ Y1))))))),
% 0.90/0.39    inference(definition_unfolding,[],[f35,f27,f21,f26])).
% 0.90/0.39  thf(f39,plain,(
% 0.90/0.39    ((^[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)))))))))))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | ((!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((~ (irel @ Y3 @ Y5)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y0 @ Y6)))))) | (~ (irel @ Y5 @ Y4))) | (Y1 @ Y4)))))) & (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((~ (irel @ Y3 @ Y5)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y1 @ Y6)))))) | (~ (irel @ Y5 @ Y4))) | (Y0 @ Y4)))))))))))))))))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f38])).
% 0.90/0.39  thf(f84,plain,(
% 0.90/0.39    ( ! [X3 : $i] : ((((d2unsorted @ d_unsorted_0)) = X3)) )),
% 0.90/0.39    inference(forward_demodulation,[],[f12,f13])).
% 0.90/0.39  thf(f88,plain,(
% 0.90/0.39    ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) )),
% 0.90/0.39    inference(constrained_superposition,[],[f84,f84])).
% 0.90/0.39  thf(f118,plain,(
% 0.90/0.39    ((((^[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)))))))))))))))))))) @ sK2)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | ((!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((~ (irel @ Y3 @ Y5)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y0 @ Y6)))))) | (~ (irel @ Y5 @ Y4))) | (Y1 @ Y4)))))) & (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((~ (irel @ Y3 @ Y5)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y5 @ Y6)) | (Y1 @ Y6)))))) | (~ (irel @ Y5 @ Y4))) | (Y0 @ Y4)))))))))))))))) @ sK2)))),
% 0.90/0.39    inference(negative_extensionality,[],[f39])).
% 0.90/0.39  thf(f119,plain,(
% 0.90/0.39    ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y1 @ Y6)) | (((((~ (irel @ Y6 @ Y5)) | (~ (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y5 @ Y7)) | (sK2 @ Y7)))))) | (~ (irel @ Y5 @ Y4))) | (Y0 @ Y4)) & ((((~ (irel @ Y6 @ Y3)) | (~ (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y3 @ Y7)) | (Y0 @ Y7)))))) | (~ (irel @ Y3 @ Y2))) | (sK2 @ Y2)))))))))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y0 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (sK2 @ Y3)))))))))))))))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f118])).
% 0.90/0.39  thf(f122,plain,(
% 0.90/0.39    ((((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y1 @ Y6)) | (((((~ (irel @ Y6 @ Y5)) | (~ (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y5 @ Y7)) | (sK2 @ Y7)))))) | (~ (irel @ Y5 @ Y4))) | (Y0 @ Y4)) & ((((~ (irel @ Y6 @ Y3)) | (~ (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y3 @ Y7)) | (Y0 @ Y7)))))) | (~ (irel @ Y3 @ Y2))) | (sK2 @ Y2)))))))))))))))))) @ sK3)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (Y0 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y4 @ Y3))) | (sK2 @ Y3)))))))))))))) @ sK3)))),
% 0.90/0.39    inference(negative_extensionality,[],[f119])).
% 0.90/0.39  thf(f123,plain,(
% 0.90/0.39    ((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y0 @ Y5)) | (((((~ (irel @ Y5 @ Y4)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y4 @ Y6)) | (sK2 @ Y6)))))) | (~ (irel @ Y4 @ Y3))) | (sK3 @ Y3)) & ((((~ (irel @ Y5 @ Y2)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y2 @ Y6)) | (sK3 @ Y6)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))))))))))))) != (^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)))))) & (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y3 @ Y2))) | (sK2 @ Y2)))))))))))))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f122])).
% 0.90/0.39  thf(f124,plain,(
% 0.90/0.39    ((((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y0 @ Y5)) | (((((~ (irel @ Y5 @ Y4)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y4 @ Y6)) | (sK2 @ Y6)))))) | (~ (irel @ Y4 @ Y3))) | (sK3 @ Y3)) & ((((~ (irel @ Y5 @ Y2)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y2 @ Y6)) | (sK3 @ Y6)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))))))))))))) @ sK4)) != (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)))))) & (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y3 @ Y2))) | (sK2 @ Y2)))))))))))) @ sK4)))),
% 0.90/0.39    inference(negative_extensionality,[],[f123])).
% 0.90/0.39  thf(f125,plain,(
% 0.90/0.39    ($true = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y0 @ Y5)) | (((((~ (irel @ Y5 @ Y4)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y4 @ Y6)) | (sK2 @ Y6)))))) | (~ (irel @ Y4 @ Y3))) | (sK3 @ Y3)) & ((((~ (irel @ Y5 @ Y2)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y2 @ Y6)) | (sK3 @ Y6)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))))))))))))) @ sK4))) | ($true = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)))))) & (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y3 @ Y2))) | (sK2 @ Y2)))))))))))) @ sK4)))),
% 0.90/0.39    inference(xor_proxy_clausification,[],[f124])).
% 0.90/0.39  thf(f126,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y0 @ Y5)) | (((((~ (irel @ Y5 @ Y4)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y4 @ Y6)) | (sK2 @ Y6)))))) | (~ (irel @ Y4 @ Y3))) | (sK3 @ Y3)) & ((((~ (irel @ Y5 @ Y2)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (irel @ Y2 @ Y6)) | (sK3 @ Y6)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))))))))))))) @ sK4))) | ($false = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)))))) & (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((~ (irel @ Y1 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y3 @ Y2))) | (sK2 @ Y2)))))))))))) @ sK4)))),
% 0.90/0.39    inference(xor_proxy_clausification,[],[f124])).
% 0.90/0.39  thf(f127,plain,(
% 0.90/0.39    ($false = ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ sK4 @ Y4)) | (((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)) & ((((~ (irel @ Y4 @ Y1)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y1 @ Y5)) | (sK3 @ Y5)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))))))))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))))))))))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f126])).
% 0.90/0.39  thf(f128,plain,(
% 0.90/0.39    ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ sK4 @ Y4)) | (((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)) & ((((~ (irel @ Y4 @ Y1)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y1 @ Y5)) | (sK3 @ Y5)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)))))))))))))))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))))))))))),
% 0.90/0.39    inference(not_proxy_clausification,[],[f127])).
% 0.90/0.39  thf(f129,plain,(
% 0.90/0.39    ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ sK4 @ Y4)) | (((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)) & ((((~ (irel @ Y4 @ Y1)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y1 @ Y5)) | (sK3 @ Y5)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))))) @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))))))))))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f128])).
% 0.90/0.39  thf(f130,plain,(
% 0.90/0.39    ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ sK4 @ Y4)) | (((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)) & ((((~ (irel @ Y4 @ Y1)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y1 @ Y5)) | (sK3 @ Y5)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))))) @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1))))))))))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f129])).
% 0.90/0.39  thf(f131,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ sK4 @ Y4)) | (((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)) & ((((~ (irel @ Y4 @ Y1)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y1 @ Y5)) | (sK3 @ Y5)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))))) @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1))))))))) @ X2)))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f130])).
% 0.90/0.39  thf(f132,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1)))))))))))))) | ($true = (((~ (irel @ sK4 @ X2)) | ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)))))) & (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f131])).
% 0.90/0.39  thf(f133,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1))))))))))) @ X3))) | ($true = (((~ (irel @ sK4 @ X2)) | ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)))))) & (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f132])).
% 0.90/0.39  thf(f134,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1))))))))))) @ X3))) | ($true = (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)))))) & (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))) | ($true = ((~ (irel @ sK4 @ X2))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f133])).
% 0.90/0.39  thf(f135,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1))))))))))) @ X3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)))))))) | ($true = ((~ (irel @ sK4 @ X2))))) )),
% 0.90/0.39    inference(and_proxy_clausification,[],[f134])).
% 0.90/0.39  thf(f136,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1))))))))))) @ X3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)))))))) | ($true = ((~ (irel @ sK4 @ X2))))) )),
% 0.90/0.39    inference(and_proxy_clausification,[],[f134])).
% 0.90/0.39  thf(f137,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1))))))))))) @ X3))) | ($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0))))) @ X4))) | ($true = ((~ (irel @ sK4 @ X2))))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f136])).
% 0.90/0.39  thf(f138,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1))))))))))) @ X3))) | ($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0))))) @ X4))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f137])).
% 0.90/0.39  thf(f139,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ X3)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ X3 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1)))))))))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ X4))) | (sK3 @ X4)))))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f138])).
% 0.90/0.39  thf(f140,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ X3)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ X3 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))))) @ X5))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ X4))) | (sK3 @ X4)))))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f139])).
% 0.90/0.39  thf(f141,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ X3)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ X3 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))))) @ X5))) | ($true = (((^[Y0 : $i]: ((((~ (irel @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ X4))) | (sK3 @ X4))) @ X6))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f140])).
% 0.90/0.39  thf(f142,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1)))))))))) | ($true = (((((~ (irel @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X6 @ X4))) | (sK3 @ X4)))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f141])).
% 0.90/0.39  thf(f143,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = (((((~ (irel @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X6 @ X4))) | (sK3 @ X4)))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f142])).
% 0.90/0.39  thf(f144,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($true = ((((~ (irel @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X6 @ X4)))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f143])).
% 0.90/0.39  thf(f145,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($true = ((~ (irel @ X6 @ X4)))) | ($true = (((~ (irel @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f144])).
% 0.90/0.39  thf(f146,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($true = (((~ (irel @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f145])).
% 0.90/0.39  thf(f147,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK2 @ Y0))))))) | ($true = ((~ (irel @ X2 @ X6))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f146])).
% 0.90/0.39  thf(f148,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK2 @ Y0)))))) | ($true = ((~ (irel @ X2 @ X6))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f147])).
% 0.90/0.39  thf(f149,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK2 @ Y0))) @ (sK5 @ X6)))) | ($true = ((~ (irel @ X2 @ X6))))) )),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f148])).
% 0.90/0.39  thf(f150,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK2 @ Y0))) @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6)))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f149])).
% 0.90/0.39  thf(f151,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ X7)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X7 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ X7 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y0 @ X3)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X3 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1)))))))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = (((~ (irel @ X6 @ (sK5 @ X6))) | (sK2 @ (sK5 @ X6))))) | ($false = ((irel @ X2 @ X6)))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f150])).
% 0.90/0.39  thf(f152,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ X7)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X7 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ X7 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y0 @ X3)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X3 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))) @ X8))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = (((~ (irel @ X6 @ (sK5 @ X6))) | (sK2 @ (sK5 @ X6))))) | ($false = ((irel @ X2 @ X6)))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f151])).
% 0.90/0.39  thf(f153,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ X7)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X7 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ X7 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y0 @ X3)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X3 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))) @ X8))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6)))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f152])).
% 0.90/0.39  thf(f184,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((~ (irel @ sK4 @ X8)) | (((((~ (irel @ X8 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X7 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ X8 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1)))))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6)))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f153])).
% 0.90/0.39  thf(f185,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((((((~ (irel @ X8 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X7 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ X8 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($true = ((~ (irel @ sK4 @ X8))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f184])).
% 0.90/0.39  thf(f187,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((((~ (irel @ X8 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X7 @ X5))) | (sK3 @ X5)))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($true = ((~ (irel @ sK4 @ X8))))) )),
% 0.90/0.39    inference(and_proxy_clausification,[],[f185])).
% 0.90/0.39  thf(f188,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($true = ((~ (irel @ sK4 @ X8)))) | ($true = ((((~ (irel @ X8 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X7 @ X5)))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f187])).
% 0.90/0.39  thf(f189,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($true = ((((~ (irel @ X8 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X7 @ X5)))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f188])).
% 0.90/0.39  thf(f190,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($true = ((~ (irel @ X7 @ X5)))) | ($true = (((~ (irel @ X8 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f189])).
% 0.90/0.39  thf(f191,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($true = (((~ (irel @ X8 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f190])).
% 0.90/0.39  thf(f192,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0))))))) | ($true = ((~ (irel @ X8 @ X7))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f191])).
% 0.90/0.39  thf(f193,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0)))))) | ($true = ((~ (irel @ X8 @ X7))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f192])).
% 0.90/0.39  thf(f194,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($false = (((^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0))) @ (sK8 @ X7)))) | ($true = ((~ (irel @ X8 @ X7))))) )),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f193])).
% 0.90/0.39  thf(f195,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($false = (((^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0))) @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f194])).
% 0.90/0.39  thf(f196,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($false = (((~ (irel @ X7 @ (sK8 @ X7))) | (sK2 @ (sK8 @ X7))))) | ($false = ((irel @ X8 @ X7)))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f195])).
% 0.90/0.39  thf(f197,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($false = ((sK2 @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f196])).
% 0.90/0.39  thf(f212,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1))))))))))) @ X3))) | ($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))) @ X4))) | ($true = ((~ (irel @ sK4 @ X2))))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f135])).
% 0.90/0.39  thf(f213,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ X1))) | (sK2 @ X1))))))))))) @ X3))) | ($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))) @ X4))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f212])).
% 0.90/0.39  thf(f214,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ X3)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ X3 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1)))))))))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ Y0 @ X4))) | (sK2 @ X4)))))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f213])).
% 0.90/0.39  thf(f215,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ X3)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ X3 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))))) @ X5))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ Y0 @ X4))) | (sK2 @ X4)))))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f214])).
% 0.90/0.39  thf(f216,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ X3)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ X3 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))))) @ X5))) | ($true = (((^[Y0 : $i]: ((((~ (irel @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ Y0 @ X4))) | (sK2 @ X4))) @ X6))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f215])).
% 0.90/0.39  thf(f217,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1)))))))))) | ($true = (((((~ (irel @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ X6 @ X4))) | (sK2 @ X4)))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f216])).
% 0.90/0.39  thf(f218,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = (((((~ (irel @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ X6 @ X4))) | (sK2 @ X4)))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f217])).
% 0.90/0.39  thf(f219,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($true = ((((~ (irel @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ X6 @ X4)))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f218])).
% 0.90/0.39  thf(f220,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($true = ((~ (irel @ X6 @ X4)))) | ($true = (((~ (irel @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK3 @ Y0))))))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f219])).
% 0.90/0.39  thf(f221,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($true = (((~ (irel @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK3 @ Y0))))))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f220])).
% 0.90/0.39  thf(f222,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK3 @ Y0))))))) | ($true = ((~ (irel @ X2 @ X6))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f221])).
% 0.90/0.39  thf(f223,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK3 @ Y0)))))) | ($true = ((~ (irel @ X2 @ X6))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f222])).
% 0.90/0.39  thf(f224,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK3 @ Y0))) @ (sK10 @ X6)))) | ($true = ((~ (irel @ X2 @ X6))))) )),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f223])).
% 0.90/0.39  thf(f225,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y1 @ X3)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ X3 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))))) @ X7))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X6 @ Y0)) | (sK3 @ Y0))) @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6)))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f224])).
% 0.90/0.39  thf(f226,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ X7)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X7 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ X7 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y0 @ X3)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X3 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1)))))))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = (((~ (irel @ X6 @ (sK10 @ X6))) | (sK3 @ (sK10 @ X6))))) | ($false = ((irel @ X2 @ X6)))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f225])).
% 0.90/0.39  thf(f227,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ X7)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X7 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ X7 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y0 @ X3)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X3 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))) @ X8))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = (((~ (irel @ X6 @ (sK10 @ X6))) | (sK3 @ (sK10 @ X6))))) | ($false = ((irel @ X2 @ X6)))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f226])).
% 0.90/0.39  thf(f228,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ X7)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X7 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ X7 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ Y0 @ X3)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X3 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))) @ X8))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6)))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f227])).
% 0.90/0.39  thf(f259,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = (((~ (irel @ sK4 @ X8)) | (((((~ (irel @ X8 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X7 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ X8 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1)))))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6)))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f228])).
% 0.90/0.39  thf(f260,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((((((~ (irel @ X8 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X7 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ X7 @ X5))) | (sK3 @ X5)) & ((((~ (irel @ X8 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1))))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($true = ((~ (irel @ sK4 @ X8))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f259])).
% 0.90/0.39  thf(f261,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = (((((~ (irel @ X8 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ X3 @ X1))) | (sK2 @ X1)))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($true = ((~ (irel @ sK4 @ X8))))) )),
% 0.90/0.39    inference(and_proxy_clausification,[],[f260])).
% 0.90/0.39  thf(f275,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($true = ((~ (irel @ sK4 @ X8)))) | ($true = ((((~ (irel @ X8 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ X3 @ X1)))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f261])).
% 0.90/0.39  thf(f276,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($true = ((((~ (irel @ X8 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ X3 @ X1)))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f275])).
% 0.90/0.39  thf(f277,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($true = ((~ (irel @ X3 @ X1)))) | ($true = (((~ (irel @ X8 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0))))))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f276])).
% 0.90/0.39  thf(f278,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($false = ((irel @ X3 @ X1))) | ($true = (((~ (irel @ X8 @ X3)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0))))))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f277])).
% 0.90/0.39  thf(f279,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($false = ((irel @ X3 @ X1))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0))))))) | ($true = ((~ (irel @ X8 @ X3))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f278])).
% 0.90/0.39  thf(f280,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($false = ((irel @ X3 @ X1))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0)))))) | ($true = ((~ (irel @ X8 @ X3))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f279])).
% 0.90/0.39  thf(f281,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($false = ((irel @ X3 @ X1))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0))) @ (sK14 @ X3)))) | ($true = ((~ (irel @ X8 @ X3))))) )),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f280])).
% 0.90/0.39  thf(f282,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($false = ((irel @ X3 @ X1))) | ($false = (((^[Y0 : $i]: ((~ (irel @ X3 @ Y0)) | (sK3 @ Y0))) @ (sK14 @ X3)))) | ($false = ((irel @ X8 @ X3)))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f281])).
% 0.90/0.39  thf(f283,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($false = ((irel @ X3 @ X1))) | ($false = (((~ (irel @ X3 @ (sK14 @ X3))) | (sK3 @ (sK14 @ X3))))) | ($false = ((irel @ X8 @ X3)))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f282])).
% 0.90/0.39  thf(f284,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK4 @ X2))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($false = ((irel @ X3 @ X1))) | ($false = ((sK3 @ (sK14 @ X3)))) | ($false = ((irel @ X8 @ X3)))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f283])).
% 0.90/0.39  thf(f287,plain,(
% 0.90/0.39    ($true = ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ sK4 @ Y4)) | (((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)) & ((((~ (irel @ Y4 @ Y1)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y1 @ Y5)) | (sK3 @ Y5)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))))))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))))))))))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f125])).
% 0.90/0.39  thf(f288,plain,(
% 0.90/0.39    ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ sK4 @ Y4)) | (((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)) & ((((~ (irel @ Y4 @ Y1)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y1 @ Y5)) | (sK3 @ Y5)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)))))))))))))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))))))))))),
% 0.90/0.39    inference(not_proxy_clausification,[],[f287])).
% 0.90/0.39  thf(f289,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ sK4 @ Y4)) | (((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)) & ((((~ (irel @ Y4 @ Y1)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y1 @ Y5)) | (sK3 @ Y5)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))))) @ sK15))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1)))))))))))))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f288])).
% 0.90/0.39  thf(f290,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ sK4 @ Y4)) | (((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)) & ((((~ (irel @ Y4 @ Y1)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y1 @ Y5)) | (sK3 @ Y5)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))))) @ sK15))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1))))))))))))),
% 0.90/0.39    inference(not_proxy_clausification,[],[f289])).
% 0.90/0.39  thf(f291,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ sK4 @ Y4)) | (((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (sK2 @ Y5)))))) | (~ (irel @ Y3 @ Y2))) | (sK3 @ Y2)) & ((((~ (irel @ Y4 @ Y1)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y1 @ Y5)) | (sK3 @ Y5)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))))) @ sK15))) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((~ (irel @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ Y2 @ Y1))) | (sK2 @ Y1))))))))) @ sK16)))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f290])).
% 0.90/0.39  thf(f292,plain,(
% 0.90/0.39    ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ sK15))) | (sK2 @ sK15)))))))))))))) | ($false = (((~ (irel @ sK4 @ sK16)) | ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)))))) & (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f291])).
% 0.90/0.39  thf(f293,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ sK15))) | (sK2 @ sK15))))))))))) @ sK17))) | ($false = (((~ (irel @ sK4 @ sK16)) | ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)))))) & (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))))))))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f292])).
% 0.90/0.39  thf(f294,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ sK15))) | (sK2 @ sK15))))))))))) @ sK17))) | ($false = (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)))))) & (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)))))))))),
% 0.90/0.39    inference(or_proxy_clausification,[],[f293])).
% 0.90/0.39  thf(f295,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ sK15))) | (sK2 @ sK15))))))))))) @ sK17))) | ($false = ((~ (irel @ sK4 @ sK16))))),
% 0.90/0.39    inference(or_proxy_clausification,[],[f293])).
% 0.90/0.39  thf(f296,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ sK15))) | (sK2 @ sK15))))))))))) @ sK17))) | ($true = ((irel @ sK4 @ sK16)))),
% 0.90/0.39    inference(not_proxy_clausification,[],[f295])).
% 0.90/0.39  thf(f297,plain,(
% 0.90/0.39    ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ sK17)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK17 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))))))))))) | ($true = ((irel @ sK4 @ sK16)))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f296])).
% 0.90/0.39  thf(f298,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ sK17)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK17 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))))) @ sK18))) | ($true = ((irel @ sK4 @ sK16)))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f297])).
% 0.90/0.39  thf(f299,plain,(
% 0.90/0.39    ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK18))) | (sK3 @ sK18)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))))))))) | ($true = ((irel @ sK4 @ sK16)))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f298])).
% 0.90/0.39  thf(f300,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK18))) | (sK3 @ sK18)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK19))) | ($true = ((irel @ sK4 @ sK16)))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f299])).
% 0.90/0.39  thf(f301,plain,(
% 0.90/0.39    ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ sK19)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK19 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK19 @ sK18))) | (sK3 @ sK18)) & ((((~ (irel @ Y0 @ sK17)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK17 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))))))) | ($true = ((irel @ sK4 @ sK16)))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f300])).
% 0.90/0.39  thf(f302,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ sK19)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK19 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK19 @ sK18))) | (sK3 @ sK18)) & ((((~ (irel @ Y0 @ sK17)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK17 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))) @ sK20))) | ($true = ((irel @ sK4 @ sK16)))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f301])).
% 0.90/0.39  thf(f303,plain,(
% 0.90/0.39    ($false = (((~ (irel @ sK4 @ sK20)) | (((((~ (irel @ sK20 @ sK19)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK19 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK19 @ sK18))) | (sK3 @ sK18)) & ((((~ (irel @ sK20 @ sK17)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))))) | ($true = ((irel @ sK4 @ sK16)))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f302])).
% 0.90/0.39  thf(f305,plain,(
% 0.90/0.39    ($false = ((~ (irel @ sK4 @ sK20)))) | ($true = ((irel @ sK4 @ sK16)))),
% 0.90/0.39    inference(or_proxy_clausification,[],[f303])).
% 0.90/0.39  thf(f306,plain,(
% 0.90/0.39    ($true = ((irel @ sK4 @ sK20))) | ($true = ((irel @ sK4 @ sK16)))),
% 0.90/0.39    inference(not_proxy_clausification,[],[f305])).
% 0.90/0.39  thf(f381,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ sK15))) | (sK2 @ sK15))))))))))) @ sK17))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0)))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0))))))))),
% 0.90/0.39    inference(and_proxy_clausification,[],[f294])).
% 0.90/0.39  thf(f382,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ sK15))) | (sK2 @ sK15))))))))))) @ sK17))) | ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))) @ sK21))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0))))))))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f381])).
% 0.90/0.39  thf(f383,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK4 @ Y3)) | (((((~ (irel @ Y3 @ Y2)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK2 @ Y4)))))) | (~ (irel @ Y2 @ Y1))) | (sK3 @ Y1)) & ((((~ (irel @ Y3 @ Y0)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y0 @ Y4)) | (sK3 @ Y4)))))) | (~ (irel @ Y0 @ sK15))) | (sK2 @ sK15))))))))))) @ sK17))) | ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK2 @ Y0))))) @ sK21))) | ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((~ (irel @ sK16 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0))))) @ sK22)))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f382])).
% 0.90/0.39  thf(f384,plain,(
% 0.90/0.39    ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ sK17)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK17 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))))))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK16 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ Y0 @ sK21))) | (sK2 @ sK21)))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK16 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK22))) | (sK3 @ sK22))))))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f383])).
% 0.90/0.39  thf(f385,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ sK17)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK17 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))))) @ sK23))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK16 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ Y0 @ sK21))) | (sK2 @ sK21)))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK16 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK22))) | (sK3 @ sK22))))))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f384])).
% 0.90/0.39  thf(f386,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ sK17)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK17 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))))) @ sK23))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK16 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ Y0 @ sK21))) | (sK2 @ sK21))) @ sK24))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((~ (irel @ sK16 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK22))) | (sK3 @ sK22))))))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f385])).
% 0.90/0.39  thf(f387,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK4 @ Y2)) | (((((~ (irel @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK2 @ Y3)))))) | (~ (irel @ Y1 @ Y0))) | (sK3 @ Y0)) & ((((~ (irel @ Y2 @ sK17)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ sK17 @ Y3)) | (sK3 @ Y3)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))))) @ sK23))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK16 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ Y0 @ sK21))) | (sK2 @ sK21))) @ sK24))) | ($false = (((^[Y0 : $i]: ((((~ (irel @ sK16 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ Y0 @ sK22))) | (sK3 @ sK22))) @ sK25)))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f386])).
% 0.90/0.39  thf(f388,plain,(
% 0.90/0.39    ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))))))))) | ($false = (((((~ (irel @ sK16 @ sK24)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ sK24 @ sK21))) | (sK2 @ sK21)))) | ($false = (((((~ (irel @ sK16 @ sK25)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK25 @ sK22))) | (sK3 @ sK22))))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f387])).
% 0.90/0.39  thf(f389,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($false = (((((~ (irel @ sK16 @ sK24)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ sK24 @ sK21))) | (sK2 @ sK21)))) | ($false = (((((~ (irel @ sK16 @ sK25)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK25 @ sK22))) | (sK3 @ sK22))))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f388])).
% 0.90/0.39  thf(f390,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($false = ((sK2 @ sK21))) | ($false = (((((~ (irel @ sK16 @ sK25)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK25 @ sK22))) | (sK3 @ sK22))))),
% 0.90/0.39    inference(or_proxy_clausification,[],[f389])).
% 0.90/0.39  thf(f391,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($false = ((((~ (irel @ sK16 @ sK24)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ sK24 @ sK21))))) | ($false = (((((~ (irel @ sK16 @ sK25)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK25 @ sK22))) | (sK3 @ sK22))))),
% 0.90/0.39    inference(or_proxy_clausification,[],[f389])).
% 0.90/0.39  thf(f393,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($false = (((~ (irel @ sK16 @ sK24)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0)))))))) | ($false = (((((~ (irel @ sK16 @ sK25)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK25 @ sK22))) | (sK3 @ sK22))))),
% 0.90/0.39    inference(or_proxy_clausification,[],[f391])).
% 0.90/0.39  thf(f394,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0))))))) | ($false = (((((~ (irel @ sK16 @ sK25)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK25 @ sK22))) | (sK3 @ sK22))))),
% 0.90/0.39    inference(or_proxy_clausification,[],[f393])).
% 0.90/0.39  thf(f729,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0)))))) | ($false = (((((~ (irel @ sK16 @ sK25)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK25 @ sK22))) | (sK3 @ sK22))))),
% 0.90/0.39    inference(not_proxy_clausification,[],[f394])).
% 0.90/0.39  thf(f730,plain,(
% 0.90/0.39    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0))) @ X1))) | ($false = (((((~ (irel @ sK16 @ sK25)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK25 @ sK22))) | (sK3 @ sK22))))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f729])).
% 0.90/0.39  thf(f732,plain,(
% 0.90/0.39    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0))) @ X1))) | ($false = ((((~ (irel @ sK16 @ sK25)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK25 @ sK22)))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f730])).
% 0.90/0.39  thf(f734,plain,(
% 0.90/0.39    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0))) @ X1))) | ($false = (((~ (irel @ sK16 @ sK25)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f732])).
% 0.90/0.39  thf(f735,plain,(
% 0.90/0.39    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0))) @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0)))))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f734])).
% 0.90/0.39  thf(f820,plain,(
% 0.90/0.39    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0))) @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0))))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f735])).
% 0.90/0.39  thf(f821,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK24 @ Y0)) | (sK3 @ Y0))) @ X1))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK25 @ Y0)) | (sK2 @ Y0))) @ X2)))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f820])).
% 0.90/0.39  thf(f822,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ sK26)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK26 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y0 @ sK17)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK17 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))))))) | ($true = (((~ (irel @ sK24 @ X1)) | (sK3 @ X1)))) | ($true = (((~ (irel @ sK25 @ X2)) | (sK2 @ X2))))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f821])).
% 0.90/0.39  thf(f823,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ sK26)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK26 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y0 @ sK17)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK17 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))) @ sK32))) | ($true = (((~ (irel @ sK24 @ X1)) | (sK3 @ X1)))) | ($true = (((~ (irel @ sK25 @ X2)) | (sK2 @ X2))))) )),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f822])).
% 0.90/0.39  thf(f824,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ sK26)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK26 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y0 @ sK17)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK17 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))) @ sK32))) | ($true = ((sK3 @ X1))) | ($true = (((~ (irel @ sK25 @ X2)) | (sK2 @ X2)))) | ($true = ((~ (irel @ sK24 @ X1))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f823])).
% 0.90/0.39  thf(f825,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ sK26)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK26 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y0 @ sK17)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK17 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))) @ sK32))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($true = ((~ (irel @ sK24 @ X1)))) | ($true = ((~ (irel @ sK25 @ X2))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f824])).
% 0.90/0.39  thf(f826,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ sK26)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK26 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y0 @ sK17)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK17 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))) @ sK32))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($true = ((~ (irel @ sK25 @ X2))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f825])).
% 0.90/0.39  thf(f827,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ sK26)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK26 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y0 @ sK17)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK17 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))) @ sK32))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2)))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f826])).
% 0.90/0.39  thf(f828,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = (((~ (irel @ sK4 @ sK32)) | (((((~ (irel @ sK32 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ sK32 @ sK17)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2)))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f827])).
% 0.90/0.39  thf(f829,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = ((((((~ (irel @ sK32 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ sK32 @ sK17)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2)))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f828])).
% 0.90/0.39  thf(f832,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = (((((~ (irel @ sK32 @ sK17)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($false = (((((~ (irel @ sK32 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23))))) )),
% 0.90/0.39    inference(and_proxy_clausification,[],[f829])).
% 0.90/0.39  thf(f834,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = ((((~ (irel @ sK32 @ sK17)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ sK17 @ sK15))))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($false = (((((~ (irel @ sK32 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f832])).
% 0.90/0.39  thf(f836,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = (((~ (irel @ sK32 @ sK17)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0)))))))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($false = (((((~ (irel @ sK32 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f834])).
% 0.90/0.39  thf(f837,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0))))))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($false = (((((~ (irel @ sK32 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f836])).
% 0.90/0.39  thf(f853,plain,(
% 0.90/0.39    ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0)))))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($false = (((((~ (irel @ sK32 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f837])).
% 0.90/0.39  thf(f854,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0))) @ X3))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($false = (((((~ (irel @ sK32 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23))))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f853])).
% 0.90/0.39  thf(f856,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0))) @ X3))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($false = ((((~ (irel @ sK32 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23)))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f854])).
% 0.90/0.39  thf(f858,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0))) @ X3))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($false = (((~ (irel @ sK32 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0))))))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f856])).
% 0.90/0.39  thf(f859,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0))) @ X3))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f858])).
% 0.90/0.39  thf(f865,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0))) @ X3))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0))))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f859])).
% 0.90/0.39  thf(f866,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0))) @ X3))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0))) @ X4)))) )),
% 0.90/0.39    inference(pi_proxy_clausification,[],[f865])).
% 0.90/0.39  thf(f867,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((~ (irel @ sK17 @ X3)) | (sK3 @ X3)))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = (((~ (irel @ sK26 @ X4)) | (sK2 @ X4))))) )),
% 0.90/0.39    inference(beta-eta_normalization,[],[f866])).
% 0.90/0.39  thf(f868,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK3 @ X3))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = (((~ (irel @ sK26 @ X4)) | (sK2 @ X4)))) | ($true = ((~ (irel @ sK17 @ X3))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f867])).
% 0.90/0.39  thf(f869,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK3 @ X3))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($true = ((~ (irel @ sK17 @ X3)))) | ($true = ((~ (irel @ sK26 @ X4))))) )),
% 0.90/0.39    inference(or_proxy_clausification,[],[f868])).
% 0.90/0.39  thf(f870,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK3 @ X3))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($true = ((~ (irel @ sK26 @ X4))))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f869])).
% 0.90/0.39  thf(f871,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK3 @ X3))) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) )),
% 0.90/0.39    inference(not_proxy_clausification,[],[f870])).
% 0.90/0.39  thf(f1404,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK4 @ Y1)) | (((((~ (irel @ Y1 @ Y0)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y1 @ sK17)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ sK17 @ Y2)) | (sK3 @ Y2)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))))) @ sK26))) | ($false = ((sK2 @ sK21))) | ($false = ((sK3 @ sK22)))),
% 0.90/0.39    inference(or_proxy_clausification,[],[f390])).
% 0.90/0.39  thf(f1656,plain,(
% 0.90/0.39    ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ sK26)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK26 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y0 @ sK17)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK17 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))))))) | ($false = ((sK2 @ sK21))) | ($false = ((sK3 @ sK22)))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f1404])).
% 0.90/0.39  thf(f1657,plain,(
% 0.90/0.39    ($false = (((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (((((~ (irel @ Y0 @ sK26)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK26 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ Y0 @ sK17)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK17 @ Y1)) | (sK3 @ Y1)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))) @ sK42))) | ($false = ((sK2 @ sK21))) | ($false = ((sK3 @ sK22)))),
% 0.90/0.39    inference(sigma_proxy_clausification,[],[f1656])).
% 0.90/0.39  thf(f1658,plain,(
% 0.90/0.39    ($false = (((~ (irel @ sK4 @ sK42)) | (((((~ (irel @ sK42 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ sK42 @ sK17)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))))) | ($false = ((sK2 @ sK21))) | ($false = ((sK3 @ sK22)))),
% 0.90/0.39    inference(beta-eta_normalization,[],[f1657])).
% 0.90/0.39  thf(f1659,plain,(
% 0.90/0.39    ($false = ((((((~ (irel @ sK42 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23)) & ((((~ (irel @ sK42 @ sK17)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15))))) | ($false = ((sK2 @ sK21))) | ($false = ((sK3 @ sK22)))),
% 0.90/0.39    inference(or_proxy_clausification,[],[f1658])).
% 0.90/0.39  thf(f1662,plain,(
% 0.90/0.39    ($false = (((((~ (irel @ sK42 @ sK17)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK17 @ Y0)) | (sK3 @ Y0)))))) | (~ (irel @ sK17 @ sK15))) | (sK2 @ sK15)))) | ($false = ((sK2 @ sK21))) | ($false = ((sK3 @ sK22))) | ($false = (((((~ (irel @ sK42 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23))))),
% 0.90/0.39    inference(and_proxy_clausification,[],[f1659])).
% 0.90/0.39  thf(f1663,plain,(
% 0.90/0.39    ($false = ((sK2 @ sK15))) | ($false = ((sK2 @ sK21))) | ($false = ((sK3 @ sK22))) | ($false = (((((~ (irel @ sK42 @ sK26)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK26 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK26 @ sK23))) | (sK3 @ sK23))))),
% 0.90/0.39    inference(or_proxy_clausification,[],[f1662])).
% 0.90/0.39  thf(f1723,plain,(
% 0.90/0.39    ($false = ((sK2 @ sK15))) | ($false = ((sK2 @ sK21))) | ($false = ((sK3 @ sK22))) | ($false = ((sK3 @ sK23)))),
% 0.90/0.39    inference(or_proxy_clausification,[],[f1663])).
% 0.90/0.39  thf(f1737,definition,(
% 0.90/0.39    spl1_3 <=> ($true = ((irel @ sK4 @ sK16)))),
% 0.90/0.39    introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition])).
% 0.90/0.39  thf(f1738,plain,(
% 0.90/0.39    ($true != ((irel @ sK4 @ sK16))) | spl1_3),
% 0.90/0.39    inference(avatar_component_clause,[],[f1737])).
% 0.90/0.39  thf(f1739,plain,(
% 0.90/0.39    ($true = ((irel @ sK4 @ sK16))) | ~spl1_3),
% 0.90/0.39    inference(avatar_component_clause,[],[f1737])).
% 0.90/0.39  thf(f1741,definition,(
% 0.90/0.39    spl1_4 <=> ($true = ((irel @ sK4 @ sK20)))),
% 0.90/0.39    introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition])).
% 0.90/0.39  thf(f1742,plain,(
% 0.90/0.39    ($true != ((irel @ sK4 @ sK20))) | spl1_4),
% 0.90/0.39    inference(avatar_component_clause,[],[f1741])).
% 0.90/0.39  thf(f1743,plain,(
% 0.90/0.39    ($true = ((irel @ sK4 @ sK20))) | ~spl1_4),
% 0.90/0.39    inference(avatar_component_clause,[],[f1741])).
% 0.90/0.39  thf(f1744,plain,(
% 0.90/0.39    spl1_3 | spl1_4),
% 0.90/0.39    inference(avatar_split_clause,[],[f306,f1741,f1737])).
% 0.90/0.39  thf(f1745,plain,(
% 0.90/0.39    ( ! [X0 : $i] : (($true = ((irel @ sK4 @ X0)))) ) | ~spl1_4),
% 0.90/0.39    inference(constrained_superposition,[],[f1743,f88])).
% 0.90/0.39  thf(f1749,plain,(
% 0.90/0.39    ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X0 @ X1)))) ) | ~spl1_4),
% 0.90/0.39    inference(constrained_superposition,[],[f1745,f88])).
% 0.90/0.39  thf(f1754,definition,(
% 0.90/0.39    spl1_5 <=> ($false = ((sK3 @ sK23)))),
% 0.90/0.39    introduced(definition,[new_symbols(definition,[spl1_5])],[avatar_definition])).
% 0.90/0.39  thf(f1755,plain,(
% 0.90/0.39    ($false != ((sK3 @ sK23))) | spl1_5),
% 0.90/0.39    inference(avatar_component_clause,[],[f1754])).
% 0.90/0.39  thf(f1756,plain,(
% 0.90/0.39    ($false = ((sK3 @ sK23))) | ~spl1_5),
% 0.90/0.39    inference(avatar_component_clause,[],[f1754])).
% 0.90/0.39  thf(f1758,definition,(
% 0.90/0.39    spl1_6 <=> ($false = ((sK3 @ sK22)))),
% 0.90/0.39    introduced(definition,[new_symbols(definition,[spl1_6])],[avatar_definition])).
% 0.90/0.39  thf(f1760,plain,(
% 0.90/0.39    ($false = ((sK3 @ sK22))) | ~spl1_6),
% 0.90/0.39    inference(avatar_component_clause,[],[f1758])).
% 0.90/0.39  thf(f1762,definition,(
% 0.90/0.39    spl1_7 <=> ($false = ((sK2 @ sK21)))),
% 0.90/0.39    introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition])).
% 0.90/0.39  thf(f1763,plain,(
% 0.90/0.39    ($false != ((sK2 @ sK21))) | spl1_7),
% 0.90/0.39    inference(avatar_component_clause,[],[f1762])).
% 0.90/0.39  thf(f1764,plain,(
% 0.90/0.39    ($false = ((sK2 @ sK21))) | ~spl1_7),
% 0.90/0.39    inference(avatar_component_clause,[],[f1762])).
% 0.90/0.39  thf(f1766,definition,(
% 0.90/0.39    spl1_8 <=> ($false = ((sK2 @ sK15)))),
% 0.90/0.39    introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition])).
% 0.90/0.39  thf(f1768,plain,(
% 0.90/0.39    ($false = ((sK2 @ sK15))) | ~spl1_8),
% 0.90/0.39    inference(avatar_component_clause,[],[f1766])).
% 0.90/0.39  thf(f1769,plain,(
% 0.90/0.39    spl1_5 | spl1_6 | spl1_7 | spl1_8),
% 0.90/0.39    inference(avatar_split_clause,[],[f1723,f1766,f1762,f1758,f1754])).
% 0.90/0.39  thf(f1770,plain,(
% 0.90/0.39    ( ! [X0 : $i] : (($false = ((sK3 @ X0)))) ) | ~spl1_5),
% 0.90/0.39    inference(constrained_superposition,[],[f1756,f88])).
% 0.90/0.39  thf(f1774,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = $false) | ($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($false = ((sK2 @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) ) | ~spl1_4),
% 0.90/0.39    inference(forward_demodulation,[],[f197,f1749])).
% 0.90/0.39  thf(f1775,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($false = ((sK2 @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) ) | ~spl1_4),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1774])).
% 0.90/0.39  thf(f1776,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = $false) | ($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($false = ((sK2 @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) ) | ~spl1_4),
% 0.90/0.39    inference(forward_demodulation,[],[f1775,f1749])).
% 0.90/0.39  thf(f1777,plain,(
% 0.90/0.39    ( ! [X2 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($false = ((sK2 @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) ) | ~spl1_4),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1776])).
% 0.90/0.39  thf(f1778,plain,(
% 0.90/0.39    ( ! [X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = $false) | ($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($false = ((sK2 @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) ) | ~spl1_4),
% 0.90/0.39    inference(forward_demodulation,[],[f1777,f1749])).
% 0.90/0.39  thf(f1779,plain,(
% 0.90/0.39    ( ! [X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((irel @ sK4 @ X8))) | (((irel @ X7 @ X5)) = $false) | ($false = ((sK2 @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) ) | ~spl1_4),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1778])).
% 0.90/0.39  thf(f1780,plain,(
% 0.90/0.39    ( ! [X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = $false) | ($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | (((irel @ X7 @ X5)) = $false) | ($false = ((sK2 @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) ) | ~spl1_4),
% 0.90/0.39    inference(forward_demodulation,[],[f1779,f1749])).
% 0.90/0.39  thf(f1781,plain,(
% 0.90/0.39    ( ! [X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | (((irel @ X7 @ X5)) = $false) | ($false = ((sK2 @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) ) | ~spl1_4),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1780])).
% 0.90/0.39  thf(f1782,plain,(
% 0.90/0.39    ( ! [X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = $false) | ($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((sK2 @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) ) | ~spl1_4),
% 0.90/0.39    inference(forward_demodulation,[],[f1781,f1749])).
% 0.90/0.39  thf(f1783,plain,(
% 0.90/0.39    ( ! [X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((sK2 @ (sK8 @ X7)))) | ($false = ((irel @ X8 @ X7)))) ) | ~spl1_4),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1782])).
% 0.90/0.39  thf(f1784,plain,(
% 0.90/0.39    ( ! [X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = $false) | ($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((sK2 @ (sK8 @ X7))))) ) | ~spl1_4),
% 0.90/0.39    inference(forward_demodulation,[],[f1783,f1749])).
% 0.90/0.39  thf(f1785,plain,(
% 0.90/0.39    ( ! [X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((sK3 @ X5))) | ($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((sK2 @ (sK8 @ X7))))) ) | ~spl1_4),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1784])).
% 0.90/0.39  thf(f1788,plain,(
% 0.90/0.39    ( ! [X6 : $i,X7 : $i,X4 : $i] : (($true = $false) | ($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((sK2 @ (sK8 @ X7))))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(forward_demodulation,[],[f1785,f1770])).
% 0.90/0.39  thf(f1789,plain,(
% 0.90/0.39    ( ! [X6 : $i,X7 : $i,X4 : $i] : (($true = ((sK3 @ X4))) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((sK2 @ (sK8 @ X7))))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1788])).
% 0.90/0.39  thf(f1790,plain,(
% 0.90/0.39    ( ! [X6 : $i,X7 : $i] : (($true = $false) | ($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((sK2 @ (sK8 @ X7))))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(forward_demodulation,[],[f1789,f1770])).
% 0.90/0.39  thf(f1791,plain,(
% 0.90/0.39    ( ! [X6 : $i,X7 : $i] : (($false = ((sK2 @ (sK5 @ X6)))) | ($false = ((sK2 @ (sK8 @ X7))))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1790])).
% 0.90/0.39  thf(f1793,definition,(
% 0.90/0.39    spl1_9 <=> ! [X7 : $i] : ($false = ((sK2 @ (sK8 @ X7))))),
% 0.90/0.39    introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition])).
% 0.90/0.39  thf(f1794,plain,(
% 0.90/0.39    ( ! [X7 : $i] : (($false = ((sK2 @ (sK8 @ X7))))) ) | ~spl1_9),
% 0.90/0.39    inference(avatar_component_clause,[],[f1793])).
% 0.90/0.39  thf(f1796,definition,(
% 0.90/0.39    spl1_10 <=> ! [X6 : $i] : ($false = ((sK2 @ (sK5 @ X6))))),
% 0.90/0.39    introduced(definition,[new_symbols(definition,[spl1_10])],[avatar_definition])).
% 0.90/0.39  thf(f1797,plain,(
% 0.90/0.39    ( ! [X6 : $i] : (($false = ((sK2 @ (sK5 @ X6))))) ) | ~spl1_10),
% 0.90/0.39    inference(avatar_component_clause,[],[f1796])).
% 0.90/0.39  thf(f1798,plain,(
% 0.90/0.39    spl1_9 | spl1_10 | ~spl1_4 | ~spl1_5),
% 0.90/0.39    inference(avatar_split_clause,[],[f1791,f1754,f1741,f1796,f1793])).
% 0.90/0.39  thf(f1799,plain,(
% 0.90/0.39    ( ! [X0 : $i] : (($false != ((sK3 @ X0)))) ) | spl1_5),
% 0.90/0.39    inference(constrained_superposition,[],[f1755,f88])).
% 0.90/0.39  thf(f1806,plain,(
% 0.90/0.39    $false | (spl1_5 | ~spl1_6)),
% 0.90/0.39    inference(backward_subsumption_resolution,[],[f1760,f1799])).
% 0.90/0.39  thf(f1808,plain,(
% 0.90/0.39    spl1_5 | ~spl1_6),
% 0.90/0.39    inference(avatar_contradiction_clause,[],[f1806])).
% 0.90/0.39  thf(f1809,plain,(
% 0.90/0.39    ( ! [X0 : $i] : (($false = ((sK2 @ X0)))) ) | ~spl1_9),
% 0.90/0.39    inference(constrained_superposition,[],[f1794,f88])).
% 0.90/0.39  thf(f1826,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = $false) | ($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | ~spl1_5),
% 0.90/0.39    inference(forward_demodulation,[],[f871,f1770])).
% 0.90/0.39  thf(f1827,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK3 @ X1))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | ~spl1_5),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1826])).
% 0.90/0.39  thf(f1828,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = $false) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | ~spl1_5),
% 0.90/0.39    inference(forward_demodulation,[],[f1827,f1770])).
% 0.90/0.39  thf(f1829,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X2))) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | ~spl1_5),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1828])).
% 0.90/0.39  thf(f1830,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = $false) | ($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(forward_demodulation,[],[f1829,f1809])).
% 0.90/0.39  thf(f1831,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ sK24 @ X1))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1830])).
% 0.90/0.39  thf(f1832,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X4 : $i] : (($true = $false) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(forward_demodulation,[],[f1831,f1749])).
% 0.90/0.39  thf(f1833,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X4 : $i] : (($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1832])).
% 0.90/0.39  thf(f1834,plain,(
% 0.90/0.39    ( ! [X3 : $i,X4 : $i] : (($true = $false) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(forward_demodulation,[],[f1833,f1749])).
% 0.90/0.39  thf(f1835,plain,(
% 0.90/0.39    ( ! [X3 : $i,X4 : $i] : (($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1834])).
% 0.90/0.39  thf(f1836,plain,(
% 0.90/0.39    ( ! [X3 : $i,X4 : $i] : (($true = $false) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(forward_demodulation,[],[f1835,f1809])).
% 0.90/0.39  thf(f1837,plain,(
% 0.90/0.39    ( ! [X3 : $i,X4 : $i] : (($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1836])).
% 0.90/0.39  thf(f1838,plain,(
% 0.90/0.39    ( ! [X4 : $i] : (($true = $false) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(forward_demodulation,[],[f1837,f1749])).
% 0.90/0.39  thf(f1839,plain,(
% 0.90/0.39    ( ! [X4 : $i] : (($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1838])).
% 0.90/0.39  thf(f1840,plain,(
% 0.90/0.39    ($true = $false) | (~spl1_4 | ~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(forward_demodulation,[],[f1839,f1749])).
% 0.90/0.39  thf(f1841,plain,(
% 0.90/0.39    $false | (~spl1_4 | ~spl1_5 | ~spl1_9)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1840])).
% 0.90/0.39  thf(f1842,plain,(
% 0.90/0.39    ~spl1_4 | ~spl1_5 | ~spl1_9),
% 0.90/0.39    inference(avatar_contradiction_clause,[],[f1841])).
% 0.90/0.39  thf(f1851,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X4 : $i] : (($true = $false) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(forward_demodulation,[],[f1829,f1749])).
% 0.90/0.39  thf(f1852,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X4 : $i] : (($true = ((sK2 @ X2))) | ($false = ((irel @ sK25 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1851])).
% 0.90/0.39  thf(f1861,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X4 : $i] : (($true = $false) | ($true = ((sK2 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(forward_demodulation,[],[f1852,f1749])).
% 0.90/0.39  thf(f1862,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X4 : $i] : (($true = ((sK2 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK17 @ X3))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1861])).
% 0.90/0.39  thf(f1867,plain,(
% 0.90/0.39    ( ! [X2 : $i,X4 : $i] : (($true = $false) | ($true = ((sK2 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(forward_demodulation,[],[f1862,f1749])).
% 0.90/0.39  thf(f1868,plain,(
% 0.90/0.39    ( ! [X2 : $i,X4 : $i] : (($true = ((sK2 @ X2))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ sK26 @ X4)))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1867])).
% 0.90/0.39  thf(f1873,plain,(
% 0.90/0.39    ( ! [X2 : $i,X4 : $i] : (($true = $false) | ($true = ((sK2 @ X2))) | ($true = ((sK2 @ X4)))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(forward_demodulation,[],[f1868,f1749])).
% 0.90/0.39  thf(f1874,plain,(
% 0.90/0.39    ( ! [X2 : $i,X4 : $i] : (($true = ((sK2 @ X2))) | ($true = ((sK2 @ X4)))) ) | (~spl1_4 | ~spl1_5)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1873])).
% 0.90/0.39  thf(f1875,plain,(
% 0.90/0.39    ( ! [X0 : $i] : (($false = ((sK2 @ X0)))) ) | ~spl1_10),
% 0.90/0.39    inference(constrained_superposition,[],[f1797,f88])).
% 0.90/0.39  thf(f1882,plain,(
% 0.90/0.39    ( ! [X4 : $i] : (($true = $false) | ($true = ((sK2 @ X4)))) ) | (~spl1_4 | ~spl1_5 | ~spl1_10)),
% 0.90/0.39    inference(forward_demodulation,[],[f1874,f1875])).
% 0.90/0.39  thf(f1883,plain,(
% 0.90/0.39    ( ! [X4 : $i] : (($true = ((sK2 @ X4)))) ) | (~spl1_4 | ~spl1_5 | ~spl1_10)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1882])).
% 0.90/0.39  thf(f1884,plain,(
% 0.90/0.39    ($true = $false) | (~spl1_4 | ~spl1_5 | ~spl1_10)),
% 0.90/0.39    inference(forward_demodulation,[],[f1883,f1875])).
% 0.90/0.39  thf(f1885,plain,(
% 0.90/0.39    $false | (~spl1_4 | ~spl1_5 | ~spl1_10)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f1884])).
% 0.90/0.39  thf(f1886,plain,(
% 0.90/0.39    ~spl1_4 | ~spl1_5 | ~spl1_10),
% 0.90/0.39    inference(avatar_contradiction_clause,[],[f1885])).
% 0.90/0.39  thf(f2059,plain,(
% 0.90/0.39    ( ! [X0 : $i] : (($true = ((irel @ sK4 @ X0)))) ) | ~spl1_3),
% 0.90/0.39    inference(constrained_superposition,[],[f1739,f88])).
% 0.90/0.39  thf(f2069,plain,(
% 0.90/0.39    $false | (~spl1_3 | spl1_4)),
% 0.90/0.39    inference(backward_subsumption_resolution,[],[f1742,f2059])).
% 0.90/0.39  thf(f2072,plain,(
% 0.90/0.39    ~spl1_3 | spl1_4),
% 0.90/0.39    inference(avatar_contradiction_clause,[],[f2069])).
% 0.90/0.39  thf(f2075,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = $false) | ($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($false = ((irel @ X3 @ X1))) | ($false = ((sK3 @ (sK14 @ X3)))) | ($false = ((irel @ X8 @ X3)))) ) | ~spl1_3),
% 0.90/0.39    inference(forward_demodulation,[],[f284,f2059])).
% 0.90/0.39  thf(f2076,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ sK4 @ X8))) | ($false = ((irel @ X3 @ X1))) | ($false = ((sK3 @ (sK14 @ X3)))) | ($false = ((irel @ X8 @ X3)))) ) | ~spl1_3),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f2075])).
% 0.90/0.39  thf(f2105,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = $false) | ($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ X3 @ X1))) | ($false = ((sK3 @ (sK14 @ X3)))) | ($false = ((irel @ X8 @ X3)))) ) | ~spl1_3),
% 0.90/0.39    inference(forward_demodulation,[],[f2076,f2059])).
% 0.90/0.39  thf(f2106,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ X3 @ X1))) | ($false = ((sK3 @ (sK14 @ X3)))) | ($false = ((irel @ X8 @ X3)))) ) | ~spl1_3),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f2105])).
% 0.90/0.39  thf(f2139,plain,(
% 0.90/0.39    ( ! [X0 : $i] : (($false = ((sK2 @ X0)))) ) | ~spl1_7),
% 0.90/0.39    inference(constrained_superposition,[],[f1764,f88])).
% 0.90/0.39  thf(f2148,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ X6 @ X4))) | ($false = ((sK3 @ (sK10 @ X6)))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | spl1_5)),
% 0.90/0.39    inference(forward_subsumption_resolution,[],[f2106,f1799])).
% 0.90/0.39  thf(f2149,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X1))) | ($true = ((sK2 @ X4))) | ($false = ((irel @ X6 @ X4))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | spl1_5)),
% 0.90/0.39    inference(forward_subsumption_resolution,[],[f2148,f1799])).
% 0.90/0.39  thf(f2150,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = $false) | ($true = ((sK2 @ X4))) | ($false = ((irel @ X6 @ X4))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(forward_demodulation,[],[f2149,f2139])).
% 0.90/0.39  thf(f2151,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = ((sK2 @ X4))) | ($false = ((irel @ X6 @ X4))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f2150])).
% 0.90/0.39  thf(f2152,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($true = $false) | ($false = ((irel @ X6 @ X4))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(forward_demodulation,[],[f2151,f2139])).
% 0.90/0.39  thf(f2153,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i,X4 : $i] : (($false = ((irel @ X6 @ X4))) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f2152])).
% 0.90/0.39  thf(f2154,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i] : (($true = $false) | ($false = ((irel @ X2 @ X6))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | ~spl1_4 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(forward_demodulation,[],[f2153,f1749])).
% 0.90/0.39  thf(f2155,plain,(
% 0.90/0.39    ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : $i,X6 : $i] : (($false = ((irel @ X2 @ X6))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | ~spl1_4 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f2154])).
% 0.90/0.39  thf(f2156,plain,(
% 0.90/0.39    ( ! [X3 : $i,X1 : $i,X8 : $i] : (($true = $false) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | ~spl1_4 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(forward_demodulation,[],[f2155,f1749])).
% 0.90/0.39  thf(f2157,plain,(
% 0.90/0.39    ( ! [X3 : $i,X1 : $i,X8 : $i] : (($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | ~spl1_4 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f2156])).
% 0.90/0.39  thf(f2158,plain,(
% 0.90/0.39    ( ! [X3 : $i,X8 : $i] : (($true = $false) | ($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | ~spl1_4 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(forward_demodulation,[],[f2157,f1749])).
% 0.90/0.39  thf(f2159,plain,(
% 0.90/0.39    ( ! [X3 : $i,X8 : $i] : (($false = ((irel @ X8 @ X3)))) ) | (~spl1_3 | ~spl1_4 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f2158])).
% 0.90/0.39  thf(f2160,plain,(
% 0.90/0.39    ($true = $false) | (~spl1_3 | ~spl1_4 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(backward_demodulation,[],[f1749,f2159])).
% 0.90/0.39  thf(f2163,plain,(
% 0.90/0.39    $false | (~spl1_3 | ~spl1_4 | spl1_5 | ~spl1_7)),
% 0.90/0.39    inference(trivial_inequality_removal,[],[f2160])).
% 0.90/0.39  thf(f2164,plain,(
% 0.90/0.39    ~spl1_3 | ~spl1_4 | spl1_5 | ~spl1_7),
% 0.90/0.39    inference(avatar_contradiction_clause,[],[f2163])).
% 0.90/0.39  thf(f2170,plain,(
% 0.90/0.39    ( ! [X0 : $i] : (($false != ((sK2 @ X0)))) ) | spl1_7),
% 0.90/0.39    inference(constrained_superposition,[],[f1763,f88])).
% 0.90/0.39  thf(f2177,plain,(
% 0.90/0.39    $false | (spl1_7 | ~spl1_8)),
% 0.90/0.39    inference(backward_subsumption_resolution,[],[f1768,f2170])).
% 0.90/0.39  thf(f2179,plain,(
% 0.90/0.39    spl1_7 | ~spl1_8),
% 0.90/0.39    inference(avatar_contradiction_clause,[],[f2177])).
% 0.90/0.39  thf(f2196,plain,(
% 0.90/0.39    ( ! [X0 : $i] : (($true != ((irel @ sK4 @ X0)))) ) | spl1_3),
% 0.90/0.39    inference(constrained_superposition,[],[f1738,f88])).
% 0.90/0.39  thf(f2216,plain,(
% 0.90/0.39    $false | (spl1_3 | ~spl1_4)),
% 0.90/0.39    inference(backward_subsumption_resolution,[],[f1743,f2196])).
% 0.90/0.39  thf(f2221,plain,(
% 0.90/0.39    spl1_3 | ~spl1_4),
% 0.90/0.39    inference(avatar_contradiction_clause,[],[f2216])).
% 0.90/0.39  cnf(s3, plain, spl1_3 | spl1_4, inference(sat_conversion,[],[f1744])).
% 0.90/0.39  cnf(s4, plain, spl1_5 | spl1_6 | spl1_7 | spl1_8, inference(sat_conversion,[],[f1769])).
% 0.90/0.39  cnf(s5, plain, ~spl1_4 | ~spl1_5 | spl1_9 | spl1_10, inference(sat_conversion,[],[f1798])).
% 0.90/0.39  cnf(s6, plain, spl1_5 | ~spl1_6, inference(sat_conversion,[],[f1808])).
% 0.90/0.39  cnf(s7, plain, ~spl1_4 | ~spl1_5 | ~spl1_9, inference(sat_conversion,[],[f1842])).
% 0.90/0.39  cnf(s8, plain, ~spl1_4 | ~spl1_5 | ~spl1_10, inference(sat_conversion,[],[f1886])).
% 0.90/0.39  cnf(s9, plain, ~spl1_3 | spl1_4, inference(sat_conversion,[],[f2072])).
% 0.90/0.39  cnf(s10, plain, ~spl1_3 | ~spl1_4 | spl1_5 | ~spl1_7, inference(sat_conversion,[],[f2164])).
% 0.90/0.39  cnf(s11, plain, spl1_7 | ~spl1_8, inference(sat_conversion,[],[f2179])).
% 0.90/0.39  cnf(s12, plain, spl1_3 | ~spl1_4, inference(sat_conversion,[],[f2221])).
% 0.90/0.39  cnf(s13, plain, spl1_3, inference(rat,[],[s3,s12])).
% 0.90/0.39  cnf(s14, plain, spl1_4, inference(rat,[],[s9,s13])).
% 0.90/0.39  cnf(s15, plain, spl1_5, inference(rat,[],[s4,s11,s10,s6,s13,s14])).
% 0.90/0.39  cnf(s16, plain, ~spl1_10, inference(rat,[],[s8,s14,s15])).
% 0.90/0.39  cnf(s17, plain, ~spl1_9, inference(rat,[],[s7,s14,s15])).
% 0.90/0.39  cnf(s18, plain, $false, inference(rat,[],[s5,s16,s14,s17,s15])).
% 0.90/0.39  thf(f2222,plain,(
% 0.90/0.39    $false),
% 0.90/0.39    inference(avatar_sat_refutation,[],[s18])).
% 0.90/0.39  % SZS output end Proof for theBenchmark
% 0.90/0.39  % (540456)------------------------------
% 0.90/0.39  % (540456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.90/0.39  % (540456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.90/0.39  % (540456)CaDiCaL version: 2.1.3
% 0.90/0.39  % (540456)Termination reason: Refutation
% 0.90/0.39  % (540456)Time elapsed: 0.050 s
% 0.90/0.39  % (540456)Peak memory usage: 13 MB
% 0.90/0.39  % (540456)Instructions burned: 226 (million)
% 0.90/0.39  % (540431)Success in time 0.155 s
% 0.90/0.39  % Vampire exiting
%------------------------------------------------------------------------------