%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN545+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 : n007.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 : CounterSatisfiable 5.84s 1.91s
% Output : Saturation 5.84s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u870,negated_conjecture,
ndr1_0 ).
cnf(u814,negated_conjecture,
( c4_1(X154)
| c5_1(X154)
| c3_1(X154) ) ).
cnf(u1221,negated_conjecture,
~ c6_0 ).
cnf(u4172,negated_conjecture,
~ c7_2(a294,a295) ).
cnf(u848,negated_conjecture,
c1_0 ).
cnf(u852,negated_conjecture,
~ c8_2(a294,a295) ).
cnf(u856,negated_conjecture,
~ c2_2(a294,a295) ).
cnf(u860,negated_conjecture,
ndr1_1(a294) ).
cnf(u868,negated_conjecture,
c2_1(a294) ).
cnf(u976,negated_conjecture,
c4_0 ).
cnf(u877,negated_conjecture,
( ~ c1_2(X152,a293)
| c4_1(X152)
| c8_2(X152,a292) ) ).
cnf(u880,negated_conjecture,
~ c2_0 ).
cnf(u884,negated_conjecture,
( ~ c3_2(X152,a293)
| c4_1(X152)
| c8_2(X152,a292) ) ).
cnf(u888,negated_conjecture,
( c8_2(X152,a292)
| c4_1(X152)
| c4_2(X152,a293) ) ).
cnf(u892,negated_conjecture,
( ~ c1_2(X152,a293)
| c4_1(X152)
| c7_2(X152,a292) ) ).
cnf(u896,negated_conjecture,
( ~ c3_2(X152,a293)
| c4_1(X152)
| c7_2(X152,a292) ) ).
cnf(u900,negated_conjecture,
( c4_2(X152,a293)
| c4_1(X152)
| c7_2(X152,a292) ) ).
cnf(u904,negated_conjecture,
( ~ c5_2(X152,a292)
| c4_1(X152)
| ~ c1_2(X152,a293) ) ).
cnf(u908,negated_conjecture,
( ~ c5_2(X152,a292)
| c4_1(X152)
| ~ c3_2(X152,a293) ) ).
cnf(u912,negated_conjecture,
( ~ c5_2(X152,a292)
| c4_1(X152)
| c4_2(X152,a293) ) ).
cnf(u2555,negated_conjecture,
~ sP0 ).
cnf(u943,negated_conjecture,
ndr1_1(a288) ).
cnf(u926,negated_conjecture,
( ~ c8_2(a288,X151)
| ~ c4_2(a288,X151)
| ~ c5_2(a288,X151) ) ).
cnf(u933,negated_conjecture,
~ c5_2(a288,a289) ).
cnf(u937,negated_conjecture,
~ c4_2(a288,a289) ).
cnf(u941,negated_conjecture,
~ c8_2(a288,a289) ).
cnf(u947,negated_conjecture,
~ c8_1(a288) ).
cnf(u951,negated_conjecture,
c8_1(a287) ).
cnf(u954,negated_conjecture,
c5_0 ).
cnf(u977,negated_conjecture,
~ c3_0 ).
cnf(u961,negated_conjecture,
~ c5_1(a287) ).
cnf(u965,negated_conjecture,
c3_1(a287) ).
cnf(u970,negated_conjecture,
c8_0 ).
cnf(u981,negated_conjecture,
( c6_1(X146)
| c1_1(X146)
| ~ c8_1(X146) ) ).
cnf(u2592,negated_conjecture,
~ sP2 ).
cnf(u1016,negated_conjecture,
c2_1(a279) ).
cnf(u1037,negated_conjecture,
ndr1_1(a279) ).
cnf(u1023,negated_conjecture,
( c6_2(a279,X144)
| c3_2(a279,X144)
| ~ c5_2(a279,X144) ) ).
cnf(u1027,negated_conjecture,
c8_2(a279,a280) ).
cnf(u1031,negated_conjecture,
~ c1_2(a279,a280) ).
cnf(u1035,negated_conjecture,
~ c4_2(a279,a280) ).
cnf(u1215,negated_conjecture,
~ c7_0 ).
cnf(u1057,negated_conjecture,
~ ndr1_1(a277) ).
cnf(u2619,negated_conjecture,
~ sP3 ).
cnf(u1079,negated_conjecture,
~ c7_1(a274) ).
cnf(u2646,negated_conjecture,
~ sP4 ).
cnf(u1086,negated_conjecture,
~ ndr1_1(a274) ).
cnf(u1097,negated_conjecture,
~ c7_1(a268) ).
cnf(u1101,negated_conjecture,
c1_2(a268,a270) ).
cnf(u1105,negated_conjecture,
c8_2(a268,a270) ).
cnf(u1109,negated_conjecture,
c6_2(a268,a270) ).
cnf(u3802,negated_conjecture,
~ ndr1_1(a268) ).
cnf(u1117,negated_conjecture,
c5_2(a268,a269) ).
cnf(u1121,negated_conjecture,
c2_2(a268,a269) ).
cnf(u1125,negated_conjecture,
~ c6_2(a268,a269) ).
cnf(u1131,negated_conjecture,
~ ndr1_1(a267) ).
cnf(u1166,negated_conjecture,
( ~ c7_1(X133)
| ~ c2_1(X133) ) ).
cnf(u1214,negated_conjecture,
( ~ c8_2(X129,X130)
| c2_1(X129)
| ~ c7_1(X129)
| ~ ndr1_1(X129)
| ~ c5_2(X129,X130)
| c3_2(X129,X130) ) ).
cnf(u1237,negated_conjecture,
( ~ c1_2(X123,a260)
| c1_2(X123,a261)
| ~ c7_2(X123,X124)
| ~ ndr1_1(X123)
| c1_2(X123,X124)
| c8_2(X123,X124) ) ).
cnf(u1241,negated_conjecture,
( ~ c1_2(X123,a260)
| c2_2(X123,a261)
| ~ c7_2(X123,X124)
| ~ ndr1_1(X123)
| c1_2(X123,X124)
| c8_2(X123,X124) ) ).
cnf(u1245,negated_conjecture,
( ~ c1_2(X123,a260)
| ~ c6_2(X123,a261)
| ~ c7_2(X123,X124)
| ~ ndr1_1(X123)
| c1_2(X123,X124)
| c8_2(X123,X124) ) ).
cnf(u1249,negated_conjecture,
( ~ c7_2(X123,X124)
| c1_2(X123,a261)
| ~ c2_2(X123,a260)
| ~ ndr1_1(X123)
| c1_2(X123,X124)
| c8_2(X123,X124) ) ).
cnf(u1253,negated_conjecture,
( ~ c7_2(X123,X124)
| c2_2(X123,a261)
| ~ c2_2(X123,a260)
| ~ ndr1_1(X123)
| c1_2(X123,X124)
| c8_2(X123,X124) ) ).
cnf(u1257,negated_conjecture,
( ~ c6_2(X123,a261)
| ~ c7_2(X123,X124)
| ~ c2_2(X123,a260)
| ~ ndr1_1(X123)
| c1_2(X123,X124)
| c8_2(X123,X124) ) ).
cnf(u1261,negated_conjecture,
( ~ c7_2(X123,a260)
| c1_2(X123,a261)
| ~ c7_2(X123,X124)
| ~ ndr1_1(X123)
| c1_2(X123,X124)
| c8_2(X123,X124) ) ).
cnf(u1265,negated_conjecture,
( ~ c7_2(X123,a260)
| c2_2(X123,a261)
| ~ c7_2(X123,X124)
| ~ ndr1_1(X123)
| c1_2(X123,X124)
| c8_2(X123,X124) ) ).
cnf(u1269,negated_conjecture,
( ~ c7_2(X123,a260)
| ~ c6_2(X123,a261)
| ~ c7_2(X123,X124)
| ~ ndr1_1(X123)
| c1_2(X123,X124)
| c8_2(X123,X124) ) ).
cnf(u1273,negated_conjecture,
~ c7_1(a259) ).
cnf(u1280,negated_conjecture,
c6_1(a259) ).
cnf(u1284,negated_conjecture,
~ ndr1_1(a259) ).
cnf(u1309,negated_conjecture,
( ~ c5_1(X120)
| c3_1(X120)
| c1_1(X120) ) ).
cnf(u2680,negated_conjecture,
~ sP5 ).
cnf(u1341,negated_conjecture,
~ ndr1_1(a253) ).
cnf(u1351,negated_conjecture,
~ c7_1(a253) ).
cnf(u1355,negated_conjecture,
~ c8_1(a253) ).
cnf(u1362,negated_conjecture,
~ ndr1_1(a252) ).
cnf(u1369,negated_conjecture,
~ c7_1(a252) ).
cnf(u1373,negated_conjecture,
c1_1(a252) ).
cnf(u1417,negated_conjecture,
~ ndr1_1(a249) ).
cnf(u1427,negated_conjecture,
~ c7_1(a249) ).
cnf(u1431,negated_conjecture,
~ c1_1(a249) ).
cnf(u1469,negated_conjecture,
( ~ ndr1_1(X104)
| c2_1(X104)
| ~ c8_2(X104,X105)
| ~ c6_2(X104,X105)
| ~ c3_2(X104,X105)
| c3_1(X104) ) ).
cnf(u2721,negated_conjecture,
~ sP6 ).
cnf(u2757,negated_conjecture,
~ sP7 ).
cnf(u1505,negated_conjecture,
~ c7_1(a237) ).
cnf(u1509,negated_conjecture,
~ c1_2(a237,a238) ).
cnf(u1513,negated_conjecture,
~ c7_2(a237,a238) ).
cnf(u1517,negated_conjecture,
c2_2(a237,a238) ).
cnf(u1521,negated_conjecture,
ndr1_1(a237) ).
cnf(u1525,negated_conjecture,
c1_1(a237) ).
cnf(u1529,negated_conjecture,
( ~ c4_2(X103,a236)
| ~ c8_1(X103)
| ~ c6_1(X103) ) ).
cnf(u1533,negated_conjecture,
( ~ c6_2(X103,a236)
| ~ c8_1(X103)
| ~ c6_1(X103) ) ).
cnf(u1537,negated_conjecture,
( c5_2(X103,a236)
| ~ c8_1(X103)
| ~ c6_1(X103) ) ).
cnf(u1551,negated_conjecture,
sP8 ).
cnf(u1564,negated_conjecture,
( c1_2(X100,X101)
| ~ ndr1_1(X100)
| ~ c4_2(X100,X101)
| ~ c1_1(X100)
| ~ c7_2(X100,X101)
| c2_1(X100) ) ).
cnf(u1606,negated_conjecture,
~ ndr1_1(a229) ).
cnf(u1617,negated_conjecture,
c1_1(a229) ).
cnf(u2809,negated_conjecture,
~ sP9 ).
cnf(u1625,negated_conjecture,
~ c5_1(a226) ).
cnf(u1629,negated_conjecture,
~ ndr1_1(a226) ).
cnf(u2832,negated_conjecture,
~ sP10 ).
cnf(u1644,negated_conjecture,
~ ndr1_1(a223) ).
cnf(u1655,negated_conjecture,
~ c4_1(a223) ).
cnf(u1660,negated_conjecture,
~ c6_1(a222) ).
cnf(u3548,negated_conjecture,
c1_1(a222) ).
cnf(u1671,negated_conjecture,
~ ndr1_1(a222) ).
cnf(u2861,negated_conjecture,
~ sP11 ).
cnf(u1701,negated_conjecture,
( ~ c5_2(X85,a220)
| ~ c4_2(X85,X87)
| ~ c8_2(X85,X87)
| c6_2(X85,X87)
| ~ c1_2(X85,X86)
| ~ ndr1_1(X85)
| c8_2(X85,X86)
| ~ c7_2(X85,X86) ) ).
cnf(u1705,negated_conjecture,
( ~ c3_2(X85,a220)
| ~ c4_2(X85,X87)
| ~ c8_2(X85,X87)
| c6_2(X85,X87)
| ~ c1_2(X85,X86)
| ~ ndr1_1(X85)
| c8_2(X85,X86)
| ~ c7_2(X85,X86) ) ).
cnf(u1713,negated_conjecture,
~ c1_1(a217) ).
cnf(u1717,negated_conjecture,
c7_1(a217) ).
cnf(u1721,negated_conjecture,
c8_1(a217) ).
cnf(u1771,negated_conjecture,
( c7_2(X79,a213)
| c5_1(X79)
| ~ c4_1(X79) ) ).
cnf(u2882,negated_conjecture,
~ sP12 ).
cnf(u1778,negated_conjecture,
( ~ c3_2(X79,a213)
| c5_1(X79)
| ~ c4_1(X79) ) ).
cnf(u1782,negated_conjecture,
( c2_2(X79,a213)
| c5_1(X79)
| ~ c4_1(X79) ) ).
cnf(u1786,negated_conjecture,
( ~ c4_1(X79)
| ndr1_1(X79)
| c5_1(X79) ) ).
cnf(u1809,negated_conjecture,
( ~ c1_2(X75,X77)
| c7_1(X75)
| ~ c7_2(X75,X77)
| c4_2(X75,X77)
| c7_2(X75,X76)
| ~ ndr1_1(X75)
| ~ c6_2(X75,X76)
| c4_2(X75,X76) ) ).
cnf(u1836,negated_conjecture,
( ~ c5_2(X73,a207)
| ~ c5_2(X73,X74)
| c4_2(X73,a206)
| ~ ndr1_1(X73)
| ~ c4_2(X73,X74) ) ).
cnf(u1840,negated_conjecture,
( ~ c4_2(X73,X74)
| c8_2(X73,a207)
| c4_2(X73,a206)
| ~ ndr1_1(X73)
| ~ c5_2(X73,X74) ) ).
cnf(u1844,negated_conjecture,
( ~ c3_2(X73,a207)
| ~ c5_2(X73,X74)
| c4_2(X73,a206)
| ~ ndr1_1(X73)
| ~ c4_2(X73,X74) ) ).
cnf(u1848,negated_conjecture,
( ~ c5_2(X73,a207)
| ~ c5_2(X73,X74)
| c6_2(X73,a206)
| ~ ndr1_1(X73)
| ~ c4_2(X73,X74) ) ).
cnf(u1852,negated_conjecture,
( ~ c4_2(X73,X74)
| c8_2(X73,a207)
| c6_2(X73,a206)
| ~ ndr1_1(X73)
| ~ c5_2(X73,X74) ) ).
cnf(u1856,negated_conjecture,
( ~ c3_2(X73,a207)
| ~ c5_2(X73,X74)
| c6_2(X73,a206)
| ~ ndr1_1(X73)
| ~ c4_2(X73,X74) ) ).
cnf(u1860,negated_conjecture,
( ~ c5_2(X73,a207)
| ~ c5_2(X73,X74)
| c3_2(X73,a206)
| ~ ndr1_1(X73)
| ~ c4_2(X73,X74) ) ).
cnf(u1864,negated_conjecture,
( ~ c4_2(X73,X74)
| c8_2(X73,a207)
| c3_2(X73,a206)
| ~ ndr1_1(X73)
| ~ c5_2(X73,X74) ) ).
cnf(u1868,negated_conjecture,
( ~ c3_2(X73,a207)
| ~ c5_2(X73,X74)
| c3_2(X73,a206)
| ~ ndr1_1(X73)
| ~ c4_2(X73,X74) ) ).
cnf(u1872,negated_conjecture,
c3_2(a204,a205) ).
cnf(u1876,negated_conjecture,
c7_2(a204,a205) ).
cnf(u1880,negated_conjecture,
ndr1_1(a204) ).
cnf(u1884,negated_conjecture,
c8_1(a204) ).
cnf(u1889,negated_conjecture,
( c2_2(a204,X72)
| c8_2(a204,X72) ) ).
cnf(u1906,negated_conjecture,
( c2_2(X67,X68)
| ~ c2_1(X67)
| ~ ndr1_1(X67)
| ~ c5_2(X67,X68)
| c4_2(X67,X68) ) ).
cnf(u2903,negated_conjecture,
~ sP13 ).
cnf(u1933,negated_conjecture,
c6_1(a200) ).
cnf(u1940,negated_conjecture,
~ c1_1(a200) ).
cnf(u1945,negated_conjecture,
~ c1_2(a197,a198) ).
cnf(u1949,negated_conjecture,
~ c6_2(a197,a198) ).
cnf(u1953,negated_conjecture,
c4_2(a197,a198) ).
cnf(u1957,negated_conjecture,
ndr1_1(a197) ).
cnf(u1965,negated_conjecture,
~ c8_1(a197) ).
cnf(u1976,negated_conjecture,
~ ndr1_1(a195) ).
cnf(u1997,negated_conjecture,
( ~ c6_2(X61,X62)
| c5_1(X61)
| ~ c3_1(X61)
| ~ ndr1_1(X61)
| c2_2(X61,X62)
| ~ c7_2(X61,X62) ) ).
cnf(u2916,negated_conjecture,
~ sP14 ).
cnf(u2024,negated_conjecture,
( ~ c6_2(X58,X60)
| c8_1(X58)
| ~ c2_2(X58,X60)
| c3_2(X58,X60)
| ~ ndr1_1(X58)
| c7_2(X58,X59)
| c6_2(X58,X59) ) ).
cnf(u2046,negated_conjecture,
~ ndr1_1(a189) ).
cnf(u2937,negated_conjecture,
~ sP15 ).
cnf(u2060,negated_conjecture,
~ c6_1(a189) ).
cnf(u2100,negated_conjecture,
( ~ c5_2(X44,X46)
| ~ c7_2(X44,X46)
| c5_2(X44,X45)
| c6_1(X44)
| ~ ndr1_1(X44)
| ~ c8_2(X44,X45)
| ~ c6_2(X44,X45) ) ).
cnf(u2104,negated_conjecture,
c4_1(a183) ).
cnf(u2108,negated_conjecture,
c3_2(a183,a184) ).
cnf(u2112,negated_conjecture,
c5_2(a183,a184) ).
cnf(u2116,negated_conjecture,
c7_2(a183,a184) ).
cnf(u2120,negated_conjecture,
ndr1_1(a183) ).
cnf(u2124,negated_conjecture,
c1_1(a183) ).
cnf(u2129,negated_conjecture,
~ c1_1(a182) ).
cnf(u2133,negated_conjecture,
~ ndr1_1(a182) ).
cnf(u2146,negated_conjecture,
( ~ c1_2(X40,X41)
| c1_1(X40)
| ~ ndr1_1(X40)
| c5_2(X40,X41)
| c8_1(X40)
| c7_2(X40,X41) ) ).
cnf(u2156,negated_conjecture,
( ~ c3_1(X35)
| ~ c6_2(X35,X37)
| ~ c5_2(X35,X37)
| ~ c8_2(X35,X36)
| ~ ndr1_1(X35)
| ~ c3_2(X35,X36)
| ~ c1_2(X35,X36) ) ).
cnf(u2168,negated_conjecture,
c6_2(a179,a180) ).
cnf(u2958,negated_conjecture,
~ sP16 ).
cnf(u2175,negated_conjecture,
c3_2(a179,a180) ).
cnf(u2179,negated_conjecture,
c2_2(a179,a180) ).
cnf(u2183,negated_conjecture,
ndr1_1(a179) ).
cnf(u2187,negated_conjecture,
~ c2_1(a179) ).
cnf(u2192,negated_conjecture,
( c2_2(a179,X34)
| ~ c3_2(a179,X34) ) ).
cnf(u2994,negated_conjecture,
~ sP17 ).
cnf(u2206,negated_conjecture,
~ c6_1(a173) ).
cnf(u2218,negated_conjecture,
~ ndr1_1(a173) ).
cnf(u2236,negated_conjecture,
( c3_1(X30)
| c5_1(X30)
| ~ c4_1(X30) ) ).
cnf(u2260,negated_conjecture,
~ ndr1_1(a170) ).
cnf(u2267,negated_conjecture,
~ c7_1(a170) ).
cnf(u2271,negated_conjecture,
~ c5_1(a170) ).
cnf(u2277,negated_conjecture,
~ c6_1(a169) ).
cnf(u2281,negated_conjecture,
c8_1(a169) ).
cnf(u2285,negated_conjecture,
c2_1(a169) ).
cnf(u2290,negated_conjecture,
( c2_2(X27,X28)
| ~ c7_1(X27)
| c1_1(X27)
| ~ ndr1_1(X27)
| ~ c5_2(X27,X28)
| c3_2(X27,X28) ) ).
cnf(u2297,negated_conjecture,
( ~ ndr1_1(X22)
| ~ c1_2(X22,X24)
| ~ c3_2(X22,X24)
| ~ c6_2(X22,X24)
| ~ c8_1(X22)
| ~ c4_2(X22,X23)
| ~ c1_2(X22,X23) ) ).
cnf(u2301,negated_conjecture,
~ c6_1(a168) ).
cnf(u2305,negated_conjecture,
~ ndr1_1(a168) ).
cnf(u2312,negated_conjecture,
~ c2_1(a168) ).
cnf(u3007,negated_conjecture,
~ sP18 ).
cnf(u2320,negated_conjecture,
c6_1(a164) ).
cnf(u2341,negated_conjecture,
ndr1_1(a164) ).
cnf(u2327,negated_conjecture,
( ~ c8_2(a164,X20)
| ~ c2_2(a164,X20) ) ).
cnf(u2331,negated_conjecture,
c3_2(a164,a165) ).
cnf(u2335,negated_conjecture,
~ c5_2(a164,a165) ).
cnf(u2339,negated_conjecture,
~ c2_2(a164,a165) ).
cnf(u2346,negated_conjecture,
c8_2(a162,a163) ).
cnf(u2350,negated_conjecture,
~ c6_2(a162,a163) ).
cnf(u2354,negated_conjecture,
~ c5_2(a162,a163) ).
cnf(u2358,negated_conjecture,
ndr1_1(a162) ).
cnf(u2363,negated_conjecture,
( c8_2(a162,X19)
| ~ c7_2(a162,X19)
| c3_2(a162,X19) ) ).
cnf(u2367,negated_conjecture,
~ c8_1(a162) ).
cnf(u2372,negated_conjecture,
( c2_2(X17,X18)
| c5_1(X17)
| ~ ndr1_1(X17)
| c4_1(X17)
| ~ c7_2(X17,X18) ) ).
cnf(u2403,negated_conjecture,
c2_1(a159) ).
cnf(u2410,negated_conjecture,
~ c4_1(a159) ).
cnf(u2414,negated_conjecture,
~ ndr1_1(a159) ).
cnf(u2421,negated_conjecture,
c1_1(a158) ).
cnf(u2425,negated_conjecture,
~ c4_1(a158) ).
cnf(u2429,negated_conjecture,
~ ndr1_1(a158) ).
cnf(u2437,negated_conjecture,
c5_1(a157) ).
cnf(u3033,negated_conjecture,
~ sP19 ).
cnf(u2447,negated_conjecture,
~ c4_1(a157) ).
cnf(u2462,negated_conjecture,
~ ndr1_1(a153) ).
cnf(u2469,negated_conjecture,
~ c1_1(a153) ).
cnf(u2473,negated_conjecture,
~ c4_1(a153) ).
cnf(u2478,negated_conjecture,
( ~ c5_1(X8)
| ~ c3_2(X8,X9)
| c7_2(X8,a152)
| ~ ndr1_1(X8)
| ~ c5_2(X8,X9)
| c7_2(X8,X9) ) ).
cnf(u2482,negated_conjecture,
( ~ c3_2(X8,a152)
| ~ c5_1(X8)
| ~ c3_2(X8,X9)
| ~ ndr1_1(X8)
| ~ c5_2(X8,X9)
| c7_2(X8,X9) ) ).
cnf(u2486,negated_conjecture,
( ~ c4_2(X8,a152)
| ~ c5_1(X8)
| ~ c3_2(X8,X9)
| ~ ndr1_1(X8)
| ~ c5_2(X8,X9)
| c7_2(X8,X9) ) ).
cnf(u2493,negated_conjecture,
( c6_1(X6)
| c2_1(X6)
| c8_1(X6) ) ).
cnf(u2513,negated_conjecture,
~ c8_2(a148,a150) ).
cnf(u2517,negated_conjecture,
~ c1_2(a148,a150) ).
cnf(u2521,negated_conjecture,
ndr1_1(a148) ).
cnf(u2526,negated_conjecture,
( ~ c8_2(a148,X3)
| ~ c4_2(a148,X3)
| c5_2(a148,X3) ) ).
cnf(u2530,negated_conjecture,
c2_2(a148,a149) ).
cnf(u2534,negated_conjecture,
c7_2(a148,a149) ).
cnf(u2538,negated_conjecture,
~ c1_2(a148,a149) ).
cnf(u2806,axiom,
ndr1_1(a233) ).
cnf(u2788,axiom,
( c6_2(a233,X1)
| ~ c8_2(a233,X1) ) ).
cnf(u2792,axiom,
( ~ c4_2(a233,X0)
| ~ c3_2(a233,X0) ) ).
cnf(u2796,axiom,
c1_2(a233,a234) ).
cnf(u2800,axiom,
c3_2(a233,a234) ).
cnf(u2804,axiom,
c6_2(a233,a234) ).
cnf(u3086,negated_conjecture,
~ c2_2(a164,a292) ).
cnf(u3101,negated_conjecture,
~ c8_1(a294) ).
cnf(u3130,negated_conjecture,
~ c7_2(a268,a269) ).
cnf(u3138,negated_conjecture,
~ c8_1(a237) ).
cnf(u3148,negated_conjecture,
~ ndr1_1(a287) ).
cnf(u3195,negated_conjecture,
( ~ c1_2(a237,X0)
| c4_2(a237,X0)
| c5_2(a237,X0) ) ).
cnf(u3204,negated_conjecture,
~ c8_1(a200) ).
cnf(u3209,negated_conjecture,
( ~ c4_2(a233,X1)
| ~ c1_2(a233,X1) ) ).
cnf(u3459,negated_conjecture,
c8_1(a233) ).
cnf(u3226,negated_conjecture,
c2_1(a237) ).
cnf(u3231,negated_conjecture,
( ~ c6_2(a197,X0)
| ~ c3_2(a197,X0)
| ~ c8_2(a197,X0) ) ).
cnf(u3241,negated_conjecture,
( ~ c8_2(a233,X0)
| ~ c3_2(a233,X0) ) ).
cnf(u3255,negated_conjecture,
~ c3_2(a233,a292) ).
cnf(u3263,negated_conjecture,
c3_1(a162) ).
cnf(u3281,negated_conjecture,
~ c6_1(a279) ).
cnf(u3429,negated_conjecture,
c8_1(a279) ).
cnf(u3293,negated_conjecture,
~ c8_1(a148) ).
cnf(u3300,negated_conjecture,
c3_1(a148) ).
cnf(u3318,negated_conjecture,
~ c4_2(a148,a292) ).
cnf(u3323,negated_conjecture,
c1_1(a157) ).
cnf(u3339,negated_conjecture,
c2_1(a204) ).
cnf(u3343,negated_conjecture,
( ~ c1_2(a204,X1)
| ~ c4_2(a204,X1) ) ).
cnf(u3355,negated_conjecture,
c6_1(a183) ).
cnf(u3368,negated_conjecture,
~ c8_1(a268) ).
cnf(u3375,negated_conjecture,
c3_1(a268) ).
cnf(u3399,negated_conjecture,
~ c7_2(a233,a234) ).
cnf(u3412,negated_conjecture,
~ c7_2(a268,a270) ).
cnf(u3441,negated_conjecture,
~ c2_2(a268,a270) ).
cnf(u3453,negated_conjecture,
~ c8_2(a233,a236) ).
cnf(u3468,negated_conjecture,
~ c8_1(a164) ).
cnf(u3478,negated_conjecture,
( ~ c6_2(a164,X0)
| ~ c3_2(a164,X0)
| ~ c8_2(a164,X0) ) ).
cnf(u3491,negated_conjecture,
( ~ c3_2(a279,X0)
| ~ c6_2(a279,X0)
| ~ c1_2(a279,X0) ) ).
cnf(u3498,negated_conjecture,
~ c5_2(a197,a198) ).
cnf(u3510,negated_conjecture,
( ~ c3_2(a162,X1)
| ~ c1_2(a162,X1)
| ~ c8_2(a162,X1) ) ).
cnf(u3518,negated_conjecture,
~ ndr1_1(a217) ).
cnf(u3527,negated_conjecture,
~ ndr1_1(a157) ).
cnf(u3540,negated_conjecture,
c8_1(a222) ).
cnf(u3555,negated_conjecture,
( ~ c3_2(a148,X1)
| ~ c1_2(a148,X1)
| ~ c8_2(a148,X1) ) ).
cnf(u3581,negated_conjecture,
~ c2_2(a204,a260) ).
cnf(u3592,negated_conjecture,
~ c2_2(a294,a260) ).
cnf(u3602,negated_conjecture,
~ c2_2(a148,a260) ).
cnf(u3638,negated_conjecture,
~ c2_2(a279,a260) ).
cnf(u3648,negated_conjecture,
~ c2_2(a233,a260) ).
cnf(u3665,negated_conjecture,
~ c8_1(a179) ).
cnf(u3676,negated_conjecture,
( ~ c6_2(a179,X0)
| ~ c3_2(a179,X0)
| ~ c8_2(a179,X0) ) ).
cnf(u3706,negated_conjecture,
c5_2(a268,a270) ).
cnf(u3737,negated_conjecture,
~ c2_2(a183,a260) ).
cnf(u3751,negated_conjecture,
~ c7_2(a148,a150) ).
cnf(u3754,negated_conjecture,
~ c1_1(a148) ).
cnf(u3769,negated_conjecture,
~ c7_2(a294,a260) ).
cnf(u3779,negated_conjecture,
~ c5_2(a294,a260) ).
cnf(u3811,negated_conjecture,
c1_1(a168) ).
cnf(u3823,negated_conjecture,
~ c8_1(a183) ).
cnf(u3836,negated_conjecture,
c2_1(a183) ).
cnf(u3847,negated_conjecture,
~ c7_2(a148,a260) ).
cnf(u3857,negated_conjecture,
~ c5_2(a148,a260) ).
cnf(u3876,negated_conjecture,
~ c7_2(a233,a260) ).
cnf(u3886,negated_conjecture,
~ c5_2(a233,a260) ).
cnf(u3899,negated_conjecture,
~ c7_2(a197,a198) ).
cnf(u3912,negated_conjecture,
~ c7_2(a279,a260) ).
cnf(u3925,negated_conjecture,
~ c5_2(a279,a260) ).
cnf(u3928,negated_conjecture,
c1_1(a279) ).
cnf(u3960,negated_conjecture,
~ c7_2(a204,a260) ).
cnf(u3973,negated_conjecture,
~ c5_2(a204,a260) ).
cnf(u3998,negated_conjecture,
~ c7_2(a164,a165) ).
cnf(u4018,negated_conjecture,
~ c7_2(a164,a292) ).
cnf(u4025,negated_conjecture,
~ c5_2(a164,a292) ).
cnf(u4061,negated_conjecture,
c3_1(a288) ).
cnf(u4076,negated_conjecture,
( ~ c6_2(a288,X0)
| ~ c5_2(a288,X0) ) ).
cnf(u4089,negated_conjecture,
~ c7_2(a183,a260) ).
cnf(u4102,negated_conjecture,
~ c5_2(a183,a260) ).
cnf(u4140,negated_conjecture,
c8_1(a173) ).
cnf(u4138,negated_conjecture,
c1_1(a173) ).
cnf(u4159,negated_conjecture,
~ c5_2(a294,a295) ).
cnf(u4188,negated_conjecture,
c8_1(a189) ).
cnf(u4186,negated_conjecture,
c1_1(a189) ).
cnf(u3144,negated_conjecture,
( ~ c7_2(X0,a293)
| c8_2(X0,a292)
| ~ ndr1_1(X0)
| ~ c1_1(X0)
| c4_1(X0)
| c2_1(X0) ) ).
cnf(u3494,negated_conjecture,
( ~ c5_2(X0,a293)
| c4_2(X0,a206)
| ~ ndr1_1(X0)
| c8_2(X0,a207)
| c4_1(X0)
| c7_2(X0,a292) ) ).
cnf(u3949,negated_conjecture,
c8_2(a204,a260) ).
cnf(u3613,negated_conjecture,
( ~ c5_2(X0,a293)
| c6_2(X0,a206)
| ~ ndr1_1(X0)
| c8_2(X0,a207)
| c4_1(X0)
| c7_2(X0,a292) ) ).
cnf(u3360,negated_conjecture,
( ~ c1_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X2)
| c5_1(X0) ) ).
cnf(u205,axiom,
( ~ sP1(X0)
| ~ c7_2(X0,a285) ) ).
cnf(u4052,negated_conjecture,
~ c8_2(a179,a180) ).
cnf(u3813,negated_conjecture,
c8_1(a168) ).
cnf(u3078,negated_conjecture,
( c2_2(X61,X62)
| c5_1(X61)
| ~ ndr1_1(X61)
| ~ c6_2(X61,X62)
| ~ c7_2(X61,X62) ) ).
cnf(u3523,negated_conjecture,
~ c2_1(a217) ).
cnf(u3060,negated_conjecture,
( ~ c7_1(X129)
| ~ c8_2(X129,X130)
| ~ ndr1_1(X129)
| ~ c5_2(X129,X130)
| c3_2(X129,X130) ) ).
cnf(u3061,negated_conjecture,
( c3_1(X30)
| c5_1(X30) ) ).
cnf(u3571,negated_conjecture,
( ~ c4_1(X0)
| ~ c2_2(X0,a260)
| c1_2(X0,a213)
| c8_2(X0,a213)
| c5_1(X0)
| c1_2(X0,a261) ) ).
cnf(u3563,negated_conjecture,
( ~ c5_2(X0,a293)
| c3_2(X0,a206)
| ~ ndr1_1(X0)
| c8_2(X0,a207)
| c4_1(X0)
| c7_2(X0,a292) ) ).
cnf(u206,axiom,
( ~ sP1(X0)
| c3_2(X0,a285) ) ).
cnf(u4124,negated_conjecture,
( ~ c4_2(X0,X2)
| ~ c5_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X2)
| c5_1(X0)
| ~ c6_2(X0,X1)
| ~ c1_1(X0)
| ~ c7_2(X0,X2)
| c2_1(X0) ) ).
cnf(u3611,negated_conjecture,
c1_1(a169) ).
cnf(u208,axiom,
( ~ sP1(X0)
| ndr1_1(X0) ) ).
cnf(u3682,negated_conjecture,
( c2_2(X0,a261)
| ~ c2_2(X0,a260)
| c1_2(X0,a213)
| c8_2(X0,a213)
| c5_1(X0)
| ~ c4_1(X0) ) ).
cnf(u207,axiom,
( ~ sP1(X0)
| ~ c8_2(X0,a285) ) ).
cnf(u3272,negated_conjecture,
( ~ c7_2(X0,a293)
| c7_2(X0,a292)
| ~ ndr1_1(X0)
| ~ c1_1(X0)
| c4_1(X0)
| c2_1(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN545+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.08/0.16 % Computer : n007.cluster.edu
% 0.08/0.16 % Model : x86_64 x86_64
% 0.08/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.16 % Memory : 8046.5625MB
% 0.08/0.16 % OS : Linux 6.8.0-71-generic
% 0.08/0.16 % CPULimit : 300
% 0.08/0.16 % WCLimit : 300
% 0.08/0.16 % DateTime : Mon Sep 28 16:26:07 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 Running first-order theorem proving
% 0.08/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
% 5.84/1.91 % (2535158)Detected formulas, will run a generic FOF schedule.
% 5.84/1.91 % (2535286)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1561920612:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.84/1.91 % (2535284)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=221499493:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.84/1.91 % (2535282)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=627432789:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.84/1.91 % (2535283)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=1826230665:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.84/1.91 % (2535286)Refutation not found, incomplete strategy
% 5.84/1.91 % (2535286)------------------------------
% 5.84/1.91 % (2535286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535286)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535286)Termination reason: Refutation not found, incomplete strategy
% 5.84/1.91 % (2535286)Time elapsed: 0.030 s
% 5.84/1.91 % (2535286)Peak memory usage: 91 MB
% 5.84/1.91 % (2535286)Instructions burned: 95 (million)
% 5.84/1.91 % (2535288)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2666717700:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.84/1.91 % (2535289)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1629617469:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.84/1.91 % (2535290)dis-21_1_sil=8000:lcm=predicate:random_seed=946803081: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)
% 5.84/1.91 % (2535289)Refutation not found, incomplete strategy
% 5.84/1.91 % (2535289)------------------------------
% 5.84/1.91 % (2535289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535289)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535289)Termination reason: Refutation not found, incomplete strategy
% 5.84/1.91 % (2535289)Time elapsed: 0.039 s
% 5.84/1.91 % (2535289)Peak memory usage: 90 MB
% 5.84/1.91 % (2535289)Instructions burned: 64 (million)
% 5.84/1.91 % (2535288)Instruction limit reached!
% 5.84/1.91 % (2535288)------------------------------
% 5.84/1.91 % (2535288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535288)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535288)Termination reason: Instruction limit
% 5.84/1.91 % (2535288)Termination phase: Saturation
% 5.84/1.91 % (2535288)Time elapsed: 0.066 s
% 5.84/1.91 % (2535288)Peak memory usage: 89 MB
% 5.84/1.91 % (2535288)Instructions burned: 121 (million)
% 5.84/1.91 % (2535290)Instruction limit reached!
% 5.84/1.91 % (2535290)------------------------------
% 5.84/1.91 % (2535290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535290)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535290)Termination reason: Instruction limit
% 5.84/1.91 % (2535290)Termination phase: Saturation
% 5.84/1.91 % (2535290)Time elapsed: 0.074 s
% 5.84/1.91 % (2535290)Peak memory usage: 91 MB
% 5.84/1.91 % (2535290)Instructions burned: 130 (million)
% 5.84/1.91 % (2535286)------------------------------
% 5.84/1.91 % (2535286)------------------------------
% 5.84/1.91 % (2535352)lrs+10_1_sil=8000:sp=occurrence:random_seed=2316040135:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.84/1.91 % (2535360)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2260030744:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.84/1.91 % (2535384)lrs+1011_1_sil=32000:sp=occurrence:random_seed=583716105:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 5.84/1.91 % (2535360)Refutation not found, incomplete strategy
% 5.84/1.91 % (2535360)------------------------------
% 5.84/1.91 % (2535360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535360)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535360)Termination reason: Refutation not found, incomplete strategy
% 5.84/1.91 % (2535360)Time elapsed: 0.027 s
% 5.84/1.91 % (2535360)Peak memory usage: 90 MB
% 5.84/1.91 % (2535360)Instructions burned: 43 (million)
% 5.84/1.91 % (2535384)Refutation not found, incomplete strategy
% 5.84/1.91 % (2535384)------------------------------
% 5.84/1.91 % (2535384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535384)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535384)Termination reason: Refutation not found, incomplete strategy
% 5.84/1.91 % (2535384)Time elapsed: 0.012 s
% 5.84/1.91 % (2535384)Peak memory usage: 90 MB
% 5.84/1.91 % (2535384)Instructions burned: 34 (million)
% 5.84/1.91 % (2535289)------------------------------
% 5.84/1.91 % (2535289)------------------------------
% 5.84/1.91 % (2535352)Instruction limit reached!
% 5.84/1.91 % (2535352)------------------------------
% 5.84/1.91 % (2535352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535352)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535352)Termination reason: Instruction limit
% 5.84/1.91 % (2535352)Termination phase: Saturation
% 5.84/1.91 % (2535352)Time elapsed: 0.153 s
% 5.84/1.91 % (2535352)Peak memory usage: 93 MB
% 5.84/1.91 % (2535352)Instructions burned: 287 (million)
% 5.84/1.91 % (2535384)------------------------------
% 5.84/1.91 % (2535384)------------------------------
% 5.84/1.91 % (2535432)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=4001739538:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.84/1.91 % (2535432)Refutation not found, incomplete strategy
% 5.84/1.91 % (2535432)------------------------------
% 5.84/1.91 % (2535432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535432)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535432)Termination reason: Refutation not found, incomplete strategy
% 5.84/1.91 % (2535432)Time elapsed: 0.032 s
% 5.84/1.91 % (2535432)Peak memory usage: 90 MB
% 5.84/1.91 % (2535432)Instructions burned: 51 (million)
% 5.84/1.91 % (2535360)------------------------------
% 5.84/1.91 % (2535360)------------------------------
% 5.84/1.91 % (2535433)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=545290434:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 5.84/1.91 % (2535439)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2327938127:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 5.84/1.91 % (2535481)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2212162825:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 5.84/1.91 % (2535433)Instruction limit reached!
% 5.84/1.91 % (2535433)------------------------------
% 5.84/1.91 % (2535433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535433)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535433)Termination reason: Instruction limit
% 5.84/1.91 % (2535433)Termination phase: Saturation
% 5.84/1.91 % (2535433)Time elapsed: 0.159 s
% 5.84/1.91 % (2535433)Peak memory usage: 91 MB
% 5.84/1.91 % (2535433)Instructions burned: 295 (million)
% 5.84/1.91 % (2535432)------------------------------
% 5.84/1.91 % (2535432)------------------------------
% 5.84/1.91 % (2535481)Refutation not found, incomplete strategy
% 5.84/1.91 % (2535481)------------------------------
% 5.84/1.91 % (2535481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535481)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535481)Termination reason: Refutation not found, incomplete strategy
% 5.84/1.91 % (2535481)Time elapsed: 0.060 s
% 5.84/1.91 % (2535481)Peak memory usage: 91 MB
% 5.84/1.91 % (2535481)Instructions burned: 100 (million)
% 5.84/1.91 % (2535283)First to succeed.
% 5.84/1.91 % (2535283)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2535158"
% 5.84/1.91 % (2535487)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4084938741:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 5.84/1.91 % (2535282)Also succeeded, but the first one will report.
% 5.84/1.91 % (2535488)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1508964023:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 5.84/1.91 % (2535487)Instruction limit reached!
% 5.84/1.91 % (2535487)------------------------------
% 5.84/1.91 % (2535487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535487)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535487)Termination reason: Instruction limit
% 5.84/1.91 % (2535487)Termination phase: Saturation
% 5.84/1.91 % (2535487)Time elapsed: 0.067 s
% 5.84/1.91 % (2535487)Peak memory usage: 90 MB
% 5.84/1.91 % (2535487)Instructions burned: 128 (million)
% 5.84/1.91 % (2535488)Instruction limit reached!
% 5.84/1.91 % (2535488)------------------------------
% 5.84/1.91 % (2535488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.91 % (2535488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.91 % (2535488)CaDiCaL version: 2.1.3
% 5.84/1.91 % (2535488)Termination reason: Instruction limit
% 5.84/1.91 % (2535488)Termination phase: Saturation
% 5.84/1.91 % (2535488)Time elapsed: 0.061 s
% 5.84/1.91 % (2535488)Peak memory usage: 90 MB
% 5.84/1.91 % (2535488)Instructions burned: 116 (million)
% 5.84/1.91 % (2535481)------------------------------
% 5.84/1.91 % (2535481)------------------------------
% 5.84/1.91 % SZS status CounterSatisfiable for theBenchmark
% 5.84/1.91 % SZS output start Saturation.
% See solution above
% 5.84/1.92 % SZS output start Definitions and Model Updates.
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_1(X145) | sP1(X145) | ~c7_2(X145,a286) | ~ndr1_0 | c6_0 | c1_1(X146) | ~c8_1(X146) | c6_1(X146) | ~ndr1_0 is false, set ~c7_2(X145,a286) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c5_0 | ~c7_2(X131,a263) | ~c6_1(X131) | ndr1_1(X131) | ~ndr1_0 | ~c3_0 is false, set ~c7_2(X131,a263) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c5_2(X145,a284) | sP1(X145) | ndr1_1(X145) | ~ndr1_0 | c6_0 | c1_1(X146) | ~c8_1(X146) | c6_1(X146) | ~ndr1_0 is false, set c5_2(X145,a284) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c3_1(X112) | c5_2(X112,a250) | ndr1_1(X112) | ~ndr1_0 | c8_0 | ~c6_0 is false, set c5_2(X112,a250) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c5_0 | ndr1_1(X131) | ~c6_1(X131) | c5_2(X131,a264) | ~ndr1_0 | ~c3_0 is false, set c5_2(X131,a264) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c2_0 | c7_2(X152,a292) | ndr1_1(X152) | c4_1(X152) | ~ndr1_0 | ~c4_0 is false, set c7_2(X152,a292) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c3_1(X112) | c7_2(X112,a250) | ndr1_1(X112) | ~ndr1_0 | c8_0 | ~c6_0 is false, set c7_2(X112,a250) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c5_0 | ndr1_1(X131) | ~c6_1(X131) | c7_2(X131,a264) | ~ndr1_0 | ~c3_0 is false, set c7_2(X131,a264) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_1(X0) | c5_1(X0) | c7_2(X0,a255) | ~ndr1_0 | ~sP5 is false, set c7_2(X0,a255) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c3_1(X112) | ndr1_1(X112) | ~c3_2(X112,a251) | ~ndr1_0 | c8_0 | ~c6_0 is false, set ~c3_2(X112,a251) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c2_0 | ndr1_1(X152) | ~c3_2(X152,a293) | c4_1(X152) | ~ndr1_0 | ~c4_0 is false, set ~c3_2(X152,a293) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_1(X0) | c5_1(X0) | ~c3_2(X0,a255) | ~ndr1_0 | ~sP5 is false, set ~c3_2(X0,a255) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_1(X0) | c1_1(X0) | ~c4_2(X0,a225) | ~ndr1_0 | ~sP10 is false, set ~c4_2(X0,a225) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c3_1(X112) | ndr1_1(X112) | ~c2_2(X112,a251) | ~ndr1_0 | c8_0 | ~c6_0 is false, set ~c2_2(X112,a251) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_1(X0) | c5_1(X0) | ~c8_2(X0,a255) | ~ndr1_0 | ~sP5 is false, set ~c8_2(X0,a255) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c7_0 | ~c8_2(a265,a266) | ndr1_0 is false, set ~c8_2(a265,a266) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c3_1(X112) | ndr1_1(X112) | ~c8_2(X112,a251) | ~ndr1_0 | c8_0 | ~c6_0 is false, set ~c8_2(X112,a251) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c5_0 | ~c5_2(X131,a263) | ~c6_1(X131) | ndr1_1(X131) | ~ndr1_0 | ~c3_0 is false, set ~c5_2(X131,a263) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c2_0 | ~c5_2(X152,a292) | ndr1_1(X152) | c4_1(X152) | ~ndr1_0 | ~c4_0 is false, set ~c5_2(X152,a292) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c5_2(X0,a224) | c1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP10 is false, set ~c5_2(X0,a224) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c5_2(X0,a254) | c5_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP5 is false, set ~c5_2(X0,a254) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c5_0 | c4_2(X131,a263) | ~c6_1(X131) | ndr1_1(X131) | ~ndr1_0 | ~c3_0 is false, set c4_2(X131,a263) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c2_0 | ndr1_1(X152) | c4_2(X152,a293) | c4_1(X152) | ~ndr1_0 | ~c4_0 is false, set c4_2(X152,a293) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c1_2(X0,a254) | c5_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP5 is false, set c1_2(X0,a254) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c5_0 | ndr1_1(X131) | ~c6_1(X131) | c1_2(X131,a264) | ~ndr1_0 | ~c3_0 is false, set c1_2(X131,a264) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c1_2(X145,a284) | sP1(X145) | ndr1_1(X145) | ~ndr1_0 | c6_0 | c1_1(X146) | ~c8_1(X146) | c6_1(X146) | ~ndr1_0 is false, set c1_2(X145,a284) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c7_0 | ndr1_0 | c6_2(a267,X135) | c3_2(a267,X135) | ~ndr1_1(a267) is false, set c3_2(a267,X135) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c3_2(X145,a284) | sP1(X145) | ndr1_1(X145) | ~ndr1_0 | c6_0 | c1_1(X146) | ~c8_1(X146) | c6_1(X146) | ~ndr1_0 is false, set c3_2(X145,a284) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c3_2(X0,a224) | c1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP10 is false, set c3_2(X0,a224) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_0 | ~c2_0 | ~c1_1(a222) is false, set ~c1_1(a222) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c1_1(a221) | ~c2_0 | ndr1_0 is false, set ~c1_1(a221) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c3_1(X112) | c8_2(X112,a250) | ndr1_1(X112) | ~ndr1_0 | c8_0 | ~c6_0 is false, set c8_2(X112,a250) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_1(X0) | c1_1(X0) | c8_2(X0,a225) | ~ndr1_0 | ~sP10 is false, set c8_2(X0,a225) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c2_0 | c8_2(X152,a292) | ndr1_1(X152) | c4_1(X152) | ~ndr1_0 | ~c4_0 is false, set c8_2(X152,a292) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_1(X145) | sP1(X145) | ~c1_2(X145,a286) | ~ndr1_0 | c6_0 | c1_1(X146) | ~c8_1(X146) | c6_1(X146) | ~ndr1_0 is false, set ~c1_2(X145,a286) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c2_0 | ndr1_1(X152) | ~c1_2(X152,a293) | c4_1(X152) | ~ndr1_0 | ~c4_0 is false, set ~c1_2(X152,a293) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c7_0 | ~c3_2(X8,X9) | c7_2(X8,X9) | ~c5_2(X8,X9) | ~ndr1_1(X8) | ndr1_1(X8) | ~c5_1(X8) | ~ndr1_0 is false, set ~c5_1(X8) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c2_1(a221) | ~c2_0 | ndr1_0 is false, set ~c2_1(a221) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c6_2(X0,a254) | c5_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP5 is false, set ~c6_2(X0,a254) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c1_2(X63,X64) | ~c6_2(X63,X64) | ~c3_2(X63,X64) | ~ndr1_1(X63) | ~c4_1(X63) | ~c2_1(X63) | ~ndr1_0 | ndr1_0 | ndr1_0 is false, set ~c4_1(X63) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c1_2(X63,X64) | ~c6_2(X63,X64) | ~c3_2(X63,X64) | ~ndr1_1(X63) | ~c4_1(X63) | ~c2_1(X63) | ~ndr1_0 | c4_2(a195,X65) | ~c6_2(a195,X65) | c5_2(a195,X65) | ~ndr1_1(a195) | ndr1_0 is false, set ~c4_1(X63) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_0 | sP19 | ~c4_1(a157) is false, set ~c4_1(a157) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c1_2(X63,X64) | ~c6_2(X63,X64) | ~c3_2(X63,X64) | ~ndr1_1(X63) | ~c4_1(X63) | ~c2_1(X63) | ~ndr1_0 | ndr1_0 | ~c4_1(a196) is false, set ~c4_1(X63) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c1_2(X63,X64) | ~c6_2(X63,X64) | ~c3_2(X63,X64) | ~ndr1_1(X63) | ~c4_1(X63) | ~c2_1(X63) | ~ndr1_0 | ndr1_0 | ~c1_2(a196,X66) | ~c4_2(a196,X66) | ~ndr1_1(a196) is false, set ~c4_1(X63) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c2_1(a154) | sP19 | ndr1_0 is false, set c2_1(a154) to true
% 5.84/1.92 for all groundings, until fixed point,
% 5.84/1.92 whenever ~c1_2(X63,X64) | ~c6_2(X63,X64) | ~c3_2(X63,X64) | ~ndr1_1(X63) | ~c4_1(X63) | ~c2_1(X63) | ~ndr1_0 | ndr1_0 | c2_1(a196) is false, set c2_1(a196) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_0 | ~c6_2(X98,X99) | c3_2(X98,X99) | ~ndr1_1(X98) | ~c3_1(X98) | ~c5_1(X98) | ~ndr1_0 | ~c1_1(X100) | c2_1(X100) | ~c7_2(X100,X101) | c1_2(X100,X101) | ~c4_2(X100,X101) | ~ndr1_1(X100) | ~ndr1_0 is false, set c2_1(X100) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_0 | c7_2(X75,X76) | c4_2(X75,X76) | ~c6_2(X75,X76) | ~ndr1_1(X75) | ~c1_2(X75,X77) | c4_2(X75,X77) | ~c7_2(X75,X77) | ~ndr1_1(X75) | c7_1(X75) | ~ndr1_0 | ~c8_0 is false, set ~c8_0 to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_1(X0) | c1_1(X0) | c2_2(X0,a225) | ~ndr1_0 | ~sP10 is false, set c2_2(X0,a225) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c2_2(X67,X68) | c4_2(X67,X68) | ~c5_2(X67,X68) | ~ndr1_1(X67) | ~c2_1(X67) | ~ndr1_0 | ndr1_0 | ndr1_0 is false, set c2_2(X67,X68) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c2_2(X67,X68) | c4_2(X67,X68) | ~c5_2(X67,X68) | ~ndr1_1(X67) | ~c2_1(X67) | ~ndr1_0 | ndr1_0 | c8_1(a203) is false, set c2_2(X67,X68) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c2_2(X67,X68) | c4_2(X67,X68) | ~c5_2(X67,X68) | ~ndr1_1(X67) | ~c2_1(X67) | ~ndr1_0 | ndr1_0 | ~c1_2(a203,X71) | ~c5_2(a203,X71) | ~c8_2(a203,X71) | ~ndr1_1(a203) is false, set c2_2(X67,X68) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c2_2(X67,X68) | c4_2(X67,X68) | ~c5_2(X67,X68) | ~ndr1_1(X67) | ~c2_1(X67) | ~ndr1_0 | c7_1(a202) | ndr1_0 is false, set c2_2(X67,X68) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c2_2(X67,X68) | c4_2(X67,X68) | ~c5_2(X67,X68) | ~ndr1_1(X67) | ~c2_1(X67) | ~ndr1_0 | ~c6_2(a202,X69) | c3_2(a202,X69) | c8_2(a202,X69) | ~ndr1_1(a202) | ndr1_0 is false, set c2_2(X67,X68) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c2_2(X67,X68) | c4_2(X67,X68) | ~c5_2(X67,X68) | ~ndr1_1(X67) | ~c2_1(X67) | ~ndr1_0 | c6_2(a202,X70) | c7_2(a202,X70) | ~c3_2(a202,X70) | ~ndr1_1(a202) | ndr1_0 is false, set c2_2(X67,X68) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ~c7_2(a221,X88) | c2_2(a221,X88) | c4_2(a221,X88) | ~ndr1_1(a221) | ~c2_0 | ndr1_0 is false, set c2_2(a221,X88) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_0 | ~c2_0 | c5_2(a222,X89) | c2_2(a222,X89) | ~ndr1_1(a222) is false, set c2_2(a222,X89) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c7_0 | c2_2(a265,a266) | ndr1_0 is false, set c2_2(a265,a266) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c2_1(X125) | ndr1_1(X125) | c5_2(X125,X126) | c1_2(X125,X126) | ~c3_2(X125,X126) | ~ndr1_1(X125) | ~ndr1_0 | ~c6_0 | c1_0 is false, set c1_0 to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c6_1(a154) | sP19 | ndr1_0 is false, set c6_1(a154) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c2_2(X67,X68) | c4_2(X67,X68) | ~c5_2(X67,X68) | ~ndr1_1(X67) | ~c2_1(X67) | ~ndr1_0 | ndr1_0 | c4_1(a203) is false, set c4_1(a203) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c4_1(a154) | sP19 | ndr1_0 is false, set c4_1(a154) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_0 | ~c2_0 | ~c6_1(a222) is false, set ~c6_1(a222) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c7_0 | ~c6_1(a265) | ndr1_0 is false, set ~c6_1(a265) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_0 | ~c5_1(X120) | c1_1(X120) | c3_1(X120) | ~ndr1_0 | c6_0 is false, set c6_0 to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_0 | sP19 | c5_1(a157) is false, set c5_1(a157) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever ndr1_0 | c8_1(X16) | ~c1_1(X16) | ~ndr1_0 | c4_1(X17) | ~c7_2(X17,X18) | c2_2(X17,X18) | ~ndr1_1(X17) | c5_1(X17) | ~ndr1_0 is false, set c5_1(X17) to true
% 5.84/1.92 for all groundings,
% 5.84/1.92 whenever c1_0 | ~c6_2(X61,X62) | ~c7_2(X61,X62) | c2_2(X61,X62) | ~ndr1_1(X61) | ~c3_1(X61) | c5_1(X61) | ~ndr1_0 | ndr1_0 is false, set c5_1(X61) to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c6_0 | ndr1_0 | c3_1(X154) | c4_1(X154) | c5_1(X154) | ~ndr1_0 is false, set c5_1(X154) to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c1_0 | c3_1(X30) | ~c4_1(X30) | c5_1(X30) | ~ndr1_0 | ndr1_0 is false, set c5_1(X30) to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c3_0 | ~c5_2(X73,X74) | ~c4_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | ndr1_1(X73) | ~ndr1_0 | c4_0 is false, set c3_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c3_0 | ~c5_2(X73,X74) | ~c4_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | c8_2(X73,a207) | ~ndr1_0 | c4_0 is false, set c3_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c3_0 | ~c5_2(X73,X74) | ~c4_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | ~c3_2(X73,a207) | ~ndr1_0 | c4_0 is false, set c3_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c3_0 | ~c5_2(X73,X74) | ~c4_2(X73,X74) | ~ndr1_1(X73) | c3_2(X73,a206) | ndr1_1(X73) | ~ndr1_0 | c4_0 is false, set c3_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c3_0 | ~c5_2(X73,X74) | ~c4_2(X73,X74) | ~ndr1_1(X73) | c6_2(X73,a206) | ndr1_1(X73) | ~ndr1_0 | c4_0 is false, set c3_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c3_0 | ~c5_2(X73,X74) | ~c4_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | ~c5_2(X73,a207) | ~ndr1_0 | c4_0 is false, set c3_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c3_0 | ~c5_2(X73,X74) | ~c4_2(X73,X74) | ~ndr1_1(X73) | c4_2(X73,a206) | ndr1_1(X73) | ~ndr1_0 | c4_0 is false, set c3_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c3_0 | c3_2(X0,X1) | c4_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c5_2(X0,X2) | c4_2(X0,X2) | ~c7_2(X0,X2) | ~ndr1_1(X0) | ~ndr1_0 is false, set ~c3_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | ~c4_0 | ~c8_1(X114) | ~ndr1_0 is false, set ~c8_1(X114) to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c6_0 | c5_0 | ~c7_2(X123,X124) | c8_2(X123,X124) | c1_2(X123,X124) | ~ndr1_1(X123) | ndr1_1(X123) | c1_2(X123,a261) | ~ndr1_0 is false, set c5_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c8_2(X35,X36) | ~c1_2(X35,X36) | ~c3_2(X35,X36) | ~ndr1_1(X35) | ~c3_1(X35) | ~c5_2(X35,X37) | ~c6_2(X35,X37) | ~ndr1_1(X35) | ~ndr1_0 | c5_0 | ndr1_0 is false, set c5_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c6_0 | c5_0 | ~c7_2(X123,X124) | c8_2(X123,X124) | c1_2(X123,X124) | ~ndr1_1(X123) | ndr1_1(X123) | ~c6_2(X123,a261) | ~ndr1_0 is false, set c5_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c6_0 | c5_0 | ~c7_2(X123,X124) | c8_2(X123,X124) | c1_2(X123,X124) | ~ndr1_1(X123) | ndr1_1(X123) | c2_2(X123,a261) | ~ndr1_0 is false, set c5_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c6_0 | c5_0 | ~c7_2(X123,X124) | c8_2(X123,X124) | c1_2(X123,X124) | ~ndr1_1(X123) | ndr1_1(X123) | ndr1_1(X123) | ~ndr1_0 is false, set c5_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c6_0 | c5_0 | ~c7_2(X123,X124) | c8_2(X123,X124) | c1_2(X123,X124) | ~ndr1_1(X123) | ~c2_2(X123,a260) | ndr1_1(X123) | ~ndr1_0 is false, set c5_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c6_0 | c5_0 | ~c7_2(X123,X124) | c8_2(X123,X124) | c1_2(X123,X124) | ~ndr1_1(X123) | ~c1_2(X123,a260) | ndr1_1(X123) | ~ndr1_0 is false, set c5_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c6_0 | c5_0 | ~c7_2(X123,X124) | c8_2(X123,X124) | c1_2(X123,X124) | ~ndr1_1(X123) | ~c7_2(X123,a260) | ndr1_1(X123) | ~ndr1_0 is false, set c5_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c7_0 | ~c7_1(X121) | ndr1_1(X121) | c1_1(X121) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X121) to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c7_0 | ~c7_1(X121) | ~c7_2(X121,a258) | c1_1(X121) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X121) to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c7_0 | ~c7_1(X121) | c3_2(X121,a258) | c1_1(X121) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X121) to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c7_0 | ~c7_1(X121) | c4_2(X121,a258) | c1_1(X121) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X121) to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c8_0 | c7_2(X96,X97) | ~c4_2(X96,X97) | ~c6_2(X96,X97) | ~ndr1_1(X96) | ndr1_1(X96) | c7_1(X96) | ~ndr1_0 | ~c1_0 is false, set c8_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_1(X0) | c4_2(X0,X1) | c3_2(X0,X1) | c6_2(X0,X1) | ~ndr1_1(X0) | c3_1(X0) | ~ndr1_0 | ~sP17 is false, set ~sP17 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c6_1(X149) | ~c3_2(X149,X150) | c7_2(X149,X150) | c5_2(X149,X150) | ~ndr1_1(X149) | ~c2_1(X149) | ~ndr1_0 | ndr1_0 | sP0 is false, set sP0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c1_1(X115) | ~c3_1(X115) | ~ndr1_0 | ndr1_0 | sP5 is false, set sP5 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | sP7 | c6_0 is false, set sP7 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c1_0 | ndr1_0 | sP10 is false, set sP10 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever sP4 | ndr1_0 | ~c1_1(X138) | c5_2(X138,X139) | ~c6_2(X138,X139) | ~ndr1_1(X138) | ~ndr1_0 is false, set sP4 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c3_1(X12) | ~c4_2(X12,X13) | c8_2(X12,X13) | c2_2(X12,X13) | ~ndr1_1(X12) | c2_1(X12) | ~ndr1_0 | ndr1_0 | ~c2_0 is false, set ~c2_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c2_0 | ndr1_1(X110) | ~c8_1(X110) | c2_1(X110) | ~ndr1_0 | ndr1_0 is false, set ~c2_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c2_0 | c3_2(X110,a248) | ~c8_1(X110) | c2_1(X110) | ~ndr1_0 | ndr1_0 is false, set ~c2_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c2_0 | ~c6_2(X110,a248) | ~c8_1(X110) | c2_1(X110) | ~ndr1_0 | ndr1_0 is false, set ~c2_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c2_0 | c7_2(X110,a248) | ~c8_1(X110) | c2_1(X110) | ~ndr1_0 | ndr1_0 is false, set ~c2_0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c3_2(X0,a290) | c7_2(X0,X1) | c5_2(X0,X1) | c3_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c1_2(X0,a290) | c7_2(X0,X1) | c5_2(X0,X1) | c3_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c8_2(X0,a290) | c7_2(X0,X1) | c5_2(X0,X1) | c3_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_1(X0) | c7_2(X0,X1) | c5_2(X0,X1) | c3_2(X0,X1) | ~ndr1_1(X0) | ~c4_2(X0,a291) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_1(X0) | c7_2(X0,X1) | c5_2(X0,X1) | c3_2(X0,X1) | ~ndr1_1(X0) | c2_2(X0,a291) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_1(X0) | c7_2(X0,X1) | c5_2(X0,X1) | c3_2(X0,X1) | ~ndr1_1(X0) | c7_2(X0,a291) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_1(X0) | c7_2(X0,X1) | c5_2(X0,X1) | c3_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c5_2(X0,a239) | ~c5_2(X0,X1) | c8_2(X0,X1) | c7_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_1(X0) | ~c5_2(X0,X1) | c8_2(X0,X1) | c7_2(X0,X1) | ~ndr1_1(X0) | c7_2(X0,a240) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_1(X0) | ~c5_2(X0,X1) | c8_2(X0,X1) | c7_2(X0,X1) | ~ndr1_1(X0) | ~c1_2(X0,a240) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c8_2(X0,a239) | ~c5_2(X0,X1) | c8_2(X0,X1) | c7_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c7_2(X0,a239) | ~c5_2(X0,X1) | c8_2(X0,X1) | c7_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_1(X0) | ~c5_2(X0,X1) | c8_2(X0,X1) | c7_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c2_2(X0,X1) | c7_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c2_1(X0) | ~ndr1_0 | ~sP13 is false, set ~sP13 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever sP11 | ~c1_2(X85,X86) | ~c7_2(X85,X86) | c8_2(X85,X86) | ~ndr1_1(X85) | ndr1_1(X85) | c6_2(X85,X87) | ~c8_2(X85,X87) | ~c4_2(X85,X87) | ~ndr1_1(X85) | ~ndr1_0 | c4_0 is false, set sP11 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever sP15 | ndr1_0 | c2_2(X54,X55) | c4_2(X54,X55) | c1_2(X54,X55) | ~ndr1_1(X54) | ~c3_2(X54,X56) | c6_2(X54,X56) | ~c8_2(X54,X56) | ~ndr1_1(X54) | ~c7_1(X54) | ~ndr1_0 is false, set sP15 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | ~sP15 is false, set ~sP15 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | ~sP14 is false, set ~sP14 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever c1_1(a199) | ndr1_0 | sP13 is false, set sP13 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | c6_1(a200) | sP13 is false, set sP13 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | ~c1_1(a200) | sP13 is false, set sP13 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | ~c8_2(a174,X33) | ~c5_2(a174,X33) | c6_2(a174,X33) | ~ndr1_1(a174) | sP17 is false, set sP17 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | c5_1(a174) | sP17 is false, set sP17 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c8_2(a173,X31) | ~c1_2(a173,X31) | ~ndr1_1(a173) | ndr1_0 | sP17 is false, set sP17 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | ~c3_1(a174) | sP17 is false, set sP17 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c6_1(a173) | ndr1_0 | sP17 is false, set sP17 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ~c7_2(a173,X32) | c8_2(a173,X32) | c5_2(a173,X32) | ~ndr1_1(a173) | ndr1_0 | sP17 is false, set sP17 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | ndr1_0 | sP17 is false, set sP17 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | ndr1_0 | sP13 is false, set sP13 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | ~sP4 is false, set ~sP4 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | ~sP11 is false, set ~sP11 to true
% 9.44/2.11 for all groundings,
% 9.44/2.11 whenever ndr1_0 | ~sP12 is false, set ~sP12 to true
% 9.44/2.11 % SZS output end Definitions and Model Updates.
% 9.44/2.11 % (2535283)------------------------------
% 9.44/2.11 % (2535283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.11 % (2535283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.11 % (2535283)CaDiCaL version: 2.1.3
% 9.44/2.11 % (2535283)Termination reason: Satisfiable
% 9.44/2.11 % (2535283)Time elapsed: 0.814 s
% 9.44/2.11 % (2535283)Peak memory usage: 133 MB
% 9.44/2.11 % (2535283)Instructions burned: 1233 (million)
% 9.44/2.11 % (2535283)------------------------------
% 9.44/2.11 % (2535283)------------------------------
% 9.44/2.11 % (2535158)Success in time 1.262 s
% 9.44/2.11 % Vampire exiting
%------------------------------------------------------------------------------