============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13075 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:11 2006 The command was "/home/mccune/bin/prover9 -f HWV006-1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file HWV006-1.in set(prolog_style_variables). clauses(sos). - p9(A,c16) | p1(f12(c5,f19(A)),f11(c13,f17(A))). - p2(f12(c5,A),c4) | - p9(A,c15) | p2(f11(c5,A),c5) | - p6(A,c7). p1(f12(c22,A),f12(c5,f18(A))) | - p9(A,c16). p9(f25(A),c16) | - p9(A,c23). - p3(c4,c5). - p9(A,c16) | p1(f12(c5,f18(A)),f11(c5,f19(A))). p1(f12(c21,A),f12(c5,f17(A))) | - p9(A,c16). - p9(A,c23) | p1(f11(c5,A),f11(c5,f25(A))). - p6(A,c7) | - p2(f11(B,A),c5) | - p9(A,c14) | p2(f12(c5,A),c5). - p2(f12(c5,A),c4) | - p9(A,c14) | p2(f11(c5,A),c4) | - p6(A,c7). p2(f11(c13,A),c4) | - p2(f12(c5,A),c4) | p2(f11(c5,A),c4) | - p6(A,c7) | - p9(A,c10). p1(f12(c21,A),f12(c21,f25(A))) | - p9(A,c23). p6(A,c7) | - p9(A,B) | p6(A,c8). - p1(A,B) | p2(B,C) | - p2(A,C). - p6(A,c8) | - p6(A,c7). p2(A,B) | - p1(A,C) | - p2(C,B). - p9(A,c16) | p9(f19(A),c15). p2(f11(c5,A),c5) | - p2(f12(c5,A),c5) | - p6(A,c7) | p2(f11(c13,A),c5) | - p9(A,c14). p2(f12(c5,A),c5) | - p9(A,c10) | - p6(A,c7) | - p2(f11(c5,A),c5) | - p2(f11(c13,A),c5). p1(f11(c5,A),f11(c5,f20(A))) | - p9(A,c16). p9(f24(A),c16) | - p9(A,c23). - p9(A,c16) | p1(f12(c5,f20(A)),f11(c5,f17(A))). p1(f12(c21,f24(A)),f11(c13,f25(A))) | - p9(A,c23). p1(f11(c13,A),f11(c5,f24(A))) | - p9(A,c23). p1(f12(c22,f24(A)),f11(c13,f20(A))) | - p9(A,c23). - p9(A,c10) | - p2(f12(c5,A),c5) | - p6(A,c7) | p2(f11(c5,A),c5). p1(f12(c22,A),f12(c5,f20(A))) | - p9(A,c23). - p3(c5,c4). - p6(A,c7) | - p9(A,c10) | - p2(f12(c5,A),c5) | p2(f11(c13,A),c5). - p2(f12(c5,A),c4) | p2(f11(c13,A),c4) | - p6(A,c7) | - p9(A,c14). p2(f11(c5,A),c4) | - p2(f12(c5,A),c5) | - p6(A,c7) | - p9(A,c15). - p9(A,c16) | p1(f11(c13,A),f11(c13,f20(A))). - p2(f11(c13,A),c4) | - p9(A,c14) | p2(f12(c5,A),c4) | - p2(f11(c5,A),c4) | - p6(A,c7). p1(f11(c5,A),f11(c5,f18(A))) | - p9(A,c16). p9(f17(A),c10) | - p9(A,c16). p1(f11(c22,A),f11(c13,f24(A))) | - p9(A,c23). - p9(A,c16) | p1(f11(c13,A),f11(c13,f18(A))). p3(A,B) | - p2(C,B) | - p2(C,A). - p9(A,c23) | p9(f20(A),c14). p2(f12(c5,A),c4) | - p9(A,c10) | - p2(f11(B,A),c4) | - p6(A,c7). - p9(A,c23) | p1(f12(c22,f25(A)),f11(c5,f20(A))). p2(f12(c5,A),c5) | - p6(A,c7) | - p9(A,c15) | - p2(f11(c5,A),c4). p9(f20(A),c14) | - p9(A,c16). - p2(f11(c5,A),c5) | p2(f12(c5,A),c4) | - p9(A,c15) | - p6(A,c7). p9(f18(A),c10) | - p9(A,c16). - p6(f19(f24(c26)),c8). - p6(f17(f24(c26)),c8). - p6(f18(f25(c26)),c8). - p6(f18(f24(c26)),c8). - p6(f17(f25(c26)),c8) | - p6(f20(c26),c8). p2(f12(c21,c26),c5). p2(f11(c13,c26),c4). p2(f11(c22,c26),c5). p2(f11(c5,c26),c5). - p6(f20(f24(c26)),c8). p9(c26,c23). - p6(f19(f25(c26)),c8) | - p6(f20(c26),c8). p2(f12(c22,c26),c4). end_of_list. ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 - p9(A,c16) | p1(f12(c5,f19(A)),f11(c13,f17(A))). [input]. 2 - p2(f12(c5,A),c4) | - p9(A,c15) | p2(f11(c5,A),c5) | - p6(A,c7). [input]. 3 p1(f12(c22,A),f12(c5,f18(A))) | - p9(A,c16). [input]. 4 p9(f25(A),c16) | - p9(A,c23). [input]. 5 - p3(c4,c5). [input]. 6 - p9(A,c16) | p1(f12(c5,f18(A)),f11(c5,f19(A))). [input]. 7 p1(f12(c21,A),f12(c5,f17(A))) | - p9(A,c16). [input]. 8 - p9(A,c23) | p1(f11(c5,A),f11(c5,f25(A))). [input]. 9 - p6(A,c7) | - p2(f11(B,A),c5) | - p9(A,c14) | p2(f12(c5,A),c5). [input]. 10 - p2(f12(c5,A),c4) | - p9(A,c14) | p2(f11(c5,A),c4) | - p6(A,c7). [input]. 11 p2(f11(c13,A),c4) | - p2(f12(c5,A),c4) | p2(f11(c5,A),c4) | - p6(A,c7) | - p9(A,c10). [input]. 12 p1(f12(c21,A),f12(c21,f25(A))) | - p9(A,c23). [input]. 13 p6(A,c7) | - p9(A,B) | p6(A,c8). [input]. 14 - p1(A,B) | p2(B,C) | - p2(A,C). [input]. 15 - p6(A,c8) | - p6(A,c7). [input]. 16 p2(A,B) | - p1(A,C) | - p2(C,B). [input]. 17 - p9(A,c16) | p9(f19(A),c15). [input]. 18 p2(f11(c5,A),c5) | - p2(f12(c5,A),c5) | - p6(A,c7) | p2(f11(c13,A),c5) | - p9(A,c14). [input]. 19 p2(f12(c5,A),c5) | - p9(A,c10) | - p6(A,c7) | - p2(f11(c5,A),c5) | - p2(f11(c13,A),c5). [input]. 20 p1(f11(c5,A),f11(c5,f20(A))) | - p9(A,c16). [input]. 21 p9(f24(A),c16) | - p9(A,c23). [input]. 22 - p9(A,c16) | p1(f12(c5,f20(A)),f11(c5,f17(A))). [input]. 23 p1(f12(c21,f24(A)),f11(c13,f25(A))) | - p9(A,c23). [input]. 24 p1(f11(c13,A),f11(c5,f24(A))) | - p9(A,c23). [input]. 25 p1(f12(c22,f24(A)),f11(c13,f20(A))) | - p9(A,c23). [input]. 26 - p9(A,c10) | - p2(f12(c5,A),c5) | - p6(A,c7) | p2(f11(c5,A),c5). [input]. 27 p1(f12(c22,A),f12(c5,f20(A))) | - p9(A,c23). [input]. 28 - p3(c5,c4). [input]. 29 - p6(A,c7) | - p9(A,c10) | - p2(f12(c5,A),c5) | p2(f11(c13,A),c5). [input]. 30 - p2(f12(c5,A),c4) | p2(f11(c13,A),c4) | - p6(A,c7) | - p9(A,c14). [input]. 31 p2(f11(c5,A),c4) | - p2(f12(c5,A),c5) | - p6(A,c7) | - p9(A,c15). [input]. 32 - p9(A,c16) | p1(f11(c13,A),f11(c13,f20(A))). [input]. 33 - p2(f11(c13,A),c4) | - p9(A,c14) | p2(f12(c5,A),c4) | - p2(f11(c5,A),c4) | - p6(A,c7). [input]. 34 p1(f11(c5,A),f11(c5,f18(A))) | - p9(A,c16). [input]. 35 p9(f17(A),c10) | - p9(A,c16). [input]. 36 p1(f11(c22,A),f11(c13,f24(A))) | - p9(A,c23). [input]. 37 - p9(A,c16) | p1(f11(c13,A),f11(c13,f18(A))). [input]. 38 p3(A,B) | - p2(C,B) | - p2(C,A). [input]. 39 - p9(A,c23) | p9(f20(A),c14). [input]. 40 p2(f12(c5,A),c4) | - p9(A,c10) | - p2(f11(B,A),c4) | - p6(A,c7). [input]. 41 - p9(A,c23) | p1(f12(c22,f25(A)),f11(c5,f20(A))). [input]. 42 p2(f12(c5,A),c5) | - p6(A,c7) | - p9(A,c15) | - p2(f11(c5,A),c4). [input]. 43 p9(f20(A),c14) | - p9(A,c16). [input]. 44 - p2(f11(c5,A),c5) | p2(f12(c5,A),c4) | - p9(A,c15) | - p6(A,c7). [input]. 45 p9(f18(A),c10) | - p9(A,c16). [input]. 46 - p6(f19(f24(c26)),c8). [input]. 47 - p6(f17(f24(c26)),c8). [input]. 48 - p6(f18(f25(c26)),c8). [input]. 49 - p6(f18(f24(c26)),c8). [input]. 50 - p6(f17(f25(c26)),c8) | - p6(f20(c26),c8). [input]. 51 p2(f12(c21,c26),c5). [input]. 52 p2(f11(c13,c26),c4). [input]. 53 p2(f11(c22,c26),c5). [input]. 54 p2(f11(c5,c26),c5). [input]. 55 - p6(f20(f24(c26)),c8). [input]. 56 p9(c26,c23). [input]. 57 - p6(f19(f25(c26)),c8) | - p6(f20(c26),c8). [input]. 58 p2(f12(c22,c26),c4). [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: p1/2 p3/2. Auto_denials: no changes. Term ordering decisions: Relation symbol precedence: lex([ p2, p9, p6, p3, p1 ]). Function symbol precedence: lex([ c5, c13, c16, c23, c4, c7, c22, c21, c10, c14, c26, c15, c8, f11, f12, f20, f18, f24, f25, f17, f19 ]). After inverse_order: Function symbol precedence: lex([ c5, c13, c16, c23, c4, c7, c22, c21, c10, c14, c26, c15, c8, f11, f12, f20, f18, f24, f25, f17, f19 ]). Unfolding symbols: (none). Auto_inference settings: % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 95 - p2(f12(c5,A),c4) | - p9(A,c15) | p2(f11(c5,A),c5) | - p6(A,c7). [input]. 96 p9(f25(A),c16) | - p9(A,c23). [input]. 97 - p6(A,c7) | - p2(f11(B,A),c5) | - p9(A,c14) | p2(f12(c5,A),c5). [input]. 98 - p2(f12(c5,A),c4) | - p9(A,c14) | p2(f11(c5,A),c4) | - p6(A,c7). [input]. 99 p2(f11(c13,A),c4) | - p2(f12(c5,A),c4) | p2(f11(c5,A),c4) | - p6(A,c7) | - p9(A,c10). [input]. 100 p6(A,c7) | - p9(A,B) | p6(A,c8). [input]. 101 - p6(A,c8) | - p6(A,c7). [input]. 102 - p9(A,c16) | p9(f19(A),c15). [input]. 103 p2(f11(c5,A),c5) | - p2(f12(c5,A),c5) | - p6(A,c7) | p2(f11(c13,A),c5) | - p9(A,c14). [input]. 104 p2(f12(c5,A),c5) | - p9(A,c10) | - p6(A,c7) | - p2(f11(c5,A),c5) | - p2(f11(c13,A),c5). [input]. 105 p9(f24(A),c16) | - p9(A,c23). [input]. 106 - p9(A,c10) | - p2(f12(c5,A),c5) | - p6(A,c7) | p2(f11(c5,A),c5). [input]. 107 - p6(A,c7) | - p9(A,c10) | - p2(f12(c5,A),c5) | p2(f11(c13,A),c5). [input]. 108 - p2(f12(c5,A),c4) | p2(f11(c13,A),c4) | - p6(A,c7) | - p9(A,c14). [input]. 109 p2(f11(c5,A),c4) | - p2(f12(c5,A),c5) | - p6(A,c7) | - p9(A,c15). [input]. 110 - p2(f11(c13,A),c4) | - p9(A,c14) | p2(f12(c5,A),c4) | - p2(f11(c5,A),c4) | - p6(A,c7). [input]. 111 p9(f17(A),c10) | - p9(A,c16). [input]. 112 - p9(A,c23) | p9(f20(A),c14). [input]. 113 p2(f12(c5,A),c4) | - p9(A,c10) | - p2(f11(B,A),c4) | - p6(A,c7). [input]. 114 p2(f12(c5,A),c5) | - p6(A,c7) | - p9(A,c15) | - p2(f11(c5,A),c4). [input]. 115 p9(f20(A),c14) | - p9(A,c16). [input]. 116 - p2(f11(c5,A),c5) | p2(f12(c5,A),c4) | - p9(A,c15) | - p6(A,c7). [input]. 117 p9(f18(A),c10) | - p9(A,c16). [input]. 118 - p6(f19(f24(c26)),c8). [input]. 119 - p6(f17(f24(c26)),c8). [input]. 120 - p6(f18(f25(c26)),c8). [input]. 121 - p6(f18(f24(c26)),c8). [input]. 122 - p6(f17(f25(c26)),c8) | - p6(f20(c26),c8). [input]. 123 p2(f12(c21,c26),c5). [input]. 124 p2(f11(c13,c26),c4). [input]. 125 p2(f11(c22,c26),c5). [input]. 126 p2(f11(c5,c26),c5). [input]. 127 - p6(f20(f24(c26)),c8). [input]. 128 p9(c26,c23). [input]. 129 - p6(f19(f25(c26)),c8) | - p6(f20(c26),c8). [input]. 130 p2(f12(c22,c26),c4). [input]. 131 p2(f11(c13,f17(A)),B) | - p2(f12(c5,f19(A)),B) | - p9(A,c16). [resolve(14,a,1,b)]. 132 p2(f12(c5,f18(A)),B) | - p2(f12(c22,A),B) | - p9(A,c16). [resolve(14,a,3,a)]. 133 p2(f11(c5,f19(A)),B) | - p2(f12(c5,f18(A)),B) | - p9(A,c16). [resolve(14,a,6,b)]. 134 p2(f12(c5,f17(A)),B) | - p2(f12(c21,A),B) | - p9(A,c16). [resolve(14,a,7,a)]. 135 p2(f11(c5,f25(A)),B) | - p2(f11(c5,A),B) | - p9(A,c23). [resolve(14,a,8,b)]. 136 p2(f12(c21,f25(A)),B) | - p2(f12(c21,A),B) | - p9(A,c23). [resolve(14,a,12,a)]. 137 p2(f12(c5,f19(A)),B) | - p2(f11(c13,f17(A)),B) | - p9(A,c16). [resolve(16,b,1,b)]. 138 p2(f12(c22,A),B) | - p2(f12(c5,f18(A)),B) | - p9(A,c16). [resolve(16,b,3,a)]. 139 p2(f12(c5,f18(A)),B) | - p2(f11(c5,f19(A)),B) | - p9(A,c16). [resolve(16,b,6,b)]. 140 p2(f12(c21,A),B) | - p2(f12(c5,f17(A)),B) | - p9(A,c16). [resolve(16,b,7,a)]. 141 p2(f11(c5,A),B) | - p2(f11(c5,f25(A)),B) | - p9(A,c23). [resolve(16,b,8,b)]. 142 p2(f12(c21,A),B) | - p2(f12(c21,f25(A)),B) | - p9(A,c23). [resolve(16,b,12,a)]. 143 - p9(A,c16) | p2(f11(c5,f20(A)),B) | - p2(f11(c5,A),B). [resolve(20,a,14,a)]. 144 - p9(A,c16) | p2(f11(c5,A),B) | - p2(f11(c5,f20(A)),B). [resolve(20,a,16,b)]. 145 - p9(A,c16) | p2(f11(c5,f17(A)),B) | - p2(f12(c5,f20(A)),B). [resolve(22,b,14,a)]. 146 - p9(A,c16) | p2(f12(c5,f20(A)),B) | - p2(f11(c5,f17(A)),B). [resolve(22,b,16,b)]. 147 - p9(A,c23) | p2(f11(c13,f25(A)),B) | - p2(f12(c21,f24(A)),B). [resolve(23,a,14,a)]. 148 - p9(A,c23) | p2(f12(c21,f24(A)),B) | - p2(f11(c13,f25(A)),B). [resolve(23,a,16,b)]. 149 - p9(A,c23) | p2(f11(c5,f24(A)),B) | - p2(f11(c13,A),B). [resolve(24,a,14,a)]. 150 - p9(A,c23) | p2(f11(c13,A),B) | - p2(f11(c5,f24(A)),B). [resolve(24,a,16,b)]. 151 - p9(A,c23) | p2(f11(c13,f20(A)),B) | - p2(f12(c22,f24(A)),B). [resolve(25,a,14,a)]. 152 - p9(A,c23) | p2(f12(c22,f24(A)),B) | - p2(f11(c13,f20(A)),B). [resolve(25,a,16,b)]. 153 - p9(A,c23) | p2(f12(c5,f20(A)),B) | - p2(f12(c22,A),B). [resolve(27,a,14,a)]. 154 - p9(A,c23) | p2(f12(c22,A),B) | - p2(f12(c5,f20(A)),B). [resolve(27,a,16,b)]. 155 - p9(A,c16) | p2(f11(c13,f20(A)),B) | - p2(f11(c13,A),B). [resolve(32,b,14,a)]. 156 - p9(A,c16) | p2(f11(c13,A),B) | - p2(f11(c13,f20(A)),B). [resolve(32,b,16,b)]. 157 - p9(A,c16) | p2(f11(c5,f18(A)),B) | - p2(f11(c5,A),B). [resolve(34,a,14,a)]. 158 - p9(A,c16) | p2(f11(c5,A),B) | - p2(f11(c5,f18(A)),B). [resolve(34,a,16,b)]. 159 - p9(A,c23) | p2(f11(c13,f24(A)),B) | - p2(f11(c22,A),B). [resolve(36,a,14,a)]. 160 - p9(A,c23) | p2(f11(c22,A),B) | - p2(f11(c13,f24(A)),B). [resolve(36,a,16,b)]. 161 - p9(A,c16) | p2(f11(c13,f18(A)),B) | - p2(f11(c13,A),B). [resolve(37,b,14,a)]. 162 - p9(A,c16) | p2(f11(c13,A),B) | - p2(f11(c13,f18(A)),B). [resolve(37,b,16,b)]. 163 - p9(A,c23) | p2(f11(c5,f20(A)),B) | - p2(f12(c22,f25(A)),B). [resolve(41,b,14,a)]. 164 - p9(A,c23) | p2(f12(c22,f25(A)),B) | - p2(f11(c5,f20(A)),B). [resolve(41,b,16,b)]. 165 - p2(A,c5) | - p2(A,c4). [resolve(38,a,5,a)]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=16): 95 - p2(f12(c5,A),c4) | - p9(A,c15) | p2(f11(c5,A),c5) | - p6(A,c7). [input]. given #2 (I,wt=7): 96 p9(f25(A),c16) | - p9(A,c23). [input]. given #3 (I,wt=16): 97 - p6(A,c7) | - p2(f11(B,A),c5) | - p9(A,c14) | p2(f12(c5,A),c5). [input]. given #4 (I,wt=16): 98 - p2(f12(c5,A),c4) | - p9(A,c14) | p2(f11(c5,A),c4) | - p6(A,c7). [input]. given #5 (I,wt=21): 99 p2(f11(c13,A),c4) | - p2(f12(c5,A),c4) | p2(f11(c5,A),c4) | - p6(A,c7) | - p9(A,c10). [input]. given #6 (I,wt=9): 100 p6(A,c7) | - p9(A,B) | p6(A,c8). [input]. given #7 (I,wt=6): 101 - p6(A,c8) | - p6(A,c7). [input]. given #8 (I,wt=7): 102 - p9(A,c16) | p9(f19(A),c15). [input]. given #9 (I,wt=21): 103 p2(f11(c5,A),c5) | - p2(f12(c5,A),c5) | - p6(A,c7) | p2(f11(c13,A),c5) | - p9(A,c14). [input]. given #10 (I,wt=21): 104 p2(f12(c5,A),c5) | - p9(A,c10) | - p6(A,c7) | - p2(f11(c5,A),c5) | - p2(f11(c13,A),c5). [input]. given #11 (I,wt=7): 105 p9(f24(A),c16) | - p9(A,c23). [input]. given #12 (I,wt=16): 106 - p9(A,c10) | - p2(f12(c5,A),c5) | - p6(A,c7) | p2(f11(c5,A),c5). [input]. given #13 (I,wt=16): 107 - p6(A,c7) | - p9(A,c10) | - p2(f12(c5,A),c5) | p2(f11(c13,A),c5). [input]. given #14 (I,wt=16): 108 - p2(f12(c5,A),c4) | p2(f11(c13,A),c4) | - p6(A,c7) | - p9(A,c14). [input]. given #15 (I,wt=16): 109 p2(f11(c5,A),c4) | - p2(f12(c5,A),c5) | - p6(A,c7) | - p9(A,c15). [input]. given #16 (I,wt=21): 110 - p2(f11(c13,A),c4) | - p9(A,c14) | p2(f12(c5,A),c4) | - p2(f11(c5,A),c4) | - p6(A,c7). [input]. given #17 (I,wt=7): 111 p9(f17(A),c10) | - p9(A,c16). [input]. given #18 (I,wt=7): 112 - p9(A,c23) | p9(f20(A),c14). [input]. given #19 (I,wt=16): 113 p2(f12(c5,A),c4) | - p9(A,c10) | - p2(f11(B,A),c4) | - p6(A,c7). [input]. given #20 (I,wt=16): 114 p2(f12(c5,A),c5) | - p6(A,c7) | - p9(A,c15) | - p2(f11(c5,A),c4). [input]. given #21 (I,wt=7): 115 p9(f20(A),c14) | - p9(A,c16). [input]. given #22 (I,wt=16): 116 - p2(f11(c5,A),c5) | p2(f12(c5,A),c4) | - p9(A,c15) | - p6(A,c7). [input]. given #23 (I,wt=7): 117 p9(f18(A),c10) | - p9(A,c16). [input]. given #24 (I,wt=5): 118 - p6(f19(f24(c26)),c8). [input]. given #25 (I,wt=5): 119 - p6(f17(f24(c26)),c8). [input]. given #26 (I,wt=5): 120 - p6(f18(f25(c26)),c8). [input]. given #27 (I,wt=5): 121 - p6(f18(f24(c26)),c8). [input]. given #28 (I,wt=9): 122 - p6(f17(f25(c26)),c8) | - p6(f20(c26),c8). [input]. given #29 (I,wt=5): 123 p2(f12(c21,c26),c5). [input]. given #30 (I,wt=5): 124 p2(f11(c13,c26),c4). [input]. given #31 (I,wt=5): 125 p2(f11(c22,c26),c5). [input]. given #32 (I,wt=5): 126 p2(f11(c5,c26),c5). [input]. given #33 (I,wt=5): 127 - p6(f20(f24(c26)),c8). [input]. given #34 (I,wt=3): 128 p9(c26,c23). [input]. given #35 (I,wt=9): 129 - p6(f19(f25(c26)),c8) | - p6(f20(c26),c8). [input]. given #36 (I,wt=5): 130 p2(f12(c22,c26),c4). [input]. given #37 (I,wt=15): 131 p2(f11(c13,f17(A)),B) | - p2(f12(c5,f19(A)),B) | - p9(A,c16). [resolve(14,a,1,b)]. given #38 (I,wt=14): 132 p2(f12(c5,f18(A)),B) | - p2(f12(c22,A),B) | - p9(A,c16). [resolve(14,a,3,a)]. given #39 (I,wt=15): 133 p2(f11(c5,f19(A)),B) | - p2(f12(c5,f18(A)),B) | - p9(A,c16). [resolve(14,a,6,b)]. given #40 (I,wt=14): 134 p2(f12(c5,f17(A)),B) | - p2(f12(c21,A),B) | - p9(A,c16). [resolve(14,a,7,a)]. given #41 (I,wt=14): 135 p2(f11(c5,f25(A)),B) | - p2(f11(c5,A),B) | - p9(A,c23). [resolve(14,a,8,b)]. given #42 (I,wt=14): 136 p2(f12(c21,f25(A)),B) | - p2(f12(c21,A),B) | - p9(A,c23). [resolve(14,a,12,a)]. given #43 (I,wt=15): 137 p2(f12(c5,f19(A)),B) | - p2(f11(c13,f17(A)),B) | - p9(A,c16). [resolve(16,b,1,b)]. given #44 (I,wt=14): 138 p2(f12(c22,A),B) | - p2(f12(c5,f18(A)),B) | - p9(A,c16). [resolve(16,b,3,a)]. given #45 (I,wt=15): 139 p2(f12(c5,f18(A)),B) | - p2(f11(c5,f19(A)),B) | - p9(A,c16). [resolve(16,b,6,b)]. given #46 (I,wt=14): 140 p2(f12(c21,A),B) | - p2(f12(c5,f17(A)),B) | - p9(A,c16). [resolve(16,b,7,a)]. given #47 (I,wt=14): 141 p2(f11(c5,A),B) | - p2(f11(c5,f25(A)),B) | - p9(A,c23). [resolve(16,b,8,b)]. given #48 (I,wt=14): 142 p2(f12(c21,A),B) | - p2(f12(c21,f25(A)),B) | - p9(A,c23). [resolve(16,b,12,a)]. given #49 (I,wt=14): 143 - p9(A,c16) | p2(f11(c5,f20(A)),B) | - p2(f11(c5,A),B). [resolve(20,a,14,a)]. given #50 (I,wt=14): 144 - p9(A,c16) | p2(f11(c5,A),B) | - p2(f11(c5,f20(A)),B). [resolve(20,a,16,b)]. given #51 (I,wt=15): 145 - p9(A,c16) | p2(f11(c5,f17(A)),B) | - p2(f12(c5,f20(A)),B). [resolve(22,b,14,a)]. given #52 (I,wt=15): 146 - p9(A,c16) | p2(f12(c5,f20(A)),B) | - p2(f11(c5,f17(A)),B). [resolve(22,b,16,b)]. given #53 (I,wt=15): 147 - p9(A,c23) | p2(f11(c13,f25(A)),B) | - p2(f12(c21,f24(A)),B). [resolve(23,a,14,a)]. given #54 (I,wt=15): 148 - p9(A,c23) | p2(f12(c21,f24(A)),B) | - p2(f11(c13,f25(A)),B). [resolve(23,a,16,b)]. given #55 (I,wt=14): 149 - p9(A,c23) | p2(f11(c5,f24(A)),B) | - p2(f11(c13,A),B). [resolve(24,a,14,a)]. given #56 (I,wt=14): 150 - p9(A,c23) | p2(f11(c13,A),B) | - p2(f11(c5,f24(A)),B). [resolve(24,a,16,b)]. given #57 (I,wt=15): 151 - p9(A,c23) | p2(f11(c13,f20(A)),B) | - p2(f12(c22,f24(A)),B). [resolve(25,a,14,a)]. given #58 (I,wt=15): 152 - p9(A,c23) | p2(f12(c22,f24(A)),B) | - p2(f11(c13,f20(A)),B). [resolve(25,a,16,b)]. given #59 (I,wt=14): 153 - p9(A,c23) | p2(f12(c5,f20(A)),B) | - p2(f12(c22,A),B). [resolve(27,a,14,a)]. given #60 (I,wt=14): 154 - p9(A,c23) | p2(f12(c22,A),B) | - p2(f12(c5,f20(A)),B). [resolve(27,a,16,b)]. given #61 (I,wt=14): 155 - p9(A,c16) | p2(f11(c13,f20(A)),B) | - p2(f11(c13,A),B). [resolve(32,b,14,a)]. given #62 (I,wt=14): 156 - p9(A,c16) | p2(f11(c13,A),B) | - p2(f11(c13,f20(A)),B). [resolve(32,b,16,b)]. given #63 (I,wt=14): 157 - p9(A,c16) | p2(f11(c5,f18(A)),B) | - p2(f11(c5,A),B). [resolve(34,a,14,a)]. given #64 (I,wt=14): 158 - p9(A,c16) | p2(f11(c5,A),B) | - p2(f11(c5,f18(A)),B). [resolve(34,a,16,b)]. given #65 (I,wt=14): 159 - p9(A,c23) | p2(f11(c13,f24(A)),B) | - p2(f11(c22,A),B). [resolve(36,a,14,a)]. given #66 (I,wt=14): 160 - p9(A,c23) | p2(f11(c22,A),B) | - p2(f11(c13,f24(A)),B). [resolve(36,a,16,b)]. given #67 (I,wt=14): 161 - p9(A,c16) | p2(f11(c13,f18(A)),B) | - p2(f11(c13,A),B). [resolve(37,b,14,a)]. given #68 (I,wt=14): 162 - p9(A,c16) | p2(f11(c13,A),B) | - p2(f11(c13,f18(A)),B). [resolve(37,b,16,b)]. given #69 (I,wt=15): 163 - p9(A,c23) | p2(f11(c5,f20(A)),B) | - p2(f12(c22,f25(A)),B). [resolve(41,b,14,a)]. given #70 (I,wt=15): 164 - p9(A,c23) | p2(f12(c22,f25(A)),B) | - p2(f11(c5,f20(A)),B). [resolve(41,b,16,b)]. given #71 (I,wt=6): 165 - p2(A,c5) | - p2(A,c4). [resolve(38,a,5,a)]. given #72 (F,wt=5): 186 - p2(f12(c22,c26),c5). [resolve(165,b,130,a)]. given #73 (F,wt=5): 187 - p2(f11(c13,c26),c5). [resolve(165,b,124,a)]. given #74 (T,wt=4): 166 p9(f20(c26),c14). [resolve(128,a,112,a)]. given #75 (T,wt=4): 167 p9(f24(c26),c16). [resolve(128,a,105,b)]. given #76 (A,wt=6): 168 p6(c26,c7) | p6(c26,c8). [resolve(128,a,100,b)]. given #77 (F,wt=5): 188 - p2(f11(c5,c26),c4). [ur(165,a,126,a)]. given #78 (F,wt=5): 189 - p2(f11(c22,c26),c4). [ur(165,a,125,a)]. given #79 (T,wt=4): 169 p9(f25(c26),c16). [resolve(128,a,96,b)]. given #80 (T,wt=5): 212 p9(f18(f24(c26)),c10). [resolve(167,a,117,b)]. given #81 (A,wt=11): 170 p2(f11(c5,f25(c26)),A) | - p2(f11(c5,c26),A). [resolve(135,c,128,a)]. given #82 (F,wt=5): 190 - p2(f12(c21,c26),c4). [ur(165,a,123,a)]. given #83 (F,wt=6): 191 - p2(f12(c5,f20(c26)),c5). [ur(154,a,128,a,b,186,a)]. given #84 (T,wt=5): 213 p9(f20(f24(c26)),c14). [resolve(167,a,115,b)]. given #85 (T,wt=5): 214 p9(f17(f24(c26)),c10). [resolve(167,a,111,b)]. given #86 (A,wt=11): 171 p2(f12(c21,f25(c26)),A) | - p2(f12(c21,c26),A). [resolve(136,c,128,a)]. given #87 (F,wt=6): 192 - p2(f11(c5,f24(c26)),c5). [ur(150,a,128,a,b,187,a)]. given #88 (F,wt=6): 217 - p2(f11(c5,f25(c26)),c4). [ur(141,a,188,a,c,128,a)]. given #89 (T,wt=5): 215 p9(f19(f24(c26)),c15). [resolve(167,a,102,a)]. given #90 (T,wt=5): 237 p9(f18(f25(c26)),c10). [resolve(169,a,117,b)]. given #91 (A,wt=11): 172 p2(f11(c5,c26),A) | - p2(f11(c5,f25(c26)),A). [resolve(141,c,128,a)]. given #92 (F,wt=6): 218 - p2(f11(c13,f24(c26)),c4). [ur(160,a,128,a,b,189,a)]. given #93 (F,wt=6): 244 - p2(f12(c21,f25(c26)),c4). [ur(142,a,190,a,c,128,a)]. given #94 (T,wt=5): 238 p9(f20(f25(c26)),c14). [resolve(169,a,115,b)]. given #95 (T,wt=5): 239 p9(f17(f25(c26)),c10). [resolve(169,a,111,b)]. given #96 (A,wt=11): 173 p2(f12(c21,c26),A) | - p2(f12(c21,f25(c26)),A). [resolve(142,c,128,a)]. given #97 (F,wt=7): 248 - p2(f11(c5,f18(f24(c26))),c5). [ur(158,a,167,a,b,192,a)]. given #98 (F,wt=7): 249 - p2(f11(c5,f20(f24(c26))),c5). [ur(144,a,167,a,b,192,a)]. given #99 (T,wt=5): 240 p9(f19(f25(c26)),c15). [resolve(169,a,102,a)]. given #100 (T,wt=5): 242 p6(f18(f24(c26)),c7). [resolve(212,a,100,b),unit_del(b,121)]. given #101 (A,wt=12): 174 p2(f11(c13,f25(c26)),A) | - p2(f12(c21,f24(c26)),A). [resolve(147,a,128,a)]. given #102 (F,wt=7): 250 - p2(f11(c5,f18(f25(c26))),c4). [ur(158,a,169,a,b,217,a)]. given #103 (F,wt=7): 251 - p2(f11(c5,f20(f25(c26))),c4). [ur(144,a,169,a,b,217,a)]. given #104 (T,wt=5): 245 p6(f20(f24(c26)),c7). [resolve(213,a,100,b),unit_del(b,127)]. given #105 (T,wt=5): 246 p6(f17(f24(c26)),c7). [resolve(214,a,100,b),unit_del(b,119)]. given #106 (A,wt=12): 175 p2(f12(c21,f24(c26)),A) | - p2(f11(c13,f25(c26)),A). [resolve(148,a,128,a)]. given #107 (F,wt=7): 254 - p2(f11(c13,f18(f24(c26))),c4). [ur(162,a,167,a,b,218,a)]. given #108 (F,wt=7): 255 - p2(f11(c13,f20(f24(c26))),c4). [ur(156,a,167,a,b,218,a)]. given #109 (T,wt=5): 252 p6(f19(f24(c26)),c7). [resolve(215,a,100,b),unit_del(b,118)]. given #110 (T,wt=5): 253 p6(f18(f25(c26)),c7). [resolve(237,a,100,b),unit_del(b,120)]. given #111 (A,wt=11): 176 p2(f11(c5,f24(c26)),A) | - p2(f11(c13,c26),A). [resolve(149,a,128,a)]. given #112 (F,wt=7): 256 - p2(f12(c5,f17(f25(c26))),c4). [ur(140,a,244,a,c,169,a)]. given #113 (F,wt=7): 265 - p2(f12(c5,f18(f24(c26))),c5). [resolve(242,a,106,c),unit_del(a,212),unit_del(c,248)]. given #114 (T,wt=6): 243 p2(f11(c5,f25(c26)),c5). [resolve(170,b,126,a)]. given #115 (T,wt=6): 247 p2(f12(c21,f25(c26)),c5). [resolve(171,b,123,a)]. given #116 (A,wt=11): 177 p2(f11(c13,c26),A) | - p2(f11(c5,f24(c26)),A). [resolve(150,a,128,a)]. given #117 (F,wt=6): 318 - p2(f12(c22,f24(c26)),c5). [ur(132,a,265,a,c,167,a)]. given #118 (F,wt=6): 324 - p2(f11(c13,f20(c26)),c5). [ur(152,a,128,a,b,318,a)]. given #119 (T,wt=6): 316 p2(f11(c5,f24(c26)),c4). [resolve(176,b,124,a)]. given #120 (T,wt=8): 193 p6(f20(c26),c7) | p6(f20(c26),c8). [resolve(166,a,100,b)]. given #121 (A,wt=12): 178 p2(f11(c13,f20(c26)),A) | - p2(f12(c22,f24(c26)),A). [resolve(151,a,128,a)]. given #122 (F,wt=7): 273 - p2(f12(c5,f20(f24(c26))),c4). [resolve(245,a,108,c),unit_del(b,255),unit_del(c,213)]. given #123 (F,wt=7): 317 - p2(f11(c5,f19(f24(c26))),c5). [ur(139,a,265,a,c,167,a)]. given #124 (T,wt=8): 216 p6(f24(c26),c7) | p6(f24(c26),c8). [resolve(167,a,100,b)]. given #125 (T,wt=8): 241 p6(f25(c26),c7) | p6(f25(c26),c8). [resolve(169,a,100,b)]. given #126 (A,wt=12): 179 p2(f12(c22,f24(c26)),A) | - p2(f11(c13,f20(c26)),A). [resolve(152,a,128,a)]. given #127 (F,wt=7): 319 - p2(f12(c5,f19(f24(c26))),c4). [back_unit_del(304),unit_del(b,317)]. given #128 (F,wt=7): 330 - p2(f12(c5,f17(f24(c26))),c4). [back_unit_del(327),unit_del(a,329)]. given #129 (T,wt=10): 257 p6(f20(f25(c26)),c7) | p6(f20(f25(c26)),c8). [resolve(238,a,100,b)]. given #130 (T,wt=10): 258 p6(f17(f25(c26)),c7) | p6(f17(f25(c26)),c8). [resolve(239,a,100,b)]. given #131 (A,wt=11): 180 p2(f12(c5,f20(c26)),A) | - p2(f12(c22,c26),A). [resolve(153,a,128,a)]. given #132 (F,wt=6): 333 - p2(f12(c21,f24(c26)),c4). [ur(134,a,330,a,c,167,a)]. given #133 (F,wt=6): 336 - p2(f11(c13,f25(c26)),c4). [ur(175,a,333,a)]. given #134 (T,wt=6): 335 p2(f12(c5,f20(c26)),c4). [resolve(180,b,130,a)]. given #135 (T,wt=9): 334 p6(f17(f25(c26)),c7) | - p6(f20(c26),c8). [resolve(258,b,122,a)]. given #136 (A,wt=11): 181 p2(f12(c22,c26),A) | - p2(f12(c5,f20(c26)),A). [resolve(154,a,128,a)]. given #137 (F,wt=7): 331 - p2(f11(A,f17(f24(c26))),c4). [back_unit_del(281),unit_del(a,330)]. given #138 (F,wt=7): 338 - p2(f11(c13,f20(f25(c26))),c4). [ur(156,a,169,a,b,336,a)]. given #139 (T,wt=9): 342 p6(f17(f25(c26)),c7) | p6(f20(c26),c7). [resolve(334,b,193,b)]. given #140 (T,wt=10): 259 p6(f19(f25(c26)),c7) | p6(f19(f25(c26)),c8). [resolve(240,a,100,b)]. given #141 (A,wt=11): 182 p2(f11(c13,f24(c26)),A) | - p2(f11(c22,c26),A). [resolve(159,a,128,a)]. given #142 (F,wt=7): 339 - p2(f12(c5,f18(f25(c26))),c4). [back_unit_del(312),unit_del(a,337)]. given #143 (F,wt=6): 354 - p2(f12(c22,f25(c26)),c4). [ur(132,a,339,a,c,169,a)]. given #144 (T,wt=6): 352 p2(f11(c13,f24(c26)),c5). [resolve(182,b,125,a)]. given #145 (T,wt=9): 351 p6(f19(f25(c26)),c7) | - p6(f20(c26),c8). [resolve(259,b,129,a)]. given #146 (A,wt=11): 183 p2(f11(c22,c26),A) | - p2(f11(c13,f24(c26)),A). [resolve(160,a,128,a)]. given #147 (F,wt=6): 355 - p2(f11(c5,f20(c26)),c4). [ur(164,a,128,a,b,354,a)]. given #148 (F,wt=4): 357 - p6(f20(c26),c7). [ur(98,a,335,a,b,166,a,c,355,a)]. given #149 (T,wt=4): 367 p6(f20(c26),c8). [back_unit_del(193),unit_del(a,357)]. given #150 (T,wt=5): 358 p6(f19(f25(c26)),c7). [back_unit_del(356),unit_del(b,357)]. given #151 (A,wt=12): 184 p2(f11(c5,f20(c26)),A) | - p2(f12(c22,f25(c26)),A). [resolve(163,a,128,a)]. given #152 (F,wt=5): 369 - p6(f19(f25(c26)),c8). [back_unit_del(129),unit_del(b,367)]. given #153 (F,wt=5): 370 - p6(f17(f25(c26)),c8). [back_unit_del(122),unit_del(b,367)]. given #154 (T,wt=5): 366 p6(f17(f25(c26)),c7). [back_unit_del(342),unit_del(b,357)]. given #155 (T,wt=12): 185 p2(f12(c22,f25(c26)),A) | - p2(f11(c5,f20(c26)),A). [resolve(164,a,128,a)]. given #156 (A,wt=13): 194 p2(f11(c13,f24(c26)),A) | - p2(f11(c13,f18(f24(c26))),A). [resolve(167,a,162,a)]. given #157 (F,wt=7): 340 - p2(f11(A,f18(f25(c26))),c4). [back_unit_del(306),unit_del(a,339)]. given #158 (F,wt=7): 353 - p2(f11(c5,f19(f25(c26))),c4). [ur(139,a,339,a,c,169,a)]. given #159 (T,wt=13): 195 p2(f11(c13,f18(f24(c26))),A) | - p2(f11(c13,f24(c26)),A). [resolve(167,a,161,a)]. given #160 (T,wt=7): 380 p2(f11(c13,f18(f24(c26))),c5). [resolve(195,b,352,a)]. given #161 (A,wt=13): 196 p2(f11(c5,f24(c26)),A) | - p2(f11(c5,f18(f24(c26))),A). [resolve(167,a,158,a)]. given #162 (F,wt=5): 381 - p9(f18(f24(c26)),c14). [ur(97,a,242,a,b,380,a,d,265,a)]. given #163 (F,wt=7): 364 - p2(f11(A,f17(f25(c26))),c4). [back_unit_del(345),unit_del(a,357)]. given #164 (T,wt=13): 197 p2(f11(c5,f18(f24(c26))),A) | - p2(f11(c5,f24(c26)),A). [resolve(167,a,157,a)]. given #165 (T,wt=7): 386 p2(f11(c5,f18(f24(c26))),c4). [resolve(197,b,316,a)]. given #166 (A,wt=13): 198 p2(f11(c13,f24(c26)),A) | - p2(f11(c13,f20(f24(c26))),A). [resolve(167,a,156,a)]. given #167 (F,wt=5): 387 - p9(f18(f24(c26)),c15). [back_unit_del(269),unit_del(b,386)]. given #168 (F,wt=7): 373 - p2(f12(c5,f19(f25(c26))),c5). [resolve(358,a,109,c),unit_del(a,353),unit_del(c,240)]. given #169 (T,wt=13): 199 p2(f11(c13,f20(f24(c26))),A) | - p2(f11(c13,f24(c26)),A). [resolve(167,a,155,a)]. given #170 (T,wt=7): 391 p2(f11(c13,f20(f24(c26))),c5). [resolve(199,b,352,a)]. given #171 (A,wt=14): 200 p2(f12(c5,f20(f24(c26))),A) | - p2(f11(c5,f17(f24(c26))),A). [resolve(167,a,146,a)]. given #172 (F,wt=7): 382 - p2(f12(c5,f20(f25(c26))),c4). [ur(145,a,169,a,b,364,a)]. given #173 (F,wt=7): 383 - p2(f12(c5,f19(f25(c26))),c4). [ur(131,a,364,a,c,169,a)]. given #174 (T,wt=13): 202 p2(f11(c5,f24(c26)),A) | - p2(f11(c5,f20(f24(c26))),A). [resolve(167,a,144,a)]. given #175 (T,wt=13): 203 p2(f11(c5,f20(f24(c26))),A) | - p2(f11(c5,f24(c26)),A). [resolve(167,a,143,a)]. given #176 (A,wt=14): 201 p2(f11(c5,f17(f24(c26))),A) | - p2(f12(c5,f20(f24(c26))),A). [resolve(167,a,145,a)]. given #177 (F,wt=7): 385 - p2(f11(c5,f19(f25(c26))),c5). [back_unit_del(371),unit_del(b,383)]. given #178 (F,wt=7): 388 - p2(f11(c13,f17(f25(c26))),c5). [ur(137,a,373,a,c,169,a)]. given #179 (T,wt=7): 392 p2(f11(c5,f20(f24(c26))),c4). [resolve(203,b,316,a)]. given #180 (T,wt=12): 393 p2(f12(c5,f20(f24(c26))),c5) | - p9(f20(f24(c26)),c15). [back_unit_del(270),unit_del(c,392)]. given #181 (A,wt=13): 204 p2(f12(c21,f24(c26)),A) | - p2(f12(c5,f17(f24(c26))),A). [resolve(167,a,140,c)]. given #182 (F,wt=5): 397 - p9(f20(f24(c26)),c10). [ur(113,a,273,a,c,392,a,d,245,a)]. given #183 (F,wt=7): 389 - p2(f12(c5,f17(f25(c26))),c5). [back_unit_del(362),unit_del(b,388)]. ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds. % Length of proof is 125. % Level of proof is 21. % Maximum clause weight is 21. % Given clauses 183. 1 - p9(A,c16) | p1(f12(c5,f19(A)),f11(c13,f17(A))). [input]. 3 p1(f12(c22,A),f12(c5,f18(A))) | - p9(A,c16). [input]. 5 - p3(c4,c5). [input]. 6 - p9(A,c16) | p1(f12(c5,f18(A)),f11(c5,f19(A))). [input]. 7 p1(f12(c21,A),f12(c5,f17(A))) | - p9(A,c16). [input]. 8 - p9(A,c23) | p1(f11(c5,A),f11(c5,f25(A))). [input]. 12 p1(f12(c21,A),f12(c21,f25(A))) | - p9(A,c23). [input]. 14 - p1(A,B) | p2(B,C) | - p2(A,C). [input]. 16 p2(A,B) | - p1(A,C) | - p2(C,B). [input]. 22 - p9(A,c16) | p1(f12(c5,f20(A)),f11(c5,f17(A))). [input]. 23 p1(f12(c21,f24(A)),f11(c13,f25(A))) | - p9(A,c23). [input]. 24 p1(f11(c13,A),f11(c5,f24(A))) | - p9(A,c23). [input]. 27 p1(f12(c22,A),f12(c5,f20(A))) | - p9(A,c23). [input]. 32 - p9(A,c16) | p1(f11(c13,A),f11(c13,f20(A))). [input]. 34 p1(f11(c5,A),f11(c5,f18(A))) | - p9(A,c16). [input]. 36 p1(f11(c22,A),f11(c13,f24(A))) | - p9(A,c23). [input]. 37 - p9(A,c16) | p1(f11(c13,A),f11(c13,f18(A))). [input]. 38 p3(A,B) | - p2(C,B) | - p2(C,A). [input]. 41 - p9(A,c23) | p1(f12(c22,f25(A)),f11(c5,f20(A))). [input]. 95 - p2(f12(c5,A),c4) | - p9(A,c15) | p2(f11(c5,A),c5) | - p6(A,c7). [input]. 96 p9(f25(A),c16) | - p9(A,c23). [input]. 98 - p2(f12(c5,A),c4) | - p9(A,c14) | p2(f11(c5,A),c4) | - p6(A,c7). [input]. 99 p2(f11(c13,A),c4) | - p2(f12(c5,A),c4) | p2(f11(c5,A),c4) | - p6(A,c7) | - p9(A,c10). [input]. 100 p6(A,c7) | - p9(A,B) | p6(A,c8). [input]. 102 - p9(A,c16) | p9(f19(A),c15). [input]. 105 p9(f24(A),c16) | - p9(A,c23). [input]. 106 - p9(A,c10) | - p2(f12(c5,A),c5) | - p6(A,c7) | p2(f11(c5,A),c5). [input]. 107 - p6(A,c7) | - p9(A,c10) | - p2(f12(c5,A),c5) | p2(f11(c13,A),c5). [input]. 108 - p2(f12(c5,A),c4) | p2(f11(c13,A),c4) | - p6(A,c7) | - p9(A,c14). [input]. 109 p2(f11(c5,A),c4) | - p2(f12(c5,A),c5) | - p6(A,c7) | - p9(A,c15). [input]. 111 p9(f17(A),c10) | - p9(A,c16). [input]. 112 - p9(A,c23) | p9(f20(A),c14). [input]. 115 p9(f20(A),c14) | - p9(A,c16). [input]. 117 p9(f18(A),c10) | - p9(A,c16). [input]. 118 - p6(f19(f24(c26)),c8). [input]. 119 - p6(f17(f24(c26)),c8). [input]. 120 - p6(f18(f25(c26)),c8). [input]. 121 - p6(f18(f24(c26)),c8). [input]. 122 - p6(f17(f25(c26)),c8) | - p6(f20(c26),c8). [input]. 123 p2(f12(c21,c26),c5). [input]. 124 p2(f11(c13,c26),c4). [input]. 125 p2(f11(c22,c26),c5). [input]. 126 p2(f11(c5,c26),c5). [input]. 127 - p6(f20(f24(c26)),c8). [input]. 128 p9(c26,c23). [input]. 129 - p6(f19(f25(c26)),c8) | - p6(f20(c26),c8). [input]. 130 p2(f12(c22,c26),c4). [input]. 132 p2(f12(c5,f18(A)),B) | - p2(f12(c22,A),B) | - p9(A,c16). [resolve(14,a,3,a)]. 134 p2(f12(c5,f17(A)),B) | - p2(f12(c21,A),B) | - p9(A,c16). [resolve(14,a,7,a)]. 136 p2(f12(c21,f25(A)),B) | - p2(f12(c21,A),B) | - p9(A,c23). [resolve(14,a,12,a)]. 137 p2(f12(c5,f19(A)),B) | - p2(f11(c13,f17(A)),B) | - p9(A,c16). [resolve(16,b,1,b)]. 139 p2(f12(c5,f18(A)),B) | - p2(f11(c5,f19(A)),B) | - p9(A,c16). [resolve(16,b,6,b)]. 141 p2(f11(c5,A),B) | - p2(f11(c5,f25(A)),B) | - p9(A,c23). [resolve(16,b,8,b)]. 146 - p9(A,c16) | p2(f12(c5,f20(A)),B) | - p2(f11(c5,f17(A)),B). [resolve(22,b,16,b)]. 148 - p9(A,c23) | p2(f12(c21,f24(A)),B) | - p2(f11(c13,f25(A)),B). [resolve(23,a,16,b)]. 150 - p9(A,c23) | p2(f11(c13,A),B) | - p2(f11(c5,f24(A)),B). [resolve(24,a,16,b)]. 153 - p9(A,c23) | p2(f12(c5,f20(A)),B) | - p2(f12(c22,A),B). [resolve(27,a,14,a)]. 156 - p9(A,c16) | p2(f11(c13,A),B) | - p2(f11(c13,f20(A)),B). [resolve(32,b,16,b)]. 158 - p9(A,c16) | p2(f11(c5,A),B) | - p2(f11(c5,f18(A)),B). [resolve(34,a,16,b)]. 160 - p9(A,c23) | p2(f11(c22,A),B) | - p2(f11(c13,f24(A)),B). [resolve(36,a,16,b)]. 162 - p9(A,c16) | p2(f11(c13,A),B) | - p2(f11(c13,f18(A)),B). [resolve(37,b,16,b)]. 164 - p9(A,c23) | p2(f12(c22,f25(A)),B) | - p2(f11(c5,f20(A)),B). [resolve(41,b,16,b)]. 165 - p2(A,c5) | - p2(A,c4). [resolve(38,a,5,a)]. 166 p9(f20(c26),c14). [resolve(128,a,112,a)]. 167 p9(f24(c26),c16). [resolve(128,a,105,b)]. 169 p9(f25(c26),c16). [resolve(128,a,96,b)]. 171 p2(f12(c21,f25(c26)),A) | - p2(f12(c21,c26),A). [resolve(136,c,128,a)]. 175 p2(f12(c21,f24(c26)),A) | - p2(f11(c13,f25(c26)),A). [resolve(148,a,128,a)]. 180 p2(f12(c5,f20(c26)),A) | - p2(f12(c22,c26),A). [resolve(153,a,128,a)]. 187 - p2(f11(c13,c26),c5). [resolve(165,b,124,a)]. 188 - p2(f11(c5,c26),c4). [ur(165,a,126,a)]. 189 - p2(f11(c22,c26),c4). [ur(165,a,125,a)]. 192 - p2(f11(c5,f24(c26)),c5). [ur(150,a,128,a,b,187,a)]. 193 p6(f20(c26),c7) | p6(f20(c26),c8). [resolve(166,a,100,b)]. 212 p9(f18(f24(c26)),c10). [resolve(167,a,117,b)]. 213 p9(f20(f24(c26)),c14). [resolve(167,a,115,b)]. 214 p9(f17(f24(c26)),c10). [resolve(167,a,111,b)]. 215 p9(f19(f24(c26)),c15). [resolve(167,a,102,a)]. 217 - p2(f11(c5,f25(c26)),c4). [ur(141,a,188,a,c,128,a)]. 218 - p2(f11(c13,f24(c26)),c4). [ur(160,a,128,a,b,189,a)]. 237 p9(f18(f25(c26)),c10). [resolve(169,a,117,b)]. 239 p9(f17(f25(c26)),c10). [resolve(169,a,111,b)]. 240 p9(f19(f25(c26)),c15). [resolve(169,a,102,a)]. 242 p6(f18(f24(c26)),c7). [resolve(212,a,100,b),unit_del(b,121)]. 245 p6(f20(f24(c26)),c7). [resolve(213,a,100,b),unit_del(b,127)]. 246 p6(f17(f24(c26)),c7). [resolve(214,a,100,b),unit_del(b,119)]. 247 p2(f12(c21,f25(c26)),c5). [resolve(171,b,123,a)]. 248 - p2(f11(c5,f18(f24(c26))),c5). [ur(158,a,167,a,b,192,a)]. 250 - p2(f11(c5,f18(f25(c26))),c4). [ur(158,a,169,a,b,217,a)]. 252 p6(f19(f24(c26)),c7). [resolve(215,a,100,b),unit_del(b,118)]. 253 p6(f18(f25(c26)),c7). [resolve(237,a,100,b),unit_del(b,120)]. 255 - p2(f11(c13,f20(f24(c26))),c4). [ur(156,a,167,a,b,218,a)]. 258 p6(f17(f25(c26)),c7) | p6(f17(f25(c26)),c8). [resolve(239,a,100,b)]. 259 p6(f19(f25(c26)),c7) | p6(f19(f25(c26)),c8). [resolve(240,a,100,b)]. 265 - p2(f12(c5,f18(f24(c26))),c5). [resolve(242,a,106,c),unit_del(a,212),unit_del(c,248)]. 273 - p2(f12(c5,f20(f24(c26))),c4). [resolve(245,a,108,c),unit_del(b,255),unit_del(c,213)]. 287 p2(f11(c13,f17(f24(c26))),c4) | - p2(f12(c5,f17(f24(c26))),c4) | p2(f11(c5,f17(f24(c26))),c4). [resolve(246,a,99,d),unit_del(d,214)]. 304 - p2(f12(c5,f19(f24(c26))),c4) | p2(f11(c5,f19(f24(c26))),c5). [resolve(252,a,95,d),unit_del(b,215)]. 312 p2(f11(c13,f18(f25(c26))),c4) | - p2(f12(c5,f18(f25(c26))),c4). [resolve(253,a,99,d),unit_del(c,250),unit_del(d,237)]. 317 - p2(f11(c5,f19(f24(c26))),c5). [ur(139,a,265,a,c,167,a)]. 319 - p2(f12(c5,f19(f24(c26))),c4). [back_unit_del(304),unit_del(b,317)]. 325 - p2(f11(c5,f17(f24(c26))),c4). [ur(146,a,167,a,b,273,a)]. 327 p2(f11(c13,f17(f24(c26))),c4) | - p2(f12(c5,f17(f24(c26))),c4). [back_unit_del(287),unit_del(c,325)]. 329 - p2(f11(c13,f17(f24(c26))),c4). [ur(137,a,319,a,c,167,a)]. 330 - p2(f12(c5,f17(f24(c26))),c4). [back_unit_del(327),unit_del(a,329)]. 333 - p2(f12(c21,f24(c26)),c4). [ur(134,a,330,a,c,167,a)]. 334 p6(f17(f25(c26)),c7) | - p6(f20(c26),c8). [resolve(258,b,122,a)]. 335 p2(f12(c5,f20(c26)),c4). [resolve(180,b,130,a)]. 336 - p2(f11(c13,f25(c26)),c4). [ur(175,a,333,a)]. 337 - p2(f11(c13,f18(f25(c26))),c4). [ur(162,a,169,a,b,336,a)]. 339 - p2(f12(c5,f18(f25(c26))),c4). [back_unit_del(312),unit_del(a,337)]. 342 p6(f17(f25(c26)),c7) | p6(f20(c26),c7). [resolve(334,b,193,b)]. 347 p6(f20(c26),c7) | - p2(f12(c5,f17(f25(c26))),c5) | p2(f11(c13,f17(f25(c26))),c5). [resolve(342,a,107,a),unit_del(b,239)]. 351 p6(f19(f25(c26)),c7) | - p6(f20(c26),c8). [resolve(259,b,129,a)]. 353 - p2(f11(c5,f19(f25(c26))),c4). [ur(139,a,339,a,c,169,a)]. 354 - p2(f12(c22,f25(c26)),c4). [ur(132,a,339,a,c,169,a)]. 355 - p2(f11(c5,f20(c26)),c4). [ur(164,a,128,a,b,354,a)]. 356 p6(f19(f25(c26)),c7) | p6(f20(c26),c7). [resolve(351,b,193,b)]. 357 - p6(f20(c26),c7). [ur(98,a,335,a,b,166,a,c,355,a)]. 358 p6(f19(f25(c26)),c7). [back_unit_del(356),unit_del(b,357)]. 362 - p2(f12(c5,f17(f25(c26))),c5) | p2(f11(c13,f17(f25(c26))),c5). [back_unit_del(347),unit_del(a,357)]. 373 - p2(f12(c5,f19(f25(c26))),c5). [resolve(358,a,109,c),unit_del(a,353),unit_del(c,240)]. 388 - p2(f11(c13,f17(f25(c26))),c5). [ur(137,a,373,a,c,169,a)]. 389 - p2(f12(c5,f17(f25(c26))),c5). [back_unit_del(362),unit_del(b,388)]. 398 $F. [ur(134,a,389,a,c,169,a),unit_del(a,247)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=183. Generated=461. Kept=303. proofs=1. Usable=174. Sos=48. Demods=0. Denials=0. Limbo=0, Disabled=174. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=157. Back_subsumed=44. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=37. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=35. Nonunit_bsub_feature_tests=269. Megabytes=0.33. User_CPU=0.02, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13075 exit (max_proofs) Mon Jun 19 16:41:11 2006