WATCH: 0.00 CPU 0.01 WC ----- Otter 3.3f, August 2004 ----- The process was started by sutcliff on cl5-018, Wed Aug 3 15:13:07 2011 The command was "/CW/home-0/sutcliff/Systems/Otter---3.3/otter". The process ID is 8340. 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 equal(zero,multiplication(zero,A)). all A equal(addition(A,zero),A). all A B C equal(addition(multiplication(A,B),multiplication(A,C)),multiplication(A,addition(B,C))). all A leq(addition(one,multiplication(star(A),A)),star(A)). all A equal(A,multiplication(one,A)). all A B C (leq(addition(multiplication(A,B),C),B)->leq(multiplication(star(A),C),B)). all C B A equal(addition(addition(A,B),C),addition(A,addition(B,C))). all A B C equal(addition(multiplication(A,C),multiplication(B,C)),multiplication(addition(A,B),C)). all A B (equal(addition(A,B),B)<->leq(A,B)). all A leq(addition(one,multiplication(A,star(A))),star(A)). all A equal(multiplication(A,zero),zero). all A equal(A,multiplication(A,one)). all A equal(addition(A,A),A). all A B C equal(multiplication(multiplication(A,B),C),multiplication(A,multiplication(B,C))). all A B C (leq(addition(multiplication(A,B),C),A)->leq(multiplication(C,star(B)),A)). all A B equal(addition(A,B),addition(B,A)). -leq(multiplication(a,multiplication(a,multiplication(a,a))),star(a)). end_of_list. -------> usable clausifies to: list(usable). 0 [] equal(X,X). 0 [] equal(zero,multiplication(zero,A)). 0 [] equal(addition(A,zero),A). 0 [] equal(addition(multiplication(A,B),multiplication(A,C)),multiplication(A,addition(B,C))). 0 [] leq(addition(one,multiplication(star(A),A)),star(A)). 0 [] equal(A,multiplication(one,A)). 0 [] -leq(addition(multiplication(A,B),C),B)|leq(multiplication(star(A),C),B). 0 [] equal(addition(addition(A,B),C),addition(A,addition(B,C))). 0 [] equal(addition(multiplication(A,C),multiplication(B,C)),multiplication(addition(A,B),C)). 0 [] -equal(addition(A,B),B)|leq(A,B). 0 [] equal(addition(A,B),B)| -leq(A,B). 0 [] leq(addition(one,multiplication(A,star(A))),star(A)). 0 [] equal(multiplication(A,zero),zero). 0 [] equal(A,multiplication(A,one)). 0 [] equal(addition(A,A),A). 0 [] equal(multiplication(multiplication(A,B),C),multiplication(A,multiplication(B,C))). 0 [] -leq(addition(multiplication(A,B),C),A)|leq(multiplication(C,star(B)),A). 0 [] equal(addition(A,B),addition(B,A)). 0 [] -leq(multiplication(a,multiplication(a,multiplication(a,a))),star(a)). 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=13): 1 [] -leq(addition(multiplication(A,B),C),B)|leq(multiplication(star(A),C),B). ** KEPT (pick-wt=8): 2 [] -equal(addition(A,B),B)|leq(A,B). ** KEPT (pick-wt=8): 3 [] equal(addition(A,B),B)| -leq(A,B). ** KEPT (pick-wt=13): 4 [] -leq(addition(multiplication(A,B),C),A)|leq(multiplication(C,star(B)),A). ** KEPT (pick-wt=10): 5 [] -leq(multiplication(a,multiplication(a,multiplication(a,a))),star(a)). ------------> process sos: ** KEPT (pick-wt=3): 6 [] equal(A,A). ** KEPT (pick-wt=5): 8 [copy,7,flip.1] equal(multiplication(zero,A),zero). ---> New Demodulator: 9 [new_demod,8] equal(multiplication(zero,A),zero). ** KEPT (pick-wt=5): 10 [] equal(addition(A,zero),A). ---> New Demodulator: 11 [new_demod,10] equal(addition(A,zero),A). ** KEPT (pick-wt=13): 13 [copy,12,flip.1] equal(multiplication(A,addition(B,C)),addition(multiplication(A,B),multiplication(A,C))). ---> New Demodulator: 14 [new_demod,13] equal(multiplication(A,addition(B,C)),addition(multiplication(A,B),multiplication(A,C))). ** KEPT (pick-wt=9): 15 [] leq(addition(one,multiplication(star(A),A)),star(A)). ** KEPT (pick-wt=5): 17 [copy,16,flip.1] equal(multiplication(one,A),A). ---> New Demodulator: 18 [new_demod,17] equal(multiplication(one,A),A). ** KEPT (pick-wt=11): 19 [] equal(addition(addition(A,B),C),addition(A,addition(B,C))). ---> New Demodulator: 20 [new_demod,19] equal(addition(addition(A,B),C),addition(A,addition(B,C))). ** KEPT (pick-wt=13): 22 [copy,21,flip.1] equal(multiplication(addition(A,B),C),addition(multiplication(A,C),multiplication(B,C))). ---> New Demodulator: 23 [new_demod,22] equal(multiplication(addition(A,B),C),addition(multiplication(A,C),multiplication(B,C))). ** KEPT (pick-wt=9): 24 [] leq(addition(one,multiplication(A,star(A))),star(A)). ** KEPT (pick-wt=5): 25 [] equal(multiplication(A,zero),zero). ---> New Demodulator: 26 [new_demod,25] equal(multiplication(A,zero),zero). ** KEPT (pick-wt=5): 28 [copy,27,flip.1] equal(multiplication(A,one),A). ---> New Demodulator: 29 [new_demod,28] equal(multiplication(A,one),A). ** KEPT (pick-wt=5): 30 [] equal(addition(A,A),A). ---> New Demodulator: 31 [new_demod,30] equal(addition(A,A),A). ** KEPT (pick-wt=11): 32 [] equal(multiplication(multiplication(A,B),C),multiplication(A,multiplication(B,C))). ---> New Demodulator: 33 [new_demod,32] equal(multiplication(multiplication(A,B),C),multiplication(A,multiplication(B,C))). ** KEPT (pick-wt=7): 34 [] equal(addition(A,B),addition(B,A)). Following clause subsumed by 6 during input processing: 0 [copy,6,flip.1] equal(A,A). >>>> Starting back demodulation with 9. >>>> Starting back demodulation with 11. >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 18. >>>> Starting back demodulation with 20. >>>> Starting back demodulation with 23. >>>> Starting back demodulation with 26. >>>> Starting back demodulation with 29. >>>> Starting back demodulation with 31. >>>> Starting back demodulation with 33. Following clause subsumed by 34 during input processing: 0 [copy,34,flip.1] equal(addition(A,B),addition(B,A)). ======= end of input processing ======= =========== start of search ===========  Resetting weight limit to 10. Resetting weight limit to 10. sos_size=1364  Resetting weight limit to 9. Resetting weight limit to 9. sos_size=1569 WATCH: 2.92 CPU 3.02 WC WATCH: 5.92 CPU 6.03 WC WATCH: 8.93 CPU 9.04 WC WATCH: 11.93 CPU 12.05 WC WATCH: 14.94 CPU 15.06 WC WATCH: 17.94 CPU 18.07 WC WATCH: 20.95 CPU 21.07 WC WATCH: 23.95 CPU 24.08 WC WATCH: 26.96 CPU 27.09 WC WATCH: 29.96 CPU 30.10 WC WATCH: 32.97 CPU 33.11 WC WATCH: 35.97 CPU 36.12 WC WATCH: 38.98 CPU 39.13 WC WATCH: 41.98 CPU 42.14 WC WATCH: 44.99 CPU 45.15 WC WATCH: 47.99 CPU 48.16 WC WATCH: 51.00 CPU 51.17 WC WATCH: 54.00 CPU 54.18 WC WATCH: 57.00 CPU 57.20 WC WATCH: 60.01 CPU 60.21 WC WATCH: 63.02 CPU 63.22 WC WATCH: 66.03 CPU 66.24 WC WATCH: 69.04 CPU 69.26 WC WATCH: 72.05 CPU 72.27 WC WATCH: 75.06 CPU 75.28 WC WATCH: 78.07 CPU 78.30 WC WATCH: 81.09 CPU 81.32 WC WATCH: 84.09 CPU 84.33 WC WATCH: 87.10 CPU 87.34 WC WATCH: 90.10 CPU 90.35 WC WATCH: 93.10 CPU 93.36 WC WATCH: 96.11 CPU 96.37 WC WATCH: 99.11 CPU 99.38 WC WATCH: 102.12 CPU 102.39 WC WATCH: 105.12 CPU 105.40 WC WATCH: 108.13 CPU 108.41 WC WATCH: 111.13 CPU 111.41 WC WATCH: 114.14 CPU 114.42 WC WATCH: 117.14 CPU 117.43 WC WATCH: 120.14 CPU 120.44 WC WATCH: 123.15 CPU 123.45 WC WATCH: 126.15 CPU 126.46 WC WATCH: 129.16 CPU 129.47 WC WATCH: 132.16 CPU 132.48 WC WATCH: 135.17 CPU 135.49 WC WATCH: 138.17 CPU 138.50 WC WATCH: 141.18 CPU 141.51 WC WATCH: 144.18 CPU 144.52 WC WATCH: 147.19 CPU 147.53 WC WATCH: 150.19 CPU 150.54 WC WATCH: 153.20 CPU 153.55 WC WATCH: 156.20 CPU 156.56 WC WATCH: 159.20 CPU 159.57 WC WATCH: 162.21 CPU 162.58 WC WATCH: 165.21 CPU 165.59 WC WATCH: 168.22 CPU 168.60 WC WATCH: 171.22 CPU 171.61 WC WATCH: 174.23 CPU 174.62 WC WATCH: 177.23 CPU 177.63 WC WATCH: 180.24 CPU 180.64 WC WATCH: 183.24 CPU 183.65 WC WATCH: 186.24 CPU 186.66 WC WATCH: 189.25 CPU 189.67 WC WATCH: 192.25 CPU 192.68 WC WATCH: 195.26 CPU 195.69 WC WATCH: 198.26 CPU 198.70 WC WATCH: 201.27 CPU 201.71 WC WATCH: 204.27 CPU 204.72 WC WATCH: 207.27 CPU 207.73 WC WATCH: 210.28 CPU 210.74 WC WATCH: 213.28 CPU 213.75 WC WATCH: 216.29 CPU 216.76 WC WATCH: 219.29 CPU 219.77 WC WATCH: 222.30 CPU 222.78 WC WATCH: 225.30 CPU 225.79 WC WATCH: 228.31 CPU 228.80 WC WATCH: 231.31 CPU 231.81 WC WATCH: 234.32 CPU 234.82 WC WATCH: 237.32 CPU 237.82 WC WATCH: 240.33 CPU 240.83 WC WATCH: 243.33 CPU 243.84 WC WATCH: 246.34 CPU 246.85 WC WATCH: 249.34 CPU 249.86 WC WATCH: 252.35 CPU 252.87 WC WATCH: 255.35 CPU 255.88 WC WATCH: 258.36 CPU 258.90 WC WATCH: 261.36 CPU 261.91 WC WATCH: 264.37 CPU 264.92 WC WATCH: 267.38 CPU 267.94 WC WATCH: 270.39 CPU 270.95 WC WATCH: 273.40 CPU 273.96 WC WATCH: 276.41 CPU 276.98 WC WATCH: 279.42 CPU 279.99 WC WATCH: 282.42 CPU 283.01 WC WATCH: 285.43 CPU 286.02 WC WATCH: 288.44 CPU 289.03 WC WATCH: 291.45 CPU 292.05 WC WATCH: 294.46 CPU 295.06 WC WATCH: 297.46 CPU 298.07 WC WATCH: 300.47 CPU 301.08 WC FINAL WATCH: 300.47 CPU 301.20 WC