WATCH: 0.00 CPU 0.01 WC ----- Otter 3.3f, August 2004 ----- The process was started by sutcliff on cl5-021, Wed Aug 3 14:36:52 2011 The command was "/CW/home-0/sutcliff/Systems/Otter---3.3/otter". The process ID is 12056. set(prolog_style_variables). set(tptp_eq). set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). clear(print_given). formula_list(usable). all X equal(X,X). all A B C equal(multiplication(A,multiplication(B,C)),multiplication(multiplication(A,B),C)). all A equal(A,addition(A,zero)). all C B A equal(addition(A,addition(B,C)),addition(addition(A,B),C)). all A equal(addition(A,A),A). all A equal(multiplication(zero,A),zero). all A equal(multiplication(A,zero),zero). all A B C equal(multiplication(addition(A,B),C),addition(multiplication(A,C),multiplication(B,C))). all A equal(A,multiplication(one,A)). all A B C equal(addition(multiplication(A,B),multiplication(A,C)),multiplication(A,addition(B,C))). all A B (equal(addition(A,B),B)<->leq(A,B)). all A equal(A,multiplication(A,one)). all A B equal(addition(A,B),addition(B,A)). all X0 equal(one,addition(antidomain(antidomain(X0)),antidomain(X0))). all X0 equal(codomain(X0),coantidomain(coantidomain(X0))). all X0 equal(one,addition(coantidomain(coantidomain(X0)),coantidomain(X0))). all X0 equal(domain(X0),antidomain(antidomain(X0))). all X0 X1 equal(addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))). all X0 X1 equal(antidomain(multiplication(X0,antidomain(antidomain(X1)))),addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1)))))). all X0 equal(multiplication(antidomain(X0),X0),zero). all X0 equal(multiplication(X0,coantidomain(X0)),zero). all X0 X1 equal(backward_diamond(X0,X1),codomain(multiplication(codomain(X1),X0))). all X0 equal(antidomain(domain(X0)),c(X0)). all X0 X1 equal(forward_diamond(X0,X1),domain(multiplication(X0,domain(X1)))). all X0 X1 equal(multiplication(domain(X0),antidomain(X1)),domain_difference(X0,X1)). all X0 X1 equal(backward_box(X0,X1),c(backward_diamond(X0,c(X1)))). all X0 X1 equal(c(forward_diamond(X0,c(X1))),forward_box(X0,X1)). -(all X0 X1 X2 (equal(addition(domain(X1),backward_box(X0,domain(X2))),one)->equal(addition(forward_box(X0,domain(X1)),domain(X2)),one))). end_of_list. -------> usable clausifies to: list(usable). 0 [] equal(X,X). 0 [] equal(multiplication(A,multiplication(B,C)),multiplication(multiplication(A,B),C)). 0 [] equal(A,addition(A,zero)). 0 [] equal(addition(A,addition(B,C)),addition(addition(A,B),C)). 0 [] equal(addition(A,A),A). 0 [] equal(multiplication(zero,A),zero). 0 [] equal(multiplication(A,zero),zero). 0 [] equal(multiplication(addition(A,B),C),addition(multiplication(A,C),multiplication(B,C))). 0 [] equal(A,multiplication(one,A)). 0 [] equal(addition(multiplication(A,B),multiplication(A,C)),multiplication(A,addition(B,C))). 0 [] -equal(addition(A,B),B)|leq(A,B). 0 [] equal(addition(A,B),B)| -leq(A,B). 0 [] equal(A,multiplication(A,one)). 0 [] equal(addition(A,B),addition(B,A)). 0 [] equal(one,addition(antidomain(antidomain(X0)),antidomain(X0))). 0 [] equal(codomain(X0),coantidomain(coantidomain(X0))). 0 [] equal(one,addition(coantidomain(coantidomain(X0)),coantidomain(X0))). 0 [] equal(domain(X0),antidomain(antidomain(X0))). 0 [] equal(addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))). 0 [] equal(antidomain(multiplication(X0,antidomain(antidomain(X1)))),addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1)))))). 0 [] equal(multiplication(antidomain(X0),X0),zero). 0 [] equal(multiplication(X0,coantidomain(X0)),zero). 0 [] equal(backward_diamond(X0,X1),codomain(multiplication(codomain(X1),X0))). 0 [] equal(antidomain(domain(X0)),c(X0)). 0 [] equal(forward_diamond(X0,X1),domain(multiplication(X0,domain(X1)))). 0 [] equal(multiplication(domain(X0),antidomain(X1)),domain_difference(X0,X1)). 0 [] equal(backward_box(X0,X1),c(backward_diamond(X0,c(X1)))). 0 [] equal(c(forward_diamond(X0,c(X1))),forward_box(X0,X1)). 0 [] equal(addition(domain($c2),backward_box($c3,domain($c1))),one). 0 [] -equal(addition(forward_box($c3,domain($c2)),domain($c1)),one). end_of_list. SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. This is a Horn set with equality. The strategy will be Knuth-Bendix and hyper_res, with positive clauses in sos and nonpositive clauses in usable. dependent: set(knuth_bendix). dependent: set(anl_eq). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(lrpo). dependent: set(hyper_res). dependent: clear(order_hyper). ------------> process usable: ** KEPT (pick-wt=8): 1 [] -equal(addition(A,B),B)|leq(A,B). ** KEPT (pick-wt=8): 2 [] equal(addition(A,B),B)| -leq(A,B). ** KEPT (pick-wt=9): 3 [] -equal(addition(forward_box($c3,domain($c2)),domain($c1)),one). ------------> process sos: ** KEPT (pick-wt=3): 4 [] equal(A,A). ** KEPT (pick-wt=11): 6 [copy,5,flip.1] equal(multiplication(multiplication(A,B),C),multiplication(A,multiplication(B,C))). ---> New Demodulator: 7 [new_demod,6] equal(multiplication(multiplication(A,B),C),multiplication(A,multiplication(B,C))). ** KEPT (pick-wt=5): 9 [copy,8,flip.1] equal(addition(A,zero),A). ---> New Demodulator: 10 [new_demod,9] equal(addition(A,zero),A). ** KEPT (pick-wt=11): 12 [copy,11,flip.1] equal(addition(addition(A,B),C),addition(A,addition(B,C))). ---> New Demodulator: 13 [new_demod,12] equal(addition(addition(A,B),C),addition(A,addition(B,C))). ** KEPT (pick-wt=5): 14 [] equal(addition(A,A),A). ---> New Demodulator: 15 [new_demod,14] equal(addition(A,A),A). ** KEPT (pick-wt=5): 16 [] equal(multiplication(zero,A),zero). ---> New Demodulator: 17 [new_demod,16] equal(multiplication(zero,A),zero). ** KEPT (pick-wt=5): 18 [] equal(multiplication(A,zero),zero). ---> New Demodulator: 19 [new_demod,18] equal(multiplication(A,zero),zero). ** KEPT (pick-wt=13): 20 [] equal(multiplication(addition(A,B),C),addition(multiplication(A,C),multiplication(B,C))). ---> New Demodulator: 21 [new_demod,20] equal(multiplication(addition(A,B),C),addition(multiplication(A,C),multiplication(B,C))). ** KEPT (pick-wt=5): 23 [copy,22,flip.1] equal(multiplication(one,A),A). ---> New Demodulator: 24 [new_demod,23] equal(multiplication(one,A),A). ** KEPT (pick-wt=13): 26 [copy,25,flip.1] equal(multiplication(A,addition(B,C)),addition(multiplication(A,B),multiplication(A,C))). ---> New Demodulator: 27 [new_demod,26] equal(multiplication(A,addition(B,C)),addition(multiplication(A,B),multiplication(A,C))). ** KEPT (pick-wt=5): 29 [copy,28,flip.1] equal(multiplication(A,one),A). ---> New Demodulator: 30 [new_demod,29] equal(multiplication(A,one),A). ** KEPT (pick-wt=7): 31 [] equal(addition(A,B),addition(B,A)). ** KEPT (pick-wt=8): 33 [copy,32,flip.1] equal(addition(antidomain(antidomain(A)),antidomain(A)),one). ---> New Demodulator: 34 [new_demod,33] equal(addition(antidomain(antidomain(A)),antidomain(A)),one). ** KEPT (pick-wt=6): 35 [] equal(codomain(A),coantidomain(coantidomain(A))). ---> New Demodulator: 36 [new_demod,35] equal(codomain(A),coantidomain(coantidomain(A))). ** KEPT (pick-wt=8): 38 [copy,37,flip.1] equal(addition(coantidomain(coantidomain(A)),coantidomain(A)),one). ---> New Demodulator: 39 [new_demod,38] equal(addition(coantidomain(coantidomain(A)),coantidomain(A)),one). ** KEPT (pick-wt=6): 40 [] equal(domain(A),antidomain(antidomain(A))). ---> New Demodulator: 41 [new_demod,40] equal(domain(A),antidomain(antidomain(A))). ** KEPT (pick-wt=18): 42 [] equal(addition(coantidomain(multiplication(A,B)),coantidomain(multiplication(coantidomain(coantidomain(A)),B))),coantidomain(multiplication(coantidomain(coantidomain(A)),B))). ---> New Demodulator: 43 [new_demod,42] equal(addition(coantidomain(multiplication(A,B)),coantidomain(multiplication(coantidomain(coantidomain(A)),B))),coantidomain(multiplication(coantidomain(coantidomain(A)),B))). ** KEPT (pick-wt=18): 45 [copy,44,flip.1] equal(addition(antidomain(multiplication(A,B)),antidomain(multiplication(A,antidomain(antidomain(B))))),antidomain(multiplication(A,antidomain(antidomain(B))))). ---> New Demodulator: 46 [new_demod,45] equal(addition(antidomain(multiplication(A,B)),antidomain(multiplication(A,antidomain(antidomain(B))))),antidomain(multiplication(A,antidomain(antidomain(B))))). ** KEPT (pick-wt=6): 47 [] equal(multiplication(antidomain(A),A),zero). ---> New Demodulator: 48 [new_demod,47] equal(multiplication(antidomain(A),A),zero). ** KEPT (pick-wt=6): 49 [] equal(multiplication(A,coantidomain(A)),zero). ---> New Demodulator: 50 [new_demod,49] equal(multiplication(A,coantidomain(A)),zero). ** KEPT (pick-wt=11): 52 [copy,51,demod,36,36,flip.1] equal(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(A)),B))),backward_diamond(B,A)). ---> New Demodulator: 53 [new_demod,52] equal(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(A)),B))),backward_diamond(B,A)). ** KEPT (pick-wt=7): 55 [copy,54,demod,41,flip.1] equal(c(A),antidomain(antidomain(antidomain(A)))). ---> New Demodulator: 56 [new_demod,55] equal(c(A),antidomain(antidomain(antidomain(A)))). ** KEPT (pick-wt=11): 58 [copy,57,demod,41,41,flip.1] equal(antidomain(antidomain(multiplication(A,antidomain(antidomain(B))))),forward_diamond(A,B)). ---> New Demodulator: 59 [new_demod,58] equal(antidomain(antidomain(multiplication(A,antidomain(antidomain(B))))),forward_diamond(A,B)). ** KEPT (pick-wt=10): 61 [copy,60,demod,41] equal(multiplication(antidomain(antidomain(A)),antidomain(B)),domain_difference(A,B)). ---> New Demodulator: 62 [new_demod,61] equal(multiplication(antidomain(antidomain(A)),antidomain(B)),domain_difference(A,B)). ** KEPT (pick-wt=13): 64 [copy,63,demod,56,56,flip.1] equal(antidomain(antidomain(antidomain(backward_diamond(A,antidomain(antidomain(antidomain(B))))))),backward_box(A,B)). ---> New Demodulator: 65 [new_demod,64] equal(antidomain(antidomain(antidomain(backward_diamond(A,antidomain(antidomain(antidomain(B))))))),backward_box(A,B)). ** KEPT (pick-wt=13): 67 [copy,66,demod,56,56] equal(antidomain(antidomain(antidomain(forward_diamond(A,antidomain(antidomain(antidomain(B))))))),forward_box(A,B)). ---> New Demodulator: 68 [new_demod,67] equal(antidomain(antidomain(antidomain(forward_diamond(A,antidomain(antidomain(antidomain(B))))))),forward_box(A,B)). ** KEPT (pick-wt=11): 70 [copy,69,demod,41,41] equal(addition(antidomain(antidomain($c2)),backward_box($c3,antidomain(antidomain($c1)))),one). ---> New Demodulator: 71 [new_demod,70] equal(addition(antidomain(antidomain($c2)),backward_box($c3,antidomain(antidomain($c1)))),one). Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] equal(A,A). >>>> Starting back demodulation with 7. >>>> Starting back demodulation with 10. >>>> Starting back demodulation with 13. >>>> Starting back demodulation with 15. >>>> Starting back demodulation with 17. >>>> Starting back demodulation with 19. >>>> Starting back demodulation with 21. >>>> Starting back demodulation with 24. >>>> Starting back demodulation with 27. >>>> Starting back demodulation with 30. Following clause subsumed by 31 during input processing: 0 [copy,31,flip.1] equal(addition(A,B),addition(B,A)). >>>> Starting back demodulation with 34. >>>> Starting back demodulation with 36. >>>> Starting back demodulation with 39. >>>> Starting back demodulation with 41. >> back demodulating 3 with 41. >>>> Starting back demodulation with 43. >>>> Starting back demodulation with 46. >>>> Starting back demodulation with 48. >>>> Starting back demodulation with 50. >>>> Starting back demodulation with 53. >>>> Starting back demodulation with 56. >>>> Starting back demodulation with 59. >>>> Starting back demodulation with 62. >>>> Starting back demodulation with 65. >>>> Starting back demodulation with 68. >>>> Starting back demodulation with 71. ======= end of input processing ======= =========== start of search ===========  Resetting weight limit to 8. Resetting weight limit to 8. sos_size=203  Resetting weight limit to 6. Resetting weight limit to 6. sos_size=58 Search stopped because sos empty. Search stopped because sos empty. ============ end of search ============ -------------- statistics ------------- clauses given 440 clauses generated 65165 clauses kept 622 clauses forward subsumed 17547 clauses back subsumed 46 Kbytes malloced 6835 ----------- times (seconds) ----------- user CPU time 0.26 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) Process 12056 finished Wed Aug 3 14:36:52 2011 Otter interrupted PROOF NOT FOUND WATCH: 0.42 CPU 0.58 WC FINAL WATCH: 0.42 CPU 0.58 WC