%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU679^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:32:57 AM UTC 2026
% Result : Theorem 2.51s 0.58s
% Output : Refutation 2.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU679^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n013.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 14:07:22 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.51/0.58 % (2173032)Will run a generic schedule for satisfiability detection.
% 2.51/0.58 % (2173038)% WARNING: option uhcvi not known.
% 2.51/0.58 % (2173038)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3787590081:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.51/0.58 % (2173038)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.51/0.58 % (2173038)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.51/0.58 % (2173040)dis+10_1_sil=32000:sp=arity:random_seed=187095625:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.51/0.58 % (2173037)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4183097650_2999 on theBenchmark for (2999ds/0Mi)
% 2.51/0.58 % (2173041)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1869054502:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.51/0.58 % (2173039)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=878626017:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.51/0.58 % (2173042)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2194400166:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.51/0.58 % (2173043)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4169937760:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.51/0.58 % (2173041)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.51/0.58 % Exception at run slice level
% 2.51/0.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.51/0.58 % (2173051)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=574742422:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.51/0.58 % Exception at run slice level
% 2.51/0.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.51/0.58 % (2173053)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2359791735:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.51/0.58 % (2173040)Instruction limit reached!
% 2.51/0.58 % (2173040)------------------------------
% 2.51/0.58 % (2173040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.58 % (2173040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.58 % (2173040)CaDiCaL version: 2.1.3
% 2.51/0.58 % (2173040)Termination reason: Instruction limit
% 2.51/0.58 % (2173040)Termination phase: Saturation
% 2.51/0.58 % (2173040)Time elapsed: 0.052 s
% 2.51/0.58 % (2173040)Peak memory usage: 12 MB
% 2.51/0.58 % (2173040)Instructions burned: 104 (million)
% 2.51/0.58 % (2173041)Instruction limit reached!
% 2.51/0.58 % (2173041)------------------------------
% 2.51/0.58 % (2173041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.58 % (2173041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.58 % (2173041)CaDiCaL version: 2.1.3
% 2.51/0.58 % (2173041)Termination reason: Instruction limit
% 2.51/0.58 % (2173041)Termination phase: Saturation
% 2.51/0.58 % (2173041)Time elapsed: 0.059 s
% 2.51/0.58 % (2173041)Peak memory usage: 12 MB
% 2.51/0.58 % (2173041)Instructions burned: 116 (million)
% 2.51/0.58 % (2173042)Instruction limit reached!
% 2.51/0.58 % (2173042)------------------------------
% 2.51/0.58 % (2173042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.58 % (2173042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.58 % (2173042)CaDiCaL version: 2.1.3
% 2.51/0.58 % (2173042)Termination reason: Instruction limit
% 2.51/0.58 % (2173042)Termination phase: Saturation
% 2.51/0.58 % (2173042)Time elapsed: 0.068 s
% 2.51/0.58 % (2173042)Peak memory usage: 13 MB
% 2.51/0.58 % (2173042)Instructions burned: 131 (million)
% 2.51/0.58 % (2173055)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=1836294033:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 2.51/0.58 % (2173055)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.51/0.58 % (2173055)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.51/0.58 % (2173056)ott-21_1_sil=16000:fs=off:random_seed=2548660924:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 2.51/0.58 % (2173043)Instruction limit reached!
% 2.51/0.58 % (2173043)------------------------------
% 2.51/0.58 % (2173043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.58 % (2173043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.58 % (2173043)CaDiCaL version: 2.1.3
% 2.51/0.58 % (2173043)Termination reason: Instruction limit
% 2.51/0.58 % (2173043)Termination phase: Saturation
% 2.51/0.58 % (2173043)Time elapsed: 0.083 s
% 2.51/0.58 % (2173043)Peak memory usage: 12 MB
% 2.51/0.58 % (2173043)Instructions burned: 159 (million)
% 2.51/0.58 % (2173057)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1959194592:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 2.51/0.58 % (2173060)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2684768750:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 2.51/0.58 % Exception at run slice level
% 2.51/0.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.51/0.58 % (2173053)Instruction limit reached!
% 2.51/0.58 % (2173053)------------------------------
% 2.51/0.58 % (2173053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.58 % (2173053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.58 % (2173053)CaDiCaL version: 2.1.3
% 2.51/0.58 % (2173053)Termination reason: Instruction limit
% 2.51/0.58 % (2173053)Termination phase: Saturation
% 2.51/0.58 % (2173053)Time elapsed: 0.069 s
% 2.51/0.58 % (2173053)Peak memory usage: 13 MB
% 2.51/0.58 % (2173053)Instructions burned: 131 (million)
% 2.51/0.58 % (2173063)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3409816630:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 2.51/0.58 % (2173064)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=653397778:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 2.51/0.58 % Exception at run slice level
% 2.51/0.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.51/0.58 % (2173067)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=113769628:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 2.51/0.58 % (2173067)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.51/0.58 % (2173056)Instruction limit reached!
% 2.51/0.58 % (2173056)------------------------------
% 2.51/0.58 % (2173056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.58 % (2173056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.58 % (2173056)CaDiCaL version: 2.1.3
% 2.51/0.58 % (2173056)Termination reason: Instruction limit
% 2.51/0.58 % (2173056)Termination phase: Saturation
% 2.51/0.58 % (2173056)Time elapsed: 0.084 s
% 2.51/0.58 % (2173056)Peak memory usage: 12 MB
% 2.51/0.58 % (2173056)Instructions burned: 182 (million)
% 2.51/0.58 % (2173069)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=764920013:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 2.51/0.58 % (2173069)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.51/0.58 % (2173038) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2173032-2173038"...
% 2.51/0.58 % (2173038)...printing done.
% 2.51/0.58 % (2173038)Refutation found. Thanks to Tanya!
% 2.51/0.58 % SZS status Theorem for theBenchmark
% 2.51/0.58 % SZS output start Proof for theBenchmark
% 2.51/0.58 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 2.51/0.58 thf(func_def_0, type, in: ($i > $i > $o)).
% 2.51/0.58 thf(func_def_2, type, setadjoin: ($i > $i > $i)).
% 2.51/0.58 thf(func_def_3, type, dsetconstr: ($i > ($i > $o) > $i)).
% 2.51/0.58 thf(func_def_4, type, subset: ($i > $i > $o)).
% 2.51/0.58 thf(func_def_5, type, kpair: ($i > $i > $i)).
% 2.51/0.58 thf(func_def_6, type, cartprod: ($i > $i > $i)).
% 2.51/0.58 thf(func_def_7, type, singleton: ($i > $o)).
% 2.51/0.58 thf(func_def_9, type, ex1: ($i > ($i > $o) > $o)).
% 2.51/0.58 thf(func_def_10, type, breln: ($i > $i > $i > $o)).
% 2.51/0.58 thf(func_def_11, type, dpsetconstr: ($i > $i > ($i > $i > $o) > $i)).
% 2.51/0.58 thf(func_def_12, type, func: ($i > $i > $i > $o)).
% 2.51/0.58 thf(func_def_13, type, lamProp: $o).
% 2.51/0.58 thf(func_def_14, type, lam: ($i > $i > ($i > $i) > $i)).
% 2.51/0.58 thf(func_def_15, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.51/0.58 thf(func_def_16, type, vAND: ($o > $o > $o)).
% 2.51/0.58 thf(func_def_17, type, db0: !>[X0: $tType]:(X0)).
% 2.51/0.58 thf(func_def_18, type, db1: !>[X0: $tType]:(X0)).
% 2.51/0.58 thf(func_def_19, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.51/0.58 thf(func_def_20, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 2.51/0.58 thf(func_def_21, type, db2: !>[X0: $tType]:(X0)).
% 2.51/0.58 thf(func_def_22, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.51/0.58 thf(func_def_23, type, vIMP: ($o > $o > $o)).
% 2.51/0.58 thf(func_def_24, type, db3: !>[X0: $tType]:(X0)).
% 2.51/0.58 thf(func_def_25, type, db4: !>[X0: $tType]:(X0)).
% 2.51/0.58 thf(func_def_30, type, sK2: ($i > $i)).
% 2.51/0.58 thf(func_def_31, type, vNOT: ($o > $o)).
% 2.51/0.58 thf(func_def_33, type, db5: !>[X0: $tType]:(X0)).
% 2.51/0.58 thf(func_def_34, type, sK4: ($i > ($i > $i) > $i > $i)).
% 2.51/0.58 thf(func_def_35, type, sK5: (($i > $i) > $i > $i > $i > $i)).
% 2.51/0.58 thf(func_def_36, type, sK6: (($i > $i) > $i > $i > $i > $i)).
% 2.51/0.58 thf(func_def_38, type, sK8: ($i > $i > ($i > $i > $i) > $i > ($i > $i) > ($i > $i) > $i > ($i > $i > $i) > $i)).
% 2.51/0.58 thf(func_def_39, type, sK9: ($i > $i > ($i > $i > $i) > $i > ($i > $i) > ($i > $i) > $i > ($i > $i > $i) > $i)).
% 2.51/0.58 thf(func_def_40, type, sK10: ($i > $i > ($i > $i > $i) > $i > ($i > $i) > ($i > $i) > $i > ($i > $i > $i) > $i)).
% 2.51/0.58 thf(func_def_41, type, sK11: ($i > $i > ($i > $i > $i) > $i > ($i > $i) > ($i > $i) > $i > ($i > $i > $i) > $i)).
% 2.51/0.58 thf(func_def_42, type, sK12: ($i > $i > $i)).
% 2.51/0.58 thf(func_def_43, type, sK13: ($i > $i > $i)).
% 2.51/0.58 thf(func_def_44, type, sK14: (($i > $i) > $i)).
% 2.51/0.58 thf(func_def_45, type, sK15: (($i > $i) > $i)).
% 2.51/0.58 thf(func_def_46, type, sK16: (($i > $i) > $i)).
% 2.51/0.58 thf(func_def_47, type, sK17: ($i > $i)).
% 2.51/0.58 thf(func_def_48, type, sK18: (($i > $i) > $i)).
% 2.51/0.58 thf(func_def_49, type, sK19: ($i > $i)).
% 2.51/0.58 thf(func_def_50, type, sK20: (($i > $i) > $i)).
% 2.51/0.58 thf(func_def_51, type, sK21: (($i > $i) > $i)).
% 2.51/0.58 thf(func_def_52, type, sK22: (($i > $i) > ($i > $i) > $i)).
% 2.51/0.58 thf(func_def_53, type, sK23: ($i > $i)).
% 2.51/0.58 thf(func_def_54, type, sK24: (($i > $i) > ($i > $i) > $i)).
% 2.51/0.58 thf(func_def_55, type, sK25: (($i > $i) > ($i > $i) > $i)).
% 2.51/0.58 thf(func_def_56, type, sK26: (($i > $i) > ($i > $i) > $i)).
% 2.51/0.58 thf(f1,axiom,(
% 2.51/0.58 (singleton = (^[X0 : $i] : (? [X1 : $i] : ((X0 = ((setadjoin @ X1 @ emptyset))) & (in @ X1 @ X0)))))),
% 2.51/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton)).
% 2.51/0.58 thf(f2,axiom,(
% 2.51/0.58 (ex1 = (^[X0 : $i, X1 : ($i > $o)] : ((singleton @ (dsetconstr @ X0 @ (^[X2 : $i] : ((X1 @ X2))))))))),
% 2.51/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ex1)).
% 2.51/0.58 thf(f3,axiom,(
% 2.51/0.58 (breln = (^[X0 : $i, X1 : $i, X2 : $i] : ((subset @ X2 @ (cartprod @ X0 @ X1)))))),
% 2.51/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p',breln)).
% 2.51/0.58 thf(f4,axiom,(
% 2.51/0.58 (func = (^[X0 : $i, X1 : $i, X2 : $i] : (! [X3 : $i] : ((in @ X3 @ X0) => (ex1 @ X1 @ (^[X4 : $i] : ((in @ (kpair @ X3 @ X4) @ X2))))) & (breln @ X0 @ X1 @ X2))))),
% 2.51/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p',func)).
% 2.51/0.58 thf(f5,axiom,(
% 2.51/0.58 (lamProp = ! [X0 : $i,X1 : $i,X2 : ($i > $i)] : (! [X3 : $i] : ((in @ X3 @ X0) => (in @ (X2 @ X3) @ X1)) => (func @ X0 @ X1 @ (dpsetconstr @ X0 @ X1 @ (^[X3 : $i, X4 : $i] : ((((X2 @ X3)) = X4)))))))),
% 2.51/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p',lamProp)).
% 2.51/0.58 thf(f6,axiom,(
% 2.51/0.58 (lam = (^[X0 : $i, X1 : $i, X2 : ($i > $i)] : ((dpsetconstr @ X0 @ X1 @ (^[X3 : $i, X4 : $i] : ((((X2 @ X3)) = X4)))))))),
% 2.51/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p',lam)).
% 2.51/0.58 thf(f7,conjecture,(
% 2.51/0.58 lamProp => ! [X0 : $i,X1 : $i,X2 : ($i > $i)] : (! [X3 : $i] : ((in @ X3 @ X0) => (in @ (X2 @ X3) @ X1)) => (func @ X0 @ X1 @ (lam @ X0 @ X1 @ (^[X3 : $i] : ((X2 @ X3))))))),
% 2.51/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p',lamp)).
% 2.51/0.58 thf(f8,negated_conjecture,(
% 2.51/0.58 ~(lamProp => ! [X0 : $i,X1 : $i,X2 : ($i > $i)] : (! [X3 : $i] : ((in @ X3 @ X0) => (in @ (X2 @ X3) @ X1)) => (func @ X0 @ X1 @ (lam @ X0 @ X1 @ (^[X3 : $i] : ((X2 @ X3)))))))),
% 2.51/0.58 inference(negated_conjecture,[status(cth)],[f7])).
% 2.51/0.58 thf(f9,plain,(
% 2.51/0.58 (singleton = (^[X0 : $i] : (? [X1 : $i] : ((X0 = ((setadjoin @ X1 @ emptyset))) & (in @ X1 @ X0)))))),
% 2.51/0.58 inference(rectify,[],[f1])).
% 2.51/0.58 thf(f10,plain,(
% 2.51/0.58 (singleton = (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) & ((setadjoin @ Y1 @ emptyset) = Y0))))))),
% 2.51/0.58 inference(fool_elimination,[],[f9])).
% 2.51/0.58 thf(f11,plain,(
% 2.51/0.58 (ex1 = (^[X0 : $i, X1 : ($i > $o)] : ((singleton @ (dsetconstr @ X0 @ (^[X2 : $i] : ((X1 @ X2))))))))),
% 2.51/0.58 inference(rectify,[],[f2])).
% 2.51/0.58 thf(f12,plain,(
% 2.51/0.58 (ex1 = (^[Y0 : $i]: ((^[Y1 : $i > $o]: (singleton @ (dsetconstr @ Y0 @ (^[Y2 : $i]: (Y1 @ Y2))))))))),
% 2.51/0.58 inference(fool_elimination,[],[f11])).
% 2.51/0.58 thf(f13,plain,(
% 2.51/0.58 (breln = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (subset @ Y2 @ (cartprod @ Y0 @ Y1))))))))),
% 2.51/0.58 inference(fool_elimination,[],[f3])).
% 2.51/0.58 thf(f14,plain,(
% 2.51/0.58 (func = (^[X0 : $i, X1 : $i, X2 : $i] : (! [X3 : $i] : ((in @ X3 @ X0) => (ex1 @ X1 @ (^[X4 : $i] : ((in @ (kpair @ X3 @ X4) @ X2))))) & (breln @ X0 @ X1 @ X2))))),
% 2.51/0.58 inference(rectify,[],[f4])).
% 2.51/0.58 thf(f15,plain,(
% 2.51/0.58 (func = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((breln @ Y0 @ Y1 @ Y2) & (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y0) => (ex1 @ Y1 @ (^[Y4 : $i]: (in @ (kpair @ Y3 @ Y4) @ Y2)))))))))))))),
% 2.51/0.58 inference(fool_elimination,[],[f14])).
% 2.51/0.58 thf(f16,plain,(
% 2.51/0.58 (lamProp = ! [X0 : $i,X1 : $i,X2 : ($i > $i)] : (! [X3 : $i] : ((in @ X3 @ X0) => (in @ (X2 @ X3) @ X1)) => (func @ X0 @ X1 @ (dpsetconstr @ X0 @ X1 @ (^[X4 : $i, X5 : $i] : ((((X2 @ X4)) = X5)))))))),
% 2.51/0.58 inference(rectify,[],[f5])).
% 2.51/0.58 thf(f17,plain,(
% 2.51/0.58 (lamProp = ((!! @ ($i > $i) @ (^[Y0 : $i > $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y2) => (in @ (Y0 @ Y3) @ Y1)))) => (func @ Y2 @ Y1 @ (dpsetconstr @ Y2 @ Y1 @ (^[Y3 : $i]: ((^[Y4 : $i]: ((Y0 @ Y3) = Y4)))))))))))))))),
% 2.51/0.58 inference(fool_elimination,[],[f16])).
% 2.51/0.58 thf(f18,plain,(
% 2.51/0.58 (lam = (^[X0 : $i, X1 : $i, X2 : ($i > $i)] : ((dpsetconstr @ X0 @ X1 @ (^[X3 : $i, X4 : $i] : ((((X2 @ X3)) = X4)))))))),
% 2.51/0.58 inference(rectify,[],[f6])).
% 2.51/0.58 thf(f19,plain,(
% 2.51/0.58 (lam = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (dpsetconstr @ Y0 @ Y1 @ (^[Y3 : $i]: ((^[Y4 : $i]: ((Y2 @ Y3) = Y4)))))))))))),
% 2.51/0.58 inference(fool_elimination,[],[f18])).
% 2.51/0.58 thf(f20,plain,(
% 2.51/0.58 ~(lamProp => ! [X0 : $i,X1 : $i,X2 : ($i > $i)] : (! [X3 : $i] : ((in @ X3 @ X0) => (in @ (X2 @ X3) @ X1)) => (func @ X0 @ X1 @ (lam @ X0 @ X1 @ (^[X4 : $i] : ((X2 @ X4)))))))),
% 2.51/0.58 inference(rectify,[],[f8])).
% 2.51/0.58 thf(f21,plain,(
% 2.51/0.58 ~((lamProp = $true) => ! [X0 : $i,X1 : $i,X2 : ($i > $i)] : (! [X3 : $i] : ((((in @ X3 @ X0)) = $true) => (((in @ (X2 @ X3) @ X1)) = $true)) => ($true = ((func @ X0 @ X1 @ (lam @ X0 @ X1 @ (^[Y0 : $i]: (X2 @ Y0))))))))),
% 2.51/0.58 inference(fool_elimination,[],[f20])).
% 2.51/0.58 thf(f22,plain,(
% 2.51/0.58 ? [X0 : $i,X1 : $i,X2 : ($i > $i)] : (($true != ((func @ X0 @ X1 @ (lam @ X0 @ X1 @ (^[Y0 : $i]: (X2 @ Y0)))))) & ! [X3 : $i] : ((((in @ (X2 @ X3) @ X1)) = $true) | (((in @ X3 @ X0)) != $true))) & (lamProp = $true)),
% 2.51/0.58 inference(ennf_transformation,[],[f21])).
% 2.51/0.58 thf(f23,plain,(
% 2.51/0.58 (($true != ((func @ sK0 @ sK1 @ (lam @ sK0 @ sK1 @ (^[Y0 : $i]: (sK2 @ Y0)))))) & ! [X3 : $i] : (($true = ((in @ (sK2 @ X3) @ sK1))) | ($true != ((in @ X3 @ sK0))))) & (lamProp = $true)),
% 2.51/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f22])).
% 2.51/0.58 thf(f24,plain,(
% 2.51/0.58 (singleton = (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) & ((setadjoin @ Y1 @ emptyset) = Y0))))))),
% 2.51/0.58 inference(cnf_transformation,[],[f10])).
% 2.51/0.58 thf(f25,plain,(
% 2.51/0.58 (ex1 = (^[Y0 : $i]: ((^[Y1 : $i > $o]: (singleton @ (dsetconstr @ Y0 @ (^[Y2 : $i]: (Y1 @ Y2))))))))),
% 2.51/0.58 inference(cnf_transformation,[],[f12])).
% 2.51/0.58 thf(f26,plain,(
% 2.51/0.58 (breln = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (subset @ Y2 @ (cartprod @ Y0 @ Y1))))))))),
% 2.51/0.58 inference(cnf_transformation,[],[f13])).
% 2.51/0.58 thf(f27,plain,(
% 2.51/0.58 (func = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((breln @ Y0 @ Y1 @ Y2) & (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y0) => (ex1 @ Y1 @ (^[Y4 : $i]: (in @ (kpair @ Y3 @ Y4) @ Y2)))))))))))))),
% 2.51/0.58 inference(cnf_transformation,[],[f15])).
% 2.51/0.58 thf(f28,plain,(
% 2.51/0.58 (lamProp = ((!! @ ($i > $i) @ (^[Y0 : $i > $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y2) => (in @ (Y0 @ Y3) @ Y1)))) => (func @ Y2 @ Y1 @ (dpsetconstr @ Y2 @ Y1 @ (^[Y3 : $i]: ((^[Y4 : $i]: ((Y0 @ Y3) = Y4)))))))))))))))),
% 2.51/0.58 inference(cnf_transformation,[],[f17])).
% 2.51/0.58 thf(f29,plain,(
% 2.51/0.58 (lam = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (dpsetconstr @ Y0 @ Y1 @ (^[Y3 : $i]: ((^[Y4 : $i]: ((Y2 @ Y3) = Y4)))))))))))),
% 2.51/0.58 inference(cnf_transformation,[],[f19])).
% 2.51/0.58 thf(f30,plain,(
% 2.51/0.58 (lamProp = $true)),
% 2.51/0.58 inference(cnf_transformation,[],[f23])).
% 2.51/0.58 thf(f31,plain,(
% 2.51/0.58 ( ! [X3 : $i] : (($true != ((in @ X3 @ sK0))) | ($true = ((in @ (sK2 @ X3) @ sK1)))) )),
% 2.51/0.58 inference(cnf_transformation,[],[f23])).
% 2.51/0.58 thf(f32,plain,(
% 2.51/0.58 ($true != ((func @ sK0 @ sK1 @ (lam @ sK0 @ sK1 @ (^[Y0 : $i]: (sK2 @ Y0))))))),
% 2.51/0.58 inference(cnf_transformation,[],[f23])).
% 2.51/0.58 thf(f34,definition,(
% 2.51/0.58 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 2.51/0.58 introduced(theory,[fool_exhaustiveness_axiom])).
% 2.51/0.58 thf(f35,plain,(
% 2.51/0.58 (ex1 = (^[Y0 : $i]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (?? @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y2) & ((setadjoin @ Y3 @ emptyset) = Y2))))) @ (dsetconstr @ Y0 @ (^[Y2 : $i]: (Y1 @ Y2))))))))),
% 2.51/0.58 inference(definition_unfolding,[],[f25,f24])).
% 2.51/0.58 thf(f36,plain,(
% 2.51/0.58 (func = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i]: (subset @ Y5 @ (cartprod @ Y3 @ Y4))))))) @ Y0 @ Y1 @ Y2) & (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y0) => ((^[Y4 : $i]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: (?? @ $i @ (^[Y7 : $i]: ((in @ Y7 @ Y6) & ((setadjoin @ Y7 @ emptyset) = Y6))))) @ (dsetconstr @ Y4 @ (^[Y6 : $i]: (Y5 @ Y6))))))) @ Y1 @ (^[Y4 : $i]: (in @ (kpair @ Y3 @ Y4) @ Y2)))))))))))))),
% 2.51/0.58 inference(definition_unfolding,[],[f27,f26,f35])).
% 2.51/0.58 thf(f37,plain,(
% 2.51/0.58 ($true = ((!! @ ($i > $i) @ (^[Y0 : $i > $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y2) => (in @ (Y0 @ Y3) @ Y1)))) => ((^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i]: (((^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i]: (subset @ Y8 @ (cartprod @ Y6 @ Y7))))))) @ Y3 @ Y4 @ Y5) & (!! @ $i @ (^[Y6 : $i]: ((in @ Y6 @ Y3) => ((^[Y7 : $i]: ((^[Y8 : $i > $o]: ((^[Y9 : $i]: (?? @ $i @ (^[Y10 : $i]: ((in @ Y10 @ Y9) & ((setadjoin @ Y10 @ emptyset) = Y9))))) @ (dsetconstr @ Y7 @ (^[Y9 : $i]: (Y8 @ Y9))))))) @ Y4 @ (^[Y7 : $i]: (in @ (kpair @ Y6 @ Y7) @ Y5)))))))))))) @ Y2 @ Y1 @ (dpsetconstr @ Y2 @ Y1 @ (^[Y3 : $i]: ((^[Y4 : $i]: ((Y0 @ Y3) = Y4)))))))))))))))),
% 2.51/0.58 inference(definition_unfolding,[],[f28,f30,f36])).
% 2.51/0.58 thf(f38,plain,(
% 2.51/0.58 ($true != (((^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (((^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i]: (subset @ Y5 @ (cartprod @ Y3 @ Y4))))))) @ Y0 @ Y1 @ Y2) & (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y0) => ((^[Y4 : $i]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: (?? @ $i @ (^[Y7 : $i]: ((in @ Y7 @ Y6) & ((setadjoin @ Y7 @ emptyset) = Y6))))) @ (dsetconstr @ Y4 @ (^[Y6 : $i]: (Y5 @ Y6))))))) @ Y1 @ (^[Y4 : $i]: (in @ (kpair @ Y3 @ Y4) @ Y2)))))))))))) @ sK0 @ sK1 @ ((^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i > $i]: (dpsetconstr @ Y0 @ Y1 @ (^[Y3 : $i]: ((^[Y4 : $i]: ((Y2 @ Y3) = Y4)))))))))) @ sK0 @ sK1 @ (^[Y0 : $i]: (sK2 @ Y0))))))),
% 2.51/0.58 inference(definition_unfolding,[],[f32,f36,f29])).
% 2.51/0.58 thf(f39,plain,(
% 2.51/0.58 ($true != (((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1)) & (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ sK0) => (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ sK1 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y3 : $i]: (= @ (sK2 @ Y3)))))))) & ((setadjoin @ Y1 @ emptyset) = (dsetconstr @ sK1 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y3 : $i]: (= @ (sK2 @ Y3)))))))))))))))))),
% 2.51/0.58 inference(beta-eta_normalization,[],[f38])).
% 2.51/0.58 thf(f40,plain,(
% 2.51/0.58 ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ sK0) => (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ sK1 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y3 : $i]: (= @ (sK2 @ Y3)))))))) & ((setadjoin @ Y1 @ emptyset) = (dsetconstr @ sK1 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y3 : $i]: (= @ (sK2 @ Y3)))))))))))))))) | ($false = ((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1))))),
% 2.51/0.58 inference(and_proxy_clausification,[],[f39])).
% 2.51/0.58 thf(f41,plain,(
% 2.51/0.58 ($false = (((^[Y0 : $i]: ((in @ Y0 @ sK0) => (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ sK1 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y3 : $i]: (= @ (sK2 @ Y3)))))))) & ((setadjoin @ Y1 @ emptyset) = (dsetconstr @ sK1 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y3 : $i]: (= @ (sK2 @ Y3))))))))))))) @ sK3))) | ($false = ((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1))))),
% 2.51/0.58 inference(sigma_proxy_clausification,[],[f40])).
% 2.51/0.58 thf(f42,plain,(
% 2.51/0.58 ($false = (((in @ sK3 @ sK0) => (?? @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ sK1 @ (^[Y1 : $i]: (in @ (kpair @ sK3 @ Y1) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y2 : $i]: (= @ (sK2 @ Y2)))))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ sK1 @ (^[Y1 : $i]: (in @ (kpair @ sK3 @ Y1) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y2 : $i]: (= @ (sK2 @ Y2)))))))))))))) | ($false = ((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1))))),
% 2.51/0.58 inference(beta-eta_normalization,[],[f41])).
% 2.51/0.58 thf(f43,plain,(
% 2.51/0.58 ($false = ((?? @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ sK1 @ (^[Y1 : $i]: (in @ (kpair @ sK3 @ Y1) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y2 : $i]: (= @ (sK2 @ Y2)))))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ sK1 @ (^[Y1 : $i]: (in @ (kpair @ sK3 @ Y1) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y2 : $i]: (= @ (sK2 @ Y2))))))))))))) | ($false = ((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1))))),
% 2.51/0.58 inference(imp_proxy_clausification,[],[f42])).
% 2.51/0.58 thf(f44,plain,(
% 2.51/0.58 ($true = ((in @ sK3 @ sK0))) | ($false = ((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1))))),
% 2.51/0.58 inference(imp_proxy_clausification,[],[f42])).
% 2.51/0.58 thf(f45,plain,(
% 2.51/0.58 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ sK1 @ (^[Y1 : $i]: (in @ (kpair @ sK3 @ Y1) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y2 : $i]: (= @ (sK2 @ Y2)))))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ sK1 @ (^[Y1 : $i]: (in @ (kpair @ sK3 @ Y1) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y2 : $i]: (= @ (sK2 @ Y2)))))))))) @ X1))) | ($false = ((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1))))) )),
% 2.51/0.58 inference(pi_proxy_clausification,[],[f43])).
% 2.51/0.58 thf(f46,plain,(
% 2.51/0.58 ( ! [X1 : $i] : (($false = (((in @ X1 @ (dsetconstr @ sK1 @ (^[Y0 : $i]: (in @ (kpair @ sK3 @ Y0) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y1 : $i]: (= @ (sK2 @ Y1)))))))) & ((setadjoin @ X1 @ emptyset) = (dsetconstr @ sK1 @ (^[Y0 : $i]: (in @ (kpair @ sK3 @ Y0) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y1 : $i]: (= @ (sK2 @ Y1))))))))))) | ($false = ((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1))))) )),
% 2.51/0.58 inference(beta-eta_normalization,[],[f45])).
% 2.51/0.58 thf(f47,plain,(
% 2.51/0.58 ( ! [X1 : $i] : (($false = (((setadjoin @ X1 @ emptyset) = (dsetconstr @ sK1 @ (^[Y0 : $i]: (in @ (kpair @ sK3 @ Y0) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y1 : $i]: (= @ (sK2 @ Y1)))))))))) | ($false = ((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1)))) | ($false = ((in @ X1 @ (dsetconstr @ sK1 @ (^[Y0 : $i]: (in @ (kpair @ sK3 @ Y0) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y1 : $i]: (= @ (sK2 @ Y1))))))))))) )),
% 2.51/0.58 inference(and_proxy_clausification,[],[f46])).
% 2.51/0.58 thf(f48,plain,(
% 2.51/0.58 ( ! [X1 : $i] : ((((setadjoin @ X1 @ emptyset)) != ((dsetconstr @ sK1 @ (^[Y0 : $i]: (in @ (kpair @ sK3 @ Y0) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y1 : $i]: (= @ (sK2 @ Y1))))))))) | ($false = ((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1)))) | ($false = ((in @ X1 @ (dsetconstr @ sK1 @ (^[Y0 : $i]: (in @ (kpair @ sK3 @ Y0) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y1 : $i]: (= @ (sK2 @ Y1))))))))))) )),
% 2.51/0.58 inference(equality_proxy_clausification,[],[f47])).
% 2.51/0.58 thf(f49,plain,(
% 2.51/0.58 ( ! [X1 : ($i > $i)] : (($true = (((^[Y0 : $i > $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y2) => (in @ (Y0 @ Y3) @ Y1)))) => ((^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i]: (((^[Y6 : $i]: ((^[Y7 : $i]: ((^[Y8 : $i]: (subset @ Y8 @ (cartprod @ Y6 @ Y7))))))) @ Y3 @ Y4 @ Y5) & (!! @ $i @ (^[Y6 : $i]: ((in @ Y6 @ Y3) => ((^[Y7 : $i]: ((^[Y8 : $i > $o]: ((^[Y9 : $i]: (?? @ $i @ (^[Y10 : $i]: ((in @ Y10 @ Y9) & ((setadjoin @ Y10 @ emptyset) = Y9))))) @ (dsetconstr @ Y7 @ (^[Y9 : $i]: (Y8 @ Y9))))))) @ Y4 @ (^[Y7 : $i]: (in @ (kpair @ Y6 @ Y7) @ Y5)))))))))))) @ Y2 @ Y1 @ (dpsetconstr @ Y2 @ Y1 @ (^[Y3 : $i]: ((^[Y4 : $i]: ((Y0 @ Y3) = Y4)))))))))))) @ X1)))) )),
% 2.51/0.58 inference(pi_proxy_clausification,[],[f37])).
% 2.51/0.58 thf(f50,plain,(
% 2.51/0.58 ( ! [X1 : ($i > $i)] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ (X1 @ Y2) @ Y0)))) => ((subset @ (dpsetconstr @ Y1 @ Y0 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))) @ (cartprod @ Y1 @ Y0)) & (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (?? @ $i @ (^[Y3 : $i]: ((in @ Y3 @ (dsetconstr @ Y0 @ (^[Y4 : $i]: (in @ (kpair @ Y2 @ Y4) @ (dpsetconstr @ Y1 @ Y0 @ (^[Y5 : $i]: (= @ (X1 @ Y5)))))))) & ((setadjoin @ Y3 @ emptyset) = (dsetconstr @ Y0 @ (^[Y4 : $i]: (in @ (kpair @ Y2 @ Y4) @ (dpsetconstr @ Y1 @ Y0 @ (^[Y5 : $i]: (= @ (X1 @ Y5))))))))))))))))))))))) )),
% 2.51/0.58 inference(beta-eta_normalization,[],[f49])).
% 2.51/0.58 thf(f51,plain,(
% 2.51/0.58 ( ! [X2 : $i,X1 : ($i > $i)] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ (X1 @ Y2) @ Y0)))) => ((subset @ (dpsetconstr @ Y1 @ Y0 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))) @ (cartprod @ Y1 @ Y0)) & (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (?? @ $i @ (^[Y3 : $i]: ((in @ Y3 @ (dsetconstr @ Y0 @ (^[Y4 : $i]: (in @ (kpair @ Y2 @ Y4) @ (dpsetconstr @ Y1 @ Y0 @ (^[Y5 : $i]: (= @ (X1 @ Y5)))))))) & ((setadjoin @ Y3 @ emptyset) = (dsetconstr @ Y0 @ (^[Y4 : $i]: (in @ (kpair @ Y2 @ Y4) @ (dpsetconstr @ Y1 @ Y0 @ (^[Y5 : $i]: (= @ (X1 @ Y5))))))))))))))))))) @ X2)))) )),
% 2.51/0.58 inference(pi_proxy_clausification,[],[f50])).
% 2.51/0.58 thf(f52,plain,(
% 2.51/0.58 ( ! [X2 : $i,X1 : ($i > $i)] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => (in @ (X1 @ Y1) @ X2)))) => ((subset @ (dpsetconstr @ Y0 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1)))) @ (cartprod @ Y0 @ X2)) & (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => (?? @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ X2 @ (^[Y3 : $i]: (in @ (kpair @ Y1 @ Y3) @ (dpsetconstr @ Y0 @ X2 @ (^[Y4 : $i]: (= @ (X1 @ Y4)))))))) & ((setadjoin @ Y2 @ emptyset) = (dsetconstr @ X2 @ (^[Y3 : $i]: (in @ (kpair @ Y1 @ Y3) @ (dpsetconstr @ Y0 @ X2 @ (^[Y4 : $i]: (= @ (X1 @ Y4))))))))))))))))))))) )),
% 2.51/0.58 inference(beta-eta_normalization,[],[f51])).
% 2.51/0.58 thf(f53,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i)] : (($true = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => (in @ (X1 @ Y1) @ X2)))) => ((subset @ (dpsetconstr @ Y0 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1)))) @ (cartprod @ Y0 @ X2)) & (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => (?? @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ X2 @ (^[Y3 : $i]: (in @ (kpair @ Y1 @ Y3) @ (dpsetconstr @ Y0 @ X2 @ (^[Y4 : $i]: (= @ (X1 @ Y4)))))))) & ((setadjoin @ Y2 @ emptyset) = (dsetconstr @ X2 @ (^[Y3 : $i]: (in @ (kpair @ Y1 @ Y3) @ (dpsetconstr @ Y0 @ X2 @ (^[Y4 : $i]: (= @ (X1 @ Y4))))))))))))))))) @ X3)))) )),
% 2.51/0.58 inference(pi_proxy_clausification,[],[f52])).
% 2.51/0.58 thf(f54,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i)] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (in @ (X1 @ Y0) @ X2)))) => ((subset @ (dpsetconstr @ X3 @ X2 @ (^[Y0 : $i]: (= @ (X1 @ Y0)))) @ (cartprod @ X3 @ X2)) & (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ X3 @ X2 @ (^[Y3 : $i]: (= @ (X1 @ Y3)))))))) & ((setadjoin @ Y1 @ emptyset) = (dsetconstr @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ X3 @ X2 @ (^[Y3 : $i]: (= @ (X1 @ Y3))))))))))))))))))) )),
% 2.51/0.58 inference(beta-eta_normalization,[],[f53])).
% 2.51/0.58 thf(f55,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i)] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (in @ (X1 @ Y0) @ X2)))))) | ($true = (((subset @ (dpsetconstr @ X3 @ X2 @ (^[Y0 : $i]: (= @ (X1 @ Y0)))) @ (cartprod @ X3 @ X2)) & (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ X3 @ X2 @ (^[Y3 : $i]: (= @ (X1 @ Y3)))))))) & ((setadjoin @ Y1 @ emptyset) = (dsetconstr @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ X3 @ X2 @ (^[Y3 : $i]: (= @ (X1 @ Y3)))))))))))))))))) )),
% 2.51/0.58 inference(imp_proxy_clausification,[],[f54])).
% 2.51/0.58 thf(f56,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i)] : (($false = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (in @ (X1 @ Y0) @ X2))) @ (sK4 @ X3 @ X1 @ X2)))) | ($true = (((subset @ (dpsetconstr @ X3 @ X2 @ (^[Y0 : $i]: (= @ (X1 @ Y0)))) @ (cartprod @ X3 @ X2)) & (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ X3 @ X2 @ (^[Y3 : $i]: (= @ (X1 @ Y3)))))))) & ((setadjoin @ Y1 @ emptyset) = (dsetconstr @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ X3 @ X2 @ (^[Y3 : $i]: (= @ (X1 @ Y3)))))))))))))))))) )),
% 2.51/0.58 inference(sigma_proxy_clausification,[],[f55])).
% 2.51/0.58 thf(f57,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i)] : (($false = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (in @ (X1 @ Y0) @ X2))) @ (sK4 @ X3 @ X1 @ X2)))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ X3 @ X2 @ (^[Y3 : $i]: (= @ (X1 @ Y3)))))))) & ((setadjoin @ Y1 @ emptyset) = (dsetconstr @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ X3 @ X2 @ (^[Y3 : $i]: (= @ (X1 @ Y3))))))))))))))))) )),
% 2.51/0.58 inference(and_proxy_clausification,[],[f56])).
% 2.51/0.58 thf(f58,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i)] : (($false = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (in @ (X1 @ Y0) @ X2))) @ (sK4 @ X3 @ X1 @ X2)))) | ($true = ((subset @ (dpsetconstr @ X3 @ X2 @ (^[Y0 : $i]: (= @ (X1 @ Y0)))) @ (cartprod @ X3 @ X2))))) )),
% 2.51/0.58 inference(and_proxy_clausification,[],[f56])).
% 2.51/0.58 thf(f59,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i)] : (($false = (((in @ (sK4 @ X3 @ X1 @ X2) @ X3) => (in @ (X1 @ (sK4 @ X3 @ X1 @ X2)) @ X2)))) | ($true = ((subset @ (dpsetconstr @ X3 @ X2 @ (^[Y0 : $i]: (= @ (X1 @ Y0)))) @ (cartprod @ X3 @ X2))))) )),
% 2.51/0.58 inference(beta-eta_normalization,[],[f58])).
% 2.51/0.58 thf(f60,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i)] : (($false = ((in @ (X1 @ (sK4 @ X3 @ X1 @ X2)) @ X2))) | ($true = ((subset @ (dpsetconstr @ X3 @ X2 @ (^[Y0 : $i]: (= @ (X1 @ Y0)))) @ (cartprod @ X3 @ X2))))) )),
% 2.51/0.58 inference(imp_proxy_clausification,[],[f59])).
% 2.51/0.58 thf(f61,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i)] : (($true = ((subset @ (dpsetconstr @ X3 @ X2 @ (^[Y0 : $i]: (= @ (X1 @ Y0)))) @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK4 @ X3 @ X1 @ X2) @ X3)))) )),
% 2.51/0.58 inference(imp_proxy_clausification,[],[f59])).
% 2.51/0.58 thf(f62,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($false = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (in @ (X1 @ Y0) @ X2))) @ (sK4 @ X3 @ X1 @ X2)))) | ($true = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ X3 @ X2 @ (^[Y3 : $i]: (= @ (X1 @ Y3)))))))) & ((setadjoin @ Y1 @ emptyset) = (dsetconstr @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y0 @ Y2) @ (dpsetconstr @ X3 @ X2 @ (^[Y3 : $i]: (= @ (X1 @ Y3))))))))))))) @ X4)))) )),
% 2.51/0.58 inference(pi_proxy_clausification,[],[f57])).
% 2.51/0.58 thf(f63,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($false = (((in @ (sK4 @ X3 @ X1 @ X2) @ X3) => (in @ (X1 @ (sK4 @ X3 @ X1 @ X2)) @ X2)))) | ($true = (((in @ X4 @ X3) => (?? @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2))))))))))))))) )),
% 2.51/0.58 inference(beta-eta_normalization,[],[f62])).
% 2.51/0.58 thf(f64,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($false = ((in @ (X1 @ (sK4 @ X3 @ X1 @ X2)) @ X2))) | ($true = (((in @ X4 @ X3) => (?? @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2))))))))))))))) )),
% 2.51/0.58 inference(imp_proxy_clausification,[],[f63])).
% 2.51/0.58 thf(f65,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($true = ((in @ (sK4 @ X3 @ X1 @ X2) @ X3))) | ($true = (((in @ X4 @ X3) => (?? @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2))))))))))))))) )),
% 2.51/0.58 inference(imp_proxy_clausification,[],[f63])).
% 2.51/0.58 thf(f66,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($true = ((in @ (sK4 @ X3 @ X1 @ X2) @ X3))) | ($false = ((in @ X4 @ X3))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))))))))))))) )),
% 2.51/0.58 inference(imp_proxy_clausification,[],[f65])).
% 2.51/0.58 thf(f67,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($true = ((in @ (sK4 @ X3 @ X1 @ X2) @ X3))) | ($false = ((in @ X4 @ X3))) | ($true = (((^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))))))))) @ (sK5 @ X1 @ X2 @ X3 @ X4))))) )),
% 2.51/0.58 inference(sigma_proxy_clausification,[],[f66])).
% 2.51/0.58 thf(f68,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($true = ((in @ (sK4 @ X3 @ X1 @ X2) @ X3))) | ($false = ((in @ X4 @ X3))) | ($true = (((in @ (sK5 @ X1 @ X2 @ X3 @ X4) @ (dsetconstr @ X2 @ (^[Y0 : $i]: (in @ (kpair @ X4 @ Y0) @ (dpsetconstr @ X3 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1)))))))) & ((setadjoin @ (sK5 @ X1 @ X2 @ X3 @ X4) @ emptyset) = (dsetconstr @ X2 @ (^[Y0 : $i]: (in @ (kpair @ X4 @ Y0) @ (dpsetconstr @ X3 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1)))))))))))) )),
% 2.51/0.58 inference(beta-eta_normalization,[],[f67])).
% 2.51/0.58 thf(f69,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($true = ((in @ (sK4 @ X3 @ X1 @ X2) @ X3))) | ($false = ((in @ X4 @ X3))) | ($true = (((setadjoin @ (sK5 @ X1 @ X2 @ X3 @ X4) @ emptyset) = (dsetconstr @ X2 @ (^[Y0 : $i]: (in @ (kpair @ X4 @ Y0) @ (dpsetconstr @ X3 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1))))))))))) )),
% 2.51/0.58 inference(and_proxy_clausification,[],[f68])).
% 2.51/0.58 thf(f70,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($true = ((in @ (sK5 @ X1 @ X2 @ X3 @ X4) @ (dsetconstr @ X2 @ (^[Y0 : $i]: (in @ (kpair @ X4 @ Y0) @ (dpsetconstr @ X3 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1)))))))))) | ($false = ((in @ X4 @ X3))) | ($true = ((in @ (sK4 @ X3 @ X1 @ X2) @ X3)))) )),
% 2.51/0.58 inference(and_proxy_clausification,[],[f68])).
% 2.51/0.58 thf(f71,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : ((((dsetconstr @ X2 @ (^[Y0 : $i]: (in @ (kpair @ X4 @ Y0) @ (dpsetconstr @ X3 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1)))))))) = ((setadjoin @ (sK5 @ X1 @ X2 @ X3 @ X4) @ emptyset))) | ($true = ((in @ (sK4 @ X3 @ X1 @ X2) @ X3))) | ($false = ((in @ X4 @ X3)))) )),
% 2.51/0.58 inference(equality_proxy_clausification,[],[f69])).
% 2.51/0.58 thf(f72,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($false = ((in @ (X1 @ (sK4 @ X3 @ X1 @ X2)) @ X2))) | ($false = ((in @ X4 @ X3))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))))))))))))) )),
% 2.51/0.58 inference(imp_proxy_clausification,[],[f64])).
% 2.51/0.58 thf(f73,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($false = ((in @ (X1 @ (sK4 @ X3 @ X1 @ X2)) @ X2))) | ($false = ((in @ X4 @ X3))) | ($true = (((^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ X2 @ (^[Y1 : $i]: (in @ (kpair @ X4 @ Y1) @ (dpsetconstr @ X3 @ X2 @ (^[Y2 : $i]: (= @ (X1 @ Y2)))))))))) @ (sK6 @ X1 @ X2 @ X3 @ X4))))) )),
% 2.51/0.58 inference(sigma_proxy_clausification,[],[f72])).
% 2.51/0.58 thf(f74,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($false = ((in @ (X1 @ (sK4 @ X3 @ X1 @ X2)) @ X2))) | ($false = ((in @ X4 @ X3))) | ($true = (((in @ (sK6 @ X1 @ X2 @ X3 @ X4) @ (dsetconstr @ X2 @ (^[Y0 : $i]: (in @ (kpair @ X4 @ Y0) @ (dpsetconstr @ X3 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1)))))))) & ((setadjoin @ (sK6 @ X1 @ X2 @ X3 @ X4) @ emptyset) = (dsetconstr @ X2 @ (^[Y0 : $i]: (in @ (kpair @ X4 @ Y0) @ (dpsetconstr @ X3 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1)))))))))))) )),
% 2.51/0.58 inference(beta-eta_normalization,[],[f73])).
% 2.51/0.58 thf(f75,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($false = ((in @ (X1 @ (sK4 @ X3 @ X1 @ X2)) @ X2))) | ($false = ((in @ X4 @ X3))) | ($true = (((setadjoin @ (sK6 @ X1 @ X2 @ X3 @ X4) @ emptyset) = (dsetconstr @ X2 @ (^[Y0 : $i]: (in @ (kpair @ X4 @ Y0) @ (dpsetconstr @ X3 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1))))))))))) )),
% 2.51/0.58 inference(and_proxy_clausification,[],[f74])).
% 2.51/0.58 thf(f76,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : (($true = ((in @ (sK6 @ X1 @ X2 @ X3 @ X4) @ (dsetconstr @ X2 @ (^[Y0 : $i]: (in @ (kpair @ X4 @ Y0) @ (dpsetconstr @ X3 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1)))))))))) | ($false = ((in @ X4 @ X3))) | ($false = ((in @ (X1 @ (sK4 @ X3 @ X1 @ X2)) @ X2)))) )),
% 2.51/0.58 inference(and_proxy_clausification,[],[f74])).
% 2.51/0.58 thf(f77,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X1 : ($i > $i),X4 : $i] : ((((dsetconstr @ X2 @ (^[Y0 : $i]: (in @ (kpair @ X4 @ Y0) @ (dpsetconstr @ X3 @ X2 @ (^[Y1 : $i]: (= @ (X1 @ Y1)))))))) = ((setadjoin @ (sK6 @ X1 @ X2 @ X3 @ X4) @ emptyset))) | ($false = ((in @ (X1 @ (sK4 @ X3 @ X1 @ X2)) @ X2))) | ($false = ((in @ X4 @ X3)))) )),
% 2.51/0.58 inference(equality_proxy_clausification,[],[f75])).
% 2.51/0.58 thf(f79,definition,(
% 2.51/0.58 spl7_1 <=> ($false = ((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1))))),
% 2.51/0.58 introduced(definition,[new_symbols(definition,[spl7_1])],[avatar_definition])).
% 2.51/0.58 thf(f81,plain,(
% 2.51/0.58 ($false = ((subset @ (dpsetconstr @ sK0 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ Y0)))) @ (cartprod @ sK0 @ sK1)))) | ~spl7_1),
% 2.51/0.58 inference(avatar_component_clause,[],[f79])).
% 2.51/0.58 thf(f83,definition,(
% 2.51/0.58 spl7_2 <=> ($true = ((in @ sK3 @ sK0)))),
% 2.51/0.58 introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition])).
% 2.51/0.58 thf(f85,plain,(
% 2.51/0.58 ($true = ((in @ sK3 @ sK0))) | ~spl7_2),
% 2.51/0.58 inference(avatar_component_clause,[],[f83])).
% 2.51/0.58 thf(f86,plain,(
% 2.51/0.58 spl7_1 | spl7_2),
% 2.51/0.58 inference(avatar_split_clause,[],[f44,f83,f79])).
% 2.51/0.58 thf(f88,definition,(
% 2.51/0.58 spl7_3 <=> ! [X1 : $i] : ((((setadjoin @ X1 @ emptyset)) != ((dsetconstr @ sK1 @ (^[Y0 : $i]: (in @ (kpair @ sK3 @ Y0) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y1 : $i]: (= @ (sK2 @ Y1))))))))) | ($false = ((in @ X1 @ (dsetconstr @ sK1 @ (^[Y0 : $i]: (in @ (kpair @ sK3 @ Y0) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y1 : $i]: (= @ (sK2 @ Y1)))))))))))),
% 2.51/0.58 introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition])).
% 2.51/0.58 thf(f89,plain,(
% 2.51/0.58 ( ! [X1 : $i] : ((((setadjoin @ X1 @ emptyset)) != ((dsetconstr @ sK1 @ (^[Y0 : $i]: (in @ (kpair @ sK3 @ Y0) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y1 : $i]: (= @ (sK2 @ Y1))))))))) | ($false = ((in @ X1 @ (dsetconstr @ sK1 @ (^[Y0 : $i]: (in @ (kpair @ sK3 @ Y0) @ (dpsetconstr @ sK0 @ sK1 @ (^[Y1 : $i]: (= @ (sK2 @ Y1))))))))))) ) | ~spl7_3),
% 2.51/0.58 inference(avatar_component_clause,[],[f88])).
% 2.51/0.58 thf(f90,plain,(
% 2.51/0.58 spl7_1 | spl7_3),
% 2.51/0.58 inference(avatar_split_clause,[],[f48,f88,f79])).
% 2.51/0.58 thf(f95,plain,(
% 2.51/0.58 ( ! [X0 : $i] : (($true != $true) | ($true = ((in @ (sK2 @ X0) @ sK1))) | ($false = ((in @ X0 @ sK0)))) )),
% 2.51/0.58 inference(constrained_superposition,[],[f31,f34])).
% 2.51/0.58 thf(f97,plain,(
% 2.51/0.58 ( ! [X0 : $i] : (($true = ((in @ (sK2 @ X0) @ sK1))) | ($false = ((in @ X0 @ sK0)))) )),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f95])).
% 2.51/0.58 thf(f105,plain,(
% 2.51/0.58 ( ! [X2 : $i,X0 : $i,X1 : ($i > $i)] : (($true = $false) | ($false = ((in @ X0 @ sK0))) | ($true = ((subset @ (dpsetconstr @ X2 @ sK1 @ (^[Y0 : $i]: (= @ ((^[Y1 : $i]: (sK2 @ (X1 @ Y1))) @ Y0)))) @ (cartprod @ X2 @ sK1)))) | (((X1 @ (sK4 @ X2 @ (^[Y0 : $i]: (sK2 @ (X1 @ Y0))) @ sK1))) != X0)) )),
% 2.51/0.58 inference(constrained_superposition,[],[f97,f60])).
% 2.51/0.58 thf(f106,plain,(
% 2.51/0.58 ( ! [X2 : $i,X0 : $i,X1 : ($i > $i)] : (($false = ((in @ X0 @ sK0))) | ($true = ((subset @ (dpsetconstr @ X2 @ sK1 @ (^[Y0 : $i]: (= @ ((^[Y1 : $i]: (sK2 @ (X1 @ Y1))) @ Y0)))) @ (cartprod @ X2 @ sK1)))) | (((X1 @ (sK4 @ X2 @ (^[Y0 : $i]: (sK2 @ (X1 @ Y0))) @ sK1))) != X0)) )),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f105])).
% 2.51/0.58 thf(f107,plain,(
% 2.51/0.58 ( ! [X2 : $i,X0 : $i,X1 : ($i > $i)] : (($false = ((in @ X0 @ sK0))) | ($true = ((subset @ (dpsetconstr @ X2 @ sK1 @ (^[Y0 : $i]: (= @ (sK2 @ (X1 @ Y0))))) @ (cartprod @ X2 @ sK1)))) | (((X1 @ (sK4 @ X2 @ (^[Y0 : $i]: (sK2 @ (X1 @ Y0))) @ sK1))) != X0)) )),
% 2.51/0.58 inference(beta-eta_normalization,[],[f106])).
% 2.51/0.58 thf(f123,plain,(
% 2.51/0.58 ( ! [X2 : $i,X0 : ($i > $i),X1 : $i] : ((((setadjoin @ (sK5 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1 @ sK0 @ X1) @ emptyset)) != ((setadjoin @ X2 @ emptyset))) | ($false = ((in @ X2 @ (setadjoin @ (sK5 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1 @ sK0 @ X1) @ emptyset)))) | ($true = ((in @ (sK4 @ sK0 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1) @ sK0))) | ($false = ((in @ X1 @ sK0))) | ((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: ((^[Y1 : $i]: (Y1))))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X1)))) ) | ~spl7_3),
% 2.51/0.58 inference(constrained_superposition,[],[f89,f71])).
% 2.51/0.58 thf(f124,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i),X1 : $i,X6 : $i,X4 : ($i > $i),X5 : $i] : (($true = ((in @ (sK5 @ X4 @ X1 @ X5 @ X6) @ (setadjoin @ (sK5 @ X0 @ X1 @ X2 @ X3) @ emptyset)))) | ($true = ((in @ (sK4 @ X5 @ X4 @ X1) @ X5))) | ($true = ((in @ (sK4 @ X2 @ X0 @ X1) @ X2))) | ($false = ((in @ X6 @ X5))) | ($false = ((in @ X3 @ X2))) | ((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: (X4))) | ((^[Y0 : $i]: (X3)) != (^[Y0 : $i]: (X6))) | ((^[Y0 : $i]: (X2)) != (^[Y0 : $i]: (X5)))) )),
% 2.51/0.58 inference(constrained_superposition,[],[f70,f71])).
% 2.51/0.58 thf(f148,plain,(
% 2.51/0.58 ( ! [X2 : $i,X0 : ($i > $i),X1 : $i] : ((((setadjoin @ X2 @ emptyset)) != ((setadjoin @ (sK6 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1 @ sK0 @ X1) @ emptyset))) | ($false = ((in @ X2 @ (setadjoin @ (sK6 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1 @ sK0 @ X1) @ emptyset)))) | ($false = ((in @ ((^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ (sK4 @ sK0 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1)) @ sK1))) | ($false = ((in @ X1 @ sK0))) | ((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: ((^[Y1 : $i]: (Y1))))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X1)))) ) | ~spl7_3),
% 2.51/0.58 inference(constrained_superposition,[],[f89,f77])).
% 2.51/0.58 thf(f149,plain,(
% 2.51/0.58 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i),X1 : $i,X6 : $i,X4 : ($i > $i),X5 : $i] : (($true = ((in @ (sK6 @ X4 @ X1 @ X5 @ X6) @ (setadjoin @ (sK6 @ X0 @ X1 @ X2 @ X3) @ emptyset)))) | ($false = ((in @ (X4 @ (sK4 @ X5 @ X4 @ X1)) @ X1))) | ($false = ((in @ (X0 @ (sK4 @ X2 @ X0 @ X1)) @ X1))) | ($false = ((in @ X6 @ X5))) | ($false = ((in @ X3 @ X2))) | ((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: (X4))) | ((^[Y0 : $i]: (X3)) != (^[Y0 : $i]: (X6))) | ((^[Y0 : $i]: (X2)) != (^[Y0 : $i]: (X5)))) )),
% 2.51/0.58 inference(constrained_superposition,[],[f76,f77])).
% 2.51/0.58 thf(f165,plain,(
% 2.51/0.58 ( ! [X2 : $i,X0 : ($i > $i),X1 : $i] : ((((setadjoin @ X2 @ emptyset)) != ((setadjoin @ (sK6 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1 @ sK0 @ X1) @ emptyset))) | ($false = ((in @ X2 @ (setadjoin @ (sK6 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1 @ sK0 @ X1) @ emptyset)))) | ($false = ((in @ (sK2 @ (X0 @ (sK4 @ sK0 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1))) @ sK1))) | ($false = ((in @ X1 @ sK0))) | ((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: ((^[Y1 : $i]: (Y1))))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X1)))) ) | ~spl7_3),
% 2.51/0.58 inference(beta-eta_normalization,[],[f148])).
% 2.51/0.58 thf(f198,definition,(
% 2.51/0.58 spl7_4 <=> ! [X2 : $i] : (($false = ((in @ X2 @ sK0))) | (((sK4 @ sK0 @ sK2 @ sK1)) != X2))),
% 2.51/0.58 introduced(definition,[new_symbols(definition,[spl7_4])],[avatar_definition])).
% 2.51/0.58 thf(f199,plain,(
% 2.51/0.58 ( ! [X2 : $i] : ((((sK4 @ sK0 @ sK2 @ sK1)) != X2) | ($false = ((in @ X2 @ sK0)))) ) | ~spl7_4),
% 2.51/0.58 inference(avatar_component_clause,[],[f198])).
% 2.51/0.58 thf(f204,plain,(
% 2.51/0.58 ($false = ((in @ (sK4 @ sK0 @ sK2 @ sK1) @ sK0))) | ~spl7_4),
% 2.51/0.58 inference(equality_resolution,[],[f199])).
% 2.51/0.58 thf(f295,plain,(
% 2.51/0.58 ( ! [X0 : ($i > $i),X1 : $i] : (((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: ((^[Y1 : $i]: (Y1))))) | ($true = ((in @ (sK4 @ sK0 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1) @ sK0))) | ($false = ((in @ X1 @ sK0))) | ($false = ((in @ (sK5 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1 @ sK0 @ X1) @ (setadjoin @ (sK5 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1 @ sK0 @ X1) @ emptyset)))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X1)))) ) | ~spl7_3),
% 2.51/0.58 inference(equality_resolution,[],[f123])).
% 2.51/0.58 thf(f1293,plain,(
% 2.51/0.58 ( ! [X0 : ($i > $i),X1 : $i] : (((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: ((^[Y1 : $i]: (Y1))))) | ($false = ((in @ (sK2 @ (X0 @ (sK4 @ sK0 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1))) @ sK1))) | ($false = ((in @ X1 @ sK0))) | ($false = ((in @ (sK6 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1 @ sK0 @ X1) @ (setadjoin @ (sK6 @ (^[Y0 : $i]: (sK2 @ (X0 @ Y0))) @ sK1 @ sK0 @ X1) @ emptyset)))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X1)))) ) | ~spl7_3),
% 2.51/0.58 inference(equality_resolution,[],[f165])).
% 2.51/0.58 thf(f1806,plain,(
% 2.51/0.58 ( ! [X0 : $i] : (($false = ((in @ (sK2 @ ((^[Y0 : $i]: (Y0)) @ (sK4 @ sK0 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK1))) @ sK1))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (sK6 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK1 @ sK0 @ X0) @ (setadjoin @ (sK6 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK1 @ sK0 @ X0) @ emptyset)))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X0)))) ) | ~spl7_3),
% 2.51/0.58 inference(equality_resolution,[],[f1293])).
% 2.51/0.58 thf(f1807,plain,(
% 2.51/0.58 ( ! [X0 : $i] : (($false = ((in @ (sK2 @ (sK4 @ sK0 @ sK2 @ sK1)) @ sK1))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (sK6 @ sK2 @ sK1 @ sK0 @ X0) @ (setadjoin @ (sK6 @ sK2 @ sK1 @ sK0 @ X0) @ emptyset)))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X0)))) ) | ~spl7_3),
% 2.51/0.58 inference(beta-eta_normalization,[],[f1806])).
% 2.51/0.58 thf(f1810,definition,(
% 2.51/0.58 spl7_6 <=> ! [X0 : $i] : (($false = ((in @ X0 @ sK0))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X0))) | ($false = ((in @ (sK6 @ sK2 @ sK1 @ sK0 @ X0) @ (setadjoin @ (sK6 @ sK2 @ sK1 @ sK0 @ X0) @ emptyset)))))),
% 2.51/0.58 introduced(definition,[new_symbols(definition,[spl7_6])],[avatar_definition])).
% 2.51/0.58 thf(f1811,plain,(
% 2.51/0.58 ( ! [X0 : $i] : (((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X0))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (sK6 @ sK2 @ sK1 @ sK0 @ X0) @ (setadjoin @ (sK6 @ sK2 @ sK1 @ sK0 @ X0) @ emptyset))))) ) | ~spl7_6),
% 2.51/0.58 inference(avatar_component_clause,[],[f1810])).
% 2.51/0.58 thf(f1813,definition,(
% 2.51/0.58 spl7_7 <=> ($false = ((in @ (sK2 @ (sK4 @ sK0 @ sK2 @ sK1)) @ sK1)))),
% 2.51/0.58 introduced(definition,[new_symbols(definition,[spl7_7])],[avatar_definition])).
% 2.51/0.58 thf(f1815,plain,(
% 2.51/0.58 ($false = ((in @ (sK2 @ (sK4 @ sK0 @ sK2 @ sK1)) @ sK1))) | ~spl7_7),
% 2.51/0.58 inference(avatar_component_clause,[],[f1813])).
% 2.51/0.58 thf(f1819,plain,(
% 2.51/0.58 ( ! [X0 : $i] : (($true = $false) | ($false = ((in @ X0 @ sK0))) | ((((^[Y0 : $i]: (Y0)) @ (sK4 @ sK0 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK1))) != X0)) ) | ~spl7_1),
% 2.51/0.58 inference(constrained_superposition,[],[f81,f107])).
% 2.51/0.58 thf(f1822,plain,(
% 2.51/0.58 ($true = $false) | ($true = ((in @ (sK4 @ sK0 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK1) @ sK0))) | ~spl7_1),
% 2.51/0.58 inference(constrained_superposition,[],[f61,f81])).
% 2.51/0.58 thf(f1826,plain,(
% 2.51/0.58 ($true = ((in @ (sK4 @ sK0 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK1) @ sK0))) | ~spl7_1),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f1822])).
% 2.51/0.58 thf(f1827,plain,(
% 2.51/0.58 ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1) @ sK0))) | ~spl7_1),
% 2.51/0.58 inference(beta-eta_normalization,[],[f1826])).
% 2.51/0.58 thf(f1837,plain,(
% 2.51/0.58 ($true = $false) | (~spl7_1 | ~spl7_4)),
% 2.51/0.58 inference(forward_demodulation,[],[f1827,f204])).
% 2.51/0.58 thf(f1838,plain,(
% 2.51/0.58 $false | (~spl7_1 | ~spl7_4)),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f1837])).
% 2.51/0.58 thf(f1839,plain,(
% 2.51/0.58 ~spl7_1 | ~spl7_4),
% 2.51/0.58 inference(avatar_contradiction_clause,[],[f1838])).
% 2.51/0.58 thf(f1924,plain,(
% 2.51/0.58 spl7_6 | spl7_7 | ~spl7_3),
% 2.51/0.58 inference(avatar_split_clause,[],[f1807,f88,f1813,f1810])).
% 2.51/0.58 thf(f1946,definition,(
% 2.51/0.58 spl7_8 <=> ! [X0 : $i] : (($false = ((in @ X0 @ sK0))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X0))) | ($false = ((in @ (sK5 @ sK2 @ sK1 @ sK0 @ X0) @ (setadjoin @ (sK5 @ sK2 @ sK1 @ sK0 @ X0) @ emptyset)))))),
% 2.51/0.58 introduced(definition,[new_symbols(definition,[spl7_8])],[avatar_definition])).
% 2.51/0.58 thf(f1947,plain,(
% 2.51/0.58 ( ! [X0 : $i] : (((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X0))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (sK5 @ sK2 @ sK1 @ sK0 @ X0) @ (setadjoin @ (sK5 @ sK2 @ sK1 @ sK0 @ X0) @ emptyset))))) ) | ~spl7_8),
% 2.51/0.58 inference(avatar_component_clause,[],[f1946])).
% 2.51/0.58 thf(f1949,definition,(
% 2.51/0.58 spl7_9 <=> ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1) @ sK0)))),
% 2.51/0.58 introduced(definition,[new_symbols(definition,[spl7_9])],[avatar_definition])).
% 2.51/0.58 thf(f1950,plain,(
% 2.51/0.58 ($true != ((in @ (sK4 @ sK0 @ sK2 @ sK1) @ sK0))) | spl7_9),
% 2.51/0.58 inference(avatar_component_clause,[],[f1949])).
% 2.51/0.58 thf(f1951,plain,(
% 2.51/0.58 ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1) @ sK0))) | ~spl7_9),
% 2.51/0.58 inference(avatar_component_clause,[],[f1949])).
% 2.51/0.58 thf(f1972,plain,(
% 2.51/0.58 ($true != $true) | ($true = ((in @ (sK2 @ (sK4 @ sK0 @ sK2 @ sK1)) @ sK1))) | ~spl7_9),
% 2.51/0.58 inference(constrained_superposition,[],[f31,f1951])).
% 2.51/0.58 thf(f1973,plain,(
% 2.51/0.58 ($true = ((in @ (sK2 @ (sK4 @ sK0 @ sK2 @ sK1)) @ sK1))) | ~spl7_9),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f1972])).
% 2.51/0.58 thf(f2149,plain,(
% 2.51/0.58 ($false = ((in @ sK3 @ sK0))) | ($false = ((in @ (sK6 @ sK2 @ sK1 @ sK0 @ sK3) @ (setadjoin @ (sK6 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset)))) | ~spl7_6),
% 2.51/0.58 inference(equality_resolution,[],[f1811])).
% 2.51/0.58 thf(f2151,plain,(
% 2.51/0.58 ($true = $false) | ($false = ((in @ (sK6 @ sK2 @ sK1 @ sK0 @ sK3) @ (setadjoin @ (sK6 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset)))) | (~spl7_2 | ~spl7_6)),
% 2.51/0.58 inference(forward_demodulation,[],[f2149,f85])).
% 2.51/0.58 thf(f2152,plain,(
% 2.51/0.58 ($false = ((in @ (sK6 @ sK2 @ sK1 @ sK0 @ sK3) @ (setadjoin @ (sK6 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset)))) | (~spl7_2 | ~spl7_6)),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f2151])).
% 2.51/0.58 thf(f2177,plain,(
% 2.51/0.58 ( ! [X0 : $i] : (($true = ((in @ (sK4 @ sK0 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK1) @ sK0))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (sK5 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK1 @ sK0 @ X0) @ (setadjoin @ (sK5 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK1 @ sK0 @ X0) @ emptyset)))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X0)))) ) | ~spl7_3),
% 2.51/0.58 inference(equality_resolution,[],[f295])).
% 2.51/0.58 thf(f2178,plain,(
% 2.51/0.58 ( ! [X0 : $i] : (($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1) @ sK0))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (sK5 @ sK2 @ sK1 @ sK0 @ X0) @ (setadjoin @ (sK5 @ sK2 @ sK1 @ sK0 @ X0) @ emptyset)))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (X0)))) ) | ~spl7_3),
% 2.51/0.58 inference(beta-eta_normalization,[],[f2177])).
% 2.51/0.58 thf(f2185,plain,(
% 2.51/0.58 ($true = $false) | ($false = ((in @ (sK2 @ (sK4 @ sK0 @ sK2 @ sK1)) @ sK1))) | ($false = ((in @ (sK2 @ (sK4 @ sK0 @ sK2 @ sK1)) @ sK1))) | ($false = ((in @ sK3 @ sK0))) | ($false = ((in @ sK3 @ sK0))) | ((^[Y0 : $i]: (sK2)) != (^[Y0 : $i]: (sK2))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (sK3))) | ((^[Y0 : $i]: (sK0)) != (^[Y0 : $i]: (sK0))) | (~spl7_2 | ~spl7_6)),
% 2.51/0.58 inference(constrained_superposition,[],[f149,f2152])).
% 2.51/0.58 thf(f2186,plain,(
% 2.51/0.58 ($true = $false) | ($false = ((in @ (sK2 @ (sK4 @ sK0 @ sK2 @ sK1)) @ sK1))) | ($false = ((in @ sK3 @ sK0))) | ((^[Y0 : $i]: (sK2)) != (^[Y0 : $i]: (sK2))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (sK3))) | ((^[Y0 : $i]: (sK0)) != (^[Y0 : $i]: (sK0))) | (~spl7_2 | ~spl7_6)),
% 2.51/0.58 inference(duplicate_literal_removal,[],[f2185])).
% 2.51/0.58 thf(f2187,plain,(
% 2.51/0.58 ($false = ((in @ (sK2 @ (sK4 @ sK0 @ sK2 @ sK1)) @ sK1))) | ($false = ((in @ sK3 @ sK0))) | (~spl7_2 | ~spl7_6)),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f2186])).
% 2.51/0.58 thf(f2191,plain,(
% 2.51/0.58 ($true = $false) | ($false = ((in @ (sK2 @ (sK4 @ sK0 @ sK2 @ sK1)) @ sK1))) | (~spl7_2 | ~spl7_6)),
% 2.51/0.58 inference(forward_demodulation,[],[f2187,f85])).
% 2.51/0.58 thf(f2192,plain,(
% 2.51/0.58 ($false = ((in @ (sK2 @ (sK4 @ sK0 @ sK2 @ sK1)) @ sK1))) | (~spl7_2 | ~spl7_6)),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f2191])).
% 2.51/0.58 thf(f2201,plain,(
% 2.51/0.58 spl7_7 | ~spl7_2 | ~spl7_6),
% 2.51/0.58 inference(avatar_split_clause,[],[f2192,f1810,f83,f1813])).
% 2.51/0.58 thf(f2209,plain,(
% 2.51/0.58 ($true = $false) | (~spl7_7 | ~spl7_9)),
% 2.51/0.58 inference(constrained_superposition,[],[f1815,f1973])).
% 2.51/0.58 thf(f2217,plain,(
% 2.51/0.58 $false | (~spl7_7 | ~spl7_9)),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f2209])).
% 2.51/0.58 thf(f2218,plain,(
% 2.51/0.58 ~spl7_7 | ~spl7_9),
% 2.51/0.58 inference(avatar_contradiction_clause,[],[f2217])).
% 2.51/0.58 thf(f2220,plain,(
% 2.51/0.58 spl7_8 | spl7_9 | ~spl7_3),
% 2.51/0.58 inference(avatar_split_clause,[],[f2178,f88,f1949,f1946])).
% 2.51/0.58 thf(f3016,plain,(
% 2.51/0.58 ($false = ((in @ sK3 @ sK0))) | ($false = ((in @ (sK5 @ sK2 @ sK1 @ sK0 @ sK3) @ (setadjoin @ (sK5 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset)))) | ~spl7_8),
% 2.51/0.58 inference(equality_resolution,[],[f1947])).
% 2.51/0.58 thf(f3018,plain,(
% 2.51/0.58 ($true = $false) | ($false = ((in @ (sK5 @ sK2 @ sK1 @ sK0 @ sK3) @ (setadjoin @ (sK5 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset)))) | (~spl7_2 | ~spl7_8)),
% 2.51/0.58 inference(forward_demodulation,[],[f3016,f85])).
% 2.51/0.58 thf(f3019,plain,(
% 2.51/0.58 ($false = ((in @ (sK5 @ sK2 @ sK1 @ sK0 @ sK3) @ (setadjoin @ (sK5 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset)))) | (~spl7_2 | ~spl7_8)),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f3018])).
% 2.51/0.58 thf(f3038,plain,(
% 2.51/0.58 ($true = $false) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1) @ sK0))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1) @ sK0))) | ($false = ((in @ sK3 @ sK0))) | ($false = ((in @ sK3 @ sK0))) | ((^[Y0 : $i]: (sK2)) != (^[Y0 : $i]: (sK2))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (sK3))) | ((^[Y0 : $i]: (sK0)) != (^[Y0 : $i]: (sK0))) | (~spl7_2 | ~spl7_8)),
% 2.51/0.58 inference(constrained_superposition,[],[f124,f3019])).
% 2.51/0.58 thf(f3039,plain,(
% 2.51/0.58 ($true = $false) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1) @ sK0))) | ($false = ((in @ sK3 @ sK0))) | ((^[Y0 : $i]: (sK2)) != (^[Y0 : $i]: (sK2))) | ((^[Y0 : $i]: (sK3)) != (^[Y0 : $i]: (sK3))) | ((^[Y0 : $i]: (sK0)) != (^[Y0 : $i]: (sK0))) | (~spl7_2 | ~spl7_8)),
% 2.51/0.58 inference(duplicate_literal_removal,[],[f3038])).
% 2.51/0.58 thf(f3040,plain,(
% 2.51/0.58 ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1) @ sK0))) | ($false = ((in @ sK3 @ sK0))) | (~spl7_2 | ~spl7_8)),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f3039])).
% 2.51/0.58 thf(f3044,plain,(
% 2.51/0.58 ($false = ((in @ sK3 @ sK0))) | (~spl7_2 | ~spl7_8 | spl7_9)),
% 2.51/0.58 inference(forward_subsumption_resolution,[],[f3040,f1950])).
% 2.51/0.58 thf(f3064,plain,(
% 2.51/0.58 ($true = $false) | (~spl7_2 | ~spl7_8 | spl7_9)),
% 2.51/0.58 inference(constrained_superposition,[],[f3044,f85])).
% 2.51/0.58 thf(f3071,plain,(
% 2.51/0.58 $false | (~spl7_2 | ~spl7_8 | spl7_9)),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f3064])).
% 2.51/0.58 thf(f3072,plain,(
% 2.51/0.58 ~spl7_2 | ~spl7_8 | spl7_9),
% 2.51/0.58 inference(avatar_contradiction_clause,[],[f3071])).
% 2.51/0.58 thf(f3077,plain,(
% 2.51/0.58 ( ! [X0 : $i] : (($false = ((in @ X0 @ sK0))) | ((((^[Y0 : $i]: (Y0)) @ (sK4 @ sK0 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK1))) != X0)) ) | ~spl7_1),
% 2.51/0.58 inference(trivial_inequality_removal,[],[f1819])).
% 2.51/0.58 thf(f3078,plain,(
% 2.51/0.58 ( ! [X0 : $i] : (($false = ((in @ X0 @ sK0))) | (((sK4 @ sK0 @ sK2 @ sK1)) != X0)) ) | ~spl7_1),
% 2.51/0.58 inference(beta-eta_normalization,[],[f3077])).
% 2.51/0.58 thf(f3094,plain,(
% 2.51/0.58 spl7_4 | ~spl7_1),
% 2.51/0.58 inference(avatar_split_clause,[],[f3078,f79,f198])).
% 2.51/0.58 cnf(s1, plain, spl7_1 | spl7_2, inference(sat_conversion,[],[f86])).
% 2.51/0.58 cnf(s2, plain, spl7_1 | spl7_3, inference(sat_conversion,[],[f90])).
% 2.51/0.58 cnf(s5, plain, ~spl7_1 | ~spl7_4, inference(sat_conversion,[],[f1839])).
% 2.51/0.58 cnf(s10, plain, ~spl7_3 | spl7_6 | spl7_7, inference(sat_conversion,[],[f1924])).
% 2.51/0.58 cnf(s18, plain, ~spl7_2 | ~spl7_6 | spl7_7, inference(sat_conversion,[],[f2201])).
% 2.51/0.58 cnf(s21, plain, ~spl7_7 | ~spl7_9, inference(sat_conversion,[],[f2218])).
% 2.51/0.58 cnf(s22, plain, ~spl7_3 | spl7_8 | spl7_9, inference(sat_conversion,[],[f2220])).
% 2.51/0.58 cnf(s24, plain, ~spl7_2 | ~spl7_8 | spl7_9, inference(sat_conversion,[],[f3072])).
% 2.51/0.58 cnf(s26, plain, ~spl7_1 | spl7_4, inference(sat_conversion,[],[f3094])).
% 2.51/0.58 cnf(s37, plain, spl7_9 | spl7_1, inference(rat,[],[s24,s22,s2,s1])).
% 2.51/0.58 cnf(s38, plain, spl7_1, inference(rat,[],[s18,s10,s21,s37,s1,s2])).
% 2.51/0.58 cnf(s40, plain, spl7_4, inference(rat,[],[s26,s38])).
% 2.51/0.58 cnf(s42, plain, $false, inference(rat,[],[s5,s40,s38])).
% 2.51/0.58 thf(f3105,plain,(
% 2.51/0.58 $false),
% 2.51/0.58 inference(avatar_sat_refutation,[],[s42])).
% 2.51/0.58 % SZS output end Proof for theBenchmark
% 2.51/0.58 % (2173038)------------------------------
% 2.51/0.58 % (2173038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.58 % (2173038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.58 % (2173038)CaDiCaL version: 2.1.3
% 2.51/0.58 % (2173038)Termination reason: Refutation
% 2.51/0.58 % (2173038)Time elapsed: 0.333 s
% 2.51/0.58 % (2173038)Peak memory usage: 15 MB
% 2.51/0.58 % (2173038)Instructions burned: 1427 (million)
% 2.51/0.58 % (2173032)Success in time 0.36 s
% 2.51/0.58 % Vampire exiting
%------------------------------------------------------------------------------