%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : DAT214^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:49:03 AM UTC 2026
% Result : Theorem 85.28s 14.31s
% Output : Refutation 85.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : DAT214^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.12 % Computer : n012.cluster.edu
% 0.08/0.12 % Model : x86_64 x86_64
% 0.08/0.12 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.12 % Memory : 8046.5625MB
% 0.08/0.12 % OS : Linux 6.8.0-71-generic
% 0.08/0.12 % CPULimit : 300
% 0.08/0.12 % WCLimit : 300
% 0.08/0.12 % DateTime : Tue Sep 29 18:09:18 UTC 2026
% 0.08/0.13 % CPUTime :
% 0.08/0.13 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.14 Running first-order model finding
% 0.08/0.14 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
% 3.46/0.76 % (486762)Will run a generic schedule for satisfiability detection.
% 3.46/0.76 % (486768)% WARNING: option uhcvi not known.
% 3.46/0.76 % (486768)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=712924671:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.46/0.76 % (486771)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3947212637:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.46/0.76 % (486770)dis+10_1_sil=32000:sp=arity:random_seed=4287149565:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.46/0.76 % (486767)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=479579969_2999 on theBenchmark for (2999ds/0Mi)
% 3.46/0.76 % (486773)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=766507303:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.46/0.76 % (486769)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1746417290:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.46/0.76 % (486771)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.46/0.76 % (486772)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3676071675:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.46/0.76 % (486768)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.46/0.76 % Exception at run slice level
% 3.46/0.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.46/0.76 % (486770)Instruction limit reached!
% 3.46/0.76 % (486770)------------------------------
% 3.46/0.76 % (486770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.46/0.76 % (486770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/0.76 % (486770)CaDiCaL version: 2.1.3
% 3.46/0.76 % (486770)Termination reason: Instruction limit
% 3.46/0.76 % (486770)Termination phase: Saturation
% 3.46/0.76 % (486770)Time elapsed: 0.025 s
% 3.46/0.76 % (486770)Peak memory usage: 12 MB
% 3.46/0.76 % (486770)Instructions burned: 105 (million)
% 3.46/0.76 % (486771)Instruction limit reached!
% 3.46/0.76 % (486771)------------------------------
% 3.46/0.76 % (486771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.46/0.76 % (486771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/0.76 % (486771)CaDiCaL version: 2.1.3
% 3.46/0.76 % (486771)Termination reason: Instruction limit
% 3.46/0.76 % (486771)Termination phase: Saturation
% 3.46/0.76 % (486771)Time elapsed: 0.028 s
% 3.46/0.76 % (486771)Peak memory usage: 13 MB
% 3.46/0.76 % (486771)Instructions burned: 119 (million)
% 3.46/0.76 % (486781)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4185571972:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.46/0.76 % (486768)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.46/0.76 % (486782)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=932438694:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.46/0.76 % (486784)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=4055386616:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.46/0.76 % (486773)Instruction limit reached!
% 3.46/0.76 % (486773)------------------------------
% 3.46/0.76 % (486773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.46/0.76 % (486773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/0.76 % (486773)CaDiCaL version: 2.1.3
% 3.46/0.76 % (486773)Termination reason: Instruction limit
% 3.46/0.76 % (486773)Termination phase: Saturation
% 3.46/0.76 % (486773)Time elapsed: 0.039 s
% 3.46/0.76 % (486773)Peak memory usage: 14 MB
% 3.46/0.76 % (486773)Instructions burned: 160 (million)
% 3.46/0.76 % (486784)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.46/0.76 % Exception at run slice level
% 3.46/0.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.46/0.76 % (486787)ott-21_1_sil=16000:fs=off:random_seed=1962380007:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 3.46/0.76 % (486784)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.46/0.76 % (486788)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2614735776:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 11.94/2.01 % (486772)Instruction limit reached!
% 11.94/2.01 % (486772)------------------------------
% 11.94/2.01 % (486772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.94/2.01 % (486772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.94/2.01 % (486772)CaDiCaL version: 2.1.3
% 11.94/2.01 % (486772)Termination reason: Instruction limit
% 11.94/2.01 % (486772)Termination phase: Saturation
% 11.94/2.01 % (486772)Time elapsed: 0.055 s
% 11.94/2.01 % (486772)Peak memory usage: 13 MB
% 11.94/2.01 % (486772)Instructions burned: 133 (million)
% 11.94/2.01 % (486782)Instruction limit reached!
% 11.94/2.01 % (486782)------------------------------
% 11.94/2.01 % (486782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.94/2.01 % (486782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.94/2.01 % (486782)CaDiCaL version: 2.1.3
% 11.94/2.01 % (486782)Termination reason: Instruction limit
% 11.94/2.01 % (486782)Termination phase: Saturation
% 11.94/2.01 % (486782)Time elapsed: 0.035 s
% 11.94/2.01 % (486782)Peak memory usage: 13 MB
% 11.94/2.01 % (486782)Instructions burned: 134 (million)
% 11.94/2.01 % (486792)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2215001886:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 11.94/2.01 % (486791)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1704714818:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 11.94/2.01 % Exception at run slice level
% 11.94/2.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 11.94/2.01 % (486787)Instruction limit reached!
% 11.94/2.01 % (486787)------------------------------
% 11.94/2.01 % (486787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.94/2.01 % (486787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.94/2.01 % (486787)CaDiCaL version: 2.1.3
% 11.94/2.01 % (486787)Termination reason: Instruction limit
% 11.94/2.01 % (486787)Termination phase: Saturation
% 11.94/2.01 % (486787)Time elapsed: 0.067 s
% 11.94/2.01 % (486787)Peak memory usage: 13 MB
% 11.94/2.01 % (486787)Instructions burned: 181 (million)
% 11.94/2.01 % (486795)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3094960898:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 11.94/2.01 % (486796)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=470020952:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 11.94/2.01 % (486796)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 11.94/2.01 % Exception at run slice level
% 11.94/2.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 11.94/2.01 % (486799)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1746832322:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 11.94/2.01 % (486799)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 11.94/2.01 % (486788)Instruction limit reached!
% 11.94/2.01 % (486788)------------------------------
% 11.94/2.01 % (486788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.94/2.01 % (486788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.94/2.01 % (486788)CaDiCaL version: 2.1.3
% 11.94/2.01 % (486788)Termination reason: Instruction limit
% 11.94/2.01 % (486788)Termination phase: Saturation
% 11.94/2.01 % (486788)Time elapsed: 0.129 s
% 11.94/2.01 % (486788)Peak memory usage: 14 MB
% 11.94/2.01 % (486788)Instructions burned: 478 (million)
% 11.94/2.01 % (486801)fmb+10_1_sil=64000:random_seed=524843229:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 11.94/2.01 % (486784)Instruction limit reached!
% 11.94/2.01 % (486784)------------------------------
% 11.94/2.01 % (486784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.94/2.01 % (486784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.94/2.01 % (486784)CaDiCaL version: 2.1.3
% 11.94/2.01 % (486784)Termination reason: Instruction limit
% 11.94/2.01 % (486784)Termination phase: Saturation
% 11.94/2.01 % (486784)Time elapsed: 0.170 s
% 11.94/2.01 % (486784)Peak memory usage: 15 MB
% 11.94/2.01 % (486784)Instructions burned: 687 (million)
% 11.94/2.01 % (486803)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3933752392:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 40.45/5.92 % (486801)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 40.45/5.92 % Exception at run slice level
% 40.45/5.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 40.45/5.92 % Exception at run slice level
% 40.45/5.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 40.45/5.92 % (486805)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=788544803:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 40.45/5.92 % (486806)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4073021677:i=5131_2997 on theBenchmark for (2997ds/5131Mi)
% 40.45/5.92 % (486806)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 40.45/5.92 % Exception at run slice level
% 40.45/5.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 40.45/5.92 % (486809)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2358718592:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi)
% 40.45/5.92 % (486809)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 40.45/5.92 % (486809)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 40.45/5.92 % (486796)Instruction limit reached!
% 40.45/5.92 % (486796)------------------------------
% 40.45/5.92 % (486796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/5.92 % (486796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/5.92 % (486796)CaDiCaL version: 2.1.3
% 40.45/5.92 % (486796)Termination reason: Instruction limit
% 40.45/5.92 % (486796)Termination phase: Saturation
% 40.45/5.92 % (486796)Time elapsed: 0.172 s
% 40.45/5.92 % (486796)Peak memory usage: 18 MB
% 40.45/5.92 % (486796)Instructions burned: 692 (million)
% 40.45/5.92 % (486811)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=116732547:i=6324_2996 on theBenchmark for (2996ds/6324Mi)
% 40.45/5.92 % Exception at run slice level
% 40.45/5.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 40.45/5.92 % (486813)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=782631261:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi)
% 40.45/5.92 % Exception at run slice level
% 40.45/5.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 40.45/5.92 % (486815)ott-2_1_sil=16000:newcnf=on:random_seed=1889948888:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi)
% 40.45/5.92 % (486815)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 40.45/5.92 % (486792)Instruction limit reached!
% 40.45/5.92 % (486792)------------------------------
% 40.45/5.92 % (486792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/5.92 % (486792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/5.92 % (486792)CaDiCaL version: 2.1.3
% 40.45/5.92 % (486792)Termination reason: Instruction limit
% 40.45/5.92 % (486792)Termination phase: Saturation
% 40.45/5.92 % (486792)Time elapsed: 0.306 s
% 40.45/5.92 % (486792)Peak memory usage: 18 MB
% 40.45/5.92 % (486792)Instructions burned: 1179 (million)
% 40.45/5.92 % (486817)ott+10_1_sil=32000:tgt=ground:random_seed=2213959803:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi)
% 40.45/5.92 % (486799)Instruction limit reached!
% 40.45/5.92 % (486799)------------------------------
% 40.45/5.92 % (486799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/5.92 % (486799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.45/5.92 % (486799)CaDiCaL version: 2.1.3
% 40.45/5.92 % (486799)Termination reason: Instruction limit
% 40.45/5.92 % (486799)Termination phase: Saturation
% 40.45/5.92 % (486799)Time elapsed: 0.388 s
% 40.45/5.92 % (486799)Peak memory usage: 18 MB
% 40.45/5.92 % (486799)Instructions burned: 881 (million)
% 40.45/5.92 % (486819)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2331786012:i=54282_2994 on theBenchmark for (2994ds/54282Mi)
% 40.45/5.92 % (486815)Instruction limit reached!
% 40.45/5.92 % (486815)------------------------------
% 40.45/5.92 % (486815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.45/5.92 % (486815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.90/11.43 % (486815)CaDiCaL version: 2.1.3
% 78.90/11.43 % (486815)Termination reason: Instruction limit
% 78.90/11.43 % (486815)Termination phase: Saturation
% 78.90/11.43 % (486815)Time elapsed: 0.206 s
% 78.90/11.43 % (486815)Peak memory usage: 17 MB
% 78.90/11.43 % (486815)Instructions burned: 871 (million)
% 78.90/11.43 % (486821)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1102033046:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 78.90/11.43 % Exception at run slice level
% 78.90/11.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 78.90/11.43 % (486821)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 78.90/11.43 % (486823)dis+21_1_sil=32000:sas=cadical:random_seed=3032842238:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi)
% 78.90/11.43 % (486809)Instruction limit reached!
% 78.90/11.43 % (486809)------------------------------
% 78.90/11.43 % (486809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.90/11.43 % (486809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.90/11.43 % (486809)CaDiCaL version: 2.1.3
% 78.90/11.43 % (486809)Termination reason: Instruction limit
% 78.90/11.43 % (486809)Termination phase: Saturation
% 78.90/11.43 % (486809)Time elapsed: 0.479 s
% 78.90/11.43 % (486809)Peak memory usage: 19 MB
% 78.90/11.43 % (486809)Instructions burned: 1475 (million)
% 78.90/11.43 % (486825)ott+11_1_sil=16000:gs=on:random_seed=30993075:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2992 on theBenchmark for (2992ds/2251Mi)
% 78.90/11.43 % (486825)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 78.90/11.43 % (486825)Instruction limit reached!
% 78.90/11.43 % (486825)------------------------------
% 78.90/11.43 % (486825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.90/11.43 % (486825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.90/11.43 % (486825)CaDiCaL version: 2.1.3
% 78.90/11.43 % (486825)Termination reason: Instruction limit
% 78.90/11.43 % (486825)Termination phase: Saturation
% 78.90/11.43 % (486825)Time elapsed: 0.792 s
% 78.90/11.43 % (486825)Peak memory usage: 24 MB
% 78.90/11.43 % (486825)Instructions burned: 2251 (million)
% 78.90/11.43 % (486821)Instruction limit reached!
% 78.90/11.43 % (486821)------------------------------
% 78.90/11.43 % (486821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.90/11.43 % (486821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.90/11.43 % (486821)CaDiCaL version: 2.1.3
% 78.90/11.43 % (486821)Termination reason: Instruction limit
% 78.90/11.43 % (486821)Termination phase: Saturation
% 78.90/11.43 % (486821)Time elapsed: 0.977 s
% 78.90/11.43 % (486821)Peak memory usage: 29 MB
% 78.90/11.43 % (486821)Instructions burned: 3512 (million)
% 78.90/11.43 % (486834)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3710338069:fmbsr=1.6:i=67534_2984 on theBenchmark for (2984ds/67534Mi)
% 78.90/11.43 % (486835)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2364278126:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi)
% 78.90/11.43 % Exception at run slice level
% 78.90/11.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 78.90/11.43 % (486838)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1539290409:i=29340_2983 on theBenchmark for (2983ds/29340Mi)
% 78.90/11.43 % (486806)Instruction limit reached!
% 78.90/11.43 % (486806)------------------------------
% 78.90/11.43 % (486806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.90/11.43 % (486806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.90/11.43 % (486806)CaDiCaL version: 2.1.3
% 78.90/11.43 % (486806)Termination reason: Instruction limit
% 78.90/11.43 % (486806)Termination phase: Saturation
% 78.90/11.43 % (486806)Time elapsed: 1.411 s
% 78.90/11.43 % (486806)Peak memory usage: 35 MB
% 78.90/11.43 % (486806)Instructions burned: 5132 (million)
% 78.90/11.43 % (486840)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3167732865:i=5211_2983 on theBenchmark for (2983ds/5211Mi)
% 78.90/11.43 % (486817)Instruction limit reached!
% 78.90/11.43 % (486817)------------------------------
% 78.90/11.43 % (486817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.90/11.43 % (486817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.07/13.81 % (486817)CaDiCaL version: 2.1.3
% 96.07/13.81 % (486817)Termination reason: Instruction limit
% 96.07/13.81 % (486817)Termination phase: Saturation
% 96.07/13.81 % (486817)Time elapsed: 1.433 s
% 96.07/13.81 % (486817)Peak memory usage: 37 MB
% 96.07/13.81 % (486817)Instructions burned: 5115 (million)
% 96.07/13.81 % (486842)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3843393383:i=5497:nm=2_2981 on theBenchmark for (2981ds/5497Mi)
% 96.07/13.81 % Exception at run slice level
% 96.07/13.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 96.07/13.81 % (486844)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1614005054:fmbsr=2:i=46332_2981 on theBenchmark for (2981ds/46332Mi)
% 96.07/13.81 % Exception at run slice level
% 96.07/13.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 96.07/13.81 % (486846)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=816467740:i=14071_2980 on theBenchmark for (2980ds/14071Mi)
% 96.07/13.81 % Exception at run slice level
% 96.07/13.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 96.07/13.81 % (486848)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1536966780:i=22565:add=on:rawr=on_2980 on theBenchmark for (2980ds/22565Mi)
% 96.07/13.81 % (486823)Instruction limit reached!
% 96.07/13.81 % (486823)------------------------------
% 96.07/13.81 % (486823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.07/13.81 % (486823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.07/13.81 % (486823)CaDiCaL version: 2.1.3
% 96.07/13.81 % (486823)Termination reason: Instruction limit
% 96.07/13.81 % (486823)Termination phase: Saturation
% 96.07/13.81 % (486823)Time elapsed: 1.654 s
% 96.07/13.81 % (486823)Peak memory usage: 30 MB
% 96.07/13.81 % (486823)Instructions burned: 3775 (million)
% 96.07/13.81 % (486850)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1343841898:i=8173:av=off_2976 on theBenchmark for (2976ds/8173Mi)
% 96.07/13.81 % (486840)Instruction limit reached!
% 96.07/13.81 % (486840)------------------------------
% 96.07/13.81 % (486840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.07/13.81 % (486840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.07/13.81 % (486840)CaDiCaL version: 2.1.3
% 96.07/13.81 % (486840)Termination reason: Instruction limit
% 96.07/13.81 % (486840)Termination phase: Saturation
% 96.07/13.81 % (486840)Time elapsed: 1.520 s
% 96.07/13.81 % (486840)Peak memory usage: 42 MB
% 96.07/13.81 % (486840)Instructions burned: 5215 (million)
% 96.07/13.81 % (486852)dis+10_16:1_sil=16000:random_seed=3807541607:i=9155:fsr=off_2967 on theBenchmark for (2967ds/9155Mi)
% 96.07/13.81 % (486835)Instruction limit reached!
% 96.07/13.81 % (486835)------------------------------
% 96.07/13.81 % (486835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.07/13.81 % (486835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.07/13.81 % (486835)CaDiCaL version: 2.1.3
% 96.07/13.81 % (486835)Termination reason: Instruction limit
% 96.07/13.81 % (486835)Termination phase: Saturation
% 96.07/13.81 % (486835)Time elapsed: 1.897 s
% 96.07/13.81 % (486835)Peak memory usage: 31 MB
% 96.07/13.81 % (486835)Instructions burned: 4593 (million)
% 96.07/13.81 % (486854)ott-3_8_sil=64000:random_seed=1822644755:i=20139:bs=on_2964 on theBenchmark for (2964ds/20139Mi)
% 96.07/13.81 % (486850)Instruction limit reached!
% 96.07/13.81 % (486850)------------------------------
% 96.07/13.81 % (486850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.07/13.81 % (486850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.07/13.81 % (486850)CaDiCaL version: 2.1.3
% 96.07/13.81 % (486850)Termination reason: Instruction limit
% 96.07/13.81 % (486850)Termination phase: Saturation
% 96.07/13.81 % (486850)Time elapsed: 3.343 s
% 96.07/13.81 % (486850)Peak memory usage: 57 MB
% 96.07/13.81 % (486850)Instructions burned: 8174 (million)
% 96.07/13.81 % (486866)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=728021504:fmbsr=2:i=32576_2943 on theBenchmark for (2943ds/32576Mi)
% 96.07/13.81 % Exception at run slice level
% 96.07/13.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 96.07/13.81 % (486868)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1410946660:i=11404_2942 on theBenchmark for (2942ds/11404Mi)
% 85.28/14.31 % (486852)Instruction limit reached!
% 85.28/14.31 % (486852)------------------------------
% 85.28/14.31 % (486852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486852)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486852)Termination reason: Instruction limit
% 85.28/14.31 % (486852)Termination phase: Saturation
% 85.28/14.31 % (486852)Time elapsed: 2.628 s
% 85.28/14.31 % (486852)Peak memory usage: 58 MB
% 85.28/14.31 % (486852)Instructions burned: 9156 (million)
% 85.28/14.31 % (486870)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=50388195:i=14134_2941 on theBenchmark for (2941ds/14134Mi)
% 85.28/14.31 % (486870)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 85.28/14.31 % (486848)Instruction limit reached!
% 85.28/14.31 % (486848)------------------------------
% 85.28/14.31 % (486848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486848)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486848)Termination reason: Instruction limit
% 85.28/14.31 % (486848)Termination phase: Saturation
% 85.28/14.31 % (486848)Time elapsed: 4.662 s
% 85.28/14.31 % (486848)Peak memory usage: 42 MB
% 85.28/14.31 % (486848)Instructions burned: 22568 (million)
% 85.28/14.31 % (486872)dis+33_16_sil=32000:sac=on:random_seed=1074499925:i=15851:nm=0_2933 on theBenchmark for (2933ds/15851Mi)
% 85.28/14.31 % (486854)Instruction limit reached!
% 85.28/14.31 % (486854)------------------------------
% 85.28/14.31 % (486854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486854)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486854)Termination reason: Instruction limit
% 85.28/14.31 % (486854)Termination phase: Saturation
% 85.28/14.31 % (486854)Time elapsed: 6.239 s
% 85.28/14.31 % (486854)Peak memory usage: 30 MB
% 85.28/14.31 % (486854)Instructions burned: 20141 (million)
% 85.28/14.31 % (486870)Instruction limit reached!
% 85.28/14.31 % (486870)------------------------------
% 85.28/14.31 % (486870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486870)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486870)Termination reason: Instruction limit
% 85.28/14.31 % (486870)Termination phase: Saturation
% 85.28/14.31 % (486870)Time elapsed: 3.901 s
% 85.28/14.31 % (486870)Peak memory usage: 84 MB
% 85.28/14.31 % (486870)Instructions burned: 14137 (million)
% 85.28/14.31 % (486874)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2118004040:avsq=on:i=17627:add=on:amm=off_2902 on theBenchmark for (2902ds/17627Mi)
% 85.28/14.31 % (486875)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2032673544:s2a=on:i=53295_2902 on theBenchmark for (2902ds/53295Mi)
% 85.28/14.31 % (486868)Instruction limit reached!
% 85.28/14.31 % (486868)------------------------------
% 85.28/14.31 % (486868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486868)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486868)Termination reason: Instruction limit
% 85.28/14.31 % (486868)Termination phase: Saturation
% 85.28/14.31 % (486868)Time elapsed: 5.149 s
% 85.28/14.31 % (486868)Peak memory usage: 81 MB
% 85.28/14.31 % (486868)Instructions burned: 11406 (million)
% 85.28/14.31 % (486878)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3787096102:i=26857:ins=20_2890 on theBenchmark for (2890ds/26857Mi)
% 85.28/14.31 % Exception at run slice level
% 85.28/14.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 85.28/14.31 % (486880)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3980201916:i=28120:bs=on:fsr=off_2890 on theBenchmark for (2890ds/28120Mi)
% 85.28/14.31 % (486872)Instruction limit reached!
% 85.28/14.31 % (486872)------------------------------
% 85.28/14.31 % (486872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486872)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486872)Termination reason: Instruction limit
% 85.28/14.31 % (486872)Termination phase: Saturation
% 85.28/14.31 % (486872)Time elapsed: 4.613 s
% 85.28/14.31 % (486872)Peak memory usage: 33 MB
% 85.28/14.31 % (486872)Instructions burned: 15855 (million)
% 85.28/14.31 % (486882)fmb+10_1_sil=256000:fmbss=7:random_seed=2974667091:fmbsr=1.6:i=182295_2887 on theBenchmark for (2887ds/182295Mi)
% 85.28/14.31 % Exception at run slice level
% 85.28/14.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 85.28/14.31 % (486884)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2155343648:i=44625:gsp=on_2886 on theBenchmark for (2886ds/44625Mi)
% 85.28/14.31 % (486884)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 85.28/14.31 % (486884)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 85.28/14.31 % Exception at run slice level
% 85.28/14.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 85.28/14.31 % (486886)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2210006599:i=160505_2886 on theBenchmark for (2886ds/160505Mi)
% 85.28/14.31 % Exception at run slice level
% 85.28/14.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 85.28/14.31 % (486888)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=756988287:fmbsr=1.3:i=225729_2886 on theBenchmark for (2886ds/225729Mi)
% 85.28/14.31 % Exception at run slice level
% 85.28/14.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 85.28/14.31 % (486890)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2056563559:fmbsr=2:i=185024:ins=7_2885 on theBenchmark for (2885ds/185024Mi)
% 85.28/14.31 % Exception at run slice level
% 85.28/14.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 85.28/14.31 % (486892)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1464201371:rtra=on_2885 on theBenchmark for (2885ds/0Mi)
% 85.28/14.31 % Exception at run slice level
% 85.28/14.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 85.28/14.31 % (486894)% WARNING: option uhcvi not known.
% 85.28/14.31 % (486894)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=254504826:i=271062:add=off:rtra=on:rawr=on_2885 on theBenchmark for (2885ds/271062Mi)
% 85.28/14.31 % (486894)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 85.28/14.31 % (486894)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 85.28/14.31 % (486838)Instruction limit reached!
% 85.28/14.31 % (486838)------------------------------
% 85.28/14.31 % (486838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486838)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486838)Termination reason: Instruction limit
% 85.28/14.31 % (486838)Termination phase: Saturation
% 85.28/14.31 % (486838)Time elapsed: 10.508 s
% 85.28/14.31 % (486838)Peak memory usage: 143 MB
% 85.28/14.31 % (486838)Instructions burned: 29342 (million)
% 85.28/14.31 % (486897)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1733219811:i=176048:add=on:rtra=on:rawr=on_2878 on theBenchmark for (2878ds/176048Mi)
% 85.28/14.31 % (486874)Instruction limit reached!
% 85.28/14.31 % (486874)------------------------------
% 85.28/14.31 % (486874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486874)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486874)Termination reason: Instruction limit
% 85.28/14.31 % (486874)Termination phase: Saturation
% 85.28/14.31 % (486874)Time elapsed: 3.793 s
% 85.28/14.31 % (486874)Peak memory usage: 20 MB
% 85.28/14.31 % (486874)Instructions burned: 17633 (million)
% 85.28/14.31 % (486906)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4008011232:i=206:fgj=on:rtra=on_2863 on theBenchmark for (2863ds/206Mi)
% 85.28/14.31 % (486906)Instruction limit reached!
% 85.28/14.31 % (486906)------------------------------
% 85.28/14.31 % (486906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486906)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486906)Termination reason: Instruction limit
% 85.28/14.31 % (486906)Termination phase: Saturation
% 85.28/14.31 % (486906)Time elapsed: 0.051 s
% 85.28/14.31 % (486906)Peak memory usage: 13 MB
% 85.28/14.31 % (486906)Instructions burned: 207 (million)
% 85.28/14.31 % (486908)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2563209209:i=232:rtra=on_2863 on theBenchmark for (2863ds/232Mi)
% 85.28/14.31 % (486908)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 85.28/14.31 % (486908)Instruction limit reached!
% 85.28/14.31 % (486908)------------------------------
% 85.28/14.31 % (486908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486908)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486908)Termination reason: Instruction limit
% 85.28/14.31 % (486908)Termination phase: Saturation
% 85.28/14.31 % (486908)Time elapsed: 0.057 s
% 85.28/14.31 % (486908)Peak memory usage: 14 MB
% 85.28/14.31 % (486908)Instructions burned: 233 (million)
% 85.28/14.31 % (486910)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3343973363:i=262:rtra=on_2862 on theBenchmark for (2862ds/262Mi)
% 85.28/14.31 % (486910)Instruction limit reached!
% 85.28/14.31 % (486910)------------------------------
% 85.28/14.31 % (486910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486910)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486910)Termination reason: Instruction limit
% 85.28/14.31 % (486910)Termination phase: Saturation
% 85.28/14.31 % (486910)Time elapsed: 0.066 s
% 85.28/14.31 % (486910)Peak memory usage: 14 MB
% 85.28/14.31 % (486910)Instructions burned: 263 (million)
% 85.28/14.31 % (486912)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1613092827:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2861 on theBenchmark for (2861ds/318Mi)
% 85.28/14.31 % (486912)Instruction limit reached!
% 85.28/14.31 % (486912)------------------------------
% 85.28/14.31 % (486912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486912)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486912)Termination reason: Instruction limit
% 85.28/14.31 % (486912)Termination phase: Saturation
% 85.28/14.31 % (486912)Time elapsed: 0.078 s
% 85.28/14.31 % (486912)Peak memory usage: 14 MB
% 85.28/14.31 % (486912)Instructions burned: 318 (million)
% 85.28/14.31 % (486914)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=547703660:i=1428:nm=2:rtra=on_2860 on theBenchmark for (2860ds/1428Mi)
% 85.28/14.31 % Exception at run slice level
% 85.28/14.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 85.28/14.31 % (486916)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2994982154:i=262:bd=preordered:rtra=on:fsd=on_2860 on theBenchmark for (2860ds/262Mi)
% 85.28/14.31 % (486916)Instruction limit reached!
% 85.28/14.31 % (486916)------------------------------
% 85.28/14.31 % (486916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486916)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486916)Termination reason: Instruction limit
% 85.28/14.31 % (486916)Termination phase: Saturation
% 85.28/14.31 % (486916)Time elapsed: 0.072 s
% 85.28/14.31 % (486916)Peak memory usage: 14 MB
% 85.28/14.31 % (486916)Instructions burned: 262 (million)
% 85.28/14.31 % (486918)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=827330087:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2859 on theBenchmark for (2859ds/1368Mi)
% 85.28/14.31 % (486918)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 85.28/14.31 % (486918)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 85.28/14.31 % (486768) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-486762-486768"...
% 85.28/14.31 % (486768)...printing done.
% 85.28/14.31 % (486768)Refutation found. Thanks to Tanya!
% 85.28/14.31 % SZS status Theorem for theBenchmark
% 85.28/14.31 % SZS output start Proof for theBenchmark
% 85.28/14.31 thf(type_def_5, type, splay_2011811431op_s_t: $tType > $tType).
% 85.28/14.31 thf(type_def_6, type, code_natural: $tType).
% 85.28/14.31 thf(type_def_7, type, product_prod: ($tType * $tType) > $tType).
% 85.28/14.31 thf(type_def_8, type, sum_sum: ($tType * $tType) > $tType).
% 85.28/14.31 thf(type_def_9, type, tree: $tType > $tType).
% 85.28/14.31 thf(type_def_10, type, real: $tType).
% 85.28/14.31 thf(type_def_11, type, nat: $tType).
% 85.28/14.31 thf(type_def_12, type, itself: $tType > $tType).
% 85.28/14.31 thf(type_def_13, type, a: $tType).
% 85.28/14.31 thf(type_def_14, type, sTfun: ($tType * $tType) > $tType).
% 85.28/14.31 thf(func_def_0, type, type: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_1, type, size: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_2, type, one: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_3, type, zero: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_4, type, neg_numeral: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_5, type, group_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_6, type, monoid_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_7, type, ln: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_8, type, linorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_9, type, zero_neq_one: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_10, type, zero_less_one: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_11, type, semigroup_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_12, type, comm_semiring_1: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_13, type, linordered_idom: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_14, type, comm_monoid_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_15, type, linordered_field: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_16, type, ab_semigroup_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_17, type, linordered_semidom: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_18, type, cancel_semigroup_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_19, type, cancel1352612707id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_20, type, linord219039673up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_21, type, ordere216010020id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_22, type, ordere779506340up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_23, type, linord1659791738miring: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_24, type, canoni770627133id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_25, type, strict797366125id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_26, type, ordere236663937imp_le: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_27, type, ordere223160158up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_28, type, strict2144017051up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_29, type, ordere516151231imp_le: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_30, type, semiri456707255roduct: !>[X0: $tType]:((itself @ X0 > $o))).
% 85.28/14.31 thf(func_def_31, type, code_case_natural: !>[X0: $tType]:((X0 > (code_natural > X0) > code_natural > X0))).
% 85.28/14.31 thf(func_def_32, type, code_rec_natural: !>[X0: $tType]:((X0 > (code_natural > X0 > X0) > code_natural > X0))).
% 85.28/14.31 thf(func_def_33, type, code_size_natural: (code_natural > nat)).
% 85.28/14.31 thf(func_def_34, type, one_one: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_35, type, plus_plus: !>[X0: $tType]:((X0 > X0 > X0))).
% 85.28/14.31 thf(func_def_36, type, zero_zero: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_37, type, size_bool: ($o > nat)).
% 85.28/14.31 thf(func_def_38, type, if: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 85.28/14.31 thf(func_def_39, type, size_size: !>[X0: $tType]:((X0 > nat))).
% 85.28/14.31 thf(func_def_40, type, neg_numeral_dbl_dec: !>[X0: $tType]:((X0 > X0))).
% 85.28/14.31 thf(func_def_41, type, neg_numeral_dbl_inc: !>[X0: $tType]:((X0 > X0))).
% 85.28/14.31 thf(func_def_42, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 85.28/14.31 thf(func_def_43, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 85.28/14.31 thf(func_def_44, type, product_rec_bool: !>[X0: $tType]:((X0 > X0 > $o > X0))).
% 85.28/14.31 thf(func_def_45, type, type2: !>[X0: $tType]:(itself @ X0)).
% 85.28/14.31 thf(func_def_46, type, set_fo292404081st_nat: !>[X0: $tType]:(((nat > X0 > X0) > nat > nat > X0 > X0))).
% 85.28/14.31 thf(func_def_47, type, splay_splay: !>[X0: $tType]:((X0 > tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_48, type, splay_splay_max: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_49, type, splay_914434265_splay: !>[X0: $tType]:((X0 > tree @ X0 > nat))).
% 85.28/14.31 thf(func_def_50, type, splay_878424299ay_max: !>[X0: $tType]:((tree @ X0 > nat))).
% 85.28/14.31 thf(func_def_51, type, splay_1816415694ax_rel: !>[X0: $tType]:((tree @ X0 > tree @ X0 > $o))).
% 85.28/14.31 thf(func_def_52, type, splay_266122055elle_A: !>[X0: $tType]:((X0 > tree @ X0 > real))).
% 85.28/14.31 thf(func_def_53, type, ln_ln: !>[X0: $tType]:((X0 > X0))).
% 85.28/14.31 thf(func_def_54, type, powr: !>[X0: $tType]:((X0 > X0 > X0))).
% 85.28/14.31 thf(func_def_55, type, linorder_bst: !>[X0: $tType]:((tree @ X0 > $o))).
% 85.28/14.31 thf(func_def_56, type, path_len: !>[X0: $tType]:((tree @ X0 > nat))).
% 85.28/14.31 thf(func_def_57, type, path_len_rel: !>[X0: $tType]:((tree @ X0 > tree @ X0 > $o))).
% 85.28/14.31 thf(func_def_58, type, size1: !>[X0: $tType]:((tree @ X0 > nat))).
% 85.28/14.31 thf(func_def_59, type, leaf: !>[X0: $tType]:(tree @ X0)).
% 85.28/14.31 thf(func_def_60, type, node: !>[X0: $tType]:((tree @ X0 > X0 > tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_61, type, size_tree: !>[X0: $tType]:(((X0 > nat) > tree @ X0 > nat))).
% 85.28/14.31 thf(func_def_62, type, accp: !>[X0: $tType]:(((X0 > X0 > $o) > X0 > $o))).
% 85.28/14.31 thf(func_def_63, type, b: a).
% 85.28/14.31 thf(func_def_64, type, c: a).
% 85.28/14.31 thf(func_def_65, type, l: tree @ a).
% 85.28/14.31 thf(func_def_66, type, l2: tree @ a).
% 85.28/14.31 thf(func_def_67, type, r: tree @ a).
% 85.28/14.31 thf(func_def_68, type, rl: tree @ a).
% 85.28/14.31 thf(func_def_69, type, rr: tree @ a).
% 85.28/14.31 thf(func_def_70, type, u: a).
% 85.28/14.31 thf(func_def_74, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 85.28/14.31 thf(func_def_75, type, db0: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_76, type, db1: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_77, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 85.28/14.31 thf(func_def_78, type, vAND: ($o > $o > $o)).
% 85.28/14.31 thf(func_def_79, type, vNOT: ($o > $o)).
% 85.28/14.31 thf(func_def_80, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 85.28/14.31 thf(func_def_81, type, db2: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_82, type, vOR: ($o > $o > $o)).
% 85.28/14.31 thf(func_def_83, type, db3: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_84, type, sP0: !>[X0: $tType]:((tree @ X0 > nat > $o))).
% 85.28/14.31 thf(func_def_85, type, sP1: !>[X0: $tType]:((tree @ X0 > nat > $o))).
% 85.28/14.31 thf(func_def_86, type, sP2: !>[X0: $tType]:((tree @ X0 > nat > $o))).
% 85.28/14.31 thf(func_def_87, type, sP3: !>[X0: $tType]:((tree @ X0 > nat > $o))).
% 85.28/14.31 thf(func_def_88, type, sK4: tree @ a).
% 85.28/14.31 thf(func_def_89, type, sK5: a).
% 85.28/14.31 thf(func_def_90, type, sK6: tree @ a).
% 85.28/14.31 thf(func_def_91, type, sK7: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_92, type, sK8: !>[X0: $tType]:(((tree @ X0 > $o) > X0))).
% 85.28/14.31 thf(func_def_93, type, sK9: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_94, type, sK10: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_95, type, sK11: !>[X0: $tType]:((tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_96, type, sK12: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_97, type, sK13: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_98, type, sK14: !>[X0: $tType]:(((tree @ X0 > $o) > X0))).
% 85.28/14.31 thf(func_def_99, type, sK15: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_100, type, sK16: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_101, type, sK17: !>[X0: $tType]:((tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_102, type, sK18: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_103, type, sK19: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_104, type, sK20: !>[X0: $tType]:(((tree @ X0 > $o) > X0))).
% 85.28/14.31 thf(func_def_105, type, sK21: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_106, type, sK22: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_107, type, sK23: !>[X0: $tType]:((tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_108, type, sK24: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_109, type, sK25: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_110, type, sK26: !>[X0: $tType]:(((tree @ X0 > $o) > X0))).
% 85.28/14.31 thf(func_def_111, type, sK27: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_112, type, sK28: !>[X0: $tType]:(((tree @ X0 > $o) > X0))).
% 85.28/14.31 thf(func_def_113, type, sK29: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_114, type, sK30: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_115, type, sK31: !>[X0: $tType]:(((tree @ X0 > $o) > X0))).
% 85.28/14.31 thf(func_def_116, type, sK32: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_117, type, sK33: !>[X0: $tType]:((tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_118, type, sK34: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_119, type, sK35: !>[X0: $tType]:((tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_120, type, sK36: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_121, type, sK37: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_122, type, sK38: !>[X0: $tType]:((tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_123, type, sK39: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_124, type, sK40: !>[X0: $tType]:(((tree @ X0 > $o) > X0))).
% 85.28/14.31 thf(func_def_125, type, sK41: !>[X0: $tType]:(((tree @ X0 > $o) > tree @ X0))).
% 85.28/14.31 thf(func_def_126, type, sK42: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 85.28/14.31 thf(func_def_127, type, sK43: !>[X0: $tType]:((tree @ X0 > nat > tree @ X0))).
% 85.28/14.31 thf(func_def_128, type, sK44: !>[X0: $tType]:((tree @ X0 > nat > X0))).
% 85.28/14.31 thf(func_def_129, type, sK45: !>[X0: $tType]:((tree @ X0 > nat > tree @ X0))).
% 85.28/14.31 thf(func_def_130, type, sK46: !>[X0: $tType]:((tree @ X0 > nat > X0))).
% 85.28/14.31 thf(func_def_131, type, sK47: !>[X0: $tType]:((tree @ X0 > nat > tree @ X0))).
% 85.28/14.31 thf(func_def_132, type, sK48: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_133, type, sK49: !>[X0: $tType]:((tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_134, type, sK50: !>[X0: $tType]:((tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_135, type, sK51: !>[X0: $tType]:((X0 > tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_136, type, sK52: !>[X0: $tType]:((X0 > tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_137, type, sK53: !>[X0: $tType]:((X0 > tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_138, type, sK54: !>[X0: $tType]:((nat > tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_139, type, sK55: !>[X0: $tType]:((nat > tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_140, type, sK56: !>[X0: $tType]:((nat > tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_141, type, sK57: !>[X0: $tType]:((tree @ X0 > nat > tree @ X0))).
% 85.28/14.31 thf(func_def_142, type, sK58: !>[X0: $tType]:((tree @ X0 > nat > X0))).
% 85.28/14.31 thf(func_def_143, type, sK59: !>[X0: $tType]:((tree @ X0 > nat > tree @ X0))).
% 85.28/14.31 thf(func_def_144, type, sK60: !>[X0: $tType]:((tree @ X0 > nat > X0))).
% 85.28/14.31 thf(func_def_145, type, sK61: !>[X0: $tType]:((tree @ X0 > nat > tree @ X0))).
% 85.28/14.31 thf(func_def_146, type, sK62: !>[X0: $tType]:((nat > tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_147, type, sK63: !>[X0: $tType]:((nat > tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_148, type, sK64: ((nat > $o) > nat)).
% 85.28/14.31 thf(func_def_149, type, sK65: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 85.28/14.31 thf(func_def_150, type, sK66: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 85.28/14.31 thf(func_def_151, type, sK67: !>[X0: $tType]:((X0 > X0))).
% 85.28/14.31 thf(func_def_152, type, sK68: !>[X0: $tType]:((X0 > X0))).
% 85.28/14.31 thf(func_def_153, type, sK69: (nat > nat > nat)).
% 85.28/14.31 thf(func_def_154, type, sK70: !>[X0: $tType]:((nat > tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_155, type, sK71: !>[X0: $tType]:((nat > tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_156, type, sK72: !>[X0: $tType]:((nat > tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_157, type, sK73: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 85.28/14.31 thf(func_def_158, type, sK74: ((nat > $o) > nat)).
% 85.28/14.31 thf(func_def_159, type, sK75: ((nat > $o) > nat)).
% 85.28/14.31 thf(func_def_160, type, sK76: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 85.28/14.31 thf(func_def_161, type, sK77: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 85.28/14.31 thf(func_def_162, type, sK78: !>[X0: $tType]:((((nat > X0 > X0) > nat > nat > X0 > $o) > nat > X0 > X0))).
% 85.28/14.31 thf(func_def_163, type, sK79: !>[X0: $tType]:((((nat > X0 > X0) > nat > nat > X0 > $o) > nat))).
% 85.28/14.31 thf(func_def_164, type, sK80: !>[X0: $tType]:((((nat > X0 > X0) > nat > nat > X0 > $o) > nat))).
% 85.28/14.31 thf(func_def_165, type, sK81: !>[X0: $tType]:((((nat > X0 > X0) > nat > nat > X0 > $o) > X0))).
% 85.28/14.31 thf(func_def_166, type, sK82: ((nat > nat > $o) > nat)).
% 85.28/14.31 thf(func_def_167, type, sK83: ((nat > nat > $o) > nat)).
% 85.28/14.31 thf(func_def_168, type, sK84: ((nat > nat > $o) > nat)).
% 85.28/14.31 thf(func_def_169, type, sK85: ((nat > nat > $o) > nat)).
% 85.28/14.31 thf(func_def_170, type, sK86: ((nat > nat > $o) > nat)).
% 85.28/14.31 thf(func_def_171, type, sK87: (real > real > real)).
% 85.28/14.31 thf(func_def_172, type, sK88: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_173, type, sK89: !>[X0: $tType]:((tree @ X0 > X0))).
% 85.28/14.31 thf(func_def_174, type, sK90: !>[X0: $tType]:((tree @ X0 > tree @ X0))).
% 85.28/14.31 thf(func_def_176, type, db6: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_177, type, db5: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_178, type, db4: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_179, type, db10: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_180, type, db9: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_181, type, db8: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(func_def_182, type, db7: !>[X0: $tType]:(X0)).
% 85.28/14.31 thf(f2,axiom,(
% 85.28/14.31 (((splay_splay_max @ a @ rr)) = ((node @ a @ l @ u @ r)))),
% 85.28/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_sp)).
% 85.28/14.31 thf(f7,axiom,(
% 85.28/14.31 ! [X0 : $tType] : ((linorder @ X0 @ type2 @ X0) => ! [X1 : tree @ X0,X2 : tree @ X0,X3 : X0,X4 : tree @ X0] : ((((splay_splay_max @ X0 @ X1)) = ((node @ X0 @ X2 @ X3 @ X4))) => (((size_size @ tree @ X0 @ X1)) = ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ X0 @ X2) @ (size_size @ tree @ X0 @ X4)) @ one_one @ nat)))))),
% 85.28/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_size__if__splay__max)).
% 85.28/14.31 thf(f19,axiom,(
% 85.28/14.31 ! [X0 : $tType] : ((linorder @ X0 @ type2 @ X0) => ! [X1 : tree @ X0,X2 : tree @ X0,X3 : X0,X4 : tree @ X0] : ((((splay_splay_max @ X0 @ X1)) = ((node @ X0 @ X2 @ X3 @ X4))) => (X4 = leaf @ X0)))),
% 85.28/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_splay__max__Leaf)).
% 85.28/14.31 thf(f88,axiom,(
% 85.28/14.31 ! [X0 : nat] : (((plus_plus @ nat @ X0 @ zero_zero @ nat)) = X0)),
% 85.28/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_87_Nat_Oadd__0__right)).
% 85.28/14.31 thf(f155,axiom,(
% 85.28/14.31 ! [X0 : $tType] : (((size_size @ tree @ X0 @ leaf @ X0)) = zero_zero @ nat)),
% 85.28/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_154_tree_Osize_I3_J)).
% 85.28/14.31 thf(f335,axiom,(
% 85.28/14.31 (linorder @ a @ type2 @ a)),
% 85.28/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tfree_0)).
% 85.28/14.31 thf(f336,conjecture,(
% 85.28/14.31 (((size_size @ tree @ a @ rr)) = ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ a @ l) @ (size_size @ tree @ a @ r)) @ one_one @ nat)))),
% 85.28/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 85.28/14.31 thf(f337,negated_conjecture,(
% 85.28/14.31 ~ (((size_size @ tree @ a @ rr)) = ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ a @ l) @ (size_size @ tree @ a @ r)) @ one_one @ nat)))),
% 85.28/14.31 inference(negated_conjecture,[status(cth)],[f336])).
% 85.28/14.31 thf(f342,plain,(
% 85.28/14.31 ! [X0 : $tType] : ((linorder @ X0 @ type2 @ X0) => ! [X1 : tree @ X0,X2 : tree @ X0,X3 : X0,X4 : tree @ X0] : ((((splay_splay_max @ X0 @ X1)) = ((node @ X0 @ X2 @ X3 @ X4))) => (((size_size @ tree @ X0 @ X1)) = ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ X0 @ X2) @ (size_size @ tree @ X0 @ X4)) @ one_one @ nat)))))),
% 85.28/14.31 inference(rectify,[],[f7])).
% 85.28/14.31 thf(f343,plain,(
% 85.28/14.31 ! [X0 : $tType] : ((((linorder @ X0 @ type2 @ X0)) = $true) => ! [X1 : tree @ X0,X2 : tree @ X0,X3 : X0,X4 : tree @ X0] : ((((splay_splay_max @ X0 @ X1)) = ((node @ X0 @ X2 @ X3 @ X4))) => (((size_size @ tree @ X0 @ X1)) = ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ X0 @ X2) @ (size_size @ tree @ X0 @ X4)) @ one_one @ nat)))))),
% 85.28/14.31 inference(fool_elimination,[],[f342])).
% 85.28/14.31 thf(f362,plain,(
% 85.28/14.31 ! [X0 : $tType] : ((linorder @ X0 @ type2 @ X0) => ! [X1 : tree @ X0,X2 : tree @ X0,X3 : X0,X4 : tree @ X0] : ((((splay_splay_max @ X0 @ X1)) = ((node @ X0 @ X2 @ X3 @ X4))) => (X4 = leaf @ X0)))),
% 85.28/14.31 inference(rectify,[],[f19])).
% 85.28/14.31 thf(f363,plain,(
% 85.28/14.31 ! [X0 : $tType] : ((((linorder @ X0 @ type2 @ X0)) = $true) => ! [X1 : tree @ X0,X2 : tree @ X0,X3 : X0,X4 : tree @ X0] : ((((splay_splay_max @ X0 @ X1)) = ((node @ X0 @ X2 @ X3 @ X4))) => (leaf @ X0 = X4)))),
% 85.28/14.31 inference(fool_elimination,[],[f362])).
% 85.28/14.31 thf(f930,plain,(
% 85.28/14.31 (linorder @ a @ type2 @ a)),
% 85.28/14.31 inference(rectify,[],[f335])).
% 85.28/14.31 thf(f931,plain,(
% 85.28/14.31 (((linorder @ a @ type2 @ a)) = $true)),
% 85.28/14.31 inference(fool_elimination,[],[f930])).
% 85.28/14.31 thf(f954,plain,(
% 85.28/14.31 (((size_size @ tree @ a @ rr)) != ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ a @ l) @ (size_size @ tree @ a @ r)) @ one_one @ nat)))),
% 85.28/14.31 inference(flattening,[],[f337])).
% 85.28/14.31 thf(f958,plain,(
% 85.28/14.31 ! [X0 : $tType] : (! [X1 : tree @ X0,X2 : tree @ X0,X3 : X0,X4 : tree @ X0] : ((((size_size @ tree @ X0 @ X1)) = ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ X0 @ X2) @ (size_size @ tree @ X0 @ X4)) @ one_one @ nat))) | (((splay_splay_max @ X0 @ X1)) != ((node @ X0 @ X2 @ X3 @ X4)))) | (((linorder @ X0 @ type2 @ X0)) != $true))),
% 85.28/14.31 inference(ennf_transformation,[],[f343])).
% 85.28/14.31 thf(f967,plain,(
% 85.28/14.31 ! [X0 : $tType] : (! [X1 : tree @ X0,X2 : tree @ X0,X3 : X0,X4 : tree @ X0] : ((leaf @ X0 = X4) | (((splay_splay_max @ X0 @ X1)) != ((node @ X0 @ X2 @ X3 @ X4)))) | (((linorder @ X0 @ type2 @ X0)) != $true))),
% 85.28/14.31 inference(ennf_transformation,[],[f363])).
% 85.28/14.31 thf(f1255,plain,(
% 85.28/14.31 (((splay_splay_max @ a @ rr)) = ((node @ a @ l @ u @ r)))),
% 85.28/14.31 inference(cnf_transformation,[],[f2])).
% 85.28/14.31 thf(f1260,plain,(
% 85.28/14.31 ( ! [X0 : $tType,X2 : tree @ X0,X3 : X0,X1 : tree @ X0,X4 : tree @ X0] : ((((splay_splay_max @ X0 @ X1)) != ((node @ X0 @ X2 @ X3 @ X4))) | (((size_size @ tree @ X0 @ X1)) = ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ X0 @ X2) @ (size_size @ tree @ X0 @ X4)) @ one_one @ nat))) | (((linorder @ X0 @ type2 @ X0)) != $true)) )),
% 85.28/14.31 inference(cnf_transformation,[],[f958])).
% 85.28/14.31 thf(f1272,plain,(
% 85.28/14.31 ( ! [X0 : $tType,X2 : tree @ X0,X3 : X0,X1 : tree @ X0,X4 : tree @ X0] : ((((splay_splay_max @ X0 @ X1)) != ((node @ X0 @ X2 @ X3 @ X4))) | (leaf @ X0 = X4) | (((linorder @ X0 @ type2 @ X0)) != $true)) )),
% 85.28/14.31 inference(cnf_transformation,[],[f967])).
% 85.28/14.31 thf(f1369,plain,(
% 85.28/14.31 ( ! [X0 : nat] : ((((plus_plus @ nat @ X0 @ zero_zero @ nat)) = X0)) )),
% 85.28/14.31 inference(cnf_transformation,[],[f88])).
% 85.28/14.31 thf(f1448,plain,(
% 85.28/14.31 ( ! [X0 : $tType] : ((zero_zero @ nat = ((size_size @ tree @ X0 @ leaf @ X0)))) )),
% 85.28/14.31 inference(cnf_transformation,[],[f155])).
% 85.28/14.31 thf(f1644,plain,(
% 85.28/14.31 (((linorder @ a @ type2 @ a)) = $true)),
% 85.28/14.31 inference(cnf_transformation,[],[f931])).
% 85.28/14.31 thf(f1645,plain,(
% 85.28/14.31 (((size_size @ tree @ a @ rr)) != ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ a @ l) @ (size_size @ tree @ a @ r)) @ one_one @ nat)))),
% 85.28/14.31 inference(cnf_transformation,[],[f954])).
% 85.28/14.31 thf(f9327,plain,(
% 85.28/14.31 ( ! [X0 : tree @ a] : ((((splay_splay_max @ a @ rr)) != ((splay_splay_max @ a @ X0))) | (r = leaf @ a) | (((linorder @ a @ type2 @ a)) != $true)) )),
% 85.28/14.31 inference(constrained_superposition,[],[f1272,f1255])).
% 85.28/14.31 thf(f9330,plain,(
% 85.28/14.31 ( ! [X0 : tree @ a] : ((((splay_splay_max @ a @ rr)) != ((splay_splay_max @ a @ X0))) | (r = leaf @ a)) )),
% 85.28/14.31 inference(forward_subsumption_resolution,[],[f9327,f1644])).
% 85.28/14.31 thf(f9336,definition,(
% 85.28/14.31 spl91_103 <=> ! [X0 : tree @ a] : (((splay_splay_max @ a @ rr)) != ((splay_splay_max @ a @ X0)))),
% 85.28/14.31 introduced(definition,[new_symbols(definition,[spl91_103])],[avatar_definition])).
% 85.28/14.31 thf(f9337,plain,(
% 85.28/14.31 ( ! [X0 : tree @ a] : ((((splay_splay_max @ a @ rr)) != ((splay_splay_max @ a @ X0)))) ) | ~spl91_103),
% 85.28/14.31 inference(avatar_component_clause,[],[f9336])).
% 85.28/14.31 thf(f9340,definition,(
% 85.28/14.31 spl91_104 <=> (r = leaf @ a)),
% 85.28/14.31 introduced(definition,[new_symbols(definition,[spl91_104])],[avatar_definition])).
% 85.28/14.31 thf(f9342,plain,(
% 85.28/14.31 (r = leaf @ a) | ~spl91_104),
% 85.28/14.31 inference(avatar_component_clause,[],[f9340])).
% 85.28/14.31 thf(f9343,plain,(
% 85.28/14.31 spl91_104 | spl91_103),
% 85.28/14.31 inference(avatar_split_clause,[],[f9330,f9336,f9340])).
% 85.28/14.31 thf(f14375,plain,(
% 85.28/14.31 $false | ~spl91_103),
% 85.28/14.31 inference(equality_resolution,[],[f9337])).
% 85.28/14.31 thf(f14376,plain,(
% 85.28/14.31 ~spl91_103),
% 85.28/14.31 inference(avatar_contradiction_clause,[],[f14375])).
% 85.28/14.31 thf(f15311,plain,(
% 85.28/14.31 ( ! [X0 : tree @ a] : ((((splay_splay_max @ a @ rr)) != ((splay_splay_max @ a @ X0))) | (((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ a @ l) @ (size_size @ tree @ a @ r)) @ one_one @ nat)) = ((size_size @ tree @ a @ X0))) | (((linorder @ a @ type2 @ a)) != $true)) )),
% 85.28/14.31 inference(constrained_superposition,[],[f1260,f1255])).
% 85.28/14.31 thf(f15316,plain,(
% 85.28/14.31 ( ! [X0 : tree @ a] : ((((splay_splay_max @ a @ rr)) != ((splay_splay_max @ a @ X0))) | (((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ a @ l) @ (size_size @ tree @ a @ r)) @ one_one @ nat)) = ((size_size @ tree @ a @ X0)))) )),
% 85.28/14.31 inference(forward_subsumption_resolution,[],[f15311,f1644])).
% 85.28/14.31 thf(f15501,plain,(
% 85.28/14.31 (zero_zero @ nat = ((size_size @ tree @ a @ r))) | ~spl91_104),
% 85.28/14.31 inference(constrained_superposition,[],[f1448,f9342])).
% 85.28/14.31 thf(f18847,plain,(
% 85.28/14.31 (((size_size @ tree @ a @ rr)) != ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ a @ l) @ zero_zero @ nat) @ one_one @ nat))) | ~spl91_104),
% 85.28/14.31 inference(constrained_superposition,[],[f1645,f15501])).
% 85.28/14.31 thf(f18873,plain,(
% 85.28/14.31 (((size_size @ tree @ a @ rr)) != ((plus_plus @ nat @ (size_size @ tree @ a @ l) @ one_one @ nat))) | ~spl91_104),
% 85.28/14.31 inference(forward_demodulation,[],[f18847,f1369])).
% 85.28/14.31 thf(f297556,plain,(
% 85.28/14.31 ( ! [X0 : tree @ a] : ((((size_size @ tree @ a @ X0)) = ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ tree @ a @ l) @ zero_zero @ nat) @ one_one @ nat))) | (((splay_splay_max @ a @ rr)) != ((splay_splay_max @ a @ X0)))) ) | ~spl91_104),
% 85.28/14.31 inference(forward_demodulation,[],[f15316,f15501])).
% 85.28/14.31 thf(f297557,plain,(
% 85.28/14.31 ( ! [X0 : tree @ a] : ((((splay_splay_max @ a @ rr)) != ((splay_splay_max @ a @ X0))) | (((size_size @ tree @ a @ X0)) = ((plus_plus @ nat @ (size_size @ tree @ a @ l) @ one_one @ nat)))) ) | ~spl91_104),
% 85.28/14.31 inference(forward_demodulation,[],[f297556,f1369])).
% 85.28/14.31 thf(f297617,plain,(
% 85.28/14.31 (((size_size @ tree @ a @ rr)) = ((plus_plus @ nat @ (size_size @ tree @ a @ l) @ one_one @ nat))) | ~spl91_104),
% 85.28/14.31 inference(equality_resolution,[],[f297557])).
% 85.28/14.31 thf(f297622,plain,(
% 85.28/14.31 $false | ~spl91_104),
% 85.28/14.31 inference(forward_subsumption_resolution,[],[f297617,f18873])).
% 85.28/14.31 thf(f297623,plain,(
% 85.28/14.31 ~spl91_104),
% 85.28/14.31 inference(avatar_contradiction_clause,[],[f297622])).
% 85.28/14.31 cnf(s242, plain, spl91_103 | spl91_104, inference(sat_conversion,[],[f9343])).
% 85.28/14.31 cnf(s340, plain, ~spl91_103, inference(sat_conversion,[],[f14376])).
% 85.28/14.31 cnf(s19381, plain, ~spl91_104, inference(sat_conversion,[],[f297623])).
% 85.28/14.31 cnf(s19404, plain, $false, inference(rat,[],[s242,s19381,s340])).
% 85.28/14.31 thf(f297626,plain,(
% 85.28/14.31 $false),
% 85.28/14.31 inference(avatar_sat_refutation,[],[s19404])).
% 85.28/14.31 % SZS output end Proof for theBenchmark
% 85.28/14.31 % (486768)------------------------------
% 85.28/14.31 % (486768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.28/14.31 % (486768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.28/14.31 % (486768)CaDiCaL version: 2.1.3
% 85.28/14.31 % (486768)Termination reason: Refutation
% 85.28/14.31 % (486768)Time elapsed: 14.108 s
% 85.28/14.31 % (486768)Peak memory usage: 139 MB
% 85.28/14.31 % (486768)Instructions burned: 42091 (million)
% 85.28/14.31 % (486762)Success in time 14.16 s
% 85.28/14.31 % Vampire exiting
%------------------------------------------------------------------------------