----- Otter 3.0.4, August 1995 ----- The job was started by brings on hopfield.phil.rpi.edu, Thu Apr 23 14:35:11 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_proofs,-1). formula_list(usable). all x (Job(x,nurse)|Job(x,teacher)). all x (Job(x,nurse)->Male(x)). all x ((Female(x)|Male(x))& -(Female(x)&Male(x))). Female(roberta). Male(steve). steve!=roberta. all x y (Job(x,teacher)&x!=y->Job(y,nurse)). all x y (Job(x,teacher)&x!=y-> -Job(y,teacher)). all x y (Job(x,nurse)&y!=x->Job(y,teacher)). all x y (Job(x,nurse)&y!=x-> -Job(y,nurse)). -Job(steve,nurse). end_of_list. -------> usable clausifies to: list(usable). 0 [] Job(x,nurse)|Job(x,teacher). 0 [] -Job(x,nurse)|Male(x). 0 [] Female(x)|Male(x). 0 [] -Female(x)| -Male(x). 0 [] Female(roberta). 0 [] Male(steve). 0 [] steve!=roberta. 0 [] -Job(x,teacher)|x=y|Job(y,nurse). 0 [] -Job(x,teacher)|x=y| -Job(y,teacher). 0 [] -Job(x,nurse)|y=x|Job(y,teacher). 0 [] -Job(x,nurse)|y=x| -Job(y,nurse). 0 [] -Job(steve,nurse). 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=5): 1 [] -Job(x,nurse)|Male(x). ** KEPT (pick-wt=4): 2 [] -Female(x)| -Male(x). ** KEPT (pick-wt=3): 3 [] steve!=roberta. ** KEPT (pick-wt=9): 4 [] -Job(x,teacher)|x=y|Job(y,nurse). ** KEPT (pick-wt=9): 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). ** KEPT (pick-wt=9): 6 [] -Job(x,nurse)|y=x|Job(y,teacher). ** KEPT (pick-wt=9): 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). ** KEPT (pick-wt=3): 8 [] -Job(steve,nurse). ------------> process sos: ** KEPT (pick-wt=6): 11 [] Job(x,nurse)|Job(x,teacher). ** KEPT (pick-wt=4): 12 [] Female(x)|Male(x). ** KEPT (pick-wt=2): 13 [] Female(roberta). ** KEPT (pick-wt=2): 14 [] Male(steve). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=6) 11 [] Job(x,nurse)|Job(x,teacher). given clause #2: (wt=2) 13 [] Female(roberta). given clause #3: (wt=2) 14 [] Male(steve). given clause #4: (wt=3) 16 [hyper,11,8] Job(steve,teacher). given clause #5: (wt=3) 45 [hyper,16,9] steve=steve. given clause #6: (wt=4) 12 [] Female(x)|Male(x). given clause #7: (wt=5) 18 [hyper,11,1] Job(x,teacher)|Male(x). given clause #8: (wt=3) 52 [hyper,18,2,13] Job(roberta,teacher). ----> UNIT CONFLICT at 0.15 sec ----> 60 [binary,58.1,3.1] $F. Length of proof is 4. Level of proof is 3. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 3 [] steve!=roberta. 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 52 [hyper,18,2,13] Job(roberta,teacher). 58 [hyper,52,5,16] steve=roberta. 60 [binary,58.1,3.1] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.18 sec ----> 70 [binary,69.1,57.1] $F. Length of proof is 7. Level of proof is 4. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 3 [] steve!=roberta. 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 8 [] -Job(steve,nurse). 9 [factor,5,1,3] -Job(x,teacher)|x=x. 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 52 [hyper,18,2,13] Job(roberta,teacher). 57 [hyper,52,9] roberta=roberta. 59,58 [hyper,52,5,16] steve=roberta. 69 [back_demod,3,demod,59] roberta!=roberta. 70 [binary,69.1,57.1] $F. ------------ end of proof ------------- given clause #9: (wt=2) 67 [back_demod,14,demod,59] Male(roberta). -----> EMPTY CLAUSE at 0.20 sec ----> 71 [hyper,67,2,13] $F. Length of proof is 5. Level of proof is 4. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 67 [back_demod,14,demod,59] Male(roberta). 71 [hyper,67,2,13] $F. ------------ end of proof ------------- given clause #10: (wt=3) 57 [hyper,52,9] roberta=roberta. given clause #11: (wt=6) 15 [hyper,11,10] Job(x,teacher)|x=x. ----> UNIT CONFLICT at 0.22 sec ----> 73 [binary,72.1,69.1] $F. Length of proof is 9. Level of proof is 4. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 3 [] steve!=roberta. 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 9 [factor,5,1,3] -Job(x,teacher)|x=x. 10 [factor,7,1,3] -Job(x,nurse)|x=x. 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 15 [hyper,11,10] Job(x,teacher)|x=x. 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 69 [back_demod,3,demod,59] roberta!=roberta. 72 [hyper,15,9,factor_simp] x=x. 73 [binary,72.1,69.1] $F. ------------ end of proof ------------- given clause #12: (wt=3) 58 [hyper,52,5,16] steve=roberta. given clause #13: (wt=3) 68 [back_demod,8,demod,59] -Job(roberta,nurse). given clause #14: (wt=3) 69 [back_demod,3,demod,59] roberta!=roberta. given clause #15: (wt=3) 72 [hyper,15,9,factor_simp] x=x. -----> EMPTY CLAUSE at 0.26 sec ----> 80 [hyper,72,69] $F. Length of proof is 9. Level of proof is 4. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 3 [] steve!=roberta. 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 9 [factor,5,1,3] -Job(x,teacher)|x=x. 10 [factor,7,1,3] -Job(x,nurse)|x=x. 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 15 [hyper,11,10] Job(x,teacher)|x=x. 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 69 [back_demod,3,demod,59] roberta!=roberta. 72 [hyper,15,9,factor_simp] x=x. 80 [hyper,72,69] $F. ------------ end of proof ------------- given clause #16: (wt=9) 17 [hyper,11,7,11] Job(x,teacher)|x=y|Job(y,teacher). given clause #17: (wt=5) 43 [para_into,14.1.1,5.2.1,unit_del,16] Male(x)| -Job(x,teacher). given clause #18: (wt=5) 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). ----> UNIT CONFLICT at 0.67 sec ----> 141 [binary,140.1,68.1] $F. Length of proof is 7. Level of proof is 4. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 141 [binary,140.1,68.1] $F. ------------ end of proof ------------- given clause #19: (wt=3) 140 [hyper,44,2,13] Job(roberta,nurse). -----> EMPTY CLAUSE at 0.71 sec ----> 147 [hyper,140,68] $F. Length of proof is 7. Level of proof is 4. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 147 [hyper,140,68] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.72 sec ----> 152 [binary,151.1,68.1] $F. Length of proof is 8. Level of proof is 4. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 152 [binary,151.1,68.1] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.73 sec ----> 155 [binary,154.1,68.1] $F. Length of proof is 9. Level of proof is 5. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 154 [para_into,140.1.2,7.2.1,unit_del,151,151] Job(roberta,x). 155 [binary,154.1,68.1] $F. ------------ end of proof ------------- given clause #20: (wt=3) 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). -----> EMPTY CLAUSE at 0.74 sec ----> 157 [hyper,151,68] $F. Length of proof is 8. Level of proof is 4. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 157 [hyper,151,68] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.74 sec ----> 159 [binary,158.1,69.1] $F. Length of proof is 9. Level of proof is 5. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 3 [] steve!=roberta. 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 69 [back_demod,3,demod,59] roberta!=roberta. 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 158 [hyper,151,7,151] x=y. 159 [binary,158.1,69.1] $F. ------------ end of proof ------------- given clause #21: (wt=12) 21 [para_into,11.1.2,7.2.1] Job(x,y)|Job(x,teacher)| -Job(y,nurse)| -Job(nurse,nurse). given clause #22: (wt=2) 160 [hyper,151,1] Male(x). -----> EMPTY CLAUSE at 0.75 sec ----> 162 [hyper,160,2,13] $F. Length of proof is 7. Level of proof is 5. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 160 [hyper,151,1] Male(x). 162 [hyper,160,2,13] $F. ------------ end of proof ------------- given clause #23: (wt=3) 154 [para_into,140.1.2,7.2.1,unit_del,151,151] Job(roberta,x). -----> EMPTY CLAUSE at 0.76 sec ----> 163 [hyper,154,68] $F. Length of proof is 9. Level of proof is 5. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 154 [para_into,140.1.2,7.2.1,unit_del,151,151] Job(roberta,x). 163 [hyper,154,68] $F. ------------ end of proof ------------- given clause #24: (wt=3) 158 [hyper,151,7,151] x=y. -----> EMPTY CLAUSE at 0.76 sec ----> 164 [hyper,158,69] $F. Length of proof is 9. Level of proof is 5. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 3 [] steve!=roberta. 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 69 [back_demod,3,demod,59] roberta!=roberta. 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 158 [hyper,151,7,151] x=y. 164 [hyper,158,69] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.77 sec ----> 166 [binary,165.1,68.1] $F. Length of proof is 11. Level of proof is 6. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 154 [para_into,140.1.2,7.2.1,unit_del,151,151] Job(roberta,x). 158 [hyper,151,7,151] x=y. 165 [para_from,158.1.1,154.1.1] Job(x,y). 166 [binary,165.1,68.1] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.78 sec ----> 168 [binary,167.1,165.1] $F. Length of proof is 12. Level of proof is 6. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 154 [para_into,140.1.2,7.2.1,unit_del,151,151] Job(roberta,x). 158 [hyper,151,7,151] x=y. 165 [para_from,158.1.1,154.1.1] Job(x,y). 167 [para_from,158.1.1,68.1.1] -Job(x,nurse). 168 [binary,167.1,165.1] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.78 sec ----> 169 [binary,167.1,154.1] $F. Length of proof is 11. Level of proof is 6. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 154 [para_into,140.1.2,7.2.1,unit_del,151,151] Job(roberta,x). 158 [hyper,151,7,151] x=y. 167 [para_from,158.1.1,68.1.1] -Job(x,nurse). 169 [binary,167.1,154.1] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.78 sec ----> 170 [binary,167.1,151.1] $F. Length of proof is 10. Level of proof is 6. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 158 [hyper,151,7,151] x=y. 167 [para_from,158.1.1,68.1.1] -Job(x,nurse). 170 [binary,167.1,151.1] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.78 sec ----> 173 [binary,172.1,165.1] $F. Length of proof is 12. Level of proof is 6. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 154 [para_into,140.1.2,7.2.1,unit_del,151,151] Job(roberta,x). 158 [hyper,151,7,151] x=y. 165 [para_from,158.1.1,154.1.1] Job(x,y). 172 [para_from,158.1.1,68.1.2] -Job(roberta,x). 173 [binary,172.1,165.1] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.79 sec ----> 174 [binary,172.1,161.1] $F. Length of proof is 12. Level of proof is 6. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 21 [para_into,11.1.2,7.2.1] Job(x,y)|Job(x,teacher)| -Job(y,nurse)| -Job(nurse,nurse). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 158 [hyper,151,7,151] x=y. 161 [hyper,21,151,151,factor_simp] Job(x,teacher). 172 [para_from,158.1.1,68.1.2] -Job(roberta,x). 174 [binary,172.1,161.1] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.79 sec ----> 175 [binary,172.1,154.1] $F. Length of proof is 11. Level of proof is 6. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 154 [para_into,140.1.2,7.2.1,unit_del,151,151] Job(roberta,x). 158 [hyper,151,7,151] x=y. 172 [para_from,158.1.1,68.1.2] -Job(roberta,x). 175 [binary,172.1,154.1] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.79 sec ----> 176 [binary,172.1,151.1] $F. Length of proof is 10. Level of proof is 6. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 158 [hyper,151,7,151] x=y. 172 [para_from,158.1.1,68.1.2] -Job(roberta,x). 176 [binary,172.1,151.1] $F. ------------ end of proof ------------- given clause #25: (wt=2) 171 [para_from,158.1.1,13.1.1] Female(x). -----> EMPTY CLAUSE at 0.79 sec ----> 177 [hyper,171,2,160] $F. Length of proof is 9. Level of proof is 6. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 158 [hyper,151,7,151] x=y. 160 [hyper,151,1] Male(x). 171 [para_from,158.1.1,13.1.1] Female(x). 177 [hyper,171,2,160] $F. ------------ end of proof ------------- given clause #26: (wt=3) 165 [para_from,158.1.1,154.1.1] Job(x,y). given clause #27: (wt=3) 167 [para_from,158.1.1,68.1.1] -Job(x,nurse). -----> EMPTY CLAUSE at 0.79 sec ----> 178 [hyper,167,165] $F. Length of proof is 12. Level of proof is 6. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 154 [para_into,140.1.2,7.2.1,unit_del,151,151] Job(roberta,x). 158 [hyper,151,7,151] x=y. 165 [para_from,158.1.1,154.1.1] Job(x,y). 167 [para_from,158.1.1,68.1.1] -Job(x,nurse). 178 [hyper,167,165] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.81 sec ----> 180 [binary,179.1,165.1] $F. Length of proof is 13. Level of proof is 7. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 154 [para_into,140.1.2,7.2.1,unit_del,151,151] Job(roberta,x). 158 [hyper,151,7,151] x=y. 165 [para_from,158.1.1,154.1.1] Job(x,y). 167 [para_from,158.1.1,68.1.1] -Job(x,nurse). 179 [para_into,167.1.2,158.1.1] -Job(x,y). 180 [binary,179.1,165.1] $F. ------------ end of proof ------------- given clause #28: (wt=3) 179 [para_into,167.1.2,158.1.1] -Job(x,y). -----> EMPTY CLAUSE at 0.82 sec ----> 181 [hyper,179,165] $F. Length of proof is 13. Level of proof is 7. ---------------- PROOF ---------------- 1 [] -Job(x,nurse)|Male(x). 2 [] -Female(x)| -Male(x). 4 [] -Job(x,teacher)|x=y|Job(y,nurse). 5 [] -Job(x,teacher)|x=y| -Job(y,teacher). 7 [] -Job(x,nurse)|y=x| -Job(y,nurse). 8 [] -Job(steve,nurse). 11 [] Job(x,nurse)|Job(x,teacher). 13 [] Female(roberta). 14 [] Male(steve). 16 [hyper,11,8] Job(steve,teacher). 18 [hyper,11,1] Job(x,teacher)|Male(x). 44 [para_into,14.1.1,4.2.1,unit_del,16] Male(x)|Job(x,nurse). 52 [hyper,18,2,13] Job(roberta,teacher). 59,58 [hyper,52,5,16] steve=roberta. 68 [back_demod,8,demod,59] -Job(roberta,nurse). 140 [hyper,44,2,13] Job(roberta,nurse). 151 [para_into,140.1.1,4.2.1,unit_del,52,factor_simp] Job(x,nurse). 154 [para_into,140.1.2,7.2.1,unit_del,151,151] Job(roberta,x). 158 [hyper,151,7,151] x=y. 165 [para_from,158.1.1,154.1.1] Job(x,y). 167 [para_from,158.1.1,68.1.1] -Job(x,nurse). 179 [para_into,167.1.2,158.1.1] -Job(x,y). 181 [hyper,179,165] $F. ------------ end of proof ------------- Search stopped because sos empty. ============ end of search ============ -------------- statistics ------------- clauses given 28 clauses generated 363 clauses kept 154 clauses forward subsumed 220 clauses back subsumed 136 Kbytes malloced 159 ----------- times (seconds) ----------- user CPU time 0.82 (0 hr, 0 min, 0 sec) system CPU time 0.37 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.02 para_into time 0.02 para_from time 0.00 for_sub time 0.18 back_sub time 0.05 conflict time 0.12 demod time 0.01 The job finished Thu Apr 23 14:35:12 1998