%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX181^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 : n026.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.20s 0.35s
% Output : Refutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX181^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.08/0.18 % Computer : n026.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 16:12:57 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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.20/0.35 % (797593)Will run a generic schedule for satisfiability detection.
% 0.20/0.35 % (797599)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=852649467_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.35 % (797600)% WARNING: option uhcvi not known.
% 0.20/0.35 % (797600)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1956911360:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.35 % (797601)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3473220529:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.35 % (797605)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2012338030:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.35 % Exception at run slice level
% 0.20/0.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.35 % (797603)dis+10_1_sil=32000:sp=arity:random_seed=2277280918:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.35 % (797604)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=387539945:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.35 % (797606)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3980660796:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.35 % (797600)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.35 % (797604)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.35 % (797613)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3135002192:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.20/0.35 % (797600)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.20/0.35 % Exception at run slice level
% 0.20/0.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.35 % (797617)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4119495973:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.35 % (797603)Instruction limit reached!
% 0.20/0.35 % (797603)------------------------------
% 0.20/0.35 % (797603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (797603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (797603)CaDiCaL version: 2.1.3
% 0.20/0.35 % (797603)Termination reason: Instruction limit
% 0.20/0.35 % (797603)Termination phase: Saturation
% 0.20/0.35 % (797603)Time elapsed: 0.043 s
% 0.20/0.35 % (797603)Peak memory usage: 13 MB
% 0.20/0.35 % (797603)Instructions burned: 103 (million)
% 0.20/0.35 % (797604)Instruction limit reached!
% 0.20/0.35 % (797604)------------------------------
% 0.20/0.35 % (797604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (797604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (797604)CaDiCaL version: 2.1.3
% 0.20/0.35 % (797604)Termination reason: Instruction limit
% 0.20/0.35 % (797604)Termination phase: Saturation
% 0.20/0.35 % (797604)Time elapsed: 0.048 s
% 0.20/0.35 % (797604)Peak memory usage: 12 MB
% 0.20/0.35 % (797604)Instructions burned: 118 (million)
% 0.20/0.35 % (797605)Instruction limit reached!
% 0.20/0.35 % (797605)------------------------------
% 0.20/0.35 % (797605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (797605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (797605)CaDiCaL version: 2.1.3
% 0.20/0.35 % (797605)Termination reason: Instruction limit
% 0.20/0.35 % (797605)Termination phase: Saturation
% 0.20/0.35 % (797605)Time elapsed: 0.054 s
% 0.20/0.35 % (797605)Peak memory usage: 13 MB
% 0.20/0.35 % (797605)Instructions burned: 132 (million)
% 0.20/0.35 % (797617)Instruction limit reached!
% 0.20/0.35 % (797617)------------------------------
% 0.20/0.35 % (797617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (797617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (797617)CaDiCaL version: 2.1.3
% 0.20/0.35 % (797617)Termination reason: Instruction limit
% 0.20/0.35 % (797617)Termination phase: Saturation
% 0.20/0.35 % (797617)Time elapsed: 0.028 s
% 0.20/0.35 % (797617)Peak memory usage: 13 MB
% 0.20/0.35 % (797617)Instructions burned: 133 (million)
% 0.20/0.35 % (797619)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=1622642516:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.20/0.35 % (797622)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=331775601:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 0.20/0.35 % (797620)ott-21_1_sil=16000:fs=off:random_seed=373302963:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.20/0.35 % (797600) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-797593-797600"...
% 0.20/0.35 % (797619)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.35 % (797621)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2851375537:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 0.20/0.35 % Exception at run slice level
% 0.20/0.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.35 % (797619)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.20/0.35 % (797606)Instruction limit reached!
% 0.20/0.35 % (797606)------------------------------
% 0.20/0.35 % (797606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (797606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (797606)CaDiCaL version: 2.1.3
% 0.20/0.35 % (797606)Termination reason: Instruction limit
% 0.20/0.35 % (797606)Termination phase: Saturation
% 0.20/0.35 % (797606)Time elapsed: 0.078 s
% 0.20/0.35 % (797606)Peak memory usage: 13 MB
% 0.20/0.35 % (797606)Instructions burned: 160 (million)
% 0.20/0.35 % (797627)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1325630144:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 0.20/0.35 % (797600)...printing done.
% 0.20/0.35 % (797600)Refutation found. Thanks to Tanya!
% 0.20/0.35 % SZS status Theorem for theBenchmark
% 0.20/0.35 % SZS output start Proof for theBenchmark
% 0.20/0.35 thf(type_def_5, type, unsorted: $tType).
% 0.20/0.35 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.20/0.35 thf(type_def_7, type, d_unsorted: $tType).
% 0.20/0.35 thf(func_def_0, type, subrel: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_1, type, inv: (($i > $i > $o) > $i > $i > $o)).
% 0.20/0.35 thf(func_def_2, type, idem: ((($i > $i > $o) > $i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_3, type, infl: ((($i > $i > $o) > $i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_4, type, mono: ((($i > $i > $o) > $i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_5, type, refl: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_6, type, irrefl: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_7, type, rc: (($i > $i > $o) > $i > $i > $o)).
% 0.20/0.35 thf(func_def_8, type, symm: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_9, type, antisymm: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_10, type, asymm: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_11, type, sc: (($i > $i > $o) > $i > $i > $o)).
% 0.20/0.35 thf(func_def_12, type, trans: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_13, type, tc: (($i > $i > $o) > $i > $i > $o)).
% 0.20/0.35 thf(func_def_14, type, trc: (($i > $i > $o) > $i > $i > $o)).
% 0.20/0.35 thf(func_def_15, type, trsc: (($i > $i > $o) > $i > $i > $o)).
% 0.20/0.35 thf(func_def_16, type, po: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_17, type, so: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_18, type, total: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_19, type, term: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_20, type, ind: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_21, type, innf: (($i > $i > $o) > $i > $o)).
% 0.20/0.35 thf(func_def_22, type, nfof: (($i > $i > $o) > $i > $i > $o)).
% 0.20/0.35 thf(func_def_23, type, norm: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_24, type, join: (($i > $i > $o) > $i > $i > $o)).
% 0.20/0.35 thf(func_def_25, type, lconfl: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_26, type, sconfl: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_27, type, confl: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_28, type, cr: (($i > $i > $o) > $o)).
% 0.20/0.35 thf(func_def_29, type, d2unsorted: (d_unsorted > $i)).
% 0.20/0.35 thf(func_def_30, type, d_unsorted_0: d_unsorted).
% 0.20/0.35 thf(func_def_32, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.20/0.35 thf(func_def_33, type, vOR: ($o > $o > $o)).
% 0.20/0.35 thf(func_def_34, type, vNOT: ($o > $o)).
% 0.20/0.35 thf(func_def_35, type, db3: !>[X0: $tType]:(X0)).
% 0.20/0.35 thf(func_def_36, type, db0: !>[X0: $tType]:(X0)).
% 0.20/0.35 thf(func_def_37, type, db1: !>[X0: $tType]:(X0)).
% 0.20/0.35 thf(func_def_38, type, db2: !>[X0: $tType]:(X0)).
% 0.20/0.35 thf(func_def_39, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.20/0.35 thf(func_def_40, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.20/0.35 thf(func_def_41, type, db4: !>[X0: $tType]:(X0)).
% 0.20/0.35 thf(func_def_42, type, db5: !>[X0: $tType]:(X0)).
% 0.20/0.35 thf(func_def_43, type, vAND: ($o > $o > $o)).
% 0.20/0.35 thf(func_def_44, type, db7: !>[X0: $tType]:(X0)).
% 0.20/0.35 thf(func_def_45, type, db6: !>[X0: $tType]:(X0)).
% 0.20/0.35 thf(func_def_46, type, db9: !>[X0: $tType]:(X0)).
% 0.20/0.35 thf(func_def_47, type, db8: !>[X0: $tType]:(X0)).
% 0.20/0.35 thf(func_def_48, type, sK0: ($i > d_unsorted)).
% 0.20/0.35 thf(func_def_51, type, sK1: ($i > $i > $o)).
% 0.20/0.35 thf(func_def_54, type, sK4: ($i > $i > $o)).
% 0.20/0.35 thf(func_def_55, type, sK5: ($i > $i > $o)).
% 0.20/0.35 thf(func_def_56, type, sK6: ($i > $i > $o)).
% 0.20/0.35 thf(func_def_57, type, sK7: ($i > $i > $o)).
% 0.20/0.35 thf(func_def_58, type, sK8: ($i > $i > $o)).
% 0.20/0.35 thf(func_def_59, type, sK9: ($i > $i > $o)).
% 0.20/0.35 thf(func_def_60, type, sK10: ($i > $i > $o)).
% 0.20/0.35 thf(func_def_61, type, sK11: ($i > $i > $o)).
% 0.20/0.35 thf(func_def_62, type, sK12: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_63, type, sK13: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_64, type, sK14: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_65, type, sK15: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_66, type, sK16: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_67, type, sK17: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_68, type, sK18: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_69, type, sK19: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_70, type, sK20: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_71, type, sK21: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_72, type, sK22: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_73, type, sK23: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_74, type, sK24: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_75, type, sK25: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_76, type, sK26: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_77, type, sK27: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_78, type, sK28: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_79, type, sK29: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_80, type, sK30: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_81, type, sK31: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_82, type, sK32: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_83, type, sK33: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_84, type, sK34: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_85, type, sK35: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_86, type, sK36: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_87, type, sK37: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_88, type, sK38: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_89, type, sK39: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_90, type, sK40: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_91, type, sK41: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_92, type, sK42: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_93, type, sK43: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_94, type, sK44: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_95, type, sK45: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_96, type, sK46: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_97, type, sK47: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_98, type, sK48: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_99, type, sK49: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_100, type, sK50: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_101, type, sK51: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_102, type, sK52: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_103, type, sK53: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_104, type, sK54: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_105, type, sK55: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_106, type, sK56: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_107, type, sK57: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_108, type, sK58: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_109, type, sK59: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_110, type, sK60: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_111, type, sK61: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_112, type, sK62: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_113, type, sK63: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_114, type, sK64: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_115, type, sK65: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_116, type, sK66: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_117, type, sK67: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_118, type, sK68: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_119, type, sK69: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_120, type, sK70: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_121, type, sK71: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_122, type, sK72: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_123, type, sK73: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_124, type, sK74: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_125, type, sK75: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_126, type, sK76: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_127, type, sK77: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_128, type, sK78: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_129, type, sK79: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_130, type, sK80: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_131, type, sK81: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_132, type, sK82: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_133, type, sK83: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_134, type, sK84: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_135, type, sK85: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_136, type, sK86: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_137, type, sK87: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_138, type, sK88: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_139, type, sK89: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_140, type, sK90: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(func_def_141, type, sK91: (($i > $i > $o) > $i)).
% 0.20/0.35 thf(f1,axiom,(
% 0.20/0.35 (cr = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i,X36 : ($i > $i > $o),X37 : ($i > $i > $o)] : ((X37 @ X6 @ X7) | ~ ! [X14 : $i,X15 : $i] : ((X37 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X26 : $i] : ((X37 @ X12 @ X26) | ~(X37 @ X13 @ X26) | ~(X37 @ X12 @ X13)) | (X36 @ X7 @ X6) | ~ ! [X14 : $i,X15 : $i] : ((X36 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X25 : $i] : ((X36 @ X12 @ X25) | ~(X36 @ X13 @ X25) | ~(X36 @ X12 @ X13)) | ~ ! [X27 : $i] : (~ ! [X5 : ($i > $i > $o)] : ((X5 @ X6 @ X27) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X26 : $i] : ((X5 @ X12 @ X26) | ~(X5 @ X13 @ X26) | ~(X5 @ X12 @ X13))) | ~ ! [X5 : ($i > $i > $o)] : ((X5 @ X7 @ X27) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X25 : $i] : ((X5 @ X12 @ X25) | ~(X5 @ X13 @ X25) | ~(X5 @ X12 @ X13)))) | (X6 = X7) | (~ ! [X5 : ($i > $i > $o)] : ((X5 @ X6 @ X7) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X11 : $i] : ((X5 @ X12 @ X11) | ~(X5 @ X13 @ X11) | ~(X5 @ X12 @ X13))) & ~ ! [X5 : ($i > $i > $o)] : ((X5 @ X7 @ X6) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X11 : $i] : ((X5 @ X12 @ X11) | ~(X5 @ X13 @ X11) | ~(X5 @ X12 @ X13))) & (X6 != X7)))))) & (confl = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i,X11 : $i,X33 : ($i > $i > $o),X34 : ($i > $i > $o)] : ((X34 @ X11 @ X7) | ~ ! [X14 : $i,X15 : $i] : ((X34 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X26 : $i] : ((X34 @ X12 @ X26) | ~(X34 @ X13 @ X26) | ~(X34 @ X12 @ X13)) | (X33 @ X7 @ X11) | ~ ! [X14 : $i,X15 : $i] : ((X33 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X25 : $i] : ((X33 @ X12 @ X25) | ~(X33 @ X13 @ X25) | ~(X33 @ X12 @ X13)) | ~ ! [X27 : $i] : (~ ! [X5 : ($i > $i > $o)] : ((X5 @ X11 @ X27) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X26 : $i] : ((X5 @ X12 @ X26) | ~(X5 @ X13 @ X26) | ~(X5 @ X12 @ X13))) | ~ ! [X5 : ($i > $i > $o)] : ((X5 @ X7 @ X27) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X25 : $i] : ((X5 @ X12 @ X25) | ~(X5 @ X13 @ X25) | ~(X5 @ X12 @ X13)))) | (X7 = X11) | (~ ! [X5 : ($i > $i > $o)] : ((X5 @ X6 @ X7) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X35 : $i] : ((X5 @ X12 @ X35) | ~(X5 @ X13 @ X35) | ~(X5 @ X12 @ X13))) & (X6 != X7)) | (~ ! [X5 : ($i > $i > $o)] : ((X5 @ X6 @ X11) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X26 : $i] : ((X5 @ X12 @ X26) | ~(X5 @ X13 @ X26) | ~(X5 @ X12 @ X13))) & (X6 != X11)))))) & (sconfl = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i,X11 : $i,X30 : ($i > $i > $o),X31 : ($i > $i > $o)] : ((X31 @ X11 @ X7) | ~ ! [X14 : $i,X15 : $i] : ((X31 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X26 : $i] : ((X31 @ X12 @ X26) | ~(X31 @ X13 @ X26) | ~(X31 @ X12 @ X13)) | (X30 @ X7 @ X11) | ~ ! [X14 : $i,X15 : $i] : ((X30 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X25 : $i] : ((X30 @ X12 @ X25) | ~(X30 @ X13 @ X25) | ~(X30 @ X12 @ X13)) | ~ ! [X27 : $i] : (~ ! [X5 : ($i > $i > $o)] : ((X5 @ X11 @ X27) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X26 : $i] : ((X5 @ X12 @ X26) | ~(X5 @ X13 @ X26) | ~(X5 @ X12 @ X13))) | ~ ! [X5 : ($i > $i > $o)] : ((X5 @ X7 @ X27) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X25 : $i] : ((X5 @ X12 @ X25) | ~(X5 @ X13 @ X25) | ~(X5 @ X12 @ X13)))) | (X7 = X11) | (~ ! [X5 : ($i > $i > $o)] : ((X5 @ X6 @ X7) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X32 : $i] : ((X5 @ X12 @ X32) | ~(X5 @ X13 @ X32) | ~(X5 @ X12 @ X13))) & (X6 != X7)) | ~(X4 @ X6 @ X11))))) & (lconfl = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i,X11 : $i,X28 : ($i > $i > $o),X29 : ($i > $i > $o)] : ((X29 @ X11 @ X7) | ~ ! [X14 : $i,X15 : $i] : ((X29 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X26 : $i] : ((X29 @ X12 @ X26) | ~(X29 @ X13 @ X26) | ~(X29 @ X12 @ X13)) | (X28 @ X7 @ X11) | ~ ! [X14 : $i,X15 : $i] : ((X28 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X25 : $i] : ((X28 @ X12 @ X25) | ~(X28 @ X13 @ X25) | ~(X28 @ X12 @ X13)) | ~ ! [X27 : $i] : (~ ! [X5 : ($i > $i > $o)] : ((X5 @ X11 @ X27) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X26 : $i] : ((X5 @ X12 @ X26) | ~(X5 @ X13 @ X26) | ~(X5 @ X12 @ X13))) | ~ ! [X5 : ($i > $i > $o)] : ((X5 @ X7 @ X27) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X25 : $i] : ((X5 @ X12 @ X25) | ~(X5 @ X13 @ X25) | ~(X5 @ X12 @ X13)))) | (X7 = X11) | ~(X4 @ X6 @ X7) | ~(X4 @ X6 @ X11))))) & (join = (^[X4 : ($i > $i > $o), X6 : $i, X7 : $i] : (~(! [X27 : $i] : (~ ! [X5 : ($i > $i > $o)] : ((X5 @ X6 @ X27) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X26 : $i] : ((X5 @ X12 @ X26) | ~(X5 @ X13 @ X26) | ~(X5 @ X12 @ X13))) | ~ ! [X5 : ($i > $i > $o)] : ((X5 @ X7 @ X27) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X25 : $i] : ((X5 @ X12 @ X25) | ~(X5 @ X13 @ X25) | ~(X5 @ X12 @ X13)))) & ~ ! [X5 : ($i > $i > $o)] : ((X5 @ X6 @ X7) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X26 : $i] : ((X5 @ X12 @ X26) | ~(X5 @ X13 @ X26) | ~(X5 @ X12 @ X13))) & ~ ! [X5 : ($i > $i > $o)] : ((X5 @ X7 @ X6) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X25 : $i] : ((X5 @ X12 @ X25) | ~(X5 @ X13 @ X25) | ~(X5 @ X12 @ X13))) & (X6 != X7))))) & (norm = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X23 : $i] : (~ ! [X24 : $i] : (~ ! [X22 : $i] : ~(X4 @ X24 @ X22) | ~ ! [X5 : ($i > $i > $o)] : ((X5 @ X6 @ X24) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X11 : $i] : ((X5 @ X12 @ X11) | ~(X5 @ X13 @ X11) | ~(X5 @ X12 @ X13)))) | ~(X4 @ X6 @ X23))))) & (nfof = (^[X4 : ($i > $i > $o), X6 : $i, X7 : $i] : (! [X22 : $i] : ~(X4 @ X6 @ X22) & (! [X5 : ($i > $i > $o)] : ((X5 @ X7 @ X6) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X11 : $i] : ((X5 @ X12 @ X11) | ~(X5 @ X13 @ X11) | ~(X5 @ X12 @ X13))) | (X6 = X7))))) & (innf = (^[X4 : ($i > $i > $o), X6 : $i] : (! [X7 : $i] : ~(X4 @ X6 @ X7)))) & (ind = (^[X4 : ($i > $i > $o)] : (! [X20 : ($i > $o),X21 : $i] : ((X20 @ X21) | ~ ! [X6 : $i] : ((X20 @ X6) | ~ ! [X7 : $i] : ((X20 @ X7) | ~ ! [X5 : ($i > $i > $o)] : ((X5 @ X6 @ X7) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X11 : $i] : ((X5 @ X12 @ X11) | ~(X5 @ X13 @ X11) | ~(X5 @ X12 @ X13))))))))) & (term = (^[X4 : ($i > $i > $o)] : (! [X18 : ($i > $o),X19 : $i] : (~ ! [X6 : $i] : (~ ! [X7 : $i] : (~(X4 @ X6 @ X7) | ~(X18 @ X7)) | ~(X18 @ X6)) | ~(X18 @ X19))))) & (total = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i] : ((X4 @ X7 @ X6) | (X4 @ X6 @ X7) | (X6 = X7))))) & (so = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i,X11 : $i] : ((X4 @ X6 @ X11) | ~(X4 @ X7 @ X11) | ~(X4 @ X6 @ X7)) & ! [X6 : $i,X7 : $i] : (~(X4 @ X7 @ X6) | ~(X4 @ X6 @ X7))))) & (po = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i,X11 : $i] : ((X4 @ X6 @ X11) | ~(X4 @ X7 @ X11) | ~(X4 @ X6 @ X7)) & ! [X6 : $i,X7 : $i] : ((X6 = X7) | ~(X4 @ X7 @ X6) | ~(X4 @ X6 @ X7)) & ! [X6 : $i] : (X4 @ X6 @ X6)))) & (trsc = (^[X4 : ($i > $i > $o), X16 : $i, X17 : $i] : (! [X5 : ($i > $i > $o)] : ((X5 @ X16 @ X17) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X11 : $i] : ((X5 @ X12 @ X11) | ~(X5 @ X13 @ X11) | ~(X5 @ X12 @ X13))) | ! [X5 : ($i > $i > $o)] : ((X5 @ X17 @ X16) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X11 : $i] : ((X5 @ X12 @ X11) | ~(X5 @ X13 @ X11) | ~(X5 @ X12 @ X13))) | (X16 = X17)))) & (trc = (^[X4 : ($i > $i > $o), X16 : $i, X17 : $i] : (! [X5 : ($i > $i > $o)] : ((X5 @ X16 @ X17) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X11 : $i] : ((X5 @ X12 @ X11) | ~(X5 @ X13 @ X11) | ~(X5 @ X12 @ X13))) | (X16 = X17)))) & (tc = (^[X4 : ($i > $i > $o), X6 : $i, X7 : $i] : (! [X5 : ($i > $i > $o)] : ((X5 @ X6 @ X7) | ~ ! [X14 : $i,X15 : $i] : ((X5 @ X14 @ X15) | ~(X4 @ X14 @ X15)) | ~ ! [X12 : $i,X13 : $i,X11 : $i] : ((X5 @ X12 @ X11) | ~(X5 @ X13 @ X11) | ~(X5 @ X12 @ X13)))))) & (trans = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i,X11 : $i] : ((X4 @ X6 @ X11) | ~(X4 @ X7 @ X11) | ~(X4 @ X6 @ X7))))) & (sc = (^[X4 : ($i > $i > $o), X6 : $i, X7 : $i] : ((X4 @ X6 @ X7) | (X4 @ X7 @ X6)))) & (asymm = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i] : (~(X4 @ X7 @ X6) | ~(X4 @ X6 @ X7))))) & (antisymm = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i] : ((X6 = X7) | ~(X4 @ X7 @ X6) | ~(X4 @ X6 @ X7))))) & (symm = (^[X4 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i] : ((X4 @ X7 @ X6) | ~(X4 @ X6 @ X7))))) & (rc = (^[X4 : ($i > $i > $o), X6 : $i, X7 : $i] : ((X4 @ X6 @ X7) | (X6 = X7)))) & (irrefl = (^[X4 : ($i > $i > $o)] : (! [X6 : $i] : ~(X4 @ X6 @ X6)))) & (refl = (^[X4 : ($i > $i > $o)] : (! [X6 : $i] : (X4 @ X6 @ X6)))) & (mono = (^[X8 : (($i > $i > $o) > $i > $i > $o)] : (! [X4 : ($i > $i > $o),X5 : ($i > $i > $o),X9 : $i,X10 : $i] : ((X8 @ X5 @ X9 @ X10) | ~(X8 @ X4 @ X9 @ X10) | ~ ! [X6 : $i,X7 : $i] : ((X5 @ X6 @ X7) | ~(X4 @ X6 @ X7)))))) & (infl = (^[X8 : (($i > $i > $o) > $i > $i > $o)] : (! [X4 : ($i > $i > $o),X6 : $i,X7 : $i] : ((X8 @ X4 @ X6 @ X7) | ~(X4 @ X6 @ X7))))) & (idem = (^[X8 : (($i > $i > $o) > $i > $i > $o)] : (! [X4 : ($i > $i > $o)] : (((X8 @ X4)) = ((X8 @ (X8 @ X4))))))) & (inv = (^[X4 : ($i > $i > $o), X6 : $i, X7 : $i] : ((X4 @ X7 @ X6)))) & (subrel = (^[X4 : ($i > $i > $o), X5 : ($i > $i > $o)] : (! [X6 : $i,X7 : $i] : ((X5 @ X6 @ X7) | ~(X4 @ X6 @ X7))))) & ! [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.20/0.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p',sev441_1)).
% 0.20/0.35 thf(f2,conjecture,(
% 0.20/0.35 (trsc = (^[X0 : ($i > $i > $o)] : ((sc @ (rc @ (tc @ X0))))))),
% 0.20/0.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitive_reflexive_symmetric_closure)).
% 0.20/0.35 thf(f3,negated_conjecture,(
% 0.20/0.35 ~ (trsc = (^[X0 : ($i > $i > $o)] : ((sc @ (rc @ (tc @ X0))))))),
% 0.20/0.35 inference(negated_conjecture,[status(cth)],[f2])).
% 0.20/0.35 thf(f4,plain,(
% 0.20/0.35 (cr = (^[X0 : ($i > $i > $o)] : (! [X1 : $i,X2 : $i,X3 : ($i > $i > $o),X4 : ($i > $i > $o)] : ((X4 @ X1 @ X2) | ~ ! [X5 : $i,X6 : $i] : ((X4 @ X5 @ X6) | ~(X0 @ X5 @ X6)) | ~ ! [X7 : $i,X8 : $i,X9 : $i] : ((X4 @ X7 @ X9) | ~(X4 @ X8 @ X9) | ~(X4 @ X7 @ X8)) | (X3 @ X2 @ X1) | ~ ! [X10 : $i,X11 : $i] : ((X3 @ X10 @ X11) | ~(X0 @ X10 @ X11)) | ~ ! [X12 : $i,X13 : $i,X14 : $i] : ((X3 @ X12 @ X14) | ~(X3 @ X13 @ X14) | ~(X3 @ X12 @ X13)) | ~ ! [X15 : $i] : (~ ! [X16 : ($i > $i > $o)] : ((X16 @ X1 @ X15) | ~ ! [X17 : $i,X18 : $i] : ((X16 @ X17 @ X18) | ~(X0 @ X17 @ X18)) | ~ ! [X19 : $i,X20 : $i,X21 : $i] : ((X16 @ X19 @ X21) | ~(X16 @ X20 @ X21) | ~(X16 @ X19 @ X20))) | ~ ! [X22 : ($i > $i > $o)] : ((X22 @ X2 @ X15) | ~ ! [X23 : $i,X24 : $i] : ((X22 @ X23 @ X24) | ~(X0 @ X23 @ X24)) | ~ ! [X25 : $i,X26 : $i,X27 : $i] : ((X22 @ X25 @ X27) | ~(X22 @ X26 @ X27) | ~(X22 @ X25 @ X26)))) | (X1 = X2) | (~ ! [X28 : ($i > $i > $o)] : ((X28 @ X1 @ X2) | ~ ! [X29 : $i,X30 : $i] : ((X28 @ X29 @ X30) | ~(X0 @ X29 @ X30)) | ~ ! [X31 : $i,X32 : $i,X33 : $i] : ((X28 @ X31 @ X33) | ~(X28 @ X32 @ X33) | ~(X28 @ X31 @ X32))) & ~ ! [X34 : ($i > $i > $o)] : ((X34 @ X2 @ X1) | ~ ! [X35 : $i,X36 : $i] : ((X34 @ X35 @ X36) | ~(X0 @ X35 @ X36)) | ~ ! [X37 : $i,X38 : $i,X39 : $i] : ((X34 @ X37 @ X39) | ~(X34 @ X38 @ X39) | ~(X34 @ X37 @ X38))) & (X1 != X2)))))) & (confl = (^[X40 : ($i > $i > $o)] : (! [X41 : $i,X42 : $i,X43 : $i,X44 : ($i > $i > $o),X45 : ($i > $i > $o)] : ((X45 @ X43 @ X42) | ~ ! [X46 : $i,X47 : $i] : ((X45 @ X46 @ X47) | ~(X40 @ X46 @ X47)) | ~ ! [X48 : $i,X49 : $i,X50 : $i] : ((X45 @ X48 @ X50) | ~(X45 @ X49 @ X50) | ~(X45 @ X48 @ X49)) | (X44 @ X42 @ X43) | ~ ! [X51 : $i,X52 : $i] : ((X44 @ X51 @ X52) | ~(X40 @ X51 @ X52)) | ~ ! [X53 : $i,X54 : $i,X55 : $i] : ((X44 @ X53 @ X55) | ~(X44 @ X54 @ X55) | ~(X44 @ X53 @ X54)) | ~ ! [X56 : $i] : (~ ! [X57 : ($i > $i > $o)] : ((X57 @ X43 @ X56) | ~ ! [X58 : $i,X59 : $i] : ((X57 @ X58 @ X59) | ~(X40 @ X58 @ X59)) | ~ ! [X60 : $i,X61 : $i,X62 : $i] : ((X57 @ X60 @ X62) | ~(X57 @ X61 @ X62) | ~(X57 @ X60 @ X61))) | ~ ! [X63 : ($i > $i > $o)] : ((X63 @ X42 @ X56) | ~ ! [X64 : $i,X65 : $i] : ((X63 @ X64 @ X65) | ~(X40 @ X64 @ X65)) | ~ ! [X66 : $i,X67 : $i,X68 : $i] : ((X63 @ X66 @ X68) | ~(X63 @ X67 @ X68) | ~(X63 @ X66 @ X67)))) | (X42 = X43) | (~ ! [X69 : ($i > $i > $o)] : ((X69 @ X41 @ X42) | ~ ! [X70 : $i,X71 : $i] : ((X69 @ X70 @ X71) | ~(X40 @ X70 @ X71)) | ~ ! [X72 : $i,X73 : $i,X74 : $i] : ((X69 @ X72 @ X74) | ~(X69 @ X73 @ X74) | ~(X69 @ X72 @ X73))) & (X41 != X42)) | (~ ! [X75 : ($i > $i > $o)] : ((X75 @ X41 @ X43) | ~ ! [X76 : $i,X77 : $i] : ((X75 @ X76 @ X77) | ~(X40 @ X76 @ X77)) | ~ ! [X78 : $i,X79 : $i,X80 : $i] : ((X75 @ X78 @ X80) | ~(X75 @ X79 @ X80) | ~(X75 @ X78 @ X79))) & (X41 != X43)))))) & (sconfl = (^[X81 : ($i > $i > $o)] : (! [X82 : $i,X83 : $i,X84 : $i,X85 : ($i > $i > $o),X86 : ($i > $i > $o)] : ((X86 @ X84 @ X83) | ~ ! [X87 : $i,X88 : $i] : ((X86 @ X87 @ X88) | ~(X81 @ X87 @ X88)) | ~ ! [X89 : $i,X90 : $i,X91 : $i] : ((X86 @ X89 @ X91) | ~(X86 @ X90 @ X91) | ~(X86 @ X89 @ X90)) | (X85 @ X83 @ X84) | ~ ! [X92 : $i,X93 : $i] : ((X85 @ X92 @ X93) | ~(X81 @ X92 @ X93)) | ~ ! [X94 : $i,X95 : $i,X96 : $i] : ((X85 @ X94 @ X96) | ~(X85 @ X95 @ X96) | ~(X85 @ X94 @ X95)) | ~ ! [X97 : $i] : (~ ! [X98 : ($i > $i > $o)] : ((X98 @ X84 @ X97) | ~ ! [X99 : $i,X100 : $i] : ((X98 @ X99 @ X100) | ~(X81 @ X99 @ X100)) | ~ ! [X101 : $i,X102 : $i,X103 : $i] : ((X98 @ X101 @ X103) | ~(X98 @ X102 @ X103) | ~(X98 @ X101 @ X102))) | ~ ! [X104 : ($i > $i > $o)] : ((X104 @ X83 @ X97) | ~ ! [X105 : $i,X106 : $i] : ((X104 @ X105 @ X106) | ~(X81 @ X105 @ X106)) | ~ ! [X107 : $i,X108 : $i,X109 : $i] : ((X104 @ X107 @ X109) | ~(X104 @ X108 @ X109) | ~(X104 @ X107 @ X108)))) | (X83 = X84) | (~ ! [X110 : ($i > $i > $o)] : ((X110 @ X82 @ X83) | ~ ! [X111 : $i,X112 : $i] : ((X110 @ X111 @ X112) | ~(X81 @ X111 @ X112)) | ~ ! [X113 : $i,X114 : $i,X115 : $i] : ((X110 @ X113 @ X115) | ~(X110 @ X114 @ X115) | ~(X110 @ X113 @ X114))) & (X82 != X83)) | ~(X81 @ X82 @ X84))))) & (lconfl = (^[X116 : ($i > $i > $o)] : (! [X117 : $i,X118 : $i,X119 : $i,X120 : ($i > $i > $o),X121 : ($i > $i > $o)] : ((X121 @ X119 @ X118) | ~ ! [X122 : $i,X123 : $i] : ((X121 @ X122 @ X123) | ~(X116 @ X122 @ X123)) | ~ ! [X124 : $i,X125 : $i,X126 : $i] : ((X121 @ X124 @ X126) | ~(X121 @ X125 @ X126) | ~(X121 @ X124 @ X125)) | (X120 @ X118 @ X119) | ~ ! [X127 : $i,X128 : $i] : ((X120 @ X127 @ X128) | ~(X116 @ X127 @ X128)) | ~ ! [X129 : $i,X130 : $i,X131 : $i] : ((X120 @ X129 @ X131) | ~(X120 @ X130 @ X131) | ~(X120 @ X129 @ X130)) | ~ ! [X132 : $i] : (~ ! [X133 : ($i > $i > $o)] : ((X133 @ X119 @ X132) | ~ ! [X134 : $i,X135 : $i] : ((X133 @ X134 @ X135) | ~(X116 @ X134 @ X135)) | ~ ! [X136 : $i,X137 : $i,X138 : $i] : ((X133 @ X136 @ X138) | ~(X133 @ X137 @ X138) | ~(X133 @ X136 @ X137))) | ~ ! [X139 : ($i > $i > $o)] : ((X139 @ X118 @ X132) | ~ ! [X140 : $i,X141 : $i] : ((X139 @ X140 @ X141) | ~(X116 @ X140 @ X141)) | ~ ! [X142 : $i,X143 : $i,X144 : $i] : ((X139 @ X142 @ X144) | ~(X139 @ X143 @ X144) | ~(X139 @ X142 @ X143)))) | (X118 = X119) | ~(X116 @ X117 @ X118) | ~(X116 @ X117 @ X119))))) & (join = (^[X145 : ($i > $i > $o), X146 : $i, X147 : $i] : (~(! [X148 : $i] : (~ ! [X149 : ($i > $i > $o)] : ((X149 @ X146 @ X148) | ~ ! [X150 : $i,X151 : $i] : ((X149 @ X150 @ X151) | ~(X145 @ X150 @ X151)) | ~ ! [X152 : $i,X153 : $i,X154 : $i] : ((X149 @ X152 @ X154) | ~(X149 @ X153 @ X154) | ~(X149 @ X152 @ X153))) | ~ ! [X155 : ($i > $i > $o)] : ((X155 @ X147 @ X148) | ~ ! [X156 : $i,X157 : $i] : ((X155 @ X156 @ X157) | ~(X145 @ X156 @ X157)) | ~ ! [X158 : $i,X159 : $i,X160 : $i] : ((X155 @ X158 @ X160) | ~(X155 @ X159 @ X160) | ~(X155 @ X158 @ X159)))) & ~ ! [X161 : ($i > $i > $o)] : ((X161 @ X146 @ X147) | ~ ! [X162 : $i,X163 : $i] : ((X161 @ X162 @ X163) | ~(X145 @ X162 @ X163)) | ~ ! [X164 : $i,X165 : $i,X166 : $i] : ((X161 @ X164 @ X166) | ~(X161 @ X165 @ X166) | ~(X161 @ X164 @ X165))) & ~ ! [X167 : ($i > $i > $o)] : ((X167 @ X147 @ X146) | ~ ! [X168 : $i,X169 : $i] : ((X167 @ X168 @ X169) | ~(X145 @ X168 @ X169)) | ~ ! [X170 : $i,X171 : $i,X172 : $i] : ((X167 @ X170 @ X172) | ~(X167 @ X171 @ X172) | ~(X167 @ X170 @ X171))) & (X146 != X147))))) & (norm = (^[X173 : ($i > $i > $o)] : (! [X174 : $i,X175 : $i] : (~ ! [X176 : $i] : (~ ! [X177 : $i] : ~(X173 @ X176 @ X177) | ~ ! [X178 : ($i > $i > $o)] : ((X178 @ X174 @ X176) | ~ ! [X179 : $i,X180 : $i] : ((X178 @ X179 @ X180) | ~(X173 @ X179 @ X180)) | ~ ! [X181 : $i,X182 : $i,X183 : $i] : ((X178 @ X181 @ X183) | ~(X178 @ X182 @ X183) | ~(X178 @ X181 @ X182)))) | ~(X173 @ X174 @ X175))))) & (nfof = (^[X184 : ($i > $i > $o), X185 : $i, X186 : $i] : (! [X187 : $i] : ~(X184 @ X185 @ X187) & (! [X188 : ($i > $i > $o)] : ((X188 @ X186 @ X185) | ~ ! [X189 : $i,X190 : $i] : ((X188 @ X189 @ X190) | ~(X184 @ X189 @ X190)) | ~ ! [X191 : $i,X192 : $i,X193 : $i] : ((X188 @ X191 @ X193) | ~(X188 @ X192 @ X193) | ~(X188 @ X191 @ X192))) | (X185 = X186))))) & (innf = (^[X194 : ($i > $i > $o), X195 : $i] : (! [X196 : $i] : ~(X194 @ X195 @ X196)))) & (ind = (^[X197 : ($i > $i > $o)] : (! [X198 : ($i > $o),X199 : $i] : ((X198 @ X199) | ~ ! [X200 : $i] : ((X198 @ X200) | ~ ! [X201 : $i] : ((X198 @ X201) | ~ ! [X202 : ($i > $i > $o)] : ((X202 @ X200 @ X201) | ~ ! [X203 : $i,X204 : $i] : ((X202 @ X203 @ X204) | ~(X197 @ X203 @ X204)) | ~ ! [X205 : $i,X206 : $i,X207 : $i] : ((X202 @ X205 @ X207) | ~(X202 @ X206 @ X207) | ~(X202 @ X205 @ X206))))))))) & (term = (^[X208 : ($i > $i > $o)] : (! [X209 : ($i > $o),X210 : $i] : (~ ! [X211 : $i] : (~ ! [X212 : $i] : (~(X208 @ X211 @ X212) | ~(X209 @ X212)) | ~(X209 @ X211)) | ~(X209 @ X210))))) & (total = (^[X213 : ($i > $i > $o)] : (! [X214 : $i,X215 : $i] : ((X213 @ X215 @ X214) | (X213 @ X214 @ X215) | (X214 = X215))))) & (so = (^[X216 : ($i > $i > $o)] : (! [X217 : $i,X218 : $i,X219 : $i] : ((X216 @ X217 @ X219) | ~(X216 @ X218 @ X219) | ~(X216 @ X217 @ X218)) & ! [X220 : $i,X221 : $i] : (~(X216 @ X221 @ X220) | ~(X216 @ X220 @ X221))))) & (po = (^[X222 : ($i > $i > $o)] : (! [X223 : $i,X224 : $i,X225 : $i] : ((X222 @ X223 @ X225) | ~(X222 @ X224 @ X225) | ~(X222 @ X223 @ X224)) & ! [X226 : $i,X227 : $i] : ((X226 = X227) | ~(X222 @ X227 @ X226) | ~(X222 @ X226 @ X227)) & ! [X228 : $i] : (X222 @ X228 @ X228)))) & (trsc = (^[X229 : ($i > $i > $o), X230 : $i, X231 : $i] : (! [X232 : ($i > $i > $o)] : ((X232 @ X230 @ X231) | ~ ! [X233 : $i,X234 : $i] : ((X232 @ X233 @ X234) | ~(X229 @ X233 @ X234)) | ~ ! [X235 : $i,X236 : $i,X237 : $i] : ((X232 @ X235 @ X237) | ~(X232 @ X236 @ X237) | ~(X232 @ X235 @ X236))) | ! [X238 : ($i > $i > $o)] : ((X238 @ X231 @ X230) | ~ ! [X239 : $i,X240 : $i] : ((X238 @ X239 @ X240) | ~(X229 @ X239 @ X240)) | ~ ! [X241 : $i,X242 : $i,X243 : $i] : ((X238 @ X241 @ X243) | ~(X238 @ X242 @ X243) | ~(X238 @ X241 @ X242))) | (X230 = X231)))) & (trc = (^[X244 : ($i > $i > $o), X245 : $i, X246 : $i] : (! [X247 : ($i > $i > $o)] : ((X247 @ X245 @ X246) | ~ ! [X248 : $i,X249 : $i] : ((X247 @ X248 @ X249) | ~(X244 @ X248 @ X249)) | ~ ! [X250 : $i,X251 : $i,X252 : $i] : ((X247 @ X250 @ X252) | ~(X247 @ X251 @ X252) | ~(X247 @ X250 @ X251))) | (X245 = X246)))) & (tc = (^[X253 : ($i > $i > $o), X254 : $i, X255 : $i] : (! [X256 : ($i > $i > $o)] : ((X256 @ X254 @ X255) | ~ ! [X257 : $i,X258 : $i] : ((X256 @ X257 @ X258) | ~(X253 @ X257 @ X258)) | ~ ! [X259 : $i,X260 : $i,X261 : $i] : ((X256 @ X259 @ X261) | ~(X256 @ X260 @ X261) | ~(X256 @ X259 @ X260)))))) & (trans = (^[X262 : ($i > $i > $o)] : (! [X263 : $i,X264 : $i,X265 : $i] : ((X262 @ X263 @ X265) | ~(X262 @ X264 @ X265) | ~(X262 @ X263 @ X264))))) & (sc = (^[X266 : ($i > $i > $o), X267 : $i, X268 : $i] : ((X266 @ X267 @ X268) | (X266 @ X268 @ X267)))) & (asymm = (^[X269 : ($i > $i > $o)] : (! [X270 : $i,X271 : $i] : (~(X269 @ X271 @ X270) | ~(X269 @ X270 @ X271))))) & (antisymm = (^[X272 : ($i > $i > $o)] : (! [X273 : $i,X274 : $i] : ((X273 = X274) | ~(X272 @ X274 @ X273) | ~(X272 @ X273 @ X274))))) & (symm = (^[X275 : ($i > $i > $o)] : (! [X276 : $i,X277 : $i] : ((X275 @ X277 @ X276) | ~(X275 @ X276 @ X277))))) & (rc = (^[X278 : ($i > $i > $o), X279 : $i, X280 : $i] : ((X278 @ X279 @ X280) | (X279 = X280)))) & (irrefl = (^[X281 : ($i > $i > $o)] : (! [X282 : $i] : ~(X281 @ X282 @ X282)))) & (refl = (^[X283 : ($i > $i > $o)] : (! [X284 : $i] : (X283 @ X284 @ X284)))) & (mono = (^[X285 : (($i > $i > $o) > $i > $i > $o)] : (! [X286 : ($i > $i > $o),X287 : ($i > $i > $o),X288 : $i,X289 : $i] : ((X285 @ X287 @ X288 @ X289) | ~(X285 @ X286 @ X288 @ X289) | ~ ! [X290 : $i,X291 : $i] : ((X287 @ X290 @ X291) | ~(X286 @ X290 @ X291)))))) & (infl = (^[X292 : (($i > $i > $o) > $i > $i > $o)] : (! [X293 : ($i > $i > $o),X294 : $i,X295 : $i] : ((X292 @ X293 @ X294 @ X295) | ~(X293 @ X294 @ X295))))) & (idem = (^[X296 : (($i > $i > $o) > $i > $i > $o)] : (! [X297 : ($i > $i > $o)] : (((X296 @ X297)) = ((X296 @ (X296 @ X297))))))) & (inv = (^[X298 : ($i > $i > $o), X299 : $i, X300 : $i] : ((X298 @ X300 @ X299)))) & (subrel = (^[X301 : ($i > $i > $o), X302 : ($i > $i > $o)] : (! [X303 : $i,X304 : $i] : ((X302 @ X303 @ X304) | ~(X301 @ X303 @ X304))))) & ! [X305 : d_unsorted,X306 : d_unsorted] : ((((d2unsorted @ X305)) = ((d2unsorted @ X306))) => (X305 = X306)) & ! [X307 : d_unsorted] : (d_unsorted_0 = X307) & ! [X308 : $i] : ? [X309 : d_unsorted] : (((d2unsorted @ X309)) = X308)),
% 0.20/0.35 inference(rectify,[],[f1])).
% 0.20/0.35 thf(f5,plain,(
% 0.20/0.35 (cr = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((((((((((~ (Y4 = Y3)) & (~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y3 @ Y4)))))) & (~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y4 @ Y3)))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y3 @ Y5))))) | (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y4 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y2 @ Y7 @ Y6)) | (~ (Y2 @ Y6 @ Y5))) | (Y2 @ Y7 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y2 @ Y6 @ Y5)))))))) | (Y2 @ Y3 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y1 @ Y7 @ Y6)) | (~ (Y1 @ Y6 @ Y5))) | (Y1 @ Y7 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y1 @ Y6 @ Y5)))))))) | (Y1 @ Y4 @ Y3)))))))))))) & (confl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((((((((~ (Y5 = Y3)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y3)))))) | ((~ (Y5 = Y4)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y4))))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (sconfl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((((((((~ (Y0 @ Y5 @ Y3)) | ((~ (Y5 = Y4)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y4))))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (lconfl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((((((((~ (Y0 @ Y5 @ Y3)) | (~ (Y0 @ Y5 @ Y4))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (join = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (~ ((((~ (Y1 = Y2)) & (~ (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1)))))) & (~ (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y2 @ Y3))))) | (~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y1 @ Y3)))))))))))))))) & (norm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y4 : $i]: (~ (Y0 @ Y3 @ Y4)))))))))))))))) & (nfof = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) & (!! @ $i @ (^[Y3 : $i]: (~ (Y0 @ Y1 @ Y3))))))))))) & (innf = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2)))))))) & (ind = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ $i @ (^[Y4 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y3 @ Y4))))) | (Y2 @ Y4))))) | (Y2 @ Y3))))) | (Y2 @ Y1)))))))) & (term = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((~ (Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y2 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y2 @ Y4)) | (~ (Y0 @ Y3 @ Y4))))))))))))))))) & (total = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((Y2 = Y1) | (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (so = (^[Y0 : $i > $i > $o]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))))) & (po = (^[Y0 : $i > $i > $o]: (((!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))) | (Y2 = Y1))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))))) & (trsc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2))))))))))) & (trc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2))))))))))) & (tc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))))))) & (trans = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1)))))))))) & (sc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y0 @ Y2 @ Y1) | (Y0 @ Y1 @ Y2)))))))) & (asymm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))))))))) & (antisymm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))) | (Y2 = Y1)))))))) & (symm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (rc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y1 = Y2) | (Y0 @ Y1 @ Y2)))))))) & (irrefl = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1 @ Y1)))))) & (refl = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mono = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y4 @ Y6 @ Y5)) | (Y3 @ Y6 @ Y5))))))) | (~ (Y0 @ Y4 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y2 @ Y1)))))))))))) & (infl = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: ((~ (Y3 @ Y2 @ Y1)) | (Y0 @ Y3 @ Y2 @ Y1)))))))))) & (idem = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: ((Y0 @ Y1) = (Y0 @ (Y0 @ Y1))))))) & (inv = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (Y0 @ Y2 @ Y1))))))) & (subrel = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $i > $o]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))))) & ! [X305 : d_unsorted,X306 : d_unsorted] : ((((d2unsorted @ X305)) = ((d2unsorted @ X306))) => (X305 = X306)) & ! [X307 : d_unsorted] : (d_unsorted_0 = X307) & ! [X308 : $i] : ? [X309 : d_unsorted] : (((d2unsorted @ X309)) = X308)),
% 0.20/0.35 inference(fool_elimination,[],[f4])).
% 0.20/0.35 thf(f6,plain,(
% 0.20/0.35 ~ (trsc = (^[Y0 : $i > $i > $o]: (sc @ (rc @ (tc @ Y0)))))),
% 0.20/0.35 inference(fool_elimination,[],[f3])).
% 0.20/0.35 thf(f7,plain,(
% 0.20/0.35 (cr = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((((((((((~ (Y4 = Y3)) & (~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y3 @ Y4)))))) & (~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y4 @ Y3)))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y3 @ Y5))))) | (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y4 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y2 @ Y7 @ Y6)) | (~ (Y2 @ Y6 @ Y5))) | (Y2 @ Y7 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y2 @ Y6 @ Y5)))))))) | (Y2 @ Y3 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y1 @ Y7 @ Y6)) | (~ (Y1 @ Y6 @ Y5))) | (Y1 @ Y7 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y1 @ Y6 @ Y5)))))))) | (Y1 @ Y4 @ Y3)))))))))))) & (confl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((((((((~ (Y5 = Y3)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y3)))))) | ((~ (Y5 = Y4)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y4))))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (sconfl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((((((((~ (Y0 @ Y5 @ Y3)) | ((~ (Y5 = Y4)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y4))))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (lconfl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((((((((~ (Y0 @ Y5 @ Y3)) | (~ (Y0 @ Y5 @ Y4))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (join = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (~ ((((~ (Y1 = Y2)) & (~ (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1)))))) & (~ (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y2 @ Y3))))) | (~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y1 @ Y3)))))))))))))))) & (norm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y4 : $i]: (~ (Y0 @ Y3 @ Y4)))))))))))))))) & (nfof = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) & (!! @ $i @ (^[Y3 : $i]: (~ (Y0 @ Y1 @ Y3))))))))))) & (innf = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2)))))))) & (ind = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ $i @ (^[Y4 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y3 @ Y4))))) | (Y2 @ Y4))))) | (Y2 @ Y3))))) | (Y2 @ Y1)))))))) & (term = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((~ (Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y2 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y2 @ Y4)) | (~ (Y0 @ Y3 @ Y4))))))))))))))))) & (total = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((Y2 = Y1) | (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (so = (^[Y0 : $i > $i > $o]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))))) & (po = (^[Y0 : $i > $i > $o]: (((!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))) | (Y2 = Y1))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))))) & (trsc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2))))))))))) & (trc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2))))))))))) & (tc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))))))) & (trans = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1)))))))))) & (sc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y0 @ Y2 @ Y1) | (Y0 @ Y1 @ Y2)))))))) & (asymm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))))))))) & (antisymm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))) | (Y2 = Y1)))))))) & (symm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (rc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y1 = Y2) | (Y0 @ Y1 @ Y2)))))))) & (irrefl = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1 @ Y1)))))) & (refl = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mono = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y4 @ Y6 @ Y5)) | (Y3 @ Y6 @ Y5))))))) | (~ (Y0 @ Y4 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y2 @ Y1)))))))))))) & (infl = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: ((~ (Y3 @ Y2 @ Y1)) | (Y0 @ Y3 @ Y2 @ Y1)))))))))) & (idem = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: ((Y0 @ Y1) = (Y0 @ (Y0 @ Y1))))))) & (inv = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (Y0 @ Y2 @ Y1))))))) & (subrel = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $i > $o]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))))) & ! [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.20/0.35 inference(rectify,[],[f5])).
% 0.20/0.35 thf(f8,plain,(
% 0.20/0.35 (trsc != (^[Y0 : $i > $i > $o]: (sc @ (rc @ (tc @ Y0)))))),
% 0.20/0.35 inference(flattening,[],[f6])).
% 0.20/0.35 thf(f9,plain,(
% 0.20/0.35 (cr = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((((((((((~ (Y4 = Y3)) & (~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y3 @ Y4)))))) & (~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y4 @ Y3)))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y3 @ Y5))))) | (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y4 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y2 @ Y7 @ Y6)) | (~ (Y2 @ Y6 @ Y5))) | (Y2 @ Y7 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y2 @ Y6 @ Y5)))))))) | (Y2 @ Y3 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y1 @ Y7 @ Y6)) | (~ (Y1 @ Y6 @ Y5))) | (Y1 @ Y7 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y1 @ Y6 @ Y5)))))))) | (Y1 @ Y4 @ Y3)))))))))))) & (confl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((((((((~ (Y5 = Y3)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y3)))))) | ((~ (Y5 = Y4)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y4))))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (sconfl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((((((((~ (Y0 @ Y5 @ Y3)) | ((~ (Y5 = Y4)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y4))))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (lconfl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((((((((~ (Y0 @ Y5 @ Y3)) | (~ (Y0 @ Y5 @ Y4))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (join = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (~ ((((~ (Y1 = Y2)) & (~ (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1)))))) & (~ (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y2 @ Y3))))) | (~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y1 @ Y3)))))))))))))))) & (norm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y4 : $i]: (~ (Y0 @ Y3 @ Y4)))))))))))))))) & (nfof = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) & (!! @ $i @ (^[Y3 : $i]: (~ (Y0 @ Y1 @ Y3))))))))))) & (innf = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2)))))))) & (ind = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ $i @ (^[Y4 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y3 @ Y4))))) | (Y2 @ Y4))))) | (Y2 @ Y3))))) | (Y2 @ Y1)))))))) & (term = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((~ (Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y2 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y2 @ Y4)) | (~ (Y0 @ Y3 @ Y4))))))))))))))))) & (total = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((Y2 = Y1) | (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (so = (^[Y0 : $i > $i > $o]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))))) & (po = (^[Y0 : $i > $i > $o]: (((!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))) | (Y2 = Y1))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))))) & (trsc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2))))))))))) & (trc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2))))))))))) & (tc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))))))) & (trans = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1)))))))))) & (sc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y0 @ Y2 @ Y1) | (Y0 @ Y1 @ Y2)))))))) & (asymm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))))))))) & (antisymm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))) | (Y2 = Y1)))))))) & (symm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (rc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y1 = Y2) | (Y0 @ Y1 @ Y2)))))))) & (irrefl = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1 @ Y1)))))) & (refl = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mono = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y4 @ Y6 @ Y5)) | (Y3 @ Y6 @ Y5))))))) | (~ (Y0 @ Y4 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y2 @ Y1)))))))))))) & (infl = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: ((~ (Y3 @ Y2 @ Y1)) | (Y0 @ Y3 @ Y2 @ Y1)))))))))) & (idem = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: ((Y0 @ Y1) = (Y0 @ (Y0 @ Y1))))))) & (inv = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (Y0 @ Y2 @ Y1))))))) & (subrel = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $i > $o]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))))) & ! [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.20/0.35 inference(ennf_transformation,[],[f7])).
% 0.20/0.35 thf(f10,plain,(
% 0.20/0.35 (cr = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((((((((((~ (Y4 = Y3)) & (~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y3 @ Y4)))))) & (~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y4 @ Y3)))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y3 @ Y5))))) | (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y4 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y2 @ Y7 @ Y6)) | (~ (Y2 @ Y6 @ Y5))) | (Y2 @ Y7 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y2 @ Y6 @ Y5)))))))) | (Y2 @ Y3 @ Y4)) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y1 @ Y7 @ Y6)) | (~ (Y1 @ Y6 @ Y5))) | (Y1 @ Y7 @ Y5)))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y1 @ Y6 @ Y5)))))))) | (Y1 @ Y4 @ Y3)))))))))))) & (confl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((((((((~ (Y5 = Y3)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y3)))))) | ((~ (Y5 = Y4)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y4))))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (sconfl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((((((((~ (Y0 @ Y5 @ Y3)) | ((~ (Y5 = Y4)) & (~ (!! @ ($i > $i > $o) @ (^[Y6 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (((~ (Y6 @ Y9 @ Y8)) | (~ (Y6 @ Y8 @ Y7))) | (Y6 @ Y9 @ Y7))))))))) | (~ (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: ((~ (Y0 @ Y8 @ Y7)) | (Y6 @ Y8 @ Y7)))))))) | (Y6 @ Y5 @ Y4))))))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (lconfl = (^[Y0 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((((((((((~ (Y0 @ Y5 @ Y3)) | (~ (Y0 @ Y5 @ Y4))) | (Y4 = Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y4 @ Y6))))) | (~ (!! @ ($i > $i > $o) @ (^[Y7 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: (!! @ $i @ (^[Y10 : $i]: (((~ (Y7 @ Y10 @ Y9)) | (~ (Y7 @ Y9 @ Y8))) | (Y7 @ Y10 @ Y8))))))))) | (~ (!! @ $i @ (^[Y8 : $i]: (!! @ $i @ (^[Y9 : $i]: ((~ (Y0 @ Y9 @ Y8)) | (Y7 @ Y9 @ Y8)))))))) | (Y7 @ Y3 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y2 @ Y8 @ Y7)) | (~ (Y2 @ Y7 @ Y6))) | (Y2 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y2 @ Y7 @ Y6)))))))) | (Y2 @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y1 @ Y8 @ Y7)) | (~ (Y1 @ Y7 @ Y6))) | (Y1 @ Y8 @ Y6)))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y1 @ Y7 @ Y6)))))))) | (Y1 @ Y3 @ Y4)))))))))))))) & (join = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (~ ((((~ (Y1 = Y2)) & (~ (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1)))))) & (~ (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y2 @ Y3))))) | (~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y1 @ Y3)))))))))))))))) & (norm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y0 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y4 : $i]: (~ (Y0 @ Y3 @ Y4)))))))))))))))) & (nfof = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) & (!! @ $i @ (^[Y3 : $i]: (~ (Y0 @ Y1 @ Y3))))))))))) & (innf = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (~ (Y0 @ Y1 @ Y2)))))))) & (ind = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (!! @ $i @ (^[Y4 : $i]: ((~ (!! @ ($i > $i > $o) @ (^[Y5 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (!! @ $i @ (^[Y8 : $i]: (((~ (Y5 @ Y8 @ Y7)) | (~ (Y5 @ Y7 @ Y6))) | (Y5 @ Y8 @ Y6))))))))) | (~ (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (Y0 @ Y7 @ Y6)) | (Y5 @ Y7 @ Y6)))))))) | (Y5 @ Y3 @ Y4))))) | (Y2 @ Y4))))) | (Y2 @ Y3))))) | (Y2 @ Y1)))))))) & (term = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((~ (Y2 @ Y1)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (Y2 @ Y3)) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (Y2 @ Y4)) | (~ (Y0 @ Y3 @ Y4))))))))))))))))) & (total = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((Y2 = Y1) | (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (so = (^[Y0 : $i > $i > $o]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))))) & (po = (^[Y0 : $i > $i > $o]: (((!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))) | (Y2 = Y1))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))))) & (trsc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2))))))))))) & (trc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2))))))))))) & (tc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))))))) & (trans = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1)))))))))) & (sc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y0 @ Y2 @ Y1) | (Y0 @ Y1 @ Y2)))))))) & (asymm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))))))))) & (antisymm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((~ (Y0 @ Y2 @ Y1)) | (~ (Y0 @ Y1 @ Y2))) | (Y2 = Y1)))))))) & (symm = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (Y0 @ Y2 @ Y1)) | (Y0 @ Y1 @ Y2)))))))) & (rc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y1 = Y2) | (Y0 @ Y1 @ Y2)))))))) & (irrefl = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1 @ Y1)))))) & (refl = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1))))) & (mono = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y4 @ Y6 @ Y5)) | (Y3 @ Y6 @ Y5))))))) | (~ (Y0 @ Y4 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y2 @ Y1)))))))))))) & (infl = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: ((~ (Y3 @ Y2 @ Y1)) | (Y0 @ Y3 @ Y2 @ Y1)))))))))) & (idem = (^[Y0 : ($i > $i > $o) > $i > $i > $o]: (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: ((Y0 @ Y1) = (Y0 @ (Y0 @ Y1))))))) & (inv = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (Y0 @ Y2 @ Y1))))))) & (subrel = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $i > $o]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))))) & ! [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.20/0.35 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X4,sK0 @ X3)],[f9])).
% 0.20/0.35 thf(f11,plain,(
% 0.20/0.35 ( ! [X3 : $i] : ((((d2unsorted @ (sK0 @ X3))) = X3)) )),
% 0.20/0.35 inference(cnf_transformation,[],[f10])).
% 0.20/0.35 thf(f12,plain,(
% 0.20/0.35 ( ! [X2 : d_unsorted] : ((d_unsorted_0 = X2)) )),
% 0.20/0.35 inference(cnf_transformation,[],[f10])).
% 0.20/0.35 thf(f21,plain,(
% 0.20/0.35 (rc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y1 = Y2) | (Y0 @ Y1 @ Y2))))))))),
% 0.20/0.35 inference(cnf_transformation,[],[f10])).
% 0.20/0.35 thf(f25,plain,(
% 0.20/0.35 (sc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((Y0 @ Y2 @ Y1) | (Y0 @ Y1 @ Y2))))))))),
% 0.20/0.35 inference(cnf_transformation,[],[f10])).
% 0.20/0.35 thf(f27,plain,(
% 0.20/0.35 (tc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2))))))))))),
% 0.20/0.35 inference(cnf_transformation,[],[f10])).
% 0.20/0.35 thf(f29,plain,(
% 0.20/0.35 (trsc = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))))))))),
% 0.20/0.35 inference(cnf_transformation,[],[f10])).
% 0.20/0.35 thf(f43,plain,(
% 0.20/0.35 (trsc != (^[Y0 : $i > $i > $o]: (sc @ (rc @ (tc @ Y0)))))),
% 0.20/0.35 inference(cnf_transformation,[],[f8])).
% 0.20/0.35 thf(f46,plain,(
% 0.20/0.35 ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))))))) != (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((Y1 @ Y3 @ Y2) | (Y1 @ Y2 @ Y3))))))) @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((Y2 = Y3) | (Y1 @ Y2 @ Y3))))))) @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: (!! @ ($i > $i > $o) @ (^[Y4 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: (((~ (Y4 @ Y7 @ Y6)) | (~ (Y4 @ Y6 @ Y5))) | (Y4 @ Y7 @ Y5))))))))) | (~ (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y1 @ Y6 @ Y5)) | (Y4 @ Y6 @ Y5)))))))) | (Y4 @ Y2 @ Y3))))))))) @ Y0)))))),
% 0.20/0.35 inference(definition_unfolding,[],[f43,f29,f25,f21,f27])).
% 0.20/0.35 thf(f47,plain,(
% 0.20/0.35 ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))))))) != (^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y2 = Y1) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) | ((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2))))))))))))),
% 0.20/0.35 inference(beta-eta_normalization,[],[f46])).
% 0.20/0.35 thf(f58,plain,(
% 0.20/0.35 ( ! [X3 : $i] : ((((d2unsorted @ d_unsorted_0)) = X3)) )),
% 0.20/0.35 inference(forward_demodulation,[],[f11,f12])).
% 0.20/0.35 thf(f62,plain,(
% 0.20/0.35 ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) )),
% 0.20/0.35 inference(constrained_superposition,[],[f58,f58])).
% 0.20/0.35 thf(f65,plain,(
% 0.20/0.35 ((((^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2)))))))))) @ sK1)) != (((^[Y0 : $i > $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((Y2 = Y1) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y2 @ Y1))))) | ((Y1 = Y2) | (!! @ ($i > $i > $o) @ (^[Y3 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((~ (Y3 @ Y6 @ Y5)) | (~ (Y3 @ Y5 @ Y4))) | (Y3 @ Y6 @ Y4))))))))) | (~ (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y0 @ Y5 @ Y4)) | (Y3 @ Y5 @ Y4)))))))) | (Y3 @ Y1 @ Y2))))))))))) @ sK1)))),
% 0.20/0.35 inference(negative_extensionality,[],[f47])).
% 0.20/0.35 thf(f66,plain,(
% 0.20/0.35 ((^[Y0 : $i]: ((^[Y1 : $i]: (((Y0 = Y1) | (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((~ (Y2 @ Y5 @ Y4)) | (~ (Y2 @ Y4 @ Y3))) | (Y2 @ Y5 @ Y3))))))))) | (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (sK1 @ Y4 @ Y3)) | (Y2 @ Y4 @ Y3)))))))) | (Y2 @ Y1 @ Y0))))) | (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((~ (Y2 @ Y5 @ Y4)) | (~ (Y2 @ Y4 @ Y3))) | (Y2 @ Y5 @ Y3))))))))) | (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (sK1 @ Y4 @ Y3)) | (Y2 @ Y4 @ Y3)))))))) | (Y2 @ Y0 @ Y1)))))))) != (^[Y0 : $i]: ((^[Y1 : $i]: (((Y1 = Y0) | (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((~ (Y2 @ Y5 @ Y4)) | (~ (Y2 @ Y4 @ Y3))) | (Y2 @ Y5 @ Y3))))))))) | (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (sK1 @ Y4 @ Y3)) | (Y2 @ Y4 @ Y3)))))))) | (Y2 @ Y1 @ Y0))))) | ((Y0 = Y1) | (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((~ (Y2 @ Y5 @ Y4)) | (~ (Y2 @ Y4 @ Y3))) | (Y2 @ Y5 @ Y3))))))))) | (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (sK1 @ Y4 @ Y3)) | (Y2 @ Y4 @ Y3)))))))) | (Y2 @ Y0 @ Y1))))))))))),
% 0.20/0.35 inference(beta-eta_normalization,[],[f65])).
% 0.20/0.35 thf(f67,plain,(
% 0.20/0.35 ((((^[Y0 : $i]: ((^[Y1 : $i]: (((Y0 = Y1) | (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((~ (Y2 @ Y5 @ Y4)) | (~ (Y2 @ Y4 @ Y3))) | (Y2 @ Y5 @ Y3))))))))) | (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (sK1 @ Y4 @ Y3)) | (Y2 @ Y4 @ Y3)))))))) | (Y2 @ Y1 @ Y0))))) | (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((~ (Y2 @ Y5 @ Y4)) | (~ (Y2 @ Y4 @ Y3))) | (Y2 @ Y5 @ Y3))))))))) | (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (sK1 @ Y4 @ Y3)) | (Y2 @ Y4 @ Y3)))))))) | (Y2 @ Y0 @ Y1)))))))) @ sK2)) != (((^[Y0 : $i]: ((^[Y1 : $i]: (((Y1 = Y0) | (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((~ (Y2 @ Y5 @ Y4)) | (~ (Y2 @ Y4 @ Y3))) | (Y2 @ Y5 @ Y3))))))))) | (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (sK1 @ Y4 @ Y3)) | (Y2 @ Y4 @ Y3)))))))) | (Y2 @ Y1 @ Y0))))) | ((Y0 = Y1) | (!! @ ($i > $i > $o) @ (^[Y2 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((~ (Y2 @ Y5 @ Y4)) | (~ (Y2 @ Y4 @ Y3))) | (Y2 @ Y5 @ Y3))))))))) | (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (sK1 @ Y4 @ Y3)) | (Y2 @ Y4 @ Y3)))))))) | (Y2 @ Y0 @ Y1))))))))) @ sK2)))),
% 0.20/0.35 inference(negative_extensionality,[],[f66])).
% 0.20/0.35 thf(f68,plain,(
% 0.20/0.35 ((^[Y0 : $i]: (((sK2 = Y0) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ Y0 @ sK2))))) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ sK2 @ Y0)))))) != (^[Y0 : $i]: (((Y0 = sK2) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ Y0 @ sK2))))) | ((sK2 = Y0) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ sK2 @ Y0))))))))),
% 0.20/0.35 inference(beta-eta_normalization,[],[f67])).
% 0.20/0.35 thf(f69,plain,(
% 0.20/0.35 ((((^[Y0 : $i]: (((sK2 = Y0) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ Y0 @ sK2))))) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ sK2 @ Y0)))))) @ sK3)) != (((^[Y0 : $i]: (((Y0 = sK2) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ Y0 @ sK2))))) | ((sK2 = Y0) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ sK2 @ Y0))))))) @ sK3)))),
% 0.20/0.35 inference(negative_extensionality,[],[f68])).
% 0.20/0.35 thf(f71,plain,(
% 0.20/0.35 ($false = (((^[Y0 : $i]: (((sK2 = Y0) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ Y0 @ sK2))))) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ sK2 @ Y0)))))) @ sK3))) | ($false = (((^[Y0 : $i]: (((Y0 = sK2) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ Y0 @ sK2))))) | ((sK2 = Y0) | (!! @ ($i > $i > $o) @ (^[Y1 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((~ (Y1 @ Y4 @ Y3)) | (~ (Y1 @ Y3 @ Y2))) | (Y1 @ Y4 @ Y2))))))))) | (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (sK1 @ Y3 @ Y2)) | (Y1 @ Y3 @ Y2)))))))) | (Y1 @ sK2 @ Y0))))))) @ sK3)))),
% 0.20/0.35 inference(xor_proxy_clausification,[],[f69])).
% 0.20/0.35 thf(f72,plain,(
% 0.20/0.35 ($false = ((((sK2 = sK3) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK3 @ sK2))))) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK2 @ sK3))))))) | ($false = ((((sK3 = sK2) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK3 @ sK2))))) | ((sK2 = sK3) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK2 @ sK3))))))))),
% 0.20/0.35 inference(beta-eta_normalization,[],[f71])).
% 0.20/0.35 thf(f74,plain,(
% 0.20/0.35 ($false = (((sK2 = sK3) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK3 @ sK2))))))) | ($false = ((((sK3 = sK2) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK3 @ sK2))))) | ((sK2 = sK3) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK2 @ sK3))))))))),
% 0.20/0.35 inference(or_proxy_clausification,[],[f72])).
% 0.20/0.35 thf(f76,plain,(
% 0.20/0.35 ($false = ((sK2 = sK3))) | ($false = ((((sK3 = sK2) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK3 @ sK2))))) | ((sK2 = sK3) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK2 @ sK3))))))))),
% 0.20/0.35 inference(or_proxy_clausification,[],[f74])).
% 0.20/0.35 thf(f77,plain,(
% 0.20/0.35 (sK2 != sK3) | ($false = ((((sK3 = sK2) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK3 @ sK2))))) | ((sK2 = sK3) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK2 @ sK3))))))))),
% 0.20/0.35 inference(equality_proxy_clausification,[],[f76])).
% 0.20/0.35 thf(f79,plain,(
% 0.20/0.35 (sK2 != sK3) | ($false = (((sK3 = sK2) | (!! @ ($i > $i > $o) @ (^[Y0 : $i > $i > $o]: (((~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((~ (Y0 @ Y3 @ Y2)) | (~ (Y0 @ Y2 @ Y1))) | (Y0 @ Y3 @ Y1))))))))) | (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (sK1 @ Y2 @ Y1)) | (Y0 @ Y2 @ Y1)))))))) | (Y0 @ sK3 @ sK2)))))))),
% 0.20/0.35 inference(or_proxy_clausification,[],[f77])).
% 0.20/0.35 thf(f81,plain,(
% 0.20/0.35 (sK2 != sK3) | ($false = ((sK3 = sK2)))),
% 0.20/0.35 inference(or_proxy_clausification,[],[f79])).
% 0.20/0.35 thf(f82,plain,(
% 0.20/0.35 (sK2 != sK3) | (sK2 != sK3)),
% 0.20/0.35 inference(equality_proxy_clausification,[],[f81])).
% 0.20/0.35 thf(f83,plain,(
% 0.20/0.35 (sK2 != sK3)),
% 0.20/0.35 inference(duplicate_literal_removal,[],[f82])).
% 0.20/0.35 thf(f4695,plain,(
% 0.20/0.35 $false),
% 0.20/0.35 inference(forward_subsumption_resolution,[],[f83,f62])).
% 0.20/0.35 % SZS output end Proof for theBenchmark
% 0.20/0.35 % (797600)------------------------------
% 0.20/0.35 % (797600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (797600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (797600)CaDiCaL version: 2.1.3
% 0.20/0.35 % (797600)Termination reason: Refutation
% 0.20/0.35 % (797600)Time elapsed: 0.091 s
% 0.20/0.35 % (797600)Peak memory usage: 14 MB
% 0.20/0.35 % (797600)Instructions burned: 227 (million)
% 0.20/0.35 % (797593)Success in time 0.127 s
% 0.20/0.35 % Vampire exiting
%------------------------------------------------------------------------------