%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN453-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 : n009.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:54 PM UTC 2026
% Result : Satisfiable 0.19s 0.26s
% Output : Saturation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u347,negated_conjecture,
( ~ c0_1(X2)
| c1_1(X2)
| ~ c3_1(X2) ) ).
cnf(u350,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1) ) ).
cnf(u353,negated_conjecture,
ndr1_0 ).
cnf(u367,negated_conjecture,
( ~ c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ) ).
cnf(u374,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1) ) ).
cnf(u381,negated_conjecture,
( c1_1(X2)
| c2_1(X2)
| c3_1(X2) ) ).
cnf(u389,negated_conjecture,
hskp0 ).
cnf(u396,negated_conjecture,
~ hskp30 ).
cnf(u405,negated_conjecture,
hskp24 ).
cnf(u412,negated_conjecture,
~ hskp56 ).
cnf(u420,negated_conjecture,
~ hskp42 ).
cnf(u434,negated_conjecture,
hskp10 ).
cnf(u439,negated_conjecture,
hskp20 ).
cnf(u447,negated_conjecture,
hskp28 ).
cnf(u452,negated_conjecture,
hskp27 ).
cnf(u462,negated_conjecture,
~ hskp54 ).
cnf(u471,negated_conjecture,
hskp9 ).
cnf(u479,negated_conjecture,
hskp6 ).
cnf(u484,negated_conjecture,
hskp39 ).
cnf(u488,negated_conjecture,
~ hskp38 ).
cnf(u494,negated_conjecture,
hskp2 ).
cnf(u502,negated_conjecture,
hskp33 ).
cnf(u509,negated_conjecture,
~ hskp66 ).
cnf(u513,negated_conjecture,
( c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ).
cnf(u518,negated_conjecture,
hskp47 ).
cnf(u523,negated_conjecture,
hskp43 ).
cnf(u527,negated_conjecture,
~ hskp11 ).
cnf(u531,negated_conjecture,
( ~ c3_1(X1)
| c0_1(X1)
| c2_1(X1) ) ).
cnf(u538,negated_conjecture,
~ hskp3 ).
cnf(u542,negated_conjecture,
( c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ).
cnf(u548,negated_conjecture,
hskp14 ).
cnf(u552,negated_conjecture,
~ hskp7 ).
cnf(u557,negated_conjecture,
~ hskp8 ).
cnf(u562,negated_conjecture,
~ hskp32 ).
cnf(u570,negated_conjecture,
~ hskp48 ).
cnf(u576,negated_conjecture,
hskp67 ).
cnf(u580,negated_conjecture,
~ hskp59 ).
cnf(u585,negated_conjecture,
~ hskp22 ).
cnf(u590,negated_conjecture,
hskp21 ).
cnf(u595,negated_conjecture,
~ hskp46 ).
cnf(u600,negated_conjecture,
hskp5 ).
cnf(u604,negated_conjecture,
~ hskp12 ).
cnf(u608,negated_conjecture,
~ hskp44 ).
cnf(u613,negated_conjecture,
~ hskp1 ).
cnf(u618,negated_conjecture,
hskp36 ).
cnf(u623,negated_conjecture,
hskp29 ).
cnf(u626,negated_conjecture,
~ hskp70 ).
cnf(u632,negated_conjecture,
hskp65 ).
cnf(u635,negated_conjecture,
~ hskp25 ).
cnf(u641,negated_conjecture,
hskp63 ).
cnf(u644,negated_conjecture,
~ hskp62 ).
cnf(u652,negated_conjecture,
~ hskp61 ).
cnf(u657,negated_conjecture,
hskp60 ).
cnf(u661,negated_conjecture,
~ hskp52 ).
cnf(u665,negated_conjecture,
~ hskp16 ).
cnf(u669,negated_conjecture,
( ~ c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) ).
cnf(u674,negated_conjecture,
hskp15 ).
cnf(u677,negated_conjecture,
~ hskp51 ).
cnf(u682,negated_conjecture,
~ hskp40 ).
cnf(u688,negated_conjecture,
hskp37 ).
cnf(u691,negated_conjecture,
~ hskp4 ).
cnf(u696,negated_conjecture,
~ hskp35 ).
cnf(u701,negated_conjecture,
hskp34 ).
cnf(u705,negated_conjecture,
~ hskp31 ).
cnf(u710,negated_conjecture,
~ hskp64 ).
cnf(u718,negated_conjecture,
~ hskp41 ).
cnf(u724,negated_conjecture,
~ c3_1(a1994) ).
cnf(u729,negated_conjecture,
~ c1_1(a1994) ).
cnf(u733,negated_conjecture,
c1_1(a1998) ).
cnf(u739,negated_conjecture,
~ c3_1(a1999) ).
cnf(u744,negated_conjecture,
~ c2_1(a1999) ).
cnf(u758,negated_conjecture,
c1_1(a2001) ).
cnf(u764,negated_conjecture,
~ c2_1(a2001) ).
cnf(u769,negated_conjecture,
~ c3_1(a2001) ).
cnf(u774,negated_conjecture,
~ c0_1(a2006) ).
cnf(u779,negated_conjecture,
~ c1_1(a2006) ).
cnf(u784,negated_conjecture,
~ c1_1(a2009) ).
cnf(u789,negated_conjecture,
~ c0_1(a2009) ).
cnf(u794,negated_conjecture,
~ c2_1(a2011) ).
cnf(u799,negated_conjecture,
~ c3_1(a2011) ).
cnf(u819,negated_conjecture,
~ c0_1(a2014) ).
cnf(u824,negated_conjecture,
~ c2_1(a2014) ).
cnf(u829,negated_conjecture,
~ c3_1(a2014) ).
cnf(u834,negated_conjecture,
~ c0_1(a2015) ).
cnf(u839,negated_conjecture,
~ c1_1(a2016) ).
cnf(u858,negated_conjecture,
hskp13 ).
cnf(u863,negated_conjecture,
~ c2_1(a2020) ).
cnf(u868,negated_conjecture,
~ c3_1(a2020) ).
cnf(u873,negated_conjecture,
~ c3_1(a2023) ).
cnf(u878,negated_conjecture,
~ c0_1(a2031) ).
cnf(u883,negated_conjecture,
~ c3_1(a2031) ).
cnf(u888,negated_conjecture,
~ c2_1(a2031) ).
cnf(u892,negated_conjecture,
c2_1(a2032) ).
cnf(u897,negated_conjecture,
c1_1(a2032) ).
cnf(u903,negated_conjecture,
~ hskp17 ).
cnf(u907,negated_conjecture,
~ c0_1(a2034) ).
cnf(u911,negated_conjecture,
c1_1(a2034) ).
cnf(u917,negated_conjecture,
~ c2_1(a2034) ).
cnf(u922,negated_conjecture,
~ hskp18 ).
cnf(u926,negated_conjecture,
~ c1_1(a2036) ).
cnf(u931,negated_conjecture,
~ hskp19 ).
cnf(u934,negated_conjecture,
c3_1(a2038) ).
cnf(u940,negated_conjecture,
~ c0_1(a2041) ).
cnf(u945,negated_conjecture,
~ c0_1(a2044) ).
cnf(u950,negated_conjecture,
~ c1_1(a2044) ).
cnf(u964,negated_conjecture,
hskp23 ).
cnf(u969,negated_conjecture,
~ c3_1(a2050) ).
cnf(u974,negated_conjecture,
~ c0_1(a2050) ).
cnf(u979,negated_conjecture,
~ c2_1(a2050) ).
cnf(u984,negated_conjecture,
~ c0_1(a2057) ).
cnf(u989,negated_conjecture,
~ c3_1(a2057) ).
cnf(u994,negated_conjecture,
~ c2_1(a2062) ).
cnf(u998,negated_conjecture,
c1_1(a2062) ).
cnf(u1004,negated_conjecture,
~ c3_1(a2062) ).
cnf(u1009,negated_conjecture,
~ hskp26 ).
cnf(u1018,negated_conjecture,
~ c2_1(a2068) ).
cnf(u1023,negated_conjecture,
~ c0_1(a2069) ).
cnf(u1028,negated_conjecture,
~ c1_1(a2079) ).
cnf(u1032,negated_conjecture,
c2_1(a2080) ).
cnf(u1037,negated_conjecture,
c0_1(a2080) ).
cnf(u1042,negated_conjecture,
c1_1(a2080) ).
cnf(u1047,negated_conjecture,
c2_1(a2081) ).
cnf(u1052,negated_conjecture,
c3_1(a2081) ).
cnf(u1057,negated_conjecture,
c1_1(a2081) ).
cnf(u1062,negated_conjecture,
c1_1(a2083) ).
cnf(u1068,negated_conjecture,
~ c3_1(a2083) ).
cnf(u1073,negated_conjecture,
~ c2_1(a2083) ).
cnf(u1078,negated_conjecture,
~ c3_1(a1995) ).
cnf(u1083,negated_conjecture,
~ c3_1(a1997) ).
cnf(u1088,negated_conjecture,
~ c2_1(a1997) ).
cnf(u1093,negated_conjecture,
~ c0_1(a2002) ).
cnf(u1123,negated_conjecture,
~ c0_1(a2017) ).
cnf(u1128,negated_conjecture,
~ c1_1(a2017) ).
cnf(u1138,negated_conjecture,
~ hskp45 ).
cnf(u1152,negated_conjecture,
~ c3_1(a2026) ).
cnf(u1157,negated_conjecture,
~ hskp49 ).
cnf(u1160,negated_conjecture,
c1_1(a2028) ).
cnf(u1165,negated_conjecture,
hskp50 ).
cnf(u1170,negated_conjecture,
~ c3_1(a2029) ).
cnf(u1179,negated_conjecture,
c1_1(a2033) ).
cnf(u1185,negated_conjecture,
~ c3_1(a2033) ).
cnf(u1189,negated_conjecture,
hskp53 ).
cnf(u1194,negated_conjecture,
~ c0_1(a2035) ).
cnf(u1203,negated_conjecture,
c2_1(a2047) ).
cnf(u1209,negated_conjecture,
~ hskp57 ).
cnf(u1212,negated_conjecture,
c1_1(a2048) ).
cnf(u1218,negated_conjecture,
~ c3_1(a2048) ).
cnf(u1223,negated_conjecture,
~ hskp58 ).
cnf(u1226,negated_conjecture,
c1_1(a2051) ).
cnf(u1231,negated_conjecture,
c2_1(a2051) ).
cnf(u1236,negated_conjecture,
c1_1(a2052) ).
cnf(u1242,negated_conjecture,
~ c2_1(a2053) ).
cnf(u1252,negated_conjecture,
~ c3_1(a2059) ).
cnf(u1262,negated_conjecture,
~ c3_1(a2063) ).
cnf(u1267,negated_conjecture,
~ c0_1(a2070) ).
cnf(u1272,negated_conjecture,
~ c1_1(a2070) ).
cnf(u1277,negated_conjecture,
~ hskp68 ).
cnf(u1286,negated_conjecture,
~ hskp69 ).
cnf(u1300,negated_conjecture,
c0_1(a1994) ).
cnf(u1304,negated_conjecture,
~ c3_1(a1998) ).
cnf(u1310,negated_conjecture,
c0_1(a1998) ).
cnf(u1315,negated_conjecture,
c1_1(a1999) ).
cnf(u1325,negated_conjecture,
c2_1(a2006) ).
cnf(u1330,negated_conjecture,
c3_1(a2009) ).
cnf(u1334,negated_conjecture,
~ c0_1(a2011) ).
cnf(u1340,negated_conjecture,
c1_1(a2015) ).
cnf(u1345,negated_conjecture,
c3_1(a2015) ).
cnf(u1350,negated_conjecture,
c2_1(a2016) ).
cnf(u1354,negated_conjecture,
~ c0_1(a2016) ).
cnf(u1360,negated_conjecture,
c1_1(a2020) ).
cnf(u1365,negated_conjecture,
c0_1(a2023) ).
cnf(u1370,negated_conjecture,
c2_1(a2023) ).
cnf(u1375,negated_conjecture,
c0_1(a2032) ).
cnf(u1379,negated_conjecture,
~ c0_1(a2036) ).
cnf(u1385,negated_conjecture,
c3_1(a2036) ).
cnf(u1389,negated_conjecture,
~ c0_1(a2038) ).
cnf(u1395,negated_conjecture,
c1_1(a2038) ).
cnf(u1400,negated_conjecture,
c3_1(a2041) ).
cnf(u1405,negated_conjecture,
c1_1(a2041) ).
cnf(u1410,negated_conjecture,
c3_1(a2044) ).
cnf(u1420,negated_conjecture,
c2_1(a2057) ).
cnf(u1435,negated_conjecture,
c1_1(a2068) ).
cnf(u1440,negated_conjecture,
c0_1(a2068) ).
cnf(u1445,negated_conjecture,
c2_1(a2069) ).
cnf(u1450,negated_conjecture,
c1_1(a2069) ).
cnf(u1455,negated_conjecture,
c2_1(a2079) ).
cnf(u1460,negated_conjecture,
c3_1(a2079) ).
cnf(u1465,negated_conjecture,
c0_1(a1993) ).
cnf(u1470,negated_conjecture,
c1_1(a1993) ).
cnf(u1475,negated_conjecture,
c2_1(a1993) ).
cnf(u1480,negated_conjecture,
c1_1(a1995) ).
cnf(u1485,negated_conjecture,
c0_1(a1995) ).
cnf(u1489,negated_conjecture,
~ c0_1(a1996) ).
cnf(u1495,negated_conjecture,
c3_1(a1996) ).
cnf(u1500,negated_conjecture,
c2_1(a1996) ).
cnf(u1505,negated_conjecture,
c1_1(a1997) ).
cnf(u1510,negated_conjecture,
c1_1(a2002) ).
cnf(u1515,negated_conjecture,
c3_1(a2002) ).
cnf(u1525,negated_conjecture,
c1_1(a2004) ).
cnf(u1530,negated_conjecture,
c2_1(a2004) ).
cnf(u1535,negated_conjecture,
c0_1(a2004) ).
cnf(u1570,negated_conjecture,
c2_1(a2017) ).
cnf(u1605,negated_conjecture,
c0_1(a2026) ).
cnf(u1610,negated_conjecture,
c2_1(a2026) ).
cnf(u1614,negated_conjecture,
~ c0_1(a2027) ).
cnf(u1620,negated_conjecture,
c3_1(a2027) ).
cnf(u1624,negated_conjecture,
~ c1_1(a2027) ).
cnf(u1629,negated_conjecture,
~ c3_1(a2028) ).
cnf(u1635,negated_conjecture,
c0_1(a2028) ).
cnf(u1640,negated_conjecture,
c2_1(a2029) ).
cnf(u1645,negated_conjecture,
c1_1(a2029) ).
cnf(u1660,negated_conjecture,
c2_1(a2033) ).
cnf(u1665,negated_conjecture,
c1_1(a2035) ).
cnf(u1670,negated_conjecture,
c2_1(a2035) ).
cnf(u1685,negated_conjecture,
c2_1(a2046) ).
cnf(u1688,negated_conjecture,
hskp55 ).
cnf(u1694,negated_conjecture,
c1_1(a2046) ).
cnf(u1699,negated_conjecture,
c0_1(a2046) ).
cnf(u1704,negated_conjecture,
c0_1(a2047) ).
cnf(u1708,negated_conjecture,
~ c3_1(a2047) ).
cnf(u1714,negated_conjecture,
c0_1(a2048) ).
cnf(u1718,negated_conjecture,
~ c3_1(a2051) ).
cnf(u1724,negated_conjecture,
c2_1(a2052) ).
cnf(u1729,negated_conjecture,
c0_1(a2052) ).
cnf(u1734,negated_conjecture,
c1_1(a2053) ).
cnf(u1739,negated_conjecture,
c0_1(a2053) ).
cnf(u1743,negated_conjecture,
~ c3_1(a2054) ).
cnf(u1749,negated_conjecture,
c2_1(a2054) ).
cnf(u1754,negated_conjecture,
c1_1(a2054) ).
cnf(u1769,negated_conjecture,
c1_1(a2059) ).
cnf(u1774,negated_conjecture,
c2_1(a2059) ).
cnf(u1789,negated_conjecture,
c1_1(a2063) ).
cnf(u1794,negated_conjecture,
c0_1(a2063) ).
cnf(u1799,negated_conjecture,
c2_1(a2067) ).
cnf(u1803,negated_conjecture,
~ c3_1(a2067) ).
cnf(u1809,negated_conjecture,
c0_1(a2067) ).
cnf(u1814,negated_conjecture,
c3_1(a2070) ).
cnf(u1833,negated_conjecture,
~ c3_1(a2078) ).
cnf(u1839,negated_conjecture,
c0_1(a2078) ).
cnf(u1844,negated_conjecture,
c2_1(a2078) ).
cnf(u3300,negated_conjecture,
c2_1(a2002) ).
cnf(u1878,negated_conjecture,
( ~ c3_1(X1)
| ~ c0_1(X1) ) ).
cnf(u2790,negated_conjecture,
c1_1(a2011) ).
cnf(u2151,negated_conjecture,
c2_1(a2070) ).
cnf(u2026,negated_conjecture,
c2_1(a2009) ).
cnf(u1972,negated_conjecture,
( c2_1(X1)
| c1_1(X1) ) ).
cnf(u3306,negated_conjecture,
c2_1(a2036) ).
cnf(u2025,negated_conjecture,
c2_1(a2015) ).
cnf(u2024,negated_conjecture,
c2_1(a2044) ).
cnf(u2796,negated_conjecture,
c1_1(a2014) ).
cnf(u2160,negated_conjecture,
c1_1(a2050) ).
cnf(u2630,negated_conjecture,
~ c0_1(a2081) ).
cnf(u1882,negated_conjecture,
( ~ c3_1(X1)
| c2_1(X1) ) ).
cnf(u3305,negated_conjecture,
c2_1(a2038) ).
cnf(u3324,negated_conjecture,
c1_1(a2031) ).
cnf(u2022,negated_conjecture,
c2_1(a2027) ).
cnf(u3412,negated_conjecture,
c1_1(a2057) ).
cnf(u2045,negated_conjecture,
c2_1(a2041) ).
cnf(u1959,negated_conjecture,
~ c0_1(a2079) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN453-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n009.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 16:05:15 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 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.19/0.26 % (3187872)Will run a generic schedule for satisfiability detection.
% 0.19/0.26 % (3187881)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1611330628:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.26 % (3187878)% WARNING: option uhcvi not known.
% 0.19/0.26 % (3187877)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3160175712_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.26 % (3187879)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3619810542:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.26 % (3187878)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2497385051:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.26 % (3187880)dis+10_1_sil=32000:sp=arity:random_seed=1746154677:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.26 % (3187882)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=544708671:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.26 % (3187883)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=845365514:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.26 % Detected minimum model sizes of [1]
% 0.19/0.26 % Detected maximum model sizes of [71]
% 0.19/0.26 % TRYING [1]
% 0.19/0.26 % TRYING [2]
% 0.19/0.26 % (3187881) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3187872-3187881"...
% 0.19/0.26 % (3187881)...printing done.
% 0.19/0.26 % SZS status Satisfiable for theBenchmark
% 0.19/0.26 % 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 ~hskp10 | ndr1_0 is false, set ~hskp10 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp2 | ndr1_0 is false, set ~hskp2 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 ~hskp43 | ndr1_0 is false, set ~hskp43 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 ~hskp37 | ndr1_0 is false, set ~hskp37 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 ~hskp54 | ndr1_0 is false, set ~hskp54 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 ~hskp51 | ndr1_0 is false, set ~hskp51 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 ~hskp67 | ndr1_0 is false, set ~hskp67 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 ~hskp14 | ndr1_0 is false, set ~hskp14 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp66 | ndr1_0 is false, set ~hskp66 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 ~hskp11 | ndr1_0 is false, set ~hskp11 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 ~hskp46 | ndr1_0 is false, set ~hskp46 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 ~hskp65 | ndr1_0 is false, set ~hskp65 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 ~hskp64 | ndr1_0 is false, set ~hskp64 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 ~hskp4 | ndr1_0 is false, set ~hskp4 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp3 | ndr1_0 is false, set ~hskp3 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp1 | ndr1_0 is false, set ~hskp1 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 ~hskp62 | ndr1_0 is false, set ~hskp62 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 ~hskp63 | ndr1_0 is false, set ~hskp63 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 ~hskp61 | ndr1_0 is false, set ~hskp61 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp60 | ndr1_0 is false, set ~hskp60 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 ~hskp35 | ndr1_0 is false, set ~hskp35 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 ~hskp32 | ndr1_0 is false, set ~hskp32 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.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 ~hskp28 | ndr1_0 is false, set ~hskp28 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 ~hskp25 | ndr1_0 is false, set ~hskp25 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp24 | ndr1_0 is false, set ~hskp24 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 ~hskp52 | ndr1_0 is false, set ~hskp52 to true
% 0.19/0.27 for all groundings,
% 0.19/0.27 whenever ~hskp70 | ndr1_0 is false, set ~hskp70 to true
% 0.19/0.27 % SZS output end Definitions and Model Updates.
% 0.19/0.27 % (3187881)------------------------------
% 0.19/0.27 % (3187881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.27 % (3187881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.27 % (3187881)CaDiCaL version: 2.1.3
% 0.19/0.27 % (3187881)Termination reason: Satisfiable
% 0.19/0.27 % (3187881)Time elapsed: 0.017 s
% 0.19/0.27 % (3187881)Peak memory usage: 13 MB
% 0.19/0.27 % (3187881)Instructions burned: 50 (million)
% 0.19/0.27 % (3187872)Success in time 0.043 s
% 0.19/0.27 % Vampire exiting
%------------------------------------------------------------------------------