%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN544+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 : n002.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:54 PM UTC 2026
% Result : CounterSatisfiable 9.65s 2.11s
% Output : Saturation 9.65s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u794,negated_conjecture,
c7_0 ).
cnf(u841,negated_conjecture,
~ ndr1_1(a120) ).
cnf(u859,negated_conjecture,
~ c5_1(a120) ).
cnf(u900,negated_conjecture,
~ c8_0 ).
cnf(u1124,negated_conjecture,
~ c5_0 ).
cnf(u909,negated_conjecture,
( ~ c4_2(a103,X107)
| ~ c5_2(a103,X107)
| c8_2(a103,X107) ) ).
cnf(u917,negated_conjecture,
( c5_2(a103,X106)
| c1_2(a103,X106)
| c4_2(a103,X106) ) ).
cnf(u963,negated_conjecture,
sP5 ).
cnf(u991,negated_conjecture,
~ c1_0 ).
cnf(u994,negated_conjecture,
c7_1(a81) ).
cnf(u998,negated_conjecture,
~ c6_1(a81) ).
cnf(u1002,negated_conjecture,
c3_2(a81,a82) ).
cnf(u1006,negated_conjecture,
c8_2(a81,a82) ).
cnf(u1010,negated_conjecture,
c4_2(a81,a82) ).
cnf(u1014,negated_conjecture,
ndr1_1(a81) ).
cnf(u1066,negated_conjecture,
~ c3_1(a66) ).
cnf(u1073,negated_conjecture,
~ ndr1_1(a66) ).
cnf(u1483,negated_conjecture,
~ sP7 ).
cnf(u1130,negated_conjecture,
c8_1(a52) ).
cnf(u1137,negated_conjecture,
( ~ c8_2(a52,X49)
| ~ c7_2(a52,X49)
| ~ c5_2(a52,X49) ) ).
cnf(u1141,negated_conjecture,
c5_1(a52) ).
cnf(u1150,negated_conjecture,
c7_2(a47,a49) ).
cnf(u1154,negated_conjecture,
~ c1_2(a47,a49) ).
cnf(u1158,negated_conjecture,
~ c2_2(a47,a49) ).
cnf(u1162,negated_conjecture,
ndr1_1(a47) ).
cnf(u1166,negated_conjecture,
~ c6_1(a47) ).
cnf(u1170,negated_conjecture,
~ c1_2(a47,a48) ).
cnf(u1174,negated_conjecture,
c8_2(a47,a48) ).
cnf(u1178,negated_conjecture,
~ c2_2(a47,a48) ).
cnf(u1537,negated_conjecture,
~ sP9 ).
cnf(u1572,negated_conjecture,
~ sP10 ).
cnf(u1198,negated_conjecture,
~ c4_1(a35) ).
cnf(u1202,negated_conjecture,
~ c4_2(a35,a36) ).
cnf(u1206,negated_conjecture,
~ c3_2(a35,a36) ).
cnf(u1210,negated_conjecture,
~ c2_2(a35,a36) ).
cnf(u1214,negated_conjecture,
ndr1_1(a35) ).
cnf(u1219,negated_conjecture,
( ~ c2_2(a35,X35)
| c8_2(a35,X35)
| ~ c1_2(a35,X35) ) ).
cnf(u1631,negated_conjecture,
~ sP12 ).
cnf(u1241,negated_conjecture,
~ c4_2(a27,a28) ).
cnf(u1597,negated_conjecture,
~ sP11 ).
cnf(u1248,negated_conjecture,
c2_2(a27,a28) ).
cnf(u1252,negated_conjecture,
~ c6_2(a27,a28) ).
cnf(u1256,negated_conjecture,
ndr1_1(a27) ).
cnf(u1261,negated_conjecture,
( c5_2(a27,X28)
| ~ c7_2(a27,X28)
| c8_2(a27,X28) ) ).
cnf(u1265,negated_conjecture,
c8_1(a27) ).
cnf(u1317,axiom,
~ sP0 ).
cnf(u1340,axiom,
~ sP1 ).
cnf(u1343,axiom,
~ c6_1(a129) ).
cnf(u1347,axiom,
c8_2(a129,a131) ).
cnf(u1351,axiom,
~ c7_2(a129,a131) ).
cnf(u1355,axiom,
c1_2(a129,a131) ).
cnf(u1363,axiom,
c3_2(a129,a130) ).
cnf(u1367,axiom,
~ c8_2(a129,a130) ).
cnf(u1371,axiom,
~ c6_2(a129,a130) ).
cnf(u1376,axiom,
~ sP2 ).
cnf(u1417,axiom,
~ sP4 ).
cnf(u1451,axiom,
c7_1(a85) ).
cnf(u1455,axiom,
c7_2(a85,a86) ).
cnf(u1459,axiom,
~ c1_2(a85,a86) ).
cnf(u1463,axiom,
~ c8_2(a85,a86) ).
cnf(u1467,axiom,
ndr1_1(a85) ).
cnf(u1471,axiom,
~ c4_1(a85) ).
cnf(u1515,axiom,
~ sP8 ).
cnf(u1518,axiom,
~ ndr1_1(a44) ).
cnf(u1521,axiom,
( ~ c4_2(a44,X0)
| ~ c5_2(a44,X0) ) ).
cnf(u1525,axiom,
~ c8_2(a44,a45) ).
cnf(u1529,axiom,
c5_2(a44,a45) ).
cnf(u1535,axiom,
~ c2_1(a44) ).
cnf(u1600,axiom,
~ c6_2(a24,a26) ).
cnf(u1608,axiom,
~ c7_2(a24,a26) ).
cnf(u3690,axiom,
~ ndr1_1(a24) ).
cnf(u1616,axiom,
~ c2_1(a24) ).
cnf(u1620,axiom,
c1_2(a24,a25) ).
cnf(u1624,axiom,
c3_2(a24,a25) ).
cnf(u1628,axiom,
~ c6_2(a24,a25) ).
cnf(u1634,axiom,
~ ndr1_1(a29) ).
cnf(u1637,axiom,
( ~ c6_2(a29,X0)
| c5_2(a29,X0)
| c1_2(a29,X0) ) ).
cnf(u1641,axiom,
c6_2(a29,a31) ).
cnf(u1645,axiom,
c5_2(a29,a31) ).
cnf(u1651,axiom,
c1_2(a29,a30) ).
cnf(u1655,axiom,
c2_2(a29,a30) ).
cnf(u1659,axiom,
c7_2(a29,a30) ).
cnf(u1664,axiom,
~ sP13 ).
cnf(u1691,axiom,
~ sP14 ).
cnf(u1734,negated_conjecture,
ndr1_1(a134) ).
cnf(u1720,negated_conjecture,
( c1_2(a134,X144)
| c8_2(a134,X144) ) ).
cnf(u1724,negated_conjecture,
c3_2(a134,a135) ).
cnf(u1728,negated_conjecture,
c8_2(a134,a135) ).
cnf(u1732,negated_conjecture,
~ c4_2(a134,a135) ).
cnf(u1738,negated_conjecture,
~ c1_1(a134) ).
cnf(u1742,negated_conjecture,
( ~ c1_1(X141)
| ~ ndr1_1(X141)
| ~ c8_2(X141,X142)
| c7_2(X141,X142)
| ~ c4_2(X141,X142)
| ~ c6_2(X141,a132) ) ).
cnf(u1746,negated_conjecture,
( ~ c8_2(X141,a132)
| ~ ndr1_1(X141)
| ~ c8_2(X141,X142)
| c7_2(X141,X142)
| ~ c4_2(X141,X142)
| ~ c1_1(X141) ) ).
cnf(u1750,negated_conjecture,
( ~ c1_1(X141)
| ~ ndr1_1(X141)
| ~ c8_2(X141,X142)
| c7_2(X141,X142)
| ~ c4_2(X141,X142)
| ~ c3_2(X141,a132) ) ).
cnf(u1757,negated_conjecture,
( ~ c1_1(X138)
| ~ ndr1_1(X138)
| c3_2(X138,X139)
| ~ c2_2(X138,X139)
| c7_2(X138,X139)
| ~ c8_1(X138) ) ).
cnf(u1782,negated_conjecture,
~ c5_1(a127) ).
cnf(u1785,negated_conjecture,
( ~ ndr1_1(X133)
| c6_2(X133,X135)
| c8_2(X133,X135)
| ~ c7_2(X133,X135)
| ~ c4_1(X133)
| c4_2(X133,X134)
| c3_2(X133,X134)
| ~ c8_2(X133,X134) ) ).
cnf(u1789,negated_conjecture,
c3_1(a127) ).
cnf(u1801,negated_conjecture,
( ~ ndr1_1(X123)
| c7_1(X123)
| c1_2(X123,X124)
| c6_2(X123,X124)
| ~ c4_2(X123,X124)
| c4_1(X123) ) ).
cnf(u1804,negated_conjecture,
( ~ c5_2(X122,a116)
| c4_1(X122)
| c8_1(X122) ) ).
cnf(u1808,negated_conjecture,
( c1_2(X122,a116)
| c4_1(X122)
| c8_1(X122) ) ).
cnf(u1812,negated_conjecture,
( c2_2(X122,a116)
| c4_1(X122)
| c8_1(X122) ) ).
cnf(u1827,negated_conjecture,
~ ndr1_1(a113) ).
cnf(u1853,negated_conjecture,
~ c8_1(a113) ).
cnf(u1863,negated_conjecture,
~ ndr1_1(a104) ).
cnf(u1873,negated_conjecture,
~ c5_1(a104) ).
cnf(u1877,negated_conjecture,
( ~ c8_1(X108)
| c4_1(X108)
| c6_1(X108) ) ).
cnf(u2464,negated_conjecture,
~ sP3 ).
cnf(u1888,negated_conjecture,
( ~ ndr1_1(X104)
| c5_2(X104,a100)
| c4_2(X104,X105)
| ~ c2_2(X104,X105)
| c7_2(X104,X105)
| c8_1(X104) ) ).
cnf(u1896,negated_conjecture,
( c4_1(X103)
| c3_1(X103)
| ~ c1_1(X103) ) ).
cnf(u1903,negated_conjecture,
( ~ c2_1(X98)
| ~ ndr1_1(X98)
| ~ c5_2(X98,X99)
| c3_2(X98,X99)
| ~ c1_2(X98,X99)
| c7_1(X98) ) ).
cnf(u1927,negated_conjecture,
( ~ c5_1(X91)
| c1_1(X91)
| c4_1(X91) ) ).
cnf(u1967,negated_conjecture,
~ ndr1_1(a93) ).
cnf(u2004,negated_conjecture,
( ~ c2_1(X85)
| ~ ndr1_1(X85)
| ~ c6_2(X85,X86)
| c1_2(X85,X86)
| c4_2(X85,X86)
| c3_1(X85) ) ).
cnf(u2039,negated_conjecture,
( ~ c3_1(X77)
| ~ ndr1_1(X77)
| c1_2(X77,X78)
| c7_2(X77,X78)
| ~ c3_2(X77,X78)
| c7_1(X77) ) ).
cnf(u2044,negated_conjecture,
( c5_2(X69,a71)
| c4_1(X69)
| c7_2(X69,a72) ) ).
cnf(u2048,negated_conjecture,
( c5_2(X69,a71)
| c4_1(X69)
| c8_2(X69,a72) ) ).
cnf(u2052,negated_conjecture,
( c5_2(X69,a71)
| c4_1(X69)
| ~ c1_2(X69,a72) ) ).
cnf(u2060,negated_conjecture,
( ~ c3_2(X69,a71)
| c4_1(X69)
| c8_2(X69,a72) ) ).
cnf(u2064,negated_conjecture,
( ~ c1_2(X69,a72)
| c4_1(X69)
| ~ c3_2(X69,a71) ) ).
cnf(u2068,negated_conjecture,
( ~ c1_2(X69,a71)
| c4_1(X69)
| c7_2(X69,a72) ) ).
cnf(u2072,negated_conjecture,
( ~ c1_2(X69,a71)
| c4_1(X69)
| c8_2(X69,a72) ) ).
cnf(u2076,negated_conjecture,
( ~ c1_2(X69,a72)
| c4_1(X69)
| ~ c1_2(X69,a71) ) ).
cnf(u2092,negated_conjecture,
( c5_2(X68,a69)
| ~ c6_2(X68,a70)
| ~ c3_1(X68) ) ).
cnf(u2096,negated_conjecture,
( ~ c3_1(X68)
| c4_2(X68,a70)
| ~ c6_2(X68,a69) ) ).
cnf(u2100,negated_conjecture,
( ~ c6_2(X68,a69)
| c7_2(X68,a70)
| ~ c3_1(X68) ) ).
cnf(u2104,negated_conjecture,
( ~ c3_1(X68)
| ~ c6_2(X68,a70)
| ~ c6_2(X68,a69) ) ).
cnf(u2108,negated_conjecture,
( ~ c3_1(X68)
| c4_2(X68,a70)
| ~ c1_2(X68,a69) ) ).
cnf(u2112,negated_conjecture,
( ~ c3_1(X68)
| c7_2(X68,a70)
| ~ c1_2(X68,a69) ) ).
cnf(u2116,negated_conjecture,
( ~ c3_1(X68)
| ~ c6_2(X68,a70)
| ~ c1_2(X68,a69) ) ).
cnf(u2120,negated_conjecture,
( ~ c3_1(X68)
| ndr1_1(X68) ) ).
cnf(u2124,negated_conjecture,
c5_1(a68) ).
cnf(u2127,negated_conjecture,
( ~ c7_2(X66,a67)
| c2_1(X66)
| c6_1(X66) ) ).
cnf(u2138,negated_conjecture,
c2_1(a68) ).
cnf(u2142,negated_conjecture,
( ~ c4_2(X66,a67)
| c2_1(X66)
| c6_1(X66) ) ).
cnf(u2148,negated_conjecture,
( ndr1_1(X66)
| c2_1(X66)
| c6_1(X66) ) ).
cnf(u2166,negated_conjecture,
( ~ c3_1(X55)
| ~ ndr1_1(X55)
| c6_2(X55,X56)
| c5_2(X55,X56)
| ~ c3_2(X55,X56)
| ~ c2_1(X55) ) ).
cnf(u2501,negated_conjecture,
~ sP6 ).
cnf(u2212,negated_conjecture,
( ~ c6_2(X50,X51)
| c7_2(X50,a56)
| ~ ndr1_1(X50)
| c5_1(X50)
| ~ c1_2(X50,X51)
| ~ c4_2(X50,X51) ) ).
cnf(u2216,negated_conjecture,
( ~ c2_2(X50,a56)
| c5_1(X50)
| ~ ndr1_1(X50)
| ~ c6_2(X50,X51)
| ~ c1_2(X50,X51)
| ~ c4_2(X50,X51) ) ).
cnf(u2220,negated_conjecture,
( ~ c6_2(X50,X51)
| c3_2(X50,a56)
| ~ ndr1_1(X50)
| c5_1(X50)
| ~ c1_2(X50,X51)
| ~ c4_2(X50,X51) ) ).
cnf(u2224,negated_conjecture,
( ~ c6_1(X47)
| c1_1(X47)
| ~ ndr1_1(X47)
| ~ c3_2(X47,X48)
| ~ c6_2(X47,X48)
| c4_2(X47,X48) ) ).
cnf(u2238,negated_conjecture,
( ~ c6_2(X39,X40)
| ~ c7_1(X39)
| ~ c3_2(X39,a46)
| ~ ndr1_1(X39)
| c5_2(X39,X40)
| c4_2(X39,X40) ) ).
cnf(u2243,negated_conjecture,
( ~ c8_2(X39,a46)
| ~ c7_1(X39)
| c4_2(X39,X40)
| ~ ndr1_1(X39)
| c5_2(X39,X40)
| ~ c6_2(X39,X40) ) ).
cnf(u2253,negated_conjecture,
( ~ c2_2(X36,X37)
| c7_1(X36)
| ~ c8_1(X36)
| ~ ndr1_1(X36)
| ~ c6_2(X36,X37)
| c3_2(X36,X37) ) ).
cnf(u2282,negated_conjecture,
c2_1(a32) ).
cnf(u2315,negated_conjecture,
( ~ c2_2(X26,a23)
| ~ ndr1_1(X26)
| ~ c5_2(X26,X27)
| c1_2(X26,X27)
| ~ c8_2(X26,X27)
| ~ c6_2(X26,a22) ) ).
cnf(u2319,negated_conjecture,
( ~ c6_2(X26,a22)
| ~ ndr1_1(X26)
| ~ c5_2(X26,X27)
| c1_2(X26,X27)
| ~ c8_2(X26,X27)
| ~ c3_2(X26,a23) ) ).
cnf(u2323,negated_conjecture,
( ~ c6_2(X26,a23)
| ~ ndr1_1(X26)
| ~ c5_2(X26,X27)
| c1_2(X26,X27)
| ~ c8_2(X26,X27)
| ~ c6_2(X26,a22) ) ).
cnf(u2327,negated_conjecture,
( ~ c2_2(X26,a23)
| ~ ndr1_1(X26)
| ~ c5_2(X26,X27)
| c1_2(X26,X27)
| ~ c8_2(X26,X27)
| ~ c7_2(X26,a22) ) ).
cnf(u2331,negated_conjecture,
( ~ c7_2(X26,a22)
| ~ ndr1_1(X26)
| ~ c5_2(X26,X27)
| c1_2(X26,X27)
| ~ c8_2(X26,X27)
| ~ c3_2(X26,a23) ) ).
cnf(u2335,negated_conjecture,
( ~ c6_2(X26,a23)
| ~ ndr1_1(X26)
| ~ c5_2(X26,X27)
| c1_2(X26,X27)
| ~ c8_2(X26,X27)
| ~ c7_2(X26,a22) ) ).
cnf(u2350,negated_conjecture,
~ c8_1(a16) ).
cnf(u2354,negated_conjecture,
~ c2_1(a16) ).
cnf(u2373,negated_conjecture,
( ~ ndr1_1(X6)
| c3_2(X6,a7)
| c3_2(X6,X7)
| c4_2(X6,X7)
| ~ c2_2(X6,X7)
| ~ c8_1(X6) ) ).
cnf(u2380,negated_conjecture,
( c3_2(X6,X7)
| ~ ndr1_1(X6)
| c6_2(X6,a7)
| c4_2(X6,X7)
| ~ c2_2(X6,X7)
| ~ c8_1(X6) ) ).
cnf(u2384,negated_conjecture,
( c3_2(X6,X7)
| ~ ndr1_1(X6)
| c1_2(X6,a7)
| c4_2(X6,X7)
| ~ c2_2(X6,X7)
| ~ c8_1(X6) ) ).
cnf(u2467,negated_conjecture,
( ~ c4_2(X0,a102)
| c2_2(X0,X1)
| c4_2(X0,a101)
| ~ ndr1_1(X0)
| c4_2(X0,X1) ) ).
cnf(u2471,negated_conjecture,
( ~ c1_2(X0,a102)
| c2_2(X0,X1)
| c4_2(X0,a101)
| ~ ndr1_1(X0)
| c4_2(X0,X1) ) ).
cnf(u2479,negated_conjecture,
( ~ c2_2(X0,a101)
| ~ c4_2(X0,a102)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| c4_2(X0,X1) ) ).
cnf(u2483,negated_conjecture,
( ~ c2_2(X0,a101)
| ~ c1_2(X0,a102)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| c4_2(X0,X1) ) ).
cnf(u2487,negated_conjecture,
( ~ c2_2(X0,a101)
| c7_2(X0,a102)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| c4_2(X0,X1) ) ).
cnf(u2491,negated_conjecture,
( ~ c4_2(X0,a102)
| c2_2(X0,X1)
| c7_2(X0,a101)
| ~ ndr1_1(X0)
| c4_2(X0,X1) ) ).
cnf(u2495,negated_conjecture,
( ~ c1_2(X0,a102)
| c2_2(X0,X1)
| c7_2(X0,a101)
| ~ ndr1_1(X0)
| c4_2(X0,X1) ) ).
cnf(u2541,negated_conjecture,
( ~ c8_1(X121)
| ~ c8_2(X121,a115) ) ).
cnf(u2545,negated_conjecture,
( ~ c8_1(X121)
| ~ c7_2(X121,a115) ) ).
cnf(u2549,negated_conjecture,
( ~ c8_1(X121)
| ~ c3_2(X121,a115) ) ).
cnf(u2553,negated_conjecture,
( ~ c8_1(X121)
| ndr1_1(X121) ) ).
cnf(u2557,negated_conjecture,
~ c1_2(a96,a97) ).
cnf(u2564,negated_conjecture,
~ c6_2(a96,a97) ).
cnf(u2568,negated_conjecture,
c7_2(a96,a97) ).
cnf(u2572,negated_conjecture,
ndr1_1(a96) ).
cnf(u2576,negated_conjecture,
c3_1(a96) ).
cnf(u2580,negated_conjecture,
c2_1(a96) ).
cnf(u2584,negated_conjecture,
( ~ c2_1(X74)
| c7_1(X74)
| c3_1(X74) ) ).
cnf(u2588,negated_conjecture,
~ ndr1_1(a64) ).
cnf(u2598,negated_conjecture,
~ c1_1(a64) ).
cnf(u2627,negated_conjecture,
( c5_2(a59,X52)
| c7_2(a59,X52) ) ).
cnf(u2631,negated_conjecture,
~ ndr1_1(a51) ).
cnf(u2638,negated_conjecture,
( ~ c5_1(X44)
| c2_1(X44)
| c6_1(X44) ) ).
cnf(u2643,negated_conjecture,
~ ndr1_1(a34) ).
cnf(u2658,negated_conjecture,
c1_1(a18) ).
cnf(u2665,negated_conjecture,
c6_1(a18) ).
cnf(u2693,negated_conjecture,
( ~ c4_2(X10,X12)
| ~ c8_2(X10,X11)
| ~ c2_2(X10,X12)
| ~ c8_2(X10,X12)
| c7_1(X10)
| ~ ndr1_1(X10)
| c7_2(X10,X11) ) ).
cnf(u2703,negated_conjecture,
~ c4_1(a81) ).
cnf(u2715,negated_conjecture,
c6_1(a27) ).
cnf(u2718,negated_conjecture,
c4_1(a27) ).
cnf(u2746,negated_conjecture,
~ c4_1(a47) ).
cnf(u2741,negated_conjecture,
c7_1(a47) ).
cnf(u2759,negated_conjecture,
~ c7_2(a27,a116) ).
cnf(u2783,negated_conjecture,
~ c6_2(a103,a70) ).
cnf(u3239,negated_conjecture,
~ c8_1(a81) ).
cnf(u2809,negated_conjecture,
c4_2(a81,a100) ).
cnf(u2819,negated_conjecture,
( ~ c8_2(a103,X0)
| ~ c5_2(a103,X0) ) ).
cnf(u2837,negated_conjecture,
c5_2(a81,a100) ).
cnf(u2841,negated_conjecture,
c2_2(a81,a100) ).
cnf(u2850,negated_conjecture,
c6_1(a52) ).
cnf(u5288,negated_conjecture,
~ c4_1(a52) ).
cnf(u2862,negated_conjecture,
c1_1(a52) ).
cnf(u2869,negated_conjecture,
c2_1(a52) ).
cnf(u2876,negated_conjecture,
c8_1(a35) ).
cnf(u2928,negated_conjecture,
( c3_2(a81,X1)
| c4_2(a81,X1)
| c6_2(a81,X1) ) ).
cnf(u2944,negated_conjecture,
c7_1(a35) ).
cnf(u2951,negated_conjecture,
( c3_2(a35,X1)
| c4_2(a35,X1)
| c6_2(a35,X1) ) ).
cnf(u2964,negated_conjecture,
( ~ c1_2(a35,X0)
| c4_2(a35,X0)
| c2_2(a35,X0) ) ).
cnf(u2967,negated_conjecture,
c6_1(a35) ).
cnf(u4192,negated_conjecture,
~ c1_1(a35) ).
cnf(u2975,negated_conjecture,
( ~ c1_2(a81,X0)
| c4_2(a81,X0)
| c2_2(a81,X0) ) ).
cnf(u4275,negated_conjecture,
~ c1_1(a81) ).
cnf(u2988,negated_conjecture,
c6_1(a122) ).
cnf(u3885,negated_conjecture,
~ c4_1(a122) ).
cnf(u5296,negated_conjecture,
~ c4_1(a136) ).
cnf(u3018,negated_conjecture,
c4_2(a81,a71) ).
cnf(u3025,negated_conjecture,
c6_2(a35,a71) ).
cnf(u3056,negated_conjecture,
~ c4_2(a35,a71) ).
cnf(u3039,negated_conjecture,
c8_2(a136,a72) ).
cnf(u3083,negated_conjecture,
c6_1(a24) ).
cnf(u4791,negated_conjecture,
~ c8_1(a24) ).
cnf(u4144,negated_conjecture,
c4_1(a24) ).
cnf(u3142,negated_conjecture,
~ c4_2(a29,a31) ).
cnf(u3169,negated_conjecture,
c6_1(a29) ).
cnf(u4779,negated_conjecture,
~ c8_1(a29) ).
cnf(u3250,negated_conjecture,
( ~ c2_2(a35,X0)
| c3_2(a35,X0)
| c4_2(a35,X0) ) ).
cnf(u3270,negated_conjecture,
~ ndr1_1(a16) ).
cnf(u3748,negated_conjecture,
~ c1_1(a85) ).
cnf(u3372,negated_conjecture,
~ c8_1(a85) ).
cnf(u3388,negated_conjecture,
( c5_2(a85,X0)
| c8_2(a85,X0)
| c1_2(a85,X0) ) ).
cnf(u3393,negated_conjecture,
( ~ c2_2(a85,X0)
| c7_2(a85,X0)
| c4_2(a85,X0) ) ).
cnf(u3419,negated_conjecture,
~ c1_2(a96,a69) ).
cnf(u3434,negated_conjecture,
~ c6_2(a96,a69) ).
cnf(u3439,negated_conjecture,
c5_2(a96,a69) ).
cnf(u3446,negated_conjecture,
c7_1(a96) ).
cnf(u3523,negated_conjecture,
c8_1(a96) ).
cnf(u4908,negated_conjecture,
~ c1_2(a96,a7) ).
cnf(u3463,negated_conjecture,
( ~ c2_2(a96,X0)
| c5_2(a96,X0)
| c4_2(a96,X0)
| c6_2(a96,X0) ) ).
cnf(u3467,negated_conjecture,
c6_2(a96,a7) ).
cnf(u3486,negated_conjecture,
~ c4_1(a96) ).
cnf(u3493,negated_conjecture,
( ~ c2_2(a96,X0)
| c7_2(a96,X0)
| c4_2(a96,X0) ) ).
cnf(u3521,negated_conjecture,
c3_2(a96,a7) ).
cnf(u3533,negated_conjecture,
c3_1(a32) ).
cnf(u3536,negated_conjecture,
c7_1(a32) ).
cnf(u3552,negated_conjecture,
~ c1_2(a32,a69) ).
cnf(u3567,negated_conjecture,
~ c6_2(a32,a69) ).
cnf(u3572,negated_conjecture,
c5_2(a32,a69) ).
cnf(u3585,negated_conjecture,
( c3_2(a27,X1)
| c4_2(a27,X1)
| c6_2(a27,X1) ) ).
cnf(u3599,negated_conjecture,
( ~ c7_2(a27,X0)
| c6_2(a27,X0)
| c8_2(a27,X0) ) ).
cnf(u3603,negated_conjecture,
( c3_2(a27,X0)
| ~ c2_2(a27,X0)
| c4_2(a27,X0) ) ).
cnf(u3615,negated_conjecture,
c6_2(a27,a71) ).
cnf(u3630,negated_conjecture,
~ c4_2(a27,a71) ).
cnf(u3624,negated_conjecture,
~ c2_2(a27,a71) ).
cnf(u5307,negated_conjecture,
~ c5_1(a27) ).
cnf(u3653,negated_conjecture,
~ c3_2(a52,a132) ).
cnf(u3660,negated_conjecture,
~ c6_2(a52,a132) ).
cnf(u3682,negated_conjecture,
c7_2(a27,a28) ).
cnf(u3685,negated_conjecture,
c1_1(a27) ).
cnf(u3701,negated_conjecture,
c4_1(a68) ).
cnf(u3715,negated_conjecture,
c3_1(a52) ).
cnf(u3729,negated_conjecture,
c1_1(a51) ).
cnf(u3733,negated_conjecture,
c6_1(a51) ).
cnf(u5254,negated_conjecture,
~ c2_1(a51) ).
cnf(u3757,negated_conjecture,
( ~ c2_2(a81,X0)
| c5_2(a81,X0)
| c8_2(a81,X0) ) ).
cnf(u3788,negated_conjecture,
~ c1_2(a59,a69) ).
cnf(u3803,negated_conjecture,
~ c6_2(a59,a69) ).
cnf(u3808,negated_conjecture,
c5_2(a59,a69) ).
cnf(u3813,negated_conjecture,
~ c2_1(a59) ).
cnf(u3821,negated_conjecture,
c7_1(a59) ).
cnf(u3832,negated_conjecture,
c8_1(a59) ).
cnf(u3895,negated_conjecture,
c3_2(a122,a7) ).
cnf(u3955,negated_conjecture,
c5_2(a27,a71) ).
cnf(u3962,negated_conjecture,
c5_2(a35,a36) ).
cnf(u3969,negated_conjecture,
c5_2(a35,a71) ).
cnf(u4005,negated_conjecture,
c7_2(a85,a116) ).
cnf(u4012,negated_conjecture,
c1_1(a136) ).
cnf(u4016,negated_conjecture,
c6_1(a136) ).
cnf(u5971,negated_conjecture,
~ c2_1(a136) ).
cnf(u5617,negated_conjecture,
c7_1(a136) ).
cnf(u4033,negated_conjecture,
( ~ c4_2(a136,X0)
| ~ c2_2(a136,X0)
| ~ c5_2(a136,X0) ) ).
cnf(u4037,negated_conjecture,
~ c3_2(a136,a132) ).
cnf(u4044,negated_conjecture,
~ c6_2(a136,a132) ).
cnf(u4059,negated_conjecture,
~ c1_2(a52,a69) ).
cnf(u4074,negated_conjecture,
~ c6_2(a52,a69) ).
cnf(u4079,negated_conjecture,
c5_2(a52,a69) ).
cnf(u4088,negated_conjecture,
~ ndr1_1(a18) ).
cnf(u4116,negated_conjecture,
~ c5_2(a129,a131) ).
cnf(u4121,negated_conjecture,
c6_2(a136,a108) ).
cnf(u4124,negated_conjecture,
~ c5_2(a136,a72) ).
cnf(u4128,negated_conjecture,
~ c5_2(a47,a48) ).
cnf(u4136,negated_conjecture,
~ c2_2(a129,a131) ).
cnf(u4161,negated_conjecture,
( ~ c4_2(a27,X0)
| ~ c2_2(a27,X0)
| ~ c5_2(a27,X0) ) ).
cnf(u4171,negated_conjecture,
( ~ c8_2(a27,X0)
| ~ c4_2(a27,X0)
| c7_2(a27,X0) ) ).
cnf(u4175,negated_conjecture,
~ c6_2(a27,a132) ).
cnf(u4227,negated_conjecture,
c6_2(a35,a115) ).
cnf(u4230,negated_conjecture,
c4_2(a35,a115) ).
cnf(u4241,negated_conjecture,
~ c1_2(a35,a115) ).
cnf(u4253,negated_conjecture,
c7_2(a136,a132) ).
cnf(u4292,negated_conjecture,
c4_2(a136,a100) ).
cnf(u4296,negated_conjecture,
c5_2(a136,a100) ).
cnf(u4375,negated_conjecture,
c7_2(a81,a102) ).
cnf(u4385,negated_conjecture,
c7_2(a59,a102) ).
cnf(u4405,negated_conjecture,
c7_2(a35,a102) ).
cnf(u4432,negated_conjecture,
c6_1(a117) ).
cnf(u4742,negated_conjecture,
~ c4_1(a117) ).
cnf(u4450,negated_conjecture,
( ~ c2_2(a47,X0)
| c7_2(a47,X0)
| c4_2(a47,X0) ) ).
cnf(u4488,negated_conjecture,
~ c2_1(a127) ).
cnf(u4498,negated_conjecture,
~ c1_2(a127,a69) ).
cnf(u4513,negated_conjecture,
~ c6_2(a127,a69) ).
cnf(u4518,negated_conjecture,
c5_2(a127,a69) ).
cnf(u4524,negated_conjecture,
c7_1(a127) ).
cnf(u5336,negated_conjecture,
~ c4_1(a127) ).
cnf(u4550,negated_conjecture,
c3_1(a68) ).
cnf(u4553,negated_conjecture,
c7_1(a68) ).
cnf(u4574,negated_conjecture,
c7_2(a136,a101) ).
cnf(u4578,negated_conjecture,
c7_2(a122,a101) ).
cnf(u4582,negated_conjecture,
c7_2(a96,a101) ).
cnf(u4586,negated_conjecture,
c7_2(a85,a101) ).
cnf(u4598,negated_conjecture,
c7_2(a52,a101) ).
cnf(u4605,negated_conjecture,
c7_2(a47,a101) ).
cnf(u4616,negated_conjecture,
c7_2(a27,a101) ).
cnf(u4759,negated_conjecture,
~ c5_1(a47) ).
cnf(u5047,negated_conjecture,
~ c1_1(a47) ).
cnf(u4681,negated_conjecture,
~ c1_2(a68,a69) ).
cnf(u4684,negated_conjecture,
~ c6_2(a68,a70) ).
cnf(u4688,negated_conjecture,
c7_2(a68,a70) ).
cnf(u4692,negated_conjecture,
c4_2(a68,a70) ).
cnf(u4706,negated_conjecture,
( ~ c1_2(a68,X0)
| ~ c5_2(a68,X0)
| c3_2(a68,X0) ) ).
cnf(u4715,negated_conjecture,
( ~ c3_2(a68,X0)
| c1_2(a68,X0)
| c7_2(a68,X0) ) ).
cnf(u4731,negated_conjecture,
~ c8_2(a68,a70) ).
cnf(u4749,negated_conjecture,
( ~ c3_2(a117,X0)
| c4_2(a117,X0)
| ~ c6_2(a117,X0) ) ).
cnf(u5482,negated_conjecture,
~ c1_1(a117) ).
cnf(u4767,negated_conjecture,
~ c6_2(a122,a7) ).
cnf(u4802,negated_conjecture,
c3_2(a27,a28) ).
cnf(u4847,negated_conjecture,
c4_2(a47,a116) ).
cnf(u4889,negated_conjecture,
~ c1_1(a113) ).
cnf(u4924,negated_conjecture,
~ c3_2(a96,a46) ).
cnf(u4973,negated_conjecture,
c7_2(a129,a102) ).
cnf(u4990,negated_conjecture,
c4_2(a27,a115) ).
cnf(u4994,negated_conjecture,
~ c2_2(a27,a115) ).
cnf(u5009,negated_conjecture,
c6_1(a120) ).
cnf(u5021,negated_conjecture,
~ c3_2(a68,a23) ).
cnf(u5057,negated_conjecture,
( ~ c3_2(a59,X0)
| c4_2(a59,X0)
| ~ c6_2(a59,X0) ) ).
cnf(u5075,negated_conjecture,
c4_1(a32) ).
cnf(u5109,negated_conjecture,
~ c5_1(a32) ).
cnf(u5124,negated_conjecture,
c7_2(a32,a102) ).
cnf(u5129,negated_conjecture,
( ~ c8_2(a32,X1)
| c4_2(a32,X1)
| c3_2(a32,X1) ) ).
cnf(u5142,negated_conjecture,
c1_1(a96) ).
cnf(u5154,negated_conjecture,
~ c3_2(a96,a132) ).
cnf(u5161,negated_conjecture,
~ c6_2(a96,a132) ).
cnf(u5189,negated_conjecture,
c8_2(a27,a101) ).
cnf(u5216,negated_conjecture,
~ c1_2(a51,a69) ).
cnf(u5223,negated_conjecture,
c7_2(a51,a70) ).
cnf(u5227,negated_conjecture,
c4_2(a51,a70) ).
cnf(u5231,negated_conjecture,
~ c6_2(a51,a69) ).
cnf(u5245,negated_conjecture,
~ c3_2(a51,a132) ).
cnf(u5252,negated_conjecture,
~ c6_2(a51,a132) ).
cnf(u5266,negated_conjecture,
~ c8_2(a51,a70) ).
cnf(u5331,negated_conjecture,
c5_2(a127,a100) ).
cnf(u5390,negated_conjecture,
~ c3_2(a68,a46) ).
cnf(u5405,negated_conjecture,
c3_1(a136) ).
cnf(u5424,negated_conjecture,
( ~ c8_2(a68,X1)
| c4_2(a68,X1)
| c3_2(a68,X1) ) ).
cnf(u5442,negated_conjecture,
c6_1(a104) ).
cnf(u5492,negated_conjecture,
c6_1(a64) ).
cnf(u5506,negated_conjecture,
c7_1(a64) ).
cnf(u5533,negated_conjecture,
c6_1(a113) ).
cnf(u5550,negated_conjecture,
c6_1(a16) ).
cnf(u5609,negated_conjecture,
c5_2(a136,a108) ).
cnf(u5649,negated_conjecture,
c2_1(a93) ).
cnf(u5660,negated_conjecture,
c7_1(a93) ).
cnf(u5680,negated_conjecture,
c8_1(a68) ).
cnf(u5693,negated_conjecture,
c6_2(a134,a108) ).
cnf(u5696,negated_conjecture,
c7_1(a134) ).
cnf(u5702,negated_conjecture,
~ c5_2(a134,a135) ).
cnf(u5705,negated_conjecture,
c6_1(a134) ).
cnf(u5834,negated_conjecture,
~ c4_1(a134) ).
cnf(u5723,negated_conjecture,
c8_2(a134,a71) ).
cnf(u5734,negated_conjecture,
( c2_2(a134,X0)
| c4_2(a134,X0) ) ).
cnf(u5763,negated_conjecture,
~ c8_1(a134) ).
cnf(u5781,negated_conjecture,
( ~ c6_2(a134,X0)
| ~ c4_2(a134,X0)
| ~ c1_2(a134,X0) ) ).
cnf(u5793,negated_conjecture,
~ c6_2(a134,a22) ).
cnf(u5803,negated_conjecture,
~ c7_2(a134,a22) ).
cnf(u5825,negated_conjecture,
( c7_2(a134,X0)
| c4_2(a134,X0) ) ).
cnf(u5855,negated_conjecture,
~ c1_2(a134,a108) ).
cnf(u5875,negated_conjecture,
~ c3_2(a134,a46) ).
cnf(u5911,negated_conjecture,
c5_2(a32,a100) ).
cnf(u5916,negated_conjecture,
c6_1(a34) ).
cnf(u5948,negated_conjecture,
~ c1_2(a136,a69) ).
cnf(u5963,negated_conjecture,
~ c6_2(a136,a69) ).
cnf(u5982,negated_conjecture,
c2_1(a66) ).
cnf(u50,axiom,
( ~ sP15(X0)
| ndr1_1(X0) ) ).
cnf(u4437,negated_conjecture,
c6_1(a96) ).
cnf(u3228,negated_conjecture,
c7_1(a27) ).
cnf(u833,negated_conjecture,
~ c1_2(a122,a123) ).
cnf(u3231,negated_conjecture,
c7_1(a117) ).
cnf(u3746,negated_conjecture,
~ c3_2(a35,a115) ).
cnf(u2205,negated_conjecture,
~ c4_1(a59) ).
cnf(u835,negated_conjecture,
ndr1_1(a122) ).
cnf(u5436,negated_conjecture,
( ~ c2_2(X0,X1)
| c6_1(X0)
| c5_2(X0,a100)
| c4_2(X0,X1)
| c2_1(X0)
| c7_2(X0,X1)
| c8_1(X0) ) ).
cnf(u4484,negated_conjecture,
ndr1_1(a127) ).
cnf(u834,negated_conjecture,
c5_2(a122,a123) ).
cnf(u49,axiom,
( ~ sP15(X0)
| ~ c1_2(X0,a2) ) ).
cnf(u5475,negated_conjecture,
( ~ c1_1(X0)
| c6_2(X0,X1)
| c8_2(X0,X1)
| ~ c7_2(X0,X1)
| c2_1(X0)
| c4_2(X0,X2)
| c3_2(X0,X2)
| ~ c8_2(X0,X2)
| c3_1(X0)
| c6_1(X0) ) ).
cnf(u2847,negated_conjecture,
~ c3_2(a52,a115) ).
cnf(u391,negated_conjecture,
c6_0 ).
cnf(u830,negated_conjecture,
~ c1_1(a122) ).
cnf(u5881,negated_conjecture,
( ~ c3_2(a134,X0)
| ~ c6_2(a134,X0)
| c4_2(a134,X0) ) ).
cnf(u2845,negated_conjecture,
~ c8_2(a52,a115) ).
cnf(u3744,negated_conjecture,
~ c7_2(a35,a115) ).
cnf(u3745,negated_conjecture,
~ c8_2(a35,a115) ).
cnf(u4082,negated_conjecture,
( ~ c3_2(a52,X0)
| c5_2(a52,X0)
| c6_2(a52,X0) ) ).
cnf(u3782,negated_conjecture,
ndr1_1(a59) ).
cnf(u4438,negated_conjecture,
c6_1(a59) ).
cnf(u3995,negated_conjecture,
~ c8_2(a96,a115) ).
cnf(u5577,negated_conjecture,
( ~ c4_2(X0,X1)
| c1_2(X0,X1)
| c6_2(X0,X1)
| c7_1(X0)
| c4_1(X0)
| c2_1(X0)
| c6_1(X0) ) ).
cnf(u4772,negated_conjecture,
~ c2_2(a136,a100) ).
cnf(u215,negated_conjecture,
ndr1_1(a136) ).
cnf(u2844,negated_conjecture,
~ c7_2(a52,a115) ).
cnf(u3861,negated_conjecture,
~ c7_2(a59,a115) ).
cnf(u212,negated_conjecture,
c5_2(a136,a137) ).
cnf(u3763,negated_conjecture,
c8_2(a81,a116) ).
cnf(u3227,negated_conjecture,
c7_1(a122) ).
cnf(u2982,negated_conjecture,
~ c7_2(a122,a115) ).
cnf(u1859,negated_conjecture,
( ~ c5_2(X112,a108)
| ~ c5_2(X112,X113)
| ~ c8_2(X112,X113)
| ~ ndr1_1(X112)
| c7_1(X112) ) ).
cnf(u3232,negated_conjecture,
ndr1_1(a117) ).
cnf(u47,axiom,
( ~ sP15(X0)
| c4_2(X0,a2) ) ).
cnf(u3226,negated_conjecture,
c7_1(a52) ).
cnf(u4421,negated_conjecture,
( ~ c2_2(X6,X7)
| c1_2(X6,a7)
| c4_2(X6,X7)
| c3_2(X6,X7)
| ~ c8_1(X6) ) ).
cnf(u5877,negated_conjecture,
c8_2(a134,a108) ).
cnf(u832,negated_conjecture,
~ c3_2(a122,a123) ).
cnf(u2712,negated_conjecture,
~ c3_2(a27,a115) ).
cnf(u3994,negated_conjecture,
~ c7_2(a96,a115) ).
cnf(u3546,negated_conjecture,
ndr1_1(a32) ).
cnf(u2709,negated_conjecture,
~ c7_2(a27,a115) ).
cnf(u4263,negated_conjecture,
( ~ c3_2(a122,X0)
| ~ c6_2(a122,X0)
| c4_2(a122,X0) ) ).
cnf(u2231,negated_conjecture,
c5_1(a51) ).
cnf(u812,negated_conjecture,
( c3_2(a136,X146)
| c8_2(a136,X146)
| c7_2(a136,X146) ) ).
cnf(u4420,negated_conjecture,
( ~ c2_2(X6,X7)
| c6_2(X6,a7)
| c4_2(X6,X7)
| c3_2(X6,X7)
| ~ c8_1(X6) ) ).
cnf(u5896,negated_conjecture,
~ c8_2(a68,a115) ).
cnf(u188,negated_conjecture,
~ c3_0 ).
cnf(u5987,negated_conjecture,
c7_1(a66) ).
cnf(u870,negated_conjecture,
~ c2_1(a117) ).
cnf(u5435,negated_conjecture,
( ~ c8_2(X0,X1)
| c6_1(X0)
| ~ c5_2(X0,X1)
| c2_1(X0)
| c7_1(X0)
| c6_2(X0,a108) ) ).
cnf(u5434,negated_conjecture,
( ~ c4_1(X0)
| c6_1(X0)
| c6_2(X0,X1)
| c8_2(X0,X1)
| ~ c7_2(X0,X1)
| c2_1(X0)
| c4_2(X0,X2)
| c3_2(X0,X2)
| ~ c8_2(X0,X2) ) ).
cnf(u5284,negated_conjecture,
( ~ c2_2(X138,X139)
| c3_2(X138,X139)
| ~ c1_1(X138)
| c7_2(X138,X139)
| ~ c8_1(X138) ) ).
cnf(u5836,negated_conjecture,
c4_2(a134,a22) ).
cnf(u5883,negated_conjecture,
~ c6_2(a134,a135) ).
cnf(u5891,negated_conjecture,
( c5_2(X0,a100)
| c6_1(X0)
| c4_2(X0,a116)
| c2_1(X0)
| c7_2(X0,a116)
| c4_1(X0) ) ).
cnf(u869,negated_conjecture,
c8_1(a117) ).
cnf(u5194,negated_conjecture,
c8_2(a27,a28) ).
cnf(u1858,negated_conjecture,
( ~ c7_2(X112,a108)
| ~ c5_2(X112,X113)
| ~ c8_2(X112,X113)
| ~ ndr1_1(X112)
| c7_1(X112) ) ).
cnf(u3257,negated_conjecture,
( ~ c2_2(X0,a71)
| c4_2(X0,a71)
| c6_2(X0,a7)
| ~ c8_1(X0)
| c4_1(X0)
| c8_2(X0,a72) ) ).
cnf(u3233,negated_conjecture,
~ c7_2(a117,a115) ).
cnf(u4712,negated_conjecture,
( ~ c3_2(a68,X0)
| c5_2(a68,X0)
| c6_2(a68,X0) ) ).
cnf(u390,negated_conjecture,
c4_0 ).
cnf(u3665,negated_conjecture,
c6_2(a35,a36) ).
cnf(u217,negated_conjecture,
c5_1(a136) ).
cnf(u5563,negated_conjecture,
c6_1(a44) ).
cnf(u3234,negated_conjecture,
~ c8_2(a117,a115) ).
cnf(u48,axiom,
( ~ sP15(X0)
| c7_2(X0,a2) ) ).
cnf(u213,negated_conjecture,
c3_2(a136,a137) ).
cnf(u2204,negated_conjecture,
c3_1(a59) ).
cnf(u2843,negated_conjecture,
ndr1_1(a52) ).
cnf(u3996,negated_conjecture,
~ c3_2(a96,a115) ).
cnf(u5895,negated_conjecture,
~ c7_2(a68,a115) ).
cnf(u3863,negated_conjecture,
~ c3_2(a59,a115) ).
cnf(u5688,negated_conjecture,
( ~ c3_2(a32,X0)
| c5_2(a32,X0)
| c6_2(a32,X0) ) ).
cnf(u5897,negated_conjecture,
~ c3_2(a68,a115) ).
cnf(u4558,negated_conjecture,
( ~ c3_2(a35,X0)
| ~ c6_2(a35,X0)
| c4_2(a35,X0) ) ).
cnf(u3235,negated_conjecture,
~ c3_2(a117,a115) ).
cnf(u4675,negated_conjecture,
ndr1_1(a68) ).
cnf(u2985,negated_conjecture,
~ c3_2(a122,a115) ).
cnf(u2983,negated_conjecture,
~ c8_2(a122,a115) ).
cnf(u218,negated_conjecture,
ndr1_0 ).
cnf(u190,negated_conjecture,
~ c2_0 ).
cnf(u214,negated_conjecture,
c1_2(a136,a137) ).
cnf(u3443,negated_conjecture,
( ~ c3_2(a96,X0)
| c5_2(a96,X0)
| c6_2(a96,X0) ) ).
cnf(u2036,negated_conjecture,
( ~ c8_1(X80)
| c7_1(X80) ) ).
cnf(u3862,negated_conjecture,
~ c8_2(a59,a115) ).
cnf(u4418,negated_conjecture,
( ~ c2_2(X6,X7)
| c3_2(X6,X7)
| c4_2(X6,X7)
| c3_2(X6,a7)
| ~ c8_1(X6) ) ).
cnf(u2710,negated_conjecture,
~ c8_2(a27,a115) ).
cnf(u1860,negated_conjecture,
( ~ ndr1_1(X112)
| ~ c5_2(X112,X113)
| ~ c8_2(X112,X113)
| c7_1(X112)
| c6_2(X112,a108) ) ).
cnf(u2230,negated_conjecture,
~ c7_1(a51) ).
cnf(u831,negated_conjecture,
c8_1(a122) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SYN544+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 % Computer : n002.cluster.edu
% 0.10/0.24 % Model : x86_64 x86_64
% 0.10/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.24 % Memory : 8046.5625MB
% 0.10/0.24 % OS : Linux 6.8.0-71-generic
% 0.10/0.25 % CPULimit : 300
% 0.10/0.25 % WCLimit : 300
% 0.10/0.25 % DateTime : Mon Sep 28 16:29:52 UTC 2026
% 0.10/0.25 % CPUTime :
% 0.10/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.29 Running first-order theorem proving
% 0.23/0.29 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
% 9.65/2.11 % (496706)Detected formulas, will run a generic FOF schedule.
% 9.65/2.11 % (496719)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=3816913886:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.65/2.11 % (496723)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3581220826:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.65/2.11 % (496716)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=3587174811:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.65/2.11 % (496721)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3742775707:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.65/2.11 % (496717)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=1508030829:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.65/2.11 % (496720)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=687674248:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.65/2.11 % (496725)dis-21_1_sil=8000:lcm=predicate:random_seed=1258414136: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)
% 9.65/2.11 % (496723)Refutation not found, incomplete strategy
% 9.65/2.11 % (496723)------------------------------
% 9.65/2.11 % (496723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496723)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496723)Termination reason: Refutation not found, incomplete strategy
% 9.65/2.11 % (496723)Time elapsed: 0.026 s
% 9.65/2.11 % (496723)Peak memory usage: 90 MB
% 9.65/2.11 % (496723)Instructions burned: 41 (million)
% 9.65/2.11 % (496721)Instruction limit reached!
% 9.65/2.11 % (496721)------------------------------
% 9.65/2.11 % (496721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496721)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496721)Termination reason: Instruction limit
% 9.65/2.11 % (496721)Termination phase: Saturation
% 9.65/2.11 % (496721)Time elapsed: 0.064 s
% 9.65/2.11 % (496721)Peak memory usage: 88 MB
% 9.65/2.11 % (496721)Instructions burned: 121 (million)
% 9.65/2.11 % (496720)Instruction limit reached!
% 9.65/2.11 % (496720)------------------------------
% 9.65/2.11 % (496720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496720)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496720)Termination reason: Instruction limit
% 9.65/2.11 % (496720)Termination phase: Saturation
% 9.65/2.11 % (496720)Time elapsed: 0.064 s
% 9.65/2.11 % (496720)Peak memory usage: 90 MB
% 9.65/2.11 % (496720)Instructions burned: 110 (million)
% 9.65/2.11 % (496725)Instruction limit reached!
% 9.65/2.11 % (496725)------------------------------
% 9.65/2.11 % (496725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496725)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496725)Termination reason: Instruction limit
% 9.65/2.11 % (496725)Termination phase: Saturation
% 9.65/2.11 % (496725)Time elapsed: 0.073 s
% 9.65/2.11 % (496725)Peak memory usage: 91 MB
% 9.65/2.11 % (496725)Instructions burned: 130 (million)
% 9.65/2.11 % (496793)lrs+10_1_sil=8000:sp=occurrence:random_seed=1232808654:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 9.65/2.11 % (496794)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3737869920:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.65/2.11 % (496794)Refutation not found, incomplete strategy
% 9.65/2.11 % (496794)------------------------------
% 9.65/2.11 % (496794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496794)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496794)Termination reason: Refutation not found, incomplete strategy
% 9.65/2.11 % (496794)Time elapsed: 0.019 s
% 9.65/2.11 % (496794)Peak memory usage: 90 MB
% 9.65/2.11 % (496794)Instructions burned: 30 (million)
% 9.65/2.11 % (496801)lrs+1011_1_sil=32000:sp=occurrence:random_seed=597754685:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 9.65/2.11 % (496801)Refutation not found, incomplete strategy
% 9.65/2.11 % (496801)------------------------------
% 9.65/2.11 % (496801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496801)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496801)Termination reason: Refutation not found, incomplete strategy
% 9.65/2.11 % (496801)Time elapsed: 0.020 s
% 9.65/2.11 % (496801)Peak memory usage: 90 MB
% 9.65/2.11 % (496801)Instructions burned: 30 (million)
% 9.65/2.11 % (496723)------------------------------
% 9.65/2.11 % (496723)------------------------------
% 9.65/2.11 % (496793)Instruction limit reached!
% 9.65/2.11 % (496793)------------------------------
% 9.65/2.11 % (496793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496793)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496793)Termination reason: Instruction limit
% 9.65/2.11 % (496793)Termination phase: Saturation
% 9.65/2.11 % (496793)Time elapsed: 0.145 s
% 9.65/2.11 % (496793)Peak memory usage: 92 MB
% 9.65/2.11 % (496793)Instructions burned: 286 (million)
% 9.65/2.11 % (496837)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=2782070896:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 9.65/2.11 % (496837)Refutation not found, incomplete strategy
% 9.65/2.11 % (496837)------------------------------
% 9.65/2.11 % (496837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496837)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496837)Termination reason: Refutation not found, incomplete strategy
% 9.65/2.11 % (496837)Time elapsed: 0.023 s
% 9.65/2.11 % (496837)Peak memory usage: 90 MB
% 9.65/2.11 % (496837)Instructions burned: 35 (million)
% 9.65/2.11 % (496794)------------------------------
% 9.65/2.11 % (496794)------------------------------
% 9.65/2.11 % (496838)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=483792068:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 9.65/2.11 % (496801)------------------------------
% 9.65/2.11 % (496801)------------------------------
% 9.65/2.11 % (496884)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=471301182:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 9.65/2.11 % (496838)Refutation not found, incomplete strategy
% 9.65/2.11 % (496838)------------------------------
% 9.65/2.11 % (496838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496838)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496838)Termination reason: Refutation not found, incomplete strategy
% 9.65/2.11 % (496838)Time elapsed: 0.137 s
% 9.65/2.11 % (496838)Peak memory usage: 92 MB
% 9.65/2.11 % (496838)Instructions burned: 242 (million)
% 9.65/2.11 % (496889)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2658681860:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 9.65/2.11 % (496837)------------------------------
% 9.65/2.11 % (496837)------------------------------
% 9.65/2.11 % (496889)Instruction limit reached!
% 9.65/2.11 % (496889)------------------------------
% 9.65/2.11 % (496889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496889)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496889)Termination reason: Instruction limit
% 9.65/2.11 % (496889)Termination phase: Saturation
% 9.65/2.11 % (496889)Time elapsed: 0.066 s
% 9.65/2.11 % (496889)Peak memory usage: 91 MB
% 9.65/2.11 % (496889)Instructions burned: 114 (million)
% 9.65/2.11 % (496892)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1723909441:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 9.65/2.11 % (496893)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2012375196:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 9.65/2.11 % (496838)------------------------------
% 9.65/2.11 % (496838)------------------------------
% 9.65/2.11 % (496893)Refutation not found, incomplete strategy
% 9.65/2.11 % (496893)------------------------------
% 9.65/2.11 % (496893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496893)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496893)Termination reason: Refutation not found, incomplete strategy
% 9.65/2.11 % (496893)Time elapsed: 0.050 s
% 9.65/2.11 % (496893)Peak memory usage: 90 MB
% 9.65/2.11 % (496893)Instructions burned: 98 (million)
% 9.65/2.11 % (496892)Instruction limit reached!
% 9.65/2.11 % (496892)------------------------------
% 9.65/2.11 % (496892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496892)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496892)Termination reason: Instruction limit
% 9.65/2.11 % (496892)Termination phase: Saturation
% 9.65/2.11 % (496892)Time elapsed: 0.065 s
% 9.65/2.11 % (496892)Peak memory usage: 89 MB
% 9.65/2.11 % (496892)Instructions burned: 128 (million)
% 9.65/2.11 % (496896)lrs+10_1_sil=8000:sp=occurrence:random_seed=2236293052:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 9.65/2.11 % (496717)First to succeed.
% 9.65/2.11 % (496717)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-496706"
% 9.65/2.11 % (496897)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1266111461:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 9.65/2.11 % (496897)Refutation not found, incomplete strategy
% 9.65/2.11 % (496897)------------------------------
% 9.65/2.11 % (496897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496897)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496897)Termination reason: Refutation not found, incomplete strategy
% 9.65/2.11 % (496897)Time elapsed: 0.059 s
% 9.65/2.11 % (496897)Peak memory usage: 91 MB
% 9.65/2.11 % (496897)Instructions burned: 103 (million)
% 9.65/2.11 % (496893)------------------------------
% 9.65/2.11 % (496893)------------------------------
% 9.65/2.11 % (496719)Refutation not found, incomplete strategy
% 9.65/2.11 % (496719)------------------------------
% 9.65/2.11 % (496719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/2.11 % (496719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/2.11 % (496719)CaDiCaL version: 2.1.3
% 9.65/2.11 % (496719)Termination reason: Refutation not found, incomplete strategy
% 9.65/2.11 % (496719)Time elapsed: 1.266 s
% 9.65/2.11 % (496719)Peak memory usage: 148 MB
% 9.65/2.11 % (496719)Instructions burned: 3528 (million)
% 9.65/2.11 % (496900)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1037640737:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 9.65/2.11 % SZS status CounterSatisfiable for theBenchmark
% 9.65/2.11 % SZS output start Saturation.
% See solution above
% 9.65/2.12 % SZS output start Definitions and Model Updates.
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_1(X0) | ~c5_1(X0) | c2_1(X0) | ~ndr1_0 | ~c4_2(X1,a1) | sP15(X1) | ndr1_1(X1) | ~ndr1_0 | ~c5_0 is false, set ~c4_2(X1,a1) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c1_1(X2) | ~c4_2(X2,a4) | ndr1_1(X2) | ~ndr1_0 | ~c2_2(X3,X4) | ~c4_2(X3,X4) | ~c5_2(X3,X4) | ~ndr1_1(X3) | ~c1_1(X3) | c2_1(X3) | ~ndr1_0 | ~c8_0 is false, set ~c4_2(X2,a4) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c1_1(X2) | ndr1_1(X2) | ~c4_2(X2,a5) | ~ndr1_0 | ~c2_2(X3,X4) | ~c4_2(X3,X4) | ~c5_2(X3,X4) | ~ndr1_1(X3) | ~c1_1(X3) | c2_1(X3) | ~ndr1_0 | ~c8_0 is false, set ~c4_2(X2,a5) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_1(X0) | ~c5_1(X0) | c2_1(X0) | ~ndr1_0 | ~c1_2(X1,a1) | sP15(X1) | ndr1_1(X1) | ~ndr1_0 | ~c5_0 is false, set ~c1_2(X1,a1) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_1(X69) | ~c1_2(X69,a72) | c4_1(X69) | ~ndr1_0 | ~c8_0 | c5_0 is false, set ~c1_2(X69,a72) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_0 | ~c8_0 | ~c3_1(X68) | ~c1_2(X68,a69) | ndr1_1(X68) | ~ndr1_0 is false, set ~c1_2(X68,a69) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c1_2(X69,a71) | ndr1_1(X69) | c4_1(X69) | ~ndr1_0 | ~c8_0 | c5_0 is false, set ~c1_2(X69,a71) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_0 | ~c8_0 | ~c3_1(X68) | ndr1_1(X68) | c4_2(X68,a70) | ~ndr1_0 is false, set c4_2(X68,a70) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c2_2(X0,a57) | ~c3_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set c2_2(X0,a57) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c5_0 | ~c5_1(X91) | c4_1(X91) | c1_1(X91) | ~ndr1_0 | ~c2_1(X92) | c2_2(X92,a94) | ndr1_1(X92) | ~ndr1_0 is false, set c2_2(X92,a94) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c5_0 | ~c5_1(X91) | c4_1(X91) | c1_1(X91) | ~ndr1_0 | ~c2_1(X92) | ~c5_2(X92,a94) | ndr1_1(X92) | ~ndr1_0 is false, set ~c5_2(X92,a94) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c5_2(a120,X129) | ~c1_2(a120,X129) | ~c7_2(a120,X129) | ~ndr1_1(a120) | ndr1_0 is false, set ~c5_2(a120,X129) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_1(X0) | ~c3_1(X0) | ~c5_2(X0,a58) | ~ndr1_0 | ~sP6 is false, set ~c5_2(X0,a58) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c1_1(X2) | ndr1_1(X2) | ~c5_2(X2,a5) | ~ndr1_0 | ~c2_2(X3,X4) | ~c4_2(X3,X4) | ~c5_2(X3,X4) | ~ndr1_1(X3) | ~c1_1(X3) | c2_1(X3) | ~ndr1_0 | ~c8_0 is false, set ~c5_2(X2,a5) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_0 | ~c8_0 | ~c3_1(X68) | ndr1_1(X68) | ~c6_2(X68,a70) | ~ndr1_0 is false, set ~c6_2(X68,a70) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_0 | ~c8_0 | ~c3_1(X68) | ~c6_2(X68,a69) | ndr1_1(X68) | ~ndr1_0 is false, set ~c6_2(X68,a69) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c8_2(a120,X128) | c1_2(a120,X128) | ~c6_2(a120,X128) | ~ndr1_1(a120) | ndr1_0 is false, set ~c8_2(a120,X128) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_1(X0) | ~c3_1(X0) | ~c3_2(X0,a58) | ~ndr1_0 | ~sP6 is false, set ~c3_2(X0,a58) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c1_1(X2) | ~c3_2(X2,a4) | ndr1_1(X2) | ~ndr1_0 | ~c2_2(X3,X4) | ~c4_2(X3,X4) | ~c5_2(X3,X4) | ~ndr1_1(X3) | ~c1_1(X3) | c2_1(X3) | ~ndr1_0 | ~c8_0 is false, set ~c3_2(X2,a4) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c3_2(X69,a71) | ndr1_1(X69) | c4_1(X69) | ~ndr1_0 | ~c8_0 | c5_0 is false, set ~c3_2(X69,a71) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c5_2(X0,a57) | ~c3_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set c5_2(X0,a57) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c1_2(a65,X62) | c4_2(a65,X62) | c5_2(a65,X62) | ~ndr1_1(a65) | ndr1_0 | ~c1_0 is false, set c5_2(a65,X62) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_0 | ~c8_0 | ~c3_1(X68) | c5_2(X68,a69) | ndr1_1(X68) | ~ndr1_0 is false, set c5_2(X68,a69) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c5_2(X69,a71) | ndr1_1(X69) | c4_1(X69) | ~ndr1_0 | ~c8_0 | c5_0 is false, set c5_2(X69,a71) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_1(X82) | ~c4_2(X82,X83) | c8_2(X82,X83) | c7_2(X82,X83) | ~ndr1_1(X82) | ~c5_1(X82) | ~ndr1_0 | c5_2(X84,a87) | ~c7_1(X84) | ndr1_1(X84) | ~ndr1_0 | ~c2_1(X85) | c3_1(X85) | c4_2(X85,X86) | c1_2(X85,X86) | ~c6_2(X85,X86) | ~ndr1_1(X85) | ~ndr1_0 is false, set c5_2(X84,a87) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c5_0 | ~c5_1(X91) | c4_1(X91) | c1_1(X91) | ~ndr1_0 | ~c2_1(X92) | ndr1_1(X92) | c5_2(X92,a95) | ~ndr1_0 is false, set c5_2(X92,a95) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c5_0 | ~c5_1(X91) | c4_1(X91) | c1_1(X91) | ~ndr1_0 | ~c2_1(X92) | c6_2(X92,a94) | ndr1_1(X92) | ~ndr1_0 is false, set c6_2(X92,a94) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_1(X0) | ~c3_1(X0) | c6_2(X0,a58) | ~ndr1_0 | ~sP6 is false, set c6_2(X0,a58) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_1(X0) | ~c5_1(X0) | c2_1(X0) | ~ndr1_0 | ndr1_1(X1) | sP15(X1) | c6_2(X1,a3) | ~ndr1_0 | ~c5_0 is false, set c6_2(X1,a3) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c5_0 | ~c5_1(X91) | c4_1(X91) | c1_1(X91) | ~ndr1_0 | ~c2_1(X92) | ndr1_1(X92) | c6_2(X92,a95) | ~ndr1_0 is false, set c6_2(X92,a95) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_2(X0,a57) | ~c3_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~c7_2(X0,a57) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_1(X0) | ~c5_1(X0) | c2_1(X0) | ~ndr1_0 | ndr1_1(X1) | sP15(X1) | ~c7_2(X1,a3) | ~ndr1_0 | ~c5_0 is false, set ~c7_2(X1,a3) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c1_1(X2) | ~c7_2(X2,a4) | ndr1_1(X2) | ~ndr1_0 | ~c2_2(X3,X4) | ~c4_2(X3,X4) | ~c5_2(X3,X4) | ~ndr1_1(X3) | ~c1_1(X3) | c2_1(X3) | ~ndr1_0 | ~c8_0 is false, set ~c7_2(X2,a4) to true
% 9.65/2.12 for all groundings, until fixed point,
% 9.65/2.12 whenever ~c7_1(X82) | ~c4_2(X82,X83) | c8_2(X82,X83) | c7_2(X82,X83) | ~ndr1_1(X82) | ~c5_1(X82) | ~ndr1_0 | ndr1_1(X84) | ~c7_1(X84) | ~c7_2(X84,a88) | ~ndr1_0 | ~c2_1(X85) | c3_1(X85) | c4_2(X85,X86) | c1_2(X85,X86) | ~c6_2(X85,X86) | ~ndr1_1(X85) | ~ndr1_0 is false, set ~c7_2(X84,a88) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_1(X82) | ~c4_2(X82,X83) | c8_2(X82,X83) | c7_2(X82,X83) | ~ndr1_1(X82) | ~c5_1(X82) | ~ndr1_0 | ndr1_1(X84) | ~c7_1(X84) | c1_2(X84,a88) | ~ndr1_0 | ~c2_1(X85) | c3_1(X85) | c4_2(X85,X86) | c1_2(X85,X86) | ~c6_2(X85,X86) | ~ndr1_1(X85) | ~ndr1_0 is false, set c1_2(X84,a88) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_1(X82) | ~c4_2(X82,X83) | c8_2(X82,X83) | c7_2(X82,X83) | ~ndr1_1(X82) | ~c5_1(X82) | ~ndr1_0 | c1_2(X84,a87) | ~c7_1(X84) | ndr1_1(X84) | ~ndr1_0 | ~c2_1(X85) | c3_1(X85) | c4_2(X85,X86) | c1_2(X85,X86) | ~c6_2(X85,X86) | ~ndr1_1(X85) | ~ndr1_0 is false, set c1_2(X84,a87) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c5_0 | ~c5_1(X91) | c4_1(X91) | c1_1(X91) | ~ndr1_0 | ~c2_1(X92) | ndr1_1(X92) | c1_2(X92,a95) | ~ndr1_0 is false, set c1_2(X92,a95) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_0 | ~c8_0 | ~c3_1(X68) | ndr1_1(X68) | c7_2(X68,a70) | ~ndr1_0 is false, set c7_2(X68,a70) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_1(X69) | c7_2(X69,a72) | c4_1(X69) | ~ndr1_0 | ~c8_0 | c5_0 is false, set c7_2(X69,a72) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c7_1(X112) | ~c5_2(X112,X113) | ~c8_2(X112,X113) | ~ndr1_1(X112) | ndr1_1(X112) | ~ndr1_0 | c2_0 is false, set c2_0 to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_0 | c3_1(a121) is false, set c3_1(a121) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c5_1(a65) | ndr1_0 | ~c1_0 is false, set c5_1(a65) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_0 | c5_1(a121) is false, set c5_1(a121) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c7_1(X82) | ~c4_2(X82,X83) | c8_2(X82,X83) | c7_2(X82,X83) | ~ndr1_1(X82) | ~c5_1(X82) | ~ndr1_0 | c8_2(X84,a87) | ~c7_1(X84) | ndr1_1(X84) | ~ndr1_0 | ~c2_1(X85) | c3_1(X85) | c4_2(X85,X86) | c1_2(X85,X86) | ~c6_2(X85,X86) | ~ndr1_1(X85) | ~ndr1_0 is false, set c8_2(X84,a87) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_1(X69) | c8_2(X69,a72) | c4_1(X69) | ~ndr1_0 | ~c8_0 | c5_0 is false, set c8_2(X69,a72) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_0 | c8_2(a121,X130) | ~c7_2(a121,X130) | c5_2(a121,X130) | ~ndr1_1(a121) is false, set c8_2(a121,X130) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c7_0 | c1_1(X75) | ndr1_1(X75) | c8_2(X75,X76) | c7_2(X75,X76) | ~c3_2(X75,X76) | ~ndr1_1(X75) | ~ndr1_0 | ~c2_0 is false, set c7_0 to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_0 | ~c3_1(a66) | ~c1_0 is false, set ~c3_1(a66) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ~c1_1(X2) | ndr1_1(X2) | c3_2(X2,a5) | ~ndr1_0 | ~c2_2(X3,X4) | ~c4_2(X3,X4) | ~c5_2(X3,X4) | ~ndr1_1(X3) | ~c1_1(X3) | c2_1(X3) | ~ndr1_0 | ~c8_0 is false, set c3_2(X2,a5) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_0 | c2_2(a66,X64) | ~c8_2(a66,X64) | c3_2(a66,X64) | ~ndr1_1(a66) | ~c1_0 is false, set c3_2(a66,X64) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever ndr1_0 | c3_2(a66,X63) | ~c8_2(a66,X63) | c5_2(a66,X63) | ~ndr1_1(a66) | ~c1_0 is false, set c3_2(a66,X63) to true
% 9.65/2.12 for all groundings,
% 9.65/2.12 whenever c1_1(X53) | ~c4_1(X53) | ~ndr1_0 | ndr1_0 | ~c2_1(X55) | ~c3_1(X55) | ~c3_2(X55,X56) | c5_2(X55,X56) | c6_2(X55,X56) | ~ndr1_1(X55) | ~ndr1_0 is false, set ~c4_1(X53) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c4_2(X133,X134) | ~c8_2(X133,X134) | c3_2(X133,X134) | ~ndr1_1(X133) | ~c4_1(X133) | ~c7_2(X133,X135) | c8_2(X133,X135) | c6_2(X133,X135) | ~ndr1_1(X133) | ~ndr1_0 | ndr1_0 | ~c7_0 is false, set ~c7_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | c8_1(X145) | ~c2_1(X145) | ~ndr1_0 is false, set c8_1(X145) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c2_0 | ~c5_1(X8) | ndr1_1(X8) | ~ndr1_0 | ndr1_0 is false, set ~c5_1(X8) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c2_0 | ~c5_1(X8) | ~c4_2(X8,a8) | ~ndr1_0 | ndr1_0 is false, set ~c5_1(X8) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c2_0 | ~c5_1(X8) | c2_2(X8,a8) | ~ndr1_0 | ndr1_0 is false, set ~c5_1(X8) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c5_1(a120) | ndr1_0 is false, set ~c5_1(a120) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c2_2(X96,X97) | ~c1_2(X96,X97) | c6_2(X96,X97) | ~ndr1_1(X96) | ndr1_1(X96) | ~ndr1_0 | c7_1(X98) | ~c2_1(X98) | ~c1_2(X98,X99) | c3_2(X98,X99) | ~c5_2(X98,X99) | ~ndr1_1(X98) | ~ndr1_0 | ~c8_0 is false, set ~c8_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_1(X141) | ~c1_1(X141) | ~c4_2(X141,X142) | c7_2(X141,X142) | ~c8_2(X141,X142) | ~ndr1_1(X141) | ~ndr1_0 | ~c8_0 is false, set ~c8_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c8_0 | ~c2_2(X36,X37) | c3_2(X36,X37) | ~c6_2(X36,X37) | ~ndr1_1(X36) | ~c8_1(X36) | c7_1(X36) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X36) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | ~c3_0 | c7_1(X131) | ~c6_1(X131) | c6_2(X131,X132) | c8_2(X131,X132) | ~c2_2(X131,X132) | ~ndr1_1(X131) | ~ndr1_0 is false, set ~c3_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c7_1(X57) | c6_1(X57) | ~c2_2(X57,a63) | ~ndr1_0 | ndr1_0 | c2_0 is false, set c6_1(X57) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c7_1(X57) | c6_1(X57) | ndr1_1(X57) | ~ndr1_0 | ndr1_0 | c2_0 is false, set c6_1(X57) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c7_1(X57) | c6_1(X57) | ~c5_2(X57,a63) | ~ndr1_0 | ndr1_0 | c2_0 is false, set c6_1(X57) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c7_0 | ndr1_1(X66) | c6_1(X66) | c2_1(X66) | ~ndr1_0 | ndr1_0 is false, set c6_1(X66) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c6_1(a65) | ndr1_0 | ~c1_0 is false, set c6_1(a65) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c7_1(X57) | c6_1(X57) | c4_2(X57,a63) | ~ndr1_0 | ndr1_0 | c2_0 is false, set c6_1(X57) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c7_0 | ~c7_2(X66,a67) | c6_1(X66) | c2_1(X66) | ~ndr1_0 | ndr1_0 is false, set c6_1(X66) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c4_2(X93,X94) | ~c1_2(X93,X94) | c2_2(X93,X94) | ~ndr1_1(X93) | c6_1(X93) | c1_1(X93) | ~ndr1_0 | c3_0 | ndr1_0 is false, set c6_1(X93) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c7_0 | ~c4_2(X66,a67) | c6_1(X66) | c2_1(X66) | ~ndr1_0 | ndr1_0 is false, set c6_1(X66) to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c5_0 | c8_2(X5,a6) | ~c2_1(X5) | ~c3_1(X5) | ~ndr1_0 | ndr1_1(X6) | ~c8_1(X6) | ~c2_2(X6,X7) | c4_2(X6,X7) | c3_2(X6,X7) | ~ndr1_1(X6) | ~ndr1_0 is false, set c5_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c5_0 | ~c7_2(X5,a6) | ~c2_1(X5) | ~c3_1(X5) | ~ndr1_0 | ndr1_1(X6) | ~c8_1(X6) | ~c2_2(X6,X7) | c4_2(X6,X7) | c3_2(X6,X7) | ~ndr1_1(X6) | ~ndr1_0 is false, set c5_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_1(X26) | ~c2_2(X26,a23) | ~c8_2(X26,X27) | c1_2(X26,X27) | ~c5_2(X26,X27) | ~ndr1_1(X26) | ~ndr1_0 | c5_0 | c8_0 is false, set c5_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_1(X26) | ~c3_2(X26,a23) | ~c8_2(X26,X27) | c1_2(X26,X27) | ~c5_2(X26,X27) | ~ndr1_1(X26) | ~ndr1_0 | c5_0 | c8_0 is false, set c5_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c7_2(X26,a22) | ndr1_1(X26) | ~c8_2(X26,X27) | c1_2(X26,X27) | ~c5_2(X26,X27) | ~ndr1_1(X26) | ~ndr1_0 | c5_0 | c8_0 is false, set c5_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_1(X26) | ~c6_2(X26,a23) | ~c8_2(X26,X27) | c1_2(X26,X27) | ~c5_2(X26,X27) | ~ndr1_1(X26) | ~ndr1_0 | c5_0 | c8_0 is false, set c5_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c6_2(X26,a22) | ndr1_1(X26) | ~c8_2(X26,X27) | c1_2(X26,X27) | ~c5_2(X26,X27) | ~ndr1_1(X26) | ~ndr1_0 | c5_0 | c8_0 is false, set c5_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_1(X26) | ndr1_1(X26) | ~c8_2(X26,X27) | c1_2(X26,X27) | ~c5_2(X26,X27) | ~ndr1_1(X26) | ~ndr1_0 | c5_0 | c8_0 is false, set c5_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c5_0 | c2_2(X5,a6) | ~c2_1(X5) | ~c3_1(X5) | ~ndr1_0 | ndr1_1(X6) | ~c8_1(X6) | ~c2_2(X6,X7) | c4_2(X6,X7) | c3_2(X6,X7) | ~ndr1_1(X6) | ~ndr1_0 is false, set c5_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c5_0 | ndr1_1(X5) | ~c2_1(X5) | ~c3_1(X5) | ~ndr1_0 | ndr1_1(X6) | ~c8_1(X6) | ~c2_2(X6,X7) | c4_2(X6,X7) | c3_2(X6,X7) | ~ndr1_1(X6) | ~ndr1_0 is false, set c5_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c6_2(X109,X110) | c5_2(X109,X110) | ~c2_2(X109,X110) | ~ndr1_1(X109) | ~c2_1(X109) | ~c6_1(X109) | ~ndr1_0 | c5_0 | ndr1_0 is false, set c5_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | ~sP4 is false, set ~sP4 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_1(X104) | c8_1(X104) | c7_2(X104,X105) | ~c2_2(X104,X105) | c4_2(X104,X105) | ~ndr1_1(X104) | ~ndr1_0 | ~c5_0 | sP3 is false, set sP3 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c8_0 | c5_1(X50) | ~c4_2(X50,X51) | ~c1_2(X50,X51) | ~c6_2(X50,X51) | ~ndr1_1(X50) | ndr1_1(X50) | ~ndr1_0 | sP6 is false, set sP6 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c5_1(X87) | c2_2(X87,a89) | ~ndr1_0 | sP4 | ndr1_0 is false, set sP4 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c5_1(X87) | ~c7_2(X87,a89) | ~ndr1_0 | sP4 | ndr1_0 is false, set sP4 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c5_1(X87) | ndr1_1(X87) | ~ndr1_0 | sP4 | ndr1_0 is false, set sP4 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c5_1(X87) | c1_2(X87,a89) | ~ndr1_0 | sP4 | ndr1_0 is false, set sP4 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | c1_1(X31) | c4_2(X31,a33) | ~c4_1(X31) | ~ndr1_0 | ~c1_0 is false, set ~c1_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | c1_1(X31) | ndr1_1(X31) | ~c4_1(X31) | ~ndr1_0 | ~c1_0 is false, set ~c1_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | c1_1(X31) | c3_2(X31,a33) | ~c4_1(X31) | ~ndr1_0 | ~c1_0 is false, set ~c1_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | c1_1(X31) | c1_2(X31,a33) | ~c4_1(X31) | ~ndr1_0 | ~c1_0 is false, set ~c1_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | c5_2(X116,a114) | c3_1(X116) | ~c7_1(X116) | ~ndr1_0 | ~c1_0 is false, set ~c1_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | ndr1_1(X116) | c3_1(X116) | ~c7_1(X116) | ~ndr1_0 | ~c1_0 is false, set ~c1_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | c8_2(X116,a114) | c3_1(X116) | ~c7_1(X116) | ~ndr1_0 | ~c1_0 is false, set ~c1_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | c1_2(X116,a114) | c3_1(X116) | ~c7_1(X116) | ~ndr1_0 | ~c1_0 is false, set ~c1_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c2_0 | ~c1_0 | ndr1_1(X149) | c2_1(X149) | c5_2(X149,X150) | ~c1_2(X149,X150) | c8_2(X149,X150) | ~ndr1_1(X149) | ~ndr1_0 is false, set ~c1_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c5_2(X17,X18) | c1_2(X17,X18) | ~ndr1_1(X17) | ~c1_1(X17) | ndr1_1(X17) | ~ndr1_0 | sP13 | ~c3_0 is false, set sP13 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_1(X15) | c3_2(X15,X16) | c2_2(X15,X16) | ~c1_2(X15,X16) | ~ndr1_1(X15) | ~c1_1(X15) | ~ndr1_0 | sP14 | c7_0 is false, set sP14 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever sP8 | c4_2(X39,X40) | ~c6_2(X39,X40) | c5_2(X39,X40) | ~ndr1_1(X39) | ndr1_1(X39) | ~c7_1(X39) | ~ndr1_0 | c3_1(X41) | c3_2(X41,X42) | c6_2(X41,X42) | c4_2(X41,X42) | ~ndr1_1(X41) | c5_2(X41,X43) | c1_2(X41,X43) | c8_2(X41,X43) | ~ndr1_1(X41) | ~ndr1_0 is false, set sP8 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | ~sP2 is false, set ~sP2 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c2_2(X0,X1) | c4_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c4_2(X0,a102) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c2_2(X0,X1) | c4_2(X0,X1) | ~ndr1_1(X0) | c7_2(X0,a101) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c2_2(X0,X1) | c4_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c1_2(X0,a102) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c2_2(X0,X1) | c4_2(X0,X1) | ~ndr1_1(X0) | c4_2(X0,a101) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c2_2(X0,X1) | c4_2(X0,X1) | ~ndr1_1(X0) | ~c2_2(X0,a101) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c2_2(X0,X1) | c4_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | c7_2(X0,a102) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c2_2(X0,X1) | c4_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | ~sP1 is false, set ~sP1 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ~c6_0 | ~c1_2(X23,X24) | ~c7_2(X23,X24) | c2_2(X23,X24) | ~ndr1_1(X23) | c2_1(X23) | c3_1(X23) | ~ndr1_0 | ndr1_0 is false, set ~c6_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | ~sP14 is false, set ~sP14 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | ~sP13 is false, set ~sP13 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever c7_0 | c6_0 | ndr1_0 is false, set c6_0 to true
% 0.25/2.31 for all groundings,
% 0.25/2.31 whenever ndr1_0 | ~sP8 is false, set ~sP8 to true
% 0.25/2.31 % SZS output end Definitions and Model Updates.
% 0.25/2.31 % (496717)------------------------------
% 0.25/2.31 % (496717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.25/2.31 % (496717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.25/2.31 % (496717)CaDiCaL version: 2.1.3
% 0.25/2.31 % (496717)Termination reason: Satisfiable
% 0.25/2.31 % (496717)Time elapsed: 0.975 s
% 0.25/2.31 % (496717)Peak memory usage: 135 MB
% 0.25/2.31 % (496717)Instructions burned: 1464 (million)
% 0.25/2.31 % (496717)------------------------------
% 0.25/2.31 % (496717)------------------------------
% 0.25/2.31 % (496706)Success in time 1.381 s
% 0.25/2.31 % Vampire exiting
%------------------------------------------------------------------------------