%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NLP263+1 : TPTP v9.3.1. Bugfixed v4.0.1. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n011.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 : Tue Sep 29 12:09:44 PM UTC 2026 % Result : Satisfiable 39.02s 19.29s % Output : Saturation 39.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NLP263+1 : TPTP v9.3.1. Bugfixed v4.0.1. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.12/0.41 % Computer : n011.cluster.edu % 0.12/0.41 % Model : x86_64 x86_64 % 0.12/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.41 % Memory : 8046.5625MB % 0.12/0.41 % OS : Linux 6.8.0-71-generic % 0.12/0.41 % CPULimit : 300 % 0.12/0.41 % WCLimit : 300 % 0.12/0.41 % DateTime : Sun Sep 27 18:38:01 UTC 2026 % 0.12/0.41 % CPUTime : % 0.12/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.12/0.44 Running first-order model finding % 0.12/0.45 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 % 26.90/18.24 % (2681057)Will run a generic schedule for satisfiability detection. % 26.90/18.24 % (2681298)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4090115610_2856 on theBenchmark for (2856ds/0Mi) % 26.90/18.24 % (2681300)% WARNING: option uhcvi not known. % 26.90/18.24 % (2681300)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=620258869:i=135531:add=off:rawr=on_2856 on theBenchmark for (2856ds/135531Mi) % 26.90/18.24 % (2681302)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3167192434:i=88024:add=on:rawr=on_2856 on theBenchmark for (2856ds/88024Mi) % 26.90/18.24 % (2681304)dis+10_1_sil=32000:sp=arity:random_seed=1077914058:i=103:fgj=on_2856 on theBenchmark for (2856ds/103Mi) % 26.90/18.24 % (2681306)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2046941618:i=116_2856 on theBenchmark for (2856ds/116Mi) % 26.90/18.24 % (2681308)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3308724440:i=131_2856 on theBenchmark for (2856ds/131Mi) % 26.90/18.24 % (2681304)Instruction limit reached! % 26.90/18.24 % (2681304)------------------------------ % 26.90/18.24 % (2681304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.90/18.24 % (2681304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.90/18.24 % (2681304)CaDiCaL version: 2.1.3 % 26.90/18.24 % (2681304)Termination reason: Instruction limit % 26.90/18.24 % (2681304)Termination phase: Preprocessing 1 % 26.90/18.24 % (2681304)Time elapsed: 0.078 s % 26.90/18.24 % (2681304)Peak memory usage: 954 MB % 26.90/18.24 % (2681304)Instructions burned: 104 (million) % 26.90/18.24 % (2681310)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1781441201:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2856 on theBenchmark for (2856ds/159Mi) % 26.90/18.24 % (2681308)Instruction limit reached! % 26.90/18.24 % (2681308)------------------------------ % 26.90/18.24 % (2681308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.90/18.24 % (2681308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.90/18.24 % (2681308)CaDiCaL version: 2.1.3 % 26.90/18.24 % (2681308)Termination reason: Instruction limit % 26.90/18.24 % (2681308)Termination phase: Preprocessing 1 % 26.90/18.24 % (2681308)Time elapsed: 0.097 s % 26.90/18.24 % (2681308)Peak memory usage: 954 MB % 26.90/18.24 % (2681308)Instructions burned: 131 (million) % 26.90/18.24 % (2681306)Instruction limit reached! % 26.90/18.24 % (2681306)------------------------------ % 26.90/18.24 % (2681306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.90/18.24 % (2681306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.90/18.24 % (2681306)CaDiCaL version: 2.1.3 % 26.90/18.24 % (2681306)Termination reason: Instruction limit % 26.90/18.24 % (2681306)Termination phase: Preprocessing 1 % 26.90/18.24 % (2681306)Time elapsed: 0.135 s % 26.90/18.24 % (2681306)Peak memory usage: 954 MB % 26.90/18.24 % (2681306)Instructions burned: 116 (million) % 26.90/18.24 % (2681312)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2888133202:i=714:nm=2_2854 on theBenchmark for (2854ds/714Mi) % 26.90/18.24 % (2681310)Instruction limit reached! % 26.90/18.24 % (2681310)------------------------------ % 26.90/18.24 % (2681310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.90/18.24 % (2681310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.90/18.24 % (2681310)CaDiCaL version: 2.1.3 % 26.90/18.24 % (2681310)Termination reason: Instruction limit % 26.90/18.24 % (2681310)Termination phase: Preprocessing 1 % 26.90/18.24 % (2681310)Time elapsed: 0.119 s % 26.90/18.24 % (2681310)Peak memory usage: 954 MB % 26.90/18.24 % (2681310)Instructions burned: 159 (million) % 26.90/18.24 % (2681314)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=538827154:i=131:bd=preordered:fsd=on_2853 on theBenchmark for (2853ds/131Mi) % 26.90/18.24 % (2681316)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=4050851647:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2852 on theBenchmark for (2852ds/684Mi) % 26.90/18.24 % (2681318)ott-21_1_sil=16000:fs=off:random_seed=786952504:i=180:av=off:fsr=off_2852 on theBenchmark for (2852ds/180Mi) % 26.90/18.24 % (2681314)Instruction limit reached! % 26.90/18.24 % (2681314)------------------------------ % 26.90/18.24 % (2681314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.90/18.24 % (2681314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681314)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681314)Termination reason: Instruction limit % 39.02/19.29 % (2681314)Termination phase: Preprocessing 1 % 39.02/19.29 % (2681314)Time elapsed: 0.097 s % 39.02/19.29 % (2681314)Peak memory usage: 954 MB % 39.02/19.29 % (2681314)Instructions burned: 131 (million) % 39.02/19.29 % (2681321)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1605893955:i=477:bd=all_2851 on theBenchmark for (2851ds/477Mi) % 39.02/19.29 % (2681318)Instruction limit reached! % 39.02/19.29 % (2681318)------------------------------ % 39.02/19.29 % (2681318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.02/19.29 % (2681318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681318)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681318)Termination reason: Instruction limit % 39.02/19.29 % (2681318)Termination phase: Preprocessing 1 % 39.02/19.29 % (2681318)Time elapsed: 0.159 s % 39.02/19.29 % (2681318)Peak memory usage: 954 MB % 39.02/19.29 % (2681318)Instructions burned: 181 (million) % 39.02/19.29 % (2681323)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3423780780:fmbsr=1.3:i=865:ins=25_2850 on theBenchmark for (2850ds/865Mi) % 39.02/19.29 % (2681312)Instruction limit reached! % 39.02/19.29 % (2681312)------------------------------ % 39.02/19.29 % (2681312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.02/19.29 % (2681312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681312)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681312)Termination reason: Instruction limit % 39.02/19.29 % (2681312)Termination phase: Preprocessing 1 % 39.02/19.29 % (2681312)Time elapsed: 0.528 s % 39.02/19.29 % (2681312)Peak memory usage: 954 MB % 39.02/19.29 % (2681312)Instructions burned: 715 (million) % 39.02/19.29 % (2681316)Instruction limit reached! % 39.02/19.29 % (2681316)------------------------------ % 39.02/19.29 % (2681316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.02/19.29 % (2681316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681316)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681316)Termination reason: Instruction limit % 39.02/19.29 % (2681316)Termination phase: SInE selection % 39.02/19.29 % (2681316)Time elapsed: 0.453 s % 39.02/19.29 % (2681316)Peak memory usage: 958 MB % 39.02/19.29 % (2681316)Instructions burned: 685 (million) % 39.02/19.29 % (2681325)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=223498060:i=1179_2847 on theBenchmark for (2847ds/1179Mi) % 39.02/19.29 % (2681321)Instruction limit reached! % 39.02/19.29 % (2681321)------------------------------ % 39.02/19.29 % (2681321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.02/19.29 % (2681321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681321)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681321)Termination reason: Instruction limit % 39.02/19.29 % (2681321)Termination phase: Preprocessing 1 % 39.02/19.29 % (2681321)Time elapsed: 0.353 s % 39.02/19.29 % (2681321)Peak memory usage: 954 MB % 39.02/19.29 % (2681321)Instructions burned: 477 (million) % 39.02/19.29 % (2681327)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=655950723:i=889:ins=1_2847 on theBenchmark for (2847ds/889Mi) % 39.02/19.29 % (2681329)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=4269795106:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2846 on theBenchmark for (2846ds/692Mi) % 39.02/19.29 % (2681323)Instruction limit reached! % 39.02/19.29 % (2681323)------------------------------ % 39.02/19.29 % (2681323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.02/19.29 % (2681323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681323)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681323)Termination reason: Instruction limit % 39.02/19.29 % (2681323)Termination phase: Preprocessing 2 % 39.02/19.29 % (2681323)Time elapsed: 0.664 s % 39.02/19.29 % (2681323)Peak memory usage: 954 MB % 39.02/19.29 % (2681323)Instructions burned: 867 (million) % 39.02/19.29 % (2681331)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=340696695:i=879:kws=inv_precedence:fsr=off_2842 on theBenchmark for (2842ds/879Mi) % 39.02/19.29 % (2681329)Instruction limit reached! % 39.02/19.29 % (2681329)------------------------------ % 39.02/19.29 % (2681329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.02/19.29 % (2681329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681329)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681329)Termination reason: Instruction limit % 39.02/19.29 % (2681329)Termination phase: SInE selection % 39.02/19.29 % (2681329)Time elapsed: 0.448 s % 39.02/19.29 % (2681329)Peak memory usage: 958 MB % 39.02/19.29 % (2681329)Instructions burned: 692 (million) % 39.02/19.29 % (2681333)fmb+10_1_sil=64000:random_seed=3025928725:i=22061:nm=2:gsp=on_2841 on theBenchmark for (2841ds/22061Mi) % 39.02/19.29 % (2681327)Instruction limit reached! % 39.02/19.29 % (2681327)------------------------------ % 39.02/19.29 % (2681327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.02/19.29 % (2681327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681327)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681327)Termination reason: Instruction limit % 39.02/19.29 % (2681327)Termination phase: Unused predicate definition removal % 39.02/19.29 % (2681327)Time elapsed: 0.708 s % 39.02/19.29 % (2681327)Peak memory usage: 968 MB % 39.02/19.29 % (2681327)Instructions burned: 889 (million) % 39.02/19.29 % (2681335)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2198507284:i=9515:nm=5_2839 on theBenchmark for (2839ds/9515Mi) % 39.02/19.29 % (2681298) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2681057-2681298"... % 39.02/19.29 % (2681325)Instruction limit reached! % 39.02/19.29 % (2681325)------------------------------ % 39.02/19.29 % (2681325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.02/19.29 % (2681325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681325)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681325)Termination reason: Instruction limit % 39.02/19.29 % (2681325)Termination phase: Unused predicate definition removal % 39.02/19.29 % (2681325)Time elapsed: 1.171 s % 39.02/19.29 % (2681325)Peak memory usage: 1014 MB % 39.02/19.29 % (2681325)Instructions burned: 1179 (million) % 39.02/19.29 % (2681337)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3512722137:fmbsr=1.7:i=920_2834 on theBenchmark for (2834ds/920Mi) % 39.02/19.29 % (2681331)Instruction limit reached! % 39.02/19.29 % (2681331)------------------------------ % 39.02/19.29 % (2681331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.02/19.29 % (2681331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681331)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681331)Termination reason: Instruction limit % 39.02/19.29 % (2681331)Termination phase: Unused predicate definition removal % 39.02/19.29 % (2681331)Time elapsed: 0.979 s % 39.02/19.29 % (2681331)Peak memory usage: 978 MB % 39.02/19.29 % (2681331)Instructions burned: 879 (million) % 39.02/19.29 % (2681339)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=838569136:i=5131_2831 on theBenchmark for (2831ds/5131Mi) % 39.02/19.29 % (2681337)Instruction limit reached! % 39.02/19.29 % (2681337)------------------------------ % 39.02/19.29 % (2681337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.02/19.29 % (2681337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681337)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681337)Termination reason: Instruction limit % 39.02/19.29 % (2681337)Termination phase: Unused predicate definition removal % 39.02/19.29 % (2681337)Time elapsed: 0.850 s % 39.02/19.29 % (2681337)Peak memory usage: 978 MB % 39.02/19.29 % (2681337)Instructions burned: 922 (million) % 39.02/19.29 % (2681341)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4155657818:i=1472:ins=7:fdi=8:gsp=on_2825 on theBenchmark for (2825ds/1472Mi) % 39.02/19.29 % (2681298)...printing done. % 39.02/19.29 % SZS status Satisfiable for theBenchmark % 39.02/19.29 % SZS output start Saturation. % 39.02/19.29 % SZS output end Saturation. % 39.02/19.29 % SZS output start Definitions and Model Updates. % 39.02/19.29 globally flip the polarity of every occurrence of predicate "region__domain__of" % 39.02/19.29 globally flip the polarity of every occurrence of predicate "entailment" % 39.02/19.29 globally flip the polarity of every occurrence of predicate "has__usage__domain" % 39.02/19.29 globally flip the polarity of every occurrence of predicate "verbgroup" % 39.02/19.29 globally flip the polarity of every occurrence of predicate "holonym__substance" % 39.02/19.29 globally flip the polarity of every occurrence of predicate "meronym__part" % 39.02/19.29 globally flip the polarity of every occurrence of predicate "similar" % 39.02/19.29 globally flip the polarity of every occurrence of predicate "holonym__member" % 39.02/19.29 globally flip the polarity of every occurrence of predicate "has__region__domain" % 39.02/19.29 globally flip the polarity of every occurrence of predicate "derived" % 39.02/19.29 globally flip the polarity of every occurrence of predicate "hypernym" % 39.02/19.29 for all inputs, % 39.02/19.29 define has__gloss(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define derivation(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define lexical__category(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define hypernym(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define lexicalization(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define antonym(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define holonym__part(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define instance(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define means(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define hyponym(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define attribute(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define has__category(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define derived(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define has__region__domain(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define meronym__member(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define holonym__member(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define similar(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define category__of(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define meronym__part(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define holonym__substance(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define closely__related(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define verbgroup(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define meronym__substance(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define has__usage__domain(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define has__instance(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define entailment(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define cause(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define region__domain__of(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define usage__domain__of(X0,X1) := $true % 39.02/19.29 for all inputs, % 39.02/19.29 define derived__participle(X0,X1) := $true % 39.02/19.29 % SZS output end Definitions and Model Updates. % 39.02/19.29 % (2681298)------------------------------ % 39.02/19.29 % (2681298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.02/19.29 % (2681298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.02/19.29 % (2681298)CaDiCaL version: 2.1.3 % 39.02/19.29 % (2681298)Termination reason: Satisfiable % 39.02/19.29 % (2681298)Time elapsed: 1.886 s % 39.02/19.29 % (2681298)Peak memory usage: 1122 MB % 39.02/19.29 % (2681298)Instructions burned: 1789 (million) % 39.02/19.29 % (2681057)Success in time 17.789 s % 39.02/19.29 % Vampire exiting %------------------------------------------------------------------------------