%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN437-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 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:08:14 PM UTC 2026
% Result : Satisfiable 0.19s 0.27s
% Output : Saturation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u265,negated_conjecture,
ndr1_0 ).
cnf(u269,negated_conjecture,
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u273,negated_conjecture,
( ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1) ) ).
cnf(u276,negated_conjecture,
( ~ c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ).
cnf(u280,negated_conjecture,
( c3_1(X2)
| ~ c0_1(X2)
| c2_1(X2) ) ).
cnf(u284,negated_conjecture,
( ~ c0_1(X0)
| c1_1(X0)
| c3_1(X0) ) ).
cnf(u291,negated_conjecture,
( ~ c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1) ) ).
cnf(u295,negated_conjecture,
~ hskp7 ).
cnf(u306,negated_conjecture,
( ~ c3_1(X1)
| c2_1(X1)
| c1_1(X1) ) ).
cnf(u309,negated_conjecture,
( ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0) ) ).
cnf(u313,negated_conjecture,
~ hskp1 ).
cnf(u317,negated_conjecture,
( ~ c3_1(X0)
| c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u322,negated_conjecture,
hskp34 ).
cnf(u325,negated_conjecture,
( ~ c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) ) ).
cnf(u330,negated_conjecture,
hskp36 ).
cnf(u337,negated_conjecture,
~ hskp19 ).
cnf(u346,negated_conjecture,
hskp11 ).
cnf(u353,negated_conjecture,
( ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0) ) ).
cnf(u361,negated_conjecture,
~ hskp5 ).
cnf(u369,negated_conjecture,
~ hskp46 ).
cnf(u377,negated_conjecture,
~ hskp44 ).
cnf(u382,negated_conjecture,
~ hskp43 ).
cnf(u386,negated_conjecture,
( ~ c1_1(X1)
| c3_1(X1)
| ~ c2_1(X1) ) ).
cnf(u393,negated_conjecture,
~ hskp0 ).
cnf(u397,negated_conjecture,
( ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1) ) ).
cnf(u401,negated_conjecture,
~ hskp32 ).
cnf(u405,negated_conjecture,
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ) ).
cnf(u409,negated_conjecture,
( ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0) ) ).
cnf(u413,negated_conjecture,
~ hskp40 ).
cnf(u418,negated_conjecture,
~ hskp37 ).
cnf(u423,negated_conjecture,
~ hskp16 ).
cnf(u432,negated_conjecture,
hskp14 ).
cnf(u439,negated_conjecture,
~ hskp42 ).
cnf(u445,negated_conjecture,
~ hskp31 ).
cnf(u450,negated_conjecture,
~ hskp4 ).
cnf(u455,negated_conjecture,
~ hskp21 ).
cnf(u459,negated_conjecture,
~ hskp47 ).
cnf(u464,negated_conjecture,
~ hskp15 ).
cnf(u468,negated_conjecture,
~ hskp45 ).
cnf(u473,negated_conjecture,
~ hskp49 ).
cnf(u478,negated_conjecture,
~ hskp20 ).
cnf(u483,negated_conjecture,
~ hskp18 ).
cnf(u488,negated_conjecture,
hskp17 ).
cnf(u492,negated_conjecture,
~ hskp41 ).
cnf(u497,negated_conjecture,
hskp13 ).
cnf(u501,negated_conjecture,
~ hskp12 ).
cnf(u505,negated_conjecture,
~ hskp38 ).
cnf(u510,negated_conjecture,
~ hskp2 ).
cnf(u514,negated_conjecture,
~ hskp27 ).
cnf(u519,negated_conjecture,
~ hskp23 ).
cnf(u524,negated_conjecture,
hskp22 ).
cnf(u531,negated_conjecture,
~ hskp10 ).
cnf(u536,negated_conjecture,
hskp9 ).
cnf(u540,negated_conjecture,
~ hskp8 ).
cnf(u544,negated_conjecture,
~ hskp35 ).
cnf(u550,negated_conjecture,
hskp6 ).
cnf(u553,negated_conjecture,
~ hskp33 ).
cnf(u558,negated_conjecture,
~ hskp30 ).
cnf(u562,negated_conjecture,
~ hskp29 ).
cnf(u567,negated_conjecture,
~ hskp26 ).
cnf(u572,negated_conjecture,
hskp25 ).
cnf(u577,negated_conjecture,
hskp39 ).
cnf(u581,negated_conjecture,
c1_1(a402) ).
cnf(u586,negated_conjecture,
c2_1(a402) ).
cnf(u591,negated_conjecture,
c3_1(a402) ).
cnf(u596,negated_conjecture,
c1_1(a403) ).
cnf(u601,negated_conjecture,
c2_1(a405) ).
cnf(u606,negated_conjecture,
hskp3 ).
cnf(u611,negated_conjecture,
~ c3_1(a407) ).
cnf(u616,negated_conjecture,
~ c0_1(a407) ).
cnf(u621,negated_conjecture,
~ c1_1(a407) ).
cnf(u625,negated_conjecture,
c3_1(a411) ).
cnf(u630,negated_conjecture,
c1_1(a411) ).
cnf(u635,negated_conjecture,
c2_1(a411) ).
cnf(u640,negated_conjecture,
c3_1(a413) ).
cnf(u645,negated_conjecture,
c1_1(a413) ).
cnf(u651,negated_conjecture,
~ c1_1(a416) ).
cnf(u656,negated_conjecture,
~ c3_1(a416) ).
cnf(u660,negated_conjecture,
c2_1(a418) ).
cnf(u665,negated_conjecture,
c3_1(a418) ).
cnf(u670,negated_conjecture,
c3_1(a420) ).
cnf(u675,negated_conjecture,
c2_1(a420) ).
cnf(u681,negated_conjecture,
~ c0_1(a421) ).
cnf(u696,negated_conjecture,
~ c2_1(a428) ).
cnf(u701,negated_conjecture,
~ c1_1(a428) ).
cnf(u706,negated_conjecture,
~ c0_1(a428) ).
cnf(u710,negated_conjecture,
c2_1(a430) ).
cnf(u716,negated_conjecture,
~ c0_1(a433) ).
cnf(u721,negated_conjecture,
~ c3_1(a433) ).
cnf(u726,negated_conjecture,
~ c2_1(a433) ).
cnf(u731,negated_conjecture,
~ c2_1(a437) ).
cnf(u736,negated_conjecture,
~ c1_1(a437) ).
cnf(u741,negated_conjecture,
~ c3_1(a437) ).
cnf(u745,negated_conjecture,
c3_1(a440) ).
cnf(u761,negated_conjecture,
~ c0_1(a443) ).
cnf(u766,negated_conjecture,
~ c1_1(a443) ).
cnf(u811,negated_conjecture,
~ c2_1(a451) ).
cnf(u816,negated_conjecture,
~ c3_1(a451) ).
cnf(u821,negated_conjecture,
~ c0_1(a451) ).
cnf(u826,negated_conjecture,
~ c0_1(a452) ).
cnf(u831,negated_conjecture,
~ c1_1(a452) ).
cnf(u836,negated_conjecture,
~ hskp24 ).
cnf(u839,negated_conjecture,
c2_1(a454) ).
cnf(u844,negated_conjecture,
c3_1(a454) ).
cnf(u850,negated_conjecture,
~ c0_1(a460) ).
cnf(u859,negated_conjecture,
c2_1(a404) ).
cnf(u864,negated_conjecture,
c3_1(a404) ).
cnf(u870,negated_conjecture,
~ hskp28 ).
cnf(u873,negated_conjecture,
c3_1(a408) ).
cnf(u879,negated_conjecture,
~ c0_1(a408) ).
cnf(u883,negated_conjecture,
c3_1(a409) ).
cnf(u888,negated_conjecture,
c1_1(a409) ).
cnf(u893,negated_conjecture,
c2_1(a410) ).
cnf(u899,negated_conjecture,
~ c0_1(a410) ).
cnf(u918,negated_conjecture,
c3_1(a415) ).
cnf(u924,negated_conjecture,
~ c0_1(a417) ).
cnf(u929,negated_conjecture,
~ c0_1(a424) ).
cnf(u934,negated_conjecture,
~ c2_1(a427) ).
cnf(u939,negated_conjecture,
~ c1_1(a427) ).
cnf(u943,negated_conjecture,
c3_1(a429) ).
cnf(u949,negated_conjecture,
~ c0_1(a429) ).
cnf(u953,negated_conjecture,
c3_1(a432) ).
cnf(u974,negated_conjecture,
~ c2_1(a439) ).
cnf(u978,negated_conjecture,
c3_1(a446) ).
cnf(u983,negated_conjecture,
c2_1(a446) ).
cnf(u988,negated_conjecture,
c3_1(a449) ).
cnf(u1004,negated_conjecture,
~ hskp50 ).
cnf(u1007,negated_conjecture,
c1_1(a462) ).
cnf(u1013,negated_conjecture,
~ hskp51 ).
cnf(u1017,negated_conjecture,
~ c2_1(a464) ).
cnf(u1022,negated_conjecture,
c3_1(a403) ).
cnf(u1027,negated_conjecture,
c2_1(a403) ).
cnf(u1031,negated_conjecture,
~ c0_1(a405) ).
cnf(u1037,negated_conjecture,
c1_1(a405) ).
cnf(u1041,negated_conjecture,
~ c0_1(a413) ).
cnf(u1047,negated_conjecture,
c2_1(a416) ).
cnf(u1052,negated_conjecture,
c1_1(a418) ).
cnf(u1057,negated_conjecture,
c1_1(a420) ).
cnf(u1062,negated_conjecture,
c2_1(a421) ).
cnf(u1067,negated_conjecture,
c3_1(a421) ).
cnf(u1077,negated_conjecture,
c3_1(a430) ).
cnf(u1082,negated_conjecture,
c1_1(a430) ).
cnf(u1086,negated_conjecture,
~ c0_1(a440) ).
cnf(u1092,negated_conjecture,
c2_1(a440) ).
cnf(u1102,negated_conjecture,
c2_1(a443) ).
cnf(u1126,negated_conjecture,
~ c3_1(a452) ).
cnf(u1131,negated_conjecture,
~ c0_1(a454) ).
cnf(u1137,negated_conjecture,
c2_1(a460) ).
cnf(u1142,negated_conjecture,
c1_1(a460) ).
cnf(u1157,negated_conjecture,
c1_1(a404) ).
cnf(u1162,negated_conjecture,
c2_1(a408) ).
cnf(u1166,negated_conjecture,
~ c0_1(a409) ).
cnf(u1172,negated_conjecture,
c1_1(a410) ).
cnf(u1191,negated_conjecture,
~ c0_1(a415) ).
cnf(u1197,negated_conjecture,
c1_1(a415) ).
cnf(u1202,negated_conjecture,
c2_1(a417) ).
cnf(u1207,negated_conjecture,
c1_1(a417) ).
cnf(u1227,negated_conjecture,
c2_1(a424) ).
cnf(u1232,negated_conjecture,
c3_1(a424) ).
cnf(u1236,negated_conjecture,
~ c3_1(a427) ).
cnf(u1242,negated_conjecture,
c1_1(a429) ).
cnf(u1247,negated_conjecture,
c2_1(a431) ).
cnf(u1252,negated_conjecture,
c1_1(a431) ).
cnf(u1257,negated_conjecture,
c3_1(a431) ).
cnf(u1262,negated_conjecture,
c2_1(a432) ).
cnf(u1267,negated_conjecture,
c1_1(a432) ).
cnf(u1316,negated_conjecture,
~ c0_1(a439) ).
cnf(u1321,negated_conjecture,
~ c3_1(a439) ).
cnf(u1327,negated_conjecture,
c1_1(a446) ).
cnf(u1332,negated_conjecture,
c1_1(a449) ).
cnf(u1336,negated_conjecture,
~ c0_1(a449) ).
cnf(u1342,negated_conjecture,
c1_1(a455) ).
cnf(u1345,negated_conjecture,
hskp48 ).
cnf(u1351,negated_conjecture,
c2_1(a455) ).
cnf(u1356,negated_conjecture,
c3_1(a455) ).
cnf(u1365,negated_conjecture,
~ c0_1(a462) ).
cnf(u1371,negated_conjecture,
c3_1(a462) ).
cnf(u1375,negated_conjecture,
~ c0_1(a464) ).
cnf(u1380,negated_conjecture,
~ c1_1(a464) ).
cnf(u1865,negated_conjecture,
c1_1(a424) ).
cnf(u1764,negated_conjecture,
~ c1_1(a433) ).
cnf(u1761,negated_conjecture,
~ c0_1(X0) ).
cnf(u1872,negated_conjecture,
c1_1(a440) ).
cnf(u1604,negated_conjecture,
( c3_1(X1)
| ~ c1_1(X1) ) ).
cnf(u1959,negated_conjecture,
c2_1(a413) ).
cnf(u1949,negated_conjecture,
c2_1(a409) ).
cnf(u1870,negated_conjecture,
c1_1(a454) ).
cnf(u1498,negated_conjecture,
( ~ c0_1(X0)
| c1_1(X0) ) ).
cnf(u1946,negated_conjecture,
c2_1(a429) ).
cnf(u1400,negated_conjecture,
( c2_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1758,negated_conjecture,
( ~ c3_1(X1)
| ~ c0_1(X1) ) ).
cnf(u1399,negated_conjecture,
( ~ c3_1(X1)
| c2_1(X1) ) ).
cnf(u1874,negated_conjecture,
c1_1(a421) ).
cnf(u1655,negated_conjecture,
( ~ c3_1(X0)
| c1_1(X0) ) ).
cnf(u1660,negated_conjecture,
~ c1_1(a439) ).
cnf(u1942,negated_conjecture,
c2_1(a449) ).
cnf(u1948,negated_conjecture,
c2_1(a415) ).
cnf(u1484,negated_conjecture,
~ c1_1(a451) ).
cnf(u1868,negated_conjecture,
c1_1(a408) ).
cnf(u1940,negated_conjecture,
c2_1(a462) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN437-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n001.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 16:06:04 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.27 % (459393)Will run a generic schedule for satisfiability detection.
% 0.19/0.27 % (459402)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=527708778:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.27 % (459399)% WARNING: option uhcvi not known.
% 0.19/0.27 % (459398)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3452514200_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.27 % (459399)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1772845182:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.27 % (459400)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=713225127:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.27 % (459401)dis+10_1_sil=32000:sp=arity:random_seed=3507482039:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.27 % (459403)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1858695923:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.27 % (459404)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2413904904:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.27 % (459402) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-459393-459402"...
% 0.19/0.27 % (459402)...printing done.
% 0.19/0.27 % SZS status Satisfiable for theBenchmark
% 0.19/0.27 % SZS output start Saturation.
% See solution above
% 0.19/0.27 % SZS output start Definitions and Model Updates.
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp11 | ndr1_0 is false, set ~hskp11 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp40 | ndr1_0 is false, set ~hskp40 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp36 | ndr1_0 is false, set ~hskp36 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp34 | ndr1_0 is false, set ~hskp34 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp0 | ndr1_0 is false, set ~hskp0 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp30 | ndr1_0 is false, set ~hskp30 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp29 | ndr1_0 is false, set ~hskp29 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp27 | ndr1_0 is false, set ~hskp27 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp45 | ndr1_0 is false, set ~hskp45 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp26 | ndr1_0 is false, set ~hskp26 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp25 | ndr1_0 is false, set ~hskp25 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp44 | ndr1_0 is false, set ~hskp44 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp43 | ndr1_0 is false, set ~hskp43 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp23 | ndr1_0 is false, set ~hskp23 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp22 | ndr1_0 is false, set ~hskp22 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp21 | ndr1_0 is false, set ~hskp21 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp20 | ndr1_0 is false, set ~hskp20 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp41 | ndr1_0 is false, set ~hskp41 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp19 | ndr1_0 is false, set ~hskp19 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp42 | ndr1_0 is false, set ~hskp42 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp18 | ndr1_0 is false, set ~hskp18 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp16 | ndr1_0 is false, set ~hskp16 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp15 | ndr1_0 is false, set ~hskp15 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp39 | ndr1_0 is false, set ~hskp39 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp14 | ndr1_0 is false, set ~hskp14 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp38 | ndr1_0 is false, set ~hskp38 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp13 | ndr1_0 is false, set ~hskp13 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp12 | ndr1_0 is false, set ~hskp12 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp10 | ndr1_0 is false, set ~hskp10 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp9 | ndr1_0 is false, set ~hskp9 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp49 | ndr1_0 is false, set ~hskp49 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp8 | ndr1_0 is false, set ~hskp8 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp35 | ndr1_0 is false, set ~hskp35 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp7 | ndr1_0 is false, set ~hskp7 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp6 | ndr1_0 is false, set ~hskp6 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp5 | ndr1_0 is false, set ~hskp5 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp4 | ndr1_0 is false, set ~hskp4 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp33 | ndr1_0 is false, set ~hskp33 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp32 | ndr1_0 is false, set ~hskp32 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp47 | ndr1_0 is false, set ~hskp47 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp31 | ndr1_0 is false, set ~hskp31 to true
% 0.19/0.28 % SZS output end Definitions and Model Updates.
% 0.19/0.28 % (459402)------------------------------
% 0.19/0.28 % (459402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.28 % (459402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.28 % (459402)CaDiCaL version: 2.1.3
% 0.19/0.28 % (459402)Termination reason: Satisfiable
% 0.19/0.28 % (459402)Time elapsed: 0.010 s
% 0.19/0.28 % (459402)Peak memory usage: 12 MB
% 0.19/0.28 % (459402)Instructions burned: 31 (million)
% 0.19/0.28 % (459393)Success in time 0.042 s
% 0.19/0.28 % Vampire exiting
%------------------------------------------------------------------------------