%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYN159-1 : TPTP v9.0.0. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 09:27:01 PM UTC 2025
% Result : Unsatisfiable 4.79s 1.00s
% Output : CNFRefutation 4.79s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named prove_this)
% Comments :
%------------------------------------------------------------------------------
cnf(361,plain,
~ n5(a,e),
inference(cnf,[status(esa)],[prove_this]) ).
cnf(l0,plain,
~ n5(a,e),
inference(instantiation,[status(thm)],[361]) ).
cnf(337,plain,
( ~ n4(X0,X1)
| ~ p4(X2,X2,X3)
| ~ q4(X4,X1)
| ~ n5(X2,X3)
| n5(X0,X3) ),
inference(cnf,[status(esa)],[rule_307]) ).
cnf(l1,plain,
( ~ n4(a,e)
| ~ p4(e,e,e)
| ~ q4(e,e)
| ~ n5(e,e)
| n5(a,e) ),
inference(instantiation,[status(thm)],[337]) ).
cnf(311,plain,
( ~ p3(X0,X1,X1)
| ~ n4(X0,X0)
| n4(X0,X1) ),
inference(cnf,[status(esa)],[rule_281]) ).
cnf(l2,plain,
( ~ p3(a,e,e)
| ~ n4(a,a)
| n4(a,e) ),
inference(instantiation,[status(thm)],[311]) ).
cnf(345,plain,
( ~ s1(X0)
| ~ k4(X0)
| n5(X0,X0) ),
inference(cnf,[status(esa)],[rule_315]) ).
cnf(l4,plain,
( ~ s1(e)
| ~ k4(e)
| n5(e,e) ),
inference(instantiation,[status(thm)],[345]) ).
cnf(283,plain,
( ~ p2(X0,X1,X2)
| ~ m3(X1,X3,X2)
| p3(X0,X1,X1) ),
inference(cnf,[status(esa)],[rule_251]) ).
cnf(l106,plain,
( ~ p2(a,e,e)
| ~ m3(e,e,e)
| p3(a,e,e) ),
inference(instantiation,[status(thm)],[283]) ).
cnf(189,plain,
( ~ k1(X0)
| ~ p2(e,X1,X2)
| p2(X1,X2,X2) ),
inference(cnf,[status(esa)],[rule_155]) ).
cnf(l174,plain,
( ~ k1(b)
| ~ p2(e,a,e)
| p2(a,e,e) ),
inference(instantiation,[status(thm)],[189]) ).
cnf(326,plain,
( ~ r1(X0)
| ~ l4(X1)
| ~ q4(X1,X2)
| q4(X0,X0) ),
inference(cnf,[status(esa)],[rule_296]) ).
cnf(l7,plain,
( ~ r1(e)
| ~ l4(b)
| ~ q4(b,b)
| q4(e,e) ),
inference(instantiation,[status(thm)],[326]) ).
cnf(308,plain,
( ~ p3(X0,X1,X2)
| l4(X2) ),
inference(cnf,[status(esa)],[rule_277]) ).
cnf(l34,plain,
( ~ p3(b,b,b)
| l4(b) ),
inference(instantiation,[status(thm)],[308]) ).
cnf(159,plain,
( ~ s0(d)
| ~ q0(X0,X1)
| ~ q1(d,X1,d)
| r1(X0) ),
inference(cnf,[status(esa)],[rule_124]) ).
cnf(l12,plain,
( ~ s0(d)
| ~ q0(e,d)
| ~ q1(d,d,d)
| r1(e) ),
inference(instantiation,[status(thm)],[159]) ).
cnf(314,plain,
( ~ m3(X0,X0,X0)
| ~ k4(X1)
| n4(X0,X0) ),
inference(cnf,[status(esa)],[rule_284]) ).
cnf(l13,plain,
( ~ m3(a,a,a)
| ~ k4(c)
| n4(a,a) ),
inference(instantiation,[status(thm)],[314]) ).
cnf(306,plain,
( ~ n0(c,d)
| ~ n3(e)
| ~ q3(e,b)
| k4(c) ),
inference(cnf,[status(esa)],[rule_274]) ).
cnf(l60,plain,
( ~ n0(c,d)
| ~ n3(e)
| ~ q3(e,b)
| k4(c) ),
inference(instantiation,[status(thm)],[306]) ).
cnf(38,plain,
( ~ n0(X0,X1)
| k1(X1) ),
inference(cnf,[status(esa)],[rule_001]) ).
cnf(l257,plain,
( ~ n0(d,b)
| k1(b) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(6,plain,
n0(d,b),
inference(cnf,[status(esa)],[axiom_7]) ).
cnf(l419,plain,
n0(d,b),
inference(instantiation,[status(thm)],[6]) ).
cnf(287,plain,
( ~ n0(X0,X1)
| ~ q2(X0,X1,X2)
| q3(X1,X2) ),
inference(cnf,[status(esa)],[rule_255]) ).
cnf(l420,plain,
( ~ n0(e,e)
| ~ q2(e,e,b)
| q3(e,b) ),
inference(instantiation,[status(thm)],[287]) ).
cnf(257,plain,
( ~ m0(X0,X1,X1)
| ~ m0(X2,X2,X3)
| ~ l2(X1,X0)
| ~ s2(X2)
| m3(X0,X3,X0) ),
inference(cnf,[status(esa)],[rule_225]) ).
cnf(l55,plain,
( ~ m0(a,a,a)
| ~ m0(a,a,a)
| ~ l2(a,a)
| ~ s2(a)
| m3(a,a,a) ),
inference(instantiation,[status(thm)],[257]) ).
cnf(325,plain,
( ~ q2(X0,X1,X2)
| ~ k3(X3,X3,X2)
| ~ m3(X0,X4,X0)
| q4(X2,X1) ),
inference(cnf,[status(esa)],[rule_295]) ).
cnf(l10,plain,
( ~ q2(b,b,b)
| ~ k3(b,b,b)
| ~ m3(b,b,b)
| q4(b,b) ),
inference(instantiation,[status(thm)],[325]) ).
cnf(0,plain,
s0(d),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l16,plain,
s0(d),
inference(instantiation,[status(thm)],[0]) ).
cnf(128,plain,
( ~ q0(X0,X1)
| q1(X1,X1,X1) ),
inference(cnf,[status(esa)],[rule_093]) ).
cnf(l126,plain,
( ~ q0(d,d)
| q1(d,d,d) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(1,plain,
q0(e,d),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l98,plain,
q0(e,d),
inference(instantiation,[status(thm)],[1]) ).
cnf(168,plain,
( ~ p0(X0,X1)
| ~ m0(X0,X1,X2)
| ~ m1(X2,X0,X0)
| l2(X1,X1) ),
inference(cnf,[status(esa)],[rule_134]) ).
cnf(l452,plain,
( ~ p0(b,a)
| ~ m0(b,a,a)
| ~ m1(a,b,b)
| l2(a,a) ),
inference(instantiation,[status(thm)],[168]) ).
cnf(212,plain,
( ~ q0(X0,X1)
| ~ n1(X0,X1,X2)
| q2(X1,X1,X1) ),
inference(cnf,[status(esa)],[rule_178]) ).
cnf(l15,plain,
( ~ q0(b,b)
| ~ n1(b,b,b)
| q2(b,b,b) ),
inference(instantiation,[status(thm)],[212]) ).
cnf(11,plain,
m0(a,X0,a),
inference(cnf,[status(esa)],[axiom_12]) ).
cnf(l422,plain,
m0(a,a,a),
inference(instantiation,[status(thm)],[11]) ).
cnf(264,plain,
( ~ l2(X0,X0)
| ~ n2(X0)
| m3(X0,X0,X0) ),
inference(cnf,[status(esa)],[rule_232]) ).
cnf(l445,plain,
( ~ l2(b,b)
| ~ n2(b)
| m3(b,b,b) ),
inference(instantiation,[status(thm)],[264]) ).
cnf(272,plain,
( ~ p2(X0,X1,X2)
| n3(X2) ),
inference(cnf,[status(esa)],[rule_240]) ).
cnf(l428,plain,
( ~ p2(e,e,e)
| n3(e) ),
inference(instantiation,[status(thm)],[272]) ).
cnf(29,plain,
n0(e,e),
inference(cnf,[status(esa)],[axiom_30]) ).
cnf(l429,plain,
n0(e,e),
inference(instantiation,[status(thm)],[29]) ).
cnf(88,plain,
( ~ s0(X0)
| ~ p0(X1,X2)
| ~ m0(X2,X2,X2)
| ~ k1(X0)
| n1(X0,X0,X0) ),
inference(cnf,[status(esa)],[rule_052]) ).
cnf(l156,plain,
( ~ s0(b)
| ~ p0(b,d)
| ~ m0(d,d,d)
| ~ k1(b)
| n1(b,b,b) ),
inference(instantiation,[status(thm)],[88]) ).
cnf(13,plain,
p0(b,X0),
inference(cnf,[status(esa)],[axiom_14]) ).
cnf(l502,plain,
p0(b,a),
inference(instantiation,[status(thm)],[13]) ).
cnf(220,plain,
( ~ l1(X0,X1)
| q2(X1,X1,X0) ),
inference(cnf,[status(esa)],[rule_186]) ).
cnf(l421,plain,
( ~ l1(b,e)
| q2(e,e,b) ),
inference(instantiation,[status(thm)],[220]) ).
cnf(5,plain,
q0(b,b),
inference(cnf,[status(esa)],[axiom_6]) ).
cnf(l78,plain,
q0(b,b),
inference(instantiation,[status(thm)],[5]) ).
cnf(18,plain,
m0(X0,d,X1),
inference(cnf,[status(esa)],[axiom_19]) ).
cnf(l158,plain,
m0(d,d,d),
inference(instantiation,[status(thm)],[18]) ).
cnf(24,plain,
q0(d,d),
inference(cnf,[status(esa)],[axiom_25]) ).
cnf(l163,plain,
q0(d,d),
inference(instantiation,[status(thm)],[24]) ).
cnf(210,plain,
( ~ m1(X0,X1,X0)
| p2(X1,X0,X1) ),
inference(cnf,[status(esa)],[rule_176]) ).
cnf(l438,plain,
( ~ m1(e,e,e)
| p2(e,e,e) ),
inference(instantiation,[status(thm)],[210]) ).
cnf(223,plain,
( ~ s1(b)
| ~ q2(b,X0,b)
| s2(X0) ),
inference(cnf,[status(esa)],[rule_189]) ).
cnf(l465,plain,
( ~ s1(b)
| ~ q2(b,a,b)
| s2(a) ),
inference(instantiation,[status(thm)],[223]) ).
cnf(l450,plain,
m0(a,a,a),
inference(instantiation,[status(thm)],[11]) ).
cnf(37,plain,
m0(b,a,a),
inference(cnf,[status(esa)],[axiom_38]) ).
cnf(l457,plain,
m0(b,a,a),
inference(instantiation,[status(thm)],[37]) ).
cnf(4,plain,
s0(b),
inference(cnf,[status(esa)],[axiom_5]) ).
cnf(l467,plain,
s0(b),
inference(instantiation,[status(thm)],[4]) ).
cnf(l609,plain,
( ~ n0(e,b)
| k1(b) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(171,plain,
( ~ p1(X0,X1,X2)
| n2(X2) ),
inference(cnf,[status(esa)],[rule_137]) ).
cnf(l472,plain,
( ~ p1(e,e,b)
| n2(b) ),
inference(instantiation,[status(thm)],[171]) ).
cnf(239,plain,
( ~ p2(X0,X1,X1)
| k3(X1,X0,X1) ),
inference(cnf,[status(esa)],[rule_206]) ).
cnf(l430,plain,
( ~ p2(b,b,b)
| k3(b,b,b) ),
inference(instantiation,[status(thm)],[239]) ).
cnf(278,plain,
( ~ l2(X0,X0)
| p3(X0,X0,X0) ),
inference(cnf,[status(esa)],[rule_246]) ).
cnf(l50,plain,
( ~ l2(b,b)
| p3(b,b,b) ),
inference(instantiation,[status(thm)],[278]) ).
cnf(33,plain,
n0(c,d),
inference(cnf,[status(esa)],[axiom_34]) ).
cnf(l119,plain,
n0(c,d),
inference(instantiation,[status(thm)],[33]) ).
cnf(307,plain,
( ~ q1(a,a,X0)
| ~ r3(X1,e,X0)
| ~ q3(X1,X1)
| k4(e) ),
inference(cnf,[status(esa)],[rule_276]) ).
cnf(l432,plain,
( ~ q1(a,a,a)
| ~ r3(a,e,a)
| ~ q3(a,a)
| k4(e) ),
inference(instantiation,[status(thm)],[307]) ).
cnf(321,plain,
( ~ p3(X0,X0,X1)
| p4(X1,X1,X1) ),
inference(cnf,[status(esa)],[rule_291]) ).
cnf(l3,plain,
( ~ p3(e,e,e)
| p4(e,e,e) ),
inference(instantiation,[status(thm)],[321]) ).
cnf(304,plain,
( ~ k2(X0,X1)
| ~ r2(X1)
| ~ r3(X1,X2,X2)
| r3(X2,X0,X1) ),
inference(cnf,[status(esa)],[rule_272]) ).
cnf(l436,plain,
( ~ k2(e,a)
| ~ r2(a)
| ~ r3(a,a,a)
| r3(a,e,a) ),
inference(instantiation,[status(thm)],[304]) ).
cnf(99,plain,
( ~ n0(d,X0)
| ~ k0(X1)
| p1(X0,X0,X1) ),
inference(cnf,[status(esa)],[rule_063]) ).
cnf(l489,plain,
( ~ n0(d,e)
| ~ k0(b)
| p1(e,e,b) ),
inference(instantiation,[status(thm)],[99]) ).
cnf(175,plain,
( ~ q1(X0,a,X0)
| p2(X0,a,X0) ),
inference(cnf,[status(esa)],[rule_141]) ).
cnf(l198,plain,
( ~ q1(e,a,e)
| p2(e,a,e) ),
inference(instantiation,[status(thm)],[175]) ).
cnf(222,plain,
( ~ l0(X0)
| ~ r1(X0)
| r2(X0) ),
inference(cnf,[status(esa)],[rule_188]) ).
cnf(l481,plain,
( ~ l0(a)
| ~ r1(a)
| r2(a) ),
inference(instantiation,[status(thm)],[222]) ).
cnf(167,plain,
( ~ p0(X0,X0)
| ~ m0(X1,X2,X3)
| ~ s1(X2)
| l2(X3,X3) ),
inference(cnf,[status(esa)],[rule_133]) ).
cnf(l488,plain,
( ~ p0(b,b)
| ~ m0(X0_490,d,b)
| ~ s1(d)
| l2(b,b) ),
inference(instantiation,[status(thm)],[167]) ).
cnf(216,plain,
( ~ p1(X0,X0,X1)
| ~ n1(X2,X0,X1)
| ~ q2(X2,X1,X0)
| q2(X0,X2,X0) ),
inference(cnf,[status(esa)],[rule_182]) ).
cnf(l468,plain,
( ~ p1(b,b,b)
| ~ n1(a,b,b)
| ~ q2(a,b,b)
| q2(b,a,b) ),
inference(instantiation,[status(thm)],[216]) ).
cnf(l538,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(293,plain,
( ~ l1(X0,X1)
| ~ n1(X1,X1,X1)
| ~ r2(X2)
| r3(X2,X2,X2) ),
inference(cnf,[status(esa)],[rule_261]) ).
cnf(l549,plain,
( ~ l1(e,e)
| ~ n1(e,e,e)
| ~ r2(a)
| r3(a,a,a) ),
inference(instantiation,[status(thm)],[293]) ).
cnf(211,plain,
( ~ k0(X0)
| ~ p1(X1,X1,X1)
| q2(X1,X0,X0) ),
inference(cnf,[status(esa)],[rule_177]) ).
cnf(l469,plain,
( ~ k0(b)
| ~ p1(a,a,a)
| q2(a,b,b) ),
inference(instantiation,[status(thm)],[211]) ).
cnf(127,plain,
( ~ p0(X0,X1)
| ~ n0(X2,X3)
| q1(X1,X3,X1) ),
inference(cnf,[status(esa)],[rule_092]) ).
cnf(l446,plain,
( ~ p0(b,e)
| ~ n0(b,a)
| q1(e,a,e) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l490,plain,
m0(X0_490,d,b),
inference(instantiation,[status(thm)],[18]) ).
cnf(162,plain,
( ~ k1(X0)
| ~ m1(X1,X2,X3)
| ~ k2(X0,X2)
| k2(X3,X2) ),
inference(cnf,[status(esa)],[rule_127]) ).
cnf(l572,plain,
( ~ k1(a)
| ~ m1(b,a,e)
| ~ k2(a,a)
| k2(e,a) ),
inference(instantiation,[status(thm)],[162]) ).
cnf(l589,plain,
( ~ n0(b,a)
| k1(a) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(39,plain,
( ~ n0(X0,X1)
| l1(X1,X1) ),
inference(cnf,[status(esa)],[rule_002]) ).
cnf(l681,plain,
( ~ n0(d,e)
| l1(e,e) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(266,plain,
( ~ p2(X0,e,e)
| ~ n2(e)
| m3(X0,e,e) ),
inference(cnf,[status(esa)],[rule_234]) ).
cnf(l177,plain,
( ~ p2(e,e,e)
| ~ n2(e)
| m3(e,e,e) ),
inference(instantiation,[status(thm)],[266]) ).
cnf(36,plain,
n0(b,a),
inference(cnf,[status(esa)],[axiom_37]) ).
cnf(l590,plain,
n0(b,a),
inference(instantiation,[status(thm)],[36]) ).
cnf(62,plain,
( ~ m0(X0,X1,X2)
| m1(X2,X2,X2) ),
inference(cnf,[status(esa)],[rule_025]) ).
cnf(l453,plain,
( ~ m0(a,e,e)
| m1(e,e,e) ),
inference(instantiation,[status(thm)],[62]) ).
cnf(116,plain,
( ~ q0(X0,X1)
| ~ l0(X2)
| ~ m1(X3,X0,X4)
| p1(X4,X4,X4) ),
inference(cnf,[status(esa)],[rule_081]) ).
cnf(l577,plain,
( ~ q0(d,c)
| ~ l0(a)
| ~ m1(a,d,a)
| p1(a,a,a) ),
inference(instantiation,[status(thm)],[116]) ).
cnf(l540,plain,
p0(b,d),
inference(instantiation,[status(thm)],[13]) ).
cnf(77,plain,
( ~ m0(X0,X1,e)
| ~ k1(X0)
| n1(X0,e,e) ),
inference(cnf,[status(esa)],[rule_040]) ).
cnf(l706,plain,
( ~ m0(e,d,e)
| ~ k1(e)
| n1(e,e,e) ),
inference(instantiation,[status(thm)],[77]) ).
cnf(2,plain,
n0(d,e),
inference(cnf,[status(esa)],[axiom_3]) ).
cnf(l702,plain,
n0(d,e),
inference(instantiation,[status(thm)],[2]) ).
cnf(l621,plain,
n0(d,e),
inference(instantiation,[status(thm)],[2]) ).
cnf(22,plain,
m0(a,e,e),
inference(cnf,[status(esa)],[axiom_23]) ).
cnf(l459,plain,
m0(a,e,e),
inference(instantiation,[status(thm)],[22]) ).
cnf(l80,plain,
( ~ p0(b,b)
| ~ m0(X0_531,d,b)
| ~ s1(d)
| l2(b,b) ),
inference(instantiation,[status(thm)],[167]) ).
cnf(131,plain,
( ~ p0(X0,X1)
| ~ m1(X2,X3,X0)
| ~ n1(X0,X3,X3)
| ~ q1(X1,X0,X3)
| q1(X2,X2,X2) ),
inference(cnf,[status(esa)],[rule_096]) ).
cnf(l434,plain,
( ~ p0(b,b)
| ~ m1(a,b,b)
| ~ n1(b,b,b)
| ~ q1(b,b,b)
| q1(a,a,a) ),
inference(instantiation,[status(thm)],[131]) ).
cnf(147,plain,
( ~ s0(b)
| ~ k1(X0)
| q1(X0,X0,X0) ),
inference(cnf,[status(esa)],[rule_112]) ).
cnf(l890,plain,
( ~ s0(b)
| ~ k1(b)
| q1(b,b,b) ),
inference(instantiation,[status(thm)],[147]) ).
cnf(l574,plain,
( ~ s0(d)
| ~ q0(a,d)
| ~ q1(d,d,d)
| r1(a) ),
inference(instantiation,[status(thm)],[159]) ).
cnf(208,plain,
( ~ k1(e)
| ~ n2(X0)
| p2(X0,X0,X0) ),
inference(cnf,[status(esa)],[rule_174]) ).
cnf(l315,plain,
( ~ k1(e)
| ~ n2(e)
| p2(e,e,e) ),
inference(instantiation,[status(thm)],[208]) ).
cnf(280,plain,
( ~ p2(X0,X1,X1)
| ~ n3(X1)
| p3(X1,X1,X1) ),
inference(cnf,[status(esa)],[rule_248]) ).
cnf(l14,plain,
( ~ p2(e,e,e)
| ~ n3(e)
| p3(e,e,e) ),
inference(instantiation,[status(thm)],[280]) ).
cnf(95,plain,
( ~ m0(X0,X1,X2)
| ~ m0(X1,X3,X3)
| n1(X2,X2,X0) ),
inference(cnf,[status(esa)],[rule_059]) ).
cnf(l893,plain,
( ~ m0(b,d,b)
| ~ m0(d,d,d)
| n1(b,b,b) ),
inference(instantiation,[status(thm)],[95]) ).
cnf(101,plain,
( ~ p0(X0,X1)
| ~ n0(X1,X1)
| ~ l1(X1,X1)
| p1(X0,X0,X0) ),
inference(cnf,[status(esa)],[rule_065]) ).
cnf(l482,plain,
( ~ p0(b,e)
| ~ n0(e,e)
| ~ l1(e,e)
| p1(b,b,b) ),
inference(instantiation,[status(thm)],[101]) ).
cnf(l810,plain,
n0(b,a),
inference(instantiation,[status(thm)],[36]) ).
cnf(l651,plain,
( ~ n0(e,e)
| l1(e,e) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l439,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(31,plain,
k0(b),
inference(cnf,[status(esa)],[axiom_32]) ).
cnf(l614,plain,
k0(b),
inference(instantiation,[status(thm)],[31]) ).
cnf(19,plain,
l0(a),
inference(cnf,[status(esa)],[axiom_20]) ).
cnf(l586,plain,
l0(a),
inference(instantiation,[status(thm)],[19]) ).
cnf(160,plain,
( ~ p0(X0,X0)
| s1(X0) ),
inference(cnf,[status(esa)],[rule_125]) ).
cnf(l499,plain,
( ~ p0(b,b)
| s1(b) ),
inference(instantiation,[status(thm)],[160]) ).
cnf(l531,plain,
m0(X0_531,d,b),
inference(instantiation,[status(thm)],[18]) ).
cnf(179,plain,
( ~ r0(e)
| ~ p1(X0,X1,e)
| p2(e,X0,X1) ),
inference(cnf,[status(esa)],[rule_145]) ).
cnf(l153,plain,
( ~ r0(e)
| ~ p1(e,e,e)
| p2(e,e,e) ),
inference(instantiation,[status(thm)],[179]) ).
cnf(149,plain,
( ~ m0(X0,X0,X1)
| ~ k0(X1)
| q1(X0,X0,X0) ),
inference(cnf,[status(esa)],[rule_114]) ).
cnf(l800,plain,
( ~ m0(d,d,e)
| ~ k0(e)
| q1(d,d,d) ),
inference(instantiation,[status(thm)],[149]) ).
cnf(l783,plain,
( ~ l0(a)
| ~ r1(a)
| r2(a) ),
inference(instantiation,[status(thm)],[222]) ).
cnf(l891,plain,
s0(b),
inference(instantiation,[status(thm)],[4]) ).
cnf(l503,plain,
p0(b,e),
inference(instantiation,[status(thm)],[13]) ).
cnf(l897,plain,
( ~ n0(d,b)
| k1(b) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l505,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(10,plain,
n0(e,b),
inference(cnf,[status(esa)],[axiom_11]) ).
cnf(l610,plain,
n0(e,b),
inference(instantiation,[status(thm)],[10]) ).
cnf(l437,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(l900,plain,
n0(d,b),
inference(instantiation,[status(thm)],[6]) ).
cnf(l823,plain,
l0(a),
inference(instantiation,[status(thm)],[19]) ).
cnf(l565,plain,
n0(e,e),
inference(instantiation,[status(thm)],[29]) ).
cnf(161,plain,
( ~ q0(X0,X1)
| ~ s1(X2)
| s1(X0) ),
inference(cnf,[status(esa)],[rule_126]) ).
cnf(l491,plain,
( ~ q0(d,c)
| ~ s1(X0_656)
| s1(d) ),
inference(instantiation,[status(thm)],[161]) ).
cnf(l798,plain,
( ~ q0(d,b)
| ~ l0(a)
| ~ m1(e,d,e)
| p1(e,e,e) ),
inference(instantiation,[status(thm)],[116]) ).
cnf(l319,plain,
( ~ n0(e,e)
| k1(e) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(174,plain,
( ~ r0(e)
| ~ p1(b,X0,X1)
| ~ r1(b)
| n2(e) ),
inference(cnf,[status(esa)],[rule_140]) ).
cnf(l320,plain,
( ~ r0(e)
| ~ p1(b,b,b)
| ~ r1(b)
| n2(e) ),
inference(instantiation,[status(thm)],[174]) ).
cnf(28,plain,
q0(d,b),
inference(cnf,[status(esa)],[axiom_29]) ).
cnf(l912,plain,
q0(d,b),
inference(instantiation,[status(thm)],[28]) ).
cnf(l462,plain,
( ~ m1(b,b,b)
| p2(b,b,b) ),
inference(instantiation,[status(thm)],[210]) ).
cnf(l575,plain,
s0(d),
inference(instantiation,[status(thm)],[0]) ).
cnf(53,plain,
( ~ m1(X0,X1,X2)
| ~ m1(X0,X3,X1)
| m1(X2,X1,X1) ),
inference(cnf,[status(esa)],[rule_016]) ).
cnf(l498,plain,
( ~ m1(a,b,a)
| ~ m1(a,a,b)
| m1(a,b,b) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l894,plain,
m0(b,d,b),
inference(instantiation,[status(thm)],[18]) ).
cnf(12,plain,
r0(e),
inference(cnf,[status(esa)],[axiom_13]) ).
cnf(l504,plain,
r0(e),
inference(instantiation,[status(thm)],[12]) ).
cnf(164,plain,
( ~ q1(X0,X1,X1)
| k2(X1,X1) ),
inference(cnf,[status(esa)],[rule_129]) ).
cnf(l799,plain,
( ~ q1(a,a,a)
| k2(a,a) ),
inference(instantiation,[status(thm)],[164]) ).
cnf(l530,plain,
( ~ q0(d,d)
| ~ s1(b)
| s1(d) ),
inference(instantiation,[status(thm)],[161]) ).
cnf(90,plain,
( ~ l0(X0)
| ~ l1(X0,X1)
| ~ n1(X1,X2,X1)
| n1(X1,X2,X2) ),
inference(cnf,[status(esa)],[rule_054]) ).
cnf(l553,plain,
( ~ l0(a)
| ~ l1(a,a)
| ~ n1(a,b,a)
| n1(a,b,b) ),
inference(instantiation,[status(thm)],[90]) ).
cnf(42,plain,
( ~ m0(X0,X0,X1)
| m1(X1,X0,X1) ),
inference(cnf,[status(esa)],[rule_005]) ).
cnf(l904,plain,
( ~ m0(d,d,e)
| m1(e,d,e) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l852,plain,
r0(e),
inference(instantiation,[status(thm)],[12]) ).
cnf(l895,plain,
m0(d,d,d),
inference(instantiation,[status(thm)],[18]) ).
cnf(105,plain,
( ~ p0(X0,X1)
| p1(X1,X1,X0) ),
inference(cnf,[status(esa)],[rule_069]) ).
cnf(l493,plain,
( ~ p0(b,b)
| p1(b,b,b) ),
inference(instantiation,[status(thm)],[105]) ).
cnf(l866,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(32,plain,
q0(d,c),
inference(cnf,[status(esa)],[axiom_33]) ).
cnf(l558,plain,
q0(d,c),
inference(instantiation,[status(thm)],[32]) ).
cnf(16,plain,
q0(X0,d),
inference(cnf,[status(esa)],[axiom_17]) ).
cnf(l582,plain,
q0(d,d),
inference(instantiation,[status(thm)],[16]) ).
cnf(l595,plain,
( ~ q0(X0_656,d)
| ~ s1(X0_917)
| s1(X0_656) ),
inference(instantiation,[status(thm)],[161]) ).
cnf(l539,plain,
n0(e,e),
inference(instantiation,[status(thm)],[29]) ).
cnf(l562,plain,
k0(b),
inference(instantiation,[status(thm)],[31]) ).
cnf(l930,plain,
m0(d,d,e),
inference(instantiation,[status(thm)],[18]) ).
cnf(l559,plain,
l0(a),
inference(instantiation,[status(thm)],[19]) ).
cnf(l699,plain,
( ~ m0(d,d,a)
| m1(a,d,a) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l179,plain,
( ~ r0(e)
| ~ p1(b,b,b)
| ~ r1(b)
| n2(e) ),
inference(instantiation,[status(thm)],[174]) ).
cnf(l911,plain,
l0(a),
inference(instantiation,[status(thm)],[19]) ).
cnf(41,plain,
( ~ l0(X0)
| ~ k1(X1)
| ~ l1(X0,X0)
| l1(X1,X1) ),
inference(cnf,[status(esa)],[rule_004]) ).
cnf(l556,plain,
( ~ l0(c)
| ~ k1(a)
| ~ l1(c,c)
| l1(a,a) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l51,plain,
( ~ p2(e,e,e)
| n3(e) ),
inference(instantiation,[status(thm)],[272]) ).
cnf(l719,plain,
( ~ n0(e,e)
| k1(e) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l730,plain,
n0(e,e),
inference(instantiation,[status(thm)],[29]) ).
cnf(44,plain,
( ~ r0(X0)
| ~ p0(X1,X2)
| m1(X0,X2,X0) ),
inference(cnf,[status(esa)],[rule_007]) ).
cnf(l511,plain,
( ~ r0(b)
| ~ p0(b,b)
| m1(b,b,b) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l674,plain,
( ~ n0(d,c)
| l1(c,c) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l324,plain,
( ~ s0(d)
| ~ q0(b,e)
| ~ q1(d,e,d)
| r1(b) ),
inference(instantiation,[status(thm)],[159]) ).
cnf(l470,plain,
( ~ q0(a,b)
| ~ l0(a)
| ~ m1(b,a,b)
| p1(b,b,b) ),
inference(instantiation,[status(thm)],[116]) ).
cnf(40,plain,
( ~ r0(X0)
| ~ p0(X1,X2)
| ~ m0(X3,X2,X1)
| l1(X2,X3) ),
inference(cnf,[status(esa)],[rule_003]) ).
cnf(l431,plain,
( ~ r0(b)
| ~ p0(c,b)
| ~ m0(e,b,c)
| l1(b,e) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(8,plain,
r0(b),
inference(cnf,[status(esa)],[axiom_9]) ).
cnf(l433,plain,
r0(b),
inference(instantiation,[status(thm)],[8]) ).
cnf(7,plain,
m0(e,d,e),
inference(cnf,[status(esa)],[axiom_8]) ).
cnf(l707,plain,
m0(e,d,e),
inference(instantiation,[status(thm)],[7]) ).
cnf(l931,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(l701,plain,
q0(d,c),
inference(instantiation,[status(thm)],[32]) ).
cnf(26,plain,
m0(e,b,c),
inference(cnf,[status(esa)],[axiom_27]) ).
cnf(l449,plain,
m0(e,b,c),
inference(instantiation,[status(thm)],[26]) ).
cnf(23,plain,
l0(c),
inference(cnf,[status(esa)],[axiom_24]) ).
cnf(l672,plain,
l0(c),
inference(instantiation,[status(thm)],[23]) ).
cnf(l501,plain,
l0(a),
inference(instantiation,[status(thm)],[19]) ).
cnf(l786,plain,
( ~ s0(d)
| ~ q0(a,d)
| ~ q1(d,d,d)
| r1(a) ),
inference(instantiation,[status(thm)],[159]) ).
cnf(20,plain,
q0(b,e),
inference(cnf,[status(esa)],[axiom_21]) ).
cnf(l708,plain,
q0(b,e),
inference(instantiation,[status(thm)],[20]) ).
cnf(86,plain,
( ~ s0(b)
| ~ p0(b,X0)
| ~ l0(X1)
| n1(X1,X0,X1) ),
inference(cnf,[status(esa)],[rule_050]) ).
cnf(l617,plain,
( ~ s0(b)
| ~ p0(b,b)
| ~ l0(a)
| n1(a,b,a) ),
inference(instantiation,[status(thm)],[86]) ).
cnf(290,plain,
( ~ s1(X0)
| ~ l2(X1,X1)
| ~ r2(X2)
| q3(X2,X2) ),
inference(cnf,[status(esa)],[rule_258]) ).
cnf(l440,plain,
( ~ s1(d)
| ~ l2(a,a)
| ~ r2(a)
| q3(a,a) ),
inference(instantiation,[status(thm)],[290]) ).
cnf(l915,plain,
q0(a,d),
inference(instantiation,[status(thm)],[16]) ).
cnf(l583,plain,
q0(a,d),
inference(instantiation,[status(thm)],[16]) ).
cnf(l660,plain,
n0(e,e),
inference(instantiation,[status(thm)],[29]) ).
cnf(l683,plain,
s0(b),
inference(instantiation,[status(thm)],[4]) ).
cnf(l597,plain,
p0(b,e),
inference(instantiation,[status(thm)],[13]) ).
cnf(l593,plain,
( ~ p0(b,b)
| s1(b) ),
inference(instantiation,[status(thm)],[160]) ).
cnf(l656,plain,
q0(X0_656,d),
inference(instantiation,[status(thm)],[16]) ).
cnf(61,plain,
( ~ q0(X0,X1)
| ~ m0(a,X2,a)
| ~ m1(X1,c,X1)
| m1(X0,a,X1) ),
inference(cnf,[status(esa)],[rule_024]) ).
cnf(l584,plain,
( ~ q0(b,e)
| ~ m0(a,d,a)
| ~ m1(e,c,e)
| m1(b,a,e) ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l444,plain,
( ~ m1(a,b,a)
| ~ m1(a,a,b)
| m1(a,b,b) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l749,plain,
l0(a),
inference(instantiation,[status(thm)],[19]) ).
cnf(l826,plain,
s0(d),
inference(instantiation,[status(thm)],[0]) ).
cnf(l483,plain,
r0(e),
inference(instantiation,[status(thm)],[12]) ).
cnf(l496,plain,
( ~ l0(a)
| ~ r1(a)
| r2(a) ),
inference(instantiation,[status(thm)],[222]) ).
cnf(135,plain,
( ~ n0(X0,X1)
| q1(X1,X1,X1) ),
inference(cnf,[status(esa)],[rule_100]) ).
cnf(l806,plain,
( ~ n0(b,a)
| q1(a,a,a) ),
inference(instantiation,[status(thm)],[135]) ).
cnf(72,plain,
( ~ r0(X0)
| ~ l0(X1)
| m1(X0,X1,X0) ),
inference(cnf,[status(esa)],[rule_035]) ).
cnf(l733,plain,
( ~ r0(e)
| ~ l0(c)
| m1(e,c,e) ),
inference(instantiation,[status(thm)],[72]) ).
cnf(25,plain,
n0(d,c),
inference(cnf,[status(esa)],[axiom_26]) ).
cnf(l705,plain,
n0(d,c),
inference(instantiation,[status(thm)],[25]) ).
cnf(l774,plain,
r0(e),
inference(instantiation,[status(thm)],[12]) ).
cnf(l725,plain,
q0(b,e),
inference(instantiation,[status(thm)],[20]) ).
cnf(l442,plain,
( ~ p0(b,b)
| ~ m0(c,b,a)
| ~ s1(b)
| l2(a,a) ),
inference(instantiation,[status(thm)],[167]) ).
cnf(l814,plain,
m0(d,d,e),
inference(instantiation,[status(thm)],[18]) ).
cnf(l596,plain,
m0(a,d,a),
inference(instantiation,[status(thm)],[18]) ).
cnf(l686,plain,
l0(a),
inference(instantiation,[status(thm)],[19]) ).
cnf(l790,plain,
( ~ q0(X0_917,d)
| ~ s1(b)
| s1(X0_917) ),
inference(instantiation,[status(thm)],[161]) ).
cnf(l536,plain,
l0(a),
inference(instantiation,[status(thm)],[19]) ).
cnf(17,plain,
p0(c,b),
inference(cnf,[status(esa)],[axiom_18]) ).
cnf(l435,plain,
p0(c,b),
inference(instantiation,[status(thm)],[17]) ).
cnf(l515,plain,
( ~ p0(b,b)
| s1(b) ),
inference(instantiation,[status(thm)],[160]) ).
cnf(58,plain,
( ~ l0(X0)
| ~ k0(X1)
| m1(X0,X1,X0) ),
inference(cnf,[status(esa)],[rule_021]) ).
cnf(l513,plain,
( ~ l0(a)
| ~ k0(b)
| m1(a,b,a) ),
inference(instantiation,[status(thm)],[58]) ).
cnf(35,plain,
q0(a,b),
inference(cnf,[status(esa)],[axiom_36]) ).
cnf(l514,plain,
q0(a,b),
inference(instantiation,[status(thm)],[35]) ).
cnf(l325,plain,
s0(d),
inference(instantiation,[status(thm)],[0]) ).
cnf(l709,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(l510,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(l637,plain,
k0(b),
inference(instantiation,[status(thm)],[31]) ).
cnf(l932,plain,
l0(c),
inference(instantiation,[status(thm)],[23]) ).
cnf(l537,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(201,plain,
( ~ k1(X0)
| ~ s1(X0)
| p2(X0,X0,X0) ),
inference(cnf,[status(esa)],[rule_167]) ).
cnf(l841,plain,
( ~ k1(e)
| ~ s1(e)
| p2(e,e,e) ),
inference(instantiation,[status(thm)],[201]) ).
cnf(l6,plain,
( ~ q0(e,d)
| ~ s1(b)
| s1(e) ),
inference(instantiation,[status(thm)],[161]) ).
cnf(l923,plain,
( ~ p0(b,b)
| s1(b) ),
inference(instantiation,[status(thm)],[160]) ).
cnf(l937,plain,
( ~ n0(e,e)
| k1(e) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l645,plain,
l0(a),
inference(instantiation,[status(thm)],[19]) ).
cnf(l19,plain,
( ~ p0(b,b)
| s1(b) ),
inference(instantiation,[status(thm)],[160]) ).
cnf(l613,plain,
( ~ q0(a,b)
| ~ m0(a,X0_638,a)
| ~ m1(b,c,b)
| m1(a,a,b) ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l23,plain,
q0(e,d),
inference(instantiation,[status(thm)],[16]) ).
cnf(15,plain,
m0(c,b,a),
inference(cnf,[status(esa)],[axiom_16]) ).
cnf(l448,plain,
m0(c,b,a),
inference(instantiation,[status(thm)],[15]) ).
cnf(l661,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(l616,plain,
q0(a,b),
inference(instantiation,[status(thm)],[35]) ).
cnf(l500,plain,
( ~ s0(d)
| ~ q0(a,b)
| ~ q1(d,b,d)
| r1(a) ),
inference(instantiation,[status(thm)],[159]) ).
cnf(l808,plain,
n0(b,a),
inference(instantiation,[status(thm)],[36]) ).
cnf(l842,plain,
( ~ q0(e,d)
| ~ s1(X0_942)
| s1(e) ),
inference(instantiation,[status(thm)],[161]) ).
cnf(27,plain,
k0(e),
inference(cnf,[status(esa)],[axiom_28]) ).
cnf(l809,plain,
k0(e),
inference(instantiation,[status(thm)],[27]) ).
cnf(l714,plain,
( ~ p0(b,d)
| ~ n0(e,e)
| q1(d,e,d) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l485,plain,
( ~ q0(d,b)
| ~ s1(b)
| s1(d) ),
inference(instantiation,[status(thm)],[161]) ).
cnf(l517,plain,
q0(a,b),
inference(instantiation,[status(thm)],[35]) ).
cnf(l792,plain,
s0(d),
inference(instantiation,[status(thm)],[0]) ).
cnf(l938,plain,
n0(e,e),
inference(instantiation,[status(thm)],[29]) ).
cnf(9,plain,
p0(b,d),
inference(cnf,[status(esa)],[axiom_10]) ).
cnf(l721,plain,
p0(b,d),
inference(instantiation,[status(thm)],[9]) ).
cnf(l750,plain,
( ~ s0(d)
| ~ q0(b,d)
| ~ q1(d,d,d)
| r1(b) ),
inference(instantiation,[status(thm)],[159]) ).
cnf(l523,plain,
( ~ p0(b,b)
| s1(b) ),
inference(instantiation,[status(thm)],[160]) ).
cnf(l678,plain,
( ~ r0(b)
| ~ l0(c)
| m1(b,c,b) ),
inference(instantiation,[status(thm)],[72]) ).
cnf(l857,plain,
m0(d,d,a),
inference(instantiation,[status(thm)],[18]) ).
cnf(l477,plain,
( ~ r0(b)
| ~ p0(b,a)
| m1(b,a,b) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l62,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(l901,plain,
s0(d),
inference(instantiation,[status(thm)],[0]) ).
cnf(l512,plain,
r0(b),
inference(instantiation,[status(thm)],[8]) ).
cnf(l638,plain,
m0(a,X0_638,a),
inference(instantiation,[status(thm)],[11]) ).
cnf(l690,plain,
l0(c),
inference(instantiation,[status(thm)],[23]) ).
cnf(l925,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(l934,plain,
r0(b),
inference(instantiation,[status(thm)],[8]) ).
cnf(l525,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(l718,plain,
n0(e,e),
inference(instantiation,[status(thm)],[29]) ).
cnf(141,plain,
( ~ s0(X0)
| q1(X0,X0,X0) ),
inference(cnf,[status(esa)],[rule_106]) ).
cnf(l905,plain,
( ~ s0(d)
| q1(d,d,d) ),
inference(instantiation,[status(thm)],[141]) ).
cnf(l693,plain,
( ~ n0(b,a)
| k1(a) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l941,plain,
( ~ q0(X0_942,d)
| ~ s1(b)
| s1(X0_942) ),
inference(instantiation,[status(thm)],[161]) ).
cnf(l944,plain,
( ~ p0(b,b)
| s1(b) ),
inference(instantiation,[status(thm)],[160]) ).
cnf(l688,plain,
r0(b),
inference(instantiation,[status(thm)],[8]) ).
cnf(l910,plain,
q0(b,d),
inference(instantiation,[status(thm)],[16]) ).
cnf(l945,plain,
p0(b,b),
inference(instantiation,[status(thm)],[13]) ).
cnf(l940,plain,
q0(e,d),
inference(instantiation,[status(thm)],[16]) ).
cnf(l874,plain,
( ~ q0(d,d)
| q1(d,d,d) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l902,plain,
q0(d,d),
inference(instantiation,[status(thm)],[24]) ).
cnf(l791,plain,
( ~ p0(b,d)
| ~ n0(a,b)
| q1(d,b,d) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l793,plain,
p0(b,d),
inference(instantiation,[status(thm)],[13]) ).
cnf(l529,plain,
q0(d,b),
inference(instantiation,[status(thm)],[28]) ).
cnf(l917,plain,
q0(X0_917,d),
inference(instantiation,[status(thm)],[16]) ).
cnf(l936,plain,
p0(b,a),
inference(instantiation,[status(thm)],[13]) ).
cnf(l913,plain,
s0(d),
inference(instantiation,[status(thm)],[0]) ).
cnf(l703,plain,
n0(b,a),
inference(instantiation,[status(thm)],[36]) ).
cnf(14,plain,
n0(a,b),
inference(cnf,[status(esa)],[axiom_15]) ).
cnf(l926,plain,
n0(a,b),
inference(instantiation,[status(thm)],[14]) ).
cnf(l671,plain,
( ~ l0(a)
| ~ k0(b)
| m1(a,b,a) ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l680,plain,
k0(b),
inference(instantiation,[status(thm)],[31]) ).
cnf(l682,plain,
( ~ q0(a,b)
| ~ m0(a,d,a)
| ~ m1(b,c,b)
| m1(a,a,b) ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l685,plain,
q0(a,b),
inference(instantiation,[status(thm)],[35]) ).
cnf(l942,plain,
q0(X0_942,d),
inference(instantiation,[status(thm)],[16]) ).
cnf(l696,plain,
m0(a,d,a),
inference(instantiation,[status(thm)],[18]) ).
cnf(l691,plain,
l0(a),
inference(instantiation,[status(thm)],[19]) ).
cnf(66,plain,
( ~ s0(X0)
| ~ p0(X0,X1)
| m1(X0,X1,X0) ),
inference(cnf,[status(esa)],[rule_029]) ).
cnf(l695,plain,
( ~ s0(b)
| ~ p0(b,c)
| m1(b,c,b) ),
inference(instantiation,[status(thm)],[66]) ).
cnf(l947,plain,
p0(b,c),
inference(instantiation,[status(thm)],[13]) ).
cnf(l946,plain,
s0(b),
inference(instantiation,[status(thm)],[4]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l4,l106,l174,l7,l34,l12,l13,l60,l257,l419,l420,l55,l10,l16,l126,l98,l452,l15,l422,l445,l428,l429,l156,l502,l421,l78,l158,l163,l438,l465,l450,l457,l467,l609,l472,l430,l50,l119,l432,l3,l436,l489,l198,l481,l488,l468,l538,l549,l469,l446,l490,l572,l589,l681,l177,l590,l453,l577,l540,l706,l702,l621,l459,l80,l434,l890,l574,l315,l14,l893,l482,l810,l651,l439,l614,l586,l499,l531,l153,l800,l783,l891,l503,l897,l505,l610,l437,l900,l823,l565,l491,l798,l319,l320,l912,l462,l575,l498,l894,l504,l799,l530,l553,l904,l852,l895,l493,l866,l558,l582,l595,l539,l562,l930,l559,l699,l179,l911,l556,l51,l719,l730,l511,l674,l324,l470,l431,l433,l707,l931,l701,l449,l672,l501,l786,l708,l617,l440,l915,l583,l660,l683,l597,l593,l656,l584,l444,l749,l826,l483,l496,l806,l733,l705,l774,l725,l442,l814,l596,l686,l790,l536,l435,l515,l513,l514,l325,l709,l510,l637,l932,l537,l841,l6,l923,l937,l645,l19,l613,l23,l448,l661,l616,l500,l808,l842,l809,l714,l485,l517,l792,l938,l721,l750,l523,l678,l857,l477,l62,l901,l512,l638,l690,l925,l934,l525,l718,l905,l693,l941,l944,l688,l910,l945,l940,l874,l902,l791,l793,l529,l917,l936,l913,l703,l926,l671,l680,l682,l685,l942,l696,l691,l695,l947,l946]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN159-1 : TPTP v9.0.0. Released v1.1.0.
% 0.07/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.34 % Computer : n028.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue Jul 22 15:39:49 EDT 2025
% 0.14/0.34 % CPUTime :
% 0.14/0.35 % launching worker at depth: 1
% 0.14/0.35 % launching worker at depth: 2
% 0.14/0.35 % launching worker at depth: 3
% 0.14/0.35 % launching worker at depth: 4
% 0.14/0.35 % launching worker at depth: 7
% 0.14/0.35 % launching worker at depth: 6
% 0.14/0.35 % launching worker at depth: 8
% 0.14/0.35 % launching worker at depth: 5
% 0.14/0.35 % launching worker at depth: 9
% 0.14/0.35 % launching worker at depth: 10
% 0.14/0.36 % launching worker at depth: 11
% 0.14/0.38 % launching worker at depth: 12
% 0.20/0.46 % launching worker at depth: 13
% 3.64/0.82 % launching worker at depth: 14
% 4.79/1.00 % SZS status Theorem for theBenchmark
% 4.79/1.00 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------