----- Otter 3.0.4, August 1995 ----- The job was started by brings on cortez.sss.rpi.edu, Mon Apr 27 00:06:49 1998 The command was "otter". set(ur_res). set(back_demod). dependent: set(dynamic_demod). dependent: set(order_eq). set(dynamic_demod_all). WARNING: assign(max_proofs,1) already has that value. assign(max_proofs,1). weight_list(pick_and_purge). weight(roberta,1). weight(thelma,2). weight(steve,3). weight(pete,4). end_of_list. list(usable). 1 [] Female(x)|Male(x). 2 [] -Female(x)| -Male(x). 3 [] -HasJob(x,nurse)|Male(x). 4 [] -HasJob(x,actor)|Male(x). 5 [] HasJob(x,job1(x)). 6 [] HasJob(x,job2(x)). 7 [] HasJob(jobholder(y),y). 8 [] -Husband(x,jobholder(chef))|HasJob(x,clerk). 9 [] -HasJob(x,clerk)|Husband(x,jobholder(chef)). 10 [] Female(jobholder(chef)). 11 [] -Husband(x,y)|Male(x). 12 [] -Husband(x,y)|Female(y). 13 [] -HasJob(x,nurse)|GreaterThan(ed-level(x),9). 14 [] -HasJob(x,policeofficer)|GreaterThan(ed-level(x),9). 15 [] -HasJob(x,teacher)|GreaterThan(ed-level(x),9). 16 [] -HasJob(x,chef)| -HasJob(x,policeofficer). 17 [] -Equalp(roberta,thelma). 18 [] -Equalp(roberta,steve). 19 [] -Equalp(roberta,pete). 20 [] -Equalp(thelma,steve). 21 [] -Equalp(thelma,pete). 22 [] -Equalp(pete,steve). 23 [] -Equalj(job1(x),job2(x)). 24 [] Equalp(x,x). 25 [] Equalj(x,x). 26 [] Equal(x,x). 27 [] Equalj(y,job2(x))|Equalj(y,job1(x)). 28 [] Equalp(x,x)| -HasJob(x,y)| -HasJob(z,y). 29 [] -Female(jobholder(y))|HasJob(roberta,y)|HasJob(thelma,y). 30 [] -Male(jobholder(y))|HasJob(steve,y)|HasJob(pete,y). 31 [] PossJobs(l(pj(roberta,chef),l(pj(roberta,guard),l(pj(roberta,nurse),l(pj(roberta,clerk),l(pj(roberta,policeofficer),l(pj(roberta,teacher),l(pj(roberta,actor),l(pj(roberta,boxer),end))))))))). 32 [] PossJobs(l(pj(thelma,chef),l(pj(thelma,guard),l(pj(thelma,nurse),l(pj(thelma,clerk),l(pj(thelma,policeofficer),l(pj(thelma,teacher),l(pj(thelma,actor),l(pj(thelma,boxer),end))))))))). 33 [] PossJobs(l(pj(steve,chef),l(pj(steve,guard),l(pj(steve,nurse),l(pj(steve,clerk),l(pj(steve,policeofficer),l(pj(steve,teacher),l(pj(steve,actor),l(pj(steve,boxer),end))))))))). 34 [] PossJobs(l(pj(pete,chef),l(pj(pete,guard),l(pj(pete,nurse),l(pj(pete,clerk),l(pj(pete,policeofficer),l(pj(pete,teacher),l(pj(pete,actor),l(pj(pete,boxer),end))))))))). 35 [] PossPeople(l(pj(roberta,chef),l(pj(steve,chef),l(pj(thelma,chef),l(pj(pete,chef),end))))). 36 [] PossPeople(l(pj(roberta,guard),l(pj(steve,guard),l(pj(thelma,guard),l(pj(pete,guard),end))))). 37 [] PossPeople(l(pj(roberta,nurse),l(pj(steve,nurse),l(pj(thelma,nurse),l(pj(pete,nurse),end))))). 38 [] PossPeople(l(pj(roberta,clerk),l(pj(steve,clerk),l(pj(thelma,clerk),l(pj(pete,clerk),end))))). 39 [] PossPeople(l(pj(roberta,policeofficer),l(pj(steve,policeofficer),l(pj(thelma,policeofficer),l(pj(pete,policeofficer),end))))). 40 [] PossPeople(l(pj(roberta,teacher),l(pj(steve,teacher),l(pj(thelma,teacher),l(pj(pete,teacher),end))))). 41 [] PossPeople(l(pj(roberta,actor),l(pj(steve,actor),l(pj(thelma,actor),l(pj(pete,actor),end))))). 42 [] PossPeople(l(pj(roberta,boxer),l(pj(steve,boxer),l(pj(thelma,boxer),l(pj(pete,boxer),end))))). 43 [] HasJob(x,y)|Equal(pj(x,y),crossed). 44 [] Equal(l(crossed,x),x). 45 [] -PossJobs(l(pj(x,y),l(pj(x,z),end)))|Equalp(x,w)|Equal(pj(w,y),crossed). 46 [] -PossJobs(l(pj(x,y),l(pj(x,z),end)))|HasJob(x,y). 47 [] -PossJobs(l(pj(x,y),l(pj(x,z),end)))|HasJob(x,z). 48 [] -PossPeople(l(pj(x,y),end))|HasJob(x,y). 49 [] StillDo(l(jobsof(roberta),l(jobsof(steve),l(jobsof(thelma),l(jobsof(pete),end))))). 50 [] -PossJobs(l(pj(x,y),l(pj(x,z),end)))|Equal(jobsof(x),crossed). 51 [] -StillDo(end). 52 [] -HasJob(x,y)|Equal(pj(x,y),j(x,y)). 53 [] Equal(l(pj(x,y),l(j(x,z),w)),l(j(x,z),l(pj(x,y),w))). 54 [] Equal(l(j(x,y),l(j(x,z),l(v,w))),l(j(x,y),l(j(x,z),end))). 55 [] -PossJobs(l(j(x,y),l(j(x,z),end)))|Equal(jobsof(x),crossed). 56 [] -PossJobs(l(j(x,y),l(pj(x,z),end)))|HasJob(x,z). end_of_list. list(sos). 57 [] Female(roberta). 58 [] Female(thelma). 59 [] Male(steve). 60 [] Male(pete). 61 [] -HasJob(roberta,boxer). 62 [] -GreaterThan(ed-level(pete),9). 63 [] -HasJob(roberta,chef). 64 [] -HasJob(roberta,policeofficer). end_of_list. list(demodulators). 65 [] Equal(l(crossed,x),x). end_of_list. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=2) 57 [] Female(roberta). ** KEPT (pick-wt=2): 66 [ur,57,2] -Male(roberta). given clause #2: (wt=2) 66 [ur,57,2] -Male(roberta). ** KEPT (pick-wt=3): 67 [ur,66,11] -Husband(roberta,x). ** KEPT (pick-wt=3): 68 [ur,66,4] -HasJob(roberta,actor). ** KEPT (pick-wt=3): 69 [ur,66,3] -HasJob(roberta,nurse). given clause #3: (wt=3) 58 [] Female(thelma). ** KEPT (pick-wt=3): 70 [ur,58,2] -Male(thelma). given clause #4: (wt=3) 61 [] -HasJob(roberta,boxer). ** KEPT (pick-wt=10): 71 [ur,61,56] -PossJobs(l(j(roberta,x),l(pj(roberta,boxer),end))). ** KEPT (pick-wt=6): 72 [ur,61,48] -PossPeople(l(pj(roberta,boxer),end)). ** KEPT (pick-wt=10): 73 [ur,61,47] -PossJobs(l(pj(roberta,x),l(pj(roberta,boxer),end))). ** KEPT (pick-wt=10): 74 [ur,61,46] -PossJobs(l(pj(roberta,boxer),l(pj(roberta,x),end))). ** KEPT (pick-wt=5): 75 [ur,61,43] Equal(pj(roberta,boxer),crossed). ---> New Demodulator: 76 [new_demod,75] Equal(pj(roberta,boxer),crossed). >>>> Starting back demodulation with 76. >> back demodulating 74 with 76. ** KEPT (pick-wt=6): 77 [back_demod,74,demod,76,65] -PossJobs(l(pj(roberta,x),end)). >> back demodulating 73 with 76. >> back demodulating 72 with 76. ** KEPT (pick-wt=2): 78 [back_demod,72,demod,76,65] -PossPeople(end). >> back demodulating 71 with 76. ** KEPT (pick-wt=6): 79 [back_demod,71,demod,76,65] -PossJobs(l(j(roberta,x),end)). >> back demodulating 42 with 76. ** KEPT (pick-wt=20): 80 [back_demod,42,demod,76,65] PossPeople(l(pj(steve,boxer),l(pj(thelma,boxer),l(pj(pete,boxer),end)))). >> back demodulating 31 with 76. ** KEPT (pick-wt=30): 81 [back_demod,31,demod,76,65] PossJobs(l(pj(roberta,chef),l(pj(roberta,guard),l(pj(roberta,nurse),l(pj(roberta,clerk),l(pj(roberta,policeofficer),l(pj(roberta,teacher),l(pj(roberta,actor),end)))))))). given clause #5: (wt=2) 78 [back_demod,72,demod,76,65] -PossPeople(end). given clause #6: (wt=3) 63 [] -HasJob(roberta,chef). ** KEPT (pick-wt=10): 82 [ur,63,56] -PossJobs(l(j(roberta,x),l(pj(roberta,chef),end))). ** KEPT (pick-wt=6): 83 [ur,63,48] -PossPeople(l(pj(roberta,chef),end)). ** KEPT (pick-wt=10): 84 [ur,63,47] -PossJobs(l(pj(roberta,x),l(pj(roberta,chef),end))). ** KEPT (pick-wt=10): 85 [ur,63,46] -PossJobs(l(pj(roberta,chef),l(pj(roberta,x),end))). ** KEPT (pick-wt=5): 86 [ur,63,43] Equal(pj(roberta,chef),crossed). ---> New Demodulator: 87 [new_demod,86] Equal(pj(roberta,chef),crossed). ** KEPT (pick-wt=4): 88 [ur,63,29,10] HasJob(thelma,chef). >>>> Starting back demodulation with 87. >> back demodulating 85 with 87. >> back demodulating 84 with 87. >> back demodulating 83 with 87. >> back demodulating 82 with 87. >> back demodulating 81 with 87. ** KEPT (pick-wt=26): 89 [back_demod,81,demod,87,65] PossJobs(l(pj(roberta,guard),l(pj(roberta,nurse),l(pj(roberta,clerk),l(pj(roberta,policeofficer),l(pj(roberta,teacher),l(pj(roberta,actor),end))))))). >> back demodulating 35 with 87. ** KEPT (pick-wt=20): 90 [back_demod,35,demod,87,65] PossPeople(l(pj(steve,chef),l(pj(thelma,chef),l(pj(pete,chef),end)))). given clause #7: (wt=3) 64 [] -HasJob(roberta,policeofficer). ** KEPT (pick-wt=10): 91 [ur,64,56] -PossJobs(l(j(roberta,x),l(pj(roberta,policeofficer),end))). ** KEPT (pick-wt=6): 92 [ur,64,48] -PossPeople(l(pj(roberta,policeofficer),end)). ** KEPT (pick-wt=10): 93 [ur,64,47] -PossJobs(l(pj(roberta,x),l(pj(roberta,policeofficer),end))). ** KEPT (pick-wt=10): 94 [ur,64,46] -PossJobs(l(pj(roberta,policeofficer),l(pj(roberta,x),end))). ** KEPT (pick-wt=5): 95 [ur,64,43] Equal(pj(roberta,policeofficer),crossed). ---> New Demodulator: 96 [new_demod,95] Equal(pj(roberta,policeofficer),crossed). >>>> Starting back demodulation with 96. >> back demodulating 94 with 96. >> back demodulating 93 with 96. >> back demodulating 92 with 96. >> back demodulating 91 with 96. >> back demodulating 89 with 96. ** KEPT (pick-wt=22): 97 [back_demod,89,demod,96,65] PossJobs(l(pj(roberta,guard),l(pj(roberta,nurse),l(pj(roberta,clerk),l(pj(roberta,teacher),l(pj(roberta,actor),end)))))). >> back demodulating 39 with 96. ** KEPT (pick-wt=20): 98 [back_demod,39,demod,96,65] PossPeople(l(pj(steve,policeofficer),l(pj(thelma,policeofficer),l(pj(pete,policeofficer),end)))). given clause #8: (wt=3) 67 [ur,66,11] -Husband(roberta,x). ** KEPT (pick-wt=3): 99 [ur,67,9] -HasJob(roberta,clerk). given clause #9: (wt=3) 68 [ur,66,4] -HasJob(roberta,actor). ** KEPT (pick-wt=10): 100 [ur,68,56] -PossJobs(l(j(roberta,x),l(pj(roberta,actor),end))). ** KEPT (pick-wt=6): 101 [ur,68,48] -PossPeople(l(pj(roberta,actor),end)). ** KEPT (pick-wt=10): 102 [ur,68,47] -PossJobs(l(pj(roberta,x),l(pj(roberta,actor),end))). ** KEPT (pick-wt=10): 103 [ur,68,46] -PossJobs(l(pj(roberta,actor),l(pj(roberta,x),end))). ** KEPT (pick-wt=5): 104 [ur,68,43] Equal(pj(roberta,actor),crossed). ---> New Demodulator: 105 [new_demod,104] Equal(pj(roberta,actor),crossed). >>>> Starting back demodulation with 105. >> back demodulating 103 with 105. >> back demodulating 102 with 105. >> back demodulating 101 with 105. >> back demodulating 100 with 105. >> back demodulating 97 with 105. ** KEPT (pick-wt=18): 106 [back_demod,97,demod,105,65] PossJobs(l(pj(roberta,guard),l(pj(roberta,nurse),l(pj(roberta,clerk),l(pj(roberta,teacher),end))))). >> back demodulating 41 with 105. ** KEPT (pick-wt=20): 107 [back_demod,41,demod,105,65] PossPeople(l(pj(steve,actor),l(pj(thelma,actor),l(pj(pete,actor),end)))). given clause #10: (wt=3) 69 [ur,66,3] -HasJob(roberta,nurse). ** KEPT (pick-wt=10): 108 [ur,69,56] -PossJobs(l(j(roberta,x),l(pj(roberta,nurse),end))). ** KEPT (pick-wt=6): 109 [ur,69,48] -PossPeople(l(pj(roberta,nurse),end)). ** KEPT (pick-wt=10): 110 [ur,69,47] -PossJobs(l(pj(roberta,x),l(pj(roberta,nurse),end))). ** KEPT (pick-wt=10): 111 [ur,69,46] -PossJobs(l(pj(roberta,nurse),l(pj(roberta,x),end))). ** KEPT (pick-wt=5): 112 [ur,69,43] Equal(pj(roberta,nurse),crossed). ---> New Demodulator: 113 [new_demod,112] Equal(pj(roberta,nurse),crossed). >>>> Starting back demodulation with 113. >> back demodulating 111 with 113. >> back demodulating 110 with 113. >> back demodulating 109 with 113. >> back demodulating 108 with 113. >> back demodulating 106 with 113. ** KEPT (pick-wt=14): 114 [back_demod,106,demod,113,65] PossJobs(l(pj(roberta,guard),l(pj(roberta,clerk),l(pj(roberta,teacher),end)))). >> back demodulating 37 with 113. ** KEPT (pick-wt=20): 115 [back_demod,37,demod,113,65] PossPeople(l(pj(steve,nurse),l(pj(thelma,nurse),l(pj(pete,nurse),end)))). given clause #11: (wt=3) 70 [ur,58,2] -Male(thelma). ** KEPT (pick-wt=4): 116 [ur,70,11] -Husband(thelma,x). ** KEPT (pick-wt=4): 117 [ur,70,4] -HasJob(thelma,actor). ** KEPT (pick-wt=4): 118 [ur,70,3] -HasJob(thelma,nurse). given clause #12: (wt=3) 99 [ur,67,9] -HasJob(roberta,clerk). ** KEPT (pick-wt=10): 119 [ur,99,56] -PossJobs(l(j(roberta,x),l(pj(roberta,clerk),end))). ** KEPT (pick-wt=6): 120 [ur,99,48] -PossPeople(l(pj(roberta,clerk),end)). ** KEPT (pick-wt=10): 121 [ur,99,47] -PossJobs(l(pj(roberta,x),l(pj(roberta,clerk),end))). ** KEPT (pick-wt=10): 122 [ur,99,46] -PossJobs(l(pj(roberta,clerk),l(pj(roberta,x),end))). ** KEPT (pick-wt=5): 123 [ur,99,43] Equal(pj(roberta,clerk),crossed). ---> New Demodulator: 124 [new_demod,123] Equal(pj(roberta,clerk),crossed). >>>> Starting back demodulation with 124. >> back demodulating 122 with 124. >> back demodulating 121 with 124. >> back demodulating 120 with 124. >> back demodulating 119 with 124. >> back demodulating 114 with 124. ** KEPT (pick-wt=10): 125 [back_demod,114,demod,124,65] PossJobs(l(pj(roberta,guard),l(pj(roberta,teacher),end))). >> back demodulating 38 with 124. ** KEPT (pick-wt=20): 126 [back_demod,38,demod,124,65] PossPeople(l(pj(steve,clerk),l(pj(thelma,clerk),l(pj(pete,clerk),end)))). given clause #13: (wt=4) 59 [] Male(steve). ** KEPT (pick-wt=4): 127 [ur,59,2] -Female(steve). given clause #14: (wt=4) 88 [ur,63,29,10] HasJob(thelma,chef). ** KEPT (pick-wt=9): 128 [ur,88,52] Equal(pj(thelma,chef),j(thelma,chef)). ---> New Demodulator: 129 [new_demod,128] Equal(pj(thelma,chef),j(thelma,chef)). ** KEPT (pick-wt=4): 130 [ur,88,16] -HasJob(thelma,policeofficer). >>>> Starting back demodulation with 129. >> back demodulating 90 with 129. ** KEPT (pick-wt=20): 131 [back_demod,90,demod,129] PossPeople(l(pj(steve,chef),l(j(thelma,chef),l(pj(pete,chef),end)))). >> back demodulating 32 with 129. ** KEPT (pick-wt=42): 132 [back_demod,32,demod,129] PossJobs(l(j(thelma,chef),l(pj(thelma,guard),l(pj(thelma,nurse),l(pj(thelma,clerk),l(pj(thelma,policeofficer),l(pj(thelma,teacher),l(pj(thelma,actor),l(pj(thelma,boxer),end))))))))). given clause #15: (wt=4) 116 [ur,70,11] -Husband(thelma,x). ** KEPT (pick-wt=4): 133 [ur,116,9] -HasJob(thelma,clerk). given clause #16: (wt=4) 117 [ur,70,4] -HasJob(thelma,actor). ** KEPT (pick-wt=12): 134 [ur,117,56] -PossJobs(l(j(thelma,x),l(pj(thelma,actor),end))). ** KEPT (pick-wt=7): 135 [ur,117,48] -PossPeople(l(pj(thelma,actor),end)). ** KEPT (pick-wt=12): 136 [ur,117,47] -PossJobs(l(pj(thelma,x),l(pj(thelma,actor),end))). ** KEPT (pick-wt=12): 137 [ur,117,46] -PossJobs(l(pj(thelma,actor),l(pj(thelma,x),end))). ** KEPT (pick-wt=6): 138 [ur,117,43] Equal(pj(thelma,actor),crossed). ---> New Demodulator: 139 [new_demod,138] Equal(pj(thelma,actor),crossed). ** KEPT (pick-wt=3): 140 [ur,117,29,68] -Female(jobholder(actor)). >>>> Starting back demodulation with 139. >> back demodulating 137 with 139. ** KEPT (pick-wt=7): 141 [back_demod,137,demod,139,65] -PossJobs(l(pj(thelma,x),end)). >> back demodulating 136 with 139. >> back demodulating 135 with 139. >> back demodulating 134 with 139. ** KEPT (pick-wt=7): 142 [back_demod,134,demod,139,65] -PossJobs(l(j(thelma,x),end)). >> back demodulating 132 with 139. ** KEPT (pick-wt=37): 143 [back_demod,132,demod,139,65] PossJobs(l(j(thelma,chef),l(pj(thelma,guard),l(pj(thelma,nurse),l(pj(thelma,clerk),l(pj(thelma,policeofficer),l(pj(thelma,teacher),l(pj(thelma,boxer),end)))))))). >> back demodulating 107 with 139. ** KEPT (pick-wt=15): 144 [back_demod,107,demod,139,65] PossPeople(l(pj(steve,actor),l(pj(pete,actor),end))). given clause #17: (wt=3) 140 [ur,117,29,68] -Female(jobholder(actor)). ** KEPT (pick-wt=4): 145 [ur,140,12] -Husband(x,jobholder(actor)). ** KEPT (pick-wt=3): 146 [ur,140,1] Male(jobholder(actor)). given clause #18: (wt=3) 146 [ur,140,1] Male(jobholder(actor)). given clause #19: (wt=4) 118 [ur,70,3] -HasJob(thelma,nurse). ** KEPT (pick-wt=12): 147 [ur,118,56] -PossJobs(l(j(thelma,x),l(pj(thelma,nurse),end))). ** KEPT (pick-wt=7): 148 [ur,118,48] -PossPeople(l(pj(thelma,nurse),end)). ** KEPT (pick-wt=12): 149 [ur,118,47] -PossJobs(l(pj(thelma,x),l(pj(thelma,nurse),end))). ** KEPT (pick-wt=12): 150 [ur,118,46] -PossJobs(l(pj(thelma,nurse),l(pj(thelma,x),end))). ** KEPT (pick-wt=6): 151 [ur,118,43] Equal(pj(thelma,nurse),crossed). ---> New Demodulator: 152 [new_demod,151] Equal(pj(thelma,nurse),crossed). ** KEPT (pick-wt=3): 153 [ur,118,29,69] -Female(jobholder(nurse)). >>>> Starting back demodulation with 152. >> back demodulating 150 with 152. >> back demodulating 149 with 152. >> back demodulating 148 with 152. >> back demodulating 147 with 152. >> back demodulating 143 with 152. ** KEPT (pick-wt=32): 154 [back_demod,143,demod,152,65] PossJobs(l(j(thelma,chef),l(pj(thelma,guard),l(pj(thelma,clerk),l(pj(thelma,policeofficer),l(pj(thelma,teacher),l(pj(thelma,boxer),end))))))). >> back demodulating 115 with 152. ** KEPT (pick-wt=15): 155 [back_demod,115,demod,152,65] PossPeople(l(pj(steve,nurse),l(pj(pete,nurse),end))). given clause #20: (wt=3) 153 [ur,118,29,69] -Female(jobholder(nurse)). ** KEPT (pick-wt=4): 156 [ur,153,12] -Husband(x,jobholder(nurse)). ** KEPT (pick-wt=3): 157 [ur,153,1] Male(jobholder(nurse)). given clause #21: (wt=3) 157 [ur,153,1] Male(jobholder(nurse)). given clause #22: (wt=4) 127 [ur,59,2] -Female(steve). ** KEPT (pick-wt=5): 158 [ur,127,12] -Husband(x,steve). given clause #23: (wt=4) 130 [ur,88,16] -HasJob(thelma,policeofficer). ** KEPT (pick-wt=12): 159 [ur,130,56] -PossJobs(l(j(thelma,x),l(pj(thelma,policeofficer),end))). ** KEPT (pick-wt=7): 160 [ur,130,48] -PossPeople(l(pj(thelma,policeofficer),end)). ** KEPT (pick-wt=12): 161 [ur,130,47] -PossJobs(l(pj(thelma,x),l(pj(thelma,policeofficer),end))). ** KEPT (pick-wt=12): 162 [ur,130,46] -PossJobs(l(pj(thelma,policeofficer),l(pj(thelma,x),end))). ** KEPT (pick-wt=6): 163 [ur,130,43] Equal(pj(thelma,policeofficer),crossed). ---> New Demodulator: 164 [new_demod,163] Equal(pj(thelma,policeofficer),crossed). ** KEPT (pick-wt=3): 165 [ur,130,29,64] -Female(jobholder(policeofficer)). >>>> Starting back demodulation with 164. >> back demodulating 162 with 164. >> back demodulating 161 with 164. >> back demodulating 160 with 164. >> back demodulating 159 with 164. >> back demodulating 154 with 164. ** KEPT (pick-wt=27): 166 [back_demod,154,demod,164,65] PossJobs(l(j(thelma,chef),l(pj(thelma,guard),l(pj(thelma,clerk),l(pj(thelma,teacher),l(pj(thelma,boxer),end)))))). >> back demodulating 98 with 164. ** KEPT (pick-wt=15): 167 [back_demod,98,demod,164,65] PossPeople(l(pj(steve,policeofficer),l(pj(pete,policeofficer),end))). given clause #24: (wt=3) 165 [ur,130,29,64] -Female(jobholder(policeofficer)). ** KEPT (pick-wt=4): 168 [ur,165,12] -Husband(x,jobholder(policeofficer)). ** KEPT (pick-wt=3): 169 [ur,165,1] Male(jobholder(policeofficer)). given clause #25: (wt=3) 169 [ur,165,1] Male(jobholder(policeofficer)). given clause #26: (wt=4) 133 [ur,116,9] -HasJob(thelma,clerk). ** KEPT (pick-wt=12): 170 [ur,133,56] -PossJobs(l(j(thelma,x),l(pj(thelma,clerk),end))). ** KEPT (pick-wt=7): 171 [ur,133,48] -PossPeople(l(pj(thelma,clerk),end)). ** KEPT (pick-wt=12): 172 [ur,133,47] -PossJobs(l(pj(thelma,x),l(pj(thelma,clerk),end))). ** KEPT (pick-wt=12): 173 [ur,133,46] -PossJobs(l(pj(thelma,clerk),l(pj(thelma,x),end))). ** KEPT (pick-wt=6): 174 [ur,133,43] Equal(pj(thelma,clerk),crossed). ---> New Demodulator: 175 [new_demod,174] Equal(pj(thelma,clerk),crossed). ** KEPT (pick-wt=3): 176 [ur,133,29,99] -Female(jobholder(clerk)). >>>> Starting back demodulation with 175. >> back demodulating 173 with 175. >> back demodulating 172 with 175. >> back demodulating 171 with 175. >> back demodulating 170 with 175. >> back demodulating 166 with 175. ** KEPT (pick-wt=22): 177 [back_demod,166,demod,175,65] PossJobs(l(j(thelma,chef),l(pj(thelma,guard),l(pj(thelma,teacher),l(pj(thelma,boxer),end))))). >> back demodulating 126 with 175. ** KEPT (pick-wt=15): 178 [back_demod,126,demod,175,65] PossPeople(l(pj(steve,clerk),l(pj(pete,clerk),end))). given clause #27: (wt=3) 176 [ur,133,29,99] -Female(jobholder(clerk)). ** KEPT (pick-wt=4): 179 [ur,176,12] -Husband(x,jobholder(clerk)). ** KEPT (pick-wt=3): 180 [ur,176,1] Male(jobholder(clerk)). given clause #28: (wt=3) 180 [ur,176,1] Male(jobholder(clerk)). given clause #29: (wt=4) 145 [ur,140,12] -Husband(x,jobholder(actor)). given clause #30: (wt=4) 156 [ur,153,12] -Husband(x,jobholder(nurse)). given clause #31: (wt=4) 168 [ur,165,12] -Husband(x,jobholder(policeofficer)). given clause #32: (wt=4) 179 [ur,176,12] -Husband(x,jobholder(clerk)). given clause #33: (wt=5) 60 [] Male(pete). ** KEPT (pick-wt=5): 181 [ur,60,2] -Female(pete). given clause #34: (wt=5) 75 [ur,61,43] Equal(pj(roberta,boxer),crossed). given clause #35: (wt=5) 86 [ur,63,43] Equal(pj(roberta,chef),crossed). given clause #36: (wt=5) 95 [ur,64,43] Equal(pj(roberta,policeofficer),crossed). given clause #37: (wt=5) 104 [ur,68,43] Equal(pj(roberta,actor),crossed). given clause #38: (wt=5) 112 [ur,69,43] Equal(pj(roberta,nurse),crossed). given clause #39: (wt=5) 123 [ur,99,43] Equal(pj(roberta,clerk),crossed). given clause #40: (wt=5) 158 [ur,127,12] -Husband(x,steve). given clause #41: (wt=5) 181 [ur,60,2] -Female(pete). ** KEPT (pick-wt=6): 182 [ur,181,12] -Husband(x,pete). given clause #42: (wt=6) 77 [back_demod,74,demod,76,65] -PossJobs(l(pj(roberta,x),end)). given clause #43: (wt=6) 79 [back_demod,71,demod,76,65] -PossJobs(l(j(roberta,x),end)). given clause #44: (wt=6) 138 [ur,117,43] Equal(pj(thelma,actor),crossed). given clause #45: (wt=6) 151 [ur,118,43] Equal(pj(thelma,nurse),crossed). given clause #46: (wt=6) 163 [ur,130,43] Equal(pj(thelma,policeofficer),crossed). given clause #47: (wt=6) 174 [ur,133,43] Equal(pj(thelma,clerk),crossed). given clause #48: (wt=6) 182 [ur,181,12] -Husband(x,pete). given clause #49: (wt=7) 141 [back_demod,137,demod,139,65] -PossJobs(l(pj(thelma,x),end)). given clause #50: (wt=7) 142 [back_demod,134,demod,139,65] -PossJobs(l(j(thelma,x),end)). given clause #51: (wt=9) 62 [] -GreaterThan(ed-level(pete),9). ** KEPT (pick-wt=6): 183 [ur,62,15] -HasJob(pete,teacher). ** KEPT (pick-wt=6): 184 [ur,62,14] -HasJob(pete,policeofficer). ** KEPT (pick-wt=6): 185 [ur,62,13] -HasJob(pete,nurse). given clause #52: (wt=6) 183 [ur,62,15] -HasJob(pete,teacher). ** KEPT (pick-wt=16): 186 [ur,183,56] -PossJobs(l(j(pete,x),l(pj(pete,teacher),end))). ** KEPT (pick-wt=9): 187 [ur,183,48] -PossPeople(l(pj(pete,teacher),end)). ** KEPT (pick-wt=16): 188 [ur,183,47] -PossJobs(l(pj(pete,x),l(pj(pete,teacher),end))). ** KEPT (pick-wt=16): 189 [ur,183,46] -PossJobs(l(pj(pete,teacher),l(pj(pete,x),end))). ** KEPT (pick-wt=8): 190 [ur,183,43] Equal(pj(pete,teacher),crossed). ---> New Demodulator: 191 [new_demod,190] Equal(pj(pete,teacher),crossed). >>>> Starting back demodulation with 191. >> back demodulating 189 with 191. ** KEPT (pick-wt=9): 192 [back_demod,189,demod,191,65] -PossJobs(l(pj(pete,x),end)). >> back demodulating 188 with 191. >> back demodulating 187 with 191. >> back demodulating 186 with 191. ** KEPT (pick-wt=9): 193 [back_demod,186,demod,191,65] -PossJobs(l(j(pete,x),end)). >> back demodulating 40 with 191. ** KEPT (pick-wt=17): 194 [back_demod,40,demod,191,65] PossPeople(l(pj(roberta,teacher),l(pj(steve,teacher),l(pj(thelma,teacher),end)))). >> back demodulating 34 with 191. ** KEPT (pick-wt=51): 195 [back_demod,34,demod,191,65] PossJobs(l(pj(pete,chef),l(pj(pete,guard),l(pj(pete,nurse),l(pj(pete,clerk),l(pj(pete,policeofficer),l(pj(pete,actor),l(pj(pete,boxer),end)))))))). given clause #53: (wt=6) 184 [ur,62,14] -HasJob(pete,policeofficer). ** KEPT (pick-wt=16): 196 [ur,184,56] -PossJobs(l(j(pete,x),l(pj(pete,policeofficer),end))). ** KEPT (pick-wt=9): 197 [ur,184,48] -PossPeople(l(pj(pete,policeofficer),end)). ** KEPT (pick-wt=16): 198 [ur,184,47] -PossJobs(l(pj(pete,x),l(pj(pete,policeofficer),end))). ** KEPT (pick-wt=16): 199 [ur,184,46] -PossJobs(l(pj(pete,policeofficer),l(pj(pete,x),end))). ** KEPT (pick-wt=8): 200 [ur,184,43] Equal(pj(pete,policeofficer),crossed). ---> New Demodulator: 201 [new_demod,200] Equal(pj(pete,policeofficer),crossed). ** KEPT (pick-wt=5): 202 [ur,184,30,169] HasJob(steve,policeofficer). >>>> Starting back demodulation with 201. >> back demodulating 199 with 201. >> back demodulating 198 with 201. >> back demodulating 197 with 201. >> back demodulating 196 with 201. >> back demodulating 195 with 201. ** KEPT (pick-wt=44): 203 [back_demod,195,demod,201,65] PossJobs(l(pj(pete,chef),l(pj(pete,guard),l(pj(pete,nurse),l(pj(pete,clerk),l(pj(pete,actor),l(pj(pete,boxer),end))))))). >> back demodulating 167 with 201. ** KEPT (pick-wt=8): 204 [back_demod,167,demod,201,65] PossPeople(l(pj(steve,policeofficer),end)). given clause #54: (wt=5) 202 [ur,184,30,169] HasJob(steve,policeofficer). ** KEPT (pick-wt=11): 205 [ur,202,52] Equal(pj(steve,policeofficer),j(steve,policeofficer)). ---> New Demodulator: 206 [new_demod,205] Equal(pj(steve,policeofficer),j(steve,policeofficer)). ** KEPT (pick-wt=5): 207 [ur,202,16] -HasJob(steve,chef). ** KEPT (pick-wt=8): 208 [ur,202,14] GreaterThan(ed-level(steve),9). >>>> Starting back demodulation with 206. >> back demodulating 204 with 206. ** KEPT (pick-wt=8): 209 [back_demod,204,demod,206] PossPeople(l(j(steve,policeofficer),end)). >> back demodulating 33 with 206. ** KEPT (pick-wt=50): 210 [back_demod,33,demod,206] PossJobs(l(pj(steve,chef),l(pj(steve,guard),l(pj(steve,nurse),l(pj(steve,clerk),l(j(steve,policeofficer),l(pj(steve,teacher),l(pj(steve,actor),l(pj(steve,boxer),end))))))))). given clause #55: (wt=5) 207 [ur,202,16] -HasJob(steve,chef). ** KEPT (pick-wt=14): 211 [ur,207,56] -PossJobs(l(j(steve,x),l(pj(steve,chef),end))). ** KEPT (pick-wt=8): 212 [ur,207,48] -PossPeople(l(pj(steve,chef),end)). ** KEPT (pick-wt=14): 213 [ur,207,47] -PossJobs(l(pj(steve,x),l(pj(steve,chef),end))). ** KEPT (pick-wt=14): 214 [ur,207,46] -PossJobs(l(pj(steve,chef),l(pj(steve,x),end))). ** KEPT (pick-wt=7): 215 [ur,207,43] Equal(pj(steve,chef),crossed). ---> New Demodulator: 216 [new_demod,215] Equal(pj(steve,chef),crossed). >>>> Starting back demodulation with 216. >> back demodulating 214 with 216. ** KEPT (pick-wt=8): 217 [back_demod,214,demod,216,65] -PossJobs(l(pj(steve,x),end)). >> back demodulating 213 with 216. >> back demodulating 212 with 216. >> back demodulating 211 with 216. ** KEPT (pick-wt=8): 218 [back_demod,211,demod,216,65] -PossJobs(l(j(steve,x),end)). >> back demodulating 210 with 216. ** KEPT (pick-wt=44): 219 [back_demod,210,demod,216,65] PossJobs(l(pj(steve,guard),l(pj(steve,nurse),l(pj(steve,clerk),l(j(steve,policeofficer),l(pj(steve,teacher),l(pj(steve,actor),l(pj(steve,boxer),end)))))))). >> back demodulating 131 with 216. ** KEPT (pick-wt=14): 220 [back_demod,131,demod,216,65] PossPeople(l(j(thelma,chef),l(pj(pete,chef),end))). given clause #56: (wt=6) 185 [ur,62,13] -HasJob(pete,nurse). ** KEPT (pick-wt=16): 221 [ur,185,56] -PossJobs(l(j(pete,x),l(pj(pete,nurse),end))). ** KEPT (pick-wt=9): 222 [ur,185,48] -PossPeople(l(pj(pete,nurse),end)). ** KEPT (pick-wt=16): 223 [ur,185,47] -PossJobs(l(pj(pete,x),l(pj(pete,nurse),end))). ** KEPT (pick-wt=16): 224 [ur,185,46] -PossJobs(l(pj(pete,nurse),l(pj(pete,x),end))). ** KEPT (pick-wt=8): 225 [ur,185,43] Equal(pj(pete,nurse),crossed). ---> New Demodulator: 226 [new_demod,225] Equal(pj(pete,nurse),crossed). ** KEPT (pick-wt=5): 227 [ur,185,30,157] HasJob(steve,nurse). >>>> Starting back demodulation with 226. >> back demodulating 224 with 226. >> back demodulating 223 with 226. >> back demodulating 222 with 226. >> back demodulating 221 with 226. >> back demodulating 203 with 226. ** KEPT (pick-wt=37): 228 [back_demod,203,demod,226,65] PossJobs(l(pj(pete,chef),l(pj(pete,guard),l(pj(pete,clerk),l(pj(pete,actor),l(pj(pete,boxer),end)))))). >> back demodulating 155 with 226. ** KEPT (pick-wt=8): 229 [back_demod,155,demod,226,65] PossPeople(l(pj(steve,nurse),end)). given clause #57: (wt=5) 227 [ur,185,30,157] HasJob(steve,nurse). ** KEPT (pick-wt=11): 230 [ur,227,52] Equal(pj(steve,nurse),j(steve,nurse)). ---> New Demodulator: 231 [new_demod,230] Equal(pj(steve,nurse),j(steve,nurse)). >>>> Starting back demodulation with 231. >> back demodulating 229 with 231. ** KEPT (pick-wt=8): 232 [back_demod,229,demod,231] PossPeople(l(j(steve,nurse),end)). >> back demodulating 219 with 231. ** KEPT (pick-wt=44): 233 [back_demod,219,demod,231] PossJobs(l(pj(steve,guard),l(j(steve,nurse),l(pj(steve,clerk),l(j(steve,policeofficer),l(pj(steve,teacher),l(pj(steve,actor),l(pj(steve,boxer),end)))))))). given clause #58: (wt=7) 215 [ur,207,43] Equal(pj(steve,chef),crossed). given clause #59: (wt=8) 190 [ur,183,43] Equal(pj(pete,teacher),crossed). given clause #60: (wt=8) 200 [ur,184,43] Equal(pj(pete,policeofficer),crossed). given clause #61: (wt=8) 208 [ur,202,14] GreaterThan(ed-level(steve),9). given clause #62: (wt=8) 209 [back_demod,204,demod,206] PossPeople(l(j(steve,policeofficer),end)). given clause #63: (wt=8) 217 [back_demod,214,demod,216,65] -PossJobs(l(pj(steve,x),end)). given clause #64: (wt=8) 218 [back_demod,211,demod,216,65] -PossJobs(l(j(steve,x),end)). given clause #65: (wt=8) 225 [ur,185,43] Equal(pj(pete,nurse),crossed). given clause #66: (wt=8) 232 [back_demod,229,demod,231] PossPeople(l(j(steve,nurse),end)). given clause #67: (wt=9) 128 [ur,88,52] Equal(pj(thelma,chef),j(thelma,chef)). given clause #68: (wt=9) 192 [back_demod,189,demod,191,65] -PossJobs(l(pj(pete,x),end)). given clause #69: (wt=9) 193 [back_demod,186,demod,191,65] -PossJobs(l(j(pete,x),end)). given clause #70: (wt=10) 125 [back_demod,114,demod,124,65] PossJobs(l(pj(roberta,guard),l(pj(roberta,teacher),end))). ** KEPT (pick-wt=4): 234 [ur,125,50] Equal(jobsof(roberta),crossed). ---> New Demodulator: 235 [new_demod,234] Equal(jobsof(roberta),crossed). ** KEPT (pick-wt=3): 236 [ur,125,47] HasJob(roberta,teacher). ** KEPT (pick-wt=3): 237 [ur,125,46] HasJob(roberta,guard). ** KEPT (pick-wt=8): 238 [ur,125,45,19] Equal(pj(pete,guard),crossed). ---> New Demodulator: 239 [new_demod,238] Equal(pj(pete,guard),crossed). ** KEPT (pick-wt=7): 240 [ur,125,45,18] Equal(pj(steve,guard),crossed). ---> New Demodulator: 241 [new_demod,240] Equal(pj(steve,guard),crossed). ** KEPT (pick-wt=6): 242 [ur,125,45,17] Equal(pj(thelma,guard),crossed). ---> New Demodulator: 243 [new_demod,242] Equal(pj(thelma,guard),crossed). >>>> Starting back demodulation with 235. >> back demodulating 49 with 235. ** KEPT (pick-wt=17): 244 [back_demod,49,demod,235,65] StillDo(l(jobsof(steve),l(jobsof(thelma),l(jobsof(pete),end)))). >>>> Starting back demodulation with 239. >> back demodulating 228 with 239. ** KEPT (pick-wt=30): 245 [back_demod,228,demod,239,65] PossJobs(l(pj(pete,chef),l(pj(pete,clerk),l(pj(pete,actor),l(pj(pete,boxer),end))))). >> back demodulating 36 with 239. ** KEPT (pick-wt=6): 246 [back_demod,36,demod,241,243,239,65,65,65] PossPeople(l(pj(roberta,guard),end)). >>>> Starting back demodulation with 241. >> back demodulating 233 with 241. ** KEPT (pick-wt=38): 247 [back_demod,233,demod,241,65] PossJobs(l(j(steve,nurse),l(pj(steve,clerk),l(j(steve,policeofficer),l(pj(steve,teacher),l(pj(steve,actor),l(pj(steve,boxer),end))))))). >>>> Starting back demodulation with 243. >> back demodulating 177 with 243. ** KEPT (pick-wt=17): 248 [back_demod,177,demod,243,65] PossJobs(l(j(thelma,chef),l(pj(thelma,teacher),l(pj(thelma,boxer),end)))). given clause #71: (wt=3) 236 [ur,125,47] HasJob(roberta,teacher). ** KEPT (pick-wt=7): 249 [ur,236,52] Equal(pj(roberta,teacher),j(roberta,teacher)). ---> New Demodulator: 250 [new_demod,249] Equal(pj(roberta,teacher),j(roberta,teacher)). ** KEPT (pick-wt=6): 251 [ur,236,15] GreaterThan(ed-level(roberta),9). >>>> Starting back demodulation with 250. >> back demodulating 194 with 250. ** KEPT (pick-wt=17): 252 [back_demod,194,demod,250] PossPeople(l(j(roberta,teacher),l(pj(steve,teacher),l(pj(thelma,teacher),end)))). >> back demodulating 125 with 250. ** KEPT (pick-wt=10): 253 [back_demod,125,demod,250] PossJobs(l(pj(roberta,guard),l(j(roberta,teacher),end))). given clause #72: (wt=3) 237 [ur,125,46] HasJob(roberta,guard). ** KEPT (pick-wt=7): 254 [ur,237,52] Equal(pj(roberta,guard),j(roberta,guard)). ---> New Demodulator: 255 [new_demod,254] Equal(pj(roberta,guard),j(roberta,guard)). >>>> Starting back demodulation with 255. >> back demodulating 253 with 255. ** KEPT (pick-wt=10): 256 [back_demod,253,demod,255] PossJobs(l(j(roberta,guard),l(j(roberta,teacher),end))). >> back demodulating 246 with 255. ** KEPT (pick-wt=6): 257 [back_demod,246,demod,255] PossPeople(l(j(roberta,guard),end)). given clause #73: (wt=4) 234 [ur,125,50] Equal(jobsof(roberta),crossed). given clause #74: (wt=6) 242 [ur,125,45,17] Equal(pj(thelma,guard),crossed). given clause #75: (wt=6) 251 [ur,236,15] GreaterThan(ed-level(roberta),9). given clause #76: (wt=6) 257 [back_demod,246,demod,255] PossPeople(l(j(roberta,guard),end)). given clause #77: (wt=7) 240 [ur,125,45,18] Equal(pj(steve,guard),crossed). given clause #78: (wt=7) 249 [ur,236,52] Equal(pj(roberta,teacher),j(roberta,teacher)). given clause #79: (wt=7) 254 [ur,237,52] Equal(pj(roberta,guard),j(roberta,guard)). given clause #80: (wt=8) 238 [ur,125,45,19] Equal(pj(pete,guard),crossed). given clause #81: (wt=10) 256 [back_demod,253,demod,255] PossJobs(l(j(roberta,guard),l(j(roberta,teacher),end))). given clause #82: (wt=11) 205 [ur,202,52] Equal(pj(steve,policeofficer),j(steve,policeofficer)). given clause #83: (wt=11) 230 [ur,227,52] Equal(pj(steve,nurse),j(steve,nurse)). given clause #84: (wt=14) 220 [back_demod,131,demod,216,65] PossPeople(l(j(thelma,chef),l(pj(pete,chef),end))). given clause #85: (wt=15) 144 [back_demod,107,demod,139,65] PossPeople(l(pj(steve,actor),l(pj(pete,actor),end))). given clause #86: (wt=15) 178 [back_demod,126,demod,175,65] PossPeople(l(pj(steve,clerk),l(pj(pete,clerk),end))). given clause #87: (wt=17) 244 [back_demod,49,demod,235,65] StillDo(l(jobsof(steve),l(jobsof(thelma),l(jobsof(pete),end)))). given clause #88: (wt=17) 248 [back_demod,177,demod,243,65] PossJobs(l(j(thelma,chef),l(pj(thelma,teacher),l(pj(thelma,boxer),end)))). given clause #89: (wt=17) 252 [back_demod,194,demod,250] PossPeople(l(j(roberta,teacher),l(pj(steve,teacher),l(pj(thelma,teacher),end)))). given clause #90: (wt=20) 80 [back_demod,42,demod,76,65] PossPeople(l(pj(steve,boxer),l(pj(thelma,boxer),l(pj(pete,boxer),end)))). given clause #91: (wt=30) 245 [back_demod,228,demod,239,65] PossJobs(l(pj(pete,chef),l(pj(pete,clerk),l(pj(pete,actor),l(pj(pete,boxer),end))))). given clause #92: (wt=38) 247 [back_demod,233,demod,241,65] PossJobs(l(j(steve,nurse),l(pj(steve,clerk),l(j(steve,policeofficer),l(pj(steve,teacher),l(pj(steve,actor),l(pj(steve,boxer),end))))))). Search stopped because sos empty. ============ end of search ============ -------------- statistics ------------- clauses given 92 clauses generated 150 ur_res generated 150 demod & eval rewrites 193 clauses wt,lit,sk delete 0 tautologies deleted 0 clauses forward subsumed 80 (subsumed by sos) 35 unit deletions 0 factor simplifications 0 clauses kept 169 new demodulators 23 empty clauses 0 clauses back demodulated 99 clauses back subsumed 0 usable size 134 sos size 0 demodulators size 24 passive size 0 hot size 0 Kbytes malloced 223 ----------- times (seconds) ----------- user CPU time 1.08 (0 hr, 0 min, 1 sec) system CPU time 0.15 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) input time 0.47 clausify time 0.00 ur_res time 0.07 pre_process time 0.30 renumber time 0.01 demod time 0.01 order equalities 0.00 unit deleletion 0.00 factor simplify 0.00 weigh cl time 0.00 hints keep time 0.00 sort lits time 0.00 forward subsume 0.01 delete cl time 0.00 keep cl time 0.11 hints time 0.00 print_cl time 0.06 conflict time 0.06 new demod time 0.01 post_process time 0.12 back demod time 0.07 back subsume 0.03 factor time 0.00 unindex time 0.02 The job finished Mon Apr 27 00:06:50 1998