----- Otter 3.0.4, August 1995 ----- The job was started by brings on hopfield.phil.rpi.edu, Tue Feb 10 12:18:45 1998 The command was "otter". set(auto). 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). assign(max_seconds,60). formula_list(usable). all x (Killer(x)->Mansion(x)). Mansion(Agatha). Mansion(butler). Mansion(Charles). Killer(Agatha)|Killer(butler)|Killer(Charles). all x (Killer(x)->Hates(x,Agatha)). all x (Killer(x)-> -Richer(x,Agatha)). all x (Hates(Agatha,x)-> -Hates(Charles,x)). all x (x!=butler->Hates(Agatha,x)). all x (-Richer(x,Agatha)->Hates(butler,x)). all x (Hates(Agatha,x)->Hates(butler,x)). all x exists y (-Hates(x,y)). butler!=Agatha. -Killer(Agatha). end_of_list. -------> usable clausifies to: list(usable). 0 [] -Killer(x)|Mansion(x). 0 [] Mansion(Agatha). 0 [] Mansion(butler). 0 [] Mansion(Charles). 0 [] Killer(Agatha)|Killer(butler)|Killer(Charles). 0 [] -Killer(x)|Hates(x,Agatha). 0 [] -Killer(x)| -Richer(x,Agatha). 0 [] -Hates(Agatha,x)| -Hates(Charles,x). 0 [] x=butler|Hates(Agatha,x). 0 [] Richer(x,Agatha)|Hates(butler,x). 0 [] -Hates(Agatha,x)|Hates(butler,x). 0 [] -Hates(x,$f1(x)). 0 [] butler!=Agatha. 0 [] -Killer(Agatha). end_of_list. SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=3. This ia a non-Horn set with equality. The strategy will be Knuth-Bendix, ordered hyper_res, factoring, and unit deleteion, with positive clauses in sos and nonpositive clauses in usable. dependent: set(knuth_bendix). 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: set(unit_deletion). dependent: set(factor). ------------> process usable: ** KEPT (pick-wt=4): 1 [] -Killer(x)|Mansion(x). ** KEPT (pick-wt=5): 2 [] -Killer(x)|Hates(x,Agatha). ** KEPT (pick-wt=5): 3 [] -Killer(x)| -Richer(x,Agatha). ** KEPT (pick-wt=6): 4 [] -Hates(Agatha,x)| -Hates(Charles,x). ** KEPT (pick-wt=6): 5 [] -Hates(Agatha,x)|Hates(butler,x). ** KEPT (pick-wt=4): 6 [] -Hates(x,$f1(x)). ** KEPT (pick-wt=3): 7 [] butler!=Agatha. ** KEPT (pick-wt=2): 8 [] -Killer(Agatha). ------------> process sos: ** KEPT (pick-wt=2): 9 [] Mansion(Agatha). ** KEPT (pick-wt=2): 10 [] Mansion(butler). ** KEPT (pick-wt=2): 11 [] Mansion(Charles). ** KEPT (pick-wt=4): 13 [copy,12,unit_del,8] Killer(butler)|Killer(Charles). ** KEPT (pick-wt=6): 14 [] x=butler|Hates(Agatha,x). ** KEPT (pick-wt=6): 15 [] Richer(x,Agatha)|Hates(butler,x). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=2) 9 [] Mansion(Agatha). given clause #2: (wt=2) 10 [] Mansion(butler). given clause #3: (wt=2) 11 [] Mansion(Charles). given clause #4: (wt=4) 13 [copy,12,unit_del,8] Killer(butler)|Killer(Charles). given clause #5: (wt=5) 16 [hyper,13,2] Killer(Charles)|Hates(butler,Agatha). given clause #6: (wt=6) 14 [] x=butler|Hates(Agatha,x). given clause #7: (wt=4) 19 [hyper,14,6] $f1(Agatha)=butler. given clause #8: (wt=3) 32 [para_into,19.1.1,19.1.1] butler=butler. given clause #9: (wt=3) 33 [para_from,19.1.1,6.1.2] -Hates(Agatha,butler). given clause #10: (wt=5) 17 [hyper,13,2] Killer(butler)|Hates(Charles,Agatha). given clause #11: (wt=6) 15 [] Richer(x,Agatha)|Hates(butler,x). given clause #12: (wt=5) 24 [para_from,14.1.1,13.2.1,factor_simp] Killer(butler)|Hates(Agatha,Charles). given clause #13: (wt=5) 27 [para_from,14.1.1,8.1.1] -Killer(butler)|Hates(Agatha,Agatha). given clause #14: (wt=5) 38 [hyper,15,3,13] Hates(butler,Charles)|Killer(butler). given clause #15: (wt=5) 39 [hyper,15,3,13] Hates(butler,butler)|Killer(Charles). given clause #16: (wt=6) 18 [hyper,16,2] Hates(butler,Agatha)|Hates(Charles,Agatha). given clause #17: (wt=3) 48 [hyper,18,4,14,unit_del,7] Hates(butler,Agatha). given clause #18: (wt=5) 45 [hyper,27,13] Hates(Agatha,Agatha)|Killer(Charles). given clause #19: (wt=6) 21 [hyper,14,5] x=butler|Hates(butler,x). given clause #20: (wt=4) 50 [hyper,21,6] $f1(butler)=butler. given clause #21: (wt=7) 22 [para_from,14.1.1,6.1.2] -Hates(x,butler)|Hates(Agatha,$f1(x)). given clause #22: (wt=3) 54 [para_from,50.1.1,6.1.2] -Hates(butler,butler). given clause #23: (wt=6) 36 [hyper,15,3,17] Hates(butler,butler)|Hates(Charles,Agatha). -----> EMPTY CLAUSE at 0.18 sec ----> 56 [hyper,36,4,14,unit_del,54,7] $F. Length of proof is 6. Level of proof is 3. ---------------- PROOF ---------------- 2 [] -Killer(x)|Hates(x,Agatha). 3 [] -Killer(x)| -Richer(x,Agatha). 4 [] -Hates(Agatha,x)| -Hates(Charles,x). 5 [] -Hates(Agatha,x)|Hates(butler,x). 6 [] -Hates(x,$f1(x)). 7 [] butler!=Agatha. 8 [] -Killer(Agatha). 12 [] Killer(Agatha)|Killer(butler)|Killer(Charles). 13 [copy,12,unit_del,8] Killer(butler)|Killer(Charles). 14 [] x=butler|Hates(Agatha,x). 15 [] Richer(x,Agatha)|Hates(butler,x). 17 [hyper,13,2] Killer(butler)|Hates(Charles,Agatha). 21 [hyper,14,5] x=butler|Hates(butler,x). 36 [hyper,15,3,17] Hates(butler,butler)|Hates(Charles,Agatha). 50 [hyper,21,6] $f1(butler)=butler. 54 [para_from,50.1.1,6.1.2] -Hates(butler,butler). 56 [hyper,36,4,14,unit_del,54,7] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 23 clauses generated 150 clauses kept 52 clauses forward subsumed 111 clauses back subsumed 7 Kbytes malloced 95 ----------- times (seconds) ----------- user CPU time 0.18 (0 hr, 0 min, 0 sec) system CPU time 0.18 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.03 para_into time 0.00 para_from time 0.02 for_sub time 0.00 back_sub time 0.01 conflict time 0.00 demod time 0.00 The job finished Tue Feb 10 12:18:46 1998