%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV064^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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:38:56 AM UTC 2026
% Result : Theorem 1.02s 0.40s
% Output : Refutation 1.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV064^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n018.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 15:08:11 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 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.02/0.40 % (199022)Will run a generic schedule for satisfiability detection.
% 1.02/0.40 % (199032)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1754413621:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.02/0.40 % (199028)% WARNING: option uhcvi not known.
% 1.02/0.40 % (199027)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1947264636_2999 on theBenchmark for (2999ds/0Mi)
% 1.02/0.40 % (199028)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4120670116:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.02/0.40 % (199029)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2479292646:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.02/0.40 % (199030)dis+10_1_sil=32000:sp=arity:random_seed=2845220331:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.02/0.40 % (199028)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.02/0.40 % (199028)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.02/0.40 % Exception at run slice level
% 1.02/0.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.02/0.40 % (199033)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=392498435:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.02/0.40 % (199031)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2652854649:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.02/0.40 % (199031)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.02/0.40 % (199039)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3316967029:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.02/0.40 % Exception at run slice level
% 1.02/0.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.02/0.40 % (199032)Instruction limit reached!
% 1.02/0.40 % (199032)------------------------------
% 1.02/0.40 % (199032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.40 % (199032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.40 % (199032)CaDiCaL version: 2.1.3
% 1.02/0.40 % (199032)Termination reason: Instruction limit
% 1.02/0.40 % (199032)Termination phase: Saturation
% 1.02/0.40 % (199032)Time elapsed: 0.033 s
% 1.02/0.40 % (199032)Peak memory usage: 14 MB
% 1.02/0.40 % (199032)Instructions burned: 135 (million)
% 1.02/0.40 % (199044)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=108289003:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.02/0.40 % (199044)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.02/0.40 % (199044)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.02/0.40 % (199043)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2859142448:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.02/0.40 % (199030)Instruction limit reached!
% 1.02/0.40 % (199030)------------------------------
% 1.02/0.40 % (199030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.40 % (199030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.40 % (199030)CaDiCaL version: 2.1.3
% 1.02/0.40 % (199030)Termination reason: Instruction limit
% 1.02/0.40 % (199030)Termination phase: Saturation
% 1.02/0.40 % (199030)Time elapsed: 0.050 s
% 1.02/0.40 % (199030)Peak memory usage: 12 MB
% 1.02/0.40 % (199030)Instructions burned: 104 (million)
% 1.02/0.40 % (199031)Instruction limit reached!
% 1.02/0.40 % (199031)------------------------------
% 1.02/0.40 % (199031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.40 % (199031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.40 % (199031)CaDiCaL version: 2.1.3
% 1.02/0.40 % (199031)Termination reason: Instruction limit
% 1.02/0.40 % (199031)Termination phase: Saturation
% 1.02/0.40 % (199031)Time elapsed: 0.050 s
% 1.02/0.40 % (199031)Peak memory usage: 12 MB
% 1.02/0.40 % (199031)Instructions burned: 118 (million)
% 1.02/0.40 % (199047)ott-21_1_sil=16000:fs=off:random_seed=2244030019:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.02/0.40 % (199033)Instruction limit reached!
% 1.02/0.40 % (199033)------------------------------
% 1.02/0.40 % (199033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.40 % (199033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.40 % (199033)CaDiCaL version: 2.1.3
% 1.02/0.40 % (199033)Termination reason: Instruction limit
% 1.02/0.40 % (199033)Termination phase: Saturation
% 1.02/0.40 % (199033)Time elapsed: 0.075 s
% 1.02/0.40 % (199033)Peak memory usage: 13 MB
% 1.02/0.40 % (199033)Instructions burned: 161 (million)
% 1.02/0.40 % (199048)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1280875209:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.02/0.40 % (199043)Instruction limit reached!
% 1.02/0.40 % (199043)------------------------------
% 1.02/0.40 % (199043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.40 % (199043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.40 % (199043)CaDiCaL version: 2.1.3
% 1.02/0.40 % (199043)Termination reason: Instruction limit
% 1.02/0.40 % (199043)Termination phase: Saturation
% 1.02/0.40 % (199043)Time elapsed: 0.063 s
% 1.02/0.40 % (199043)Peak memory usage: 13 MB
% 1.02/0.40 % (199043)Instructions burned: 131 (million)
% 1.02/0.40 % (199050)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3890092353:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.02/0.40 % Exception at run slice level
% 1.02/0.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.02/0.40 % (199052)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=62330202:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.02/0.40 % (199054)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=290233814:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.02/0.40 % Exception at run slice level
% 1.02/0.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.02/0.40 % (199028) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-199022-199028"...
% 1.02/0.40 % (199028)...printing done.
% 1.02/0.40 % (199028)Refutation found. Thanks to Tanya!
% 1.02/0.40 % SZS status Theorem for theBenchmark
% 1.02/0.40 % SZS output start Proof for theBenchmark
% 1.02/0.40 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.02/0.40 thf(func_def_3, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.02/0.40 thf(func_def_4, type, sK0: ((($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i > $o)).
% 1.02/0.40 thf(func_def_5, type, sK1: ((($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i > $o)).
% 1.02/0.40 thf(func_def_6, type, sK2: ((($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i > $o)).
% 1.02/0.40 thf(func_def_7, type, sK3: ((($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i)).
% 1.02/0.40 thf(func_def_8, type, sK4: ((($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i > $o)).
% 1.02/0.40 thf(func_def_9, type, sK5: ((($i > $o) > ($i > $o) > $i > $o) > (($i > $o) > ($i > $o) > $i > $o) > $i)).
% 1.02/0.40 thf(func_def_10, type, vNOT: ($o > $o)).
% 1.02/0.40 thf(func_def_11, type, db1: !>[X0: $tType]:(X0)).
% 1.02/0.40 thf(func_def_12, type, db2: !>[X0: $tType]:(X0)).
% 1.02/0.40 thf(func_def_13, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.02/0.40 thf(func_def_14, type, db0: !>[X0: $tType]:(X0)).
% 1.02/0.40 thf(func_def_16, type, sK7: ((($i > $o) > ($i > $o) > $i > $o) > $i)).
% 1.02/0.40 thf(func_def_18, type, sK9: ((($i > $o) > ($i > $o) > $i > $o) > $i)).
% 1.02/0.40 thf(func_def_19, type, db4: !>[X0: $tType]:(X0)).
% 1.02/0.40 thf(func_def_20, type, db3: !>[X0: $tType]:(X0)).
% 1.02/0.40 thf(func_def_22, type, sK11: ((($i > $o) > ($i > $o) > $i > $o) > $i)).
% 1.02/0.40 thf(f1,conjecture,(
% 1.02/0.40 ? [X0 : (($i > $o) > ($i > $o) > $i > $o),X1 : (($i > $o) > ($i > $o) > $i > $o)] : (! [X3 : ($i > $o),X4 : ($i > $o),X5 : ($i > $o)] : ((! [X2 : $i] : ((X0 @ X4 @ X5 @ X2) | (X1 @ X4 @ X5 @ X2)) & ! [X2 : $i] : ((X0 @ X3 @ X4 @ X2) | (X1 @ X3 @ X4 @ X2))) => ! [X2 : $i] : ((X0 @ X3 @ X5 @ X2) | (X1 @ X3 @ X5 @ X2))) & ! [X3 : ($i > $o),X2 : $i] : ((X0 @ X3 @ X3 @ X2) | (X1 @ X3 @ X3 @ X2)) & ~ ! [X2 : $i] : ((X0 @ (^[X3 : $i] : ($true)) @ (^[X3 : $i] : ($false)) @ X2) | (X1 @ (^[X3 : $i] : ($true)) @ (^[X3 : $i] : ($false)) @ X2)))),
% 1.02/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM120C_pme)).
% 1.02/0.40 thf(f2,negated_conjecture,(
% 1.02/0.40 ~ ? [X0 : (($i > $o) > ($i > $o) > $i > $o),X1 : (($i > $o) > ($i > $o) > $i > $o)] : (! [X3 : ($i > $o),X4 : ($i > $o),X5 : ($i > $o)] : ((! [X2 : $i] : ((X0 @ X4 @ X5 @ X2) | (X1 @ X4 @ X5 @ X2)) & ! [X2 : $i] : ((X0 @ X3 @ X4 @ X2) | (X1 @ X3 @ X4 @ X2))) => ! [X2 : $i] : ((X0 @ X3 @ X5 @ X2) | (X1 @ X3 @ X5 @ X2))) & ! [X3 : ($i > $o),X2 : $i] : ((X0 @ X3 @ X3 @ X2) | (X1 @ X3 @ X3 @ X2)) & ~ ! [X2 : $i] : ((X0 @ (^[X3 : $i] : ($true)) @ (^[X3 : $i] : ($false)) @ X2) | (X1 @ (^[X3 : $i] : ($true)) @ (^[X3 : $i] : ($false)) @ X2)))),
% 1.02/0.40 inference(negated_conjecture,[status(cth)],[f1])).
% 1.02/0.40 thf(f3,plain,(
% 1.02/0.40 ~ ? [X0 : (($i > $o) > ($i > $o) > $i > $o),X1 : (($i > $o) > ($i > $o) > $i > $o)] : (! [X2 : ($i > $o),X3 : ($i > $o),X4 : ($i > $o)] : ((! [X5 : $i] : ((X0 @ X3 @ X4 @ X5) | (X1 @ X3 @ X4 @ X5)) & ! [X6 : $i] : ((X0 @ X2 @ X3 @ X6) | (X1 @ X2 @ X3 @ X6))) => ! [X7 : $i] : ((X0 @ X2 @ X4 @ X7) | (X1 @ X2 @ X4 @ X7))) & ! [X8 : ($i > $o),X9 : $i] : ((X0 @ X8 @ X8 @ X9) | (X1 @ X8 @ X8 @ X9)) & ~ ! [X10 : $i] : ((X0 @ (^[X11 : $i] : ($true)) @ (^[X12 : $i] : ($false)) @ X10) | (X1 @ (^[X13 : $i] : ($true)) @ (^[X14 : $i] : ($false)) @ X10)))),
% 1.02/0.40 inference(rectify,[],[f2])).
% 1.02/0.40 thf(f4,plain,(
% 1.02/0.40 ~ ? [X0 : (($i > $o) > ($i > $o) > $i > $o),X1 : (($i > $o) > ($i > $o) > $i > $o)] : (! [X2 : ($i > $o),X3 : ($i > $o),X4 : ($i > $o)] : ((! [X5 : $i] : ((((X0 @ X3 @ X4 @ X5)) = $true) | (((X1 @ X3 @ X4 @ X5)) = $true)) & ! [X6 : $i] : ((((X0 @ X2 @ X3 @ X6)) = $true) | (((X1 @ X2 @ X3 @ X6)) = $true))) => ! [X7 : $i] : ((((X0 @ X2 @ X4 @ X7)) = $true) | (((X1 @ X2 @ X4 @ X7)) = $true))) & ! [X8 : ($i > $o),X9 : $i] : ((((X0 @ X8 @ X8 @ X9)) = $true) | (((X1 @ X8 @ X8 @ X9)) = $true)) & ~ ! [X10 : $i] : (($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))))),
% 1.02/0.40 inference(fool_elimination,[],[f3])).
% 1.02/0.40 thf(f5,plain,(
% 1.02/0.40 ! [X0 : (($i > $o) > ($i > $o) > $i > $o),X1 : (($i > $o) > ($i > $o) > $i > $o)] : (? [X2 : ($i > $o),X3 : ($i > $o),X4 : ($i > $o)] : (? [X7 : $i] : ((((X0 @ X2 @ X4 @ X7)) != $true) & (((X1 @ X2 @ X4 @ X7)) != $true)) & (! [X5 : $i] : ((((X0 @ X3 @ X4 @ X5)) = $true) | (((X1 @ X3 @ X4 @ X5)) = $true)) & ! [X6 : $i] : ((((X0 @ X2 @ X3 @ X6)) = $true) | (((X1 @ X2 @ X3 @ X6)) = $true)))) | ? [X8 : ($i > $o),X9 : $i] : ((((X0 @ X8 @ X8 @ X9)) != $true) & (((X1 @ X8 @ X8 @ X9)) != $true)) | ! [X10 : $i] : (($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))))),
% 1.02/0.40 inference(ennf_transformation,[],[f4])).
% 1.02/0.40 thf(f6,plain,(
% 1.02/0.40 ! [X0 : (($i > $o) > ($i > $o) > $i > $o),X1 : (($i > $o) > ($i > $o) > $i > $o)] : (? [X2 : ($i > $o),X3 : ($i > $o),X4 : ($i > $o)] : (? [X7 : $i] : ((((X0 @ X2 @ X4 @ X7)) != $true) & (((X1 @ X2 @ X4 @ X7)) != $true)) & ! [X5 : $i] : ((((X0 @ X3 @ X4 @ X5)) = $true) | (((X1 @ X3 @ X4 @ X5)) = $true)) & ! [X6 : $i] : ((((X0 @ X2 @ X3 @ X6)) = $true) | (((X1 @ X2 @ X3 @ X6)) = $true))) | ? [X8 : ($i > $o),X9 : $i] : ((((X0 @ X8 @ X8 @ X9)) != $true) & (((X1 @ X8 @ X8 @ X9)) != $true)) | ! [X10 : $i] : (($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))))),
% 1.02/0.40 inference(flattening,[],[f5])).
% 1.02/0.40 thf(f7,plain,(
% 1.02/0.40 ! [X0 : (($i > $o) > ($i > $o) > $i > $o),X1 : (($i > $o) > ($i > $o) > $i > $o)] : (? [X2 : ($i > $o),X3 : ($i > $o),X4 : ($i > $o)] : (? [X5 : $i] : (($true != ((X0 @ X2 @ X4 @ X5))) & ($true != ((X1 @ X2 @ X4 @ X5)))) & ! [X6 : $i] : (($true = ((X0 @ X3 @ X4 @ X6))) | ($true = ((X1 @ X3 @ X4 @ X6)))) & ! [X7 : $i] : (($true = ((X0 @ X2 @ X3 @ X7))) | ($true = ((X1 @ X2 @ X3 @ X7))))) | ? [X8 : ($i > $o),X9 : $i] : ((((X0 @ X8 @ X8 @ X9)) != $true) & (((X1 @ X8 @ X8 @ X9)) != $true)) | ! [X10 : $i] : (($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))))),
% 1.02/0.40 inference(rectify,[],[f6])).
% 1.02/0.40 thf(f8,plain,(
% 1.02/0.40 ! [X0 : (($i > $o) > ($i > $o) > $i > $o),X1 : (($i > $o) > ($i > $o) > $i > $o)] : (((($true != ((X0 @ (sK0 @ X1 @ X0) @ (sK2 @ X1 @ X0) @ (sK3 @ X1 @ X0)))) & ($true != ((X1 @ (sK0 @ X1 @ X0) @ (sK2 @ X1 @ X0) @ (sK3 @ X1 @ X0))))) & ! [X6 : $i] : (($true = ((X0 @ (sK1 @ X1 @ X0) @ (sK2 @ X1 @ X0) @ X6))) | ($true = ((X1 @ (sK1 @ X1 @ X0) @ (sK2 @ X1 @ X0) @ X6)))) & ! [X7 : $i] : (($true = ((X0 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X7))) | ($true = ((X1 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X7))))) | (($true != ((X0 @ (sK4 @ X1 @ X0) @ (sK4 @ X1 @ X0) @ (sK5 @ X1 @ X0)))) & ($true != ((X1 @ (sK4 @ X1 @ X0) @ (sK4 @ X1 @ X0) @ (sK5 @ X1 @ X0))))) | ! [X10 : $i] : (($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))))),
% 1.02/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP,vAPP,vAPP,vAPP]),skolemize(X9,sK5 @ X1 @ X0),skolemize(X9,sK5 @ X1 @ X0),skolemize(X9,sK5 @ X1 @ X0),skolemize(X9,sK5 @ X1 @ X0),skolemize(X9,sK5 @ X1 @ X0),skolemize(X9,sK5 @ X1 @ X0)],[f7])).
% 1.02/0.40 thf(f9,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X1 : (($i > $o) > ($i > $o) > $i > $o),X7 : $i] : (($true != ((X1 @ (sK4 @ X1 @ X0) @ (sK4 @ X1 @ X0) @ (sK5 @ X1 @ X0)))) | ($true = ((X1 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X7))) | ($true = ((X0 @ (sK0 @ X1 @ X0) @ (sK1 @ X1 @ X0) @ X7))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))) )),
% 1.02/0.40 inference(cnf_transformation,[],[f8])).
% 1.02/0.40 thf(f11,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X1 : (($i > $o) > ($i > $o) > $i > $o),X6 : $i] : (($true != ((X1 @ (sK4 @ X1 @ X0) @ (sK4 @ X1 @ X0) @ (sK5 @ X1 @ X0)))) | ($true = ((X1 @ (sK1 @ X1 @ X0) @ (sK2 @ X1 @ X0) @ X6))) | ($true = ((X0 @ (sK1 @ X1 @ X0) @ (sK2 @ X1 @ X0) @ X6))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))) )),
% 1.02/0.40 inference(cnf_transformation,[],[f8])).
% 1.02/0.40 thf(f13,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X1 : (($i > $o) > ($i > $o) > $i > $o)] : (($true != ((X1 @ (sK4 @ X1 @ X0) @ (sK4 @ X1 @ X0) @ (sK5 @ X1 @ X0)))) | ($true != ((X1 @ (sK0 @ X1 @ X0) @ (sK2 @ X1 @ X0) @ (sK3 @ X1 @ X0)))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = ((X1 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))) )),
% 1.02/0.40 inference(cnf_transformation,[],[f8])).
% 1.02/0.40 thf(f26,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o)] : (($true != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK3 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))) )),
% 1.02/0.40 inference(primitive_instantiation,[],[f13])).
% 1.02/0.40 thf(f52,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o)] : (($true != (((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) = (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true != (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) = (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))))) )),
% 1.02/0.40 inference(beta-eta_normalization,[],[f26])).
% 1.02/0.40 thf(f53,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o)] : ((((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true != (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) = (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))))) )),
% 1.02/0.40 inference(equality_proxy_clausification,[],[f52])).
% 1.02/0.40 thf(f54,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o)] : ((((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))))) )),
% 1.02/0.40 inference(equality_proxy_clausification,[],[f53])).
% 1.02/0.40 thf(f55,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o)] : ((((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))) )),
% 1.02/0.40 inference(equality_proxy_clausification,[],[f54])).
% 1.02/0.40 thf(f56,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o)] : ((((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))) )),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f55])).
% 1.02/0.40 thf(f58,definition,(
% 1.02/0.40 spl6_1 <=> ((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition])).
% 1.02/0.40 thf(f59,plain,(
% 1.02/0.40 ((^[Y0 : $i]: ($true)) != (^[Y0 : $i]: ($false))) | spl6_1),
% 1.02/0.40 inference(avatar_component_clause,[],[f58])).
% 1.02/0.40 thf(f60,plain,(
% 1.02/0.40 ((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false))) | ~spl6_1),
% 1.02/0.40 inference(avatar_component_clause,[],[f58])).
% 1.02/0.40 thf(f62,definition,(
% 1.02/0.40 spl6_2 <=> ! [X0 : (($i > $o) > ($i > $o) > $i > $o),X10 : $i] : ((((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))))),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition])).
% 1.02/0.40 thf(f63,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o)] : ((((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))) ) | ~spl6_2),
% 1.02/0.40 inference(avatar_component_clause,[],[f62])).
% 1.02/0.40 thf(f64,plain,(
% 1.02/0.40 spl6_1 | spl6_2),
% 1.02/0.40 inference(avatar_split_clause,[],[f56,f62,f58])).
% 1.02/0.40 thf(f165,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X7 : $i] : (($true != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X7))) | ($true = ((X0 @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X7))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))) )),
% 1.02/0.40 inference(primitive_instantiation,[],[f9])).
% 1.02/0.40 thf(f193,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X7 : $i] : (($true != (((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) = (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true = (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) = (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true = ((X0 @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X7))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))))) )),
% 1.02/0.40 inference(beta-eta_normalization,[],[f165])).
% 1.02/0.40 thf(f194,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X7 : $i] : ((((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) = (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true = ((X0 @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X7))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))))) )),
% 1.02/0.40 inference(equality_proxy_clausification,[],[f193])).
% 1.02/0.40 thf(f195,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X7 : $i] : ((((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X7))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))))) )),
% 1.02/0.40 inference(equality_proxy_clausification,[],[f194])).
% 1.02/0.40 thf(f196,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X7 : $i] : ((((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X7))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))) )),
% 1.02/0.40 inference(equality_proxy_clausification,[],[f195])).
% 1.02/0.40 thf(f197,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X7 : $i] : ((((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X7))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))) )),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f196])).
% 1.02/0.40 thf(f198,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X7 : $i] : ((((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X7))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))) ) | spl6_1),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f197,f59])).
% 1.02/0.40 thf(f373,definition,(
% 1.02/0.40 spl6_18 <=> ! [X0 : (($i > $o) > ($i > $o) > $i > $o),X7 : $i,X10 : $i] : ((((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = ((X0 @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X7))))),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl6_18])],[avatar_definition])).
% 1.02/0.40 thf(f374,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X7 : $i] : (($true = ((X0 @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X7))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) ) | ~spl6_18),
% 1.02/0.40 inference(avatar_component_clause,[],[f373])).
% 1.02/0.40 thf(f380,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X6 : $i] : (($true != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X6))) | ($true = ((X0 @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X6))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10)))) )),
% 1.02/0.40 inference(primitive_instantiation,[],[f11])).
% 1.02/0.40 thf(f408,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X6 : $i] : (($true != (((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) = (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true = (((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) = (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true = ((X0 @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X6))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))))) )),
% 1.02/0.40 inference(beta-eta_normalization,[],[f380])).
% 1.02/0.40 thf(f409,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X6 : $i] : ((((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = (((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) = (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) | ($true = ((X0 @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X6))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))))) )),
% 1.02/0.40 inference(equality_proxy_clausification,[],[f408])).
% 1.02/0.40 thf(f410,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X6 : $i] : ((((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | (((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X6))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = (((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))))) )),
% 1.02/0.40 inference(equality_proxy_clausification,[],[f409])).
% 1.02/0.40 thf(f411,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X6 : $i] : ((((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) != ((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | (((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X6))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))) )),
% 1.02/0.40 inference(equality_proxy_clausification,[],[f410])).
% 1.02/0.40 thf(f412,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X6 : $i] : ((((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X6))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: ($false)))) )),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f411])).
% 1.02/0.40 thf(f414,definition,(
% 1.02/0.40 spl6_20 <=> ! [X6 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X10 : $i] : ((((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | ($true = ((X0 @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X6))))),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl6_20])],[avatar_definition])).
% 1.02/0.40 thf(f415,plain,(
% 1.02/0.40 ( ! [X10 : $i,X0 : (($i > $o) > ($i > $o) > $i > $o),X6 : $i] : (($true = ((X0 @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0) @ X6))) | ($true = ((X0 @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | (((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ X0)))) ) | ~spl6_20),
% 1.02/0.40 inference(avatar_component_clause,[],[f414])).
% 1.02/0.40 thf(f416,plain,(
% 1.02/0.40 spl6_1 | spl6_20),
% 1.02/0.40 inference(avatar_split_clause,[],[f412,f414,f58])).
% 1.02/0.40 thf(f417,plain,(
% 1.02/0.40 ( ! [X1 : $i] : (((((^[Y0 : $i]: ($true)) @ X1)) = (((^[Y0 : $i]: ($false)) @ X1)))) ) | ~spl6_1),
% 1.02/0.40 inference(argument_congruence,[],[f60])).
% 1.02/0.40 thf(f419,plain,(
% 1.02/0.40 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ($true)) @ X1))) | ($true = (((^[Y0 : $i]: ($false)) @ X1)))) ) | ~spl6_1),
% 1.02/0.40 inference(iff_proxy_clausification,[],[f417])).
% 1.02/0.40 thf(f420,plain,(
% 1.02/0.40 ($true = $false) | ($true = $false) | ~spl6_1),
% 1.02/0.40 inference(beta-eta_normalization,[],[f419])).
% 1.02/0.40 thf(f421,plain,(
% 1.02/0.40 ($true = $false) | ~spl6_1),
% 1.02/0.40 inference(duplicate_literal_removal,[],[f420])).
% 1.02/0.40 thf(f422,plain,(
% 1.02/0.40 $false | ~spl6_1),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f421])).
% 1.02/0.40 thf(f423,plain,(
% 1.02/0.40 ~spl6_1),
% 1.02/0.40 inference(avatar_contradiction_clause,[],[f422])).
% 1.02/0.40 thf(f530,plain,(
% 1.02/0.40 spl6_18 | spl6_1),
% 1.02/0.40 inference(avatar_split_clause,[],[f198,f58,f373])).
% 1.02/0.40 thf(f742,plain,(
% 1.02/0.40 ( ! [X10 : $i,X7 : $i] : (($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))) @ X7))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))))) ) | ~spl6_18),
% 1.02/0.40 inference(primitive_instantiation,[],[f374])).
% 1.02/0.40 thf(f857,plain,(
% 1.02/0.40 ($true = $false) | ($true = $false) | (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))))) | ~spl6_18),
% 1.02/0.40 inference(beta-eta_normalization,[],[f742])).
% 1.02/0.40 thf(f858,plain,(
% 1.02/0.40 ($true = $false) | (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))))) | ~spl6_18),
% 1.02/0.40 inference(duplicate_literal_removal,[],[f857])).
% 1.02/0.40 thf(f859,plain,(
% 1.02/0.40 (((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))))) | ~spl6_18),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f858])).
% 1.02/0.40 thf(f1118,plain,(
% 1.02/0.40 ( ! [X10 : $i,X6 : $i] : (($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))) @ (sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))) @ X6))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X10))) | (((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))))) ) | ~spl6_20),
% 1.02/0.40 inference(primitive_instantiation,[],[f415])).
% 1.02/0.40 thf(f1237,plain,(
% 1.02/0.40 ($true = $false) | ($true = $false) | (((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))))) | ~spl6_20),
% 1.02/0.40 inference(beta-eta_normalization,[],[f1118])).
% 1.02/0.40 thf(f1238,plain,(
% 1.02/0.40 ($true = $false) | (((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))))) | ~spl6_20),
% 1.02/0.40 inference(duplicate_literal_removal,[],[f1237])).
% 1.02/0.40 thf(f1239,plain,(
% 1.02/0.40 (((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))) = ((sK1 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))))) | ~spl6_20),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f1238])).
% 1.02/0.40 thf(f1294,plain,(
% 1.02/0.40 (((sK2 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))) = ((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))))) | (~spl6_18 | ~spl6_20)),
% 1.02/0.40 inference(forward_demodulation,[],[f1239,f859])).
% 1.02/0.40 thf(f1497,plain,(
% 1.02/0.40 ( ! [X0 : $i] : ((((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))))) != ((sK0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (Y0 = Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false))))))))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X0)))) ) | (~spl6_2 | ~spl6_18 | ~spl6_20)),
% 1.02/0.40 inference(constrained_superposition,[],[f63,f1294])).
% 1.02/0.40 thf(f1498,plain,(
% 1.02/0.40 ( ! [X0 : $i] : (($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ($false)))))) @ (^[Y0 : $i]: ($true)) @ (^[Y0 : $i]: ($false)) @ X0)))) ) | (~spl6_2 | ~spl6_18 | ~spl6_20)),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f1497])).
% 1.02/0.40 thf(f1499,plain,(
% 1.02/0.40 ($true = $false) | (~spl6_2 | ~spl6_18 | ~spl6_20)),
% 1.02/0.40 inference(beta-eta_normalization,[],[f1498])).
% 1.02/0.40 thf(f1500,plain,(
% 1.02/0.40 $false | (~spl6_2 | ~spl6_18 | ~spl6_20)),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f1499])).
% 1.02/0.40 thf(f1501,plain,(
% 1.02/0.40 ~spl6_2 | ~spl6_18 | ~spl6_20),
% 1.02/0.40 inference(avatar_contradiction_clause,[],[f1500])).
% 1.02/0.40 cnf(s1, plain, spl6_1 | spl6_2, inference(sat_conversion,[],[f64])).
% 1.02/0.40 cnf(s16, plain, spl6_1 | spl6_20, inference(sat_conversion,[],[f416])).
% 1.02/0.40 cnf(s17, plain, ~spl6_1, inference(sat_conversion,[],[f423])).
% 1.02/0.40 cnf(s18, plain, spl6_1 | spl6_18, inference(sat_conversion,[],[f530])).
% 1.02/0.40 cnf(s142, plain, ~spl6_2 | ~spl6_18 | ~spl6_20, inference(sat_conversion,[],[f1501])).
% 1.02/0.40 cnf(s144, plain, spl6_18, inference(rat,[],[s18,s17])).
% 1.02/0.40 cnf(s145, plain, spl6_20, inference(rat,[],[s16,s17])).
% 1.02/0.40 cnf(s146, plain, ~spl6_2, inference(rat,[],[s142,s144,s145])).
% 1.02/0.40 cnf(s150, plain, $false, inference(rat,[],[s1,s146,s17])).
% 1.02/0.40 thf(f1511,plain,(
% 1.02/0.40 $false),
% 1.02/0.40 inference(avatar_sat_refutation,[],[s150])).
% 1.02/0.40 % SZS output end Proof for theBenchmark
% 1.02/0.40 % (199028)------------------------------
% 1.02/0.40 % (199028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.40 % (199028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.40 % (199028)CaDiCaL version: 2.1.3
% 1.02/0.40 % (199028)Termination reason: Refutation
% 1.02/0.40 % (199028)Time elapsed: 0.143 s
% 1.02/0.40 % (199028)Peak memory usage: 14 MB
% 1.02/0.40 % (199028)Instructions burned: 323 (million)
% 1.02/0.40 % (199022)Success in time 0.191 s
% 1.02/0.40 % Vampire exiting
%------------------------------------------------------------------------------