%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN546+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 : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:00:55 PM UTC 2026
% Result : CounterSatisfiable 7.41s 1.90s
% Output : Saturation 8.97s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1042,negated_conjecture,
~ c7_0 ).
cnf(u829,negated_conjecture,
~ c4_0 ).
cnf(u853,negated_conjecture,
ndr1_0 ).
cnf(u857,negated_conjecture,
c3_1(a453) ).
cnf(u875,negated_conjecture,
~ c1_0 ).
cnf(u865,negated_conjecture,
~ ndr1_1(a453) ).
cnf(u1185,negated_conjecture,
~ c2_0 ).
cnf(u920,negated_conjecture,
c3_0 ).
cnf(u2522,negated_conjecture,
~ sP0 ).
cnf(u945,negated_conjecture,
( c4_2(X138,a444)
| ~ c8_1(X138)
| ~ c4_1(X138) ) ).
cnf(u1020,negated_conjecture,
c6_0 ).
cnf(u952,negated_conjecture,
( c2_2(X138,a444)
| ~ c8_1(X138)
| ~ c4_1(X138) ) ).
cnf(u956,negated_conjecture,
( c7_2(X138,a444)
| ~ c8_1(X138)
| ~ c4_1(X138) ) ).
cnf(u960,negated_conjecture,
( ~ c4_1(X138)
| ndr1_1(X138)
| ~ c8_1(X138) ) ).
cnf(u967,negated_conjecture,
~ c5_0 ).
cnf(u982,negated_conjecture,
~ c2_1(a442) ).
cnf(u985,negated_conjecture,
~ c8_1(a441) ).
cnf(u2556,negated_conjecture,
~ sP1 ).
cnf(u996,negated_conjecture,
~ ndr1_1(a442) ).
cnf(u1003,negated_conjecture,
c5_1(a441) ).
cnf(u1012,negated_conjecture,
( c1_2(a441,X131)
| c4_2(a441,X131) ) ).
cnf(u1135,negated_conjecture,
( c7_1(X118)
| c5_1(X118) ) ).
cnf(u1331,negated_conjecture,
c8_0 ).
cnf(u1172,negated_conjecture,
c3_1(a428) ).
cnf(u1176,negated_conjecture,
~ ndr1_1(a428) ).
cnf(u2583,negated_conjecture,
~ sP2 ).
cnf(u1238,negated_conjecture,
( ~ c7_1(X108)
| ~ c7_2(X108,X110)
| ~ c5_2(X108,X110)
| ~ c6_2(X108,X110)
| ~ ndr1_1(X108)
| ~ c8_2(X108,X109)
| c5_2(X108,X109)
| c4_2(X108,X109) ) ).
cnf(u1292,negated_conjecture,
( ~ c6_1(X107)
| ~ c4_2(X107,a416) ) ).
cnf(u1296,negated_conjecture,
( ~ c6_1(X107)
| ~ c7_2(X107,a416) ) ).
cnf(u1300,negated_conjecture,
( ~ c6_1(X107)
| ~ c8_2(X107,a416) ) ).
cnf(u1304,negated_conjecture,
( ~ c6_1(X107)
| ndr1_1(X107) ) ).
cnf(u1335,negated_conjecture,
c4_1(a413) ).
cnf(u2609,negated_conjecture,
~ sP3 ).
cnf(u1342,negated_conjecture,
~ c3_1(a413) ).
cnf(u1346,negated_conjecture,
~ c8_1(a413) ).
cnf(u1353,negated_conjecture,
~ ndr1_1(a410) ).
cnf(u1360,negated_conjecture,
~ c6_1(a410) ).
cnf(u1364,negated_conjecture,
c1_1(a410) ).
cnf(u1426,negated_conjecture,
( ~ c6_2(X101,a404)
| c2_1(X101)
| c8_1(X101) ) ).
cnf(u1430,negated_conjecture,
( ~ c3_2(X101,a404)
| c2_1(X101)
| c8_1(X101) ) ).
cnf(u1434,negated_conjecture,
( c1_2(X101,a404)
| c2_1(X101)
| c8_1(X101) ) ).
cnf(u1438,negated_conjecture,
( c8_1(X101)
| ndr1_1(X101)
| c2_1(X101) ) ).
cnf(u1442,negated_conjecture,
~ c7_1(a402) ).
cnf(u1463,negated_conjecture,
ndr1_1(a402) ).
cnf(u1449,negated_conjecture,
( c2_2(a402,X100)
| c8_2(a402,X100)
| ~ c6_2(a402,X100) ) ).
cnf(u1453,negated_conjecture,
c3_2(a402,a403) ).
cnf(u1457,negated_conjecture,
c6_2(a402,a403) ).
cnf(u1461,negated_conjecture,
~ c4_2(a402,a403) ).
cnf(u1484,negated_conjecture,
c5_1(a400) ).
cnf(u2646,negated_conjecture,
~ sP4 ).
cnf(u1491,negated_conjecture,
~ ndr1_1(a400) ).
cnf(u1498,negated_conjecture,
c7_1(a400) ).
cnf(u1530,negated_conjecture,
( ~ c5_2(X90,X93)
| c8_2(X90,X93)
| c4_2(X90,X91)
| c3_2(X90,X93)
| ~ c7_2(X90,X92)
| c3_2(X90,X92)
| ~ ndr1_1(X90)
| ~ c7_2(X90,X91) ) ).
cnf(u1559,negated_conjecture,
( ~ c4_2(X85,a392)
| ~ c4_2(X85,X86)
| ~ c3_1(X85)
| ~ ndr1_1(X85)
| c8_2(X85,X86) ) ).
cnf(u1566,negated_conjecture,
( ~ c4_2(X85,X86)
| c2_2(X85,a392)
| ~ c3_1(X85)
| ~ ndr1_1(X85)
| c8_2(X85,X86) ) ).
cnf(u2681,negated_conjecture,
~ sP5 ).
cnf(u1592,negated_conjecture,
c1_1(a387) ).
cnf(u1596,negated_conjecture,
c6_1(a387) ).
cnf(u1600,negated_conjecture,
~ c8_2(a387,a388) ).
cnf(u1604,negated_conjecture,
c3_2(a387,a388) ).
cnf(u1608,negated_conjecture,
c7_2(a387,a388) ).
cnf(u1612,negated_conjecture,
ndr1_1(a387) ).
cnf(u1617,negated_conjecture,
~ c6_2(a385,a386) ).
cnf(u1621,negated_conjecture,
~ c3_2(a385,a386) ).
cnf(u1625,negated_conjecture,
~ c8_2(a385,a386) ).
cnf(u1629,negated_conjecture,
ndr1_1(a385) ).
cnf(u1633,negated_conjecture,
c2_1(a385) ).
cnf(u1637,negated_conjecture,
c5_1(a385) ).
cnf(u1658,negated_conjecture,
c1_2(a380,a383) ).
cnf(u1662,negated_conjecture,
~ c8_2(a380,a383) ).
cnf(u1666,negated_conjecture,
c6_2(a380,a383) ).
cnf(u1670,negated_conjecture,
ndr1_1(a380) ).
cnf(u1674,negated_conjecture,
c3_2(a380,a382) ).
cnf(u1678,negated_conjecture,
~ c1_2(a380,a382) ).
cnf(u1682,negated_conjecture,
~ c6_2(a380,a382) ).
cnf(u1687,negated_conjecture,
~ c1_2(a380,a381) ).
cnf(u1691,negated_conjecture,
~ c8_2(a380,a381) ).
cnf(u1695,negated_conjecture,
c2_2(a380,a381) ).
cnf(u1701,negated_conjecture,
~ c1_1(a379) ).
cnf(u1708,negated_conjecture,
c3_1(a379) ).
cnf(u1712,negated_conjecture,
~ ndr1_1(a379) ).
cnf(u1789,negated_conjecture,
c5_1(a373) ).
cnf(u1796,negated_conjecture,
c3_1(a373) ).
cnf(u1800,negated_conjecture,
c8_1(a373) ).
cnf(u1816,negated_conjecture,
~ ndr1_1(a371) ).
cnf(u1823,negated_conjecture,
c3_1(a371) ).
cnf(u2719,negated_conjecture,
~ sP6 ).
cnf(u2745,negated_conjecture,
~ sP7 ).
cnf(u1846,negated_conjecture,
~ ndr1_1(a366) ).
cnf(u1879,negated_conjecture,
( c5_2(X65,X66)
| c7_1(X65)
| ~ ndr1_1(X65)
| ~ c7_2(X65,X66)
| c8_2(X65,X66)
| c1_1(X65) ) ).
cnf(u1897,negated_conjecture,
( ~ c8_2(X59,X60)
| ~ c8_2(X59,X61)
| ~ c2_2(X59,X61)
| ~ c7_2(X59,X61)
| c8_1(X59)
| ~ ndr1_1(X59)
| ~ c3_2(X59,X60) ) ).
cnf(u1928,negated_conjecture,
( ~ c6_1(X54)
| ~ c4_2(X54,a361) ) ).
cnf(u2758,negated_conjecture,
~ sP8 ).
cnf(u2795,negated_conjecture,
~ sP9 ).
cnf(u1938,negated_conjecture,
( ~ c6_1(X54)
| ~ c5_2(X54,a361) ) ).
cnf(u1942,negated_conjecture,
( ~ c6_1(X54)
| c7_2(X54,a361) ) ).
cnf(u2821,negated_conjecture,
~ sP10 ).
cnf(u2847,negated_conjecture,
~ sP11 ).
cnf(u1975,negated_conjecture,
~ ndr1_1(a351) ).
cnf(u2016,negated_conjecture,
sP12 ).
cnf(u2023,negated_conjecture,
c2_1(a345) ).
cnf(u2027,negated_conjecture,
c2_2(a345,a346) ).
cnf(u2031,negated_conjecture,
~ c1_2(a345,a346) ).
cnf(u2039,negated_conjecture,
ndr1_1(a345) ).
cnf(u2045,negated_conjecture,
( ~ c6_2(X44,a344)
| c6_1(X44)
| ~ ndr1_1(X44)
| c4_2(X44,X45)
| ~ c6_2(X44,X45) ) ).
cnf(u2048,negated_conjecture,
sP13 ).
cnf(u2063,negated_conjecture,
( ~ c2_1(X40)
| c7_2(X40,X42)
| c8_2(X40,X42)
| ~ c6_2(X40,X42)
| c8_2(X40,X41)
| ~ ndr1_1(X40)
| c3_2(X40,X41) ) ).
cnf(u2070,negated_conjecture,
( ~ c3_2(X37,a340)
| ~ c2_1(X37)
| c7_2(X37,a341) ) ).
cnf(u2074,negated_conjecture,
( ~ c3_2(X37,a340)
| ~ c2_1(X37)
| c1_2(X37,a341) ) ).
cnf(u2078,negated_conjecture,
( ~ c2_1(X37)
| c6_2(X37,a340)
| c7_2(X37,a341) ) ).
cnf(u2082,negated_conjecture,
( ~ c2_1(X37)
| c6_2(X37,a340)
| c1_2(X37,a341) ) ).
cnf(u2086,negated_conjecture,
( ~ c8_2(X37,a340)
| ~ c2_1(X37)
| c7_2(X37,a341) ) ).
cnf(u2090,negated_conjecture,
( ~ c8_2(X37,a340)
| ~ c2_1(X37)
| c1_2(X37,a341) ) ).
cnf(u2094,negated_conjecture,
( ~ c2_1(X37)
| ndr1_1(X37) ) ).
cnf(u2118,negated_conjecture,
c1_1(a338) ).
cnf(u2926,negated_conjecture,
~ sP14 ).
cnf(u2149,negated_conjecture,
( ~ c5_2(X30,X31)
| ~ ndr1_1(X30)
| c8_2(X30,X31)
| c4_1(X30)
| ~ c1_2(X30,X31)
| c6_2(X30,a333) ) ).
cnf(u2153,negated_conjecture,
( ~ c5_2(X30,X31)
| ~ ndr1_1(X30)
| c8_2(X30,X31)
| c4_1(X30)
| ~ c1_2(X30,X31)
| c2_2(X30,a333) ) ).
cnf(u2157,negated_conjecture,
( ~ c7_2(X30,a333)
| ~ ndr1_1(X30)
| c8_2(X30,X31)
| ~ c5_2(X30,X31)
| ~ c1_2(X30,X31)
| c4_1(X30) ) ).
cnf(u2951,negated_conjecture,
~ sP15 ).
cnf(u2209,negated_conjecture,
ndr1_1(a326) ).
cnf(u2192,negated_conjecture,
( c7_2(a326,X29)
| ~ c8_2(a326,X29) ) ).
cnf(u2199,negated_conjecture,
~ c2_2(a326,a327) ).
cnf(u2203,negated_conjecture,
c8_2(a326,a327) ).
cnf(u2207,negated_conjecture,
~ c1_2(a326,a327) ).
cnf(u2213,negated_conjecture,
c8_1(a326) ).
cnf(u2217,negated_conjecture,
c6_1(a325) ).
cnf(u2986,negated_conjecture,
~ sP16 ).
cnf(u3180,negated_conjecture,
ndr1_1(a325) ).
cnf(u2227,negated_conjecture,
( ~ c7_2(a325,X25)
| ~ c1_2(a325,X25)
| ~ c5_2(a325,X25) ) ).
cnf(u2231,negated_conjecture,
c4_1(a325) ).
cnf(u3008,negated_conjecture,
~ sP17 ).
cnf(u2239,negated_conjecture,
( ~ c6_1(X24)
| c1_1(X24)
| c4_1(X24) ) ).
cnf(u2267,negated_conjecture,
( ~ c1_2(X17,a318)
| c3_2(X17,X18)
| ~ ndr1_1(X17)
| ~ c8_2(X17,X18)
| ~ c1_2(X17,X18) ) ).
cnf(u2270,negated_conjecture,
~ ndr1_1(a317) ).
cnf(u2277,negated_conjecture,
( ~ c2_2(X17,a318)
| c3_2(X17,X18)
| ~ ndr1_1(X17)
| ~ c8_2(X17,X18)
| ~ c1_2(X17,X18) ) ).
cnf(u2281,negated_conjecture,
( ~ c8_2(X17,X18)
| c7_2(X17,a318)
| ~ ndr1_1(X17)
| c3_2(X17,X18)
| ~ c1_2(X17,X18) ) ).
cnf(u2300,negated_conjecture,
~ c2_1(a315) ).
cnf(u2304,negated_conjecture,
~ ndr1_1(a315) ).
cnf(u2311,negated_conjecture,
~ c4_1(a315) ).
cnf(u2370,negated_conjecture,
( ~ c3_2(X9,a310)
| c4_1(X9)
| ~ ndr1_1(X9)
| ~ c5_2(X9,X10)
| c7_2(X9,X10)
| ~ c1_2(X9,X10) ) ).
cnf(u2374,negated_conjecture,
( ~ c5_2(X9,X10)
| c6_2(X9,a310)
| ~ ndr1_1(X9)
| c4_1(X9)
| c7_2(X9,X10)
| ~ c1_2(X9,X10) ) ).
cnf(u2378,negated_conjecture,
( ~ c5_2(X9,X10)
| c7_2(X9,a310)
| ~ ndr1_1(X9)
| c4_1(X9)
| c7_2(X9,X10)
| ~ c1_2(X9,X10) ) ).
cnf(u2389,negated_conjecture,
c3_1(a309) ).
cnf(u2393,negated_conjecture,
~ ndr1_1(a309) ).
cnf(u2400,negated_conjecture,
~ c7_1(a309) ).
cnf(u2428,negated_conjecture,
c8_2(a305,a306) ).
cnf(u2432,negated_conjecture,
c2_2(a305,a306) ).
cnf(u2436,negated_conjecture,
~ c3_2(a305,a306) ).
cnf(u2440,negated_conjecture,
ndr1_1(a305) ).
cnf(u2444,negated_conjecture,
~ c5_1(a305) ).
cnf(u2449,negated_conjecture,
( ~ c6_2(a305,X4)
| ~ c8_2(a305,X4)
| c4_2(a305,X4) ) ).
cnf(u2470,negated_conjecture,
c2_1(a302) ).
cnf(u3030,negated_conjecture,
~ sP18 ).
cnf(u2477,negated_conjecture,
~ c5_2(a302,a303) ).
cnf(u2481,negated_conjecture,
~ c1_2(a302,a303) ).
cnf(u2485,negated_conjecture,
c6_2(a302,a303) ).
cnf(u2489,negated_conjecture,
ndr1_1(a302) ).
cnf(u2877,axiom,
c8_1(a347) ).
cnf(u2881,axiom,
c3_2(a347,a348) ).
cnf(u2885,axiom,
~ c4_2(a347,a348) ).
cnf(u2889,axiom,
c2_2(a347,a348) ).
cnf(u2893,axiom,
ndr1_1(a347) ).
cnf(u2897,axiom,
c4_1(a347) ).
cnf(u2903,axiom,
~ c4_2(a342,a343) ).
cnf(u2907,axiom,
c8_2(a342,a343) ).
cnf(u2911,axiom,
c7_2(a342,a343) ).
cnf(u2915,axiom,
ndr1_1(a342) ).
cnf(u2920,axiom,
( ~ c8_2(a342,X1)
| ~ c4_2(a342,X1)
| c5_2(a342,X1) ) ).
cnf(u2924,axiom,
( c4_2(a342,X0)
| c5_2(a342,X0) ) ).
cnf(u3062,negated_conjecture,
~ c1_2(a305,a306) ).
cnf(u3111,negated_conjecture,
~ c1_2(a342,a343) ).
cnf(u3156,negated_conjecture,
~ c3_2(a342,a343) ).
cnf(u3665,negated_conjecture,
~ c8_1(a342) ).
cnf(u3179,negated_conjecture,
~ c8_1(a325) ).
cnf(u3189,negated_conjecture,
~ c6_2(a402,a318) ).
cnf(u3224,negated_conjecture,
( c3_2(a302,X1)
| c8_2(a302,X1) ) ).
cnf(u3240,negated_conjecture,
c8_2(a302,a310) ).
cnf(u3252,negated_conjecture,
c4_1(a345) ).
cnf(u3262,negated_conjecture,
~ c8_2(a326,a333) ).
cnf(u3278,negated_conjecture,
~ c3_1(a342) ).
cnf(u3301,negated_conjecture,
( ~ c6_2(a385,X0)
| c7_2(a385,X0)
| c8_2(a385,X0) ) ).
cnf(u3329,negated_conjecture,
c7_2(a385,a341) ).
cnf(u3336,negated_conjecture,
c7_2(a302,a341) ).
cnf(u3353,negated_conjecture,
c1_2(a385,a341) ).
cnf(u3357,negated_conjecture,
c1_2(a302,a341) ).
cnf(u3366,negated_conjecture,
c7_2(a345,a341) ).
cnf(u3369,negated_conjecture,
c6_2(a345,a340) ).
cnf(u3373,negated_conjecture,
c1_2(a345,a341) ).
cnf(u3377,negated_conjecture,
( c3_2(a345,X1)
| c8_2(a345,X1) ) ).
cnf(u3390,negated_conjecture,
~ c1_2(a302,a310) ).
cnf(u3398,negated_conjecture,
~ c3_2(a302,a310) ).
cnf(u3448,negated_conjecture,
( ~ c8_2(a441,X0)
| ~ c1_2(a441,X0)
| c3_2(a441,X0) ) ).
cnf(u3464,negated_conjecture,
c7_1(a325) ).
cnf(u3470,negated_conjecture,
( ~ c8_2(a325,X1)
| c4_2(a325,X1)
| c5_2(a325,X1) ) ).
cnf(u3489,negated_conjecture,
c6_2(a441,a333) ).
cnf(u3495,negated_conjecture,
( ~ c7_2(a441,X0)
| c4_2(a441,X0)
| c8_2(a441,X0) ) ).
cnf(u3503,negated_conjecture,
~ c7_2(a380,a383) ).
cnf(u3543,negated_conjecture,
~ c7_2(a302,a303) ).
cnf(u3546,negated_conjecture,
c7_1(a302) ).
cnf(u3559,negated_conjecture,
c1_1(a385) ).
cnf(u3597,negated_conjecture,
( ~ c8_2(a302,X1)
| c4_2(a302,X1)
| c5_2(a302,X1) ) ).
cnf(u3605,negated_conjecture,
c5_2(a302,a310) ).
cnf(u3639,negated_conjecture,
( ~ c8_2(a326,X2)
| c3_2(a326,X2) ) ).
cnf(u3655,negated_conjecture,
( ~ c7_2(a342,X1)
| c3_2(a342,X1)
| c8_2(a342,X1) ) ).
cnf(u3698,negated_conjecture,
( ~ c7_2(a347,X1)
| c4_2(a347,X1) ) ).
cnf(u3122,negated_conjecture,
~ c8_2(a387,a416) ).
cnf(u3169,negated_conjecture,
~ c8_2(a325,a416) ).
cnf(u3575,negated_conjecture,
c5_1(a402) ).
cnf(u3682,negated_conjecture,
c3_2(a326,a327) ).
cnf(u3171,negated_conjecture,
~ c4_2(a325,a361) ).
cnf(u3121,negated_conjecture,
~ c7_2(a387,a416) ).
cnf(u3419,negated_conjecture,
( c2_2(X0,a392)
| ~ c4_1(X0)
| ~ c8_1(X0)
| ~ c3_1(X0)
| c8_2(X0,a444) ) ).
cnf(u3125,negated_conjecture,
~ c4_2(a387,a361) ).
cnf(u3173,negated_conjecture,
c7_2(a325,a361) ).
cnf(u3127,negated_conjecture,
c7_2(a387,a361) ).
cnf(u3407,negated_conjecture,
ndr1_1(a413) ).
cnf(u3518,negated_conjecture,
( c2_2(X0,a333)
| c4_1(X0)
| c8_2(X0,a404)
| c7_1(X0)
| ~ c7_2(X0,a404)
| c1_1(X0)
| c2_1(X0)
| c8_1(X0) ) ).
cnf(u3629,negated_conjecture,
( ~ c4_1(X0)
| c3_2(X0,X2)
| c8_2(X0,X2)
| c3_2(X0,a444)
| ~ c7_2(X0,X1)
| c7_1(X0)
| ~ c7_2(X0,X2)
| c1_1(X0)
| ~ c8_1(X0)
| c4_2(X0,X1) ) ).
cnf(u3126,negated_conjecture,
~ c5_2(a387,a361) ).
cnf(u3204,negated_conjecture,
( ~ c7_2(X0,X3)
| c4_2(X0,X2)
| c3_2(X0,X1)
| c8_2(X0,X1)
| c3_2(X0,X3)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X2)
| c7_1(X0)
| ~ c7_2(X0,X1)
| c1_1(X0) ) ).
cnf(u3199,negated_conjecture,
( ~ c1_2(X0,X1)
| c8_2(X0,X1)
| c4_1(X0)
| ~ ndr1_1(X0)
| c2_2(X0,a333)
| c7_1(X0)
| ~ c7_2(X0,X1)
| c1_1(X0) ) ).
cnf(u3119,negated_conjecture,
( ~ c5_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X2)
| c5_2(X0,X2)
| c4_2(X0,X2)
| c5_1(X0) ) ).
cnf(u3120,negated_conjecture,
~ c4_2(a387,a416) ).
cnf(u3441,negated_conjecture,
ndr1_1(a441) ).
cnf(u3168,negated_conjecture,
~ c7_2(a325,a416) ).
cnf(u3479,negated_conjecture,
( ~ c7_2(X0,a404)
| c4_1(X0)
| c6_2(X0,a333)
| c7_1(X0)
| c8_2(X0,a404)
| c1_1(X0)
| c2_1(X0)
| c8_1(X0) ) ).
cnf(u3166,negated_conjecture,
( ~ c1_2(X0,X1)
| c8_2(X0,X1)
| c4_1(X0)
| ~ ndr1_1(X0)
| c6_2(X0,a333)
| c7_1(X0)
| ~ c7_2(X0,X1)
| c1_1(X0) ) ).
cnf(u3167,negated_conjecture,
~ c4_2(a325,a416) ).
cnf(u3319,axiom,
c5_2(a342,a343) ).
cnf(u3172,negated_conjecture,
~ c5_2(a325,a361) ).
cnf(u3550,negated_conjecture,
c5_1(a309) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN546+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.07/0.19 % Computer : n020.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 16:28:04 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running first-order theorem proving
% 0.07/0.23 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
% 7.41/1.90 % (286855)Detected formulas, will run a generic FOF schedule.
% 7.41/1.90 % (286961)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=4078907079:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.41/1.90 % (286964)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2097535729:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.41/1.90 % (286963)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1340015668:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.41/1.90 % (286958)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=3335463217:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.41/1.90 % (286960)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=3235749192:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.41/1.90 % (286962)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2818759269:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.41/1.90 % (286965)dis-21_1_sil=8000:lcm=predicate:random_seed=3440815152:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 7.41/1.90 % (286964)Refutation not found, incomplete strategy
% 7.41/1.90 % (286964)------------------------------
% 7.41/1.90 % (286964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (286964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (286964)CaDiCaL version: 2.1.3
% 7.41/1.90 % (286964)Termination reason: Refutation not found, incomplete strategy
% 7.41/1.90 % (286964)Time elapsed: 0.031 s
% 7.41/1.90 % (286964)Peak memory usage: 90 MB
% 7.41/1.90 % (286964)Instructions burned: 35 (million)
% 7.41/1.90 % (286963)Instruction limit reached!
% 7.41/1.90 % (286963)------------------------------
% 7.41/1.90 % (286963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (286963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (286963)CaDiCaL version: 2.1.3
% 7.41/1.90 % (286963)Termination reason: Instruction limit
% 7.41/1.90 % (286963)Termination phase: Saturation
% 7.41/1.90 % (286963)Time elapsed: 0.075 s
% 7.41/1.90 % (286963)Peak memory usage: 88 MB
% 7.41/1.90 % (286963)Instructions burned: 121 (million)
% 7.41/1.90 % (286962)Instruction limit reached!
% 7.41/1.90 % (286962)------------------------------
% 7.41/1.90 % (286962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (286962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (286962)CaDiCaL version: 2.1.3
% 7.41/1.90 % (286962)Termination reason: Instruction limit
% 7.41/1.90 % (286962)Termination phase: Saturation
% 7.41/1.90 % (286962)Time elapsed: 0.074 s
% 7.41/1.90 % (286962)Peak memory usage: 91 MB
% 7.41/1.90 % (286962)Instructions burned: 110 (million)
% 7.41/1.90 % (286965)Instruction limit reached!
% 7.41/1.90 % (286965)------------------------------
% 7.41/1.90 % (286965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (286965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (286965)CaDiCaL version: 2.1.3
% 7.41/1.90 % (286965)Termination reason: Instruction limit
% 7.41/1.90 % (286965)Termination phase: Saturation
% 7.41/1.90 % (286965)Time elapsed: 0.079 s
% 7.41/1.90 % (286965)Peak memory usage: 92 MB
% 7.41/1.90 % (286965)Instructions burned: 130 (million)
% 7.41/1.90 % (287014)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1179593936:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 7.41/1.90 % (287013)lrs+10_1_sil=8000:sp=occurrence:random_seed=2958929871:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 7.41/1.90 % (287014)Refutation not found, incomplete strategy
% 7.41/1.90 % (287014)------------------------------
% 7.41/1.90 % (287014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (287014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (287014)CaDiCaL version: 2.1.3
% 7.41/1.90 % (287014)Termination reason: Refutation not found, incomplete strategy
% 7.41/1.90 % (287014)Time elapsed: 0.022 s
% 7.41/1.90 % (287014)Peak memory usage: 90 MB
% 7.41/1.90 % (287014)Instructions burned: 35 (million)
% 7.41/1.90 % (287015)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2792954451:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 7.41/1.90 % (286964)------------------------------
% 7.41/1.90 % (286964)------------------------------
% 7.41/1.90 % (287015)Refutation not found, incomplete strategy
% 7.41/1.90 % (287015)------------------------------
% 7.41/1.90 % (287015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (287015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (287015)CaDiCaL version: 2.1.3
% 7.41/1.90 % (287015)Termination reason: Refutation not found, incomplete strategy
% 7.41/1.90 % (287015)Time elapsed: 0.023 s
% 7.41/1.90 % (287015)Peak memory usage: 90 MB
% 7.41/1.90 % (287015)Instructions burned: 36 (million)
% 7.41/1.90 % (287013)Instruction limit reached!
% 7.41/1.90 % (287013)------------------------------
% 7.41/1.90 % (287013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (287013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (287013)CaDiCaL version: 2.1.3
% 7.41/1.90 % (287013)Termination reason: Instruction limit
% 7.41/1.90 % (287013)Termination phase: Saturation
% 7.41/1.90 % (287013)Time elapsed: 0.154 s
% 7.41/1.90 % (287013)Peak memory usage: 93 MB
% 7.41/1.90 % (287013)Instructions burned: 286 (million)
% 7.41/1.90 % (287047)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=84685270:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 7.41/1.90 % (287047)Refutation not found, incomplete strategy
% 7.41/1.90 % (287047)------------------------------
% 7.41/1.90 % (287047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (287047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (287047)CaDiCaL version: 2.1.3
% 7.41/1.90 % (287047)Termination reason: Refutation not found, incomplete strategy
% 7.41/1.90 % (287047)Time elapsed: 0.023 s
% 7.41/1.90 % (287047)Peak memory usage: 90 MB
% 7.41/1.90 % (287047)Instructions burned: 37 (million)
% 7.41/1.90 % (287014)------------------------------
% 7.41/1.90 % (287014)------------------------------
% 7.41/1.90 % (287015)------------------------------
% 7.41/1.90 % (287015)------------------------------
% 7.41/1.90 % (287087)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1456232276:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 7.41/1.90 % (287113)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=460814385:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 7.41/1.90 % (287117)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3827614665:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 7.41/1.90 % (287047)------------------------------
% 7.41/1.90 % (287047)------------------------------
% 7.41/1.90 % (287087)Instruction limit reached!
% 7.41/1.90 % (287087)------------------------------
% 7.41/1.90 % (287087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (287087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (287087)CaDiCaL version: 2.1.3
% 7.41/1.90 % (287087)Termination reason: Instruction limit
% 7.41/1.90 % (287087)Termination phase: Saturation
% 7.41/1.90 % (287087)Time elapsed: 0.163 s
% 7.41/1.90 % (287087)Peak memory usage: 92 MB
% 7.41/1.90 % (287087)Instructions burned: 295 (million)
% 7.41/1.90 % (287117)Instruction limit reached!
% 7.41/1.90 % (287117)------------------------------
% 7.41/1.90 % (287117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (287117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (287117)CaDiCaL version: 2.1.3
% 7.41/1.90 % (287117)Termination reason: Instruction limit
% 7.41/1.90 % (287117)Termination phase: Saturation
% 7.41/1.90 % (287117)Time elapsed: 0.067 s
% 7.41/1.90 % (287117)Peak memory usage: 91 MB
% 7.41/1.90 % (287117)Instructions burned: 114 (million)
% 7.41/1.90 % (286960)First to succeed.
% 7.41/1.90 % (286960)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-286855"
% 7.41/1.90 % (287138)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1497105599:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 7.41/1.90 % (287137)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2589312566:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 7.41/1.90 % (286958)Also succeeded, but the first one will report.
% 7.41/1.90 % (287154)lrs+10_1_sil=8000:sp=occurrence:random_seed=4158406573:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 7.41/1.90 % (287138)Refutation not found, incomplete strategy
% 7.41/1.90 % (287138)------------------------------
% 7.41/1.90 % (287138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (287138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (287138)CaDiCaL version: 2.1.3
% 7.41/1.90 % (287138)Termination reason: Refutation not found, incomplete strategy
% 7.41/1.90 % (287138)Time elapsed: 0.055 s
% 7.41/1.90 % (287138)Peak memory usage: 90 MB
% 7.41/1.90 % (287138)Instructions burned: 106 (million)
% 7.41/1.90 % (287137)Instruction limit reached!
% 7.41/1.90 % (287137)------------------------------
% 7.41/1.90 % (287137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.90 % (287137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.90 % (287137)CaDiCaL version: 2.1.3
% 7.41/1.90 % (287137)Termination reason: Instruction limit
% 7.41/1.90 % (287137)Termination phase: Saturation
% 7.41/1.90 % (287137)Time elapsed: 0.068 s
% 7.41/1.90 % (287137)Peak memory usage: 90 MB
% 7.41/1.90 % (287137)Instructions burned: 129 (million)
% 7.41/1.90 % SZS status CounterSatisfiable for theBenchmark
% 7.41/1.90 % SZS output start Saturation.
% See solution above
% 8.97/1.90 % SZS output start Definitions and Model Updates.
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ndr1_1(X37) | c1_2(X37,a341) | ~c2_1(X37) | ~ndr1_0 | c2_0 is false, set c1_2(X37,a341) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c3_2(X37,a340) | ndr1_1(X37) | ~c2_1(X37) | ~ndr1_0 | c2_0 is false, set ~c3_2(X37,a340) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c7_2(X0,a389) | ndr1_1(X0) | ~c2_1(X0) | ~ndr1_0 | ~sP5 is false, set c7_2(X0,a389) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ndr1_1(X37) | c7_2(X37,a341) | ~c2_1(X37) | ~ndr1_0 | c2_0 is false, set c7_2(X37,a341) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ndr1_1(X0) | ~c7_2(X0,a390) | ~c2_1(X0) | ~ndr1_0 | ~sP5 is false, set ~c7_2(X0,a390) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ndr1_1(X0) | ~c8_2(X0,a390) | ~c2_1(X0) | ~ndr1_0 | ~sP5 is false, set ~c8_2(X0,a390) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c8_2(X37,a340) | ndr1_1(X37) | ~c2_1(X37) | ~ndr1_0 | c2_0 is false, set ~c8_2(X37,a340) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever sP1 | ndr1_0 | c8_2(a442,X132) | ~c7_2(a442,X132) | c6_2(a442,X132) | ~ndr1_1(a442) is false, set c6_2(a442,X132) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c6_2(X37,a340) | ndr1_1(X37) | ~c2_1(X37) | ~ndr1_0 | c2_0 is false, set c6_2(X37,a340) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c2_2(a315,X14) | ~c5_2(a315,X14) | ~c1_2(a315,X14) | ~ndr1_1(a315) | ~c6_0 | ndr1_0 is false, set ~c2_2(a315,X14) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c6_2(X0,a389) | ndr1_1(X0) | ~c2_1(X0) | ~ndr1_0 | ~sP5 is false, set ~c6_2(X0,a389) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ndr1_0 | c1_2(a351,X49) | ~c6_2(a351,X49) | ~c7_2(a351,X49) | ~ndr1_1(a351) | sP11 is false, set ~c6_2(a351,X49) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c2_2(X0,a389) | ndr1_1(X0) | ~c2_1(X0) | ~ndr1_0 | ~sP5 is false, set c2_2(X0,a389) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c3_2(a350,X47) | c4_2(a350,X47) | ~c5_2(a350,X47) | ~ndr1_1(a350) | ndr1_0 | sP11 is false, set c4_2(a350,X47) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c2_2(a350,X48) | ~c6_2(a350,X48) | c4_2(a350,X48) | ~ndr1_1(a350) | ndr1_0 | sP11 is false, set c4_2(a350,X48) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c1_2(a350,X46) | c8_2(a350,X46) | c4_2(a350,X46) | ~ndr1_1(a350) | ndr1_0 | sP11 is false, set c4_2(a350,X46) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ndr1_0 | c2_2(a351,X50) | c4_2(a351,X50) | c5_2(a351,X50) | ~ndr1_1(a351) | sP11 is false, set c4_2(a351,X50) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever sP1 | c4_2(a441,X131) | c1_2(a441,X131) | ~ndr1_1(a441) | ndr1_0 is false, set c4_2(a441,X131) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever sP1 | c5_1(a441) | ndr1_0 is false, set c5_1(a441) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ndr1_1(X0) | c3_2(X0,a390) | ~c2_1(X0) | ~ndr1_0 | ~sP5 is false, set c3_2(X0,a390) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ndr1_0 | ~c5_2(X141,X142) | c1_2(X141,X142) | ~ndr1_1(X141) | c5_2(X141,X143) | c7_2(X141,X143) | ~c2_2(X141,X143) | ~ndr1_1(X141) | c3_2(X141,X144) | ~c5_2(X141,X144) | c8_2(X141,X144) | ~ndr1_1(X141) | ~ndr1_0 | c3_0 is false, set c3_2(X141,X144) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c4_1(a315) | ~c6_0 | ndr1_0 is false, set ~c4_1(a315) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c2_0 | ndr1_1(X111) | ~c1_2(X111,X112) | c4_2(X111,X112) | c5_2(X111,X112) | ~ndr1_1(X111) | c1_2(X111,X113) | c3_2(X111,X113) | c5_2(X111,X113) | ~ndr1_1(X111) | ~ndr1_0 | c6_0 is false, set c6_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever sP1 | ndr1_0 | ~c8_1(a442) is false, set ~c8_1(a442) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever sP1 | ~c8_1(a441) | ndr1_0 is false, set ~c8_1(a441) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c2_1(a315) | ~c6_0 | ndr1_0 is false, set ~c2_1(a315) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c2_1(X79) | ndr1_1(X79) | c3_1(X79) | ~ndr1_0 | ndr1_0 | c5_0 is false, set ~c2_1(X79) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c2_1(X79) | c6_2(X79,a378) | c3_1(X79) | ~ndr1_0 | ndr1_0 | c5_0 is false, set ~c2_1(X79) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c2_1(X79) | ~c2_2(X79,a378) | c3_1(X79) | ~ndr1_0 | ndr1_0 | c5_0 is false, set ~c2_1(X79) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c2_1(X79) | ~c5_2(X79,a378) | c3_1(X79) | ~ndr1_0 | ndr1_0 | c5_0 is false, set ~c2_1(X79) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever sP1 | ndr1_0 | ~c2_1(a442) is false, set ~c2_1(a442) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c4_0 | ~c6_0 | c8_2(X19,X20) | c6_2(X19,X20) | ~ndr1_1(X19) | ndr1_1(X19) | c1_2(X19,X21) | ~c2_2(X19,X21) | c5_2(X19,X21) | ~ndr1_1(X19) | ~ndr1_0 is false, set ~c4_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c2_0 | ~c1_0 | c7_2(X115,X116) | c5_2(X115,X116) | ~ndr1_1(X115) | ndr1_1(X115) | ~c2_1(X115) | ~ndr1_0 is false, set ~c1_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c7_1(X108) | c4_2(X108,X109) | c5_2(X108,X109) | ~c8_2(X108,X109) | ~ndr1_1(X108) | ~c6_2(X108,X110) | ~c5_2(X108,X110) | ~c7_2(X108,X110) | ~ndr1_1(X108) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X108) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c8_0 | ndr1_0 | c3_2(X17,X18) | ~c1_2(X17,X18) | ~c8_2(X17,X18) | ~ndr1_1(X17) | ~c2_2(X17,a318) | ~ndr1_0 is false, set ~c8_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c8_0 | c3_2(a317,X15) | c6_2(a317,X15) | c7_2(a317,X15) | ~ndr1_1(a317) | c3_2(X17,X18) | ~c1_2(X17,X18) | ~c8_2(X17,X18) | ~ndr1_1(X17) | ndr1_1(X17) | ~ndr1_0 is false, set ~c8_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c8_0 | ndr1_0 | c3_2(X17,X18) | ~c1_2(X17,X18) | ~c8_2(X17,X18) | ~ndr1_1(X17) | ~c1_2(X17,a318) | ~ndr1_0 is false, set ~c8_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c8_0 | ndr1_0 | c3_2(X17,X18) | ~c1_2(X17,X18) | ~c8_2(X17,X18) | ~ndr1_1(X17) | c7_2(X17,a318) | ~ndr1_0 is false, set ~c8_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c8_0 | ndr1_0 | c3_2(X17,X18) | ~c1_2(X17,X18) | ~c8_2(X17,X18) | ~ndr1_1(X17) | ndr1_1(X17) | ~ndr1_0 is false, set ~c8_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c8_0 | c4_2(a317,X16) | c8_2(a317,X16) | c5_2(a317,X16) | ~ndr1_1(a317) | c3_2(X17,X18) | ~c1_2(X17,X18) | ~c8_2(X17,X18) | ~ndr1_1(X17) | ndr1_1(X17) | ~ndr1_0 is false, set ~c8_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c3_1(X32) | ~c2_1(X32) | ndr1_1(X32) | ~ndr1_0 | ndr1_0 | c4_0 is false, set c4_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c3_1(X32) | ~c2_1(X32) | c5_2(X32,a337) | ~ndr1_0 | ndr1_0 | c4_0 is false, set c4_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c3_1(X32) | ~c2_1(X32) | c8_2(X32,a337) | ~ndr1_0 | ndr1_0 | c4_0 is false, set c4_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c6_0 | ndr1_1(X129) | c1_2(X129,X130) | ~c8_2(X129,X130) | ~c5_2(X129,X130) | ~ndr1_1(X129) | c6_1(X129) | ~ndr1_0 | c4_0 is false, set c4_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c3_1(X32) | ~c2_1(X32) | ~c7_2(X32,a337) | ~ndr1_0 | ndr1_0 | c4_0 is false, set c4_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c2_0 | ~c1_1(X73) | c8_2(X73,X74) | c3_2(X73,X74) | ~c1_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | ~ndr1_0 | c5_1(a373) is false, set ~c1_1(X73) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c2_0 | ~c1_1(X73) | c8_2(X73,X74) | c3_2(X73,X74) | ~c1_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | ~ndr1_0 | c3_1(a373) is false, set ~c1_1(X73) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c2_0 | ~c1_1(X73) | c8_2(X73,X74) | c3_2(X73,X74) | ~c1_2(X73,X74) | ~ndr1_1(X73) | c4_2(X73,a372) | ~ndr1_0 | ndr1_0 is false, set ~c1_1(X73) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c2_0 | ~c1_1(X73) | c8_2(X73,X74) | c3_2(X73,X74) | ~c1_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | ~ndr1_0 | ndr1_0 is false, set ~c1_1(X73) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c2_0 | ~c1_1(X73) | c8_2(X73,X74) | c3_2(X73,X74) | ~c1_2(X73,X74) | ~ndr1_1(X73) | ~c8_2(X73,a372) | ~ndr1_0 | ndr1_0 is false, set ~c1_1(X73) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c2_0 | ~c1_1(X73) | c8_2(X73,X74) | c3_2(X73,X74) | ~c1_2(X73,X74) | ~ndr1_1(X73) | ~c5_2(X73,a372) | ~ndr1_0 | ndr1_0 is false, set ~c1_1(X73) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c2_1(X87) | ~c4_2(X87,X88) | ~c5_2(X87,X88) | ~c7_2(X87,X88) | ~ndr1_1(X87) | ~c1_1(X87) | ~ndr1_0 | c6_0 | ndr1_0 is false, set ~c1_1(X87) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c3_0 | ~c7_0 | ndr1_1(X96) | ~c1_1(X96) | ~c2_2(X96,X97) | ~c6_2(X96,X97) | ~ndr1_1(X96) | ~ndr1_0 is false, set ~c3_0 to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever ~c8_2(X1,X2) | c3_2(X1,X2) | c2_2(X1,X2) | ~ndr1_1(X1) | ~c5_1(X1) | c5_2(X1,X3) | ~c8_2(X1,X3) | ~ndr1_1(X1) | ~ndr1_0 | c6_0 | ndr1_0 is false, set ~c5_1(X1) to true
% 8.97/1.90 for all groundings,
% 8.97/1.90 whenever c4_2(X122,X123) | ~c1_2(X122,X123) | ~c7_2(X122,X123) | ~ndr1_1(X122) | ndr1_1(X122) | c1_2(X122,a433) | ~ndr1_0 | ~c3_1(X124) | ~c5_1(X124) | c2_1(X124) | ~ndr1_0 | c6_0 is false, set ~c5_1(X124) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c4_2(X122,X123) | ~c1_2(X122,X123) | ~c7_2(X122,X123) | ~ndr1_1(X122) | ndr1_1(X122) | c2_2(X122,a433) | ~ndr1_0 | ~c3_1(X124) | ~c5_1(X124) | c2_1(X124) | ~ndr1_0 | c6_0 is false, set ~c5_1(X124) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c4_2(X122,X123) | ~c1_2(X122,X123) | ~c7_2(X122,X123) | ~ndr1_1(X122) | ndr1_1(X122) | c5_2(X122,a433) | ~ndr1_0 | ~c3_1(X124) | ~c5_1(X124) | c2_1(X124) | ~ndr1_0 | c6_0 is false, set ~c5_1(X124) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c4_2(X122,X123) | ~c1_2(X122,X123) | ~c7_2(X122,X123) | ~ndr1_1(X122) | c6_2(X122,a432) | ndr1_1(X122) | ~ndr1_0 | ~c3_1(X124) | ~c5_1(X124) | c2_1(X124) | ~ndr1_0 | c6_0 is false, set ~c5_1(X124) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c4_2(X122,X123) | ~c1_2(X122,X123) | ~c7_2(X122,X123) | ~ndr1_1(X122) | ndr1_1(X122) | ndr1_1(X122) | ~ndr1_0 | ~c3_1(X124) | ~c5_1(X124) | c2_1(X124) | ~ndr1_0 | c6_0 is false, set ~c5_1(X124) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c1_2(X26,X27) | ~c6_2(X26,X27) | ~ndr1_1(X26) | c5_2(X26,X28) | c7_2(X26,X28) | ~c8_2(X26,X28) | ~ndr1_1(X26) | ~c5_1(X26) | ~ndr1_0 | ndr1_0 is false, set ~c5_1(X26) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c4_2(X122,X123) | ~c1_2(X122,X123) | ~c7_2(X122,X123) | ~ndr1_1(X122) | ~c7_2(X122,a432) | ndr1_1(X122) | ~ndr1_0 | ~c3_1(X124) | ~c5_1(X124) | c2_1(X124) | ~ndr1_0 | c6_0 is false, set ~c5_1(X124) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c4_2(X122,X123) | ~c1_2(X122,X123) | ~c7_2(X122,X123) | ~ndr1_1(X122) | c1_2(X122,a432) | ndr1_1(X122) | ~ndr1_0 | ~c3_1(X124) | ~c5_1(X124) | c2_1(X124) | ~ndr1_0 | c6_0 is false, set ~c5_1(X124) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c7_1(X55) | c4_2(X55,X56) | ~c7_2(X55,X56) | c2_2(X55,X56) | ~ndr1_1(X55) | c7_2(X55,X57) | ~c3_2(X55,X57) | c5_2(X55,X57) | ~ndr1_1(X55) | ~ndr1_0 | ndr1_0 | ~c3_2(X59,X60) | ~c8_2(X59,X60) | ~ndr1_1(X59) | c8_1(X59) | ~c7_2(X59,X61) | ~c2_2(X59,X61) | ~c8_2(X59,X61) | ~ndr1_1(X59) | ~ndr1_0 is false, set c8_1(X59) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c2_0 | ~c1_1(X73) | c8_2(X73,X74) | c3_2(X73,X74) | ~c1_2(X73,X74) | ~ndr1_1(X73) | ndr1_1(X73) | ~ndr1_0 | c8_1(a373) is false, set c8_1(a373) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c8_0 | c8_1(a317) | c3_2(X17,X18) | ~c1_2(X17,X18) | ~c8_2(X17,X18) | ~ndr1_1(X17) | ndr1_1(X17) | ~ndr1_0 is false, set c8_1(a317) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c7_2(X133,X134) | ~c3_2(X133,X134) | ~c2_2(X133,X134) | ~ndr1_1(X133) | c1_2(X133,X135) | c8_2(X133,X135) | ~c2_2(X133,X135) | ~ndr1_1(X133) | c8_1(X133) | ~ndr1_0 | ~c5_0 | ~c4_1(X136) | ndr1_1(X136) | ~c7_2(X136,X137) | ~c2_2(X136,X137) | ~c3_2(X136,X137) | ~ndr1_1(X136) | ~ndr1_0 is false, set c8_1(X133) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c5_1(X84) | ~c6_1(X84) | ndr1_1(X84) | ~ndr1_0 | c1_0 | ~c4_2(X85,X86) | c8_2(X85,X86) | ~ndr1_1(X85) | ~c3_1(X85) | ndr1_1(X85) | ~ndr1_0 is false, set ~c6_1(X84) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c5_1(X84) | ~c6_1(X84) | c7_2(X84,a391) | ~ndr1_0 | c1_0 | ~c4_2(X85,X86) | c8_2(X85,X86) | ~ndr1_1(X85) | ~c3_1(X85) | ndr1_1(X85) | ~ndr1_0 is false, set ~c6_1(X84) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c5_1(X84) | ~c6_1(X84) | c8_2(X84,a391) | ~ndr1_0 | c1_0 | ~c4_2(X85,X86) | c8_2(X85,X86) | ~ndr1_1(X85) | ~c3_1(X85) | ndr1_1(X85) | ~ndr1_0 is false, set ~c6_1(X84) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c4_0 | ndr1_0 | ~c6_1(X106) | c8_1(X106) | c5_1(X106) | ~ndr1_0 is false, set ~c6_1(X106) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c5_1(X84) | ~c6_1(X84) | ~c4_2(X84,a391) | ~ndr1_0 | c1_0 | ~c4_2(X85,X86) | c8_2(X85,X86) | ~ndr1_1(X85) | ~c3_1(X85) | ndr1_1(X85) | ~ndr1_0 is false, set ~c6_1(X84) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c3_1(X0) | ndr1_1(X0) | ~c1_2(X0,X1) | ~c6_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | sP5 is false, set sP5 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever sP3 | ndr1_0 | ~c3_0 is false, set sP3 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | ~c6_0 | c4_1(a316) is false, set c4_1(a316) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c4_1(X9) | ~c1_2(X9,X10) | c7_2(X9,X10) | ~c5_2(X9,X10) | ~ndr1_1(X9) | ndr1_1(X9) | ~ndr1_0 | ~c6_0 | c7_0 is false, set c4_1(X9) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c4_1(X62) | ~c1_1(X62) | ~c2_1(X62) | ~ndr1_0 | c5_2(X63,X64) | ~c8_2(X63,X64) | ~c6_2(X63,X64) | ~ndr1_1(X63) | ndr1_1(X63) | c8_1(X63) | ~ndr1_0 | c1_1(X65) | c5_2(X65,X66) | c8_2(X65,X66) | ~c7_2(X65,X66) | ~ndr1_1(X65) | c7_1(X65) | ~ndr1_0 is false, set c4_1(X62) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c2_0 | c8_1(X102) | c6_2(X102,X103) | c2_2(X102,X103) | c3_2(X102,X103) | ~ndr1_1(X102) | c4_1(X102) | ~ndr1_0 | ndr1_0 is false, set c4_1(X102) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c4_1(X119) | c7_1(X119) | ~c5_2(X119,X120) | c3_2(X119,X120) | c4_2(X119,X120) | ~ndr1_1(X119) | ~ndr1_0 | c6_0 | ndr1_0 is false, set c4_1(X119) to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c3_1(X43) | c1_1(X43) | ~c2_1(X43) | ~ndr1_0 | sP13 | ndr1_1(X44) | ~c6_2(X44,X45) | c4_2(X44,X45) | ~ndr1_1(X44) | c6_1(X44) | ~ndr1_0 is false, set sP13 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c3_0 | c4_1(X30) | ndr1_1(X30) | ~c1_2(X30,X31) | ~c5_2(X30,X31) | c8_2(X30,X31) | ~ndr1_1(X30) | ~ndr1_0 | sP14 is false, set sP14 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_1(X22) | ~c6_1(X22) | c4_2(X22,X23) | ~c7_2(X22,X23) | ~ndr1_1(X22) | ~ndr1_0 | ~c6_1(X24) | c4_1(X24) | c1_1(X24) | ~ndr1_0 | sP17 is false, set sP17 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c7_2(X0,X1) | c3_2(X0,X1) | c6_2(X0,X1) | ~ndr1_1(X0) | c3_2(X0,a411) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_1(X0) | c7_2(X0,X1) | c4_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ~c4_2(X0,a360) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c6_2(X0,a359) | c7_2(X0,X1) | c4_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_1(X0) | c7_2(X0,X1) | c4_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ~c8_2(X0,a360) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_1(X0) | c7_2(X0,X1) | c4_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ~c5_2(X0,a360) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_1(X0) | c7_2(X0,X1) | c4_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | ~sP0 is false, set ~sP0 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c8_2(X0,a359) | c7_2(X0,X1) | c4_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c4_2(X0,a359) | c7_2(X0,X1) | c4_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~sP8 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | ~sP9 is false, set ~sP9 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | ~sP14 is false, set ~sP14 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | ~sP13 is false, set ~sP13 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | ~sP17 is false, set ~sP17 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c4_2(a365,X67) | c5_2(a365,X67) | ~ndr1_1(a365) | ndr1_0 | sP7 is false, set sP7 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ~c7_1(a365) | ndr1_0 | sP7 is false, set sP7 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c1_1(a365) | ndr1_0 | sP7 is false, set sP7 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | c8_2(a366,X70) | c4_2(a366,X70) | ~ndr1_1(a366) | sP7 is false, set sP7 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | c7_2(a366,X69) | c1_2(a366,X69) | ~ndr1_1(a366) | sP7 is false, set sP7 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | c1_2(a366,X68) | c2_2(a366,X68) | ~c4_2(a366,X68) | ~ndr1_1(a366) | sP7 is false, set sP7 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | ndr1_0 | sP7 is false, set sP7 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c7_2(X0,X1) | c3_2(X0,X1) | c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | c2_2(X0,a412) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c7_2(X0,X1) | c3_2(X0,X1) | c6_2(X0,X1) | ~ndr1_1(X0) | ~c8_2(X0,a411) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c7_2(X0,X1) | c3_2(X0,X1) | c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | c8_2(X0,a412) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c7_2(X0,X1) | c3_2(X0,X1) | c6_2(X0,X1) | ~ndr1_1(X0) | ~c2_2(X0,a411) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c7_2(X0,X1) | c3_2(X0,X1) | c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | c6_2(X0,a412) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever c7_2(X0,X1) | c3_2(X0,X1) | c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set ~sP3 to true
% 9.10/2.08 for all groundings,
% 9.10/2.08 whenever ndr1_0 | ~sP6 is false, set ~sP6 to true
% 9.10/2.08 % SZS output end Definitions and Model Updates.
% 9.10/2.08 % (286960)------------------------------
% 9.10/2.08 % (286960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.10/2.08 % (286960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.08 % (286960)CaDiCaL version: 2.1.3
% 9.10/2.08 % (286960)Termination reason: Satisfiable
% 9.10/2.08 % (286960)Time elapsed: 0.777 s
% 9.10/2.08 % (286960)Peak memory usage: 134 MB
% 9.10/2.08 % (286960)Instructions burned: 1160 (million)
% 9.10/2.08 % (286960)------------------------------
% 9.10/2.08 % (286960)------------------------------
% 9.10/2.08 % (286855)Success in time 1.215 s
% 9.10/2.08 % Vampire exiting
%------------------------------------------------------------------------------