%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU938^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 : n010.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:34:26 AM UTC 2026
% Result : Theorem 4.19s 0.94s
% Output : Refutation 4.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU938^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19 % Computer : n010.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 14:47:18 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.23 Running first-order model finding
% 0.07/0.23 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
% 4.19/0.94 % (2958611)Will run a generic schedule for satisfiability detection.
% 4.19/0.94 % (2958618)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3323465980:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.19/0.94 % (2958617)% WARNING: option uhcvi not known.
% 4.19/0.94 % (2958617)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3992843037:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.19/0.94 % (2958616)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=864914304_2999 on theBenchmark for (2999ds/0Mi)
% 4.19/0.94 % (2958619)dis+10_1_sil=32000:sp=arity:random_seed=3245517886:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.19/0.94 % (2958620)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2042636883:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.19/0.94 % (2958617)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.19/0.94 % (2958620)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.19/0.94 % (2958617)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.19/0.94 % Exception at run slice level
% 4.19/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.19/0.94 % (2958622)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1671926099:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.19/0.94 % (2958621)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3885724249:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.19/0.94 % (2958628)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3424266293:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.19/0.94 % Exception at run slice level
% 4.19/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.19/0.94 % (2958632)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2675894548:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.19/0.94 % (2958619)Instruction limit reached!
% 4.19/0.94 % (2958619)------------------------------
% 4.19/0.94 % (2958619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.19/0.94 % (2958619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/0.94 % (2958619)CaDiCaL version: 2.1.3
% 4.19/0.94 % (2958619)Termination reason: Instruction limit
% 4.19/0.94 % (2958619)Termination phase: Saturation
% 4.19/0.94 % (2958619)Time elapsed: 0.052 s
% 4.19/0.94 % (2958619)Peak memory usage: 12 MB
% 4.19/0.94 % (2958619)Instructions burned: 104 (million)
% 4.19/0.94 % (2958620)Instruction limit reached!
% 4.19/0.94 % (2958620)------------------------------
% 4.19/0.94 % (2958620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.19/0.94 % (2958620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/0.94 % (2958620)CaDiCaL version: 2.1.3
% 4.19/0.94 % (2958620)Termination reason: Instruction limit
% 4.19/0.94 % (2958620)Termination phase: Saturation
% 4.19/0.94 % (2958620)Time elapsed: 0.056 s
% 4.19/0.94 % (2958620)Peak memory usage: 12 MB
% 4.19/0.94 % (2958620)Instructions burned: 116 (million)
% 4.19/0.94 % (2958634)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=171998100:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.19/0.94 % (2958634)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.19/0.94 % (2958634)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.19/0.94 % (2958635)ott-21_1_sil=16000:fs=off:random_seed=1558042502:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.19/0.94 % (2958622)Instruction limit reached!
% 4.19/0.94 % (2958622)------------------------------
% 4.19/0.94 % (2958622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.19/0.94 % (2958622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/0.94 % (2958622)CaDiCaL version: 2.1.3
% 4.19/0.94 % (2958622)Termination reason: Instruction limit
% 4.19/0.94 % (2958622)Termination phase: Saturation
% 4.19/0.94 % (2958622)Time elapsed: 0.082 s
% 4.19/0.94 % (2958622)Peak memory usage: 13 MB
% 4.19/0.94 % (2958622)Instructions burned: 159 (million)
% 4.19/0.94 % (2958621)Instruction limit reached!
% 4.19/0.94 % (2958621)------------------------------
% 4.19/0.94 % (2958621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.19/0.94 % (2958621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/0.94 % (2958621)CaDiCaL version: 2.1.3
% 4.19/0.94 % (2958621)Termination reason: Instruction limit
% 4.19/0.94 % (2958621)Termination phase: Saturation
% 4.19/0.94 % (2958621)Time elapsed: 0.089 s
% 4.19/0.94 % (2958621)Peak memory usage: 13 MB
% 4.19/0.94 % (2958621)Instructions burned: 132 (million)
% 4.19/0.94 % (2958638)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3741604076:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.19/0.94 % (2958632)Instruction limit reached!
% 4.19/0.94 % (2958632)------------------------------
% 4.19/0.94 % (2958632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.19/0.94 % (2958632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/0.94 % (2958632)CaDiCaL version: 2.1.3
% 4.19/0.94 % (2958632)Termination reason: Instruction limit
% 4.19/0.94 % (2958632)Termination phase: Saturation
% 4.19/0.94 % (2958632)Time elapsed: 0.072 s
% 4.19/0.94 % (2958632)Peak memory usage: 13 MB
% 4.19/0.94 % (2958632)Instructions burned: 132 (million)
% 4.19/0.94 % (2958639)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2333044563:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 4.19/0.94 % Exception at run slice level
% 4.19/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.19/0.94 % (2958641)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=685905846:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 4.19/0.94 % (2958643)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3210793419:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 4.19/0.94 % Exception at run slice level
% 4.19/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.19/0.94 % (2958646)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=2038359676: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)
% 4.19/0.94 % (2958646)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.19/0.94 % (2958635)Instruction limit reached!
% 4.19/0.94 % (2958635)------------------------------
% 4.19/0.94 % (2958635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.19/0.94 % (2958635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/0.94 % (2958635)CaDiCaL version: 2.1.3
% 4.19/0.94 % (2958635)Termination reason: Instruction limit
% 4.19/0.94 % (2958635)Termination phase: Saturation
% 4.19/0.94 % (2958635)Time elapsed: 0.085 s
% 4.19/0.94 % (2958635)Peak memory usage: 12 MB
% 4.19/0.94 % (2958635)Instructions burned: 181 (million)
% 4.19/0.94 % (2958648)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2537741572:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 4.19/0.94 % (2958648)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.19/0.94 % (2958638)Instruction limit reached!
% 4.19/0.94 % (2958638)------------------------------
% 4.19/0.94 % (2958638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.19/0.94 % (2958638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/0.94 % (2958638)CaDiCaL version: 2.1.3
% 4.19/0.94 % (2958638)Termination reason: Instruction limit
% 4.19/0.94 % (2958638)Termination phase: Saturation
% 4.19/0.94 % (2958638)Time elapsed: 0.233 s
% 4.19/0.94 % (2958638)Peak memory usage: 13 MB
% 4.19/0.94 % (2958638)Instructions burned: 478 (million)
% 4.19/0.94 % (2958651)fmb+10_1_sil=64000:random_seed=2536178237:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 4.19/0.94 % (2958651)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.19/0.94 % Exception at run slice level
% 4.19/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.19/0.94 % (2958653)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=761196544:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 4.19/0.94 % Exception at run slice level
% 4.19/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.19/0.94 % (2958634)Instruction limit reached!
% 4.19/0.94 % (2958634)------------------------------
% 4.19/0.94 % (2958634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.19/0.94 % (2958634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/0.94 % (2958634)CaDiCaL version: 2.1.3
% 4.19/0.94 % (2958634)Termination reason: Instruction limit
% 4.19/0.94 % (2958634)Termination phase: Saturation
% 4.19/0.94 % (2958634)Time elapsed: 0.325 s
% 4.19/0.94 % (2958634)Peak memory usage: 14 MB
% 4.19/0.94 % (2958634)Instructions burned: 686 (million)
% 4.19/0.94 % (2958655)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=830837053:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 4.19/0.94 % Exception at run slice level
% 4.19/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.19/0.94 % (2958656)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1215489682:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 4.19/0.94 % (2958656)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.19/0.94 % (2958658)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=520123352:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 4.19/0.94 % (2958658)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.19/0.94 % (2958658)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.19/0.94 % (2958646)Instruction limit reached!
% 4.19/0.94 % (2958646)------------------------------
% 4.19/0.94 % (2958646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.19/0.94 % (2958646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/0.94 % (2958646)CaDiCaL version: 2.1.3
% 4.19/0.94 % (2958646)Termination reason: Instruction limit
% 4.19/0.94 % (2958646)Termination phase: Saturation
% 4.19/0.94 % (2958646)Time elapsed: 0.438 s
% 4.19/0.94 % (2958646)Peak memory usage: 15 MB
% 4.19/0.94 % (2958646)Instructions burned: 694 (million)
% 4.19/0.94 % (2958661)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1359000368:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 4.19/0.94 % Exception at run slice level
% 4.19/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.19/0.94 % (2958648)Instruction limit reached!
% 4.19/0.94 % (2958648)------------------------------
% 4.19/0.94 % (2958648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.19/0.94 % (2958648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/0.94 % (2958648)CaDiCaL version: 2.1.3
% 4.19/0.94 % (2958648)Termination reason: Instruction limit
% 4.19/0.94 % (2958648)Termination phase: Saturation
% 4.19/0.94 % (2958648)Time elapsed: 0.441 s
% 4.19/0.94 % (2958648)Peak memory usage: 15 MB
% 4.19/0.94 % (2958648)Instructions burned: 880 (million)
% 4.19/0.94 % (2958663)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3092201428:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 4.19/0.94 % Exception at run slice level
% 4.19/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.19/0.94 % (2958664)ott-2_1_sil=16000:newcnf=on:random_seed=3377916712:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 4.19/0.94 % (2958664)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.19/0.94 % (2958617) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2958611-2958617"...
% 4.19/0.94 % (2958666)ott+10_1_sil=32000:tgt=ground:random_seed=3280435620:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 4.19/0.94 % (2958617)...printing done.
% 4.19/0.94 % (2958617)Refutation found. Thanks to Tanya!
% 4.19/0.94 % SZS status Theorem for theBenchmark
% 4.19/0.94 % SZS output start Proof for theBenchmark
% 4.19/0.94 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 4.19/0.94 thf(func_def_2, type, h: ($i > $i)).
% 4.19/0.94 thf(func_def_6, type, db0: !>[X0: $tType]:(X0)).
% 4.19/0.94 thf(func_def_7, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 4.19/0.94 thf(func_def_8, type, sK0: ((($i > $i) > $o) > ($i > $i) > $i > $i)).
% 4.19/0.94 thf(func_def_9, type, sK1: (($i > $i) > ($i > $i) > ($i > $i) > $o)).
% 4.19/0.94 thf(func_def_10, type, sK2: (($i > $i) > ($i > $i) > $i)).
% 4.19/0.94 thf(func_def_11, type, vNOT: ($o > $o)).
% 4.19/0.94 thf(func_def_12, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 4.19/0.94 thf(func_def_14, type, db1: !>[X0: $tType]:(X0)).
% 4.19/0.94 thf(func_def_15, type, db2: !>[X0: $tType]:(X0)).
% 4.19/0.94 thf(f1,conjecture,(
% 4.19/0.94 (! [X0 : ($i > $i),X1 : ($i > $i)] : (! [X2 : $i] : (((X0 @ X2)) = ((X1 @ X2))) => (X0 = X1)) & (((h @ b)) != a) & (((h @ a)) = a)) => ~ ! [X3 : ($i > $i),X4 : ($i > $i)] : (! [X5 : (($i > $i) > $o)] : ((! [X6 : ($i > $i)] : ((X5 @ X6) => (X5 @ (^[X2 : $i] : ((X3 @ (X6 @ X2)))))) & (X5 @ X3)) => (X5 @ (^[X2 : $i] : ((X4 @ (X3 @ X2)))))) => ! [X5 : (($i > $i) > $o)] : ((! [X7 : ($i > $i)] : ((X5 @ X7) => (X5 @ (^[X2 : $i] : ((X3 @ (X7 @ X2)))))) & (X5 @ X3)) => (X5 @ X4)))),
% 4.19/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM196_pme)).
% 4.19/0.94 thf(f2,negated_conjecture,(
% 4.19/0.94 ~((! [X0 : ($i > $i),X1 : ($i > $i)] : (! [X2 : $i] : (((X0 @ X2)) = ((X1 @ X2))) => (X0 = X1)) & (((h @ b)) != a) & (((h @ a)) = a)) => ~ ! [X3 : ($i > $i),X4 : ($i > $i)] : (! [X5 : (($i > $i) > $o)] : ((! [X6 : ($i > $i)] : ((X5 @ X6) => (X5 @ (^[X2 : $i] : ((X3 @ (X6 @ X2)))))) & (X5 @ X3)) => (X5 @ (^[X2 : $i] : ((X4 @ (X3 @ X2)))))) => ! [X5 : (($i > $i) > $o)] : ((! [X7 : ($i > $i)] : ((X5 @ X7) => (X5 @ (^[X2 : $i] : ((X3 @ (X7 @ X2)))))) & (X5 @ X3)) => (X5 @ X4))))),
% 4.19/0.94 inference(negated_conjecture,[status(cth)],[f1])).
% 4.19/0.94 thf(f3,plain,(
% 4.19/0.94 ~((! [X0 : ($i > $i),X1 : ($i > $i)] : (! [X2 : $i] : (((X0 @ X2)) = ((X1 @ X2))) => (X0 = X1)) & (((h @ b)) != a) & (((h @ a)) = a)) => ~ ! [X3 : ($i > $i),X4 : ($i > $i)] : (! [X5 : (($i > $i) > $o)] : ((! [X6 : ($i > $i)] : ((X5 @ X6) => (X5 @ (^[X7 : $i] : ((X3 @ (X6 @ X7)))))) & (X5 @ X3)) => (X5 @ (^[X8 : $i] : ((X4 @ (X3 @ X8)))))) => ! [X9 : (($i > $i) > $o)] : ((! [X10 : ($i > $i)] : ((X9 @ X10) => (X9 @ (^[X11 : $i] : ((X3 @ (X10 @ X11)))))) & (X9 @ X3)) => (X9 @ X4))))),
% 4.19/0.94 inference(rectify,[],[f2])).
% 4.19/0.94 thf(f4,plain,(
% 4.19/0.94 ~((! [X0 : ($i > $i),X1 : ($i > $i)] : (! [X2 : $i] : (((X0 @ X2)) = ((X1 @ X2))) => (X0 = X1)) & (a != ((h @ b))) & (a = ((h @ a)))) => ~ ! [X3 : ($i > $i),X4 : ($i > $i)] : (! [X5 : (($i > $i) > $o)] : ((! [X6 : ($i > $i)] : ((((X5 @ X6)) = $true) => ($true = ((X5 @ (^[Y0 : $i]: (X3 @ (X6 @ Y0))))))) & (((X5 @ X3)) = $true)) => ($true = ((X5 @ (^[Y0 : $i]: (X4 @ (X3 @ Y0))))))) => ! [X9 : (($i > $i) > $o)] : ((! [X10 : ($i > $i)] : ((((X9 @ X10)) = $true) => ($true = ((X9 @ (^[Y0 : $i]: (X3 @ (X10 @ Y0))))))) & (((X9 @ X3)) = $true)) => (((X9 @ X4)) = $true))))),
% 4.19/0.94 inference(fool_elimination,[],[f3])).
% 4.19/0.94 thf(f5,plain,(
% 4.19/0.94 ~((! [X0 : ($i > $i),X1 : ($i > $i)] : (! [X2 : $i] : (((X0 @ X2)) = ((X1 @ X2))) => (X0 = X1)) & (a != ((h @ b))) & (a = ((h @ a)))) => ~ ! [X3 : ($i > $i),X4 : ($i > $i)] : (! [X5 : (($i > $i) > $o)] : ((! [X6 : ($i > $i)] : ((((X5 @ X6)) = $true) => ($true = ((X5 @ (^[Y0 : $i]: (X3 @ (X6 @ Y0))))))) & (((X5 @ X3)) = $true)) => ($true = ((X5 @ (^[Y0 : $i]: (X4 @ (X3 @ Y0))))))) => ! [X7 : (($i > $i) > $o)] : ((! [X8 : ($i > $i)] : (($true = ((X7 @ X8))) => ($true = ((X7 @ (^[Y0 : $i]: (X3 @ (X8 @ Y0))))))) & ($true = ((X7 @ X3)))) => ($true = ((X7 @ X4))))))),
% 4.19/0.94 inference(rectify,[],[f4])).
% 4.19/0.94 thf(f6,plain,(
% 4.19/0.94 ! [X3 : ($i > $i),X4 : ($i > $i)] : (! [X7 : (($i > $i) > $o)] : (($true = ((X7 @ X4))) | (? [X8 : ($i > $i)] : (($true != ((X7 @ (^[Y0 : $i]: (X3 @ (X8 @ Y0)))))) & ($true = ((X7 @ X8)))) | ($true != ((X7 @ X3))))) | ? [X5 : (($i > $i) > $o)] : (($true != ((X5 @ (^[Y0 : $i]: (X4 @ (X3 @ Y0)))))) & (! [X6 : ($i > $i)] : (($true = ((X5 @ (^[Y0 : $i]: (X3 @ (X6 @ Y0)))))) | (((X5 @ X6)) != $true)) & (((X5 @ X3)) = $true)))) & (! [X0 : ($i > $i),X1 : ($i > $i)] : ((X0 = X1) | ? [X2 : $i] : (((X0 @ X2)) != ((X1 @ X2)))) & (a != ((h @ b))) & (a = ((h @ a))))),
% 4.19/0.94 inference(ennf_transformation,[],[f5])).
% 4.19/0.94 thf(f7,plain,(
% 4.19/0.94 ! [X3 : ($i > $i),X4 : ($i > $i)] : (! [X7 : (($i > $i) > $o)] : (($true = ((X7 @ X4))) | ? [X8 : ($i > $i)] : (($true != ((X7 @ (^[Y0 : $i]: (X3 @ (X8 @ Y0)))))) & ($true = ((X7 @ X8)))) | ($true != ((X7 @ X3)))) | ? [X5 : (($i > $i) > $o)] : (($true != ((X5 @ (^[Y0 : $i]: (X4 @ (X3 @ Y0)))))) & ! [X6 : ($i > $i)] : (($true = ((X5 @ (^[Y0 : $i]: (X3 @ (X6 @ Y0)))))) | (((X5 @ X6)) != $true)) & (((X5 @ X3)) = $true))) & ! [X0 : ($i > $i),X1 : ($i > $i)] : ((X0 = X1) | ? [X2 : $i] : (((X0 @ X2)) != ((X1 @ X2)))) & (a != ((h @ b))) & (a = ((h @ a)))),
% 4.19/0.94 inference(flattening,[],[f6])).
% 4.19/0.94 thf(f8,plain,(
% 4.19/0.94 ! [X0 : ($i > $i),X1 : ($i > $i)] : (! [X2 : (($i > $i) > $o)] : (($true = ((X2 @ X1))) | ? [X3 : ($i > $i)] : (($true != ((X2 @ (^[Y0 : $i]: (X0 @ (X3 @ Y0)))))) & ($true = ((X2 @ X3)))) | ($true != ((X2 @ X0)))) | ? [X4 : (($i > $i) > $o)] : (($true != ((X4 @ (^[Y0 : $i]: (X1 @ (X0 @ Y0)))))) & ! [X5 : ($i > $i)] : (($true = ((X4 @ (^[Y0 : $i]: (X0 @ (X5 @ Y0)))))) | ($true != ((X4 @ X5)))) & ($true = ((X4 @ X0))))) & ! [X6 : ($i > $i),X7 : ($i > $i)] : ((X6 = X7) | ? [X8 : $i] : (((X6 @ X8)) != ((X7 @ X8)))) & (a != ((h @ b))) & (a = ((h @ a)))),
% 4.19/0.94 inference(rectify,[],[f7])).
% 4.19/0.94 thf(f9,plain,(
% 4.19/0.94 ! [X0 : ($i > $i),X1 : ($i > $i)] : (! [X2 : (($i > $i) > $o)] : (($true = ((X2 @ X1))) | (($true != ((X2 @ (^[Y0 : $i]: (X0 @ (sK0 @ X2 @ X0 @ Y0)))))) & ($true = ((X2 @ (sK0 @ X2 @ X0))))) | ($true != ((X2 @ X0)))) | (($true != ((sK1 @ X1 @ X0 @ (^[Y0 : $i]: (X1 @ (X0 @ Y0)))))) & ! [X5 : ($i > $i)] : (($true = ((sK1 @ X1 @ X0 @ (^[Y0 : $i]: (X0 @ (X5 @ Y0)))))) | ($true != ((sK1 @ X1 @ X0 @ X5)))) & ($true = ((sK1 @ X1 @ X0 @ X0))))) & ! [X6 : ($i > $i),X7 : ($i > $i)] : ((X6 = X7) | (((X6 @ (sK2 @ X7 @ X6))) != ((X7 @ (sK2 @ X7 @ X6))))) & (a != ((h @ b))) & (a = ((h @ a)))),
% 4.19/0.94 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP]),skolemize(X8,sK2 @ X7 @ X6),skolemize(X8,sK2 @ X7 @ X6),skolemize(X8,sK2 @ X7 @ X6)],[f8])).
% 4.19/0.94 thf(f10,plain,(
% 4.19/0.94 (a = ((h @ a)))),
% 4.19/0.94 inference(cnf_transformation,[],[f9])).
% 4.19/0.94 thf(f11,plain,(
% 4.19/0.94 (a != ((h @ b)))),
% 4.19/0.94 inference(cnf_transformation,[],[f9])).
% 4.19/0.94 thf(f16,plain,(
% 4.19/0.94 ( ! [X2 : (($i > $i) > $o),X0 : ($i > $i),X1 : ($i > $i)] : (($true != ((X2 @ (^[Y0 : $i]: (X0 @ (sK0 @ X2 @ X0 @ Y0)))))) | ($true = ((X2 @ X1))) | ($true != ((X2 @ X0))) | ($true = ((sK1 @ X1 @ X0 @ X0)))) )),
% 4.19/0.94 inference(cnf_transformation,[],[f9])).
% 4.19/0.94 thf(f18,plain,(
% 4.19/0.94 ( ! [X2 : (($i > $i) > $o),X0 : ($i > $i),X1 : ($i > $i)] : (($true != ((sK1 @ X1 @ X0 @ (^[Y0 : $i]: (X1 @ (X0 @ Y0)))))) | ($true != ((X2 @ (^[Y0 : $i]: (X0 @ (sK0 @ X2 @ X0 @ Y0)))))) | ($true != ((X2 @ X0))) | ($true = ((X2 @ X1)))) )),
% 4.19/0.94 inference(cnf_transformation,[],[f9])).
% 4.19/0.94 thf(f90,plain,(
% 4.19/0.94 ( ! [X0 : ($i > $i),X1 : ($i > $i)] : (((^[Y0 : $i]: (X0 @ (sK0 @ (^[Y1 : $i > $i]: (~ (Y1 = X1))) @ X0 @ Y0))) = X1) | ($true != (((^[Y0 : $i > $i]: (~ (Y0 = X1))) @ X0))) | ($true = ((sK1 @ X1 @ X0 @ X0)))) )),
% 4.19/0.94 inference(leibniz_equality_elimination,[],[f16])).
% 4.19/0.94 thf(f108,plain,(
% 4.19/0.94 ( ! [X0 : ($i > $i),X1 : ($i > $i)] : (((^[Y0 : $i]: (X0 @ (sK0 @ (^[Y1 : $i > $i]: (~ (Y1 = X1))) @ X0 @ Y0))) = X1) | ($true != ((~ (X0 = X1)))) | ($true = ((sK1 @ X1 @ X0 @ X0)))) )),
% 4.19/0.94 inference(beta-eta_normalization,[],[f90])).
% 4.19/0.94 thf(f109,plain,(
% 4.19/0.94 ( ! [X0 : ($i > $i),X1 : ($i > $i)] : (((^[Y0 : $i]: (X0 @ (sK0 @ (^[Y1 : $i > $i]: (~ (Y1 = X1))) @ X0 @ Y0))) = X1) | ($true = ((X0 = X1))) | ($true = ((sK1 @ X1 @ X0 @ X0)))) )),
% 4.19/0.94 inference(not_proxy_clausification,[],[f108])).
% 4.19/0.94 thf(f110,plain,(
% 4.19/0.94 ( ! [X0 : ($i > $i),X1 : ($i > $i)] : (((^[Y0 : $i]: (X0 @ (sK0 @ (^[Y1 : $i > $i]: (~ (Y1 = X1))) @ X0 @ Y0))) = X1) | (X0 = X1) | ($true = ((sK1 @ X1 @ X0 @ X0)))) )),
% 4.19/0.94 inference(equality_proxy_clausification,[],[f109])).
% 4.19/0.94 thf(f111,plain,(
% 4.19/0.94 ( ! [X0 : ($i > $i),X1 : ($i > $i)] : (((^[Y0 : $i]: (X0 @ (sK0 @ (^[Y1 : $i > $i]: (~ (Y1 = X1))) @ X0 @ Y0))) = X1) | ($true != ((sK1 @ X1 @ X0 @ (^[Y0 : $i]: (X1 @ (X0 @ Y0)))))) | ($true != (((^[Y0 : $i > $i]: (~ (Y0 = X1))) @ X0)))) )),
% 4.19/0.94 inference(leibniz_equality_elimination,[],[f18])).
% 4.19/0.94 thf(f114,plain,(
% 4.19/0.94 ( ! [X0 : ($i > $i),X1 : ($i > $i)] : (((^[Y0 : $i]: (X0 @ (sK0 @ (^[Y1 : $i > $i]: (~ (Y1 = X1))) @ X0 @ Y0))) = X1) | ($true != ((sK1 @ X1 @ X0 @ (^[Y0 : $i]: (X1 @ (X0 @ Y0)))))) | ($true != ((~ (X0 = X1))))) )),
% 4.19/0.94 inference(beta-eta_normalization,[],[f111])).
% 4.19/0.94 thf(f115,plain,(
% 4.19/0.94 ( ! [X0 : ($i > $i),X1 : ($i > $i)] : (((^[Y0 : $i]: (X0 @ (sK0 @ (^[Y1 : $i > $i]: (~ (Y1 = X1))) @ X0 @ Y0))) = X1) | ($true != ((sK1 @ X1 @ X0 @ (^[Y0 : $i]: (X1 @ (X0 @ Y0)))))) | ($true = ((X0 = X1)))) )),
% 4.19/0.94 inference(not_proxy_clausification,[],[f114])).
% 4.19/0.94 thf(f116,plain,(
% 4.19/0.94 ( ! [X0 : ($i > $i),X1 : ($i > $i)] : (($true != ((sK1 @ X1 @ X0 @ (^[Y0 : $i]: (X1 @ (X0 @ Y0)))))) | ((^[Y0 : $i]: (X0 @ (sK0 @ (^[Y1 : $i > $i]: (~ (Y1 = X1))) @ X0 @ Y0))) = X1) | (X0 = X1)) )),
% 4.19/0.94 inference(equality_proxy_clausification,[],[f115])).
% 4.19/0.94 thf(f732,plain,(
% 4.19/0.94 ( ! [X2 : $i,X0 : ($i > $i),X1 : ($i > $i)] : ((((X1 @ X2)) = (((^[Y0 : $i]: (X0 @ (sK0 @ (^[Y1 : $i > $i]: (~ (Y1 = X1))) @ X0 @ Y0))) @ X2))) | (X0 = X1) | ($true = ((sK1 @ X1 @ X0 @ X0)))) )),
% 4.19/0.94 inference(argument_congruence,[],[f110])).
% 4.19/0.94 thf(f750,plain,(
% 4.19/0.94 ( ! [X2 : $i,X0 : ($i > $i),X1 : ($i > $i)] : ((((X1 @ X2)) = ((X0 @ (sK0 @ (^[Y0 : $i > $i]: (~ (Y0 = X1))) @ X0 @ X2)))) | (X0 = X1) | ($true = ((sK1 @ X1 @ X0 @ X0)))) )),
% 4.19/0.94 inference(beta-eta_normalization,[],[f732])).
% 4.19/0.94 thf(f2631,plain,(
% 4.19/0.94 ( ! [X0 : ($i > $i),X1 : $i] : ((a != ((X0 @ X1))) | ((^[Y0 : $i]: (h @ ((^[Y1 : $i]: (b)) @ Y0))) = X0) | ($true = ((sK1 @ X0 @ (^[Y0 : $i]: (h @ ((^[Y1 : $i]: (b)) @ Y0))) @ (^[Y0 : $i]: (h @ ((^[Y1 : $i]: (b)) @ Y0))))))) )),
% 4.19/0.94 inference(constrained_superposition,[],[f11,f750])).
% 4.19/0.94 thf(f2701,plain,(
% 4.19/0.94 ( ! [X0 : ($i > $i),X1 : $i] : ((a != ((X0 @ X1))) | ((^[Y0 : $i]: (h @ b)) = X0) | ($true = ((sK1 @ X0 @ (^[Y0 : $i]: (h @ b)) @ (^[Y0 : $i]: (h @ b)))))) )),
% 4.19/0.94 inference(beta-eta_normalization,[],[f2631])).
% 4.19/0.94 thf(f4147,definition,(
% 4.19/0.94 spl3_18 <=> ($true = ((sK1 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i]: (h @ b)) @ (^[Y0 : $i]: (h @ b)))))),
% 4.19/0.94 introduced(definition,[new_symbols(definition,[spl3_18])],[avatar_definition])).
% 4.19/0.94 thf(f4149,plain,(
% 4.19/0.94 ($true = ((sK1 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i]: (h @ b)) @ (^[Y0 : $i]: (h @ b))))) | ~spl3_18),
% 4.19/0.94 inference(avatar_component_clause,[],[f4147])).
% 4.19/0.94 thf(f4151,definition,(
% 4.19/0.94 spl3_19 <=> ((^[Y0 : $i]: (Y0)) = (^[Y0 : $i]: (h @ b)))),
% 4.19/0.94 introduced(definition,[new_symbols(definition,[spl3_19])],[avatar_definition])).
% 4.19/0.94 thf(f4153,plain,(
% 4.19/0.94 ((^[Y0 : $i]: (Y0)) = (^[Y0 : $i]: (h @ b))) | ~spl3_19),
% 4.19/0.94 inference(avatar_component_clause,[],[f4151])).
% 4.19/0.94 thf(f4169,definition,(
% 4.19/0.94 spl3_23 <=> ! [X1 : $i] : (a != X1)),
% 4.19/0.94 introduced(definition,[new_symbols(definition,[spl3_23])],[avatar_definition])).
% 4.19/0.94 thf(f4170,plain,(
% 4.19/0.94 ( ! [X1 : $i] : ((a != X1)) ) | ~spl3_23),
% 4.19/0.94 inference(avatar_component_clause,[],[f4169])).
% 4.19/0.94 thf(f5604,plain,(
% 4.19/0.94 $false | ~spl3_23),
% 4.19/0.94 inference(backward_subsumption_resolution,[],[f10,f4170])).
% 4.19/0.94 thf(f5614,plain,(
% 4.19/0.94 ~spl3_23),
% 4.19/0.94 inference(avatar_contradiction_clause,[],[f5604])).
% 4.19/0.94 thf(f5666,plain,(
% 4.19/0.94 ( ! [X0 : $i] : ((a != a) | ((^[Y0 : $i]: (Y0)) = (^[Y0 : $i]: (h @ b))) | ($true = ((sK1 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i]: (h @ b)) @ (^[Y0 : $i]: (h @ b))))) | (a != X0)) )),
% 4.19/0.94 inference(constrained_superposition,[],[f2701,f10])).
% 4.19/0.94 thf(f5693,plain,(
% 4.19/0.94 ( ! [X0 : $i] : (((^[Y0 : $i]: (Y0)) = (^[Y0 : $i]: (h @ b))) | ($true = ((sK1 @ (^[Y0 : $i]: (Y0)) @ (^[Y0 : $i]: (h @ b)) @ (^[Y0 : $i]: (h @ b))))) | (a != X0)) )),
% 4.19/0.94 inference(trivial_inequality_removal,[],[f5666])).
% 4.19/0.94 thf(f5747,plain,(
% 4.19/0.94 spl3_23 | spl3_18 | spl3_19),
% 4.19/0.94 inference(avatar_split_clause,[],[f5693,f4151,f4147,f4169])).
% 4.19/0.94 thf(f7717,plain,(
% 4.19/0.94 ($true != $true) | ((^[Y0 : $i]: (Y0)) = (^[Y0 : $i]: ((^[Y1 : $i]: (h @ b)) @ (sK0 @ (^[Y1 : $i > $i]: (~ (Y1 = (^[Y2 : $i]: (Y2))))) @ (^[Y1 : $i]: (h @ b)) @ Y0)))) | ((^[Y0 : $i]: (Y0)) = (^[Y0 : $i]: (h @ b))) | ~spl3_18),
% 4.19/0.94 inference(constrained_superposition,[],[f116,f4149])).
% 4.19/0.94 thf(f7740,plain,(
% 4.19/0.94 ((^[Y0 : $i]: (Y0)) = (^[Y0 : $i]: ((^[Y1 : $i]: (h @ b)) @ (sK0 @ (^[Y1 : $i > $i]: (~ (Y1 = (^[Y2 : $i]: (Y2))))) @ (^[Y1 : $i]: (h @ b)) @ Y0)))) | ((^[Y0 : $i]: (Y0)) = (^[Y0 : $i]: (h @ b))) | ~spl3_18),
% 4.19/0.94 inference(trivial_inequality_removal,[],[f7717])).
% 4.19/0.94 thf(f7741,plain,(
% 4.19/0.94 ((^[Y0 : $i]: (Y0)) = (^[Y0 : $i]: (h @ b))) | ((^[Y0 : $i]: (Y0)) = (^[Y0 : $i]: (h @ b))) | ~spl3_18),
% 4.19/0.94 inference(beta-eta_normalization,[],[f7740])).
% 4.19/0.94 thf(f7742,plain,(
% 4.19/0.94 ((^[Y0 : $i]: (Y0)) = (^[Y0 : $i]: (h @ b))) | ~spl3_18),
% 4.19/0.94 inference(duplicate_literal_removal,[],[f7741])).
% 4.19/0.94 thf(f7862,plain,(
% 4.19/0.94 spl3_19 | ~spl3_18),
% 4.19/0.94 inference(avatar_split_clause,[],[f7742,f4147,f4151])).
% 4.19/0.94 thf(f7954,plain,(
% 4.19/0.94 ( ! [X1 : $i] : (((((^[Y0 : $i]: (Y0)) @ X1)) = (((^[Y0 : $i]: (h @ b)) @ X1)))) ) | ~spl3_19),
% 4.19/0.94 inference(argument_congruence,[],[f4153])).
% 4.19/0.94 thf(f8045,plain,(
% 4.19/0.94 ( ! [X1 : $i] : ((((h @ b)) = X1)) ) | ~spl3_19),
% 4.19/0.94 inference(beta-eta_normalization,[],[f7954])).
% 4.19/0.94 thf(f8131,plain,(
% 4.19/0.94 $false | ~spl3_19),
% 4.19/0.94 inference(backward_subsumption_resolution,[],[f11,f8045])).
% 4.19/0.94 thf(f8318,plain,(
% 4.19/0.94 ~spl3_19),
% 4.19/0.94 inference(avatar_contradiction_clause,[],[f8131])).
% 4.19/0.94 cnf(s46, plain, ~spl3_23, inference(sat_conversion,[],[f5614])).
% 4.19/0.94 cnf(s49, plain, spl3_18 | spl3_19 | spl3_23, inference(sat_conversion,[],[f5747])).
% 4.19/0.94 cnf(s59, plain, ~spl3_18 | spl3_19, inference(sat_conversion,[],[f7862])).
% 4.19/0.94 cnf(s63, plain, ~spl3_19, inference(sat_conversion,[],[f8318])).
% 4.19/0.94 cnf(s83, plain, ~spl3_18, inference(rat,[],[s59,s63])).
% 4.19/0.94 cnf(s84, plain, spl3_23, inference(rat,[],[s49,s63,s83])).
% 4.19/0.94 cnf(s85, plain, $false, inference(rat,[],[s46,s84])).
% 4.19/0.94 thf(f8564,plain,(
% 4.19/0.94 $false),
% 4.19/0.94 inference(avatar_sat_refutation,[],[s85])).
% 4.19/0.94 % SZS output end Proof for theBenchmark
% 4.19/0.94 % (2958617)------------------------------
% 4.19/0.94 % (2958617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.19/0.94 % (2958617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/0.94 % (2958617)CaDiCaL version: 2.1.3
% 4.19/0.94 % (2958617)Termination reason: Refutation
% 4.19/0.94 % (2958617)Time elapsed: 0.658 s
% 4.19/0.94 % (2958617)Peak memory usage: 16 MB
% 4.19/0.94 % (2958617)Instructions burned: 1480 (million)
% 4.19/0.94 % (2958611)Success in time 0.703 s
% 4.19/0.94 % Vampire exiting
%------------------------------------------------------------------------------