%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SYN517+1 : TPTP v9.3.1. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n002.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 02:17:25 PM UTC 2026 % Result : CounterSatisfiable 0.07s 0.25s % Output : Saturation 0.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SYN517+1 : TPTP v9.3.1. Released v2.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.19 % Computer : n002.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 16:26:00 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.07/0.25 % (490897)Will run a generic schedule for satisfiability detection. % 0.07/0.25 % (490906)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=817873333:i=116_2999 on theBenchmark for (2999ds/116Mi) % 0.07/0.25 % (490906) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-490897-490906"... % 0.07/0.25 % (490906)...printing done. % 0.07/0.25 % (490903)% WARNING: option uhcvi not known. % 0.07/0.25 % SZS status CounterSatisfiable for theBenchmark % 0.07/0.25 % SZS output start Saturation. % 0.07/0.25 % SZS output end Saturation. % 0.07/0.25 % SZS output start Definitions and Model Updates. % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_1(a60) | ~c3_0 | ~c5_0 is false, set ~c5_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~ndr1_1(a60) | c4_2(a60,X7) | c5_2(a60,X7) | ~c3_0 | ~c5_0 is false, set ~c5_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_2(a60,a61) | ~c3_0 | ~c5_0 is false, set ~c5_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_2(a60,a61) | ~c3_0 | ~c5_0 is false, set ~c5_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c5_0 | c4_0 is false, set c4_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_0 | ndr1_1(a55) | ~c2_0 is false, set ~c2_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c5_0 | ~c3_0 | ~c2_0 is false, set ~c2_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | ndr1_1(a65) is false, set ndr1_1(a65) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_0 | c3_0 is false, set ndr1_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_0 | ndr1_0 | ~c2_0 is false, set ndr1_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_0 | ndr1_1(a57) | c3_0 is false, set ndr1_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_0 | ~c3_0 | ~c5_0 is false, set ndr1_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ndr1_0 is false, set ndr1_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | ndr1_0 is false, set ndr1_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_0 | c3_0 is false, set ndr1_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ndr1_0 | ndr1_1(a62) is false, set ndr1_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | ~c3_2(a65,a66) is false, set ~c3_2(a65,a66) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_0 | ~c3_2(a55,a56) | ~c2_0 is false, set ~c3_2(a55,a56) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | c4_2(a65,a66) is false, set c4_2(a65,a66) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_0 | c4_2(a55,a56) | ~c2_0 is false, set c4_2(a55,a56) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_1(a59) | c2_2(a57,a58) | c3_0 is false, set ~c4_1(a59) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_1(a59) | c4_2(a57,a58) | c3_0 is false, set ~c4_1(a59) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_1(a59) | ndr1_1(a57) | c3_0 is false, set ~c4_1(a59) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | ~ndr1_1(a65) | ~c3_2(a65,X9) | ~c1_2(a65,X9) is false, set ~c1_2(a65,X9) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c1_0 | ~c5_0 | ~ndr1_0 | c1_2(X3,a52) | c4_1(X3) | ~ndr1_1(X3) | ~c2_2(X3,X4) | ~c4_2(X3,X4) | c3_2(X3,X4) is false, set ~c1_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c1_0 | ~c5_0 | ~ndr1_0 | ~c3_2(X3,a52) | c4_1(X3) | ~ndr1_1(X3) | ~c2_2(X3,X4) | ~c4_2(X3,X4) | c3_2(X3,X4) is false, set ~c1_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | ndr1_1(a53) | c1_0 is false, set ndr1_1(a53) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_0 | ~c5_1(a57) | c3_0 is false, set ~c5_1(a57) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_1(a59) | ~c5_1(a57) | c3_0 is false, set ~c5_1(a57) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | c3_2(a53,a54) | c1_0 is false, set c3_2(a53,a54) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ndr1_0 | c3_2(a62,a63) is false, set c3_2(a62,a63) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ~c5_1(a64) | ndr1_0 is false, set ~c5_1(a64) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ~c5_1(a64) | ndr1_1(a62) is false, set ~c5_1(a64) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ~c5_1(a64) | c3_2(a62,a63) is false, set ~c5_1(a64) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c3_1(a68) | ndr1_0 | c3_0 is false, set ~c3_1(a68) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c5_1(a59) | ndr1_1(a57) | c3_0 is false, set c5_1(a59) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c5_1(a60) | ~c3_0 | ~c5_0 is false, set c5_1(a60) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | c5_1(a53) | c1_0 is false, set c5_1(a53) to true % 0.07/0.25 for all groundings, until fixed point, % 0.07/0.25 whenever c5_1(a59) | ~c5_1(a57) | c3_0 is false, set c5_1(a59) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c5_1(a59) | c2_2(a57,a58) | c3_0 is false, set c5_1(a59) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_0 | c5_1(a55) | ~c2_0 is false, set c5_1(a55) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c5_1(a59) | c4_2(a57,a58) | c3_0 is false, set c5_1(a59) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c5_1(a59) | ndr1_0 | c3_0 is false, set c5_1(a59) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c1_0 | ~c5_0 | ~ndr1_0 | ~c2_2(X3,a52) | c4_1(X3) | ~ndr1_1(X3) | ~c2_2(X3,X4) | ~c4_2(X3,X4) | c3_2(X3,X4) is false, set ~c2_2(X3,a52) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ndr1_0 | ~c2_2(a62,a63) is false, set ~c2_2(a62,a63) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ~c5_1(a64) | ~c2_2(a62,a63) is false, set ~c2_2(a62,a63) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~ndr1_0 | ~ndr1_1(X1) | c4_2(X1,X2) | ~c3_2(X1,X2) | c3_1(X1) | c5_1(X1) | ndr1_1(a50) | c1_0 is false, set c3_1(X1) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~ndr1_0 | ~ndr1_1(X1) | c4_2(X1,X2) | ~c3_2(X1,X2) | c3_1(X1) | c5_1(X1) | ~ndr1_1(a50) | c3_2(a50,X0) | c4_2(a50,X0) | ~c2_2(a50,X0) | c1_0 is false, set c4_2(a50,X0) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~ndr1_1(a68) | c3_2(a68,X11) | ~c5_2(a68,X11) | ~c4_2(a68,X11) | ~ndr1_1(a67) | ~c3_2(a67,X10) | c1_2(a67,X10) | ~c2_2(a67,X10) | c3_0 is false, set ~c5_2(a68,X11) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ~c5_1(a64) | ~ndr1_1(a62) | c1_2(a62,X8) | ~c5_2(a62,X8) | c2_2(a62,X8) is false, set ~c5_2(a62,X8) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~ndr1_0 | ~ndr1_1(X1) | c4_2(X1,X2) | ~c3_2(X1,X2) | c3_1(X1) | c5_1(X1) | ~c4_2(a50,a51) | c1_0 is false, set c3_1(X1) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c4_0 | ~ndr1_1(X13) | c3_2(X13,X14) | c4_2(X13,X14) | c2_2(X13,X14) | c3_1(X13) | ~c5_1(X13) | ~ndr1_0 | c3_1(X12) | c4_1(X12) | c5_2(X12,a69) is false, set c3_1(X13) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~ndr1_0 | ~ndr1_1(X1) | c4_2(X1,X2) | ~c3_2(X1,X2) | c3_1(X1) | c5_1(X1) | c3_2(a50,a51) | c1_0 is false, set c3_1(X1) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c4_0 | ~ndr1_1(X13) | c3_2(X13,X14) | c4_2(X13,X14) | c2_2(X13,X14) | c3_1(X13) | ~c5_1(X13) | ~ndr1_0 | c3_1(X12) | c4_1(X12) | ndr1_1(X12) is false, set c3_1(X13) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c4_0 | ~ndr1_1(X13) | c3_2(X13,X14) | c4_2(X13,X14) | c2_2(X13,X14) | c3_1(X13) | ~c5_1(X13) | ~ndr1_0 | c3_1(X12) | c4_1(X12) | ~c1_2(X12,a69) is false, set c3_1(X12) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c4_0 | ~ndr1_1(X13) | c3_2(X13,X14) | c4_2(X13,X14) | c2_2(X13,X14) | c3_1(X13) | ~c5_1(X13) | ~ndr1_0 | c3_1(X12) | c4_1(X12) | c4_2(X12,a69) is false, set c3_1(X13) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c3_1(a68) | ~ndr1_1(a67) | ~c3_2(a67,X10) | c1_2(a67,X10) | ~c2_2(a67,X10) | c3_0 is false, set ~c2_2(a67,X10) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | c2_2(a53,a54) | c1_0 is false, set c2_2(a53,a54) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_0 | c2_2(a57,a58) | c3_0 is false, set c2_2(a57,a58) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c5_1(a59) | ~c1_2(a57,a58) | c3_0 is false, set ~c1_2(a57,a58) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_1(a59) | ~c1_2(a57,a58) | c3_0 is false, set ~c1_2(a57,a58) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | c5_2(a65,a66) is false, set c5_2(a65,a66) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c5_1(a59) | ~ndr1_1(a57) | c2_2(a57,X6) | c5_2(a57,X6) | ~c3_2(a57,X6) | c3_0 is false, set c5_2(a57,X6) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_1(a59) | ~ndr1_1(a57) | c2_2(a57,X6) | c5_2(a57,X6) | ~c3_2(a57,X6) | c3_0 is false, set c5_2(a57,X6) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~ndr1_0 | ~ndr1_1(X1) | c4_2(X1,X2) | ~c3_2(X1,X2) | c3_1(X1) | c5_1(X1) | ~c1_2(a50,a51) | c1_0 is false, set ~c1_2(a50,a51) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | ~c1_2(a53,a54) | c1_0 is false, set ~c1_2(a53,a54) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_0 | ~c1_2(a57,a58) | c3_0 is false, set ~c1_2(a57,a58) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c1_2(a60,a61) | ~c3_0 | ~c5_0 is false, set ~c1_2(a60,a61) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_0 | c1_2(a55,a56) | ~c2_0 is false, set c1_2(a55,a56) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_0 | ~ndr1_1(a67) | ~c3_2(a67,X10) | c1_2(a67,X10) | ~c2_2(a67,X10) | c3_0 is false, set c1_2(a67,X10) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_0 | ~ndr1_1(a55) | c1_2(a55,X5) | c5_2(a55,X5) | c3_2(a55,X5) | ~c2_0 is false, set c1_2(a55,X5) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_0 | c4_2(a57,a58) | c3_0 is false, set c4_2(a57,a58) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_0 | ~ndr1_1(a57) | c2_2(a57,X6) | c5_2(a57,X6) | ~c3_2(a57,X6) | c3_0 is false, set c5_2(a57,X6) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~ndr1_1(a68) | c3_2(a68,X11) | ~c5_2(a68,X11) | ~c4_2(a68,X11) | ndr1_0 | c3_0 is false, set ~c5_2(a68,X11) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ndr1_0 | ~ndr1_1(a62) | c1_2(a62,X8) | ~c5_2(a62,X8) | c2_2(a62,X8) is false, set ~c5_2(a62,X8) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ndr1_0 | ~c5_2(a62,a63) is false, set ~c5_2(a62,a63) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ~c5_1(a64) | ~c5_2(a62,a63) is false, set ~c5_2(a62,a63) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c4_1(a59) | ndr1_0 | c3_0 is false, set ~c4_1(a59) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~ndr1_0 | ~ndr1_1(X1) | c4_2(X1,X2) | ~c3_2(X1,X2) | c3_1(X1) | c5_1(X1) | c3_1(a50) | c1_0 is false, set c3_1(a50) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ndr1_0 | ~c1_1(a67) | c3_0 is false, set ~c1_1(a67) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c3_1(a68) | ~c1_1(a67) | c3_0 is false, set ~c1_1(a67) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | ndr1_0 | c1_0 is false, set c1_0 to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ~c5_1(a64) | c1_1(a62) is false, set c1_1(a62) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever c2_0 | c1_1(a53) | c1_0 is false, set c1_1(a53) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~ndr1_1(a68) | c3_2(a68,X11) | ~c5_2(a68,X11) | ~c4_2(a68,X11) | ~c1_1(a67) | c3_0 is false, set ~c1_1(a67) to true % 0.07/0.25 for all groundings, % 0.07/0.25 whenever ~c5_0 | ndr1_0 | c1_1(a62) is false, set c1_1(a62) to true % 0.07/0.25 for all inputs, % 0.07/0.25 define c2_1(X0) := $true % 0.07/0.25 % SZS output end Definitions and Model Updates. % 0.07/0.25 % (490906)------------------------------ % 0.07/0.25 % (490906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.07/0.25 % (490906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.07/0.25 % (490906)CaDiCaL version: 2.1.3 % 0.07/0.25 % (490906)Termination reason: Satisfiable % 0.07/0.25 % (490906)Time elapsed: 0.002 s % 0.07/0.25 % (490906)Peak memory usage: 11 MB % 0.07/0.25 % (490906)Instructions burned: 5 (million) % 0.07/0.25 % (490897)Success in time 0.018 s % 0.07/0.25 % Vampire exiting %------------------------------------------------------------------------------