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

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

% Computer : n007.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:50:28 AM UTC 2026

% Result   : Theorem 1.65s 0.52s
% Output   : Refutation 1.65s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SYO856^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20  % Computer : n007.cluster.edu
% 0.08/0.20  % Model    : x86_64 x86_64
% 0.08/0.20  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20  % Memory   : 8046.5625MB
% 0.08/0.20  % OS       : Linux 6.8.0-71-generic
% 0.08/0.20  % CPULimit : 300
% 0.08/0.20  % WCLimit  : 300
% 0.08/0.20  % DateTime : Tue Sep 29 17:16:56 UTC 2026
% 0.08/0.20  % CPUTime  : 
% 0.08/0.20  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23  Running first-order model finding
% 0.08/0.23  Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.65/0.52  % (3673132)Will run a generic schedule for satisfiability detection.
% 1.65/0.52  % (3673138)% WARNING: option uhcvi not known.
% 1.65/0.52  % (3673142)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4210946921:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.65/0.52  % (3673140)dis+10_1_sil=32000:sp=arity:random_seed=801304730:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.65/0.52  % (3673139)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4181865287:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.65/0.52  % (3673137)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=644380692_2999 on theBenchmark for (2999ds/0Mi)
% 1.65/0.52  % (3673141)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1231653727:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.65/0.52  % (3673138)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=716455602:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.65/0.52  % (3673143)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1111404423:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.65/0.52  % (3673142)Instruction limit reached! 
% 1.65/0.52  % (3673142)------------------------------
% 1.65/0.52  % (3673142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.52  % (3673142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.52  % (3673142)CaDiCaL version: 2.1.3
% 1.65/0.52  % (3673142)Termination reason: Instruction limit
% 1.65/0.52  % (3673142)Termination phase: Property scanning
% 1.65/0.52  % (3673142)Time elapsed: 0.028 s
% 1.65/0.52  % (3673142)Peak memory usage: 11 MB
% 1.65/0.52  % (3673142)Instructions burned: 133 (million)
% 1.65/0.52  % (3673141)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.65/0.52  % (3673138)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.65/0.52  % (3673151)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3782858769:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.65/0.52  % (3673140)Instruction limit reached! 
% 1.65/0.52  % (3673140)------------------------------
% 1.65/0.52  % (3673140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.52  % (3673140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.52  % (3673140)CaDiCaL version: 2.1.3
% 1.65/0.52  % (3673140)Termination reason: Instruction limit
% 1.65/0.52  % (3673140)Termination phase: Property scanning
% 1.65/0.52  % (3673140)Time elapsed: 0.062 s
% 1.65/0.52  % (3673140)Peak memory usage: 11 MB
% 1.65/0.52  % (3673140)Instructions burned: 105 (million)
% 1.65/0.52  % (3673141)Instruction limit reached! 
% 1.65/0.52  % (3673141)------------------------------
% 1.65/0.52  % (3673141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.52  % (3673141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.52  % (3673141)CaDiCaL version: 2.1.3
% 1.65/0.52  % (3673141)Termination reason: Instruction limit
% 1.65/0.52  % (3673141)Termination phase: Property scanning
% 1.65/0.52  % (3673141)Time elapsed: 0.066 s
% 1.65/0.52  % (3673141)Peak memory usage: 11 MB
% 1.65/0.52  % (3673141)Instructions burned: 117 (million)
% 1.65/0.52  % (3673153)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3256501467:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.65/0.52  % (3673154)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=1840639755:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.65/0.52  % Exception at run slice level
% 1.65/0.52  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.65/0.52  % (3673157)ott-21_1_sil=16000:fs=off:random_seed=1793331696:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.65/0.52  % (3673154)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.65/0.52  % (3673138)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.65/0.52  % Exception at run slice level
% 1.65/0.52  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.65/0.52  % (3673143)Instruction limit reached! 
% 1.65/0.52  % (3673143)------------------------------
% 1.65/0.52  % (3673143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.52  % (3673143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.52  % (3673143)CaDiCaL version: 2.1.3
% 1.65/0.52  % (3673143)Termination reason: Instruction limit
% 1.65/0.52  % (3673143)Termination phase: Property scanning
% 1.65/0.52  % (3673143)Time elapsed: 0.116 s
% 1.65/0.52  % (3673143)Peak memory usage: 11 MB
% 1.65/0.52  % (3673143)Instructions burned: 160 (million)
% 1.65/0.52  % (3673159)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1281575392:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.65/0.52  % (3673157)Instruction limit reached! 
% 1.65/0.52  % (3673157)------------------------------
% 1.65/0.52  % (3673157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.52  % (3673157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.52  % (3673157)CaDiCaL version: 2.1.3
% 1.65/0.52  % (3673157)Termination reason: Instruction limit
% 1.65/0.52  % (3673157)Termination phase: Property scanning
% 1.65/0.52  % (3673157)Time elapsed: 0.038 s
% 1.65/0.52  % (3673157)Peak memory usage: 11 MB
% 1.65/0.52  % (3673157)Instructions burned: 182 (million)
% 1.65/0.52  % (3673153)Instruction limit reached! 
% 1.65/0.52  % (3673153)------------------------------
% 1.65/0.52  % (3673153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.52  % (3673153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.52  % (3673153)CaDiCaL version: 2.1.3
% 1.65/0.52  % (3673153)Termination reason: Instruction limit
% 1.65/0.52  % (3673153)Termination phase: Property scanning
% 1.65/0.52  % (3673153)Time elapsed: 0.054 s
% 1.65/0.52  % (3673153)Peak memory usage: 11 MB
% 1.65/0.52  % (3673153)Instructions burned: 133 (million)
% 1.65/0.52  % (3673161)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1184005661:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.65/0.52  % (3673162)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=785062592:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.65/0.52  % (3673163)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=270728985:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.65/0.52  % (3673154)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.65/0.52  % (3673162) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3673132-3673162"...
% 1.65/0.52  % Exception at run slice level
% 1.65/0.52  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.65/0.52  % (3673162)...printing done.
% 1.65/0.52  % (3673162)Refutation found. Thanks to Tanya!
% 1.65/0.52  % SZS status Theorem for theBenchmark
% 1.65/0.52  % SZS output start Proof for theBenchmark
% 1.65/0.52  thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.65/0.52  thf(func_def_0, type, c_Eps_i: (($i > $o) > $i)).
% 1.65/0.52  thf(func_def_1, type, c_False: $o).
% 1.65/0.52  thf(func_def_2, type, c_True: $o).
% 1.65/0.52  thf(func_def_3, type, c_not: ($o > $o)).
% 1.65/0.52  thf(func_def_4, type, c_and: ($o > $o > $o)).
% 1.65/0.52  thf(func_def_5, type, c_or: ($o > $o > $o)).
% 1.65/0.52  thf(func_def_6, type, c_iff: ($o > $o > $o)).
% 1.65/0.52  thf(func_def_7, type, c_In: ($i > $i > $o)).
% 1.65/0.52  thf(func_def_8, type, c_Subq: ($i > $i > $o)).
% 1.65/0.52  thf(func_def_10, type, c_Union: ($i > $i)).
% 1.65/0.52  thf(func_def_11, type, c_Power: ($i > $i)).
% 1.65/0.52  thf(func_def_12, type, c_Repl: ($i > ($i > $i) > $i)).
% 1.65/0.52  thf(func_def_13, type, c_TransSet: ($i > $o)).
% 1.65/0.52  thf(func_def_14, type, c_atleast2: ($i > $o)).
% 1.65/0.52  thf(func_def_15, type, c_atleast3: ($i > $o)).
% 1.65/0.52  thf(func_def_16, type, c_atleast4: ($i > $o)).
% 1.65/0.52  thf(func_def_17, type, c_atleast5: ($i > $o)).
% 1.65/0.52  thf(func_def_18, type, c_atleast6: ($i > $o)).
% 1.65/0.52  thf(func_def_19, type, c_exactly2: ($i > $o)).
% 1.65/0.52  thf(func_def_20, type, c_exactly3: ($i > $o)).
% 1.65/0.52  thf(func_def_21, type, c_exactly4: ($i > $o)).
% 1.65/0.52  thf(func_def_22, type, c_exactly5: ($i > $o)).
% 1.65/0.52  thf(func_def_23, type, c_exu_i: (($i > $o) > $o)).
% 1.65/0.52  thf(func_def_24, type, c_reflexive_i: (($i > $i > $o) > $o)).
% 1.65/0.52  thf(func_def_25, type, c_irreflexive_i: (($i > $i > $o) > $o)).
% 1.65/0.52  thf(func_def_26, type, c_symmetric_i: (($i > $i > $o) > $o)).
% 1.65/0.52  thf(func_def_27, type, c_antisymmetric_i: (($i > $i > $o) > $o)).
% 1.65/0.52  thf(func_def_28, type, c_transitive_i: (($i > $i > $o) > $o)).
% 1.65/0.52  thf(func_def_29, type, c_eqreln_i: (($i > $i > $o) > $o)).
% 1.65/0.52  thf(func_def_30, type, c_per_i: (($i > $i > $o) > $o)).
% 1.65/0.52  thf(func_def_31, type, c_linear_i: (($i > $i > $o) > $o)).
% 1.65/0.53  thf(func_def_32, type, c_trichotomous_or_i: (($i > $i > $o) > $o)).
% 1.65/0.53  thf(func_def_33, type, c_partialorder_i: (($i > $i > $o) > $o)).
% 1.65/0.53  thf(func_def_34, type, c_totalorder_i: (($i > $i > $o) > $o)).
% 1.65/0.53  thf(func_def_35, type, c_strictpartialorder_i: (($i > $i > $o) > $o)).
% 1.65/0.53  thf(func_def_36, type, c_stricttotalorder_i: (($i > $i > $o) > $o)).
% 1.65/0.53  thf(func_def_37, type, c_If_i: ($o > $i > $i > $i)).
% 1.65/0.53  thf(func_def_38, type, c_exactly1of2: ($o > $o > $o)).
% 1.65/0.53  thf(func_def_39, type, c_exactly1of3: ($o > $o > $o > $o)).
% 1.65/0.53  thf(func_def_40, type, c_nIn: ($i > $i > $o)).
% 1.65/0.53  thf(func_def_41, type, c_nSubq: ($i > $i > $o)).
% 1.65/0.53  thf(func_def_42, type, c_UPair: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_43, type, c_Sing: ($i > $i)).
% 1.65/0.53  thf(func_def_44, type, c_binunion: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_45, type, c_SetAdjoin: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_46, type, c_famunion: ($i > ($i > $i) > $i)).
% 1.65/0.53  thf(func_def_47, type, c_Sep: ($i > ($i > $o) > $i)).
% 1.65/0.53  thf(func_def_48, type, c_ReplSep: ($i > ($i > $o) > ($i > $i) > $i)).
% 1.65/0.53  thf(func_def_49, type, c_binintersect: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_50, type, c_setminus: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_51, type, c_inj: ($i > $i > ($i > $i) > $o)).
% 1.65/0.53  thf(func_def_52, type, c_bij: ($i > $i > ($i > $i) > $o)).
% 1.65/0.53  thf(func_def_53, type, c_atleastp: ($i > $i > $o)).
% 1.65/0.53  thf(func_def_54, type, c_equip: ($i > $i > $o)).
% 1.65/0.53  thf(func_def_55, type, c_In_rec_poly_G_i: (($i > ($i > $i) > $i) > $i > $i > $o)).
% 1.65/0.53  thf(func_def_56, type, c_In_rec_poly_i: (($i > ($i > $i) > $i) > $i > $i)).
% 1.65/0.53  thf(func_def_57, type, c_ordsucc: ($i > $i)).
% 1.65/0.53  thf(func_def_58, type, c_nat_p: ($i > $o)).
% 1.65/0.53  thf(func_def_59, type, c_nat_primrec: ($i > ($i > $i > $i) > $i > $i)).
% 1.65/0.53  thf(func_def_60, type, c_add_nat: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_61, type, c_mul_nat: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_62, type, c_ordinal: ($i > $o)).
% 1.65/0.53  thf(func_def_63, type, c_V_: ($i > $i)).
% 1.65/0.53  thf(func_def_64, type, c_Inj1: ($i > $i)).
% 1.65/0.53  thf(func_def_65, type, c_Inj0: ($i > $i)).
% 1.65/0.53  thf(func_def_66, type, c_Unj: ($i > $i)).
% 1.65/0.53  thf(func_def_67, type, c_combine_funcs: ($i > $i > ($i > $i) > ($i > $i) > $i > $i)).
% 1.65/0.53  thf(func_def_68, type, c_setsum: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_69, type, c_proj0: ($i > $i)).
% 1.65/0.53  thf(func_def_70, type, c_proj1: ($i > $i)).
% 1.65/0.53  thf(func_def_71, type, c_binrep: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_72, type, c_lam: ($i > ($i > $i) > $i)).
% 1.65/0.53  thf(func_def_73, type, c_setprod: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_74, type, c_ap: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_75, type, c_setsum_p: ($i > $o)).
% 1.65/0.53  thf(func_def_76, type, c_tuple_p: ($i > $i > $o)).
% 1.65/0.53  thf(func_def_77, type, c_Pi: ($i > ($i > $i) > $i)).
% 1.65/0.53  thf(func_def_78, type, c_setexp: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_79, type, c_Sep2: ($i > ($i > $i) > ($i > $i > $o) > $i)).
% 1.65/0.53  thf(func_def_80, type, c_set_of_pairs: ($i > $o)).
% 1.65/0.53  thf(func_def_81, type, c_lam2: ($i > ($i > $i) > ($i > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_82, type, c_PNoEq_: ($i > ($i > $o) > ($i > $o) > $o)).
% 1.65/0.53  thf(func_def_83, type, c_PNoLt_: ($i > ($i > $o) > ($i > $o) > $o)).
% 1.65/0.53  thf(func_def_84, type, c_PNoLt: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 1.65/0.53  thf(func_def_85, type, c_PNoLe: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 1.65/0.53  thf(func_def_86, type, c_PNo_downc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 1.65/0.53  thf(func_def_87, type, c_PNo_upc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 1.65/0.53  thf(func_def_88, type, c_SNoElts_: ($i > $i)).
% 1.65/0.53  thf(func_def_89, type, c_SNo_: ($i > $i > $o)).
% 1.65/0.53  thf(func_def_90, type, c_PSNo: ($i > ($i > $o) > $i)).
% 1.65/0.53  thf(func_def_91, type, c_SNo: ($i > $o)).
% 1.65/0.53  thf(func_def_92, type, c_SNoLev: ($i > $i)).
% 1.65/0.53  thf(func_def_93, type, c_SNoEq_: ($i > $i > $i > $o)).
% 1.65/0.53  thf(func_def_94, type, c_SNoLt: ($i > $i > $o)).
% 1.65/0.53  thf(func_def_95, type, c_SNoLe: ($i > $i > $o)).
% 1.65/0.53  thf(func_def_96, type, c_binop_on: ($i > ($i > $i > $i) > $o)).
% 1.65/0.53  thf(func_def_97, type, c_Loop: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > $o)).
% 1.65/0.53  thf(func_def_98, type, c_Loop_with_defs: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 1.65/0.53  thf(func_def_99, type, c_Loop_with_defs_cex1: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 1.65/0.53  thf(func_def_100, type, c_Loop_with_defs_cex2: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 1.65/0.53  thf(func_def_101, type, c_combinator: ($i > $o)).
% 1.65/0.53  thf(func_def_102, type, c_combinator_equiv: ($i > $i > $o)).
% 1.65/0.53  thf(func_def_103, type, c_equip_mod: ($i > $i > $i > $o)).
% 1.65/0.53  thf(func_def_107, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.65/0.53  thf(func_def_108, type, db0: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_109, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.65/0.53  thf(func_def_110, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.65/0.53  thf(func_def_111, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.65/0.53  thf(func_def_112, type, vIMP: ($o > $o > $o)).
% 1.65/0.53  thf(func_def_113, type, db2: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_114, type, db1: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_115, type, db3: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_116, type, db4: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_117, type, db5: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_118, type, db6: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_119, type, db13: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_120, type, db12: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_121, type, db11: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_122, type, db10: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_123, type, db9: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_124, type, db14: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_125, type, db15: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_126, type, db16: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_127, type, db8: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_128, type, db7: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_129, type, db17: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_130, type, db18: !>[X0: $tType]:(X0)).
% 1.65/0.53  thf(func_def_131, type, sP0: (($i > $o) > $o)).
% 1.65/0.53  thf(func_def_132, type, sP1: (($i > $o) > $o)).
% 1.65/0.53  thf(func_def_133, type, sK2: (($i > $o) > $i)).
% 1.65/0.53  thf(func_def_134, type, sK3: (($i > $o) > $i > $i)).
% 1.65/0.53  thf(func_def_135, type, sK4: (($i > $o) > $i)).
% 1.65/0.53  thf(func_def_136, type, sK5: (($i > $o) > $i)).
% 1.65/0.53  thf(func_def_137, type, sK6: (($i > $o) > $i)).
% 1.65/0.53  thf(func_def_138, type, sK7: (($i > $o) > $i)).
% 1.65/0.53  thf(func_def_139, type, sK8: (($i > $o) > $i)).
% 1.65/0.53  thf(func_def_140, type, sK9: ((($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i) > ($i > $i > ($i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_141, type, sK10: (($i > ((($i > $i) > $i > $i) > $i > $i > $i) > $i) > $i > $i)).
% 1.65/0.53  thf(func_def_142, type, sK11: (($i > $i > $i) > ($i > $i) > $i > $i > $i > $i)).
% 1.65/0.53  thf(func_def_143, type, sK12: ((((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i)).
% 1.65/0.53  thf(func_def_164, type, sF33: ($i > $i)).
% 1.65/0.53  thf(func_def_165, type, sF34: ($i > $i)).
% 1.65/0.53  thf(func_def_166, type, sF35: (((($i > $i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_172, type, sF41: ($i > $i)).
% 1.65/0.53  thf(func_def_174, type, sF43: ($i > $i)).
% 1.65/0.53  thf(func_def_175, type, sF44: ($i > $i)).
% 1.65/0.53  thf(func_def_176, type, sF45: (((($i > $i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_177, type, sF46: (($i > ($i > $i > $i) > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_178, type, sF47: (($i > ($i > $i > $i) > $i > $i) > ((($i > $i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_179, type, sF48: (((($i > $i > $i) > $i > $i) > $i) > ($i > ($i > $i > $i) > $i > $i) > $i > $i)).
% 1.65/0.53  thf(func_def_181, type, sF50: ($i > ($i > ($i > $i > $i) > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_182, type, sF51: ($i > $i > ($i > ($i > $i > $i) > $i > $i) > ((($i > $i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_183, type, sF52: (($i > ($i > $i > $i) > $i > $i) > $i > $i > ((($i > $i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_188, type, sF57: (((($i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_190, type, sF59: ($i > $i)).
% 1.65/0.53  thf(func_def_191, type, sF60: ($i > ((($i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_192, type, sF61: (((($i > $i) > $i > $i) > $i) > $i > $i)).
% 1.65/0.53  thf(func_def_193, type, sF62: ($i > $i)).
% 1.65/0.53  thf(func_def_194, type, sF63: ($i > $i)).
% 1.65/0.53  thf(func_def_199, type, sF68: (((($i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_200, type, sF69: (((($i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_203, type, sF72: (((($i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_204, type, sF73: (((($i > $i) > $i > $i) > $i) > $i > $i)).
% 1.65/0.53  thf(func_def_205, type, sF74: (($i > $i) > $i)).
% 1.65/0.53  thf(func_def_206, type, sF75: (($i > $i) > $i)).
% 1.65/0.53  thf(func_def_208, type, sF77: (((($i > $i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_209, type, sF78: (((($i > $i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_210, type, sF79: ((((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_211, type, sF80: ((((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i) > ($i > $i) > ((($i > $i > $i) > $i > $i) > $i) > $i)).
% 1.65/0.53  thf(func_def_212, type, sF81: (($i > $i) > $i)).
% 1.65/0.53  thf(func_def_213, type, sF82: (($i > $i) > $i)).
% 1.65/0.53  thf(func_def_214, type, sF83: (((($i > $i > $i) > $i > $i) > $i) > ($i > $i) > (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_215, type, sF84: ((((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_216, type, sF85: ((((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_217, type, sF86: ((((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_218, type, sF87: (($i > $i) > $i)).
% 1.65/0.53  thf(func_def_219, type, sF88: ((((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i) > ((($i > $i > $i) > $i > $i) > $i) > ($i > $i) > $i)).
% 1.65/0.53  thf(func_def_226, type, sF95: (($i > $i) > $i)).
% 1.65/0.53  thf(func_def_227, type, sF96: ($i > ($i > $i) > $i)).
% 1.65/0.53  thf(func_def_228, type, sF97: (($i > $i) > $i)).
% 1.65/0.53  thf(func_def_230, type, sF99: ($i > $i)).
% 1.65/0.53  thf(func_def_232, type, sF101: ($i > $i)).
% 1.65/0.53  thf(func_def_233, type, sF102: ($i > ($i > $i) > $i)).
% 1.65/0.53  thf(func_def_236, type, sF105: (((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_237, type, sF106: ((((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_238, type, sF107: ((((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i) > ((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_239, type, sF108: (((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i) > (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_240, type, sF109: ((((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i) > ((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_241, type, sF110: (((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i) > (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i) > $i)).
% 1.65/0.53  thf(func_def_242, type, vNOT: ($o > $o)).
% 1.65/0.53  thf(func_def_243, type, sK111: $o).
% 1.65/0.53  thf(func_def_244, type, sK112: $o).
% 1.65/0.53  thf(func_def_245, type, sK113: (($i > $i) > $i > $i > $i)).
% 1.65/0.53  thf(func_def_246, type, sK114: ($i > ($i > $i) > $i > $i > $o)).
% 1.65/0.53  thf(func_def_247, type, sK115: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_248, type, sK116: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_249, type, sK117: ($i > $i > $i > $o)).
% 1.65/0.53  thf(func_def_250, type, sK118: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_251, type, sK119: ($i > $i > $i)).
% 1.65/0.53  thf(func_def_252, type, sK120: ($o > $o > $o)).
% 1.65/0.53  thf(func_def_253, type, sK121: ($o > $o > $o)).
% 1.65/0.53  thf(f5,axiom,(
% 1.65/0.53    (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 1.65/0.53    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5)).
% 1.65/0.53  thf(f6,axiom,(
% 1.65/0.53    ! [X0 : $i,X1 : $i] : (c_iff @ (c_In @ X1 @ (c_Union @ X0)) @ ? [X2 : $i] : (c_and @ (c_In @ X1 @ X2) @ (c_In @ X2 @ X0)))),
% 1.65/0.53    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6)).
% 1.65/0.53  thf(f7,axiom,(
% 1.65/0.53    ! [X0 : $i,X1 : $i] : (c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))),
% 1.65/0.53    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7)).
% 1.65/0.53  thf(f13,axiom,(
% 1.65/0.53    (c_not = (^[X0 : $o] : (X0 => c_False)))),
% 1.65/0.53    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13)).
% 1.65/0.53  thf(f14,axiom,(
% 1.65/0.53    (c_and = (^[X0 : $o, X1 : $o] : (! [X2 : $o] : ((X0 => (X1 => X2)) => X2))))),
% 1.65/0.53    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14)).
% 1.65/0.53  thf(f16,axiom,(
% 1.65/0.53    (c_iff = (^[X0 : $o, X1 : $o] : ((c_and @ X0 => X1 @ X1 => X0))))),
% 1.65/0.53    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16)).
% 1.65/0.53  thf(f17,axiom,(
% 1.65/0.53    (c_Subq = (^[X0 : $i, X1 : $i] : (! [X2 : $i] : ((c_In @ X2 @ X0) => (c_In @ X2 @ X1)))))),
% 1.65/0.53    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17)).
% 1.65/0.53  thf(f109,conjecture,(
% 1.65/0.53    ! [X0 : ((($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i) > ($i > $i > ($i > $i) > $i) > $i),X1 : (($i > ((($i > $i) > $i > $i) > $i > $i > $i) > $i) > $i > $i),X2 : (($i > $i > $i) > ($i > $i) > $i > $i > $i > $i),X3 : ((((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i)] : (! [X4 : (($i > $i > $i) > $i),X5 : $i,X6 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i),X7 : ((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i)] : (((X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((c_setsum @ (X0 @ (^[X9 : ($i > $i), X10 : (($i > $i > $i) > $i > $i), X11 : $i, X12 : ($i > $i)] : ((X1 @ (^[X13 : $i, X14 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_setsum @ c_Empty @ c_Empty))) @ (c_Inj1 @ c_Empty)))) @ (^[X9 : $i, X10 : $i, X11 : ($i > $i)] : (c_Empty))) @ (X1 @ (^[X9 : $i, X10 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ (X2 @ (^[X9 : $i, X10 : $i] : ((X7 @ (^[X11 : ($i > $i > $i)] : (c_Empty)) @ (^[X11 : $i] : (c_Empty)) @ c_Empty @ c_Empty))) @ (^[X9 : $i] : (c_Empty)) @ (X6 @ (^[X9 : (($i > $i) > $i), X10 : ($i > $i), X11 : $i] : (c_Empty)) @ c_Empty) @ (X1 @ (^[X9 : $i, X10 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty)))))) @ (^[X8 : $i] : (X8)))) = ((c_Inj1 @ c_Empty))) => (! [X4 : $i,X5 : $i,X6 : ($i > $i),X7 : $i] : (((X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X8 : $i] : ((X6 @ X8))))) = ((X6 @ (c_setsum @ (X2 @ (^[X8 : $i, X9 : $i] : ((X1 @ (^[X10 : $i, X11 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ (c_setsum @ c_Empty @ c_Empty)))) @ (^[X8 : $i] : (X8)) @ X5 @ c_Empty @ c_Empty) @ (X1 @ (^[X8 : $i, X9 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((X9 @ (^[X10 : ($i > $i), X11 : $i] : (c_Empty)) @ X8 @ (X2 @ (^[X10 : $i, X11 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))) @ c_Empty))))) => (! [X4 : $i,X5 : (($i > ($i > $i) > $i) > $i),X6 : $i,X7 : ($i > $i)] : (((X2 @ (^[X8 : $i, X9 : $i] : (c_Empty)) @ (^[X8 : $i] : ((X2 @ (^[X9 : $i, X10 : $i] : ((X2 @ (^[X11 : $i, X12 : $i] : (c_Empty)) @ (^[X11 : $i] : (c_Empty)) @ (X0 @ (^[X11 : ($i > $i), X12 : (($i > $i > $i) > $i > $i), X13 : $i, X14 : ($i > $i)] : ((c_setsum @ c_Empty @ c_Empty))) @ (^[X11 : $i, X12 : $i, X13 : ($i > $i)] : ((X0 @ (^[X14 : ($i > $i), X15 : (($i > $i > $i) > $i > $i), X16 : $i, X17 : ($i > $i)] : (c_Empty)) @ (^[X14 : $i, X15 : $i, X16 : ($i > $i)] : (c_Empty)))))) @ (X7 @ X10) @ X10))) @ (^[X9 : $i] : (X8)) @ (X1 @ (^[X9 : $i, X10 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ (X2 @ (^[X9 : $i, X10 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X9 : $i] : ((X1 @ (^[X10 : $i, X11 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))) @ (X3 @ (^[X9 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X9 : $i] : (c_Empty))) @ (c_Inj1 @ c_Empty) @ (X0 @ (^[X9 : ($i > $i), X10 : (($i > $i > $i) > $i > $i), X11 : $i, X12 : ($i > $i)] : (c_Empty)) @ (^[X9 : $i, X10 : $i, X11 : ($i > $i)] : (c_Empty))))) @ (X7 @ c_Empty) @ c_Empty))) @ X4 @ (X0 @ (^[X8 : ($i > $i), X9 : (($i > $i > $i) > $i > $i), X10 : $i, X11 : ($i > $i)] : ((c_Inj0 @ c_Empty))) @ (^[X8 : $i, X9 : $i, X10 : ($i > $i)] : ((c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (X1 @ (^[X11 : $i, X12 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty)))))) @ (c_setsum @ c_Empty @ (X7 @ c_Empty)))) = X4) => (! [X4 : ($i > $i > $i),X5 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i),X6 : ((($i > $i > $i) > $i > $i) > $i),X7 : ($i > $i)] : (((X2 @ (^[X8 : $i, X9 : $i] : ((X2 @ (^[X10 : $i, X11 : $i] : (c_Empty)) @ (^[X10 : $i] : (X8)) @ (X7 @ c_Empty) @ (X6 @ (^[X10 : ($i > $i > $i), X11 : $i] : ((c_setsum @ c_Empty @ (X0 @ (^[X12 : ($i > $i), X13 : (($i > $i > $i) > $i > $i), X14 : $i, X15 : ($i > $i)] : (c_Empty)) @ (^[X12 : $i, X13 : $i, X14 : ($i > $i)] : (c_Empty))))))) @ c_Empty))) @ (^[X8 : $i] : (c_Empty)) @ (X5 @ (^[X8 : (($i > $i) > $i), X9 : ($i > $i), X10 : $i] : (c_Empty)) @ c_Empty @ (X2 @ (^[X8 : $i, X9 : $i] : ((X3 @ (^[X10 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (X9)) @ (^[X10 : $i] : ((c_Inj0 @ c_Empty)))))) @ (^[X8 : $i] : ((X3 @ (^[X9 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((X6 @ (^[X10 : ($i > $i > $i), X11 : $i] : (c_Empty))))) @ (^[X9 : $i] : ((c_Inj0 @ c_Empty)))))) @ (X7 @ c_Empty) @ c_Empty @ (X5 @ (^[X8 : (($i > $i) > $i), X9 : ($i > $i), X10 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X7 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X5 @ (^[X8 : (($i > $i) > $i), X9 : ($i > $i), X10 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X7 @ (c_Inj1 @ c_Empty)))) = ((X7 @ (c_Inj0 @ c_Empty)))) => (! [X4 : $i,X5 : ($i > $i > ($i > $i) > $i > $i),X6 : ((($i > $i) > $i > $i) > $i),X7 : $i] : (((X1 @ (^[X8 : $i, X9 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (X2 @ (^[X10 : $i, X11 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X3 @ (^[X10 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X10 : $i] : (c_Empty))))) @ (c_setsum @ (c_setsum @ (X0 @ (^[X10 : ($i > $i), X11 : (($i > $i > $i) > $i > $i), X12 : $i, X13 : ($i > $i)] : (c_Empty)) @ (^[X10 : $i, X11 : $i, X12 : ($i > $i)] : (c_Empty))) @ c_Empty) @ (X9 @ (^[X10 : ($i > $i), X11 : $i] : ((c_Inj0 @ c_Empty))) @ (X9 @ (^[X10 : ($i > $i), X11 : $i] : (c_Empty)) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty)))))) @ (X2 @ (^[X8 : $i, X9 : $i] : (c_Empty)) @ (^[X8 : $i] : ((X6 @ (^[X9 : ($i > $i), X10 : $i] : ((c_setsum @ (c_Inj1 @ c_Empty) @ (X2 @ (^[X11 : $i, X12 : $i] : (c_Empty)) @ (^[X11 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))) @ (c_setsum @ X4 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))) = ((X2 @ (^[X8 : $i, X9 : $i] : ((c_setsum @ X7 @ (c_Inj1 @ X7)))) @ (^[X8 : $i] : ((X0 @ (^[X9 : ($i > $i), X10 : (($i > $i > $i) > $i > $i), X11 : $i, X12 : ($i > $i)] : ((c_Inj1 @ c_Empty))) @ (^[X9 : $i, X10 : $i, X11 : ($i > $i)] : (c_Empty))))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (X0 @ (^[X8 : ($i > $i), X9 : (($i > $i > $i) > $i > $i), X10 : $i, X11 : ($i > $i)] : ((c_Inj1 @ c_Empty))) @ (^[X8 : $i, X9 : $i, X10 : ($i > $i)] : ((c_Inj0 @ (X2 @ (^[X11 : $i, X12 : $i] : (c_Empty)) @ (^[X11 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_Inj1 @ (X6 @ (^[X8 : ($i > $i), X9 : $i] : ((c_Inj1 @ c_Empty))))) @ (c_setsum @ (X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((X8 @ (^[X9 : ($i > $i > $i), X10 : ($i > $i)] : (c_Empty)) @ c_Empty @ c_Empty))) @ (^[X8 : $i] : ((c_Inj1 @ c_Empty)))) @ (c_setsum @ c_Empty @ c_Empty)))))) => (! [X4 : ($i > ($i > $i > $i) > $i > $i),X5 : $i,X6 : $i,X7 : ((($i > $i > $i) > $i > $i) > $i)] : (((X1 @ (^[X8 : $i, X9 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_setsum @ (X1 @ (^[X10 : $i, X11 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (X8)) @ (c_setsum @ (X2 @ (^[X10 : $i, X11 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X1 @ (^[X10 : $i, X11 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))) @ c_Empty))) @ (X2 @ (^[X8 : $i, X9 : $i] : (X9)) @ (^[X8 : $i] : ((X0 @ (^[X9 : ($i > $i), X10 : (($i > $i > $i) > $i > $i), X11 : $i, X12 : ($i > $i)] : (X11)) @ (^[X9 : $i, X10 : $i, X11 : ($i > $i)] : ((X3 @ (^[X12 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((X12 @ (^[X13 : ($i > $i > $i), X14 : ($i > $i)] : (c_Empty)) @ c_Empty @ c_Empty))) @ (^[X12 : $i] : (c_Empty)))))))) @ X5 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (X2 @ (^[X8 : $i, X9 : $i] : (c_Empty)) @ (^[X8 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) = ((X2 @ (^[X8 : $i, X9 : $i] : ((c_Inj0 @ c_Empty))) @ (^[X8 : $i] : ((X1 @ (^[X9 : $i, X10 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((X7 @ (^[X11 : ($i > $i > $i), X12 : $i] : ((X10 @ (^[X13 : ($i > $i), X14 : $i] : ((X2 @ (^[X15 : $i, X16 : $i] : (c_Empty)) @ (^[X15 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ c_Empty @ (X1 @ (^[X13 : $i, X14 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))))))) @ c_Empty))) @ (c_Inj0 @ (X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (^[X8 : $i] : ((X3 @ (^[X9 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((c_setsum @ c_Empty @ c_Empty))) @ (^[X9 : $i] : ((X2 @ (^[X10 : $i, X11 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))))) @ (c_setsum @ (c_setsum @ X5 @ (X1 @ (^[X8 : $i, X9 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_Inj0 @ c_Empty))) @ (X2 @ (^[X8 : $i, X9 : $i] : (c_Empty)) @ (^[X8 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (X1 @ (^[X8 : $i, X9 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_Inj0 @ (X0 @ (^[X10 : ($i > $i), X11 : (($i > $i > $i) > $i > $i), X12 : $i, X13 : ($i > $i)] : (c_Empty)) @ (^[X10 : $i, X11 : $i, X12 : ($i > $i)] : (c_Empty)))))) @ X5)) @ (c_setsum @ (c_setsum @ X6 @ (X2 @ (^[X8 : $i, X9 : $i] : (X9)) @ (^[X8 : $i] : ((X7 @ (^[X9 : ($i > $i > $i), X10 : $i] : (c_Empty))))) @ (X4 @ c_Empty @ (^[X8 : $i, X9 : $i] : (c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X8 : $i] : (c_Empty))))) @ (X4 @ (X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X8 : $i] : ((X0 @ (^[X9 : ($i > $i), X10 : (($i > $i > $i) > $i > $i), X11 : $i, X12 : ($i > $i)] : (c_Empty)) @ (^[X9 : $i, X10 : $i, X11 : ($i > $i)] : (c_Empty)))))) @ (^[X8 : $i, X9 : $i] : ((X1 @ (^[X10 : $i, X11 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((X11 @ (^[X12 : ($i > $i), X13 : $i] : (c_Empty)) @ c_Empty @ c_Empty))) @ X9))) @ X5))))) => (! [X4 : (($i > $i) > $i),X5 : ($i > $i),X6 : $i,X7 : $i] : (((X0 @ (^[X8 : ($i > $i), X9 : (($i > $i > $i) > $i > $i), X10 : $i, X11 : ($i > $i)] : (c_Empty)) @ (^[X8 : $i, X9 : $i, X10 : ($i > $i)] : ((X0 @ (^[X11 : ($i > $i), X12 : (($i > $i > $i) > $i > $i), X13 : $i, X14 : ($i > $i)] : ((X2 @ (^[X15 : $i, X16 : $i] : ((X14 @ X13))) @ (^[X15 : $i] : (X15)) @ c_Empty @ (X14 @ (X3 @ (^[X15 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X15 : $i] : (c_Empty)))) @ (X0 @ (^[X15 : ($i > $i), X16 : (($i > $i > $i) > $i > $i), X17 : $i, X18 : ($i > $i)] : ((c_Inj0 @ c_Empty))) @ (^[X15 : $i, X16 : $i, X17 : ($i > $i)] : ((X1 @ (^[X18 : $i, X19 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))))))) @ (^[X11 : $i, X12 : $i, X13 : ($i > $i)] : ((c_Inj1 @ (X0 @ (^[X14 : ($i > $i), X15 : (($i > $i > $i) > $i > $i), X16 : $i, X17 : ($i > $i)] : (c_Empty)) @ (^[X14 : $i, X15 : $i, X16 : ($i > $i)] : ((X13 @ c_Empty)))))))))))) = ((X0 @ (^[X8 : ($i > $i), X9 : (($i > $i > $i) > $i > $i), X10 : $i, X11 : ($i > $i)] : ((c_setsum @ (X0 @ (^[X12 : ($i > $i), X13 : (($i > $i > $i) > $i > $i), X14 : $i, X15 : ($i > $i)] : (c_Empty)) @ (^[X12 : $i, X13 : $i, X14 : ($i > $i)] : (c_Empty))) @ c_Empty))) @ (^[X8 : $i, X9 : $i, X10 : ($i > $i)] : ((c_setsum @ c_Empty @ c_Empty)))))) => (! [X4 : $i,X5 : $i,X6 : $i,X7 : $i] : (((X0 @ (^[X8 : ($i > $i), X9 : (($i > $i > $i) > $i > $i), X10 : $i, X11 : ($i > $i)] : (c_Empty)) @ (^[X8 : $i, X9 : $i, X10 : ($i > $i)] : (c_Empty)))) = X4) => c_False))))))))),
% 1.65/0.53    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 1.65/0.53  thf(f110,negated_conjecture,(
% 1.65/0.53    ~ ! [X0 : ((($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i) > ($i > $i > ($i > $i) > $i) > $i),X1 : (($i > ((($i > $i) > $i > $i) > $i > $i > $i) > $i) > $i > $i),X2 : (($i > $i > $i) > ($i > $i) > $i > $i > $i > $i),X3 : ((((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i)] : (! [X4 : (($i > $i > $i) > $i),X5 : $i,X6 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i),X7 : ((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i)] : (((X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((c_setsum @ (X0 @ (^[X9 : ($i > $i), X10 : (($i > $i > $i) > $i > $i), X11 : $i, X12 : ($i > $i)] : ((X1 @ (^[X13 : $i, X14 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_setsum @ c_Empty @ c_Empty))) @ (c_Inj1 @ c_Empty)))) @ (^[X9 : $i, X10 : $i, X11 : ($i > $i)] : (c_Empty))) @ (X1 @ (^[X9 : $i, X10 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ (X2 @ (^[X9 : $i, X10 : $i] : ((X7 @ (^[X11 : ($i > $i > $i)] : (c_Empty)) @ (^[X11 : $i] : (c_Empty)) @ c_Empty @ c_Empty))) @ (^[X9 : $i] : (c_Empty)) @ (X6 @ (^[X9 : (($i > $i) > $i), X10 : ($i > $i), X11 : $i] : (c_Empty)) @ c_Empty) @ (X1 @ (^[X9 : $i, X10 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty)))))) @ (^[X8 : $i] : (X8)))) = ((c_Inj1 @ c_Empty))) => (! [X4 : $i,X5 : $i,X6 : ($i > $i),X7 : $i] : (((X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X8 : $i] : ((X6 @ X8))))) = ((X6 @ (c_setsum @ (X2 @ (^[X8 : $i, X9 : $i] : ((X1 @ (^[X10 : $i, X11 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ (c_setsum @ c_Empty @ c_Empty)))) @ (^[X8 : $i] : (X8)) @ X5 @ c_Empty @ c_Empty) @ (X1 @ (^[X8 : $i, X9 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((X9 @ (^[X10 : ($i > $i), X11 : $i] : (c_Empty)) @ X8 @ (X2 @ (^[X10 : $i, X11 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))) @ c_Empty))))) => (! [X4 : $i,X5 : (($i > ($i > $i) > $i) > $i),X6 : $i,X7 : ($i > $i)] : (((X2 @ (^[X8 : $i, X9 : $i] : (c_Empty)) @ (^[X8 : $i] : ((X2 @ (^[X9 : $i, X10 : $i] : ((X2 @ (^[X11 : $i, X12 : $i] : (c_Empty)) @ (^[X11 : $i] : (c_Empty)) @ (X0 @ (^[X11 : ($i > $i), X12 : (($i > $i > $i) > $i > $i), X13 : $i, X14 : ($i > $i)] : ((c_setsum @ c_Empty @ c_Empty))) @ (^[X11 : $i, X12 : $i, X13 : ($i > $i)] : ((X0 @ (^[X14 : ($i > $i), X15 : (($i > $i > $i) > $i > $i), X16 : $i, X17 : ($i > $i)] : (c_Empty)) @ (^[X14 : $i, X15 : $i, X16 : ($i > $i)] : (c_Empty)))))) @ (X7 @ X10) @ X10))) @ (^[X9 : $i] : (X8)) @ (X1 @ (^[X9 : $i, X10 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ (X2 @ (^[X9 : $i, X10 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X9 : $i] : ((X1 @ (^[X10 : $i, X11 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))) @ (X3 @ (^[X9 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X9 : $i] : (c_Empty))) @ (c_Inj1 @ c_Empty) @ (X0 @ (^[X9 : ($i > $i), X10 : (($i > $i > $i) > $i > $i), X11 : $i, X12 : ($i > $i)] : (c_Empty)) @ (^[X9 : $i, X10 : $i, X11 : ($i > $i)] : (c_Empty))))) @ (X7 @ c_Empty) @ c_Empty))) @ X4 @ (X0 @ (^[X8 : ($i > $i), X9 : (($i > $i > $i) > $i > $i), X10 : $i, X11 : ($i > $i)] : ((c_Inj0 @ c_Empty))) @ (^[X8 : $i, X9 : $i, X10 : ($i > $i)] : ((c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (X1 @ (^[X11 : $i, X12 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty)))))) @ (c_setsum @ c_Empty @ (X7 @ c_Empty)))) = X4) => (! [X4 : ($i > $i > $i),X5 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i),X6 : ((($i > $i > $i) > $i > $i) > $i),X7 : ($i > $i)] : (((X2 @ (^[X8 : $i, X9 : $i] : ((X2 @ (^[X10 : $i, X11 : $i] : (c_Empty)) @ (^[X10 : $i] : (X8)) @ (X7 @ c_Empty) @ (X6 @ (^[X10 : ($i > $i > $i), X11 : $i] : ((c_setsum @ c_Empty @ (X0 @ (^[X12 : ($i > $i), X13 : (($i > $i > $i) > $i > $i), X14 : $i, X15 : ($i > $i)] : (c_Empty)) @ (^[X12 : $i, X13 : $i, X14 : ($i > $i)] : (c_Empty))))))) @ c_Empty))) @ (^[X8 : $i] : (c_Empty)) @ (X5 @ (^[X8 : (($i > $i) > $i), X9 : ($i > $i), X10 : $i] : (c_Empty)) @ c_Empty @ (X2 @ (^[X8 : $i, X9 : $i] : ((X3 @ (^[X10 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (X9)) @ (^[X10 : $i] : ((c_Inj0 @ c_Empty)))))) @ (^[X8 : $i] : ((X3 @ (^[X9 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((X6 @ (^[X10 : ($i > $i > $i), X11 : $i] : (c_Empty))))) @ (^[X9 : $i] : ((c_Inj0 @ c_Empty)))))) @ (X7 @ c_Empty) @ c_Empty @ (X5 @ (^[X8 : (($i > $i) > $i), X9 : ($i > $i), X10 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X7 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X5 @ (^[X8 : (($i > $i) > $i), X9 : ($i > $i), X10 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X7 @ (c_Inj1 @ c_Empty)))) = ((X7 @ (c_Inj0 @ c_Empty)))) => (! [X4 : $i,X5 : ($i > $i > ($i > $i) > $i > $i),X6 : ((($i > $i) > $i > $i) > $i),X7 : $i] : (((X1 @ (^[X8 : $i, X9 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (X2 @ (^[X10 : $i, X11 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X3 @ (^[X10 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X10 : $i] : (c_Empty))))) @ (c_setsum @ (c_setsum @ (X0 @ (^[X10 : ($i > $i), X11 : (($i > $i > $i) > $i > $i), X12 : $i, X13 : ($i > $i)] : (c_Empty)) @ (^[X10 : $i, X11 : $i, X12 : ($i > $i)] : (c_Empty))) @ c_Empty) @ (X9 @ (^[X10 : ($i > $i), X11 : $i] : ((c_Inj0 @ c_Empty))) @ (X9 @ (^[X10 : ($i > $i), X11 : $i] : (c_Empty)) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty)))))) @ (X2 @ (^[X8 : $i, X9 : $i] : (c_Empty)) @ (^[X8 : $i] : ((X6 @ (^[X9 : ($i > $i), X10 : $i] : ((c_setsum @ (c_Inj1 @ c_Empty) @ (X2 @ (^[X11 : $i, X12 : $i] : (c_Empty)) @ (^[X11 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))) @ (c_setsum @ X4 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))) = ((X2 @ (^[X8 : $i, X9 : $i] : ((c_setsum @ X7 @ (c_Inj1 @ X7)))) @ (^[X8 : $i] : ((X0 @ (^[X9 : ($i > $i), X10 : (($i > $i > $i) > $i > $i), X11 : $i, X12 : ($i > $i)] : ((c_Inj1 @ c_Empty))) @ (^[X9 : $i, X10 : $i, X11 : ($i > $i)] : (c_Empty))))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (X0 @ (^[X8 : ($i > $i), X9 : (($i > $i > $i) > $i > $i), X10 : $i, X11 : ($i > $i)] : ((c_Inj1 @ c_Empty))) @ (^[X8 : $i, X9 : $i, X10 : ($i > $i)] : ((c_Inj0 @ (X2 @ (^[X11 : $i, X12 : $i] : (c_Empty)) @ (^[X11 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_Inj1 @ (X6 @ (^[X8 : ($i > $i), X9 : $i] : ((c_Inj1 @ c_Empty))))) @ (c_setsum @ (X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((X8 @ (^[X9 : ($i > $i > $i), X10 : ($i > $i)] : (c_Empty)) @ c_Empty @ c_Empty))) @ (^[X8 : $i] : ((c_Inj1 @ c_Empty)))) @ (c_setsum @ c_Empty @ c_Empty)))))) => (! [X4 : ($i > ($i > $i > $i) > $i > $i),X5 : $i,X6 : $i,X7 : ((($i > $i > $i) > $i > $i) > $i)] : (((X1 @ (^[X8 : $i, X9 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_setsum @ (X1 @ (^[X10 : $i, X11 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (X8)) @ (c_setsum @ (X2 @ (^[X10 : $i, X11 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X1 @ (^[X10 : $i, X11 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))) @ c_Empty))) @ (X2 @ (^[X8 : $i, X9 : $i] : (X9)) @ (^[X8 : $i] : ((X0 @ (^[X9 : ($i > $i), X10 : (($i > $i > $i) > $i > $i), X11 : $i, X12 : ($i > $i)] : (X11)) @ (^[X9 : $i, X10 : $i, X11 : ($i > $i)] : ((X3 @ (^[X12 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((X12 @ (^[X13 : ($i > $i > $i), X14 : ($i > $i)] : (c_Empty)) @ c_Empty @ c_Empty))) @ (^[X12 : $i] : (c_Empty)))))))) @ X5 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (X2 @ (^[X8 : $i, X9 : $i] : (c_Empty)) @ (^[X8 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) = ((X2 @ (^[X8 : $i, X9 : $i] : ((c_Inj0 @ c_Empty))) @ (^[X8 : $i] : ((X1 @ (^[X9 : $i, X10 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((X7 @ (^[X11 : ($i > $i > $i), X12 : $i] : ((X10 @ (^[X13 : ($i > $i), X14 : $i] : ((X2 @ (^[X15 : $i, X16 : $i] : (c_Empty)) @ (^[X15 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ c_Empty @ (X1 @ (^[X13 : $i, X14 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))))))) @ c_Empty))) @ (c_Inj0 @ (X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (^[X8 : $i] : ((X3 @ (^[X9 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((c_setsum @ c_Empty @ c_Empty))) @ (^[X9 : $i] : ((X2 @ (^[X10 : $i, X11 : $i] : (c_Empty)) @ (^[X10 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))))) @ (c_setsum @ (c_setsum @ X5 @ (X1 @ (^[X8 : $i, X9 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_Inj0 @ c_Empty))) @ (X2 @ (^[X8 : $i, X9 : $i] : (c_Empty)) @ (^[X8 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (X1 @ (^[X8 : $i, X9 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_Inj0 @ (X0 @ (^[X10 : ($i > $i), X11 : (($i > $i > $i) > $i > $i), X12 : $i, X13 : ($i > $i)] : (c_Empty)) @ (^[X10 : $i, X11 : $i, X12 : ($i > $i)] : (c_Empty)))))) @ X5)) @ (c_setsum @ (c_setsum @ X6 @ (X2 @ (^[X8 : $i, X9 : $i] : (X9)) @ (^[X8 : $i] : ((X7 @ (^[X9 : ($i > $i > $i), X10 : $i] : (c_Empty))))) @ (X4 @ c_Empty @ (^[X8 : $i, X9 : $i] : (c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X8 : $i] : (c_Empty))))) @ (X4 @ (X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X8 : $i] : ((X0 @ (^[X9 : ($i > $i), X10 : (($i > $i > $i) > $i > $i), X11 : $i, X12 : ($i > $i)] : (c_Empty)) @ (^[X9 : $i, X10 : $i, X11 : ($i > $i)] : (c_Empty)))))) @ (^[X8 : $i, X9 : $i] : ((X1 @ (^[X10 : $i, X11 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((X11 @ (^[X12 : ($i > $i), X13 : $i] : (c_Empty)) @ c_Empty @ c_Empty))) @ X9))) @ X5))))) => (! [X4 : (($i > $i) > $i),X5 : ($i > $i),X6 : $i,X7 : $i] : (((X0 @ (^[X8 : ($i > $i), X9 : (($i > $i > $i) > $i > $i), X10 : $i, X11 : ($i > $i)] : (c_Empty)) @ (^[X8 : $i, X9 : $i, X10 : ($i > $i)] : ((X0 @ (^[X11 : ($i > $i), X12 : (($i > $i > $i) > $i > $i), X13 : $i, X14 : ($i > $i)] : ((X2 @ (^[X15 : $i, X16 : $i] : ((X14 @ X13))) @ (^[X15 : $i] : (X15)) @ c_Empty @ (X14 @ (X3 @ (^[X15 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X15 : $i] : (c_Empty)))) @ (X0 @ (^[X15 : ($i > $i), X16 : (($i > $i > $i) > $i > $i), X17 : $i, X18 : ($i > $i)] : ((c_Inj0 @ c_Empty))) @ (^[X15 : $i, X16 : $i, X17 : ($i > $i)] : ((X1 @ (^[X18 : $i, X19 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))))))) @ (^[X11 : $i, X12 : $i, X13 : ($i > $i)] : ((c_Inj1 @ (X0 @ (^[X14 : ($i > $i), X15 : (($i > $i > $i) > $i > $i), X16 : $i, X17 : ($i > $i)] : (c_Empty)) @ (^[X14 : $i, X15 : $i, X16 : ($i > $i)] : ((X13 @ c_Empty)))))))))))) = ((X0 @ (^[X8 : ($i > $i), X9 : (($i > $i > $i) > $i > $i), X10 : $i, X11 : ($i > $i)] : ((c_setsum @ (X0 @ (^[X12 : ($i > $i), X13 : (($i > $i > $i) > $i > $i), X14 : $i, X15 : ($i > $i)] : (c_Empty)) @ (^[X12 : $i, X13 : $i, X14 : ($i > $i)] : (c_Empty))) @ c_Empty))) @ (^[X8 : $i, X9 : $i, X10 : ($i > $i)] : ((c_setsum @ c_Empty @ c_Empty)))))) => (! [X4 : $i,X5 : $i,X6 : $i,X7 : $i] : (((X0 @ (^[X8 : ($i > $i), X9 : (($i > $i > $i) > $i > $i), X10 : $i, X11 : ($i > $i)] : (c_Empty)) @ (^[X8 : $i, X9 : $i, X10 : ($i > $i)] : (c_Empty)))) = X4) => c_False))))))))),
% 1.65/0.53    inference(negated_conjecture,[status(cth)],[f109])).
% 1.65/0.53  thf(f119,plain,(
% 1.65/0.53    (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 1.65/0.53    inference(rectify,[],[f5])).
% 1.65/0.53  thf(f120,plain,(
% 1.65/0.53    ($true = ((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 1.65/0.53    inference(fool_elimination,[],[f119])).
% 1.65/0.53  thf(f121,plain,(
% 1.65/0.53    ! [X0 : $i,X1 : $i] : (c_iff @ (c_In @ X1 @ (c_Union @ X0)) @ ? [X2 : $i] : (c_and @ (c_In @ X1 @ X2) @ (c_In @ X2 @ X0)))),
% 1.65/0.53    inference(rectify,[],[f6])).
% 1.65/0.53  thf(f122,plain,(
% 1.65/0.53    ! [X0 : $i,X1 : $i] : ($true = ((c_iff @ (c_In @ X1 @ (c_Union @ X0)) @ (?? @ $i @ (^[Y0 : $i]: (c_and @ (c_In @ X1 @ Y0) @ (c_In @ Y0 @ X0)))))))),
% 1.65/0.53    inference(fool_elimination,[],[f121])).
% 1.65/0.53  thf(f123,plain,(
% 1.65/0.53    ! [X0 : $i,X1 : $i] : (c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))),
% 1.65/0.53    inference(rectify,[],[f7])).
% 1.65/0.53  thf(f124,plain,(
% 1.65/0.53    ! [X0 : $i,X1 : $i] : (((c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))) = $true)),
% 1.65/0.53    inference(fool_elimination,[],[f123])).
% 1.65/0.53  thf(f135,plain,(
% 1.65/0.53    (c_not = (^[X0 : $o] : (X0 => c_False)))),
% 1.65/0.53    inference(rectify,[],[f13])).
% 1.65/0.53  thf(f136,plain,(
% 1.65/0.53    (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 1.65/0.53    inference(fool_elimination,[],[f135])).
% 1.65/0.53  thf(f137,plain,(
% 1.65/0.53    (c_and = (^[X0 : $o, X1 : $o] : (! [X2 : $o] : ((X0 => (X1 => X2)) => X2))))),
% 1.65/0.53    inference(rectify,[],[f14])).
% 1.65/0.53  thf(f138,plain,(
% 1.65/0.53    (c_and = (^[Y0 : $o]: ((^[Y1 : $o]: (!! @ $o @ (^[Y2 : $o]: ((Y0 => (Y1 => Y2)) => Y2)))))))),
% 1.65/0.53    inference(fool_elimination,[],[f137])).
% 1.65/0.53  thf(f141,plain,(
% 1.65/0.53    (c_iff = (^[X0 : $o, X1 : $o] : ((c_and @ X0 => X1 @ X1 => X0))))),
% 1.65/0.53    inference(rectify,[],[f16])).
% 1.65/0.53  thf(f142,plain,(
% 1.65/0.53    (c_iff = (^[Y0 : $o]: ((^[Y1 : $o]: (c_and @ (Y0 => Y1) @ (Y1 => Y0))))))),
% 1.65/0.53    inference(fool_elimination,[],[f141])).
% 1.65/0.53  thf(f143,plain,(
% 1.65/0.53    (c_Subq = (^[X0 : $i, X1 : $i] : (! [X2 : $i] : ((c_In @ X2 @ X0) => (c_In @ X2 @ X1)))))),
% 1.65/0.53    inference(rectify,[],[f17])).
% 1.65/0.53  thf(f144,plain,(
% 1.65/0.53    (c_Subq = (^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))))),
% 1.65/0.53    inference(fool_elimination,[],[f143])).
% 1.65/0.53  thf(f306,plain,(
% 1.65/0.53    ~ ! [X0 : ((($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i) > ($i > $i > ($i > $i) > $i) > $i),X1 : (($i > ((($i > $i) > $i > $i) > $i > $i > $i) > $i) > $i > $i),X2 : (($i > $i > $i) > ($i > $i) > $i > $i > $i > $i),X3 : ((((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i)] : (! [X6 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i),X7 : ((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i)] : (((X3 @ (^[X8 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((c_setsum @ (X0 @ (^[X9 : ($i > $i), X10 : (($i > $i > $i) > $i > $i), X11 : $i, X12 : ($i > $i)] : ((X1 @ (^[X13 : $i, X14 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_setsum @ c_Empty @ c_Empty))) @ (c_Inj1 @ c_Empty)))) @ (^[X15 : $i, X16 : $i, X17 : ($i > $i)] : (c_Empty))) @ (X1 @ (^[X18 : $i, X19 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ (X2 @ (^[X20 : $i, X21 : $i] : ((X7 @ (^[X22 : ($i > $i > $i)] : (c_Empty)) @ (^[X23 : $i] : (c_Empty)) @ c_Empty @ c_Empty))) @ (^[X24 : $i] : (c_Empty)) @ (X6 @ (^[X25 : (($i > $i) > $i), X26 : ($i > $i), X27 : $i] : (c_Empty)) @ c_Empty) @ (X1 @ (^[X28 : $i, X29 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty)))))) @ (^[X30 : $i] : (X30)))) = ((c_Inj1 @ c_Empty))) => (! [X32 : $i,X33 : ($i > $i)] : (((X3 @ (^[X35 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X36 : $i] : ((X33 @ X36))))) = ((X33 @ (c_setsum @ (X2 @ (^[X37 : $i, X38 : $i] : ((X1 @ (^[X39 : $i, X40 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ (c_setsum @ c_Empty @ c_Empty)))) @ (^[X41 : $i] : (X41)) @ X32 @ c_Empty @ c_Empty) @ (X1 @ (^[X42 : $i, X43 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((X43 @ (^[X44 : ($i > $i), X45 : $i] : (c_Empty)) @ X42 @ (X2 @ (^[X46 : $i, X47 : $i] : (c_Empty)) @ (^[X48 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))) @ c_Empty))))) => (! [X49 : $i,X52 : ($i > $i)] : (((X2 @ (^[X53 : $i, X54 : $i] : (c_Empty)) @ (^[X55 : $i] : ((X2 @ (^[X56 : $i, X57 : $i] : ((X2 @ (^[X58 : $i, X59 : $i] : (c_Empty)) @ (^[X60 : $i] : (c_Empty)) @ (X0 @ (^[X61 : ($i > $i), X62 : (($i > $i > $i) > $i > $i), X63 : $i, X64 : ($i > $i)] : ((c_setsum @ c_Empty @ c_Empty))) @ (^[X65 : $i, X66 : $i, X67 : ($i > $i)] : ((X0 @ (^[X68 : ($i > $i), X69 : (($i > $i > $i) > $i > $i), X70 : $i, X71 : ($i > $i)] : (c_Empty)) @ (^[X72 : $i, X73 : $i, X74 : ($i > $i)] : (c_Empty)))))) @ (X52 @ X57) @ X57))) @ (^[X75 : $i] : (X55)) @ (X1 @ (^[X76 : $i, X77 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ (X2 @ (^[X78 : $i, X79 : $i] : ((c_Inj1 @ c_Empty))) @ (^[X80 : $i] : ((X1 @ (^[X81 : $i, X82 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))) @ (X3 @ (^[X83 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X84 : $i] : (c_Empty))) @ (c_Inj1 @ c_Empty) @ (X0 @ (^[X85 : ($i > $i), X86 : (($i > $i > $i) > $i > $i), X87 : $i, X88 : ($i > $i)] : (c_Empty)) @ (^[X89 : $i, X90 : $i, X91 : ($i > $i)] : (c_Empty))))) @ (X52 @ c_Empty) @ c_Empty))) @ X49 @ (X0 @ (^[X92 : ($i > $i), X93 : (($i > $i > $i) > $i > $i), X94 : $i, X95 : ($i > $i)] : ((c_Inj0 @ c_Empty))) @ (^[X96 : $i, X97 : $i, X98 : ($i > $i)] : ((c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (X1 @ (^[X99 : $i, X100 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty)))))) @ (c_setsum @ c_Empty @ (X52 @ c_Empty)))) = X49) => (! [X102 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i),X103 : ((($i > $i > $i) > $i > $i) > $i),X104 : ($i > $i)] : (((X2 @ (^[X105 : $i, X106 : $i] : ((X2 @ (^[X107 : $i, X108 : $i] : (c_Empty)) @ (^[X109 : $i] : (X105)) @ (X104 @ c_Empty) @ (X103 @ (^[X110 : ($i > $i > $i), X111 : $i] : ((c_setsum @ c_Empty @ (X0 @ (^[X112 : ($i > $i), X113 : (($i > $i > $i) > $i > $i), X114 : $i, X115 : ($i > $i)] : (c_Empty)) @ (^[X116 : $i, X117 : $i, X118 : ($i > $i)] : (c_Empty))))))) @ c_Empty))) @ (^[X119 : $i] : (c_Empty)) @ (X102 @ (^[X120 : (($i > $i) > $i), X121 : ($i > $i), X122 : $i] : (c_Empty)) @ c_Empty @ (X2 @ (^[X123 : $i, X124 : $i] : ((X3 @ (^[X125 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (X124)) @ (^[X126 : $i] : ((c_Inj0 @ c_Empty)))))) @ (^[X127 : $i] : ((X3 @ (^[X128 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((X103 @ (^[X129 : ($i > $i > $i), X130 : $i] : (c_Empty))))) @ (^[X131 : $i] : ((c_Inj0 @ c_Empty)))))) @ (X104 @ c_Empty) @ c_Empty @ (X102 @ (^[X132 : (($i > $i) > $i), X133 : ($i > $i), X134 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X104 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X102 @ (^[X135 : (($i > $i) > $i), X136 : ($i > $i), X137 : $i] : ((c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X104 @ (c_Inj1 @ c_Empty)))) = ((X104 @ (c_Inj0 @ c_Empty)))) => (! [X138 : $i,X140 : ((($i > $i) > $i > $i) > $i),X141 : $i] : (((X1 @ (^[X142 : $i, X143 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (X2 @ (^[X144 : $i, X145 : $i] : (c_Empty)) @ (^[X146 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X3 @ (^[X147 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X148 : $i] : (c_Empty))))) @ (c_setsum @ (c_setsum @ (X0 @ (^[X149 : ($i > $i), X150 : (($i > $i > $i) > $i > $i), X151 : $i, X152 : ($i > $i)] : (c_Empty)) @ (^[X153 : $i, X154 : $i, X155 : ($i > $i)] : (c_Empty))) @ c_Empty) @ (X143 @ (^[X156 : ($i > $i), X157 : $i] : ((c_Inj0 @ c_Empty))) @ (X143 @ (^[X158 : ($i > $i), X159 : $i] : (c_Empty)) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty)))))) @ (X2 @ (^[X160 : $i, X161 : $i] : (c_Empty)) @ (^[X162 : $i] : ((X140 @ (^[X163 : ($i > $i), X164 : $i] : ((c_setsum @ (c_Inj1 @ c_Empty) @ (X2 @ (^[X165 : $i, X166 : $i] : (c_Empty)) @ (^[X167 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))) @ (c_setsum @ X138 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))) = ((X2 @ (^[X168 : $i, X169 : $i] : ((c_setsum @ X141 @ (c_Inj1 @ X141)))) @ (^[X170 : $i] : ((X0 @ (^[X171 : ($i > $i), X172 : (($i > $i > $i) > $i > $i), X173 : $i, X174 : ($i > $i)] : ((c_Inj1 @ c_Empty))) @ (^[X175 : $i, X176 : $i, X177 : ($i > $i)] : (c_Empty))))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (X0 @ (^[X178 : ($i > $i), X179 : (($i > $i > $i) > $i > $i), X180 : $i, X181 : ($i > $i)] : ((c_Inj1 @ c_Empty))) @ (^[X182 : $i, X183 : $i, X184 : ($i > $i)] : ((c_Inj0 @ (X2 @ (^[X185 : $i, X186 : $i] : (c_Empty)) @ (^[X187 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_Inj1 @ (X140 @ (^[X188 : ($i > $i), X189 : $i] : ((c_Inj1 @ c_Empty))))) @ (c_setsum @ (X3 @ (^[X190 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((X190 @ (^[X191 : ($i > $i > $i), X192 : ($i > $i)] : (c_Empty)) @ c_Empty @ c_Empty))) @ (^[X193 : $i] : ((c_Inj1 @ c_Empty)))) @ (c_setsum @ c_Empty @ c_Empty)))))) => (! [X194 : ($i > ($i > $i > $i) > $i > $i),X195 : $i,X196 : $i,X197 : ((($i > $i > $i) > $i > $i) > $i)] : (((X1 @ (^[X198 : $i, X199 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_setsum @ (X1 @ (^[X200 : $i, X201 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (X198)) @ (c_setsum @ (X2 @ (^[X202 : $i, X203 : $i] : (c_Empty)) @ (^[X204 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X1 @ (^[X205 : $i, X206 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))) @ c_Empty))) @ (X2 @ (^[X207 : $i, X208 : $i] : (X208)) @ (^[X209 : $i] : ((X0 @ (^[X210 : ($i > $i), X211 : (($i > $i > $i) > $i > $i), X212 : $i, X213 : ($i > $i)] : (X212)) @ (^[X214 : $i, X215 : $i, X216 : ($i > $i)] : ((X3 @ (^[X217 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((X217 @ (^[X218 : ($i > $i > $i), X219 : ($i > $i)] : (c_Empty)) @ c_Empty @ c_Empty))) @ (^[X220 : $i] : (c_Empty)))))))) @ X195 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (X2 @ (^[X221 : $i, X222 : $i] : (c_Empty)) @ (^[X223 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) = ((X2 @ (^[X224 : $i, X225 : $i] : ((c_Inj0 @ c_Empty))) @ (^[X226 : $i] : ((X1 @ (^[X227 : $i, X228 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((X197 @ (^[X229 : ($i > $i > $i), X230 : $i] : ((X228 @ (^[X231 : ($i > $i), X232 : $i] : ((X2 @ (^[X233 : $i, X234 : $i] : (c_Empty)) @ (^[X235 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ c_Empty @ (X1 @ (^[X236 : $i, X237 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))))))) @ c_Empty))) @ (c_Inj0 @ (X3 @ (^[X238 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (^[X239 : $i] : ((X3 @ (^[X240 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : ((c_setsum @ c_Empty @ c_Empty))) @ (^[X241 : $i] : ((X2 @ (^[X242 : $i, X243 : $i] : (c_Empty)) @ (^[X244 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))))) @ (c_setsum @ (c_setsum @ X195 @ (X1 @ (^[X245 : $i, X246 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_Inj0 @ c_Empty))) @ (X2 @ (^[X247 : $i, X248 : $i] : (c_Empty)) @ (^[X249 : $i] : (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (X1 @ (^[X250 : $i, X251 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((c_Inj0 @ (X0 @ (^[X252 : ($i > $i), X253 : (($i > $i > $i) > $i > $i), X254 : $i, X255 : ($i > $i)] : (c_Empty)) @ (^[X256 : $i, X257 : $i, X258 : ($i > $i)] : (c_Empty)))))) @ X195)) @ (c_setsum @ (c_setsum @ X196 @ (X2 @ (^[X259 : $i, X260 : $i] : (X260)) @ (^[X261 : $i] : ((X197 @ (^[X262 : ($i > $i > $i), X263 : $i] : (c_Empty))))) @ (X194 @ c_Empty @ (^[X264 : $i, X265 : $i] : (c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (X3 @ (^[X266 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X267 : $i] : (c_Empty))))) @ (X194 @ (X3 @ (^[X268 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X269 : $i] : ((X0 @ (^[X270 : ($i > $i), X271 : (($i > $i > $i) > $i > $i), X272 : $i, X273 : ($i > $i)] : (c_Empty)) @ (^[X274 : $i, X275 : $i, X276 : ($i > $i)] : (c_Empty)))))) @ (^[X277 : $i, X278 : $i] : ((X1 @ (^[X279 : $i, X280 : ((($i > $i) > $i > $i) > $i > $i > $i)] : ((X280 @ (^[X281 : ($i > $i), X282 : $i] : (c_Empty)) @ c_Empty @ c_Empty))) @ X278))) @ X195))))) => ((((X0 @ (^[X287 : ($i > $i), X288 : (($i > $i > $i) > $i > $i), X289 : $i, X290 : ($i > $i)] : (c_Empty)) @ (^[X291 : $i, X292 : $i, X293 : ($i > $i)] : ((X0 @ (^[X294 : ($i > $i), X295 : (($i > $i > $i) > $i > $i), X296 : $i, X297 : ($i > $i)] : ((X2 @ (^[X298 : $i, X299 : $i] : ((X297 @ X296))) @ (^[X300 : $i] : (X300)) @ c_Empty @ (X297 @ (X3 @ (^[X301 : ((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i)] : (c_Empty)) @ (^[X302 : $i] : (c_Empty)))) @ (X0 @ (^[X303 : ($i > $i), X304 : (($i > $i > $i) > $i > $i), X305 : $i, X306 : ($i > $i)] : ((c_Inj0 @ c_Empty))) @ (^[X307 : $i, X308 : $i, X309 : ($i > $i)] : ((X1 @ (^[X310 : $i, X311 : ((($i > $i) > $i > $i) > $i > $i > $i)] : (c_Empty)) @ c_Empty))))))) @ (^[X312 : $i, X313 : $i, X314 : ($i > $i)] : ((c_Inj1 @ (X0 @ (^[X315 : ($i > $i), X316 : (($i > $i > $i) > $i > $i), X317 : $i, X318 : ($i > $i)] : (c_Empty)) @ (^[X319 : $i, X320 : $i, X321 : ($i > $i)] : ((X314 @ c_Empty)))))))))))) = ((X0 @ (^[X322 : ($i > $i), X323 : (($i > $i > $i) > $i > $i), X324 : $i, X325 : ($i > $i)] : ((c_setsum @ (X0 @ (^[X326 : ($i > $i), X327 : (($i > $i > $i) > $i > $i), X328 : $i, X329 : ($i > $i)] : (c_Empty)) @ (^[X330 : $i, X331 : $i, X332 : ($i > $i)] : (c_Empty))) @ c_Empty))) @ (^[X333 : $i, X334 : $i, X335 : ($i > $i)] : ((c_setsum @ c_Empty @ c_Empty)))))) => (! [X336 : $i] : (((X0 @ (^[X340 : ($i > $i), X341 : (($i > $i > $i) > $i > $i), X342 : $i, X343 : ($i > $i)] : (c_Empty)) @ (^[X344 : $i, X345 : $i, X346 : ($i > $i)] : (c_Empty)))) = X336) => c_False))))))))),
% 1.65/0.53    inference(rectify,[],[f110])).
% 1.65/0.53  thf(f307,plain,(
% 1.65/0.53    ~ ! [X0 : ((($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i) > ($i > $i > ($i > $i) > $i) > $i),X1 : (($i > ((($i > $i) > $i > $i) > $i > $i > $i) > $i) > $i > $i),X2 : (($i > $i > $i) > ($i > $i) > $i > $i > $i > $i),X3 : ((((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i)] : (! [X6 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i),X7 : ((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i)] : (((c_Inj1 @ c_Empty)) = ((X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (X1 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (c_Inj1 @ c_Empty))))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (X7 @ (^[Y3 : $i > $i > $i]: (c_Empty)) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty)))) @ (^[Y1 : $i]: (c_Empty)) @ (X6 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ c_Empty) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty))))) @ (^[Y0 : $i]: (Y0))))) => (! [X32 : $i,X33 : ($i > $i)] : (((X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (X33 @ Y0)))) = ((X33 @ (c_setsum @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (c_setsum @ c_Empty @ c_Empty))))) @ (^[Y0 : $i]: (Y0)) @ X32 @ c_Empty @ c_Empty) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ Y0 @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ c_Empty))))) => (! [X49 : $i,X52 : ($i > $i)] : (((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ (X0 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_setsum @ c_Empty @ c_Empty)))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (X0 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (c_Empty))))))))))))) @ (X52 @ Y2) @ Y2)))) @ (^[Y1 : $i]: (Y0)) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ (^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty)) @ (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y1 : $i]: (c_Empty))) @ (c_Inj1 @ c_Empty) @ (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (X52 @ c_Empty) @ c_Empty)) @ X49 @ (X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (X1 @ (^[Y3 : $i]: ((^[Y4 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ (c_setsum @ c_Empty @ (X52 @ c_Empty)))) = X49) => (! [X102 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i),X103 : ((($i > $i > $i) > $i > $i) > $i),X104 : ($i > $i)] : (((X104 @ (c_Inj0 @ c_Empty))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (Y0)) @ (X104 @ c_Empty) @ (X103 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ (X0 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty)))))))))))) @ c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ (X102 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ c_Empty @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X3 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y1)) @ (^[Y2 : $i]: (c_Inj0 @ c_Empty)))))) @ (^[Y0 : $i]: (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (X103 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (X104 @ c_Empty) @ c_Empty @ (X102 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X104 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X102 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X104 @ (c_Inj1 @ c_Empty))))) => (! [X138 : $i,X140 : ((($i > $i) > $i > $i) > $i),X141 : $i] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X3 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y2 : $i]: (c_Empty))))) @ (c_setsum @ (c_setsum @ (X0 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))) @ c_Empty) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Inj0 @ c_Empty)))) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty))))))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (X140 @ (^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ (c_Inj1 @ c_Empty) @ (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))) @ (c_setsum @ X138 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ X141 @ (c_Inj1 @ X141))))) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))))) @ (c_setsum @ (c_Inj1 @ (X140 @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty)))))) @ (c_setsum @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y0 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y0 : $i]: (c_Inj1 @ c_Empty))) @ (c_setsum @ c_Empty @ c_Empty)))))) => (! [X194 : ($i > ($i > $i > $i) > $i > $i),X195 : $i,X196 : $i,X197 : ((($i > $i > $i) > $i > $i) > $i)] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y0)))) @ (c_setsum @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))) @ c_Empty)))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (Y3)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (X3 @ (^[Y4 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y4 @ (^[Y5 : $i > $i > $i]: ((^[Y6 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y4 : $i]: (c_Empty)))))))))) @ X195 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (^[Y0 : $i]: (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (X197 @ (^[Y3 : $i > $i > $i]: ((^[Y4 : $i]: (Y2 @ (^[Y5 : $i > $i]: ((^[Y6 : $i]: (X2 @ (^[Y7 : $i]: ((^[Y8 : $i]: (c_Empty)))) @ (^[Y7 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))) @ c_Empty @ (X1 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ c_Empty)) @ (c_Inj0 @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[Y0 : $i]: (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)) @ (^[Y1 : $i]: (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_setsum @ X195 @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ c_Empty)))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ (X0 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))))))) @ X195)) @ (c_setsum @ (c_setsum @ X196 @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (X197 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ (X194 @ c_Empty @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) @ (X194 @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y3 @ (^[Y4 : $i > $i]: ((^[Y5 : $i]: (c_Empty)))) @ c_Empty @ c_Empty)))) @ Y1)))) @ X195))))) => ((((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (X0 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (X2 @ (^[Y7 : $i]: ((^[Y8 : $i]: (Y6 @ Y5)))) @ (^[Y7 : $i]: (Y7)) @ c_Empty @ (Y6 @ (X3 @ (^[Y7 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y7 : $i]: (c_Empty)))) @ (X0 @ (^[Y7 : $i > $i]: ((^[Y8 : ($i > $i > $i) > $i > $i]: ((^[Y9 : $i]: ((^[Y10 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y7 : $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (X1 @ (^[Y10 : $i]: ((^[Y11 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Inj1 @ (X0 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (Y5 @ c_Empty))))))))))))))))))))) = ((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_setsum @ (X0 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty))))))) @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_setsum @ c_Empty @ c_Empty))))))))) => (! [X336 : $i] : (((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Empty)))))))) = X336) => (c_False = $true)))))))))),
% 1.65/0.53    inference(fool_elimination,[],[f306])).
% 1.65/0.53  thf(f309,plain,(
% 1.65/0.53    ~ ! [X0 : ((($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i) > ($i > $i > ($i > $i) > $i) > $i),X1 : (($i > ((($i > $i) > $i > $i) > $i > $i > $i) > $i) > $i > $i),X2 : (($i > $i > $i) > ($i > $i) > $i > $i > $i > $i),X3 : ((((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i)] : (! [X4 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i),X5 : ((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i)] : (((c_Inj1 @ c_Empty)) = ((X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (X1 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (c_Inj1 @ c_Empty))))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (X5 @ (^[Y3 : $i > $i > $i]: (c_Empty)) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty)))) @ (^[Y1 : $i]: (c_Empty)) @ (X4 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ c_Empty) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty))))) @ (^[Y0 : $i]: (Y0))))) => (! [X6 : $i,X7 : ($i > $i)] : (((X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (X7 @ Y0)))) = ((X7 @ (c_setsum @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (c_setsum @ c_Empty @ c_Empty))))) @ (^[Y0 : $i]: (Y0)) @ X6 @ c_Empty @ c_Empty) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ Y0 @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ c_Empty))))) => (! [X8 : $i,X9 : ($i > $i)] : (((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ (X0 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_setsum @ c_Empty @ c_Empty)))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (X0 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (c_Empty))))))))))))) @ (X9 @ Y2) @ Y2)))) @ (^[Y1 : $i]: (Y0)) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ (^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty)) @ (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y1 : $i]: (c_Empty))) @ (c_Inj1 @ c_Empty) @ (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (X9 @ c_Empty) @ c_Empty)) @ X8 @ (X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (X1 @ (^[Y3 : $i]: ((^[Y4 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ (c_setsum @ c_Empty @ (X9 @ c_Empty)))) = X8) => (! [X10 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i),X11 : ((($i > $i > $i) > $i > $i) > $i),X12 : ($i > $i)] : (((X12 @ (c_Inj0 @ c_Empty))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (Y0)) @ (X12 @ c_Empty) @ (X11 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ (X0 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty)))))))))))) @ c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ (X10 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ c_Empty @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X3 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y1)) @ (^[Y2 : $i]: (c_Inj0 @ c_Empty)))))) @ (^[Y0 : $i]: (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (X11 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (X12 @ c_Empty) @ c_Empty @ (X10 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X12 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X10 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X12 @ (c_Inj1 @ c_Empty))))) => (! [X13 : $i,X14 : ((($i > $i) > $i > $i) > $i),X15 : $i] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X3 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y2 : $i]: (c_Empty))))) @ (c_setsum @ (c_setsum @ (X0 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))) @ c_Empty) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Inj0 @ c_Empty)))) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty))))))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (X14 @ (^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ (c_Inj1 @ c_Empty) @ (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))) @ (c_setsum @ X13 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ X15 @ (c_Inj1 @ X15))))) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))))) @ (c_setsum @ (c_Inj1 @ (X14 @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty)))))) @ (c_setsum @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y0 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y0 : $i]: (c_Inj1 @ c_Empty))) @ (c_setsum @ c_Empty @ c_Empty)))))) => (! [X16 : ($i > ($i > $i > $i) > $i > $i),X17 : $i,X18 : $i,X19 : ((($i > $i > $i) > $i > $i) > $i)] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y0)))) @ (c_setsum @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))) @ c_Empty)))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (Y3)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (X3 @ (^[Y4 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y4 @ (^[Y5 : $i > $i > $i]: ((^[Y6 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y4 : $i]: (c_Empty)))))))))) @ X17 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (^[Y0 : $i]: (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (X19 @ (^[Y3 : $i > $i > $i]: ((^[Y4 : $i]: (Y2 @ (^[Y5 : $i > $i]: ((^[Y6 : $i]: (X2 @ (^[Y7 : $i]: ((^[Y8 : $i]: (c_Empty)))) @ (^[Y7 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))) @ c_Empty @ (X1 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ c_Empty)) @ (c_Inj0 @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[Y0 : $i]: (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)) @ (^[Y1 : $i]: (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_setsum @ X17 @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ c_Empty)))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ (X0 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))))))) @ X17)) @ (c_setsum @ (c_setsum @ X18 @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (X19 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ (X16 @ c_Empty @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) @ (X16 @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y3 @ (^[Y4 : $i > $i]: ((^[Y5 : $i]: (c_Empty)))) @ c_Empty @ c_Empty)))) @ Y1)))) @ X17))))) => ((((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (X0 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (X2 @ (^[Y7 : $i]: ((^[Y8 : $i]: (Y6 @ Y5)))) @ (^[Y7 : $i]: (Y7)) @ c_Empty @ (Y6 @ (X3 @ (^[Y7 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y7 : $i]: (c_Empty)))) @ (X0 @ (^[Y7 : $i > $i]: ((^[Y8 : ($i > $i > $i) > $i > $i]: ((^[Y9 : $i]: ((^[Y10 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y7 : $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (X1 @ (^[Y10 : $i]: ((^[Y11 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Inj1 @ (X0 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (Y5 @ c_Empty))))))))))))))))))))) = ((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_setsum @ (X0 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty))))))) @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_setsum @ c_Empty @ c_Empty))))))))) => (! [X20 : $i] : (((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Empty)))))))) = X20) => (c_False = $true)))))))))),
% 1.65/0.53    inference(rectify,[],[f307])).
% 1.65/0.53  thf(f318,plain,(
% 1.65/0.53    ? [X0 : ((($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i) > ($i > $i > ($i > $i) > $i) > $i),X1 : (($i > ((($i > $i) > $i > $i) > $i > $i > $i) > $i) > $i > $i),X2 : (($i > $i > $i) > ($i > $i) > $i > $i > $i > $i),X3 : ((((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i)] : (((((((((c_False != $true) & ! [X20 : $i] : (((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Empty)))))))) = X20)) & (((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (X0 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (X2 @ (^[Y7 : $i]: ((^[Y8 : $i]: (Y6 @ Y5)))) @ (^[Y7 : $i]: (Y7)) @ c_Empty @ (Y6 @ (X3 @ (^[Y7 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y7 : $i]: (c_Empty)))) @ (X0 @ (^[Y7 : $i > $i]: ((^[Y8 : ($i > $i > $i) > $i > $i]: ((^[Y9 : $i]: ((^[Y10 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y7 : $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (X1 @ (^[Y10 : $i]: ((^[Y11 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Inj1 @ (X0 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (Y5 @ c_Empty))))))))))))))))))))) = ((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_setsum @ (X0 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty))))))) @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_setsum @ c_Empty @ c_Empty)))))))))) & ! [X16 : ($i > ($i > $i > $i) > $i > $i),X17 : $i,X18 : $i,X19 : ((($i > $i > $i) > $i > $i) > $i)] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y0)))) @ (c_setsum @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))) @ c_Empty)))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (Y3)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (X3 @ (^[Y4 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y4 @ (^[Y5 : $i > $i > $i]: ((^[Y6 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y4 : $i]: (c_Empty)))))))))) @ X17 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (^[Y0 : $i]: (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (X19 @ (^[Y3 : $i > $i > $i]: ((^[Y4 : $i]: (Y2 @ (^[Y5 : $i > $i]: ((^[Y6 : $i]: (X2 @ (^[Y7 : $i]: ((^[Y8 : $i]: (c_Empty)))) @ (^[Y7 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))) @ c_Empty @ (X1 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ c_Empty)) @ (c_Inj0 @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[Y0 : $i]: (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)) @ (^[Y1 : $i]: (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_setsum @ X17 @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ c_Empty)))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ (X0 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))))))) @ X17)) @ (c_setsum @ (c_setsum @ X18 @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (X19 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ (X16 @ c_Empty @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) @ (X16 @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y3 @ (^[Y4 : $i > $i]: ((^[Y5 : $i]: (c_Empty)))) @ c_Empty @ c_Empty)))) @ Y1)))) @ X17)))))) & ! [X13 : $i,X14 : ((($i > $i) > $i > $i) > $i),X15 : $i] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X3 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y2 : $i]: (c_Empty))))) @ (c_setsum @ (c_setsum @ (X0 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))) @ c_Empty) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Inj0 @ c_Empty)))) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty))))))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (X14 @ (^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ (c_Inj1 @ c_Empty) @ (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))) @ (c_setsum @ X13 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ X15 @ (c_Inj1 @ X15))))) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))))) @ (c_setsum @ (c_Inj1 @ (X14 @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty)))))) @ (c_setsum @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y0 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y0 : $i]: (c_Inj1 @ c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))))))) & ! [X10 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i),X11 : ((($i > $i > $i) > $i > $i) > $i),X12 : ($i > $i)] : (((X12 @ (c_Inj0 @ c_Empty))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (Y0)) @ (X12 @ c_Empty) @ (X11 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ (X0 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty)))))))))))) @ c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ (X10 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ c_Empty @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X3 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y1)) @ (^[Y2 : $i]: (c_Inj0 @ c_Empty)))))) @ (^[Y0 : $i]: (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (X11 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (X12 @ c_Empty) @ c_Empty @ (X10 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X12 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X10 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X12 @ (c_Inj1 @ c_Empty)))))) & ! [X8 : $i,X9 : ($i > $i)] : (((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ (X0 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_setsum @ c_Empty @ c_Empty)))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (X0 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (c_Empty))))))))))))) @ (X9 @ Y2) @ Y2)))) @ (^[Y1 : $i]: (Y0)) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ (^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty)) @ (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y1 : $i]: (c_Empty))) @ (c_Inj1 @ c_Empty) @ (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (X9 @ c_Empty) @ c_Empty)) @ X8 @ (X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (X1 @ (^[Y3 : $i]: ((^[Y4 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ (c_setsum @ c_Empty @ (X9 @ c_Empty)))) = X8)) & ! [X6 : $i,X7 : ($i > $i)] : (((X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (X7 @ Y0)))) = ((X7 @ (c_setsum @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (c_setsum @ c_Empty @ c_Empty))))) @ (^[Y0 : $i]: (Y0)) @ X6 @ c_Empty @ c_Empty) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ Y0 @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ c_Empty)))))) & ! [X4 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i),X5 : ((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i)] : (((c_Inj1 @ c_Empty)) = ((X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (X1 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (c_Inj1 @ c_Empty))))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (X5 @ (^[Y3 : $i > $i > $i]: (c_Empty)) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty)))) @ (^[Y1 : $i]: (c_Empty)) @ (X4 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ c_Empty) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty))))) @ (^[Y0 : $i]: (Y0))))))),
% 1.65/0.53    inference(ennf_transformation,[],[f309])).
% 1.65/0.53  thf(f319,plain,(
% 1.65/0.53    ? [X0 : ((($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i) > ($i > $i > ($i > $i) > $i) > $i),X1 : (($i > ((($i > $i) > $i > $i) > $i > $i > $i) > $i) > $i > $i),X2 : (($i > $i > $i) > ($i > $i) > $i > $i > $i > $i),X3 : ((((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i)] : ((c_False != $true) & ! [X20 : $i] : (((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Empty)))))))) = X20) & (((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (X0 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (X2 @ (^[Y7 : $i]: ((^[Y8 : $i]: (Y6 @ Y5)))) @ (^[Y7 : $i]: (Y7)) @ c_Empty @ (Y6 @ (X3 @ (^[Y7 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y7 : $i]: (c_Empty)))) @ (X0 @ (^[Y7 : $i > $i]: ((^[Y8 : ($i > $i > $i) > $i > $i]: ((^[Y9 : $i]: ((^[Y10 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y7 : $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (X1 @ (^[Y10 : $i]: ((^[Y11 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Inj1 @ (X0 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (Y5 @ c_Empty))))))))))))))))))))) = ((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_setsum @ (X0 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty))))))) @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_setsum @ c_Empty @ c_Empty))))))))) & ! [X16 : ($i > ($i > $i > $i) > $i > $i),X17 : $i,X18 : $i,X19 : ((($i > $i > $i) > $i > $i) > $i)] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y0)))) @ (c_setsum @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))) @ c_Empty)))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (Y3)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (X3 @ (^[Y4 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y4 @ (^[Y5 : $i > $i > $i]: ((^[Y6 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y4 : $i]: (c_Empty)))))))))) @ X17 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (^[Y0 : $i]: (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (X19 @ (^[Y3 : $i > $i > $i]: ((^[Y4 : $i]: (Y2 @ (^[Y5 : $i > $i]: ((^[Y6 : $i]: (X2 @ (^[Y7 : $i]: ((^[Y8 : $i]: (c_Empty)))) @ (^[Y7 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))) @ c_Empty @ (X1 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ c_Empty)) @ (c_Inj0 @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[Y0 : $i]: (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)) @ (^[Y1 : $i]: (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_setsum @ X17 @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ c_Empty)))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ (X0 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))))))) @ X17)) @ (c_setsum @ (c_setsum @ X18 @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (X19 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ (X16 @ c_Empty @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) @ (X16 @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y3 @ (^[Y4 : $i > $i]: ((^[Y5 : $i]: (c_Empty)))) @ c_Empty @ c_Empty)))) @ Y1)))) @ X17))))) & ! [X13 : $i,X14 : ((($i > $i) > $i > $i) > $i),X15 : $i] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X3 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y2 : $i]: (c_Empty))))) @ (c_setsum @ (c_setsum @ (X0 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))) @ c_Empty) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Inj0 @ c_Empty)))) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty))))))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (X14 @ (^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ (c_Inj1 @ c_Empty) @ (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))) @ (c_setsum @ X13 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ X15 @ (c_Inj1 @ X15))))) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))))) @ (c_setsum @ (c_Inj1 @ (X14 @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty)))))) @ (c_setsum @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y0 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y0 : $i]: (c_Inj1 @ c_Empty))) @ (c_setsum @ c_Empty @ c_Empty)))))) & ! [X10 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i),X11 : ((($i > $i > $i) > $i > $i) > $i),X12 : ($i > $i)] : (((X12 @ (c_Inj0 @ c_Empty))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (Y0)) @ (X12 @ c_Empty) @ (X11 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ (X0 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty)))))))))))) @ c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ (X10 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ c_Empty @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X3 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y1)) @ (^[Y2 : $i]: (c_Inj0 @ c_Empty)))))) @ (^[Y0 : $i]: (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (X11 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (X12 @ c_Empty) @ c_Empty @ (X10 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X12 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X10 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X12 @ (c_Inj1 @ c_Empty))))) & ! [X8 : $i,X9 : ($i > $i)] : (((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ (X0 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_setsum @ c_Empty @ c_Empty)))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (X0 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (c_Empty))))))))))))) @ (X9 @ Y2) @ Y2)))) @ (^[Y1 : $i]: (Y0)) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ (^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty)) @ (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y1 : $i]: (c_Empty))) @ (c_Inj1 @ c_Empty) @ (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (X9 @ c_Empty) @ c_Empty)) @ X8 @ (X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (X1 @ (^[Y3 : $i]: ((^[Y4 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ (c_setsum @ c_Empty @ (X9 @ c_Empty)))) = X8) & ! [X6 : $i,X7 : ($i > $i)] : (((X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (X7 @ Y0)))) = ((X7 @ (c_setsum @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (c_setsum @ c_Empty @ c_Empty))))) @ (^[Y0 : $i]: (Y0)) @ X6 @ c_Empty @ c_Empty) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ Y0 @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ c_Empty))))) & ! [X4 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i),X5 : ((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i)] : (((c_Inj1 @ c_Empty)) = ((X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (X1 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (c_Inj1 @ c_Empty))))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (X5 @ (^[Y3 : $i > $i > $i]: (c_Empty)) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty)))) @ (^[Y1 : $i]: (c_Empty)) @ (X4 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ c_Empty) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty))))) @ (^[Y0 : $i]: (Y0))))))),
% 1.65/0.53    inference(flattening,[],[f318])).
% 1.65/0.53  thf(f320,definition,(
% 1.65/0.53    ! [X0 : ($i > $o)] : (? [X1 : $i] : (? [X2 : $i] : ((((X0 @ X2)) != $true) & (((c_In @ X2 @ X1)) = $true)) & (((X0 @ X1)) = $true)) | ~ ($true = ((sP0 @ X0))))),
% 1.65/0.53    introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 1.65/0.53  thf(f326,plain,(
% 1.65/0.53    ! [X0 : ($i > $o)] : (? [X1 : $i] : (? [X2 : $i] : ((((X0 @ X2)) != $true) & (((c_In @ X2 @ X1)) = $true)) & (((X0 @ X1)) = $true)) | ($true != ((sP0 @ X0))))),
% 1.65/0.53    inference(nnf_transformation,[],[f320])).
% 1.65/0.53  thf(f327,plain,(
% 1.65/0.53    ! [X0 : ($i > $o)] : (((($true != ((X0 @ (sK5 @ X0)))) & ($true = ((c_In @ (sK5 @ X0) @ (sK4 @ X0))))) & ($true = ((X0 @ (sK4 @ X0))))) | ($true != ((sP0 @ X0))))),
% 1.65/0.53    inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X2,sK3 @ X0),skolemize(X2,sK3 @ X0)],[f326])).
% 1.65/0.53  thf(f332,plain,(
% 1.65/0.53    ? [X0 : ((($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i) > ($i > $i > ($i > $i) > $i) > $i),X1 : (($i > ((($i > $i) > $i > $i) > $i > $i > $i) > $i) > $i > $i),X2 : (($i > $i > $i) > ($i > $i) > $i > $i > $i > $i),X3 : ((((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i)] : ((c_False != $true) & ! [X4 : $i] : (((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Empty)))))))) = X4) & (((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (X0 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (X2 @ (^[Y7 : $i]: ((^[Y8 : $i]: (Y6 @ Y5)))) @ (^[Y7 : $i]: (Y7)) @ c_Empty @ (Y6 @ (X3 @ (^[Y7 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y7 : $i]: (c_Empty)))) @ (X0 @ (^[Y7 : $i > $i]: ((^[Y8 : ($i > $i > $i) > $i > $i]: ((^[Y9 : $i]: ((^[Y10 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y7 : $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (X1 @ (^[Y10 : $i]: ((^[Y11 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Inj1 @ (X0 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (Y5 @ c_Empty))))))))))))))))))))) = ((X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_setsum @ (X0 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty))))))) @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_setsum @ c_Empty @ c_Empty))))))))) & ! [X5 : ($i > ($i > $i > $i) > $i > $i),X6 : $i,X7 : $i,X8 : ((($i > $i > $i) > $i > $i) > $i)] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y0)))) @ (c_setsum @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))) @ c_Empty)))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (Y3)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (X3 @ (^[Y4 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y4 @ (^[Y5 : $i > $i > $i]: ((^[Y6 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y4 : $i]: (c_Empty)))))))))) @ X6 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (^[Y0 : $i]: (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (X8 @ (^[Y3 : $i > $i > $i]: ((^[Y4 : $i]: (Y2 @ (^[Y5 : $i > $i]: ((^[Y6 : $i]: (X2 @ (^[Y7 : $i]: ((^[Y8 : $i]: (c_Empty)))) @ (^[Y7 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))) @ c_Empty @ (X1 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ c_Empty)) @ (c_Inj0 @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[Y0 : $i]: (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)) @ (^[Y1 : $i]: (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_setsum @ X6 @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ c_Empty)))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ (X0 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))))))) @ X6)) @ (c_setsum @ (c_setsum @ X7 @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (X8 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ (X5 @ c_Empty @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) @ (X5 @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y3 @ (^[Y4 : $i > $i]: ((^[Y5 : $i]: (c_Empty)))) @ c_Empty @ c_Empty)))) @ Y1)))) @ X6))))) & ! [X9 : $i,X10 : ((($i > $i) > $i > $i) > $i),X11 : $i] : (((X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X3 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y2 : $i]: (c_Empty))))) @ (c_setsum @ (c_setsum @ (X0 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))) @ c_Empty) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Inj0 @ c_Empty)))) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty))))))) @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (X10 @ (^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ (c_Inj1 @ c_Empty) @ (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))) @ (c_setsum @ X9 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ X11 @ (c_Inj1 @ X11))))) @ (^[Y0 : $i]: (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))))) @ (c_setsum @ (c_Inj1 @ (X10 @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty)))))) @ (c_setsum @ (X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y0 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y0 : $i]: (c_Inj1 @ c_Empty))) @ (c_setsum @ c_Empty @ c_Empty)))))) & ! [X12 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i),X13 : ((($i > $i > $i) > $i > $i) > $i),X14 : ($i > $i)] : (((X14 @ (c_Inj0 @ c_Empty))) = ((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (Y0)) @ (X14 @ c_Empty) @ (X13 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ (X0 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty)))))))))))) @ c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ (X12 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ c_Empty @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X3 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y1)) @ (^[Y2 : $i]: (c_Inj0 @ c_Empty)))))) @ (^[Y0 : $i]: (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (X13 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (X14 @ c_Empty) @ c_Empty @ (X12 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X14 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X12 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X14 @ (c_Inj1 @ c_Empty))))) & ! [X15 : $i,X16 : ($i > $i)] : (((X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (X2 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ (X0 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_setsum @ c_Empty @ c_Empty)))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (X0 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (c_Empty))))))))))))) @ (X16 @ Y2) @ Y2)))) @ (^[Y1 : $i]: (Y0)) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ (^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty)) @ (X3 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y1 : $i]: (c_Empty))) @ (c_Inj1 @ c_Empty) @ (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (X16 @ c_Empty) @ c_Empty)) @ X15 @ (X0 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (X1 @ (^[Y3 : $i]: ((^[Y4 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ (c_setsum @ c_Empty @ (X16 @ c_Empty)))) = X15) & ! [X17 : $i,X18 : ($i > $i)] : (((X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (X18 @ Y0)))) = ((X18 @ (c_setsum @ (X2 @ (^[Y0 : $i]: ((^[Y1 : $i]: (X1 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (c_setsum @ c_Empty @ c_Empty))))) @ (^[Y0 : $i]: (Y0)) @ X17 @ c_Empty @ c_Empty) @ (X1 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ Y0 @ (X2 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ c_Empty))))) & ! [X19 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i),X20 : ((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i)] : (((c_Inj1 @ c_Empty)) = ((X3 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (X0 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (X1 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (c_Inj1 @ c_Empty))))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (X2 @ (^[Y1 : $i]: ((^[Y2 : $i]: (X20 @ (^[Y3 : $i > $i > $i]: (c_Empty)) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty)))) @ (^[Y1 : $i]: (c_Empty)) @ (X19 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ c_Empty) @ (X1 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty))))) @ (^[Y0 : $i]: (Y0))))))),
% 1.65/0.53    inference(rectify,[],[f319])).
% 1.65/0.53  thf(f333,plain,(
% 1.65/0.53    (c_False != $true) & ! [X4 : $i] : (((sK9 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Empty)))))))) = X4) & (((sK9 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (sK9 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (sK11 @ (^[Y7 : $i]: ((^[Y8 : $i]: (Y6 @ Y5)))) @ (^[Y7 : $i]: (Y7)) @ c_Empty @ (Y6 @ (sK12 @ (^[Y7 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y7 : $i]: (c_Empty)))) @ (sK9 @ (^[Y7 : $i > $i]: ((^[Y8 : ($i > $i > $i) > $i > $i]: ((^[Y9 : $i]: ((^[Y10 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y7 : $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (sK10 @ (^[Y10 : $i]: ((^[Y11 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Inj1 @ (sK9 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (Y5 @ c_Empty))))))))))))))))))))) = ((sK9 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_setsum @ (sK9 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty))))))) @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_setsum @ c_Empty @ c_Empty))))))))) & ! [X5 : ($i > ($i > $i > $i) > $i > $i),X6 : $i,X7 : $i,X8 : ((($i > $i > $i) > $i > $i) > $i)] : (((sK10 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (sK10 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y0)))) @ (c_setsum @ (sK11 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (sK10 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))) @ c_Empty)))) @ (sK11 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (sK9 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (Y3)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (sK12 @ (^[Y4 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y4 @ (^[Y5 : $i > $i > $i]: ((^[Y6 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y4 : $i]: (c_Empty)))))))))) @ X6 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (sK11 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) = ((sK11 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (^[Y0 : $i]: (sK10 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (X8 @ (^[Y3 : $i > $i > $i]: ((^[Y4 : $i]: (Y2 @ (^[Y5 : $i > $i]: ((^[Y6 : $i]: (sK11 @ (^[Y7 : $i]: ((^[Y8 : $i]: (c_Empty)))) @ (^[Y7 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))) @ c_Empty @ (sK10 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ c_Empty)) @ (c_Inj0 @ (sK12 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[Y0 : $i]: (sK12 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)) @ (^[Y1 : $i]: (sK11 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_setsum @ X6 @ (sK10 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ c_Empty)))) @ (sK11 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (sK10 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Inj0 @ (sK9 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))))))) @ X6)) @ (c_setsum @ (c_setsum @ X7 @ (sK11 @ (^[Y0 : $i]: ((^[Y1 : $i]: (Y1)))) @ (^[Y0 : $i]: (X8 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ (X5 @ c_Empty @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (sK12 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (c_Empty))))) @ (X5 @ (sK12 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (sK9 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: (sK10 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y3 @ (^[Y4 : $i > $i]: ((^[Y5 : $i]: (c_Empty)))) @ c_Empty @ c_Empty)))) @ Y1)))) @ X6))))) & ! [X9 : $i,X10 : ((($i > $i) > $i > $i) > $i),X11 : $i] : (((sK10 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (sK11 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (sK12 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y2 : $i]: (c_Empty))))) @ (c_setsum @ (c_setsum @ (sK9 @ (^[Y2 : $i > $i]: ((^[Y3 : ($i > $i > $i) > $i > $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (c_Empty)))))))) @ (^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty))))))) @ c_Empty) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Inj0 @ c_Empty)))) @ (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty))))))) @ (sK11 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (X10 @ (^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ (c_Inj1 @ c_Empty) @ (sK11 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))) @ (c_setsum @ X9 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))) = ((sK11 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_setsum @ X11 @ (c_Inj1 @ X11))))) @ (^[Y0 : $i]: (sK9 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (sK9 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj1 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (sK11 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))))))) @ (c_setsum @ (c_Inj1 @ (X10 @ (^[Y0 : $i > $i]: ((^[Y1 : $i]: (c_Inj1 @ c_Empty)))))) @ (c_setsum @ (sK12 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y0 @ (^[Y1 : $i > $i > $i]: ((^[Y2 : $i > $i]: (c_Empty)))) @ c_Empty @ c_Empty)) @ (^[Y0 : $i]: (c_Inj1 @ c_Empty))) @ (c_setsum @ c_Empty @ c_Empty)))))) & ! [X12 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i),X13 : ((($i > $i > $i) > $i > $i) > $i),X14 : ($i > $i)] : (((X14 @ (c_Inj0 @ c_Empty))) = ((sK11 @ (^[Y0 : $i]: ((^[Y1 : $i]: (sK11 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (Y0)) @ (X14 @ c_Empty) @ (X13 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_setsum @ c_Empty @ (sK9 @ (^[Y4 : $i > $i]: ((^[Y5 : ($i > $i > $i) > $i > $i]: ((^[Y6 : $i]: ((^[Y7 : $i > $i]: (c_Empty)))))))) @ (^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_Empty)))))))))))) @ c_Empty)))) @ (^[Y0 : $i]: (c_Empty)) @ (X12 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_Empty)))))) @ c_Empty @ (sK11 @ (^[Y0 : $i]: ((^[Y1 : $i]: (sK12 @ (^[Y2 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (Y1)) @ (^[Y2 : $i]: (c_Inj0 @ c_Empty)))))) @ (^[Y0 : $i]: (sK12 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (X13 @ (^[Y2 : $i > $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ (^[Y1 : $i]: (c_Inj0 @ c_Empty)))) @ (X14 @ c_Empty) @ c_Empty @ (X12 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X14 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X12 @ (^[Y0 : ($i > $i) > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (c_setsum @ c_Empty @ c_Empty)))))) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X14 @ (c_Inj1 @ c_Empty))))) & ! [X15 : $i,X16 : ($i > $i)] : (((sK11 @ (^[Y0 : $i]: ((^[Y1 : $i]: (c_Empty)))) @ (^[Y0 : $i]: (sK11 @ (^[Y1 : $i]: ((^[Y2 : $i]: (sK11 @ (^[Y3 : $i]: ((^[Y4 : $i]: (c_Empty)))) @ (^[Y3 : $i]: (c_Empty)) @ (sK9 @ (^[Y3 : $i > $i]: ((^[Y4 : ($i > $i > $i) > $i > $i]: ((^[Y5 : $i]: ((^[Y6 : $i > $i]: (c_setsum @ c_Empty @ c_Empty)))))))) @ (^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i > $i]: (sK9 @ (^[Y6 : $i > $i]: ((^[Y7 : ($i > $i > $i) > $i > $i]: ((^[Y8 : $i]: ((^[Y9 : $i > $i]: (c_Empty)))))))) @ (^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i > $i]: (c_Empty))))))))))))) @ (X16 @ Y2) @ Y2)))) @ (^[Y1 : $i]: (Y0)) @ (sK10 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (sK11 @ (^[Y1 : $i]: ((^[Y2 : $i]: (c_Inj1 @ c_Empty)))) @ (^[Y1 : $i]: (sK10 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty)) @ (sK12 @ (^[Y1 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y1 : $i]: (c_Empty))) @ (c_Inj1 @ c_Empty) @ (sK9 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (c_Empty)))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))))) @ (X16 @ c_Empty) @ c_Empty)) @ X15 @ (sK9 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Inj0 @ c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (sK10 @ (^[Y3 : $i]: ((^[Y4 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty))))))))) @ (c_setsum @ c_Empty @ (X16 @ c_Empty)))) = X15) & ! [X17 : $i,X18 : ($i > $i)] : (((sK12 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_Empty)) @ (^[Y0 : $i]: (X18 @ Y0)))) = ((X18 @ (c_setsum @ (sK11 @ (^[Y0 : $i]: ((^[Y1 : $i]: (sK10 @ (^[Y2 : $i]: ((^[Y3 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (c_setsum @ c_Empty @ c_Empty))))) @ (^[Y0 : $i]: (Y0)) @ X17 @ c_Empty @ c_Empty) @ (sK10 @ (^[Y0 : $i]: ((^[Y1 : (($i > $i) > $i > $i) > $i > $i > $i]: (Y1 @ (^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))) @ Y0 @ (sK11 @ (^[Y2 : $i]: ((^[Y3 : $i]: (c_Empty)))) @ (^[Y2 : $i]: (c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ c_Empty))))) & ! [X19 : (((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i),X20 : ((($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i)] : (((c_Inj1 @ c_Empty)) = ((sK12 @ (^[Y0 : (($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]: (c_setsum @ (sK9 @ (^[Y1 : $i > $i]: ((^[Y2 : ($i > $i > $i) > $i > $i]: ((^[Y3 : $i]: ((^[Y4 : $i > $i]: (sK10 @ (^[Y5 : $i]: ((^[Y6 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_setsum @ c_Empty @ c_Empty)))) @ (c_Inj1 @ c_Empty))))))))) @ (^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty))))))) @ (sK10 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ (sK11 @ (^[Y1 : $i]: ((^[Y2 : $i]: (X20 @ (^[Y3 : $i > $i > $i]: (c_Empty)) @ (^[Y3 : $i]: (c_Empty)) @ c_Empty @ c_Empty)))) @ (^[Y1 : $i]: (c_Empty)) @ (X19 @ (^[Y1 : ($i > $i) > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (c_Empty)))))) @ c_Empty) @ (sK10 @ (^[Y1 : $i]: ((^[Y2 : (($i > $i) > $i > $i) > $i > $i > $i]: (c_Empty)))) @ c_Empty) @ (c_Inj0 @ c_Empty))))) @ (^[Y0 : $i]: (Y0)))))),
% 1.65/0.53    inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11,sK12]),skolemize(X0,sK9),skolemize(X1,sK10),skolemize(X2,sK11),skolemize(X3,sK12)],[f332])).
% 1.65/0.53  thf(f338,plain,(
% 1.65/0.53    ($true = ((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 1.65/0.53    inference(cnf_transformation,[],[f120])).
% 1.65/0.53  thf(f339,plain,(
% 1.65/0.53    ( ! [X0 : $i,X1 : $i] : (($true = ((c_iff @ (c_In @ X1 @ (c_Union @ X0)) @ (?? @ $i @ (^[Y0 : $i]: (c_and @ (c_In @ X1 @ Y0) @ (c_In @ Y0 @ X0)))))))) )),
% 1.65/0.53    inference(cnf_transformation,[],[f122])).
% 1.65/0.53  thf(f340,plain,(
% 1.65/0.53    ( ! [X0 : $i,X1 : $i] : ((((c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))) = $true)) )),
% 1.65/0.53    inference(cnf_transformation,[],[f124])).
% 1.65/0.53  thf(f345,plain,(
% 1.65/0.53    ( ! [X0 : ($i > $o)] : (($true = ((X0 @ (sK4 @ X0)))) | ($true != ((sP0 @ X0)))) )),
% 1.65/0.53    inference(cnf_transformation,[],[f327])).
% 1.65/0.53  thf(f347,plain,(
% 1.65/0.53    ( ! [X0 : ($i > $o)] : (($true != ((X0 @ (sK5 @ X0)))) | ($true != ((sP0 @ X0)))) )),
% 1.65/0.53    inference(cnf_transformation,[],[f327])).
% 1.65/0.53  thf(f356,plain,(
% 1.65/0.53    (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 1.65/0.53    inference(cnf_transformation,[],[f136])).
% 1.65/0.53  thf(f357,plain,(
% 1.65/0.53    (c_and = (^[Y0 : $o]: ((^[Y1 : $o]: (!! @ $o @ (^[Y2 : $o]: ((Y0 => (Y1 => Y2)) => Y2)))))))),
% 1.65/0.53    inference(cnf_transformation,[],[f138])).
% 1.65/0.53  thf(f359,plain,(
% 1.65/0.53    (c_iff = (^[Y0 : $o]: ((^[Y1 : $o]: (c_and @ (Y0 => Y1) @ (Y1 => Y0))))))),
% 1.65/0.53    inference(cnf_transformation,[],[f142])).
% 1.65/0.53  thf(f360,plain,(
% 1.65/0.53    (c_Subq = (^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))))),
% 1.65/0.53    inference(cnf_transformation,[],[f144])).
% 1.65/0.53  thf(f459,plain,(
% 1.65/0.53    ( ! [X4 : $i] : ((((sK9 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Empty)))))))) = X4)) )),
% 1.65/0.53    inference(cnf_transformation,[],[f333])).
% 1.65/0.53  thf(f460,plain,(
% 1.65/0.53    (c_False != $true)),
% 1.65/0.53    inference(cnf_transformation,[],[f333])).
% 1.65/0.53  thf(f463,plain,(
% 1.65/0.53    (c_iff = (^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: ((^[Y3 : $o]: (!! @ $o @ (^[Y4 : $o]: ((Y2 => (Y3 => Y4)) => Y4)))))) @ (Y0 => Y1) @ (Y1 => Y0))))))),
% 1.65/0.53    inference(definition_unfolding,[],[f359,f357])).
% 1.65/0.53  thf(f551,plain,(
% 1.65/0.53    ($true = (((^[Y0 : $o]: (Y0 => c_False)) @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 1.65/0.53    inference(definition_unfolding,[],[f338,f356])).
% 1.65/0.53  thf(f552,plain,(
% 1.65/0.53    ( ! [X0 : $i,X1 : $i] : (($true = (((^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: ((^[Y3 : $o]: (!! @ $o @ (^[Y4 : $o]: ((Y2 => (Y3 => Y4)) => Y4)))))) @ (Y0 => Y1) @ (Y1 => Y0))))) @ (c_In @ X1 @ (c_Union @ X0)) @ (?? @ $i @ (^[Y0 : $i]: ((^[Y1 : $o]: ((^[Y2 : $o]: (!! @ $o @ (^[Y3 : $o]: ((Y1 => (Y2 => Y3)) => Y3)))))) @ (c_In @ X1 @ Y0) @ (c_In @ Y0 @ X0)))))))) )),
% 1.65/0.53    inference(definition_unfolding,[],[f339,f463,f357])).
% 1.65/0.53  thf(f553,plain,(
% 1.65/0.53    ( ! [X0 : $i,X1 : $i] : (($true = (((^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: ((^[Y3 : $o]: (!! @ $o @ (^[Y4 : $o]: ((Y2 => (Y3 => Y4)) => Y4)))))) @ (Y0 => Y1) @ (Y1 => Y0))))) @ (c_In @ X1 @ (c_Power @ X0)) @ ((^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))) @ X1 @ X0))))) )),
% 1.65/0.53    inference(definition_unfolding,[],[f340,f463,f360])).
% 1.65/0.53  thf(f562,definition,(
% 1.65/0.53    (sF13 = ((sK9 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Empty)))))))))),
% 1.65/0.53    introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 1.65/0.53  thf(f563,plain,(
% 1.65/0.53    (((sK9 @ (^[Y0 : $i > $i]: ((^[Y1 : ($i > $i > $i) > $i > $i]: ((^[Y2 : $i]: ((^[Y3 : $i > $i]: (c_Empty)))))))) @ (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (c_Empty)))))))) = sF13)),
% 1.65/0.53    inference(reorient_equations,[],[f562])).
% 1.65/0.53  thf(f564,plain,(
% 1.65/0.53    ( ! [X4 : $i] : ((sF13 = X4)) )),
% 1.65/0.53    inference(definition_folding,[],[f459,f563])).
% 1.65/0.53  thf(f811,plain,(
% 1.65/0.53    ( ! [X0 : $i,X1 : $i] : (($true = ((!! @ $o @ (^[Y0 : $o]: ((((c_In @ X1 @ (c_Power @ X0)) => (!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X1) => (c_In @ Y1 @ X0))))) => (((!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X1) => (c_In @ Y1 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))) => Y0)) => Y0)))))) )),
% 1.65/0.53    inference(beta-eta_normalization,[],[f553])).
% 1.65/0.53  thf(f812,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = (((^[Y0 : $o]: ((((c_In @ X1 @ (c_Power @ X0)) => (!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X1) => (c_In @ Y1 @ X0))))) => (((!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X1) => (c_In @ Y1 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))) => Y0)) => Y0)) @ X2)))) )),
% 1.65/0.53    inference(pi_proxy_clausification,[],[f811])).
% 1.65/0.53  thf(f813,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = (((((c_In @ X1 @ (c_Power @ X0)) => (!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0))))) => (((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))) => X2)) => X2)))) )),
% 1.65/0.53    inference(beta-eta_normalization,[],[f812])).
% 1.65/0.53  thf(f814,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = ((((c_In @ X1 @ (c_Power @ X0)) => (!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0))))) => (((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))) => X2)))) | ($true = X2)) )),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f813])).
% 1.65/0.53  thf(f815,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = ((((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))) => X2))) | ($true = X2)) )),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f814])).
% 1.65/0.53  thf(f822,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))))) | ($true = X2)) )),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f815])).
% 1.65/0.53  thf(f823,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0)))))) | ($true = X2) | (((c_In @ X1 @ (c_Power @ X0))) = $true)) )),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f822])).
% 1.65/0.53  thf(f824,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0))) @ (sK115 @ X1 @ X0)))) | ($true = X2) | (((c_In @ X1 @ (c_Power @ X0))) = $true)) )),
% 1.65/0.53    inference(sigma_proxy_clausification,[],[f823])).
% 1.65/0.53  thf(f825,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = (((c_In @ (sK115 @ X1 @ X0) @ X1) => (c_In @ (sK115 @ X1 @ X0) @ X0)))) | ($true = X2) | (((c_In @ X1 @ (c_Power @ X0))) = $true)) )),
% 1.65/0.53    inference(beta-eta_normalization,[],[f824])).
% 1.65/0.53  thf(f827,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = ((c_In @ (sK115 @ X1 @ X0) @ X1))) | ($true = X2) | (((c_In @ X1 @ (c_Power @ X0))) = $true)) )),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f825])).
% 1.65/0.53  thf(f828,plain,(
% 1.65/0.53    ( ! [X0 : $i,X1 : $i] : (($true = ((!! @ $o @ (^[Y0 : $o]: ((((c_In @ X1 @ (c_Union @ X0)) => (?? @ $i @ (^[Y1 : $i]: (!! @ $o @ (^[Y2 : $o]: (((c_In @ X1 @ Y1) => ((c_In @ Y1 @ X0) => Y2)) => Y2)))))) => (((?? @ $i @ (^[Y1 : $i]: (!! @ $o @ (^[Y2 : $o]: (((c_In @ X1 @ Y1) => ((c_In @ Y1 @ X0) => Y2)) => Y2))))) => (c_In @ X1 @ (c_Union @ X0))) => Y0)) => Y0)))))) )),
% 1.65/0.53    inference(beta-eta_normalization,[],[f552])).
% 1.65/0.53  thf(f829,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = (((^[Y0 : $o]: ((((c_In @ X1 @ (c_Union @ X0)) => (?? @ $i @ (^[Y1 : $i]: (!! @ $o @ (^[Y2 : $o]: (((c_In @ X1 @ Y1) => ((c_In @ Y1 @ X0) => Y2)) => Y2)))))) => (((?? @ $i @ (^[Y1 : $i]: (!! @ $o @ (^[Y2 : $o]: (((c_In @ X1 @ Y1) => ((c_In @ Y1 @ X0) => Y2)) => Y2))))) => (c_In @ X1 @ (c_Union @ X0))) => Y0)) => Y0)) @ X2)))) )),
% 1.65/0.53    inference(pi_proxy_clausification,[],[f828])).
% 1.65/0.53  thf(f830,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = (((((c_In @ X1 @ (c_Union @ X0)) => (?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ X1 @ Y0) => ((c_In @ Y0 @ X0) => Y1)) => Y1)))))) => (((?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ X1 @ Y0) => ((c_In @ Y0 @ X0) => Y1)) => Y1))))) => (c_In @ X1 @ (c_Union @ X0))) => X2)) => X2)))) )),
% 1.65/0.53    inference(beta-eta_normalization,[],[f829])).
% 1.65/0.53  thf(f831,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = ((((c_In @ X1 @ (c_Union @ X0)) => (?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ X1 @ Y0) => ((c_In @ Y0 @ X0) => Y1)) => Y1)))))) => (((?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ X1 @ Y0) => ((c_In @ Y0 @ X0) => Y1)) => Y1))))) => (c_In @ X1 @ (c_Union @ X0))) => X2)))) | ($true = X2)) )),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f830])).
% 1.65/0.53  thf(f833,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = (((c_In @ X1 @ (c_Union @ X0)) => (?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ X1 @ Y0) => ((c_In @ Y0 @ X0) => Y1)) => Y1)))))))) | ($true = X2)) )),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f831])).
% 1.65/0.53  thf(f834,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : ((((c_In @ X1 @ (c_Union @ X0))) = $false) | ($true = X2) | ($true = ((?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ X1 @ Y0) => ((c_In @ Y0 @ X0) => Y1)) => Y1)))))))) )),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f833])).
% 1.65/0.53  thf(f835,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : ((((c_In @ X1 @ (c_Union @ X0))) = $false) | ($true = X2) | ($true = (((^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ X1 @ Y0) => ((c_In @ Y0 @ X0) => Y1)) => Y1)))) @ (sK116 @ X1 @ X0))))) )),
% 1.65/0.53    inference(sigma_proxy_clausification,[],[f834])).
% 1.65/0.53  thf(f836,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : ((((c_In @ X1 @ (c_Union @ X0))) = $false) | ($true = X2) | ($true = ((!! @ $o @ (^[Y0 : $o]: (((c_In @ X1 @ (sK116 @ X1 @ X0)) => ((c_In @ (sK116 @ X1 @ X0) @ X0) => Y0)) => Y0)))))) )),
% 1.65/0.53    inference(beta-eta_normalization,[],[f835])).
% 1.65/0.53  thf(f837,plain,(
% 1.65/0.53    ( ! [X2 : $o,X3 : $o,X0 : $i,X1 : $i] : ((((c_In @ X1 @ (c_Union @ X0))) = $false) | ($true = X2) | ($true = (((^[Y0 : $o]: (((c_In @ X1 @ (sK116 @ X1 @ X0)) => ((c_In @ (sK116 @ X1 @ X0) @ X0) => Y0)) => Y0)) @ X3)))) )),
% 1.65/0.53    inference(pi_proxy_clausification,[],[f836])).
% 1.65/0.53  thf(f838,plain,(
% 1.65/0.53    ( ! [X2 : $o,X3 : $o,X0 : $i,X1 : $i] : ((((c_In @ X1 @ (c_Union @ X0))) = $false) | ($true = X2) | ($true = ((((c_In @ X1 @ (sK116 @ X1 @ X0)) => ((c_In @ (sK116 @ X1 @ X0) @ X0) => X3)) => X3)))) )),
% 1.65/0.53    inference(beta-eta_normalization,[],[f837])).
% 1.65/0.53  thf(f839,plain,(
% 1.65/0.53    ( ! [X2 : $o,X3 : $o,X0 : $i,X1 : $i] : ((((c_In @ X1 @ (c_Union @ X0))) = $false) | ($true = X2) | ($false = (((c_In @ X1 @ (sK116 @ X1 @ X0)) => ((c_In @ (sK116 @ X1 @ X0) @ X0) => X3)))) | ($true = X3)) )),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f838])).
% 1.65/0.53  thf(f840,plain,(
% 1.65/0.53    ( ! [X2 : $o,X3 : $o,X0 : $i,X1 : $i] : ((((c_In @ X1 @ (c_Union @ X0))) = $false) | ($true = X2) | ($false = (((c_In @ (sK116 @ X1 @ X0) @ X0) => X3))) | ($true = X3)) )),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f839])).
% 1.65/0.53  thf(f843,plain,(
% 1.65/0.53    ( ! [X2 : $o,X3 : $o,X0 : $i,X1 : $i] : ((((c_In @ X1 @ (c_Union @ X0))) = $false) | ($true = X2) | ($true = ((c_In @ (sK116 @ X1 @ X0) @ X0))) | ($true = X3)) )),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f840])).
% 1.65/0.53  thf(f855,plain,(
% 1.65/0.53    ($true = (((?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))) => c_False)))),
% 1.65/0.53    inference(beta-eta_normalization,[],[f551])).
% 1.65/0.53  thf(f856,plain,(
% 1.65/0.53    (((?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty)))) = $false) | (c_False = $true)),
% 1.65/0.53    inference(imp_proxy_clausification,[],[f855])).
% 1.65/0.53  thf(f857,plain,(
% 1.65/0.53    ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (c_In @ Y0 @ c_Empty)) @ X1))) | (c_False = $true)) )),
% 1.65/0.53    inference(pi_proxy_clausification,[],[f856])).
% 1.65/0.53  thf(f858,plain,(
% 1.65/0.53    ( ! [X1 : $i] : (($false = ((c_In @ X1 @ c_Empty))) | (c_False = $true)) )),
% 1.65/0.53    inference(beta-eta_normalization,[],[f857])).
% 1.65/0.53  thf(f977,definition,(
% 1.65/0.53    spl122_6 <=> ! [X1 : $o] : ($true = X1)),
% 1.65/0.53    introduced(definition,[new_symbols(definition,[spl122_6])],[avatar_definition])).
% 1.65/0.53  thf(f978,plain,(
% 1.65/0.53    ( ! [X1 : $o] : (($true = X1)) ) | ~spl122_6),
% 1.65/0.53    inference(avatar_component_clause,[],[f977])).
% 1.65/0.53  thf(f991,plain,(
% 1.65/0.53    ( ! [X0 : ($i > $o)] : (($true = ((X0 @ sF13))) | ($true != ((sP0 @ X0)))) )),
% 1.65/0.53    inference(forward_demodulation,[],[f345,f564])).
% 1.65/0.53  thf(f993,plain,(
% 1.65/0.53    ( ! [X0 : ($i > $o)] : (($true != ((X0 @ sF13))) | ($true != ((sP0 @ X0)))) )),
% 1.65/0.53    inference(forward_demodulation,[],[f347,f564])).
% 1.65/0.53  thf(f1004,plain,(
% 1.65/0.53    ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = ((c_In @ sF13 @ X1))) | ($true = X2) | (((c_In @ X1 @ (c_Power @ X0))) = $true)) )),
% 1.65/0.53    inference(forward_demodulation,[],[f827,f564])).
% 1.65/0.53  thf(f1007,plain,(
% 1.65/0.53    ( ! [X2 : $o,X3 : $o,X0 : $i,X1 : $i] : (($false = ((c_In @ X1 @ sF13))) | ($true = X2) | ($true = ((c_In @ (sK116 @ X1 @ X0) @ X0))) | ($true = X3)) )),
% 1.65/0.53    inference(forward_demodulation,[],[f843,f564])).
% 1.65/0.53  thf(f1011,plain,(
% 1.65/0.53    ( ! [X1 : $i] : (($false = ((c_In @ X1 @ c_Empty)))) )),
% 1.65/0.53    inference(forward_subsumption_resolution,[],[f858,f460])).
% 1.65/0.53  thf(f1119,plain,(
% 1.65/0.53    ( ! [X0 : ($i > $o)] : (($true != ((sP0 @ X0)))) )),
% 1.65/0.53    inference(forward_subsumption_resolution,[],[f993,f991])).
% 1.65/0.53  thf(f1124,definition,(
% 1.65/0.53    spl122_8 <=> ! [X2 : $i] : ($false = ((c_In @ X2 @ sF13)))),
% 1.65/0.53    introduced(definition,[new_symbols(definition,[spl122_8])],[avatar_definition])).
% 1.65/0.53  thf(f1125,plain,(
% 1.65/0.53    ( ! [X2 : $i] : (($false = ((c_In @ X2 @ sF13)))) ) | ~spl122_8),
% 1.65/0.53    inference(avatar_component_clause,[],[f1124])).
% 1.65/0.53  thf(f1136,plain,(
% 1.65/0.53    ( ! [X2 : $o,X1 : $i] : (($true = ((c_In @ X1 @ sF13))) | ($true = ((c_In @ sF13 @ X1))) | ($true = X2)) )),
% 1.65/0.53    inference(forward_demodulation,[],[f1004,f564])).
% 1.65/0.53  thf(f1139,plain,(
% 1.65/0.53    ( ! [X2 : $o,X3 : $o,X0 : $i,X1 : $i] : (($true = ((c_In @ sF13 @ X0))) | ($false = ((c_In @ X1 @ sF13))) | ($true = X2) | ($true = X3)) )),
% 1.65/0.53    inference(forward_demodulation,[],[f1007,f564])).
% 1.65/0.53  thf(f1161,definition,(
% 1.65/0.53    spl122_13 <=> ! [X0 : ($i > $o)] : ($true != ((sP0 @ X0)))),
% 1.65/0.53    introduced(definition,[new_symbols(definition,[spl122_13])],[avatar_definition])).
% 1.65/0.53  thf(f1162,plain,(
% 1.65/0.53    ( ! [X0 : ($i > $o)] : (($true != ((sP0 @ X0)))) ) | ~spl122_13),
% 1.65/0.53    inference(avatar_component_clause,[],[f1161])).
% 1.65/0.53  thf(f1168,plain,(
% 1.65/0.53    spl122_13),
% 1.65/0.53    inference(avatar_split_clause,[],[f1119,f1161])).
% 1.65/0.53  thf(f1170,definition,(
% 1.65/0.53    spl122_15 <=> ! [X0 : $i] : ($true = ((c_In @ sF13 @ X0)))),
% 1.65/0.53    introduced(definition,[new_symbols(definition,[spl122_15])],[avatar_definition])).
% 1.65/0.53  thf(f1171,plain,(
% 1.65/0.53    ( ! [X0 : $i] : (($true = ((c_In @ sF13 @ X0)))) ) | ~spl122_15),
% 1.65/0.53    inference(avatar_component_clause,[],[f1170])).
% 1.65/0.53  thf(f1175,definition,(
% 1.65/0.53    spl122_16 <=> ! [X1 : $i] : (($true = ((c_In @ X1 @ sF13))) | ($true = ((c_In @ sF13 @ X1))))),
% 1.65/0.53    introduced(definition,[new_symbols(definition,[spl122_16])],[avatar_definition])).
% 1.65/0.53  thf(f1176,plain,(
% 1.65/0.53    ( ! [X1 : $i] : (($true = ((c_In @ X1 @ sF13))) | ($true = ((c_In @ sF13 @ X1)))) ) | ~spl122_16),
% 1.65/0.53    inference(avatar_component_clause,[],[f1175])).
% 1.65/0.53  thf(f1177,plain,(
% 1.65/0.53    spl122_6 | spl122_16),
% 1.65/0.53    inference(avatar_split_clause,[],[f1136,f1175,f977])).
% 1.65/0.53  thf(f1189,plain,(
% 1.65/0.53    spl122_6 | spl122_6 | spl122_8 | spl122_15),
% 1.65/0.53    inference(avatar_split_clause,[],[f1139,f1170,f1124,f977,f977])).
% 1.65/0.53  thf(f1194,plain,(
% 1.65/0.53    $false | (~spl122_6 | ~spl122_13)),
% 1.65/0.53    inference(forward_subsumption_resolution,[],[f1162,f978])).
% 1.65/0.53  thf(f1195,plain,(
% 1.65/0.53    ~spl122_6 | ~spl122_13),
% 1.65/0.53    inference(avatar_contradiction_clause,[],[f1194])).
% 1.65/0.53  thf(f1202,plain,(
% 1.65/0.53    ( ! [X1 : $i] : (($true = $false) | ($true = ((c_In @ sF13 @ X1)))) ) | (~spl122_8 | ~spl122_16)),
% 1.65/0.53    inference(forward_demodulation,[],[f1176,f1125])).
% 1.65/0.53  thf(f1217,plain,(
% 1.65/0.53    ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) )),
% 1.65/0.53    inference(constrained_superposition,[],[f564,f564])).
% 1.65/0.53  thf(f1224,plain,(
% 1.65/0.53    ( ! [X0 : $i,X1 : $i] : ((((c_In @ X1 @ X0)) = $false)) )),
% 1.65/0.53    inference(constrained_superposition,[],[f1011,f1217])).
% 1.65/0.53  thf(f1225,plain,(
% 1.65/0.53    ( ! [X0 : $i,X1 : $i] : ((((c_In @ X0 @ X1)) = $true)) ) | ~spl122_15),
% 1.65/0.53    inference(constrained_superposition,[],[f1171,f564])).
% 1.65/0.53  thf(f1240,plain,(
% 1.65/0.53    ($true = $false) | ~spl122_15),
% 1.65/0.53    inference(forward_demodulation,[],[f1225,f1224])).
% 1.65/0.53  thf(f1241,plain,(
% 1.65/0.53    $false | ~spl122_15),
% 1.65/0.53    inference(trivial_inequality_removal,[],[f1240])).
% 1.65/0.53  thf(f1242,plain,(
% 1.65/0.53    ~spl122_15),
% 1.65/0.53    inference(avatar_contradiction_clause,[],[f1241])).
% 1.65/0.53  thf(f1246,plain,(
% 1.65/0.53    ( ! [X1 : $i] : (($true = ((c_In @ sF13 @ X1)))) ) | (~spl122_8 | ~spl122_16)),
% 1.65/0.53    inference(trivial_inequality_removal,[],[f1202])).
% 1.65/0.53  thf(f1249,plain,(
% 1.65/0.53    ($true = $false) | (~spl122_8 | ~spl122_16)),
% 1.65/0.53    inference(forward_demodulation,[],[f1246,f1224])).
% 1.65/0.53  thf(f1250,plain,(
% 1.65/0.53    $false | (~spl122_8 | ~spl122_16)),
% 1.65/0.53    inference(trivial_inequality_removal,[],[f1249])).
% 1.65/0.53  thf(f1251,plain,(
% 1.65/0.53    ~spl122_8 | ~spl122_16),
% 1.65/0.53    inference(avatar_contradiction_clause,[],[f1250])).
% 1.65/0.53  cnf(s18, plain, spl122_13, inference(sat_conversion,[],[f1168])).
% 1.65/0.53  cnf(s21, plain, spl122_6 | spl122_16, inference(sat_conversion,[],[f1177])).
% 1.65/0.53  cnf(s25, plain, spl122_6 | spl122_6 | spl122_8 | spl122_15, inference(sat_conversion,[],[f1189])).
% 1.65/0.53  cnf(s26, plain, spl122_6 | spl122_8 | spl122_15, inference(rat,[],[s25])).
% 1.65/0.53  cnf(s28, plain, ~spl122_6 | ~spl122_13, inference(sat_conversion,[],[f1195])).
% 1.65/0.53  cnf(s36, plain, ~spl122_15, inference(sat_conversion,[],[f1242])).
% 1.65/0.53  cnf(s37, plain, ~spl122_8 | ~spl122_16, inference(sat_conversion,[],[f1251])).
% 1.65/0.53  cnf(s39, plain, spl122_6 | spl122_8, inference(rat,[],[s26,s36])).
% 1.65/0.53  cnf(s41, plain, ~spl122_6, inference(rat,[],[s28,s18])).
% 1.65/0.53  cnf(s43, plain, spl122_8, inference(rat,[],[s39,s41])).
% 1.65/0.53  cnf(s45, plain, spl122_16, inference(rat,[],[s21,s41])).
% 1.65/0.53  cnf(s46, plain, $false, inference(rat,[],[s37,s45,s43])).
% 1.65/0.53  thf(f1255,plain,(
% 1.65/0.53    $false),
% 1.65/0.53    inference(avatar_sat_refutation,[],[s46])).
% 1.65/0.53  % SZS output end Proof for theBenchmark
% 1.65/0.53  % (3673162)------------------------------
% 1.65/0.53  % (3673162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.53  % (3673162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.53  % (3673162)CaDiCaL version: 2.1.3
% 1.65/0.53  % (3673162)Termination reason: Refutation
% 1.65/0.53  % (3673162)Time elapsed: 0.097 s
% 1.65/0.53  % (3673162)Peak memory usage: 14 MB
% 1.65/0.53  % (3673162)Instructions burned: 433 (million)
% 1.65/0.53  % (3673132)Success in time 0.285 s
% 1.65/0.53  % Vampire exiting
%------------------------------------------------------------------------------