============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 10892 was started by mccune on cleo.thornwood, Sat Aug 12 20:59:02 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). formulas(sos). -p9(X1,c16) | p1(f12(c5,f19(X1)),f11(c13,f17(X1))). -p2(f12(c5,X1),c4) | -p9(X1,c15) | p2(f11(c5,X1),c5) | -p6(X1,c7). p1(f12(c22,X1),f12(c5,f18(X1))) | -p9(X1,c16). p9(f25(X1),c16) | -p9(X1,c23). -p3(c4,c5). -p9(X1,c16) | p1(f12(c5,f18(X1)),f11(c5,f19(X1))). p1(f12(c21,X1),f12(c5,f17(X1))) | -p9(X1,c16). -p9(X1,c23) | p1(f11(c5,X1),f11(c5,f25(X1))). -p6(X2,c7) | -p2(f11(X1,X2),c5) | -p9(X2,c14) | p2(f12(c5,X2),c5). -p2(f12(c5,X1),c4) | -p9(X1,c14) | p2(f11(c5,X1),c4) | -p6(X1,c7). p2(f11(c13,X1),c4) | -p2(f12(c5,X1),c4) | p2(f11(c5,X1),c4) | -p6(X1,c7) | -p9(X1,c10). p1(f12(c21,X1),f12(c21,f25(X1))) | -p9(X1,c23). p6(X2,c7) | -p9(X2,X1) | p6(X2,c8). -p1(X1,X2) | p2(X2,X3) | -p2(X1,X3). -p6(X1,c8) | -p6(X1,c7). p2(X2,X3) | -p1(X2,X1) | -p2(X1,X3). -p9(X1,c16) | p9(f19(X1),c15). p2(f11(c5,X1),c5) | -p2(f12(c5,X1),c5) | -p6(X1,c7) | p2(f11(c13,X1),c5) | -p9(X1,c14). p2(f12(c5,X1),c5) | -p9(X1,c10) | -p6(X1,c7) | -p2(f11(c5,X1),c5) | -p2(f11(c13,X1),c5). p1(f11(c5,X1),f11(c5,f20(X1))) | -p9(X1,c16). p9(f24(X1),c16) | -p9(X1,c23). -p9(X1,c16) | p1(f12(c5,f20(X1)),f11(c5,f17(X1))). p1(f12(c21,f24(X1)),f11(c13,f25(X1))) | -p9(X1,c23). p1(f11(c13,X1),f11(c5,f24(X1))) | -p9(X1,c23). p1(f12(c22,f24(X1)),f11(c13,f20(X1))) | -p9(X1,c23). -p9(X1,c10) | -p2(f12(c5,X1),c5) | -p6(X1,c7) | p2(f11(c5,X1),c5). p1(f12(c22,X1),f12(c5,f20(X1))) | -p9(X1,c23). -p3(c5,c4). -p6(X1,c7) | -p9(X1,c10) | -p2(f12(c5,X1),c5) | p2(f11(c13,X1),c5). -p2(f12(c5,X1),c4) | p2(f11(c13,X1),c4) | -p6(X1,c7) | -p9(X1,c14). p2(f11(c5,X1),c4) | -p2(f12(c5,X1),c5) | -p6(X1,c7) | -p9(X1,c15). -p9(X1,c16) | p1(f11(c13,X1),f11(c13,f20(X1))). -p2(f11(c13,X1),c4) | -p9(X1,c14) | p2(f12(c5,X1),c4) | -p2(f11(c5,X1),c4) | -p6(X1,c7). p1(f11(c5,X1),f11(c5,f18(X1))) | -p9(X1,c16). p9(f17(X1),c10) | -p9(X1,c16). p1(f11(c22,X1),f11(c13,f24(X1))) | -p9(X1,c23). -p9(X1,c16) | p1(f11(c13,X1),f11(c13,f18(X1))). p3(X2,X3) | -p2(X1,X3) | -p2(X1,X2). -p9(X1,c23) | p9(f20(X1),c14). p2(f12(c5,X2),c4) | -p9(X2,c10) | -p2(f11(X1,X2),c4) | -p6(X2,c7). -p9(X1,c23) | p1(f12(c22,f25(X1)),f11(c5,f20(X1))). p2(f12(c5,X1),c5) | -p6(X1,c7) | -p9(X1,c15) | -p2(f11(c5,X1),c4). p9(f20(X1),c14) | -p9(X1,c16). -p2(f11(c5,X1),c5) | p2(f12(c5,X1),c4) | -p9(X1,c15) | -p6(X1,c7). p9(f18(X1),c10) | -p9(X1,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 NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -p9(A,c16) | p1(f12(c5,f19(A)),f11(c13,f17(A))). [assumption]. -p2(f12(c5,A),c4) | -p9(A,c15) | p2(f11(c5,A),c5) | -p6(A,c7). [assumption]. p1(f12(c22,A),f12(c5,f18(A))) | -p9(A,c16). [assumption]. p9(f25(A),c16) | -p9(A,c23). [assumption]. -p3(c4,c5). [assumption]. -p9(A,c16) | p1(f12(c5,f18(A)),f11(c5,f19(A))). [assumption]. p1(f12(c21,A),f12(c5,f17(A))) | -p9(A,c16). [assumption]. -p9(A,c23) | p1(f11(c5,A),f11(c5,f25(A))). [assumption]. -p6(A,c7) | -p2(f11(B,A),c5) | -p9(A,c14) | p2(f12(c5,A),c5). [assumption]. -p2(f12(c5,A),c4) | -p9(A,c14) | p2(f11(c5,A),c4) | -p6(A,c7). [assumption]. p2(f11(c13,A),c4) | -p2(f12(c5,A),c4) | p2(f11(c5,A),c4) | -p6(A,c7) | -p9(A,c10). [assumption]. p1(f12(c21,A),f12(c21,f25(A))) | -p9(A,c23). [assumption]. p6(A,c7) | -p9(A,B) | p6(A,c8). [assumption]. -p1(A,B) | p2(B,C) | -p2(A,C). [assumption]. -p6(A,c8) | -p6(A,c7). [assumption]. p2(A,B) | -p1(A,C) | -p2(C,B). [assumption]. -p9(A,c16) | p9(f19(A),c15). [assumption]. p2(f11(c5,A),c5) | -p2(f12(c5,A),c5) | -p6(A,c7) | p2(f11(c13,A),c5) | -p9(A,c14). [assumption]. p2(f12(c5,A),c5) | -p9(A,c10) | -p6(A,c7) | -p2(f11(c5,A),c5) | -p2(f11(c13,A),c5). [assumption]. p1(f11(c5,A),f11(c5,f20(A))) | -p9(A,c16). [assumption]. p9(f24(A),c16) | -p9(A,c23). [assumption]. -p9(A,c16) | p1(f12(c5,f20(A)),f11(c5,f17(A))). [assumption]. p1(f12(c21,f24(A)),f11(c13,f25(A))) | -p9(A,c23). [assumption]. p1(f11(c13,A),f11(c5,f24(A))) | -p9(A,c23). [assumption]. p1(f12(c22,f24(A)),f11(c13,f20(A))) | -p9(A,c23). [assumption]. -p9(A,c10) | -p2(f12(c5,A),c5) | -p6(A,c7) | p2(f11(c5,A),c5). [assumption]. p1(f12(c22,A),f12(c5,f20(A))) | -p9(A,c23). [assumption]. -p3(c5,c4). [assumption]. -p6(A,c7) | -p9(A,c10) | -p2(f12(c5,A),c5) | p2(f11(c13,A),c5). [assumption]. -p2(f12(c5,A),c4) | p2(f11(c13,A),c4) | -p6(A,c7) | -p9(A,c14). [assumption]. p2(f11(c5,A),c4) | -p2(f12(c5,A),c5) | -p6(A,c7) | -p9(A,c15). [assumption]. -p9(A,c16) | p1(f11(c13,A),f11(c13,f20(A))). [assumption]. -p2(f11(c13,A),c4) | -p9(A,c14) | p2(f12(c5,A),c4) | -p2(f11(c5,A),c4) | -p6(A,c7). [assumption]. p1(f11(c5,A),f11(c5,f18(A))) | -p9(A,c16). [assumption]. p9(f17(A),c10) | -p9(A,c16). [assumption]. p1(f11(c22,A),f11(c13,f24(A))) | -p9(A,c23). [assumption]. -p9(A,c16) | p1(f11(c13,A),f11(c13,f18(A))). [assumption]. p3(A,B) | -p2(C,B) | -p2(C,A). [assumption]. -p9(A,c23) | p9(f20(A),c14). [assumption]. p2(f12(c5,A),c4) | -p9(A,c10) | -p2(f11(B,A),c4) | -p6(A,c7). [assumption]. -p9(A,c23) | p1(f12(c22,f25(A)),f11(c5,f20(A))). [assumption]. p2(f12(c5,A),c5) | -p6(A,c7) | -p9(A,c15) | -p2(f11(c5,A),c4). [assumption]. p9(f20(A),c14) | -p9(A,c16). [assumption]. -p2(f11(c5,A),c5) | p2(f12(c5,A),c4) | -p9(A,c15) | -p6(A,c7). [assumption]. p9(f18(A),c10) | -p9(A,c16). [assumption]. -p6(f19(f24(c26)),c8). [assumption]. -p6(f17(f24(c26)),c8). [assumption]. -p6(f18(f25(c26)),c8). [assumption]. -p6(f18(f24(c26)),c8). [assumption]. -p6(f17(f25(c26)),c8) | -p6(f20(c26),c8). [assumption]. p2(f12(c21,c26),c5). [assumption]. p2(f11(c13,c26),c4). [assumption]. p2(f11(c22,c26),c5). [assumption]. p2(f11(c5,c26),c5). [assumption]. -p6(f20(f24(c26)),c8). [assumption]. p9(c26,c23). [assumption]. -p6(f19(f25(c26)),c8) | -p6(f20(c26),c8). [assumption]. p2(f12(c22,c26),c4). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating p1/2 1 -p1(A,B) | p2(B,C) | -p2(A,C). [assumption]. 2 -p9(A,c16) | p1(f12(c5,f19(A)),f11(c13,f17(A))). [assumption]. 3 p1(f12(c22,A),f12(c5,f18(A))) | -p9(A,c16). [assumption]. 4 -p9(A,c16) | p1(f12(c5,f18(A)),f11(c5,f19(A))). [assumption]. 5 p1(f12(c21,A),f12(c5,f17(A))) | -p9(A,c16). [assumption]. 6 -p9(A,c23) | p1(f11(c5,A),f11(c5,f25(A))). [assumption]. 7 p1(f12(c21,A),f12(c21,f25(A))) | -p9(A,c23). [assumption]. Derived: p2(f11(c13,f17(A)),B) | -p2(f12(c5,f19(A)),B) | -p9(A,c16). [resolve(1,a,2,b)]. Derived: p2(f12(c5,f18(A)),B) | -p2(f12(c22,A),B) | -p9(A,c16). [resolve(1,a,3,a)]. Derived: p2(f11(c5,f19(A)),B) | -p2(f12(c5,f18(A)),B) | -p9(A,c16). [resolve(1,a,4,b)]. Derived: p2(f12(c5,f17(A)),B) | -p2(f12(c21,A),B) | -p9(A,c16). [resolve(1,a,5,a)]. Derived: p2(f11(c5,f25(A)),B) | -p2(f11(c5,A),B) | -p9(A,c23). [resolve(1,a,6,b)]. Derived: p2(f12(c21,f25(A)),B) | -p2(f12(c21,A),B) | -p9(A,c23). [resolve(1,a,7,a)]. 8 p2(A,B) | -p1(A,C) | -p2(C,B). [assumption]. Derived: p2(f12(c5,f19(A)),B) | -p2(f11(c13,f17(A)),B) | -p9(A,c16). [resolve(8,b,2,b)]. Derived: p2(f12(c22,A),B) | -p2(f12(c5,f18(A)),B) | -p9(A,c16). [resolve(8,b,3,a)]. Derived: p2(f12(c5,f18(A)),B) | -p2(f11(c5,f19(A)),B) | -p9(A,c16). [resolve(8,b,4,b)]. Derived: p2(f12(c21,A),B) | -p2(f12(c5,f17(A)),B) | -p9(A,c16). [resolve(8,b,5,a)]. Derived: p2(f11(c5,A),B) | -p2(f11(c5,f25(A)),B) | -p9(A,c23). [resolve(8,b,6,b)]. Derived: p2(f12(c21,A),B) | -p2(f12(c21,f25(A)),B) | -p9(A,c23). [resolve(8,b,7,a)]. 9 p1(f11(c5,A),f11(c5,f20(A))) | -p9(A,c16). [assumption]. Derived: -p9(A,c16) | p2(f11(c5,f20(A)),B) | -p2(f11(c5,A),B). [resolve(9,a,1,a)]. Derived: -p9(A,c16) | p2(f11(c5,A),B) | -p2(f11(c5,f20(A)),B). [resolve(9,a,8,b)]. 10 -p9(A,c16) | p1(f12(c5,f20(A)),f11(c5,f17(A))). [assumption]. Derived: -p9(A,c16) | p2(f11(c5,f17(A)),B) | -p2(f12(c5,f20(A)),B). [resolve(10,b,1,a)]. Derived: -p9(A,c16) | p2(f12(c5,f20(A)),B) | -p2(f11(c5,f17(A)),B). [resolve(10,b,8,b)]. 11 p1(f12(c21,f24(A)),f11(c13,f25(A))) | -p9(A,c23). [assumption]. Derived: -p9(A,c23) | p2(f11(c13,f25(A)),B) | -p2(f12(c21,f24(A)),B). [resolve(11,a,1,a)]. Derived: -p9(A,c23) | p2(f12(c21,f24(A)),B) | -p2(f11(c13,f25(A)),B). [resolve(11,a,8,b)]. 12 p1(f11(c13,A),f11(c5,f24(A))) | -p9(A,c23). [assumption]. Derived: -p9(A,c23) | p2(f11(c5,f24(A)),B) | -p2(f11(c13,A),B). [resolve(12,a,1,a)]. Derived: -p9(A,c23) | p2(f11(c13,A),B) | -p2(f11(c5,f24(A)),B). [resolve(12,a,8,b)]. 13 p1(f12(c22,f24(A)),f11(c13,f20(A))) | -p9(A,c23). [assumption]. Derived: -p9(A,c23) | p2(f11(c13,f20(A)),B) | -p2(f12(c22,f24(A)),B). [resolve(13,a,1,a)]. Derived: -p9(A,c23) | p2(f12(c22,f24(A)),B) | -p2(f11(c13,f20(A)),B). [resolve(13,a,8,b)]. 14 p1(f12(c22,A),f12(c5,f20(A))) | -p9(A,c23). [assumption]. Derived: -p9(A,c23) | p2(f12(c5,f20(A)),B) | -p2(f12(c22,A),B). [resolve(14,a,1,a)]. Derived: -p9(A,c23) | p2(f12(c22,A),B) | -p2(f12(c5,f20(A)),B). [resolve(14,a,8,b)]. 15 -p9(A,c16) | p1(f11(c13,A),f11(c13,f20(A))). [assumption]. Derived: -p9(A,c16) | p2(f11(c13,f20(A)),B) | -p2(f11(c13,A),B). [resolve(15,b,1,a)]. Derived: -p9(A,c16) | p2(f11(c13,A),B) | -p2(f11(c13,f20(A)),B). [resolve(15,b,8,b)]. 16 p1(f11(c5,A),f11(c5,f18(A))) | -p9(A,c16). [assumption]. Derived: -p9(A,c16) | p2(f11(c5,f18(A)),B) | -p2(f11(c5,A),B). [resolve(16,a,1,a)]. Derived: -p9(A,c16) | p2(f11(c5,A),B) | -p2(f11(c5,f18(A)),B). [resolve(16,a,8,b)]. 17 p1(f11(c22,A),f11(c13,f24(A))) | -p9(A,c23). [assumption]. Derived: -p9(A,c23) | p2(f11(c13,f24(A)),B) | -p2(f11(c22,A),B). [resolve(17,a,1,a)]. Derived: -p9(A,c23) | p2(f11(c22,A),B) | -p2(f11(c13,f24(A)),B). [resolve(17,a,8,b)]. 18 -p9(A,c16) | p1(f11(c13,A),f11(c13,f18(A))). [assumption]. Derived: -p9(A,c16) | p2(f11(c13,f18(A)),B) | -p2(f11(c13,A),B). [resolve(18,b,1,a)]. Derived: -p9(A,c16) | p2(f11(c13,A),B) | -p2(f11(c13,f18(A)),B). [resolve(18,b,8,b)]. 19 -p9(A,c23) | p1(f12(c22,f25(A)),f11(c5,f20(A))). [assumption]. Derived: -p9(A,c23) | p2(f11(c5,f20(A)),B) | -p2(f12(c22,f25(A)),B). [resolve(19,b,1,a)]. Derived: -p9(A,c23) | p2(f12(c22,f25(A)),B) | -p2(f11(c5,f20(A)),B). [resolve(19,b,8,b)]. Eliminating p3/2 20 p3(A,B) | -p2(C,B) | -p2(C,A). [assumption]. 21 -p3(c4,c5). [assumption]. 22 -p3(c5,c4). [assumption]. Derived: -p2(A,c5) | -p2(A,c4). [resolve(20,a,21,a)]. ============================== end predicate elimination ============= 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: (no changes). 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: formulas(usable). end_of_list. formulas(sos). 23 -p2(f12(c5,A),c4) | -p9(A,c15) | p2(f11(c5,A),c5) | -p6(A,c7). [assumption]. 24 p9(f25(A),c16) | -p9(A,c23). [assumption]. 25 -p6(A,c7) | -p2(f11(B,A),c5) | -p9(A,c14) | p2(f12(c5,A),c5). [assumption]. 26 -p2(f12(c5,A),c4) | -p9(A,c14) | p2(f11(c5,A),c4) | -p6(A,c7). [assumption]. 27 p2(f11(c13,A),c4) | -p2(f12(c5,A),c4) | p2(f11(c5,A),c4) | -p6(A,c7) | -p9(A,c10). [assumption]. 28 p6(A,c7) | -p9(A,B) | p6(A,c8). [assumption]. 29 -p6(A,c8) | -p6(A,c7). [assumption]. 30 -p9(A,c16) | p9(f19(A),c15). [assumption]. 31 p2(f11(c5,A),c5) | -p2(f12(c5,A),c5) | -p6(A,c7) | p2(f11(c13,A),c5) | -p9(A,c14). [assumption]. 32 p2(f12(c5,A),c5) | -p9(A,c10) | -p6(A,c7) | -p2(f11(c5,A),c5) | -p2(f11(c13,A),c5). [assumption]. 33 p9(f24(A),c16) | -p9(A,c23). [assumption]. 34 -p9(A,c10) | -p2(f12(c5,A),c5) | -p6(A,c7) | p2(f11(c5,A),c5). [assumption]. 35 -p6(A,c7) | -p9(A,c10) | -p2(f12(c5,A),c5) | p2(f11(c13,A),c5). [assumption]. 36 -p2(f12(c5,A),c4) | p2(f11(c13,A),c4) | -p6(A,c7) | -p9(A,c14). [assumption]. 37 p2(f11(c5,A),c4) | -p2(f12(c5,A),c5) | -p6(A,c7) | -p9(A,c15). [assumption]. 38 -p2(f11(c13,A),c4) | -p9(A,c14) | p2(f12(c5,A),c4) | -p2(f11(c5,A),c4) | -p6(A,c7). [assumption]. 39 p9(f17(A),c10) | -p9(A,c16). [assumption]. 40 -p9(A,c23) | p9(f20(A),c14). [assumption]. 41 p2(f12(c5,A),c4) | -p9(A,c10) | -p2(f11(B,A),c4) | -p6(A,c7). [assumption]. 42 p2(f12(c5,A),c5) | -p6(A,c7) | -p9(A,c15) | -p2(f11(c5,A),c4). [assumption]. 43 p9(f20(A),c14) | -p9(A,c16). [assumption]. 44 -p2(f11(c5,A),c5) | p2(f12(c5,A),c4) | -p9(A,c15) | -p6(A,c7). [assumption]. 45 p9(f18(A),c10) | -p9(A,c16). [assumption]. 46 -p6(f19(f24(c26)),c8). [assumption]. 47 -p6(f17(f24(c26)),c8). [assumption]. 48 -p6(f18(f25(c26)),c8). [assumption]. 49 -p6(f18(f24(c26)),c8). [assumption]. 50 -p6(f17(f25(c26)),c8) | -p6(f20(c26),c8). [assumption]. 51 p2(f12(c21,c26),c5). [assumption]. 52 p2(f11(c13,c26),c4). [assumption]. 53 p2(f11(c22,c26),c5). [assumption]. 54 p2(f11(c5,c26),c5). [assumption]. 55 -p6(f20(f24(c26)),c8). [assumption]. 56 p9(c26,c23). [assumption]. 57 -p6(f19(f25(c26)),c8) | -p6(f20(c26),c8). [assumption]. 58 p2(f12(c22,c26),c4). [assumption]. 59 p2(f11(c13,f17(A)),B) | -p2(f12(c5,f19(A)),B) | -p9(A,c16). [resolve(1,a,2,b)]. 60 p2(f12(c5,f18(A)),B) | -p2(f12(c22,A),B) | -p9(A,c16). [resolve(1,a,3,a)]. 61 p2(f11(c5,f19(A)),B) | -p2(f12(c5,f18(A)),B) | -p9(A,c16). [resolve(1,a,4,b)]. 62 p2(f12(c5,f17(A)),B) | -p2(f12(c21,A),B) | -p9(A,c16). [resolve(1,a,5,a)]. 63 p2(f11(c5,f25(A)),B) | -p2(f11(c5,A),B) | -p9(A,c23). [resolve(1,a,6,b)]. 64 p2(f12(c21,f25(A)),B) | -p2(f12(c21,A),B) | -p9(A,c23). [resolve(1,a,7,a)]. 65 p2(f12(c5,f19(A)),B) | -p2(f11(c13,f17(A)),B) | -p9(A,c16). [resolve(8,b,2,b)]. 66 p2(f12(c22,A),B) | -p2(f12(c5,f18(A)),B) | -p9(A,c16). [resolve(8,b,3,a)]. 67 p2(f12(c5,f18(A)),B) | -p2(f11(c5,f19(A)),B) | -p9(A,c16). [resolve(8,b,4,b)]. 68 p2(f12(c21,A),B) | -p2(f12(c5,f17(A)),B) | -p9(A,c16). [resolve(8,b,5,a)]. 69 p2(f11(c5,A),B) | -p2(f11(c5,f25(A)),B) | -p9(A,c23). [resolve(8,b,6,b)]. 70 p2(f12(c21,A),B) | -p2(f12(c21,f25(A)),B) | -p9(A,c23). [resolve(8,b,7,a)]. 71 -p9(A,c16) | p2(f11(c5,f20(A)),B) | -p2(f11(c5,A),B). [resolve(9,a,1,a)]. 72 -p9(A,c16) | p2(f11(c5,A),B) | -p2(f11(c5,f20(A)),B). [resolve(9,a,8,b)]. 73 -p9(A,c16) | p2(f11(c5,f17(A)),B) | -p2(f12(c5,f20(A)),B). [resolve(10,b,1,a)]. 74 -p9(A,c16) | p2(f12(c5,f20(A)),B) | -p2(f11(c5,f17(A)),B). [resolve(10,b,8,b)]. 75 -p9(A,c23) | p2(f11(c13,f25(A)),B) | -p2(f12(c21,f24(A)),B). [resolve(11,a,1,a)]. 76 -p9(A,c23) | p2(f12(c21,f24(A)),B) | -p2(f11(c13,f25(A)),B). [resolve(11,a,8,b)]. 77 -p9(A,c23) | p2(f11(c5,f24(A)),B) | -p2(f11(c13,A),B). [resolve(12,a,1,a)]. 78 -p9(A,c23) | p2(f11(c13,A),B) | -p2(f11(c5,f24(A)),B). [resolve(12,a,8,b)]. 79 -p9(A,c23) | p2(f11(c13,f20(A)),B) | -p2(f12(c22,f24(A)),B). [resolve(13,a,1,a)]. 80 -p9(A,c23) | p2(f12(c22,f24(A)),B) | -p2(f11(c13,f20(A)),B). [resolve(13,a,8,b)]. 81 -p9(A,c23) | p2(f12(c5,f20(A)),B) | -p2(f12(c22,A),B). [resolve(14,a,1,a)]. 82 -p9(A,c23) | p2(f12(c22,A),B) | -p2(f12(c5,f20(A)),B). [resolve(14,a,8,b)]. 83 -p9(A,c16) | p2(f11(c13,f20(A)),B) | -p2(f11(c13,A),B). [resolve(15,b,1,a)]. 84 -p9(A,c16) | p2(f11(c13,A),B) | -p2(f11(c13,f20(A)),B). [resolve(15,b,8,b)]. 85 -p9(A,c16) | p2(f11(c5,f18(A)),B) | -p2(f11(c5,A),B). [resolve(16,a,1,a)]. 86 -p9(A,c16) | p2(f11(c5,A),B) | -p2(f11(c5,f18(A)),B). [resolve(16,a,8,b)]. 87 -p9(A,c23) | p2(f11(c13,f24(A)),B) | -p2(f11(c22,A),B). [resolve(17,a,1,a)]. 88 -p9(A,c23) | p2(f11(c22,A),B) | -p2(f11(c13,f24(A)),B). [resolve(17,a,8,b)]. 89 -p9(A,c16) | p2(f11(c13,f18(A)),B) | -p2(f11(c13,A),B). [resolve(18,b,1,a)]. 90 -p9(A,c16) | p2(f11(c13,A),B) | -p2(f11(c13,f18(A)),B). [resolve(18,b,8,b)]. 91 -p9(A,c23) | p2(f11(c5,f20(A)),B) | -p2(f12(c22,f25(A)),B). [resolve(19,b,1,a)]. 92 -p9(A,c23) | p2(f12(c22,f25(A)),B) | -p2(f11(c5,f20(A)),B). [resolve(19,b,8,b)]. 93 -p2(A,c5) | -p2(A,c4). [resolve(20,a,21,a)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=16): 23 -p2(f12(c5,A),c4) | -p9(A,c15) | p2(f11(c5,A),c5) | -p6(A,c7). [assumption]. given #2 (I,wt=7): 24 p9(f25(A),c16) | -p9(A,c23). [assumption]. given #3 (I,wt=16): 25 -p6(A,c7) | -p2(f11(B,A),c5) | -p9(A,c14) | p2(f12(c5,A),c5). [assumption]. given #4 (I,wt=16): 26 -p2(f12(c5,A),c4) | -p9(A,c14) | p2(f11(c5,A),c4) | -p6(A,c7). [assumption]. given #5 (I,wt=21): 27 p2(f11(c13,A),c4) | -p2(f12(c5,A),c4) | p2(f11(c5,A),c4) | -p6(A,c7) | -p9(A,c10). [assumption]. given #6 (I,wt=9): 28 p6(A,c7) | -p9(A,B) | p6(A,c8). [assumption]. given #7 (I,wt=6): 29 -p6(A,c8) | -p6(A,c7). [assumption]. given #8 (I,wt=7): 30 -p9(A,c16) | p9(f19(A),c15). [assumption]. given #9 (I,wt=21): 31 p2(f11(c5,A),c5) | -p2(f12(c5,A),c5) | -p6(A,c7) | p2(f11(c13,A),c5) | -p9(A,c14). [assumption]. given #10 (I,wt=21): 32 p2(f12(c5,A),c5) | -p9(A,c10) | -p6(A,c7) | -p2(f11(c5,A),c5) | -p2(f11(c13,A),c5). [assumption]. given #11 (I,wt=7): 33 p9(f24(A),c16) | -p9(A,c23). [assumption]. given #12 (I,wt=16): 34 -p9(A,c10) | -p2(f12(c5,A),c5) | -p6(A,c7) | p2(f11(c5,A),c5). [assumption]. given #13 (I,wt=16): 35 -p6(A,c7) | -p9(A,c10) | -p2(f12(c5,A),c5) | p2(f11(c13,A),c5). [assumption]. given #14 (I,wt=16): 36 -p2(f12(c5,A),c4) | p2(f11(c13,A),c4) | -p6(A,c7) | -p9(A,c14). [assumption]. given #15 (I,wt=16): 37 p2(f11(c5,A),c4) | -p2(f12(c5,A),c5) | -p6(A,c7) | -p9(A,c15). [assumption]. given #16 (I,wt=21): 38 -p2(f11(c13,A),c4) | -p9(A,c14) | p2(f12(c5,A),c4) | -p2(f11(c5,A),c4) | -p6(A,c7). [assumption]. given #17 (I,wt=7): 39 p9(f17(A),c10) | -p9(A,c16). [assumption]. given #18 (I,wt=7): 40 -p9(A,c23) | p9(f20(A),c14). [assumption]. given #19 (I,wt=16): 41 p2(f12(c5,A),c4) | -p9(A,c10) | -p2(f11(B,A),c4) | -p6(A,c7). [assumption]. given #20 (I,wt=16): 42 p2(f12(c5,A),c5) | -p6(A,c7) | -p9(A,c15) | -p2(f11(c5,A),c4). [assumption]. given #21 (I,wt=7): 43 p9(f20(A),c14) | -p9(A,c16). [assumption]. given #22 (I,wt=16): 44 -p2(f11(c5,A),c5) | p2(f12(c5,A),c4) | -p9(A,c15) | -p6(A,c7). [assumption]. given #23 (I,wt=7): 45 p9(f18(A),c10) | -p9(A,c16). [assumption]. given #24 (I,wt=5): 46 -p6(f19(f24(c26)),c8). [assumption]. given #25 (I,wt=5): 47 -p6(f17(f24(c26)),c8). [assumption]. given #26 (I,wt=5): 48 -p6(f18(f25(c26)),c8). [assumption]. given #27 (I,wt=5): 49 -p6(f18(f24(c26)),c8). [assumption]. given #28 (I,wt=9): 50 -p6(f17(f25(c26)),c8) | -p6(f20(c26),c8). [assumption]. given #29 (I,wt=5): 51 p2(f12(c21,c26),c5). [assumption]. given #30 (I,wt=5): 52 p2(f11(c13,c26),c4). [assumption]. given #31 (I,wt=5): 53 p2(f11(c22,c26),c5). [assumption]. given #32 (I,wt=5): 54 p2(f11(c5,c26),c5). [assumption]. given #33 (I,wt=5): 55 -p6(f20(f24(c26)),c8). [assumption]. given #34 (I,wt=3): 56 p9(c26,c23). [assumption]. given #35 (I,wt=9): 57 -p6(f19(f25(c26)),c8) | -p6(f20(c26),c8). [assumption]. given #36 (I,wt=5): 58 p2(f12(c22,c26),c4). [assumption]. given #37 (I,wt=15): 59 p2(f11(c13,f17(A)),B) | -p2(f12(c5,f19(A)),B) | -p9(A,c16). [resolve(1,a,2,b)]. given #38 (I,wt=14): 60 p2(f12(c5,f18(A)),B) | -p2(f12(c22,A),B) | -p9(A,c16). [resolve(1,a,3,a)]. given #39 (I,wt=15): 61 p2(f11(c5,f19(A)),B) | -p2(f12(c5,f18(A)),B) | -p9(A,c16). [resolve(1,a,4,b)]. given #40 (I,wt=14): 62 p2(f12(c5,f17(A)),B) | -p2(f12(c21,A),B) | -p9(A,c16). [resolve(1,a,5,a)]. given #41 (I,wt=14): 63 p2(f11(c5,f25(A)),B) | -p2(f11(c5,A),B) | -p9(A,c23). [resolve(1,a,6,b)]. given #42 (I,wt=14): 64 p2(f12(c21,f25(A)),B) | -p2(f12(c21,A),B) | -p9(A,c23). [resolve(1,a,7,a)]. given #43 (I,wt=15): 65 p2(f12(c5,f19(A)),B) | -p2(f11(c13,f17(A)),B) | -p9(A,c16). [resolve(8,b,2,b)]. given #44 (I,wt=14): 66 p2(f12(c22,A),B) | -p2(f12(c5,f18(A)),B) | -p9(A,c16). [resolve(8,b,3,a)]. given #45 (I,wt=15): 67 p2(f12(c5,f18(A)),B) | -p2(f11(c5,f19(A)),B) | -p9(A,c16). [resolve(8,b,4,b)]. given #46 (I,wt=14): 68 p2(f12(c21,A),B) | -p2(f12(c5,f17(A)),B) | -p9(A,c16). [resolve(8,b,5,a)]. given #47 (I,wt=14): 69 p2(f11(c5,A),B) | -p2(f11(c5,f25(A)),B) | -p9(A,c23). [resolve(8,b,6,b)]. given #48 (I,wt=14): 70 p2(f12(c21,A),B) | -p2(f12(c21,f25(A)),B) | -p9(A,c23). [resolve(8,b,7,a)]. given #49 (I,wt=14): 71 -p9(A,c16) | p2(f11(c5,f20(A)),B) | -p2(f11(c5,A),B). [resolve(9,a,1,a)]. given #50 (I,wt=14): 72 -p9(A,c16) | p2(f11(c5,A),B) | -p2(f11(c5,f20(A)),B). [resolve(9,a,8,b)]. given #51 (I,wt=15): 73 -p9(A,c16) | p2(f11(c5,f17(A)),B) | -p2(f12(c5,f20(A)),B). [resolve(10,b,1,a)]. given #52 (I,wt=15): 74 -p9(A,c16) | p2(f12(c5,f20(A)),B) | -p2(f11(c5,f17(A)),B). [resolve(10,b,8,b)]. given #53 (I,wt=15): 75 -p9(A,c23) | p2(f11(c13,f25(A)),B) | -p2(f12(c21,f24(A)),B). [resolve(11,a,1,a)]. given #54 (I,wt=15): 76 -p9(A,c23) | p2(f12(c21,f24(A)),B) | -p2(f11(c13,f25(A)),B). [resolve(11,a,8,b)]. given #55 (I,wt=14): 77 -p9(A,c23) | p2(f11(c5,f24(A)),B) | -p2(f11(c13,A),B). [resolve(12,a,1,a)]. given #56 (I,wt=14): 78 -p9(A,c23) | p2(f11(c13,A),B) | -p2(f11(c5,f24(A)),B). [resolve(12,a,8,b)]. given #57 (I,wt=15): 79 -p9(A,c23) | p2(f11(c13,f20(A)),B) | -p2(f12(c22,f24(A)),B). [resolve(13,a,1,a)]. given #58 (I,wt=15): 80 -p9(A,c23) | p2(f12(c22,f24(A)),B) | -p2(f11(c13,f20(A)),B). [resolve(13,a,8,b)]. given #59 (I,wt=14): 81 -p9(A,c23) | p2(f12(c5,f20(A)),B) | -p2(f12(c22,A),B). [resolve(14,a,1,a)]. given #60 (I,wt=14): 82 -p9(A,c23) | p2(f12(c22,A),B) | -p2(f12(c5,f20(A)),B). [resolve(14,a,8,b)]. given #61 (I,wt=14): 83 -p9(A,c16) | p2(f11(c13,f20(A)),B) | -p2(f11(c13,A),B). [resolve(15,b,1,a)]. given #62 (I,wt=14): 84 -p9(A,c16) | p2(f11(c13,A),B) | -p2(f11(c13,f20(A)),B). [resolve(15,b,8,b)]. given #63 (I,wt=14): 85 -p9(A,c16) | p2(f11(c5,f18(A)),B) | -p2(f11(c5,A),B). [resolve(16,a,1,a)]. given #64 (I,wt=14): 86 -p9(A,c16) | p2(f11(c5,A),B) | -p2(f11(c5,f18(A)),B). [resolve(16,a,8,b)]. given #65 (I,wt=14): 87 -p9(A,c23) | p2(f11(c13,f24(A)),B) | -p2(f11(c22,A),B). [resolve(17,a,1,a)]. given #66 (I,wt=14): 88 -p9(A,c23) | p2(f11(c22,A),B) | -p2(f11(c13,f24(A)),B). [resolve(17,a,8,b)]. given #67 (I,wt=14): 89 -p9(A,c16) | p2(f11(c13,f18(A)),B) | -p2(f11(c13,A),B). [resolve(18,b,1,a)]. given #68 (I,wt=14): 90 -p9(A,c16) | p2(f11(c13,A),B) | -p2(f11(c13,f18(A)),B). [resolve(18,b,8,b)]. given #69 (I,wt=15): 91 -p9(A,c23) | p2(f11(c5,f20(A)),B) | -p2(f12(c22,f25(A)),B). [resolve(19,b,1,a)]. given #70 (I,wt=15): 92 -p9(A,c23) | p2(f12(c22,f25(A)),B) | -p2(f11(c5,f20(A)),B). [resolve(19,b,8,b)]. given #71 (I,wt=6): 93 -p2(A,c5) | -p2(A,c4). [resolve(20,a,21,a)]. given #72 (F,wt=5): 114 -p2(f12(c22,c26),c5). [resolve(93,b,58,a)]. given #73 (F,wt=5): 115 -p2(f11(c13,c26),c5). [resolve(93,b,52,a)]. given #74 (T,wt=4): 94 p9(f20(c26),c14). [resolve(56,a,40,a)]. given #75 (T,wt=4): 95 p9(f24(c26),c16). [resolve(56,a,33,b)]. given #76 (A,wt=6): 96 p6(c26,c7) | p6(c26,c8). [resolve(56,a,28,b)]. given #77 (F,wt=5): 116 -p2(f11(c5,c26),c4). [ur(93,a,54,a)]. given #78 (F,wt=5): 117 -p2(f11(c22,c26),c4). [ur(93,a,53,a)]. given #79 (T,wt=4): 97 p9(f25(c26),c16). [resolve(56,a,24,b)]. given #80 (T,wt=5): 140 p9(f18(f24(c26)),c10). [resolve(95,a,45,b)]. given #81 (A,wt=11): 98 p2(f11(c5,f25(c26)),A) | -p2(f11(c5,c26),A). [resolve(63,c,56,a)]. given #82 (F,wt=5): 118 -p2(f12(c21,c26),c4). [ur(93,a,51,a)]. given #83 (F,wt=6): 119 -p2(f12(c5,f20(c26)),c5). [ur(82,a,56,a,b,114,a)]. given #84 (T,wt=5): 141 p9(f20(f24(c26)),c14). [resolve(95,a,43,b)]. given #85 (T,wt=5): 142 p9(f17(f24(c26)),c10). [resolve(95,a,39,b)]. given #86 (A,wt=11): 99 p2(f12(c21,f25(c26)),A) | -p2(f12(c21,c26),A). [resolve(64,c,56,a)]. given #87 (F,wt=6): 120 -p2(f11(c5,f24(c26)),c5). [ur(78,a,56,a,b,115,a)]. given #88 (F,wt=6): 145 -p2(f11(c5,f25(c26)),c4). [ur(69,a,116,a,c,56,a)]. given #89 (T,wt=5): 143 p9(f19(f24(c26)),c15). [resolve(95,a,30,a)]. given #90 (T,wt=5): 165 p9(f18(f25(c26)),c10). [resolve(97,a,45,b)]. given #91 (A,wt=11): 100 p2(f11(c5,c26),A) | -p2(f11(c5,f25(c26)),A). [resolve(69,c,56,a)]. given #92 (F,wt=6): 146 -p2(f11(c13,f24(c26)),c4). [ur(88,a,56,a,b,117,a)]. given #93 (F,wt=6): 172 -p2(f12(c21,f25(c26)),c4). [ur(70,a,118,a,c,56,a)]. given #94 (T,wt=5): 166 p9(f20(f25(c26)),c14). [resolve(97,a,43,b)]. given #95 (T,wt=5): 167 p9(f17(f25(c26)),c10). [resolve(97,a,39,b)]. given #96 (A,wt=11): 101 p2(f12(c21,c26),A) | -p2(f12(c21,f25(c26)),A). [resolve(70,c,56,a)]. given #97 (F,wt=7): 176 -p2(f11(c5,f18(f24(c26))),c5). [ur(86,a,95,a,b,120,a)]. given #98 (F,wt=7): 177 -p2(f11(c5,f20(f24(c26))),c5). [ur(72,a,95,a,b,120,a)]. given #99 (T,wt=5): 168 p9(f19(f25(c26)),c15). [resolve(97,a,30,a)]. given #100 (T,wt=5): 170 p6(f18(f24(c26)),c7). [resolve(140,a,28,b),unit_del(b,49)]. given #101 (A,wt=12): 102 p2(f11(c13,f25(c26)),A) | -p2(f12(c21,f24(c26)),A). [resolve(75,a,56,a)]. given #102 (F,wt=7): 178 -p2(f11(c5,f18(f25(c26))),c4). [ur(86,a,97,a,b,145,a)]. given #103 (F,wt=7): 179 -p2(f11(c5,f20(f25(c26))),c4). [ur(72,a,97,a,b,145,a)]. given #104 (T,wt=5): 173 p6(f20(f24(c26)),c7). [resolve(141,a,28,b),unit_del(b,55)]. given #105 (T,wt=5): 174 p6(f17(f24(c26)),c7). [resolve(142,a,28,b),unit_del(b,47)]. given #106 (A,wt=12): 103 p2(f12(c21,f24(c26)),A) | -p2(f11(c13,f25(c26)),A). [resolve(76,a,56,a)]. given #107 (F,wt=7): 182 -p2(f11(c13,f18(f24(c26))),c4). [ur(90,a,95,a,b,146,a)]. given #108 (F,wt=7): 183 -p2(f11(c13,f20(f24(c26))),c4). [ur(84,a,95,a,b,146,a)]. given #109 (T,wt=5): 180 p6(f19(f24(c26)),c7). [resolve(143,a,28,b),unit_del(b,46)]. given #110 (T,wt=5): 181 p6(f18(f25(c26)),c7). [resolve(165,a,28,b),unit_del(b,48)]. given #111 (A,wt=11): 104 p2(f11(c5,f24(c26)),A) | -p2(f11(c13,c26),A). [resolve(77,a,56,a)]. given #112 (F,wt=7): 184 -p2(f12(c5,f17(f25(c26))),c4). [ur(68,a,172,a,c,97,a)]. given #113 (F,wt=7): 193 -p2(f12(c5,f18(f24(c26))),c5). [resolve(170,a,34,c),unit_del(a,140),unit_del(c,176)]. given #114 (T,wt=6): 171 p2(f11(c5,f25(c26)),c5). [resolve(98,b,54,a)]. given #115 (T,wt=6): 175 p2(f12(c21,f25(c26)),c5). [resolve(99,b,51,a)]. given #116 (A,wt=11): 105 p2(f11(c13,c26),A) | -p2(f11(c5,f24(c26)),A). [resolve(78,a,56,a)]. given #117 (F,wt=6): 246 -p2(f12(c22,f24(c26)),c5). [ur(60,a,193,a,c,95,a)]. given #118 (F,wt=6): 252 -p2(f11(c13,f20(c26)),c5). [ur(80,a,56,a,b,246,a)]. given #119 (T,wt=6): 244 p2(f11(c5,f24(c26)),c4). [resolve(104,b,52,a)]. given #120 (T,wt=8): 121 p6(f20(c26),c7) | p6(f20(c26),c8). [resolve(94,a,28,b)]. given #121 (A,wt=12): 106 p2(f11(c13,f20(c26)),A) | -p2(f12(c22,f24(c26)),A). [resolve(79,a,56,a)]. given #122 (F,wt=7): 201 -p2(f12(c5,f20(f24(c26))),c4). [resolve(173,a,36,c),unit_del(b,183),unit_del(c,141)]. given #123 (F,wt=7): 245 -p2(f11(c5,f19(f24(c26))),c5). [ur(67,a,193,a,c,95,a)]. given #124 (T,wt=8): 144 p6(f24(c26),c7) | p6(f24(c26),c8). [resolve(95,a,28,b)]. given #125 (T,wt=8): 169 p6(f25(c26),c7) | p6(f25(c26),c8). [resolve(97,a,28,b)]. given #126 (A,wt=12): 107 p2(f12(c22,f24(c26)),A) | -p2(f11(c13,f20(c26)),A). [resolve(80,a,56,a)]. given #127 (F,wt=7): 247 -p2(f12(c5,f19(f24(c26))),c4). [back_unit_del(232),unit_del(b,245)]. given #128 (F,wt=7): 258 -p2(f12(c5,f17(f24(c26))),c4). [back_unit_del(255),unit_del(a,257)]. given #129 (T,wt=10): 185 p6(f20(f25(c26)),c7) | p6(f20(f25(c26)),c8). [resolve(166,a,28,b)]. given #130 (T,wt=10): 186 p6(f17(f25(c26)),c7) | p6(f17(f25(c26)),c8). [resolve(167,a,28,b)]. given #131 (A,wt=11): 108 p2(f12(c5,f20(c26)),A) | -p2(f12(c22,c26),A). [resolve(81,a,56,a)]. given #132 (F,wt=6): 261 -p2(f12(c21,f24(c26)),c4). [ur(62,a,258,a,c,95,a)]. given #133 (F,wt=6): 264 -p2(f11(c13,f25(c26)),c4). [ur(103,a,261,a)]. given #134 (T,wt=6): 263 p2(f12(c5,f20(c26)),c4). [resolve(108,b,58,a)]. given #135 (T,wt=9): 262 p6(f17(f25(c26)),c7) | -p6(f20(c26),c8). [resolve(186,b,50,a)]. given #136 (A,wt=11): 109 p2(f12(c22,c26),A) | -p2(f12(c5,f20(c26)),A). [resolve(82,a,56,a)]. given #137 (F,wt=7): 259 -p2(f11(A,f17(f24(c26))),c4). [back_unit_del(209),unit_del(a,258)]. given #138 (F,wt=7): 266 -p2(f11(c13,f20(f25(c26))),c4). [ur(84,a,97,a,b,264,a)]. given #139 (T,wt=9): 270 p6(f17(f25(c26)),c7) | p6(f20(c26),c7). [resolve(262,b,121,b)]. given #140 (T,wt=10): 187 p6(f19(f25(c26)),c7) | p6(f19(f25(c26)),c8). [resolve(168,a,28,b)]. given #141 (A,wt=11): 110 p2(f11(c13,f24(c26)),A) | -p2(f11(c22,c26),A). [resolve(87,a,56,a)]. given #142 (F,wt=7): 267 -p2(f12(c5,f18(f25(c26))),c4). [back_unit_del(240),unit_del(a,265)]. given #143 (F,wt=6): 282 -p2(f12(c22,f25(c26)),c4). [ur(60,a,267,a,c,97,a)]. given #144 (T,wt=6): 280 p2(f11(c13,f24(c26)),c5). [resolve(110,b,53,a)]. given #145 (T,wt=9): 279 p6(f19(f25(c26)),c7) | -p6(f20(c26),c8). [resolve(187,b,57,a)]. given #146 (A,wt=11): 111 p2(f11(c22,c26),A) | -p2(f11(c13,f24(c26)),A). [resolve(88,a,56,a)]. given #147 (F,wt=6): 283 -p2(f11(c5,f20(c26)),c4). [ur(92,a,56,a,b,282,a)]. given #148 (F,wt=4): 285 -p6(f20(c26),c7). [ur(26,a,263,a,b,94,a,c,283,a)]. given #149 (T,wt=4): 295 p6(f20(c26),c8). [back_unit_del(121),unit_del(a,285)]. given #150 (T,wt=5): 286 p6(f19(f25(c26)),c7). [back_unit_del(284),unit_del(b,285)]. given #151 (A,wt=12): 112 p2(f11(c5,f20(c26)),A) | -p2(f12(c22,f25(c26)),A). [resolve(91,a,56,a)]. given #152 (F,wt=5): 297 -p6(f19(f25(c26)),c8). [back_unit_del(57),unit_del(b,295)]. given #153 (F,wt=5): 298 -p6(f17(f25(c26)),c8). [back_unit_del(50),unit_del(b,295)]. given #154 (T,wt=5): 294 p6(f17(f25(c26)),c7). [back_unit_del(270),unit_del(b,285)]. given #155 (T,wt=12): 113 p2(f12(c22,f25(c26)),A) | -p2(f11(c5,f20(c26)),A). [resolve(92,a,56,a)]. given #156 (A,wt=13): 122 p2(f11(c13,f24(c26)),A) | -p2(f11(c13,f18(f24(c26))),A). [resolve(95,a,90,a)]. given #157 (F,wt=7): 268 -p2(f11(A,f18(f25(c26))),c4). [back_unit_del(234),unit_del(a,267)]. given #158 (F,wt=7): 281 -p2(f11(c5,f19(f25(c26))),c4). [ur(67,a,267,a,c,97,a)]. given #159 (T,wt=13): 123 p2(f11(c13,f18(f24(c26))),A) | -p2(f11(c13,f24(c26)),A). [resolve(95,a,89,a)]. given #160 (T,wt=7): 308 p2(f11(c13,f18(f24(c26))),c5). [resolve(123,b,280,a)]. given #161 (A,wt=13): 124 p2(f11(c5,f24(c26)),A) | -p2(f11(c5,f18(f24(c26))),A). [resolve(95,a,86,a)]. given #162 (F,wt=5): 309 -p9(f18(f24(c26)),c14). [ur(25,a,170,a,b,308,a,d,193,a)]. given #163 (F,wt=7): 292 -p2(f11(A,f17(f25(c26))),c4). [back_unit_del(273),unit_del(a,285)]. given #164 (T,wt=13): 125 p2(f11(c5,f18(f24(c26))),A) | -p2(f11(c5,f24(c26)),A). [resolve(95,a,85,a)]. given #165 (T,wt=7): 314 p2(f11(c5,f18(f24(c26))),c4). [resolve(125,b,244,a)]. given #166 (A,wt=13): 126 p2(f11(c13,f24(c26)),A) | -p2(f11(c13,f20(f24(c26))),A). [resolve(95,a,84,a)]. given #167 (F,wt=5): 315 -p9(f18(f24(c26)),c15). [back_unit_del(197),unit_del(b,314)]. given #168 (F,wt=7): 301 -p2(f12(c5,f19(f25(c26))),c5). [resolve(286,a,37,c),unit_del(a,281),unit_del(c,168)]. given #169 (T,wt=13): 127 p2(f11(c13,f20(f24(c26))),A) | -p2(f11(c13,f24(c26)),A). [resolve(95,a,83,a)]. given #170 (T,wt=7): 319 p2(f11(c13,f20(f24(c26))),c5). [resolve(127,b,280,a)]. given #171 (A,wt=14): 128 p2(f12(c5,f20(f24(c26))),A) | -p2(f11(c5,f17(f24(c26))),A). [resolve(95,a,74,a)]. given #172 (F,wt=7): 310 -p2(f12(c5,f20(f25(c26))),c4). [ur(73,a,97,a,b,292,a)]. given #173 (F,wt=7): 311 -p2(f12(c5,f19(f25(c26))),c4). [ur(59,a,292,a,c,97,a)]. given #174 (T,wt=13): 130 p2(f11(c5,f24(c26)),A) | -p2(f11(c5,f20(f24(c26))),A). [resolve(95,a,72,a)]. given #175 (T,wt=13): 131 p2(f11(c5,f20(f24(c26))),A) | -p2(f11(c5,f24(c26)),A). [resolve(95,a,71,a)]. given #176 (A,wt=14): 129 p2(f11(c5,f17(f24(c26))),A) | -p2(f12(c5,f20(f24(c26))),A). [resolve(95,a,73,a)]. given #177 (F,wt=7): 313 -p2(f11(c5,f19(f25(c26))),c5). [back_unit_del(299),unit_del(b,311)]. given #178 (F,wt=7): 316 -p2(f11(c13,f17(f25(c26))),c5). [ur(65,a,301,a,c,97,a)]. given #179 (T,wt=7): 320 p2(f11(c5,f20(f24(c26))),c4). [resolve(131,b,244,a)]. given #180 (T,wt=12): 321 p2(f12(c5,f20(f24(c26))),c5) | -p9(f20(f24(c26)),c15). [back_unit_del(198),unit_del(c,320)]. given #181 (A,wt=13): 132 p2(f12(c21,f24(c26)),A) | -p2(f12(c5,f17(f24(c26))),A). [resolve(95,a,68,c)]. given #182 (F,wt=5): 325 -p9(f20(f24(c26)),c10). [ur(41,a,201,a,c,320,a,d,173,a)]. given #183 (F,wt=7): 317 -p2(f12(c5,f17(f25(c26))),c5). [back_unit_del(290),unit_del(b,316)]. ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.00) seconds. % Length of proof is 125. % Level of proof is 21. % Maximum clause weight is 21. % Given clauses 183. 1 -p1(A,B) | p2(B,C) | -p2(A,C). [assumption]. 2 -p9(A,c16) | p1(f12(c5,f19(A)),f11(c13,f17(A))). [assumption]. 3 p1(f12(c22,A),f12(c5,f18(A))) | -p9(A,c16). [assumption]. 4 -p9(A,c16) | p1(f12(c5,f18(A)),f11(c5,f19(A))). [assumption]. 5 p1(f12(c21,A),f12(c5,f17(A))) | -p9(A,c16). [assumption]. 6 -p9(A,c23) | p1(f11(c5,A),f11(c5,f25(A))). [assumption]. 7 p1(f12(c21,A),f12(c21,f25(A))) | -p9(A,c23). [assumption]. 8 p2(A,B) | -p1(A,C) | -p2(C,B). [assumption]. 10 -p9(A,c16) | p1(f12(c5,f20(A)),f11(c5,f17(A))). [assumption]. 11 p1(f12(c21,f24(A)),f11(c13,f25(A))) | -p9(A,c23). [assumption]. 12 p1(f11(c13,A),f11(c5,f24(A))) | -p9(A,c23). [assumption]. 14 p1(f12(c22,A),f12(c5,f20(A))) | -p9(A,c23). [assumption]. 15 -p9(A,c16) | p1(f11(c13,A),f11(c13,f20(A))). [assumption]. 16 p1(f11(c5,A),f11(c5,f18(A))) | -p9(A,c16). [assumption]. 17 p1(f11(c22,A),f11(c13,f24(A))) | -p9(A,c23). [assumption]. 18 -p9(A,c16) | p1(f11(c13,A),f11(c13,f18(A))). [assumption]. 19 -p9(A,c23) | p1(f12(c22,f25(A)),f11(c5,f20(A))). [assumption]. 20 p3(A,B) | -p2(C,B) | -p2(C,A). [assumption]. 21 -p3(c4,c5). [assumption]. 23 -p2(f12(c5,A),c4) | -p9(A,c15) | p2(f11(c5,A),c5) | -p6(A,c7). [assumption]. 24 p9(f25(A),c16) | -p9(A,c23). [assumption]. 26 -p2(f12(c5,A),c4) | -p9(A,c14) | p2(f11(c5,A),c4) | -p6(A,c7). [assumption]. 27 p2(f11(c13,A),c4) | -p2(f12(c5,A),c4) | p2(f11(c5,A),c4) | -p6(A,c7) | -p9(A,c10). [assumption]. 28 p6(A,c7) | -p9(A,B) | p6(A,c8). [assumption]. 30 -p9(A,c16) | p9(f19(A),c15). [assumption]. 33 p9(f24(A),c16) | -p9(A,c23). [assumption]. 34 -p9(A,c10) | -p2(f12(c5,A),c5) | -p6(A,c7) | p2(f11(c5,A),c5). [assumption]. 35 -p6(A,c7) | -p9(A,c10) | -p2(f12(c5,A),c5) | p2(f11(c13,A),c5). [assumption]. 36 -p2(f12(c5,A),c4) | p2(f11(c13,A),c4) | -p6(A,c7) | -p9(A,c14). [assumption]. 37 p2(f11(c5,A),c4) | -p2(f12(c5,A),c5) | -p6(A,c7) | -p9(A,c15). [assumption]. 39 p9(f17(A),c10) | -p9(A,c16). [assumption]. 40 -p9(A,c23) | p9(f20(A),c14). [assumption]. 43 p9(f20(A),c14) | -p9(A,c16). [assumption]. 45 p9(f18(A),c10) | -p9(A,c16). [assumption]. 46 -p6(f19(f24(c26)),c8). [assumption]. 47 -p6(f17(f24(c26)),c8). [assumption]. 48 -p6(f18(f25(c26)),c8). [assumption]. 49 -p6(f18(f24(c26)),c8). [assumption]. 50 -p6(f17(f25(c26)),c8) | -p6(f20(c26),c8). [assumption]. 51 p2(f12(c21,c26),c5). [assumption]. 52 p2(f11(c13,c26),c4). [assumption]. 53 p2(f11(c22,c26),c5). [assumption]. 54 p2(f11(c5,c26),c5). [assumption]. 55 -p6(f20(f24(c26)),c8). [assumption]. 56 p9(c26,c23). [assumption]. 57 -p6(f19(f25(c26)),c8) | -p6(f20(c26),c8). [assumption]. 58 p2(f12(c22,c26),c4). [assumption]. 60 p2(f12(c5,f18(A)),B) | -p2(f12(c22,A),B) | -p9(A,c16). [resolve(1,a,3,a)]. 62 p2(f12(c5,f17(A)),B) | -p2(f12(c21,A),B) | -p9(A,c16). [resolve(1,a,5,a)]. 64 p2(f12(c21,f25(A)),B) | -p2(f12(c21,A),B) | -p9(A,c23). [resolve(1,a,7,a)]. 65 p2(f12(c5,f19(A)),B) | -p2(f11(c13,f17(A)),B) | -p9(A,c16). [resolve(8,b,2,b)]. 67 p2(f12(c5,f18(A)),B) | -p2(f11(c5,f19(A)),B) | -p9(A,c16). [resolve(8,b,4,b)]. 69 p2(f11(c5,A),B) | -p2(f11(c5,f25(A)),B) | -p9(A,c23). [resolve(8,b,6,b)]. 74 -p9(A,c16) | p2(f12(c5,f20(A)),B) | -p2(f11(c5,f17(A)),B). [resolve(10,b,8,b)]. 76 -p9(A,c23) | p2(f12(c21,f24(A)),B) | -p2(f11(c13,f25(A)),B). [resolve(11,a,8,b)]. 78 -p9(A,c23) | p2(f11(c13,A),B) | -p2(f11(c5,f24(A)),B). [resolve(12,a,8,b)]. 81 -p9(A,c23) | p2(f12(c5,f20(A)),B) | -p2(f12(c22,A),B). [resolve(14,a,1,a)]. 84 -p9(A,c16) | p2(f11(c13,A),B) | -p2(f11(c13,f20(A)),B). [resolve(15,b,8,b)]. 86 -p9(A,c16) | p2(f11(c5,A),B) | -p2(f11(c5,f18(A)),B). [resolve(16,a,8,b)]. 88 -p9(A,c23) | p2(f11(c22,A),B) | -p2(f11(c13,f24(A)),B). [resolve(17,a,8,b)]. 90 -p9(A,c16) | p2(f11(c13,A),B) | -p2(f11(c13,f18(A)),B). [resolve(18,b,8,b)]. 92 -p9(A,c23) | p2(f12(c22,f25(A)),B) | -p2(f11(c5,f20(A)),B). [resolve(19,b,8,b)]. 93 -p2(A,c5) | -p2(A,c4). [resolve(20,a,21,a)]. 94 p9(f20(c26),c14). [resolve(56,a,40,a)]. 95 p9(f24(c26),c16). [resolve(56,a,33,b)]. 97 p9(f25(c26),c16). [resolve(56,a,24,b)]. 99 p2(f12(c21,f25(c26)),A) | -p2(f12(c21,c26),A). [resolve(64,c,56,a)]. 103 p2(f12(c21,f24(c26)),A) | -p2(f11(c13,f25(c26)),A). [resolve(76,a,56,a)]. 108 p2(f12(c5,f20(c26)),A) | -p2(f12(c22,c26),A). [resolve(81,a,56,a)]. 115 -p2(f11(c13,c26),c5). [resolve(93,b,52,a)]. 116 -p2(f11(c5,c26),c4). [ur(93,a,54,a)]. 117 -p2(f11(c22,c26),c4). [ur(93,a,53,a)]. 120 -p2(f11(c5,f24(c26)),c5). [ur(78,a,56,a,b,115,a)]. 121 p6(f20(c26),c7) | p6(f20(c26),c8). [resolve(94,a,28,b)]. 140 p9(f18(f24(c26)),c10). [resolve(95,a,45,b)]. 141 p9(f20(f24(c26)),c14). [resolve(95,a,43,b)]. 142 p9(f17(f24(c26)),c10). [resolve(95,a,39,b)]. 143 p9(f19(f24(c26)),c15). [resolve(95,a,30,a)]. 145 -p2(f11(c5,f25(c26)),c4). [ur(69,a,116,a,c,56,a)]. 146 -p2(f11(c13,f24(c26)),c4). [ur(88,a,56,a,b,117,a)]. 165 p9(f18(f25(c26)),c10). [resolve(97,a,45,b)]. 167 p9(f17(f25(c26)),c10). [resolve(97,a,39,b)]. 168 p9(f19(f25(c26)),c15). [resolve(97,a,30,a)]. 170 p6(f18(f24(c26)),c7). [resolve(140,a,28,b),unit_del(b,49)]. 173 p6(f20(f24(c26)),c7). [resolve(141,a,28,b),unit_del(b,55)]. 174 p6(f17(f24(c26)),c7). [resolve(142,a,28,b),unit_del(b,47)]. 175 p2(f12(c21,f25(c26)),c5). [resolve(99,b,51,a)]. 176 -p2(f11(c5,f18(f24(c26))),c5). [ur(86,a,95,a,b,120,a)]. 178 -p2(f11(c5,f18(f25(c26))),c4). [ur(86,a,97,a,b,145,a)]. 180 p6(f19(f24(c26)),c7). [resolve(143,a,28,b),unit_del(b,46)]. 181 p6(f18(f25(c26)),c7). [resolve(165,a,28,b),unit_del(b,48)]. 183 -p2(f11(c13,f20(f24(c26))),c4). [ur(84,a,95,a,b,146,a)]. 186 p6(f17(f25(c26)),c7) | p6(f17(f25(c26)),c8). [resolve(167,a,28,b)]. 187 p6(f19(f25(c26)),c7) | p6(f19(f25(c26)),c8). [resolve(168,a,28,b)]. 193 -p2(f12(c5,f18(f24(c26))),c5). [resolve(170,a,34,c),unit_del(a,140),unit_del(c,176)]. 201 -p2(f12(c5,f20(f24(c26))),c4). [resolve(173,a,36,c),unit_del(b,183),unit_del(c,141)]. 215 p2(f11(c13,f17(f24(c26))),c4) | -p2(f12(c5,f17(f24(c26))),c4) | p2(f11(c5,f17(f24(c26))),c4). [resolve(174,a,27,d),unit_del(d,142)]. 232 -p2(f12(c5,f19(f24(c26))),c4) | p2(f11(c5,f19(f24(c26))),c5). [resolve(180,a,23,d),unit_del(b,143)]. 240 p2(f11(c13,f18(f25(c26))),c4) | -p2(f12(c5,f18(f25(c26))),c4). [resolve(181,a,27,d),unit_del(c,178),unit_del(d,165)]. 245 -p2(f11(c5,f19(f24(c26))),c5). [ur(67,a,193,a,c,95,a)]. 247 -p2(f12(c5,f19(f24(c26))),c4). [back_unit_del(232),unit_del(b,245)]. 253 -p2(f11(c5,f17(f24(c26))),c4). [ur(74,a,95,a,b,201,a)]. 255 p2(f11(c13,f17(f24(c26))),c4) | -p2(f12(c5,f17(f24(c26))),c4). [back_unit_del(215),unit_del(c,253)]. 257 -p2(f11(c13,f17(f24(c26))),c4). [ur(65,a,247,a,c,95,a)]. 258 -p2(f12(c5,f17(f24(c26))),c4). [back_unit_del(255),unit_del(a,257)]. 261 -p2(f12(c21,f24(c26)),c4). [ur(62,a,258,a,c,95,a)]. 262 p6(f17(f25(c26)),c7) | -p6(f20(c26),c8). [resolve(186,b,50,a)]. 263 p2(f12(c5,f20(c26)),c4). [resolve(108,b,58,a)]. 264 -p2(f11(c13,f25(c26)),c4). [ur(103,a,261,a)]. 265 -p2(f11(c13,f18(f25(c26))),c4). [ur(90,a,97,a,b,264,a)]. 267 -p2(f12(c5,f18(f25(c26))),c4). [back_unit_del(240),unit_del(a,265)]. 270 p6(f17(f25(c26)),c7) | p6(f20(c26),c7). [resolve(262,b,121,b)]. 275 p6(f20(c26),c7) | -p2(f12(c5,f17(f25(c26))),c5) | p2(f11(c13,f17(f25(c26))),c5). [resolve(270,a,35,a),unit_del(b,167)]. 279 p6(f19(f25(c26)),c7) | -p6(f20(c26),c8). [resolve(187,b,57,a)]. 281 -p2(f11(c5,f19(f25(c26))),c4). [ur(67,a,267,a,c,97,a)]. 282 -p2(f12(c22,f25(c26)),c4). [ur(60,a,267,a,c,97,a)]. 283 -p2(f11(c5,f20(c26)),c4). [ur(92,a,56,a,b,282,a)]. 284 p6(f19(f25(c26)),c7) | p6(f20(c26),c7). [resolve(279,b,121,b)]. 285 -p6(f20(c26),c7). [ur(26,a,263,a,b,94,a,c,283,a)]. 286 p6(f19(f25(c26)),c7). [back_unit_del(284),unit_del(b,285)]. 290 -p2(f12(c5,f17(f25(c26))),c5) | p2(f11(c13,f17(f25(c26))),c5). [back_unit_del(275),unit_del(a,285)]. 301 -p2(f12(c5,f19(f25(c26))),c5). [resolve(286,a,37,c),unit_del(a,281),unit_del(c,168)]. 316 -p2(f11(c13,f17(f25(c26))),c5). [ur(65,a,301,a,c,97,a)]. 317 -p2(f12(c5,f17(f25(c26))),c5). [back_unit_del(290),unit_del(b,316)]. 326 $F. [ur(62,a,317,a,c,97,a),unit_del(a,175)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=183. Generated=461. Kept=303. proofs=1. Usable=174. Sos=48. Demods=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.32. User_CPU=0.03, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 10892 exit (max_proofs) Sat Aug 12 20:59:02 2006