% SZS status Satisfiable for NXF_Finite-Finite-Global % (32388)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32388)------------------------------ % (32388)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32388)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32388)Termination reason: Unknown % (32388)Termination phase: Finite model building constraint generation % (32388)Memory used [KB]: 811 % (32388)Time elapsed: 0.006 s % (32388)Instructions burned: 4 (million) % (32388)------------------------------ % (32388)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa194fd 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) % (32384)Running in auto input_syntax mode. Trying TPTP % (32387)fmb+10_1:1_sil=256000:fmbes=contour:i=214858:bce=on_0 on NXF_Finite-Finite-Global for (300ds/214858Mi) % (32384)Running in auto input_syntax mode. Trying TPTP % (32385)fmb+10_1:1_sil=256000:i=98885:tgt=full:fmbsr=1.3:fmbss=10_0 on NXF_Finite-Finite-Global for (300ds/98885Mi) % (32384)Running in auto input_syntax mode. Trying TPTP % (32391)ott-4_1:1_sil=4000:sp=reverse_arity:lcm=predicate:newcnf=on:i=115:bce=on:fd=off:fs=off:fsr=off_0 on NXF_Finite-Finite-Global for (300ds/115Mi) % (32384)Running in auto input_syntax mode. Trying TPTP % (32389)ott+21_1:1_sil=4000:i=104:fsd=on:fd=off:newcnf=on_0 on NXF_Finite-Finite-Global for (300ds/104Mi) Detected minimum model sizes of [1,1,1,1] Detected maximum model sizes of [2,10,6,4] TRYING [10,10,10,10] Detected minimum model sizes of [1,1,1,1] Detected maximum model sizes of [2,10,6,4] TRYING [1,1,1,1] TRYING [1,1,1,2] TRYING [2,1,1,2] Finite Model Found! % SZS status Satisfiable for NXF_Finite-Finite-Global % (32387)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32387)------------------------------ % (32387)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32387)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32387)Termination reason: Unknown % (32387)Termination phase: Finite model building constraint generation % (32387)Memory used [KB]: 806 % (32387)Time elapsed: 0.006 s % (32387)Instructions burned: 10 (million) % (32387)------------------------------ % (32387)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa15c89 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) Finite Model Found! % SZS status Satisfiable for NXF_Finite-Finite-Global % (32385)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32385)------------------------------ % (32385)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32385)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32385)Termination reason: Unknown % (32385)Termination phase: Finite model building constraint generation % (32385)Memory used [KB]: 1004 % (32385)Time elapsed: 0.009 s % (32385)Instructions burned: 17 (million) % (32385)------------------------------ % (32385)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa15c89 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) % (32389)Instruction limit reached! % (32389)------------------------------ % (32389)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32389)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32389)Termination reason: Time limit % (32389)Termination phase: Saturation % (32389)Memory used [KB]: 763 % (32389)Time elapsed: 0.042 s % (32389)Instructions burned: 106 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32392)dis+11_1:3_bsr=unit_only:sil=2000:rp=on:newcnf=on:i=404:kws=precedence:lsd=100_0 on NXF_Finite-Finite-Global for (299ds/404Mi) % (32391)Instruction limit reached! % (32391)------------------------------ % (32391)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32391)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32391)Termination reason: Time limit % (32391)Termination phase: Saturation % (32391)Memory used [KB]: 1505 % (32391)Time elapsed: 0.049 s % (32391)Instructions burned: 116 (million) % (32390)Instruction limit reached! % (32390)------------------------------ % (32390)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32384)Running in auto input_syntax mode. Trying TPTP % (32393)ott-21_1:1_sil=4000:sp=const_frequency:i=175:fsr=off:fs=off:av=off_0 on NXF_Finite-Finite-Global for (299ds/175Mi) % (32390)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32390)Termination reason: Time limit % (32390)Termination phase: Saturation % (32390)Memory used [KB]: 1038 % (32390)Time elapsed: 0.058 s % (32390)Instructions burned: 149 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32394)ott+33_1:1_to=lpo:sil=8000:sp=weighted_frequency:rp=on:i=270:nm=3:fsr=off:sac=on_0 on NXF_Finite-Finite-Global for (299ds/270Mi) % (32384)Running in auto input_syntax mode. Trying TPTP % (32395)ott+4_1:1_sil=2000:i=900:bd=off:fsr=off_0 on NXF_Finite-Finite-Global for (299ds/900Mi) % (32384)Running in auto input_syntax mode. Trying TPTP % (32396)fmb+10_1:1_sil=8000:fde=unused:fmbes=contour:i=7859:nm=2:fmbswr=0_0 on NXF_Finite-Finite-Global for (298ds/7859Mi) Detected minimum model sizes of [1,1,1,1] Detected maximum model sizes of [3,10,6,4] TRYING [1,1,1,1] TRYING [1,1,1,2] TRYING [2,1,1,2] Finite Model Found! % SZS status Satisfiable for NXF_Finite-Finite-Global % (32384)Running in auto input_syntax mode. Trying TPTP % (32397)ott+11_1:2_anc=none:sil=2000:sp=const_max:spb=units:s2a=on:i=2145:s2at=5.0:awrs=converge:awrsf=170:rawr=on:gs=on:fsr=off_0 on NXF_Finite-Finite-Global for (298ds/2145Mi) % (32396)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32396)------------------------------ % (32396)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32396)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32396)Termination reason: Unknown % (32396)Termination phase: Finite model building constraint generation % (32396)Memory used [KB]: 805 % (32396)Time elapsed: 0.007 s % (32396)Instructions burned: 9 (million) % (32396)------------------------------ % (32396)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa15c89 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) % (32393)Instruction limit reached! % (32393)------------------------------ % (32393)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32393)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32393)Termination reason: Time limit % (32393)Termination phase: Saturation % (32393)Memory used [KB]: 3281 % (32393)Time elapsed: 0.058 s % (32393)Instructions burned: 175 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32398)ott-30_1:1024_sil=4000:alpa=true:newcnf=on:i=1187:bs=unit_only:ins=1:amm=off_0 on NXF_Finite-Finite-Global for (298ds/1187Mi) % (32394)Instruction limit reached! % (32394)------------------------------ % (32394)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32394)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32394)Termination reason: Time limit % (32394)Termination phase: Saturation % (32394)Memory used [KB]: 961 % (32394)Time elapsed: 0.079 s % (32394)Instructions burned: 270 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32399)fmb+10_1:1_sil=32000:i=23580:newcnf=on_0 on NXF_Finite-Finite-Global for (298ds/23580Mi) Detected minimum model sizes of [1,1] Detected maximum model sizes of [2,max] TRYING [1,1] TRYING [2,1] Finite Model Found! % SZS status Satisfiable for NXF_Finite-Finite-Global % (32399)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32399)------------------------------ % (32399)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32399)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32399)Termination reason: Unknown % (32399)Termination phase: Finite model building constraint generation % (32399)Memory used [KB]: 676 % (32399)Time elapsed: 0.002 s % (32399)Instructions burned: 1 (million) % (32399)------------------------------ % (32399)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa194fd 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) % (32392)Instruction limit reached! % (32392)------------------------------ % (32392)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32392)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32392)Termination reason: Time limit % (32392)Termination phase: Saturation % (32392)Memory used [KB]: 1519 % (32392)Time elapsed: 0.114 s % (32392)Instructions burned: 407 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32400)fmb+10_1:1_sil=32000:fmbss=17:fmbsr=2.0:i=2892_0 on NXF_Finite-Finite-Global for (298ds/2892Mi) Detected minimum model sizes of [1,1,1,1] Detected maximum model sizes of [2,10,6,4] TRYING [17,17,17,17] Finite Model Found! % SZS status Satisfiable for NXF_Finite-Finite-Global % (32400)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32400)------------------------------ % (32400)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32400)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32400)Termination reason: Unknown % (32400)Termination phase: Finite model building constraint generation % (32400)Memory used [KB]: 1477 % (32400)Time elapsed: 0.010 s % (32400)Instructions burned: 32 (million) % (32400)------------------------------ % (32400)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa15c89 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) % (32384)Running in auto input_syntax mode. Trying TPTP % (32401)ott-10_1:1_sil=4000:i=1693_0 on NXF_Finite-Finite-Global for (298ds/1693Mi) % (32384)Running in auto input_syntax mode. Trying TPTP % (32402)dis+21_1:1_sil=4000:gs=on:sac=on:newcnf=on:gsem=off:i=1735:gsaa=full_model:abs=on:anc=none_0 on NXF_Finite-Finite-Global for (297ds/1735Mi) % (32384)Running in auto input_syntax mode. Trying TPTP % (32403)fmb+10_1:1_fmbas=expand:sil=128000:i=131798:nm=2:fmbksg=on:fmbss=4:fmbsr=1.77:rp=on_0 on NXF_Finite-Finite-Global for (297ds/131798Mi) Detected minimum model sizes of [1,1,1,1] Detected maximum model sizes of [2,10,6,4] TRYING [4,4,4,4] Finite Model Found! % SZS status Satisfiable for NXF_Finite-Finite-Global % (32403)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32403)------------------------------ % (32403)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32403)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32403)Termination reason: Unknown % (32403)Termination phase: Finite model building constraint generation % (32403)Memory used [KB]: 868 % (32403)Time elapsed: 0.005 s % (32403)Instructions burned: 10 (million) % (32403)------------------------------ % (32403)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa15c89 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) % (32384)Running in auto input_syntax mode. Trying TPTP % (32404)fmb+10_1:1_sil=16000:fmbss=16:i=3451:newcnf=on_0 on NXF_Finite-Finite-Global for (297ds/3451Mi) Detected minimum model sizes of [1,1] Detected maximum model sizes of [2,max] TRYING [16,16] Finite Model Found! % SZS status Satisfiable for NXF_Finite-Finite-Global % (32404)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32404)------------------------------ % (32404)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32404)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32404)Termination reason: Unknown % (32404)Termination phase: Finite model building constraint generation % (32404)Memory used [KB]: 743 % (32404)Time elapsed: 0.003 s % (32404)Instructions burned: 3 (million) % (32404)------------------------------ % (32404)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa194fd 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) % (32384)Running in auto input_syntax mode. Trying TPTP % (32405)ott+11_1:64_sil=4000:rp=on:i=3978:bd=off:fsr=off_0 on NXF_Finite-Finite-Global for (296ds/3978Mi) % (32395)Instruction limit reached! % (32395)------------------------------ % (32395)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32395)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32395)Termination reason: Time limit % (32395)Termination phase: Saturation % (32395)Memory used [KB]: 2139 % (32395)Time elapsed: 0.229 s % (32395)Instructions burned: 902 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32406)dis+35_1:64_to=lpo:sil=32000:sp=occurrence:urr=on:sac=on:i=33091:fsr=off_0 on NXF_Finite-Finite-Global for (296ds/33091Mi) % (32398)Instruction limit reached! % (32398)------------------------------ % (32398)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32398)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32398)Termination reason: Time limit % (32398)Termination phase: Saturation % (32398)Memory used [KB]: 1872 % (32398)Time elapsed: 0.274 s % (32398)Instructions burned: 1187 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32407)dis-4_1:1_sil=16000:sp=const_frequency:sac=on:newcnf=on:i=9564_0 on NXF_Finite-Finite-Global for (295ds/9564Mi) % (32401)Instruction limit reached! % (32401)------------------------------ % (32401)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32401)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32401)Termination reason: Time limit % (32401)Termination phase: Saturation % (32401)Memory used [KB]: 2728 % (32401)Time elapsed: 0.395 s % (32401)Instructions burned: 1694 (million) % (32402)Instruction limit reached! % (32402)------------------------------ % (32402)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32402)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32402)Termination reason: Time limit % (32402)Termination phase: Saturation % (32402)Memory used [KB]: 2133 % (32402)Time elapsed: 0.394 s % (32402)Instructions burned: 1738 (million) % (32397)Instruction limit reached! % (32397)------------------------------ % (32397)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32397)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32397)Termination reason: Time limit % (32397)Termination phase: Saturation % (32397)Memory used [KB]: 4617 % (32397)Time elapsed: 0.499 s % (32397)Instructions burned: 2145 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32408)fmb+10_1:1_sil=64000:i=50409:nm=2:gsp=on_0 on NXF_Finite-Finite-Global for (293ds/50409Mi) Detected minimum model sizes of [1,1,1,1] Detected maximum model sizes of [2,10,6,4] TRYING [1,1,1,1] TRYING [1,1,1,2] TRYING [2,1,1,2] Finite Model Found! % SZS status Satisfiable for NXF_Finite-Finite-Global % (32408)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32408)------------------------------ % (32408)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32408)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32408)Termination reason: Unknown % (32408)Termination phase: Finite model building constraint generation % (32408)Memory used [KB]: 805 % (32408)Time elapsed: 0.004 s % (32408)Instructions burned: 9 (million) % (32408)------------------------------ % (32408)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa15c89 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) % (32384)Running in auto input_syntax mode. Trying TPTP % (32409)dis+2_3:1_bsr=on:sil=64000:abs=on:i=10852:gsp=on:fs=off:fsr=off_0 on NXF_Finite-Finite-Global for (293ds/10852Mi) % (32384)Running in auto input_syntax mode. Trying TPTP % (32410)dis+11_61:31_bsr=unit_only:sil=16000:sp=frequency:rp=on:newcnf=on:i=11327:uhcvi=on:rawr=on:abs=on:lsd=5:add=off_0 on NXF_Finite-Finite-Global for (293ds/11327Mi) % (32384)Running in auto input_syntax mode. Trying TPTP % (32411)fmb+10_1:1_fmbas=expand:sil=128000:i=17908:nm=2:fmbss=15:gsp=on_0 on NXF_Finite-Finite-Global for (293ds/17908Mi) Detected minimum model sizes of [1,1,1,1] Detected maximum model sizes of [2,10,6,4] TRYING [15,15,15,15] Finite Model Found! % SZS status Satisfiable for NXF_Finite-Finite-Global % (32411)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32411)------------------------------ % (32411)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32411)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32411)Termination reason: Unknown % (32411)Termination phase: Finite model building constraint generation % (32411)Memory used [KB]: 1360 % (32411)Time elapsed: 0.008 s % (32411)Instructions burned: 27 (million) % (32411)------------------------------ % (32411)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa15c89 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) % (32384)Running in auto input_syntax mode. Trying TPTP % (32412)dis+11_1:1_anc=all:sil=64000:rp=on:newcnf=on:i=22636:alpa=false:atotf=0.1:gs=on_0 on NXF_Finite-Finite-Global for (292ds/22636Mi) % (32405)Instruction limit reached! % (32405)------------------------------ % (32405)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32405)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32405)Termination reason: Time limit % (32405)Termination phase: Saturation % (32405)Memory used [KB]: 5243 % (32405)Time elapsed: 0.902 s % (32405)Instructions burned: 3982 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32413)fmb+10_1:1_i=30223_0 on NXF_Finite-Finite-Global for (287ds/30223Mi) Detected minimum model sizes of [1,1,1,1] Detected maximum model sizes of [2,10,6,4] TRYING [1,1,1,1] TRYING [1,1,1,2] TRYING [2,1,1,2] Finite Model Found! % SZS status Satisfiable for NXF_Finite-Finite-Global % (32413)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32413)------------------------------ % (32413)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32413)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32413)Termination reason: Unknown % (32413)Termination phase: Finite model building constraint generation % (32413)Memory used [KB]: 805 % (32413)Time elapsed: 0.005 s % (32413)Instructions burned: 9 (million) % (32413)------------------------------ % (32413)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa15c89 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) % (32384)Running in auto input_syntax mode. Trying TPTP % (32414)ott+11_8:1_sil=64000:i=37350:fsr=off:bsr=unit_only:newcnf=on_0 on NXF_Finite-Finite-Global for (287ds/37350Mi) % (32407)Instruction limit reached! % (32407)------------------------------ % (32407)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32407)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32407)Termination reason: Time limit % (32407)Termination phase: Saturation % (32407)Memory used [KB]: 2946 % (32407)Time elapsed: 2.002 s % (32407)Instructions burned: 9568 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32415)dis-2_2:3_amm=sco:anc=none:bce=on:fsr=off:gsp=on:nm=16:nwc=1.2:nicw=on:sac=on:sp=weighted_frequency:i=80557_0 on NXF_Finite-Finite-Global for (274ds/80557Mi) % (32409)Instruction limit reached! % (32409)------------------------------ % (32409)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32409)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32409)Termination reason: Time limit % (32409)Termination phase: Saturation % (32409)Memory used [KB]: 28152 % (32409)Time elapsed: 2.355 s % (32409)Instructions burned: 10856 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32416)fmb+10_1:1_sil=128000:fmbss=21:newcnf=on:i=44200:gsp=on_0 on NXF_Finite-Finite-Global for (269ds/44200Mi) Detected minimum model sizes of [1,1] Detected maximum model sizes of [2,max] TRYING [21,21] Finite Model Found! % SZS status Satisfiable for NXF_Finite-Finite-Global % (32416)Aborted by signal SIGSEGV on NXF_Finite-Finite-Global.s % (32416)------------------------------ % (32416)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32416)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32416)Termination reason: Unknown % (32416)Termination phase: Finite model building constraint generation % (32416)Memory used [KB]: 745 % (32416)Time elapsed: 0.003 s % (32416)Instructions burned: 4 (million) % (32416)------------------------------ % (32416)------------------------------ Version : Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) call stack: 0x416001 0x1cd76a0 0x1cd5fa4 0x41c856 0x4193c6 0xa45fc5 0xa4c1bf 0xa4cf76 0xa4d5a0 0x769598 0x7693f1 0x4f70af 0xa0aff8 0xa194fd 0x1ceab70 0x489180 0x41f883 (use '--traceback on' to get a human-readable stack trace) % (32384)Running in auto input_syntax mode. Trying TPTP % (32417)dis+2_11_add=large:afr=on:amm=off:bd=off:bce=on:fsd=off:fde=none:gs=on:gsaa=full_model:gsem=off:irw=on:msp=off:nm=4:nwc=1.3:sas=z3:sims=off:sac=on:sp=reverse_arity:i=55207_0 on NXF_Finite-Finite-Global for (269ds/55207Mi) % (32410)Instruction limit reached! % (32410)------------------------------ % (32410)Version: Vampire 4.9 (commit 18c118a85 on 2024-06-08 21:14:20 +0100) % (32410)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d % (32410)Termination reason: Time limit % (32410)Termination phase: Saturation % (32410)Memory used [KB]: 7748 % (32410)Time elapsed: 2.424 s % (32410)Instructions burned: 11330 (million) % (32384)Running in auto input_syntax mode. Trying TPTP % (32418)dis+1_20_av=off:lcm=predicate:nm=2:nwc=2.0:i=81447_0 on NXF_Finite-Finite-Global for (268ds/81447Mi) % Vampire exiting % END OF SYSTEM OUTPUT RESULT: NXF_Finite-Finite-Global - Vampire-SAT---4.9 says Satisfiable - CPU = 0.05 WC = 0.13 OUTPUT: NXF_Finite-Finite-Global - Vampire-SAT---4.9 says Assurance - CPU = 0.05 WC = 0.13