%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYN010-1.005.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 : 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:26:36 PM UTC 2025
% Result : Unsatisfiable 2.10s 0.58s
% Output : CNFRefutation 2.25s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause_23)
% Comments :
%------------------------------------------------------------------------------
cnf(22,plain,
p_5_1,
inference(cnf,[status(esa)],[clause_23]) ).
cnf(l0,plain,
p_5_1,
inference(instantiation,[status(thm)],[22]) ).
cnf(18,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_2 ),
inference(cnf,[status(esa)],[clause_19]) ).
cnf(l1,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_2 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(26,plain,
p_5_5,
inference(cnf,[status(esa)],[clause_27]) ).
cnf(l2,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(25,plain,
p_5_4,
inference(cnf,[status(esa)],[clause_26]) ).
cnf(l3,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(12,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_1 ),
inference(cnf,[status(esa)],[clause_13]) ).
cnf(l4,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_1 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(24,plain,
p_5_3,
inference(cnf,[status(esa)],[clause_25]) ).
cnf(l5,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(11,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_5 ),
inference(cnf,[status(esa)],[clause_12]) ).
cnf(l6,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_5 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(23,plain,
p_5_2,
inference(cnf,[status(esa)],[clause_24]) ).
cnf(l7,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(17,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(cnf,[status(esa)],[clause_18]) ).
cnf(l8,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(2,plain,
( ~ p_2_4
| ~ p_2_5
| ~ p_2_1
| ~ p_2_2
| ~ p_2_3
| p_1_1 ),
inference(cnf,[status(esa)],[clause_3]) ).
cnf(l9,plain,
( ~ p_2_4
| ~ p_2_5
| ~ p_2_1
| ~ p_2_2
| ~ p_2_3
| p_1_1 ),
inference(instantiation,[status(thm)],[2]) ).
cnf(13,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(cnf,[status(esa)],[clause_14]) ).
cnf(l10,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(20,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(cnf,[status(esa)],[clause_21]) ).
cnf(l11,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(15,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(cnf,[status(esa)],[clause_16]) ).
cnf(l13,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l14,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l15,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(9,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_3 ),
inference(cnf,[status(esa)],[clause_10]) ).
cnf(l16,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l17,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l18,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(7,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_1 ),
inference(cnf,[status(esa)],[clause_8]) ).
cnf(l19,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_1 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l20,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(21,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(cnf,[status(esa)],[clause_22]) ).
cnf(l21,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(14,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(cnf,[status(esa)],[clause_15]) ).
cnf(l22,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l23,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l24,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l25,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l26,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l27,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l28,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l29,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l30,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(16,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(cnf,[status(esa)],[clause_17]) ).
cnf(l31,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l32,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l33,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l34,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l35,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l36,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l37,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l38,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l39,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l40,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l41,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l42,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(8,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_2 ),
inference(cnf,[status(esa)],[clause_9]) ).
cnf(l43,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_2 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l44,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l45,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l46,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l47,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l48,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(19,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(cnf,[status(esa)],[clause_20]) ).
cnf(l49,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l50,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l51,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l52,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l53,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(10,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_4 ),
inference(cnf,[status(esa)],[clause_11]) ).
cnf(l54,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_4 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l55,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l56,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l57,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l58,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l59,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l60,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l61,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l62,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l63,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l64,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l65,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l66,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l67,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l68,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l69,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l70,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l71,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l72,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l73,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l74,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l75,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l76,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l77,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l78,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l79,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l80,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l81,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l82,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l83,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l84,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l85,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l86,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l87,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l88,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l89,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l90,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l91,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l92,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l93,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l94,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l95,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(1,plain,
( ~ p_1_1
| ~ p_1_2
| ~ p_1_3
| ~ p_1_4
| ~ p_1_5
| p_0 ),
inference(cnf,[status(esa)],[clause_2]) ).
cnf(l96,plain,
( ~ p_1_1
| ~ p_1_2
| ~ p_1_3
| ~ p_1_4
| ~ p_1_5
| p_0 ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l97,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l98,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l99,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l100,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l101,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l102,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l103,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l104,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l105,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l106,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l107,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l108,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l109,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l110,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l111,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l112,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l113,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l114,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l115,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l116,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l117,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l118,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l119,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l120,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l121,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l122,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l123,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l124,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l125,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l126,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l127,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l128,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l129,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l130,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l131,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l132,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l133,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l134,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l135,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l136,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l137,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l138,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l139,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l140,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l141,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l142,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l143,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l144,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l145,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l146,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l147,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l148,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l149,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l150,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l151,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l152,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l153,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l154,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l155,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l156,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l157,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l158,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l159,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l160,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l161,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l162,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l163,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l164,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l165,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l166,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l167,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l168,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l169,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(0,plain,
~ p_0,
inference(cnf,[status(esa)],[clause_1]) ).
cnf(l170,plain,
~ p_0,
inference(instantiation,[status(thm)],[0]) ).
cnf(l171,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l172,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l173,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l174,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l175,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l176,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l177,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l178,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l179,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l180,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l181,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l182,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l183,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l184,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l185,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l186,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l187,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l188,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l189,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l190,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l191,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l192,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l193,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l194,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l195,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l196,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l197,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l198,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l199,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l200,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l201,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(5,plain,
( ~ p_2_4
| ~ p_2_5
| ~ p_2_1
| ~ p_2_2
| ~ p_2_3
| p_1_4 ),
inference(cnf,[status(esa)],[clause_6]) ).
cnf(l202,plain,
( ~ p_2_4
| ~ p_2_5
| ~ p_2_1
| ~ p_2_2
| ~ p_2_3
| p_1_4 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l203,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l204,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l205,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l206,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l207,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l208,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l209,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l210,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l211,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l212,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l213,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l214,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l215,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l216,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l217,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l218,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l219,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l220,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l221,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l222,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l223,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l224,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l225,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l226,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l227,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l228,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l229,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l230,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l231,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l232,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l233,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l234,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l235,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l236,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l237,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l238,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l239,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l240,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l241,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l242,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l243,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l244,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l245,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l246,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l247,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l248,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l249,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l250,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l251,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l252,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l253,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l254,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l255,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l256,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l257,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l258,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l259,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l260,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l261,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l262,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l263,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l264,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l265,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l266,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l267,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l268,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l269,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l270,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l271,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l272,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l273,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l274,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l275,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l276,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(6,plain,
( ~ p_2_4
| ~ p_2_5
| ~ p_2_1
| ~ p_2_2
| ~ p_2_3
| p_1_5 ),
inference(cnf,[status(esa)],[clause_7]) ).
cnf(l277,plain,
( ~ p_2_4
| ~ p_2_5
| ~ p_2_1
| ~ p_2_2
| ~ p_2_3
| p_1_5 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l278,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l279,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l280,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l281,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l282,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l283,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l284,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l285,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l286,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l287,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l288,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_4 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l289,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l290,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l291,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l292,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l293,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l294,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l295,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l296,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l297,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l298,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l299,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l300,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l301,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l302,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l303,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_1 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l304,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l305,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l306,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l307,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l308,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l309,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l310,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l311,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l312,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l313,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l314,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l315,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_2 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l316,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l317,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l318,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l319,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l320,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l321,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l322,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l323,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_4 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l324,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l325,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l326,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l327,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l328,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l329,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l330,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l331,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l332,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l333,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l334,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l335,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l336,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l337,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l338,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l339,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l340,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l341,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l342,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l343,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l344,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l345,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l346,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l347,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l348,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l349,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l350,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l351,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l352,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l353,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l354,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l355,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l356,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l357,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l358,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l359,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l360,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l361,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l362,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l363,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l364,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l365,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l366,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l367,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l368,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l369,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l370,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l371,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l372,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l373,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l374,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l375,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l376,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l377,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l378,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(3,plain,
( ~ p_2_4
| ~ p_2_5
| ~ p_2_1
| ~ p_2_2
| ~ p_2_3
| p_1_2 ),
inference(cnf,[status(esa)],[clause_4]) ).
cnf(l379,plain,
( ~ p_2_4
| ~ p_2_5
| ~ p_2_1
| ~ p_2_2
| ~ p_2_3
| p_1_2 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l380,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l381,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l382,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l383,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l384,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l385,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l386,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l387,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l388,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l389,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l390,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l391,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l392,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l393,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l394,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l395,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l396,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l397,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l398,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l399,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l400,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l401,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l402,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l403,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l404,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l405,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l406,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l407,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l408,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l409,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_2 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l410,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l411,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l412,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l413,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l414,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l415,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l416,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l417,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l418,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l419,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l420,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l421,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l422,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l423,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l424,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l425,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l426,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l427,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l428,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l429,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l430,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l431,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l432,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l433,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l434,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l435,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l436,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l437,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_1 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l438,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l439,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l440,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l441,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l442,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l443,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l444,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l445,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l446,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l447,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l448,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l449,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l450,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l451,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l452,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l453,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l454,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l455,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l456,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l457,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l458,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l459,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l460,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l461,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l462,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l463,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l464,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l465,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l466,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l467,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l468,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l469,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l470,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l471,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l472,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l473,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l474,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l475,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l476,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l477,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l478,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l479,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l480,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l481,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l482,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l483,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l484,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l485,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l486,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l487,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_2 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l488,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l489,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l490,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l491,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l492,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l493,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l494,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l495,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l496,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l497,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l498,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l499,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l500,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l501,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l502,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l503,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(4,plain,
( ~ p_2_4
| ~ p_2_5
| ~ p_2_1
| ~ p_2_2
| ~ p_2_3
| p_1_3 ),
inference(cnf,[status(esa)],[clause_5]) ).
cnf(l504,plain,
( ~ p_2_4
| ~ p_2_5
| ~ p_2_1
| ~ p_2_2
| ~ p_2_3
| p_1_3 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l505,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l506,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l507,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l508,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l509,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l510,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l511,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l512,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l513,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l514,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l515,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l516,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l517,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l518,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l519,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l520,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l521,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l522,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l523,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l524,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l525,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l526,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l527,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l528,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l529,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l530,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l531,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l532,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_2 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l533,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l534,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l535,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l536,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l537,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l538,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l539,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l540,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l541,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l542,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l543,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l544,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l545,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l546,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l547,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l548,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l549,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l550,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l551,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l552,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l553,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l554,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l555,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l556,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l557,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l558,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l559,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l560,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_1 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l561,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l562,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l563,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l564,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l565,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l566,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_4 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l567,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l568,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l569,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l570,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l571,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l572,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l573,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l574,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l575,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l576,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l577,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l578,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l579,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l580,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l581,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l582,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l583,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l584,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l585,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l586,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l587,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l588,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l589,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l590,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l591,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l592,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l593,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l594,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_4 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l595,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l596,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l597,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l598,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l599,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l600,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l601,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l602,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l603,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l604,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l605,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l606,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_1 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l607,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l608,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l609,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l610,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l611,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l612,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l613,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l614,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l615,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l616,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l617,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l618,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l619,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l620,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l621,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l622,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l623,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l624,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l625,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l626,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l627,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l628,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l629,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l630,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l631,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l632,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l633,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l634,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l635,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l636,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l637,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l638,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l639,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l640,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l641,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l642,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l643,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l644,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l645,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l646,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l647,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l648,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l649,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l650,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l651,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l652,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l653,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l654,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l655,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l656,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l657,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l658,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l659,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l660,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l661,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l662,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l663,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l664,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l665,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l666,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l667,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l668,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l669,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l670,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l671,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l672,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l673,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l674,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l675,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l676,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l677,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l678,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l679,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l680,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l681,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l682,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l683,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l684,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l685,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l686,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l687,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l688,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l689,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l690,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l691,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l692,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l693,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l694,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l695,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l696,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l697,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l698,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l699,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l700,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l701,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l702,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l703,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l704,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l705,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l706,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l707,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l708,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l709,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l710,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l711,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l712,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l713,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l714,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l715,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l716,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l717,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l718,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l719,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l720,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l721,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l722,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l723,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l724,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l725,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l726,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l727,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l728,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l729,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l730,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l731,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l732,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l733,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l734,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l735,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l736,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l737,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l738,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l739,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l740,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l741,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l742,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l743,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l744,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l745,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l746,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l747,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l748,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l749,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l750,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l751,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l752,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l753,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l754,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l755,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l756,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l757,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l758,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l759,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l760,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l761,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l762,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l763,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l764,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l765,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l766,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l767,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l768,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l769,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l770,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l771,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l772,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l773,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l774,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l775,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l776,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l777,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l778,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l779,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l780,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l781,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l782,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l783,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l784,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l785,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l786,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l787,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l788,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l789,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l790,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l791,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l792,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l793,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l794,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l795,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l796,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l797,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l798,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l799,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l800,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l801,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l802,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l803,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l804,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l805,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l806,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l807,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l808,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l809,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l810,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l811,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l812,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l813,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l814,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l815,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l816,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l817,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l818,plain,
( ~ p_3_5
| ~ p_3_1
| ~ p_3_4
| ~ p_3_2
| ~ p_3_3
| p_2_3 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l819,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l820,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l821,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l822,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l823,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l824,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l825,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l826,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l827,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l828,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l829,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l830,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l831,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l832,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l833,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l834,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l835,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l836,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l837,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l838,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l839,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l840,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l841,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l842,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l843,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l844,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l845,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l846,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l847,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l848,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l849,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l850,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l851,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l852,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l853,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l854,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l855,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l856,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l857,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l858,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l859,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l860,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l861,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l862,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l863,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l864,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l865,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l866,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l867,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l868,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l869,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l870,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l871,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l872,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l873,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l874,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l875,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l876,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l877,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l878,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l879,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l880,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l881,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l882,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l883,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l884,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l885,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l886,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l887,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l888,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l889,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l890,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l891,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l892,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l893,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l894,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l895,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l896,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l897,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l898,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l899,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l900,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l901,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l902,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l903,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l904,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l905,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l906,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l907,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l908,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l909,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l910,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l911,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l912,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l913,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l914,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l915,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l916,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l917,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l918,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l919,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l920,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l921,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l922,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l923,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l924,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l925,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l926,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l927,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l928,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l929,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l930,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l931,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l932,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l933,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l934,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l935,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l936,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l937,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l938,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l939,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l940,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l941,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l942,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l943,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l944,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l945,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l946,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l947,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l948,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l949,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l950,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l951,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l952,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l953,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l954,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l955,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l956,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l957,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l958,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l959,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l960,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l961,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l962,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l963,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l964,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l965,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l966,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l967,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l968,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l969,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l970,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l971,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l972,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l973,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l974,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l975,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l976,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l977,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l978,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l979,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l980,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l981,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l982,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l983,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l984,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l985,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l986,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l987,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l988,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l989,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l990,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l991,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l992,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l993,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l994,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l995,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l996,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l997,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l998,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l999,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1000,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1001,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1002,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1003,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1004,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1005,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1006,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1007,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1008,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1009,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1010,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1011,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1012,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1013,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1014,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1015,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1016,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1017,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1018,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1019,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1020,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1021,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1022,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1023,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1024,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1025,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1026,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1027,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1028,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1029,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1030,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1031,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1032,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1033,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1034,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1035,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1036,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1037,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1038,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1039,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1040,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1041,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1042,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1043,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1044,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1045,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1046,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1047,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1048,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1049,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1050,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1051,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1052,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1053,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1054,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1055,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1056,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1057,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1058,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1059,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1060,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1061,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1062,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1063,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1064,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1065,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1066,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1067,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1068,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1069,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1070,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1071,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1072,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1073,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1074,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1075,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1076,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1077,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1078,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1079,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1080,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1081,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1082,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1083,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1084,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1085,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1086,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1087,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1088,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1089,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1090,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1091,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1092,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1093,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1094,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1095,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1096,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1097,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1098,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1099,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1100,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1101,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1102,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1103,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1104,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1105,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1106,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1107,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1108,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1109,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1110,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1111,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1112,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1113,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1114,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1115,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1116,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1117,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1118,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1119,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1120,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1121,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1122,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1123,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1124,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1125,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1126,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1127,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1128,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1129,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1130,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1131,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1132,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1133,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1134,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1135,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1136,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1137,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1138,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1139,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1140,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1141,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1142,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1143,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1144,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1145,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1146,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1147,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1148,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1149,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1150,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1151,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1152,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1153,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1154,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1155,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1156,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1157,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1158,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1159,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1160,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1161,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1162,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1163,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1164,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1165,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1166,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1167,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1168,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1169,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1170,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1171,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1172,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1173,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1174,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1175,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1176,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1177,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1178,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1179,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1180,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1181,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1182,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1183,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1184,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1185,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1186,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1187,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1188,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1189,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1190,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1191,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1192,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1193,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1194,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1195,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1196,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1197,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1198,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1199,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1200,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1201,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1202,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1203,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1204,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1205,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1206,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1207,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1208,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1209,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1210,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1211,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1212,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1213,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_5 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1214,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1215,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1216,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1217,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1218,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1219,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1220,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1221,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1222,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1223,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1224,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1225,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1226,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1227,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1228,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1229,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1230,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1231,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1232,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1233,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1234,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1235,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1236,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1237,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1238,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1239,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1240,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1241,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1242,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1243,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1244,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1245,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1246,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1247,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1248,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1249,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1250,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1251,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1252,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1253,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1254,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1255,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1256,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1257,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1258,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1259,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1260,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1261,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1262,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1263,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1264,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1265,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1266,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1267,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1268,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1269,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1270,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1271,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1272,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1273,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1274,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1275,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1276,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1277,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1278,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1279,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1280,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1281,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1282,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1283,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1284,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1285,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1286,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1287,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1288,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1289,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1290,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1291,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1292,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1293,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1294,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1295,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1296,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1297,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1298,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1299,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1300,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1301,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1302,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1303,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1304,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1305,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1306,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1307,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1308,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1309,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1310,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1311,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1312,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1313,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1314,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1315,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1316,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1317,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1318,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1319,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1320,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1321,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1322,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1323,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1324,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1325,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1326,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1327,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1328,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1329,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1330,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1331,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1332,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1333,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1334,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1335,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1336,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1337,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1338,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1339,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1340,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1341,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1342,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1343,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1344,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1345,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1346,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1347,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1348,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1349,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1350,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1351,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1352,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1353,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1354,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1355,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1356,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1357,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1358,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1359,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1360,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1361,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1362,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1363,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1364,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1365,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1366,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1367,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1368,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1369,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1370,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1371,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1372,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1373,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1374,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1375,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1376,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1377,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1378,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1379,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1380,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1381,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1382,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1383,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1384,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1385,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1386,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1387,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1388,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1389,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1390,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1391,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1392,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1393,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1394,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1395,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1396,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1397,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1398,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1399,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1400,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1401,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1402,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1403,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1404,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1405,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1406,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1407,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1408,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1409,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1410,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1411,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1412,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1413,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1414,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1415,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1416,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1417,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1418,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1419,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1420,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1421,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1422,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1423,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1424,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1425,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1426,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1427,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1428,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1429,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1430,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1431,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1432,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1433,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1434,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1435,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1436,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1437,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1438,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1439,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1440,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1441,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1442,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1443,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1444,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1445,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1446,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1447,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1448,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1449,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1450,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1451,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1452,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1453,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1454,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1455,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1456,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1457,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1458,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1459,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1460,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1461,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1462,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1463,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1464,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1465,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1466,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1467,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1468,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1469,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1470,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1471,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1472,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1473,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1474,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1475,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1476,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1477,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1478,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1479,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1480,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1481,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1482,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1483,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1484,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1485,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1486,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1487,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1488,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1489,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1490,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1491,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1492,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1493,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1494,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1495,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1496,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1497,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1498,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1499,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1500,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1501,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1502,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1503,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1504,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1505,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1506,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1507,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1508,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1509,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1510,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1511,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1512,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1513,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1514,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1515,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1516,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1517,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1518,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1519,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1520,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1521,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1522,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1523,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1524,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1525,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1526,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1527,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1528,plain,
( ~ p_4_4
| ~ p_4_1
| ~ p_4_2
| ~ p_4_3
| ~ p_4_5
| p_3_2 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1529,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1530,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1531,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1532,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1533,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1534,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1535,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1536,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1537,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1538,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1539,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1540,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1541,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1542,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1543,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1544,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1545,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1546,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1547,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1548,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1549,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1550,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1551,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1552,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1553,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1554,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1555,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1556,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1557,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1558,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1559,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1560,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1561,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1562,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1563,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1564,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1565,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1566,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1567,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1568,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1569,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1570,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1571,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1572,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1573,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1574,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1575,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1576,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1577,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1578,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1579,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1580,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1581,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1582,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1583,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1584,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1585,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1586,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1587,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1588,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1589,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1590,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1591,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1592,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1593,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1594,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1595,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1596,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1597,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1598,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1599,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1600,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1601,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1602,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1603,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1604,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1605,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1606,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1607,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1608,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1609,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1610,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1611,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1612,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1613,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1614,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1615,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1616,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1617,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1618,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1619,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1620,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1621,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1622,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1623,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1624,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1625,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1626,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1627,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1628,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1629,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1630,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1631,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1632,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1633,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1634,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1635,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1636,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1637,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1638,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1639,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1640,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1641,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1642,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1643,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1644,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1645,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1646,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1647,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1648,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1649,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1650,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1651,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1652,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1653,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1654,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1655,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1656,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1657,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1658,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1659,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1660,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1661,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1662,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1663,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1664,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1665,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1666,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1667,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1668,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1669,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1670,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1671,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1672,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1673,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1674,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1675,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1676,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1677,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1678,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1679,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1680,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1681,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1682,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1683,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1684,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1685,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1686,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1687,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1688,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1689,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1690,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1691,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1692,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1693,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1694,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1695,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1696,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1697,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1698,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1699,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1700,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1701,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1702,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1703,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1704,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1705,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1706,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1707,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1708,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1709,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1710,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1711,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1712,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1713,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1714,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1715,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1716,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1717,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1718,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1719,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1720,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1721,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1722,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1723,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1724,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1725,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1726,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1727,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1728,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1729,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1730,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1731,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1732,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1733,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1734,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1735,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1736,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1737,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1738,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1739,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_4 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1740,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1741,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1742,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1743,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1744,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1745,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1746,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1747,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1748,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1749,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1750,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1751,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1752,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1753,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1754,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1755,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1756,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1757,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1758,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1759,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1760,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1761,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1762,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1763,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1764,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1765,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1766,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1767,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1768,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_5 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1769,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1770,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1771,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1772,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1773,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1774,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1775,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1776,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1777,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1778,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1779,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1780,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1781,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1782,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1783,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1784,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1785,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1786,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1787,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1788,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1789,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1790,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1791,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1792,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1793,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1794,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1795,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1796,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1797,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1798,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1799,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1800,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1801,plain,
( ~ p_5_1
| ~ p_5_5
| ~ p_5_2
| ~ p_5_3
| ~ p_5_4
| p_4_1 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1802,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1803,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1804,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1805,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1806,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1807,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1808,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1809,plain,
p_5_3,
inference(instantiation,[status(thm)],[24]) ).
cnf(l1810,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1811,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1812,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1813,plain,
p_5_5,
inference(instantiation,[status(thm)],[26]) ).
cnf(l1814,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1815,plain,
p_5_4,
inference(instantiation,[status(thm)],[25]) ).
cnf(l1816,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1817,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l1818,plain,
p_5_2,
inference(instantiation,[status(thm)],[23]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15,l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31,l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47,l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63,l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79,l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95,l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111,l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127,l128,l129,l130,l131,l132,l133,l134,l135,l136,l137,l138,l139,l140,l141,l142,l143,l144,l145,l146,l147,l148,l149,l150,l151,l152,l153,l154,l155,l156,l157,l158,l159,l160,l161,l162,l163,l164,l165,l166,l167,l168,l169,l170,l171,l172,l173,l174,l175,l176,l177,l178,l179,l180,l181,l182,l183,l184,l185,l186,l187,l188,l189,l190,l191,l192,l193,l194,l195,l196,l197,l198,l199,l200,l201,l202,l203,l204,l205,l206,l207,l208,l209,l210,l211,l212,l213,l214,l215,l216,l217,l218,l219,l220,l221,l222,l223,l224,l225,l226,l227,l228,l229,l230,l231,l232,l233,l234,l235,l236,l237,l238,l239,l240,l241,l242,l243,l244,l245,l246,l247,l248,l249,l250,l251,l252,l253,l254,l255,l256,l257,l258,l259,l260,l261,l262,l263,l264,l265,l266,l267,l268,l269,l270,l271,l272,l273,l274,l275,l276,l277,l278,l279,l280,l281,l282,l283,l284,l285,l286,l287,l288,l289,l290,l291,l292,l293,l294,l295,l296,l297,l298,l299,l300,l301,l302,l303,l304,l305,l306,l307,l308,l309,l310,l311,l312,l313,l314,l315,l316,l317,l318,l319,l320,l321,l322,l323,l324,l325,l326,l327,l328,l329,l330,l331,l332,l333,l334,l335,l336,l337,l338,l339,l340,l341,l342,l343,l344,l345,l346,l347,l348,l349,l350,l351,l352,l353,l354,l355,l356,l357,l358,l359,l360,l361,l362,l363,l364,l365,l366,l367,l368,l369,l370,l371,l372,l373,l374,l375,l376,l377,l378,l379,l380,l381,l382,l383,l384,l385,l386,l387,l388,l389,l390,l391,l392,l393,l394,l395,l396,l397,l398,l399,l400,l401,l402,l403,l404,l405,l406,l407,l408,l409,l410,l411,l412,l413,l414,l415,l416,l417,l418,l419,l420,l421,l422,l423,l424,l425,l426,l427,l428,l429,l430,l431,l432,l433,l434,l435,l436,l437,l438,l439,l440,l441,l442,l443,l444,l445,l446,l447,l448,l449,l450,l451,l452,l453,l454,l455,l456,l457,l458,l459,l460,l461,l462,l463,l464,l465,l466,l467,l468,l469,l470,l471,l472,l473,l474,l475,l476,l477,l478,l479,l480,l481,l482,l483,l484,l485,l486,l487,l488,l489,l490,l491,l492,l493,l494,l495,l496,l497,l498,l499,l500,l501,l502,l503,l504,l505,l506,l507,l508,l509,l510,l511,l512,l513,l514,l515,l516,l517,l518,l519,l520,l521,l522,l523,l524,l525,l526,l527,l528,l529,l530,l531,l532,l533,l534,l535,l536,l537,l538,l539,l540,l541,l542,l543,l544,l545,l546,l547,l548,l549,l550,l551,l552,l553,l554,l555,l556,l557,l558,l559,l560,l561,l562,l563,l564,l565,l566,l567,l568,l569,l570,l571,l572,l573,l574,l575,l576,l577,l578,l579,l580,l581,l582,l583,l584,l585,l586,l587,l588,l589,l590,l591,l592,l593,l594,l595,l596,l597,l598,l599,l600,l601,l602,l603,l604,l605,l606,l607,l608,l609,l610,l611,l612,l613,l614,l615,l616,l617,l618,l619,l620,l621,l622,l623,l624,l625,l626,l627,l628,l629,l630,l631,l632,l633,l634,l635,l636,l637,l638,l639,l640,l641,l642,l643,l644,l645,l646,l647,l648,l649,l650,l651,l652,l653,l654,l655,l656,l657,l658,l659,l660,l661,l662,l663,l664,l665,l666,l667,l668,l669,l670,l671,l672,l673,l674,l675,l676,l677,l678,l679,l680,l681,l682,l683,l684,l685,l686,l687,l688,l689,l690,l691,l692,l693,l694,l695,l696,l697,l698,l699,l700,l701,l702,l703,l704,l705,l706,l707,l708,l709,l710,l711,l712,l713,l714,l715,l716,l717,l718,l719,l720,l721,l722,l723,l724,l725,l726,l727,l728,l729,l730,l731,l732,l733,l734,l735,l736,l737,l738,l739,l740,l741,l742,l743,l744,l745,l746,l747,l748,l749,l750,l751,l752,l753,l754,l755,l756,l757,l758,l759,l760,l761,l762,l763,l764,l765,l766,l767,l768,l769,l770,l771,l772,l773,l774,l775,l776,l777,l778,l779,l780,l781,l782,l783,l784,l785,l786,l787,l788,l789,l790,l791,l792,l793,l794,l795,l796,l797,l798,l799,l800,l801,l802,l803,l804,l805,l806,l807,l808,l809,l810,l811,l812,l813,l814,l815,l816,l817,l818,l819,l820,l821,l822,l823,l824,l825,l826,l827,l828,l829,l830,l831,l832,l833,l834,l835,l836,l837,l838,l839,l840,l841,l842,l843,l844,l845,l846,l847,l848,l849,l850,l851,l852,l853,l854,l855,l856,l857,l858,l859,l860,l861,l862,l863,l864,l865,l866,l867,l868,l869,l870,l871,l872,l873,l874,l875,l876,l877,l878,l879,l880,l881,l882,l883,l884,l885,l886,l887,l888,l889,l890,l891,l892,l893,l894,l895,l896,l897,l898,l899,l900,l901,l902,l903,l904,l905,l906,l907,l908,l909,l910,l911,l912,l913,l914,l915,l916,l917,l918,l919,l920,l921,l922,l923,l924,l925,l926,l927,l928,l929,l930,l931,l932,l933,l934,l935,l936,l937,l938,l939,l940,l941,l942,l943,l944,l945,l946,l947,l948,l949,l950,l951,l952,l953,l954,l955,l956,l957,l958,l959,l960,l961,l962,l963,l964,l965,l966,l967,l968,l969,l970,l971,l972,l973,l974,l975,l976,l977,l978,l979,l980,l981,l982,l983,l984,l985,l986,l987,l988,l989,l990,l991,l992,l993,l994,l995,l996,l997,l998,l999,l1000,l1001,l1002,l1003,l1004,l1005,l1006,l1007,l1008,l1009,l1010,l1011,l1012,l1013,l1014,l1015,l1016,l1017,l1018,l1019,l1020,l1021,l1022,l1023,l1024,l1025,l1026,l1027,l1028,l1029,l1030,l1031,l1032,l1033,l1034,l1035,l1036,l1037,l1038,l1039,l1040,l1041,l1042,l1043,l1044,l1045,l1046,l1047,l1048,l1049,l1050,l1051,l1052,l1053,l1054,l1055,l1056,l1057,l1058,l1059,l1060,l1061,l1062,l1063,l1064,l1065,l1066,l1067,l1068,l1069,l1070,l1071,l1072,l1073,l1074,l1075,l1076,l1077,l1078,l1079,l1080,l1081,l1082,l1083,l1084,l1085,l1086,l1087,l1088,l1089,l1090,l1091,l1092,l1093,l1094,l1095,l1096,l1097,l1098,l1099,l1100,l1101,l1102,l1103,l1104,l1105,l1106,l1107,l1108,l1109,l1110,l1111,l1112,l1113,l1114,l1115,l1116,l1117,l1118,l1119,l1120,l1121,l1122,l1123,l1124,l1125,l1126,l1127,l1128,l1129,l1130,l1131,l1132,l1133,l1134,l1135,l1136,l1137,l1138,l1139,l1140,l1141,l1142,l1143,l1144,l1145,l1146,l1147,l1148,l1149,l1150,l1151,l1152,l1153,l1154,l1155,l1156,l1157,l1158,l1159,l1160,l1161,l1162,l1163,l1164,l1165,l1166,l1167,l1168,l1169,l1170,l1171,l1172,l1173,l1174,l1175,l1176,l1177,l1178,l1179,l1180,l1181,l1182,l1183,l1184,l1185,l1186,l1187,l1188,l1189,l1190,l1191,l1192,l1193,l1194,l1195,l1196,l1197,l1198,l1199,l1200,l1201,l1202,l1203,l1204,l1205,l1206,l1207,l1208,l1209,l1210,l1211,l1212,l1213,l1214,l1215,l1216,l1217,l1218,l1219,l1220,l1221,l1222,l1223,l1224,l1225,l1226,l1227,l1228,l1229,l1230,l1231,l1232,l1233,l1234,l1235,l1236,l1237,l1238,l1239,l1240,l1241,l1242,l1243,l1244,l1245,l1246,l1247,l1248,l1249,l1250,l1251,l1252,l1253,l1254,l1255,l1256,l1257,l1258,l1259,l1260,l1261,l1262,l1263,l1264,l1265,l1266,l1267,l1268,l1269,l1270,l1271,l1272,l1273,l1274,l1275,l1276,l1277,l1278,l1279,l1280,l1281,l1282,l1283,l1284,l1285,l1286,l1287,l1288,l1289,l1290,l1291,l1292,l1293,l1294,l1295,l1296,l1297,l1298,l1299,l1300,l1301,l1302,l1303,l1304,l1305,l1306,l1307,l1308,l1309,l1310,l1311,l1312,l1313,l1314,l1315,l1316,l1317,l1318,l1319,l1320,l1321,l1322,l1323,l1324,l1325,l1326,l1327,l1328,l1329,l1330,l1331,l1332,l1333,l1334,l1335,l1336,l1337,l1338,l1339,l1340,l1341,l1342,l1343,l1344,l1345,l1346,l1347,l1348,l1349,l1350,l1351,l1352,l1353,l1354,l1355,l1356,l1357,l1358,l1359,l1360,l1361,l1362,l1363,l1364,l1365,l1366,l1367,l1368,l1369,l1370,l1371,l1372,l1373,l1374,l1375,l1376,l1377,l1378,l1379,l1380,l1381,l1382,l1383,l1384,l1385,l1386,l1387,l1388,l1389,l1390,l1391,l1392,l1393,l1394,l1395,l1396,l1397,l1398,l1399,l1400,l1401,l1402,l1403,l1404,l1405,l1406,l1407,l1408,l1409,l1410,l1411,l1412,l1413,l1414,l1415,l1416,l1417,l1418,l1419,l1420,l1421,l1422,l1423,l1424,l1425,l1426,l1427,l1428,l1429,l1430,l1431,l1432,l1433,l1434,l1435,l1436,l1437,l1438,l1439,l1440,l1441,l1442,l1443,l1444,l1445,l1446,l1447,l1448,l1449,l1450,l1451,l1452,l1453,l1454,l1455,l1456,l1457,l1458,l1459,l1460,l1461,l1462,l1463,l1464,l1465,l1466,l1467,l1468,l1469,l1470,l1471,l1472,l1473,l1474,l1475,l1476,l1477,l1478,l1479,l1480,l1481,l1482,l1483,l1484,l1485,l1486,l1487,l1488,l1489,l1490,l1491,l1492,l1493,l1494,l1495,l1496,l1497,l1498,l1499,l1500,l1501,l1502,l1503,l1504,l1505,l1506,l1507,l1508,l1509,l1510,l1511,l1512,l1513,l1514,l1515,l1516,l1517,l1518,l1519,l1520,l1521,l1522,l1523,l1524,l1525,l1526,l1527,l1528,l1529,l1530,l1531,l1532,l1533,l1534,l1535,l1536,l1537,l1538,l1539,l1540,l1541,l1542,l1543,l1544,l1545,l1546,l1547,l1548,l1549,l1550,l1551,l1552,l1553,l1554,l1555,l1556,l1557,l1558,l1559,l1560,l1561,l1562,l1563,l1564,l1565,l1566,l1567,l1568,l1569,l1570,l1571,l1572,l1573,l1574,l1575,l1576,l1577,l1578,l1579,l1580,l1581,l1582,l1583,l1584,l1585,l1586,l1587,l1588,l1589,l1590,l1591,l1592,l1593,l1594,l1595,l1596,l1597,l1598,l1599,l1600,l1601,l1602,l1603,l1604,l1605,l1606,l1607,l1608,l1609,l1610,l1611,l1612,l1613,l1614,l1615,l1616,l1617,l1618,l1619,l1620,l1621,l1622,l1623,l1624,l1625,l1626,l1627,l1628,l1629,l1630,l1631,l1632,l1633,l1634,l1635,l1636,l1637,l1638,l1639,l1640,l1641,l1642,l1643,l1644,l1645,l1646,l1647,l1648,l1649,l1650,l1651,l1652,l1653,l1654,l1655,l1656,l1657,l1658,l1659,l1660,l1661,l1662,l1663,l1664,l1665,l1666,l1667,l1668,l1669,l1670,l1671,l1672,l1673,l1674,l1675,l1676,l1677,l1678,l1679,l1680,l1681,l1682,l1683,l1684,l1685,l1686,l1687,l1688,l1689,l1690,l1691,l1692,l1693,l1694,l1695,l1696,l1697,l1698,l1699,l1700,l1701,l1702,l1703,l1704,l1705,l1706,l1707,l1708,l1709,l1710,l1711,l1712,l1713,l1714,l1715,l1716,l1717,l1718,l1719,l1720,l1721,l1722,l1723,l1724,l1725,l1726,l1727,l1728,l1729,l1730,l1731,l1732,l1733,l1734,l1735,l1736,l1737,l1738,l1739,l1740,l1741,l1742,l1743,l1744,l1745,l1746,l1747,l1748,l1749,l1750,l1751,l1752,l1753,l1754,l1755,l1756,l1757,l1758,l1759,l1760,l1761,l1762,l1763,l1764,l1765,l1766,l1767,l1768,l1769,l1770,l1771,l1772,l1773,l1774,l1775,l1776,l1777,l1778,l1779,l1780,l1781,l1782,l1783,l1784,l1785,l1786,l1787,l1788,l1789,l1790,l1791,l1792,l1793,l1794,l1795,l1796,l1797,l1798,l1799,l1800,l1801,l1802,l1803,l1804,l1805,l1806,l1807,l1808,l1809,l1810,l1811,l1812,l1813,l1814,l1815,l1816,l1817,l1818]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYN010-1.005.005 : TPTP v9.0.0. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.32 % Computer : n028.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Tue Jul 22 15:25:04 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.11/0.32 % launching worker at depth: 2
% 0.11/0.32 % launching worker at depth: 3
% 0.11/0.32 % launching worker at depth: 1
% 0.11/0.32 % launching worker at depth: 4
% 0.11/0.32 % launching worker at depth: 5
% 0.11/0.32 % launching worker at depth: 6
% 0.11/0.32 % launching worker at depth: 7
% 0.11/0.32 % launching worker at depth: 8
% 2.10/0.58 % SZS status Theorem for theBenchmark
% 2.10/0.58 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------