%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV058^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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 0.60s 0.27s
% Output : Refutation 0.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEV058^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Tue Sep 29 15:05:18 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.13 Running first-order model finding
% 0.10/0.13 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.60/0.27 % (223285)Will run a generic schedule for satisfiability detection.
% 0.60/0.27 % (223293)dis+10_1_sil=32000:sp=arity:random_seed=1864237109:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.60/0.27 % (223292)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4285903823:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.60/0.27 % (223290)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4238067904_2999 on theBenchmark for (2999ds/0Mi)
% 0.60/0.27 % (223295)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3489236359:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.60/0.27 % Exception at run slice level
% 0.60/0.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.60/0.27 % (223291)% WARNING: option uhcvi not known.
% 0.60/0.27 % (223291)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=40815763:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.60/0.27 % (223291)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.60/0.27 % (223291)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.60/0.27 % (223294)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=807974993:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.60/0.27 % (223301)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=576961432:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.60/0.27 % (223296)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3998994313:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.60/0.27 % Exception at run slice level
% 0.60/0.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.60/0.27 % (223294)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.60/0.27 % (223306)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3681172568:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.60/0.27 % (223293)Instruction limit reached!
% 0.60/0.27 % (223293)------------------------------
% 0.60/0.27 % (223293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.27 % (223293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.27 % (223293)CaDiCaL version: 2.1.3
% 0.60/0.27 % (223293)Termination reason: Instruction limit
% 0.60/0.27 % (223293)Termination phase: Saturation
% 0.60/0.27 % (223293)Time elapsed: 0.026 s
% 0.60/0.27 % (223293)Peak memory usage: 12 MB
% 0.60/0.27 % (223293)Instructions burned: 105 (million)
% 0.60/0.27 % (223295)Instruction limit reached!
% 0.60/0.27 % (223295)------------------------------
% 0.60/0.27 % (223295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.27 % (223295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.27 % (223295)CaDiCaL version: 2.1.3
% 0.60/0.27 % (223295)Termination reason: Instruction limit
% 0.60/0.27 % (223295)Termination phase: Saturation
% 0.60/0.27 % (223295)Time elapsed: 0.032 s
% 0.60/0.27 % (223295)Peak memory usage: 13 MB
% 0.60/0.27 % (223295)Instructions burned: 133 (million)
% 0.60/0.27 % (223308)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=1214790527:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.60/0.27 % (223308)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.60/0.27 % (223308)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.60/0.27 % (223309)ott-21_1_sil=16000:fs=off:random_seed=834916796:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.60/0.27 % (223306)Instruction limit reached!
% 0.60/0.27 % (223306)------------------------------
% 0.60/0.27 % (223306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.27 % (223306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.27 % (223306)CaDiCaL version: 2.1.3
% 0.60/0.27 % (223306)Termination reason: Instruction limit
% 0.60/0.27 % (223306)Termination phase: Saturation
% 0.60/0.27 % (223306)Time elapsed: 0.033 s
% 0.60/0.27 % (223306)Peak memory usage: 13 MB
% 0.60/0.27 % (223306)Instructions burned: 134 (million)
% 0.60/0.27 % (223312)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=583529445:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 0.60/0.27 % (223294)Instruction limit reached!
% 0.60/0.27 % (223294)------------------------------
% 0.60/0.27 % (223294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.27 % (223294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.27 % (223294)CaDiCaL version: 2.1.3
% 0.60/0.27 % (223294)Termination reason: Instruction limit
% 0.60/0.27 % (223294)Termination phase: Saturation
% 0.60/0.27 % (223294)Time elapsed: 0.060 s
% 0.60/0.27 % (223294)Peak memory usage: 13 MB
% 0.60/0.27 % (223294)Instructions burned: 119 (million)
% 0.60/0.27 % (223296)Instruction limit reached!
% 0.60/0.27 % (223296)------------------------------
% 0.60/0.27 % (223296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.27 % (223296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.27 % (223296)CaDiCaL version: 2.1.3
% 0.60/0.27 % (223296)Termination reason: Instruction limit
% 0.60/0.27 % (223296)Termination phase: Saturation
% 0.60/0.27 % (223296)Time elapsed: 0.074 s
% 0.60/0.27 % (223296)Peak memory usage: 13 MB
% 0.60/0.27 % (223296)Instructions burned: 162 (million)
% 0.60/0.27 % (223314)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=678666815:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 0.60/0.27 % Exception at run slice level
% 0.60/0.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.60/0.27 % (223315)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2233579280:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 0.60/0.27 % (223317)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3761698461:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 0.60/0.27 % Exception at run slice level
% 0.60/0.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.60/0.27 % (223309)Instruction limit reached!
% 0.60/0.27 % (223309)------------------------------
% 0.60/0.27 % (223309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.27 % (223309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.27 % (223309)CaDiCaL version: 2.1.3
% 0.60/0.27 % (223309)Termination reason: Instruction limit
% 0.60/0.27 % (223309)Termination phase: Saturation
% 0.60/0.27 % (223309)Time elapsed: 0.064 s
% 0.60/0.27 % (223309)Peak memory usage: 12 MB
% 0.60/0.27 % (223309)Instructions burned: 181 (million)
% 0.60/0.27 % (223291) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-223285-223291"...
% 0.60/0.27 % (223291)...printing done.
% 0.60/0.27 % (223291)Refutation found. Thanks to Tanya!
% 0.60/0.27 % SZS status Theorem for theBenchmark
% 0.60/0.27 % SZS output start Proof for theBenchmark
% 0.60/0.27 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.60/0.27 thf(func_def_3, type, sP0: ((($i > $o) > ($i > $o) > $o) > $o)).
% 0.60/0.27 thf(func_def_4, type, sK1: ((($i > $o) > ($i > $o) > $o) > $i > $o)).
% 0.60/0.27 thf(func_def_5, type, sK2: ((($i > $o) > ($i > $o) > $o) > $i > $o)).
% 0.60/0.27 thf(func_def_6, type, sK3: ((($i > $o) > ($i > $o) > $o) > $i)).
% 0.60/0.27 thf(func_def_7, type, sK4: ((($i > $o) > ($i > $o) > $o) > $i > $o)).
% 0.60/0.27 thf(func_def_8, type, sK5: ((($i > $o) > ($i > $o) > $o) > $i > $o)).
% 0.60/0.27 thf(func_def_9, type, sK6: ((($i > $o) > ($i > $o) > $o) > $i > $o)).
% 0.60/0.27 thf(func_def_10, type, sK7: ((($i > $o) > ($i > $o) > $o) > $i > $o)).
% 0.60/0.27 thf(func_def_11, type, vNOT: ($o > $o)).
% 0.60/0.27 thf(func_def_12, type, db0: !>[X0: $tType]:(X0)).
% 0.60/0.27 thf(func_def_13, type, db1: !>[X0: $tType]:(X0)).
% 0.60/0.27 thf(func_def_14, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.60/0.27 thf(func_def_15, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.60/0.27 thf(func_def_17, type, db2: !>[X0: $tType]:(X0)).
% 0.60/0.27 thf(func_def_18, type, db3: !>[X0: $tType]:(X0)).
% 0.60/0.27 thf(func_def_19, type, db4: !>[X0: $tType]:(X0)).
% 0.60/0.27 thf(f1,conjecture,(
% 0.60/0.27 ? [X0 : (($i > $o) > ($i > $o) > $o)] : (! [X4 : ($i > $o),X5 : ($i > $o),X3 : ($i > $o)] : (((X0 @ X5 @ X3) & (X0 @ X4 @ X5)) => (X0 @ X4 @ X3)) & ! [X4 : ($i > $o)] : (X0 @ X4 @ X4) & ! [X1 : ($i > $o),X2 : ($i > $o)] : ((X0 @ X1 @ X2) => ! [X3 : $i] : ((X1 @ X3) => (X2 @ X3))))),
% 0.60/0.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM122_pme)).
% 0.60/0.27 thf(f2,negated_conjecture,(
% 0.60/0.27 ~ ? [X0 : (($i > $o) > ($i > $o) > $o)] : (! [X4 : ($i > $o),X5 : ($i > $o),X3 : ($i > $o)] : (((X0 @ X5 @ X3) & (X0 @ X4 @ X5)) => (X0 @ X4 @ X3)) & ! [X4 : ($i > $o)] : (X0 @ X4 @ X4) & ! [X1 : ($i > $o),X2 : ($i > $o)] : ((X0 @ X1 @ X2) => ! [X3 : $i] : ((X1 @ X3) => (X2 @ X3))))),
% 0.60/0.27 inference(negated_conjecture,[status(cth)],[f1])).
% 0.60/0.27 thf(f3,plain,(
% 0.60/0.27 ~ ? [X0 : (($i > $o) > ($i > $o) > $o)] : (! [X1 : ($i > $o),X2 : ($i > $o),X3 : ($i > $o)] : (((X0 @ X2 @ X3) & (X0 @ X1 @ X2)) => (X0 @ X1 @ X3)) & ! [X4 : ($i > $o)] : (X0 @ X4 @ X4) & ! [X5 : ($i > $o),X6 : ($i > $o)] : ((X0 @ X5 @ X6) => ! [X7 : $i] : ((X5 @ X7) => (X6 @ X7))))),
% 0.60/0.27 inference(rectify,[],[f2])).
% 0.60/0.27 thf(f4,plain,(
% 0.60/0.27 ~ ? [X0 : (($i > $o) > ($i > $o) > $o)] : (! [X1 : ($i > $o),X2 : ($i > $o),X3 : ($i > $o)] : (((((X0 @ X2 @ X3)) = $true) & (((X0 @ X1 @ X2)) = $true)) => (((X0 @ X1 @ X3)) = $true)) & ! [X4 : ($i > $o)] : (((X0 @ X4 @ X4)) = $true) & ! [X5 : ($i > $o),X6 : ($i > $o)] : ((((X0 @ X5 @ X6)) = $true) => ! [X7 : $i] : ((((X5 @ X7)) = $true) => (((X6 @ X7)) = $true))))),
% 0.60/0.27 inference(fool_elimination,[],[f3])).
% 0.60/0.27 thf(f5,plain,(
% 0.60/0.27 ! [X0 : (($i > $o) > ($i > $o) > $o)] : (? [X1 : ($i > $o),X2 : ($i > $o),X3 : ($i > $o)] : ((((X0 @ X1 @ X3)) != $true) & ((((X0 @ X2 @ X3)) = $true) & (((X0 @ X1 @ X2)) = $true))) | ? [X4 : ($i > $o)] : (((X0 @ X4 @ X4)) != $true) | ? [X5 : ($i > $o),X6 : ($i > $o)] : (? [X7 : $i] : ((((X6 @ X7)) != $true) & (((X5 @ X7)) = $true)) & (((X0 @ X5 @ X6)) = $true)))),
% 0.60/0.27 inference(ennf_transformation,[],[f4])).
% 0.60/0.27 thf(f6,plain,(
% 0.60/0.27 ! [X0 : (($i > $o) > ($i > $o) > $o)] : (? [X1 : ($i > $o),X2 : ($i > $o),X3 : ($i > $o)] : ((((X0 @ X1 @ X3)) != $true) & (((X0 @ X2 @ X3)) = $true) & (((X0 @ X1 @ X2)) = $true)) | ? [X4 : ($i > $o)] : (((X0 @ X4 @ X4)) != $true) | ? [X5 : ($i > $o),X6 : ($i > $o)] : (? [X7 : $i] : ((((X6 @ X7)) != $true) & (((X5 @ X7)) = $true)) & (((X0 @ X5 @ X6)) = $true)))),
% 0.60/0.27 inference(flattening,[],[f5])).
% 0.60/0.27 thf(f7,definition,(
% 0.60/0.27 ! [X0 : (($i > $o) > ($i > $o) > $o)] : (? [X5 : ($i > $o),X6 : ($i > $o)] : (? [X7 : $i] : ((((X6 @ X7)) != $true) & (((X5 @ X7)) = $true)) & (((X0 @ X5 @ X6)) = $true)) | ~ ($true = ((sP0 @ X0))))),
% 0.60/0.27 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 0.60/0.27 thf(f8,plain,(
% 0.60/0.27 ! [X0 : (($i > $o) > ($i > $o) > $o)] : (? [X1 : ($i > $o),X2 : ($i > $o),X3 : ($i > $o)] : ((((X0 @ X1 @ X3)) != $true) & (((X0 @ X2 @ X3)) = $true) & (((X0 @ X1 @ X2)) = $true)) | ? [X4 : ($i > $o)] : (((X0 @ X4 @ X4)) != $true) | ($true = ((sP0 @ X0))))),
% 0.60/0.27 inference(definition_folding,[],[f6,f7])).
% 0.60/0.27 thf(f9,plain,(
% 0.60/0.27 ! [X0 : (($i > $o) > ($i > $o) > $o)] : (? [X5 : ($i > $o),X6 : ($i > $o)] : (? [X7 : $i] : ((((X6 @ X7)) != $true) & (((X5 @ X7)) = $true)) & (((X0 @ X5 @ X6)) = $true)) | ($true != ((sP0 @ X0))))),
% 0.60/0.27 inference(nnf_transformation,[],[f7])).
% 0.60/0.27 thf(f10,plain,(
% 0.60/0.27 ! [X0 : (($i > $o) > ($i > $o) > $o)] : (? [X1 : ($i > $o),X2 : ($i > $o)] : (? [X3 : $i] : ((((X2 @ X3)) != $true) & (((X1 @ X3)) = $true)) & (((X0 @ X1 @ X2)) = $true)) | ($true != ((sP0 @ X0))))),
% 0.60/0.27 inference(rectify,[],[f9])).
% 0.60/0.27 thf(f11,plain,(
% 0.60/0.27 ! [X0 : (($i > $o) > ($i > $o) > $o)] : (((($true != ((sK2 @ X0 @ (sK3 @ X0)))) & ($true = ((sK1 @ X0 @ (sK3 @ X0))))) & ($true = ((X0 @ (sK1 @ X0) @ (sK2 @ X0))))) | ($true != ((sP0 @ X0))))),
% 0.60/0.27 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP]),skolemize(X3,sK3 @ X0),skolemize(X3,sK3 @ X0),skolemize(X3,sK3 @ X0)],[f10])).
% 0.60/0.27 thf(f12,plain,(
% 0.60/0.27 ! [X0 : (($i > $o) > ($i > $o) > $o)] : ((($true != ((X0 @ (sK4 @ X0) @ (sK6 @ X0)))) & ($true = ((X0 @ (sK5 @ X0) @ (sK6 @ X0)))) & ($true = ((X0 @ (sK4 @ X0) @ (sK5 @ X0))))) | ($true != ((X0 @ (sK7 @ X0) @ (sK7 @ X0)))) | ($true = ((sP0 @ X0))))),
% 0.60/0.27 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP,vAPP]),skolemize(X3,sK3 @ X0),skolemize(X3,sK3 @ X0),skolemize(X3,sK3 @ X0),skolemize(X3,sK3 @ X0)],[f8])).
% 0.60/0.27 thf(f13,plain,(
% 0.60/0.27 ( ! [X0 : (($i > $o) > ($i > $o) > $o)] : (($true != ((sP0 @ X0))) | ($true = ((X0 @ (sK1 @ X0) @ (sK2 @ X0))))) )),
% 0.60/0.27 inference(cnf_transformation,[],[f11])).
% 0.60/0.27 thf(f14,plain,(
% 0.60/0.27 ( ! [X0 : (($i > $o) > ($i > $o) > $o)] : (($true != ((sP0 @ X0))) | ($true = ((sK1 @ X0 @ (sK3 @ X0))))) )),
% 0.60/0.27 inference(cnf_transformation,[],[f11])).
% 0.60/0.27 thf(f15,plain,(
% 0.60/0.27 ( ! [X0 : (($i > $o) > ($i > $o) > $o)] : (($true != ((sK2 @ X0 @ (sK3 @ X0)))) | ($true != ((sP0 @ X0)))) )),
% 0.60/0.27 inference(cnf_transformation,[],[f11])).
% 0.60/0.27 thf(f16,plain,(
% 0.60/0.27 ( ! [X0 : (($i > $o) > ($i > $o) > $o)] : (($true != ((X0 @ (sK7 @ X0) @ (sK7 @ X0)))) | ($true = ((X0 @ (sK4 @ X0) @ (sK5 @ X0)))) | ($true = ((sP0 @ X0)))) )),
% 0.60/0.27 inference(cnf_transformation,[],[f12])).
% 0.60/0.27 thf(f17,plain,(
% 0.60/0.27 ( ! [X0 : (($i > $o) > ($i > $o) > $o)] : (($true != ((X0 @ (sK7 @ X0) @ (sK7 @ X0)))) | ($true = ((X0 @ (sK5 @ X0) @ (sK6 @ X0)))) | ($true = ((sP0 @ X0)))) )),
% 0.60/0.27 inference(cnf_transformation,[],[f12])).
% 0.60/0.27 thf(f18,plain,(
% 0.60/0.27 ( ! [X0 : (($i > $o) > ($i > $o) > $o)] : (($true != ((X0 @ (sK7 @ X0) @ (sK7 @ X0)))) | ($true != ((X0 @ (sK4 @ X0) @ (sK6 @ X0)))) | ($true = ((sP0 @ X0)))) )),
% 0.60/0.27 inference(cnf_transformation,[],[f12])).
% 0.60/0.27 thf(f20,definition,(
% 0.60/0.27 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.60/0.27 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.60/0.27 thf(f28,plain,(
% 0.60/0.27 ($true != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1)))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1)))))))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1)))) @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1))))) @ (sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1)))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1)))))))),
% 0.60/0.27 inference(primitive_instantiation,[],[f16])).
% 0.60/0.27 thf(f49,plain,(
% 0.60/0.27 ($true != (((sK7 @ =) = (sK7 @ =)))) | ($true = (((sK4 @ =) = (sK5 @ =)))) | ($true = ((sP0 @ =)))),
% 0.60/0.27 inference(beta-eta_normalization,[],[f28])).
% 0.60/0.27 thf(f50,plain,(
% 0.60/0.27 (((sK7 @ =)) != ((sK7 @ =))) | ($true = (((sK4 @ =) = (sK5 @ =)))) | ($true = ((sP0 @ =)))),
% 0.60/0.27 inference(equality_proxy_clausification,[],[f49])).
% 0.60/0.27 thf(f51,plain,(
% 0.60/0.27 (((sK7 @ =)) != ((sK7 @ =))) | (((sK5 @ =)) = ((sK4 @ =))) | ($true = ((sP0 @ =)))),
% 0.60/0.27 inference(equality_proxy_clausification,[],[f50])).
% 0.60/0.27 thf(f52,plain,(
% 0.60/0.27 (((sK5 @ =)) = ((sK4 @ =))) | ($true = ((sP0 @ =)))),
% 0.60/0.27 inference(trivial_inequality_removal,[],[f51])).
% 0.60/0.27 thf(f54,definition,(
% 0.60/0.27 spl8_1 <=> ($true = ((sP0 @ =)))),
% 0.60/0.27 introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition])).
% 0.60/0.27 thf(f56,plain,(
% 0.60/0.27 ($true = ((sP0 @ =))) | ~spl8_1),
% 0.60/0.27 inference(avatar_component_clause,[],[f54])).
% 0.60/0.27 thf(f58,definition,(
% 0.60/0.27 spl8_2 <=> (((sK5 @ =)) = ((sK4 @ =)))),
% 0.60/0.27 introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition])).
% 0.60/0.27 thf(f60,plain,(
% 0.60/0.27 (((sK5 @ =)) = ((sK4 @ =))) | ~spl8_2),
% 0.60/0.27 inference(avatar_component_clause,[],[f58])).
% 0.60/0.27 thf(f61,plain,(
% 0.60/0.27 spl8_1 | spl8_2),
% 0.60/0.27 inference(avatar_split_clause,[],[f52,f58,f54])).
% 0.60/0.27 thf(f72,plain,(
% 0.60/0.27 ( ! [X1 : (($i > $o) > ($i > $o) > $o)] : (($true != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))) @ (sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) )),
% 0.60/0.27 inference(primitive_instantiation,[],[f17])).
% 0.60/0.27 thf(f82,plain,(
% 0.60/0.27 ( ! [X1 : (($i > $o) > ($i > $o) > $o)] : (($true != ((~ (X1 @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))))))) | ($true = ((~ (X1 @ (sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) )),
% 0.60/0.27 inference(beta-eta_normalization,[],[f72])).
% 0.60/0.27 thf(f83,plain,(
% 0.60/0.27 ( ! [X1 : (($i > $o) > ($i > $o) > $o)] : (($true = ((X1 @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) | ($true = ((~ (X1 @ (sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) )),
% 0.60/0.27 inference(not_proxy_clausification,[],[f82])).
% 0.60/0.27 thf(f84,plain,(
% 0.60/0.27 ( ! [X1 : (($i > $o) > ($i > $o) > $o)] : (($false = ((X1 @ (sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) | ($true = ((X1 @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) )),
% 0.60/0.27 inference(not_proxy_clausification,[],[f83])).
% 0.60/0.27 thf(f98,definition,(
% 0.60/0.27 spl8_3 <=> (((sK4 @ =)) = ((sK6 @ =)))),
% 0.60/0.27 introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition])).
% 0.60/0.27 thf(f112,plain,(
% 0.60/0.27 ( ! [X1 : (($i > $o) > ($i > $o) > $o)] : (($true != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) | ($true != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))) @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) )),
% 0.60/0.27 inference(primitive_instantiation,[],[f18])).
% 0.60/0.27 thf(f127,plain,(
% 0.60/0.27 ( ! [X1 : (($i > $o) > ($i > $o) > $o)] : (($true != ((~ (X1 @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))))))) | ($true != ((~ (X1 @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) )),
% 0.60/0.27 inference(beta-eta_normalization,[],[f112])).
% 0.60/0.27 thf(f128,plain,(
% 0.60/0.27 ( ! [X1 : (($i > $o) > ($i > $o) > $o)] : (($true = ((X1 @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) | ($true != ((~ (X1 @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) )),
% 0.60/0.27 inference(not_proxy_clausification,[],[f127])).
% 0.60/0.27 thf(f129,plain,(
% 0.60/0.27 ( ! [X1 : (($i > $o) > ($i > $o) > $o)] : (($true = ((X1 @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) | ($true = ((X1 @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1)))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (X1 @ Y0 @ Y1))))))))) )),
% 0.60/0.27 inference(not_proxy_clausification,[],[f128])).
% 0.60/0.27 thf(f154,plain,(
% 0.60/0.27 ($true != $true) | ($true = ((sK1 @ = @ (sK3 @ =)))) | ~spl8_1),
% 0.60/0.27 inference(constrained_superposition,[],[f14,f56])).
% 0.60/0.27 thf(f155,plain,(
% 0.60/0.27 ($true = ((sK1 @ = @ (sK3 @ =)))) | ~spl8_1),
% 0.60/0.27 inference(trivial_inequality_removal,[],[f154])).
% 0.60/0.27 thf(f220,plain,(
% 0.60/0.27 ( ! [X0 : (($i > $o) > ($i > $o) > $o)] : (($true != $true) | ($true != ((sP0 @ X0))) | (((sK2 @ X0 @ (sK3 @ X0))) = $false)) )),
% 0.60/0.27 inference(constrained_superposition,[],[f15,f20])).
% 0.60/0.27 thf(f221,plain,(
% 0.60/0.27 ( ! [X0 : (($i > $o) > ($i > $o) > $o)] : (($true != ((sP0 @ X0))) | (((sK2 @ X0 @ (sK3 @ X0))) = $false)) )),
% 0.60/0.27 inference(trivial_inequality_removal,[],[f220])).
% 0.60/0.27 thf(f223,plain,(
% 0.60/0.27 ($true != $true) | ($true = (((sK1 @ =) = (sK2 @ =)))) | ~spl8_1),
% 0.60/0.27 inference(constrained_superposition,[],[f13,f56])).
% 0.60/0.27 thf(f224,plain,(
% 0.60/0.27 ($true != $true) | (((sK1 @ =)) = ((sK2 @ =))) | ~spl8_1),
% 0.60/0.27 inference(equality_proxy_clausification,[],[f223])).
% 0.60/0.27 thf(f225,plain,(
% 0.60/0.27 (((sK1 @ =)) = ((sK2 @ =))) | ~spl8_1),
% 0.60/0.27 inference(trivial_inequality_removal,[],[f224])).
% 0.60/0.27 thf(f327,plain,(
% 0.60/0.27 ( ! [X1 : $i] : ((((sK1 @ = @ X1)) = ((sK2 @ = @ X1)))) ) | ~spl8_1),
% 0.60/0.27 inference(argument_congruence,[],[f225])).
% 0.60/0.27 thf(f329,plain,(
% 0.60/0.27 ( ! [X1 : $i] : (($true = ((sK2 @ = @ X1))) | ($false = ((sK1 @ = @ X1)))) ) | ~spl8_1),
% 0.60/0.27 inference(iff_proxy_clausification,[],[f327])).
% 0.60/0.27 thf(f434,plain,(
% 0.60/0.27 ($false = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (Y0 = Y1))))) @ (sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: (~ (Y2 = Y3))))) @ Y0 @ Y1)))))) @ (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: (~ (Y2 = Y3))))) @ Y0 @ Y1))))))))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (Y0 = Y1))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: (~ (Y2 = Y3))))) @ Y0 @ Y1)))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: (~ (Y2 = Y3))))) @ Y0 @ Y1))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: (~ (Y2 = Y3))))) @ Y0 @ Y1))))))))),
% 0.60/0.27 inference(primitive_instantiation,[],[f84])).
% 0.60/0.27 thf(f519,plain,(
% 0.60/0.27 ($false = ((~ ((sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))))) | ($true = ((~ ((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(beta-eta_normalization,[],[f434])).
% 0.60/0.27 thf(f520,plain,(
% 0.60/0.27 ($true = (((sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))) | ($true = ((~ ((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(not_proxy_clausification,[],[f519])).
% 0.60/0.27 thf(f521,plain,(
% 0.60/0.27 (((sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))) = ((sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))) | ($true = ((~ ((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(equality_proxy_clausification,[],[f520])).
% 0.60/0.27 thf(f522,plain,(
% 0.60/0.27 (((sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))) = ((sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))) | ($false = (((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(not_proxy_clausification,[],[f521])).
% 0.60/0.27 thf(f523,plain,(
% 0.60/0.27 (((sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))) = ((sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))) | (((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))) != ((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(equality_proxy_clausification,[],[f522])).
% 0.60/0.27 thf(f524,plain,(
% 0.60/0.27 (((sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))) = ((sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(trivial_inequality_removal,[],[f523])).
% 0.60/0.27 thf(f525,plain,(
% 0.60/0.27 (((sK5 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1)))))) = ((sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(boolean_simplification,[],[f524])).
% 0.60/0.27 thf(f526,plain,(
% 0.60/0.27 (((sK5 @ =)) = ((sK6 @ =))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(beta-eta_normalization,[],[f525])).
% 0.60/0.27 thf(f527,plain,(
% 0.60/0.27 (((sK5 @ =)) = ((sK6 @ =))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1)))))))),
% 0.60/0.27 inference(boolean_simplification,[],[f526])).
% 0.60/0.27 thf(f528,plain,(
% 0.60/0.27 (((sK5 @ =)) = ((sK6 @ =))) | ($true = ((sP0 @ =)))),
% 0.60/0.27 inference(beta-eta_normalization,[],[f527])).
% 0.60/0.27 thf(f535,plain,(
% 0.60/0.27 ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (Y0 = Y1))))) @ (sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: (~ (Y2 = Y3))))) @ Y0 @ Y1)))))) @ (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: (~ (Y2 = Y3))))) @ Y0 @ Y1))))))))) | ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (Y0 = Y1))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: (~ (Y2 = Y3))))) @ Y0 @ Y1)))))) @ (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: (~ (Y2 = Y3))))) @ Y0 @ Y1))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: (~ (Y2 = Y3))))) @ Y0 @ Y1))))))))),
% 0.60/0.27 inference(primitive_instantiation,[],[f129])).
% 0.60/0.27 thf(f614,plain,(
% 0.60/0.27 ($true = ((~ ((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))))) | ($true = ((~ ((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(beta-eta_normalization,[],[f535])).
% 0.60/0.27 thf(f615,plain,(
% 0.60/0.27 ($false = (((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))) | ($true = ((~ ((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(not_proxy_clausification,[],[f614])).
% 0.60/0.27 thf(f616,plain,(
% 0.60/0.27 (((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))) != ((sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))) | ($true = ((~ ((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(equality_proxy_clausification,[],[f615])).
% 0.60/0.27 thf(f617,plain,(
% 0.60/0.27 (((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))) != ((sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))) | ($false = (((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))) = (sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(not_proxy_clausification,[],[f616])).
% 0.60/0.27 thf(f618,plain,(
% 0.60/0.27 (((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))) != ((sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))) | (((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))) != ((sK7 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(equality_proxy_clausification,[],[f617])).
% 0.60/0.27 thf(f619,plain,(
% 0.60/0.27 (((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))) != ((sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1))))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(trivial_inequality_removal,[],[f618])).
% 0.60/0.27 thf(f620,plain,(
% 0.60/0.27 (((sK4 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1)))))) != ((sK6 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1))))))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(boolean_simplification,[],[f619])).
% 0.60/0.27 thf(f621,plain,(
% 0.60/0.27 (((sK4 @ =)) != ((sK6 @ =))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (~ (~ (Y0 = Y1)))))))))),
% 0.60/0.27 inference(beta-eta_normalization,[],[f620])).
% 0.60/0.27 thf(f622,plain,(
% 0.60/0.27 (((sK4 @ =)) != ((sK6 @ =))) | ($true = ((sP0 @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (Y0 = Y1)))))))),
% 0.60/0.27 inference(boolean_simplification,[],[f621])).
% 0.60/0.27 thf(f623,plain,(
% 0.60/0.27 (((sK4 @ =)) != ((sK6 @ =))) | ($true = ((sP0 @ =)))),
% 0.60/0.27 inference(beta-eta_normalization,[],[f622])).
% 0.60/0.27 thf(f702,plain,(
% 0.60/0.27 ($true != $true) | ($false = ((sK2 @ = @ (sK3 @ =)))) | ~spl8_1),
% 0.60/0.27 inference(constrained_superposition,[],[f221,f56])).
% 0.60/0.27 thf(f715,plain,(
% 0.60/0.27 ($false = ((sK2 @ = @ (sK3 @ =)))) | ~spl8_1),
% 0.60/0.27 inference(trivial_inequality_removal,[],[f702])).
% 0.60/0.27 thf(f883,plain,(
% 0.60/0.27 ($true = $false) | ($false = ((sK1 @ = @ (sK3 @ =)))) | ~spl8_1),
% 0.60/0.27 inference(constrained_superposition,[],[f715,f329])).
% 0.60/0.27 thf(f884,plain,(
% 0.60/0.27 ($false = ((sK1 @ = @ (sK3 @ =)))) | ~spl8_1),
% 0.60/0.27 inference(trivial_inequality_removal,[],[f883])).
% 0.60/0.27 thf(f905,plain,(
% 0.60/0.27 ($true = $false) | ~spl8_1),
% 0.60/0.27 inference(constrained_superposition,[],[f884,f155])).
% 0.60/0.27 thf(f937,plain,(
% 0.60/0.27 $false | ~spl8_1),
% 0.60/0.27 inference(trivial_inequality_removal,[],[f905])).
% 0.60/0.27 thf(f938,plain,(
% 0.60/0.27 ~spl8_1),
% 0.60/0.27 inference(avatar_contradiction_clause,[],[f937])).
% 0.60/0.27 thf(f941,plain,(
% 0.60/0.27 (((sK4 @ =)) = ((sK6 @ =))) | ($true = ((sP0 @ =))) | ~spl8_2),
% 0.60/0.27 inference(forward_demodulation,[],[f528,f60])).
% 0.60/0.27 thf(f942,plain,(
% 0.60/0.27 spl8_1 | ~spl8_3),
% 0.60/0.27 inference(avatar_split_clause,[],[f623,f98,f54])).
% 0.60/0.27 thf(f952,plain,(
% 0.60/0.27 spl8_1 | spl8_3 | ~spl8_2),
% 0.60/0.27 inference(avatar_split_clause,[],[f941,f58,f98,f54])).
% 0.60/0.27 cnf(s1, plain, spl8_1 | spl8_2, inference(sat_conversion,[],[f61])).
% 0.60/0.27 cnf(s26, plain, ~spl8_1, inference(sat_conversion,[],[f938])).
% 0.60/0.27 cnf(s28, plain, spl8_1 | ~spl8_3, inference(sat_conversion,[],[f942])).
% 0.60/0.27 cnf(s30, plain, spl8_1 | ~spl8_2 | spl8_3, inference(sat_conversion,[],[f952])).
% 0.60/0.27 cnf(s31, plain, ~spl8_3, inference(rat,[],[s28,s26])).
% 0.60/0.27 cnf(s32, plain, ~spl8_2, inference(rat,[],[s30,s26,s31])).
% 0.60/0.27 cnf(s33, plain, $false, inference(rat,[],[s1,s32,s26])).
% 0.60/0.27 thf(f953,plain,(
% 0.60/0.27 $false),
% 0.60/0.27 inference(avatar_sat_refutation,[],[s33])).
% 0.60/0.27 % SZS output end Proof for theBenchmark
% 0.60/0.27 % (223291)------------------------------
% 0.60/0.27 % (223291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.60/0.27 % (223291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.60/0.27 % (223291)CaDiCaL version: 2.1.3
% 0.60/0.27 % (223291)Termination reason: Refutation
% 0.60/0.27 % (223291)Time elapsed: 0.109 s
% 0.60/0.27 % (223291)Peak memory usage: 14 MB
% 0.60/0.27 % (223291)Instructions burned: 259 (million)
% 0.60/0.27 % (223285)Success in time 0.14 s
% 0.60/0.27 % Vampire exiting
%------------------------------------------------------------------------------