============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13076 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:11 2006 The command was "/home/mccune/bin/prover9 -f lifsch.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file lifsch.in clear(fof_reduction). formulas(sos). - (exists x exists x1 all y exists z exists z1 ((- p(y,y) | p(x,x) | - s(z,x)) & (s(x,y) | - s(y,z) | q(z1,z1)) & (q(x1,y) | - q(y,z1) | s(x1,x1)))). end_of_list. ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 p(f1(x,y),f1(x,y)) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [clausify]. 2 p(f1(x,y),f1(x,y)) | - s(x,f1(x,y)) | q(f1(x,y),z). [clausify]. 3 p(f1(x,y),f1(x,y)) | - s(x,f1(x,y)) | - s(y,y). [clausify]. 4 p(f1(x,y),f1(x,y)) | s(f1(x,y),z) | - q(y,f1(x,y)). [clausify]. 5 p(f1(x,y),f1(x,y)) | s(f1(x,y),z) | q(f1(x,y),u). [clausify]. 6 p(f1(x,y),f1(x,y)) | s(f1(x,y),z) | - s(y,y). [clausify]. 7 p(f1(x,y),f1(x,y)) | - q(z,z) | - q(y,f1(x,y)). [clausify]. 8 p(f1(x,y),f1(x,y)) | - q(z,z) | q(f1(x,y),z). [clausify]. 9 p(f1(x,y),f1(x,y)) | - q(z,z) | - s(y,y). [clausify]. 10 - p(x,x) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [clausify]. 11 - p(x,x) | - s(x,f1(x,y)) | q(f1(x,y),z). [clausify]. 12 - p(x,x) | - s(x,f1(x,y)) | - s(y,y). [clausify]. 13 - p(x,x) | s(f1(x,y),z) | - q(y,f1(x,y)). [clausify]. 14 - p(x,x) | s(f1(x,y),z) | q(f1(x,y),u). [clausify]. 15 - p(x,x) | s(f1(x,y),z) | - s(y,y). [clausify]. 16 - p(x,x) | - q(y,y) | - q(z,f1(x,z)). [clausify]. 17 - p(x,x) | - q(y,y) | q(f1(x,z),y). [clausify]. 18 - p(x,x) | - q(y,y) | - s(z,z). [clausify]. 19 s(x,y) | - s(y,f1(y,z)) | - q(z,f1(y,z)). [clausify]. 20 s(x,y) | - s(y,f1(y,z)) | q(f1(y,z),u). [clausify]. 21 s(x,y) | - s(y,f1(y,z)) | - s(z,z). [clausify]. 22 s(x,y) | s(f1(y,z),x) | - q(z,f1(y,z)). [clausify]. 23 s(x,y) | s(f1(y,z),x) | q(f1(y,z),u). [clausify]. 24 s(x,y) | s(f1(y,z),x) | - s(z,z). [clausify]. 25 s(x,y) | - q(z,z) | - q(u,f1(y,u)). [clausify]. 26 s(x,y) | - q(z,z) | q(f1(y,u),z). [clausify]. 27 s(x,y) | - q(z,z) | - s(u,u). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: p/2. Auto_denials: no changes. Term ordering decisions: Relation symbol precedence: lex([ s, q, p ]). Function symbol precedence: lex([ f1 ]). After inverse_order: Function symbol precedence: lex([ f1 ]). 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). 109 s(x,y) | - s(y,f1(y,z)) | - q(z,f1(y,z)). [clausify]. 110 s(x,y) | - s(y,f1(y,z)) | q(f1(y,z),u). [clausify]. 111 s(x,y) | - s(y,f1(y,z)) | - s(z,z). [clausify]. 112 s(x,y) | s(f1(y,z),x) | - q(z,f1(y,z)). [clausify]. 113 s(x,y) | s(f1(y,z),x) | q(f1(y,z),u). [clausify]. 114 s(x,y) | s(f1(y,z),x) | - s(z,z). [clausify]. 115 s(x,y) | - q(z,z) | - q(u,f1(y,u)). [clausify]. 116 s(x,y) | - q(z,z) | q(f1(y,u),z). [clausify]. 118 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(10,a,1,a)]. 119 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | q(f1(x,y),u). [resolve(10,a,2,a)]. 120 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | - s(y,y). [resolve(10,a,3,a)]. 121 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),u) | - q(y,f1(x,y)). [resolve(10,a,4,a)]. 122 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),u) | q(f1(x,y),v). [resolve(10,a,5,a)]. 123 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),u) | - s(y,y). [resolve(10,a,6,a)]. 127 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(11,a,1,a)]. 128 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | - s(x,f1(x,y)) | q(f1(x,y),v). [resolve(11,a,2,a)]. 129 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | - s(x,f1(x,y)) | - s(y,y). [resolve(11,a,3,a)]. 130 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | s(f1(x,y),v) | - q(y,f1(x,y)). [resolve(11,a,4,a)]. 131 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w). [resolve(11,a,5,a)]. 132 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | s(f1(x,y),v) | - s(y,y). [resolve(11,a,6,a)]. 133 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | - q(v,v) | - q(y,f1(x,y)). [resolve(11,a,7,a)]. 134 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | - q(v,v) | q(f1(x,y),v). [resolve(11,a,8,a)]. 136 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(12,a,1,a)]. 137 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | - s(x,f1(x,y)) | q(f1(x,y),u). [resolve(12,a,2,a)]. 138 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | - s(x,f1(x,y)) | - s(y,y). [resolve(12,a,3,a)]. 139 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | s(f1(x,y),u) | - q(y,f1(x,y)). [resolve(12,a,4,a)]. 140 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | s(f1(x,y),u) | q(f1(x,y),v). [resolve(12,a,5,a)]. 141 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | s(f1(x,y),u) | - s(y,y). [resolve(12,a,6,a)]. 145 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(13,a,1,a)]. 146 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | q(f1(x,y),v). [resolve(13,a,2,a)]. 147 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | - s(y,y). [resolve(13,a,3,a)]. 148 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),v) | - q(y,f1(x,y)). [resolve(13,a,4,a)]. 149 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),v) | q(f1(x,y),w). [resolve(13,a,5,a)]. 150 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),v) | - s(y,y). [resolve(13,a,6,a)]. 153 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(14,a,1,a)]. 154 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | - s(x,f1(x,y)) | q(f1(x,y),w). [resolve(14,a,2,a)]. 155 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | - s(x,f1(x,y)) | - s(y,y). [resolve(14,a,3,a)]. 156 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | s(f1(x,y),w) | - q(y,f1(x,y)). [resolve(14,a,4,a)]. 157 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | s(f1(x,y),w) | q(f1(x,y),v6). [resolve(14,a,5,a)]. 158 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | s(f1(x,y),w) | - s(y,y). [resolve(14,a,6,a)]. 159 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | - q(w,w) | - q(y,f1(x,y)). [resolve(14,a,7,a)]. 160 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | - q(w,w) | q(f1(x,y),w). [resolve(14,a,8,a)]. 161 s(f1(f1(x,y),z),u) | - s(z,z) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(15,a,1,a)]. 162 s(f1(f1(x,y),z),u) | - s(z,z) | - s(x,f1(x,y)) | q(f1(x,y),v). [resolve(15,a,2,a)]. 163 s(f1(f1(x,y),z),u) | - s(z,z) | - s(x,f1(x,y)) | - s(y,y). [resolve(15,a,3,a)]. 164 s(f1(f1(x,y),z),u) | - s(z,z) | s(f1(x,y),v) | - q(y,f1(x,y)). [resolve(15,a,4,a)]. 165 s(f1(f1(x,y),z),u) | - s(z,z) | s(f1(x,y),v) | q(f1(x,y),w). [resolve(15,a,5,a)]. 166 s(f1(f1(x,y),z),u) | - s(z,z) | s(f1(x,y),v) | - s(y,y). [resolve(15,a,6,a)]. 168 - q(x,x) | - q(y,f1(f1(z,u),y)) | - s(z,f1(z,u)) | q(f1(z,u),v). [resolve(16,a,2,a)]. 171 - q(x,x) | - q(y,f1(f1(z,u),y)) | s(f1(z,u),v) | q(f1(z,u),w). [resolve(16,a,5,a)]. 176 - q(x,x) | q(f1(f1(y,z),u),x) | - s(y,f1(y,z)) | q(f1(y,z),v). [resolve(17,a,2,a)]. 179 - q(x,x) | q(f1(f1(y,z),u),x) | s(f1(y,z),v) | q(f1(y,z),w). [resolve(17,a,5,a)]. 181 - q(x,x) | q(f1(f1(y,z),u),x) | - q(v,v) | q(f1(y,z),v). [resolve(17,a,8,a)]. 189 - s(f1(x,y),f1(f1(x,y),y)) | - s(y,y) | - s(x,f1(x,y)). [factor(138,b,d)]. 190 - s(f1(x,y),f1(f1(x,y),y)) | - s(y,y) | s(f1(x,y),z). [factor(141,b,d)]. 192 s(f1(f1(x,y),y),z) | - s(y,y) | - s(x,f1(x,y)). [factor(163,b,d)]. 193 s(f1(f1(x,y),y),z) | - s(y,y) | s(f1(x,y),u). [factor(166,b,d)]. 194 - q(x,x) | - q(y,f1(f1(z,u),y)) | - q(u,f1(z,u)). [factor(172,a,c)]. 195 - q(x,x) | - q(y,f1(f1(z,u),y)) | q(f1(z,u),x). [factor(173,a,c)]. 197 - q(x,x) | q(f1(f1(y,z),u),x) | - q(z,f1(y,z)). [factor(180,a,c)]. 198 - q(x,x) | q(f1(f1(y,z),u),x) | q(f1(y,z),x). [factor(181,a,c)]. 205 - q(x,x) | - s(y,y). [factor(203,b,c)]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=13): 109 s(x,y) | - s(y,f1(y,z)) | - q(z,f1(y,z)). [clausify]. given #2 (I,wt=13): 110 s(x,y) | - s(y,f1(y,z)) | q(f1(y,z),u). [clausify]. given #3 (I,wt=11): 111 s(x,y) | - s(y,f1(y,z)) | - s(z,z). [clausify]. given #4 (I,wt=13): 112 s(x,y) | s(f1(y,z),x) | - q(z,f1(y,z)). [clausify]. given #5 (I,wt=13): 113 s(x,y) | s(f1(y,z),x) | q(f1(y,z),u). [clausify]. given #6 (I,wt=11): 114 s(x,y) | s(f1(y,z),x) | - s(z,z). [clausify]. given #7 (I,wt=11): 115 s(x,y) | - q(z,z) | - q(u,f1(y,u)). [clausify]. given #8 (I,wt=11): 116 s(x,y) | - q(z,z) | q(f1(y,u),z). [clausify]. given #9 (I,wt=26): 118 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(10,a,1,a)]. given #10 (I,wt=26): 119 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | q(f1(x,y),u). [resolve(10,a,2,a)]. given #11 (I,wt=24): 120 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | - s(y,y). [resolve(10,a,3,a)]. given #12 (I,wt=26): 121 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),u) | - q(y,f1(x,y)). [resolve(10,a,4,a)]. given #13 (I,wt=26): 122 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),u) | q(f1(x,y),v). [resolve(10,a,5,a)]. given #14 (I,wt=24): 123 - s(f1(x,y),f1(f1(x,y),z)) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),u) | - s(y,y). [resolve(10,a,6,a)]. given #15 (I,wt=26): 127 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(11,a,1,a)]. given #16 (I,wt=26): 128 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | - s(x,f1(x,y)) | q(f1(x,y),v). [resolve(11,a,2,a)]. given #17 (I,wt=24): 129 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | - s(x,f1(x,y)) | - s(y,y). [resolve(11,a,3,a)]. given #18 (I,wt=26): 130 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | s(f1(x,y),v) | - q(y,f1(x,y)). [resolve(11,a,4,a)]. given #19 (I,wt=26): 131 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w). [resolve(11,a,5,a)]. given #20 (I,wt=24): 132 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | s(f1(x,y),v) | - s(y,y). [resolve(11,a,6,a)]. given #21 (I,wt=24): 133 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | - q(v,v) | - q(y,f1(x,y)). [resolve(11,a,7,a)]. given #22 (I,wt=24): 134 - s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | - q(v,v) | q(f1(x,y),v). [resolve(11,a,8,a)]. given #23 (I,wt=22): 136 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(12,a,1,a)]. given #24 (I,wt=22): 137 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | - s(x,f1(x,y)) | q(f1(x,y),u). [resolve(12,a,2,a)]. given #25 (I,wt=20): 138 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | - s(x,f1(x,y)) | - s(y,y). [resolve(12,a,3,a)]. given #26 (I,wt=22): 139 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | s(f1(x,y),u) | - q(y,f1(x,y)). [resolve(12,a,4,a)]. given #27 (I,wt=22): 140 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | s(f1(x,y),u) | q(f1(x,y),v). [resolve(12,a,5,a)]. given #28 (I,wt=20): 141 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | s(f1(x,y),u) | - s(y,y). [resolve(12,a,6,a)]. given #29 (I,wt=24): 145 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(13,a,1,a)]. given #30 (I,wt=24): 146 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | q(f1(x,y),v). [resolve(13,a,2,a)]. given #31 (I,wt=22): 147 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | - s(x,f1(x,y)) | - s(y,y). [resolve(13,a,3,a)]. given #32 (I,wt=24): 148 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),v) | - q(y,f1(x,y)). [resolve(13,a,4,a)]. given #33 (I,wt=24): 149 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),v) | q(f1(x,y),w). [resolve(13,a,5,a)]. given #34 (I,wt=22): 150 s(f1(f1(x,y),z),u) | - q(z,f1(f1(x,y),z)) | s(f1(x,y),v) | - s(y,y). [resolve(13,a,6,a)]. given #35 (I,wt=24): 153 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(14,a,1,a)]. given #36 (I,wt=24): 154 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | - s(x,f1(x,y)) | q(f1(x,y),w). [resolve(14,a,2,a)]. given #37 (I,wt=22): 155 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | - s(x,f1(x,y)) | - s(y,y). [resolve(14,a,3,a)]. given #38 (I,wt=24): 156 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | s(f1(x,y),w) | - q(y,f1(x,y)). [resolve(14,a,4,a)]. given #39 (I,wt=24): 157 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | s(f1(x,y),w) | q(f1(x,y),v6). [resolve(14,a,5,a)]. given #40 (I,wt=22): 158 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | s(f1(x,y),w) | - s(y,y). [resolve(14,a,6,a)]. given #41 (I,wt=22): 159 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | - q(w,w) | - q(y,f1(x,y)). [resolve(14,a,7,a)]. given #42 (I,wt=22): 160 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | - q(w,w) | q(f1(x,y),w). [resolve(14,a,8,a)]. given #43 (I,wt=20): 161 s(f1(f1(x,y),z),u) | - s(z,z) | - s(x,f1(x,y)) | - q(y,f1(x,y)). [resolve(15,a,1,a)]. given #44 (I,wt=20): 162 s(f1(f1(x,y),z),u) | - s(z,z) | - s(x,f1(x,y)) | q(f1(x,y),v). [resolve(15,a,2,a)]. given #45 (I,wt=18): 163 s(f1(f1(x,y),z),u) | - s(z,z) | - s(x,f1(x,y)) | - s(y,y). [resolve(15,a,3,a)]. given #46 (I,wt=20): 164 s(f1(f1(x,y),z),u) | - s(z,z) | s(f1(x,y),v) | - q(y,f1(x,y)). [resolve(15,a,4,a)]. given #47 (I,wt=20): 165 s(f1(f1(x,y),z),u) | - s(z,z) | s(f1(x,y),v) | q(f1(x,y),w). [resolve(15,a,5,a)]. given #48 (I,wt=18): 166 s(f1(f1(x,y),z),u) | - s(z,z) | s(f1(x,y),v) | - s(y,y). [resolve(15,a,6,a)]. given #49 (I,wt=20): 168 - q(x,x) | - q(y,f1(f1(z,u),y)) | - s(z,f1(z,u)) | q(f1(z,u),v). [resolve(16,a,2,a)]. given #50 (I,wt=20): 171 - q(x,x) | - q(y,f1(f1(z,u),y)) | s(f1(z,u),v) | q(f1(z,u),w). [resolve(16,a,5,a)]. given #51 (I,wt=20): 176 - q(x,x) | q(f1(f1(y,z),u),x) | - s(y,f1(y,z)) | q(f1(y,z),v). [resolve(17,a,2,a)]. given #52 (I,wt=20): 179 - q(x,x) | q(f1(f1(y,z),u),x) | s(f1(y,z),v) | q(f1(y,z),w). [resolve(17,a,5,a)]. given #53 (I,wt=18): 181 - q(x,x) | q(f1(f1(y,z),u),x) | - q(v,v) | q(f1(y,z),v). [resolve(17,a,8,a)]. given #54 (I,wt=17): 189 - s(f1(x,y),f1(f1(x,y),y)) | - s(y,y) | - s(x,f1(x,y)). [factor(138,b,d)]. given #55 (I,wt=17): 190 - s(f1(x,y),f1(f1(x,y),y)) | - s(y,y) | s(f1(x,y),z). [factor(141,b,d)]. given #56 (I,wt=15): 192 s(f1(f1(x,y),y),z) | - s(y,y) | - s(x,f1(x,y)). [factor(163,b,d)]. given #57 (I,wt=15): 193 s(f1(f1(x,y),y),z) | - s(y,y) | s(f1(x,y),u). [factor(166,b,d)]. given #58 (I,wt=15): 194 - q(x,x) | - q(y,f1(f1(z,u),y)) | - q(u,f1(z,u)). [factor(172,a,c)]. given #59 (I,wt=15): 195 - q(x,x) | - q(y,f1(f1(z,u),y)) | q(f1(z,u),x). [factor(173,a,c)]. given #60 (I,wt=15): 197 - q(x,x) | q(f1(f1(y,z),u),x) | - q(z,f1(y,z)). [factor(180,a,c)]. given #61 (I,wt=15): 198 - q(x,x) | q(f1(f1(y,z),u),x) | q(f1(y,z),x). [factor(181,a,c)]. given #62 (I,wt=6): 205 - q(x,x) | - s(y,y). [factor(203,b,c)]. given #63 (F,wt=11): 217 s(x,y) | - q(z,z) | s(f1(y,u),x). [factor(214,a,c)]. given #64 (T,wt=8): 439 s(x,y) | s(f1(y,z),x). [factor(431,b,d),merge(c)]. given #65 (T,wt=10): 498 s(f1(x,y),x) | - s(x,f1(x,x)). [factor(467,a,b)]. given #66 (A,wt=48): 259 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | s(f1(f1(v6,f1(f1(x,y),z)),v7),v8) | q(f1(f1(v6,f1(f1(x,y),z)),v7),v9) | s(f1(v6,f1(f1(x,y),z)),v10). [resolve(157,b,156,d)]. given #67 (F,wt=10): 499 s(f1(f1(x,y),z),x) | - s(y,y). [factor(468,a,b)]. given #68 (F,wt=12): 485 s(f1(x,x),x) | s(f1(f1(x,x),x),y). [factor(440,a,c)]. given #69 (T,wt=12): 500 s(f1(f1(x,y),z),x) | q(f1(x,y),u). [factor(469,a,b)]. given #70 (T,wt=10): 651 s(f1(f1(x,y),z),x) | - s(u,u). [resolve(500,b,205,a)]. given #71 (A,wt=48): 260 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | s(f1(f1(v6,f1(f1(x,y),z)),v7),v8) | q(f1(f1(v6,f1(f1(x,y),z)),v7),v9) | - s(v6,f1(v6,f1(f1(x,y),z))). [resolve(157,b,153,d)]. given #72 (F,wt=10): 701 s(f1(f1(x,y),z),x) | - q(u,u). [factor(686,a,b)]. given #73 (F,wt=7): 712 s(f1(f1(x,y),z),x). [factor(711,a,b)]. given #74 (T,wt=12): 504 s(f1(x,y),x) | - s(x,f1(x,f1(x,y))). [factor(482,a,b)]. given #75 (T,wt=13): 467 s(f1(x,y),x) | s(z,u) | - s(u,f1(u,x)). [resolve(439,a,111,c)]. given #76 (A,wt=38): 262 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | s(f1(f1(v6,v7),f1(f1(x,y),z)),v8) | s(f1(v6,v7),v9) | q(f1(v6,v7),v10). [resolve(157,b,149,b)]. given #77 (F,wt=12): 714 s(f1(x,x),x) | s(y,f1(f1(x,x),x)). [factor(713,a,c)]. given #78 (F,wt=8): 871 s(f1(x,x),x) | - s(x,x). [factor(865,a,c)]. given #79 (T,wt=5): 875 s(f1(x,x),x). [factor(874,a,b)]. given #80 (T,wt=15): 482 s(f1(x,y),x) | s(z,u) | - s(u,f1(u,f1(x,y))). [resolve(439,b,111,c)]. given #81 (A,wt=48): 263 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | s(f1(f1(v6,f1(f1(x,y),z)),v7),v8) | - q(v7,f1(f1(v6,f1(f1(x,y),z)),v7)) | s(f1(v6,f1(f1(x,y),z)),v9). [resolve(157,b,148,d)]. given #82 (F,wt=15): 489 s(f1(x,y),x) | s(f1(f1(x,y),x),z) | - s(y,y). [factor(446,a,c)]. given #83 (F,wt=17): 440 s(f1(x,y),x) | s(f1(f1(z,x),x),u) | s(f1(z,x),v). [resolve(439,a,193,b)]. given #84 (T,wt=14): 1012 s(f1(x,y),x) | s(f1(f1(z,x),x),f1(z,x)). [factor(967,b,c)]. given #85 (T,wt=14): 1031 s(f1(x,y),x) | s(f1(z,x),f1(f1(z,x),x)). [factor(992,b,c)]. given #86 (A,wt=38): 264 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | s(f1(f1(v6,v7),f1(f1(x,y),z)),v8) | s(f1(v6,v7),v9) | - q(v7,f1(v6,v7)). [resolve(157,b,148,b)]. given #87 (F,wt=10): 1047 s(f1(x,y),x) | s(z,f1(u,x)). [factor(1034,a,b)]. given #88 (F,wt=5): 1118 s(f1(x,y),x). [factor(1109,a,b)]. given #89 (T,wt=20): 332 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | - q(v6,v6). [factor(285,a,d)]. given #90 (T,wt=17): 1137 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w). [factor(1135,c,d)]. given #91 (A,wt=34): 360 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | s(f1(x,y),w) | - s(f1(f1(x,y),z),f1(f1(f1(x,y),z),f1(x,y))). [factor(343,b,e)]. given #92 (F,wt=15): 1138 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | - s(w,w). [resolve(1137,c,205,a)]. given #93 (F,wt=15): 1187 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | - q(w,w). [factor(1173,a,c)]. given #94 (T,wt=12): 1195 s(f1(f1(x,y),z),u) | s(f1(x,y),v). [factor(1194,b,c)]. given #95 (T,wt=12): 1238 s(f1(x,y),f1(f1(x,y),z)) | - s(u,u). [factor(1214,a,b)]. given #96 (A,wt=29): 1197 s(f1(x,y),z) | s(f1(f1(u,f1(f1(x,y),v)),f1(f1(x,y),v)),w) | - s(u,f1(u,f1(f1(x,y),v))). [resolve(1195,a,192,b)]. given #97 (F,wt=8): 1259 - s(x,x) | - s(y,f1(y,x)). [back_unit_del(189),unit_del(a,1247)]. given #98 (F,wt=13): 1261 - s(x,x) | - s(y,f1(y,z)) | - q(z,f1(y,z)). [back_unit_del(136),unit_del(a,1247)]. given #99 (T,wt=8): 1258 s(f1(x,y),z) | - s(u,u). [back_unit_del(1198),unit_del(c,1247)]. given #100 (T,wt=5): 1279 s(f1(x,y),z). [factor(1277,a,b)]. ============================== PROOF ================================= % Proof 1 at 0.30 (+ 0.00) seconds. % Length of proof is 31. % Level of proof is 21. % Maximum clause weight is 34. % Given clauses 100. 3 p(f1(x,y),f1(x,y)) | - s(x,f1(x,y)) | - s(y,y). [clausify]. 5 p(f1(x,y),f1(x,y)) | s(f1(x,y),z) | q(f1(x,y),u). [clausify]. 12 - p(x,x) | - s(x,f1(x,y)) | - s(y,y). [clausify]. 14 - p(x,x) | s(f1(x,y),z) | q(f1(x,y),u). [clausify]. 111 s(x,y) | - s(y,f1(y,z)) | - s(z,z). [clausify]. 115 s(x,y) | - q(z,z) | - q(u,f1(y,u)). [clausify]. 138 - s(f1(x,y),f1(f1(x,y),z)) | - s(z,z) | - s(x,f1(x,y)) | - s(y,y). [resolve(12,a,3,a)]. 157 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | s(f1(x,y),w) | q(f1(x,y),v6). [resolve(14,a,5,a)]. 189 - s(f1(x,y),f1(f1(x,y),y)) | - s(y,y) | - s(x,f1(x,y)). [factor(138,b,d)]. 285 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | s(v6,v7) | - q(v8,v8). [resolve(157,b,115,c)]. 332 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | - q(v6,v6). [factor(285,a,d)]. 1124 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | s(f1(f1(v6,v7),v8),v9) | s(f1(v6,v7),v10) | q(f1(v6,v7),v11). [resolve(332,d,157,b)]. 1132 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | s(f1(x,y),v6) | q(f1(x,y),v7). [factor(1124,a,d)]. 1135 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | q(f1(x,y),v6). [factor(1132,b,d)]. 1137 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w). [factor(1135,c,d)]. 1173 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | s(w,v6) | - q(v7,v7). [resolve(1137,c,115,c)]. 1187 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | - q(w,w). [factor(1173,a,c)]. 1193 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | s(f1(f1(w,v6),v7),v8) | s(f1(w,v6),v9). [resolve(1187,c,1137,c)]. 1194 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | s(f1(x,y),w). [factor(1193,a,c)]. 1195 s(f1(f1(x,y),z),u) | s(f1(x,y),v). [factor(1194,b,c)]. 1198 s(f1(x,y),z) | - s(u,u) | - s(f1(x,y),f1(f1(x,y),u)). [resolve(1195,a,189,a)]. 1214 s(f1(x,y),z) | s(u,f1(f1(x,y),v)) | - s(w,w). [resolve(1195,a,111,b)]. 1238 s(f1(x,y),f1(f1(x,y),z)) | - s(u,u). [factor(1214,a,b)]. 1245 s(f1(x,y),f1(f1(x,y),z)) | s(f1(u,v),w). [resolve(1238,b,1195,a)]. 1247 s(f1(x,y),f1(f1(x,y),z)). [factor(1245,a,b)]. 1258 s(f1(x,y),z) | - s(u,u). [back_unit_del(1198),unit_del(c,1247)]. 1259 - s(x,x) | - s(y,f1(y,x)). [back_unit_del(189),unit_del(a,1247)]. 1277 s(f1(x,y),z) | s(f1(u,v),w). [resolve(1258,b,1195,a)]. 1279 s(f1(x,y),z). [factor(1277,a,b)]. 1280 - s(x,x). [resolve(1279,a,1259,b)]. 1281 $F. [resolve(1280,a,1279,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=100. Generated=2702. Kept=1172. proofs=1. Usable=10. Sos=7. Demods=0. Denials=0. Limbo=0, Disabled=1252. Hints=0. Weight_deleted=14. Literals_deleted=0. Forward_subsumed=1516. Back_subsumed=1122. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=32. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=68392. Nonunit_bsub_feature_tests=41807. Megabytes=0.69. User_CPU=0.30, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13076 exit (max_proofs) Mon Jun 19 16:41:11 2006