%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN547-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:00:55 PM UTC 2026
% Result : Satisfiable 3.94s 1.29s
% Output : Saturation 5.02s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u490,negated_conjecture,
( ~ c6_2(X1,X2)
| c8_1(X1)
| c1_2(X1,X2)
| ~ c1_1(X1)
| ~ ndr1_1(X1)
| ~ c2_2(X1,X2) ) ).
cnf(u493,negated_conjecture,
ndr1_0 ).
cnf(u512,negated_conjecture,
( ~ c6_2(X2,X3)
| c6_1(X2)
| c4_2(X2,X3)
| c1_2(X2,X3)
| ~ c7_1(X2)
| ~ ndr1_1(X2) ) ).
cnf(u527,negated_conjecture,
( ~ c4_2(X1,X3)
| c6_1(X1)
| c8_2(X1,X3)
| c6_2(X1,X2)
| c2_2(X1,X2)
| ~ c2_2(X1,X3)
| ~ c8_2(X1,X2)
| ~ ndr1_1(X1) ) ).
cnf(u530,negated_conjecture,
ssSkC23 ).
cnf(u546,negated_conjecture,
~ c1_0 ).
cnf(u551,negated_conjecture,
~ ndr1_1(a573) ).
cnf(u566,negated_conjecture,
~ c2_0 ).
cnf(u580,negated_conjecture,
( ~ c7_2(X1,X3)
| c2_2(X1,X3)
| c2_2(X1,X2)
| c1_2(X1,X2)
| ~ c5_1(X1)
| ~ c1_2(X1,X3)
| ~ c5_2(X1,X2)
| ~ ndr1_1(X1) ) ).
cnf(u587,negated_conjecture,
c8_0 ).
cnf(u595,negated_conjecture,
( ~ c6_2(X0,X2)
| c6_1(X0)
| c7_2(X0,X1)
| c1_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X2)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u603,negated_conjecture,
( ~ c1_2(X0,X1)
| c8_2(X0,X2)
| c3_2(X0,X2)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c2_2(X0,X3)
| c6_2(X0,X3)
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u606,negated_conjecture,
ssSkC22 ).
cnf(u676,negated_conjecture,
( ~ c6_2(X0,X1)
| c8_2(X0,X2)
| c2_2(X0,X2)
| c7_2(X0,X2)
| c3_2(X0,X1)
| ~ c8_1(X0)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u712,negated_conjecture,
( ~ c4_2(X0,X1)
| c8_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u732,negated_conjecture,
( ~ c8_2(X0,X2)
| c5_1(X0)
| c3_2(X0,X2)
| c6_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u762,negated_conjecture,
c3_1(a573) ).
cnf(u767,negated_conjecture,
c1_1(a573) ).
cnf(u778,negated_conjecture,
( ~ c6_2(X0,X1)
| c7_1(X0)
| c4_1(X0)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u783,negated_conjecture,
~ c7_0 ).
cnf(u793,negated_conjecture,
( ~ c8_2(X1,X2)
| c4_1(X1)
| c8_1(X1)
| c3_2(X1,X2)
| c1_2(X1,X2)
| ~ ndr1_1(X1) ) ).
cnf(u800,negated_conjecture,
c6_0 ).
cnf(u808,negated_conjecture,
( ~ c4_2(X0,X1)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u812,negated_conjecture,
~ c5_0 ).
cnf(u819,negated_conjecture,
( ~ c6_1(X0)
| c5_1(X0)
| ~ c3_1(X0) ) ).
cnf(u865,negated_conjecture,
ssSkC1 ).
cnf(u922,negated_conjecture,
~ c3_1(a533) ).
cnf(u928,negated_conjecture,
ssSkC13 ).
cnf(u933,negated_conjecture,
( ~ c6_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_1(X0)
| ~ c7_2(X0,a548)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u936,negated_conjecture,
ssSkC17 ).
cnf(u941,negated_conjecture,
( ~ c6_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_1(X0)
| ~ c4_2(X0,a548)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u959,negated_conjecture,
~ ssSkC24 ).
cnf(u967,negated_conjecture,
~ ssSkC3 ).
cnf(u971,negated_conjecture,
( ~ c8_2(X0,X1)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c8_1(X0)
| ~ c7_2(X0,a479)
| ~ ndr1_1(X0) ) ).
cnf(u976,negated_conjecture,
ssSkC7 ).
cnf(u995,negated_conjecture,
( ~ c7_2(X0,X1)
| c2_1(X0)
| c3_2(X0,X1)
| ~ c6_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1028,negated_conjecture,
( ~ c2_1(X0)
| c1_1(X0)
| c1_2(X0,X1)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1037,negated_conjecture,
( ~ c6_2(X0,X1)
| c2_2(X0,a548)
| c3_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1046,negated_conjecture,
( ~ c8_2(X0,X1)
| c6_2(X0,a479)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1050,negated_conjecture,
~ ssSkC4 ).
cnf(u1054,negated_conjecture,
( ~ c6_2(X0,X1)
| c8_1(X0)
| c8_2(X0,a481)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u1058,negated_conjecture,
( ~ c6_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a481)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u1110,negated_conjecture,
ssSkC10 ).
cnf(u1114,negated_conjecture,
ssSkC9 ).
cnf(u1118,negated_conjecture,
( ~ c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_2(X0,a516)
| ~ ndr1_1(X0)
| ~ ssSkP5(X0) ) ).
cnf(u1122,negated_conjecture,
( ~ c6_2(X0,a516)
| c5_2(X0,X1)
| ~ ssSkP5(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1126,negated_conjecture,
( ~ c5_2(X0,a572)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c4_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1130,negated_conjecture,
( ~ c6_2(X0,a572)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c4_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1137,negated_conjecture,
ndr1_1(a544) ).
cnf(u1141,negated_conjecture,
( ~ c8_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1144,negated_conjecture,
ssSkC16 ).
cnf(u1153,negated_conjecture,
( ~ c4_1(X0)
| c2_2(X0,a572)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1158,negated_conjecture,
ssSkC15 ).
cnf(u1189,negated_conjecture,
ndr1_1(a566) ).
cnf(u1193,negated_conjecture,
( ~ c1_2(a566,X0)
| c5_2(a566,X0)
| ~ c2_2(a566,X0) ) ).
cnf(u1196,negated_conjecture,
ssSkC20 ).
cnf(u1200,negated_conjecture,
ssSkC19 ).
cnf(u1218,negated_conjecture,
ssSkC2 ).
cnf(u1269,negated_conjecture,
~ ssSkC5 ).
cnf(u1274,negated_conjecture,
~ ndr1_1(a538) ).
cnf(u1280,negated_conjecture,
ssSkC14 ).
cnf(u1306,negated_conjecture,
~ ndr1_1(a592) ).
cnf(u1360,negated_conjecture,
( ~ c3_2(X0,a553)
| ~ c5_1(X0)
| ~ c4_1(X0) ) ).
cnf(u1363,negated_conjecture,
ssSkC18 ).
cnf(u1368,negated_conjecture,
( ~ c2_2(X0,a553)
| ~ c5_1(X0)
| ~ c4_1(X0) ) ).
cnf(u1384,negated_conjecture,
~ ssSkC0 ).
cnf(u1388,negated_conjecture,
( ~ c3_2(X0,a459)
| ~ c8_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1392,negated_conjecture,
( ~ c6_2(X0,a459)
| ~ c8_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1396,negated_conjecture,
~ ssSkC6 ).
cnf(u1404,negated_conjecture,
~ ndr1_1(a491) ).
cnf(u1417,negated_conjecture,
~ c3_2(a544,a545) ).
cnf(u1422,negated_conjecture,
~ c4_2(a544,a545) ).
cnf(u1427,negated_conjecture,
~ c7_2(a544,a545) ).
cnf(u1447,negated_conjecture,
ssSkC25 ).
cnf(u1513,negated_conjecture,
( ~ c4_1(X0)
| c7_2(X0,a553)
| ~ c5_1(X0) ) ).
cnf(u1533,negated_conjecture,
( ~ c8_1(X0)
| c7_2(X0,a459)
| ~ c3_1(X0) ) ).
cnf(u1558,negated_conjecture,
~ ssSkC26 ).
cnf(u1563,negated_conjecture,
~ ndr1_1(a600) ).
cnf(u1600,negated_conjecture,
( ~ c4_1(X0)
| ndr1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1624,negated_conjecture,
( ~ c8_1(X0)
| ndr1_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1628,negated_conjecture,
( ~ c2_1(X0)
| c5_1(X0)
| c4_2(X0,a487) ) ).
cnf(u1632,negated_conjecture,
( ~ c2_1(X0)
| c5_1(X0)
| c1_2(X0,a487) ) ).
cnf(u1645,negated_conjecture,
~ ndr1_1(a568) ).
cnf(u1657,negated_conjecture,
( ~ c2_1(X0)
| c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u1767,negated_conjecture,
~ c8_2(a498,a499) ).
cnf(u1772,negated_conjecture,
~ c7_2(a498,a500) ).
cnf(u1780,negated_conjecture,
ssSkC11 ).
cnf(u1786,negated_conjecture,
~ c1_2(a520,a521) ).
cnf(u1791,negated_conjecture,
~ c4_2(a520,a521) ).
cnf(u1826,negated_conjecture,
~ c1_2(a566,a567) ).
cnf(u1831,negated_conjecture,
~ c8_2(a566,a567) ).
cnf(u1943,negated_conjecture,
c7_2(a498,a499) ).
cnf(u1948,negated_conjecture,
c3_2(a498,a499) ).
cnf(u1953,negated_conjecture,
c4_2(a498,a500) ).
cnf(u1958,negated_conjecture,
c8_2(a498,a500) ).
cnf(u1973,negated_conjecture,
~ c2_1(a520) ).
cnf(u1978,negated_conjecture,
~ c5_1(a520) ).
cnf(u1983,negated_conjecture,
c2_2(a520,a521) ).
cnf(u2003,negated_conjecture,
c6_2(a566,a567) ).
cnf(u2073,negated_conjecture,
~ c5_1(a491) ).
cnf(u2078,negated_conjecture,
~ c4_1(a491) ).
cnf(u2123,negated_conjecture,
~ c4_1(a568) ).
cnf(u2128,negated_conjecture,
~ c6_1(a592) ).
cnf(u2176,negated_conjecture,
c7_1(a498) ).
cnf(u2181,negated_conjecture,
ndr1_1(a498) ).
cnf(u2196,negated_conjecture,
ndr1_1(a520) ).
cnf(u2202,negated_conjecture,
c1_1(a538) ).
cnf(u2217,negated_conjecture,
c1_1(a566) ).
cnf(u2223,negated_conjecture,
c3_2(a570,a571) ).
cnf(u2228,negated_conjecture,
c1_2(a570,a571) ).
cnf(u2233,negated_conjecture,
c2_2(a570,a571) ).
cnf(u2380,negated_conjecture,
c3_1(a600) ).
cnf(u2395,negated_conjecture,
c5_1(a570) ).
cnf(u2400,negated_conjecture,
c4_1(a570) ).
cnf(u2405,negated_conjecture,
ndr1_1(a570) ).
cnf(u2467,negated_conjecture,
~ c6_1(a570) ).
cnf(u2483,negated_conjecture,
~ ssSkP5(a498) ).
cnf(u2491,negated_conjecture,
c5_2(a498,a500) ).
cnf(u2500,negated_conjecture,
~ c6_1(a498) ).
cnf(u2503,negated_conjecture,
~ c3_2(a498,a515) ).
cnf(u2507,negated_conjecture,
~ c2_1(a498) ).
cnf(u2514,negated_conjecture,
( c5_2(a570,X0)
| c2_2(a570,X0) ) ).
cnf(u2528,negated_conjecture,
~ c2_2(a566,a567) ).
cnf(u2540,negated_conjecture,
~ c7_1(a566) ).
cnf(u2557,negated_conjecture,
c1_2(a498,a500) ).
cnf(u2581,negated_conjecture,
~ c3_2(a566,a567) ).
cnf(u2621,negated_conjecture,
c4_2(a498,a515) ).
cnf(u2646,negated_conjecture,
~ c5_1(a498) ).
cnf(u2652,negated_conjecture,
~ c2_2(a498,a515) ).
cnf(u2668,negated_conjecture,
~ c1_2(a570,a553) ).
cnf(u2685,negated_conjecture,
( ~ c7_2(a498,X0)
| c6_2(a498,X0)
| c3_2(a498,X0) ) ).
cnf(u2692,negated_conjecture,
c6_2(a498,a515) ).
cnf(u2730,negated_conjecture,
~ c1_1(a498) ).
cnf(clause130,negated_conjecture,
( ssSkP2(X0)
| c4_2(X0,a492) ) ).
cnf(clause187,negated_conjecture,
( ~ c2_2(X0,a515)
| ssSkP5(X0) ) ).
cnf(clause73,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(clause181,negated_conjecture,
( ~ c6_2(X0,a554)
| ssSkP7(X0) ) ).
cnf(clause201,negated_conjecture,
( ~ c4_2(X0,a456)
| ssSkP0(X0) ) ).
cnf(clause197,negated_conjecture,
( ~ c7_2(X0,a492)
| ssSkP2(X0) ) ).
cnf(clause180,negated_conjecture,
( ~ c1_2(X0,a588)
| ssSkP8(X0) ) ).
cnf(clause75,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(clause188,negated_conjecture,
( ~ c3_2(X0,a515)
| ssSkP5(X0) ) ).
cnf(clause72,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u2493,negated_conjecture,
c7_2(a498,a515) ).
cnf(clause134,negated_conjecture,
( ssSkP0(X0)
| c8_2(X0,a456) ) ).
cnf(clause53,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(clause199,negated_conjecture,
( ~ c3_2(X0,a485)
| ssSkP1(X0) ) ).
cnf(clause116,negated_conjecture,
( ssSkP8(X0)
| c5_2(X0,a588) ) ).
cnf(clause126,negated_conjecture,
( ssSkP5(X0)
| c7_2(X0,a515) ) ).
cnf(clause198,negated_conjecture,
( ~ c2_2(X0,a485)
| ssSkP1(X0) ) ).
cnf(clause200,negated_conjecture,
( ~ c1_2(X0,a485)
| ssSkP1(X0) ) ).
cnf(clause133,negated_conjecture,
( ssSkP0(X0)
| c6_2(X0,a456) ) ).
cnf(clause182,negated_conjecture,
( ~ c3_2(X0,a554)
| ssSkP7(X0) ) ).
cnf(clause196,negated_conjecture,
( ~ c6_2(X0,a492)
| ssSkP2(X0) ) ).
cnf(clause66,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(clause46,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u2460,negated_conjecture,
c7_2(a570,a553) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN547-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.17 % Computer : n001.cluster.edu
% 0.11/0.17 % Model : x86_64 x86_64
% 0.11/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.17 % Memory : 8046.5625MB
% 0.11/0.17 % OS : Linux 6.8.0-71-generic
% 0.11/0.17 % CPULimit : 300
% 0.11/0.17 % WCLimit : 300
% 0.11/0.17 % DateTime : Mon Sep 28 16:34:00 UTC 2026
% 0.11/0.17 % CPUTime :
% 0.11/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.20 Running first-order theorem proving
% 0.11/0.20 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.94/1.29 % (470375)Input is clausal, will run a generic CNF schedule.
% 3.94/1.29 % (470384)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=637313992:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.94/1.29 % (470380)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=1910447825:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.94/1.29 % (470386)dis-21_1_sil=8000:lcm=predicate:random_seed=2450800543: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.94/1.29 % (470382)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1118661718:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.94/1.29 % (470381)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1103689559:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.94/1.29 % (470385)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=618550200:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.94/1.29 % (470383)lrs+10_1_sil=8000:sp=occurrence:random_seed=547207521:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.94/1.29 % (470384)Instruction limit reached!
% 3.94/1.29 % (470384)------------------------------
% 3.94/1.29 % (470384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.29 % (470384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.29 % (470384)CaDiCaL version: 2.1.3
% 3.94/1.29 % (470384)Termination reason: Instruction limit
% 3.94/1.29 % (470384)Termination phase: Saturation
% 3.94/1.29 % (470384)Time elapsed: 0.034 s
% 3.94/1.29 % (470384)Peak memory usage: 90 MB
% 3.94/1.29 % (470384)Instructions burned: 114 (million)
% 3.94/1.29 % (470385)Refutation not found, incomplete strategy
% 3.94/1.29 % (470385)------------------------------
% 3.94/1.29 % (470385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.29 % (470385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.29 % (470385)CaDiCaL version: 2.1.3
% 3.94/1.29 % (470385)Termination reason: Refutation not found, incomplete strategy
% 3.94/1.29 % (470385)Time elapsed: 0.020 s
% 3.94/1.29 % (470385)Peak memory usage: 89 MB
% 3.94/1.29 % (470385)Instructions burned: 32 (million)
% 3.94/1.29 % (470383)Instruction limit reached!
% 3.94/1.29 % (470383)------------------------------
% 3.94/1.29 % (470383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.29 % (470383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.29 % (470383)CaDiCaL version: 2.1.3
% 3.94/1.29 % (470383)Termination reason: Instruction limit
% 3.94/1.29 % (470383)Termination phase: Saturation
% 3.94/1.29 % (470383)Time elapsed: 0.059 s
% 3.94/1.29 % (470383)Peak memory usage: 90 MB
% 3.94/1.29 % (470383)Instructions burned: 107 (million)
% 3.94/1.29 % (470386)Instruction limit reached!
% 3.94/1.29 % (470386)------------------------------
% 3.94/1.29 % (470386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.29 % (470386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.29 % (470386)CaDiCaL version: 2.1.3
% 3.94/1.29 % (470386)Termination reason: Instruction limit
% 3.94/1.29 % (470386)Termination phase: Saturation
% 3.94/1.29 % (470386)Time elapsed: 0.064 s
% 3.94/1.29 % (470386)Peak memory usage: 90 MB
% 3.94/1.29 % (470386)Instructions burned: 118 (million)
% 3.94/1.29 % (470394)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=731106302:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.94/1.29 % (470394)Instruction limit reached!
% 3.94/1.29 % (470394)------------------------------
% 3.94/1.29 % (470394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.29 % (470394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.29 % (470394)CaDiCaL version: 2.1.3
% 3.94/1.29 % (470394)Termination reason: Instruction limit
% 3.94/1.29 % (470394)Termination phase: Saturation
% 3.94/1.29 % (470394)Time elapsed: 0.040 s
% 3.94/1.29 % (470394)Peak memory usage: 90 MB
% 3.94/1.29 % (470394)Instructions burned: 147 (million)
% 3.94/1.29 % (470396)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1007895590:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 3.94/1.29 % (470395)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1625150597:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 3.94/1.29 % (470395)Refutation not found, incomplete strategy
% 3.94/1.29 % (470395)------------------------------
% 3.94/1.29 % (470395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.29 % (470395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.29 % (470395)CaDiCaL version: 2.1.3
% 3.94/1.29 % (470395)Termination reason: Refutation not found, incomplete strategy
% 3.94/1.29 % (470395)Time elapsed: 0.030 s
% 3.94/1.29 % (470395)Peak memory usage: 89 MB
% 3.94/1.29 % (470395)Instructions burned: 51 (million)
% 3.94/1.29 % (470385)------------------------------
% 3.94/1.29 % (470385)------------------------------
% 3.94/1.29 % (470398)lrs+10_64_to=lpo:sil=8000:random_seed=1617781027:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 3.94/1.29 % (470398)First to succeed.
% 3.94/1.29 % (470398)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-470375"
% 3.94/1.29 % (470396)Instruction limit reached!
% 3.94/1.29 % (470396)------------------------------
% 3.94/1.29 % (470396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.29 % (470396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.29 % (470396)CaDiCaL version: 2.1.3
% 3.94/1.29 % (470396)Termination reason: Instruction limit
% 3.94/1.29 % (470396)Termination phase: Saturation
% 3.94/1.29 % (470396)Time elapsed: 0.113 s
% 3.94/1.29 % (470396)Peak memory usage: 90 MB
% 3.94/1.29 % (470396)Instructions burned: 219 (million)
% 3.94/1.29 % SZS status Satisfiable for theBenchmark
% 3.94/1.29 % SZS output start Saturation.
% See solution above
% 5.02/1.49 % SZS output start Definitions and Model Updates.
% 5.02/1.49 for all inputs,
% 5.02/1.49 define c3_0 := $true
% 5.02/1.49 for all inputs,
% 5.02/1.49 define ssSkP6(X0) := $true
% 5.02/1.49 for all inputs,
% 5.02/1.49 define ssSkC12 := $true
% 5.02/1.49 for all inputs,
% 5.02/1.49 define ssSkP3(X0) := $true
% 5.02/1.49 for all inputs,
% 5.02/1.49 define ssSkP4(X0) := $true
% 5.02/1.49 for all inputs,
% 5.02/1.49 define ssSkC8 := $true
% 5.02/1.49 for all inputs,
% 5.02/1.49 define c4_0 := $false
% 5.02/1.49 % SZS output end Definitions and Model Updates.
% 5.02/1.49 % (470398)------------------------------
% 5.02/1.49 % (470398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.02/1.49 % (470398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.02/1.49 % (470398)CaDiCaL version: 2.1.3
% 5.02/1.49 % (470398)Termination reason: Satisfiable
% 5.02/1.49 % (470398)Time elapsed: 0.008 s
% 5.02/1.49 % (470398)Peak memory usage: 89 MB
% 5.02/1.49 % (470398)Instructions burned: 22 (million)
% 5.02/1.49 % (470398)------------------------------
% 5.02/1.49 % (470398)------------------------------
% 5.02/1.49 % (470375)Success in time 0.637 s
% 5.02/1.49 % Vampire exiting
%------------------------------------------------------------------------------