%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYN001-1.005 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:26:34 PM UTC 2025
% Result : Unsatisfiable 16.62s 2.47s
% Output : CNFRefutation 16.62s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named ppppp)
% Comments :
%------------------------------------------------------------------------------
cnf(0,plain,
( p_4
| p_1
| p_2
| p_3
| p_5 ),
inference(cnf,[status(esa)],[ppppp]) ).
cnf(l0,plain,
( p_4
| p_1
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[0]) ).
cnf(23,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(cnf,[status(esa)],[npnnn]) ).
cnf(l3,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(14,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(cnf,[status(esa)],[pnnnp]) ).
cnf(l27,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(12,plain,
( ~ p_2
| ~ p_3
| p_4
| p_1
| p_5 ),
inference(cnf,[status(esa)],[pnnpp]) ).
cnf(l8,plain,
( ~ p_2
| ~ p_3
| p_4
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(5,plain,
( ~ p_3
| ~ p_5
| p_4
| p_1
| p_2 ),
inference(cnf,[status(esa)],[ppnpn]) ).
cnf(l104,plain,
( ~ p_3
| ~ p_5
| p_4
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(3,plain,
( ~ p_4
| ~ p_5
| p_1
| p_2
| p_3 ),
inference(cnf,[status(esa)],[pppnn]) ).
cnf(l11,plain,
( ~ p_4
| ~ p_5
| p_1
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(21,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(cnf,[status(esa)],[npnpn]) ).
cnf(l73,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(26,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(cnf,[status(esa)],[nnpnp]) ).
cnf(l1,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(13,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(cnf,[status(esa)],[pnnpn]) ).
cnf(l181,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(28,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(cnf,[status(esa)],[nnnpp]) ).
cnf(l188,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l28,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l10,plain,
( ~ p_3
| ~ p_5
| p_4
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(31,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(cnf,[status(esa)],[nnnnn]) ).
cnf(l68,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(4,plain,
( ~ p_3
| p_4
| p_1
| p_2
| p_5 ),
inference(cnf,[status(esa)],[ppnpp]) ).
cnf(l135,plain,
( ~ p_3
| p_4
| p_1
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(30,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(cnf,[status(esa)],[nnnnp]) ).
cnf(l77,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(20,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(cnf,[status(esa)],[npnpp]) ).
cnf(l562,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l182,plain,
( ~ p_3
| ~ p_5
| p_4
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l23,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(7,plain,
( ~ p_4
| ~ p_3
| ~ p_5
| p_1
| p_2 ),
inference(cnf,[status(esa)],[ppnnn]) ).
cnf(l4,plain,
( ~ p_4
| ~ p_3
| ~ p_5
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(15,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(cnf,[status(esa)],[pnnnn]) ).
cnf(l1095,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(16,plain,
( ~ p_1
| p_4
| p_2
| p_3
| p_5 ),
inference(cnf,[status(esa)],[npppp]) ).
cnf(l31,plain,
( ~ p_1
| p_4
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l105,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(25,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(cnf,[status(esa)],[nnppn]) ).
cnf(l940,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(22,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| p_2
| p_5 ),
inference(cnf,[status(esa)],[npnnp]) ).
cnf(l58,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(19,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(cnf,[status(esa)],[nppnn]) ).
cnf(l270,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l113,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(29,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(cnf,[status(esa)],[nnnpn]) ).
cnf(l17,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l370,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l34,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1205,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1508,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(6,plain,
( ~ p_4
| ~ p_3
| p_1
| p_2
| p_5 ),
inference(cnf,[status(esa)],[ppnnp]) ).
cnf(l215,plain,
( ~ p_4
| ~ p_3
| p_1
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1796,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l110,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(18,plain,
( ~ p_4
| ~ p_1
| p_2
| p_3
| p_5 ),
inference(cnf,[status(esa)],[nppnp]) ).
cnf(l79,plain,
( ~ p_4
| ~ p_1
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(27,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(cnf,[status(esa)],[nnpnn]) ).
cnf(l268,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l6,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l324,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l15,plain,
( ~ p_2
| ~ p_3
| p_4
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l74,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l107,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1103,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l22,plain,
( ~ p_2
| ~ p_3
| p_4
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l576,plain,
( ~ p_3
| p_4
| p_1
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l141,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l151,plain,
( ~ p_4
| ~ p_3
| ~ p_5
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l391,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l457,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1101,plain,
( ~ p_2
| ~ p_3
| p_4
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l103,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l26,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l988,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(10,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(cnf,[status(esa)],[pnpnp]) ).
cnf(l326,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l900,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l82,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1364,plain,
( ~ p_4
| ~ p_3
| ~ p_5
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l272,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l253,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l108,plain,
( ~ p_3
| p_4
| p_1
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l928,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l262,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(9,plain,
( ~ p_2
| ~ p_5
| p_4
| p_1
| p_3 ),
inference(cnf,[status(esa)],[pnppn]) ).
cnf(l1475,plain,
( ~ p_2
| ~ p_5
| p_4
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l484,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l14,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(11,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(cnf,[status(esa)],[pnpnn]) ).
cnf(l477,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l330,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1001,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(24,plain,
( ~ p_1
| ~ p_2
| p_4
| p_3
| p_5 ),
inference(cnf,[status(esa)],[nnppp]) ).
cnf(l30,plain,
( ~ p_1
| ~ p_2
| p_4
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(17,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(cnf,[status(esa)],[npppn]) ).
cnf(l36,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l618,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l156,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l24,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l259,plain,
( ~ p_2
| ~ p_5
| p_4
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1042,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l50,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l236,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l847,plain,
( ~ p_3
| p_4
| p_1
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l159,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1018,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l232,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l89,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l714,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1045,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1203,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l32,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1820,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l37,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l826,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l13,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l29,plain,
( ~ p_4
| ~ p_3
| p_1
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1491,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l16,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l76,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1537,plain,
( ~ p_1
| ~ p_2
| p_4
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l866,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l94,plain,
( ~ p_1
| p_4
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l139,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l508,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l349,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1827,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l264,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l209,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1067,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1116,plain,
( ~ p_3
| p_4
| p_1
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l289,plain,
( ~ p_2
| ~ p_5
| p_4
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l167,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l765,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1801,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l529,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l315,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l787,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l117,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l648,plain,
( ~ p_2
| ~ p_5
| p_4
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l109,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l724,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l176,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(2,plain,
( ~ p_4
| p_1
| p_2
| p_3
| p_5 ),
inference(cnf,[status(esa)],[pppnp]) ).
cnf(l150,plain,
( ~ p_4
| p_1
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l115,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1799,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1531,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l95,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l19,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l241,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l97,plain,
( ~ p_4
| p_1
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1086,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1798,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l12,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1826,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l200,plain,
( ~ p_4
| ~ p_1
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l510,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1814,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l210,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l806,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l116,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l206,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1633,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l51,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l21,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(1,plain,
( ~ p_5
| p_4
| p_1
| p_2
| p_3 ),
inference(cnf,[status(esa)],[ppppn]) ).
cnf(l144,plain,
( ~ p_5
| p_4
| p_1
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l538,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l626,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1408,plain,
( ~ p_1
| ~ p_2
| p_4
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l413,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l112,plain,
( ~ p_3
| ~ p_5
| p_4
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l368,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1316,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1258,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l35,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1836,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1485,plain,
( ~ p_4
| ~ p_3
| ~ p_5
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1041,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l283,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l202,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l96,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1728,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1831,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l256,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l225,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l197,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l879,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l991,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l179,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l980,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l85,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l238,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l20,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1621,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l250,plain,
( ~ p_2
| ~ p_3
| p_4
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1797,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l608,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1669,plain,
( ~ p_2
| ~ p_5
| p_4
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l170,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l932,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1311,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1139,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1844,plain,
( ~ p_1
| ~ p_2
| p_4
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l760,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l692,plain,
( ~ p_4
| ~ p_5
| p_1
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l83,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1807,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1549,plain,
( ~ p_4
| ~ p_3
| ~ p_5
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l171,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l354,plain,
( ~ p_1
| ~ p_2
| p_4
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l220,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l471,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l475,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l976,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1832,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1853,plain,
( ~ p_1
| ~ p_2
| p_4
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l257,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l818,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l66,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l207,plain,
( ~ p_4
| p_1
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1087,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l817,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1834,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l540,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l715,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1809,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1733,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l228,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1824,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1873,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1716,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l78,plain,
( ~ p_4
| p_1
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l793,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l703,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l740,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1382,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l263,plain,
( ~ p_4
| ~ p_1
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1818,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1825,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l331,plain,
( ~ p_3
| ~ p_5
| p_4
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1434,plain,
( ~ p_3
| ~ p_5
| p_4
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l308,plain,
( ~ p_4
| ~ p_3
| p_1
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l242,plain,
( ~ p_2
| ~ p_5
| p_4
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l666,plain,
( ~ p_4
| ~ p_3
| ~ p_5
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1019,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1097,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1837,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1159,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l670,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l453,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1506,plain,
( ~ p_2
| ~ p_5
| p_4
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1046,plain,
( ~ p_1
| ~ p_3
| p_4
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l294,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1062,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l674,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1811,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l737,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1805,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1343,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(8,plain,
( ~ p_2
| p_4
| p_1
| p_3
| p_5 ),
inference(cnf,[status(esa)],[pnppp]) ).
cnf(l299,plain,
( ~ p_2
| p_4
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1685,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1293,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1349,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1886,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l383,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1163,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l254,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1653,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| p_5 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l406,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l185,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l586,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l314,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l198,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l710,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1881,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l756,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1425,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l671,plain,
( ~ p_2
| ~ p_5
| p_4
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1050,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1064,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1702,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l873,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1854,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1566,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1898,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1182,plain,
( ~ p_4
| ~ p_3
| ~ p_5
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l594,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l385,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1244,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1266,plain,
( ~ p_4
| ~ p_3
| ~ p_5
| p_1
| p_2 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1224,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1384,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1843,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1409,plain,
( ~ p_2
| p_4
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1859,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1779,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l809,plain,
( ~ p_5
| p_4
| p_1
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1130,plain,
( ~ p_1
| ~ p_2
| ~ p_5
| p_4
| p_3 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l921,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1858,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l801,plain,
( ~ p_4
| ~ p_3
| p_1
| p_2
| p_5 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l227,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1659,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l766,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l686,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l551,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1806,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1362,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l929,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1903,plain,
( ~ p_1
| ~ p_2
| p_4
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l446,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1507,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l100,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1887,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1857,plain,
( ~ p_2
| p_4
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1510,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| ~ p_5
| p_1 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1451,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l742,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1206,plain,
( ~ p_4
| ~ p_1
| ~ p_3
| ~ p_5
| p_2 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1851,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l305,plain,
( ~ p_2
| ~ p_3
| p_4
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1896,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1868,plain,
( ~ p_2
| p_4
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1380,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1721,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1835,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1838,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1370,plain,
( ~ p_1
| ~ p_2
| p_4
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l482,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1866,plain,
( ~ p_2
| ~ p_3
| ~ p_5
| p_4
| p_1 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l195,plain,
( ~ p_4
| ~ p_2
| ~ p_5
| p_1
| p_3 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1880,plain,
( ~ p_2
| ~ p_3
| p_4
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1901,plain,
( ~ p_2
| p_4
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1907,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1867,plain,
( ~ p_4
| ~ p_1
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1890,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1741,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l183,plain,
( ~ p_1
| ~ p_5
| p_4
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l738,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1620,plain,
( ~ p_4
| ~ p_1
| ~ p_2
| ~ p_5
| p_3 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1883,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l757,plain,
( ~ p_4
| ~ p_2
| p_1
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1855,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| ~ p_5
| p_4 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1885,plain,
( ~ p_1
| ~ p_3
| ~ p_5
| p_4
| p_2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1460,plain,
( ~ p_4
| ~ p_1
| p_2
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1439,plain,
( ~ p_1
| ~ p_2
| ~ p_3
| p_4
| p_5 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1909,plain,
( ~ p_1
| ~ p_2
| p_4
| p_3
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l629,plain,
( ~ p_4
| ~ p_1
| ~ p_5
| p_2
| p_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1906,plain,
( ~ p_4
| ~ p_2
| ~ p_3
| p_1
| p_5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l3,l27,l8,l104,l11,l73,l1,l181,l188,l28,l10,l68,l135,l77,l562,l5,l182,l23,l4,l1095,l31,l105,l940,l58,l270,l113,l17,l370,l34,l1205,l1508,l2,l215,l1796,l110,l79,l268,l6,l324,l15,l74,l107,l1103,l22,l576,l141,l151,l391,l457,l1101,l103,l26,l988,l326,l900,l82,l1364,l272,l253,l108,l928,l262,l1475,l484,l14,l477,l330,l1001,l30,l36,l618,l156,l24,l259,l1042,l50,l236,l847,l159,l1018,l232,l89,l714,l1045,l1203,l32,l1820,l37,l826,l13,l29,l1491,l16,l7,l76,l1537,l866,l94,l139,l508,l349,l1827,l264,l209,l1067,l1116,l289,l167,l765,l1801,l529,l315,l787,l117,l648,l109,l724,l176,l150,l115,l1799,l1531,l95,l19,l241,l97,l1086,l1798,l12,l1826,l200,l510,l1814,l210,l806,l116,l206,l1633,l51,l21,l9,l144,l538,l626,l1408,l413,l112,l368,l1316,l1258,l35,l1836,l1485,l1041,l283,l202,l96,l1728,l1831,l256,l225,l197,l879,l991,l179,l980,l85,l238,l20,l1621,l250,l1797,l608,l1669,l170,l932,l1311,l1139,l1844,l760,l692,l83,l1807,l1549,l171,l354,l220,l471,l475,l976,l1832,l1853,l257,l818,l66,l207,l1087,l817,l1834,l540,l715,l1809,l1733,l228,l1824,l1873,l1716,l78,l793,l703,l740,l1382,l263,l1818,l1825,l331,l1434,l308,l242,l666,l1019,l1097,l1837,l1159,l670,l453,l1506,l1046,l294,l1062,l674,l1811,l737,l1805,l1343,l299,l1685,l1293,l1349,l1886,l383,l1163,l254,l1653,l406,l185,l586,l314,l198,l710,l1881,l756,l1425,l671,l1050,l1064,l1702,l873,l1854,l1566,l1898,l1182,l594,l385,l1244,l1266,l1224,l1384,l1843,l1409,l1859,l1779,l809,l1130,l921,l1858,l801,l227,l1659,l766,l686,l551,l1806,l1362,l929,l1903,l446,l1507,l100,l1887,l1857,l1510,l1451,l742,l1206,l1851,l305,l1896,l1868,l1380,l1721,l1835,l1838,l1370,l482,l1866,l195,l1880,l1901,l1907,l1867,l1890,l1741,l183,l738,l1620,l1883,l757,l1855,l1885,l1460,l1439,l1909,l629,l1906]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN001-1.005 : TPTP v9.0.0. Released v1.0.0.
% 0.07/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n017.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Jul 22 15:24:19 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % launching worker at depth: 3
% 0.13/0.34 % launching worker at depth: 1
% 0.13/0.34 % launching worker at depth: 5
% 0.13/0.34 % launching worker at depth: 6
% 0.13/0.34 % launching worker at depth: 2
% 0.13/0.34 % launching worker at depth: 4
% 0.13/0.34 % launching worker at depth: 7
% 0.13/0.34 % launching worker at depth: 8
% 16.62/2.47 % SZS status Theorem for theBenchmark
% 16.62/2.47 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------