----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Wed Aug 6 14:25:57 2003 The command was "../../bin/otter". The process ID is 5922. set(hyper_res). assign(stats_level,1). assign(max_given,2000). list(usable). 1 [] -H(C,xA,xB,xC,xD,xE,xF)|K1(C,F,xC,xF,xA,xB,xD,xE). 2 [] -H(D,xA,xB,xC,xD,xE,xF)|K1(D,B,xD,xB,xA,xC,xE,xF). 3 [] -H(D,xA,xB,xC,xD,xE,xF)|K1(D,E,xD,xE,xA,xB,xC,xF). 4 [] -H(E,xA,xB,xC,xD,xE,xF)|K1(E,F,xE,xF,xA,xB,xC,xD). 5 [] -K1(u,v,y,z,x1,x2,x3,x4)|K2(u,v,[],app(y,z),x1,x2,x3,x4). 6 [] -K1(u,v,[y0|y1],z,x1,x2,x3,x4)| -$TRUE(member(R,y1))|K2(u,v,[y0],app(y1,z),x1,x2,x3,x4). 7 [] -K1(u,v,[y0,y00,R],[],x1,x2,x3,x4)|K2(u,v,[y0,y00],[R],x1,x2,x3,x4). 8 [] -K2(C,F,xC,xF,xA,xB,xD,xE)|H(F,xA,xB,xC,xD,xE,xF). 9 [] -K2(D,B,xD,xB,xA,xC,xE,xF)|H(B,xA,xB,xC,xD,xE,xF). 10 [] -K2(D,E,xD,xE,xA,xB,xC,xF)|H(E,xA,xB,xC,xD,xE,xF). 11 [] -K2(E,F,xE,xF,xA,xB,xC,xD)|H(F,xA,xB,xC,xD,xE,xF). 12 [] -H(B,xA,xB,xC,xD,xE,xF)|K1(B,D,rev(xB),rev(xD),xA,xC,xE,xF). 13 [] -H(E,xA,xB,xC,xD,xE,xF)|K1(E,D,rev(xE),rev(xD),xA,xB,xC,xF). 14 [] -H(F,xA,xB,xC,xD,xE,xF)|K1(F,C,rev(xF),rev(xC),xA,xB,xD,xE). 15 [] -H(F,xA,xB,xC,xD,xE,xF)|K1(F,E,rev(xF),rev(xE),xA,xB,xC,xD). 16 [] -K2(B,D,xB,xD,xA,xC,xE,xF)|H(D,xA,rev(xB),xC,rev(xD),xE,xF). 17 [] -K2(E,D,xE,xD,xA,xB,xC,xF)|H(D,xA,xB,xC,rev(xD),rev(xE),xF). 18 [] -K2(F,C,xF,xC,xA,xB,xD,xE)|H(C,xA,xB,rev(xC),xD,xE,rev(xF)). 19 [] -K2(F,E,xF,xE,xA,xB,xC,xD)|H(E,xA,xB,xC,xD,rev(xE),rev(xF)). 20 [] -H(B,[],[R,u],xC,xD,xE,xF)|H(B,[u],[R],xC,xD,xE,xF). 21 [] -H(B,[],[R,u,v],xC,xD,xE,xF)|H(B,[v],[R,u],xC,xD,xE,xF). 22 [] -H(B,[],[u,R,v],xC,xD,xE,xF)|H(B,[v],[u,R],xC,xD,xE,xF). 23 [] -H(B,[u],xB,xC,xD,xE,xF)|H(B,[],app(xB,[u]),xC,xD,xE,xF). 24 [] -H(C,[],xB,[y0|y1],xD,xE,xF)| -$TRUE(member(R,y1))|H(C,[y0],xB,y1,xD,xE,xF). 25 [] -H(C,[y0],xB,y1,xD,xE,xF)|H(C,[],xB,[y0|y1],xD,xE,xF). end_of_list. list(sos). 26 [] H(E,[],[P],[Q],[],[R],[]). end_of_list. list(passive). 27 [] -H(E,[],[Q],[P],[],[R],[]). end_of_list. list(demodulators). 28 [] member(x,[])=$F. 29 [] member(x,[u|v])=$IF($ID(x,u),$T,member(x,v)). 30 [] rev(x)=rev2(x,[]). 31 [] rev2([],x)=x. 32 [] rev2([y1|y2],z)=rev2(y2,[y1|z]). 33 [] app([u|v],y)=[u|app(v,y)]. 34 [] app([],y)=y. end_of_list. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=14) 26 [] H(E,[],[P],[Q],[],[R],[]). ** KEPT (pick-wt=15): 35 [hyper,26,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[P],[Q],[]). ** KEPT (pick-wt=15): 36 [hyper,26,4] K1(E,F,[R],[],[],[P],[Q],[]). given clause #2: (wt=15) 35 [hyper,26,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[P],[Q],[]). ** KEPT (pick-wt=15): 37 [hyper,35,5,demod,33,34] K2(E,D,[],[R],[],[P],[Q],[]). given clause #3: (wt=15) 36 [hyper,26,4] K1(E,F,[R],[],[],[P],[Q],[]). ** KEPT (pick-wt=15): 38 [hyper,36,5,demod,33,34] K2(E,F,[],[R],[],[P],[Q],[]). given clause #4: (wt=15) 37 [hyper,35,5,demod,33,34] K2(E,D,[],[R],[],[P],[Q],[]). ** KEPT (pick-wt=14): 39 [hyper,37,17,demod,30,32,31,30,31] H(D,[],[P],[Q],[R],[],[]). given clause #5: (wt=14) 39 [hyper,37,17,demod,30,32,31,30,31] H(D,[],[P],[Q],[R],[],[]). ** KEPT (pick-wt=15): 40 [hyper,39,3] K1(D,E,[R],[],[],[P],[Q],[]). ** KEPT (pick-wt=15): 41 [hyper,39,2] K1(D,B,[R],[P],[],[Q],[],[]). given clause #6: (wt=15) 38 [hyper,36,5,demod,33,34] K2(E,F,[],[R],[],[P],[Q],[]). ** KEPT (pick-wt=14): 42 [hyper,38,11] H(F,[],[P],[Q],[],[],[R]). given clause #7: (wt=14) 42 [hyper,38,11] H(F,[],[P],[Q],[],[],[R]). ** KEPT (pick-wt=15): 43 [hyper,42,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[P],[Q],[]). ** KEPT (pick-wt=15): 44 [hyper,42,14,demod,30,32,31,30,32,31] K1(F,C,[R],[Q],[],[P],[],[]). given clause #8: (wt=15) 40 [hyper,39,3] K1(D,E,[R],[],[],[P],[Q],[]). ** KEPT (pick-wt=15): 45 [hyper,40,5,demod,33,34] K2(D,E,[],[R],[],[P],[Q],[]). given clause #9: (wt=15) 41 [hyper,39,2] K1(D,B,[R],[P],[],[Q],[],[]). ** KEPT (pick-wt=15): 46 [hyper,41,5,demod,33,34] K2(D,B,[],[R,P],[],[Q],[],[]). given clause #10: (wt=15) 43 [hyper,42,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[P],[Q],[]). ** KEPT (pick-wt=15): 47 [hyper,43,5,demod,33,34] K2(F,E,[],[R],[],[P],[Q],[]). given clause #11: (wt=15) 44 [hyper,42,14,demod,30,32,31,30,32,31] K1(F,C,[R],[Q],[],[P],[],[]). ** KEPT (pick-wt=15): 48 [hyper,44,5,demod,33,34] K2(F,C,[],[R,Q],[],[P],[],[]). given clause #12: (wt=15) 45 [hyper,40,5,demod,33,34] K2(D,E,[],[R],[],[P],[Q],[]). given clause #13: (wt=15) 46 [hyper,41,5,demod,33,34] K2(D,B,[],[R,P],[],[Q],[],[]). ** KEPT (pick-wt=14): 49 [hyper,46,9] H(B,[],[R,P],[Q],[],[],[]). given clause #14: (wt=14) 49 [hyper,46,9] H(B,[],[R,P],[Q],[],[],[]). ** KEPT (pick-wt=14): 50 [hyper,49,20] H(B,[P],[R],[Q],[],[],[]). ** KEPT (pick-wt=15): 51 [hyper,49,12,demod,30,32,32,31,30,31] K1(B,D,[P,R],[],[],[Q],[],[]). given clause #15: (wt=14) 50 [hyper,49,20] H(B,[P],[R],[Q],[],[],[]). ** KEPT (pick-wt=15): 52 [hyper,50,12,demod,30,32,31,30,31] K1(B,D,[R],[],[P],[Q],[],[]). given clause #16: (wt=15) 47 [hyper,43,5,demod,33,34] K2(F,E,[],[R],[],[P],[Q],[]). given clause #17: (wt=15) 48 [hyper,44,5,demod,33,34] K2(F,C,[],[R,Q],[],[P],[],[]). ** KEPT (pick-wt=14): 53 [hyper,48,18,demod,30,32,32,31,30,31] H(C,[],[P],[Q,R],[],[],[]). given clause #18: (wt=14) 53 [hyper,48,18,demod,30,32,32,31,30,31] H(C,[],[P],[Q,R],[],[],[]). ** KEPT (pick-wt=14): 54 [hyper,53,24,eval] H(C,[Q],[P],[R],[],[],[]). ** KEPT (pick-wt=15): 55 [hyper,53,1] K1(C,F,[Q,R],[],[],[P],[],[]). given clause #19: (wt=14) 54 [hyper,53,24,eval] H(C,[Q],[P],[R],[],[],[]). ** KEPT (pick-wt=15): 56 [hyper,54,1] K1(C,F,[R],[],[Q],[P],[],[]). given clause #20: (wt=15) 51 [hyper,49,12,demod,30,32,32,31,30,31] K1(B,D,[P,R],[],[],[Q],[],[]). ** KEPT (pick-wt=15): 57 [hyper,51,6,eval,demod,33,34] K2(B,D,[P],[R],[],[Q],[],[]). ** KEPT (pick-wt=15): 58 [hyper,51,5,demod,33,33,34] K2(B,D,[],[P,R],[],[Q],[],[]). given clause #21: (wt=15) 52 [hyper,50,12,demod,30,32,31,30,31] K1(B,D,[R],[],[P],[Q],[],[]). ** KEPT (pick-wt=15): 59 [hyper,52,5,demod,33,34] K2(B,D,[],[R],[P],[Q],[],[]). given clause #22: (wt=15) 55 [hyper,53,1] K1(C,F,[Q,R],[],[],[P],[],[]). ** KEPT (pick-wt=15): 60 [hyper,55,6,eval,demod,33,34] K2(C,F,[Q],[R],[],[P],[],[]). ** KEPT (pick-wt=15): 61 [hyper,55,5,demod,33,33,34] K2(C,F,[],[Q,R],[],[P],[],[]). given clause #23: (wt=15) 56 [hyper,54,1] K1(C,F,[R],[],[Q],[P],[],[]). ** KEPT (pick-wt=15): 62 [hyper,56,5,demod,33,34] K2(C,F,[],[R],[Q],[P],[],[]). given clause #24: (wt=15) 57 [hyper,51,6,eval,demod,33,34] K2(B,D,[P],[R],[],[Q],[],[]). given clause #25: (wt=15) 58 [hyper,51,5,demod,33,33,34] K2(B,D,[],[P,R],[],[Q],[],[]). ** KEPT (pick-wt=14): 63 [hyper,58,16,demod,30,31,30,32,32,31] H(D,[],[],[Q],[R,P],[],[]). given clause #26: (wt=14) 63 [hyper,58,16,demod,30,31,30,32,32,31] H(D,[],[],[Q],[R,P],[],[]). ** KEPT (pick-wt=15): 64 [hyper,63,3] K1(D,E,[R,P],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 65 [hyper,63,2] K1(D,B,[R,P],[],[],[Q],[],[]). given clause #27: (wt=15) 59 [hyper,52,5,demod,33,34] K2(B,D,[],[R],[P],[Q],[],[]). ** KEPT (pick-wt=14): 66 [hyper,59,16,demod,30,31,30,32,31] H(D,[P],[],[Q],[R],[],[]). given clause #28: (wt=14) 66 [hyper,59,16,demod,30,31,30,32,31] H(D,[P],[],[Q],[R],[],[]). ** KEPT (pick-wt=15): 67 [hyper,66,3] K1(D,E,[R],[],[P],[],[Q],[]). ** KEPT (pick-wt=15): 68 [hyper,66,2] K1(D,B,[R],[],[P],[Q],[],[]). given clause #29: (wt=15) 60 [hyper,55,6,eval,demod,33,34] K2(C,F,[Q],[R],[],[P],[],[]). given clause #30: (wt=15) 61 [hyper,55,5,demod,33,33,34] K2(C,F,[],[Q,R],[],[P],[],[]). ** KEPT (pick-wt=14): 69 [hyper,61,8] H(F,[],[P],[],[],[],[Q,R]). given clause #31: (wt=14) 69 [hyper,61,8] H(F,[],[P],[],[],[],[Q,R]). ** KEPT (pick-wt=15): 70 [hyper,69,15,demod,30,32,32,31,30,31] K1(F,E,[R,Q],[],[],[P],[],[]). ** KEPT (pick-wt=15): 71 [hyper,69,14,demod,30,32,32,31,30,31] K1(F,C,[R,Q],[],[],[P],[],[]). given clause #32: (wt=15) 62 [hyper,56,5,demod,33,34] K2(C,F,[],[R],[Q],[P],[],[]). ** KEPT (pick-wt=14): 72 [hyper,62,8] H(F,[Q],[P],[],[],[],[R]). given clause #33: (wt=14) 72 [hyper,62,8] H(F,[Q],[P],[],[],[],[R]). ** KEPT (pick-wt=15): 73 [hyper,72,15,demod,30,32,31,30,31] K1(F,E,[R],[],[Q],[P],[],[]). ** KEPT (pick-wt=15): 74 [hyper,72,14,demod,30,32,31,30,31] K1(F,C,[R],[],[Q],[P],[],[]). given clause #34: (wt=15) 64 [hyper,63,3] K1(D,E,[R,P],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 75 [hyper,64,5,demod,33,33,34] K2(D,E,[],[R,P],[],[],[Q],[]). given clause #35: (wt=15) 65 [hyper,63,2] K1(D,B,[R,P],[],[],[Q],[],[]). given clause #36: (wt=15) 67 [hyper,66,3] K1(D,E,[R],[],[P],[],[Q],[]). ** KEPT (pick-wt=15): 76 [hyper,67,5,demod,33,34] K2(D,E,[],[R],[P],[],[Q],[]). given clause #37: (wt=15) 68 [hyper,66,2] K1(D,B,[R],[],[P],[Q],[],[]). ** KEPT (pick-wt=15): 77 [hyper,68,5,demod,33,34] K2(D,B,[],[R],[P],[Q],[],[]). given clause #38: (wt=15) 70 [hyper,69,15,demod,30,32,32,31,30,31] K1(F,E,[R,Q],[],[],[P],[],[]). ** KEPT (pick-wt=15): 78 [hyper,70,5,demod,33,33,34] K2(F,E,[],[R,Q],[],[P],[],[]). given clause #39: (wt=15) 71 [hyper,69,14,demod,30,32,32,31,30,31] K1(F,C,[R,Q],[],[],[P],[],[]). given clause #40: (wt=15) 73 [hyper,72,15,demod,30,32,31,30,31] K1(F,E,[R],[],[Q],[P],[],[]). ** KEPT (pick-wt=15): 79 [hyper,73,5,demod,33,34] K2(F,E,[],[R],[Q],[P],[],[]). given clause #41: (wt=15) 74 [hyper,72,14,demod,30,32,31,30,31] K1(F,C,[R],[],[Q],[P],[],[]). ** KEPT (pick-wt=15): 80 [hyper,74,5,demod,33,34] K2(F,C,[],[R],[Q],[P],[],[]). given clause #42: (wt=15) 75 [hyper,64,5,demod,33,33,34] K2(D,E,[],[R,P],[],[],[Q],[]). ** KEPT (pick-wt=14): 81 [hyper,75,10] H(E,[],[],[Q],[],[R,P],[]). given clause #43: (wt=14) 81 [hyper,75,10] H(E,[],[],[Q],[],[R,P],[]). ** KEPT (pick-wt=15): 82 [hyper,81,13,demod,30,32,32,31,30,31] K1(E,D,[P,R],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 83 [hyper,81,4] K1(E,F,[R,P],[],[],[],[Q],[]). given clause #44: (wt=15) 76 [hyper,67,5,demod,33,34] K2(D,E,[],[R],[P],[],[Q],[]). ** KEPT (pick-wt=14): 84 [hyper,76,10] H(E,[P],[],[Q],[],[R],[]). given clause #45: (wt=14) 84 [hyper,76,10] H(E,[P],[],[Q],[],[R],[]). ** KEPT (pick-wt=15): 85 [hyper,84,13,demod,30,32,31,30,31] K1(E,D,[R],[],[P],[],[Q],[]). ** KEPT (pick-wt=15): 86 [hyper,84,4] K1(E,F,[R],[],[P],[],[Q],[]). given clause #46: (wt=15) 77 [hyper,68,5,demod,33,34] K2(D,B,[],[R],[P],[Q],[],[]). given clause #47: (wt=15) 78 [hyper,70,5,demod,33,33,34] K2(F,E,[],[R,Q],[],[P],[],[]). ** KEPT (pick-wt=14): 87 [hyper,78,19,demod,30,32,32,31,30,31] H(E,[],[P],[],[],[Q,R],[]). given clause #48: (wt=14) 87 [hyper,78,19,demod,30,32,32,31,30,31] H(E,[],[P],[],[],[Q,R],[]). ** KEPT (pick-wt=15): 88 [hyper,87,13,demod,30,32,32,31,30,31] K1(E,D,[R,Q],[],[],[P],[],[]). ** KEPT (pick-wt=15): 89 [hyper,87,4] K1(E,F,[Q,R],[],[],[P],[],[]). given clause #49: (wt=15) 79 [hyper,73,5,demod,33,34] K2(F,E,[],[R],[Q],[P],[],[]). ** KEPT (pick-wt=14): 90 [hyper,79,19,demod,30,32,31,30,31] H(E,[Q],[P],[],[],[R],[]). given clause #50: (wt=14) 90 [hyper,79,19,demod,30,32,31,30,31] H(E,[Q],[P],[],[],[R],[]). ** KEPT (pick-wt=15): 91 [hyper,90,13,demod,30,32,31,30,31] K1(E,D,[R],[],[Q],[P],[],[]). ** KEPT (pick-wt=15): 92 [hyper,90,4] K1(E,F,[R],[],[Q],[P],[],[]). given clause #51: (wt=15) 80 [hyper,74,5,demod,33,34] K2(F,C,[],[R],[Q],[P],[],[]). given clause #52: (wt=15) 82 [hyper,81,13,demod,30,32,32,31,30,31] K1(E,D,[P,R],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 93 [hyper,82,6,eval,demod,33,34] K2(E,D,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=15): 94 [hyper,82,5,demod,33,33,34] K2(E,D,[],[P,R],[],[],[Q],[]). given clause #53: (wt=15) 83 [hyper,81,4] K1(E,F,[R,P],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 95 [hyper,83,5,demod,33,33,34] K2(E,F,[],[R,P],[],[],[Q],[]). given clause #54: (wt=15) 85 [hyper,84,13,demod,30,32,31,30,31] K1(E,D,[R],[],[P],[],[Q],[]). ** KEPT (pick-wt=15): 96 [hyper,85,5,demod,33,34] K2(E,D,[],[R],[P],[],[Q],[]). given clause #55: (wt=15) 86 [hyper,84,4] K1(E,F,[R],[],[P],[],[Q],[]). ** KEPT (pick-wt=15): 97 [hyper,86,5,demod,33,34] K2(E,F,[],[R],[P],[],[Q],[]). given clause #56: (wt=15) 88 [hyper,87,13,demod,30,32,32,31,30,31] K1(E,D,[R,Q],[],[],[P],[],[]). ** KEPT (pick-wt=15): 98 [hyper,88,5,demod,33,33,34] K2(E,D,[],[R,Q],[],[P],[],[]). given clause #57: (wt=15) 89 [hyper,87,4] K1(E,F,[Q,R],[],[],[P],[],[]). ** KEPT (pick-wt=15): 99 [hyper,89,6,eval,demod,33,34] K2(E,F,[Q],[R],[],[P],[],[]). ** KEPT (pick-wt=15): 100 [hyper,89,5,demod,33,33,34] K2(E,F,[],[Q,R],[],[P],[],[]). given clause #58: (wt=15) 91 [hyper,90,13,demod,30,32,31,30,31] K1(E,D,[R],[],[Q],[P],[],[]). ** KEPT (pick-wt=15): 101 [hyper,91,5,demod,33,34] K2(E,D,[],[R],[Q],[P],[],[]). given clause #59: (wt=15) 92 [hyper,90,4] K1(E,F,[R],[],[Q],[P],[],[]). ** KEPT (pick-wt=15): 102 [hyper,92,5,demod,33,34] K2(E,F,[],[R],[Q],[P],[],[]). given clause #60: (wt=15) 93 [hyper,82,6,eval,demod,33,34] K2(E,D,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=14): 103 [hyper,93,17,demod,30,32,31,30,32,31] H(D,[],[],[Q],[R],[P],[]). given clause #61: (wt=14) 103 [hyper,93,17,demod,30,32,31,30,32,31] H(D,[],[],[Q],[R],[P],[]). ** KEPT (pick-wt=15): 104 [hyper,103,3] K1(D,E,[R],[P],[],[],[Q],[]). ** KEPT (pick-wt=15): 105 [hyper,103,2] K1(D,B,[R],[],[],[Q],[P],[]). given clause #62: (wt=15) 94 [hyper,82,5,demod,33,33,34] K2(E,D,[],[P,R],[],[],[Q],[]). given clause #63: (wt=15) 95 [hyper,83,5,demod,33,33,34] K2(E,F,[],[R,P],[],[],[Q],[]). ** KEPT (pick-wt=14): 106 [hyper,95,11] H(F,[],[],[Q],[],[],[R,P]). given clause #64: (wt=14) 106 [hyper,95,11] H(F,[],[],[Q],[],[],[R,P]). ** KEPT (pick-wt=15): 107 [hyper,106,15,demod,30,32,32,31,30,31] K1(F,E,[P,R],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 108 [hyper,106,14,demod,30,32,32,31,30,32,31] K1(F,C,[P,R],[Q],[],[],[],[]). given clause #65: (wt=15) 96 [hyper,85,5,demod,33,34] K2(E,D,[],[R],[P],[],[Q],[]). given clause #66: (wt=15) 97 [hyper,86,5,demod,33,34] K2(E,F,[],[R],[P],[],[Q],[]). ** KEPT (pick-wt=14): 109 [hyper,97,11] H(F,[P],[],[Q],[],[],[R]). given clause #67: (wt=14) 109 [hyper,97,11] H(F,[P],[],[Q],[],[],[R]). ** KEPT (pick-wt=15): 110 [hyper,109,15,demod,30,32,31,30,31] K1(F,E,[R],[],[P],[],[Q],[]). ** KEPT (pick-wt=15): 111 [hyper,109,14,demod,30,32,31,30,32,31] K1(F,C,[R],[Q],[P],[],[],[]). given clause #68: (wt=15) 98 [hyper,88,5,demod,33,33,34] K2(E,D,[],[R,Q],[],[P],[],[]). ** KEPT (pick-wt=14): 112 [hyper,98,17,demod,30,32,32,31,30,31] H(D,[],[P],[],[Q,R],[],[]). given clause #69: (wt=14) 112 [hyper,98,17,demod,30,32,32,31,30,31] H(D,[],[P],[],[Q,R],[],[]). ** KEPT (pick-wt=15): 113 [hyper,112,3] K1(D,E,[Q,R],[],[],[P],[],[]). ** KEPT (pick-wt=15): 114 [hyper,112,2] K1(D,B,[Q,R],[P],[],[],[],[]). given clause #70: (wt=15) 99 [hyper,89,6,eval,demod,33,34] K2(E,F,[Q],[R],[],[P],[],[]). ** KEPT (pick-wt=14): 115 [hyper,99,11] H(F,[],[P],[],[],[Q],[R]). given clause #71: (wt=14) 115 [hyper,99,11] H(F,[],[P],[],[],[Q],[R]). ** KEPT (pick-wt=15): 116 [hyper,115,15,demod,30,32,31,30,32,31] K1(F,E,[R],[Q],[],[P],[],[]). ** KEPT (pick-wt=15): 117 [hyper,115,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[P],[],[Q]). given clause #72: (wt=15) 100 [hyper,89,5,demod,33,33,34] K2(E,F,[],[Q,R],[],[P],[],[]). given clause #73: (wt=15) 101 [hyper,91,5,demod,33,34] K2(E,D,[],[R],[Q],[P],[],[]). ** KEPT (pick-wt=14): 118 [hyper,101,17,demod,30,32,31,30,31] H(D,[Q],[P],[],[R],[],[]). given clause #74: (wt=14) 118 [hyper,101,17,demod,30,32,31,30,31] H(D,[Q],[P],[],[R],[],[]). ** KEPT (pick-wt=15): 119 [hyper,118,3] K1(D,E,[R],[],[Q],[P],[],[]). ** KEPT (pick-wt=15): 120 [hyper,118,2] K1(D,B,[R],[P],[Q],[],[],[]). given clause #75: (wt=15) 102 [hyper,92,5,demod,33,34] K2(E,F,[],[R],[Q],[P],[],[]). given clause #76: (wt=15) 104 [hyper,103,3] K1(D,E,[R],[P],[],[],[Q],[]). given clause #77: (wt=15) 105 [hyper,103,2] K1(D,B,[R],[],[],[Q],[P],[]). ** KEPT (pick-wt=15): 121 [hyper,105,5,demod,33,34] K2(D,B,[],[R],[],[Q],[P],[]). given clause #78: (wt=15) 107 [hyper,106,15,demod,30,32,32,31,30,31] K1(F,E,[P,R],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 122 [hyper,107,6,eval,demod,33,34] K2(F,E,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=15): 123 [hyper,107,5,demod,33,33,34] K2(F,E,[],[P,R],[],[],[Q],[]). given clause #79: (wt=15) 108 [hyper,106,14,demod,30,32,32,31,30,32,31] K1(F,C,[P,R],[Q],[],[],[],[]). ** KEPT (pick-wt=15): 124 [hyper,108,6,eval,demod,33,34] K2(F,C,[P],[R,Q],[],[],[],[]). ** KEPT (pick-wt=15): 125 [hyper,108,5,demod,33,33,34] K2(F,C,[],[P,R,Q],[],[],[],[]). given clause #80: (wt=15) 110 [hyper,109,15,demod,30,32,31,30,31] K1(F,E,[R],[],[P],[],[Q],[]). ** KEPT (pick-wt=15): 126 [hyper,110,5,demod,33,34] K2(F,E,[],[R],[P],[],[Q],[]). given clause #81: (wt=15) 111 [hyper,109,14,demod,30,32,31,30,32,31] K1(F,C,[R],[Q],[P],[],[],[]). ** KEPT (pick-wt=15): 127 [hyper,111,5,demod,33,34] K2(F,C,[],[R,Q],[P],[],[],[]). given clause #82: (wt=15) 113 [hyper,112,3] K1(D,E,[Q,R],[],[],[P],[],[]). ** KEPT (pick-wt=15): 128 [hyper,113,6,eval,demod,33,34] K2(D,E,[Q],[R],[],[P],[],[]). ** KEPT (pick-wt=15): 129 [hyper,113,5,demod,33,33,34] K2(D,E,[],[Q,R],[],[P],[],[]). given clause #83: (wt=15) 114 [hyper,112,2] K1(D,B,[Q,R],[P],[],[],[],[]). ** KEPT (pick-wt=15): 130 [hyper,114,6,eval,demod,33,34] K2(D,B,[Q],[R,P],[],[],[],[]). ** KEPT (pick-wt=15): 131 [hyper,114,5,demod,33,33,34] K2(D,B,[],[Q,R,P],[],[],[],[]). given clause #84: (wt=15) 116 [hyper,115,15,demod,30,32,31,30,32,31] K1(F,E,[R],[Q],[],[P],[],[]). given clause #85: (wt=15) 117 [hyper,115,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[P],[],[Q]). ** KEPT (pick-wt=15): 132 [hyper,117,5,demod,33,34] K2(F,C,[],[R],[],[P],[],[Q]). given clause #86: (wt=15) 119 [hyper,118,3] K1(D,E,[R],[],[Q],[P],[],[]). ** KEPT (pick-wt=15): 133 [hyper,119,5,demod,33,34] K2(D,E,[],[R],[Q],[P],[],[]). given clause #87: (wt=15) 120 [hyper,118,2] K1(D,B,[R],[P],[Q],[],[],[]). ** KEPT (pick-wt=15): 134 [hyper,120,5,demod,33,34] K2(D,B,[],[R,P],[Q],[],[],[]). given clause #88: (wt=15) 121 [hyper,105,5,demod,33,34] K2(D,B,[],[R],[],[Q],[P],[]). ** KEPT (pick-wt=14): 135 [hyper,121,9] H(B,[],[R],[Q],[],[P],[]). given clause #89: (wt=14) 135 [hyper,121,9] H(B,[],[R],[Q],[],[P],[]). ** KEPT (pick-wt=15): 136 [hyper,135,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[Q],[P],[]). given clause #90: (wt=15) 122 [hyper,107,6,eval,demod,33,34] K2(F,E,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=14): 137 [hyper,122,19,demod,30,32,31,30,32,31] H(E,[],[],[Q],[],[R],[P]). given clause #91: (wt=14) 137 [hyper,122,19,demod,30,32,31,30,32,31] H(E,[],[],[Q],[],[R],[P]). ** KEPT (pick-wt=15): 138 [hyper,137,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[],[Q],[P]). ** KEPT (pick-wt=15): 139 [hyper,137,4] K1(E,F,[R],[P],[],[],[Q],[]). given clause #92: (wt=15) 123 [hyper,107,5,demod,33,33,34] K2(F,E,[],[P,R],[],[],[Q],[]). given clause #93: (wt=15) 124 [hyper,108,6,eval,demod,33,34] K2(F,C,[P],[R,Q],[],[],[],[]). ** KEPT (pick-wt=14): 140 [hyper,124,18,demod,30,32,32,31,30,32,31] H(C,[],[],[Q,R],[],[],[P]). given clause #94: (wt=14) 140 [hyper,124,18,demod,30,32,32,31,30,32,31] H(C,[],[],[Q,R],[],[],[P]). ** KEPT (pick-wt=14): 141 [hyper,140,24,eval] H(C,[Q],[],[R],[],[],[P]). ** KEPT (pick-wt=15): 142 [hyper,140,1] K1(C,F,[Q,R],[P],[],[],[],[]). given clause #95: (wt=14) 141 [hyper,140,24,eval] H(C,[Q],[],[R],[],[],[P]). ** KEPT (pick-wt=15): 143 [hyper,141,1] K1(C,F,[R],[P],[Q],[],[],[]). given clause #96: (wt=15) 125 [hyper,108,5,demod,33,33,34] K2(F,C,[],[P,R,Q],[],[],[],[]). ** KEPT (pick-wt=14): 144 [hyper,125,18,demod,30,32,32,32,31,30,31] H(C,[],[],[Q,R,P],[],[],[]). given clause #97: (wt=14) 144 [hyper,125,18,demod,30,32,32,32,31,30,31] H(C,[],[],[Q,R,P],[],[],[]). ** KEPT (pick-wt=14): 145 [hyper,144,24,eval] H(C,[Q],[],[R,P],[],[],[]). ** KEPT (pick-wt=15): 146 [hyper,144,1] K1(C,F,[Q,R,P],[],[],[],[],[]). given clause #98: (wt=14) 145 [hyper,144,24,eval] H(C,[Q],[],[R,P],[],[],[]). ** KEPT (pick-wt=15): 147 [hyper,145,1] K1(C,F,[R,P],[],[Q],[],[],[]). given clause #99: (wt=15) 126 [hyper,110,5,demod,33,34] K2(F,E,[],[R],[P],[],[Q],[]). given clause #100: (wt=15) 127 [hyper,111,5,demod,33,34] K2(F,C,[],[R,Q],[P],[],[],[]). ** KEPT (pick-wt=14): 148 [hyper,127,18,demod,30,32,32,31,30,31] H(C,[P],[],[Q,R],[],[],[]). given clause #101: (wt=14) 148 [hyper,127,18,demod,30,32,32,31,30,31] H(C,[P],[],[Q,R],[],[],[]). ** KEPT (pick-wt=14): 149 [hyper,148,25] H(C,[],[],[P,Q,R],[],[],[]). ** KEPT (pick-wt=15): 150 [hyper,148,1] K1(C,F,[Q,R],[],[P],[],[],[]). given clause #102: (wt=14) 149 [hyper,148,25] H(C,[],[],[P,Q,R],[],[],[]). ** KEPT (pick-wt=15): 151 [hyper,149,1] K1(C,F,[P,Q,R],[],[],[],[],[]). given clause #103: (wt=15) 128 [hyper,113,6,eval,demod,33,34] K2(D,E,[Q],[R],[],[P],[],[]). ** KEPT (pick-wt=14): 152 [hyper,128,10] H(E,[],[P],[],[Q],[R],[]). given clause #104: (wt=14) 152 [hyper,128,10] H(E,[],[P],[],[Q],[R],[]). ** KEPT (pick-wt=15): 153 [hyper,152,13,demod,30,32,31,30,32,31] K1(E,D,[R],[Q],[],[P],[],[]). ** KEPT (pick-wt=15): 154 [hyper,152,4] K1(E,F,[R],[],[],[P],[],[Q]). given clause #105: (wt=15) 129 [hyper,113,5,demod,33,33,34] K2(D,E,[],[Q,R],[],[P],[],[]). given clause #106: (wt=15) 130 [hyper,114,6,eval,demod,33,34] K2(D,B,[Q],[R,P],[],[],[],[]). ** KEPT (pick-wt=14): 155 [hyper,130,9] H(B,[],[R,P],[],[Q],[],[]). given clause #107: (wt=14) 155 [hyper,130,9] H(B,[],[R,P],[],[Q],[],[]). ** KEPT (pick-wt=14): 156 [hyper,155,20] H(B,[P],[R],[],[Q],[],[]). ** KEPT (pick-wt=15): 157 [hyper,155,12,demod,30,32,32,31,30,32,31] K1(B,D,[P,R],[Q],[],[],[],[]). given clause #108: (wt=14) 156 [hyper,155,20] H(B,[P],[R],[],[Q],[],[]). ** KEPT (pick-wt=15): 158 [hyper,156,12,demod,30,32,31,30,32,31] K1(B,D,[R],[Q],[P],[],[],[]). given clause #109: (wt=15) 131 [hyper,114,5,demod,33,33,34] K2(D,B,[],[Q,R,P],[],[],[],[]). ** KEPT (pick-wt=14): 159 [hyper,131,9] H(B,[],[Q,R,P],[],[],[],[]). given clause #110: (wt=14) 159 [hyper,131,9] H(B,[],[Q,R,P],[],[],[],[]). ** KEPT (pick-wt=14): 160 [hyper,159,22] H(B,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=15): 161 [hyper,159,12,demod,30,32,32,32,31,30,31] K1(B,D,[P,R,Q],[],[],[],[],[]). given clause #111: (wt=14) 160 [hyper,159,22] H(B,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=15): 162 [hyper,160,12,demod,30,32,32,31,30,31] K1(B,D,[R,Q],[],[P],[],[],[]). given clause #112: (wt=15) 132 [hyper,117,5,demod,33,34] K2(F,C,[],[R],[],[P],[],[Q]). ** KEPT (pick-wt=14): 163 [hyper,132,18,demod,30,32,31,30,31] H(C,[],[P],[R],[],[Q],[]). given clause #113: (wt=14) 163 [hyper,132,18,demod,30,32,31,30,31] H(C,[],[P],[R],[],[Q],[]). ** KEPT (pick-wt=15): 164 [hyper,163,1] K1(C,F,[R],[],[],[P],[],[Q]). given clause #114: (wt=15) 133 [hyper,119,5,demod,33,34] K2(D,E,[],[R],[Q],[P],[],[]). given clause #115: (wt=15) 134 [hyper,120,5,demod,33,34] K2(D,B,[],[R,P],[Q],[],[],[]). ** KEPT (pick-wt=14): 165 [hyper,134,9] H(B,[Q],[R,P],[],[],[],[]). given clause #116: (wt=14) 165 [hyper,134,9] H(B,[Q],[R,P],[],[],[],[]). ** KEPT (pick-wt=14): 166 [hyper,165,23,demod,33,33,34] H(B,[],[R,P,Q],[],[],[],[]). ** KEPT (pick-wt=15): 167 [hyper,165,12,demod,30,32,32,31,30,31] K1(B,D,[P,R],[],[Q],[],[],[]). given clause #117: (wt=14) 166 [hyper,165,23,demod,33,33,34] H(B,[],[R,P,Q],[],[],[],[]). ** KEPT (pick-wt=15): 168 [hyper,166,12,demod,30,32,32,32,31,30,31] K1(B,D,[Q,P,R],[],[],[],[],[]). given clause #118: (wt=15) 136 [hyper,135,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[Q],[P],[]). ** KEPT (pick-wt=15): 169 [hyper,136,5,demod,33,34] K2(B,D,[],[R],[],[Q],[P],[]). given clause #119: (wt=15) 138 [hyper,137,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[],[Q],[P]). ** KEPT (pick-wt=15): 170 [hyper,138,5,demod,33,34] K2(E,D,[],[R],[],[],[Q],[P]). given clause #120: (wt=15) 139 [hyper,137,4] K1(E,F,[R],[P],[],[],[Q],[]). given clause #121: (wt=15) 142 [hyper,140,1] K1(C,F,[Q,R],[P],[],[],[],[]). ** KEPT (pick-wt=15): 171 [hyper,142,6,eval,demod,33,34] K2(C,F,[Q],[R,P],[],[],[],[]). ** KEPT (pick-wt=15): 172 [hyper,142,5,demod,33,33,34] K2(C,F,[],[Q,R,P],[],[],[],[]). given clause #122: (wt=15) 143 [hyper,141,1] K1(C,F,[R],[P],[Q],[],[],[]). ** KEPT (pick-wt=15): 173 [hyper,143,5,demod,33,34] K2(C,F,[],[R,P],[Q],[],[],[]). given clause #123: (wt=15) 146 [hyper,144,1] K1(C,F,[Q,R,P],[],[],[],[],[]). given clause #124: (wt=15) 147 [hyper,145,1] K1(C,F,[R,P],[],[Q],[],[],[]). given clause #125: (wt=15) 150 [hyper,148,1] K1(C,F,[Q,R],[],[P],[],[],[]). ** KEPT (pick-wt=15): 174 [hyper,150,6,eval,demod,33,34] K2(C,F,[Q],[R],[P],[],[],[]). ** KEPT (pick-wt=15): 175 [hyper,150,5,demod,33,33,34] K2(C,F,[],[Q,R],[P],[],[],[]). given clause #126: (wt=15) 151 [hyper,149,1] K1(C,F,[P,Q,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 176 [hyper,151,7] K2(C,F,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=15): 177 [hyper,151,6,eval,demod,33,33,34] K2(C,F,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=15): 178 [hyper,151,5,demod,33,33,33,34] K2(C,F,[],[P,Q,R],[],[],[],[]). given clause #127: (wt=15) 153 [hyper,152,13,demod,30,32,31,30,32,31] K1(E,D,[R],[Q],[],[P],[],[]). given clause #128: (wt=15) 154 [hyper,152,4] K1(E,F,[R],[],[],[P],[],[Q]). ** KEPT (pick-wt=15): 179 [hyper,154,5,demod,33,34] K2(E,F,[],[R],[],[P],[],[Q]). given clause #129: (wt=15) 157 [hyper,155,12,demod,30,32,32,31,30,32,31] K1(B,D,[P,R],[Q],[],[],[],[]). ** KEPT (pick-wt=15): 180 [hyper,157,6,eval,demod,33,34] K2(B,D,[P],[R,Q],[],[],[],[]). ** KEPT (pick-wt=15): 181 [hyper,157,5,demod,33,33,34] K2(B,D,[],[P,R,Q],[],[],[],[]). given clause #130: (wt=15) 158 [hyper,156,12,demod,30,32,31,30,32,31] K1(B,D,[R],[Q],[P],[],[],[]). ** KEPT (pick-wt=15): 182 [hyper,158,5,demod,33,34] K2(B,D,[],[R,Q],[P],[],[],[]). given clause #131: (wt=15) 161 [hyper,159,12,demod,30,32,32,32,31,30,31] K1(B,D,[P,R,Q],[],[],[],[],[]). given clause #132: (wt=15) 162 [hyper,160,12,demod,30,32,32,31,30,31] K1(B,D,[R,Q],[],[P],[],[],[]). given clause #133: (wt=15) 164 [hyper,163,1] K1(C,F,[R],[],[],[P],[],[Q]). ** KEPT (pick-wt=15): 183 [hyper,164,5,demod,33,34] K2(C,F,[],[R],[],[P],[],[Q]). given clause #134: (wt=15) 167 [hyper,165,12,demod,30,32,32,31,30,31] K1(B,D,[P,R],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 184 [hyper,167,6,eval,demod,33,34] K2(B,D,[P],[R],[Q],[],[],[]). ** KEPT (pick-wt=15): 185 [hyper,167,5,demod,33,33,34] K2(B,D,[],[P,R],[Q],[],[],[]). given clause #135: (wt=15) 168 [hyper,166,12,demod,30,32,32,32,31,30,31] K1(B,D,[Q,P,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 186 [hyper,168,7] K2(B,D,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=15): 187 [hyper,168,6,eval,demod,33,33,34] K2(B,D,[Q],[P,R],[],[],[],[]). ** KEPT (pick-wt=15): 188 [hyper,168,5,demod,33,33,33,34] K2(B,D,[],[Q,P,R],[],[],[],[]). given clause #136: (wt=15) 169 [hyper,136,5,demod,33,34] K2(B,D,[],[R],[],[Q],[P],[]). given clause #137: (wt=15) 170 [hyper,138,5,demod,33,34] K2(E,D,[],[R],[],[],[Q],[P]). ** KEPT (pick-wt=14): 189 [hyper,170,17,demod,30,32,31,30,31] H(D,[],[],[Q],[R],[],[P]). given clause #138: (wt=14) 189 [hyper,170,17,demod,30,32,31,30,31] H(D,[],[],[Q],[R],[],[P]). ** KEPT (pick-wt=15): 190 [hyper,189,3] K1(D,E,[R],[],[],[],[Q],[P]). ** KEPT (pick-wt=15): 191 [hyper,189,2] K1(D,B,[R],[],[],[Q],[],[P]). given clause #139: (wt=15) 171 [hyper,142,6,eval,demod,33,34] K2(C,F,[Q],[R,P],[],[],[],[]). given clause #140: (wt=15) 172 [hyper,142,5,demod,33,33,34] K2(C,F,[],[Q,R,P],[],[],[],[]). ** KEPT (pick-wt=14): 192 [hyper,172,8] H(F,[],[],[],[],[],[Q,R,P]). given clause #141: (wt=14) 192 [hyper,172,8] H(F,[],[],[],[],[],[Q,R,P]). ** KEPT (pick-wt=15): 193 [hyper,192,15,demod,30,32,32,32,31,30,31] K1(F,E,[P,R,Q],[],[],[],[],[]). ** KEPT (pick-wt=15): 194 [hyper,192,14,demod,30,32,32,32,31,30,31] K1(F,C,[P,R,Q],[],[],[],[],[]). given clause #142: (wt=15) 173 [hyper,143,5,demod,33,34] K2(C,F,[],[R,P],[Q],[],[],[]). ** KEPT (pick-wt=14): 195 [hyper,173,8] H(F,[Q],[],[],[],[],[R,P]). given clause #143: (wt=14) 195 [hyper,173,8] H(F,[Q],[],[],[],[],[R,P]). ** KEPT (pick-wt=15): 196 [hyper,195,15,demod,30,32,32,31,30,31] K1(F,E,[P,R],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 197 [hyper,195,14,demod,30,32,32,31,30,31] K1(F,C,[P,R],[],[Q],[],[],[]). given clause #144: (wt=15) 174 [hyper,150,6,eval,demod,33,34] K2(C,F,[Q],[R],[P],[],[],[]). given clause #145: (wt=15) 175 [hyper,150,5,demod,33,33,34] K2(C,F,[],[Q,R],[P],[],[],[]). ** KEPT (pick-wt=14): 198 [hyper,175,8] H(F,[P],[],[],[],[],[Q,R]). given clause #146: (wt=14) 198 [hyper,175,8] H(F,[P],[],[],[],[],[Q,R]). ** KEPT (pick-wt=15): 199 [hyper,198,15,demod,30,32,32,31,30,31] K1(F,E,[R,Q],[],[P],[],[],[]). ** KEPT (pick-wt=15): 200 [hyper,198,14,demod,30,32,32,31,30,31] K1(F,C,[R,Q],[],[P],[],[],[]). given clause #147: (wt=15) 176 [hyper,151,7] K2(C,F,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=14): 201 [hyper,176,8] H(F,[],[],[P,Q],[],[],[R]). given clause #148: (wt=14) 201 [hyper,176,8] H(F,[],[],[P,Q],[],[],[R]). ** KEPT (pick-wt=15): 202 [hyper,201,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 203 [hyper,201,14,demod,30,32,31,30,32,32,31] K1(F,C,[R],[Q,P],[],[],[],[]). given clause #149: (wt=15) 177 [hyper,151,6,eval,demod,33,33,34] K2(C,F,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=14): 204 [hyper,177,8] H(F,[],[],[P],[],[],[Q,R]). given clause #150: (wt=14) 204 [hyper,177,8] H(F,[],[],[P],[],[],[Q,R]). ** KEPT (pick-wt=15): 205 [hyper,204,15,demod,30,32,32,31,30,31] K1(F,E,[R,Q],[],[],[],[P],[]). ** KEPT (pick-wt=15): 206 [hyper,204,14,demod,30,32,32,31,30,32,31] K1(F,C,[R,Q],[P],[],[],[],[]). given clause #151: (wt=15) 178 [hyper,151,5,demod,33,33,33,34] K2(C,F,[],[P,Q,R],[],[],[],[]). ** KEPT (pick-wt=14): 207 [hyper,178,8] H(F,[],[],[],[],[],[P,Q,R]). given clause #152: (wt=14) 207 [hyper,178,8] H(F,[],[],[],[],[],[P,Q,R]). ** KEPT (pick-wt=15): 208 [hyper,207,15,demod,30,32,32,32,31,30,31] K1(F,E,[R,Q,P],[],[],[],[],[]). ** KEPT (pick-wt=15): 209 [hyper,207,14,demod,30,32,32,32,31,30,31] K1(F,C,[R,Q,P],[],[],[],[],[]). given clause #153: (wt=15) 179 [hyper,154,5,demod,33,34] K2(E,F,[],[R],[],[P],[],[Q]). ** KEPT (pick-wt=14): 210 [hyper,179,11] H(F,[],[P],[],[Q],[],[R]). given clause #154: (wt=14) 210 [hyper,179,11] H(F,[],[P],[],[Q],[],[R]). ** KEPT (pick-wt=15): 211 [hyper,210,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[P],[],[Q]). ** KEPT (pick-wt=15): 212 [hyper,210,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[P],[Q],[]). given clause #155: (wt=15) 180 [hyper,157,6,eval,demod,33,34] K2(B,D,[P],[R,Q],[],[],[],[]). given clause #156: (wt=15) 181 [hyper,157,5,demod,33,33,34] K2(B,D,[],[P,R,Q],[],[],[],[]). ** KEPT (pick-wt=14): 213 [hyper,181,16,demod,30,31,30,32,32,32,31] H(D,[],[],[],[Q,R,P],[],[]). given clause #157: (wt=14) 213 [hyper,181,16,demod,30,31,30,32,32,32,31] H(D,[],[],[],[Q,R,P],[],[]). ** KEPT (pick-wt=15): 214 [hyper,213,3] K1(D,E,[Q,R,P],[],[],[],[],[]). ** KEPT (pick-wt=15): 215 [hyper,213,2] K1(D,B,[Q,R,P],[],[],[],[],[]). given clause #158: (wt=15) 182 [hyper,158,5,demod,33,34] K2(B,D,[],[R,Q],[P],[],[],[]). ** KEPT (pick-wt=14): 216 [hyper,182,16,demod,30,31,30,32,32,31] H(D,[P],[],[],[Q,R],[],[]). given clause #159: (wt=14) 216 [hyper,182,16,demod,30,31,30,32,32,31] H(D,[P],[],[],[Q,R],[],[]). ** KEPT (pick-wt=15): 217 [hyper,216,3] K1(D,E,[Q,R],[],[P],[],[],[]). ** KEPT (pick-wt=15): 218 [hyper,216,2] K1(D,B,[Q,R],[],[P],[],[],[]). given clause #160: (wt=15) 183 [hyper,164,5,demod,33,34] K2(C,F,[],[R],[],[P],[],[Q]). given clause #161: (wt=15) 184 [hyper,167,6,eval,demod,33,34] K2(B,D,[P],[R],[Q],[],[],[]). given clause #162: (wt=15) 185 [hyper,167,5,demod,33,33,34] K2(B,D,[],[P,R],[Q],[],[],[]). ** KEPT (pick-wt=14): 219 [hyper,185,16,demod,30,31,30,32,32,31] H(D,[Q],[],[],[R,P],[],[]). given clause #163: (wt=14) 219 [hyper,185,16,demod,30,31,30,32,32,31] H(D,[Q],[],[],[R,P],[],[]). ** KEPT (pick-wt=15): 220 [hyper,219,3] K1(D,E,[R,P],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 221 [hyper,219,2] K1(D,B,[R,P],[],[Q],[],[],[]). given clause #164: (wt=15) 186 [hyper,168,7] K2(B,D,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=14): 222 [hyper,186,16,demod,30,32,32,31,30,32,31] H(D,[],[P,Q],[],[R],[],[]). given clause #165: (wt=14) 222 [hyper,186,16,demod,30,32,32,31,30,32,31] H(D,[],[P,Q],[],[R],[],[]). ** KEPT (pick-wt=15): 223 [hyper,222,3] K1(D,E,[R],[],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 224 [hyper,222,2] K1(D,B,[R],[P,Q],[],[],[],[]). given clause #166: (wt=15) 187 [hyper,168,6,eval,demod,33,33,34] K2(B,D,[Q],[P,R],[],[],[],[]). ** KEPT (pick-wt=14): 225 [hyper,187,16,demod,30,32,31,30,32,32,31] H(D,[],[Q],[],[R,P],[],[]). given clause #167: (wt=14) 225 [hyper,187,16,demod,30,32,31,30,32,32,31] H(D,[],[Q],[],[R,P],[],[]). ** KEPT (pick-wt=15): 226 [hyper,225,3] K1(D,E,[R,P],[],[],[Q],[],[]). ** KEPT (pick-wt=15): 227 [hyper,225,2] K1(D,B,[R,P],[Q],[],[],[],[]). given clause #168: (wt=15) 188 [hyper,168,5,demod,33,33,33,34] K2(B,D,[],[Q,P,R],[],[],[],[]). ** KEPT (pick-wt=14): 228 [hyper,188,16,demod,30,31,30,32,32,32,31] H(D,[],[],[],[R,P,Q],[],[]). given clause #169: (wt=14) 228 [hyper,188,16,demod,30,31,30,32,32,32,31] H(D,[],[],[],[R,P,Q],[],[]). ** KEPT (pick-wt=15): 229 [hyper,228,3] K1(D,E,[R,P,Q],[],[],[],[],[]). ** KEPT (pick-wt=15): 230 [hyper,228,2] K1(D,B,[R,P,Q],[],[],[],[],[]). given clause #170: (wt=15) 190 [hyper,189,3] K1(D,E,[R],[],[],[],[Q],[P]). ** KEPT (pick-wt=15): 231 [hyper,190,5,demod,33,34] K2(D,E,[],[R],[],[],[Q],[P]). given clause #171: (wt=15) 191 [hyper,189,2] K1(D,B,[R],[],[],[Q],[],[P]). ** KEPT (pick-wt=15): 232 [hyper,191,5,demod,33,34] K2(D,B,[],[R],[],[Q],[],[P]). given clause #172: (wt=15) 193 [hyper,192,15,demod,30,32,32,32,31,30,31] K1(F,E,[P,R,Q],[],[],[],[],[]). ** KEPT (pick-wt=15): 233 [hyper,193,6,eval,demod,33,33,34] K2(F,E,[P],[R,Q],[],[],[],[]). ** KEPT (pick-wt=15): 234 [hyper,193,5,demod,33,33,33,34] K2(F,E,[],[P,R,Q],[],[],[],[]). given clause #173: (wt=15) 194 [hyper,192,14,demod,30,32,32,32,31,30,31] K1(F,C,[P,R,Q],[],[],[],[],[]). given clause #174: (wt=15) 196 [hyper,195,15,demod,30,32,32,31,30,31] K1(F,E,[P,R],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 235 [hyper,196,6,eval,demod,33,34] K2(F,E,[P],[R],[Q],[],[],[]). ** KEPT (pick-wt=15): 236 [hyper,196,5,demod,33,33,34] K2(F,E,[],[P,R],[Q],[],[],[]). given clause #175: (wt=15) 197 [hyper,195,14,demod,30,32,32,31,30,31] K1(F,C,[P,R],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 237 [hyper,197,6,eval,demod,33,34] K2(F,C,[P],[R],[Q],[],[],[]). ** KEPT (pick-wt=15): 238 [hyper,197,5,demod,33,33,34] K2(F,C,[],[P,R],[Q],[],[],[]). given clause #176: (wt=15) 199 [hyper,198,15,demod,30,32,32,31,30,31] K1(F,E,[R,Q],[],[P],[],[],[]). ** KEPT (pick-wt=15): 239 [hyper,199,5,demod,33,33,34] K2(F,E,[],[R,Q],[P],[],[],[]). given clause #177: (wt=15) 200 [hyper,198,14,demod,30,32,32,31,30,31] K1(F,C,[R,Q],[],[P],[],[],[]). given clause #178: (wt=15) 202 [hyper,201,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 240 [hyper,202,5,demod,33,34] K2(F,E,[],[R],[],[],[P,Q],[]). given clause #179: (wt=15) 203 [hyper,201,14,demod,30,32,31,30,32,32,31] K1(F,C,[R],[Q,P],[],[],[],[]). ** KEPT (pick-wt=15): 241 [hyper,203,5,demod,33,34] K2(F,C,[],[R,Q,P],[],[],[],[]). given clause #180: (wt=15) 205 [hyper,204,15,demod,30,32,32,31,30,31] K1(F,E,[R,Q],[],[],[],[P],[]). ** KEPT (pick-wt=15): 242 [hyper,205,5,demod,33,33,34] K2(F,E,[],[R,Q],[],[],[P],[]). given clause #181: (wt=15) 206 [hyper,204,14,demod,30,32,32,31,30,32,31] K1(F,C,[R,Q],[P],[],[],[],[]). given clause #182: (wt=15) 208 [hyper,207,15,demod,30,32,32,32,31,30,31] K1(F,E,[R,Q,P],[],[],[],[],[]). ** KEPT (pick-wt=15): 243 [hyper,208,5,demod,33,33,33,34] K2(F,E,[],[R,Q,P],[],[],[],[]). given clause #183: (wt=15) 209 [hyper,207,14,demod,30,32,32,32,31,30,31] K1(F,C,[R,Q,P],[],[],[],[],[]). given clause #184: (wt=15) 211 [hyper,210,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[P],[],[Q]). ** KEPT (pick-wt=15): 244 [hyper,211,5,demod,33,34] K2(F,E,[],[R],[],[P],[],[Q]). given clause #185: (wt=15) 212 [hyper,210,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[P],[Q],[]). ** KEPT (pick-wt=15): 245 [hyper,212,5,demod,33,34] K2(F,C,[],[R],[],[P],[Q],[]). given clause #186: (wt=15) 214 [hyper,213,3] K1(D,E,[Q,R,P],[],[],[],[],[]). ** KEPT (pick-wt=15): 246 [hyper,214,6,eval,demod,33,33,34] K2(D,E,[Q],[R,P],[],[],[],[]). ** KEPT (pick-wt=15): 247 [hyper,214,5,demod,33,33,33,34] K2(D,E,[],[Q,R,P],[],[],[],[]). given clause #187: (wt=15) 215 [hyper,213,2] K1(D,B,[Q,R,P],[],[],[],[],[]). given clause #188: (wt=15) 217 [hyper,216,3] K1(D,E,[Q,R],[],[P],[],[],[]). ** KEPT (pick-wt=15): 248 [hyper,217,6,eval,demod,33,34] K2(D,E,[Q],[R],[P],[],[],[]). ** KEPT (pick-wt=15): 249 [hyper,217,5,demod,33,33,34] K2(D,E,[],[Q,R],[P],[],[],[]). given clause #189: (wt=15) 218 [hyper,216,2] K1(D,B,[Q,R],[],[P],[],[],[]). ** KEPT (pick-wt=15): 250 [hyper,218,6,eval,demod,33,34] K2(D,B,[Q],[R],[P],[],[],[]). ** KEPT (pick-wt=15): 251 [hyper,218,5,demod,33,33,34] K2(D,B,[],[Q,R],[P],[],[],[]). given clause #190: (wt=15) 220 [hyper,219,3] K1(D,E,[R,P],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 252 [hyper,220,5,demod,33,33,34] K2(D,E,[],[R,P],[Q],[],[],[]). given clause #191: (wt=15) 221 [hyper,219,2] K1(D,B,[R,P],[],[Q],[],[],[]). given clause #192: (wt=15) 223 [hyper,222,3] K1(D,E,[R],[],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 253 [hyper,223,5,demod,33,34] K2(D,E,[],[R],[],[P,Q],[],[]). given clause #193: (wt=15) 224 [hyper,222,2] K1(D,B,[R],[P,Q],[],[],[],[]). ** KEPT (pick-wt=15): 254 [hyper,224,5,demod,33,34] K2(D,B,[],[R,P,Q],[],[],[],[]). given clause #194: (wt=15) 226 [hyper,225,3] K1(D,E,[R,P],[],[],[Q],[],[]). ** KEPT (pick-wt=15): 255 [hyper,226,5,demod,33,33,34] K2(D,E,[],[R,P],[],[Q],[],[]). given clause #195: (wt=15) 227 [hyper,225,2] K1(D,B,[R,P],[Q],[],[],[],[]). given clause #196: (wt=15) 229 [hyper,228,3] K1(D,E,[R,P,Q],[],[],[],[],[]). ** KEPT (pick-wt=15): 256 [hyper,229,5,demod,33,33,33,34] K2(D,E,[],[R,P,Q],[],[],[],[]). given clause #197: (wt=15) 230 [hyper,228,2] K1(D,B,[R,P,Q],[],[],[],[],[]). given clause #198: (wt=15) 231 [hyper,190,5,demod,33,34] K2(D,E,[],[R],[],[],[Q],[P]). given clause #199: (wt=15) 232 [hyper,191,5,demod,33,34] K2(D,B,[],[R],[],[Q],[],[P]). ** KEPT (pick-wt=14): 257 [hyper,232,9] H(B,[],[R],[Q],[],[],[P]). given clause #200: (wt=14) 257 [hyper,232,9] H(B,[],[R],[Q],[],[],[P]). ** KEPT (pick-wt=15): 258 [hyper,257,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[Q],[],[P]). given clause #201: (wt=15) 233 [hyper,193,6,eval,demod,33,33,34] K2(F,E,[P],[R,Q],[],[],[],[]). ** KEPT (pick-wt=14): 259 [hyper,233,19,demod,30,32,32,31,30,32,31] H(E,[],[],[],[],[Q,R],[P]). given clause #202: (wt=14) 259 [hyper,233,19,demod,30,32,32,31,30,32,31] H(E,[],[],[],[],[Q,R],[P]). ** KEPT (pick-wt=15): 260 [hyper,259,13,demod,30,32,32,31,30,31] K1(E,D,[R,Q],[],[],[],[],[P]). ** KEPT (pick-wt=15): 261 [hyper,259,4] K1(E,F,[Q,R],[P],[],[],[],[]). given clause #203: (wt=15) 234 [hyper,193,5,demod,33,33,33,34] K2(F,E,[],[P,R,Q],[],[],[],[]). ** KEPT (pick-wt=14): 262 [hyper,234,19,demod,30,32,32,32,31,30,31] H(E,[],[],[],[],[Q,R,P],[]). given clause #204: (wt=14) 262 [hyper,234,19,demod,30,32,32,32,31,30,31] H(E,[],[],[],[],[Q,R,P],[]). ** KEPT (pick-wt=15): 263 [hyper,262,13,demod,30,32,32,32,31,30,31] K1(E,D,[P,R,Q],[],[],[],[],[]). ** KEPT (pick-wt=15): 264 [hyper,262,4] K1(E,F,[Q,R,P],[],[],[],[],[]). given clause #205: (wt=15) 235 [hyper,196,6,eval,demod,33,34] K2(F,E,[P],[R],[Q],[],[],[]). ** KEPT (pick-wt=14): 265 [hyper,235,19,demod,30,32,31,30,32,31] H(E,[Q],[],[],[],[R],[P]). given clause #206: (wt=14) 265 [hyper,235,19,demod,30,32,31,30,32,31] H(E,[Q],[],[],[],[R],[P]). ** KEPT (pick-wt=15): 266 [hyper,265,13,demod,30,32,31,30,31] K1(E,D,[R],[],[Q],[],[],[P]). ** KEPT (pick-wt=15): 267 [hyper,265,4] K1(E,F,[R],[P],[Q],[],[],[]). given clause #207: (wt=15) 236 [hyper,196,5,demod,33,33,34] K2(F,E,[],[P,R],[Q],[],[],[]). ** KEPT (pick-wt=14): 268 [hyper,236,19,demod,30,32,32,31,30,31] H(E,[Q],[],[],[],[R,P],[]). given clause #208: (wt=14) 268 [hyper,236,19,demod,30,32,32,31,30,31] H(E,[Q],[],[],[],[R,P],[]). ** KEPT (pick-wt=15): 269 [hyper,268,13,demod,30,32,32,31,30,31] K1(E,D,[P,R],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 270 [hyper,268,4] K1(E,F,[R,P],[],[Q],[],[],[]). given clause #209: (wt=15) 237 [hyper,197,6,eval,demod,33,34] K2(F,C,[P],[R],[Q],[],[],[]). given clause #210: (wt=15) 238 [hyper,197,5,demod,33,33,34] K2(F,C,[],[P,R],[Q],[],[],[]). given clause #211: (wt=15) 239 [hyper,199,5,demod,33,33,34] K2(F,E,[],[R,Q],[P],[],[],[]). ** KEPT (pick-wt=14): 271 [hyper,239,19,demod,30,32,32,31,30,31] H(E,[P],[],[],[],[Q,R],[]). given clause #212: (wt=14) 271 [hyper,239,19,demod,30,32,32,31,30,31] H(E,[P],[],[],[],[Q,R],[]). ** KEPT (pick-wt=15): 272 [hyper,271,13,demod,30,32,32,31,30,31] K1(E,D,[R,Q],[],[P],[],[],[]). ** KEPT (pick-wt=15): 273 [hyper,271,4] K1(E,F,[Q,R],[],[P],[],[],[]). given clause #213: (wt=15) 240 [hyper,202,5,demod,33,34] K2(F,E,[],[R],[],[],[P,Q],[]). ** KEPT (pick-wt=14): 274 [hyper,240,19,demod,30,32,31,30,31] H(E,[],[],[P,Q],[],[R],[]). given clause #214: (wt=14) 274 [hyper,240,19,demod,30,32,31,30,31] H(E,[],[],[P,Q],[],[R],[]). ** KEPT (pick-wt=15): 275 [hyper,274,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 276 [hyper,274,4] K1(E,F,[R],[],[],[],[P,Q],[]). given clause #215: (wt=15) 241 [hyper,203,5,demod,33,34] K2(F,C,[],[R,Q,P],[],[],[],[]). given clause #216: (wt=15) 242 [hyper,205,5,demod,33,33,34] K2(F,E,[],[R,Q],[],[],[P],[]). ** KEPT (pick-wt=14): 277 [hyper,242,19,demod,30,32,32,31,30,31] H(E,[],[],[P],[],[Q,R],[]). given clause #217: (wt=14) 277 [hyper,242,19,demod,30,32,32,31,30,31] H(E,[],[],[P],[],[Q,R],[]). ** KEPT (pick-wt=15): 278 [hyper,277,13,demod,30,32,32,31,30,31] K1(E,D,[R,Q],[],[],[],[P],[]). ** KEPT (pick-wt=15): 279 [hyper,277,4] K1(E,F,[Q,R],[],[],[],[P],[]). given clause #218: (wt=15) 243 [hyper,208,5,demod,33,33,33,34] K2(F,E,[],[R,Q,P],[],[],[],[]). ** KEPT (pick-wt=14): 280 [hyper,243,19,demod,30,32,32,32,31,30,31] H(E,[],[],[],[],[P,Q,R],[]). given clause #219: (wt=14) 280 [hyper,243,19,demod,30,32,32,32,31,30,31] H(E,[],[],[],[],[P,Q,R],[]). ** KEPT (pick-wt=15): 281 [hyper,280,13,demod,30,32,32,32,31,30,31] K1(E,D,[R,Q,P],[],[],[],[],[]). ** KEPT (pick-wt=15): 282 [hyper,280,4] K1(E,F,[P,Q,R],[],[],[],[],[]). given clause #220: (wt=15) 244 [hyper,211,5,demod,33,34] K2(F,E,[],[R],[],[P],[],[Q]). given clause #221: (wt=15) 245 [hyper,212,5,demod,33,34] K2(F,C,[],[R],[],[P],[Q],[]). ** KEPT (pick-wt=14): 283 [hyper,245,18,demod,30,32,31,30,31] H(C,[],[P],[R],[Q],[],[]). given clause #222: (wt=14) 283 [hyper,245,18,demod,30,32,31,30,31] H(C,[],[P],[R],[Q],[],[]). ** KEPT (pick-wt=15): 284 [hyper,283,1] K1(C,F,[R],[],[],[P],[Q],[]). given clause #223: (wt=15) 246 [hyper,214,6,eval,demod,33,33,34] K2(D,E,[Q],[R,P],[],[],[],[]). ** KEPT (pick-wt=14): 285 [hyper,246,10] H(E,[],[],[],[Q],[R,P],[]). given clause #224: (wt=14) 285 [hyper,246,10] H(E,[],[],[],[Q],[R,P],[]). ** KEPT (pick-wt=15): 286 [hyper,285,13,demod,30,32,32,31,30,32,31] K1(E,D,[P,R],[Q],[],[],[],[]). ** KEPT (pick-wt=15): 287 [hyper,285,4] K1(E,F,[R,P],[],[],[],[],[Q]). given clause #225: (wt=15) 247 [hyper,214,5,demod,33,33,33,34] K2(D,E,[],[Q,R,P],[],[],[],[]). given clause #226: (wt=15) 248 [hyper,217,6,eval,demod,33,34] K2(D,E,[Q],[R],[P],[],[],[]). ** KEPT (pick-wt=14): 288 [hyper,248,10] H(E,[P],[],[],[Q],[R],[]). given clause #227: (wt=14) 288 [hyper,248,10] H(E,[P],[],[],[Q],[R],[]). ** KEPT (pick-wt=15): 289 [hyper,288,13,demod,30,32,31,30,32,31] K1(E,D,[R],[Q],[P],[],[],[]). ** KEPT (pick-wt=15): 290 [hyper,288,4] K1(E,F,[R],[],[P],[],[],[Q]). given clause #228: (wt=15) 249 [hyper,217,5,demod,33,33,34] K2(D,E,[],[Q,R],[P],[],[],[]). given clause #229: (wt=15) 250 [hyper,218,6,eval,demod,33,34] K2(D,B,[Q],[R],[P],[],[],[]). given clause #230: (wt=15) 251 [hyper,218,5,demod,33,33,34] K2(D,B,[],[Q,R],[P],[],[],[]). given clause #231: (wt=15) 252 [hyper,220,5,demod,33,33,34] K2(D,E,[],[R,P],[Q],[],[],[]). given clause #232: (wt=15) 253 [hyper,223,5,demod,33,34] K2(D,E,[],[R],[],[P,Q],[],[]). ** KEPT (pick-wt=14): 291 [hyper,253,10] H(E,[],[P,Q],[],[],[R],[]). given clause #233: (wt=14) 291 [hyper,253,10] H(E,[],[P,Q],[],[],[R],[]). ** KEPT (pick-wt=15): 292 [hyper,291,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 293 [hyper,291,4] K1(E,F,[R],[],[],[P,Q],[],[]). given clause #234: (wt=15) 254 [hyper,224,5,demod,33,34] K2(D,B,[],[R,P,Q],[],[],[],[]). given clause #235: (wt=15) 255 [hyper,226,5,demod,33,33,34] K2(D,E,[],[R,P],[],[Q],[],[]). ** KEPT (pick-wt=14): 294 [hyper,255,10] H(E,[],[Q],[],[],[R,P],[]). given clause #236: (wt=14) 294 [hyper,255,10] H(E,[],[Q],[],[],[R,P],[]). ** KEPT (pick-wt=15): 295 [hyper,294,13,demod,30,32,32,31,30,31] K1(E,D,[P,R],[],[],[Q],[],[]). ** KEPT (pick-wt=15): 296 [hyper,294,4] K1(E,F,[R,P],[],[],[Q],[],[]). given clause #237: (wt=15) 256 [hyper,229,5,demod,33,33,33,34] K2(D,E,[],[R,P,Q],[],[],[],[]). ** KEPT (pick-wt=14): 297 [hyper,256,10] H(E,[],[],[],[],[R,P,Q],[]). given clause #238: (wt=14) 297 [hyper,256,10] H(E,[],[],[],[],[R,P,Q],[]). ** KEPT (pick-wt=15): 298 [hyper,297,13,demod,30,32,32,32,31,30,31] K1(E,D,[Q,P,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 299 [hyper,297,4] K1(E,F,[R,P,Q],[],[],[],[],[]). given clause #239: (wt=15) 258 [hyper,257,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[Q],[],[P]). ** KEPT (pick-wt=15): 300 [hyper,258,5,demod,33,34] K2(B,D,[],[R],[],[Q],[],[P]). given clause #240: (wt=15) 260 [hyper,259,13,demod,30,32,32,31,30,31] K1(E,D,[R,Q],[],[],[],[],[P]). ** KEPT (pick-wt=15): 301 [hyper,260,5,demod,33,33,34] K2(E,D,[],[R,Q],[],[],[],[P]). given clause #241: (wt=15) 261 [hyper,259,4] K1(E,F,[Q,R],[P],[],[],[],[]). ** KEPT (pick-wt=15): 302 [hyper,261,6,eval,demod,33,34] K2(E,F,[Q],[R,P],[],[],[],[]). ** KEPT (pick-wt=15): 303 [hyper,261,5,demod,33,33,34] K2(E,F,[],[Q,R,P],[],[],[],[]). given clause #242: (wt=15) 263 [hyper,262,13,demod,30,32,32,32,31,30,31] K1(E,D,[P,R,Q],[],[],[],[],[]). ** KEPT (pick-wt=15): 304 [hyper,263,6,eval,demod,33,33,34] K2(E,D,[P],[R,Q],[],[],[],[]). ** KEPT (pick-wt=15): 305 [hyper,263,5,demod,33,33,33,34] K2(E,D,[],[P,R,Q],[],[],[],[]). given clause #243: (wt=15) 264 [hyper,262,4] K1(E,F,[Q,R,P],[],[],[],[],[]). given clause #244: (wt=15) 266 [hyper,265,13,demod,30,32,31,30,31] K1(E,D,[R],[],[Q],[],[],[P]). ** KEPT (pick-wt=15): 306 [hyper,266,5,demod,33,34] K2(E,D,[],[R],[Q],[],[],[P]). given clause #245: (wt=15) 267 [hyper,265,4] K1(E,F,[R],[P],[Q],[],[],[]). ** KEPT (pick-wt=15): 307 [hyper,267,5,demod,33,34] K2(E,F,[],[R,P],[Q],[],[],[]). given clause #246: (wt=15) 269 [hyper,268,13,demod,30,32,32,31,30,31] K1(E,D,[P,R],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 308 [hyper,269,6,eval,demod,33,34] K2(E,D,[P],[R],[Q],[],[],[]). ** KEPT (pick-wt=15): 309 [hyper,269,5,demod,33,33,34] K2(E,D,[],[P,R],[Q],[],[],[]). given clause #247: (wt=15) 270 [hyper,268,4] K1(E,F,[R,P],[],[Q],[],[],[]). given clause #248: (wt=15) 272 [hyper,271,13,demod,30,32,32,31,30,31] K1(E,D,[R,Q],[],[P],[],[],[]). ** KEPT (pick-wt=15): 310 [hyper,272,5,demod,33,33,34] K2(E,D,[],[R,Q],[P],[],[],[]). given clause #249: (wt=15) 273 [hyper,271,4] K1(E,F,[Q,R],[],[P],[],[],[]). ** KEPT (pick-wt=15): 311 [hyper,273,6,eval,demod,33,34] K2(E,F,[Q],[R],[P],[],[],[]). ** KEPT (pick-wt=15): 312 [hyper,273,5,demod,33,33,34] K2(E,F,[],[Q,R],[P],[],[],[]). given clause #250: (wt=15) 275 [hyper,274,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 313 [hyper,275,5,demod,33,34] K2(E,D,[],[R],[],[],[P,Q],[]). given clause #251: (wt=15) 276 [hyper,274,4] K1(E,F,[R],[],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 314 [hyper,276,5,demod,33,34] K2(E,F,[],[R],[],[],[P,Q],[]). given clause #252: (wt=15) 278 [hyper,277,13,demod,30,32,32,31,30,31] K1(E,D,[R,Q],[],[],[],[P],[]). ** KEPT (pick-wt=15): 315 [hyper,278,5,demod,33,33,34] K2(E,D,[],[R,Q],[],[],[P],[]). given clause #253: (wt=15) 279 [hyper,277,4] K1(E,F,[Q,R],[],[],[],[P],[]). ** KEPT (pick-wt=15): 316 [hyper,279,6,eval,demod,33,34] K2(E,F,[Q],[R],[],[],[P],[]). ** KEPT (pick-wt=15): 317 [hyper,279,5,demod,33,33,34] K2(E,F,[],[Q,R],[],[],[P],[]). given clause #254: (wt=15) 281 [hyper,280,13,demod,30,32,32,32,31,30,31] K1(E,D,[R,Q,P],[],[],[],[],[]). ** KEPT (pick-wt=15): 318 [hyper,281,5,demod,33,33,33,34] K2(E,D,[],[R,Q,P],[],[],[],[]). given clause #255: (wt=15) 282 [hyper,280,4] K1(E,F,[P,Q,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 319 [hyper,282,7] K2(E,F,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=15): 320 [hyper,282,6,eval,demod,33,33,34] K2(E,F,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=15): 321 [hyper,282,5,demod,33,33,33,34] K2(E,F,[],[P,Q,R],[],[],[],[]). given clause #256: (wt=15) 284 [hyper,283,1] K1(C,F,[R],[],[],[P],[Q],[]). ** KEPT (pick-wt=15): 322 [hyper,284,5,demod,33,34] K2(C,F,[],[R],[],[P],[Q],[]). given clause #257: (wt=15) 286 [hyper,285,13,demod,30,32,32,31,30,32,31] K1(E,D,[P,R],[Q],[],[],[],[]). given clause #258: (wt=15) 287 [hyper,285,4] K1(E,F,[R,P],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 323 [hyper,287,5,demod,33,33,34] K2(E,F,[],[R,P],[],[],[],[Q]). given clause #259: (wt=15) 289 [hyper,288,13,demod,30,32,31,30,32,31] K1(E,D,[R],[Q],[P],[],[],[]). given clause #260: (wt=15) 290 [hyper,288,4] K1(E,F,[R],[],[P],[],[],[Q]). ** KEPT (pick-wt=15): 324 [hyper,290,5,demod,33,34] K2(E,F,[],[R],[P],[],[],[Q]). given clause #261: (wt=15) 292 [hyper,291,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 325 [hyper,292,5,demod,33,34] K2(E,D,[],[R],[],[P,Q],[],[]). given clause #262: (wt=15) 293 [hyper,291,4] K1(E,F,[R],[],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 326 [hyper,293,5,demod,33,34] K2(E,F,[],[R],[],[P,Q],[],[]). given clause #263: (wt=15) 295 [hyper,294,13,demod,30,32,32,31,30,31] K1(E,D,[P,R],[],[],[Q],[],[]). ** KEPT (pick-wt=15): 327 [hyper,295,6,eval,demod,33,34] K2(E,D,[P],[R],[],[Q],[],[]). ** KEPT (pick-wt=15): 328 [hyper,295,5,demod,33,33,34] K2(E,D,[],[P,R],[],[Q],[],[]). given clause #264: (wt=15) 296 [hyper,294,4] K1(E,F,[R,P],[],[],[Q],[],[]). ** KEPT (pick-wt=15): 329 [hyper,296,5,demod,33,33,34] K2(E,F,[],[R,P],[],[Q],[],[]). given clause #265: (wt=15) 298 [hyper,297,13,demod,30,32,32,32,31,30,31] K1(E,D,[Q,P,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 330 [hyper,298,7] K2(E,D,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=15): 331 [hyper,298,6,eval,demod,33,33,34] K2(E,D,[Q],[P,R],[],[],[],[]). ** KEPT (pick-wt=15): 332 [hyper,298,5,demod,33,33,33,34] K2(E,D,[],[Q,P,R],[],[],[],[]). given clause #266: (wt=15) 299 [hyper,297,4] K1(E,F,[R,P,Q],[],[],[],[],[]). ** KEPT (pick-wt=15): 333 [hyper,299,5,demod,33,33,33,34] K2(E,F,[],[R,P,Q],[],[],[],[]). given clause #267: (wt=15) 300 [hyper,258,5,demod,33,34] K2(B,D,[],[R],[],[Q],[],[P]). given clause #268: (wt=15) 301 [hyper,260,5,demod,33,33,34] K2(E,D,[],[R,Q],[],[],[],[P]). ** KEPT (pick-wt=14): 334 [hyper,301,17,demod,30,32,32,31,30,31] H(D,[],[],[],[Q,R],[],[P]). given clause #269: (wt=14) 334 [hyper,301,17,demod,30,32,32,31,30,31] H(D,[],[],[],[Q,R],[],[P]). ** KEPT (pick-wt=15): 335 [hyper,334,3] K1(D,E,[Q,R],[],[],[],[],[P]). ** KEPT (pick-wt=15): 336 [hyper,334,2] K1(D,B,[Q,R],[],[],[],[],[P]). given clause #270: (wt=15) 302 [hyper,261,6,eval,demod,33,34] K2(E,F,[Q],[R,P],[],[],[],[]). ** KEPT (pick-wt=14): 337 [hyper,302,11] H(F,[],[],[],[],[Q],[R,P]). given clause #271: (wt=14) 337 [hyper,302,11] H(F,[],[],[],[],[Q],[R,P]). ** KEPT (pick-wt=15): 338 [hyper,337,15,demod,30,32,32,31,30,32,31] K1(F,E,[P,R],[Q],[],[],[],[]). ** KEPT (pick-wt=15): 339 [hyper,337,14,demod,30,32,32,31,30,31] K1(F,C,[P,R],[],[],[],[],[Q]). given clause #272: (wt=15) 303 [hyper,261,5,demod,33,33,34] K2(E,F,[],[Q,R,P],[],[],[],[]). given clause #273: (wt=15) 304 [hyper,263,6,eval,demod,33,33,34] K2(E,D,[P],[R,Q],[],[],[],[]). ** KEPT (pick-wt=14): 340 [hyper,304,17,demod,30,32,32,31,30,32,31] H(D,[],[],[],[Q,R],[P],[]). given clause #274: (wt=14) 340 [hyper,304,17,demod,30,32,32,31,30,32,31] H(D,[],[],[],[Q,R],[P],[]). ** KEPT (pick-wt=15): 341 [hyper,340,3] K1(D,E,[Q,R],[P],[],[],[],[]). ** KEPT (pick-wt=15): 342 [hyper,340,2] K1(D,B,[Q,R],[],[],[],[P],[]). given clause #275: (wt=15) 305 [hyper,263,5,demod,33,33,33,34] K2(E,D,[],[P,R,Q],[],[],[],[]). given clause #276: (wt=15) 306 [hyper,266,5,demod,33,34] K2(E,D,[],[R],[Q],[],[],[P]). ** KEPT (pick-wt=14): 343 [hyper,306,17,demod,30,32,31,30,31] H(D,[Q],[],[],[R],[],[P]). given clause #277: (wt=14) 343 [hyper,306,17,demod,30,32,31,30,31] H(D,[Q],[],[],[R],[],[P]). ** KEPT (pick-wt=15): 344 [hyper,343,3] K1(D,E,[R],[],[Q],[],[],[P]). ** KEPT (pick-wt=15): 345 [hyper,343,2] K1(D,B,[R],[],[Q],[],[],[P]). given clause #278: (wt=15) 307 [hyper,267,5,demod,33,34] K2(E,F,[],[R,P],[Q],[],[],[]). given clause #279: (wt=15) 308 [hyper,269,6,eval,demod,33,34] K2(E,D,[P],[R],[Q],[],[],[]). ** KEPT (pick-wt=14): 346 [hyper,308,17,demod,30,32,31,30,32,31] H(D,[Q],[],[],[R],[P],[]). given clause #280: (wt=14) 346 [hyper,308,17,demod,30,32,31,30,32,31] H(D,[Q],[],[],[R],[P],[]). ** KEPT (pick-wt=15): 347 [hyper,346,3] K1(D,E,[R],[P],[Q],[],[],[]). ** KEPT (pick-wt=15): 348 [hyper,346,2] K1(D,B,[R],[],[Q],[],[P],[]). given clause #281: (wt=15) 309 [hyper,269,5,demod,33,33,34] K2(E,D,[],[P,R],[Q],[],[],[]). given clause #282: (wt=15) 310 [hyper,272,5,demod,33,33,34] K2(E,D,[],[R,Q],[P],[],[],[]). given clause #283: (wt=15) 311 [hyper,273,6,eval,demod,33,34] K2(E,F,[Q],[R],[P],[],[],[]). ** KEPT (pick-wt=14): 349 [hyper,311,11] H(F,[P],[],[],[],[Q],[R]). given clause #284: (wt=14) 349 [hyper,311,11] H(F,[P],[],[],[],[Q],[R]). ** KEPT (pick-wt=15): 350 [hyper,349,15,demod,30,32,31,30,32,31] K1(F,E,[R],[Q],[P],[],[],[]). ** KEPT (pick-wt=15): 351 [hyper,349,14,demod,30,32,31,30,31] K1(F,C,[R],[],[P],[],[],[Q]). given clause #285: (wt=15) 312 [hyper,273,5,demod,33,33,34] K2(E,F,[],[Q,R],[P],[],[],[]). given clause #286: (wt=15) 313 [hyper,275,5,demod,33,34] K2(E,D,[],[R],[],[],[P,Q],[]). ** KEPT (pick-wt=14): 352 [hyper,313,17,demod,30,32,31,30,31] H(D,[],[],[P,Q],[R],[],[]). given clause #287: (wt=14) 352 [hyper,313,17,demod,30,32,31,30,31] H(D,[],[],[P,Q],[R],[],[]). ** KEPT (pick-wt=15): 353 [hyper,352,3] K1(D,E,[R],[],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 354 [hyper,352,2] K1(D,B,[R],[],[],[P,Q],[],[]). given clause #288: (wt=15) 314 [hyper,276,5,demod,33,34] K2(E,F,[],[R],[],[],[P,Q],[]). given clause #289: (wt=15) 315 [hyper,278,5,demod,33,33,34] K2(E,D,[],[R,Q],[],[],[P],[]). ** KEPT (pick-wt=14): 355 [hyper,315,17,demod,30,32,32,31,30,31] H(D,[],[],[P],[Q,R],[],[]). given clause #290: (wt=14) 355 [hyper,315,17,demod,30,32,32,31,30,31] H(D,[],[],[P],[Q,R],[],[]). ** KEPT (pick-wt=15): 356 [hyper,355,3] K1(D,E,[Q,R],[],[],[],[P],[]). ** KEPT (pick-wt=15): 357 [hyper,355,2] K1(D,B,[Q,R],[],[],[P],[],[]). given clause #291: (wt=15) 316 [hyper,279,6,eval,demod,33,34] K2(E,F,[Q],[R],[],[],[P],[]). ** KEPT (pick-wt=14): 358 [hyper,316,11] H(F,[],[],[P],[],[Q],[R]). given clause #292: (wt=14) 358 [hyper,316,11] H(F,[],[],[P],[],[Q],[R]). ** KEPT (pick-wt=15): 359 [hyper,358,15,demod,30,32,31,30,32,31] K1(F,E,[R],[Q],[],[],[P],[]). ** KEPT (pick-wt=15): 360 [hyper,358,14,demod,30,32,31,30,32,31] K1(F,C,[R],[P],[],[],[],[Q]). given clause #293: (wt=15) 317 [hyper,279,5,demod,33,33,34] K2(E,F,[],[Q,R],[],[],[P],[]). given clause #294: (wt=15) 318 [hyper,281,5,demod,33,33,33,34] K2(E,D,[],[R,Q,P],[],[],[],[]). ** KEPT (pick-wt=14): 361 [hyper,318,17,demod,30,32,32,32,31,30,31] H(D,[],[],[],[P,Q,R],[],[]). given clause #295: (wt=14) 361 [hyper,318,17,demod,30,32,32,32,31,30,31] H(D,[],[],[],[P,Q,R],[],[]). ** KEPT (pick-wt=15): 362 [hyper,361,3] K1(D,E,[P,Q,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 363 [hyper,361,2] K1(D,B,[P,Q,R],[],[],[],[],[]). given clause #296: (wt=15) 319 [hyper,282,7] K2(E,F,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=14): 364 [hyper,319,11] H(F,[],[],[],[],[P,Q],[R]). given clause #297: (wt=14) 364 [hyper,319,11] H(F,[],[],[],[],[P,Q],[R]). ** KEPT (pick-wt=15): 365 [hyper,364,15,demod,30,32,31,30,32,32,31] K1(F,E,[R],[Q,P],[],[],[],[]). ** KEPT (pick-wt=15): 366 [hyper,364,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[],[],[P,Q]). given clause #298: (wt=15) 320 [hyper,282,6,eval,demod,33,33,34] K2(E,F,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=14): 367 [hyper,320,11] H(F,[],[],[],[],[P],[Q,R]). given clause #299: (wt=14) 367 [hyper,320,11] H(F,[],[],[],[],[P],[Q,R]). ** KEPT (pick-wt=15): 368 [hyper,367,15,demod,30,32,32,31,30,32,31] K1(F,E,[R,Q],[P],[],[],[],[]). ** KEPT (pick-wt=15): 369 [hyper,367,14,demod,30,32,32,31,30,31] K1(F,C,[R,Q],[],[],[],[],[P]). given clause #300: (wt=15) 321 [hyper,282,5,demod,33,33,33,34] K2(E,F,[],[P,Q,R],[],[],[],[]). given clause #301: (wt=15) 322 [hyper,284,5,demod,33,34] K2(C,F,[],[R],[],[P],[Q],[]). given clause #302: (wt=15) 323 [hyper,287,5,demod,33,33,34] K2(E,F,[],[R,P],[],[],[],[Q]). ** KEPT (pick-wt=14): 370 [hyper,323,11] H(F,[],[],[],[Q],[],[R,P]). given clause #303: (wt=14) 370 [hyper,323,11] H(F,[],[],[],[Q],[],[R,P]). ** KEPT (pick-wt=15): 371 [hyper,370,15,demod,30,32,32,31,30,31] K1(F,E,[P,R],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 372 [hyper,370,14,demod,30,32,32,31,30,31] K1(F,C,[P,R],[],[],[],[Q],[]). given clause #304: (wt=15) 324 [hyper,290,5,demod,33,34] K2(E,F,[],[R],[P],[],[],[Q]). ** KEPT (pick-wt=14): 373 [hyper,324,11] H(F,[P],[],[],[Q],[],[R]). given clause #305: (wt=14) 373 [hyper,324,11] H(F,[P],[],[],[Q],[],[R]). ** KEPT (pick-wt=15): 374 [hyper,373,15,demod,30,32,31,30,31] K1(F,E,[R],[],[P],[],[],[Q]). ** KEPT (pick-wt=15): 375 [hyper,373,14,demod,30,32,31,30,31] K1(F,C,[R],[],[P],[],[Q],[]). given clause #306: (wt=15) 325 [hyper,292,5,demod,33,34] K2(E,D,[],[R],[],[P,Q],[],[]). given clause #307: (wt=15) 326 [hyper,293,5,demod,33,34] K2(E,F,[],[R],[],[P,Q],[],[]). ** KEPT (pick-wt=14): 376 [hyper,326,11] H(F,[],[P,Q],[],[],[],[R]). given clause #308: (wt=14) 376 [hyper,326,11] H(F,[],[P,Q],[],[],[],[R]). ** KEPT (pick-wt=15): 377 [hyper,376,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 378 [hyper,376,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[P,Q],[],[]). given clause #309: (wt=15) 327 [hyper,295,6,eval,demod,33,34] K2(E,D,[P],[R],[],[Q],[],[]). ** KEPT (pick-wt=14): 379 [hyper,327,17,demod,30,32,31,30,32,31] H(D,[],[Q],[],[R],[P],[]). given clause #310: (wt=14) 379 [hyper,327,17,demod,30,32,31,30,32,31] H(D,[],[Q],[],[R],[P],[]). ** KEPT (pick-wt=15): 380 [hyper,379,3] K1(D,E,[R],[P],[],[Q],[],[]). ** KEPT (pick-wt=15): 381 [hyper,379,2] K1(D,B,[R],[Q],[],[],[P],[]). given clause #311: (wt=15) 328 [hyper,295,5,demod,33,33,34] K2(E,D,[],[P,R],[],[Q],[],[]). given clause #312: (wt=15) 329 [hyper,296,5,demod,33,33,34] K2(E,F,[],[R,P],[],[Q],[],[]). ** KEPT (pick-wt=14): 382 [hyper,329,11] H(F,[],[Q],[],[],[],[R,P]). given clause #313: (wt=14) 382 [hyper,329,11] H(F,[],[Q],[],[],[],[R,P]). ** KEPT (pick-wt=15): 383 [hyper,382,15,demod,30,32,32,31,30,31] K1(F,E,[P,R],[],[],[Q],[],[]). ** KEPT (pick-wt=15): 384 [hyper,382,14,demod,30,32,32,31,30,31] K1(F,C,[P,R],[],[],[Q],[],[]). given clause #314: (wt=15) 330 [hyper,298,7] K2(E,D,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=14): 385 [hyper,330,17,demod,30,32,31,30,32,32,31] H(D,[],[],[],[R],[P,Q],[]). given clause #315: (wt=14) 385 [hyper,330,17,demod,30,32,31,30,32,32,31] H(D,[],[],[],[R],[P,Q],[]). ** KEPT (pick-wt=15): 386 [hyper,385,3] K1(D,E,[R],[P,Q],[],[],[],[]). ** KEPT (pick-wt=15): 387 [hyper,385,2] K1(D,B,[R],[],[],[],[P,Q],[]). given clause #316: (wt=15) 331 [hyper,298,6,eval,demod,33,33,34] K2(E,D,[Q],[P,R],[],[],[],[]). ** KEPT (pick-wt=14): 388 [hyper,331,17,demod,30,32,32,31,30,32,31] H(D,[],[],[],[R,P],[Q],[]). given clause #317: (wt=14) 388 [hyper,331,17,demod,30,32,32,31,30,32,31] H(D,[],[],[],[R,P],[Q],[]). ** KEPT (pick-wt=15): 389 [hyper,388,3] K1(D,E,[R,P],[Q],[],[],[],[]). ** KEPT (pick-wt=15): 390 [hyper,388,2] K1(D,B,[R,P],[],[],[],[Q],[]). given clause #318: (wt=15) 332 [hyper,298,5,demod,33,33,33,34] K2(E,D,[],[Q,P,R],[],[],[],[]). given clause #319: (wt=15) 333 [hyper,299,5,demod,33,33,33,34] K2(E,F,[],[R,P,Q],[],[],[],[]). ** KEPT (pick-wt=14): 391 [hyper,333,11] H(F,[],[],[],[],[],[R,P,Q]). given clause #320: (wt=14) 391 [hyper,333,11] H(F,[],[],[],[],[],[R,P,Q]). ** KEPT (pick-wt=15): 392 [hyper,391,15,demod,30,32,32,32,31,30,31] K1(F,E,[Q,P,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 393 [hyper,391,14,demod,30,32,32,32,31,30,31] K1(F,C,[Q,P,R],[],[],[],[],[]). given clause #321: (wt=15) 335 [hyper,334,3] K1(D,E,[Q,R],[],[],[],[],[P]). ** KEPT (pick-wt=15): 394 [hyper,335,6,eval,demod,33,34] K2(D,E,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=15): 395 [hyper,335,5,demod,33,33,34] K2(D,E,[],[Q,R],[],[],[],[P]). given clause #322: (wt=15) 336 [hyper,334,2] K1(D,B,[Q,R],[],[],[],[],[P]). ** KEPT (pick-wt=15): 396 [hyper,336,6,eval,demod,33,34] K2(D,B,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=15): 397 [hyper,336,5,demod,33,33,34] K2(D,B,[],[Q,R],[],[],[],[P]). given clause #323: (wt=15) 338 [hyper,337,15,demod,30,32,32,31,30,32,31] K1(F,E,[P,R],[Q],[],[],[],[]). given clause #324: (wt=15) 339 [hyper,337,14,demod,30,32,32,31,30,31] K1(F,C,[P,R],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 398 [hyper,339,6,eval,demod,33,34] K2(F,C,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=15): 399 [hyper,339,5,demod,33,33,34] K2(F,C,[],[P,R],[],[],[],[Q]). given clause #325: (wt=15) 341 [hyper,340,3] K1(D,E,[Q,R],[P],[],[],[],[]). given clause #326: (wt=15) 342 [hyper,340,2] K1(D,B,[Q,R],[],[],[],[P],[]). ** KEPT (pick-wt=15): 400 [hyper,342,6,eval,demod,33,34] K2(D,B,[Q],[R],[],[],[P],[]). ** KEPT (pick-wt=15): 401 [hyper,342,5,demod,33,33,34] K2(D,B,[],[Q,R],[],[],[P],[]). given clause #327: (wt=15) 344 [hyper,343,3] K1(D,E,[R],[],[Q],[],[],[P]). ** KEPT (pick-wt=15): 402 [hyper,344,5,demod,33,34] K2(D,E,[],[R],[Q],[],[],[P]). given clause #328: (wt=15) 345 [hyper,343,2] K1(D,B,[R],[],[Q],[],[],[P]). ** KEPT (pick-wt=15): 403 [hyper,345,5,demod,33,34] K2(D,B,[],[R],[Q],[],[],[P]). given clause #329: (wt=15) 347 [hyper,346,3] K1(D,E,[R],[P],[Q],[],[],[]). given clause #330: (wt=15) 348 [hyper,346,2] K1(D,B,[R],[],[Q],[],[P],[]). ** KEPT (pick-wt=15): 404 [hyper,348,5,demod,33,34] K2(D,B,[],[R],[Q],[],[P],[]). given clause #331: (wt=15) 350 [hyper,349,15,demod,30,32,31,30,32,31] K1(F,E,[R],[Q],[P],[],[],[]). given clause #332: (wt=15) 351 [hyper,349,14,demod,30,32,31,30,31] K1(F,C,[R],[],[P],[],[],[Q]). ** KEPT (pick-wt=15): 405 [hyper,351,5,demod,33,34] K2(F,C,[],[R],[P],[],[],[Q]). given clause #333: (wt=15) 353 [hyper,352,3] K1(D,E,[R],[],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 406 [hyper,353,5,demod,33,34] K2(D,E,[],[R],[],[],[P,Q],[]). given clause #334: (wt=15) 354 [hyper,352,2] K1(D,B,[R],[],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 407 [hyper,354,5,demod,33,34] K2(D,B,[],[R],[],[P,Q],[],[]). given clause #335: (wt=15) 356 [hyper,355,3] K1(D,E,[Q,R],[],[],[],[P],[]). ** KEPT (pick-wt=15): 408 [hyper,356,6,eval,demod,33,34] K2(D,E,[Q],[R],[],[],[P],[]). ** KEPT (pick-wt=15): 409 [hyper,356,5,demod,33,33,34] K2(D,E,[],[Q,R],[],[],[P],[]). given clause #336: (wt=15) 357 [hyper,355,2] K1(D,B,[Q,R],[],[],[P],[],[]). ** KEPT (pick-wt=15): 410 [hyper,357,6,eval,demod,33,34] K2(D,B,[Q],[R],[],[P],[],[]). ** KEPT (pick-wt=15): 411 [hyper,357,5,demod,33,33,34] K2(D,B,[],[Q,R],[],[P],[],[]). given clause #337: (wt=15) 359 [hyper,358,15,demod,30,32,31,30,32,31] K1(F,E,[R],[Q],[],[],[P],[]). given clause #338: (wt=15) 360 [hyper,358,14,demod,30,32,31,30,32,31] K1(F,C,[R],[P],[],[],[],[Q]). ** KEPT (pick-wt=15): 412 [hyper,360,5,demod,33,34] K2(F,C,[],[R,P],[],[],[],[Q]). given clause #339: (wt=15) 362 [hyper,361,3] K1(D,E,[P,Q,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 413 [hyper,362,7] K2(D,E,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=15): 414 [hyper,362,6,eval,demod,33,33,34] K2(D,E,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=15): 415 [hyper,362,5,demod,33,33,33,34] K2(D,E,[],[P,Q,R],[],[],[],[]). given clause #340: (wt=15) 363 [hyper,361,2] K1(D,B,[P,Q,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 416 [hyper,363,7] K2(D,B,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=15): 417 [hyper,363,6,eval,demod,33,33,34] K2(D,B,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=15): 418 [hyper,363,5,demod,33,33,33,34] K2(D,B,[],[P,Q,R],[],[],[],[]). given clause #341: (wt=15) 365 [hyper,364,15,demod,30,32,31,30,32,32,31] K1(F,E,[R],[Q,P],[],[],[],[]). given clause #342: (wt=15) 366 [hyper,364,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 419 [hyper,366,5,demod,33,34] K2(F,C,[],[R],[],[],[],[P,Q]). given clause #343: (wt=15) 368 [hyper,367,15,demod,30,32,32,31,30,32,31] K1(F,E,[R,Q],[P],[],[],[],[]). given clause #344: (wt=15) 369 [hyper,367,14,demod,30,32,32,31,30,31] K1(F,C,[R,Q],[],[],[],[],[P]). ** KEPT (pick-wt=15): 420 [hyper,369,5,demod,33,33,34] K2(F,C,[],[R,Q],[],[],[],[P]). given clause #345: (wt=15) 371 [hyper,370,15,demod,30,32,32,31,30,31] K1(F,E,[P,R],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 421 [hyper,371,6,eval,demod,33,34] K2(F,E,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=15): 422 [hyper,371,5,demod,33,33,34] K2(F,E,[],[P,R],[],[],[],[Q]). given clause #346: (wt=15) 372 [hyper,370,14,demod,30,32,32,31,30,31] K1(F,C,[P,R],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 423 [hyper,372,6,eval,demod,33,34] K2(F,C,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=15): 424 [hyper,372,5,demod,33,33,34] K2(F,C,[],[P,R],[],[],[Q],[]). given clause #347: (wt=15) 374 [hyper,373,15,demod,30,32,31,30,31] K1(F,E,[R],[],[P],[],[],[Q]). ** KEPT (pick-wt=15): 425 [hyper,374,5,demod,33,34] K2(F,E,[],[R],[P],[],[],[Q]). given clause #348: (wt=15) 375 [hyper,373,14,demod,30,32,31,30,31] K1(F,C,[R],[],[P],[],[Q],[]). ** KEPT (pick-wt=15): 426 [hyper,375,5,demod,33,34] K2(F,C,[],[R],[P],[],[Q],[]). given clause #349: (wt=15) 377 [hyper,376,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 427 [hyper,377,5,demod,33,34] K2(F,E,[],[R],[],[P,Q],[],[]). given clause #350: (wt=15) 378 [hyper,376,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 428 [hyper,378,5,demod,33,34] K2(F,C,[],[R],[],[P,Q],[],[]). given clause #351: (wt=15) 380 [hyper,379,3] K1(D,E,[R],[P],[],[Q],[],[]). given clause #352: (wt=15) 381 [hyper,379,2] K1(D,B,[R],[Q],[],[],[P],[]). ** KEPT (pick-wt=15): 429 [hyper,381,5,demod,33,34] K2(D,B,[],[R,Q],[],[],[P],[]). given clause #353: (wt=15) 383 [hyper,382,15,demod,30,32,32,31,30,31] K1(F,E,[P,R],[],[],[Q],[],[]). ** KEPT (pick-wt=15): 430 [hyper,383,6,eval,demod,33,34] K2(F,E,[P],[R],[],[Q],[],[]). ** KEPT (pick-wt=15): 431 [hyper,383,5,demod,33,33,34] K2(F,E,[],[P,R],[],[Q],[],[]). given clause #354: (wt=15) 384 [hyper,382,14,demod,30,32,32,31,30,31] K1(F,C,[P,R],[],[],[Q],[],[]). ** KEPT (pick-wt=15): 432 [hyper,384,6,eval,demod,33,34] K2(F,C,[P],[R],[],[Q],[],[]). ** KEPT (pick-wt=15): 433 [hyper,384,5,demod,33,33,34] K2(F,C,[],[P,R],[],[Q],[],[]). given clause #355: (wt=15) 386 [hyper,385,3] K1(D,E,[R],[P,Q],[],[],[],[]). given clause #356: (wt=15) 387 [hyper,385,2] K1(D,B,[R],[],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 434 [hyper,387,5,demod,33,34] K2(D,B,[],[R],[],[],[P,Q],[]). given clause #357: (wt=15) 389 [hyper,388,3] K1(D,E,[R,P],[Q],[],[],[],[]). given clause #358: (wt=15) 390 [hyper,388,2] K1(D,B,[R,P],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 435 [hyper,390,5,demod,33,33,34] K2(D,B,[],[R,P],[],[],[Q],[]). given clause #359: (wt=15) 392 [hyper,391,15,demod,30,32,32,32,31,30,31] K1(F,E,[Q,P,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 436 [hyper,392,7] K2(F,E,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=15): 437 [hyper,392,6,eval,demod,33,33,34] K2(F,E,[Q],[P,R],[],[],[],[]). ** KEPT (pick-wt=15): 438 [hyper,392,5,demod,33,33,33,34] K2(F,E,[],[Q,P,R],[],[],[],[]). given clause #360: (wt=15) 393 [hyper,391,14,demod,30,32,32,32,31,30,31] K1(F,C,[Q,P,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 439 [hyper,393,7] K2(F,C,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=15): 440 [hyper,393,6,eval,demod,33,33,34] K2(F,C,[Q],[P,R],[],[],[],[]). ** KEPT (pick-wt=15): 441 [hyper,393,5,demod,33,33,33,34] K2(F,C,[],[Q,P,R],[],[],[],[]). given clause #361: (wt=15) 394 [hyper,335,6,eval,demod,33,34] K2(D,E,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=14): 442 [hyper,394,10] H(E,[],[],[],[Q],[R],[P]). given clause #362: (wt=14) 442 [hyper,394,10] H(E,[],[],[],[Q],[R],[P]). ** KEPT (pick-wt=15): 443 [hyper,442,13,demod,30,32,31,30,32,31] K1(E,D,[R],[Q],[],[],[],[P]). ** KEPT (pick-wt=15): 444 [hyper,442,4] K1(E,F,[R],[P],[],[],[],[Q]). given clause #363: (wt=15) 395 [hyper,335,5,demod,33,33,34] K2(D,E,[],[Q,R],[],[],[],[P]). given clause #364: (wt=15) 396 [hyper,336,6,eval,demod,33,34] K2(D,B,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=14): 445 [hyper,396,9] H(B,[],[R],[],[Q],[],[P]). given clause #365: (wt=14) 445 [hyper,396,9] H(B,[],[R],[],[Q],[],[P]). ** KEPT (pick-wt=15): 446 [hyper,445,12,demod,30,32,31,30,32,31] K1(B,D,[R],[Q],[],[],[],[P]). given clause #366: (wt=15) 397 [hyper,336,5,demod,33,33,34] K2(D,B,[],[Q,R],[],[],[],[P]). ** KEPT (pick-wt=14): 447 [hyper,397,9] H(B,[],[Q,R],[],[],[],[P]). given clause #367: (wt=14) 447 [hyper,397,9] H(B,[],[Q,R],[],[],[],[P]). ** KEPT (pick-wt=15): 448 [hyper,447,12,demod,30,32,32,31,30,31] K1(B,D,[R,Q],[],[],[],[],[P]). given clause #368: (wt=15) 398 [hyper,339,6,eval,demod,33,34] K2(F,C,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=14): 449 [hyper,398,18,demod,30,32,31,30,32,31] H(C,[],[],[R],[],[Q],[P]). given clause #369: (wt=14) 449 [hyper,398,18,demod,30,32,31,30,32,31] H(C,[],[],[R],[],[Q],[P]). ** KEPT (pick-wt=15): 450 [hyper,449,1] K1(C,F,[R],[P],[],[],[],[Q]). given clause #370: (wt=15) 399 [hyper,339,5,demod,33,33,34] K2(F,C,[],[P,R],[],[],[],[Q]). ** KEPT (pick-wt=14): 451 [hyper,399,18,demod,30,32,32,31,30,31] H(C,[],[],[R,P],[],[Q],[]). given clause #371: (wt=14) 451 [hyper,399,18,demod,30,32,32,31,30,31] H(C,[],[],[R,P],[],[Q],[]). ** KEPT (pick-wt=15): 452 [hyper,451,1] K1(C,F,[R,P],[],[],[],[],[Q]). given clause #372: (wt=15) 400 [hyper,342,6,eval,demod,33,34] K2(D,B,[Q],[R],[],[],[P],[]). ** KEPT (pick-wt=14): 453 [hyper,400,9] H(B,[],[R],[],[Q],[P],[]). given clause #373: (wt=14) 453 [hyper,400,9] H(B,[],[R],[],[Q],[P],[]). ** KEPT (pick-wt=15): 454 [hyper,453,12,demod,30,32,31,30,32,31] K1(B,D,[R],[Q],[],[],[P],[]). given clause #374: (wt=15) 401 [hyper,342,5,demod,33,33,34] K2(D,B,[],[Q,R],[],[],[P],[]). ** KEPT (pick-wt=14): 455 [hyper,401,9] H(B,[],[Q,R],[],[],[P],[]). given clause #375: (wt=14) 455 [hyper,401,9] H(B,[],[Q,R],[],[],[P],[]). ** KEPT (pick-wt=15): 456 [hyper,455,12,demod,30,32,32,31,30,31] K1(B,D,[R,Q],[],[],[],[P],[]). given clause #376: (wt=15) 402 [hyper,344,5,demod,33,34] K2(D,E,[],[R],[Q],[],[],[P]). given clause #377: (wt=15) 403 [hyper,345,5,demod,33,34] K2(D,B,[],[R],[Q],[],[],[P]). ** KEPT (pick-wt=14): 457 [hyper,403,9] H(B,[Q],[R],[],[],[],[P]). given clause #378: (wt=14) 457 [hyper,403,9] H(B,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=14): 458 [hyper,457,23,demod,33,34] H(B,[],[R,Q],[],[],[],[P]). ** KEPT (pick-wt=15): 459 [hyper,457,12,demod,30,32,31,30,31] K1(B,D,[R],[],[Q],[],[],[P]). given clause #379: (wt=14) 458 [hyper,457,23,demod,33,34] H(B,[],[R,Q],[],[],[],[P]). ** KEPT (pick-wt=15): 460 [hyper,458,12,demod,30,32,32,31,30,31] K1(B,D,[Q,R],[],[],[],[],[P]). given clause #380: (wt=15) 404 [hyper,348,5,demod,33,34] K2(D,B,[],[R],[Q],[],[P],[]). ** KEPT (pick-wt=14): 461 [hyper,404,9] H(B,[Q],[R],[],[],[P],[]). given clause #381: (wt=14) 461 [hyper,404,9] H(B,[Q],[R],[],[],[P],[]). ** KEPT (pick-wt=14): 462 [hyper,461,23,demod,33,34] H(B,[],[R,Q],[],[],[P],[]). ** KEPT (pick-wt=15): 463 [hyper,461,12,demod,30,32,31,30,31] K1(B,D,[R],[],[Q],[],[P],[]). given clause #382: (wt=14) 462 [hyper,461,23,demod,33,34] H(B,[],[R,Q],[],[],[P],[]). ** KEPT (pick-wt=15): 464 [hyper,462,12,demod,30,32,32,31,30,31] K1(B,D,[Q,R],[],[],[],[P],[]). given clause #383: (wt=15) 405 [hyper,351,5,demod,33,34] K2(F,C,[],[R],[P],[],[],[Q]). ** KEPT (pick-wt=14): 465 [hyper,405,18,demod,30,32,31,30,31] H(C,[P],[],[R],[],[Q],[]). given clause #384: (wt=14) 465 [hyper,405,18,demod,30,32,31,30,31] H(C,[P],[],[R],[],[Q],[]). ** KEPT (pick-wt=14): 466 [hyper,465,25] H(C,[],[],[P,R],[],[Q],[]). ** KEPT (pick-wt=15): 467 [hyper,465,1] K1(C,F,[R],[],[P],[],[],[Q]). given clause #385: (wt=14) 466 [hyper,465,25] H(C,[],[],[P,R],[],[Q],[]). ** KEPT (pick-wt=15): 468 [hyper,466,1] K1(C,F,[P,R],[],[],[],[],[Q]). given clause #386: (wt=15) 406 [hyper,353,5,demod,33,34] K2(D,E,[],[R],[],[],[P,Q],[]). given clause #387: (wt=15) 407 [hyper,354,5,demod,33,34] K2(D,B,[],[R],[],[P,Q],[],[]). ** KEPT (pick-wt=14): 469 [hyper,407,9] H(B,[],[R],[P,Q],[],[],[]). given clause #388: (wt=14) 469 [hyper,407,9] H(B,[],[R],[P,Q],[],[],[]). ** KEPT (pick-wt=15): 470 [hyper,469,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[P,Q],[],[]). given clause #389: (wt=15) 408 [hyper,356,6,eval,demod,33,34] K2(D,E,[Q],[R],[],[],[P],[]). ** KEPT (pick-wt=14): 471 [hyper,408,10] H(E,[],[],[P],[Q],[R],[]). given clause #390: (wt=14) 471 [hyper,408,10] H(E,[],[],[P],[Q],[R],[]). ** KEPT (pick-wt=15): 472 [hyper,471,13,demod,30,32,31,30,32,31] K1(E,D,[R],[Q],[],[],[P],[]). ** KEPT (pick-wt=15): 473 [hyper,471,4] K1(E,F,[R],[],[],[],[P],[Q]). given clause #391: (wt=15) 409 [hyper,356,5,demod,33,33,34] K2(D,E,[],[Q,R],[],[],[P],[]). given clause #392: (wt=15) 410 [hyper,357,6,eval,demod,33,34] K2(D,B,[Q],[R],[],[P],[],[]). ** KEPT (pick-wt=14): 474 [hyper,410,9] H(B,[],[R],[P],[Q],[],[]). given clause #393: (wt=14) 474 [hyper,410,9] H(B,[],[R],[P],[Q],[],[]). ** KEPT (pick-wt=15): 475 [hyper,474,12,demod,30,32,31,30,32,31] K1(B,D,[R],[Q],[],[P],[],[]). given clause #394: (wt=15) 411 [hyper,357,5,demod,33,33,34] K2(D,B,[],[Q,R],[],[P],[],[]). ** KEPT (pick-wt=14): 476 [hyper,411,9] H(B,[],[Q,R],[P],[],[],[]). given clause #395: (wt=14) 476 [hyper,411,9] H(B,[],[Q,R],[P],[],[],[]). ** KEPT (pick-wt=15): 477 [hyper,476,12,demod,30,32,32,31,30,31] K1(B,D,[R,Q],[],[],[P],[],[]). given clause #396: (wt=15) 412 [hyper,360,5,demod,33,34] K2(F,C,[],[R,P],[],[],[],[Q]). given clause #397: (wt=15) 413 [hyper,362,7] K2(D,E,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=14): 478 [hyper,413,10] H(E,[],[],[],[P,Q],[R],[]). given clause #398: (wt=14) 478 [hyper,413,10] H(E,[],[],[],[P,Q],[R],[]). ** KEPT (pick-wt=15): 479 [hyper,478,13,demod,30,32,31,30,32,32,31] K1(E,D,[R],[Q,P],[],[],[],[]). ** KEPT (pick-wt=15): 480 [hyper,478,4] K1(E,F,[R],[],[],[],[],[P,Q]). given clause #399: (wt=15) 414 [hyper,362,6,eval,demod,33,33,34] K2(D,E,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=14): 481 [hyper,414,10] H(E,[],[],[],[P],[Q,R],[]). given clause #400: (wt=14) 481 [hyper,414,10] H(E,[],[],[],[P],[Q,R],[]). ** KEPT (pick-wt=15): 482 [hyper,481,13,demod,30,32,32,31,30,32,31] K1(E,D,[R,Q],[P],[],[],[],[]). ** KEPT (pick-wt=15): 483 [hyper,481,4] K1(E,F,[Q,R],[],[],[],[],[P]). given clause #401: (wt=15) 415 [hyper,362,5,demod,33,33,33,34] K2(D,E,[],[P,Q,R],[],[],[],[]). given clause #402: (wt=15) 416 [hyper,363,7] K2(D,B,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=14): 484 [hyper,416,9] H(B,[],[R],[],[P,Q],[],[]). given clause #403: (wt=14) 484 [hyper,416,9] H(B,[],[R],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 485 [hyper,484,12,demod,30,32,31,30,32,32,31] K1(B,D,[R],[Q,P],[],[],[],[]). given clause #404: (wt=15) 417 [hyper,363,6,eval,demod,33,33,34] K2(D,B,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=14): 486 [hyper,417,9] H(B,[],[Q,R],[],[P],[],[]). given clause #405: (wt=14) 486 [hyper,417,9] H(B,[],[Q,R],[],[P],[],[]). ** KEPT (pick-wt=15): 487 [hyper,486,12,demod,30,32,32,31,30,32,31] K1(B,D,[R,Q],[P],[],[],[],[]). given clause #406: (wt=15) 418 [hyper,363,5,demod,33,33,33,34] K2(D,B,[],[P,Q,R],[],[],[],[]). ** KEPT (pick-wt=14): 488 [hyper,418,9] H(B,[],[P,Q,R],[],[],[],[]). given clause #407: (wt=14) 488 [hyper,418,9] H(B,[],[P,Q,R],[],[],[],[]). ** KEPT (pick-wt=15): 489 [hyper,488,12,demod,30,32,32,32,31,30,31] K1(B,D,[R,Q,P],[],[],[],[],[]). given clause #408: (wt=15) 419 [hyper,366,5,demod,33,34] K2(F,C,[],[R],[],[],[],[P,Q]). ** KEPT (pick-wt=14): 490 [hyper,419,18,demod,30,32,31,30,31] H(C,[],[],[R],[],[P,Q],[]). given clause #409: (wt=14) 490 [hyper,419,18,demod,30,32,31,30,31] H(C,[],[],[R],[],[P,Q],[]). ** KEPT (pick-wt=15): 491 [hyper,490,1] K1(C,F,[R],[],[],[],[],[P,Q]). given clause #410: (wt=15) 420 [hyper,369,5,demod,33,33,34] K2(F,C,[],[R,Q],[],[],[],[P]). ** KEPT (pick-wt=14): 492 [hyper,420,18,demod,30,32,32,31,30,31] H(C,[],[],[Q,R],[],[P],[]). given clause #411: (wt=14) 492 [hyper,420,18,demod,30,32,32,31,30,31] H(C,[],[],[Q,R],[],[P],[]). ** KEPT (pick-wt=14): 493 [hyper,492,24,eval] H(C,[Q],[],[R],[],[P],[]). ** KEPT (pick-wt=15): 494 [hyper,492,1] K1(C,F,[Q,R],[],[],[],[],[P]). given clause #412: (wt=14) 493 [hyper,492,24,eval] H(C,[Q],[],[R],[],[P],[]). ** KEPT (pick-wt=15): 495 [hyper,493,1] K1(C,F,[R],[],[Q],[],[],[P]). given clause #413: (wt=15) 421 [hyper,371,6,eval,demod,33,34] K2(F,E,[P],[R],[],[],[],[Q]). given clause #414: (wt=15) 422 [hyper,371,5,demod,33,33,34] K2(F,E,[],[P,R],[],[],[],[Q]). given clause #415: (wt=15) 423 [hyper,372,6,eval,demod,33,34] K2(F,C,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=14): 496 [hyper,423,18,demod,30,32,31,30,32,31] H(C,[],[],[R],[Q],[],[P]). given clause #416: (wt=14) 496 [hyper,423,18,demod,30,32,31,30,32,31] H(C,[],[],[R],[Q],[],[P]). ** KEPT (pick-wt=15): 497 [hyper,496,1] K1(C,F,[R],[P],[],[],[Q],[]). given clause #417: (wt=15) 424 [hyper,372,5,demod,33,33,34] K2(F,C,[],[P,R],[],[],[Q],[]). ** KEPT (pick-wt=14): 498 [hyper,424,18,demod,30,32,32,31,30,31] H(C,[],[],[R,P],[Q],[],[]). given clause #418: (wt=14) 498 [hyper,424,18,demod,30,32,32,31,30,31] H(C,[],[],[R,P],[Q],[],[]). ** KEPT (pick-wt=15): 499 [hyper,498,1] K1(C,F,[R,P],[],[],[],[Q],[]). given clause #419: (wt=15) 425 [hyper,374,5,demod,33,34] K2(F,E,[],[R],[P],[],[],[Q]). given clause #420: (wt=15) 426 [hyper,375,5,demod,33,34] K2(F,C,[],[R],[P],[],[Q],[]). ** KEPT (pick-wt=14): 500 [hyper,426,18,demod,30,32,31,30,31] H(C,[P],[],[R],[Q],[],[]). given clause #421: (wt=14) 500 [hyper,426,18,demod,30,32,31,30,31] H(C,[P],[],[R],[Q],[],[]). ** KEPT (pick-wt=14): 501 [hyper,500,25] H(C,[],[],[P,R],[Q],[],[]). ** KEPT (pick-wt=15): 502 [hyper,500,1] K1(C,F,[R],[],[P],[],[Q],[]). given clause #422: (wt=14) 501 [hyper,500,25] H(C,[],[],[P,R],[Q],[],[]). ** KEPT (pick-wt=15): 503 [hyper,501,1] K1(C,F,[P,R],[],[],[],[Q],[]). given clause #423: (wt=15) 427 [hyper,377,5,demod,33,34] K2(F,E,[],[R],[],[P,Q],[],[]). given clause #424: (wt=15) 428 [hyper,378,5,demod,33,34] K2(F,C,[],[R],[],[P,Q],[],[]). ** KEPT (pick-wt=14): 504 [hyper,428,18,demod,30,32,31,30,31] H(C,[],[P,Q],[R],[],[],[]). given clause #425: (wt=14) 504 [hyper,428,18,demod,30,32,31,30,31] H(C,[],[P,Q],[R],[],[],[]). ** KEPT (pick-wt=15): 505 [hyper,504,1] K1(C,F,[R],[],[],[P,Q],[],[]). given clause #426: (wt=15) 429 [hyper,381,5,demod,33,34] K2(D,B,[],[R,Q],[],[],[P],[]). given clause #427: (wt=15) 430 [hyper,383,6,eval,demod,33,34] K2(F,E,[P],[R],[],[Q],[],[]). ** KEPT (pick-wt=14): 506 [hyper,430,19,demod,30,32,31,30,32,31] H(E,[],[Q],[],[],[R],[P]). given clause #428: (wt=14) 506 [hyper,430,19,demod,30,32,31,30,32,31] H(E,[],[Q],[],[],[R],[P]). ** KEPT (pick-wt=15): 507 [hyper,506,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[Q],[],[P]). ** KEPT (pick-wt=15): 508 [hyper,506,4] K1(E,F,[R],[P],[],[Q],[],[]). given clause #429: (wt=15) 431 [hyper,383,5,demod,33,33,34] K2(F,E,[],[P,R],[],[Q],[],[]). given clause #430: (wt=15) 432 [hyper,384,6,eval,demod,33,34] K2(F,C,[P],[R],[],[Q],[],[]). ** KEPT (pick-wt=14): 509 [hyper,432,18,demod,30,32,31,30,32,31] H(C,[],[Q],[R],[],[],[P]). given clause #431: (wt=14) 509 [hyper,432,18,demod,30,32,31,30,32,31] H(C,[],[Q],[R],[],[],[P]). ** KEPT (pick-wt=15): 510 [hyper,509,1] K1(C,F,[R],[P],[],[Q],[],[]). given clause #432: (wt=15) 433 [hyper,384,5,demod,33,33,34] K2(F,C,[],[P,R],[],[Q],[],[]). ** KEPT (pick-wt=14): 511 [hyper,433,18,demod,30,32,32,31,30,31] H(C,[],[Q],[R,P],[],[],[]). given clause #433: (wt=14) 511 [hyper,433,18,demod,30,32,32,31,30,31] H(C,[],[Q],[R,P],[],[],[]). ** KEPT (pick-wt=15): 512 [hyper,511,1] K1(C,F,[R,P],[],[],[Q],[],[]). given clause #434: (wt=15) 434 [hyper,387,5,demod,33,34] K2(D,B,[],[R],[],[],[P,Q],[]). ** KEPT (pick-wt=14): 513 [hyper,434,9] H(B,[],[R],[],[],[P,Q],[]). given clause #435: (wt=14) 513 [hyper,434,9] H(B,[],[R],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 514 [hyper,513,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[],[P,Q],[]). given clause #436: (wt=15) 435 [hyper,390,5,demod,33,33,34] K2(D,B,[],[R,P],[],[],[Q],[]). ** KEPT (pick-wt=14): 515 [hyper,435,9] H(B,[],[R,P],[],[],[Q],[]). given clause #437: (wt=14) 515 [hyper,435,9] H(B,[],[R,P],[],[],[Q],[]). ** KEPT (pick-wt=14): 516 [hyper,515,20] H(B,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=15): 517 [hyper,515,12,demod,30,32,32,31,30,31] K1(B,D,[P,R],[],[],[],[Q],[]). given clause #438: (wt=14) 516 [hyper,515,20] H(B,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=15): 518 [hyper,516,12,demod,30,32,31,30,31] K1(B,D,[R],[],[P],[],[Q],[]). given clause #439: (wt=15) 436 [hyper,392,7] K2(F,E,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=14): 519 [hyper,436,19,demod,30,32,31,30,32,32,31] H(E,[],[],[],[],[R],[P,Q]). given clause #440: (wt=14) 519 [hyper,436,19,demod,30,32,31,30,32,32,31] H(E,[],[],[],[],[R],[P,Q]). ** KEPT (pick-wt=15): 520 [hyper,519,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 521 [hyper,519,4] K1(E,F,[R],[P,Q],[],[],[],[]). given clause #441: (wt=15) 437 [hyper,392,6,eval,demod,33,33,34] K2(F,E,[Q],[P,R],[],[],[],[]). ** KEPT (pick-wt=14): 522 [hyper,437,19,demod,30,32,32,31,30,32,31] H(E,[],[],[],[],[R,P],[Q]). given clause #442: (wt=14) 522 [hyper,437,19,demod,30,32,32,31,30,32,31] H(E,[],[],[],[],[R,P],[Q]). ** KEPT (pick-wt=15): 523 [hyper,522,13,demod,30,32,32,31,30,31] K1(E,D,[P,R],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 524 [hyper,522,4] K1(E,F,[R,P],[Q],[],[],[],[]). given clause #443: (wt=15) 438 [hyper,392,5,demod,33,33,33,34] K2(F,E,[],[Q,P,R],[],[],[],[]). given clause #444: (wt=15) 439 [hyper,393,7] K2(F,C,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=14): 525 [hyper,439,18,demod,30,32,31,30,32,32,31] H(C,[],[],[R],[],[],[P,Q]). given clause #445: (wt=14) 525 [hyper,439,18,demod,30,32,31,30,32,32,31] H(C,[],[],[R],[],[],[P,Q]). ** KEPT (pick-wt=15): 526 [hyper,525,1] K1(C,F,[R],[P,Q],[],[],[],[]). given clause #446: (wt=15) 440 [hyper,393,6,eval,demod,33,33,34] K2(F,C,[Q],[P,R],[],[],[],[]). ** KEPT (pick-wt=14): 527 [hyper,440,18,demod,30,32,32,31,30,32,31] H(C,[],[],[R,P],[],[],[Q]). given clause #447: (wt=14) 527 [hyper,440,18,demod,30,32,32,31,30,32,31] H(C,[],[],[R,P],[],[],[Q]). ** KEPT (pick-wt=15): 528 [hyper,527,1] K1(C,F,[R,P],[Q],[],[],[],[]). given clause #448: (wt=15) 441 [hyper,393,5,demod,33,33,33,34] K2(F,C,[],[Q,P,R],[],[],[],[]). ** KEPT (pick-wt=14): 529 [hyper,441,18,demod,30,32,32,32,31,30,31] H(C,[],[],[R,P,Q],[],[],[]). given clause #449: (wt=14) 529 [hyper,441,18,demod,30,32,32,32,31,30,31] H(C,[],[],[R,P,Q],[],[],[]). ** KEPT (pick-wt=15): 530 [hyper,529,1] K1(C,F,[R,P,Q],[],[],[],[],[]). given clause #450: (wt=15) 443 [hyper,442,13,demod,30,32,31,30,32,31] K1(E,D,[R],[Q],[],[],[],[P]). given clause #451: (wt=15) 444 [hyper,442,4] K1(E,F,[R],[P],[],[],[],[Q]). given clause #452: (wt=15) 446 [hyper,445,12,demod,30,32,31,30,32,31] K1(B,D,[R],[Q],[],[],[],[P]). ** KEPT (pick-wt=15): 531 [hyper,446,5,demod,33,34] K2(B,D,[],[R,Q],[],[],[],[P]). given clause #453: (wt=15) 448 [hyper,447,12,demod,30,32,32,31,30,31] K1(B,D,[R,Q],[],[],[],[],[P]). given clause #454: (wt=15) 450 [hyper,449,1] K1(C,F,[R],[P],[],[],[],[Q]). ** KEPT (pick-wt=15): 532 [hyper,450,5,demod,33,34] K2(C,F,[],[R,P],[],[],[],[Q]). given clause #455: (wt=15) 452 [hyper,451,1] K1(C,F,[R,P],[],[],[],[],[Q]). given clause #456: (wt=15) 454 [hyper,453,12,demod,30,32,31,30,32,31] K1(B,D,[R],[Q],[],[],[P],[]). ** KEPT (pick-wt=15): 533 [hyper,454,5,demod,33,34] K2(B,D,[],[R,Q],[],[],[P],[]). given clause #457: (wt=15) 456 [hyper,455,12,demod,30,32,32,31,30,31] K1(B,D,[R,Q],[],[],[],[P],[]). given clause #458: (wt=15) 459 [hyper,457,12,demod,30,32,31,30,31] K1(B,D,[R],[],[Q],[],[],[P]). ** KEPT (pick-wt=15): 534 [hyper,459,5,demod,33,34] K2(B,D,[],[R],[Q],[],[],[P]). given clause #459: (wt=15) 460 [hyper,458,12,demod,30,32,32,31,30,31] K1(B,D,[Q,R],[],[],[],[],[P]). ** KEPT (pick-wt=15): 535 [hyper,460,6,eval,demod,33,34] K2(B,D,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=15): 536 [hyper,460,5,demod,33,33,34] K2(B,D,[],[Q,R],[],[],[],[P]). given clause #460: (wt=15) 463 [hyper,461,12,demod,30,32,31,30,31] K1(B,D,[R],[],[Q],[],[P],[]). ** KEPT (pick-wt=15): 537 [hyper,463,5,demod,33,34] K2(B,D,[],[R],[Q],[],[P],[]). given clause #461: (wt=15) 464 [hyper,462,12,demod,30,32,32,31,30,31] K1(B,D,[Q,R],[],[],[],[P],[]). ** KEPT (pick-wt=15): 538 [hyper,464,6,eval,demod,33,34] K2(B,D,[Q],[R],[],[],[P],[]). ** KEPT (pick-wt=15): 539 [hyper,464,5,demod,33,33,34] K2(B,D,[],[Q,R],[],[],[P],[]). given clause #462: (wt=15) 467 [hyper,465,1] K1(C,F,[R],[],[P],[],[],[Q]). ** KEPT (pick-wt=15): 540 [hyper,467,5,demod,33,34] K2(C,F,[],[R],[P],[],[],[Q]). given clause #463: (wt=15) 468 [hyper,466,1] K1(C,F,[P,R],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 541 [hyper,468,6,eval,demod,33,34] K2(C,F,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=15): 542 [hyper,468,5,demod,33,33,34] K2(C,F,[],[P,R],[],[],[],[Q]). given clause #464: (wt=15) 470 [hyper,469,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 543 [hyper,470,5,demod,33,34] K2(B,D,[],[R],[],[P,Q],[],[]). given clause #465: (wt=15) 472 [hyper,471,13,demod,30,32,31,30,32,31] K1(E,D,[R],[Q],[],[],[P],[]). given clause #466: (wt=15) 473 [hyper,471,4] K1(E,F,[R],[],[],[],[P],[Q]). ** KEPT (pick-wt=15): 544 [hyper,473,5,demod,33,34] K2(E,F,[],[R],[],[],[P],[Q]). given clause #467: (wt=15) 475 [hyper,474,12,demod,30,32,31,30,32,31] K1(B,D,[R],[Q],[],[P],[],[]). ** KEPT (pick-wt=15): 545 [hyper,475,5,demod,33,34] K2(B,D,[],[R,Q],[],[P],[],[]). given clause #468: (wt=15) 477 [hyper,476,12,demod,30,32,32,31,30,31] K1(B,D,[R,Q],[],[],[P],[],[]). given clause #469: (wt=15) 479 [hyper,478,13,demod,30,32,31,30,32,32,31] K1(E,D,[R],[Q,P],[],[],[],[]). given clause #470: (wt=15) 480 [hyper,478,4] K1(E,F,[R],[],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 546 [hyper,480,5,demod,33,34] K2(E,F,[],[R],[],[],[],[P,Q]). given clause #471: (wt=15) 482 [hyper,481,13,demod,30,32,32,31,30,32,31] K1(E,D,[R,Q],[P],[],[],[],[]). given clause #472: (wt=15) 483 [hyper,481,4] K1(E,F,[Q,R],[],[],[],[],[P]). ** KEPT (pick-wt=15): 547 [hyper,483,6,eval,demod,33,34] K2(E,F,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=15): 548 [hyper,483,5,demod,33,33,34] K2(E,F,[],[Q,R],[],[],[],[P]). given clause #473: (wt=15) 485 [hyper,484,12,demod,30,32,31,30,32,32,31] K1(B,D,[R],[Q,P],[],[],[],[]). ** KEPT (pick-wt=15): 549 [hyper,485,5,demod,33,34] K2(B,D,[],[R,Q,P],[],[],[],[]). given clause #474: (wt=15) 487 [hyper,486,12,demod,30,32,32,31,30,32,31] K1(B,D,[R,Q],[P],[],[],[],[]). given clause #475: (wt=15) 489 [hyper,488,12,demod,30,32,32,32,31,30,31] K1(B,D,[R,Q,P],[],[],[],[],[]). given clause #476: (wt=15) 491 [hyper,490,1] K1(C,F,[R],[],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 550 [hyper,491,5,demod,33,34] K2(C,F,[],[R],[],[],[],[P,Q]). given clause #477: (wt=15) 494 [hyper,492,1] K1(C,F,[Q,R],[],[],[],[],[P]). ** KEPT (pick-wt=15): 551 [hyper,494,6,eval,demod,33,34] K2(C,F,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=15): 552 [hyper,494,5,demod,33,33,34] K2(C,F,[],[Q,R],[],[],[],[P]). given clause #478: (wt=15) 495 [hyper,493,1] K1(C,F,[R],[],[Q],[],[],[P]). ** KEPT (pick-wt=15): 553 [hyper,495,5,demod,33,34] K2(C,F,[],[R],[Q],[],[],[P]). given clause #479: (wt=15) 497 [hyper,496,1] K1(C,F,[R],[P],[],[],[Q],[]). ** KEPT (pick-wt=15): 554 [hyper,497,5,demod,33,34] K2(C,F,[],[R,P],[],[],[Q],[]). given clause #480: (wt=15) 499 [hyper,498,1] K1(C,F,[R,P],[],[],[],[Q],[]). given clause #481: (wt=15) 502 [hyper,500,1] K1(C,F,[R],[],[P],[],[Q],[]). ** KEPT (pick-wt=15): 555 [hyper,502,5,demod,33,34] K2(C,F,[],[R],[P],[],[Q],[]). given clause #482: (wt=15) 503 [hyper,501,1] K1(C,F,[P,R],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 556 [hyper,503,6,eval,demod,33,34] K2(C,F,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=15): 557 [hyper,503,5,demod,33,33,34] K2(C,F,[],[P,R],[],[],[Q],[]). given clause #483: (wt=15) 505 [hyper,504,1] K1(C,F,[R],[],[],[P,Q],[],[]). ** KEPT (pick-wt=15): 558 [hyper,505,5,demod,33,34] K2(C,F,[],[R],[],[P,Q],[],[]). given clause #484: (wt=15) 507 [hyper,506,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[Q],[],[P]). ** KEPT (pick-wt=15): 559 [hyper,507,5,demod,33,34] K2(E,D,[],[R],[],[Q],[],[P]). given clause #485: (wt=15) 508 [hyper,506,4] K1(E,F,[R],[P],[],[Q],[],[]). given clause #486: (wt=15) 510 [hyper,509,1] K1(C,F,[R],[P],[],[Q],[],[]). ** KEPT (pick-wt=15): 560 [hyper,510,5,demod,33,34] K2(C,F,[],[R,P],[],[Q],[],[]). given clause #487: (wt=15) 512 [hyper,511,1] K1(C,F,[R,P],[],[],[Q],[],[]). given clause #488: (wt=15) 514 [hyper,513,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 561 [hyper,514,5,demod,33,34] K2(B,D,[],[R],[],[],[P,Q],[]). given clause #489: (wt=15) 517 [hyper,515,12,demod,30,32,32,31,30,31] K1(B,D,[P,R],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 562 [hyper,517,6,eval,demod,33,34] K2(B,D,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=15): 563 [hyper,517,5,demod,33,33,34] K2(B,D,[],[P,R],[],[],[Q],[]). given clause #490: (wt=15) 518 [hyper,516,12,demod,30,32,31,30,31] K1(B,D,[R],[],[P],[],[Q],[]). ** KEPT (pick-wt=15): 564 [hyper,518,5,demod,33,34] K2(B,D,[],[R],[P],[],[Q],[]). given clause #491: (wt=15) 520 [hyper,519,13,demod,30,32,31,30,31] K1(E,D,[R],[],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 565 [hyper,520,5,demod,33,34] K2(E,D,[],[R],[],[],[],[P,Q]). given clause #492: (wt=15) 521 [hyper,519,4] K1(E,F,[R],[P,Q],[],[],[],[]). given clause #493: (wt=15) 523 [hyper,522,13,demod,30,32,32,31,30,31] K1(E,D,[P,R],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 566 [hyper,523,6,eval,demod,33,34] K2(E,D,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=15): 567 [hyper,523,5,demod,33,33,34] K2(E,D,[],[P,R],[],[],[],[Q]). given clause #494: (wt=15) 524 [hyper,522,4] K1(E,F,[R,P],[Q],[],[],[],[]). given clause #495: (wt=15) 526 [hyper,525,1] K1(C,F,[R],[P,Q],[],[],[],[]). ** KEPT (pick-wt=15): 568 [hyper,526,5,demod,33,34] K2(C,F,[],[R,P,Q],[],[],[],[]). given clause #496: (wt=15) 528 [hyper,527,1] K1(C,F,[R,P],[Q],[],[],[],[]). given clause #497: (wt=15) 530 [hyper,529,1] K1(C,F,[R,P,Q],[],[],[],[],[]). given clause #498: (wt=15) 531 [hyper,446,5,demod,33,34] K2(B,D,[],[R,Q],[],[],[],[P]). given clause #499: (wt=15) 532 [hyper,450,5,demod,33,34] K2(C,F,[],[R,P],[],[],[],[Q]). given clause #500: (wt=15) 533 [hyper,454,5,demod,33,34] K2(B,D,[],[R,Q],[],[],[P],[]). given clause #501: (wt=15) 534 [hyper,459,5,demod,33,34] K2(B,D,[],[R],[Q],[],[],[P]). given clause #502: (wt=15) 535 [hyper,460,6,eval,demod,33,34] K2(B,D,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=14): 569 [hyper,535,16,demod,30,32,31,30,32,31] H(D,[],[Q],[],[R],[],[P]). given clause #503: (wt=14) 569 [hyper,535,16,demod,30,32,31,30,32,31] H(D,[],[Q],[],[R],[],[P]). ** KEPT (pick-wt=15): 570 [hyper,569,3] K1(D,E,[R],[],[],[Q],[],[P]). ** KEPT (pick-wt=15): 571 [hyper,569,2] K1(D,B,[R],[Q],[],[],[],[P]). given clause #504: (wt=15) 536 [hyper,460,5,demod,33,33,34] K2(B,D,[],[Q,R],[],[],[],[P]). ** KEPT (pick-wt=14): 572 [hyper,536,16,demod,30,31,30,32,32,31] H(D,[],[],[],[R,Q],[],[P]). given clause #505: (wt=14) 572 [hyper,536,16,demod,30,31,30,32,32,31] H(D,[],[],[],[R,Q],[],[P]). ** KEPT (pick-wt=15): 573 [hyper,572,3] K1(D,E,[R,Q],[],[],[],[],[P]). ** KEPT (pick-wt=15): 574 [hyper,572,2] K1(D,B,[R,Q],[],[],[],[],[P]). given clause #506: (wt=15) 537 [hyper,463,5,demod,33,34] K2(B,D,[],[R],[Q],[],[P],[]). given clause #507: (wt=15) 538 [hyper,464,6,eval,demod,33,34] K2(B,D,[Q],[R],[],[],[P],[]). given clause #508: (wt=15) 539 [hyper,464,5,demod,33,33,34] K2(B,D,[],[Q,R],[],[],[P],[]). ** KEPT (pick-wt=14): 575 [hyper,539,16,demod,30,31,30,32,32,31] H(D,[],[],[],[R,Q],[P],[]). given clause #509: (wt=14) 575 [hyper,539,16,demod,30,31,30,32,32,31] H(D,[],[],[],[R,Q],[P],[]). ** KEPT (pick-wt=15): 576 [hyper,575,3] K1(D,E,[R,Q],[P],[],[],[],[]). ** KEPT (pick-wt=15): 577 [hyper,575,2] K1(D,B,[R,Q],[],[],[],[P],[]). given clause #510: (wt=15) 540 [hyper,467,5,demod,33,34] K2(C,F,[],[R],[P],[],[],[Q]). given clause #511: (wt=15) 541 [hyper,468,6,eval,demod,33,34] K2(C,F,[P],[R],[],[],[],[Q]). given clause #512: (wt=15) 542 [hyper,468,5,demod,33,33,34] K2(C,F,[],[P,R],[],[],[],[Q]). ** KEPT (pick-wt=14): 578 [hyper,542,8] H(F,[],[],[],[],[Q],[P,R]). given clause #513: (wt=14) 578 [hyper,542,8] H(F,[],[],[],[],[Q],[P,R]). ** KEPT (pick-wt=15): 579 [hyper,578,15,demod,30,32,32,31,30,32,31] K1(F,E,[R,P],[Q],[],[],[],[]). ** KEPT (pick-wt=15): 580 [hyper,578,14,demod,30,32,32,31,30,31] K1(F,C,[R,P],[],[],[],[],[Q]). given clause #514: (wt=15) 543 [hyper,470,5,demod,33,34] K2(B,D,[],[R],[],[P,Q],[],[]). given clause #515: (wt=15) 544 [hyper,473,5,demod,33,34] K2(E,F,[],[R],[],[],[P],[Q]). ** KEPT (pick-wt=14): 581 [hyper,544,11] H(F,[],[],[P],[Q],[],[R]). given clause #516: (wt=14) 581 [hyper,544,11] H(F,[],[],[P],[Q],[],[R]). ** KEPT (pick-wt=15): 582 [hyper,581,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[],[P],[Q]). ** KEPT (pick-wt=15): 583 [hyper,581,14,demod,30,32,31,30,32,31] K1(F,C,[R],[P],[],[],[Q],[]). given clause #517: (wt=15) 545 [hyper,475,5,demod,33,34] K2(B,D,[],[R,Q],[],[P],[],[]). given clause #518: (wt=15) 546 [hyper,480,5,demod,33,34] K2(E,F,[],[R],[],[],[],[P,Q]). ** KEPT (pick-wt=14): 584 [hyper,546,11] H(F,[],[],[],[P,Q],[],[R]). given clause #519: (wt=14) 584 [hyper,546,11] H(F,[],[],[],[P,Q],[],[R]). ** KEPT (pick-wt=15): 585 [hyper,584,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 586 [hyper,584,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[],[P,Q],[]). given clause #520: (wt=15) 547 [hyper,483,6,eval,demod,33,34] K2(E,F,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=14): 587 [hyper,547,11] H(F,[],[],[],[P],[Q],[R]). given clause #521: (wt=14) 587 [hyper,547,11] H(F,[],[],[],[P],[Q],[R]). ** KEPT (pick-wt=15): 588 [hyper,587,15,demod,30,32,31,30,32,31] K1(F,E,[R],[Q],[],[],[],[P]). ** KEPT (pick-wt=15): 589 [hyper,587,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[],[P],[Q]). given clause #522: (wt=15) 548 [hyper,483,5,demod,33,33,34] K2(E,F,[],[Q,R],[],[],[],[P]). ** KEPT (pick-wt=14): 590 [hyper,548,11] H(F,[],[],[],[P],[],[Q,R]). given clause #523: (wt=14) 590 [hyper,548,11] H(F,[],[],[],[P],[],[Q,R]). ** KEPT (pick-wt=15): 591 [hyper,590,15,demod,30,32,32,31,30,31] K1(F,E,[R,Q],[],[],[],[],[P]). ** KEPT (pick-wt=15): 592 [hyper,590,14,demod,30,32,32,31,30,31] K1(F,C,[R,Q],[],[],[],[P],[]). given clause #524: (wt=15) 549 [hyper,485,5,demod,33,34] K2(B,D,[],[R,Q,P],[],[],[],[]). given clause #525: (wt=15) 550 [hyper,491,5,demod,33,34] K2(C,F,[],[R],[],[],[],[P,Q]). given clause #526: (wt=15) 551 [hyper,494,6,eval,demod,33,34] K2(C,F,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=14): 593 [hyper,551,8] H(F,[],[],[Q],[],[P],[R]). given clause #527: (wt=14) 593 [hyper,551,8] H(F,[],[],[Q],[],[P],[R]). ** KEPT (pick-wt=15): 594 [hyper,593,15,demod,30,32,31,30,32,31] K1(F,E,[R],[P],[],[],[Q],[]). ** KEPT (pick-wt=15): 595 [hyper,593,14,demod,30,32,31,30,32,31] K1(F,C,[R],[Q],[],[],[],[P]). given clause #528: (wt=15) 552 [hyper,494,5,demod,33,33,34] K2(C,F,[],[Q,R],[],[],[],[P]). given clause #529: (wt=15) 553 [hyper,495,5,demod,33,34] K2(C,F,[],[R],[Q],[],[],[P]). ** KEPT (pick-wt=14): 596 [hyper,553,8] H(F,[Q],[],[],[],[P],[R]). given clause #530: (wt=14) 596 [hyper,553,8] H(F,[Q],[],[],[],[P],[R]). ** KEPT (pick-wt=15): 597 [hyper,596,15,demod,30,32,31,30,32,31] K1(F,E,[R],[P],[Q],[],[],[]). ** KEPT (pick-wt=15): 598 [hyper,596,14,demod,30,32,31,30,31] K1(F,C,[R],[],[Q],[],[],[P]). given clause #531: (wt=15) 554 [hyper,497,5,demod,33,34] K2(C,F,[],[R,P],[],[],[Q],[]). given clause #532: (wt=15) 555 [hyper,502,5,demod,33,34] K2(C,F,[],[R],[P],[],[Q],[]). given clause #533: (wt=15) 556 [hyper,503,6,eval,demod,33,34] K2(C,F,[P],[R],[],[],[Q],[]). given clause #534: (wt=15) 557 [hyper,503,5,demod,33,33,34] K2(C,F,[],[P,R],[],[],[Q],[]). ** KEPT (pick-wt=14): 599 [hyper,557,8] H(F,[],[],[],[Q],[],[P,R]). given clause #535: (wt=14) 599 [hyper,557,8] H(F,[],[],[],[Q],[],[P,R]). ** KEPT (pick-wt=15): 600 [hyper,599,15,demod,30,32,32,31,30,31] K1(F,E,[R,P],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 601 [hyper,599,14,demod,30,32,32,31,30,31] K1(F,C,[R,P],[],[],[],[Q],[]). given clause #536: (wt=15) 558 [hyper,505,5,demod,33,34] K2(C,F,[],[R],[],[P,Q],[],[]). given clause #537: (wt=15) 559 [hyper,507,5,demod,33,34] K2(E,D,[],[R],[],[Q],[],[P]). given clause #538: (wt=15) 560 [hyper,510,5,demod,33,34] K2(C,F,[],[R,P],[],[Q],[],[]). given clause #539: (wt=15) 561 [hyper,514,5,demod,33,34] K2(B,D,[],[R],[],[],[P,Q],[]). given clause #540: (wt=15) 562 [hyper,517,6,eval,demod,33,34] K2(B,D,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=14): 602 [hyper,562,16,demod,30,32,31,30,32,31] H(D,[],[P],[],[R],[Q],[]). given clause #541: (wt=14) 602 [hyper,562,16,demod,30,32,31,30,32,31] H(D,[],[P],[],[R],[Q],[]). ** KEPT (pick-wt=15): 603 [hyper,602,3] K1(D,E,[R],[Q],[],[P],[],[]). ** KEPT (pick-wt=15): 604 [hyper,602,2] K1(D,B,[R],[P],[],[],[Q],[]). given clause #542: (wt=15) 563 [hyper,517,5,demod,33,33,34] K2(B,D,[],[P,R],[],[],[Q],[]). given clause #543: (wt=15) 564 [hyper,518,5,demod,33,34] K2(B,D,[],[R],[P],[],[Q],[]). ** KEPT (pick-wt=14): 605 [hyper,564,16,demod,30,31,30,32,31] H(D,[P],[],[],[R],[Q],[]). given clause #544: (wt=14) 605 [hyper,564,16,demod,30,31,30,32,31] H(D,[P],[],[],[R],[Q],[]). ** KEPT (pick-wt=15): 606 [hyper,605,3] K1(D,E,[R],[Q],[P],[],[],[]). ** KEPT (pick-wt=15): 607 [hyper,605,2] K1(D,B,[R],[],[P],[],[Q],[]). given clause #545: (wt=15) 565 [hyper,520,5,demod,33,34] K2(E,D,[],[R],[],[],[],[P,Q]). ** KEPT (pick-wt=14): 608 [hyper,565,17,demod,30,32,31,30,31] H(D,[],[],[],[R],[],[P,Q]). given clause #546: (wt=14) 608 [hyper,565,17,demod,30,32,31,30,31] H(D,[],[],[],[R],[],[P,Q]). ** KEPT (pick-wt=15): 609 [hyper,608,3] K1(D,E,[R],[],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 610 [hyper,608,2] K1(D,B,[R],[],[],[],[],[P,Q]). given clause #547: (wt=15) 566 [hyper,523,6,eval,demod,33,34] K2(E,D,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=14): 611 [hyper,566,17,demod,30,32,31,30,32,31] H(D,[],[],[],[R],[P],[Q]). given clause #548: (wt=14) 611 [hyper,566,17,demod,30,32,31,30,32,31] H(D,[],[],[],[R],[P],[Q]). ** KEPT (pick-wt=15): 612 [hyper,611,3] K1(D,E,[R],[P],[],[],[],[Q]). ** KEPT (pick-wt=15): 613 [hyper,611,2] K1(D,B,[R],[],[],[],[P],[Q]). given clause #549: (wt=15) 567 [hyper,523,5,demod,33,33,34] K2(E,D,[],[P,R],[],[],[],[Q]). ** KEPT (pick-wt=14): 614 [hyper,567,17,demod,30,32,32,31,30,31] H(D,[],[],[],[R,P],[],[Q]). given clause #550: (wt=14) 614 [hyper,567,17,demod,30,32,32,31,30,31] H(D,[],[],[],[R,P],[],[Q]). ** KEPT (pick-wt=15): 615 [hyper,614,3] K1(D,E,[R,P],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 616 [hyper,614,2] K1(D,B,[R,P],[],[],[],[],[Q]). given clause #551: (wt=15) 568 [hyper,526,5,demod,33,34] K2(C,F,[],[R,P,Q],[],[],[],[]). given clause #552: (wt=15) 570 [hyper,569,3] K1(D,E,[R],[],[],[Q],[],[P]). ** KEPT (pick-wt=15): 617 [hyper,570,5,demod,33,34] K2(D,E,[],[R],[],[Q],[],[P]). given clause #553: (wt=15) 571 [hyper,569,2] K1(D,B,[R],[Q],[],[],[],[P]). ** KEPT (pick-wt=15): 618 [hyper,571,5,demod,33,34] K2(D,B,[],[R,Q],[],[],[],[P]). given clause #554: (wt=15) 573 [hyper,572,3] K1(D,E,[R,Q],[],[],[],[],[P]). ** KEPT (pick-wt=15): 619 [hyper,573,5,demod,33,33,34] K2(D,E,[],[R,Q],[],[],[],[P]). given clause #555: (wt=15) 574 [hyper,572,2] K1(D,B,[R,Q],[],[],[],[],[P]). given clause #556: (wt=15) 576 [hyper,575,3] K1(D,E,[R,Q],[P],[],[],[],[]). ** KEPT (pick-wt=15): 620 [hyper,576,5,demod,33,33,34] K2(D,E,[],[R,Q,P],[],[],[],[]). given clause #557: (wt=15) 577 [hyper,575,2] K1(D,B,[R,Q],[],[],[],[P],[]). given clause #558: (wt=15) 579 [hyper,578,15,demod,30,32,32,31,30,32,31] K1(F,E,[R,P],[Q],[],[],[],[]). ** KEPT (pick-wt=15): 621 [hyper,579,5,demod,33,33,34] K2(F,E,[],[R,P,Q],[],[],[],[]). given clause #559: (wt=15) 580 [hyper,578,14,demod,30,32,32,31,30,31] K1(F,C,[R,P],[],[],[],[],[Q]). given clause #560: (wt=15) 582 [hyper,581,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[],[P],[Q]). ** KEPT (pick-wt=15): 622 [hyper,582,5,demod,33,34] K2(F,E,[],[R],[],[],[P],[Q]). given clause #561: (wt=15) 583 [hyper,581,14,demod,30,32,31,30,32,31] K1(F,C,[R],[P],[],[],[Q],[]). ** KEPT (pick-wt=15): 623 [hyper,583,5,demod,33,34] K2(F,C,[],[R,P],[],[],[Q],[]). given clause #562: (wt=15) 585 [hyper,584,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 624 [hyper,585,5,demod,33,34] K2(F,E,[],[R],[],[],[],[P,Q]). given clause #563: (wt=15) 586 [hyper,584,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 625 [hyper,586,5,demod,33,34] K2(F,C,[],[R],[],[],[P,Q],[]). given clause #564: (wt=15) 588 [hyper,587,15,demod,30,32,31,30,32,31] K1(F,E,[R],[Q],[],[],[],[P]). ** KEPT (pick-wt=15): 626 [hyper,588,5,demod,33,34] K2(F,E,[],[R,Q],[],[],[],[P]). given clause #565: (wt=15) 589 [hyper,587,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[],[P],[Q]). ** KEPT (pick-wt=15): 627 [hyper,589,5,demod,33,34] K2(F,C,[],[R],[],[],[P],[Q]). given clause #566: (wt=15) 591 [hyper,590,15,demod,30,32,32,31,30,31] K1(F,E,[R,Q],[],[],[],[],[P]). given clause #567: (wt=15) 592 [hyper,590,14,demod,30,32,32,31,30,31] K1(F,C,[R,Q],[],[],[],[P],[]). ** KEPT (pick-wt=15): 628 [hyper,592,5,demod,33,33,34] K2(F,C,[],[R,Q],[],[],[P],[]). given clause #568: (wt=15) 594 [hyper,593,15,demod,30,32,31,30,32,31] K1(F,E,[R],[P],[],[],[Q],[]). ** KEPT (pick-wt=15): 629 [hyper,594,5,demod,33,34] K2(F,E,[],[R,P],[],[],[Q],[]). given clause #569: (wt=15) 595 [hyper,593,14,demod,30,32,31,30,32,31] K1(F,C,[R],[Q],[],[],[],[P]). given clause #570: (wt=15) 597 [hyper,596,15,demod,30,32,31,30,32,31] K1(F,E,[R],[P],[Q],[],[],[]). ** KEPT (pick-wt=15): 630 [hyper,597,5,demod,33,34] K2(F,E,[],[R,P],[Q],[],[],[]). given clause #571: (wt=15) 598 [hyper,596,14,demod,30,32,31,30,31] K1(F,C,[R],[],[Q],[],[],[P]). ** KEPT (pick-wt=15): 631 [hyper,598,5,demod,33,34] K2(F,C,[],[R],[Q],[],[],[P]). given clause #572: (wt=15) 600 [hyper,599,15,demod,30,32,32,31,30,31] K1(F,E,[R,P],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 632 [hyper,600,5,demod,33,33,34] K2(F,E,[],[R,P],[],[],[],[Q]). given clause #573: (wt=15) 601 [hyper,599,14,demod,30,32,32,31,30,31] K1(F,C,[R,P],[],[],[],[Q],[]). given clause #574: (wt=15) 603 [hyper,602,3] K1(D,E,[R],[Q],[],[P],[],[]). ** KEPT (pick-wt=15): 633 [hyper,603,5,demod,33,34] K2(D,E,[],[R,Q],[],[P],[],[]). given clause #575: (wt=15) 604 [hyper,602,2] K1(D,B,[R],[P],[],[],[Q],[]). given clause #576: (wt=15) 606 [hyper,605,3] K1(D,E,[R],[Q],[P],[],[],[]). ** KEPT (pick-wt=15): 634 [hyper,606,5,demod,33,34] K2(D,E,[],[R,Q],[P],[],[],[]). given clause #577: (wt=15) 607 [hyper,605,2] K1(D,B,[R],[],[P],[],[Q],[]). ** KEPT (pick-wt=15): 635 [hyper,607,5,demod,33,34] K2(D,B,[],[R],[P],[],[Q],[]). given clause #578: (wt=15) 609 [hyper,608,3] K1(D,E,[R],[],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 636 [hyper,609,5,demod,33,34] K2(D,E,[],[R],[],[],[],[P,Q]). given clause #579: (wt=15) 610 [hyper,608,2] K1(D,B,[R],[],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 637 [hyper,610,5,demod,33,34] K2(D,B,[],[R],[],[],[],[P,Q]). given clause #580: (wt=15) 612 [hyper,611,3] K1(D,E,[R],[P],[],[],[],[Q]). ** KEPT (pick-wt=15): 638 [hyper,612,5,demod,33,34] K2(D,E,[],[R,P],[],[],[],[Q]). given clause #581: (wt=15) 613 [hyper,611,2] K1(D,B,[R],[],[],[],[P],[Q]). ** KEPT (pick-wt=15): 639 [hyper,613,5,demod,33,34] K2(D,B,[],[R],[],[],[P],[Q]). given clause #582: (wt=15) 615 [hyper,614,3] K1(D,E,[R,P],[],[],[],[],[Q]). given clause #583: (wt=15) 616 [hyper,614,2] K1(D,B,[R,P],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 640 [hyper,616,5,demod,33,33,34] K2(D,B,[],[R,P],[],[],[],[Q]). given clause #584: (wt=15) 617 [hyper,570,5,demod,33,34] K2(D,E,[],[R],[],[Q],[],[P]). given clause #585: (wt=15) 618 [hyper,571,5,demod,33,34] K2(D,B,[],[R,Q],[],[],[],[P]). given clause #586: (wt=15) 619 [hyper,573,5,demod,33,33,34] K2(D,E,[],[R,Q],[],[],[],[P]). ** KEPT (pick-wt=14): 641 [hyper,619,10] H(E,[],[],[],[],[R,Q],[P]). given clause #587: (wt=14) 641 [hyper,619,10] H(E,[],[],[],[],[R,Q],[P]). ** KEPT (pick-wt=15): 642 [hyper,641,13,demod,30,32,32,31,30,31] K1(E,D,[Q,R],[],[],[],[],[P]). ** KEPT (pick-wt=15): 643 [hyper,641,4] K1(E,F,[R,Q],[P],[],[],[],[]). given clause #588: (wt=15) 620 [hyper,576,5,demod,33,33,34] K2(D,E,[],[R,Q,P],[],[],[],[]). ** KEPT (pick-wt=14): 644 [hyper,620,10] H(E,[],[],[],[],[R,Q,P],[]). given clause #589: (wt=14) 644 [hyper,620,10] H(E,[],[],[],[],[R,Q,P],[]). ** KEPT (pick-wt=15): 645 [hyper,644,13,demod,30,32,32,32,31,30,31] K1(E,D,[P,Q,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 646 [hyper,644,4] K1(E,F,[R,Q,P],[],[],[],[],[]). given clause #590: (wt=15) 621 [hyper,579,5,demod,33,33,34] K2(F,E,[],[R,P,Q],[],[],[],[]). ** KEPT (pick-wt=14): 647 [hyper,621,19,demod,30,32,32,32,31,30,31] H(E,[],[],[],[],[Q,P,R],[]). given clause #591: (wt=14) 647 [hyper,621,19,demod,30,32,32,32,31,30,31] H(E,[],[],[],[],[Q,P,R],[]). ** KEPT (pick-wt=15): 648 [hyper,647,13,demod,30,32,32,32,31,30,31] K1(E,D,[R,P,Q],[],[],[],[],[]). ** KEPT (pick-wt=15): 649 [hyper,647,4] K1(E,F,[Q,P,R],[],[],[],[],[]). given clause #592: (wt=15) 622 [hyper,582,5,demod,33,34] K2(F,E,[],[R],[],[],[P],[Q]). given clause #593: (wt=15) 623 [hyper,583,5,demod,33,34] K2(F,C,[],[R,P],[],[],[Q],[]). given clause #594: (wt=15) 624 [hyper,585,5,demod,33,34] K2(F,E,[],[R],[],[],[],[P,Q]). given clause #595: (wt=15) 625 [hyper,586,5,demod,33,34] K2(F,C,[],[R],[],[],[P,Q],[]). ** KEPT (pick-wt=14): 650 [hyper,625,18,demod,30,32,31,30,31] H(C,[],[],[R],[P,Q],[],[]). given clause #596: (wt=14) 650 [hyper,625,18,demod,30,32,31,30,31] H(C,[],[],[R],[P,Q],[],[]). ** KEPT (pick-wt=15): 651 [hyper,650,1] K1(C,F,[R],[],[],[],[P,Q],[]). given clause #597: (wt=15) 626 [hyper,588,5,demod,33,34] K2(F,E,[],[R,Q],[],[],[],[P]). given clause #598: (wt=15) 627 [hyper,589,5,demod,33,34] K2(F,C,[],[R],[],[],[P],[Q]). ** KEPT (pick-wt=14): 652 [hyper,627,18,demod,30,32,31,30,31] H(C,[],[],[R],[P],[Q],[]). given clause #599: (wt=14) 652 [hyper,627,18,demod,30,32,31,30,31] H(C,[],[],[R],[P],[Q],[]). ** KEPT (pick-wt=15): 653 [hyper,652,1] K1(C,F,[R],[],[],[],[P],[Q]). given clause #600: (wt=15) 628 [hyper,592,5,demod,33,33,34] K2(F,C,[],[R,Q],[],[],[P],[]). ** KEPT (pick-wt=14): 654 [hyper,628,18,demod,30,32,32,31,30,31] H(C,[],[],[Q,R],[P],[],[]). given clause #601: (wt=14) 654 [hyper,628,18,demod,30,32,32,31,30,31] H(C,[],[],[Q,R],[P],[],[]). ** KEPT (pick-wt=14): 655 [hyper,654,24,eval] H(C,[Q],[],[R],[P],[],[]). ** KEPT (pick-wt=15): 656 [hyper,654,1] K1(C,F,[Q,R],[],[],[],[P],[]). given clause #602: (wt=14) 655 [hyper,654,24,eval] H(C,[Q],[],[R],[P],[],[]). ** KEPT (pick-wt=15): 657 [hyper,655,1] K1(C,F,[R],[],[Q],[],[P],[]). given clause #603: (wt=15) 629 [hyper,594,5,demod,33,34] K2(F,E,[],[R,P],[],[],[Q],[]). ** KEPT (pick-wt=14): 658 [hyper,629,19,demod,30,32,32,31,30,31] H(E,[],[],[Q],[],[P,R],[]). given clause #604: (wt=14) 658 [hyper,629,19,demod,30,32,32,31,30,31] H(E,[],[],[Q],[],[P,R],[]). ** KEPT (pick-wt=15): 659 [hyper,658,13,demod,30,32,32,31,30,31] K1(E,D,[R,P],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 660 [hyper,658,4] K1(E,F,[P,R],[],[],[],[Q],[]). given clause #605: (wt=15) 630 [hyper,597,5,demod,33,34] K2(F,E,[],[R,P],[Q],[],[],[]). ** KEPT (pick-wt=14): 661 [hyper,630,19,demod,30,32,32,31,30,31] H(E,[Q],[],[],[],[P,R],[]). given clause #606: (wt=14) 661 [hyper,630,19,demod,30,32,32,31,30,31] H(E,[Q],[],[],[],[P,R],[]). ** KEPT (pick-wt=15): 662 [hyper,661,13,demod,30,32,32,31,30,31] K1(E,D,[R,P],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 663 [hyper,661,4] K1(E,F,[P,R],[],[Q],[],[],[]). given clause #607: (wt=15) 631 [hyper,598,5,demod,33,34] K2(F,C,[],[R],[Q],[],[],[P]). given clause #608: (wt=15) 632 [hyper,600,5,demod,33,33,34] K2(F,E,[],[R,P],[],[],[],[Q]). ** KEPT (pick-wt=14): 664 [hyper,632,19,demod,30,32,32,31,30,31] H(E,[],[],[],[Q],[P,R],[]). given clause #609: (wt=14) 664 [hyper,632,19,demod,30,32,32,31,30,31] H(E,[],[],[],[Q],[P,R],[]). ** KEPT (pick-wt=15): 665 [hyper,664,13,demod,30,32,32,31,30,32,31] K1(E,D,[R,P],[Q],[],[],[],[]). ** KEPT (pick-wt=15): 666 [hyper,664,4] K1(E,F,[P,R],[],[],[],[],[Q]). given clause #610: (wt=15) 633 [hyper,603,5,demod,33,34] K2(D,E,[],[R,Q],[],[P],[],[]). ** KEPT (pick-wt=14): 667 [hyper,633,10] H(E,[],[P],[],[],[R,Q],[]). given clause #611: (wt=14) 667 [hyper,633,10] H(E,[],[P],[],[],[R,Q],[]). ** KEPT (pick-wt=15): 668 [hyper,667,13,demod,30,32,32,31,30,31] K1(E,D,[Q,R],[],[],[P],[],[]). ** KEPT (pick-wt=15): 669 [hyper,667,4] K1(E,F,[R,Q],[],[],[P],[],[]). given clause #612: (wt=15) 634 [hyper,606,5,demod,33,34] K2(D,E,[],[R,Q],[P],[],[],[]). ** KEPT (pick-wt=14): 670 [hyper,634,10] H(E,[P],[],[],[],[R,Q],[]). given clause #613: (wt=14) 670 [hyper,634,10] H(E,[P],[],[],[],[R,Q],[]). ** KEPT (pick-wt=15): 671 [hyper,670,13,demod,30,32,32,31,30,31] K1(E,D,[Q,R],[],[P],[],[],[]). ** KEPT (pick-wt=15): 672 [hyper,670,4] K1(E,F,[R,Q],[],[P],[],[],[]). given clause #614: (wt=15) 635 [hyper,607,5,demod,33,34] K2(D,B,[],[R],[P],[],[Q],[]). given clause #615: (wt=15) 636 [hyper,609,5,demod,33,34] K2(D,E,[],[R],[],[],[],[P,Q]). given clause #616: (wt=15) 637 [hyper,610,5,demod,33,34] K2(D,B,[],[R],[],[],[],[P,Q]). ** KEPT (pick-wt=14): 673 [hyper,637,9] H(B,[],[R],[],[],[],[P,Q]). given clause #617: (wt=14) 673 [hyper,637,9] H(B,[],[R],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 674 [hyper,673,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[],[],[P,Q]). given clause #618: (wt=15) 638 [hyper,612,5,demod,33,34] K2(D,E,[],[R,P],[],[],[],[Q]). given clause #619: (wt=15) 639 [hyper,613,5,demod,33,34] K2(D,B,[],[R],[],[],[P],[Q]). ** KEPT (pick-wt=14): 675 [hyper,639,9] H(B,[],[R],[],[],[P],[Q]). given clause #620: (wt=14) 675 [hyper,639,9] H(B,[],[R],[],[],[P],[Q]). ** KEPT (pick-wt=15): 676 [hyper,675,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[],[P],[Q]). given clause #621: (wt=15) 640 [hyper,616,5,demod,33,33,34] K2(D,B,[],[R,P],[],[],[],[Q]). ** KEPT (pick-wt=14): 677 [hyper,640,9] H(B,[],[R,P],[],[],[],[Q]). given clause #622: (wt=14) 677 [hyper,640,9] H(B,[],[R,P],[],[],[],[Q]). ** KEPT (pick-wt=14): 678 [hyper,677,20] H(B,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=15): 679 [hyper,677,12,demod,30,32,32,31,30,31] K1(B,D,[P,R],[],[],[],[],[Q]). given clause #623: (wt=14) 678 [hyper,677,20] H(B,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=15): 680 [hyper,678,12,demod,30,32,31,30,31] K1(B,D,[R],[],[P],[],[],[Q]). given clause #624: (wt=15) 642 [hyper,641,13,demod,30,32,32,31,30,31] K1(E,D,[Q,R],[],[],[],[],[P]). ** KEPT (pick-wt=15): 681 [hyper,642,6,eval,demod,33,34] K2(E,D,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=15): 682 [hyper,642,5,demod,33,33,34] K2(E,D,[],[Q,R],[],[],[],[P]). given clause #625: (wt=15) 643 [hyper,641,4] K1(E,F,[R,Q],[P],[],[],[],[]). ** KEPT (pick-wt=15): 683 [hyper,643,5,demod,33,33,34] K2(E,F,[],[R,Q,P],[],[],[],[]). given clause #626: (wt=15) 645 [hyper,644,13,demod,30,32,32,32,31,30,31] K1(E,D,[P,Q,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 684 [hyper,645,7] K2(E,D,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=15): 685 [hyper,645,6,eval,demod,33,33,34] K2(E,D,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=15): 686 [hyper,645,5,demod,33,33,33,34] K2(E,D,[],[P,Q,R],[],[],[],[]). given clause #627: (wt=15) 646 [hyper,644,4] K1(E,F,[R,Q,P],[],[],[],[],[]). given clause #628: (wt=15) 648 [hyper,647,13,demod,30,32,32,32,31,30,31] K1(E,D,[R,P,Q],[],[],[],[],[]). ** KEPT (pick-wt=15): 687 [hyper,648,5,demod,33,33,33,34] K2(E,D,[],[R,P,Q],[],[],[],[]). given clause #629: (wt=15) 649 [hyper,647,4] K1(E,F,[Q,P,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 688 [hyper,649,7] K2(E,F,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=15): 689 [hyper,649,6,eval,demod,33,33,34] K2(E,F,[Q],[P,R],[],[],[],[]). ** KEPT (pick-wt=15): 690 [hyper,649,5,demod,33,33,33,34] K2(E,F,[],[Q,P,R],[],[],[],[]). given clause #630: (wt=15) 651 [hyper,650,1] K1(C,F,[R],[],[],[],[P,Q],[]). ** KEPT (pick-wt=15): 691 [hyper,651,5,demod,33,34] K2(C,F,[],[R],[],[],[P,Q],[]). given clause #631: (wt=15) 653 [hyper,652,1] K1(C,F,[R],[],[],[],[P],[Q]). ** KEPT (pick-wt=15): 692 [hyper,653,5,demod,33,34] K2(C,F,[],[R],[],[],[P],[Q]). given clause #632: (wt=15) 656 [hyper,654,1] K1(C,F,[Q,R],[],[],[],[P],[]). ** KEPT (pick-wt=15): 693 [hyper,656,6,eval,demod,33,34] K2(C,F,[Q],[R],[],[],[P],[]). ** KEPT (pick-wt=15): 694 [hyper,656,5,demod,33,33,34] K2(C,F,[],[Q,R],[],[],[P],[]). given clause #633: (wt=15) 657 [hyper,655,1] K1(C,F,[R],[],[Q],[],[P],[]). ** KEPT (pick-wt=15): 695 [hyper,657,5,demod,33,34] K2(C,F,[],[R],[Q],[],[P],[]). given clause #634: (wt=15) 659 [hyper,658,13,demod,30,32,32,31,30,31] K1(E,D,[R,P],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 696 [hyper,659,5,demod,33,33,34] K2(E,D,[],[R,P],[],[],[Q],[]). given clause #635: (wt=15) 660 [hyper,658,4] K1(E,F,[P,R],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 697 [hyper,660,6,eval,demod,33,34] K2(E,F,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=15): 698 [hyper,660,5,demod,33,33,34] K2(E,F,[],[P,R],[],[],[Q],[]). given clause #636: (wt=15) 662 [hyper,661,13,demod,30,32,32,31,30,31] K1(E,D,[R,P],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 699 [hyper,662,5,demod,33,33,34] K2(E,D,[],[R,P],[Q],[],[],[]). given clause #637: (wt=15) 663 [hyper,661,4] K1(E,F,[P,R],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 700 [hyper,663,6,eval,demod,33,34] K2(E,F,[P],[R],[Q],[],[],[]). ** KEPT (pick-wt=15): 701 [hyper,663,5,demod,33,33,34] K2(E,F,[],[P,R],[Q],[],[],[]). given clause #638: (wt=15) 665 [hyper,664,13,demod,30,32,32,31,30,32,31] K1(E,D,[R,P],[Q],[],[],[],[]). given clause #639: (wt=15) 666 [hyper,664,4] K1(E,F,[P,R],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 702 [hyper,666,6,eval,demod,33,34] K2(E,F,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=15): 703 [hyper,666,5,demod,33,33,34] K2(E,F,[],[P,R],[],[],[],[Q]). given clause #640: (wt=15) 668 [hyper,667,13,demod,30,32,32,31,30,31] K1(E,D,[Q,R],[],[],[P],[],[]). ** KEPT (pick-wt=15): 704 [hyper,668,6,eval,demod,33,34] K2(E,D,[Q],[R],[],[P],[],[]). ** KEPT (pick-wt=15): 705 [hyper,668,5,demod,33,33,34] K2(E,D,[],[Q,R],[],[P],[],[]). given clause #641: (wt=15) 669 [hyper,667,4] K1(E,F,[R,Q],[],[],[P],[],[]). ** KEPT (pick-wt=15): 706 [hyper,669,5,demod,33,33,34] K2(E,F,[],[R,Q],[],[P],[],[]). given clause #642: (wt=15) 671 [hyper,670,13,demod,30,32,32,31,30,31] K1(E,D,[Q,R],[],[P],[],[],[]). ** KEPT (pick-wt=15): 707 [hyper,671,6,eval,demod,33,34] K2(E,D,[Q],[R],[P],[],[],[]). ** KEPT (pick-wt=15): 708 [hyper,671,5,demod,33,33,34] K2(E,D,[],[Q,R],[P],[],[],[]). given clause #643: (wt=15) 672 [hyper,670,4] K1(E,F,[R,Q],[],[P],[],[],[]). ** KEPT (pick-wt=15): 709 [hyper,672,5,demod,33,33,34] K2(E,F,[],[R,Q],[P],[],[],[]). given clause #644: (wt=15) 674 [hyper,673,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[],[],[P,Q]). ** KEPT (pick-wt=15): 710 [hyper,674,5,demod,33,34] K2(B,D,[],[R],[],[],[],[P,Q]). given clause #645: (wt=15) 676 [hyper,675,12,demod,30,32,31,30,31] K1(B,D,[R],[],[],[],[P],[Q]). ** KEPT (pick-wt=15): 711 [hyper,676,5,demod,33,34] K2(B,D,[],[R],[],[],[P],[Q]). given clause #646: (wt=15) 679 [hyper,677,12,demod,30,32,32,31,30,31] K1(B,D,[P,R],[],[],[],[],[Q]). ** KEPT (pick-wt=15): 712 [hyper,679,6,eval,demod,33,34] K2(B,D,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=15): 713 [hyper,679,5,demod,33,33,34] K2(B,D,[],[P,R],[],[],[],[Q]). given clause #647: (wt=15) 680 [hyper,678,12,demod,30,32,31,30,31] K1(B,D,[R],[],[P],[],[],[Q]). ** KEPT (pick-wt=15): 714 [hyper,680,5,demod,33,34] K2(B,D,[],[R],[P],[],[],[Q]). given clause #648: (wt=15) 681 [hyper,642,6,eval,demod,33,34] K2(E,D,[Q],[R],[],[],[],[P]). ** KEPT (pick-wt=14): 715 [hyper,681,17,demod,30,32,31,30,32,31] H(D,[],[],[],[R],[Q],[P]). given clause #649: (wt=14) 715 [hyper,681,17,demod,30,32,31,30,32,31] H(D,[],[],[],[R],[Q],[P]). ** KEPT (pick-wt=15): 716 [hyper,715,3] K1(D,E,[R],[Q],[],[],[],[P]). ** KEPT (pick-wt=15): 717 [hyper,715,2] K1(D,B,[R],[],[],[],[Q],[P]). given clause #650: (wt=15) 682 [hyper,642,5,demod,33,33,34] K2(E,D,[],[Q,R],[],[],[],[P]). given clause #651: (wt=15) 683 [hyper,643,5,demod,33,33,34] K2(E,F,[],[R,Q,P],[],[],[],[]). ** KEPT (pick-wt=14): 718 [hyper,683,11] H(F,[],[],[],[],[],[R,Q,P]). given clause #652: (wt=14) 718 [hyper,683,11] H(F,[],[],[],[],[],[R,Q,P]). ** KEPT (pick-wt=15): 719 [hyper,718,15,demod,30,32,32,32,31,30,31] K1(F,E,[P,Q,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 720 [hyper,718,14,demod,30,32,32,32,31,30,31] K1(F,C,[P,Q,R],[],[],[],[],[]). given clause #653: (wt=15) 684 [hyper,645,7] K2(E,D,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=14): 721 [hyper,684,17,demod,30,32,31,30,32,32,31] H(D,[],[],[],[R],[Q,P],[]). given clause #654: (wt=14) 721 [hyper,684,17,demod,30,32,31,30,32,32,31] H(D,[],[],[],[R],[Q,P],[]). ** KEPT (pick-wt=15): 722 [hyper,721,3] K1(D,E,[R],[Q,P],[],[],[],[]). ** KEPT (pick-wt=15): 723 [hyper,721,2] K1(D,B,[R],[],[],[],[Q,P],[]). given clause #655: (wt=15) 685 [hyper,645,6,eval,demod,33,33,34] K2(E,D,[P],[Q,R],[],[],[],[]). given clause #656: (wt=15) 686 [hyper,645,5,demod,33,33,33,34] K2(E,D,[],[P,Q,R],[],[],[],[]). ** KEPT (pick-wt=14): 724 [hyper,686,17,demod,30,32,32,32,31,30,31] H(D,[],[],[],[R,Q,P],[],[]). given clause #657: (wt=14) 724 [hyper,686,17,demod,30,32,32,32,31,30,31] H(D,[],[],[],[R,Q,P],[],[]). ** KEPT (pick-wt=15): 725 [hyper,724,3] K1(D,E,[R,Q,P],[],[],[],[],[]). ** KEPT (pick-wt=15): 726 [hyper,724,2] K1(D,B,[R,Q,P],[],[],[],[],[]). given clause #658: (wt=15) 687 [hyper,648,5,demod,33,33,33,34] K2(E,D,[],[R,P,Q],[],[],[],[]). ** KEPT (pick-wt=14): 727 [hyper,687,17,demod,30,32,32,32,31,30,31] H(D,[],[],[],[Q,P,R],[],[]). given clause #659: (wt=14) 727 [hyper,687,17,demod,30,32,32,32,31,30,31] H(D,[],[],[],[Q,P,R],[],[]). ** KEPT (pick-wt=15): 728 [hyper,727,3] K1(D,E,[Q,P,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 729 [hyper,727,2] K1(D,B,[Q,P,R],[],[],[],[],[]). given clause #660: (wt=15) 688 [hyper,649,7] K2(E,F,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=14): 730 [hyper,688,11] H(F,[],[],[],[],[Q,P],[R]). given clause #661: (wt=14) 730 [hyper,688,11] H(F,[],[],[],[],[Q,P],[R]). ** KEPT (pick-wt=15): 731 [hyper,730,15,demod,30,32,31,30,32,32,31] K1(F,E,[R],[P,Q],[],[],[],[]). ** KEPT (pick-wt=15): 732 [hyper,730,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[],[],[Q,P]). given clause #662: (wt=15) 689 [hyper,649,6,eval,demod,33,33,34] K2(E,F,[Q],[P,R],[],[],[],[]). given clause #663: (wt=15) 690 [hyper,649,5,demod,33,33,33,34] K2(E,F,[],[Q,P,R],[],[],[],[]). ** KEPT (pick-wt=14): 733 [hyper,690,11] H(F,[],[],[],[],[],[Q,P,R]). given clause #664: (wt=14) 733 [hyper,690,11] H(F,[],[],[],[],[],[Q,P,R]). ** KEPT (pick-wt=15): 734 [hyper,733,15,demod,30,32,32,32,31,30,31] K1(F,E,[R,P,Q],[],[],[],[],[]). ** KEPT (pick-wt=15): 735 [hyper,733,14,demod,30,32,32,32,31,30,31] K1(F,C,[R,P,Q],[],[],[],[],[]). given clause #665: (wt=15) 691 [hyper,651,5,demod,33,34] K2(C,F,[],[R],[],[],[P,Q],[]). given clause #666: (wt=15) 692 [hyper,653,5,demod,33,34] K2(C,F,[],[R],[],[],[P],[Q]). given clause #667: (wt=15) 693 [hyper,656,6,eval,demod,33,34] K2(C,F,[Q],[R],[],[],[P],[]). ** KEPT (pick-wt=14): 736 [hyper,693,8] H(F,[],[],[Q],[P],[],[R]). given clause #668: (wt=14) 736 [hyper,693,8] H(F,[],[],[Q],[P],[],[R]). ** KEPT (pick-wt=15): 737 [hyper,736,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[],[Q],[P]). ** KEPT (pick-wt=15): 738 [hyper,736,14,demod,30,32,31,30,32,31] K1(F,C,[R],[Q],[],[],[P],[]). given clause #669: (wt=15) 694 [hyper,656,5,demod,33,33,34] K2(C,F,[],[Q,R],[],[],[P],[]). given clause #670: (wt=15) 695 [hyper,657,5,demod,33,34] K2(C,F,[],[R],[Q],[],[P],[]). ** KEPT (pick-wt=14): 739 [hyper,695,8] H(F,[Q],[],[],[P],[],[R]). given clause #671: (wt=14) 739 [hyper,695,8] H(F,[Q],[],[],[P],[],[R]). ** KEPT (pick-wt=15): 740 [hyper,739,15,demod,30,32,31,30,31] K1(F,E,[R],[],[Q],[],[],[P]). ** KEPT (pick-wt=15): 741 [hyper,739,14,demod,30,32,31,30,31] K1(F,C,[R],[],[Q],[],[P],[]). given clause #672: (wt=15) 696 [hyper,659,5,demod,33,33,34] K2(E,D,[],[R,P],[],[],[Q],[]). ** KEPT (pick-wt=14): 742 [hyper,696,17,demod,30,32,32,31,30,31] H(D,[],[],[Q],[P,R],[],[]). given clause #673: (wt=14) 742 [hyper,696,17,demod,30,32,32,31,30,31] H(D,[],[],[Q],[P,R],[],[]). ** KEPT (pick-wt=15): 743 [hyper,742,3] K1(D,E,[P,R],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 744 [hyper,742,2] K1(D,B,[P,R],[],[],[Q],[],[]). given clause #674: (wt=15) 697 [hyper,660,6,eval,demod,33,34] K2(E,F,[P],[R],[],[],[Q],[]). given clause #675: (wt=15) 698 [hyper,660,5,demod,33,33,34] K2(E,F,[],[P,R],[],[],[Q],[]). ** KEPT (pick-wt=14): 745 [hyper,698,11] H(F,[],[],[Q],[],[],[P,R]). given clause #676: (wt=14) 745 [hyper,698,11] H(F,[],[],[Q],[],[],[P,R]). ** KEPT (pick-wt=15): 746 [hyper,745,15,demod,30,32,32,31,30,31] K1(F,E,[R,P],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 747 [hyper,745,14,demod,30,32,32,31,30,32,31] K1(F,C,[R,P],[Q],[],[],[],[]). given clause #677: (wt=15) 699 [hyper,662,5,demod,33,33,34] K2(E,D,[],[R,P],[Q],[],[],[]). ** KEPT (pick-wt=14): 748 [hyper,699,17,demod,30,32,32,31,30,31] H(D,[Q],[],[],[P,R],[],[]). given clause #678: (wt=14) 748 [hyper,699,17,demod,30,32,32,31,30,31] H(D,[Q],[],[],[P,R],[],[]). ** KEPT (pick-wt=15): 749 [hyper,748,3] K1(D,E,[P,R],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 750 [hyper,748,2] K1(D,B,[P,R],[],[Q],[],[],[]). given clause #679: (wt=15) 700 [hyper,663,6,eval,demod,33,34] K2(E,F,[P],[R],[Q],[],[],[]). given clause #680: (wt=15) 701 [hyper,663,5,demod,33,33,34] K2(E,F,[],[P,R],[Q],[],[],[]). ** KEPT (pick-wt=14): 751 [hyper,701,11] H(F,[Q],[],[],[],[],[P,R]). given clause #681: (wt=14) 751 [hyper,701,11] H(F,[Q],[],[],[],[],[P,R]). ** KEPT (pick-wt=15): 752 [hyper,751,15,demod,30,32,32,31,30,31] K1(F,E,[R,P],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 753 [hyper,751,14,demod,30,32,32,31,30,31] K1(F,C,[R,P],[],[Q],[],[],[]). given clause #682: (wt=15) 702 [hyper,666,6,eval,demod,33,34] K2(E,F,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=14): 754 [hyper,702,11] H(F,[],[],[],[Q],[P],[R]). given clause #683: (wt=14) 754 [hyper,702,11] H(F,[],[],[],[Q],[P],[R]). ** KEPT (pick-wt=15): 755 [hyper,754,15,demod,30,32,31,30,32,31] K1(F,E,[R],[P],[],[],[],[Q]). ** KEPT (pick-wt=15): 756 [hyper,754,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[],[Q],[P]). given clause #684: (wt=15) 703 [hyper,666,5,demod,33,33,34] K2(E,F,[],[P,R],[],[],[],[Q]). given clause #685: (wt=15) 704 [hyper,668,6,eval,demod,33,34] K2(E,D,[Q],[R],[],[P],[],[]). given clause #686: (wt=15) 705 [hyper,668,5,demod,33,33,34] K2(E,D,[],[Q,R],[],[P],[],[]). ** KEPT (pick-wt=14): 757 [hyper,705,17,demod,30,32,32,31,30,31] H(D,[],[P],[],[R,Q],[],[]). given clause #687: (wt=14) 757 [hyper,705,17,demod,30,32,32,31,30,31] H(D,[],[P],[],[R,Q],[],[]). ** KEPT (pick-wt=15): 758 [hyper,757,3] K1(D,E,[R,Q],[],[],[P],[],[]). ** KEPT (pick-wt=15): 759 [hyper,757,2] K1(D,B,[R,Q],[P],[],[],[],[]). given clause #688: (wt=15) 706 [hyper,669,5,demod,33,33,34] K2(E,F,[],[R,Q],[],[P],[],[]). ** KEPT (pick-wt=14): 760 [hyper,706,11] H(F,[],[P],[],[],[],[R,Q]). given clause #689: (wt=14) 760 [hyper,706,11] H(F,[],[P],[],[],[],[R,Q]). ** KEPT (pick-wt=15): 761 [hyper,760,15,demod,30,32,32,31,30,31] K1(F,E,[Q,R],[],[],[P],[],[]). ** KEPT (pick-wt=15): 762 [hyper,760,14,demod,30,32,32,31,30,31] K1(F,C,[Q,R],[],[],[P],[],[]). given clause #690: (wt=15) 707 [hyper,671,6,eval,demod,33,34] K2(E,D,[Q],[R],[P],[],[],[]). given clause #691: (wt=15) 708 [hyper,671,5,demod,33,33,34] K2(E,D,[],[Q,R],[P],[],[],[]). ** KEPT (pick-wt=14): 763 [hyper,708,17,demod,30,32,32,31,30,31] H(D,[P],[],[],[R,Q],[],[]). given clause #692: (wt=14) 763 [hyper,708,17,demod,30,32,32,31,30,31] H(D,[P],[],[],[R,Q],[],[]). ** KEPT (pick-wt=15): 764 [hyper,763,3] K1(D,E,[R,Q],[],[P],[],[],[]). ** KEPT (pick-wt=15): 765 [hyper,763,2] K1(D,B,[R,Q],[],[P],[],[],[]). given clause #693: (wt=15) 709 [hyper,672,5,demod,33,33,34] K2(E,F,[],[R,Q],[P],[],[],[]). ** KEPT (pick-wt=14): 766 [hyper,709,11] H(F,[P],[],[],[],[],[R,Q]). given clause #694: (wt=14) 766 [hyper,709,11] H(F,[P],[],[],[],[],[R,Q]). ** KEPT (pick-wt=15): 767 [hyper,766,15,demod,30,32,32,31,30,31] K1(F,E,[Q,R],[],[P],[],[],[]). ** KEPT (pick-wt=15): 768 [hyper,766,14,demod,30,32,32,31,30,31] K1(F,C,[Q,R],[],[P],[],[],[]). given clause #695: (wt=15) 710 [hyper,674,5,demod,33,34] K2(B,D,[],[R],[],[],[],[P,Q]). given clause #696: (wt=15) 711 [hyper,676,5,demod,33,34] K2(B,D,[],[R],[],[],[P],[Q]). given clause #697: (wt=15) 712 [hyper,679,6,eval,demod,33,34] K2(B,D,[P],[R],[],[],[],[Q]). ** KEPT (pick-wt=14): 769 [hyper,712,16,demod,30,32,31,30,32,31] H(D,[],[P],[],[R],[],[Q]). given clause #698: (wt=14) 769 [hyper,712,16,demod,30,32,31,30,32,31] H(D,[],[P],[],[R],[],[Q]). ** KEPT (pick-wt=15): 770 [hyper,769,3] K1(D,E,[R],[],[],[P],[],[Q]). ** KEPT (pick-wt=15): 771 [hyper,769,2] K1(D,B,[R],[P],[],[],[],[Q]). given clause #699: (wt=15) 713 [hyper,679,5,demod,33,33,34] K2(B,D,[],[P,R],[],[],[],[Q]). given clause #700: (wt=15) 714 [hyper,680,5,demod,33,34] K2(B,D,[],[R],[P],[],[],[Q]). ** KEPT (pick-wt=14): 772 [hyper,714,16,demod,30,31,30,32,31] H(D,[P],[],[],[R],[],[Q]). given clause #701: (wt=14) 772 [hyper,714,16,demod,30,31,30,32,31] H(D,[P],[],[],[R],[],[Q]). ** KEPT (pick-wt=15): 773 [hyper,772,3] K1(D,E,[R],[],[P],[],[],[Q]). ** KEPT (pick-wt=15): 774 [hyper,772,2] K1(D,B,[R],[],[P],[],[],[Q]). given clause #702: (wt=15) 716 [hyper,715,3] K1(D,E,[R],[Q],[],[],[],[P]). given clause #703: (wt=15) 717 [hyper,715,2] K1(D,B,[R],[],[],[],[Q],[P]). ** KEPT (pick-wt=15): 775 [hyper,717,5,demod,33,34] K2(D,B,[],[R],[],[],[Q],[P]). given clause #704: (wt=15) 719 [hyper,718,15,demod,30,32,32,32,31,30,31] K1(F,E,[P,Q,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 776 [hyper,719,7] K2(F,E,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=15): 777 [hyper,719,6,eval,demod,33,33,34] K2(F,E,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=15): 778 [hyper,719,5,demod,33,33,33,34] K2(F,E,[],[P,Q,R],[],[],[],[]). given clause #705: (wt=15) 720 [hyper,718,14,demod,30,32,32,32,31,30,31] K1(F,C,[P,Q,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 779 [hyper,720,7] K2(F,C,[P,Q],[R],[],[],[],[]). ** KEPT (pick-wt=15): 780 [hyper,720,6,eval,demod,33,33,34] K2(F,C,[P],[Q,R],[],[],[],[]). ** KEPT (pick-wt=15): 781 [hyper,720,5,demod,33,33,33,34] K2(F,C,[],[P,Q,R],[],[],[],[]). given clause #706: (wt=15) 722 [hyper,721,3] K1(D,E,[R],[Q,P],[],[],[],[]). given clause #707: (wt=15) 723 [hyper,721,2] K1(D,B,[R],[],[],[],[Q,P],[]). ** KEPT (pick-wt=15): 782 [hyper,723,5,demod,33,34] K2(D,B,[],[R],[],[],[Q,P],[]). given clause #708: (wt=15) 725 [hyper,724,3] K1(D,E,[R,Q,P],[],[],[],[],[]). given clause #709: (wt=15) 726 [hyper,724,2] K1(D,B,[R,Q,P],[],[],[],[],[]). ** KEPT (pick-wt=15): 783 [hyper,726,5,demod,33,33,33,34] K2(D,B,[],[R,Q,P],[],[],[],[]). given clause #710: (wt=15) 728 [hyper,727,3] K1(D,E,[Q,P,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 784 [hyper,728,7] K2(D,E,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=15): 785 [hyper,728,6,eval,demod,33,33,34] K2(D,E,[Q],[P,R],[],[],[],[]). ** KEPT (pick-wt=15): 786 [hyper,728,5,demod,33,33,33,34] K2(D,E,[],[Q,P,R],[],[],[],[]). given clause #711: (wt=15) 729 [hyper,727,2] K1(D,B,[Q,P,R],[],[],[],[],[]). ** KEPT (pick-wt=15): 787 [hyper,729,7] K2(D,B,[Q,P],[R],[],[],[],[]). ** KEPT (pick-wt=15): 788 [hyper,729,6,eval,demod,33,33,34] K2(D,B,[Q],[P,R],[],[],[],[]). ** KEPT (pick-wt=15): 789 [hyper,729,5,demod,33,33,33,34] K2(D,B,[],[Q,P,R],[],[],[],[]). given clause #712: (wt=15) 731 [hyper,730,15,demod,30,32,31,30,32,32,31] K1(F,E,[R],[P,Q],[],[],[],[]). given clause #713: (wt=15) 732 [hyper,730,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[],[],[Q,P]). ** KEPT (pick-wt=15): 790 [hyper,732,5,demod,33,34] K2(F,C,[],[R],[],[],[],[Q,P]). given clause #714: (wt=15) 734 [hyper,733,15,demod,30,32,32,32,31,30,31] K1(F,E,[R,P,Q],[],[],[],[],[]). given clause #715: (wt=15) 735 [hyper,733,14,demod,30,32,32,32,31,30,31] K1(F,C,[R,P,Q],[],[],[],[],[]). ** KEPT (pick-wt=15): 791 [hyper,735,5,demod,33,33,33,34] K2(F,C,[],[R,P,Q],[],[],[],[]). given clause #716: (wt=15) 737 [hyper,736,15,demod,30,32,31,30,31] K1(F,E,[R],[],[],[],[Q],[P]). ** KEPT (pick-wt=15): 792 [hyper,737,5,demod,33,34] K2(F,E,[],[R],[],[],[Q],[P]). given clause #717: (wt=15) 738 [hyper,736,14,demod,30,32,31,30,32,31] K1(F,C,[R],[Q],[],[],[P],[]). given clause #718: (wt=15) 740 [hyper,739,15,demod,30,32,31,30,31] K1(F,E,[R],[],[Q],[],[],[P]). ** KEPT (pick-wt=15): 793 [hyper,740,5,demod,33,34] K2(F,E,[],[R],[Q],[],[],[P]). given clause #719: (wt=15) 741 [hyper,739,14,demod,30,32,31,30,31] K1(F,C,[R],[],[Q],[],[P],[]). ** KEPT (pick-wt=15): 794 [hyper,741,5,demod,33,34] K2(F,C,[],[R],[Q],[],[P],[]). given clause #720: (wt=15) 743 [hyper,742,3] K1(D,E,[P,R],[],[],[],[Q],[]). ** KEPT (pick-wt=15): 795 [hyper,743,6,eval,demod,33,34] K2(D,E,[P],[R],[],[],[Q],[]). ** KEPT (pick-wt=15): 796 [hyper,743,5,demod,33,33,34] K2(D,E,[],[P,R],[],[],[Q],[]). given clause #721: (wt=15) 744 [hyper,742,2] K1(D,B,[P,R],[],[],[Q],[],[]). ** KEPT (pick-wt=15): 797 [hyper,744,6,eval,demod,33,34] K2(D,B,[P],[R],[],[Q],[],[]). ** KEPT (pick-wt=15): 798 [hyper,744,5,demod,33,33,34] K2(D,B,[],[P,R],[],[Q],[],[]). given clause #722: (wt=15) 746 [hyper,745,15,demod,30,32,32,31,30,31] K1(F,E,[R,P],[],[],[],[Q],[]). given clause #723: (wt=15) 747 [hyper,745,14,demod,30,32,32,31,30,32,31] K1(F,C,[R,P],[Q],[],[],[],[]). given clause #724: (wt=15) 749 [hyper,748,3] K1(D,E,[P,R],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 799 [hyper,749,6,eval,demod,33,34] K2(D,E,[P],[R],[Q],[],[],[]). ** KEPT (pick-wt=15): 800 [hyper,749,5,demod,33,33,34] K2(D,E,[],[P,R],[Q],[],[],[]). given clause #725: (wt=15) 750 [hyper,748,2] K1(D,B,[P,R],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 801 [hyper,750,6,eval,demod,33,34] K2(D,B,[P],[R],[Q],[],[],[]). ** KEPT (pick-wt=15): 802 [hyper,750,5,demod,33,33,34] K2(D,B,[],[P,R],[Q],[],[],[]). given clause #726: (wt=15) 752 [hyper,751,15,demod,30,32,32,31,30,31] K1(F,E,[R,P],[],[Q],[],[],[]). given clause #727: (wt=15) 753 [hyper,751,14,demod,30,32,32,31,30,31] K1(F,C,[R,P],[],[Q],[],[],[]). ** KEPT (pick-wt=15): 803 [hyper,753,5,demod,33,33,34] K2(F,C,[],[R,P],[Q],[],[],[]). given clause #728: (wt=15) 755 [hyper,754,15,demod,30,32,31,30,32,31] K1(F,E,[R],[P],[],[],[],[Q]). given clause #729: (wt=15) 756 [hyper,754,14,demod,30,32,31,30,31] K1(F,C,[R],[],[],[],[Q],[P]). ** KEPT (pick-wt=15): 804 [hy