%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYN094-1.005 : TPTP v9.0.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:52 PM UTC 2025
% Result : Unsatisfiable 17.43s 2.59s
% Output : CNFRefutation 17.43s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named u_s3_goal_1)
% Comments :
%------------------------------------------------------------------------------
cnf(0,plain,
( ~ q_0
| ~ p_0
| u_1 ),
inference(cnf,[status(esa)],[u_s3_goal_1]) ).
cnf(l0,plain,
( ~ q_0
| ~ p_0
| u_1 ),
inference(instantiation,[status(thm)],[0]) ).
cnf(1,plain,
~ u_1,
inference(cnf,[status(esa)],[u_1_s3_goal_1]) ).
cnf(l4,plain,
~ u_1,
inference(instantiation,[status(thm)],[1]) ).
cnf(5,plain,
( ~ u_3
| p_0 ),
inference(cnf,[status(esa)],[u_3_s3_type11_2]) ).
cnf(l1,plain,
( ~ u_3
| p_0 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(35,plain,
( ~ u_18
| q_0 ),
inference(cnf,[status(esa)],[u_18_s3_type12_1]) ).
cnf(l2,plain,
( ~ u_18
| q_0 ),
inference(instantiation,[status(thm)],[35]) ).
cnf(4,plain,
( ~ q_1
| ~ q_2
| p_0
| u_3 ),
inference(cnf,[status(esa)],[u_s3_type11_2]) ).
cnf(l3,plain,
( ~ q_1
| ~ q_2
| p_0
| u_3 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(38,plain,
( ~ p_2
| ~ q_3
| q_1
| u_20 ),
inference(cnf,[status(esa)],[u_s3_type12_3]) ).
cnf(l7,plain,
( ~ p_2
| ~ q_3
| q_1
| u_20 ),
inference(instantiation,[status(thm)],[38]) ).
cnf(34,plain,
( ~ p_1
| ~ q_2
| q_0
| u_18 ),
inference(cnf,[status(esa)],[u_s3_type12_1]) ).
cnf(l5,plain,
( ~ p_1
| ~ q_2
| q_0
| u_18 ),
inference(instantiation,[status(thm)],[34]) ).
cnf(10,plain,
( ~ p_3
| ~ p_4
| p_2
| u_6 ),
inference(cnf,[status(esa)],[u_s3_type11_5]) ).
cnf(l33,plain,
( ~ p_3
| ~ p_4
| p_2
| u_6 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(11,plain,
( ~ u_6
| p_2 ),
inference(cnf,[status(esa)],[u_6_s3_type11_5]) ).
cnf(l56,plain,
( ~ u_6
| p_2 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(39,plain,
( ~ u_20
| q_1 ),
inference(cnf,[status(esa)],[u_20_s3_type12_3]) ).
cnf(l16,plain,
( ~ u_20
| q_1 ),
inference(instantiation,[status(thm)],[39]) ).
cnf(44,plain,
( ~ p_4
| ~ q_3
| q_2
| u_23 ),
inference(cnf,[status(esa)],[u_s3_type12_6]) ).
cnf(l11,plain,
( ~ p_4
| ~ q_3
| q_2
| u_23 ),
inference(instantiation,[status(thm)],[44]) ).
cnf(20,plain,
( ~ q_6
| ~ q_5
| p_4
| u_11 ),
inference(cnf,[status(esa)],[u_s3_type11_10]) ).
cnf(l25,plain,
( ~ q_6
| ~ q_5
| p_4
| u_11 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(21,plain,
( ~ u_11
| p_4 ),
inference(cnf,[status(esa)],[u_11_s3_type11_10]) ).
cnf(l29,plain,
( ~ u_11
| p_4 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(45,plain,
( ~ u_23
| q_2 ),
inference(cnf,[status(esa)],[u_23_s3_type12_6]) ).
cnf(l6,plain,
( ~ u_23
| q_2 ),
inference(instantiation,[status(thm)],[45]) ).
cnf(16,plain,
( ~ q_4
| ~ q_5
| p_3
| u_9 ),
inference(cnf,[status(esa)],[u_s3_type11_8]) ).
cnf(l34,plain,
( ~ q_4
| ~ q_5
| p_3
| u_9 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(46,plain,
( ~ p_4
| ~ q_5
| u_24
| q_3 ),
inference(cnf,[status(esa)],[u_s3_type12_7]) ).
cnf(l15,plain,
( ~ p_4
| ~ q_5
| u_24
| q_3 ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l123,plain,
( ~ u_11
| p_4 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l22,plain,
( ~ q_6
| ~ q_5
| p_4
| u_11 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(7,plain,
( ~ u_4
| p_1 ),
inference(cnf,[status(esa)],[u_4_s3_type11_3]) ).
cnf(l9,plain,
( ~ u_4
| p_1 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l19,plain,
( ~ u_23
| q_2 ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l2473,plain,
( ~ u_11
| p_4 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l12,plain,
( ~ p_4
| ~ q_5
| u_24
| q_3 ),
inference(instantiation,[status(thm)],[46]) ).
cnf(58,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(cnf,[status(esa)],[u_s3_type12_13]) ).
cnf(l32,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l8,plain,
( ~ p_4
| ~ q_3
| q_2
| u_23 ),
inference(instantiation,[status(thm)],[44]) ).
cnf(6,plain,
( ~ p_2
| ~ p_3
| p_1
| u_4 ),
inference(cnf,[status(esa)],[u_s3_type11_3]) ).
cnf(l17,plain,
( ~ p_2
| ~ p_3
| p_1
| u_4 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l790,plain,
( ~ q_4
| ~ q_5
| p_3
| u_9 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(57,plain,
( ~ u_29
| q_5 ),
inference(cnf,[status(esa)],[u_29_s3_type12_12]) ).
cnf(l84,plain,
( ~ u_29
| q_5 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(47,plain,
( ~ u_24
| q_3 ),
inference(cnf,[status(esa)],[u_24_s3_type12_7]) ).
cnf(l2652,plain,
( ~ u_24
| q_3 ),
inference(instantiation,[status(thm)],[47]) ).
cnf(17,plain,
( ~ u_9
| p_3 ),
inference(cnf,[status(esa)],[u_9_s3_type11_8]) ).
cnf(l1079,plain,
( ~ u_9
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l762,plain,
( ~ u_9
| p_3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(54,plain,
( ~ q_7
| ~ p_6
| q_5
| u_28 ),
inference(cnf,[status(esa)],[u_s3_type12_11]) ).
cnf(l2894,plain,
( ~ q_7
| ~ p_6
| q_5
| u_28 ),
inference(instantiation,[status(thm)],[54]) ).
cnf(48,plain,
( ~ q_4
| ~ p_5
| q_3
| u_25 ),
inference(cnf,[status(esa)],[u_s3_type12_8]) ).
cnf(l10,plain,
( ~ q_4
| ~ p_5
| q_3
| u_25 ),
inference(instantiation,[status(thm)],[48]) ).
cnf(51,plain,
( ~ u_26
| q_4 ),
inference(cnf,[status(esa)],[u_26_s3_type12_9]) ).
cnf(l63,plain,
( ~ u_26
| q_4 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(24,plain,
( ~ q_6
| ~ q_7
| u_13
| p_5 ),
inference(cnf,[status(esa)],[u_s3_type11_12]) ).
cnf(l826,plain,
( ~ q_6
| ~ q_7
| u_13
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(49,plain,
( ~ u_25
| q_3 ),
inference(cnf,[status(esa)],[u_25_s3_type12_8]) ).
cnf(l2895,plain,
( ~ u_25
| q_3 ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l23,plain,
( ~ q_7
| ~ p_6
| q_5
| u_28 ),
inference(instantiation,[status(thm)],[54]) ).
cnf(55,plain,
( ~ u_28
| q_5 ),
inference(cnf,[status(esa)],[u_28_s3_type12_11]) ).
cnf(l2896,plain,
( ~ u_28
| q_5 ),
inference(instantiation,[status(thm)],[55]) ).
cnf(50,plain,
( ~ q_6
| ~ p_5
| q_4
| u_26 ),
inference(cnf,[status(esa)],[u_s3_type12_9]) ).
cnf(l82,plain,
( ~ q_6
| ~ p_5
| q_4
| u_26 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l2897,plain,
( ~ u_24
| q_3 ),
inference(instantiation,[status(thm)],[47]) ).
cnf(25,plain,
( ~ u_13
| p_5 ),
inference(cnf,[status(esa)],[u_13_s3_type11_12]) ).
cnf(l2898,plain,
( ~ u_13
| p_5 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l810,plain,
( ~ u_29
| q_5 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(61,plain,
( ~ u_31
| q_6 ),
inference(cnf,[status(esa)],[u_31_s3_type12_14]) ).
cnf(l30,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l41,plain,
( ~ u_11
| p_4 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l912,plain,
( ~ q_6
| ~ q_7
| u_13
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l112,plain,
( ~ q_6
| ~ q_5
| p_4
| u_11 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(56,plain,
( ~ q_6
| ~ p_7
| q_5
| u_29 ),
inference(cnf,[status(esa)],[u_s3_type12_12]) ).
cnf(l39,plain,
( ~ q_6
| ~ p_7
| q_5
| u_29 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(32,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(cnf,[status(esa)],[u_s3_type11_16]) ).
cnf(l47,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(60,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(cnf,[status(esa)],[u_s3_type12_14]) ).
cnf(l40,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(75,plain,
( ~ u_38
| p_8 ),
inference(cnf,[status(esa)],[u_38_t3_1]) ).
cnf(l50,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l854,plain,
( ~ u_26
| q_4 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l191,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l2899,plain,
( ~ u_29
| q_5 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l879,plain,
( ~ q_6
| ~ p_7
| q_5
| u_29 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(62,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(cnf,[status(esa)],[u_s3_type12_15]) ).
cnf(l2900,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l124,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(79,plain,
( ~ u_40
| q_8 ),
inference(cnf,[status(esa)],[u_40_t3_3]) ).
cnf(l245,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l2061,plain,
( ~ u_13
| p_5 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l178,plain,
( ~ q_6
| ~ p_7
| q_5
| u_29 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(59,plain,
( ~ u_30
| q_6 ),
inference(cnf,[status(esa)],[u_30_s3_type12_13]) ).
cnf(l389,plain,
( ~ u_30
| q_6 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l13,plain,
( ~ u_11
| p_4 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(33,plain,
( ~ u_17
| p_7 ),
inference(cnf,[status(esa)],[u_17_s3_type11_16]) ).
cnf(l2221,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(78,plain,
( q_8
| u_40 ),
inference(cnf,[status(esa)],[u_t3_3]) ).
cnf(l1391,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l94,plain,
( ~ u_30
| q_6 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l938,plain,
( ~ u_30
| q_6 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l1958,plain,
( ~ u_29
| q_5 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l128,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(74,plain,
( p_8
| u_38 ),
inference(cnf,[status(esa)],[u_t3_1]) ).
cnf(l64,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l53,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l254,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l1414,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l154,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(52,plain,
( ~ q_5
| ~ p_6
| q_4
| u_27 ),
inference(cnf,[status(esa)],[u_s3_type12_10]) ).
cnf(l14,plain,
( ~ q_5
| ~ p_6
| q_4
| u_27 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l979,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l189,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l978,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l2901,plain,
( ~ u_29
| q_5 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(64,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(cnf,[status(esa)],[u_s3_type12_16]) ).
cnf(l2902,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(30,plain,
( ~ p_8
| ~ p_9
| p_7
| u_16 ),
inference(cnf,[status(esa)],[u_s3_type11_15]) ).
cnf(l259,plain,
( ~ p_8
| ~ p_9
| p_7
| u_16 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l55,plain,
( ~ u_30
| q_6 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(80,plain,
( q_9
| u_41 ),
inference(cnf,[status(esa)],[u_t3_4]) ).
cnf(l2903,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l195,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l202,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l390,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l281,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l2904,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l137,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(65,plain,
( ~ u_33
| q_7 ),
inference(cnf,[status(esa)],[u_33_s3_type12_16]) ).
cnf(l54,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l2905,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l2906,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l2907,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(28,plain,
( ~ q_8
| ~ q_7
| u_15
| p_6 ),
inference(cnf,[status(esa)],[u_s3_type11_14]) ).
cnf(l2908,plain,
( ~ q_8
| ~ q_7
| u_15
| p_6 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l2909,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l184,plain,
( ~ u_28
| q_5 ),
inference(instantiation,[status(thm)],[55]) ).
cnf(29,plain,
( ~ u_15
| p_6 ),
inference(cnf,[status(esa)],[u_15_s3_type11_14]) ).
cnf(l2910,plain,
( ~ u_15
| p_6 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2911,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(81,plain,
( ~ u_41
| q_9 ),
inference(cnf,[status(esa)],[u_41_t3_4]) ).
cnf(l1579,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(77,plain,
( ~ u_39
| p_9 ),
inference(cnf,[status(esa)],[u_39_t3_2]) ).
cnf(l274,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l861,plain,
( ~ q_6
| ~ p_5
| q_4
| u_26 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l870,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l2912,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l2927,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l1426,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l2390,plain,
( ~ u_30
| q_6 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l129,plain,
( ~ q_6
| ~ q_5
| p_4
| u_11 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2958,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l1447,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l287,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l1518,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l1388,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l255,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l1394,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(76,plain,
( p_9
| u_39 ),
inference(cnf,[status(esa)],[u_t3_2]) ).
cnf(l2985,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l2915,plain,
( ~ q_8
| ~ q_7
| u_15
| p_6 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l27,plain,
( ~ p_3
| ~ p_4
| p_2
| u_6 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(63,plain,
( ~ u_32
| q_7 ),
inference(cnf,[status(esa)],[u_32_s3_type12_15]) ).
cnf(l2114,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(15,plain,
( ~ u_8
| p_3 ),
inference(cnf,[status(esa)],[u_8_s3_type11_7]) ).
cnf(l42,plain,
( ~ u_8
| p_3 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(22,plain,
( ~ p_7
| ~ p_6
| u_12
| p_5 ),
inference(cnf,[status(esa)],[u_s3_type11_11]) ).
cnf(l867,plain,
( ~ p_7
| ~ p_6
| u_12
| p_5 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l194,plain,
( ~ q_7
| ~ p_6
| q_5
| u_28 ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l2918,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l456,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l2889,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l2920,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l2846,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l2056,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l2959,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l2916,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l24,plain,
( ~ q_6
| ~ q_5
| p_4
| u_11 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l288,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2223,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l2921,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l939,plain,
( ~ q_6
| ~ p_7
| q_5
| u_29 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l2224,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l2919,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l1983,plain,
( ~ q_6
| ~ p_7
| q_5
| u_29 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l72,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l2964,plain,
( ~ u_15
| p_6 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2972,plain,
( ~ u_29
| q_5 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l2913,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l385,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l2925,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l526,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l892,plain,
( ~ p_8
| ~ p_9
| p_7
| u_16 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2933,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l1038,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l2028,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l2965,plain,
( ~ u_28
| q_5 ),
inference(instantiation,[status(thm)],[55]) ).
cnf(27,plain,
( ~ u_14
| p_6 ),
inference(cnf,[status(esa)],[u_14_s3_type11_13]) ).
cnf(l37,plain,
( ~ u_14
| p_6 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l305,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(31,plain,
( ~ u_16
| p_7 ),
inference(cnf,[status(esa)],[u_16_s3_type11_15]) ).
cnf(l954,plain,
( ~ u_16
| p_7 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l58,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(14,plain,
( ~ p_5
| ~ p_4
| u_8
| p_3 ),
inference(cnf,[status(esa)],[u_s3_type11_7]) ).
cnf(l109,plain,
( ~ p_5
| ~ p_4
| u_8
| p_3 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l391,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l1990,plain,
( ~ u_15
| p_6 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2922,plain,
( ~ q_8
| ~ q_7
| u_15
| p_6 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1404,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3007,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l2914,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3084,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l952,plain,
( ~ u_16
| p_7 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l862,plain,
( ~ u_28
| q_5 ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l3081,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l262,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l890,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(26,plain,
( ~ p_7
| ~ p_8
| u_14
| p_6 ),
inference(cnf,[status(esa)],[u_s3_type11_13]) ).
cnf(l67,plain,
( ~ p_7
| ~ p_8
| u_14
| p_6 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l2930,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l263,plain,
( ~ p_7
| ~ p_8
| u_14
| p_6 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l3000,plain,
( ~ u_30
| q_6 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l2951,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l2960,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l2111,plain,
( ~ u_30
| q_6 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l2969,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l2955,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l354,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l871,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l2932,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1395,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l87,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l68,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2956,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3085,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l1075,plain,
( ~ p_8
| ~ p_9
| p_7
| u_16 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l907,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l2924,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l2931,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l383,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l1992,plain,
( ~ p_8
| ~ p_9
| p_7
| u_16 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(67,plain,
( ~ u_34
| p_9 ),
inference(cnf,[status(esa)],[u_34_s3_type2_1]) ).
cnf(l909,plain,
( ~ u_34
| p_9 ),
inference(instantiation,[status(thm)],[67]) ).
cnf(l2934,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(23,plain,
( ~ u_12
| p_5 ),
inference(cnf,[status(esa)],[u_12_s3_type11_11]) ).
cnf(l110,plain,
( ~ u_12
| p_5 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l410,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(66,plain,
( ~ p_4
| p_9
| u_34 ),
inference(cnf,[status(esa)],[u_s3_type2_1]) ).
cnf(l3087,plain,
( ~ p_4
| p_9
| u_34 ),
inference(instantiation,[status(thm)],[66]) ).
cnf(l1635,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l2121,plain,
( ~ u_16
| p_7 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1343,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l2309,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l31,plain,
( ~ q_6
| ~ q_5
| p_4
| u_11 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1052,plain,
( ~ q_6
| ~ q_5
| p_4
| u_11 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l540,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l271,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l2026,plain,
( ~ q_6
| ~ p_7
| q_5
| u_29 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l43,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l118,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l928,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l2990,plain,
( ~ u_11
| p_4 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l557,plain,
( ~ u_16
| p_7 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l865,plain,
( ~ q_7
| ~ p_6
| q_5
| u_28 ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l198,plain,
( ~ p_7
| ~ p_6
| u_12
| p_5 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l48,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l2967,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l3079,plain,
( ~ u_14
| p_6 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1393,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l2961,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l397,plain,
( ~ p_8
| ~ p_9
| p_7
| u_16 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2929,plain,
( ~ u_12
| p_5 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l3046,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3025,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l933,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l266,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l777,plain,
( ~ q_7
| ~ p_6
| q_5
| u_28 ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l59,plain,
( ~ u_30
| q_6 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l3096,plain,
( ~ q_6
| ~ q_5
| p_4
| u_11 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l3026,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l1563,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l2274,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l535,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l66,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l866,plain,
( ~ u_14
| p_6 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2940,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1853,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l3098,plain,
( ~ u_11
| p_4 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1054,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l132,plain,
( ~ q_6
| ~ p_7
| q_5
| u_29 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l2271,plain,
( ~ u_16
| p_7 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l152,plain,
( ~ u_16
| p_7 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l800,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l3099,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l3100,plain,
( ~ q_6
| ~ p_7
| q_5
| u_29 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l1542,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3101,plain,
( ~ u_16
| p_7 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l905,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l69,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3102,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l922,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l2166,plain,
( ~ p_8
| ~ p_9
| p_7
| u_16 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3103,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l133,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l79,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l852,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3104,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(53,plain,
( ~ u_27
| q_4 ),
inference(cnf,[status(esa)],[u_27_s3_type12_10]) ).
cnf(l2917,plain,
( ~ u_27
| q_4 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l872,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l2974,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l2944,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l1076,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3092,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l570,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l1411,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l2131,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l3115,plain,
( ~ u_30
| q_6 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l308,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l2926,plain,
( ~ p_8
| ~ p_9
| p_7
| u_16 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1468,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l240,plain,
( ~ p_8
| ~ p_9
| p_7
| u_16 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3107,plain,
( ~ u_29
| q_5 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l126,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l959,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l414,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l538,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l1159,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l335,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l2938,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3091,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l2219,plain,
( ~ u_6
| p_2 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l2923,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l1243,plain,
( ~ p_4
| p_9
| u_34 ),
inference(instantiation,[status(thm)],[66]) ).
cnf(l467,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l3089,plain,
( ~ u_34
| p_9 ),
inference(instantiation,[status(thm)],[67]) ).
cnf(l2147,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l1476,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l2991,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l427,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l937,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l1970,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l3131,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(19,plain,
( ~ u_10
| p_4 ),
inference(cnf,[status(esa)],[u_10_s3_type11_9]) ).
cnf(l3169,plain,
( ~ u_10
| p_4 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1482,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l2030,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l468,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l3029,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l2310,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l1053,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l1492,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l314,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l3086,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l3127,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l3322,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l1991,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l842,plain,
( ~ u_28
| q_5 ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l3090,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3165,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3119,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3600,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l2943,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l988,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l2963,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l1288,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l138,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l71,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l3150,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l2004,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l2711,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3148,plain,
( ~ u_29
| q_5 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l230,plain,
( ~ p_7
| ~ p_8
| u_14
| p_6 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l89,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l237,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l2628,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l517,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l885,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l2297,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l3111,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l518,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l2984,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l2629,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3324,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3016,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l1662,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3134,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l899,plain,
( ~ p_7
| ~ p_8
| u_14
| p_6 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(18,plain,
( ~ p_5
| ~ p_6
| u_10
| p_4 ),
inference(cnf,[status(esa)],[u_s3_type11_9]) ).
cnf(l3175,plain,
( ~ p_5
| ~ p_6
| u_10
| p_4 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l3105,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l2936,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l2954,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l942,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l915,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l2746,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(70,plain,
( ~ q_4
| q_9
| u_36 ),
inference(cnf,[status(esa)],[u_s3_type2_3]) ).
cnf(l2667,plain,
( ~ q_4
| q_9
| u_36 ),
inference(instantiation,[status(thm)],[70]) ).
cnf(l2935,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l277,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l235,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l106,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l1239,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3140,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l650,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l2928,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l1506,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l2966,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3370,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l2053,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(71,plain,
( ~ u_36
| q_9 ),
inference(cnf,[status(esa)],[u_36_s3_type2_3]) ).
cnf(l3141,plain,
( ~ u_36
| q_9 ),
inference(instantiation,[status(thm)],[71]) ).
cnf(l3203,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3112,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l317,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3160,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3133,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3394,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3136,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l2994,plain,
( ~ u_34
| p_9 ),
inference(instantiation,[status(thm)],[67]) ).
cnf(l3161,plain,
( ~ u_27
| q_4 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l3238,plain,
( ~ q_6
| ~ q_7
| u_13
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l3220,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3147,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3237,plain,
( ~ u_15
| p_6 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1487,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1766,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l1524,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1693,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l1499,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3200,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3185,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3281,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l3542,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l282,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l883,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l440,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l2067,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l344,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l2988,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3164,plain,
( ~ q_5
| ~ p_6
| q_4
| u_27 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l3125,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3178,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1260,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3241,plain,
( ~ u_13
| p_5 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2708,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l2885,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l1540,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l544,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3396,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l2092,plain,
( ~ u_16
| p_7 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2693,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l910,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3601,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3146,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3109,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l3183,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l1102,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l273,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l3234,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3128,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l2937,plain,
( ~ u_16
| p_7 ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l3129,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3130,plain,
( ~ p_4
| p_9
| u_34 ),
inference(instantiation,[status(thm)],[66]) ).
cnf(l3082,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3114,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l897,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3223,plain,
( ~ q_8
| ~ q_7
| u_15
| p_6 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l3137,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3144,plain,
( ~ p_8
| ~ p_9
| p_7
| u_16 ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l652,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l151,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3110,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3581,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3142,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3181,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l3124,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l119,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l3306,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l884,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3323,plain,
( ~ u_30
| q_6 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l2997,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l2719,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l3132,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3443,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l3475,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l3232,plain,
( ~ q_7
| ~ p_6
| q_5
| u_28 ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l2474,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l605,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3260,plain,
( ~ p_5
| ~ p_6
| u_10
| p_4 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l3239,plain,
( ~ q_8
| ~ q_7
| u_15
| p_6 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l783,plain,
( ~ u_14
| p_6 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l3248,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3445,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3295,plain,
( ~ u_14
| p_6 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1357,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3297,plain,
( ~ p_7
| ~ p_8
| u_14
| p_6 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l3120,plain,
( ~ u_14
| p_6 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l3504,plain,
( ~ u_28
| q_5 ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l3152,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3478,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3768,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3242,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l3172,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3272,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l3609,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l3216,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3143,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3368,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3299,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3154,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l3391,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l3097,plain,
( ~ u_36
| q_9 ),
inference(instantiation,[status(thm)],[71]) ).
cnf(l3584,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3122,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3586,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3021,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3927,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l331,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l1342,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3304,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3155,plain,
( ~ q_4
| q_9
| u_36 ),
inference(instantiation,[status(thm)],[70]) ).
cnf(l3250,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l3275,plain,
( ~ u_12
| p_5 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l3850,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l1588,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l211,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l204,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3423,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3048,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3186,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3731,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3286,plain,
( ~ p_7
| ~ p_6
| u_12
| p_5 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l3604,plain,
( ~ u_26
| q_4 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l3449,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3345,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l386,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3300,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3117,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3835,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3838,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3298,plain,
( ~ u_10
| p_4 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3854,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l3256,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l2410,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l1419,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3744,plain,
( ~ p_7
| ~ p_8
| u_14
| p_6 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l3385,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3629,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l251,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3588,plain,
( ~ u_15
| p_6 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2807,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3599,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l2127,plain,
( ~ u_11
| p_4 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l3505,plain,
( ~ u_15
| p_6 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l387,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3308,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l413,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3293,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l815,plain,
( ~ p_7
| ~ p_8
| u_14
| p_6 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l3436,plain,
( ~ u_32
| q_7 ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l3433,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3458,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3982,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3437,plain,
( ~ p_8
| ~ q_9
| q_7
| u_32 ),
inference(instantiation,[status(thm)],[62]) ).
cnf(l3608,plain,
( ~ q_6
| ~ p_5
| q_4
| u_26 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l2577,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3795,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3496,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l513,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3507,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3796,plain,
( ~ u_14
| p_6 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l3928,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3813,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3508,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l464,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3553,plain,
( ~ q_8
| ~ q_7
| u_15
| p_6 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l3330,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l1698,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l3123,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3643,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l3902,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3648,plain,
( ~ q_6
| ~ q_7
| u_13
| p_5 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l3945,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3718,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l2587,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3741,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3745,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3746,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3729,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3764,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3809,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3765,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l2451,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3848,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3948,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3649,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l3194,plain,
( ~ u_36
| q_9 ),
inference(instantiation,[status(thm)],[71]) ).
cnf(l3251,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3715,plain,
( ~ u_13
| p_5 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l4054,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3950,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3644,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l4045,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3680,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3981,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l3663,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l2511,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3920,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l4067,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3766,plain,
( ~ u_17
| p_7 ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3336,plain,
( ~ q_4
| q_9
| u_36 ),
inference(instantiation,[status(thm)],[70]) ).
cnf(l3998,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3923,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3699,plain,
( ~ u_31
| q_6 ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l3929,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l3980,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l2518,plain,
( ~ q_8
| ~ q_9
| p_7
| u_17 ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l4163,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l3532,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3933,plain,
( ~ q_7
| ~ p_8
| q_6
| u_31 ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l3867,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l4004,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l1858,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3719,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3329,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3949,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l4103,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3192,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l2546,plain,
( q_9
| u_41 ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l3193,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3962,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l4107,plain,
( ~ u_41
| q_9 ),
inference(instantiation,[status(thm)],[81]) ).
cnf(l3965,plain,
( p_8
| u_38 ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l3686,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3951,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l4152,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l3819,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l4141,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l4104,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3961,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l4130,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3987,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3969,plain,
( ~ u_38
| p_8 ),
inference(instantiation,[status(thm)],[75]) ).
cnf(l4169,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l4132,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l4176,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l4171,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l3963,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l3713,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l4093,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l3676,plain,
( ~ q_5
| ~ p_6
| q_4
| u_27 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l3778,plain,
( ~ q_8
| ~ q_7
| u_15
| p_6 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l3779,plain,
( ~ q_7
| ~ p_6
| q_5
| u_28 ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l3871,plain,
( ~ u_27
| q_4 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l4083,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l4174,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l3800,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3807,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l3801,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3846,plain,
( ~ u_28
| q_5 ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l4175,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l4186,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3847,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l3825,plain,
( ~ u_15
| p_6 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3826,plain,
( ~ q_8
| ~ q_7
| u_15
| p_6 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l3831,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l4078,plain,
( ~ u_15
| p_6 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4187,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l4097,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l4178,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l4111,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l4188,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l4189,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l4182,plain,
( ~ u_33
| q_7 ),
inference(instantiation,[status(thm)],[65]) ).
cnf(l4185,plain,
( ~ q_8
| ~ p_9
| q_7
| u_33 ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l4190,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(l4191,plain,
( ~ u_40
| q_8 ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l4192,plain,
( q_8
| u_40 ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l4193,plain,
( p_9
| u_39 ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l4194,plain,
( ~ u_39
| p_9 ),
inference(instantiation,[status(thm)],[77]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l4,l1,l2,l3,l7,l5,l33,l56,l16,l11,l25,l29,l6,l34,l15,l123,l22,l9,l19,l2473,l12,l32,l8,l17,l790,l84,l2652,l1079,l762,l2894,l10,l63,l826,l2895,l23,l2896,l82,l2897,l2898,l810,l30,l41,l912,l112,l39,l47,l40,l50,l854,l191,l2899,l879,l2900,l124,l245,l2061,l178,l389,l13,l2221,l1391,l94,l938,l1958,l128,l64,l53,l254,l1414,l154,l14,l979,l189,l978,l2901,l2902,l259,l55,l2903,l195,l202,l390,l281,l2904,l137,l54,l2905,l2906,l2907,l2908,l2909,l184,l2910,l2911,l1579,l274,l861,l870,l2912,l2927,l1426,l2390,l129,l2958,l1447,l287,l1518,l1388,l255,l1394,l2985,l2915,l27,l2114,l42,l867,l194,l2918,l456,l2889,l2920,l2846,l2056,l2959,l2916,l24,l288,l2223,l2921,l939,l2224,l2919,l1983,l72,l2964,l2972,l2913,l385,l2925,l526,l892,l2933,l1038,l2028,l2965,l37,l305,l954,l58,l109,l391,l1990,l2922,l1404,l3007,l2914,l3084,l952,l862,l3081,l262,l890,l67,l2930,l263,l3000,l2951,l2960,l2111,l2969,l2955,l354,l871,l2932,l1395,l87,l68,l2956,l3085,l1075,l907,l2924,l2931,l383,l1992,l909,l2934,l110,l410,l3087,l1635,l2121,l1343,l2309,l31,l1052,l540,l271,l2026,l43,l118,l928,l2990,l557,l865,l198,l48,l2967,l3079,l1393,l2961,l397,l2929,l3046,l3025,l933,l266,l777,l59,l3096,l3026,l1563,l2274,l535,l66,l866,l2940,l1853,l3098,l1054,l132,l2271,l152,l800,l3099,l3100,l1542,l3101,l905,l69,l3102,l922,l2166,l3103,l133,l79,l852,l3104,l2917,l872,l2974,l2944,l1076,l3092,l570,l1411,l2131,l3115,l308,l2926,l1468,l240,l3107,l126,l959,l414,l538,l1159,l335,l2938,l3091,l2219,l2923,l1243,l467,l3089,l2147,l1476,l2991,l427,l937,l1970,l3131,l3169,l1482,l2030,l468,l3029,l2310,l1053,l1492,l314,l3086,l3127,l3322,l1991,l842,l3090,l3165,l3119,l3600,l2943,l988,l2963,l1288,l138,l71,l3150,l2004,l2711,l3148,l230,l89,l237,l2628,l517,l885,l2297,l3111,l518,l2984,l2629,l3324,l3016,l1662,l3134,l899,l3175,l3105,l2936,l2954,l942,l915,l2746,l2667,l2935,l277,l235,l106,l1239,l3140,l650,l2928,l1506,l2966,l3370,l2053,l3141,l3203,l3112,l317,l3160,l3133,l3394,l3136,l2994,l3161,l3238,l3220,l3147,l3237,l1487,l1766,l1524,l1693,l1499,l3200,l3185,l3281,l3542,l282,l883,l440,l2067,l344,l2988,l3164,l3125,l3178,l1260,l3241,l2708,l2885,l1540,l544,l3396,l2092,l2693,l910,l3601,l3146,l3109,l3183,l1102,l273,l3234,l3128,l2937,l3129,l3130,l3082,l3114,l897,l3223,l3137,l3144,l652,l151,l3110,l3581,l3142,l3181,l3124,l119,l3306,l884,l3323,l2997,l2719,l3132,l3443,l3475,l3232,l2474,l605,l3260,l3239,l783,l3248,l3445,l3295,l1357,l3297,l3120,l3504,l3152,l3478,l3768,l3242,l3172,l3272,l3609,l3216,l3143,l3368,l3299,l3154,l3391,l3097,l3584,l3122,l3586,l3021,l3927,l331,l1342,l3304,l3155,l3250,l3275,l3850,l1588,l211,l204,l3423,l3048,l3186,l3731,l3286,l3604,l3449,l3345,l386,l3300,l3117,l3835,l3838,l3298,l3854,l3256,l2410,l1419,l3744,l3385,l3629,l251,l3588,l2807,l3599,l2127,l3505,l387,l3308,l413,l3293,l815,l3436,l3433,l3458,l3982,l3437,l3608,l2577,l3795,l3496,l513,l3507,l3796,l3928,l3813,l3508,l464,l3553,l3330,l1698,l3123,l3643,l3902,l3648,l3945,l3718,l2587,l3741,l3745,l3746,l3729,l3764,l3809,l3765,l2451,l3848,l3948,l3649,l3194,l3251,l3715,l4054,l3950,l3644,l4045,l3680,l3981,l3663,l2511,l3920,l4067,l3766,l3336,l3998,l3923,l3699,l3929,l3980,l2518,l4163,l3532,l3933,l3867,l4004,l1858,l3719,l3329,l3949,l4103,l3192,l2546,l3193,l3962,l4107,l3965,l3686,l3951,l4152,l3819,l4141,l4104,l3961,l4130,l3987,l3969,l4169,l4132,l4176,l4171,l3963,l3713,l4093,l3676,l3778,l3779,l3871,l4083,l4174,l3800,l3807,l3801,l3846,l4175,l4186,l3847,l3825,l3826,l3831,l4078,l4187,l4097,l4178,l4111,l4188,l4189,l4182,l4185,l4190,l4191,l4192,l4193,l4194]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SYN094-1.005 : TPTP v9.0.0. Bugfixed v1.2.1.
% 0.10/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Jul 22 15:35:34 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % launching worker at depth: 1
% 0.13/0.34 % launching worker at depth: 5
% 0.13/0.34 % launching worker at depth: 3
% 0.13/0.34 % launching worker at depth: 2
% 0.13/0.34 % launching worker at depth: 4
% 0.13/0.34 % launching worker at depth: 6
% 0.13/0.34 % launching worker at depth: 7
% 0.13/0.34 % launching worker at depth: 8
% 17.43/2.59 % SZS status Theorem for theBenchmark
% 17.43/2.59 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------