%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN518+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:47 PM UTC 2026
% Result : CounterSatisfiable 7.44s 1.87s
% Output : Saturation 7.44s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u933,negated_conjecture,
~ c3_0 ).
cnf(u829,negated_conjecture,
ndr1_0 ).
cnf(u778,negated_conjecture,
( ~ c3_1(X150)
| c4_2(X150,X151)
| ~ c1_1(X150)
| ~ ndr1_1(X150)
| ~ c2_2(X150,X151) ) ).
cnf(u786,negated_conjecture,
c1_0 ).
cnf(u2302,negated_conjecture,
~ sP0 ).
cnf(u814,negated_conjecture,
~ c1_2(a1151,a1152) ).
cnf(u818,negated_conjecture,
ndr1_1(a1151) ).
cnf(u822,negated_conjecture,
c5_1(a1151) ).
cnf(u827,negated_conjecture,
( ~ c1_2(a1151,X147)
| ~ c2_2(a1151,X147)
| c5_2(a1151,X147) ) ).
cnf(u833,negated_conjecture,
c5_1(a1149) ).
cnf(u2328,negated_conjecture,
~ sP1 ).
cnf(u840,negated_conjecture,
c3_2(a1149,a1150) ).
cnf(u844,negated_conjecture,
c4_2(a1149,a1150) ).
cnf(u848,negated_conjecture,
ndr1_1(a1149) ).
cnf(u852,negated_conjecture,
~ c3_1(a1149) ).
cnf(u857,negated_conjecture,
~ c5_0 ).
cnf(u881,negated_conjecture,
~ c2_0 ).
cnf(u2355,negated_conjecture,
~ sP2 ).
cnf(u889,negated_conjecture,
~ c4_0 ).
cnf(u893,negated_conjecture,
~ c5_1(a1141) ).
cnf(u897,negated_conjecture,
c1_2(a1141,a1143) ).
cnf(u901,negated_conjecture,
~ c3_2(a1141,a1143) ).
cnf(u905,negated_conjecture,
c4_2(a1141,a1143) ).
cnf(u909,negated_conjecture,
ndr1_1(a1141) ).
cnf(u913,negated_conjecture,
~ c2_2(a1141,a1142) ).
cnf(u917,negated_conjecture,
c1_2(a1141,a1142) ).
cnf(u949,negated_conjecture,
( ~ c3_1(X139)
| ~ ndr1_1(X139)
| c4_2(X139,X140)
| c5_2(X139,X140)
| ~ c3_2(X139,X140)
| c2_2(X139,a1138) ) ).
cnf(u956,negated_conjecture,
( ~ c3_2(X139,a1138)
| ~ ndr1_1(X139)
| c4_2(X139,X140)
| c5_2(X139,X140)
| ~ c3_2(X139,X140)
| ~ c3_1(X139) ) ).
cnf(u1001,negated_conjecture,
( ~ c5_2(X129,X130)
| ~ ndr1_1(X129)
| ~ c3_2(X129,X130)
| c1_2(X129,X130) ) ).
cnf(u1006,negated_conjecture,
( ~ c5_2(X131,a1134)
| ~ ndr1_1(X131)
| c1_2(X131,X132)
| c5_2(X131,X132)
| c1_1(X131) ) ).
cnf(u1052,negated_conjecture,
( ~ c4_1(X123)
| c5_1(X123)
| ~ c1_1(X123) ) ).
cnf(u1067,negated_conjecture,
~ ndr1_1(a1129) ).
cnf(u1073,negated_conjecture,
sP3 ).
cnf(u1081,negated_conjecture,
~ c2_1(a1129) ).
cnf(u1111,negated_conjecture,
( ~ c4_1(X113)
| ~ c2_2(X113,X115)
| c1_2(X113,X115)
| ~ ndr1_1(X113)
| ~ c1_2(X113,X114)
| ~ c2_2(X113,X114) ) ).
cnf(u1146,negated_conjecture,
~ c4_1(a1121) ).
cnf(u1150,negated_conjecture,
~ c1_1(a1121) ).
cnf(u1154,negated_conjecture,
c3_1(a1121) ).
cnf(u1159,negated_conjecture,
( ~ c4_1(X111)
| ~ c3_2(X111,a1120)
| c3_1(X111) ) ).
cnf(u1163,negated_conjecture,
( ~ c4_1(X111)
| c4_2(X111,a1120)
| c3_1(X111) ) ).
cnf(u1167,negated_conjecture,
( ~ c4_1(X111)
| c5_2(X111,a1120)
| c3_1(X111) ) ).
cnf(u1171,negated_conjecture,
( ~ c4_1(X111)
| ndr1_1(X111)
| c3_1(X111) ) ).
cnf(u2422,negated_conjecture,
~ sP4 ).
cnf(u1226,negated_conjecture,
~ ndr1_1(a1113) ).
cnf(u1233,negated_conjecture,
c2_1(a1113) ).
cnf(u1237,negated_conjecture,
c1_1(a1113) ).
cnf(u1242,negated_conjecture,
c2_1(a1112) ).
cnf(u2449,negated_conjecture,
~ sP5 ).
cnf(u1249,negated_conjecture,
~ ndr1_1(a1112) ).
cnf(u2475,negated_conjecture,
~ sP6 ).
cnf(u1273,negated_conjecture,
( ~ c2_2(X102,X103)
| c4_2(X102,a1106)
| c3_1(X102)
| ~ ndr1_1(X102)
| c5_2(X102,X103)
| ~ c1_2(X102,X103) ) ).
cnf(u1277,negated_conjecture,
( ~ c3_2(X102,a1106)
| ~ c1_2(X102,X103)
| c3_1(X102)
| ~ ndr1_1(X102)
| c5_2(X102,X103)
| ~ c2_2(X102,X103) ) ).
cnf(u1281,negated_conjecture,
( ~ c2_2(X102,X103)
| c5_2(X102,a1106)
| c3_1(X102)
| ~ ndr1_1(X102)
| c5_2(X102,X103)
| ~ c1_2(X102,X103) ) ).
cnf(u1286,negated_conjecture,
~ c5_2(a1104,a1105) ).
cnf(u1290,negated_conjecture,
c3_2(a1104,a1105) ).
cnf(u1294,negated_conjecture,
ndr1_1(a1104) ).
cnf(u1298,negated_conjecture,
~ c2_1(a1104) ).
cnf(u1303,negated_conjecture,
( ~ c3_1(X100)
| ~ ndr1_1(X100)
| c1_2(X100,X101)
| ~ c5_2(X100,X101)
| c3_2(X100,X101)
| c1_1(X100) ) ).
cnf(u1307,negated_conjecture,
c5_1(a1103) ).
cnf(u1311,negated_conjecture,
~ ndr1_1(a1103) ).
cnf(u1347,negated_conjecture,
( ~ c3_2(X86,a1101)
| c3_1(X86)
| ~ c3_2(X86,X87)
| ~ ndr1_1(X86)
| ~ c2_2(X86,X87)
| c4_2(X86,X87) ) ).
cnf(u1351,negated_conjecture,
( ~ c1_2(X86,a1101)
| c3_1(X86)
| ~ c3_2(X86,X87)
| ~ ndr1_1(X86)
| ~ c2_2(X86,X87)
| c4_2(X86,X87) ) ).
cnf(u1355,negated_conjecture,
( ~ c5_2(X86,a1101)
| c3_1(X86)
| ~ c3_2(X86,X87)
| ~ ndr1_1(X86)
| ~ c2_2(X86,X87)
| c4_2(X86,X87) ) ).
cnf(u1385,negated_conjecture,
c3_2(a1097,a1098) ).
cnf(u1389,negated_conjecture,
c5_2(a1097,a1098) ).
cnf(u1393,negated_conjecture,
c1_2(a1097,a1098) ).
cnf(u1397,negated_conjecture,
ndr1_1(a1097) ).
cnf(u1401,negated_conjecture,
~ c5_1(a1097) ).
cnf(u1405,negated_conjecture,
~ c2_1(a1097) ).
cnf(u1418,negated_conjecture,
c2_2(a1094,a1095) ).
cnf(u2500,negated_conjecture,
~ sP7 ).
cnf(u2537,negated_conjecture,
~ sP8 ).
cnf(u1428,negated_conjecture,
~ c4_2(a1094,a1095) ).
cnf(u1432,negated_conjecture,
ndr1_1(a1094) ).
cnf(u1436,negated_conjecture,
~ c2_1(a1094) ).
cnf(u1441,negated_conjecture,
( ~ c4_2(a1094,X80)
| ~ c5_2(a1094,X80)
| c2_2(a1094,X80) ) ).
cnf(u2574,negated_conjecture,
~ sP9 ).
cnf(u2591,negated_conjecture,
~ sP10 ).
cnf(u1466,negated_conjecture,
c2_1(a1083) ).
cnf(u1470,negated_conjecture,
~ c1_1(a1083) ).
cnf(u1474,negated_conjecture,
~ ndr1_1(a1083) ).
cnf(u1499,negated_conjecture,
( ~ c4_2(X73,X74)
| c1_1(X73)
| ~ ndr1_1(X73)
| ~ c5_2(X73,X74)
| ~ c2_1(X73)
| ~ c1_2(X73,X74) ) ).
cnf(u1527,negated_conjecture,
~ c2_1(a1079) ).
cnf(u2622,negated_conjecture,
~ sP11 ).
cnf(u1534,negated_conjecture,
~ c1_1(a1079) ).
cnf(u1539,negated_conjecture,
~ c1_2(a1075,a1076) ).
cnf(u1542,negated_conjecture,
sP12 ).
cnf(u1546,negated_conjecture,
~ c4_2(a1075,a1076) ).
cnf(u1550,negated_conjecture,
~ c2_2(a1075,a1076) ).
cnf(u1554,negated_conjecture,
ndr1_1(a1075) ).
cnf(u1588,negated_conjecture,
~ ndr1_1(a1070) ).
cnf(u1599,negated_conjecture,
~ c4_1(a1070) ).
cnf(u1618,negated_conjecture,
~ c4_1(a1067) ).
cnf(u1622,negated_conjecture,
~ c3_1(a1067) ).
cnf(u1626,negated_conjecture,
c3_2(a1067,a1068) ).
cnf(u1630,negated_conjecture,
c2_2(a1067,a1068) ).
cnf(u1634,negated_conjecture,
~ c1_2(a1067,a1068) ).
cnf(u1638,negated_conjecture,
ndr1_1(a1067) ).
cnf(u1678,negated_conjecture,
( ~ c4_1(X58)
| ~ c5_1(X58)
| ~ ndr1_1(X58)
| ~ c4_2(X58,X59)
| ~ c5_2(X58,X59)
| c2_2(X58,X59) ) ).
cnf(u1683,negated_conjecture,
~ c1_1(a1063) ).
cnf(u1687,negated_conjecture,
~ ndr1_1(a1063) ).
cnf(u2679,negated_conjecture,
~ sP13 ).
cnf(u1701,negated_conjecture,
sP14 ).
cnf(u1705,negated_conjecture,
~ c5_1(a1062) ).
cnf(u1709,negated_conjecture,
~ ndr1_1(a1062) ).
cnf(u2733,negated_conjecture,
~ sP15 ).
cnf(u1725,negated_conjecture,
~ ndr1_1(a1053) ).
cnf(u1732,negated_conjecture,
c4_1(a1053) ).
cnf(u1736,negated_conjecture,
c1_1(a1053) ).
cnf(u1741,negated_conjecture,
c1_2(a1051,a1052) ).
cnf(u1748,negated_conjecture,
c5_2(a1051,a1052) ).
cnf(u1752,negated_conjecture,
~ c4_2(a1051,a1052) ).
cnf(u1756,negated_conjecture,
ndr1_1(a1051) ).
cnf(u1761,negated_conjecture,
( ~ c2_2(a1051,X52)
| ~ c5_2(a1051,X52)
| c4_2(a1051,X52) ) ).
cnf(u1765,negated_conjecture,
~ c2_1(a1051) ).
cnf(u1770,negated_conjecture,
~ c2_1(a1050) ).
cnf(u1774,negated_conjecture,
~ ndr1_1(a1050) ).
cnf(u1782,negated_conjecture,
~ c3_1(a1049) ).
cnf(u1789,negated_conjecture,
( ~ c3_2(a1049,X49)
| ~ c2_2(a1049,X49)
| c1_2(a1049,X49) ) ).
cnf(u1793,negated_conjecture,
c5_1(a1049) ).
cnf(u1826,negated_conjecture,
~ c4_1(a1046) ).
cnf(u2764,negated_conjecture,
~ sP16 ).
cnf(u1833,negated_conjecture,
~ c5_1(a1046) ).
cnf(u1837,negated_conjecture,
c2_1(a1046) ).
cnf(u1842,negated_conjecture,
( ~ c1_1(X43)
| ~ c1_2(X43,X44)
| c5_1(X43)
| ~ ndr1_1(X43)
| ~ c2_2(X43,X44) ) ).
cnf(u1879,negated_conjecture,
( ~ c3_2(X40,a1038)
| ~ ndr1_1(X40)
| ~ c5_2(X40,X41)
| c2_2(X40,X41)
| ~ c3_2(X40,X41)
| ~ c1_1(X40) ) ).
cnf(u1886,negated_conjecture,
( ~ c2_2(X40,a1038)
| ~ ndr1_1(X40)
| ~ c5_2(X40,X41)
| c2_2(X40,X41)
| ~ c3_2(X40,X41)
| ~ c1_1(X40) ) ).
cnf(u1890,negated_conjecture,
( ~ c4_2(X40,a1038)
| ~ ndr1_1(X40)
| ~ c5_2(X40,X41)
| c2_2(X40,X41)
| ~ c3_2(X40,X41)
| ~ c1_1(X40) ) ).
cnf(u1912,negated_conjecture,
( ~ c2_2(X37,X38)
| ~ ndr1_1(X37)
| c1_2(X37,X38)
| c5_1(X37)
| ~ c3_2(X37,X38) ) ).
cnf(u1946,negated_conjecture,
( ~ c4_2(X32,a1034)
| ~ ndr1_1(X32)
| c2_2(X32,X33)
| ~ c3_2(X32,X33)
| ~ c4_2(X32,X33) ) ).
cnf(u1950,negated_conjecture,
( ~ c4_2(X32,X33)
| ~ ndr1_1(X32)
| c2_2(X32,X33)
| ~ c3_2(X32,X33)
| c1_2(X32,a1034) ) ).
cnf(u1954,negated_conjecture,
( ~ c5_2(X32,a1034)
| ~ ndr1_1(X32)
| c2_2(X32,X33)
| ~ c3_2(X32,X33)
| ~ c4_2(X32,X33) ) ).
cnf(u1962,negated_conjecture,
c3_1(a1033) ).
cnf(u2800,negated_conjecture,
~ sP17 ).
cnf(u1969,negated_conjecture,
~ c5_1(a1033) ).
cnf(u1973,negated_conjecture,
~ ndr1_1(a1033) ).
cnf(u2822,negated_conjecture,
~ sP18 ).
cnf(u2024,negated_conjecture,
~ ndr1_1(a1025) ).
cnf(u2847,negated_conjecture,
~ sP19 ).
cnf(u2873,negated_conjecture,
~ sP20 ).
cnf(u2179,negated_conjecture,
c2_1(a1009) ).
cnf(u2183,negated_conjecture,
~ ndr1_1(a1009) ).
cnf(u2213,negated_conjecture,
( ~ c4_2(X11,a1006)
| c5_1(X11)
| ~ c1_1(X11) ) ).
cnf(u2216,negated_conjecture,
c4_1(a1005) ).
cnf(u2909,negated_conjecture,
~ sP21 ).
cnf(u2223,negated_conjecture,
( ~ c3_2(X11,a1006)
| c5_1(X11)
| ~ c1_1(X11) ) ).
cnf(u2227,negated_conjecture,
( ~ c1_1(X11)
| ndr1_1(X11)
| c5_1(X11) ) ).
cnf(u3315,negated_conjecture,
c3_1(a1005) ).
cnf(u2237,negated_conjecture,
~ ndr1_1(a1005) ).
cnf(u2262,negated_conjecture,
~ c5_2(a1000,a1001) ).
cnf(u2266,negated_conjecture,
~ c4_2(a1000,a1001) ).
cnf(u2270,negated_conjecture,
c3_2(a1000,a1001) ).
cnf(u2274,negated_conjecture,
ndr1_1(a1000) ).
cnf(u2279,negated_conjecture,
( ~ c1_2(a1000,X5)
| c2_2(a1000,X5)
| c5_2(a1000,X5) ) ).
cnf(u2283,negated_conjecture,
~ c2_1(a1000) ).
cnf(u2292,negated_conjecture,
( ~ c1_1(X0)
| ~ ndr1_1(X0)
| c5_2(X0,X1)
| c2_2(X0,X1)
| c3_2(X0,X1)
| c1_2(X0,a999) ) ).
cnf(u2296,negated_conjecture,
( ~ c1_1(X0)
| ~ ndr1_1(X0)
| c5_2(X0,X1)
| c2_2(X0,X1)
| c3_2(X0,X1)
| c3_2(X0,a999) ) ).
cnf(u2300,negated_conjecture,
( ~ c2_2(X0,a999)
| ~ ndr1_1(X0)
| c5_2(X0,X1)
| c2_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_1(X0) ) ).
cnf(u2384,axiom,
( ~ c5_2(X0,a1127)
| c3_1(X0)
| c2_2(X0,a1128) ) ).
cnf(u2388,axiom,
( ~ c5_2(X0,a1128)
| c3_1(X0)
| ~ c5_2(X0,a1127) ) ).
cnf(u2392,axiom,
( ~ c4_2(X0,a1128)
| c3_1(X0)
| ~ c5_2(X0,a1127) ) ).
cnf(u2396,axiom,
( c1_2(X0,a1127)
| c3_1(X0)
| c2_2(X0,a1128) ) ).
cnf(u2400,axiom,
( ~ c5_2(X0,a1128)
| c3_1(X0)
| c1_2(X0,a1127) ) ).
cnf(u2404,axiom,
( ~ c4_2(X0,a1128)
| c3_1(X0)
| c1_2(X0,a1127) ) ).
cnf(u2408,axiom,
( ~ c4_2(X0,a1127)
| c3_1(X0)
| c2_2(X0,a1128) ) ).
cnf(u2412,axiom,
( ~ c4_2(X0,a1127)
| c3_1(X0)
| ~ c5_2(X0,a1128) ) ).
cnf(u2416,axiom,
( ~ c4_2(X0,a1128)
| c3_1(X0)
| ~ c4_2(X0,a1127) ) ).
cnf(u2420,axiom,
( c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u2651,axiom,
~ c4_2(a1072,a1074) ).
cnf(u2655,axiom,
~ c3_2(a1072,a1074) ).
cnf(u2659,axiom,
ndr1_1(a1072) ).
cnf(u2663,axiom,
c1_1(a1072) ).
cnf(u2667,axiom,
c4_2(a1072,a1073) ).
cnf(u2671,axiom,
~ c3_2(a1072,a1073) ).
cnf(u2675,axiom,
c2_2(a1072,a1073) ).
cnf(u2682,axiom,
c1_2(a1059,a1061) ).
cnf(u2686,axiom,
c3_2(a1059,a1061) ).
cnf(u2690,axiom,
ndr1_1(a1059) ).
cnf(u2695,axiom,
( ~ c5_2(a1059,X0)
| c1_2(a1059,X0)
| c3_2(a1059,X0) ) ).
cnf(u3395,axiom,
c1_2(a1059,a1060) ).
cnf(u2703,axiom,
c2_2(a1059,a1060) ).
cnf(u2707,axiom,
c5_2(a1059,a1060) ).
cnf(u2714,axiom,
c3_2(a1057,a1058) ).
cnf(u2718,axiom,
~ c4_2(a1057,a1058) ).
cnf(u2722,axiom,
ndr1_1(a1057) ).
cnf(u2726,axiom,
~ c5_1(a1057) ).
cnf(u2730,axiom,
~ c2_1(a1057) ).
cnf(u3010,negated_conjecture,
~ c3_2(a1094,a1095) ).
cnf(u3247,negated_conjecture,
~ c1_2(a1094,a1095) ).
cnf(u3031,negated_conjecture,
~ ndr1_1(a1121) ).
cnf(u3042,negated_conjecture,
~ c1_2(a1149,a1150) ).
cnf(u3053,negated_conjecture,
~ c5_2(a1141,a1143) ).
cnf(u3098,negated_conjecture,
c5_1(a1072) ).
cnf(u3108,negated_conjecture,
c3_2(a1072,a999) ).
cnf(u3118,negated_conjecture,
c1_2(a1072,a999) ).
cnf(u3156,negated_conjecture,
c1_2(a1149,a1034) ).
cnf(u3176,negated_conjecture,
~ c3_2(a1053,a1120) ).
cnf(u3180,negated_conjecture,
c4_2(a1053,a1120) ).
cnf(u3184,negated_conjecture,
c5_2(a1053,a1120) ).
cnf(u3194,negated_conjecture,
~ c1_1(a1005) ).
cnf(u3221,negated_conjecture,
~ c2_2(a1151,a1127) ).
cnf(u3234,negated_conjecture,
c2_2(a1000,a1128) ).
cnf(u3260,negated_conjecture,
~ c1_2(a1072,a1073) ).
cnf(u3287,negated_conjecture,
~ c3_2(a1000,a1128) ).
cnf(u3295,negated_conjecture,
~ c1_2(a1000,a1128) ).
cnf(u3331,negated_conjecture,
c5_1(a1113) ).
cnf(u3170,negated_conjecture,
c5_1(a1053) ).
cnf(u3018,negated_conjecture,
c5_1(a1067) ).
cnf(u2947,negated_conjecture,
( ~ c3_1(X100)
| ~ ndr1_1(X100)
| c1_2(X100,X101)
| ~ c5_2(X100,X101)
| c1_1(X100) ) ).
cnf(u2995,negated_conjecture,
ndr1_1(a1049) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN518+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n017.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:18:43 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 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
% 7.44/1.87 % (3680215)Detected formulas, will run a generic FOF schedule.
% 7.44/1.87 % (3680224)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3454864118:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.44/1.87 % (3680224)Instruction limit reached!
% 7.44/1.87 % (3680224)------------------------------
% 7.44/1.87 % (3680224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680224)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680224)Termination reason: Instruction limit
% 7.44/1.87 % (3680224)Termination phase: Saturation
% 7.44/1.87 % (3680224)Time elapsed: 0.036 s
% 7.44/1.87 % (3680224)Peak memory usage: 89 MB
% 7.44/1.87 % (3680224)Instructions burned: 120 (million)
% 7.44/1.87 % (3680225)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=351731966:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.44/1.87 % (3680223)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=988056848:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.44/1.87 % (3680222)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=743639183:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.44/1.87 % (3680220)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=2673514342:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.44/1.87 % (3680221)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2007876495:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.44/1.87 % (3680226)dis-21_1_sil=8000:lcm=predicate:random_seed=3850469831:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 7.44/1.87 % (3680225)Refutation not found, incomplete strategy
% 7.44/1.87 % (3680225)------------------------------
% 7.44/1.87 % (3680225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680225)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680225)Termination reason: Refutation not found, incomplete strategy
% 7.44/1.87 % (3680225)Time elapsed: 0.031 s
% 7.44/1.87 % (3680225)Peak memory usage: 90 MB
% 7.44/1.87 % (3680225)Instructions burned: 49 (million)
% 7.44/1.87 % (3680223)Instruction limit reached!
% 7.44/1.87 % (3680223)------------------------------
% 7.44/1.87 % (3680223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680223)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680223)Termination reason: Instruction limit
% 7.44/1.87 % (3680223)Termination phase: Saturation
% 7.44/1.87 % (3680223)Time elapsed: 0.065 s
% 7.44/1.87 % (3680223)Peak memory usage: 90 MB
% 7.44/1.87 % (3680223)Instructions burned: 110 (million)
% 7.44/1.87 % (3680226)Instruction limit reached!
% 7.44/1.87 % (3680226)------------------------------
% 7.44/1.87 % (3680226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680226)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680226)Termination reason: Instruction limit
% 7.44/1.87 % (3680226)Termination phase: Saturation
% 7.44/1.87 % (3680226)Time elapsed: 0.076 s
% 7.44/1.87 % (3680226)Peak memory usage: 91 MB
% 7.44/1.87 % (3680226)Instructions burned: 130 (million)
% 7.44/1.87 % (3680228)lrs+10_1_sil=8000:sp=occurrence:random_seed=2430427199:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 7.44/1.87 % (3680228)Instruction limit reached!
% 7.44/1.87 % (3680228)------------------------------
% 7.44/1.87 % (3680228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680228)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680228)Termination reason: Instruction limit
% 7.44/1.87 % (3680228)Termination phase: Saturation
% 7.44/1.87 % (3680228)Time elapsed: 0.083 s
% 7.44/1.87 % (3680228)Peak memory usage: 92 MB
% 7.44/1.87 % (3680228)Instructions burned: 285 (million)
% 7.44/1.87 % (3680235)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1270223876:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 7.44/1.87 % (3680236)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2080075492:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 7.44/1.87 % (3680235)Refutation not found, incomplete strategy
% 7.44/1.87 % (3680235)------------------------------
% 7.44/1.87 % (3680235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680235)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680235)Termination reason: Refutation not found, incomplete strategy
% 7.44/1.87 % (3680235)Time elapsed: 0.023 s
% 7.44/1.87 % (3680235)Peak memory usage: 90 MB
% 7.44/1.87 % (3680235)Instructions burned: 34 (million)
% 7.44/1.87 % (3680236)Refutation not found, incomplete strategy
% 7.44/1.87 % (3680236)------------------------------
% 7.44/1.87 % (3680236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680236)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680236)Termination reason: Refutation not found, incomplete strategy
% 7.44/1.87 % (3680236)Time elapsed: 0.030 s
% 7.44/1.87 % (3680236)Peak memory usage: 90 MB
% 7.44/1.87 % (3680236)Instructions burned: 47 (million)
% 7.44/1.87 % (3680225)------------------------------
% 7.44/1.87 % (3680225)------------------------------
% 7.44/1.87 % (3680238)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=764475661:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 7.44/1.87 % (3680238)Refutation not found, incomplete strategy
% 7.44/1.87 % (3680238)------------------------------
% 7.44/1.87 % (3680238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680238)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680238)Termination reason: Refutation not found, incomplete strategy
% 7.44/1.87 % (3680238)Time elapsed: 0.013 s
% 7.44/1.87 % (3680238)Peak memory usage: 90 MB
% 7.44/1.87 % (3680238)Instructions burned: 36 (million)
% 7.44/1.87 % (3680241)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2027196278:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 7.44/1.87 % (3680238)------------------------------
% 7.44/1.87 % (3680238)------------------------------
% 7.44/1.87 % (3680235)------------------------------
% 7.44/1.87 % (3680235)------------------------------
% 7.44/1.87 % (3680236)------------------------------
% 7.44/1.87 % (3680236)------------------------------
% 7.44/1.87 % (3680244)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1916719295:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 7.44/1.87 % (3680241)Instruction limit reached!
% 7.44/1.87 % (3680241)------------------------------
% 7.44/1.87 % (3680241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680241)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680241)Termination reason: Instruction limit
% 7.44/1.87 % (3680241)Termination phase: Saturation
% 7.44/1.87 % (3680241)Time elapsed: 0.163 s
% 7.44/1.87 % (3680241)Peak memory usage: 92 MB
% 7.44/1.87 % (3680241)Instructions burned: 294 (million)
% 7.44/1.87 % (3680245)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=699085292:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 7.44/1.87 % (3680246)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2290673710:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 7.44/1.87 % (3680245)Instruction limit reached!
% 7.44/1.87 % (3680245)------------------------------
% 7.44/1.87 % (3680245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680245)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680245)Termination reason: Instruction limit
% 7.44/1.87 % (3680245)Termination phase: Saturation
% 7.44/1.87 % (3680245)Time elapsed: 0.067 s
% 7.44/1.87 % (3680245)Peak memory usage: 91 MB
% 7.44/1.87 % (3680245)Instructions burned: 113 (million)
% 7.44/1.87 % (3680221)First to succeed.
% 7.44/1.87 % (3680221)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3680215"
% 7.44/1.87 % (3680246)Instruction limit reached!
% 7.44/1.87 % (3680246)------------------------------
% 7.44/1.87 % (3680246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680246)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680246)Termination reason: Instruction limit
% 7.44/1.87 % (3680246)Termination phase: Saturation
% 7.44/1.87 % (3680246)Time elapsed: 0.067 s
% 7.44/1.87 % (3680246)Peak memory usage: 90 MB
% 7.44/1.87 % (3680246)Instructions burned: 128 (million)
% 7.44/1.87 % (3680248)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2288830973:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 7.44/1.87 % (3680220)Also succeeded, but the first one will report.
% 7.44/1.87 % (3680248)Instruction limit reached!
% 7.44/1.87 % (3680248)------------------------------
% 7.44/1.87 % (3680248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.87 % (3680248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.87 % (3680248)CaDiCaL version: 2.1.3
% 7.44/1.87 % (3680248)Termination reason: Instruction limit
% 7.44/1.87 % (3680248)Termination phase: Saturation
% 7.44/1.87 % (3680248)Time elapsed: 0.059 s
% 7.44/1.87 % (3680248)Peak memory usage: 90 MB
% 7.44/1.87 % (3680248)Instructions burned: 115 (million)
% 7.44/1.87 % (3680251)lrs+10_1_sil=8000:sp=occurrence:random_seed=389546817:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 7.44/1.87 % (3680252)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3382595674:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 7.44/1.87 % (3680254)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3529965883:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 7.44/1.87 % SZS status CounterSatisfiable for theBenchmark
% 7.44/1.87 % SZS output start Saturation.
% See solution above
% 7.44/1.88 % SZS output start Definitions and Model Updates.
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ~c2_1(X0) | c5_2(X0,a1003) | ndr1_1(X0) | ~ndr1_0 | ~sP21 is false, set c5_2(X0,a1003) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c5_2(X0,a1087) | ndr1_1(X0) | ~c2_1(X0) | ~ndr1_0 | ~sP9 is false, set c5_2(X0,a1087) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ~c2_1(X0) | ~c1_2(X0,a1003) | ndr1_1(X0) | ~ndr1_0 | ~sP21 is false, set ~c1_2(X0,a1003) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ~c2_1(X0) | ndr1_1(X0) | c4_2(X0,a1004) | ~ndr1_0 | ~sP21 is false, set c4_2(X0,a1004) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ndr1_1(X0) | c2_2(X0,a1128) | c3_1(X0) | ~ndr1_0 | ~sP3 is false, set c2_2(X0,a1128) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ndr1_1(X0) | ~c4_2(X0,a1128) | c3_1(X0) | ~ndr1_0 | ~sP3 is false, set ~c4_2(X0,a1128) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ~c4_2(X0,a1127) | ndr1_1(X0) | c3_1(X0) | ~ndr1_0 | ~sP3 is false, set ~c4_2(X0,a1127) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c1_2(X0,a1127) | ndr1_1(X0) | c3_1(X0) | ~ndr1_0 | ~sP3 is false, set c1_2(X0,a1127) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c1_2(X0,a1087) | ndr1_1(X0) | ~c2_1(X0) | ~ndr1_0 | ~sP9 is false, set c1_2(X0,a1087) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ndr1_0 | ~c3_0 | c1_2(a1027,X28) | ~c4_2(a1027,X28) | ~ndr1_1(a1027) is false, set c1_2(a1027,X28) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ~c2_1(X0) | ndr1_1(X0) | c3_2(X0,a1004) | ~ndr1_0 | ~sP21 is false, set c3_2(X0,a1004) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c3_2(X0,a1087) | ndr1_1(X0) | ~c2_1(X0) | ~ndr1_0 | ~sP9 is false, set c3_2(X0,a1087) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ~c2_1(X0) | c3_2(X0,a1003) | ndr1_1(X0) | ~ndr1_0 | ~sP21 is false, set c3_2(X0,a1003) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ~c2_1(X0) | ndr1_1(X0) | ~c5_2(X0,a1004) | ~ndr1_0 | ~sP21 is false, set ~c5_2(X0,a1004) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ndr1_1(X0) | ~c5_2(X0,a1088) | ~c2_1(X0) | ~ndr1_0 | ~sP9 is false, set ~c5_2(X0,a1088) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ndr1_1(X0) | ~c5_2(X0,a1128) | c3_1(X0) | ~ndr1_0 | ~sP3 is false, set ~c5_2(X0,a1128) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ~c5_2(X0,a1127) | ndr1_1(X0) | c3_1(X0) | ~ndr1_0 | ~sP3 is false, set ~c5_2(X0,a1127) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ~c5_2(a1026,X27) | c2_2(a1026,X27) | ~c4_2(a1026,X27) | ~ndr1_1(a1026) | ~c3_0 | ndr1_0 is false, set ~c5_2(a1026,X27) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ndr1_1(X32) | ~c4_2(X32,X33) | ~c3_2(X32,X33) | c2_2(X32,X33) | ~ndr1_1(X32) | ~ndr1_0 | c2_0 is false, set ~c3_2(X32,X33) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ~c3_1(a1026) | ~c3_0 | ndr1_0 is false, set ~c3_1(a1026) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c4_2(X136,X137) | c1_2(X136,X137) | ~c5_2(X136,X137) | ~ndr1_1(X136) | ~c5_2(X136,X138) | c4_2(X136,X138) | ~ndr1_1(X136) | ndr1_1(X136) | ~ndr1_0 | ~c3_1(X139) | ndr1_1(X139) | ~c3_2(X139,X140) | c5_2(X139,X140) | c4_2(X139,X140) | ~ndr1_1(X139) | ~ndr1_0 | c2_0 is false, set ~c3_1(X139) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c4_2(X136,X137) | c1_2(X136,X137) | ~c5_2(X136,X137) | ~ndr1_1(X136) | ~c5_2(X136,X138) | c4_2(X136,X138) | ~ndr1_1(X136) | c1_2(X136,a1137) | ~ndr1_0 | ~c3_1(X139) | ndr1_1(X139) | ~c3_2(X139,X140) | c5_2(X139,X140) | c4_2(X139,X140) | ~ndr1_1(X139) | ~ndr1_0 | c2_0 is false, set ~c3_1(X139) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c4_2(X136,X137) | c1_2(X136,X137) | ~c5_2(X136,X137) | ~ndr1_1(X136) | ~c5_2(X136,X138) | c4_2(X136,X138) | ~ndr1_1(X136) | ndr1_1(X136) | ~ndr1_0 | ~c3_1(X139) | c2_2(X139,a1138) | ~c3_2(X139,X140) | c5_2(X139,X140) | c4_2(X139,X140) | ~ndr1_1(X139) | ~ndr1_0 | c2_0 is false, set ~c3_1(X139) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c4_2(X136,X137) | c1_2(X136,X137) | ~c5_2(X136,X137) | ~ndr1_1(X136) | ~c5_2(X136,X138) | c4_2(X136,X138) | ~ndr1_1(X136) | ~c2_2(X136,a1137) | ~ndr1_0 | ~c3_1(X139) | ndr1_1(X139) | ~c3_2(X139,X140) | c5_2(X139,X140) | c4_2(X139,X140) | ~ndr1_1(X139) | ~ndr1_0 | c2_0 is false, set ~c3_1(X139) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c4_2(X136,X137) | c1_2(X136,X137) | ~c5_2(X136,X137) | ~ndr1_1(X136) | ~c5_2(X136,X138) | c4_2(X136,X138) | ~ndr1_1(X136) | ndr1_1(X136) | ~ndr1_0 | ~c3_1(X139) | ~c3_2(X139,a1138) | ~c3_2(X139,X140) | c5_2(X139,X140) | c4_2(X139,X140) | ~ndr1_1(X139) | ~ndr1_0 | c2_0 is false, set ~c3_1(X139) to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ndr1_0 | ~c4_1(X113) | ~c2_2(X113,X114) | ~c1_2(X113,X114) | ~ndr1_1(X113) | c1_2(X113,X115) | ~c2_2(X113,X115) | ~ndr1_1(X113) | ~ndr1_0 | ~c1_0 is false, set ~c1_0 to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ~c2_0 | c3_1(X61) | ~c5_2(X61,X62) | ~c2_2(X61,X62) | ~c4_2(X61,X62) | ~ndr1_1(X61) | c4_2(X61,X63) | c5_2(X61,X63) | ~ndr1_1(X61) | ~ndr1_0 | ndr1_0 is false, set ~c2_0 to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever ndr1_0 | ~c2_0 | ~c4_1(X64) | c2_1(X64) | ~ndr1_0 is false, set ~c2_0 to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c1_1(X51) | ~c3_1(X51) | ~ndr1_0 | c5_0 | ndr1_0 is false, set c5_0 to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c5_0 | c1_2(X129,X130) | ~c5_2(X129,X130) | ~c3_2(X129,X130) | ~ndr1_1(X129) | ~ndr1_0 | ndr1_1(X131) | c1_1(X131) | c5_2(X131,X132) | c1_2(X131,X132) | ~ndr1_1(X131) | ~ndr1_0 is false, set c5_0 to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c1_1(X81) | ndr1_1(X81) | ~c2_2(X81,X82) | ~c3_2(X81,X82) | ~c1_2(X81,X82) | ~ndr1_1(X81) | ~ndr1_0 | ~c2_0 | c5_0 is false, set c5_0 to true
% 7.44/1.88 for all groundings,
% 7.44/1.88 whenever c2_0 | ~c3_2(X86,X87) | c4_2(X86,X87) | ~c2_2(X86,X87) | ~ndr1_1(X86) | ndr1_1(X86) | c3_1(X86) | ~ndr1_0 | c3_0 is false, set c3_0 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c1_0 | c1_1(X127) | c1_2(X127,X128) | c2_2(X127,X128) | ~c3_2(X127,X128) | ~ndr1_1(X127) | ndr1_1(X127) | ~ndr1_0 | c3_0 is false, set c3_0 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c3_1(X45) | c2_2(X45,X46) | c1_2(X45,X46) | ~c4_2(X45,X46) | ~ndr1_1(X45) | ~c1_1(X45) | ~ndr1_0 | ~c4_0 | ndr1_0 is false, set ~c1_1(X45) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_0 | ~c1_1(X148) | ndr1_1(X148) | ~c2_2(X148,X149) | ~c5_2(X148,X149) | ~ndr1_1(X148) | ~ndr1_0 | c1_0 is false, set ~c1_1(X148) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c3_1(a1155) | ~c1_1(X148) | ndr1_1(X148) | ~c2_2(X148,X149) | ~c5_2(X148,X149) | ~ndr1_1(X148) | ~ndr1_0 | c1_0 is false, set ~c1_1(X148) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_0 | ~c1_1(X148) | ~c2_2(X148,a1156) | ~c2_2(X148,X149) | ~c5_2(X148,X149) | ~ndr1_1(X148) | ~ndr1_0 | c1_0 is false, set ~c1_1(X148) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c4_2(X150,X151) | ~c2_2(X150,X151) | ~ndr1_1(X150) | ~c1_1(X150) | ~c3_1(X150) | ~ndr1_0 | c3_0 | ndr1_0 is false, set ~c1_1(X150) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_0 | ~c1_1(X148) | c3_2(X148,a1156) | ~c2_2(X148,X149) | ~c5_2(X148,X149) | ~ndr1_1(X148) | ~ndr1_0 | c1_0 is false, set ~c1_1(X148) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_0 | ~c1_1(X148) | ~c1_2(X148,a1156) | ~c2_2(X148,X149) | ~c5_2(X148,X149) | ~ndr1_1(X148) | ~ndr1_0 | c1_0 is false, set ~c1_1(X148) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | ~c1_1(X0) | c3_2(X0,X1) | c2_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | c3_0 | c1_2(X2,X3) | ~c4_2(X2,X3) | ~ndr1_1(X2) | c1_2(X2,X4) | c2_2(X2,X4) | c5_2(X2,X4) | ~ndr1_1(X2) | c3_1(X2) | ~ndr1_0 is false, set ~c1_1(X0) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_0 | ~c3_0 | c4_1(a1027) is false, set c4_1(a1027) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_0 | c1_0 | c4_1(X36) | c2_1(X36) | ~ndr1_0 is false, set c4_1(X36) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_0 | c4_2(X67,X68) | ~c5_2(X67,X68) | ~ndr1_1(X67) | ~c5_1(X67) | c4_1(X67) | ~ndr1_0 is false, set c4_1(X67) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c2_0 | c4_1(X116) | ndr1_1(X116) | ~c3_1(X116) | ~ndr1_0 | ndr1_0 is false, set c4_1(X116) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c2_0 | c4_1(X116) | c4_2(X116,a1125) | ~c3_1(X116) | ~ndr1_0 | ndr1_0 is false, set c4_1(X116) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c2_0 | c4_1(X116) | c1_2(X116,a1125) | ~c3_1(X116) | ~ndr1_0 | ndr1_0 is false, set c4_1(X116) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c5_0 | ~c3_0 | c2_1(X141) | c4_2(X141,X142) | ~c5_2(X141,X142) | c2_2(X141,X142) | ~ndr1_1(X141) | ndr1_1(X141) | ~ndr1_0 is false, set ~c3_0 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c2_1(X84) | c3_2(X84,X85) | ~c5_2(X84,X85) | ~ndr1_1(X84) | ndr1_1(X84) | ~ndr1_0 | c4_0 | ~c3_0 is false, set ~c3_0 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c2_1(X39) | ~c1_2(X39,a1037) | c4_1(X39) | ~ndr1_0 | ~c1_0 | ~c1_1(X40) | ndr1_1(X40) | ~c3_2(X40,X41) | c2_2(X40,X41) | ~c5_2(X40,X41) | ~ndr1_1(X40) | ~ndr1_0 is false, set ~c2_1(X39) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c2_1(X39) | c5_2(X39,a1037) | c4_1(X39) | ~ndr1_0 | ~c1_0 | ~c1_1(X40) | ndr1_1(X40) | ~c3_2(X40,X41) | c2_2(X40,X41) | ~c5_2(X40,X41) | ~ndr1_1(X40) | ~ndr1_0 is false, set ~c2_1(X39) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c2_1(X39) | ndr1_1(X39) | c4_1(X39) | ~ndr1_0 | ~c1_0 | ~c1_1(X40) | ndr1_1(X40) | ~c3_2(X40,X41) | c2_2(X40,X41) | ~c5_2(X40,X41) | ~ndr1_1(X40) | ~ndr1_0 is false, set ~c2_1(X39) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c2_0 | ndr1_1(X21) | ~c3_1(X21) | c5_2(X21,X22) | c4_2(X21,X22) | ~ndr1_1(X21) | ~ndr1_0 | ~c2_1(X23) | ~c4_1(X23) | ~c4_2(X23,X24) | c2_2(X23,X24) | ~ndr1_1(X23) | ~ndr1_0 is false, set ~c2_1(X23) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c2_1(X39) | c3_2(X39,a1037) | c4_1(X39) | ~ndr1_0 | ~c1_0 | ~c1_1(X40) | ndr1_1(X40) | ~c3_2(X40,X41) | c2_2(X40,X41) | ~c5_2(X40,X41) | ~ndr1_1(X40) | ~ndr1_0 is false, set ~c2_1(X39) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_0 | c3_0 | ~c2_1(X73) | ~c1_2(X73,X74) | ~c4_2(X73,X74) | ~c5_2(X73,X74) | ~ndr1_1(X73) | c1_1(X73) | ~ndr1_0 is false, set ~c2_1(X73) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_0 | ~c3_0 | c5_1(a1027) is false, set c5_1(a1027) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c4_0 | ndr1_0 | ~c1_2(X43,X44) | ~c2_2(X43,X44) | ~ndr1_1(X43) | c5_1(X43) | ~c1_1(X43) | ~ndr1_0 is false, set c5_1(X43) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c1_2(X120,X121) | c2_2(X120,X121) | ~ndr1_1(X120) | c1_2(X120,X122) | c2_2(X120,X122) | ~c4_2(X120,X122) | ~ndr1_1(X120) | ndr1_1(X120) | ~ndr1_0 | c3_0 | ~c4_1(X123) | ~c1_1(X123) | c5_1(X123) | ~ndr1_0 is false, set c5_1(X123) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c3_0 | c3_1(X6) | c5_1(X6) | ~c2_2(X6,X7) | c5_2(X6,X7) | c3_2(X6,X7) | ~ndr1_1(X6) | ~ndr1_0 | ~c3_2(X8,X9) | ~c5_2(X8,X9) | c4_2(X8,X9) | ~ndr1_1(X8) | ndr1_1(X8) | ~ndr1_0 is false, set c5_1(X6) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c5_1(a1155) | ~c1_1(X148) | ndr1_1(X148) | ~c2_2(X148,X149) | ~c5_2(X148,X149) | ~ndr1_1(X148) | ~ndr1_0 | c1_0 is false, set c5_1(a1155) to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever sP3 | c5_0 | ndr1_0 is false, set sP3 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever sP21 | ndr1_0 | c5_1(X11) | ~c1_1(X11) | ~c4_2(X11,a1006) | ~ndr1_0 is false, set sP21 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever sP21 | ndr1_0 | c5_1(X11) | ~c1_1(X11) | ~c3_2(X11,a1006) | ~ndr1_0 is false, set sP21 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever sP21 | ndr1_0 | c5_1(X11) | ~c1_1(X11) | ndr1_1(X11) | ~ndr1_0 is false, set sP21 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever sP8 | sP7 | ndr1_0 is false, set sP7 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c1_2(X102,X103) | ~c2_2(X102,X103) | c5_2(X102,X103) | ~ndr1_1(X102) | c3_1(X102) | ndr1_1(X102) | ~ndr1_0 | c2_0 | sP6 is false, set sP6 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_0 | c1_0 | sP18 is false, set sP18 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever sP9 | ~c4_0 | ndr1_0 is false, set sP9 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c1_2(X0,a1092) | ~c5_2(X0,X1) | c2_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | ~c5_2(X0,X1) | c2_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | c2_2(X0,a1093) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | ~c5_2(X0,X1) | c2_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ~c4_2(X0,a1093) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | ~c5_2(X0,X1) | c2_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | c1_2(X0,a1093) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c2_2(X0,a1092) | ~c5_2(X0,X1) | c2_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c4_2(X0,a1092) | ~c5_2(X0,X1) | c2_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | ~c5_2(X0,X1) | c2_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | ndr1_1(X0) | ~c5_2(X0,X1) | ~c4_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | c5_2(X0,a1091) | ~c5_2(X0,X1) | ~c4_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c2_2(X0,a1090) | ndr1_1(X0) | ~c5_2(X0,X1) | ~c4_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | c4_2(X0,a1091) | ~c5_2(X0,X1) | ~c4_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | ~c2_2(X0,a1091) | ~c5_2(X0,X1) | ~c4_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c1_2(X0,a1090) | ndr1_1(X0) | ~c5_2(X0,X1) | ~c4_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c5_2(X0,a1090) | ndr1_1(X0) | ~c5_2(X0,X1) | ~c4_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | ~c5_2(X0,X1) | ~c1_2(X0,X1) | c2_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~sP6 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c4_2(X0,a1107) | ~c5_2(X0,X1) | ~c1_2(X0,X1) | c2_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~sP6 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | ~c5_2(X0,X1) | ~c1_2(X0,X1) | c2_2(X0,X1) | ~ndr1_1(X0) | c4_2(X0,a1108) | ~ndr1_0 | ~sP6 is false, set ~sP6 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c1_2(X0,a1107) | ~c5_2(X0,X1) | ~c1_2(X0,X1) | c2_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~sP6 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ndr1_1(X0) | ~c5_2(X0,X1) | ~c1_2(X0,X1) | c2_2(X0,X1) | ~ndr1_1(X0) | ~c5_2(X0,a1108) | ~ndr1_0 | ~sP6 is false, set ~sP6 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever ~c5_2(X0,a1107) | ~c5_2(X0,X1) | ~c1_2(X0,X1) | c2_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~sP6 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c2_2(X0,X1) | ~c3_2(X0,X1) | c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c4_2(X0,a1030) | ~ndr1_0 | ~sP18 is false, set ~sP18 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c2_2(X0,X1) | ~c3_2(X0,X1) | c1_2(X0,X1) | ~ndr1_1(X0) | c2_2(X0,a1029) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set ~sP18 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c2_2(X0,X1) | ~c3_2(X0,X1) | c1_2(X0,X1) | ~ndr1_1(X0) | c3_2(X0,a1029) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set ~sP18 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c2_2(X0,X1) | ~c3_2(X0,X1) | c1_2(X0,X1) | ~ndr1_1(X0) | ~c4_2(X0,a1029) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set ~sP18 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c2_2(X0,X1) | ~c3_2(X0,X1) | c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c5_2(X0,a1030) | ~ndr1_0 | ~sP18 is false, set ~sP18 to true
% 8.93/1.97 for all groundings,
% 8.93/1.97 whenever c2_2(X0,X1) | ~c3_2(X0,X1) | c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set ~sP18 to true
% 8.93/1.97 % SZS output end Definitions and Model Updates.
% 8.93/1.97 % (3680221)------------------------------
% 8.93/1.97 % (3680221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.93/1.97 % (3680221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.93/1.97 % (3680221)CaDiCaL version: 2.1.3
% 8.93/1.97 % (3680221)Termination reason: Satisfiable
% 8.93/1.97 % (3680221)Time elapsed: 0.747 s
% 8.93/1.97 % (3680221)Peak memory usage: 132 MB
% 8.93/1.97 % (3680221)Instructions burned: 1136 (million)
% 8.93/1.97 % (3680221)------------------------------
% 8.93/1.97 % (3680221)------------------------------
% 8.93/1.97 % (3680215)Success in time 1.201 s
% 8.93/1.97 % Vampire exiting
%------------------------------------------------------------------------------