%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SYN092-1.003 : TPTP v9.3.1. Bugfixed v1.2.1. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n015.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 01:49:39 PM UTC 2026 % Result : Satisfiable 3.43s 1.16s % Output : Saturation 3.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SYN092-1.003 : TPTP v9.3.1. Bugfixed v1.2.1. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.19 % Computer : n015.cluster.edu % 0.10/0.19 % Model : x86_64 x86_64 % 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.19 % Memory : 8046.5625MB % 0.10/0.19 % OS : Linux 6.8.0-71-generic % 0.10/0.19 % CPULimit : 300 % 0.10/0.19 % WCLimit : 300 % 0.10/0.19 % DateTime : Mon Sep 28 15:36:46 UTC 2026 % 0.10/0.19 % CPUTime : % 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.22 Running first-order theorem proving % 0.10/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.43/1.16 % (2721467)Input is clausal, will run a generic CNF schedule. % 3.43/1.16 % (2721472)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=381309513:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 3.43/1.16 % (2721475)lrs+10_1_sil=8000:sp=occurrence:random_seed=727091286:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 3.43/1.16 % (2721475)Refutation not found, incomplete strategy % 3.43/1.16 % (2721475)------------------------------ % 3.43/1.16 % (2721475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.43/1.16 % (2721475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.43/1.16 % (2721475)CaDiCaL version: 2.1.3 % 3.43/1.16 % (2721475)Termination reason: Refutation not found, incomplete strategy % 3.43/1.16 % (2721475)Time elapsed: 0.001 s % 3.43/1.16 % (2721475)Peak memory usage: 86 MB % 3.43/1.16 % (2721477)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1732697751:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 3.43/1.16 % (2721473)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1374793889:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 3.43/1.16 % (2721476)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3703322907:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 3.43/1.16 % (2721474)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3041262752:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 3.43/1.16 % (2721476)Refutation not found, incomplete strategy % 3.43/1.16 % (2721476)------------------------------ % 3.43/1.16 % (2721476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.43/1.16 % (2721476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.43/1.16 % (2721476)CaDiCaL version: 2.1.3 % 3.43/1.16 % (2721476)Termination reason: Refutation not found, incomplete strategy % 3.43/1.16 % (2721476)Time elapsed: 0.0000 s % 3.43/1.16 % (2721476)Peak memory usage: 86 MB % 3.43/1.16 % (2721477)First to succeed. % 3.43/1.16 % (2721477)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2721467" % 3.43/1.16 % (2721478)dis-21_1_sil=8000:lcm=predicate:random_seed=865387990:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 3.43/1.16 % (2721478)Also succeeded, but the first one will report. % 3.43/1.16 [W928 15:36:47.733956383 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 [W928 15:36:47.733991816 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 [W928 15:36:47.734026132 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 [W928 15:36:47.734036099 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 [W928 15:36:47.734050388 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 [W928 15:36:47.734057630 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 [W928 15:36:47.734071413 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 [W928 15:36:47.734077102 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 [W928 15:36:47.734089635 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 [W928 15:36:47.734095074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 [W928 15:36:47.734108082 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 [W928 15:36:47.734120015 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 3.43/1.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 3.43/1.16 % (2721475)------------------------------ % 3.43/1.16 % (2721475)------------------------------ % 3.43/1.16 % (2721476)------------------------------ % 3.43/1.16 % (2721476)------------------------------ % 3.43/1.16 % SZS status Satisfiable for theBenchmark % 3.43/1.16 % SZS output start Saturation. % 3.43/1.16 % SZS output end Saturation. % 3.43/1.16 % SZS output start Definitions and Model Updates. % 3.43/1.16 for all inputs, % 3.43/1.16 define q_3 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define q_5 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define q_2 := $false % 3.43/1.16 for all inputs, % 3.43/1.16 define p_1 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define q_0 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define p_0 := $false % 3.43/1.16 for all inputs, % 3.43/1.16 define q_1 := $false % 3.43/1.16 for all inputs, % 3.43/1.16 define p_2 := $false % 3.43/1.16 for all inputs, % 3.43/1.16 define p_3 := $false % 3.43/1.16 for all inputs, % 3.43/1.16 define p_5 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define p_4 := $false % 3.43/1.16 for all inputs, % 3.43/1.16 define q_4 := $false % 3.43/1.16 for all inputs, % 3.43/1.16 define p_6 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define q_6 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_q_3 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_q_5 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_q_2 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_p_1 := $false % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_q_0 := $false % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_p_0 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_q_1 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_p_3 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_p_5 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_p_2 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_p_4 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_q_4 := $true % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_p_6 := $false % 3.43/1.16 for all inputs, % 3.43/1.16 define sym_q_6 := $false % 3.43/1.16 % SZS output end Definitions and Model Updates. % 3.43/1.16 % (2721477)------------------------------ % 3.43/1.16 % (2721477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.43/1.16 % (2721477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.43/1.16 % (2721477)CaDiCaL version: 2.1.3 % 3.43/1.16 % (2721477)Termination reason: Satisfiable % 3.43/1.16 % (2721477)Time elapsed: 0.001 s % 3.43/1.16 % (2721477)Peak memory usage: 87 MB % 3.43/1.16 % (2721477)------------------------------ % 3.43/1.16 % (2721477)------------------------------ % 3.43/1.16 % (2721467)Success in time 0.407 s % 3.43/1.16 % Vampire exiting %------------------------------------------------------------------------------