%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO546^1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:50:24 AM UTC 2026
% Result : Theorem 0.20s 0.39s
% Output : Refutation 1.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO546^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n004.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 17:14:07 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.35 % (1591805)Will run a generic schedule for satisfiability detection.
% 0.20/0.35 % (1591813)dis+10_1_sil=32000:sp=arity:random_seed=2034472411:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.35 % (1591811)% WARNING: option uhcvi not known.
% 0.20/0.35 % (1591813)Refutation not found, incomplete strategy
% 0.20/0.35 % (1591813)------------------------------
% 0.20/0.35 % (1591813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (1591813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (1591813)CaDiCaL version: 2.1.3
% 0.20/0.35 % (1591813)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.35 % (1591813)Time elapsed: 0.004 s
% 0.20/0.35 % (1591813)Peak memory usage: 12 MB
% 0.20/0.35 % (1591813)Instructions burned: 13 (million)
% 0.20/0.35 % (1591813)------------------------------
% 0.20/0.35 % (1591813)------------------------------
% 0.20/0.35 % (1591810)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=166490744_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.35 % (1591811)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=281681659:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.35 % (1591812)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1885733615:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.35 % (1591811)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.35 % Exception at run slice level
% 0.20/0.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.35 % (1591811)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.20/0.35 % (1591811)Refutation not found, incomplete strategy
% 0.20/0.35 % (1591811)------------------------------
% 0.20/0.35 % (1591811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (1591811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (1591811)CaDiCaL version: 2.1.3
% 0.20/0.35 % (1591811)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.35 % (1591811)Time elapsed: 0.008 s
% 0.20/0.35 % (1591811)Peak memory usage: 12 MB
% 0.20/0.35 % (1591811)Instructions burned: 13 (million)
% 0.20/0.35 % (1591811)------------------------------
% 0.20/0.35 % (1591811)------------------------------
% 0.20/0.35 % (1591818)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=926952379:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.20/0.35 % Exception at run slice level
% 0.20/0.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.35 % (1591814)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=108343582:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.35 % (1591812)Refutation not found, incomplete strategy
% 0.20/0.35 % (1591812)------------------------------
% 0.20/0.35 % (1591812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (1591812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (1591812)CaDiCaL version: 2.1.3
% 0.20/0.35 % (1591812)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.35 % (1591812)Time elapsed: 0.014 s
% 0.20/0.35 % (1591812)Peak memory usage: 12 MB
% 0.20/0.35 % (1591812)Instructions burned: 22 (million)
% 0.20/0.35 % (1591814)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.35 % (1591812)------------------------------
% 0.20/0.35 % (1591812)------------------------------
% 0.20/0.35 % (1591816)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1391919700:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.35 % (1591822)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4276243503:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.35 % (1591825)ott-21_1_sil=16000:fs=off:random_seed=1053488332:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.20/0.35 % (1591815)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1702538240:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.35 % (1591822)Refutation not found, incomplete strategy
% 0.20/0.35 % (1591822)------------------------------
% 0.20/0.35 % (1591822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (1591822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591822)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591822)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591822)Time elapsed: 0.007 s
% 0.20/0.39 % (1591822)Peak memory usage: 12 MB
% 0.20/0.39 % (1591822)Instructions burned: 11 (million)
% 0.20/0.39 % (1591824)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=1095863911:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.20/0.39 % (1591822)------------------------------
% 0.20/0.39 % (1591822)------------------------------
% 0.20/0.39 % (1591824)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.39 % (1591824)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.20/0.39 % (1591815)Refutation not found, incomplete strategy
% 0.20/0.39 % (1591815)------------------------------
% 0.20/0.39 % (1591815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591815)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591815)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591815)Time elapsed: 0.011 s
% 0.20/0.39 % (1591815)Peak memory usage: 12 MB
% 0.20/0.39 % (1591815)Instructions burned: 12 (million)
% 0.20/0.39 % (1591827)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2620609759:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 0.20/0.39 % (1591814)Refutation not found, incomplete strategy
% 0.20/0.39 % (1591814)------------------------------
% 0.20/0.39 % (1591814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591814)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591814)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591814)Time elapsed: 0.022 s
% 0.20/0.39 % (1591814)Peak memory usage: 12 MB
% 0.20/0.39 % (1591814)Instructions burned: 23 (million)
% 0.20/0.39 % (1591815)------------------------------
% 0.20/0.39 % (1591815)------------------------------
% 0.20/0.39 % (1591814)------------------------------
% 0.20/0.39 % (1591814)------------------------------
% 0.20/0.39 % (1591816)Refutation not found, incomplete strategy
% 0.20/0.39 % (1591816)------------------------------
% 0.20/0.39 % (1591816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591816)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591816)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591816)Time elapsed: 0.017 s
% 0.20/0.39 % (1591816)Peak memory usage: 12 MB
% 0.20/0.39 % (1591816)Instructions burned: 13 (million)
% 0.20/0.39 % (1591816)------------------------------
% 0.20/0.39 % (1591816)------------------------------
% 0.20/0.39 % (1591824)Refutation not found, incomplete strategy
% 0.20/0.39 % (1591824)------------------------------
% 0.20/0.39 % (1591824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591824)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591824)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591824)Time elapsed: 0.011 s
% 0.20/0.39 % (1591824)Peak memory usage: 12 MB
% 0.20/0.39 % (1591824)Instructions burned: 19 (million)
% 0.20/0.39 % (1591824)------------------------------
% 0.20/0.39 % (1591824)------------------------------
% 0.20/0.39 % (1591833)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3576509683:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 0.20/0.39 % Exception at run slice level
% 0.20/0.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.39 % (1591836)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3586163343:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi)
% 0.20/0.39 % Exception at run slice level
% 0.20/0.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.39 % (1591827)Refutation not found, incomplete strategy
% 0.20/0.39 % (1591827)------------------------------
% 0.20/0.39 % (1591827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591827)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591827)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591827)Time elapsed: 0.023 s
% 0.20/0.39 % (1591827)Peak memory usage: 12 MB
% 0.20/0.39 % (1591827)Instructions burned: 40 (million)
% 0.20/0.39 % (1591827)------------------------------
% 0.20/0.39 % (1591827)------------------------------
% 0.20/0.39 % (1591838)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=825472901:i=879:kws=inv_precedence:fsr=off_2999 on theBenchmark for (2999ds/879Mi)
% 0.20/0.39 % (1591838)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.39 % (1591825)Instruction limit reached!
% 0.20/0.39 % (1591825)------------------------------
% 0.20/0.39 % (1591825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591825)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591825)Termination reason: Instruction limit
% 0.20/0.39 % (1591825)Termination phase: Saturation
% 0.20/0.39 % (1591825)Time elapsed: 0.044 s
% 0.20/0.39 % (1591825)Peak memory usage: 12 MB
% 0.20/0.39 % (1591825)Instructions burned: 181 (million)
% 0.20/0.39 % (1591840)fmb+10_1_sil=64000:random_seed=1160046371:i=22061:nm=2:gsp=on_2999 on theBenchmark for (2999ds/22061Mi)
% 0.20/0.39 % (1591835)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3236569531:i=1179_2999 on theBenchmark for (2999ds/1179Mi)
% 0.20/0.39 % (1591840)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 0.20/0.39 % Exception at run slice level
% 0.20/0.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.39 % (1591837)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=481692124: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.20/0.39 % (1591837)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.39 % (1591845)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1115685493:i=5131_2998 on theBenchmark for (2998ds/5131Mi)
% 0.20/0.39 % (1591845)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.39 % (1591842)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2205772853:i=9515:nm=5_2999 on theBenchmark for (2999ds/9515Mi)
% 0.20/0.39 % Exception at run slice level
% 0.20/0.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.39 % (1591843)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=165331354:fmbsr=1.7:i=920_2999 on theBenchmark for (2999ds/920Mi)
% 0.20/0.39 % Exception at run slice level
% 0.20/0.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.39 % (1591838)Refutation not found, incomplete strategy
% 0.20/0.39 % (1591838)------------------------------
% 0.20/0.39 % (1591838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591838)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591838)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591838)Time elapsed: 0.018 s
% 0.20/0.39 % (1591838)Peak memory usage: 12 MB
% 0.20/0.39 % (1591838)Instructions burned: 31 (million)
% 0.20/0.39 % (1591845)Refutation not found, incomplete strategy
% 0.20/0.39 % (1591845)------------------------------
% 0.20/0.39 % (1591845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591845)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591845)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591845)Time elapsed: 0.004 s
% 0.20/0.39 % (1591845)Peak memory usage: 12 MB
% 0.20/0.39 % (1591845)Instructions burned: 13 (million)
% 0.20/0.39 % (1591838)------------------------------
% 0.20/0.39 % (1591838)------------------------------
% 0.20/0.39 % (1591845)------------------------------
% 0.20/0.39 % (1591845)------------------------------
% 0.20/0.39 % (1591837)Refutation not found, incomplete strategy
% 0.20/0.39 % (1591837)------------------------------
% 0.20/0.39 % (1591837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591837)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591837)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591837)Time elapsed: 0.013 s
% 0.20/0.39 % (1591837)Peak memory usage: 12 MB
% 0.20/0.39 % (1591837)Instructions burned: 12 (million)
% 0.20/0.39 % (1591837)------------------------------
% 0.20/0.39 % (1591837)------------------------------
% 0.20/0.39 % (1591848)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2787607168:i=1472:ins=7:fdi=8:gsp=on_2998 on theBenchmark for (2998ds/1472Mi)
% 0.20/0.39 % (1591855)ott-2_1_sil=16000:newcnf=on:random_seed=1387626815:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2998 on theBenchmark for (2998ds/869Mi)
% 0.20/0.39 % (1591855)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.39 % (1591848)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 0.20/0.39 % (1591848)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.20/0.39 % (1591855)Refutation not found, incomplete strategy
% 0.20/0.39 % (1591855)------------------------------
% 0.20/0.39 % (1591855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591855)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591855)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591855)Time elapsed: 0.004 s
% 0.20/0.39 % (1591855)Peak memory usage: 12 MB
% 0.20/0.39 % (1591855)Instructions burned: 12 (million)
% 0.20/0.39 % (1591855)------------------------------
% 0.20/0.39 % (1591855)------------------------------
% 0.20/0.39 % (1591853)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2823314087:i=6324_2998 on theBenchmark for (2998ds/6324Mi)
% 0.20/0.39 % Exception at run slice level
% 0.20/0.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.39 % (1591854)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=103663993:fmbsr=2.30978:i=2174_2998 on theBenchmark for (2998ds/2174Mi)
% 0.20/0.39 % Exception at run slice level
% 0.20/0.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.39 % (1591856)ott+10_1_sil=32000:tgt=ground:random_seed=271951599:i=5114:av=off_2998 on theBenchmark for (2998ds/5114Mi)
% 0.20/0.39 % (1591863)dis+21_1_sil=32000:sas=cadical:random_seed=2048336681:i=3773:amm=off_2998 on theBenchmark for (2998ds/3773Mi)
% 0.20/0.39 % (1591835) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1591805-1591835"...
% 0.20/0.39 % (1591864)ott+11_1_sil=16000:gs=on:random_seed=4147933935:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2998 on theBenchmark for (2998ds/2251Mi)
% 0.20/0.39 % (1591864)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.20/0.39 % (1591863)Refutation not found, incomplete strategy
% 0.20/0.39 % (1591863)------------------------------
% 0.20/0.39 % (1591863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591863)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591863)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591863)Time elapsed: 0.007 s
% 0.20/0.39 % (1591863)Peak memory usage: 12 MB
% 0.20/0.39 % (1591863)Instructions burned: 13 (million)
% 0.20/0.39 % (1591864)Refutation not found, incomplete strategy
% 0.20/0.39 % (1591864)------------------------------
% 0.20/0.39 % (1591864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.39 % (1591864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.39 % (1591864)CaDiCaL version: 2.1.3
% 0.20/0.39 % (1591864)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.39 % (1591864)Time elapsed: 0.007 s
% 0.20/0.39 % (1591864)Peak memory usage: 12 MB
% 0.20/0.39 % (1591864)Instructions burned: 11 (million)
% 0.20/0.39 % (1591863)------------------------------
% 0.20/0.39 % (1591863)------------------------------
% 0.20/0.39 % (1591864)------------------------------
% 0.20/0.39 % (1591864)------------------------------
% 0.20/0.39 % (1591857)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3062061587:i=54282_2998 on theBenchmark for (2998ds/54282Mi)
% 0.20/0.39 % (1591835)...printing done.
% 0.20/0.39 % Exception at run slice level
% 0.20/0.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.39 % (1591835)Refutation found. Thanks to Tanya!
% 0.20/0.39 % SZS status Theorem for theBenchmark
% 0.20/0.39 % SZS output start Proof for theBenchmark
% 0.20/0.39 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.20/0.39 thf(func_def_0, type, eps: (($i > $o) > $i)).
% 0.20/0.39 thf(func_def_2, type, case: (($o > $o) > $i > $i > $i > $i > $i)).
% 0.20/0.39 thf(func_def_3, type, vNOT: ($o > $o)).
% 0.20/0.39 thf(func_def_4, type, f: ($o > $o)).
% 0.20/0.39 thf(func_def_7, type, vOR: ($o > $o > $o)).
% 0.20/0.39 thf(func_def_8, type, vAND: ($o > $o > $o)).
% 0.20/0.39 thf(func_def_9, type, db5: !>[X0: $tType]:(X0)).
% 0.20/0.39 thf(func_def_10, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.20/0.39 thf(func_def_11, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.20/0.39 thf(func_def_12, type, db4: !>[X0: $tType]:(X0)).
% 0.20/0.39 thf(func_def_13, type, db0: !>[X0: $tType]:(X0)).
% 0.20/0.39 thf(func_def_14, type, db3: !>[X0: $tType]:(X0)).
% 0.20/0.39 thf(func_def_15, type, db2: !>[X0: $tType]:(X0)).
% 0.20/0.39 thf(func_def_16, type, db1: !>[X0: $tType]:(X0)).
% 0.20/0.39 thf(func_def_20, type, sK3: $o).
% 0.20/0.39 thf(func_def_21, type, sK4: $o).
% 0.20/0.39 thf(func_def_22, type, sK5: $o).
% 0.20/0.39 thf(func_def_23, type, sK6: $o).
% 0.20/0.39 thf(func_def_24, type, sK7: $o).
% 0.20/0.39 thf(f1,axiom,(
% 0.20/0.39 ! [X0 : ($i > $o)] : (? [X1 : $i] : (X0 @ X1) => (X0 @ (eps @ X0)))),
% 0.20/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',choiceax)).
% 0.20/0.39 thf(f2,axiom,(
% 0.20/0.39 (case = (^[X0 : ($o > $o), X1 : $i, X2 : $i, X3 : $i, X4 : $i] : ((eps @ (^[X5 : $i] : (((X5 = X4) & (X0 = (^[X6 : $o] : ($true)))) | ((X5 = X3) & (X0 = (^[X6 : $o] : (X6)))) | ((X5 = X2) & (X0 = ~)) | ((X5 = X1) & (X0 = (^[X6 : $o] : ($false))))))))))),
% 0.20/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',caseood)).
% 0.20/0.39 thf(f3,conjecture,(
% 0.20/0.39 ! [X0 : $i] : (((case @ f @ X0 @ X0 @ X0 @ X0)) = X0)),
% 0.20/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 0.20/0.39 thf(f4,negated_conjecture,(
% 0.20/0.39 ~ ! [X0 : $i] : (((case @ f @ X0 @ X0 @ X0 @ X0)) = X0)),
% 0.20/0.39 inference(negated_conjecture,[status(cth)],[f3])).
% 0.20/0.39 thf(f5,plain,(
% 0.20/0.39 ! [X0 : ($i > $o)] : (? [X1 : $i] : (X0 @ X1) => (X0 @ (eps @ X0)))),
% 0.20/0.39 inference(rectify,[],[f1])).
% 0.20/0.39 thf(f6,plain,(
% 0.20/0.39 ! [X0 : ($i > $o)] : (? [X1 : $i] : (((X0 @ X1)) = $true) => (((X0 @ (eps @ X0))) = $true))),
% 0.20/0.39 inference(fool_elimination,[],[f5])).
% 0.20/0.39 thf(f7,plain,(
% 0.20/0.39 (case = (^[X0 : ($o > $o), X1 : $i, X2 : $i, X3 : $i, X4 : $i] : ((eps @ (^[X5 : $i] : (((X5 = X4) & (X0 = (^[X6 : $o] : ($true)))) | ((X5 = X3) & (X0 = (^[X7 : $o] : (X7)))) | ((X5 = X2) & (X0 = ~)) | ((X5 = X1) & (X0 = (^[X8 : $o] : ($false))))))))))),
% 0.20/0.39 inference(rectify,[],[f2])).
% 0.20/0.39 thf(f8,plain,(
% 0.20/0.39 (case = (^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))))),
% 0.20/0.39 inference(fool_elimination,[],[f7])).
% 0.20/0.39 thf(f9,plain,(
% 0.20/0.39 ! [X0 : ($i > $o)] : ((((X0 @ (eps @ X0))) = $true) | ! [X1 : $i] : (((X0 @ X1)) != $true))),
% 0.20/0.39 inference(ennf_transformation,[],[f6])).
% 0.20/0.39 thf(f10,plain,(
% 0.20/0.39 ? [X0 : $i] : (((case @ f @ X0 @ X0 @ X0 @ X0)) != X0)),
% 0.20/0.39 inference(ennf_transformation,[],[f4])).
% 0.20/0.39 thf(f11,plain,(
% 0.20/0.39 (sK0 != ((case @ f @ sK0 @ sK0 @ sK0 @ sK0)))),
% 0.20/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f10])).
% 0.20/0.39 thf(f12,plain,(
% 0.20/0.39 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ X1)) != $true) | (((X0 @ (eps @ X0))) = $true)) )),
% 0.20/0.39 inference(cnf_transformation,[],[f9])).
% 0.20/0.39 thf(f13,plain,(
% 0.20/0.39 (case = (^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))))),
% 0.20/0.39 inference(cnf_transformation,[],[f8])).
% 0.20/0.39 thf(f14,plain,(
% 0.20/0.39 (sK0 != ((case @ f @ sK0 @ sK0 @ sK0 @ sK0)))),
% 0.20/0.39 inference(cnf_transformation,[],[f11])).
% 0.20/0.39 thf(f16,definition,(
% 0.20/0.39 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.20/0.39 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.20/0.39 thf(f17,plain,(
% 0.20/0.39 (sK0 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))) @ f @ sK0 @ sK0 @ sK0 @ sK0)))),
% 0.20/0.39 inference(definition_unfolding,[],[f14,f13])).
% 0.20/0.39 thf(f18,definition,(
% 0.20/0.39 (sF1 = (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))) @ f @ sK0 @ sK0 @ sK0 @ sK0)))),
% 0.20/0.39 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 0.20/0.39 thf(f19,plain,(
% 0.20/0.39 ((((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))) @ f @ sK0 @ sK0 @ sK0 @ sK0)) = sF1)),
% 0.20/0.39 inference(reorient_equations,[],[f18])).
% 0.20/0.39 thf(f20,plain,(
% 0.20/0.39 (sK0 != sF1)),
% 0.20/0.39 inference(definition_folding,[],[f17,f19])).
% 0.20/0.39 thf(f21,plain,(
% 0.20/0.39 (sF1 = ((eps @ (^[Y0 : $i]: (((((f = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((~ = f) & (sK0 = Y0))) | ((f = (^[Y1 : $o]: (Y1))) & (sK0 = Y0))) | ((f = (^[Y1 : $o]: ($true))) & (sK0 = Y0)))))))),
% 0.20/0.39 inference(beta-eta_normalization,[],[f19])).
% 0.20/0.39 thf(f32,plain,(
% 0.20/0.39 ( ! [X2 : ($i > $o),X1 : $i] : (($true != (((^[Y0 : $i]: (~ (X2 @ Y0))) @ X1))) | ($true = (((^[Y0 : $i]: (~ (X2 @ Y0))) @ (eps @ (^[Y0 : $i]: (~ (X2 @ Y0)))))))) )),
% 0.20/0.39 inference(primitive_instantiation,[],[f12])).
% 0.20/0.39 thf(f34,plain,(
% 0.20/0.39 ( ! [X0 : ($i > $o),X1 : $i] : (($true != $true) | (((X0 @ (eps @ X0))) = $true) | (((X0 @ X1)) = $false)) )),
% 0.20/0.39 inference(constrained_superposition,[],[f12,f16])).
% 0.20/0.39 thf(f37,plain,(
% 0.20/0.39 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ (eps @ X0))) = $true) | (((X0 @ X1)) = $false)) )),
% 0.20/0.39 inference(trivial_inequality_removal,[],[f34])).
% 0.20/0.39 thf(f39,plain,(
% 0.20/0.39 ( ! [X2 : ($i > $o),X1 : $i] : (($true != ((~ (X2 @ X1)))) | ($true = ((~ (X2 @ (eps @ (^[Y0 : $i]: (~ (X2 @ Y0))))))))) )),
% 0.20/0.39 inference(beta-eta_normalization,[],[f32])).
% 0.20/0.39 thf(f40,plain,(
% 0.20/0.39 ( ! [X2 : ($i > $o),X1 : $i] : (($true = ((X2 @ X1))) | ($true = ((~ (X2 @ (eps @ (^[Y0 : $i]: (~ (X2 @ Y0))))))))) )),
% 0.20/0.39 inference(not_proxy_clausification,[],[f39])).
% 0.20/0.39 thf(f41,plain,(
% 0.20/0.39 ( ! [X2 : ($i > $o),X1 : $i] : (($true = ((X2 @ X1))) | ($false = ((X2 @ (eps @ (^[Y0 : $i]: (~ (X2 @ Y0)))))))) )),
% 0.20/0.39 inference(not_proxy_clausification,[],[f40])).
% 0.20/0.39 thf(f52,plain,(
% 0.20/0.39 ( ! [X0 : $i] : (($true = (((^[Y0 : $i]: (((((f = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((~ = f) & (sK0 = Y0))) | ((f = (^[Y1 : $o]: (Y1))) & (sK0 = Y0))) | ((f = (^[Y1 : $o]: ($true))) & (sK0 = Y0)))) @ sF1))) | ($false = (((^[Y0 : $i]: (((((f = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((~ = f) & (sK0 = Y0))) | ((f = (^[Y1 : $o]: (Y1))) & (sK0 = Y0))) | ((f = (^[Y1 : $o]: ($true))) & (sK0 = Y0)))) @ X0)))) )),
% 0.20/0.39 inference(constrained_superposition,[],[f37,f21])).
% 0.20/0.39 thf(f95,plain,(
% 0.20/0.39 ( ! [X0 : $i] : (($true = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: ($true))) & (sK0 = sF1))))) | ($false = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK0 = X0))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = X0))) | ((f = (^[Y0 : $o]: ($true))) & (sK0 = X0)))))) )),
% 0.20/0.39 inference(beta-eta_normalization,[],[f52])).
% 0.20/0.39 thf(f96,plain,(
% 0.20/0.39 ( ! [X0 : $i] : (($true = (((f = (^[Y0 : $o]: ($true))) & (sK0 = sF1)))) | ($false = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK0 = X0))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = X0))) | ((f = (^[Y0 : $o]: ($true))) & (sK0 = X0))))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f95])).
% 0.20/0.39 thf(f97,plain,(
% 0.20/0.39 ( ! [X0 : $i] : (($true = ((sK0 = sF1))) | ($false = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK0 = X0))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = X0))) | ((f = (^[Y0 : $o]: ($true))) & (sK0 = X0))))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f96])).
% 0.20/0.39 thf(f262,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK0 = X0))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = X0))) | ((f = (^[Y0 : $o]: ($true))) & (sK0 = X0))))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f97])).
% 0.20/0.39 thf(f263,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = (((f = (^[Y0 : $o]: ($true))) & (sK0 = X0)))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f262])).
% 0.20/0.39 thf(f264,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK0 = X0))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = X0))))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f262])).
% 0.20/0.39 thf(f265,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = (((f = (^[Y0 : $o]: (Y0))) & (sK0 = X0)))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f264])).
% 0.20/0.39 thf(f266,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK0 = X0))))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f264])).
% 0.20/0.39 thf(f267,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = (((~ = f) & (sK0 = X0)))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f266])).
% 0.20/0.39 thf(f268,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = (((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f266])).
% 0.20/0.39 thf(f269,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = ((sK0 = X0))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1))))) | ($false = ((f = (^[Y0 : $o]: ($false)))))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f268])).
% 0.20/0.39 thf(f270,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1))))) | ($false = ((f = (^[Y0 : $o]: ($false)))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f269])).
% 0.20/0.39 thf(f271,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))) | ($false = ((f = (^[Y0 : $o]: ($false))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f270])).
% 0.20/0.39 thf(f272,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = ((sK0 = sF1))) | ($false = ((f = (^[Y0 : $o]: ($false))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f271])).
% 0.20/0.39 thf(f292,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | ($false = ((f = (^[Y0 : $o]: ($false))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f272])).
% 0.20/0.39 thf(f293,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($false))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f292])).
% 0.20/0.39 thf(f294,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($false))) | ($true = (((~ = f) & (sK0 = sF1)))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f293])).
% 0.20/0.39 thf(f295,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($false))) | ($true = ((sK0 = sF1))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f294])).
% 0.20/0.39 thf(f304,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($false))) | (sK0 = sF1) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f295])).
% 0.20/0.39 thf(f305,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($false))) | (sK0 = sF1) | ($true = ((sK0 = sF1)))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f304])).
% 0.20/0.39 thf(f309,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($false))) | (sK0 = sF1) | (sK0 = sF1)) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f305])).
% 0.20/0.39 thf(f310,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (f != (^[Y0 : $o]: ($false)))) )),
% 0.20/0.39 inference(duplicate_literal_removal,[],[f309])).
% 0.20/0.39 thf(f311,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = ((sK0 = X0))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1))))) | ($false = ((~ = f)))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f267])).
% 0.20/0.39 thf(f312,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1))))) | ($false = ((~ = f)))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f311])).
% 0.20/0.39 thf(f313,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))) | ($false = ((~ = f))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f312])).
% 0.20/0.39 thf(f314,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = ((sK0 = sF1))) | ($false = ((~ = f))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f313])).
% 0.20/0.39 thf(f334,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | ($false = ((~ = f))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f314])).
% 0.20/0.39 thf(f335,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (~ != f) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f334])).
% 0.20/0.39 thf(f336,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (~ != f) | ($true = (((~ = f) & (sK0 = sF1)))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f335])).
% 0.20/0.39 thf(f337,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (~ != f) | ($true = ((sK0 = sF1))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f336])).
% 0.20/0.39 thf(f346,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (~ != f) | (sK0 = sF1) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f337])).
% 0.20/0.39 thf(f347,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (~ != f) | (sK0 = sF1) | ($true = ((sK0 = sF1)))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f346])).
% 0.20/0.39 thf(f351,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (~ != f) | (sK0 = sF1) | (sK0 = sF1)) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f347])).
% 0.20/0.39 thf(f352,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (~ != f)) )),
% 0.20/0.39 inference(duplicate_literal_removal,[],[f351])).
% 0.20/0.39 thf(f353,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = ((sK0 = X0))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1))))) | ($false = ((f = (^[Y0 : $o]: (Y0)))))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f265])).
% 0.20/0.39 thf(f354,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1))))) | ($false = ((f = (^[Y0 : $o]: (Y0)))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f353])).
% 0.20/0.39 thf(f355,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))) | ($false = ((f = (^[Y0 : $o]: (Y0))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f354])).
% 0.20/0.39 thf(f356,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = ((sK0 = sF1))) | ($false = ((f = (^[Y0 : $o]: (Y0))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f355])).
% 0.20/0.39 thf(f376,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | ($false = ((f = (^[Y0 : $o]: (Y0))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f356])).
% 0.20/0.39 thf(f377,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: (Y0))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f376])).
% 0.20/0.39 thf(f378,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: (Y0))) | ($true = (((~ = f) & (sK0 = sF1)))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 0.20/0.39 inference(or_proxy_clausification,[],[f377])).
% 0.20/0.39 thf(f379,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: (Y0))) | ($true = ((sK0 = sF1))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f378])).
% 0.20/0.39 thf(f388,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: (Y0))) | (sK0 = sF1) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f379])).
% 0.20/0.39 thf(f389,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: (Y0))) | (sK0 = sF1) | ($true = ((sK0 = sF1)))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f388])).
% 0.20/0.39 thf(f393,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: (Y0))) | (sK0 = sF1) | (sK0 = sF1)) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f389])).
% 0.20/0.39 thf(f394,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (f != (^[Y0 : $o]: (Y0)))) )),
% 0.20/0.39 inference(duplicate_literal_removal,[],[f393])).
% 0.20/0.39 thf(f395,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | ($false = ((sK0 = X0))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1))))) | ($false = ((f = (^[Y0 : $o]: ($true)))))) )),
% 0.20/0.39 inference(and_proxy_clausification,[],[f263])).
% 0.20/0.39 thf(f396,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1))) | ((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1))))) | ($false = ((f = (^[Y0 : $o]: ($true)))))) )),
% 0.20/0.39 inference(equality_proxy_clausification,[],[f395])).
% 0.20/0.39 thf(f397,plain,(
% 0.20/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK0 = sF1)))) | ($false = ((f = (^[Y0 : $o]: ($true))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 1.08/0.39 inference(or_proxy_clausification,[],[f396])).
% 1.08/0.39 thf(f398,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | ($true = ((sK0 = sF1))) | ($false = ((f = (^[Y0 : $o]: ($true))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 1.08/0.39 inference(and_proxy_clausification,[],[f397])).
% 1.08/0.39 thf(f418,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | ($false = ((f = (^[Y0 : $o]: ($true))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 1.08/0.39 inference(equality_proxy_clausification,[],[f398])).
% 1.08/0.39 thf(f419,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($true))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1)) | ((~ = f) & (sK0 = sF1)))))) )),
% 1.08/0.39 inference(equality_proxy_clausification,[],[f418])).
% 1.08/0.39 thf(f420,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($true))) | ($true = (((~ = f) & (sK0 = sF1)))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 1.08/0.39 inference(or_proxy_clausification,[],[f419])).
% 1.08/0.39 thf(f421,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($true))) | ($true = ((sK0 = sF1))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 1.08/0.39 inference(and_proxy_clausification,[],[f420])).
% 1.08/0.39 thf(f430,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($true))) | (sK0 = sF1) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF1))))) )),
% 1.08/0.39 inference(equality_proxy_clausification,[],[f421])).
% 1.08/0.39 thf(f431,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($true))) | (sK0 = sF1) | ($true = ((sK0 = sF1)))) )),
% 1.08/0.39 inference(and_proxy_clausification,[],[f430])).
% 1.08/0.39 thf(f435,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (sK0 = sF1) | (f != (^[Y0 : $o]: ($true))) | (sK0 = sF1) | (sK0 = sF1)) )),
% 1.08/0.39 inference(equality_proxy_clausification,[],[f431])).
% 1.08/0.39 thf(f436,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 = sF1) | (sK0 != X0) | (f != (^[Y0 : $o]: ($true)))) )),
% 1.08/0.39 inference(duplicate_literal_removal,[],[f435])).
% 1.08/0.39 thf(f466,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: ($false)))) )),
% 1.08/0.39 inference(forward_subsumption_resolution,[],[f310,f20])).
% 1.08/0.39 thf(f470,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 != X0) | (~ != f)) )),
% 1.08/0.39 inference(forward_subsumption_resolution,[],[f352,f20])).
% 1.08/0.39 thf(f474,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: (Y0)))) )),
% 1.08/0.39 inference(forward_subsumption_resolution,[],[f394,f20])).
% 1.08/0.39 thf(f482,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: ($true)))) )),
% 1.08/0.39 inference(forward_subsumption_resolution,[],[f436,f20])).
% 1.08/0.39 thf(f484,definition,(
% 1.08/0.39 spl2_1 <=> (~ = f)),
% 1.08/0.39 introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition])).
% 1.08/0.39 thf(f485,plain,(
% 1.08/0.39 (~ != f) | spl2_1),
% 1.08/0.39 inference(avatar_component_clause,[],[f484])).
% 1.08/0.39 thf(f488,definition,(
% 1.08/0.39 spl2_2 <=> (f = (^[Y0 : $o]: ($false)))),
% 1.08/0.39 introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition])).
% 1.08/0.39 thf(f490,plain,(
% 1.08/0.39 (f != (^[Y0 : $o]: ($false))) | spl2_2),
% 1.08/0.39 inference(avatar_component_clause,[],[f488])).
% 1.08/0.39 thf(f492,definition,(
% 1.08/0.39 spl2_3 <=> (f = (^[Y0 : $o]: (Y0)))),
% 1.08/0.39 introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition])).
% 1.08/0.39 thf(f493,plain,(
% 1.08/0.39 (f != (^[Y0 : $o]: (Y0))) | spl2_3),
% 1.08/0.39 inference(avatar_component_clause,[],[f492])).
% 1.08/0.39 thf(f496,definition,(
% 1.08/0.39 spl2_4 <=> ! [X0 : $i] : (sK0 != X0)),
% 1.08/0.39 introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition])).
% 1.08/0.39 thf(f497,plain,(
% 1.08/0.39 ( ! [X0 : $i] : ((sK0 != X0)) ) | ~spl2_4),
% 1.08/0.39 inference(avatar_component_clause,[],[f496])).
% 1.08/0.39 thf(f499,definition,(
% 1.08/0.39 spl2_5 <=> (f = (^[Y0 : $o]: ($true)))),
% 1.08/0.39 introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition])).
% 1.08/0.39 thf(f500,plain,(
% 1.08/0.39 (f != (^[Y0 : $o]: ($true))) | spl2_5),
% 1.08/0.39 inference(avatar_component_clause,[],[f499])).
% 1.08/0.39 thf(f517,plain,(
% 1.08/0.39 ~spl2_2 | spl2_4),
% 1.08/0.39 inference(avatar_split_clause,[],[f466,f496,f488])).
% 1.08/0.39 thf(f521,plain,(
% 1.08/0.39 ~spl2_1 | spl2_4),
% 1.08/0.39 inference(avatar_split_clause,[],[f470,f496,f484])).
% 1.08/0.39 thf(f525,plain,(
% 1.08/0.39 ~spl2_3 | spl2_4),
% 1.08/0.39 inference(avatar_split_clause,[],[f474,f496,f492])).
% 1.08/0.39 thf(f533,plain,(
% 1.08/0.39 ~spl2_5 | spl2_4),
% 1.08/0.39 inference(avatar_split_clause,[],[f482,f496,f499])).
% 1.08/0.39 thf(f621,plain,(
% 1.08/0.39 (((~ sK3)) != ((f @ sK3))) | spl2_1),
% 1.08/0.39 inference(negative_extensionality,[],[f485])).
% 1.08/0.39 thf(f622,plain,(
% 1.08/0.39 ($true = ((~ sK3))) | ($true = ((f @ sK3))) | spl2_1),
% 1.08/0.39 inference(xor_proxy_clausification,[],[f621])).
% 1.08/0.39 thf(f623,plain,(
% 1.08/0.39 ($false = ((~ sK3))) | ($false = ((f @ sK3))) | spl2_1),
% 1.08/0.39 inference(xor_proxy_clausification,[],[f621])).
% 1.08/0.39 thf(f624,plain,(
% 1.08/0.39 ($true = sK3) | ($false = ((f @ sK3))) | spl2_1),
% 1.08/0.39 inference(not_proxy_clausification,[],[f623])).
% 1.08/0.39 thf(f625,plain,(
% 1.08/0.39 ($false = sK3) | ($true = ((f @ sK3))) | spl2_1),
% 1.08/0.39 inference(not_proxy_clausification,[],[f622])).
% 1.08/0.39 thf(f627,definition,(
% 1.08/0.39 spl2_6 <=> ($false = ((f @ sK3)))),
% 1.08/0.39 introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition])).
% 1.08/0.39 thf(f629,plain,(
% 1.08/0.39 ($false = ((f @ sK3))) | ~spl2_6),
% 1.08/0.39 inference(avatar_component_clause,[],[f627])).
% 1.08/0.39 thf(f631,definition,(
% 1.08/0.39 spl2_7 <=> ($true = sK3)),
% 1.08/0.39 introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition])).
% 1.08/0.39 thf(f633,plain,(
% 1.08/0.39 ($true = sK3) | ~spl2_7),
% 1.08/0.39 inference(avatar_component_clause,[],[f631])).
% 1.08/0.39 thf(f634,plain,(
% 1.08/0.39 spl2_6 | spl2_7 | spl2_1),
% 1.08/0.39 inference(avatar_split_clause,[],[f624,f484,f631,f627])).
% 1.08/0.39 thf(f636,definition,(
% 1.08/0.39 spl2_8 <=> ($true = ((f @ sK3)))),
% 1.08/0.39 introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition])).
% 1.08/0.39 thf(f638,plain,(
% 1.08/0.39 ($true = ((f @ sK3))) | ~spl2_8),
% 1.08/0.39 inference(avatar_component_clause,[],[f636])).
% 1.08/0.39 thf(f640,definition,(
% 1.08/0.39 spl2_9 <=> ($false = sK3)),
% 1.08/0.39 introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition])).
% 1.08/0.39 thf(f642,plain,(
% 1.08/0.39 ($false = sK3) | ~spl2_9),
% 1.08/0.39 inference(avatar_component_clause,[],[f640])).
% 1.08/0.39 thf(f643,plain,(
% 1.08/0.39 spl2_8 | spl2_9 | spl2_1),
% 1.08/0.39 inference(avatar_split_clause,[],[f625,f484,f640,f636])).
% 1.08/0.39 thf(f1020,plain,(
% 1.08/0.39 $false | ~spl2_4),
% 1.08/0.39 inference(equality_resolution,[],[f497])).
% 1.08/0.39 thf(f1021,plain,(
% 1.08/0.39 ~spl2_4),
% 1.08/0.39 inference(avatar_contradiction_clause,[],[f1020])).
% 1.08/0.39 thf(f1022,plain,(
% 1.08/0.39 ($true = $false) | (~spl2_6 | ~spl2_8)),
% 1.08/0.39 inference(forward_demodulation,[],[f638,f629])).
% 1.08/0.39 thf(f1023,plain,(
% 1.08/0.39 $false | (~spl2_6 | ~spl2_8)),
% 1.08/0.39 inference(trivial_inequality_removal,[],[f1022])).
% 1.08/0.39 thf(f1024,plain,(
% 1.08/0.39 ~spl2_6 | ~spl2_8),
% 1.08/0.39 inference(avatar_contradiction_clause,[],[f1023])).
% 1.08/0.39 thf(f1184,plain,(
% 1.08/0.39 ($false = ((f @ $false))) | (~spl2_6 | ~spl2_9)),
% 1.08/0.39 inference(constrained_superposition,[],[f629,f642])).
% 1.08/0.39 thf(f1213,plain,(
% 1.08/0.39 (((f @ sK5)) != (((^[Y0 : $o]: ($false)) @ sK5))) | spl2_2),
% 1.08/0.39 inference(negative_extensionality,[],[f490])).
% 1.08/0.39 thf(f1214,plain,(
% 1.08/0.39 ($true = ((f @ sK5))) | ($true = (((^[Y0 : $o]: ($false)) @ sK5))) | spl2_2),
% 1.08/0.39 inference(xor_proxy_clausification,[],[f1213])).
% 1.08/0.39 thf(f1217,plain,(
% 1.08/0.39 ($true = ((f @ sK5))) | ($true = $false) | spl2_2),
% 1.08/0.39 inference(beta-eta_normalization,[],[f1214])).
% 1.08/0.39 thf(f1218,plain,(
% 1.08/0.39 ($true = ((f @ sK5))) | spl2_2),
% 1.08/0.39 inference(trivial_inequality_removal,[],[f1217])).
% 1.08/0.39 thf(f1253,plain,(
% 1.08/0.40 (((f @ sK6)) != (((^[Y0 : $o]: ($true)) @ sK6))) | spl2_5),
% 1.08/0.40 inference(negative_extensionality,[],[f500])).
% 1.08/0.40 thf(f1255,plain,(
% 1.08/0.40 ($false = ((f @ sK6))) | ($false = (((^[Y0 : $o]: ($true)) @ sK6))) | spl2_5),
% 1.08/0.40 inference(xor_proxy_clausification,[],[f1253])).
% 1.08/0.40 thf(f1256,plain,(
% 1.08/0.40 ($false = ((f @ sK6))) | ($true = $false) | spl2_5),
% 1.08/0.40 inference(beta-eta_normalization,[],[f1255])).
% 1.08/0.40 thf(f1257,plain,(
% 1.08/0.40 ($false = ((f @ sK6))) | spl2_5),
% 1.08/0.40 inference(trivial_inequality_removal,[],[f1256])).
% 1.08/0.40 thf(f1263,plain,(
% 1.08/0.40 ($true = ((f @ $false))) | ($true = (((^[Y0 : $i]: (sK5)) @ (eps @ (^[Y0 : $i]: (sK5)))))) | spl2_2),
% 1.08/0.40 inference(constrained_superposition,[],[f1218,f37])).
% 1.08/0.40 thf(f1286,plain,(
% 1.08/0.40 ($true = ((f @ $false))) | ($true = sK5) | spl2_2),
% 1.08/0.40 inference(beta-eta_normalization,[],[f1263])).
% 1.08/0.40 thf(f1290,plain,(
% 1.08/0.40 ($true = $false) | ($true = sK5) | (spl2_2 | ~spl2_6 | ~spl2_9)),
% 1.08/0.40 inference(forward_demodulation,[],[f1286,f1184])).
% 1.08/0.40 thf(f1291,plain,(
% 1.08/0.40 ($true = sK5) | (spl2_2 | ~spl2_6 | ~spl2_9)),
% 1.08/0.40 inference(trivial_inequality_removal,[],[f1290])).
% 1.08/0.40 thf(f1297,definition,(
% 1.08/0.40 spl2_15 <=> ($true = ((f @ $true)))),
% 1.08/0.40 introduced(definition,[new_symbols(definition,[spl2_15])],[avatar_definition])).
% 1.08/0.40 thf(f1299,plain,(
% 1.08/0.40 ($true = ((f @ $true))) | ~spl2_15),
% 1.08/0.40 inference(avatar_component_clause,[],[f1297])).
% 1.08/0.40 thf(f1305,plain,(
% 1.08/0.40 (((f @ sK7)) != (((^[Y0 : $o]: (Y0)) @ sK7))) | spl2_3),
% 1.08/0.40 inference(negative_extensionality,[],[f493])).
% 1.08/0.40 thf(f1306,plain,(
% 1.08/0.40 ($true = ((f @ sK7))) | ($true = (((^[Y0 : $o]: (Y0)) @ sK7))) | spl2_3),
% 1.08/0.40 inference(xor_proxy_clausification,[],[f1305])).
% 1.08/0.40 thf(f1307,plain,(
% 1.08/0.40 ($false = ((f @ sK7))) | ($false = (((^[Y0 : $o]: (Y0)) @ sK7))) | spl2_3),
% 1.08/0.40 inference(xor_proxy_clausification,[],[f1305])).
% 1.08/0.40 thf(f1308,plain,(
% 1.08/0.40 ($false = ((f @ sK7))) | ($false = sK7) | spl2_3),
% 1.08/0.40 inference(beta-eta_normalization,[],[f1307])).
% 1.08/0.40 thf(f1309,plain,(
% 1.08/0.40 ($true = ((f @ sK7))) | ($true = sK7) | spl2_3),
% 1.08/0.40 inference(beta-eta_normalization,[],[f1306])).
% 1.08/0.40 thf(f1311,definition,(
% 1.08/0.40 spl2_16 <=> ($false = sK7)),
% 1.08/0.40 introduced(definition,[new_symbols(definition,[spl2_16])],[avatar_definition])).
% 1.08/0.40 thf(f1312,plain,(
% 1.08/0.40 ($false != sK7) | spl2_16),
% 1.08/0.40 inference(avatar_component_clause,[],[f1311])).
% 1.08/0.40 thf(f1313,plain,(
% 1.08/0.40 ($false = sK7) | ~spl2_16),
% 1.08/0.40 inference(avatar_component_clause,[],[f1311])).
% 1.08/0.40 thf(f1315,definition,(
% 1.08/0.40 spl2_17 <=> ($false = ((f @ sK7)))),
% 1.08/0.40 introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition])).
% 1.08/0.40 thf(f1317,plain,(
% 1.08/0.40 ($false = ((f @ sK7))) | ~spl2_17),
% 1.08/0.40 inference(avatar_component_clause,[],[f1315])).
% 1.08/0.40 thf(f1318,plain,(
% 1.08/0.40 spl2_16 | spl2_17 | spl2_3),
% 1.08/0.40 inference(avatar_split_clause,[],[f1308,f492,f1315,f1311])).
% 1.08/0.40 thf(f1320,definition,(
% 1.08/0.40 spl2_18 <=> ($true = sK7)),
% 1.08/0.40 introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition])).
% 1.08/0.40 thf(f1322,plain,(
% 1.08/0.40 ($true = sK7) | ~spl2_18),
% 1.08/0.40 inference(avatar_component_clause,[],[f1320])).
% 1.08/0.40 thf(f1324,definition,(
% 1.08/0.40 spl2_19 <=> ($true = ((f @ sK7)))),
% 1.08/0.40 introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition])).
% 1.08/0.40 thf(f1326,plain,(
% 1.08/0.40 ($true = ((f @ sK7))) | ~spl2_19),
% 1.08/0.40 inference(avatar_component_clause,[],[f1324])).
% 1.08/0.40 thf(f1327,plain,(
% 1.08/0.40 spl2_18 | spl2_19 | spl2_3),
% 1.08/0.40 inference(avatar_split_clause,[],[f1309,f492,f1324,f1320])).
% 1.08/0.40 thf(f1328,plain,(
% 1.08/0.40 ($true = $false) | (~spl2_16 | ~spl2_18)),
% 1.08/0.40 inference(forward_demodulation,[],[f1322,f1313])).
% 1.08/0.40 thf(f1329,plain,(
% 1.08/0.40 $false | (~spl2_16 | ~spl2_18)),
% 1.08/0.40 inference(trivial_inequality_removal,[],[f1328])).
% 1.08/0.40 thf(f1330,plain,(
% 1.08/0.40 ~spl2_16 | ~spl2_18),
% 1.08/0.40 inference(avatar_contradiction_clause,[],[f1329])).
% 1.08/0.40 thf(f1335,plain,(
% 1.08/0.40 ($false != $false) | ($true = (((^[Y0 : $i]: (sK7)) @ (eps @ (^[Y0 : $i]: (sK7)))))) | spl2_16),
% 1.08/0.40 inference(constrained_superposition,[],[f1312,f37])).
% 1.08/0.40 thf(f1336,plain,(
% 1.08/0.40 ($true = (((^[Y0 : $i]: (sK7)) @ (eps @ (^[Y0 : $i]: (sK7)))))) | spl2_16),
% 1.08/0.40 inference(trivial_inequality_removal,[],[f1335])).
% 1.08/0.40 thf(f1337,plain,(
% 1.08/0.40 ($true = sK7) | spl2_16),
% 1.08/0.40 inference(beta-eta_normalization,[],[f1336])).
% 1.08/0.40 thf(f1373,plain,(
% 1.08/0.40 ($true = ((f @ $true))) | (spl2_2 | ~spl2_6 | ~spl2_9)),
% 1.08/0.40 inference(constrained_superposition,[],[f1218,f1291])).
% 1.08/0.40 thf(f1388,plain,(
% 1.08/0.40 spl2_15 | spl2_2 | ~spl2_6 | ~spl2_9),
% 1.08/0.40 inference(avatar_split_clause,[],[f1373,f640,f627,f488,f1297])).
% 1.08/0.40 thf(f1392,plain,(
% 1.08/0.40 ($false = ((f @ $true))) | ($false = (((^[Y0 : $i]: (sK6)) @ (eps @ (^[Y0 : $i]: (~ ((^[Y1 : $i]: (sK6)) @ Y0))))))) | spl2_5),
% 1.08/0.40 inference(constrained_superposition,[],[f1257,f41])).
% 1.08/0.40 thf(f1419,plain,(
% 1.08/0.40 ($false = ((f @ $true))) | ($false = sK6) | spl2_5),
% 1.08/0.40 inference(beta-eta_normalization,[],[f1392])).
% 1.08/0.40 thf(f1422,plain,(
% 1.08/0.40 ($true = $false) | ($false = sK6) | (spl2_5 | ~spl2_15)),
% 1.08/0.40 inference(forward_demodulation,[],[f1419,f1299])).
% 1.08/0.40 thf(f1423,plain,(
% 1.08/0.40 ($false = sK6) | (spl2_5 | ~spl2_15)),
% 1.08/0.40 inference(trivial_inequality_removal,[],[f1422])).
% 1.08/0.40 thf(f1468,plain,(
% 1.08/0.40 ($false = ((f @ $true))) | (~spl2_17 | ~spl2_18)),
% 1.08/0.40 inference(constrained_superposition,[],[f1317,f1322])).
% 1.08/0.40 thf(f1506,plain,(
% 1.08/0.40 ($false = ((f @ $false))) | (spl2_5 | ~spl2_15)),
% 1.08/0.40 inference(constrained_superposition,[],[f1257,f1423])).
% 1.08/0.40 thf(f1582,plain,(
% 1.08/0.40 ($true = $false) | (~spl2_15 | ~spl2_17 | ~spl2_18)),
% 1.08/0.40 inference(constrained_superposition,[],[f1468,f1299])).
% 1.08/0.40 thf(f1602,plain,(
% 1.08/0.40 $false | (~spl2_15 | ~spl2_17 | ~spl2_18)),
% 1.08/0.40 inference(trivial_inequality_removal,[],[f1582])).
% 1.08/0.40 thf(f1603,plain,(
% 1.08/0.40 ~spl2_15 | ~spl2_17 | ~spl2_18),
% 1.08/0.40 inference(avatar_contradiction_clause,[],[f1602])).
% 1.08/0.40 thf(f1612,plain,(
% 1.08/0.40 ($true = ((f @ $false))) | (~spl2_16 | ~spl2_19)),
% 1.08/0.40 inference(forward_demodulation,[],[f1326,f1313])).
% 1.08/0.40 thf(f1616,plain,(
% 1.08/0.40 ($true = ((f @ $true))) | (~spl2_7 | ~spl2_8)),
% 1.08/0.40 inference(forward_demodulation,[],[f638,f633])).
% 1.08/0.40 thf(f1639,plain,(
% 1.08/0.40 ($true = $false) | (spl2_5 | ~spl2_15 | ~spl2_16 | ~spl2_19)),
% 1.08/0.40 inference(forward_demodulation,[],[f1612,f1506])).
% 1.08/0.40 thf(f1640,plain,(
% 1.08/0.40 $false | (spl2_5 | ~spl2_15 | ~spl2_16 | ~spl2_19)),
% 1.08/0.40 inference(trivial_inequality_removal,[],[f1639])).
% 1.08/0.40 thf(f1641,plain,(
% 1.08/0.40 spl2_5 | ~spl2_15 | ~spl2_16 | ~spl2_19),
% 1.08/0.40 inference(avatar_contradiction_clause,[],[f1640])).
% 1.08/0.40 thf(f1700,plain,(
% 1.08/0.40 ($true = $false) | (~spl2_7 | ~spl2_9)),
% 1.08/0.40 inference(constrained_superposition,[],[f642,f633])).
% 1.08/0.40 thf(f1720,plain,(
% 1.08/0.40 $false | (~spl2_7 | ~spl2_9)),
% 1.08/0.40 inference(trivial_inequality_removal,[],[f1700])).
% 1.08/0.40 thf(f1721,plain,(
% 1.08/0.40 ~spl2_7 | ~spl2_9),
% 1.08/0.40 inference(avatar_contradiction_clause,[],[f1720])).
% 1.08/0.40 thf(f1732,plain,(
% 1.08/0.40 spl2_15 | ~spl2_7 | ~spl2_8),
% 1.08/0.40 inference(avatar_split_clause,[],[f1616,f636,f631,f1297])).
% 1.08/0.40 thf(f1734,plain,(
% 1.08/0.40 spl2_18 | spl2_16),
% 1.08/0.40 inference(avatar_split_clause,[],[f1337,f1311,f1320])).
% 1.08/0.40 cnf(s16, plain, ~spl2_2 | spl2_4, inference(sat_conversion,[],[f517])).
% 1.08/0.40 cnf(s20, plain, ~spl2_1 | spl2_4, inference(sat_conversion,[],[f521])).
% 1.08/0.40 cnf(s24, plain, ~spl2_3 | spl2_4, inference(sat_conversion,[],[f525])).
% 1.08/0.40 cnf(s32, plain, spl2_4 | ~spl2_5, inference(sat_conversion,[],[f533])).
% 1.08/0.40 cnf(s33, plain, spl2_1 | spl2_6 | spl2_7, inference(sat_conversion,[],[f634])).
% 1.08/0.40 cnf(s34, plain, spl2_1 | spl2_8 | spl2_9, inference(sat_conversion,[],[f643])).
% 1.08/0.40 cnf(s35, plain, ~spl2_4, inference(sat_conversion,[],[f1021])).
% 1.08/0.40 cnf(s36, plain, ~spl2_6 | ~spl2_8, inference(sat_conversion,[],[f1024])).
% 1.08/0.40 cnf(s43, plain, spl2_3 | spl2_16 | spl2_17, inference(sat_conversion,[],[f1318])).
% 1.08/0.40 cnf(s44, plain, spl2_3 | spl2_18 | spl2_19, inference(sat_conversion,[],[f1327])).
% 1.08/0.40 cnf(s45, plain, ~spl2_16 | ~spl2_18, inference(sat_conversion,[],[f1330])).
% 1.08/0.40 cnf(s46, plain, spl2_2 | ~spl2_6 | ~spl2_9 | spl2_15, inference(sat_conversion,[],[f1388])).
% 1.08/0.40 cnf(s51, plain, ~spl2_15 | ~spl2_17 | ~spl2_18, inference(sat_conversion,[],[f1603])).
% 1.08/0.40 cnf(s56, plain, spl2_5 | ~spl2_15 | ~spl2_16 | ~spl2_19, inference(sat_conversion,[],[f1641])).
% 1.08/0.40 cnf(s68, plain, ~spl2_7 | ~spl2_9, inference(sat_conversion,[],[f1721])).
% 1.08/0.40 cnf(s69, plain, ~spl2_7 | ~spl2_8 | spl2_15, inference(sat_conversion,[],[f1732])).
% 1.08/0.40 cnf(s70, plain, spl2_16 | spl2_18, inference(sat_conversion,[],[f1734])).
% 1.08/0.40 cnf(s74, plain, ~spl2_5, inference(rat,[],[s32,s35])).
% 1.08/0.40 cnf(s75, plain, ~spl2_3, inference(rat,[],[s24,s35])).
% 1.08/0.40 cnf(s76, plain, ~spl2_1, inference(rat,[],[s20,s35])).
% 1.08/0.40 cnf(s77, plain, ~spl2_2, inference(rat,[],[s16,s35])).
% 1.08/0.40 cnf(s78, plain, spl2_16 | ~spl2_15, inference(rat,[],[s51,s43,s70,s75])).
% 1.08/0.40 cnf(s79, plain, ~spl2_15, inference(rat,[],[s44,s56,s45,s78,s75,s74])).
% 1.08/0.40 cnf(s83, plain, ~spl2_7, inference(rat,[],[s34,s69,s68,s76,s79])).
% 1.08/0.40 cnf(s84, plain, spl2_6, inference(rat,[],[s33,s76,s83])).
% 1.08/0.40 cnf(s85, plain, ~spl2_8, inference(rat,[],[s36,s84])).
% 1.08/0.40 cnf(s86, plain, ~spl2_9, inference(rat,[],[s46,s79,s77,s84])).
% 1.08/0.40 cnf(s87, plain, $false, inference(rat,[],[s34,s76,s86,s85])).
% 1.08/0.40 thf(f1740,plain,(
% 1.08/0.40 $false),
% 1.08/0.40 inference(avatar_sat_refutation,[],[s87])).
% 1.08/0.40 % SZS output end Proof for theBenchmark
% 1.08/0.40 % (1591835)------------------------------
% 1.08/0.40 % (1591835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.40 % (1591835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.40 % (1591835)CaDiCaL version: 2.1.3
% 1.08/0.40 % (1591835)Termination reason: Refutation
% 1.08/0.40 % (1591835)Time elapsed: 0.056 s
% 1.08/0.40 % (1591835)Peak memory usage: 13 MB
% 1.08/0.40 % (1591835)Instructions burned: 55 (million)
% 1.08/0.40 % (1591805)Success in time 0.171 s
% 1.08/0.40 % Vampire exiting
%------------------------------------------------------------------------------