% problem-set/algebra/groups/ident2.ver1.out % created : 08/12/88 % revised : 08/12/88 OTTER version 0.91, 14 June 1988. set(UR_res). set(back_demod). set(factor). set(Unit_deletion). assign(max_kept,5000). list(axioms). 1 P(e,x,x). 2 P(g(x),x,e). 3 P(x,y,f(x,y)). 4 -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w). 5 -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w). 6 -P(x,y,z) | -P(x,y,w) | EQUAL(z,w). 7 EQUAL(x,x). 8 -EQUAL(x,y) | EQUAL(y,x). 9 -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 10 -EQUAL(x,y) | -P(x,w,z) | P(y,w,z). 11 -EQUAL(x,y) | -P(w,x,z) | P(w,y,z). 12 -EQUAL(x,y) | -P(w,z,x) | P(w,z,y). 13 -EQUAL(x,y) | EQUAL(f(x,w),f(y,w)). 14 -EQUAL(x,y) | EQUAL(f(w,x),f(w,y)). 15 -EQUAL(x,y) | EQUAL(g(x),g(y)). end_of_list. list(sos). 16 -P(k(y),y,k(y)). end_of_list. new given clause: 16 -P(k(y),y,k(y)). ** KEPT: 17 (16,12,3) -EQUAL(f(k(x),x),k(x)). ** KEPT: 18 (16,5,1,3) -P(e,f(k(x),x),k(x)). ** KEPT: 19 (16,4,2,1) -P(k(e),g(k(e)),e). ** KEPT: 20 (16,4,3,3) -P(f(k(f(x,y)),x),y,k(f(x,y))). ** KEPT: 21 (16,4,3,2) -P(f(k(e),g(x)),x,k(e)). ** KEPT: 22 (16,4,3,1) -P(f(k(x),e),x,k(x)). new given clause: 17 (16,12,3) -EQUAL(f(k(x),x),k(x)). ** KEPT: 23 (17,6,1) -P(e,k(x),f(k(x),x)). new given clause: 19 (16,4,2,1) -P(k(e),g(k(e)),e). ** KEPT: 24 (19,12,3) -EQUAL(f(k(e),g(k(e))),e). ** KEPT: 25 (19,10,2) -EQUAL(g(g(k(e))),k(e)). ** KEPT: 26 (19,5,3,2) -P(g(f(x,g(k(e)))),x,k(e)). ** KEPT: 27 (19,5,2,2) -P(g(e),g(g(k(e))),k(e)). ** KEPT: 28 (19,5,2,1) -P(e,g(g(k(e))),k(e)). ** KEPT: 29 (19,5,1,2) -P(g(g(k(e))),e,k(e)). ** KEPT: 30 (19,5,1,3) -P(e,f(k(e),g(k(e))),e). ** KEPT: 31 (19,4,1,2) -P(k(e),e,g(g(k(e)))). ** KEPT: 32 (19,4,3,1) -P(f(k(e),e),g(k(e)),e). new given clause: 25 (19,10,2) -EQUAL(g(g(k(e))),k(e)). ** KEPT: 33 (25,6,1) -P(e,k(e),g(g(k(e)))). new given clause: 18 (16,5,1,3) -P(e,f(k(x),x),k(x)). ** KEPT: 34 (18,12,3) -EQUAL(f(e,f(k(x),x)),k(x)). ** KEPT: 35 (18,5,2,3) -P(g(x),f(x,f(k(y),y)),k(y)). ** KEPT: 36 (18,5,2,2) -P(g(g(f(k(x),x))),e,k(x)). ** KEPT: 37 (18,5,2,1) -P(g(e),f(k(x),x),k(x)). ** KEPT: 38 (18,5,1,3) -P(e,f(e,f(k(x),x)),k(x)). ** KEPT: 39 (18,4,3,3) -P(f(e,k(x)),x,k(x)). ** KEPT: 40 (18,4,3,1) -P(f(e,e),f(k(x),x),k(x)). new given clause: 22 (16,4,3,1) -P(f(k(x),e),x,k(x)). ** KEPT: 41 (22,12,3) -EQUAL(f(f(k(x),e),x),k(x)). ** KEPT: 42 (22,5,3,3) -P(k(x),f(e,x),k(x)). ** KEPT: 43 (22,5,1,3) -P(e,f(f(k(x),e),x),k(x)). ** KEPT: 44 (22,4,3,3) -P(f(f(k(f(x,y)),e),x),y,k(f(x,y))). ** KEPT: 45 (22,4,3,2) -P(f(f(k(e),e),g(x)),x,k(e)). ** KEPT: 46 (22,4,3,1) -P(f(f(k(x),e),e),x,k(x)). new given clause: 23 (17,6,1) -P(e,k(x),f(k(x),x)). ** KEPT: 47 (23,12,3) -EQUAL(f(k(x),x),f(e,k(x))). ** KEPT: 48 (23,5,2,3) -P(g(x),f(x,k(y)),f(k(y),y)). ** KEPT: 49 (23,5,2,2) -P(g(g(k(x))),e,f(k(x),x)). ** KEPT: 50 (23,5,2,1) -P(g(e),k(x),f(k(x),x)). ** KEPT: 51 (23,5,1,3) -P(e,f(e,k(x)),f(k(x),x)). ** KEPT: 52 (23,4,3,1) -P(f(e,e),k(x),f(k(x),x)). new given clause: 24 (19,12,3) -EQUAL(f(k(e),g(k(e))),e). ** KEPT: 53 (24,6,2) -P(g(x),x,f(k(e),g(k(e)))). ** KEPT: 54 (24,6,1) -P(e,e,f(k(e),g(k(e)))). new given clause: 28 (19,5,2,1) -P(e,g(g(k(e))),k(e)). ** KEPT: 55 (28,12,3) -EQUAL(f(e,g(g(k(e)))),k(e)). ** KEPT: 56 (28,5,2,3) -P(g(x),f(x,g(g(k(e)))),k(e)). ** KEPT: 57 (28,5,2,2) -P(g(g(g(g(k(e))))),e,k(e)). ** KEPT: 58 (28,5,1,3) -P(e,f(e,g(g(k(e)))),k(e)). ** KEPT: 59 (28,4,3,1) -P(f(e,e),g(g(k(e))),k(e)). new given clause: 29 (19,5,1,2) -P(g(g(k(e))),e,k(e)). ---------------- PROOF ---------------- ** KEPT: 60 (29,12,3) -EQUAL(f(g(g(k(e))),e),k(e)). ** KEPT: 61 (29,5,1,3) -P(e,f(g(g(k(e))),e),k(e)). ** KEPT: 62 (29,4,2,1,2) . ** KEPT: 63 (29,4,2,1,2) . ** KEPT: 64 (29,4,3,2) -P(f(g(g(k(e))),g(x)),x,k(e)). ** KEPT: 65 (29,4,3,1) -P(f(g(g(k(e))),e),e,k(e)). ** KEPT: 66 (29,4,2,2,1) . ------------> EMPTY CLAUSE -----------> 62 (29,4,2,1,2) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 1 P(e,x,x). 2 P(g(x),x,e). 4 -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w). 5 -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w). 16 -P(k(y),y,k(y)). 19 (16,4,2,1) -P(k(e),g(k(e)),e). 29 (19,5,1,2) -P(g(g(k(e))),e,k(e)). 62 (29,4,2,1,2) . --------------- options --------------- set(UR_res). set(demod_hist). set(for_sub). set(Unit_deletion). set(print_kept). set(factor). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). set(back_demod). set(print_new_demod). set(print_back_demod). clear(binary_res). clear(hyper_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). clear(order_eq). clear(dynamic_demod). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 5000). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 3). assign(fpa_terms, 3). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). ------------- memory usage ------------ 2 mallocs of 32700 bytes each (63.9+ K) type (bytes each) gets frees in use avail bytes sym_ent ( 64) 24 0 24 0 1.5 K term ( 16) 2094 1942 152 9 2.5 K rel ( 20) 1762 1460 302 6 6.0 K term_ptr ( 8) 897 0 897 0 7.0 K fpa_head ( 12) 214 0 214 0 2.5 K fpa_tree ( 28) 1064 1064 0 19 0.5 K context ( 260) 418 418 0 5 1.3 K trail ( 12) 761 761 0 10 0.1 K imd_tree ( 24) 0 0 0 0 0.0 K imd_pos ( 416) 0 0 0 0 0.0 K is_tree ( 12) 381 0 381 0 4.5 K is_pos (1216) 2425 2425 0 3 3.6 K fsub_pos ( 8) 163 163 0 1 0.0 K literal ( 16) 193 110 83 2 1.3 K clause ( 28) 131 65 66 0 1.8 K list ( 60) 2 0 2 0 0.1 K clash_nd ( 32) 55 55 0 2 0.1 K clause_ptr ( 8) 74 8 66 8 0.6 K int_ptr ( 8) 399 208 191 0 1.5 K -------------- statistics ------------- clauses input 16 clauses given 10 clauses generated 113 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 63 (clauses subsumed by sos) 7 unit deletions 3 clauses kept 50 new demodualtors 0 empty clauses 1 factors generated 0 clauses back demodulated 0 clauses back subsumed 0 clauses not processed 7 ----------- times (seconds) ----------- run time 1.75 input time 0.25 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.47 para_into time 0.00 para_from time 0.00 pre_process time 0.72 demod time 0.00 weigh time 0.02 for_sub time 0.24 unit_del time 0.08 post_process time 0.15 back_sub time 0.04 conflict time 0.09 factor time 0.00 back demod time 0.00 FPA build time 0.10 IS build time 0.04 print_cl time 0.21 cl integrate time 0.06 window time 0.00