%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO300^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 : n009.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:49:41 AM UTC 2026
% Result : Theorem 0.91s 0.38s
% Output : Refutation 0.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO300^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n009.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 16:44:31 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 Running first-order model finding
% 0.09/0.24 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.22/0.32 % (48641)Will run a generic schedule for satisfiability detection.
% 0.22/0.32 % (48657)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2728610063:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 0.22/0.32 % (48657)Refutation not found, incomplete strategy
% 0.22/0.32 % (48657)------------------------------
% 0.22/0.32 % (48657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (48657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (48657)CaDiCaL version: 2.1.3
% 0.22/0.32 % (48657)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.32 % (48657)Time elapsed: 0.001 s
% 0.22/0.32 % (48657)Peak memory usage: 12 MB
% 0.22/0.32 % (48657)Instructions burned: 1 (million)
% 0.22/0.32 % (48657)------------------------------
% 0.22/0.32 % (48657)------------------------------
% 0.22/0.32 % (48653)% WARNING: option uhcvi not known.
% 0.22/0.32 % (48651)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=658499969_3000 on theBenchmark for (3000ds/0Mi)
% 0.22/0.32 % (48654)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1012077964:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 0.22/0.32 % (48653)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=641347396:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 0.22/0.32 % (48655)dis+10_1_sil=32000:sp=arity:random_seed=3945856917:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 0.22/0.32 % (48656)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4145461745:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 0.22/0.32 % Exception at run slice level
% 0.22/0.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.22/0.32 % (48653)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.22/0.32 % (48658)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2888266402:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 0.22/0.32 % (48653)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.22/0.32 % (48656)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.22/0.32 % (48653)Refutation not found, incomplete strategy
% 0.22/0.32 % (48653)------------------------------
% 0.22/0.32 % (48653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (48653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (48653)CaDiCaL version: 2.1.3
% 0.22/0.32 % (48655)Refutation not found, incomplete strategy
% 0.22/0.32 % (48655)------------------------------
% 0.22/0.32 % (48655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (48653)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.32 % (48653)Time elapsed: 0.002 s
% 0.22/0.32 % (48653)Peak memory usage: 12 MB
% 0.22/0.32 % (48655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (48653)Instructions burned: 1 (million)
% 0.22/0.32 % (48655)CaDiCaL version: 2.1.3
% 0.22/0.32 % (48655)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.32 % (48655)Time elapsed: 0.001 s
% 0.22/0.32 % (48655)Peak memory usage: 12 MB
% 0.22/0.32 % (48655)Instructions burned: 1 (million)
% 0.22/0.32 % (48656)Refutation not found, incomplete strategy
% 0.22/0.32 % (48656)------------------------------
% 0.22/0.32 % (48656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (48656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (48656)CaDiCaL version: 2.1.3
% 0.22/0.32 % (48656)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.32 % (48656)Time elapsed: 0.001 s
% 0.22/0.32 % (48656)Peak memory usage: 12 MB
% 0.22/0.32 % (48656)Instructions burned: 1 (million)
% 0.22/0.32 % (48658)Refutation not found, incomplete strategy
% 0.22/0.32 % (48658)------------------------------
% 0.22/0.32 % (48658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (48658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (48658)CaDiCaL version: 2.1.3
% 0.22/0.32 % (48658)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.32 % (48658)Time elapsed: 0.001 s
% 0.22/0.32 % (48658)Peak memory usage: 12 MB
% 0.22/0.32 % (48658)Instructions burned: 1 (million)
% 0.22/0.32 % (48654)Refutation not found, incomplete strategy
% 0.22/0.35 % (48654)------------------------------
% 0.22/0.35 % (48654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.35 % (48654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.35 % (48654)CaDiCaL version: 2.1.3
% 0.22/0.35 % (48654)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.35 % (48654)Time elapsed: 0.002 s
% 0.22/0.35 % (48654)Peak memory usage: 12 MB
% 0.22/0.35 % (48654)Instructions burned: 2 (million)
% 0.22/0.35 % (48653)------------------------------
% 0.22/0.35 % (48653)------------------------------
% 0.22/0.35 % (48655)------------------------------
% 0.22/0.35 % (48655)------------------------------
% 0.22/0.35 % (48656)------------------------------
% 0.22/0.35 % (48656)------------------------------
% 0.22/0.35 % (48658)------------------------------
% 0.22/0.35 % (48658)------------------------------
% 0.22/0.35 % (48654)------------------------------
% 0.22/0.35 % (48654)------------------------------
% 0.22/0.35 % (48660)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=760909511:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.22/0.35 % Exception at run slice level
% 0.22/0.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.22/0.35 % (48674)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3272980716:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi)
% 0.22/0.35 % Exception at run slice level
% 0.22/0.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.22/0.35 % (48667)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=327923640:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.22/0.35 % (48667)Refutation not found, incomplete strategy
% 0.22/0.35 % (48667)------------------------------
% 0.22/0.35 % (48667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.35 % (48667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.35 % (48667)CaDiCaL version: 2.1.3
% 0.22/0.35 % (48667)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.35 % (48667)Time elapsed: 0.002 s
% 0.22/0.35 % (48667)Peak memory usage: 12 MB
% 0.22/0.35 % (48667)Instructions burned: 1 (million)
% 0.22/0.35 % (48668)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=985658799:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.22/0.35 % (48669)ott-21_1_sil=16000:fs=off:random_seed=3331183074:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.22/0.35 % (48670)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2331981401:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 0.22/0.35 % (48671)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1719654486:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 0.22/0.35 % (48667)------------------------------
% 0.22/0.35 % (48667)------------------------------
% 0.22/0.35 % (48668)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.22/0.35 % (48672)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1501452507:i=1179_2999 on theBenchmark for (2999ds/1179Mi)
% 0.22/0.35 % (48668)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.22/0.35 % Exception at run slice level
% 0.22/0.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.22/0.35 % (48668)Refutation not found, incomplete strategy
% 0.22/0.35 % (48668)------------------------------
% 0.22/0.35 % (48668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.35 % (48668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.35 % (48668)CaDiCaL version: 2.1.3
% 0.22/0.35 % (48668)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.35 % (48668)Time elapsed: 0.002 s
% 0.22/0.35 % (48668)Peak memory usage: 12 MB
% 0.22/0.35 % (48668)Instructions burned: 1 (million)
% 0.22/0.35 % (48668)------------------------------
% 0.22/0.35 % (48668)------------------------------
% 0.22/0.35 % (48672)Refutation not found, incomplete strategy
% 0.22/0.35 % (48672)------------------------------
% 0.22/0.35 % (48672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.35 % (48672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.35 % (48672)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48672)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48672)Time elapsed: 0.002 s
% 0.91/0.38 % (48672)Peak memory usage: 12 MB
% 0.91/0.38 % (48672)Instructions burned: 2 (million)
% 0.91/0.38 % (48670)Refutation not found, incomplete strategy
% 0.91/0.38 % (48670)------------------------------
% 0.91/0.38 % (48670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48670)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48670)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48670)Time elapsed: 0.003 s
% 0.91/0.38 % (48670)Peak memory usage: 12 MB
% 0.91/0.38 % (48670)Instructions burned: 2 (million)
% 0.91/0.38 % (48672)------------------------------
% 0.91/0.38 % (48672)------------------------------
% 0.91/0.38 % (48670)------------------------------
% 0.91/0.38 % (48670)------------------------------
% 0.91/0.38 % (48676)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=539441178:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2999 on theBenchmark for (2999ds/692Mi)
% 0.91/0.38 % (48676)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.91/0.38 % (48676)Refutation not found, incomplete strategy
% 0.91/0.38 % (48676)------------------------------
% 0.91/0.38 % (48676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48676)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48676)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48676)Time elapsed: 0.001 s
% 0.91/0.38 % (48676)Peak memory usage: 12 MB
% 0.91/0.38 % (48676)Instructions burned: 1 (million)
% 0.91/0.38 % (48676)------------------------------
% 0.91/0.38 % (48676)------------------------------
% 0.91/0.38 % (48683)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3412380361:i=879:kws=inv_precedence:fsr=off_2999 on theBenchmark for (2999ds/879Mi)
% 0.91/0.38 % (48684)fmb+10_1_sil=64000:random_seed=1190571613:i=22061:nm=2:gsp=on_2999 on theBenchmark for (2999ds/22061Mi)
% 0.91/0.38 % (48683)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.91/0.38 % (48684)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 0.91/0.38 % Exception at run slice level
% 0.91/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.91/0.38 % (48685)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2413118734:i=9515:nm=5_2999 on theBenchmark for (2999ds/9515Mi)
% 0.91/0.38 % (48683)Refutation not found, incomplete strategy
% 0.91/0.38 % (48683)------------------------------
% 0.91/0.38 % (48683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48683)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48683)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48683)Time elapsed: 0.002 s
% 0.91/0.38 % (48683)Peak memory usage: 12 MB
% 0.91/0.38 % (48683)Instructions burned: 1 (million)
% 0.91/0.38 % Exception at run slice level
% 0.91/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.91/0.38 % (48686)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2382747727:fmbsr=1.7:i=920_2999 on theBenchmark for (2999ds/920Mi)
% 0.91/0.38 % (48683)------------------------------
% 0.91/0.38 % (48683)------------------------------
% 0.91/0.38 % (48688)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2430371389:i=5131_2999 on theBenchmark for (2999ds/5131Mi)
% 0.91/0.38 % Exception at run slice level
% 0.91/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.91/0.38 % (48688)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.91/0.38 % (48688)Refutation not found, incomplete strategy
% 0.91/0.38 % (48688)------------------------------
% 0.91/0.38 % (48688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48688)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48688)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48688)Time elapsed: 0.001 s
% 0.91/0.38 % (48688)Peak memory usage: 12 MB
% 0.91/0.38 % (48688)Instructions burned: 1 (million)
% 0.91/0.38 % (48689)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3124095996:i=1472:ins=7:fdi=8:gsp=on_2999 on theBenchmark for (2999ds/1472Mi)
% 0.91/0.38 % (48688)------------------------------
% 0.91/0.38 % (48688)------------------------------
% 0.91/0.38 % (48689)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 0.91/0.38 % (48689)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.91/0.38 % (48692)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=723738079:i=6324_2999 on theBenchmark for (2999ds/6324Mi)
% 0.91/0.38 % Exception at run slice level
% 0.91/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.91/0.38 % (48695)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2273137894:fmbsr=2.30978:i=2174_2999 on theBenchmark for (2999ds/2174Mi)
% 0.91/0.38 % (48697)ott-2_1_sil=16000:newcnf=on:random_seed=3849694991:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2999 on theBenchmark for (2999ds/869Mi)
% 0.91/0.38 % Exception at run slice level
% 0.91/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.91/0.38 % (48698)ott+10_1_sil=32000:tgt=ground:random_seed=2392254741:i=5114:av=off_2999 on theBenchmark for (2999ds/5114Mi)
% 0.91/0.38 % (48697)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.91/0.38 % (48697)Refutation not found, incomplete strategy
% 0.91/0.38 % (48697)------------------------------
% 0.91/0.38 % (48697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48697)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48697)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48697)Time elapsed: 0.001 s
% 0.91/0.38 % (48697)Peak memory usage: 12 MB
% 0.91/0.38 % (48697)Instructions burned: 1 (million)
% 0.91/0.38 % (48698)Refutation not found, incomplete strategy
% 0.91/0.38 % (48698)------------------------------
% 0.91/0.38 % (48698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48698)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48698)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48698)Time elapsed: 0.001 s
% 0.91/0.38 % (48698)Peak memory usage: 12 MB
% 0.91/0.38 % (48698)Instructions burned: 1 (million)
% 0.91/0.38 % (48697)------------------------------
% 0.91/0.38 % (48697)------------------------------
% 0.91/0.38 % (48700)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3165690747:i=54282_2999 on theBenchmark for (2999ds/54282Mi)
% 0.91/0.38 % (48698)------------------------------
% 0.91/0.38 % (48698)------------------------------
% 0.91/0.38 % Exception at run slice level
% 0.91/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.91/0.38 % (48708)ott+11_1_sil=16000:gs=on:random_seed=2003126681:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2999 on theBenchmark for (2999ds/2251Mi)
% 0.91/0.38 % (48708)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.91/0.38 % (48708)Refutation not found, incomplete strategy
% 0.91/0.38 % (48708)------------------------------
% 0.91/0.38 % (48708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48708)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48708)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48708)Time elapsed: 0.001 s
% 0.91/0.38 % (48708)Peak memory usage: 12 MB
% 0.91/0.38 % (48708)Instructions burned: 1 (million)
% 0.91/0.38 % (48708)------------------------------
% 0.91/0.38 % (48708)------------------------------
% 0.91/0.38 % (48702)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2498858518:i=3512:aac=none_2999 on theBenchmark for (2999ds/3512Mi)
% 0.91/0.38 % (48702)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.91/0.38 % (48702)Refutation not found, incomplete strategy
% 0.91/0.38 % (48702)------------------------------
% 0.91/0.38 % (48702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48702)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48702)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48702)Time elapsed: 0.002 s
% 0.91/0.38 % (48702)Peak memory usage: 12 MB
% 0.91/0.38 % (48702)Instructions burned: 1 (million)
% 0.91/0.38 % (48702)------------------------------
% 0.91/0.38 % (48702)------------------------------
% 0.91/0.38 % (48707)dis+21_1_sil=32000:sas=cadical:random_seed=2614633530:i=3773:amm=off_2999 on theBenchmark for (2999ds/3773Mi)
% 0.91/0.38 % (48709)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1352487920:fmbsr=1.6:i=67534_2999 on theBenchmark for (2999ds/67534Mi)
% 0.91/0.38 % Exception at run slice level
% 0.91/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.91/0.38 % (48707)Refutation not found, incomplete strategy
% 0.91/0.38 % (48707)------------------------------
% 0.91/0.38 % (48707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48707)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48707)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48707)Time elapsed: 0.001 s
% 0.91/0.38 % (48707)Peak memory usage: 12 MB
% 0.91/0.38 % (48707)Instructions burned: 1 (million)
% 0.91/0.38 % (48710)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3108071081:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2999 on theBenchmark for (2999ds/4591Mi)
% 0.91/0.38 % (48707)------------------------------
% 0.91/0.38 % (48707)------------------------------
% 0.91/0.38 % (48712)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2094091524:i=29340_2998 on theBenchmark for (2998ds/29340Mi)
% 0.91/0.38 % (48712)Refutation not found, incomplete strategy
% 0.91/0.38 % (48712)------------------------------
% 0.91/0.38 % (48712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48712)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48712)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48712)Time elapsed: 0.001 s
% 0.91/0.38 % (48712)Peak memory usage: 12 MB
% 0.91/0.38 % (48712)Instructions burned: 1 (million)
% 0.91/0.38 % (48712)------------------------------
% 0.91/0.38 % (48712)------------------------------
% 0.91/0.38 % (48669)Instruction limit reached!
% 0.91/0.38 % (48669)------------------------------
% 0.91/0.38 % (48669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48669)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48669)Termination reason: Instruction limit
% 0.91/0.38 % (48669)Termination phase: Saturation
% 0.91/0.38 % (48669)Time elapsed: 0.077 s
% 0.91/0.38 % (48669)Peak memory usage: 13 MB
% 0.91/0.38 % (48669)Instructions burned: 183 (million)
% 0.91/0.38 % (48715)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4096786512:i=5211_2998 on theBenchmark for (2998ds/5211Mi)
% 0.91/0.38 % (48723)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1827123543:i=14071_2998 on theBenchmark for (2998ds/14071Mi)
% 0.91/0.38 % Exception at run slice level
% 0.91/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.91/0.38 % (48715)Refutation not found, incomplete strategy
% 0.91/0.38 % (48715)------------------------------
% 0.91/0.38 % (48715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48715)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48715)Termination reason: Refutation not found, incomplete strategy
% 0.91/0.38 % (48715)Time elapsed: 0.002 s
% 0.91/0.38 % (48715)Peak memory usage: 13 MB
% 0.91/0.38 % (48715)Instructions burned: 1 (million)
% 0.91/0.38 % (48718)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4286766168:i=5497:nm=2_2998 on theBenchmark for (2998ds/5497Mi)
% 0.91/0.38 % (48715)------------------------------
% 0.91/0.38 % (48715)------------------------------
% 0.91/0.38 % Exception at run slice level
% 0.91/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.91/0.38 % (48689) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-48641-48689"...
% 0.91/0.38 % (48720)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3753489187:fmbsr=2:i=46332_2998 on theBenchmark for (2998ds/46332Mi)
% 0.91/0.38 % Exception at run slice level
% 0.91/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.91/0.38 % (48689)...printing done.
% 0.91/0.38 % (48689)Refutation found. Thanks to Tanya!
% 0.91/0.38 % SZS status Theorem for theBenchmark
% 0.91/0.38 % SZS output start Proof for theBenchmark
% 0.91/0.38 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.91/0.38 thf(func_def_3, type, db0: !>[X0: $tType]:(X0)).
% 0.91/0.38 thf(func_def_4, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.91/0.38 thf(func_def_5, type, sK0: ((($i > $i) > $i) > (($i > $i) > $i) > $o)).
% 0.91/0.38 thf(func_def_6, type, sF1: ((($i > $i) > $i) > (($i > $i) > $i) > $o)).
% 0.91/0.38 thf(func_def_7, type, sF2: ((($i > $i) > $i) > ((($i > $i) > $i) > (($i > $i) > $i) > $o) > (($i > $i) > $i) > $o)).
% 0.91/0.38 thf(func_def_8, type, sF3: !>[X0: $tType, X1: $tType]:(((($i > $i) > $i) > ((X0 > $i) > X1) > (((X0 > $i) > X1) > (($i > $i) > $i) > $o) > $o))).
% 0.91/0.38 thf(func_def_9, type, sF4: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((((X0 > $i) > X1) > ((X2 > X4) > X3) > $o) > ((X2 > X4) > X3) > ((X0 > $i) > X1) > $o))).
% 0.91/0.38 thf(func_def_10, type, sF5: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((((X2 > X3) > X0) > (((X1 > X4) > X5) > ((X2 > X3) > X0) > $o) > ((X1 > X4) > X5) > $o))).
% 0.91/0.38 thf(func_def_11, type, sF6: ((($i > $i) > $i) > ($i > $i) > $i)).
% 0.91/0.38 thf(func_def_12, type, sF7: !>[X0: $tType]:(((($i > $i) > $i) > ((($i > $i) > $i) > X0) > X0))).
% 0.91/0.38 thf(func_def_13, type, sF8: !>[X0: $tType, X1: $tType, X2: $tType]:((((X0 > $i) > X2) > (((X0 > $i) > X2) > X1) > X1))).
% 0.91/0.38 thf(func_def_14, type, sF9: !>[X0: $tType]:((X0 > (X0 > $i) > ($i > $i) > $i))).
% 0.91/0.38 thf(func_def_15, type, sF10: ((($i > $i) > $i) > ($i > $i) > $i)).
% 0.91/0.38 thf(func_def_16, type, sF11: ((($i > $i) > $i) > ($i > $i) > $i)).
% 0.91/0.38 thf(func_def_17, type, sF12: !>[X0: $tType]:((X0 > (X0 > $i) > $i))).
% 0.91/0.38 thf(func_def_18, type, sF13: !>[X0: $tType]:(($i > X0 > $i))).
% 0.91/0.38 thf(func_def_19, type, sF14: !>[X0: $tType, X1: $tType]:(((X0 > $i) > X1 > (X1 > (X0 > $i) > $i) > $i))).
% 0.91/0.38 thf(func_def_20, type, sF15: !>[X0: $tType, X1: $tType]:(((X0 > X1 > $i) > X0 > X1 > $i))).
% 0.91/0.38 thf(func_def_21, type, sF16: (((($i > $i) > $i) > ($i > $i) > $i) > (($i > $i) > $i) > ($i > $i) > $i)).
% 0.91/0.38 thf(func_def_22, type, sF17: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > (X0 > X2) > X1) > X0 > (X0 > X2) > X1))).
% 0.91/0.38 thf(func_def_23, type, sK18: ((($i > $i) > $i) > $i > $i)).
% 0.91/0.38 thf(func_def_24, type, sF19: !>[X0: $tType]:(((($i > $i) > $i) > ((($i > $i) > $i) > X0 > $i) > X0 > $i))).
% 0.91/0.38 thf(func_def_25, type, sF20: !>[X0: $tType]:(((X0 > $i) > ((X0 > $i) > X0) > X0))).
% 0.91/0.38 thf(func_def_26, type, sF21: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2) > ((X0 > X2) > X1) > X1))).
% 0.91/0.38 thf(func_def_27, type, sF22: !>[X0: $tType, X1: $tType, X2: $tType]:((((X0 > $i) > X2) > (((X0 > $i) > X2) > X1 > $i) > X1 > $i))).
% 0.91/0.38 thf(func_def_28, type, sF23: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1 > X2) > X0 > X1 > X2))).
% 0.91/0.38 thf(func_def_29, type, sF24: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((((X1 > X3) > X2) > X0) > ((X1 > X3) > X2) > X0))).
% 0.91/0.38 thf(func_def_30, type, sF25: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((((X2 > X0) > X1) > X3 > X4) > X3 > ((X2 > X0) > X1) > X4))).
% 0.91/0.38 thf(func_def_31, type, sF26: !>[X0: $tType, X1: $tType]:((X0 > X1 > (X1 > X0 > $i) > $i))).
% 0.91/0.38 thf(func_def_32, type, sF27: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((X1 > X0) > ((X1 > X0) > X2 > X3) > X2 > X3))).
% 0.91/0.38 thf(func_def_33, type, db1: !>[X0: $tType]:(X0)).
% 0.91/0.38 thf(func_def_34, type, sF28: !>[X0: $tType, X1: $tType]:((((X0 > X1) > ($i > $i) > $i) > (X0 > X1) > ($i > $i) > $i))).
% 0.91/0.38 thf(func_def_35, type, sF29: !>[X0: $tType]:(($i > (($i > $i) > X0) > ($i > $i) > X0))).
% 0.91/0.38 thf(func_def_36, type, sF30: !>[X0: $tType, X1: $tType]:(((X0 > X1) > ($i > $i) > X0 > X1))).
% 0.91/0.38 thf(func_def_37, type, sF31: !>[X0: $tType]:((X0 > ($i > $i) > X0))).
% 0.91/0.38 thf(func_def_38, type, sF32: !>[X0: $tType, X1: $tType]:((((X0 > X1) > ($i > $i) > $i) > ($i > $i) > (X0 > X1) > ($i > $i) > $i))).
% 0.91/0.38 thf(func_def_39, type, sF33: (($i > $i) > ($i > $i) > $i > $i)).
% 0.91/0.38 thf(func_def_40, type, sF34: !>[X0: $tType]:((((X0 > $i) > $i) > (((X0 > $i) > $i) > ($i > $i) > $i) > ($i > $i) > $i))).
% 0.91/0.38 thf(func_def_41, type, sF35: !>[X0: $tType, X1: $tType]:(((((X0 > $i) > $i) > X1) > ($i > $i) > ((X0 > $i) > $i) > X1))).
% 0.91/0.38 thf(func_def_42, type, sF36: !>[X0: $tType]:((X0 > (X0 > X0) > ($i > $i) > X0))).
% 0.91/0.38 thf(func_def_43, type, sF37: (((($i > $i) > $i) > $i) > ($i > $i) > (($i > $i) > $i) > $i)).
% 0.91/0.38 thf(func_def_44, type, sF38: ((((($i > $i) > $i) > $i) > ($i > $i) > $i) > ($i > $i) > ((($i > $i) > $i) > $i) > ($i > $i) > $i)).
% 0.91/0.38 thf(func_def_45, type, sF39: !>[X0: $tType]:((X0 > (X0 > ($i > $i) > $i) > ($i > $i) > $i))).
% 0.91/0.38 thf(func_def_46, type, sF40: !>[X0: $tType]:(((X0 > ($i > $i) > $i) > ($i > $i) > X0 > ($i > $i) > $i))).
% 0.91/0.38 thf(func_def_47, type, sF41: !>[X0: $tType]:(((X0 > $i) > ($i > $i) > X0 > $i))).
% 0.91/0.38 thf(func_def_48, type, sF42: ((($i > $i) > $i) > ($i > $i) > ($i > $i) > $i)).
% 0.91/0.38 thf(func_def_49, type, sF43: ((($i > $i) > $i) > ($i > $i) > $i)).
% 0.91/0.38 thf(func_def_50, type, sF44: !>[X0: $tType, X1: $tType]:(((X1 > $i) > ((X1 > $i) > X0) > ($i > $i) > X0))).
% 0.91/0.38 thf(func_def_51, type, sF45: !>[X0: $tType]:(((($i > $i) > X0 > $i) > ($i > $i) > X0 > $i))).
% 0.91/0.38 thf(func_def_52, type, sF46: !>[X0: $tType]:(((X0 > $i) > ((X0 > $i) > ($i > $i) > $i) > ($i > $i) > ($i > $i) > $i))).
% 0.91/0.38 thf(func_def_53, type, sF47: !>[X0: $tType, X1: $tType]:((((X0 > $i) > X1) > (X0 > $i) > X1))).
% 0.91/0.38 thf(func_def_54, type, sF48: ((($i > $i) > $i) > ($i > $i) > $i)).
% 0.91/0.38 thf(func_def_55, type, sF49: ($i > ($i > $i) > $i)).
% 0.91/0.38 thf(func_def_56, type, sF50: ((($i > $i) > $i) > ($i > $i) > $i)).
% 0.91/0.38 thf(func_def_57, type, sF51: ((($i > $i) > $i) > $i)).
% 0.91/0.38 thf(func_def_58, type, sK52: ((($i > $i) > $i) > (($i > $i) > $i) > $i > $i)).
% 0.91/0.38 thf(func_def_59, type, sF53: !>[X0: $tType]:(((X0 > $i) > ((X0 > $i) > $i) > $i))).
% 0.91/0.38 thf(func_def_60, type, sF54: ($i > $i)).
% 0.91/0.38 thf(func_def_61, type, sF55: !>[X0: $tType, X1: $tType]:(((((X0 > $i) > X1 > $i) > ($i > $i) > X1 > $i) > ((X0 > $i) > X1 > $i) > ($i > $i) > X1 > $i))).
% 0.91/0.38 thf(func_def_62, type, sF56: !>[X0: $tType, X1: $tType]:(((X1 > $i) > ((X1 > $i) > X0 > $i) > ($i > $i) > X0 > $i))).
% 0.91/0.38 thf(func_def_63, type, sF57: !>[X0: $tType, X1: $tType]:(((((X0 > $i) > X1) > ($i > $i) > X1) > ((X0 > $i) > X1) > ($i > $i) > X1))).
% 0.91/0.38 thf(func_def_64, type, sF58: !>[X0: $tType]:(((($i > $i) > $i) > ((($i > $i) > $i) > ($i > $i) > X0) > ($i > $i) > X0))).
% 0.91/0.38 thf(func_def_65, type, sF59: !>[X0: $tType, X1: $tType]:(((X0 > X1) > ((X0 > X1) > ($i > $i) > X0 > X1) > ($i > $i) > X0 > X1))).
% 0.91/0.38 thf(func_def_66, type, sF60: !>[X0: $tType, X1: $tType]:(((((X0 > $i) > $i) > X1) > ((((X0 > $i) > $i) > X1) > ($i > $i) > ((X0 > $i) > $i) > X1) > ($i > $i) > ((X0 > $i) > $i) > X1))).
% 0.91/0.38 thf(func_def_67, type, sF61: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2) > ((X0 > X2) > ($i > $i) > X1) > ($i > $i) > X1))).
% 0.91/0.38 thf(func_def_68, type, sF62: !>[X0: $tType, X1: $tType]:(((((X0 > $i) > X1) > ($i > $i) > $i) > ((X0 > $i) > X1) > ($i > $i) > $i))).
% 0.91/0.38 thf(func_def_69, type, sF63: !>[X0: $tType]:((X0 > (X0 > ($i > $i) > X0) > ($i > $i) > X0))).
% 0.91/0.38 thf(func_def_70, type, sF64: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((X0 > (X0 > (X1 > X3) > ($i > $i) > X2) > (X1 > X3) > ($i > $i) > X2))).
% 0.91/0.38 thf(func_def_71, type, sF65: ((($i > $i) > $i) > $i)).
% 0.91/0.38 thf(func_def_72, type, sF66: !>[X0: $tType, X1: $tType]:((((($i > $i) > X0) > X1) > (($i > $i) > X0) > X1))).
% 0.91/0.38 thf(func_def_73, type, sF67: !>[X0: $tType]:(((($i > $i) > X0) > ((($i > $i) > X0) > ($i > $i) > X0) > ($i > $i) > X0))).
% 0.91/0.38 thf(func_def_74, type, sF68: !>[X0: $tType, X1: $tType]:((X1 > (X1 > X0) > ($i > $i) > X0))).
% 0.91/0.38 thf(func_def_75, type, sF69: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > (X0 > X2) > ($i > $i) > X1) > X0 > (X0 > X2) > ($i > $i) > X1))).
% 0.91/0.38 thf(func_def_76, type, sF70: !>[X0: $tType, X1: $tType]:(((X0 > ($i > $i) > X1) > X0 > ($i > $i) > X1))).
% 0.91/0.38 thf(func_def_77, type, sF71: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((((X1 > X3) > X2) > ($i > $i) > X0) > ((X1 > X3) > X2) > ($i > $i) > X0))).
% 0.91/0.38 thf(func_def_78, type, sF72: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((((X2 > X4) > X1) > ($i > $i) > X3 > X0) > ((X2 > X4) > X1) > ($i > $i) > X3 > X0))).
% 0.91/0.38 thf(func_def_79, type, sF73: !>[X0: $tType, X1: $tType, X2: $tType]:((((X0 > $i) > X2) > (((X0 > $i) > X2) > ($i > $i) > X1) > ($i > $i) > X1))).
% 0.91/0.38 thf(func_def_80, type, sF74: !>[X0: $tType, X1: $tType]:(((X0 > X0) > ((X0 > X0) > X1) > X1))).
% 0.91/0.38 thf(func_def_81, type, sF75: !>[X0: $tType]:((X0 > (X0 > X0) > X0))).
% 0.91/0.38 thf(func_def_82, type, sF76: ((($i > $i) > $i > $i) > ($i > $i) > $i > $i)).
% 0.91/0.38 thf(func_def_83, type, sF77: (((($i > $i) > $i > $i) > ($i > $i) > $i > $i) > (($i > $i) > $i > $i) > ($i > $i) > $i > $i)).
% 0.91/0.38 thf(func_def_84, type, sF78: !>[X0: $tType, X1: $tType]:(((($i > $i) > X0 > X1) > X0 > X1))).
% 0.91/0.38 thf(func_def_85, type, sF79: !>[X0: $tType]:(((($i > $i) > X0) > X0))).
% 0.91/0.38 thf(func_def_86, type, sF80: !>[X0: $tType, X1: $tType]:((((X0 > X1) > $i) > (X0 > X1) > $i))).
% 0.91/0.38 thf(func_def_87, type, sF81: ((($i > $i) > $i) > $i)).
% 0.91/0.38 thf(func_def_88, type, sF82: !>[X0: $tType]:(((($i > $i) > X0 > $i) > X0 > $i))).
% 0.91/0.38 thf(func_def_89, type, sF83: !>[X0: $tType, X1: $tType]:((((X0 > $i) > X1 > $i) > (X0 > $i) > X1 > $i))).
% 0.91/0.38 thf(f1,conjecture,(
% 0.91/0.38 ! [X0 : ((($i > $i) > $i) > (($i > $i) > $i) > $o)] : ? [X1 : (($i > $i) > $i)] : (! [X2 : (($i > $i) > $i)] : (X0 @ X2 @ X2) => (X0 @ (^[X3 : ($i > $i)] : ((X3 @ (X1 @ (^[X4 : $i] : (X4)))))) @ X1))),
% 0.91/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cUNIFTHM1)).
% 0.91/0.38 thf(f2,negated_conjecture,(
% 0.91/0.38 ~ ! [X0 : ((($i > $i) > $i) > (($i > $i) > $i) > $o)] : ? [X1 : (($i > $i) > $i)] : (! [X2 : (($i > $i) > $i)] : (X0 @ X2 @ X2) => (X0 @ (^[X3 : ($i > $i)] : ((X3 @ (X1 @ (^[X4 : $i] : (X4)))))) @ X1))),
% 0.91/0.38 inference(negated_conjecture,[status(cth)],[f1])).
% 0.91/0.38 thf(f3,plain,(
% 0.91/0.38 ~ ! [X0 : ((($i > $i) > $i) > (($i > $i) > $i) > $o)] : ? [X1 : (($i > $i) > $i)] : (! [X2 : (($i > $i) > $i)] : (X0 @ X2 @ X2) => (X0 @ (^[X3 : ($i > $i)] : ((X3 @ (X1 @ (^[X4 : $i] : (X4)))))) @ X1))),
% 0.91/0.38 inference(rectify,[],[f2])).
% 0.91/0.38 thf(f4,plain,(
% 0.91/0.38 ~ ! [X0 : ((($i > $i) > $i) > (($i > $i) > $i) > $o)] : ? [X1 : (($i > $i) > $i)] : (! [X2 : (($i > $i) > $i)] : (((X0 @ X2 @ X2)) = $true) => ($true = ((X0 @ (^[Y0 : $i > $i]: (Y0 @ (X1 @ (^[Y1 : $i]: (Y1))))) @ X1))))),
% 0.91/0.38 inference(fool_elimination,[],[f3])).
% 0.91/0.38 thf(f5,plain,(
% 0.91/0.38 ? [X0 : ((($i > $i) > $i) > (($i > $i) > $i) > $o)] : ! [X1 : (($i > $i) > $i)] : (($true != ((X0 @ (^[Y0 : $i > $i]: (Y0 @ (X1 @ (^[Y1 : $i]: (Y1))))) @ X1))) & ! [X2 : (($i > $i) > $i)] : (((X0 @ X2 @ X2)) = $true))),
% 0.91/0.38 inference(ennf_transformation,[],[f4])).
% 0.91/0.38 thf(f6,plain,(
% 0.91/0.38 ! [X1 : (($i > $i) > $i)] : (($true != ((sK0 @ (^[Y0 : $i > $i]: (Y0 @ (X1 @ (^[Y1 : $i]: (Y1))))) @ X1))) & ! [X2 : (($i > $i) > $i)] : ($true = ((sK0 @ X2 @ X2))))),
% 0.91/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f5])).
% 0.91/0.38 thf(f7,plain,(
% 0.91/0.38 ( ! [X2 : (($i > $i) > $i)] : (($true = ((sK0 @ X2 @ X2)))) )),
% 0.91/0.38 inference(cnf_transformation,[],[f6])).
% 0.91/0.38 thf(f8,plain,(
% 0.91/0.38 ( ! [X1 : (($i > $i) > $i)] : (($true != ((sK0 @ (^[Y0 : $i > $i]: (Y0 @ (X1 @ (^[Y1 : $i]: (Y1))))) @ X1)))) )),
% 0.91/0.38 inference(cnf_transformation,[],[f6])).
% 0.91/0.38 thf(f10,definition,(
% 0.91/0.38 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.91/0.38 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.91/0.38 thf(f32,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : (($true != $true) | ($false = ((sK0 @ (^[Y0 : $i > $i]: (Y0 @ (X0 @ (^[Y1 : $i]: (Y1))))) @ X0)))) )),
% 0.91/0.38 inference(constrained_superposition,[],[f8,f10])).
% 0.91/0.38 thf(f35,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : (($false = ((sK0 @ (^[Y0 : $i > $i]: (Y0 @ (X0 @ (^[Y1 : $i]: (Y1))))) @ X0)))) )),
% 0.91/0.38 inference(trivial_inequality_removal,[],[f32])).
% 0.91/0.38 thf(f38,definition,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : ((((sF6 @ X0)) = (^[Y0 : $i > $i]: (Y0 @ (X0 @ (^[Y1 : $i]: (Y1))))))) )),
% 0.91/0.38 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 0.91/0.38 thf(f39,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : (((^[Y0 : $i > $i]: (Y0 @ (X0 @ (^[Y1 : $i]: (Y1))))) = ((sF6 @ X0)))) )),
% 0.91/0.38 inference(reorient_equations,[],[f38])).
% 0.91/0.38 thf(f47,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : ($i > $i)] : (((((^[Y0 : $i > $i]: (Y0 @ (X0 @ (^[Y1 : $i]: (Y1))))) @ X1)) = ((sF6 @ X0 @ X1)))) )),
% 0.91/0.38 inference(argument_congruence,[],[f39])).
% 0.91/0.38 thf(f49,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : (($false = ((sK0 @ (sF6 @ X0) @ X1))) | ((^[Y0 : $i > $i]: (X0 @ (^[Y1 : $i]: (Y1)))) != (^[Y0 : $i > $i]: (X1 @ (^[Y1 : $i]: (Y1)))))) )),
% 0.91/0.38 inference(constrained_superposition,[],[f35,f39])).
% 0.91/0.38 thf(f51,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : ($i > $i)] : ((((sF6 @ X0 @ X1)) = ((X1 @ (X0 @ (^[Y0 : $i]: (Y0))))))) )),
% 0.91/0.38 inference(beta-eta_normalization,[],[f47])).
% 0.91/0.38 thf(f57,definition,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : ((((sF10 @ X0)) = (^[Y0 : $i > $i]: (X0 @ (^[Y1 : $i]: (Y1)))))) )),
% 0.91/0.38 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 0.91/0.38 thf(f58,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : (((^[Y0 : $i > $i]: (X0 @ (^[Y1 : $i]: (Y1)))) = ((sF10 @ X0)))) )),
% 0.91/0.38 inference(reorient_equations,[],[f57])).
% 0.91/0.38 thf(f67,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : (($true = $false) | ((^[Y0 : $i > $i]: (X0 @ (^[Y1 : $i]: (Y1)))) != (^[Y0 : $i > $i]: (sF6 @ X0 @ (^[Y1 : $i]: (Y1)))))) )),
% 0.91/0.38 inference(constrained_superposition,[],[f7,f49])).
% 0.91/0.38 thf(f68,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : (((^[Y0 : $i > $i]: (X0 @ (^[Y1 : $i]: (Y1)))) != (^[Y0 : $i > $i]: (sF6 @ X0 @ (^[Y1 : $i]: (Y1)))))) )),
% 0.91/0.38 inference(trivial_inequality_removal,[],[f67])).
% 0.91/0.38 thf(f79,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : (((^[Y0 : $i > $i]: (X0 @ (^[Y1 : $i]: (Y1)))) != ((sF10 @ (sF6 @ X0))))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f68,f58])).
% 0.91/0.38 thf(f81,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : ((((sF10 @ X0)) != ((sF10 @ (sF6 @ X0))))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f79,f58])).
% 0.91/0.38 thf(f83,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : ((((sF10 @ X0 @ (sK18 @ X0))) != ((sF10 @ (sF6 @ X0) @ (sK18 @ X0))))) )),
% 0.91/0.38 inference(negative_extensionality,[],[f81])).
% 0.91/0.38 thf(f113,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : ($i > $i)] : (((((^[Y0 : $i > $i]: (X0 @ (^[Y1 : $i]: (Y1)))) @ X1)) = ((sF10 @ X0 @ X1)))) )),
% 0.91/0.38 inference(argument_congruence,[],[f58])).
% 0.91/0.38 thf(f207,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : ($i > $i)] : ((((X0 @ (^[Y0 : $i]: (Y0)))) = ((sF10 @ X0 @ X1)))) )),
% 0.91/0.38 inference(beta-eta_normalization,[],[f113])).
% 0.91/0.38 thf(f214,definition,(
% 0.91/0.38 ( ! [X0 : $tType,X1 : X0] : ((((sF31 @ X0 @ X1)) = (^[Y0 : $i > $i]: (X1)))) )),
% 0.91/0.38 introduced(definition,[new_symbols(definition,[sF31])],[function_definition])).
% 0.91/0.38 thf(f215,plain,(
% 0.91/0.38 ( ! [X0 : $tType,X1 : X0] : (((^[Y0 : $i > $i]: (X1)) = ((sF31 @ X0 @ X1)))) )),
% 0.91/0.38 inference(reorient_equations,[],[f214])).
% 0.91/0.38 thf(f296,definition,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : ((((sF50 @ X0)) = (^[Y0 : $i > $i]: (Y0 @ (Y0 @ (X0 @ Y0)))))) )),
% 0.91/0.38 introduced(definition,[new_symbols(definition,[sF50])],[function_definition])).
% 0.91/0.38 thf(f297,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : (((^[Y0 : $i > $i]: (Y0 @ (Y0 @ (X0 @ Y0)))) = ((sF50 @ X0)))) )),
% 0.91/0.38 inference(reorient_equations,[],[f296])).
% 0.91/0.38 thf(f303,definition,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : ((((sF51 @ X0)) = ((X0 @ (^[Y0 : $i]: (Y0)))))) )),
% 0.91/0.38 introduced(definition,[new_symbols(definition,[sF51])],[function_definition])).
% 0.91/0.38 thf(f304,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : ((((X0 @ (^[Y0 : $i]: (Y0)))) = ((sF51 @ X0)))) )),
% 0.91/0.38 inference(reorient_equations,[],[f303])).
% 0.91/0.38 thf(f320,definition,(
% 0.91/0.38 (sF54 = (^[Y0 : $i]: (Y0)))),
% 0.91/0.38 introduced(definition,[new_symbols(definition,[sF54])],[function_definition])).
% 0.91/0.38 thf(f321,plain,(
% 0.91/0.38 ((^[Y0 : $i]: (Y0)) = sF54)),
% 0.91/0.38 inference(reorient_equations,[],[f320])).
% 0.91/0.38 thf(f418,plain,(
% 0.91/0.38 ( ! [X0 : $tType,X2 : ($i > $i),X1 : X0] : (((((^[Y0 : $i > $i]: (X1)) @ X2)) = ((sF31 @ X0 @ X1 @ X2)))) )),
% 0.91/0.38 inference(argument_congruence,[],[f215])).
% 0.91/0.38 thf(f431,plain,(
% 0.91/0.38 ( ! [X0 : $tType,X2 : ($i > $i),X1 : X0] : ((((sF31 @ X0 @ X1 @ X2)) = X1)) )),
% 0.91/0.38 inference(beta-eta_normalization,[],[f418])).
% 0.91/0.38 thf(f479,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i)] : ((((sF51 @ X0)) = ((X0 @ sF54)))) )),
% 0.91/0.38 inference(constrained_superposition,[],[f304,f321])).
% 0.91/0.38 thf(f511,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((sF10 @ X1 @ (sK18 @ X1))) != ((sF51 @ (^[Y0 : $i > $i]: (Y0 @ ((^[Y1 : $i > $i]: (Y1 @ (X0 @ Y1))) @ Y0)))))) | (((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF10 @ (sF6 @ X1) @ (sK18 @ X1))))) )),
% 0.91/0.38 inference(constrained_superposition,[],[f83,f304])).
% 0.91/0.38 thf(f527,plain,(
% 0.91/0.38 ( ! [X2 : ($i > $i),X0 : (($i > $i) > $i),X1 : $i] : ((((sF51 @ (^[Y0 : $i > $i]: (Y0 @ ((^[Y1 : $i > $i]: (Y1 @ (X0 @ Y1))) @ Y0))))) = X1) | (((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF31 @ $i @ X1 @ X2)))) )),
% 0.91/0.38 inference(constrained_superposition,[],[f431,f304])).
% 0.91/0.38 thf(f536,plain,(
% 0.91/0.38 ( ! [X2 : ($i > $i),X0 : (($i > $i) > $i),X1 : $i] : ((((sF51 @ (^[Y0 : $i > $i]: (Y0 @ (Y0 @ (X0 @ Y0)))))) = X1) | (((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF31 @ $i @ X1 @ X2)))) )),
% 0.91/0.38 inference(beta-eta_normalization,[],[f527])).
% 0.91/0.38 thf(f548,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((sF10 @ X1 @ (sK18 @ X1))) != ((sF51 @ (^[Y0 : $i > $i]: (Y0 @ (Y0 @ (X0 @ Y0))))))) | (((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF10 @ (sF6 @ X1) @ (sK18 @ X1))))) )),
% 0.91/0.38 inference(beta-eta_normalization,[],[f511])).
% 0.91/0.38 thf(f576,plain,(
% 0.91/0.38 ( ! [X2 : ($i > $i),X0 : (($i > $i) > $i),X1 : $i] : ((((sF51 @ (sF50 @ X0))) = X1) | (((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF31 @ $i @ X1 @ X2)))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f536,f297])).
% 0.91/0.38 thf(f592,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((sF10 @ X1 @ (sK18 @ X1))) != ((sF51 @ (sF50 @ X0)))) | (((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF10 @ (sF6 @ X1) @ (sK18 @ X1))))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f548,f297])).
% 0.91/0.38 thf(f631,plain,(
% 0.91/0.38 ( ! [X2 : ($i > $i),X0 : (($i > $i) > $i),X1 : $i] : ((((sF50 @ X0 @ sF54)) = X1) | (((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF31 @ $i @ X1 @ X2)))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f576,f479])).
% 0.91/0.38 thf(f654,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((sF10 @ X1 @ (sK18 @ X1))) != ((sF50 @ X0 @ sF54))) | (((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF10 @ (sF6 @ X1) @ (sK18 @ X1))))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f592,f479])).
% 0.91/0.38 thf(f703,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : $i] : ((((X0 @ (^[Y0 : $i]: (Y0)))) != X1) | (((sF50 @ X0 @ sF54)) = X1)) )),
% 0.91/0.38 inference(forward_demodulation,[],[f631,f431])).
% 0.91/0.38 thf(f723,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((X1 @ (^[Y0 : $i]: (Y0)))) != ((sF50 @ X0 @ sF54))) | (((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF10 @ (sF6 @ X1) @ (sK18 @ X1))))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f654,f207])).
% 0.91/0.38 thf(f770,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : $i] : ((((sF51 @ X0)) != X1) | (((sF50 @ X0 @ sF54)) = X1)) )),
% 0.91/0.38 inference(forward_demodulation,[],[f703,f304])).
% 0.91/0.38 thf(f786,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((sF51 @ X1)) != ((sF50 @ X0 @ sF54))) | (((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF10 @ (sF6 @ X1) @ (sK18 @ X1))))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f723,f304])).
% 0.91/0.38 thf(f821,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : $i] : ((((X0 @ sF54)) != X1) | (((sF50 @ X0 @ sF54)) = X1)) )),
% 0.91/0.38 inference(forward_demodulation,[],[f770,f479])).
% 0.91/0.38 thf(f834,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((sF50 @ X0 @ sF54)) != ((X1 @ sF54))) | (((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF10 @ (sF6 @ X1) @ (sK18 @ X1))))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f786,f479])).
% 0.91/0.38 thf(f870,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((X0 @ (^[Y0 : $i]: (Y0)))) != ((sF6 @ X1 @ (^[Y0 : $i]: (Y0))))) | (((sF50 @ X0 @ sF54)) != ((X1 @ sF54)))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f834,f207])).
% 0.91/0.38 thf(f878,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((X0 @ (^[Y0 : $i]: (Y0)))) != (((^[Y0 : $i]: (Y0)) @ (X1 @ (^[Y0 : $i]: (Y0)))))) | (((sF50 @ X0 @ sF54)) != ((X1 @ sF54)))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f870,f51])).
% 0.91/0.38 thf(f879,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((X1 @ (^[Y0 : $i]: (Y0)))) != ((X0 @ (^[Y0 : $i]: (Y0))))) | (((sF50 @ X0 @ sF54)) != ((X1 @ sF54)))) )),
% 0.91/0.38 inference(beta-eta_normalization,[],[f878])).
% 0.91/0.38 thf(f884,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((X1 @ (^[Y0 : $i]: (Y0)))) != ((sF51 @ X0))) | (((sF50 @ X0 @ sF54)) != ((X1 @ sF54)))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f879,f304])).
% 0.91/0.38 thf(f888,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((X1 @ (^[Y0 : $i]: (Y0)))) != ((X0 @ sF54))) | (((sF50 @ X0 @ sF54)) != ((X1 @ sF54)))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f884,f479])).
% 0.91/0.38 thf(f895,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((sF51 @ X1)) != ((X0 @ sF54))) | (((sF50 @ X0 @ sF54)) != ((X1 @ sF54)))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f888,f304])).
% 0.91/0.38 thf(f903,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((X0 @ sF54)) != ((X1 @ sF54))) | (((sF50 @ X0 @ sF54)) != ((X1 @ sF54)))) )),
% 0.91/0.38 inference(forward_demodulation,[],[f895,f479])).
% 0.91/0.38 thf(f904,plain,(
% 0.91/0.38 ( ! [X0 : (($i > $i) > $i),X1 : (($i > $i) > $i)] : ((((X0 @ sF54)) != ((X1 @ sF54)))) )),
% 0.91/0.38 inference(forward_subsumption_resolution,[],[f903,f821])).
% 0.91/0.38 thf(f905,plain,(
% 0.91/0.38 $false),
% 0.91/0.38 inference(flex-flex_simplification,[],[f904])).
% 0.91/0.38 % SZS output end Proof for theBenchmark
% 0.91/0.38 % (48689)------------------------------
% 0.91/0.38 % (48689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.38 % (48689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.38 % (48689)CaDiCaL version: 2.1.3
% 0.91/0.38 % (48689)Termination reason: Refutation
% 0.91/0.38 % (48689)Time elapsed: 0.063 s
% 0.91/0.38 % (48689)Peak memory usage: 13 MB
% 0.91/0.38 % (48689)Instructions burned: 124 (million)
% 0.91/0.38 % (48641)Success in time 0.136 s
% 0.91/0.38 % Vampire exiting
%------------------------------------------------------------------------------