============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 10893 was started by mccune on cleo.thornwood, Sat Aug 12 20:59:02 2006 The command was "/home/mccune/bin/prover9 -f lifsch.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file lifsch.in formulas(goals). (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 NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (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)))). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(f1(x,y),f1(x,y)) | -s(x,f1(x,y)) | -q(y,f1(x,y)). [deny(1)]. p(f1(x,y),f1(x,y)) | -s(x,f1(x,y)) | q(f1(x,y),z). [deny(1)]. p(f1(x,y),f1(x,y)) | -s(x,f1(x,y)) | -s(y,y). [deny(1)]. p(f1(x,y),f1(x,y)) | s(f1(x,y),z) | -q(y,f1(x,y)). [deny(1)]. p(f1(x,y),f1(x,y)) | s(f1(x,y),z) | q(f1(x,y),u). [deny(1)]. p(f1(x,y),f1(x,y)) | s(f1(x,y),z) | -s(y,y). [deny(1)]. p(f1(x,y),f1(x,y)) | -q(z,z) | -q(y,f1(x,y)). [deny(1)]. p(f1(x,y),f1(x,y)) | -q(z,z) | q(f1(x,y),z). [deny(1)]. p(f1(x,y),f1(x,y)) | -q(z,z) | -s(y,y). [deny(1)]. -p(x,x) | -s(x,f1(x,y)) | -q(y,f1(x,y)). [deny(1)]. -p(x,x) | -s(x,f1(x,y)) | q(f1(x,y),z). [deny(1)]. -p(x,x) | -s(x,f1(x,y)) | -s(y,y). [deny(1)]. -p(x,x) | s(f1(x,y),z) | -q(y,f1(x,y)). [deny(1)]. -p(x,x) | s(f1(x,y),z) | q(f1(x,y),u). [deny(1)]. -p(x,x) | s(f1(x,y),z) | -s(y,y). [deny(1)]. -p(x,x) | -q(y,y) | -q(z,f1(x,z)). [deny(1)]. -p(x,x) | -q(y,y) | q(f1(x,z),y). [deny(1)]. -p(x,x) | -q(y,y) | -s(z,z). [deny(1)]. s(x,y) | -s(y,f1(y,z)) | -q(z,f1(y,z)). [deny(1)]. s(x,y) | -s(y,f1(y,z)) | q(f1(y,z),u). [deny(1)]. s(x,y) | -s(y,f1(y,z)) | -s(z,z). [deny(1)]. s(x,y) | s(f1(y,z),x) | -q(z,f1(y,z)). [deny(1)]. s(x,y) | s(f1(y,z),x) | q(f1(y,z),u). [deny(1)]. s(x,y) | s(f1(y,z),x) | -s(z,z). [deny(1)]. s(x,y) | -q(z,z) | -q(u,f1(y,u)). [deny(1)]. s(x,y) | -q(z,z) | q(f1(y,u),z). [deny(1)]. s(x,y) | -q(z,z) | -s(u,u). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating p/2 2 -p(x,x) | -s(x,f1(x,y)) | -q(y,f1(x,y)). [deny(1)]. 3 p(f1(x,y),f1(x,y)) | -s(x,f1(x,y)) | -q(y,f1(x,y)). [deny(1)]. 4 p(f1(x,y),f1(x,y)) | -s(x,f1(x,y)) | q(f1(x,y),z). [deny(1)]. 5 p(f1(x,y),f1(x,y)) | -s(x,f1(x,y)) | -s(y,y). [deny(1)]. 6 p(f1(x,y),f1(x,y)) | s(f1(x,y),z) | -q(y,f1(x,y)). [deny(1)]. 7 p(f1(x,y),f1(x,y)) | s(f1(x,y),z) | q(f1(x,y),u). [deny(1)]. 8 p(f1(x,y),f1(x,y)) | s(f1(x,y),z) | -s(y,y). [deny(1)]. 9 p(f1(x,y),f1(x,y)) | -q(z,z) | -q(y,f1(x,y)). [deny(1)]. 10 p(f1(x,y),f1(x,y)) | -q(z,z) | q(f1(x,y),z). [deny(1)]. 11 p(f1(x,y),f1(x,y)) | -q(z,z) | -s(y,y). [deny(1)]. Derived: -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(2,a,3,a)]. Derived: -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(2,a,4,a)]. Derived: -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(2,a,5,a)]. Derived: -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(2,a,6,a)]. Derived: -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(2,a,7,a)]. Derived: -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(2,a,8,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -q(z,f1(f1(x,y),z)) | -q(u,u) | -q(y,f1(x,y)). [resolve(2,a,9,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -q(z,f1(f1(x,y),z)) | -q(u,u) | q(f1(x,y),u). [resolve(2,a,10,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -q(z,f1(f1(x,y),z)) | -q(u,u) | -s(y,y). [resolve(2,a,11,a)]. 12 -p(x,x) | -s(x,f1(x,y)) | q(f1(x,y),z). [deny(1)]. Derived: -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(12,a,3,a)]. Derived: -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(12,a,4,a)]. Derived: -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(12,a,5,a)]. Derived: -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(12,a,6,a)]. Derived: -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(12,a,7,a)]. Derived: -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(12,a,8,a)]. Derived: -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(12,a,9,a)]. Derived: -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(12,a,10,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | q(f1(f1(x,y),z),u) | -q(v,v) | -s(y,y). [resolve(12,a,11,a)]. 13 -p(x,x) | -s(x,f1(x,y)) | -s(y,y). [deny(1)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -s(x,f1(x,y)) | -q(y,f1(x,y)). [resolve(13,a,3,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -s(x,f1(x,y)) | q(f1(x,y),u). [resolve(13,a,4,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -s(x,f1(x,y)) | -s(y,y). [resolve(13,a,5,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | s(f1(x,y),u) | -q(y,f1(x,y)). [resolve(13,a,6,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | s(f1(x,y),u) | q(f1(x,y),v). [resolve(13,a,7,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | s(f1(x,y),u) | -s(y,y). [resolve(13,a,8,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -q(u,u) | -q(y,f1(x,y)). [resolve(13,a,9,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -q(u,u) | q(f1(x,y),u). [resolve(13,a,10,a)]. Derived: -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -q(u,u) | -s(y,y). [resolve(13,a,11,a)]. 14 -p(x,x) | s(f1(x,y),z) | -q(y,f1(x,y)). [deny(1)]. Derived: 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(14,a,3,a)]. Derived: 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(14,a,4,a)]. Derived: s(f1(f1(x,y),z),u) | -q(z,f1(f1(x,y),z)) | -s(x,f1(x,y)) | -s(y,y). [resolve(14,a,5,a)]. Derived: 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(14,a,6,a)]. Derived: 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(14,a,7,a)]. Derived: s(f1(f1(x,y),z),u) | -q(z,f1(f1(x,y),z)) | s(f1(x,y),v) | -s(y,y). [resolve(14,a,8,a)]. Derived: s(f1(f1(x,y),z),u) | -q(z,f1(f1(x,y),z)) | -q(v,v) | -q(y,f1(x,y)). [resolve(14,a,9,a)]. Derived: s(f1(f1(x,y),z),u) | -q(z,f1(f1(x,y),z)) | -q(v,v) | q(f1(x,y),v). [resolve(14,a,10,a)]. 15 -p(x,x) | s(f1(x,y),z) | q(f1(x,y),u). [deny(1)]. Derived: 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(15,a,3,a)]. Derived: 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(15,a,4,a)]. Derived: s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | -s(x,f1(x,y)) | -s(y,y). [resolve(15,a,5,a)]. Derived: 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(15,a,6,a)]. Derived: 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(15,a,7,a)]. Derived: s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | s(f1(x,y),w) | -s(y,y). [resolve(15,a,8,a)]. Derived: s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | -q(w,w) | -q(y,f1(x,y)). [resolve(15,a,9,a)]. Derived: s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | -q(w,w) | q(f1(x,y),w). [resolve(15,a,10,a)]. 16 -p(x,x) | s(f1(x,y),z) | -s(y,y). [deny(1)]. Derived: s(f1(f1(x,y),z),u) | -s(z,z) | -s(x,f1(x,y)) | -q(y,f1(x,y)). [resolve(16,a,3,a)]. Derived: s(f1(f1(x,y),z),u) | -s(z,z) | -s(x,f1(x,y)) | q(f1(x,y),v). [resolve(16,a,4,a)]. Derived: s(f1(f1(x,y),z),u) | -s(z,z) | -s(x,f1(x,y)) | -s(y,y). [resolve(16,a,5,a)]. Derived: s(f1(f1(x,y),z),u) | -s(z,z) | s(f1(x,y),v) | -q(y,f1(x,y)). [resolve(16,a,6,a)]. Derived: s(f1(f1(x,y),z),u) | -s(z,z) | s(f1(x,y),v) | q(f1(x,y),w). [resolve(16,a,7,a)]. Derived: s(f1(f1(x,y),z),u) | -s(z,z) | s(f1(x,y),v) | -s(y,y). [resolve(16,a,8,a)]. 17 -p(x,x) | -q(y,y) | -q(z,f1(x,z)). [deny(1)]. Derived: -q(x,x) | -q(y,f1(f1(z,u),y)) | -s(z,f1(z,u)) | -q(u,f1(z,u)). [resolve(17,a,3,a)]. Derived: -q(x,x) | -q(y,f1(f1(z,u),y)) | -s(z,f1(z,u)) | q(f1(z,u),v). [resolve(17,a,4,a)]. Derived: -q(x,x) | -q(y,f1(f1(z,u),y)) | -s(z,f1(z,u)) | -s(u,u). [resolve(17,a,5,a)]. Derived: -q(x,x) | -q(y,f1(f1(z,u),y)) | s(f1(z,u),v) | -q(u,f1(z,u)). [resolve(17,a,6,a)]. Derived: -q(x,x) | -q(y,f1(f1(z,u),y)) | s(f1(z,u),v) | q(f1(z,u),w). [resolve(17,a,7,a)]. Derived: -q(x,x) | -q(y,f1(f1(z,u),y)) | -q(v,v) | -q(u,f1(z,u)). [resolve(17,a,9,a)]. Derived: -q(x,x) | -q(y,f1(f1(z,u),y)) | -q(v,v) | q(f1(z,u),v). [resolve(17,a,10,a)]. Derived: -q(x,x) | -q(y,f1(f1(z,u),y)) | -q(v,v) | -s(u,u). [resolve(17,a,11,a)]. 18 -p(x,x) | -q(y,y) | q(f1(x,z),y). [deny(1)]. Derived: -q(x,x) | q(f1(f1(y,z),u),x) | -s(y,f1(y,z)) | -q(z,f1(y,z)). [resolve(18,a,3,a)]. Derived: -q(x,x) | q(f1(f1(y,z),u),x) | -s(y,f1(y,z)) | q(f1(y,z),v). [resolve(18,a,4,a)]. Derived: -q(x,x) | q(f1(f1(y,z),u),x) | -s(y,f1(y,z)) | -s(z,z). [resolve(18,a,5,a)]. Derived: -q(x,x) | q(f1(f1(y,z),u),x) | s(f1(y,z),v) | -q(z,f1(y,z)). [resolve(18,a,6,a)]. Derived: -q(x,x) | q(f1(f1(y,z),u),x) | s(f1(y,z),v) | q(f1(y,z),w). [resolve(18,a,7,a)]. Derived: -q(x,x) | q(f1(f1(y,z),u),x) | -q(v,v) | -q(z,f1(y,z)). [resolve(18,a,9,a)]. Derived: -q(x,x) | q(f1(f1(y,z),u),x) | -q(v,v) | q(f1(y,z),v). [resolve(18,a,10,a)]. Derived: -q(x,x) | q(f1(f1(y,z),u),x) | -q(v,v) | -s(z,z). [resolve(18,a,11,a)]. 19 -p(x,x) | -q(y,y) | -s(z,z). [deny(1)]. Derived: -q(x,x) | -s(y,y) | -s(z,f1(z,u)) | -q(u,f1(z,u)). [resolve(19,a,3,a)]. Derived: -q(x,x) | -s(y,y) | -s(z,f1(z,u)) | q(f1(z,u),v). [resolve(19,a,4,a)]. Derived: -q(x,x) | -s(y,y) | -s(z,f1(z,u)) | -s(u,u). [resolve(19,a,5,a)]. Derived: -q(x,x) | -s(y,y) | -q(z,z) | -q(u,f1(v,u)). [resolve(19,a,9,a)]. Derived: -q(x,x) | -s(y,y) | -q(z,z) | q(f1(u,v),z). [resolve(19,a,10,a)]. Derived: -q(x,x) | -s(y,y) | -q(z,z) | -s(u,u). [resolve(19,a,11,a)]. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ s, q, p ]). Function symbol precedence: lex([ f1 ]). 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). 20 s(x,y) | -s(y,f1(y,z)) | -q(z,f1(y,z)). [deny(1)]. 21 s(x,y) | -s(y,f1(y,z)) | q(f1(y,z),u). [deny(1)]. 22 s(x,y) | -s(y,f1(y,z)) | -s(z,z). [deny(1)]. 23 s(x,y) | s(f1(y,z),x) | -q(z,f1(y,z)). [deny(1)]. 24 s(x,y) | s(f1(y,z),x) | q(f1(y,z),u). [deny(1)]. 25 s(x,y) | s(f1(y,z),x) | -s(z,z). [deny(1)]. 26 s(x,y) | -q(z,z) | -q(u,f1(y,u)). [deny(1)]. 27 s(x,y) | -q(z,z) | q(f1(y,u),z). [deny(1)]. 29 -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(2,a,3,a)]. 30 -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(2,a,4,a)]. 31 -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(2,a,5,a)]. 32 -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(2,a,6,a)]. 33 -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(2,a,7,a)]. 34 -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(2,a,8,a)]. 38 -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(12,a,3,a)]. 39 -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(12,a,4,a)]. 40 -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(12,a,5,a)]. 41 -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(12,a,6,a)]. 42 -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(12,a,7,a)]. 43 -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(12,a,8,a)]. 44 -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(12,a,9,a)]. 45 -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(12,a,10,a)]. 47 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -s(x,f1(x,y)) | -q(y,f1(x,y)). [resolve(13,a,3,a)]. 48 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -s(x,f1(x,y)) | q(f1(x,y),u). [resolve(13,a,4,a)]. 49 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -s(x,f1(x,y)) | -s(y,y). [resolve(13,a,5,a)]. 50 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | s(f1(x,y),u) | -q(y,f1(x,y)). [resolve(13,a,6,a)]. 51 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | s(f1(x,y),u) | q(f1(x,y),v). [resolve(13,a,7,a)]. 52 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | s(f1(x,y),u) | -s(y,y). [resolve(13,a,8,a)]. 56 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(14,a,3,a)]. 57 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(14,a,4,a)]. 58 s(f1(f1(x,y),z),u) | -q(z,f1(f1(x,y),z)) | -s(x,f1(x,y)) | -s(y,y). [resolve(14,a,5,a)]. 59 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(14,a,6,a)]. 60 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(14,a,7,a)]. 61 s(f1(f1(x,y),z),u) | -q(z,f1(f1(x,y),z)) | s(f1(x,y),v) | -s(y,y). [resolve(14,a,8,a)]. 64 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(15,a,3,a)]. 65 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(15,a,4,a)]. 66 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | -s(x,f1(x,y)) | -s(y,y). [resolve(15,a,5,a)]. 67 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(15,a,6,a)]. 68 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(15,a,7,a)]. 69 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | s(f1(x,y),w) | -s(y,y). [resolve(15,a,8,a)]. 70 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | -q(w,w) | -q(y,f1(x,y)). [resolve(15,a,9,a)]. 71 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | -q(w,w) | q(f1(x,y),w). [resolve(15,a,10,a)]. 72 s(f1(f1(x,y),z),u) | -s(z,z) | -s(x,f1(x,y)) | -q(y,f1(x,y)). [resolve(16,a,3,a)]. 73 s(f1(f1(x,y),z),u) | -s(z,z) | -s(x,f1(x,y)) | q(f1(x,y),v). [resolve(16,a,4,a)]. 74 s(f1(f1(x,y),z),u) | -s(z,z) | -s(x,f1(x,y)) | -s(y,y). [resolve(16,a,5,a)]. 75 s(f1(f1(x,y),z),u) | -s(z,z) | s(f1(x,y),v) | -q(y,f1(x,y)). [resolve(16,a,6,a)]. 76 s(f1(f1(x,y),z),u) | -s(z,z) | s(f1(x,y),v) | q(f1(x,y),w). [resolve(16,a,7,a)]. 77 s(f1(f1(x,y),z),u) | -s(z,z) | s(f1(x,y),v) | -s(y,y). [resolve(16,a,8,a)]. 79 -q(x,x) | -q(y,f1(f1(z,u),y)) | -s(z,f1(z,u)) | q(f1(z,u),v). [resolve(17,a,4,a)]. 82 -q(x,x) | -q(y,f1(f1(z,u),y)) | s(f1(z,u),v) | q(f1(z,u),w). [resolve(17,a,7,a)]. 87 -q(x,x) | q(f1(f1(y,z),u),x) | -s(y,f1(y,z)) | q(f1(y,z),v). [resolve(18,a,4,a)]. 90 -q(x,x) | q(f1(f1(y,z),u),x) | s(f1(y,z),v) | q(f1(y,z),w). [resolve(18,a,7,a)]. 92 -q(x,x) | q(f1(f1(y,z),u),x) | -q(v,v) | q(f1(y,z),v). [resolve(18,a,10,a)]. 100 -s(f1(x,y),f1(f1(x,y),y)) | -s(y,y) | -s(x,f1(x,y)). [factor(49,b,d)]. 101 -s(f1(x,y),f1(f1(x,y),y)) | -s(y,y) | s(f1(x,y),z). [factor(52,b,d)]. 103 s(f1(f1(x,y),y),z) | -s(y,y) | -s(x,f1(x,y)). [factor(74,b,d)]. 104 s(f1(f1(x,y),y),z) | -s(y,y) | s(f1(x,y),u). [factor(77,b,d)]. 105 -q(x,x) | -q(y,f1(f1(z,u),y)) | -q(u,f1(z,u)). [factor(83,a,c)]. 106 -q(x,x) | -q(y,f1(f1(z,u),y)) | q(f1(z,u),x). [factor(84,a,c)]. 108 -q(x,x) | q(f1(f1(y,z),u),x) | -q(z,f1(y,z)). [factor(91,a,c)]. 109 -q(x,x) | q(f1(f1(y,z),u),x) | q(f1(y,z),x). [factor(92,a,c)]. 116 -q(x,x) | -s(y,y). [factor(114,b,c)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=13): 20 s(x,y) | -s(y,f1(y,z)) | -q(z,f1(y,z)). [deny(1)]. given #2 (I,wt=13): 21 s(x,y) | -s(y,f1(y,z)) | q(f1(y,z),u). [deny(1)]. given #3 (I,wt=11): 22 s(x,y) | -s(y,f1(y,z)) | -s(z,z). [deny(1)]. given #4 (I,wt=13): 23 s(x,y) | s(f1(y,z),x) | -q(z,f1(y,z)). [deny(1)]. given #5 (I,wt=13): 24 s(x,y) | s(f1(y,z),x) | q(f1(y,z),u). [deny(1)]. given #6 (I,wt=11): 25 s(x,y) | s(f1(y,z),x) | -s(z,z). [deny(1)]. given #7 (I,wt=11): 26 s(x,y) | -q(z,z) | -q(u,f1(y,u)). [deny(1)]. given #8 (I,wt=11): 27 s(x,y) | -q(z,z) | q(f1(y,u),z). [deny(1)]. given #9 (I,wt=26): 29 -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(2,a,3,a)]. given #10 (I,wt=26): 30 -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(2,a,4,a)]. given #11 (I,wt=24): 31 -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(2,a,5,a)]. given #12 (I,wt=26): 32 -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(2,a,6,a)]. given #13 (I,wt=26): 33 -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(2,a,7,a)]. given #14 (I,wt=24): 34 -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(2,a,8,a)]. given #15 (I,wt=26): 38 -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(12,a,3,a)]. given #16 (I,wt=26): 39 -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(12,a,4,a)]. given #17 (I,wt=24): 40 -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(12,a,5,a)]. given #18 (I,wt=26): 41 -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(12,a,6,a)]. given #19 (I,wt=26): 42 -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(12,a,7,a)]. given #20 (I,wt=24): 43 -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(12,a,8,a)]. given #21 (I,wt=24): 44 -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(12,a,9,a)]. given #22 (I,wt=24): 45 -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(12,a,10,a)]. given #23 (I,wt=22): 47 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -s(x,f1(x,y)) | -q(y,f1(x,y)). [resolve(13,a,3,a)]. given #24 (I,wt=22): 48 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -s(x,f1(x,y)) | q(f1(x,y),u). [resolve(13,a,4,a)]. given #25 (I,wt=20): 49 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -s(x,f1(x,y)) | -s(y,y). [resolve(13,a,5,a)]. given #26 (I,wt=22): 50 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | s(f1(x,y),u) | -q(y,f1(x,y)). [resolve(13,a,6,a)]. given #27 (I,wt=22): 51 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | s(f1(x,y),u) | q(f1(x,y),v). [resolve(13,a,7,a)]. given #28 (I,wt=20): 52 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | s(f1(x,y),u) | -s(y,y). [resolve(13,a,8,a)]. given #29 (I,wt=24): 56 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(14,a,3,a)]. given #30 (I,wt=24): 57 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(14,a,4,a)]. given #31 (I,wt=22): 58 s(f1(f1(x,y),z),u) | -q(z,f1(f1(x,y),z)) | -s(x,f1(x,y)) | -s(y,y). [resolve(14,a,5,a)]. given #32 (I,wt=24): 59 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(14,a,6,a)]. given #33 (I,wt=24): 60 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(14,a,7,a)]. given #34 (I,wt=22): 61 s(f1(f1(x,y),z),u) | -q(z,f1(f1(x,y),z)) | s(f1(x,y),v) | -s(y,y). [resolve(14,a,8,a)]. given #35 (I,wt=24): 64 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(15,a,3,a)]. given #36 (I,wt=24): 65 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(15,a,4,a)]. given #37 (I,wt=22): 66 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | -s(x,f1(x,y)) | -s(y,y). [resolve(15,a,5,a)]. given #38 (I,wt=24): 67 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(15,a,6,a)]. given #39 (I,wt=24): 68 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(15,a,7,a)]. given #40 (I,wt=22): 69 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | s(f1(x,y),w) | -s(y,y). [resolve(15,a,8,a)]. given #41 (I,wt=22): 70 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | -q(w,w) | -q(y,f1(x,y)). [resolve(15,a,9,a)]. given #42 (I,wt=22): 71 s(f1(f1(x,y),z),u) | q(f1(f1(x,y),z),v) | -q(w,w) | q(f1(x,y),w). [resolve(15,a,10,a)]. given #43 (I,wt=20): 72 s(f1(f1(x,y),z),u) | -s(z,z) | -s(x,f1(x,y)) | -q(y,f1(x,y)). [resolve(16,a,3,a)]. given #44 (I,wt=20): 73 s(f1(f1(x,y),z),u) | -s(z,z) | -s(x,f1(x,y)) | q(f1(x,y),v). [resolve(16,a,4,a)]. given #45 (I,wt=18): 74 s(f1(f1(x,y),z),u) | -s(z,z) | -s(x,f1(x,y)) | -s(y,y). [resolve(16,a,5,a)]. given #46 (I,wt=20): 75 s(f1(f1(x,y),z),u) | -s(z,z) | s(f1(x,y),v) | -q(y,f1(x,y)). [resolve(16,a,6,a)]. given #47 (I,wt=20): 76 s(f1(f1(x,y),z),u) | -s(z,z) | s(f1(x,y),v) | q(f1(x,y),w). [resolve(16,a,7,a)]. given #48 (I,wt=18): 77 s(f1(f1(x,y),z),u) | -s(z,z) | s(f1(x,y),v) | -s(y,y). [resolve(16,a,8,a)]. given #49 (I,wt=20): 79 -q(x,x) | -q(y,f1(f1(z,u),y)) | -s(z,f1(z,u)) | q(f1(z,u),v). [resolve(17,a,4,a)]. given #50 (I,wt=20): 82 -q(x,x) | -q(y,f1(f1(z,u),y)) | s(f1(z,u),v) | q(f1(z,u),w). [resolve(17,a,7,a)]. given #51 (I,wt=20): 87 -q(x,x) | q(f1(f1(y,z),u),x) | -s(y,f1(y,z)) | q(f1(y,z),v). [resolve(18,a,4,a)]. given #52 (I,wt=20): 90 -q(x,x) | q(f1(f1(y,z),u),x) | s(f1(y,z),v) | q(f1(y,z),w). [resolve(18,a,7,a)]. given #53 (I,wt=18): 92 -q(x,x) | q(f1(f1(y,z),u),x) | -q(v,v) | q(f1(y,z),v). [resolve(18,a,10,a)]. given #54 (I,wt=17): 100 -s(f1(x,y),f1(f1(x,y),y)) | -s(y,y) | -s(x,f1(x,y)). [factor(49,b,d)]. given #55 (I,wt=17): 101 -s(f1(x,y),f1(f1(x,y),y)) | -s(y,y) | s(f1(x,y),z). [factor(52,b,d)]. given #56 (I,wt=15): 103 s(f1(f1(x,y),y),z) | -s(y,y) | -s(x,f1(x,y)). [factor(74,b,d)]. given #57 (I,wt=15): 104 s(f1(f1(x,y),y),z) | -s(y,y) | s(f1(x,y),u). [factor(77,b,d)]. given #58 (I,wt=15): 105 -q(x,x) | -q(y,f1(f1(z,u),y)) | -q(u,f1(z,u)). [factor(83,a,c)]. given #59 (I,wt=15): 106 -q(x,x) | -q(y,f1(f1(z,u),y)) | q(f1(z,u),x). [factor(84,a,c)]. given #60 (I,wt=15): 108 -q(x,x) | q(f1(f1(y,z),u),x) | -q(z,f1(y,z)). [factor(91,a,c)]. given #61 (I,wt=15): 109 -q(x,x) | q(f1(f1(y,z),u),x) | q(f1(y,z),x). [factor(92,a,c)]. given #62 (I,wt=6): 116 -q(x,x) | -s(y,y). [factor(114,b,c)]. given #63 (F,wt=11): 128 s(x,y) | -q(z,z) | s(f1(y,u),x). [factor(125,a,c)]. given #64 (T,wt=8): 350 s(x,y) | s(f1(y,z),x). [factor(342,b,d),merge(c)]. given #65 (T,wt=10): 409 s(f1(x,y),x) | -s(x,f1(x,x)). [factor(378,a,b)]. given #66 (A,wt=48): 170 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(68,b,67,d)]. given #67 (F,wt=10): 410 s(f1(f1(x,y),z),x) | -s(y,y). [factor(379,a,b)]. given #68 (F,wt=12): 396 s(f1(x,x),x) | s(f1(f1(x,x),x),y). [factor(351,a,c)]. given #69 (T,wt=12): 411 s(f1(f1(x,y),z),x) | q(f1(x,y),u). [factor(380,a,b)]. given #70 (T,wt=10): 562 s(f1(f1(x,y),z),x) | -s(u,u). [resolve(411,b,116,a)]. given #71 (A,wt=48): 171 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(68,b,64,d)]. given #72 (F,wt=10): 612 s(f1(f1(x,y),z),x) | -q(u,u). [factor(597,a,b)]. given #73 (F,wt=7): 623 s(f1(f1(x,y),z),x). [factor(622,a,b)]. given #74 (T,wt=12): 415 s(f1(x,y),x) | -s(x,f1(x,f1(x,y))). [factor(393,a,b)]. given #75 (T,wt=13): 378 s(f1(x,y),x) | s(z,u) | -s(u,f1(u,x)). [resolve(350,a,22,c)]. given #76 (A,wt=38): 173 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(68,b,60,b)]. given #77 (F,wt=12): 625 s(f1(x,x),x) | s(y,f1(f1(x,x),x)). [factor(624,a,c)]. given #78 (F,wt=8): 782 s(f1(x,x),x) | -s(x,x). [factor(776,a,c)]. given #79 (T,wt=5): 786 s(f1(x,x),x). [factor(785,a,b)]. given #80 (T,wt=15): 393 s(f1(x,y),x) | s(z,u) | -s(u,f1(u,f1(x,y))). [resolve(350,b,22,c)]. given #81 (A,wt=48): 174 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(68,b,59,d)]. given #82 (F,wt=15): 400 s(f1(x,y),x) | s(f1(f1(x,y),x),z) | -s(y,y). [factor(357,a,c)]. given #83 (F,wt=17): 351 s(f1(x,y),x) | s(f1(f1(z,x),x),u) | s(f1(z,x),v). [resolve(350,a,104,b)]. given #84 (T,wt=14): 923 s(f1(x,y),x) | s(f1(f1(z,x),x),f1(z,x)). [factor(878,b,c)]. given #85 (T,wt=14): 942 s(f1(x,y),x) | s(f1(z,x),f1(f1(z,x),x)). [factor(903,b,c)]. given #86 (A,wt=38): 175 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(68,b,59,b)]. given #87 (F,wt=10): 958 s(f1(x,y),x) | s(z,f1(u,x)). [factor(945,a,b)]. given #88 (F,wt=5): 1029 s(f1(x,y),x). [factor(1020,a,b)]. given #89 (T,wt=20): 243 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | -q(v6,v6). [factor(196,a,d)]. given #90 (T,wt=17): 1048 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w). [factor(1046,c,d)]. given #91 (A,wt=34): 271 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(254,b,e)]. given #92 (F,wt=15): 1049 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | -s(w,w). [resolve(1048,c,116,a)]. given #93 (F,wt=15): 1098 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | -q(w,w). [factor(1084,a,c)]. given #94 (T,wt=12): 1106 s(f1(f1(x,y),z),u) | s(f1(x,y),v). [factor(1105,b,c)]. given #95 (T,wt=12): 1149 s(f1(x,y),f1(f1(x,y),z)) | -s(u,u). [factor(1125,a,b)]. given #96 (A,wt=29): 1108 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(1106,a,103,b)]. given #97 (F,wt=8): 1170 -s(x,x) | -s(y,f1(y,x)). [back_unit_del(100),unit_del(a,1158)]. given #98 (F,wt=13): 1172 -s(x,x) | -s(y,f1(y,z)) | -q(z,f1(y,z)). [back_unit_del(47),unit_del(a,1158)]. given #99 (T,wt=8): 1169 s(f1(x,y),z) | -s(u,u). [back_unit_del(1109),unit_del(c,1158)]. given #100 (T,wt=5): 1190 s(f1(x,y),z). [factor(1188,a,b)]. ============================== PROOF ================================= % Proof 1 at 0.29 (+ 0.01) seconds. % Length of proof is 32. % Level of proof is 22. % Maximum clause weight is 34. % Given clauses 100. 1 (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)))). [goal]. 5 p(f1(x,y),f1(x,y)) | -s(x,f1(x,y)) | -s(y,y). [deny(1)]. 7 p(f1(x,y),f1(x,y)) | s(f1(x,y),z) | q(f1(x,y),u). [deny(1)]. 13 -p(x,x) | -s(x,f1(x,y)) | -s(y,y). [deny(1)]. 15 -p(x,x) | s(f1(x,y),z) | q(f1(x,y),u). [deny(1)]. 22 s(x,y) | -s(y,f1(y,z)) | -s(z,z). [deny(1)]. 26 s(x,y) | -q(z,z) | -q(u,f1(y,u)). [deny(1)]. 49 -s(f1(x,y),f1(f1(x,y),z)) | -s(z,z) | -s(x,f1(x,y)) | -s(y,y). [resolve(13,a,5,a)]. 68 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(15,a,7,a)]. 100 -s(f1(x,y),f1(f1(x,y),y)) | -s(y,y) | -s(x,f1(x,y)). [factor(49,b,d)]. 196 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | s(v6,v7) | -q(v8,v8). [resolve(68,b,26,c)]. 243 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | -q(v6,v6). [factor(196,a,d)]. 1035 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(243,d,68,b)]. 1043 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(1035,a,d)]. 1046 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w) | q(f1(x,y),v6). [factor(1043,b,d)]. 1048 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | q(f1(x,y),w). [factor(1046,c,d)]. 1084 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | s(w,v6) | -q(v7,v7). [resolve(1048,c,26,c)]. 1098 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | -q(w,w). [factor(1084,a,c)]. 1104 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(1098,c,1048,c)]. 1105 s(f1(f1(x,y),z),u) | s(f1(x,y),v) | s(f1(x,y),w). [factor(1104,a,c)]. 1106 s(f1(f1(x,y),z),u) | s(f1(x,y),v). [factor(1105,b,c)]. 1109 s(f1(x,y),z) | -s(u,u) | -s(f1(x,y),f1(f1(x,y),u)). [resolve(1106,a,100,a)]. 1125 s(f1(x,y),z) | s(u,f1(f1(x,y),v)) | -s(w,w). [resolve(1106,a,22,b)]. 1149 s(f1(x,y),f1(f1(x,y),z)) | -s(u,u). [factor(1125,a,b)]. 1156 s(f1(x,y),f1(f1(x,y),z)) | s(f1(u,v),w). [resolve(1149,b,1106,a)]. 1158 s(f1(x,y),f1(f1(x,y),z)). [factor(1156,a,b)]. 1169 s(f1(x,y),z) | -s(u,u). [back_unit_del(1109),unit_del(c,1158)]. 1170 -s(x,x) | -s(y,f1(y,x)). [back_unit_del(100),unit_del(a,1158)]. 1188 s(f1(x,y),z) | s(f1(u,v),w). [resolve(1169,b,1106,a)]. 1190 s(f1(x,y),z). [factor(1188,a,b)]. 1191 -s(x,x). [resolve(1190,a,1170,b)]. 1192 $F. [resolve(1191,a,1190,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=100. Generated=2702. Kept=1172. proofs=1. Usable=10. Sos=7. Demods=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.65. User_CPU=0.29, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 10893 exit (max_proofs) Sat Aug 12 20:59:02 2006