%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN429+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 : n014.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 01:50:37 PM UTC 2026
% Result : CounterSatisfiable 6.73s 1.71s
% Output : Saturation 6.73s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u3581,negated_conjecture,
~ sP0 ).
cnf(u1174,negated_conjecture,
~ c8_2(a213,a214) ).
cnf(u1178,negated_conjecture,
~ c6_2(a213,a214) ).
cnf(u1182,negated_conjecture,
~ c1_2(a213,a214) ).
cnf(u1186,negated_conjecture,
ndr1_1(a213) ).
cnf(u1191,negated_conjecture,
( ~ c8_2(a213,X195)
| c7_2(a213,X195)
| ~ c2_2(a213,X195) ) ).
cnf(u1195,negated_conjecture,
c8_1(a213) ).
cnf(u1199,negated_conjecture,
ndr1_0 ).
cnf(u1203,negated_conjecture,
~ c4_2(a210,a212) ).
cnf(u3612,negated_conjecture,
~ sP1 ).
cnf(u1210,negated_conjecture,
~ c10_2(a210,a212) ).
cnf(u1214,negated_conjecture,
c8_2(a210,a212) ).
cnf(u1218,negated_conjecture,
ndr1_1(a210) ).
cnf(u1222,negated_conjecture,
~ c3_2(a210,a211) ).
cnf(u1226,negated_conjecture,
c5_2(a210,a211) ).
cnf(u1230,negated_conjecture,
c10_2(a210,a211) ).
cnf(u1235,negated_conjecture,
c9_1(a210) ).
cnf(u3649,negated_conjecture,
~ sP2 ).
cnf(u1242,negated_conjecture,
c2_1(a205) ).
cnf(u1250,negated_conjecture,
c10_1(a205) ).
cnf(u1262,negated_conjecture,
( ~ c6_2(X190,X192)
| ~ c9_1(X190)
| ~ c10_2(X190,X192)
| c2_2(X190,X192)
| ~ ndr1_1(X190)
| c5_2(X190,X191)
| c2_2(X190,X191) ) ).
cnf(u3671,negated_conjecture,
~ sP3 ).
cnf(u1297,negated_conjecture,
~ ndr1_1(a199) ).
cnf(u1307,negated_conjecture,
~ c9_1(a199) ).
cnf(u1311,negated_conjecture,
c4_1(a199) ).
cnf(u3687,negated_conjecture,
~ sP4 ).
cnf(u1330,negated_conjecture,
~ ndr1_1(a194) ).
cnf(u1340,negated_conjecture,
~ c9_1(a194) ).
cnf(u1344,negated_conjecture,
~ c2_1(a194) ).
cnf(u3718,negated_conjecture,
~ sP5 ).
cnf(u1354,negated_conjecture,
( ~ c6_2(X179,X181)
| c3_1(X179)
| ~ c4_2(X179,X181)
| c9_2(X179,X181)
| ~ ndr1_1(X179)
| ~ c9_2(X179,X180)
| ~ c2_2(X179,X180)
| c5_2(X179,X180) ) ).
cnf(u1387,negated_conjecture,
( c3_1(X176)
| ~ ndr1_1(X176)
| ~ c9_2(X176,X177)
| ~ c6_2(X176,X177)
| c5_2(X176,X177)
| c5_1(X176) ) ).
cnf(u1391,negated_conjecture,
~ c9_1(a188) ).
cnf(u1395,negated_conjecture,
~ c3_1(a188) ).
cnf(u1411,negated_conjecture,
~ c9_1(a186) ).
cnf(u1421,negated_conjecture,
~ c2_1(a186) ).
cnf(u1425,negated_conjecture,
c3_1(a186) ).
cnf(u3752,negated_conjecture,
~ sP6 ).
cnf(u1444,negated_conjecture,
c8_1(a182) ).
cnf(u2401,negated_conjecture,
c9_0 ).
cnf(u1451,negated_conjecture,
c10_1(a182) ).
cnf(u1456,negated_conjecture,
c9_2(a180,a181) ).
cnf(u1463,negated_conjecture,
c7_2(a180,a181) ).
cnf(u1467,negated_conjecture,
c10_2(a180,a181) ).
cnf(u1471,negated_conjecture,
ndr1_1(a180) ).
cnf(u1476,negated_conjecture,
( c1_2(a180,X171)
| c6_2(a180,X171)
| c2_2(a180,X171) ) ).
cnf(u1480,negated_conjecture,
c5_1(a180) ).
cnf(u1484,negated_conjecture,
( ~ c2_1(X166)
| ~ c3_2(X166,a179) ) ).
cnf(u1491,negated_conjecture,
( ~ c2_1(X166)
| ~ c1_2(X166,a179) ) ).
cnf(u1495,negated_conjecture,
( ~ c2_1(X166)
| c10_2(X166,a179) ) ).
cnf(u1499,negated_conjecture,
( ~ c2_1(X166)
| ndr1_1(X166) ) ).
cnf(u3779,negated_conjecture,
~ sP7 ).
cnf(u1513,negated_conjecture,
( c9_2(X163,a175)
| c3_1(X163)
| c9_1(X163) ) ).
cnf(u1517,negated_conjecture,
( c7_2(X163,a175)
| c3_1(X163)
| c9_1(X163) ) ).
cnf(u1521,negated_conjecture,
( c4_2(X163,a175)
| c3_1(X163)
| c9_1(X163) ) ).
cnf(u1525,negated_conjecture,
( c3_1(X163)
| ndr1_1(X163)
| c9_1(X163) ) ).
cnf(u3816,negated_conjecture,
~ sP8 ).
cnf(u1535,negated_conjecture,
~ c8_0 ).
cnf(u3838,negated_conjecture,
~ sP9 ).
cnf(u1669,negated_conjecture,
~ ndr1_1(a160) ).
cnf(u3879,negated_conjecture,
~ sP10 ).
cnf(u2485,negated_conjecture,
c7_0 ).
cnf(u1686,negated_conjecture,
~ c10_1(a160) ).
cnf(u3905,negated_conjecture,
~ sP11 ).
cnf(u1694,negated_conjecture,
( ~ c9_2(X148,a155)
| ~ c6_1(X148)
| ~ c8_1(X148) ) ).
cnf(u1698,negated_conjecture,
( ~ c7_2(X148,a155)
| ~ c6_1(X148)
| ~ c8_1(X148) ) ).
cnf(u1702,negated_conjecture,
( ~ c6_1(X148)
| ~ c1_2(X148,a155)
| ~ c8_1(X148) ) ).
cnf(u1706,negated_conjecture,
( ~ c6_1(X148)
| ndr1_1(X148)
| ~ c8_1(X148) ) ).
cnf(u1763,negated_conjecture,
~ c6_0 ).
cnf(u3943,negated_conjecture,
~ sP12 ).
cnf(u1805,negated_conjecture,
~ ndr1_1(a145) ).
cnf(u2659,negated_conjecture,
c5_0 ).
cnf(u1815,negated_conjecture,
~ c8_1(a145) ).
cnf(u1819,negated_conjecture,
c1_1(a145) ).
cnf(u1824,negated_conjecture,
( ~ c8_2(X136,a144)
| c3_2(X136,X137)
| ~ c3_2(X136,X138)
| ~ c2_2(X136,X138)
| c7_2(X136,X138)
| ~ ndr1_1(X136)
| ~ c1_2(X136,X137) ) ).
cnf(u1831,negated_conjecture,
( ~ c2_2(X136,X138)
| c6_2(X136,a144)
| ~ c3_2(X136,X138)
| c3_2(X136,X137)
| c7_2(X136,X138)
| ~ ndr1_1(X136)
| ~ c1_2(X136,X137) ) ).
cnf(u1835,negated_conjecture,
( ~ c2_2(X136,X138)
| c10_2(X136,a144)
| ~ c3_2(X136,X138)
| c3_2(X136,X137)
| c7_2(X136,X138)
| ~ ndr1_1(X136)
| ~ c1_2(X136,X137) ) ).
cnf(u1845,negated_conjecture,
~ c7_2(a141,a142) ).
cnf(u1849,negated_conjecture,
~ c3_2(a141,a142) ).
cnf(u1853,negated_conjecture,
~ c10_2(a141,a142) ).
cnf(u1857,negated_conjecture,
ndr1_1(a141) ).
cnf(u1862,negated_conjecture,
( ~ c8_2(a141,X133)
| c10_2(a141,X133)
| c6_2(a141,X133) ) ).
cnf(u1866,negated_conjecture,
~ c9_1(a141) ).
cnf(u3965,negated_conjecture,
~ sP13 ).
cnf(u1898,negated_conjecture,
~ c4_0 ).
cnf(u4000,negated_conjecture,
~ sP14 ).
cnf(u1967,negated_conjecture,
( ~ c7_1(X129)
| ~ c2_2(X129,X131)
| c6_2(X129,X131)
| c3_2(X129,X131)
| ~ ndr1_1(X129)
| ~ c9_2(X129,X130)
| ~ c8_2(X129,X130)
| c1_2(X129,X130) ) ).
cnf(u2976,negated_conjecture,
c3_0 ).
cnf(u1977,negated_conjecture,
c7_2(a127,a128) ).
cnf(u4022,negated_conjecture,
~ sP15 ).
cnf(u1984,negated_conjecture,
c10_2(a127,a128) ).
cnf(u1988,negated_conjecture,
c1_2(a127,a128) ).
cnf(u1992,negated_conjecture,
ndr1_1(a127) ).
cnf(u1996,negated_conjecture,
~ c9_1(a127) ).
cnf(u2000,negated_conjecture,
~ c6_1(a127) ).
cnf(u2007,negated_conjecture,
( ~ c6_2(X124,X126)
| ~ c9_2(X124,X126)
| c8_1(X124)
| ~ c2_2(X124,X126)
| ~ ndr1_1(X124)
| ~ c5_2(X124,X125)
| c8_2(X124,X125)
| c7_2(X124,X125) ) ).
cnf(u2047,negated_conjecture,
( ~ c5_2(X122,X123)
| ~ ndr1_1(X122)
| c4_1(X122)
| ~ c10_2(X122,X123)
| ~ c1_2(X122,X123)
| c9_1(X122) ) ).
cnf(u2053,negated_conjecture,
( ~ c5_1(X120)
| ~ ndr1_1(X120)
| ~ c7_2(X120,X121)
| ~ c10_2(X120,X121)
| c2_2(X120,X121)
| ~ c9_1(X120) ) ).
cnf(u3152,negated_conjecture,
c2_0 ).
cnf(u4048,negated_conjecture,
~ sP16 ).
cnf(u2064,negated_conjecture,
~ c4_2(a119,a120) ).
cnf(u2067,negated_conjecture,
~ c10_0 ).
cnf(u4608,negated_conjecture,
c10_2(a119,a120) ).
cnf(u2075,negated_conjecture,
c1_2(a119,a120) ).
cnf(u2079,negated_conjecture,
ndr1_1(a119) ).
cnf(u2083,negated_conjecture,
c9_1(a119) ).
cnf(u2087,negated_conjecture,
c5_1(a119) ).
cnf(u4075,negated_conjecture,
~ sP17 ).
cnf(u2095,negated_conjecture,
( ~ c4_2(X119,a116)
| c9_1(X119)
| ~ c1_1(X119) ) ).
cnf(u2099,negated_conjecture,
( ~ c3_2(X119,a116)
| c9_1(X119)
| ~ c1_1(X119) ) ).
cnf(u2107,negated_conjecture,
( ~ c1_1(X119)
| ndr1_1(X119)
| c9_1(X119) ) ).
cnf(u2114,negated_conjecture,
( ~ c10_1(X117)
| c1_1(X117)
| c9_1(X117) ) ).
cnf(u2140,negated_conjecture,
~ c10_2(a111,a113) ).
cnf(u2144,negated_conjecture,
c7_2(a111,a113) ).
cnf(u2148,negated_conjecture,
ndr1_1(a111) ).
cnf(u2152,negated_conjecture,
~ c4_2(a111,a112) ).
cnf(u2156,negated_conjecture,
c8_2(a111,a112) ).
cnf(u2160,negated_conjecture,
c6_2(a111,a112) ).
cnf(u2166,negated_conjecture,
( ~ c7_2(a111,X116)
| c6_2(a111,X116)
| c9_2(a111,X116) ) ).
cnf(u2175,negated_conjecture,
( ~ c7_2(X113,a110)
| c7_1(X113)
| ~ c3_2(X113,a109) ) ).
cnf(u2179,negated_conjecture,
( ~ c1_2(X113,a110)
| c7_1(X113)
| ~ c3_2(X113,a109) ) ).
cnf(u2183,negated_conjecture,
( ~ c3_2(X113,a109)
| c9_2(X113,a110)
| c7_1(X113) ) ).
cnf(u2187,negated_conjecture,
( ~ c7_2(X113,a110)
| c7_1(X113)
| ~ c10_2(X113,a109) ) ).
cnf(u2191,negated_conjecture,
( ~ c10_2(X113,a109)
| ~ c1_2(X113,a110)
| c7_1(X113) ) ).
cnf(u2195,negated_conjecture,
( c9_2(X113,a110)
| c7_1(X113)
| ~ c10_2(X113,a109) ) ).
cnf(u2199,negated_conjecture,
( ~ c7_2(X113,a110)
| c7_1(X113)
| c5_2(X113,a109) ) ).
cnf(u2203,negated_conjecture,
( ~ c1_2(X113,a110)
| c7_1(X113)
| c5_2(X113,a109) ) ).
cnf(u2207,negated_conjecture,
( c9_2(X113,a110)
| c7_1(X113)
| c5_2(X113,a109) ) ).
cnf(u2211,negated_conjecture,
( c7_1(X113)
| ndr1_1(X113) ) ).
cnf(u2215,negated_conjecture,
~ c6_2(a107,a108) ).
cnf(u2219,negated_conjecture,
c8_2(a107,a108) ).
cnf(u2223,negated_conjecture,
c5_2(a107,a108) ).
cnf(u2227,negated_conjecture,
ndr1_1(a107) ).
cnf(u2232,negated_conjecture,
( c3_2(a107,X112)
| ~ c7_2(a107,X112)
| c10_2(a107,X112) ) ).
cnf(u2236,negated_conjecture,
c1_1(a107) ).
cnf(u2241,negated_conjecture,
~ c5_2(a104,a106) ).
cnf(u3420,negated_conjecture,
c1_0 ).
cnf(u2248,negated_conjecture,
~ c2_2(a104,a106) ).
cnf(u2252,negated_conjecture,
c4_2(a104,a106) ).
cnf(u2256,negated_conjecture,
ndr1_1(a104) ).
cnf(u2260,negated_conjecture,
~ c2_2(a104,a105) ).
cnf(u2264,negated_conjecture,
c8_2(a104,a105) ).
cnf(u2268,negated_conjecture,
c1_2(a104,a105) ).
cnf(u2273,negated_conjecture,
c1_1(a104) ).
cnf(u2278,negated_conjecture,
sP18 ).
cnf(u2281,negated_conjecture,
( ~ c5_1(X111)
| ~ c8_2(X111,a100) ) ).
cnf(u2285,negated_conjecture,
( ~ c5_1(X111)
| ~ c1_2(X111,a100) ) ).
cnf(u2300,negated_conjecture,
( ~ c2_1(X108)
| ~ ndr1_1(X108)
| ~ c9_2(X108,X109)
| ~ c7_2(X108,X109)
| c2_2(X108,X109) ) ).
cnf(u2325,negated_conjecture,
( ~ c7_1(X106)
| ~ ndr1_1(X106)
| ~ c2_2(X106,X107)
| c5_2(X106,X107)
| c1_2(X106,X107)
| ~ c1_1(X106) ) ).
cnf(u2338,negated_conjecture,
( ~ c8_1(X101)
| c4_1(X101)
| ~ c7_1(X101) ) ).
cnf(u2349,negated_conjecture,
( ~ c10_1(X100)
| ~ c9_1(X100)
| c2_1(X100) ) ).
cnf(u2369,negated_conjecture,
( c7_1(X99)
| c2_1(X99)
| c5_1(X99) ) ).
cnf(u2373,negated_conjecture,
( ~ c6_2(X98,a94)
| c5_1(X98)
| c6_2(X98,a93) ) ).
cnf(u2377,negated_conjecture,
( ~ c3_2(X98,a94)
| c5_1(X98)
| c6_2(X98,a93) ) ).
cnf(u2381,negated_conjecture,
( c1_2(X98,a93)
| ~ c6_2(X98,a94)
| c5_1(X98) ) ).
cnf(u2385,negated_conjecture,
( ~ c3_2(X98,a94)
| c5_1(X98)
| c1_2(X98,a93) ) ).
cnf(u2389,negated_conjecture,
( c5_1(X98)
| ndr1_1(X98) ) ).
cnf(u2451,negated_conjecture,
( ~ c7_2(X91,a87)
| c1_1(X91)
| ~ c9_1(X91) ) ).
cnf(u2456,negated_conjecture,
( ~ c9_1(X91)
| ~ c3_2(X91,a87)
| c1_1(X91) ) ).
cnf(u2460,negated_conjecture,
( ~ c2_2(X91,a87)
| c1_1(X91)
| ~ c9_1(X91) ) ).
cnf(u2464,negated_conjecture,
( c1_1(X91)
| ndr1_1(X91)
| ~ c9_1(X91) ) ).
cnf(u2472,negated_conjecture,
~ c1_1(a86) ).
cnf(u2476,negated_conjecture,
c7_1(a86) ).
cnf(u2546,negated_conjecture,
~ c5_1(a80) ).
cnf(u2554,negated_conjecture,
c7_1(a80) ).
cnf(u2558,negated_conjecture,
c3_1(a80) ).
cnf(u2562,negated_conjecture,
~ ndr1_1(a79) ).
cnf(u2576,negated_conjecture,
~ c3_1(a79) ).
cnf(u2592,negated_conjecture,
( ~ c9_2(X71,a77)
| ~ c6_1(X71)
| ~ ndr1_1(X71)
| ~ c5_2(X71,X72)
| ~ c2_2(X71,X72)
| c7_2(X71,X72) ) ).
cnf(u2596,negated_conjecture,
( ~ c6_1(X71)
| c3_2(X71,a77)
| ~ ndr1_1(X71)
| ~ c5_2(X71,X72)
| ~ c2_2(X71,X72)
| c7_2(X71,X72) ) ).
cnf(u2600,negated_conjecture,
( ~ c6_1(X71)
| c1_2(X71,a77)
| ~ ndr1_1(X71)
| ~ c5_2(X71,X72)
| ~ c2_2(X71,X72)
| c7_2(X71,X72) ) ).
cnf(u2604,negated_conjecture,
( c8_1(X69)
| ~ ndr1_1(X69)
| ~ c3_2(X69,X70)
| ~ c10_2(X69,X70)
| c9_2(X69,X70)
| ~ c2_1(X69) ) ).
cnf(u2932,negated_conjecture,
( ~ c8_2(X50,a55)
| ~ c4_1(X50)
| ~ ndr1_1(X50)
| ~ c6_2(X50,X51)
| c8_2(X50,X51)
| c2_2(X50,X51) ) ).
cnf(u4131,negated_conjecture,
~ sP19 ).
cnf(u2940,negated_conjecture,
( ~ c7_2(X50,a55)
| ~ c4_1(X50)
| ~ ndr1_1(X50)
| ~ c6_2(X50,X51)
| c8_2(X50,X51)
| c2_2(X50,X51) ) ).
cnf(u2952,negated_conjecture,
~ ndr1_1(a51) ).
cnf(u2963,negated_conjecture,
c6_1(a51) ).
cnf(u4169,negated_conjecture,
~ sP20 ).
cnf(u4195,negated_conjecture,
~ sP22 ).
cnf(u3203,negated_conjecture,
~ c8_2(a29,a30) ).
cnf(u4221,negated_conjecture,
~ sP23 ).
cnf(u3211,negated_conjecture,
c7_2(a29,a30) ).
cnf(u3215,negated_conjecture,
c2_2(a29,a30) ).
cnf(u3219,negated_conjecture,
ndr1_1(a29) ).
cnf(u3223,negated_conjecture,
~ c2_1(a29) ).
cnf(u3231,negated_conjecture,
( ~ c3_2(X25,X27)
| c10_2(X25,X26)
| c7_2(X25,X27)
| c6_2(X25,X27)
| ~ ndr1_1(X25)
| c8_2(X25,X26)
| c6_2(X25,X26) ) ).
cnf(u4247,negated_conjecture,
~ sP25 ).
cnf(u3274,negated_conjecture,
( ~ c2_1(X24)
| ~ c8_2(X24,a21)
| c4_1(X24) ) ).
cnf(u3278,negated_conjecture,
( ~ c2_1(X24)
| c4_2(X24,a21)
| c4_1(X24) ) ).
cnf(u3282,negated_conjecture,
( c4_1(X24)
| ndr1_1(X24)
| ~ c2_1(X24) ) ).
cnf(u3286,negated_conjecture,
( ~ c2_1(X23)
| ~ c6_1(X23)
| c7_1(X23) ) ).
cnf(u3296,negated_conjecture,
( c10_1(X17)
| ~ ndr1_1(X17)
| c9_2(X17,X18)
| c8_2(X17,X18)
| c4_2(X17,X18)
| ~ c2_1(X17) ) ).
cnf(u4903,negated_conjecture,
ndr1_1(a19) ).
cnf(u3311,negated_conjecture,
( c8_2(a19,X16)
| c10_2(a19,X16)
| c5_2(a19,X16) ) ).
cnf(u3315,negated_conjecture,
~ c6_1(a19) ).
cnf(u3319,negated_conjecture,
c4_1(a19) ).
cnf(u3360,negated_conjecture,
~ c5_2(a15,a16) ).
cnf(u3364,negated_conjecture,
c8_2(a15,a16) ).
cnf(u3368,negated_conjecture,
c1_2(a15,a16) ).
cnf(u3372,negated_conjecture,
ndr1_1(a15) ).
cnf(u3376,negated_conjecture,
~ c5_1(a15) ).
cnf(u3380,negated_conjecture,
~ c4_1(a15) ).
cnf(u4103,axiom,
~ c9_2(a101,a103) ).
cnf(u4107,axiom,
~ c4_2(a101,a103) ).
cnf(u4111,axiom,
~ c3_2(a101,a103) ).
cnf(u4115,axiom,
ndr1_1(a101) ).
cnf(u4119,axiom,
~ c3_2(a101,a102) ).
cnf(u4123,axiom,
c7_2(a101,a102) ).
cnf(u4129,axiom,
( ~ c5_2(a101,X0)
| c2_2(a101,X0) ) ).
cnf(u4303,negated_conjecture,
~ c7_2(a107,a109) ).
cnf(u4314,negated_conjecture,
c2_2(a180,a110) ).
cnf(u4320,negated_conjecture,
~ c3_2(a180,a109) ).
cnf(u4346,negated_conjecture,
~ c7_2(a107,a116) ).
cnf(u4368,negated_conjecture,
~ c3_2(a180,a110) ).
cnf(u4386,negated_conjecture,
c9_2(a111,a113) ).
cnf(u4401,negated_conjecture,
~ c2_2(a111,a112) ).
cnf(u4407,negated_conjecture,
~ c9_2(a111,a112) ).
cnf(u4418,negated_conjecture,
~ c9_1(a111) ).
cnf(u4426,negated_conjecture,
~ c3_2(a210,a87) ).
cnf(u4431,negated_conjecture,
~ c8_1(a51) ).
cnf(u4448,negated_conjecture,
( ~ c2_2(a86,X0)
| c3_2(a86,X0)
| c6_2(a86,X0) ) ).
cnf(u4453,negated_conjecture,
~ c7_1(a213) ).
cnf(u4718,negated_conjecture,
~ c4_1(a213) ).
cnf(u4464,negated_conjecture,
~ c3_2(a119,a87) ).
cnf(u4479,negated_conjecture,
~ c1_2(a107,a108) ).
cnf(u4493,negated_conjecture,
~ c7_2(a107,a94) ).
cnf(u4507,negated_conjecture,
c5_2(a19,a55) ).
cnf(u4530,negated_conjecture,
~ c7_1(a182) ).
cnf(u4883,negated_conjecture,
~ c9_1(a182) ).
cnf(u4541,negated_conjecture,
c1_1(a182) ).
cnf(u4551,negated_conjecture,
~ c9_1(a180) ).
cnf(u4568,negated_conjecture,
( c4_2(a111,X0)
| c6_2(a111,X0) ) ).
cnf(u4574,negated_conjecture,
~ c1_1(a111) ).
cnf(u4592,negated_conjecture,
c9_2(a119,a120) ).
cnf(u4616,negated_conjecture,
~ c7_2(a119,a120) ).
cnf(u4631,negated_conjecture,
( c8_2(a119,X0)
| c6_2(a119,X0)
| c10_2(a119,X0) ) ).
cnf(u4641,negated_conjecture,
( c8_2(a180,X0)
| c6_2(a180,X0)
| c10_2(a180,X0) ) ).
cnf(u4651,negated_conjecture,
~ c4_1(a180) ).
cnf(u4667,negated_conjecture,
~ c4_1(a119) ).
cnf(u4680,negated_conjecture,
c5_1(a213) ).
cnf(u4693,negated_conjecture,
~ c9_1(a213) ).
cnf(u4707,negated_conjecture,
( c8_2(a213,X0)
| c6_2(a213,X0)
| c10_2(a213,X0) ) ).
cnf(u4737,negated_conjecture,
c8_1(a205) ).
cnf(u4747,negated_conjecture,
~ c6_1(a205) ).
cnf(u4751,negated_conjecture,
c4_1(a205) ).
cnf(u4764,negated_conjecture,
c9_1(a205) ).
cnf(u4779,negated_conjecture,
~ c3_2(a205,a87) ).
cnf(u4800,negated_conjecture,
c7_1(a160) ).
cnf(u4803,negated_conjecture,
~ c6_1(a160) ).
cnf(u4810,negated_conjecture,
c4_2(a160,a21) ).
cnf(u4814,negated_conjecture,
~ c8_2(a160,a21) ).
cnf(u4823,negated_conjecture,
c9_1(a160) ).
cnf(u4838,negated_conjecture,
~ c3_2(a160,a87) ).
cnf(u4855,negated_conjecture,
~ c9_1(a86) ).
cnf(u4862,negated_conjecture,
ndr1_1(a182) ).
cnf(u4913,negated_conjecture,
~ c3_2(a79,a87) ).
cnf(u4919,negated_conjecture,
c5_1(a182) ).
cnf(u4948,negated_conjecture,
c6_2(a182,a100) ).
cnf(u4968,negated_conjecture,
~ c4_2(a182,a100) ).
cnf(u5061,negated_conjecture,
( ~ c8_2(a80,X1)
| c1_2(a80,X1)
| ~ c9_2(a80,X1) ) ).
cnf(u5071,negated_conjecture,
~ c1_1(a80) ).
cnf(u5102,negated_conjecture,
c3_2(a29,a30) ).
cnf(u5120,negated_conjecture,
c2_2(a180,a100) ).
cnf(u5135,negated_conjecture,
~ c3_2(a180,a100) ).
cnf(u5144,negated_conjecture,
~ c1_1(a29) ).
cnf(u5169,negated_conjecture,
c10_2(a180,a100) ).
cnf(u5174,negated_conjecture,
c10_2(a119,a100) ).
cnf(u5179,negated_conjecture,
c10_2(a213,a100) ).
cnf(u4869,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X1)
| ~ c1_1(X0)
| c2_1(X0)
| c5_1(X0) ) ).
cnf(u4849,negated_conjecture,
c9_1(a145) ).
cnf(u4726,negated_conjecture,
~ c3_2(a205,a179) ).
cnf(u5080,negated_conjecture,
( ~ c6_2(X176,X177)
| ~ c9_2(X176,X177)
| c3_1(X176)
| c5_2(X176,X177)
| c5_1(X176) ) ).
cnf(u4872,negated_conjecture,
( ~ c8_2(X0,a100)
| ndr1_1(X0) ) ).
cnf(u4287,negated_conjecture,
( ~ c2_1(X69)
| ~ c3_2(X69,X70)
| ~ c10_2(X69,X70)
| c9_2(X69,X70)
| c8_1(X69) ) ).
cnf(u114,axiom,
( ~ sP21(X0)
| ndr1_1(X0) ) ).
cnf(u4868,negated_conjecture,
( ~ c7_2(a119,X0)
| ~ c10_2(a119,X0)
| c2_2(a119,X0) ) ).
cnf(u4284,negated_conjecture,
( ~ c2_1(X108)
| ~ c9_2(X108,X109)
| ~ c7_2(X108,X109)
| c2_2(X108,X109) ) ).
cnf(u4709,negated_conjecture,
( ~ c2_2(a213,X0)
| c10_2(a213,X0)
| c7_2(a213,X0)
| c6_2(a213,X0) ) ).
cnf(u4547,negated_conjecture,
~ c1_2(a180,a100) ).
cnf(u4468,negated_conjecture,
~ c8_2(a119,a100) ).
cnf(u4470,negated_conjecture,
~ c1_2(a119,a100) ).
cnf(u94,axiom,
( ~ sP24(X0)
| c7_2(X0,a26) ) ).
cnf(u113,axiom,
( ~ sP21(X0)
| ~ c2_2(X0,a42) ) ).
cnf(u4714,negated_conjecture,
c10_2(a213,a214) ).
cnf(u96,axiom,
( ~ sP24(X0)
| ndr1_1(X0) ) ).
cnf(u4846,negated_conjecture,
( ~ c2_1(X17)
| c9_2(X17,X18)
| c8_2(X17,X18)
| c4_2(X17,X18)
| c10_1(X17) ) ).
cnf(u4874,negated_conjecture,
( ~ c1_2(X0,a100)
| ndr1_1(X0) ) ).
cnf(u4943,negated_conjecture,
~ c1_2(a182,a100) ).
cnf(u5081,negated_conjecture,
ndr1_1(a188) ).
cnf(u4727,negated_conjecture,
~ c1_2(a205,a179) ).
cnf(u4941,negated_conjecture,
~ c8_2(a182,a100) ).
cnf(u4847,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_1(X0)
| c2_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| ~ c9_2(X0,X2)
| ~ c8_2(X0,X2)
| c1_2(X0,X2) ) ).
cnf(u4729,negated_conjecture,
ndr1_1(a205) ).
cnf(u112,axiom,
( ~ sP21(X0)
| ~ c6_2(X0,a42) ) ).
cnf(u93,axiom,
( ~ sP24(X0)
| ~ c1_2(X0,a26) ) ).
cnf(u4689,negated_conjecture,
~ c1_2(a213,a100) ).
cnf(u4545,negated_conjecture,
~ c8_2(a180,a100) ).
cnf(u4687,negated_conjecture,
~ c8_2(a213,a100) ).
cnf(u4728,negated_conjecture,
c10_2(a205,a179) ).
cnf(u95,axiom,
( ~ sP24(X0)
| c6_2(X0,a26) ) ).
cnf(u5112,negated_conjecture,
ndr1_1(a80) ).
cnf(u4733,negated_conjecture,
( ~ c7_2(a205,X0)
| ~ c9_2(a205,X0)
| c2_2(a205,X0) ) ).
cnf(u111,axiom,
( ~ sP21(X0)
| ~ c8_2(X0,a42) ) ).
cnf(u4906,negated_conjecture,
c9_1(a79) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN429+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.14/0.17 % Computer : n014.cluster.edu
% 0.14/0.17 % Model : x86_64 x86_64
% 0.14/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.17 % Memory : 8046.5625MB
% 0.14/0.17 % OS : Linux 6.8.0-71-generic
% 0.14/0.17 % CPULimit : 300
% 0.14/0.17 % WCLimit : 300
% 0.14/0.17 % DateTime : Mon Sep 28 15:57:30 UTC 2026
% 0.14/0.18 % CPUTime :
% 0.14/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.21 Running first-order theorem proving
% 0.14/0.21 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
% 6.73/1.71 % (1898188)Detected formulas, will run a generic FOF schedule.
% 6.73/1.71 % (1898198)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3879196453:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 6.73/1.71 % (1898198)Refutation not found, incomplete strategy
% 6.73/1.71 % (1898198)------------------------------
% 6.73/1.71 % (1898198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898198)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898198)Termination reason: Refutation not found, incomplete strategy
% 6.73/1.71 % (1898198)Time elapsed: 0.016 s
% 6.73/1.71 % (1898198)Peak memory usage: 91 MB
% 6.73/1.71 % (1898198)Instructions burned: 45 (million)
% 6.73/1.71 % (1898199)dis-21_1_sil=8000:lcm=predicate:random_seed=2497214647: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)
% 6.73/1.71 % (1898197)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2458407991:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 6.73/1.71 % (1898195)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=859851014:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 6.73/1.71 % (1898194)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=1083297909:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 6.73/1.71 % (1898193)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=3520546361:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 6.73/1.71 % (1898196)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3642019018:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 6.73/1.71 % (1898196)Instruction limit reached!
% 6.73/1.71 % (1898196)------------------------------
% 6.73/1.71 % (1898196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898196)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898196)Termination reason: Instruction limit
% 6.73/1.71 % (1898196)Termination phase: Saturation
% 6.73/1.71 % (1898196)Time elapsed: 0.062 s
% 6.73/1.71 % (1898196)Peak memory usage: 91 MB
% 6.73/1.71 % (1898196)Instructions burned: 109 (million)
% 6.73/1.71 % (1898197)Instruction limit reached!
% 6.73/1.71 % (1898197)------------------------------
% 6.73/1.71 % (1898197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898197)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898197)Termination reason: Instruction limit
% 6.73/1.71 % (1898197)Termination phase: Saturation
% 6.73/1.71 % (1898197)Time elapsed: 0.066 s
% 6.73/1.71 % (1898197)Peak memory usage: 89 MB
% 6.73/1.71 % (1898197)Instructions burned: 121 (million)
% 6.73/1.71 % (1898199)Instruction limit reached!
% 6.73/1.71 % (1898199)------------------------------
% 6.73/1.71 % (1898199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898199)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898199)Termination reason: Instruction limit
% 6.73/1.71 % (1898199)Termination phase: Saturation
% 6.73/1.71 % (1898199)Time elapsed: 0.070 s
% 6.73/1.71 % (1898199)Peak memory usage: 91 MB
% 6.73/1.71 % (1898199)Instructions burned: 130 (million)
% 6.73/1.71 % (1898198)------------------------------
% 6.73/1.71 % (1898198)------------------------------
% 6.73/1.71 % (1898208)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2891293557:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 6.73/1.71 % (1898209)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2348557623:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 6.73/1.71 % (1898207)lrs+10_1_sil=8000:sp=occurrence:random_seed=2011058774:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 6.73/1.71 % (1898208)Refutation not found, incomplete strategy
% 6.73/1.71 % (1898208)------------------------------
% 6.73/1.71 % (1898208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898209)Refutation not found, incomplete strategy
% 6.73/1.71 % (1898209)------------------------------
% 6.73/1.71 % (1898209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898208)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898208)Termination reason: Refutation not found, incomplete strategy
% 6.73/1.71 % (1898208)Time elapsed: 0.027 s
% 6.73/1.71 % (1898209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898208)Peak memory usage: 91 MB
% 6.73/1.71 % (1898209)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898208)Instructions burned: 42 (million)
% 6.73/1.71 % (1898209)Termination reason: Refutation not found, incomplete strategy
% 6.73/1.71 % (1898209)Time elapsed: 0.027 s
% 6.73/1.71 % (1898209)Peak memory usage: 91 MB
% 6.73/1.71 % (1898209)Instructions burned: 41 (million)
% 6.73/1.71 % (1898210)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=2094945259:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 6.73/1.71 % (1898210)Refutation not found, incomplete strategy
% 6.73/1.71 % (1898210)------------------------------
% 6.73/1.71 % (1898210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898210)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898210)Termination reason: Refutation not found, incomplete strategy
% 6.73/1.71 % (1898210)Time elapsed: 0.015 s
% 6.73/1.71 % (1898210)Peak memory usage: 91 MB
% 6.73/1.71 % (1898210)Instructions burned: 43 (million)
% 6.73/1.71 % (1898207)Instruction limit reached!
% 6.73/1.71 % (1898207)------------------------------
% 6.73/1.71 % (1898207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898207)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898207)Termination reason: Instruction limit
% 6.73/1.71 % (1898207)Termination phase: Saturation
% 6.73/1.71 % (1898207)Time elapsed: 0.146 s
% 6.73/1.71 % (1898207)Peak memory usage: 93 MB
% 6.73/1.71 % (1898207)Instructions burned: 287 (million)
% 6.73/1.71 % (1898210)------------------------------
% 6.73/1.71 % (1898210)------------------------------
% 6.73/1.71 % (1898209)------------------------------
% 6.73/1.71 % (1898209)------------------------------
% 6.73/1.71 % (1898208)------------------------------
% 6.73/1.71 % (1898208)------------------------------
% 6.73/1.71 % (1898215)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2454958814:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 6.73/1.71 % (1898216)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=453417810:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 6.73/1.71 % (1898218)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3372344750:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 6.73/1.71 % (1898217)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=99532798:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 6.73/1.71 % (1898215)Instruction limit reached!
% 6.73/1.71 % (1898215)------------------------------
% 6.73/1.71 % (1898215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898215)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898215)Termination reason: Instruction limit
% 6.73/1.71 % (1898215)Termination phase: Saturation
% 6.73/1.71 % (1898215)Time elapsed: 0.165 s
% 6.73/1.71 % (1898215)Peak memory usage: 93 MB
% 6.73/1.71 % (1898215)Instructions burned: 295 (million)
% 6.73/1.71 % (1898217)Instruction limit reached!
% 6.73/1.71 % (1898217)------------------------------
% 6.73/1.71 % (1898217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898217)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898217)Termination reason: Instruction limit
% 6.73/1.71 % (1898217)Termination phase: Saturation
% 6.73/1.71 % (1898217)Time elapsed: 0.065 s
% 6.73/1.71 % (1898217)Peak memory usage: 92 MB
% 6.73/1.71 % (1898217)Instructions burned: 115 (million)
% 6.73/1.71 % (1898218)Instruction limit reached!
% 6.73/1.71 % (1898218)------------------------------
% 6.73/1.71 % (1898218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898218)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898218)Termination reason: Instruction limit
% 6.73/1.71 % (1898218)Termination phase: Saturation
% 6.73/1.71 % (1898218)Time elapsed: 0.067 s
% 6.73/1.71 % (1898218)Peak memory usage: 90 MB
% 6.73/1.71 % (1898218)Instructions burned: 128 (million)
% 6.73/1.71 % (1898223)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1794948463:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 6.73/1.71 % (1898194)First to succeed.
% 6.73/1.71 % (1898194)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1898188"
% 6.73/1.71 % (1898224)lrs+10_1_sil=8000:sp=occurrence:random_seed=322787510:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 6.73/1.71 % (1898225)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2749783814:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 6.73/1.71 % (1898223)Instruction limit reached!
% 6.73/1.71 % (1898223)------------------------------
% 6.73/1.71 % (1898223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898223)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898223)Termination reason: Instruction limit
% 6.73/1.71 % (1898223)Termination phase: Saturation
% 6.73/1.71 % (1898223)Time elapsed: 0.058 s
% 6.73/1.71 % (1898223)Peak memory usage: 90 MB
% 6.73/1.71 % (1898223)Instructions burned: 115 (million)
% 6.73/1.71 % (1898229)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3391357767:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 6.73/1.71 % (1898225)Instruction limit reached!
% 6.73/1.71 % (1898225)------------------------------
% 6.73/1.71 % (1898225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.71 % (1898225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.71 % (1898225)CaDiCaL version: 2.1.3
% 6.73/1.71 % (1898225)Termination reason: Instruction limit
% 6.73/1.71 % (1898225)Termination phase: Saturation
% 6.73/1.71 % (1898225)Time elapsed: 0.227 s
% 6.73/1.71 % (1898225)Peak memory usage: 94 MB
% 6.73/1.71 % (1898225)Instructions burned: 438 (million)
% 6.73/1.71 % SZS status CounterSatisfiable for theBenchmark
% 6.73/1.71 % SZS output start Saturation.
% See solution above
% 6.73/1.72 % SZS output start Definitions and Model Updates.
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c6_1(X0) | ndr1_1(X0) | c6_2(X0,a157) | ~ndr1_0 | ~sP11 is false, set c6_2(X0,a157) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_0 | ~c9_0 | c5_1(X98) | c6_2(X98,a93) | ndr1_1(X98) | ~ndr1_0 is false, set c6_2(X98,a93) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c3_0 | ~c5_0 | ndr1_1(X37) | c6_2(X37,a41) | sP21(X37) | ~ndr1_0 is false, set c6_2(X37,a41) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c4_0 | c4_1(X53) | ~c5_2(X53,a57) | ndr1_1(X53) | ~ndr1_0 is false, set ~c5_2(X53,a57) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c1_0 | ~c9_0 | ~c3_1(X13) | c2_2(X13,a10) | ndr1_1(X13) | ~ndr1_0 is false, set c2_2(X13,a10) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c10_1(X55) | c6_1(X55) | ~c1_1(X55) | ~ndr1_0 | ~c6_1(X56) | ndr1_1(X56) | c2_2(X56,a65) | ~ndr1_0 is false, set c2_2(X56,a65) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c1_0 | ~c9_0 | ~c3_1(X13) | c9_2(X13,a10) | ndr1_1(X13) | ~ndr1_0 is false, set c9_2(X13,a10) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c10_0 | ~c3_0 | c7_1(X113) | ndr1_1(X113) | c9_2(X113,a110) | ~ndr1_0 is false, set c9_2(X113,a110) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c10_0 | ~c3_0 | c7_1(X113) | ndr1_1(X113) | ~c1_2(X113,a110) | ~ndr1_0 is false, set ~c1_2(X113,a110) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c6_1(X0) | ndr1_1(X0) | ~c1_2(X0,a157) | ~ndr1_0 | ~sP11 is false, set ~c1_2(X0,a157) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c10_1(X55) | c6_1(X55) | ~c1_1(X55) | ~ndr1_0 | ~c6_1(X56) | ~c1_2(X56,a64) | ndr1_1(X56) | ~ndr1_0 is false, set ~c1_2(X56,a64) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c3_0 | ~c5_0 | ~c1_2(X37,a40) | ndr1_1(X37) | sP21(X37) | ~ndr1_0 is false, set ~c1_2(X37,a40) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c10_1(X55) | c6_1(X55) | ~c1_1(X55) | ~ndr1_0 | ~c6_1(X56) | ndr1_1(X56) | ~c7_2(X56,a65) | ~ndr1_0 is false, set ~c7_2(X56,a65) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c10_0 | ~c3_0 | c7_1(X113) | ndr1_1(X113) | ~c7_2(X113,a110) | ~ndr1_0 is false, set ~c7_2(X113,a110) to true
% 6.73/1.72 for all groundings, until fixed point,
% 6.73/1.72 whenever c10_0 | c10_2(X25,X26) | c6_2(X25,X26) | c8_2(X25,X26) | ~ndr1_1(X25) | c6_2(X25,X27) | c7_2(X25,X27) | ~c3_2(X25,X27) | ~ndr1_1(X25) | ~ndr1_0 | ~c10_2(X28,a24) | ndr1_1(X28) | sP24(X28) | ~ndr1_0 is false, set ~c10_2(X28,a24) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_1(X0) | ndr1_1(X0) | ~c10_2(X0,a54) | ~ndr1_0 | ~sP19 is false, set ~c10_2(X0,a54) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c10_0 | ~c3_0 | c7_1(X113) | ~c10_2(X113,a109) | ndr1_1(X113) | ~ndr1_0 is false, set ~c10_2(X113,a109) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_1(X0) | ndr1_1(X0) | ~c10_2(X0,a126) | ~ndr1_0 | ~sP15 is false, set ~c10_2(X0,a126) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ndr1_0 | c8_2(a73,X67) | ~c10_2(a73,X67) | ~ndr1_1(a73) is false, set ~c10_2(a73,X67) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c6_1(X0) | c3_2(X0,a156) | ndr1_1(X0) | ~ndr1_0 | ~sP11 is false, set c3_2(X0,a156) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c3_0 | c8_1(X124) | c7_2(X124,X125) | c8_2(X124,X125) | ~c5_2(X124,X125) | ~ndr1_1(X124) | ~c2_2(X124,X126) | ~c6_2(X124,X126) | ~c9_2(X124,X126) | ~ndr1_1(X124) | ~ndr1_0 | c9_1(X127) | ndr1_1(X127) | c3_2(X127,a124) | ~ndr1_0 is false, set c3_2(X127,a124) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_1(X0) | c3_2(X0,a53) | ndr1_1(X0) | ~ndr1_0 | ~sP19 is false, set c3_2(X0,a53) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c3_0 | ~c5_0 | c3_2(X37,a40) | ndr1_1(X37) | sP21(X37) | ~ndr1_0 is false, set c3_2(X37,a40) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c1_0 | ~c9_0 | ~c3_1(X13) | ndr1_1(X13) | ~c6_2(X13,a11) | ~ndr1_0 is false, set ~c6_2(X13,a11) to true
% 6.73/1.72 for all groundings, until fixed point,
% 6.73/1.72 whenever c10_0 | c10_2(X25,X26) | c6_2(X25,X26) | c8_2(X25,X26) | ~ndr1_1(X25) | c6_2(X25,X27) | c7_2(X25,X27) | ~c3_2(X25,X27) | ~ndr1_1(X25) | ~ndr1_0 | ndr1_1(X28) | ~c6_2(X28,a25) | sP24(X28) | ~ndr1_0 is false, set ~c6_2(X28,a25) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_0 | ~c9_0 | c5_1(X98) | ndr1_1(X98) | ~c6_2(X98,a94) | ~ndr1_0 is false, set ~c6_2(X98,a94) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_1(X0) | ~c6_2(X0,a53) | ndr1_1(X0) | ~ndr1_0 | ~sP19 is false, set ~c6_2(X0,a53) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_1(X0) | ndr1_1(X0) | ~c6_2(X0,a168) | ~ndr1_0 | ~sP9 is false, set ~c6_2(X0,a168) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c3_0 | c8_1(X124) | c7_2(X124,X125) | c8_2(X124,X125) | ~c5_2(X124,X125) | ~ndr1_1(X124) | ~c2_2(X124,X126) | ~c6_2(X124,X126) | ~c9_2(X124,X126) | ~ndr1_1(X124) | ~ndr1_0 | c9_1(X127) | ndr1_1(X127) | ~c6_2(X127,a124) | ~ndr1_0 is false, set ~c6_2(X127,a124) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_1(X0) | ndr1_1(X0) | ~c6_2(X0,a54) | ~ndr1_0 | ~sP19 is false, set ~c6_2(X0,a54) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c6_1(X0) | c10_2(X0,a156) | ndr1_1(X0) | ~ndr1_0 | ~sP11 is false, set c10_2(X0,a156) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_1(X0) | ~c8_2(X0,a125) | ndr1_1(X0) | ~ndr1_0 | ~sP15 is false, set ~c8_2(X0,a125) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c10_1(X55) | c6_1(X55) | ~c1_1(X55) | ~ndr1_0 | ~c6_1(X56) | c10_2(X56,a64) | ndr1_1(X56) | ~ndr1_0 is false, set c10_2(X56,a64) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_1(X0) | c10_2(X0,a167) | ndr1_1(X0) | ~ndr1_0 | ~sP9 is false, set c10_2(X0,a167) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c3_0 | ~c5_0 | ndr1_1(X37) | ~c9_2(X37,a41) | sP21(X37) | ~ndr1_0 is false, set ~c9_2(X37,a41) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c4_0 | c4_1(X53) | ~c9_2(X53,a57) | ndr1_1(X53) | ~ndr1_0 is false, set ~c9_2(X53,a57) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c4_0 | c4_1(X53) | ndr1_1(X53) | ~c9_2(X53,a58) | ~ndr1_0 is false, set ~c9_2(X53,a58) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c10_1(X55) | c6_1(X55) | ~c1_1(X55) | ~ndr1_0 | ~c6_1(X56) | ~c9_2(X56,a64) | ndr1_1(X56) | ~ndr1_0 is false, set ~c9_2(X56,a64) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_1(X0) | c4_2(X0,a125) | ndr1_1(X0) | ~ndr1_0 | ~sP15 is false, set c4_2(X0,a125) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_1(X0) | ndr1_1(X0) | c4_2(X0,a126) | ~ndr1_0 | ~sP15 is false, set c4_2(X0,a126) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c4_0 | c4_1(X53) | c4_2(X53,a57) | ndr1_1(X53) | ~ndr1_0 is false, set c4_2(X53,a57) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c10_1(X55) | c6_1(X55) | ~c1_1(X55) | ~ndr1_0 | ~c6_1(X56) | ndr1_1(X56) | c4_2(X56,a65) | ~ndr1_0 is false, set c4_2(X56,a65) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c3_0 | ~c5_0 | ndr1_1(X37) | ~c4_2(X37,a41) | sP21(X37) | ~ndr1_0 is false, set ~c4_2(X37,a41) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c3_0 | c8_1(X124) | c7_2(X124,X125) | c8_2(X124,X125) | ~c5_2(X124,X125) | ~ndr1_1(X124) | ~c2_2(X124,X126) | ~c6_2(X124,X126) | ~c9_2(X124,X126) | ~ndr1_1(X124) | ~ndr1_0 | c9_1(X127) | ~c4_2(X127,a123) | ndr1_1(X127) | ~ndr1_0 is false, set ~c4_2(X127,a123) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c3_0 | c8_1(X124) | c7_2(X124,X125) | c8_2(X124,X125) | ~c5_2(X124,X125) | ~ndr1_1(X124) | ~c2_2(X124,X126) | ~c6_2(X124,X126) | ~c9_2(X124,X126) | ~ndr1_1(X124) | ~ndr1_0 | c9_1(X127) | ndr1_1(X127) | ~c4_2(X127,a124) | ~ndr1_0 is false, set ~c4_2(X127,a124) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c1_0 | ~c9_0 | ~c3_1(X13) | ndr1_1(X13) | ~c4_2(X13,a11) | ~ndr1_0 is false, set ~c4_2(X13,a11) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | c10_2(X25,X26) | c6_2(X25,X26) | c8_2(X25,X26) | ~ndr1_1(X25) | c6_2(X25,X27) | c7_2(X25,X27) | ~c3_2(X25,X27) | ~ndr1_1(X25) | ~ndr1_0 | ~c4_2(X28,a24) | ndr1_1(X28) | sP24(X28) | ~ndr1_0 is false, set ~c4_2(X28,a24) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c6_1(X0) | ~c2_2(X0,a156) | ndr1_1(X0) | ~ndr1_0 | ~sP11 is false, set ~c2_2(X0,a156) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | c10_2(X25,X26) | c6_2(X25,X26) | c8_2(X25,X26) | ~ndr1_1(X25) | c6_2(X25,X27) | c7_2(X25,X27) | ~c3_2(X25,X27) | ~ndr1_1(X25) | ~ndr1_0 | ndr1_1(X28) | ~c2_2(X28,a25) | sP24(X28) | ~ndr1_0 is false, set ~c2_2(X28,a25) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c4_0 | c4_1(X53) | ndr1_1(X53) | ~c2_2(X53,a58) | ~ndr1_0 is false, set ~c2_2(X53,a58) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_1(X0) | ndr1_1(X0) | c8_2(X0,a54) | ~ndr1_0 | ~sP19 is false, set c8_2(X0,a54) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_1(X0) | c8_2(X0,a167) | ndr1_1(X0) | ~ndr1_0 | ~sP9 is false, set c8_2(X0,a167) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c6_1(X0) | ndr1_1(X0) | c8_2(X0,a157) | ~ndr1_0 | ~sP11 is false, set c8_2(X0,a157) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c3_0 | ~c5_0 | c5_2(X37,a40) | ndr1_1(X37) | sP21(X37) | ~ndr1_0 is false, set c5_2(X37,a40) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c10_0 | ~c3_0 | c7_1(X113) | c5_2(X113,a109) | ndr1_1(X113) | ~ndr1_0 is false, set c5_2(X113,a109) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_1(X0) | ndr1_1(X0) | c5_2(X0,a168) | ~ndr1_0 | ~sP9 is false, set c5_2(X0,a168) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c3_0 | c8_1(X124) | c7_2(X124,X125) | c8_2(X124,X125) | ~c5_2(X124,X125) | ~ndr1_1(X124) | ~c2_2(X124,X126) | ~c6_2(X124,X126) | ~c9_2(X124,X126) | ~ndr1_1(X124) | ~ndr1_0 | c9_1(X127) | c7_2(X127,a123) | ndr1_1(X127) | ~ndr1_0 is false, set c7_2(X127,a123) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c4_0 | c4_1(X53) | ndr1_1(X53) | ~c3_2(X53,a58) | ~ndr1_0 is false, set ~c3_2(X53,a58) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c10_2(a72,X66) | c5_2(a72,X66) | ~c3_2(a72,X66) | ~ndr1_1(a72) | ndr1_0 is false, set ~c3_2(a72,X66) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_0 | ~c9_0 | c5_1(X98) | ndr1_1(X98) | ~c3_2(X98,a94) | ~ndr1_0 is false, set ~c3_2(X98,a94) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c10_0 | ~c3_0 | c7_1(X113) | ~c3_2(X113,a109) | ndr1_1(X113) | ~ndr1_0 is false, set ~c3_2(X113,a109) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | c10_2(X25,X26) | c6_2(X25,X26) | c8_2(X25,X26) | ~ndr1_1(X25) | c6_2(X25,X27) | c7_2(X25,X27) | ~c3_2(X25,X27) | ~ndr1_1(X25) | ~ndr1_0 | ndr1_1(X28) | c1_2(X28,a25) | sP24(X28) | ~ndr1_0 is false, set c1_2(X28,a25) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_1(X0) | c1_2(X0,a53) | ndr1_1(X0) | ~ndr1_0 | ~sP19 is false, set c1_2(X0,a53) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_1(X0) | ndr1_1(X0) | c1_2(X0,a168) | ~ndr1_0 | ~sP9 is false, set c1_2(X0,a168) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_1(X0) | c1_2(X0,a167) | ndr1_1(X0) | ~ndr1_0 | ~sP9 is false, set c1_2(X0,a167) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_1(X0) | c1_2(X0,a125) | ndr1_1(X0) | ~ndr1_0 | ~sP15 is false, set c1_2(X0,a125) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c1_0 | ~c9_0 | ~c3_1(X13) | c1_2(X13,a10) | ndr1_1(X13) | ~ndr1_0 is false, set c1_2(X13,a10) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c1_0 | ~c9_0 | ~c3_1(X13) | ndr1_1(X13) | c1_2(X13,a11) | ~ndr1_0 is false, set c1_2(X13,a11) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | c10_2(X25,X26) | c6_2(X25,X26) | c8_2(X25,X26) | ~ndr1_1(X25) | c6_2(X25,X27) | c7_2(X25,X27) | ~c3_2(X25,X27) | ~ndr1_1(X25) | ~ndr1_0 | c1_2(X28,a24) | ndr1_1(X28) | sP24(X28) | ~ndr1_0 is false, set c1_2(X28,a24) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_0 | ~c9_0 | c5_1(X98) | c1_2(X98,a93) | ndr1_1(X98) | ~ndr1_0 is false, set c1_2(X98,a93) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c3_0 | c8_1(X124) | c7_2(X124,X125) | c8_2(X124,X125) | ~c5_2(X124,X125) | ~ndr1_1(X124) | ~c2_2(X124,X126) | ~c6_2(X124,X126) | ~c9_2(X124,X126) | ~ndr1_1(X124) | ~ndr1_0 | c9_1(X127) | c1_2(X127,a123) | ndr1_1(X127) | ~ndr1_0 is false, set c1_2(X127,a123) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c1_1(a72) | ndr1_0 is false, set c1_1(a72) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_0 | ~c3_0 | c9_2(X92,X93) | ~c3_2(X92,X93) | ~c5_2(X92,X93) | ~ndr1_1(X92) | ndr1_1(X92) | ~ndr1_0 is false, set ~c3_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c5_1(X188) | ~c9_1(X188) | c5_2(X188,X189) | ~c10_2(X188,X189) | ~c8_2(X188,X189) | ~ndr1_1(X188) | ~ndr1_0 | ~c9_1(X190) | c2_2(X190,X191) | c5_2(X190,X191) | ~ndr1_1(X190) | c2_2(X190,X192) | ~c10_2(X190,X192) | ~c6_2(X190,X192) | ~ndr1_1(X190) | ~ndr1_0 | ndr1_0 is false, set ~c5_1(X188) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c9_1(X61) | c10_2(X61,X62) | c4_2(X61,X62) | c9_2(X61,X62) | ~ndr1_1(X61) | ndr1_1(X61) | ~ndr1_0 | c1_2(a71,X63) | ~c4_2(a71,X63) | ~c8_2(a71,X63) | ~ndr1_1(a71) is false, set c5_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c9_1(X61) | c10_2(X61,X62) | c4_2(X61,X62) | c9_2(X61,X62) | ~ndr1_1(X61) | ndr1_1(X61) | ~ndr1_0 | c5_2(a71,X65) | ~c4_2(a71,X65) | ~c6_2(a71,X65) | ~ndr1_1(a71) is false, set c5_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c9_1(X61) | c10_2(X61,X62) | c4_2(X61,X62) | c9_2(X61,X62) | ~ndr1_1(X61) | ~c10_2(X61,a70) | ~ndr1_0 | ndr1_0 is false, set c5_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c9_1(X61) | c10_2(X61,X62) | c4_2(X61,X62) | c9_2(X61,X62) | ~ndr1_1(X61) | ndr1_1(X61) | ~ndr1_0 | ndr1_0 is false, set c5_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c9_1(X61) | c10_2(X61,X62) | c4_2(X61,X62) | c9_2(X61,X62) | ~ndr1_1(X61) | ndr1_1(X61) | ~ndr1_0 | c2_2(a71,X64) | c7_2(a71,X64) | ~c10_2(a71,X64) | ~ndr1_1(a71) is false, set c5_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c9_1(X61) | c10_2(X61,X62) | c4_2(X61,X62) | c9_2(X61,X62) | ~ndr1_1(X61) | c8_2(X61,a70) | ~ndr1_0 | ndr1_0 is false, set c5_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c9_1(X61) | c10_2(X61,X62) | c4_2(X61,X62) | c9_2(X61,X62) | ~ndr1_1(X61) | ~c6_2(X61,a70) | ~ndr1_0 | ndr1_0 is false, set c5_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c2_1(X57) | c6_1(X57) | ~c1_2(X57,a66) | ~ndr1_0 | ndr1_0 is false, set c2_1(X57) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c2_1(X57) | c6_1(X57) | ~c7_2(X57,a66) | ~ndr1_0 | ndr1_0 is false, set c2_1(X57) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c2_1(X57) | c6_1(X57) | ndr1_1(X57) | ~ndr1_0 | ndr1_0 is false, set c2_1(X57) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c2_1(X57) | c6_1(X57) | ~c5_2(X57,a66) | ~ndr1_0 | ndr1_0 is false, set c2_1(X57) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_0 | ~c2_1(X108) | c2_2(X108,X109) | ~c7_2(X108,X109) | ~c9_2(X108,X109) | ~ndr1_1(X108) | ~ndr1_0 | ndr1_0 is false, set ~c2_1(X108) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c9_0 | c6_1(X95) | ~c10_1(X95) | c3_2(X95,X96) | c9_2(X95,X96) | ~c8_2(X95,X96) | ~ndr1_1(X95) | ~ndr1_0 | ndr1_0 is false, set ~c10_1(X95) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c1_0 | c2_1(X100) | ~c10_1(X100) | ~c9_1(X100) | ~ndr1_0 | ndr1_0 is false, set ~c10_1(X100) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c10_0 | c1_1(X117) | c9_1(X117) | ~c10_1(X117) | ~ndr1_0 | ndr1_0 is false, set ~c10_1(X117) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ~c3_1(a72) | ndr1_0 is false, set ~c3_1(a72) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | ndr1_0 | ~c6_1(a73) is false, set ~c6_1(a73) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c5_1(X59) | ~c10_1(X59) | c3_2(X59,a68) | ~ndr1_0 | ndr1_0 is false, set c5_1(X59) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | c10_1(X17) | ~c2_1(X17) | c4_2(X17,X18) | c8_2(X17,X18) | c9_2(X17,X18) | ~ndr1_1(X17) | ~ndr1_0 | ~c2_1(X19) | c5_2(X19,X20) | c6_2(X19,X20) | ~c2_2(X19,X20) | ~ndr1_1(X19) | ndr1_1(X19) | ~ndr1_0 is false, set c10_1(X17) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_1(X172) | c2_1(X172) | ~ndr1_0 | c1_2(X173,X174) | ~c10_2(X173,X174) | ~ndr1_1(X173) | c4_2(X173,X175) | c5_2(X173,X175) | c7_2(X173,X175) | ~ndr1_1(X173) | ndr1_1(X173) | ~ndr1_0 | ~c9_1(a186) is false, set c10_1(X172) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_1(X172) | c2_1(X172) | ~ndr1_0 | c1_2(X173,X174) | ~c10_2(X173,X174) | ~ndr1_1(X173) | c4_2(X173,X175) | c5_2(X173,X175) | c7_2(X173,X175) | ~ndr1_1(X173) | ndr1_1(X173) | ~ndr1_0 | ~c2_1(a186) is false, set c10_1(X172) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_1(X172) | c2_1(X172) | ~ndr1_0 | c1_2(X173,X174) | ~c10_2(X173,X174) | ~ndr1_1(X173) | c4_2(X173,X175) | c5_2(X173,X175) | c7_2(X173,X175) | ~ndr1_1(X173) | ~c3_2(X173,a185) | ~ndr1_0 | ndr1_0 is false, set c10_1(X172) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_1(X172) | c2_1(X172) | ~ndr1_0 | c1_2(X173,X174) | ~c10_2(X173,X174) | ~ndr1_1(X173) | c4_2(X173,X175) | c5_2(X173,X175) | c7_2(X173,X175) | ~ndr1_1(X173) | ndr1_1(X173) | ~ndr1_0 | ndr1_0 is false, set c10_1(X172) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_1(X172) | c2_1(X172) | ~ndr1_0 | c1_2(X173,X174) | ~c10_2(X173,X174) | ~ndr1_1(X173) | c4_2(X173,X175) | c5_2(X173,X175) | c7_2(X173,X175) | ~ndr1_1(X173) | ~c5_2(X173,a185) | ~ndr1_0 | ndr1_0 is false, set c10_1(X172) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_1(X172) | c2_1(X172) | ~ndr1_0 | c1_2(X173,X174) | ~c10_2(X173,X174) | ~ndr1_1(X173) | c4_2(X173,X175) | c5_2(X173,X175) | c7_2(X173,X175) | ~ndr1_1(X173) | ~c6_2(X173,a185) | ~ndr1_0 | ndr1_0 is false, set c10_1(X172) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c5_1(X59) | ~c10_1(X59) | ndr1_1(X59) | ~ndr1_0 | ndr1_0 is false, set c5_1(X59) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c5_1(X59) | ~c10_1(X59) | c10_2(X59,a68) | ~ndr1_0 | ndr1_0 is false, set c5_1(X59) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c5_0 | c5_1(X59) | ~c10_1(X59) | c7_2(X59,a68) | ~ndr1_0 | ndr1_0 is false, set c5_1(X59) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c3_1(X176) | c5_1(X176) | c5_2(X176,X177) | ~c6_2(X176,X177) | ~c9_2(X176,X177) | ~ndr1_1(X176) | ~ndr1_0 | ndr1_0 | c7_2(a188,X178) | ~c2_2(a188,X178) | ~c8_2(a188,X178) | ~ndr1_1(a188) is false, set c3_1(X176) to true
% 6.73/1.72 for all groundings, until fixed point,
% 6.73/1.72 whenever c3_1(X176) | c5_1(X176) | c5_2(X176,X177) | ~c6_2(X176,X177) | ~c9_2(X176,X177) | ~ndr1_1(X176) | ~ndr1_0 | ndr1_0 | ~c3_1(a188) is false, set c3_1(X176) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c3_1(X176) | c5_1(X176) | c5_2(X176,X177) | ~c6_2(X176,X177) | ~c9_2(X176,X177) | ~ndr1_1(X176) | ~ndr1_0 | ndr1_0 | ~c9_1(a188) is false, set c3_1(X176) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c3_1(X176) | c5_1(X176) | c5_2(X176,X177) | ~c6_2(X176,X177) | ~c9_2(X176,X177) | ~ndr1_1(X176) | ~ndr1_0 | ndr1_0 | ndr1_0 is false, set c3_1(X176) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_1(X172) | c2_1(X172) | ~ndr1_0 | c1_2(X173,X174) | ~c10_2(X173,X174) | ~ndr1_1(X173) | c4_2(X173,X175) | c5_2(X173,X175) | c7_2(X173,X175) | ~ndr1_1(X173) | ndr1_1(X173) | ~ndr1_0 | c3_1(a186) is false, set c3_1(a186) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c3_1(X176) | c5_1(X176) | c5_2(X176,X177) | ~c6_2(X176,X177) | ~c9_2(X176,X177) | ~ndr1_1(X176) | ~ndr1_0 | c3_1(a187) | ndr1_0 is false, set c3_1(X176) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c6_0 | ~c3_0 | ~c6_1(X71) | c7_2(X71,X72) | ~c2_2(X71,X72) | ~c5_2(X71,X72) | ~ndr1_1(X71) | ndr1_1(X71) | ~ndr1_0 is false, set c6_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c6_0 | ~c6_1(X73) | c2_2(X73,X74) | ~c9_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | ~ndr1_0 | ndr1_0 is false, set c6_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c6_0 | ~c6_1(X73) | c2_2(X73,X74) | ~c9_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | ~ndr1_0 | c1_2(a79,X75) | c6_2(a79,X75) | ~c10_2(a79,X75) | ~ndr1_1(a79) is false, set c6_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c6_0 | ~c6_1(X73) | c2_2(X73,X74) | ~c9_2(X73,X74) | ~ndr1_1(X73) | ~c3_2(X73,a78) | ~ndr1_0 | ndr1_0 is false, set c6_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c6_0 | ~c6_1(X73) | c2_2(X73,X74) | ~c9_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | ~ndr1_0 | c4_2(a79,X76) | c7_2(a79,X76) | c8_2(a79,X76) | ~ndr1_1(a79) is false, set c6_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c6_0 | ~c6_1(X73) | c2_2(X73,X74) | ~c9_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | ~ndr1_0 | ~c3_1(a79) is false, set c6_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c6_0 | ~c6_1(X73) | c2_2(X73,X74) | ~c9_2(X73,X74) | ~ndr1_1(X73) | ~c7_2(X73,a78) | ~ndr1_0 | ndr1_0 is false, set c6_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c6_0 | ~c6_1(X73) | c2_2(X73,X74) | ~c9_2(X73,X74) | ~ndr1_1(X73) | ~c9_2(X73,a78) | ~ndr1_0 | ndr1_0 is false, set c6_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c6_0 | c1_2(X77,X78) | c5_2(X77,X78) | c6_2(X77,X78) | ~ndr1_1(X77) | c10_2(X77,X79) | c5_2(X77,X79) | ~c9_2(X77,X79) | ~ndr1_1(X77) | c4_2(X77,X80) | c6_2(X77,X80) | ~ndr1_1(X77) | ~ndr1_0 | ndr1_0 is false, set c6_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c3_1(X176) | c5_1(X176) | c5_2(X176,X177) | ~c6_2(X176,X177) | ~c9_2(X176,X177) | ~ndr1_1(X176) | ~ndr1_0 | ~c1_1(a187) | ndr1_0 is false, set ~c1_1(a187) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | ~c4_0 | c10_2(X14,X15) | ~c2_2(X14,X15) | ~c9_2(X14,X15) | ~ndr1_1(X14) | ndr1_1(X14) | c1_2(X14,a18) | ~ndr1_0 is false, set ~c4_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | ~c4_0 | c10_2(X14,X15) | ~c2_2(X14,X15) | ~c9_2(X14,X15) | ~ndr1_1(X14) | ndr1_1(X14) | ndr1_1(X14) | ~ndr1_0 is false, set ~c4_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | ~c4_0 | c10_2(X14,X15) | ~c2_2(X14,X15) | ~c9_2(X14,X15) | ~ndr1_1(X14) | ndr1_1(X14) | ~c5_2(X14,a18) | ~ndr1_0 is false, set ~c4_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | ~c4_0 | c10_2(X14,X15) | ~c2_2(X14,X15) | ~c9_2(X14,X15) | ~ndr1_1(X14) | ndr1_1(X14) | ~c9_2(X14,a18) | ~ndr1_0 is false, set ~c4_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | ~c4_0 | c10_2(X14,X15) | ~c2_2(X14,X15) | ~c9_2(X14,X15) | ~ndr1_1(X14) | c1_2(X14,a17) | ndr1_1(X14) | ~ndr1_0 is false, set ~c4_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | ~c4_0 | c10_2(X14,X15) | ~c2_2(X14,X15) | ~c9_2(X14,X15) | ~ndr1_1(X14) | c2_2(X14,a17) | ndr1_1(X14) | ~ndr1_0 is false, set ~c4_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever c10_0 | ~c4_0 | c10_2(X14,X15) | ~c2_2(X14,X15) | ~c9_2(X14,X15) | ~ndr1_1(X14) | c6_2(X14,a17) | ndr1_1(X14) | ~ndr1_0 is false, set ~c4_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c9_0 | c7_1(X164) | c10_2(X164,X165) | c9_2(X164,X165) | ~c2_2(X164,X165) | ~ndr1_1(X164) | ndr1_1(X164) | ~ndr1_0 | ~c2_1(X166) | c10_2(X166,a179) | ~ndr1_0 is false, set ~c9_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c9_0 | c7_1(X164) | c10_2(X164,X165) | c9_2(X164,X165) | ~c2_2(X164,X165) | ~ndr1_1(X164) | ndr1_1(X164) | ~ndr1_0 | ~c2_1(X166) | ndr1_1(X166) | ~ndr1_0 is false, set ~c9_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c9_0 | c7_1(X164) | c10_2(X164,X165) | c9_2(X164,X165) | ~c2_2(X164,X165) | ~ndr1_1(X164) | ndr1_1(X164) | ~ndr1_0 | ~c2_1(X166) | ~c1_2(X166,a179) | ~ndr1_0 is false, set ~c9_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c9_0 | c7_1(X164) | c10_2(X164,X165) | c9_2(X164,X165) | ~c2_2(X164,X165) | ~ndr1_1(X164) | ndr1_1(X164) | ~ndr1_0 | ~c2_1(X166) | ~c3_2(X166,a179) | ~ndr1_0 is false, set ~c9_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c9_0 | c4_2(X167,X168) | ~c3_2(X167,X168) | ~c7_2(X167,X168) | ~ndr1_1(X167) | c5_2(X167,X169) | ~c1_2(X167,X169) | ~c7_2(X167,X169) | ~ndr1_1(X167) | ~c10_2(X167,X170) | ~c5_2(X167,X170) | ~c6_2(X167,X170) | ~ndr1_1(X167) | ~ndr1_0 | ndr1_0 is false, set ~c9_0 to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c5_0 | ~c8_1(X134) | c6_2(X134,X135) | c7_2(X134,X135) | ~ndr1_1(X134) | ndr1_1(X134) | ~ndr1_0 | c3_2(X136,X137) | ~c1_2(X136,X137) | ~ndr1_1(X136) | c7_2(X136,X138) | ~c2_2(X136,X138) | ~c3_2(X136,X138) | ~ndr1_1(X136) | c6_2(X136,a144) | ~ndr1_0 is false, set ~c8_1(X134) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c5_0 | ~c8_1(X134) | c6_2(X134,X135) | c7_2(X134,X135) | ~ndr1_1(X134) | ndr1_1(X134) | ~ndr1_0 | c3_2(X136,X137) | ~c1_2(X136,X137) | ~ndr1_1(X136) | c7_2(X136,X138) | ~c2_2(X136,X138) | ~c3_2(X136,X138) | ~ndr1_1(X136) | c10_2(X136,a144) | ~ndr1_0 is false, set ~c8_1(X134) to true
% 6.73/1.72 for all groundings,
% 6.73/1.72 whenever ~c5_0 | ~c8_1(X134) | c6_2(X134,X135) | c7_2(X134,X135) | ~ndr1_1(X134) | c10_2(X134,a143) | ~ndr1_0 | c3_2(X136,X137) | ~c1_2(X136,X137) | ~ndr1_1(X136) | c7_2(X136,X138) | ~c2_2(X136,X138) | ~c3_2(X136,X138) | ~ndr1_1(X136) | ndr1_1(X136) | ~ndr1_0 is false, set ~c8_1(X134) to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c5_0 | ~c8_1(X134) | c6_2(X134,X135) | c7_2(X134,X135) | ~ndr1_1(X134) | ndr1_1(X134) | ~ndr1_0 | c3_2(X136,X137) | ~c1_2(X136,X137) | ~ndr1_1(X136) | c7_2(X136,X138) | ~c2_2(X136,X138) | ~c3_2(X136,X138) | ~ndr1_1(X136) | ~c8_2(X136,a144) | ~ndr1_0 is false, set ~c8_1(X134) to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c5_0 | ~c8_1(X134) | c6_2(X134,X135) | c7_2(X134,X135) | ~ndr1_1(X134) | ndr1_1(X134) | ~ndr1_0 | c3_2(X136,X137) | ~c1_2(X136,X137) | ~ndr1_1(X136) | c7_2(X136,X138) | ~c2_2(X136,X138) | ~c3_2(X136,X138) | ~ndr1_1(X136) | ndr1_1(X136) | ~ndr1_0 is false, set ~c8_1(X134) to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c5_0 | ~c8_1(X134) | c6_2(X134,X135) | c7_2(X134,X135) | ~ndr1_1(X134) | c5_2(X134,a143) | ~ndr1_0 | c3_2(X136,X137) | ~c1_2(X136,X137) | ~ndr1_1(X136) | c7_2(X136,X138) | ~c2_2(X136,X138) | ~c3_2(X136,X138) | ~ndr1_1(X136) | ndr1_1(X136) | ~ndr1_0 is false, set ~c8_1(X134) to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c7_0 | ~c7_1(X86) | ~c8_1(X86) | c1_2(X86,X87) | c7_2(X86,X87) | c9_2(X86,X87) | ~ndr1_1(X86) | ~ndr1_0 | c10_2(X88,X89) | c4_2(X88,X89) | c7_2(X88,X89) | ~ndr1_1(X88) | c4_2(X88,X90) | ~c3_2(X88,X90) | ~c5_2(X88,X90) | ~ndr1_1(X88) | ndr1_1(X88) | ~ndr1_0 is false, set ~c8_1(X86) to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c3_1(X176) | c5_1(X176) | c5_2(X176,X177) | ~c6_2(X176,X177) | ~c9_2(X176,X177) | ~ndr1_1(X176) | ~ndr1_0 | ~c8_1(a187) | ndr1_0 is false, set ~c8_1(a187) to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever sP1 | ndr1_0 is false, set sP1 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c8_0 | sP9 | ndr1_0 is false, set sP9 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c4_0 | sP19 | ~c4_1(X50) | c2_2(X50,X51) | c8_2(X50,X51) | ~c6_2(X50,X51) | ~ndr1_1(X50) | ndr1_1(X50) | ~ndr1_0 is false, set sP19 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ndr1_0 | ~sP3 is false, set ~sP3 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c5_0 | ndr1_0 | c4_1(a73) is false, set c4_1(a73) to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c1_0 | c4_1(X101) | ~c7_1(X101) | ~c8_1(X101) | ~ndr1_0 | ndr1_0 is false, set c4_1(X101) to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c6_0 | c1_1(X140) | c4_1(X140) | ~c5_1(X140) | ~ndr1_0 | ndr1_0 is false, set c4_1(X140) to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c8_0 | c6_1(X156) | c6_2(X156,X157) | ~c2_2(X156,X157) | ~c4_2(X156,X157) | ~ndr1_1(X156) | c9_2(X156,X158) | ~c2_2(X156,X158) | ~c3_2(X156,X158) | ~ndr1_1(X156) | ~ndr1_0 | ndr1_0 is false, set ~c8_0 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c8_0 | ~c2_1(X161) | ~c7_1(X161) | c10_2(X161,X162) | c4_2(X161,X162) | ~c6_2(X161,X162) | ~ndr1_1(X161) | ~ndr1_0 | ndr1_0 is false, set ~c8_0 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c8_0 | c3_1(X152) | c6_2(X152,X153) | ~c4_2(X152,X153) | ~c9_2(X152,X153) | ~ndr1_1(X152) | ~ndr1_0 | ndr1_0 is false, set ~c8_0 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c4_0 | ~c8_0 | c7_1(X48) | c7_2(X48,X49) | ~c1_2(X48,X49) | ~c4_2(X48,X49) | ~ndr1_1(X48) | ndr1_1(X48) | ~ndr1_0 is false, set ~c8_0 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c3_0 | sP15 | ndr1_0 is false, set sP15 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c3_1(X179) | c5_2(X179,X180) | ~c2_2(X179,X180) | ~c9_2(X179,X180) | ~ndr1_1(X179) | c9_2(X179,X181) | ~c4_2(X179,X181) | ~c6_2(X179,X181) | ~ndr1_1(X179) | ~ndr1_0 | sP5 | ndr1_0 is false, set sP5 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c9_2(X0,X1) | ~c6_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | c3_2(X0,a209) | ~ndr1_0 | ~sP1 is false, set ~sP1 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c9_2(X0,X1) | ~c6_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c10_2(X0,a209) | ~ndr1_0 | ~sP1 is false, set ~sP1 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c9_2(X0,X1) | ~c6_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | c2_2(X0,a208) | ndr1_1(X0) | ~ndr1_0 | ~sP1 is false, set ~sP1 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c9_2(X0,X1) | ~c6_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | c5_2(X0,a209) | ~ndr1_0 | ~sP1 is false, set ~sP1 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c9_2(X0,X1) | ~c6_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP1 is false, set ~sP1 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c9_2(X0,X1) | ~c6_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | c4_2(X0,a208) | ndr1_1(X0) | ~ndr1_0 | ~sP1 is false, set ~sP1 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c9_2(X0,X1) | ~c6_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | c9_2(X0,a208) | ndr1_1(X0) | ~ndr1_0 | ~sP1 is false, set ~sP1 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c6_1(X182) | c1_2(X182,X183) | c5_2(X182,X183) | ~c10_2(X182,X183) | ~ndr1_1(X182) | ~ndr1_0 | ndr1_0 | sP4 is false, set sP4 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ndr1_0 | ~sP2 is false, set ~sP2 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c2_0 | ~c5_1(X30) | c10_2(X30,X31) | c3_2(X30,X31) | ~c4_2(X30,X31) | ~ndr1_1(X30) | ndr1_1(X30) | ~ndr1_0 | sP22 is false, set sP22 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ndr1_0 | ~sP5 is false, set ~sP5 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c7_1(X193) | c1_2(X193,X194) | ~c3_2(X193,X194) | ~c4_2(X193,X194) | ~ndr1_1(X193) | c8_2(X193,a204) | ~ndr1_0 | ndr1_0 | sP2 is false, set sP2 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c7_1(X193) | c1_2(X193,X194) | ~c3_2(X193,X194) | ~c4_2(X193,X194) | ~ndr1_1(X193) | c4_2(X193,a204) | ~ndr1_0 | ndr1_0 | sP2 is false, set sP2 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c7_1(X193) | c1_2(X193,X194) | ~c3_2(X193,X194) | ~c4_2(X193,X194) | ~ndr1_1(X193) | ndr1_1(X193) | ~ndr1_0 | c2_1(a205) | sP2 is false, set sP2 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c7_1(X193) | c1_2(X193,X194) | ~c3_2(X193,X194) | ~c4_2(X193,X194) | ~ndr1_1(X193) | ndr1_1(X193) | ~ndr1_0 | c10_1(a205) | sP2 is false, set sP2 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c7_1(X193) | c1_2(X193,X194) | ~c3_2(X193,X194) | ~c4_2(X193,X194) | ~ndr1_1(X193) | ndr1_1(X193) | ~ndr1_0 | ndr1_0 | sP2 is false, set sP2 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c1_1(X185) | c8_2(X185,X186) | ~c5_2(X185,X186) | ~c7_2(X185,X186) | ~ndr1_1(X185) | c4_2(X185,a198) | ~ndr1_0 | ndr1_0 | sP3 is false, set sP3 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c1_1(X185) | c8_2(X185,X186) | ~c5_2(X185,X186) | ~c7_2(X185,X186) | ~ndr1_1(X185) | ~c2_2(X185,a198) | ~ndr1_0 | ndr1_0 | sP3 is false, set sP3 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c1_1(X185) | c8_2(X185,X186) | ~c5_2(X185,X186) | ~c7_2(X185,X186) | ~ndr1_1(X185) | c1_2(X185,a198) | ~ndr1_0 | ndr1_0 | sP3 is false, set sP3 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c1_1(X185) | c8_2(X185,X186) | ~c5_2(X185,X186) | ~c7_2(X185,X186) | ~ndr1_1(X185) | ndr1_1(X185) | ~ndr1_0 | c7_2(a199,X187) | ~c3_2(a199,X187) | ~c4_2(a199,X187) | ~ndr1_1(a199) | sP3 is false, set sP3 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c1_1(X185) | c8_2(X185,X186) | ~c5_2(X185,X186) | ~c7_2(X185,X186) | ~ndr1_1(X185) | ndr1_1(X185) | ~ndr1_0 | ~c9_1(a199) | sP3 is false, set sP3 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c1_1(X185) | c8_2(X185,X186) | ~c5_2(X185,X186) | ~c7_2(X185,X186) | ~ndr1_1(X185) | ndr1_1(X185) | ~ndr1_0 | c4_1(a199) | sP3 is false, set sP3 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ~c1_1(X185) | c8_2(X185,X186) | ~c5_2(X185,X186) | ~c7_2(X185,X186) | ~ndr1_1(X185) | ndr1_1(X185) | ~ndr1_0 | ndr1_0 | sP3 is false, set sP3 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c1_2(X0,X1) | ~c2_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | c8_2(X0,a177) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c1_2(X0,X1) | ~c2_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c1_2(X0,X1) | ~c2_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | c6_2(X0,a176) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c1_2(X0,X1) | ~c2_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c3_2(X0,a177) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c1_2(X0,X1) | ~c2_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | ~c7_2(X0,a176) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c1_2(X0,X1) | ~c2_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c2_2(X0,a177) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ndr1_0 | ~sP4 is false, set ~sP4 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c1_2(X0,X1) | ~c2_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | ~c8_2(X0,a176) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ndr1_0 | ~sP17 is false, set ~sP17 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ndr1_0 | ~sP18 is false, set ~sP18 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ndr1_0 | ~sP20 is false, set ~sP20 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever ndr1_0 | ~sP22 is false, set ~sP22 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c5_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | c7_2(X0,a22) | ndr1_1(X0) | ~ndr1_0 | ~sP25 is false, set ~sP25 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c5_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c7_2(X0,a23) | ~ndr1_0 | ~sP25 is false, set ~sP25 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c5_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c2_2(X0,a23) | ~ndr1_0 | ~sP25 is false, set ~sP25 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c5_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | c8_2(X0,a23) | ~ndr1_0 | ~sP25 is false, set ~sP25 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c5_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP25 is false, set ~sP25 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c5_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ~c5_2(X0,a22) | ndr1_1(X0) | ~ndr1_0 | ~sP25 is false, set ~sP25 to true
% 9.50/1.81 for all groundings,
% 9.50/1.81 whenever c5_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | c9_2(X0,a22) | ndr1_1(X0) | ~ndr1_0 | ~sP25 is false, set ~sP25 to true
% 9.50/1.81 % SZS output end Definitions and Model Updates.
% 9.50/1.81 % (1898194)------------------------------
% 9.50/1.81 % (1898194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.50/1.81 % (1898194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.50/1.81 % (1898194)CaDiCaL version: 2.1.3
% 9.50/1.81 % (1898194)Termination reason: Satisfiable
% 9.50/1.81 % (1898194)Time elapsed: 0.866 s
% 9.50/1.81 % (1898194)Peak memory usage: 137 MB
% 9.50/1.81 % (1898194)Instructions burned: 1326 (million)
% 9.50/1.81 % (1898194)------------------------------
% 9.50/1.81 % (1898194)------------------------------
% 9.50/1.81 % (1898188)Success in time 1.302 s
% 9.50/1.81 % Vampire exiting
%------------------------------------------------------------------------------