API tools faq
paste
Advertisement
logicmoo

Canonicalizer

logicmoo
Aug 9th, 2017
282
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Prolog 92.03 KB | None | 0 0
raw download clone embed print report
  1. */
  2.  
  3.  
  4. % ============================================================
  5. % all rooms have a door
  6. % ============================================================
  7.  
  8. :- test_boxlog(all(R, implies(room(R), exists(D, and(door(D), has(R, D)))))).
  9.  
  10.  /*
  11. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:18
  12. % :- test_boxlog(all(R_VAR,
  13. %                  implies(room(R_VAR),
  14. %                          exists(D_VAR, and(door(D_VAR), has(R_VAR, D_VAR)))))).
  15. % kif :-
  16. %       all(R,  (room(R)=>exists(D, door(D)&has(R, D)))).
  17. % qualify_nesc :-
  18. %       all(R, nesc((room(R)=>exists(D, door(D)&has(R, D))))).
  19. % debugm(user, sc_success(user, user:nnf(KB, all(R, nesc(b_d(KB, nesc, poss),  (room(R)=>exists(D, door(D)&has(R, D))))), nesc(b_d(KB, nesc, poss), ~room(R)v(door(D)v~skolem(D, skFn(door(D)&has(R, D)))))&nesc(b_d(KB, nesc, poss), ~room(R)v(has(R, D)v~skolem(D, skFn(door(D)&has(R, D)))))))).
  20. % nnf :-
  21. %       nesc(~room(R)v(door(D)v~skolem(D, skFn(door(D)&has(R, D)))))&nesc(~room(R)v(has(R, D)v~skolem(D, skFn(door(D)&has(R, D))))).
  22. % th_nnf_in :-
  23. %       (   neg(room(R))
  24. %       ;   tru(door(D))
  25. %       ;   neg(skolem(D, skFn((door(D), has(R, D)))))
  26. %       ),
  27. %       (   neg(room(R))
  28. %       ;   tru(has(R, D))
  29. %       ;   neg(skolem(D, skFn((door(D), has(R, D)))))
  30. %       ).
  31. % th_nnf_out :-
  32. %       ~ (n(neg(room(R))), n(tru(door(D))), n(neg(skolem(D, skFn((door(D), has(R, D))))));n(neg(room(R))), n(tru(has(R, D))), n(neg(skolem(D, skFn((door(D), has(R, D))))))).
  33. % proven_neg(room(R)) :-
  34. %       ~door(D),
  35. %       skolem(D, skFn((door(D), has(R, D)))).
  36. % proven_tru(door(D)) :-
  37. %       room(R),
  38. %       skolem(D, skFn((door(D), has(R, D)))).
  39. % proven_neg(skolem(D, skFn((door(D), has(R, D))))) :-
  40. %       ~door(D),
  41. %       room(R).
  42. % proven_neg(room(R)) :-
  43. %       ~has(R, D),
  44. %       skolem(D, skFn((door(D), has(R, D)))).
  45. % proven_tru(has(R, D)) :-
  46. %       room(R),
  47. %       skolem(D, skFn((door(D), has(R, D)))).
  48. % proven_neg(skolem(D, skFn((door(D), has(R, D))))) :-
  49. %       ~has(R, D),
  50. %       room(R).
  51. % pfc :-
  52. %       ~door(D), {ignore(D=skFn((door(D), has(R, D))))}, {is_unit(R)}==>proven_neg(room(R)).
  53. % pfc :-
  54. %       room(R), {is_unit(R)}==>if_missing(if_missing(proven_tru(door(_79604)), proven_tru(door(skFn(door(D)&has(R, D))))), if_missing(proven_tru(door(_79604)), proven_tru(door(skFn(door(skFn((door(D), has(R, D))))&has(R, skFn((door(D), has(R, D))))))))).
  55. % pfc :-
  56. %       ~door(D), room(R), {is_unit(D, R)}==>if_missing(proven_neg(skolem(_98630, skFn((door(_98630), has(R, _98630))))), proven_neg(skolem(skFn(door(D)&has(R, D)), skFn((door(skFn(door(D)&has(R, D))), has(R, skFn(door(D)&has(R, D)))))))).
  57. % pfc :-
  58. %       ~has(R, D), {ignore(D=skFn((door(D), has(R, D))))}, {is_unit(R)}==>proven_neg(room(R)).
  59. % pfc :-
  60. %       room(R), {is_unit(R)}==>if_missing(if_missing(proven_tru(has(R, _129926)), proven_tru(has(R, skFn(door(D)&has(R, D))))), if_missing(proven_tru(has(R, _129926)), proven_tru(has(R, skFn(door(skFn((door(D), has(R, D))))&has(R, skFn((door(D), has(R, D))))))))).
  61. % pfc :-
  62. %       ~has(R, D), room(R), {is_unit(D, R)}==>if_missing(proven_neg(skolem(_149310, skFn((door(_149310), has(R, _149310))))), proven_neg(skolem(skFn(door(D)&has(R, D)), skFn((door(skFn(door(D)&has(R, D))), has(R, skFn(door(D)&has(R, D)))))))).
  63. */
  64.  
  65.  
  66. % Should be simular in meaning to
  67. %
  68. % door(D) :-
  69. %       room(R),
  70. %       skolem(D, skIsDoorInUnkArg2ofHas_1Fn(R)).
  71. % ~room(R) :-
  72. %       \+ (
  73. %            door(D)
  74. %          ).
  75. % ~room(R) :-
  76. %       \+ (
  77. %            has(R, D)
  78. %          ).
  79. % has(R, D) :-
  80. %       room(R),
  81. %       skolem(D, skIsDoorInUnkArg2ofHas_1Fn(R)).
  82.  
  83. % ============================================================
  84. % joe knows  all rooms have a door
  85. % ============================================================
  86.  
  87. :- test_boxlog(knows(joe,
  88.                      all(R, implies(room(R), exists(D, and(door(D), has(R, D))))))).
  89.  
  90.  /*
  91. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:40
  92. % :- test_boxlog(knows(joe,
  93. %                    all(R_VAR,
  94. %                        implies(room(R_VAR),
  95. %                                exists(D_VAR,
  96. %                                       and(door(D_VAR), has(R_VAR, D_VAR))))))).
  97. % kif :-
  98. %       knows(joe, all(R,  (room(R)=>exists(D, door(D)&has(R, D))))).
  99. % qualify_nesc :-
  100. %       nesc(knows(joe, all(R,  (room(R)=>exists(D, door(D)&has(R, D)))))).
  101. % debugm(user, sc_success(user, user:nnf(KB, nesc(b_d(KB, nesc, poss), knows(joe, all(R,  (room(R)=>exists(D, door(D)&has(R, D)))))), nesc(b_d(KB, nesc, poss), ~knows(joe, room(R))v(knows(joe, door(D))v~skolem(D, skFn(knows(joe, door(D))&knows(joe, has(R, D))))))&nesc(b_d(KB, nesc, poss), ~knows(joe, room(R))v(knows(joe, has(R, D))v~skolem(D, skFn(knows(joe, door(D))&knows(joe, has(R, D))))))))).
  102. % nnf :-
  103. %       nesc(~knows(joe, room(R))v(knows(joe, door(D))v~skolem(D, skFn(knows(joe, door(D))&knows(joe, has(R, D))))))&nesc(~knows(joe, room(R))v(knows(joe, has(R, D))v~skolem(D, skFn(knows(joe, door(D))&knows(joe, has(R, D)))))).
  104. % th_nnf_in :-
  105. %       (   neg(knows(joe, room(R)))
  106. %       ;   tru(knows(joe, door(D)))
  107. %       ;   neg(skolem(D, skFn((knows(joe, door(D)), knows(joe, has(R, D))))))
  108. %       ),
  109. %       (   neg(knows(joe, room(R)))
  110. %       ;   tru(knows(joe, has(R, D)))
  111. %       ;   neg(skolem(D, skFn((knows(joe, door(D)), knows(joe, has(R, D))))))
  112. %       ).
  113. % th_nnf_out :-
  114. %       ~ (n(neg(knows(joe, room(R)))), n(tru(knows(joe, door(D)))), n(neg(skolem(D, skFn((knows(joe, door(D)), knows(joe, has(R, D)))))));n(neg(knows(joe, room(R)))), n(tru(knows(joe, has(R, D)))), n(neg(skolem(D, skFn((knows(joe, door(D)), knows(joe, has(R, D)))))))).
  115. % proven_neg(knows(joe, room(R))) :-
  116. %       ~knows(joe, door(D)),
  117. %       skolem(D, skFn((knows(joe, door(D)), knows(joe, has(R, D))))).
  118. % proven_tru(knows(joe, door(D))) :-
  119. %       knows(joe, room(R)),
  120. %       skolem(D, skFn((knows(joe, door(D)), knows(joe, has(R, D))))).
  121. % proven_neg(skolem(D, skFn((knows(joe, door(D)), knows(joe, has(R, D)))))) :-
  122. %       ~knows(joe, door(D)),
  123. %       knows(joe, room(R)).
  124. % proven_neg(knows(joe, room(R))) :-
  125. %       ~knows(joe, has(R, D)),
  126. %       skolem(D, skFn((knows(joe, door(D)), knows(joe, has(R, D))))).
  127. % proven_tru(knows(joe, has(R, D))) :-
  128. %       knows(joe, room(R)),
  129. %       skolem(D, skFn((knows(joe, door(D)), knows(joe, has(R, D))))).
  130. % proven_neg(skolem(D, skFn((knows(joe, door(D)), knows(joe, has(R, D)))))) :-
  131. %       ~knows(joe, has(R, D)),
  132. %       knows(joe, room(R)).
  133. % pfc :-
  134. %       ~knows(joe, door(D)), {ignore(D=skFn((knows(joe, door(D)), knows(joe, has(R, D)))))}, {is_unit(R)}==>proven_neg(knows(joe, room(R))).
  135. % pfc :-
  136. %       knows(joe, room(R)), {is_unit(R)}==>if_missing(if_missing(proven_tru(knows(joe, door(_97736))), proven_tru(knows(joe, door(skFn(knows(joe, door(D))&knows(joe, has(R, D))))))), if_missing(proven_tru(knows(joe, door(_97736))), proven_tru(knows(joe, door(skFn(knows(joe, door(skFn((knows(joe, door(D)), knows(joe, has(R, D))))))&knows(joe, has(R, skFn((knows(joe, door(D)), knows(joe, has(R, D)))))))))))).
  137. % pfc :-
  138. %       ~knows(joe, door(D)), knows(joe, room(R)), {is_unit(D, R)}==>if_missing(proven_neg(skolem(_124440, skFn((knows(joe, door(_124440)), knows(joe, has(R, _124440)))))), proven_neg(skolem(skFn(knows(joe, door(D))&knows(joe, has(R, D))), skFn((knows(joe, door(skFn(knows(joe, door(D))&knows(joe, has(R, D))))), knows(joe, has(R, skFn(knows(joe, door(D))&knows(joe, has(R, D)))))))))).
  139. % pfc :-
  140. %       ~knows(joe, has(R, D)), {ignore(D=skFn((knows(joe, door(D)), knows(joe, has(R, D)))))}, {is_unit(R)}==>proven_neg(knows(joe, room(R))).
  141. % pfc :-
  142. %       knows(joe, room(R)), {is_unit(R)}==>if_missing(if_missing(proven_tru(knows(joe, has(R, _166808))), proven_tru(knows(joe, has(R, skFn(knows(joe, door(D))&knows(joe, has(R, D))))))), if_missing(proven_tru(knows(joe, has(R, _166808))), proven_tru(knows(joe, has(R, skFn(knows(joe, door(skFn((knows(joe, door(D)), knows(joe, has(R, D))))))&knows(joe, has(R, skFn((knows(joe, door(D)), knows(joe, has(R, D)))))))))))).
  143. % pfc :-
  144. %       ~knows(joe, has(R, D)), knows(joe, room(R)), {is_unit(D, R)}==>if_missing(proven_neg(skolem(_193870, skFn((knows(joe, door(_193870)), knows(joe, has(R, _193870)))))), proven_neg(skolem(skFn(knows(joe, door(D))&knows(joe, has(R, D))), skFn((knows(joe, door(skFn(knows(joe, door(D))&knows(joe, has(R, D))))), knows(joe, has(R, skFn(knows(joe, door(D))&knows(joe, has(R, D)))))))))).
  145. */
  146.  
  147.  
  148. % Should be simular in meaning to
  149. % ~knows(joe, room(A)) :-
  150. %      \+ (
  151. %           knows(joe, door(B))
  152. %         ).
  153. % ~knows(joe, room(A)) :-
  154. %      \+ (
  155. %           knows(joe, has(A, B))
  156. %         ).
  157. % knows(joe, door(A)) :-
  158. %      knows(joe, room(B)),
  159. %      skolem(A, skIsDoorInUnkArg2ofHas_2Fn(B)).
  160. % knows(joe, has(A, B)) :-
  161. %      knows(joe, room(A)),
  162. %      skolem(B, skIsDoorInUnkArg2ofHas_2Fn(A)).
  163.  
  164. % ============================================================
  165. % for all rooms joe knows about he belives a door exists
  166. % ============================================================
  167.  
  168. :- test_boxlog(all(R,
  169.                    implies(knows(joe, room(R)),
  170.                            belives(joe, exists(D, and(door(D), has(R, D))))))).
  171.  
  172.  /*
  173. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:61
  174. % :- test_boxlog(all(R_VAR,
  175. %                  implies(knows(joe, room(R_VAR)),
  176. %                          belives(joe,
  177. %                                  exists(D_VAR,
  178. %                                         and(door(D_VAR), has(R_VAR, D_VAR))))))).
  179. % kif :-
  180. %       all(R,  (knows(joe, room(R))=>belives(joe, exists(D, door(D)&has(R, D))))).
  181. % qualify_nesc :-
  182. %       all(R,
  183. %           nesc((knows(joe, room(R))=>belives(joe, exists(D, door(D)&has(R, D)))))).
  184. % debugm(user, sc_success(user, user:nnf(KB, all(R, nesc(b_d(KB, nesc, poss),  (knows(joe, room(R))=>belives(joe, exists(D, door(D)&has(R, D)))))), nesc(b_d(KB, nesc, poss), ~knows(joe, room(R))v(belives(joe, door(D))v~skolem(D, skFn(belives(joe, door(D))&belives(joe, has(R, D))))))&nesc(b_d(KB, nesc, poss), ~knows(joe, room(R))v(belives(joe, has(R, D))v~skolem(D, skFn(belives(joe, door(D))&belives(joe, has(R, D))))))))).
  185. % nnf :-
  186. %       nesc(~knows(joe, room(R))v(belives(joe, door(D))v~skolem(D, skFn(belives(joe, door(D))&belives(joe, has(R, D))))))&nesc(~knows(joe, room(R))v(belives(joe, has(R, D))v~skolem(D, skFn(belives(joe, door(D))&belives(joe, has(R, D)))))).
  187. % th_nnf_in :-
  188. %       (   neg(knows(joe, room(R)))
  189. %       ;   tru(belives(joe, door(D)))
  190. %       ;   neg(skolem(D, skFn((belives(joe, door(D)), belives(joe, has(R, D))))))
  191. %       ),
  192. %       (   neg(knows(joe, room(R)))
  193. %       ;   tru(belives(joe, has(R, D)))
  194. %       ;   neg(skolem(D, skFn((belives(joe, door(D)), belives(joe, has(R, D))))))
  195. %       ).
  196. % th_nnf_out :-
  197. %       ~ (n(neg(knows(joe, room(R)))), n(tru(belives(joe, door(D)))), n(neg(skolem(D, skFn((belives(joe, door(D)), belives(joe, has(R, D)))))));n(neg(knows(joe, room(R)))), n(tru(belives(joe, has(R, D)))), n(neg(skolem(D, skFn((belives(joe, door(D)), belives(joe, has(R, D)))))))).
  198. % proven_neg(knows(joe, room(R))) :-
  199. %       ~belives(joe, door(D)),
  200. %       skolem(D, skFn((belives(joe, door(D)), belives(joe, has(R, D))))).
  201. % proven_tru(belives(joe, door(D))) :-
  202. %       knows(joe, room(R)),
  203. %       skolem(D, skFn((belives(joe, door(D)), belives(joe, has(R, D))))).
  204. % proven_neg(skolem(D, skFn((belives(joe, door(D)), belives(joe, has(R, D)))))) :-
  205. %       ~belives(joe, door(D)),
  206. %       knows(joe, room(R)).
  207. % proven_neg(knows(joe, room(R))) :-
  208. %       ~belives(joe, has(R, D)),
  209. %       skolem(D, skFn((belives(joe, door(D)), belives(joe, has(R, D))))).
  210. % proven_tru(belives(joe, has(R, D))) :-
  211. %       knows(joe, room(R)),
  212. %       skolem(D, skFn((belives(joe, door(D)), belives(joe, has(R, D))))).
  213. % proven_neg(skolem(D, skFn((belives(joe, door(D)), belives(joe, has(R, D)))))) :-
  214. %       ~belives(joe, has(R, D)),
  215. %       knows(joe, room(R)).
  216. % pfc :-
  217. %       ~belives(joe, door(D)), {ignore(D=skFn((belives(joe, door(D)), belives(joe, has(R, D)))))}, {is_unit(R)}==>proven_neg(knows(joe, room(R))).
  218. % pfc :-
  219. %       knows(joe, room(R)), {is_unit(R)}==>if_missing(if_missing(proven_tru(belives(joe, door(_97822))), proven_tru(belives(joe, door(skFn(belives(joe, door(D))&belives(joe, has(R, D))))))), if_missing(proven_tru(belives(joe, door(_97822))), proven_tru(belives(joe, door(skFn(belives(joe, door(skFn((belives(joe, door(D)), belives(joe, has(R, D))))))&belives(joe, has(R, skFn((belives(joe, door(D)), belives(joe, has(R, D)))))))))))).
  220. % pfc :-
  221. %       ~belives(joe, door(D)), knows(joe, room(R)), {is_unit(D, R)}==>if_missing(proven_neg(skolem(_124526, skFn((belives(joe, door(_124526)), belives(joe, has(R, _124526)))))), proven_neg(skolem(skFn(belives(joe, door(D))&belives(joe, has(R, D))), skFn((belives(joe, door(skFn(belives(joe, door(D))&belives(joe, has(R, D))))), belives(joe, has(R, skFn(belives(joe, door(D))&belives(joe, has(R, D)))))))))).
  222. % pfc :-
  223. %       ~belives(joe, has(R, D)), {ignore(D=skFn((belives(joe, door(D)), belives(joe, has(R, D)))))}, {is_unit(R)}==>proven_neg(knows(joe, room(R))).
  224. % pfc :-
  225. %       knows(joe, room(R)), {is_unit(R)}==>if_missing(if_missing(proven_tru(belives(joe, has(R, _166894))), proven_tru(belives(joe, has(R, skFn(belives(joe, door(D))&belives(joe, has(R, D))))))), if_missing(proven_tru(belives(joe, has(R, _166894))), proven_tru(belives(joe, has(R, skFn(belives(joe, door(skFn((belives(joe, door(D)), belives(joe, has(R, D))))))&belives(joe, has(R, skFn((belives(joe, door(D)), belives(joe, has(R, D)))))))))))).
  226. % pfc :-
  227. %       ~belives(joe, has(R, D)), knows(joe, room(R)), {is_unit(D, R)}==>if_missing(proven_neg(skolem(_193956, skFn((belives(joe, door(_193956)), belives(joe, has(R, _193956)))))), proven_neg(skolem(skFn(belives(joe, door(D))&belives(joe, has(R, D))), skFn((belives(joe, door(skFn(belives(joe, door(D))&belives(joe, has(R, D))))), belives(joe, has(R, skFn(belives(joe, door(D))&belives(joe, has(R, D)))))))))).
  228. */
  229.  
  230.  
  231. % ~knows(joe, room(A)) :-
  232. %      \+ (
  233. %           belives(joe, door(B))
  234. %         ).
  235. % ~knows(joe, room(A)) :-
  236. %      \+ (
  237. %           belives(joe, has(A, B))
  238. %         ).
  239. % belives(joe, door(A)) :-
  240. %      knows(joe, room(B)),
  241. %      skolem(A, skIsDoorInUnkArg2ofHas_3Fn(B)).
  242. % belives(joe, has(A, B)) :-
  243. %      knows(joe, room(A)),
  244. %      skolem(B, skIsDoorInUnkArg2ofHas_3Fn(A)).
  245.  
  246.  
  247.  
  248. % ============================================================
  249. % For joe to eat the food it must be possible that the food is food and joe can eat it
  250. % ============================================================
  251.  
  252. :- test_boxlog((poss(eats(joe, X)&food(X))=>eats(joe, X), food(X))).
  253.  
  254.  /*
  255. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:83
  256. % :- test_boxlog((poss(eats(joe, X_VAR)&food(X_VAR))=>eats(joe, X_VAR), food(X_VAR))).
  257. % debugm(user, sc_success(user, user:nnf(KB, all(X,  (poss(b_d(KB, nesc, poss), eats(joe, X)&food(X))=>eats(joe, X)&food(X))), nesc(b_d(KB, nesc, poss), ~eats(joe, X)v~food(X))v(eats(joe, X)&food(X))))).
  258. % nnf :-
  259. %       nesc(~eats(joe, X)v~food(X))v(eats(joe, X)&food(X)).
  260. % th_nnf_in :-
  261. %       (   (   neg(eats(joe, X))
  262. %           ;   neg(food(X))
  263. %           )
  264. %       ;   tru(eats(joe, X)),
  265. %           tru(food(X))
  266. %       ).
  267. % th_nnf_out :-
  268. %       ~ ((n(neg(eats(joe, X))), n(neg(food(X)))), (n(tru(eats(joe, X)));n(tru(food(X))))).
  269. % proven_neg(eats(joe, X)) :-
  270. %       naf(eats(joe, X)).
  271. % proven_neg(food(X)) :-
  272. %       naf(food(X)).
  273. % proven_tru(eats(joe, X)) :-
  274. %       food(X),
  275. %       poss(eats(joe, X)).
  276. % proven_tru(food(X)) :-
  277. %       eats(joe, X),
  278. %       poss(food(X)).
  279. % pfc :-
  280. %       naf(eats(joe, X)), {is_unit(X)}==>proven_neg(eats(joe, X)).
  281. % pfc :-
  282. %       naf(food(X)), {is_unit(X)}==>proven_neg(food(X)).
  283. % pfc :-
  284. %       food(X), poss(eats(joe, X)), {is_unit(X)}==>proven_tru(eats(joe, X)).
  285. % pfc :-
  286. %       eats(joe, X), poss(food(X)), {is_unit(X)}==>proven_tru(food(X)).
  287. */
  288.  
  289.  
  290. % eats(joe,X) :-
  291. %       \+ ~eats(joe,X),
  292. %       \+ ~food(X).
  293. % food(X) :-
  294. %       \+ ~eats(joe,X),
  295. %       \+ ~food(X).
  296.  
  297. % ============================================================================================
  298. % At least one man exists
  299. % ============================================================================================
  300.  
  301.  
  302. :- test_boxlog(atleast(1, X, man(X))).
  303.  
  304.  /*
  305. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:96
  306. % :- test_boxlog(atleast(1, X_VAR, man(X_VAR))).
  307. % kif :-
  308. %       all(X, atleast(1, X, man(X))).
  309. % qualify_nesc :-
  310. %       all(X, nesc(atleast(1, X, man(X)))).
  311. % debugm(user, sc_success(user, user:nnf(KB, all(X, nesc(b_d(KB, nesc, poss), atleast(1, X, man(X)))), nesc(b_d(KB, nesc, poss), man(X)v~skolem(X, skFn(man(X))))))).
  312. % nnf :-
  313. %       nesc(man(X)v~skolem(X, skFn(man(X)))).
  314. % th_nnf_in :-
  315. %       (   tru(man(X))
  316. %       ;   neg(skolem(X, skFn(man(X))))
  317. %       ).
  318. % th_nnf_out :-
  319. %       ~ (n(tru(man(X))), n(neg(skolem(X, skFn(man(X)))))).
  320. % proven_tru(man(X)) :-
  321. %       skolem(X, skFn(man(X))).
  322. % proven_neg(skolem(X, skFn(man(X)))) :-
  323. %       ~man(X).
  324. % pfc :-
  325. %       if_missing(if_missing(proven_tru(man(_414162)),
  326. %                             proven_tru(man(skFn(man(X))))),
  327. %                  if_missing(proven_tru(man(_414162)),
  328. %                             proven_tru(man(skFn(man(skFn(man(X)))))))).
  329. % pfc :-
  330. %       ~man(X), {is_unit(X)}==>if_missing(proven_neg(skolem(_427034, skFn(man(_427034)))), proven_neg(skolem(skFn(man(X)), skFn(man(skFn(man(X))))))).
  331. */
  332.  
  333.  
  334. % ============================================================================================
  335. % At least three men exist
  336. % ============================================================================================
  337.  
  338.  
  339. :- test_boxlog(atleast(3, X, man(X))).
  340.  
  341.  /*
  342. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:102
  343. % :- test_boxlog(atleast(3, X_VAR, man(X_VAR))).
  344. % kif :-
  345. %       all(X, atleast(3, X, man(X))).
  346. % qualify_nesc :-
  347. %       all(X, nesc(atleast(3, X, man(X)))).
  348. % debugm(user, sc_success(user, user:nnf(KB, all(X, nesc(b_d(KB, nesc, poss), atleast(3, X, man(X)))), nesc(b_d(KB, nesc, poss), ~man(X)v~man(_1540)v~man(_1548)v different(X, _1540))&nesc(b_d(KB, nesc, poss), ~man(X)v~man(_1540)v~man(_1548)v different(X, _1548))&nesc(b_d(KB, nesc, poss), ~man(X)v~man(_1540)v~man(_1548)v different(_1540, _1548))))).
  349. % nnf :-
  350. %       nesc(~man(X)v~man(_1540)v~man(_1548)v different(X, _1540))&nesc(~man(X)v~man(_1540)v~man(_1548)v different(X, _1548))&nesc(~man(X)v~man(_1540)v~man(_1548)v different(_1540, _1548)).
  351. % th_nnf_in :-
  352. %       ( (   (   (   neg(man(X))
  353. %                 ;   neg(man(_1540))
  354. %                 )
  355. %             ;   neg(man(_1548))
  356. %             )
  357. %         ;   tru(different(X, _1540))
  358. %         ),
  359. %         (   (   (   neg(man(X))
  360. %                 ;   neg(man(_1540))
  361. %                 )
  362. %             ;   neg(man(_1548))
  363. %             )
  364. %         ;   tru(different(X, _1548))
  365. %         )
  366. %       ),
  367. %       (   (   (   neg(man(X))
  368. %               ;   neg(man(_1540))
  369. %               )
  370. %           ;   neg(man(_1548))
  371. %           )
  372. %       ;   tru(different(_1540, _1548))
  373. %       ).
  374. % th_nnf_out :-
  375. %       ~ ((((n(neg(man(X))), n(neg(man(_1540)))), n(neg(man(_1548)))), n(tru(different(X, _1540)));((n(neg(man(X))), n(neg(man(_1540)))), n(neg(man(_1548)))), n(tru(different(X, _1548))));((n(neg(man(X))), n(neg(man(_1540)))), n(neg(man(_1548)))), n(tru(different(_1540, _1548)))).
  376. % proven_neg(man(X)) :-
  377. %       man(_1540),
  378. %       man(_1548),
  379. %       ~different(X, _1540).
  380. % proven_neg(man(_1540)) :-
  381. %       man(X),
  382. %       man(_1548),
  383. %       ~different(X, _1540).
  384. % proven_neg(man(_1548)) :-
  385. %       man(X),
  386. %       man(_1540),
  387. %       ~different(X, _1540).
  388. % proven_tru(different(X, _1540)) :-
  389. %       man(X),
  390. %       man(_1540),
  391. %       man(_1548).
  392. % proven_neg(man(X)) :-
  393. %       man(_1540),
  394. %       man(_1548),
  395. %       ~different(X, _1548).
  396. % proven_neg(man(_1540)) :-
  397. %       man(X),
  398. %       man(_1548),
  399. %       ~different(X, _1548).
  400. % proven_neg(man(_1548)) :-
  401. %       man(X),
  402. %       man(_1540),
  403. %       ~different(X, _1548).
  404. % proven_tru(different(X, _1548)) :-
  405. %       man(X),
  406. %       man(_1540),
  407. %       man(_1548).
  408. % proven_neg(man(X)) :-
  409. %       man(_1540),
  410. %       man(_1548),
  411. %       ~different(_1540, _1548).
  412. % proven_neg(man(_1540)) :-
  413. %       man(X),
  414. %       man(_1548),
  415. %       ~different(_1540, _1548).
  416. % proven_neg(man(_1548)) :-
  417. %       man(X),
  418. %       man(_1540),
  419. %       ~different(_1540, _1548).
  420. % proven_tru(different(_1540, _1548)) :-
  421. %       man(X),
  422. %       man(_1540),
  423. %       man(_1548).
  424. % pfc :-
  425. %       man(_1540), man(_1548), not_different(X, _1540), {is_unit(X)}==>proven_neg(man(X)).
  426. % pfc :-
  427. %       man(X), man(_1548), not_different(X, _1540), {is_unit(_1540)}==>proven_neg(man(_1540)).
  428. % pfc :-
  429. %       man(X), man(_1540), not_different(X, _1540), {is_unit}==>proven_neg(man(_1548)).
  430. % pfc :-
  431. %       man(X), man(_1540), man(_1548), {is_unit(_1540, X)}==>proven_tru(different(X, _1540)).
  432. % pfc :-
  433. %       man(_1540), man(_1548), not_different(X, _1548), {is_unit(X)}==>proven_neg(man(X)).
  434. % pfc :-
  435. %       man(X), man(_1548), not_different(X, _1548), {is_unit}==>proven_neg(man(_1540)).
  436. % pfc :-
  437. %       man(X), man(_1540), not_different(X, _1548), {is_unit(_1548)}==>proven_neg(man(_1548)).
  438. % pfc :-
  439. %       man(X), man(_1540), man(_1548), {is_unit(_1548, X)}==>proven_tru(different(X, _1548)).
  440. % pfc :-
  441. %       man(_1540), man(_1548), not_different(_1540, _1548), {is_unit}==>proven_neg(man(X)).
  442. % pfc :-
  443. %       man(X), man(_1548), not_different(_1540, _1548), {is_unit(_1540)}==>proven_neg(man(_1540)).
  444. % pfc :-
  445. %       man(X), man(_1540), not_different(_1540, _1548), {is_unit(_1548)}==>proven_neg(man(_1548)).
  446. % pfc :-
  447. %       man(X), man(_1540), man(_1548), {is_unit(_1548, _1540)}==>proven_tru(different(_1540, _1548)).
  448. */
  449.  
  450.  
  451. % ============================================================================================
  452. % Organized Groups of prolog programmers have prolog programmers as members
  453. % ============================================================================================
  454.  
  455.  
  456. :- test_boxlog(implies(and(instance(M, tGroupedPrologOrganization),
  457.                            hasMembers(M, A)),
  458.                        instance(A, tClazzPrologPerson))).
  459.  
  460.  /*
  461. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:108
  462. % :- test_boxlog(implies(and(instance(M_VAR, tGroupedPrologOrganization),
  463. %                          hasMembers(M_VAR, A_VAR)),
  464. %                      instance(A_VAR, tClazzPrologPerson))).
  465. % kif :-
  466. %       all(M,
  467. %           all(A,
  468. %               (tGroupedPrologOrganization(M)&hasMembers(M, A)=>tClazzPrologPerson(A)))).
  469. % qualify_nesc :-
  470. %       all(M,
  471. %           all(A,
  472. %               nesc((tGroupedPrologOrganization(M)&hasMembers(M, A)=>tClazzPrologPerson(A))))).
  473. % debugm(user, sc_success(user, user:nnf(KB, all(M, all(A, nesc(b_d(KB, nesc, poss),  (tGroupedPrologOrganization(M)&hasMembers(M, A)=>tClazzPrologPerson(A))))), nesc(b_d(KB, nesc, poss), ~tGroupedPrologOrganization(M)v~hasMembers(M, A)v tClazzPrologPerson(A))))).
  474. % nnf :-
  475. %       nesc(~tGroupedPrologOrganization(M)v~hasMembers(M, A)v tClazzPrologPerson(A)).
  476. % th_nnf_in :-
  477. %       (   (   neg(tGroupedPrologOrganization(M))
  478. %           ;   neg(hasMembers(M, A))
  479. %           )
  480. %       ;   tru(isa(A, tClazzPrologPerson))
  481. %       ).
  482. % th_nnf_out :-
  483. %       ~ ((n(neg(tGroupedPrologOrganization(M))), n(neg(hasMembers(M, A)))), n(tru(isa(A, tClazzPrologPerson)))).
  484. % proven_neg(tGroupedPrologOrganization(M)) :-
  485. %       hasMembers(M, A),
  486. %       ~isa(A, tClazzPrologPerson).
  487. % proven_neg(hasMembers(M, A)) :-
  488. %       tGroupedPrologOrganization(M),
  489. %       ~isa(A, tClazzPrologPerson).
  490. % proven_tru(isa(A, tClazzPrologPerson)) :-
  491. %       tGroupedPrologOrganization(M),
  492. %       hasMembers(M, A).
  493. % pfc :-
  494. %       hasMembers(M, A), ~tClazzPrologPerson(A), {is_unit(M)}==>proven_neg(tGroupedPrologOrganization(M)).
  495. % pfc :-
  496. %       tGroupedPrologOrganization(M), ~tClazzPrologPerson(A), {is_unit(A, M)}==>proven_neg(hasMembers(M, A)).
  497. % pfc :-
  498. %       tGroupedPrologOrganization(M), hasMembers(M, A), {is_unit(A)}==>proven_tru(tClazzPrologPerson(A)).
  499. */
  500.  
  501.  
  502.  
  503. /*
  504. ~hasMembers(_11164,_11142):- \+ (instance(_11164,tGroupedPrologOrganization),instance(_11142,tClazzPrologPerson)).
  505. ~instance(_11540,tGroupedPrologOrganization):- \+ (hasMembers(_11540,_11518),instance(_11518,tClazzPrologPerson)).
  506. instance(_11874,tClazzPrologPerson):-instance(_11896,tGroupedPrologOrganization),hasMembers(_11896,_11874).
  507. */
  508.  
  509. % ============================================================================================
  510. %  Those competeing in watersports may not wear shoes
  511. % ============================================================================================
  512.  
  513. :- test_boxlog((instance(ATH, tAgent)=>implies(and(instance(COMP, actAquaticSportsEvent), competingAgents(COMP, ATH)), holdsIn(COMP, all(CLOTHING, not(and(instance(CLOTHING, tObjectShoe), wearsClothing(ATH, CLOTHING)))))))).
  514.  
  515.  /*
  516. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:120
  517. % :- test_boxlog((instance(ATH_VAR, tAgent)=>implies(and(instance(COMP_VAR, actAquaticSportsEvent), competingAgents(COMP_VAR, ATH_VAR)), holdsIn(COMP_VAR, all(CLOTHING_VAR, not(and(instance(CLOTHING_VAR, tObjectShoe), wearsClothing(ATH_VAR, CLOTHING_VAR)))))))).
  518. % kif :-
  519. %       all(COMP,
  520. %           all(ATH,
  521. %               (tAgent(ATH)=>(actAquaticSportsEvent(COMP)&competingAgents(COMP, ATH)=>holdsIn(COMP, all(CLOTHING, ~ (tObjectShoe(CLOTHING)&wearsClothing(ATH, CLOTHING)))))))).
  522. % qualify_nesc :-
  523. %       all(COMP,
  524. %           all(ATH,
  525. %               nesc((tAgent(ATH)=>(actAquaticSportsEvent(COMP)&competingAgents(COMP, ATH)=>holdsIn(COMP, all(CLOTHING, ~ (tObjectShoe(CLOTHING)&wearsClothing(ATH, CLOTHING))))))))).
  526. % debugm(user, sc_success(user, user:nnf(KB, all(COMP, all(ATH, nesc(b_d(KB, nesc, poss),  (tAgent(ATH)=>(actAquaticSportsEvent(COMP)&competingAgents(COMP, ATH)=>holdsIn(COMP, all(CLOTHING, ~ (tObjectShoe(CLOTHING)&wearsClothing(ATH, CLOTHING))))))))), nesc(b_d(KB, nesc, poss), ~tAgent(ATH)v(~actAquaticSportsEvent(COMP)v~competingAgents(COMP, ATH)v(~occuring(COMP)v(~tObjectShoe(CLOTHING)v~wearsClothing(ATH, CLOTHING)))))))).
  527. % nnf :-
  528. %       nesc(~tAgent(ATH)v(~actAquaticSportsEvent(COMP)v~competingAgents(COMP, ATH)v(~occuring(COMP)v(~tObjectShoe(CLOTHING)v~wearsClothing(ATH, CLOTHING))))).
  529. % th_nnf_in :-
  530. %       (   neg(tAgent(ATH))
  531. %       ;   (   neg(actAquaticSportsEvent(COMP))
  532. %           ;   neg(competingAgents(COMP, ATH))
  533. %           )
  534. %       ;   neg(occuring(COMP))
  535. %       ;   neg(tObjectShoe(CLOTHING))
  536. %       ;   neg(wearsClothing(ATH, CLOTHING))
  537. %       ).
  538. % th_nnf_out :-
  539. %       ~ (n(neg(tAgent(ATH))), (n(neg(actAquaticSportsEvent(COMP))), n(neg(competingAgents(COMP, ATH)))), n(neg(occuring(COMP))), n(neg(tObjectShoe(CLOTHING))), n(neg(wearsClothing(ATH, CLOTHING)))).
  540. % proven_neg(tAgent(ATH)) :-
  541. %       actAquaticSportsEvent(COMP),
  542. %       competingAgents(COMP, ATH),
  543. %       occuring(COMP),
  544. %       tObjectShoe(CLOTHING),
  545. %       wearsClothing(ATH, CLOTHING).
  546. % proven_neg(actAquaticSportsEvent(COMP)) :-
  547. %       competingAgents(COMP, ATH),
  548. %       occuring(COMP),
  549. %       tObjectShoe(CLOTHING),
  550. %       wearsClothing(ATH, CLOTHING),
  551. %       tAgent(ATH).
  552. % proven_neg(competingAgents(COMP, ATH)) :-
  553. %       actAquaticSportsEvent(COMP),
  554. %       occuring(COMP),
  555. %       tObjectShoe(CLOTHING),
  556. %       wearsClothing(ATH, CLOTHING),
  557. %       tAgent(ATH).
  558. % proven_neg(occuring(COMP)) :-
  559. %       tObjectShoe(CLOTHING),
  560. %       wearsClothing(ATH, CLOTHING),
  561. %       actAquaticSportsEvent(COMP),
  562. %       competingAgents(COMP, ATH),
  563. %       tAgent(ATH).
  564. % proven_neg(tObjectShoe(CLOTHING)) :-
  565. %       wearsClothing(ATH, CLOTHING),
  566. %       occuring(COMP),
  567. %       actAquaticSportsEvent(COMP),
  568. %       competingAgents(COMP, ATH),
  569. %       tAgent(ATH).
  570. % proven_neg(wearsClothing(ATH, CLOTHING)) :-
  571. %       tObjectShoe(CLOTHING),
  572. %       occuring(COMP),
  573. %       actAquaticSportsEvent(COMP),
  574. %       competingAgents(COMP, ATH),
  575. %       tAgent(ATH).
  576. % pfc :-
  577. %       actAquaticSportsEvent(COMP), competingAgents(COMP, ATH), occuring(COMP), tObjectShoe(CLOTHING), wearsClothing(ATH, CLOTHING), {is_unit(ATH)}==>proven_neg(tAgent(ATH)).
  578. % pfc :-
  579. %       competingAgents(COMP, ATH), occuring(COMP), tObjectShoe(CLOTHING), wearsClothing(ATH, CLOTHING), tAgent(ATH), {is_unit(COMP)}==>proven_neg(actAquaticSportsEvent(COMP)).
  580. % pfc :-
  581. %       actAquaticSportsEvent(COMP), occuring(COMP), tObjectShoe(CLOTHING), wearsClothing(ATH, CLOTHING), tAgent(ATH), {is_unit(ATH, COMP)}==>proven_neg(competingAgents(COMP, ATH)).
  582. % pfc :-
  583. %       tObjectShoe(CLOTHING), wearsClothing(ATH, CLOTHING), actAquaticSportsEvent(COMP), competingAgents(COMP, ATH), tAgent(ATH), {is_unit(COMP)}==>proven_neg(occuring(COMP)).
  584. % pfc :-
  585. %       wearsClothing(ATH, CLOTHING), occuring(COMP), actAquaticSportsEvent(COMP), competingAgents(COMP, ATH), tAgent(ATH), {is_unit(CLOTHING)}==>proven_neg(tObjectShoe(CLOTHING)).
  586. % pfc :-
  587. %       tObjectShoe(CLOTHING), occuring(COMP), actAquaticSportsEvent(COMP), competingAgents(COMP, ATH), tAgent(ATH), {is_unit(CLOTHING, ATH)}==>proven_neg(wearsClothing(ATH, CLOTHING)).
  588. */
  589.  
  590. /*
  591. ~competingAgents(_20514,_20492):- ~holdsIn(_20514,v(~instance(_20470,tObjectShoe),~wearsClothing(_20492,_20470))),instance(_20514,actAquaticSportsEvent),instance(_20492,tAgent)
  592. ~instance(_20902,tAgent):- ~holdsIn(_20858,v(~instance(_20880,tObjectShoe),~wearsClothing(_20902,_20880))),instance(_20858,actAquaticSportsEvent),competingAgents(_20858,_20902)
  593. ~instance(_21272,actAquaticSportsEvent):- ~holdsIn(_21272,v(~instance(_21250,tObjectShoe),~wearsClothing(_21228,_21250))),competingAgents(_21272,_21228),instance(_21228,tAgent)
  594. holdsIn(_21612,v(~instance(_21634,tObjectShoe),~wearsClothing(_21590,_21634))):-instance(_21612,actAquaticSportsEvent),competingAgents(_21612,_21590),instance(_21590,tAgent)
  595. */
  596. % ~occuring(COMP) :-
  597. %       instance(ATH, tAgent),
  598. %       instance(COMP, actAquaticSportsEvent),
  599. %       competingAgents(COMP, ATH),
  600. %       instance(CLOTHING, tObjectShoe),
  601. %       wearsClothing(ATH, CLOTHING).
  602. % ~competingAgents(COMP, ATH) :-
  603. %       instance(ATH, tAgent),
  604. %       instance(COMP, actAquaticSportsEvent),
  605. %       occuring(COMP),
  606. %       instance(CLOTHING, tObjectShoe),
  607. %       wearsClothing(ATH, CLOTHING).
  608. % ~instance(CLOTHING, tObjectShoe) :-
  609. %       instance(ATH, tAgent),
  610. %       instance(COMP, actAquaticSportsEvent),
  611. %       competingAgents(COMP, ATH),
  612. %       occuring(COMP),
  613. %       wearsClothing(ATH, CLOTHING).
  614. % ~instance(COMP, actAquaticSportsEvent) :-
  615. %       instance(ATH, tAgent),
  616. %       competingAgents(COMP, ATH),
  617. %       occuring(COMP),
  618. %       instance(CLOTHING, tObjectShoe),
  619. %       wearsClothing(ATH, CLOTHING).
  620. % ~instance(ATH, tAgent) :-
  621. %       instance(COMP, actAquaticSportsEvent),
  622. %       competingAgents(COMP, ATH),
  623. %       occuring(COMP),
  624. %       instance(CLOTHING, tObjectShoe),
  625. %       wearsClothing(ATH, CLOTHING).
  626. % ~wearsClothing(ATH, CLOTHING) :-
  627. %       instance(ATH, tAgent),
  628. %       instance(COMP, actAquaticSportsEvent),
  629. %       competingAgents(COMP, ATH),
  630. %       occuring(COMP),
  631. %       instance(CLOTHING, tObjectShoe).
  632.  
  633. % ================================================================================================================
  634. %  When sightgseeing is occuring .. there is a tourist present
  635. % ================================================================================================================
  636.  
  637. :- test_boxlog(implies(and(instance(Act, actSightseeing),
  638.                            performedBy(Person, Act)),
  639.                        holdsIn(Act, instance(Person, mobTourist)))).
  640.  
  641.  /*
  642. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:168
  643. % :- test_boxlog(implies(and(instance(Act_VAR, actSightseeing),
  644. %                          performedBy(Person_VAR, Act_VAR)),
  645. %                      holdsIn(Act_VAR, instance(Person_VAR, mobTourist)))).
  646. % kif :-
  647. %       all(Act,
  648. %           all(Person,
  649. %               (actSightseeing(Act)&performedBy(Person, Act)=>holdsIn(Act, mobTourist(Person))))).
  650. % qualify_nesc :-
  651. %       all(Act,
  652. %           all(Person,
  653. %               nesc((actSightseeing(Act)&performedBy(Person, Act)=>holdsIn(Act, mobTourist(Person)))))).
  654. % debugm(user, sc_success(user, user:nnf(KB, all(Act, all(Person, nesc(b_d(KB, nesc, poss),  (actSightseeing(Act)&performedBy(Person, Act)=>holdsIn(Act, mobTourist(Person)))))), nesc(b_d(KB, nesc, poss), ~actSightseeing(Act)v~performedBy(Person, Act)v(~occuring(Act)v mobTourist(Person)))))).
  655. % nnf :-
  656. %       nesc(~actSightseeing(Act)v~performedBy(Person, Act)v(~occuring(Act)v mobTourist(Person))).
  657. % th_nnf_in :-
  658. %       (   (   neg(actSightseeing(Act))
  659. %           ;   neg(performedBy(Person, Act))
  660. %           )
  661. %       ;   neg(occuring(Act))
  662. %       ;   tru(mobTourist(Person))
  663. %       ).
  664. % th_nnf_out :-
  665. %       ~ ((n(neg(actSightseeing(Act))), n(neg(performedBy(Person, Act)))), n(neg(occuring(Act))), n(tru(mobTourist(Person)))).
  666. % proven_neg(actSightseeing(Act)) :-
  667. %       performedBy(Person, Act),
  668. %       occuring(Act),
  669. %       ~mobTourist(Person).
  670. % proven_neg(performedBy(Person, Act)) :-
  671. %       actSightseeing(Act),
  672. %       occuring(Act),
  673. %       ~mobTourist(Person).
  674. % proven_neg(occuring(Act)) :-
  675. %       ~mobTourist(Person),
  676. %       actSightseeing(Act),
  677. %       performedBy(Person, Act).
  678. % proven_tru(mobTourist(Person)) :-
  679. %       occuring(Act),
  680. %       actSightseeing(Act),
  681. %       performedBy(Person, Act).
  682. % pfc :-
  683. %       performedBy(Person, Act), occuring(Act), ~mobTourist(Person), {is_unit(Act)}==>proven_neg(actSightseeing(Act)).
  684. % pfc :-
  685. %       actSightseeing(Act), occuring(Act), ~mobTourist(Person), {is_unit(Act, Person)}==>proven_neg(performedBy(Person, Act)).
  686. % pfc :-
  687. %       ~mobTourist(Person), actSightseeing(Act), performedBy(Person, Act), {is_unit(Act)}==>proven_neg(occuring(Act)).
  688. % pfc :-
  689. %       occuring(Act), actSightseeing(Act), performedBy(Person, Act), {is_unit(Person)}==>proven_tru(mobTourist(Person)).
  690. */
  691.  
  692.  
  693. /* OLD
  694. ~instance(_11704,actSightseeing):- \+ (performedBy(_11704,_11682),holdsIn(_11704,instance(_11682,mobTourist)))
  695. ~performedBy(_12092,_12070):- \+ (instance(_12092,actSightseeing),holdsIn(_12092,instance(_12070,mobTourist)))
  696. holdsIn(_12442,instance(_12420,mobTourist)):-instance(_12442,actSightseeing),performedBy(_12442,_12420)
  697.  
  698. */
  699. % ~occuring(Act) :-
  700. %       \+ ( instance(Act, actSightseeing),
  701. %            naf(~performedBy(Person, Act)),
  702. %            instance(Y, mobTourist)
  703. %          ).
  704. % ~instance(Act, actSightseeing) :-
  705. %       \+ ( performedBy(Person, Act),
  706. %            naf(~occuring(Act)),
  707. %            instance(Y, mobTourist)
  708. %          ).
  709. % ~performedBy(Person, Act) :-
  710. %       \+ ( instance(Act, actSightseeing),
  711. %            naf(~occuring(Act)),
  712. %            instance(Y, mobTourist)
  713. %          ).
  714. % instance(Y, mobTourist) :-
  715. %       instance(Act, actSightseeing),
  716. %       performedBy(Person, Act),
  717. %       occuring(Act).
  718.  
  719.  
  720. % ================================================================================================================
  721. %  All rooms have a door (Odd syntax issue)
  722. % ================================================================================================================
  723.  
  724.  
  725. :- test_boxlog(all(R,  (room(R)=>exists(D, and([door(D), has(R, D)]))))).
  726.  
  727.  /*
  728. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:201
  729. % :- test_boxlog(all(R_VAR,
  730. %                  (room(R_VAR)=>exists(D_VAR, and([door(D_VAR), has(R_VAR, D_VAR)]))))).
  731. % kif :-
  732. %       all(R,  (room(R)=>exists(D, [door(D), has(R, D)]))).
  733. % qualify_nesc :-
  734. %       all(R, nesc((room(R)=>exists(D, [door(D), has(R, D)])))).
  735. % debugm(user, sc_success(user, user:nnf(KB, all(R, nesc(b_d(KB, nesc, poss),  (room(R)=>exists(D, [door(D), has(R, D)])))), nesc(b_d(KB, nesc, poss), ~room(R)v(~skolem(D, skFn([door(D), has(R, D)]))v[door(D), has(R, D)]))))).
  736. % nnf :-
  737. %       nesc(~room(R)v(~skolem(D, skFn([door(D), has(R, D)]))v[door(D), has(R, D)])).
  738. % th_nnf_in :-
  739. %       (   neg(room(R))
  740. %       ;   neg(skolem(D, skFn([door(D), has(R, D)])))
  741. %       ;   tru([door(D), has(R, D)])
  742. %       ).
  743. % th_nnf_out :-
  744. %       ~ (n(neg(room(R))), n(neg(skolem(D, skFn([door(D), has(R, D)])))), n(tru([door(D), has(R, D)]))).
  745. % proven_neg(room(R)) :-
  746. %       skolem(D, skFn([door(D), has(R, D)])),
  747. %       ~[door(D), has(R, D)].
  748. % proven_neg(skolem(D, skFn([door(D), has(R, D)]))) :-
  749. %       room(R),
  750. %       ~[door(D), has(R, D)].
  751. % proven_tru([door(D), has(R, D)]) :-
  752. %       room(R),
  753. %       skolem(D, skFn([door(D), has(R, D)])).
  754. % pfc :-
  755. %       {ignore(D=skFn([door(D), has(R, D)]))}, ~[door(D), has(R, D)], {is_unit(R)}==>proven_neg(room(R)).
  756. % pfc :-
  757. %       room(R), ~[door(D), has(R, D)], {is_unit(D, R)}==>if_missing(proven_neg(skolem(_186806, skFn([door(_186806), has(R, _186806)]))), proven_neg(skolem(skFn([door(D), has(R, D)]), skFn([door(skFn([door(D), has(R, D)])), has(R, skFn([door(D), has(R, D)]))])))).
  758. % pfc :-
  759. %       room(R), {is_unit(R)}==>if_missing(if_missing(proven_tru([door(_209580), has(R, _209580)]), proven_tru([door(skFn([door(D), has(R, D)])), has(R, skFn([door(D), has(R, D)]))])), if_missing(proven_tru([door(_209580), has(R, _209580)]), proven_tru([door(skFn([door(skFn([door(D), has(R, D)])), has(R, skFn([door(D), has(R, D)]))])), has(R, skFn([door(skFn([door(D), has(R, D)])), has(R, skFn([door(D), has(R, D)]))]))]))).
  760. */
  761.  
  762.  
  763. % door(D) :-
  764. %       room(R),
  765. %       skolem(D, skIsDoorInUnkArg2ofHas_2Fn(R)),
  766. %       \+ ~has(R, D).
  767. % ~room(R) :-
  768. %       \+ ( has(R, D),
  769. %            door(D)
  770. %          ).
  771. % has(R, D) :-
  772. %       room(R),
  773. %       skolem(D, skIsDoorInUnkArg2ofHas_2Fn(R)),
  774. %       \+ ~door(D).
  775.  
  776.  
  777.  
  778.  
  779. % ================================================================================================================
  780. %  No one whom pays taxes in North america can be a dependant of another in the same year
  781. % ================================================================================================================
  782.  
  783. :- test_boxlog(or(holdsIn(YEAR,
  784.                           instance(PERSON,
  785.                                    nartR(tClazzCitizenFn,
  786.                                          iGroup_UnitedStatesOfAmerica))),
  787.                   holdsIn(YEAR,
  788.                           instance(PERSON,
  789.                                    nartR(mobTaxResidentsFn, iGroup_Canada))),
  790.                   holdsIn(YEAR,
  791.                           instance(PERSON, nartR(mobTaxResidentsFn, iMexico))),
  792.                   holdsIn(YEAR,
  793.                           instance(PERSON,
  794.                                    nartR(mobTaxResidentsFn,
  795.                                          iGroup_UnitedStatesOfAmerica))),
  796.                   forbiddenToDoWrt(iCW_USIncomeTax,
  797.                                    SUPPORTER,
  798.                                    claimsAsDependent(YEAR,
  799.                                                      SUPPORTER,
  800.                                                      _SUPPORTEE)))).
  801.  
  802.  /*
  803. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:222
  804. % :- test_boxlog(or(holdsIn(YEAR_VAR,
  805. %                         instance(PERSON_VAR,
  806. %                                  nartR(tClazzCitizenFn,
  807. %                                        iGroup_UnitedStatesOfAmerica))),
  808. %                 holdsIn(YEAR_VAR,
  809. %                         instance(PERSON_VAR,
  810. %                                  nartR(mobTaxResidentsFn, iGroup_Canada))),
  811. %                 holdsIn(YEAR_VAR,
  812. %                         instance(PERSON_VAR,
  813. %                                  nartR(mobTaxResidentsFn, iMexico))),
  814. %                 holdsIn(YEAR_VAR,
  815. %                         instance(PERSON_VAR,
  816. %                                  nartR(mobTaxResidentsFn,
  817. %                                        iGroup_UnitedStatesOfAmerica))),
  818. %                 forbiddenToDoWrt(iCW_USIncomeTax,
  819. %                                  SUPPORTER_VAR,
  820. %                                  claimsAsDependent(YEAR_VAR,
  821. %                                                    SUPPORTER_VAR,
  822. %                                                    _SUPPORTEE_VAR)))).
  823. % kif :-
  824. %       all(YEAR,
  825. %           all(PERSON,
  826. %               all(SUPPORTER,
  827. %                   all(_SUPPORTEE,
  828. %                       holdsIn(YEAR, isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iGroup_Canada)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iMexico)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica)))v forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))))))))).
  829. % qualify_nesc :-
  830. %       all(YEAR,
  831. %           all(PERSON,
  832. %               all(SUPPORTER,
  833. %                   all(_SUPPORTEE,
  834. %                       (~nesc(holdsIn(YEAR, isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iGroup_Canada)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iMexico)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica)))v forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))))))=>nesc(holdsIn(YEAR, isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iGroup_Canada)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iMexico)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica)))v forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))))))))))).
  835. % debugm(user, sc_success(user, user:nnf(KB, all(YEAR, all(PERSON, all(SUPPORTER, all(_SUPPORTEE,  (~nesc(holdsIn(YEAR, isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iGroup_Canada)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iMexico)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica)))v forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))))))=>nesc(b_d(KB, nesc, poss), holdsIn(YEAR, isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iGroup_Canada)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iMexico)))v(holdsIn(YEAR, isa(PERSON, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica)))v forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))))))))))), nesc(b_d(KB, nesc, poss), ~occuring(YEAR)v isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iGroup_Canada))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iMexico))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica))v forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))))))v nesc(b_d(KB, nesc, poss), ~occuring(YEAR)v isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iGroup_Canada))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iMexico))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica))v forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))))))))).
  836. % nnf :-
  837. %       nesc(~occuring(YEAR)v isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iGroup_Canada))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iMexico))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica))v forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))))))v nesc(~occuring(YEAR)v isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iGroup_Canada))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iMexico))v(~occuring(YEAR)v isa(PERSON, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica))v forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)))))).
  838. % th_nnf_in :-
  839. %       (   (   (   neg(occuring(YEAR))
  840. %               ;   tru(isa(PERSON,
  841. %                           tClazzCitizenFn(iGroup_UnitedStatesOfAmerica)))
  842. %               )
  843. %           ;   (   neg(occuring(YEAR))
  844. %               ;   tru(isa(PERSON, mobTaxResidentsFn(iGroup_Canada)))
  845. %               )
  846. %           ;   (   neg(occuring(YEAR))
  847. %               ;   tru(isa(PERSON, mobTaxResidentsFn(iMexico)))
  848. %               )
  849. %           ;   (   neg(occuring(YEAR))
  850. %               ;   tru(isa(PERSON,
  851. %                           mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica)))
  852. %               )
  853. %           ;   tru(forbiddenToDoWrt(iCW_USIncomeTax,
  854. %                                    SUPPORTER,
  855. %                                    claimsAsDependent(YEAR,
  856. %                                                      SUPPORTER,
  857. %                                                      _SUPPORTEE)))
  858. %           )
  859. %       ;   (   neg(occuring(YEAR))
  860. %           ;   tru(isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica)))
  861. %           )
  862. %       ;   (   neg(occuring(YEAR))
  863. %           ;   tru(isa(PERSON, mobTaxResidentsFn(iGroup_Canada)))
  864. %           )
  865. %       ;   (   neg(occuring(YEAR))
  866. %           ;   tru(isa(PERSON, mobTaxResidentsFn(iMexico)))
  867. %           )
  868. %       ;   (   neg(occuring(YEAR))
  869. %           ;   tru(isa(PERSON,
  870. %                       mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica)))
  871. %           )
  872. %       ;   tru(forbiddenToDoWrt(iCW_USIncomeTax,
  873. %                                SUPPORTER,
  874. %                                claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)))
  875. %       ).
  876. % th_nnf_out :-
  877. %       ~ (((n(neg(occuring(YEAR))), n(tru(isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica))))), (n(neg(occuring(YEAR))), n(tru(isa(PERSON, mobTaxResidentsFn(iGroup_Canada))))), (n(neg(occuring(YEAR))), n(tru(isa(PERSON, mobTaxResidentsFn(iMexico))))), (n(neg(occuring(YEAR))), n(tru(isa(PERSON, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica))))), n(tru(forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))))), (n(neg(occuring(YEAR))), n(tru(isa(PERSON, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica))))), (n(neg(occuring(YEAR))), n(tru(isa(PERSON, mobTaxResidentsFn(iGroup_Canada))))), (n(neg(occuring(YEAR))), n(tru(isa(PERSON, mobTaxResidentsFn(iMexico))))), (n(neg(occuring(YEAR))), n(tru(isa(PERSON, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica))))), n(tru(forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))))).
  878. % proven_neg(occuring(YEAR)) :-
  879. %       ~isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA9_VAR),
  880. %       occuring(YEAR),
  881. %       ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA9_VAR),
  882. %       ~isa(PERSON, MOBTAXRESIDENTSFNIMEXICO9_VAR),
  883. %       ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA9_VAR),
  884. %       ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)).
  885. % proven_tru(isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA8_VAR)) :-
  886. %       ignore(mudEquals(TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA8_VAR,
  887. %                        tClazzCitizenFn(iGroup_UnitedStatesOfAmerica))),
  888. %       occuring(YEAR),
  889. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA8_VAR),
  890. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIMEXICO8_VAR),
  891. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA8_VAR),
  892. %       \+ forbiddenToDoWrt(iCW_USIncomeTax,
  893. %                           SUPPORTER,
  894. %                           claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)),
  895. %       \+ isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA8_VAR).
  896. % proven_neg(occuring(YEAR)) :-
  897. %       ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA7_VAR),
  898. %       occuring(YEAR),
  899. %       ~isa(PERSON, MOBTAXRESIDENTSFNIMEXICO7_VAR),
  900. %       ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA7_VAR),
  901. %       ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)),
  902. %       ~isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA7_VAR).
  903. % proven_tru(isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA6_VAR)) :-
  904. %       ignore(mudEquals(MOBTAXRESIDENTSFNIGROUP_CANADA6_VAR,
  905. %                        mobTaxResidentsFn(iGroup_Canada))),
  906. %       occuring(YEAR),
  907. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIMEXICO6_VAR),
  908. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA6_VAR),
  909. %       \+ forbiddenToDoWrt(iCW_USIncomeTax,
  910. %                           SUPPORTER,
  911. %                           claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)),
  912. %       \+ isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA6_VAR),
  913. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA6_VAR).
  914. % proven_neg(occuring(YEAR)) :-
  915. %       ~isa(PERSON, MOBTAXRESIDENTSFNIMEXICO5_VAR),
  916. %       occuring(YEAR),
  917. %       ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA5_VAR),
  918. %       ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)),
  919. %       ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA5_VAR),
  920. %       ~isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA5_VAR).
  921. % proven_tru(isa(PERSON, MOBTAXRESIDENTSFNIMEXICO4_VAR)) :-
  922. %       ignore(mudEquals(MOBTAXRESIDENTSFNIMEXICO4_VAR,
  923. %                        mobTaxResidentsFn(iMexico))),
  924. %       occuring(YEAR),
  925. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA4_VAR),
  926. %       \+ forbiddenToDoWrt(iCW_USIncomeTax,
  927. %                           SUPPORTER,
  928. %                           claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)),
  929. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA4_VAR),
  930. %       \+ isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA4_VAR),
  931. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIMEXICO4_VAR).
  932. % proven_neg(occuring(YEAR)) :-
  933. %       ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA3_VAR),
  934. %       ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)),
  935. %       occuring(YEAR),
  936. %       ~isa(PERSON, MOBTAXRESIDENTSFNIMEXICO3_VAR),
  937. %       ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA3_VAR),
  938. %       ~isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA3_VAR).
  939. % proven_tru(isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA2_VAR)) :-
  940. %       ignore(mudEquals(MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA2_VAR,
  941. %                        mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica))),
  942. %       occuring(YEAR),
  943. %       \+ forbiddenToDoWrt(iCW_USIncomeTax,
  944. %                           SUPPORTER,
  945. %                           claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)),
  946. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIMEXICO2_VAR),
  947. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA2_VAR),
  948. %       \+ isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA2_VAR),
  949. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA2_VAR).
  950. % proven_tru(forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))) :-
  951. %       occuring(YEAR),
  952. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA1_VAR),
  953. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIMEXICO1_VAR),
  954. %       \+ isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA1_VAR),
  955. %       \+ isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA1_VAR),
  956. %       \+ forbiddenToDoWrt(iCW_USIncomeTax,
  957. %                           SUPPORTER,
  958. %                           claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)).
  959. % pfc :-
  960. %       ~isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA9), occuring(YEAR), ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA9), ~isa(PERSON, MOBTAXRESIDENTSFNIMEXICO9), ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA9), ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)), {is_unit(YEAR)}==>proven_neg(occuring(YEAR)).
  961. % pfc :-
  962. %       ignore(mudEquals(TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA8, tClazzCitizenFn(iGroup_UnitedStatesOfAmerica))), occuring(YEAR), \+isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA8), \+isa(PERSON, MOBTAXRESIDENTSFNIMEXICO8), \+isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA8), \+forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)), \+isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA8), {is_unit(TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA8, PERSON)}==>proven_tru(isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA8)).
  963. % pfc :-
  964. %       ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA7), occuring(YEAR), ~isa(PERSON, MOBTAXRESIDENTSFNIMEXICO7), ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA7), ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)), ~isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA7), {is_unit(YEAR)}==>proven_neg(occuring(YEAR)).
  965. % pfc :-
  966. %       ignore(mudEquals(MOBTAXRESIDENTSFNIGROUP_CANADA6, mobTaxResidentsFn(iGroup_Canada))), occuring(YEAR), \+isa(PERSON, MOBTAXRESIDENTSFNIMEXICO6), \+isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA6), \+forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)), \+isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA6), \+isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA6), {is_unit(MOBTAXRESIDENTSFNIGROUP_CANADA6, PERSON)}==>proven_tru(isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA6)).
  967. % pfc :-
  968. %       ~isa(PERSON, MOBTAXRESIDENTSFNIMEXICO5), occuring(YEAR), ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA5), ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)), ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA5), ~isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA5), {is_unit(YEAR)}==>proven_neg(occuring(YEAR)).
  969. % pfc :-
  970. %       ignore(mudEquals(MOBTAXRESIDENTSFNIMEXICO4, mobTaxResidentsFn(iMexico))), occuring(YEAR), \+isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA4), \+forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)), \+isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA4), \+isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA4), \+isa(PERSON, MOBTAXRESIDENTSFNIMEXICO4), {is_unit(MOBTAXRESIDENTSFNIMEXICO4, PERSON)}==>proven_tru(isa(PERSON, MOBTAXRESIDENTSFNIMEXICO4)).
  971. % pfc :-
  972. %       ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA3), ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)), occuring(YEAR), ~isa(PERSON, MOBTAXRESIDENTSFNIMEXICO3), ~isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA3), ~isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA3), {is_unit(YEAR)}==>proven_neg(occuring(YEAR)).
  973. % pfc :-
  974. %       ignore(mudEquals(MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA2, mobTaxResidentsFn(iGroup_UnitedStatesOfAmerica))), occuring(YEAR), \+forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)), \+isa(PERSON, MOBTAXRESIDENTSFNIMEXICO2), \+isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA2), \+isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA2), \+isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA2), {is_unit(MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA2, PERSON)}==>proven_tru(isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA2)).
  975. % pfc :-
  976. %       occuring(YEAR), \+isa(PERSON, MOBTAXRESIDENTSFNIGROUP_UNITEDSTATESOFAMERICA1), \+isa(PERSON, MOBTAXRESIDENTSFNIMEXICO1), \+isa(PERSON, MOBTAXRESIDENTSFNIGROUP_CANADA1), \+isa(PERSON, TCLAZZCITIZENFNIGROUP_UNITEDSTATESOFAMERICA1), \+forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)), {is_unit(SUPPORTER, _SUPPORTEE, YEAR)}==>proven_tru(forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE))).
  977. */
  978.  
  979.  
  980.  
  981. % ~occuring(YEAR) :-
  982. %       ~instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)),
  983. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)),
  984. %       \+ ( ( forbiddenToDoWrt(iCW_USIncomeTax,
  985. %                               SUPPORTER,
  986. %                               claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)),
  987. %              instance(PERSON,
  988. %                  nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica))
  989. %            ),
  990. %            instance(PERSON, nartR(mobTaxResidentsFn, iMexico))
  991. %          ).
  992. % instance(PERSON, nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica)) :-
  993. %       occuring(YEAR),
  994. %       ~instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)),
  995. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)),
  996. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iMexico)),
  997. %       \+ ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)).
  998. % instance(PERSON, nartR(mobTaxResidentsFn, iMexico)) :-
  999. %       occuring(YEAR),
  1000. %       ~instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)),
  1001. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)),
  1002. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica)),
  1003. %       \+ ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)).
  1004. % instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)) :-
  1005. %       occuring(YEAR),
  1006. %       ~instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)),
  1007. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iMexico)),
  1008. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica)),
  1009. %       \+ ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)).
  1010. % instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)) :-
  1011. %       occuring(YEAR),
  1012. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)),
  1013. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iMexico)),
  1014. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica)),
  1015. %       \+ ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)).
  1016. % forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)) :-
  1017. %       occuring(YEAR),
  1018. %       ~instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)),
  1019. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)),
  1020. %       ~instance(PERSON, nartR(mobTaxResidentsFn, iMexico)),
  1021. %       \+ ~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica)).
  1022.  
  1023.  
  1024. % ================================================================================================================
  1025. %  Everything is human or god
  1026. % ================================================================================================================
  1027.  
  1028. :- test_boxlog(human(X)v god(X)).
  1029.  
  1030.  /*
  1031. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:276
  1032. % :- test_boxlog(human(X_VAR)v god(X_VAR)).
  1033. % kif :-
  1034. %       all(X, human(X)v god(X)).
  1035. % qualify_nesc :-
  1036. %       all(X,  (~nesc(human(X)v god(X))=>nesc(human(X)v god(X)))).
  1037. % debugm(user, sc_success(user, user:nnf(KB, all(X,  (~nesc(human(X)v god(X))=>nesc(b_d(KB, nesc, poss), human(X)v god(X)))), nesc(b_d(KB, nesc, poss), human(X)v god(X))v nesc(b_d(KB, nesc, poss), human(X)v god(X))))).
  1038. % nnf :-
  1039. %       nesc(human(X)v god(X))v nesc(human(X)v god(X)).
  1040. % th_nnf_in :-
  1041. %       (   (   tru(human(X))
  1042. %           ;   tru(god(X))
  1043. %           )
  1044. %       ;   tru(human(X))
  1045. %       ;   tru(god(X))
  1046. %       ).
  1047. % th_nnf_out :-
  1048. %       ~ ((n(tru(human(X))), n(tru(god(X)))), n(tru(human(X))), n(tru(god(X)))).
  1049. % proven_tru(human(X)) :-
  1050. %       \+ god(X),
  1051. %       \+ human(X).
  1052. % proven_tru(god(X)) :-
  1053. %       \+ human(X),
  1054. %       \+ god(X).
  1055. % pfc :-
  1056. %       \+god(X), \+human(X), {is_unit(X)}==>proven_tru(human(X)).
  1057. % pfc :-
  1058. %       \+human(X), \+god(X), {is_unit(X)}==>proven_tru(god(X)).
  1059. */
  1060.  
  1061. % human(_19658) :-
  1062. %       ~god(_19658).
  1063. % god(_23530) :-
  1064. %       ~human(_23530).
  1065.  
  1066.  
  1067.  
  1068. % ================================================================================================================
  1069. %  Everything that is human is possibly male
  1070. % ================================================================================================================
  1071.  
  1072.  
  1073. :- test_boxlog((human(X)=>poss(male(X)))).
  1074.  
  1075.  /*
  1076. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:288
  1077. % :- test_boxlog((human(X_VAR)=>poss(male(X_VAR)))).
  1078. % debugm(user, sc_success(user, user:nnf(KB, all(X,  (human(X)=>poss(b_d(KB, nesc, poss), male(X)))), ~human(X)v poss(b_d(KB, nesc, poss), male(X))))).
  1079. % nnf :-
  1080. %       ~human(X)v poss(male(X)).
  1081. % th_nnf_in :-
  1082. %       (   neg(human(X))
  1083. %       ;   poss(male(X))
  1084. %       ).
  1085. % th_nnf_out :-
  1086. %       ~ (n(neg(human(X))), n(poss(male(X)))).
  1087. % proven_neg(human(X)) :-
  1088. %       proven_not_poss(male(X)).
  1089. % proven_poss(male(X)) :-
  1090. %       poss(human(X)).
  1091. % pfc :-
  1092. %       proven_not_poss(male(X)), {is_unit(X)}==>proven_neg(human(X)).
  1093. % pfc :-
  1094. %       poss(human(X)), {is_unit(X)}==>proven_poss(male(X)).
  1095. */
  1096.  
  1097.  
  1098. % ~(human(X)) :-
  1099. %       ~poss_t(male, X).
  1100. % proven_tru(poss_t(male, X)) :-
  1101. %       human(X).
  1102.  
  1103.  
  1104. % ================================================================================================================
  1105. %  Everything is human and male
  1106. % ================================================================================================================
  1107.  
  1108. %  BAD!! these need co-mingled!
  1109.  
  1110. :- test_boxlog(human(X)&male(X)).
  1111.  
  1112.  /*
  1113. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:301
  1114. % :- test_boxlog(human(X_VAR)&male(X_VAR)).
  1115. % kif :-
  1116. %       all(X, human(X)&male(X)).
  1117. % qualify_nesc :-
  1118. %       all(X,  (~nesc(human(X)&male(X))=>nesc(human(X)&male(X)))).
  1119. % debugm(user, sc_success(user, user:nnf(KB, all(X,  (~nesc(human(X)&male(X))=>nesc(b_d(KB, nesc, poss), human(X)&male(X)))), nesc(b_d(KB, nesc, poss), human(X))&nesc(b_d(KB, nesc, poss), male(X))v(nesc(b_d(KB, nesc, poss), human(X))&nesc(b_d(KB, nesc, poss), male(X)))))).
  1120. % nnf :-
  1121. %       nesc(human(X))&nesc(male(X))v(nesc(human(X))&nesc(male(X))).
  1122. % th_nnf_in :-
  1123. %       (   tru(human(X)),
  1124. %           tru(male(X))
  1125. %       ;   tru(human(X)),
  1126. %           tru(male(X))
  1127. %       ).
  1128. % th_nnf_out :-
  1129. %       ~ ((n(tru(human(X)));n(tru(male(X)))), (n(tru(human(X)));n(tru(male(X))))).
  1130. % proven_tru(human(X)) :-
  1131. %       (   \+ human(X)
  1132. %       ;   \+ male(X)
  1133. %       ).
  1134. % proven_tru(male(X)) :-
  1135. %       (   \+ human(X)
  1136. %       ;   \+ male(X)
  1137. %       ).
  1138. % pfc :-
  1139. %       (\+human(X);\+male(X)), {is_unit(X)}==>proven_tru(human(X)).
  1140. % pfc :-
  1141. %       (\+human(X);\+male(X)), {is_unit(X)}==>proven_tru(male(X)).
  1142. */
  1143.  
  1144.  
  1145. % human(_21936).
  1146. % male(_24006).
  1147.  
  1148.  
  1149.  
  1150.  
  1151. % =======
  1152. %  Co-mingled!
  1153. % =======
  1154.  
  1155. :- P=human(X)&male(X),
  1156.    test_boxlog((poss(P)=>P)).
  1157.  
  1158.  /*
  1159. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:312
  1160. % :- test_boxlog((poss(human(X_VAR)&male(X_VAR))=>human(X_VAR)&male(X_VAR))).
  1161. % debugm(user, sc_success(user, user:nnf(KB, all(X,  (poss(b_d(KB, nesc, poss), human(X)&male(X))=>human(X)&male(X))), nesc(b_d(KB, nesc, poss), ~human(X)v~male(X))v(human(X)&male(X))))).
  1162. % nnf :-
  1163. %       nesc(~human(X)v~male(X))v(human(X)&male(X)).
  1164. % th_nnf_in :-
  1165. %       (   (   neg(human(X))
  1166. %           ;   neg(male(X))
  1167. %           )
  1168. %       ;   tru(human(X)),
  1169. %           tru(male(X))
  1170. %       ).
  1171. % th_nnf_out :-
  1172. %       ~ ((n(neg(human(X))), n(neg(male(X)))), (n(tru(human(X)));n(tru(male(X))))).
  1173. % proven_neg(human(X)) :-
  1174. %       naf(human(X)).
  1175. % proven_neg(male(X)) :-
  1176. %       naf(male(X)).
  1177. % proven_tru(human(X)) :-
  1178. %       male(X),
  1179. %       poss(human(X)).
  1180. % proven_tru(male(X)) :-
  1181. %       human(X),
  1182. %       poss(male(X)).
  1183. % pfc :-
  1184. %       naf(human(X)), {is_unit(X)}==>proven_neg(human(X)).
  1185. % pfc :-
  1186. %       naf(male(X)), {is_unit(X)}==>proven_neg(male(X)).
  1187. % pfc :-
  1188. %       male(X), poss(human(X)), {is_unit(X)}==>proven_tru(human(X)).
  1189. % pfc :-
  1190. %       human(X), poss(male(X)), {is_unit(X)}==>proven_tru(male(X)).
  1191. */
  1192.  
  1193.  
  1194. % human(X) :-
  1195. %       \+ ~human(X),
  1196. %       \+ ~male(X).
  1197. % male(X) :-
  1198. %       \+ ~human(X),
  1199. %       \+ ~male(X).
  1200.  
  1201.  
  1202. % These to?
  1203. % ~human(A) :-
  1204. %      \+ ( \+ ~male(A),
  1205. %           human(A)
  1206. %         ).
  1207. % ~human(A) :-
  1208. %      \+ ( \+ ~male(A),
  1209. %           male(A)
  1210. %         ).
  1211. % ~male(A) :-
  1212. %      \+ ( \+ ~human(A),
  1213. %           human(A)
  1214. %         ).
  1215. % ~male(A) :-
  1216. %      \+ ( \+ ~human(A),
  1217. %           male(A)
  1218. %         ).
  1219.  
  1220.  
  1221.  
  1222.  
  1223. % ================================================================================================================
  1224. %  Nothing is both human and god
  1225. % ================================================================================================================
  1226.  
  1227. :- test_boxlog(~ (human(X)&god(X))).
  1228.  
  1229.  /*
  1230. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:346
  1231. % :- test_boxlog(~ (human(X_VAR)&god(X_VAR))).
  1232. % kif :-
  1233. %       all(X, ~ (human(X)&god(X))).
  1234. % qualify_nesc :-
  1235. %       all(X, nesc(~ (human(X)&god(X)))).
  1236. % debugm(user, sc_success(user, user:nnf(KB, all(X, nesc(b_d(KB, nesc, poss), ~ (human(X)&god(X)))), nesc(b_d(KB, nesc, poss), ~human(X)v~god(X))))).
  1237. % nnf :-
  1238. %       nesc(~human(X)v~god(X)).
  1239. % th_nnf_in :-
  1240. %       (   neg(human(X))
  1241. %       ;   neg(god(X))
  1242. %       ).
  1243. % th_nnf_out :-
  1244. %       ~ (n(neg(human(X))), n(neg(god(X)))).
  1245. % proven_neg(human(X)) :-
  1246. %       god(X).
  1247. % proven_neg(god(X)) :-
  1248. %       human(X).
  1249. % pfc :-
  1250. %       god(X), {is_unit(X)}==>proven_neg(human(X)).
  1251. % pfc :-
  1252. %       human(X), {is_unit(X)}==>proven_neg(god(X)).
  1253. */
  1254.  
  1255.  
  1256. % ~human(_830) :-
  1257. %       god(_830).
  1258. % ~god(_904) :-
  1259. %       human(_904).
  1260.  
  1261. % ================================================================================================================
  1262. %  There exists something not evil
  1263. % ================================================================================================================
  1264.  
  1265. :- test_boxlog(exists(X, ~evil(X))).
  1266.  
  1267.  /*
  1268. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:356
  1269. % :- test_boxlog(exists(X_VAR, ~evil(X_VAR))).
  1270. % kif :-
  1271. %       exists(X, ~evil(X)).
  1272. % qualify_nesc :-
  1273. %       exists(X, nesc(~evil(X))).
  1274. % debugm(user, sc_success(user, user:nnf(KB, exists(X, nesc(b_d(KB, nesc, poss), ~evil(X))), nesc(b_d(KB, nesc, poss), ~evil(X))v~skolem(X, skFn(nesc(b_d(KB, nesc, poss), ~evil(X))))))).
  1275. % nnf :-
  1276. %       nesc(~evil(X))v~skolem(X, skFn(nesc(~evil(X)))).
  1277. % th_nnf_in :-
  1278. %       (   neg(evil(X))
  1279. %       ;   neg(skolem(X, skFn(nesc(~evil(X)))))
  1280. %       ).
  1281. % th_nnf_out :-
  1282. %       ~ (n(neg(evil(X))), n(neg(skolem(X, skFn(nesc(~evil(X))))))).
  1283. % proven_neg(evil(X)) :-
  1284. %       skolem(X, skFn(nesc(~evil(X)))).
  1285. % proven_neg(skolem(X, skFn(nesc(~evil(X))))) :-
  1286. %       evil(X).
  1287. % pfc :-
  1288. %       if_missing(if_missing(proven_neg(evil(_1223194)),
  1289. %                             proven_neg(evil(skFn(nesc(~evil(X)))))),
  1290. %                  if_missing(proven_neg(evil(_1223194)),
  1291. %                             proven_neg(evil(skFn(nesc(~evil(skFn(nesc(~evil(X)))))))))).
  1292. % pfc :-
  1293. %       evil(X), {is_unit(X)}==>if_missing(proven_neg(skolem(_1240538, skFn(nesc(~evil(_1240538))))), proven_neg(skolem(skFn(nesc(~evil(X))), skFn(nesc(~evil(skFn(nesc(~evil(X))))))))).
  1294. */
  1295.  
  1296.  
  1297. % ~evil(_788{sk = ...}) :-
  1298. %       skolem(_788{sk = ...}, skIsIn_8Fn).
  1299.  
  1300. % ================================================================================================================
  1301. %  There exists something evil
  1302. % ================================================================================================================
  1303.  
  1304. :- test_boxlog(exists(X, evil(X))).
  1305.  
  1306.  /*
  1307. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:364
  1308. % :- test_boxlog(exists(X_VAR, evil(X_VAR))).
  1309. % kif :-
  1310. %       exists(X, evil(X)).
  1311. % qualify_nesc :-
  1312. %       exists(X, nesc(evil(X))).
  1313. % debugm(user, sc_success(user, user:nnf(KB, exists(X, nesc(b_d(KB, nesc, poss), evil(X))), nesc(b_d(KB, nesc, poss), evil(X))v~skolem(X, skFn(nesc(b_d(KB, nesc, poss), evil(X))))))).
  1314. % nnf :-
  1315. %       nesc(evil(X))v~skolem(X, skFn(nesc(evil(X)))).
  1316. % th_nnf_in :-
  1317. %       (   tru(evil(X))
  1318. %       ;   neg(skolem(X, skFn(nesc(evil(X)))))
  1319. %       ).
  1320. % th_nnf_out :-
  1321. %       ~ (n(tru(evil(X))), n(neg(skolem(X, skFn(nesc(evil(X))))))).
  1322. % proven_tru(evil(X)) :-
  1323. %       skolem(X, skFn(nesc(evil(X)))).
  1324. % proven_neg(skolem(X, skFn(nesc(evil(X))))) :-
  1325. %       ~evil(X).
  1326. % pfc :-
  1327. %       if_missing(if_missing(proven_tru(evil(_1314492)),
  1328. %                             proven_tru(evil(skFn(nesc(evil(X)))))),
  1329. %                  if_missing(proven_tru(evil(_1314492)),
  1330. %                             proven_tru(evil(skFn(nesc(evil(skFn(nesc(evil(X)))))))))).
  1331. % pfc :-
  1332. %       ~evil(X), {is_unit(X)}==>if_missing(proven_neg(skolem(_1330982, skFn(nesc(evil(_1330982))))), proven_neg(skolem(skFn(nesc(evil(X))), skFn(nesc(evil(skFn(nesc(evil(X))))))))).
  1333. */
  1334.  
  1335. % evil(_788{sk = ...}) :-
  1336. %       skolem(_788{sk = ...}, skIsIn_9Fn).
  1337.  
  1338. % ================================================================================================================
  1339. %  When a man exists there will be a god
  1340. % ================================================================================================================
  1341.  
  1342. :- test_boxlog((exists(X, man(X))=>exists(G, god(G)))).
  1343.  
  1344.  /*
  1345. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:371
  1346. % :- test_boxlog((exists(X_VAR, man(X_VAR))=>exists(G_VAR, god(G_VAR)))).
  1347. % kif :-
  1348. %       exists(X, man(X))=>exists(G, god(G)).
  1349. % qualify_nesc :-
  1350. %       nesc((exists(X, man(X))=>exists(G, god(G)))).
  1351. % debugm(user, sc_success(user, user:nnf(KB, nesc(b_d(KB, nesc, poss),  (exists(X, man(X))=>exists(G, god(G)))), nesc(b_d(KB, nesc, poss), ~man(X)v(god(G)v~skolem(G, skFn(god(G)))))))).
  1352. % nnf :-
  1353. %       nesc(~man(X)v(god(G)v~skolem(G, skFn(god(G))))).
  1354. % th_nnf_in :-
  1355. %       (   neg(man(X))
  1356. %       ;   tru(god(G))
  1357. %       ;   neg(skolem(G, skFn(god(G))))
  1358. %       ).
  1359. % th_nnf_out :-
  1360. %       ~ (n(neg(man(X))), n(tru(god(G))), n(neg(skolem(G, skFn(god(G)))))).
  1361. % proven_neg(man(X)) :-
  1362. %       ~god(G),
  1363. %       skolem(G, skFn(god(G))).
  1364. % proven_tru(god(G)) :-
  1365. %       man(X),
  1366. %       skolem(G, skFn(god(G))).
  1367. % proven_neg(skolem(G, skFn(god(G)))) :-
  1368. %       ~god(G),
  1369. %       man(X).
  1370. % pfc :-
  1371. %       ~god(G), {ignore(G=skFn(god(G)))}, {is_unit}==>proven_neg(man(X)).
  1372. % pfc :-
  1373. %       man(X), {is_unit}==>if_missing(if_missing(proven_tru(god(_1429242)), proven_tru(god(skFn(god(G))))), if_missing(proven_tru(god(_1429242)), proven_tru(god(skFn(god(skFn(god(G)))))))).
  1374. % pfc :-
  1375. %       ~god(G), man(X), {is_unit(G)}==>if_missing(proven_neg(skolem(_1444024, skFn(god(_1444024)))), proven_neg(skolem(skFn(god(G)), skFn(god(skFn(god(G))))))).
  1376. */
  1377.  
  1378. % god(_866{sk = ...}) :-
  1379. %       man(_1082),
  1380. %       skolem(_866{sk = ...}, skIsGodIn_1Fn(_1082)).
  1381. % ~man(_2276) :-
  1382. %       \+ ( skolem(_896{sk = ...}, skIsGodIn_1Fn(_2276)),
  1383. %            god(_896{sk = ...})
  1384. %          ).
  1385.  
  1386. % this would be better though if
  1387. % god(_866{sk = ...}) :-
  1388. %       \= \+ (man(_1082)),
  1389. %       skolem(_866{sk = ...}, skIsGodIn_1Fn).
  1390. % ~man(_2276) :-
  1391. %       \+ god(_896).
  1392.  
  1393.  
  1394. % ================================================================================================================
  1395. %  When two men exists there will be a god
  1396. % ================================================================================================================
  1397.  
  1398. :- test_boxlog((atleast(2, X, man(X))=>exists(G, god(G)))).
  1399.  
  1400.  /*
  1401. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:391
  1402. % :- test_boxlog((atleast(2, X_VAR, man(X_VAR))=>exists(G_VAR, god(G_VAR)))).
  1403. % kif :-
  1404. %       all(X,  (atleast(2, X, man(X))=>exists(G, god(G)))).
  1405. % qualify_nesc :-
  1406. %       all(X, nesc((atleast(2, X, man(X))=>exists(G, god(G))))).
  1407. % debugm(user, sc_success(user, user:nnf(KB, all(X, nesc(b_d(KB, nesc, poss),  (atleast(2, X, man(X))=>exists(G, god(G))))), nesc(b_d(KB, nesc, poss), god(G)v~skolem(G, skFn(god(G)))v(~man(_2068)v(~different(X, _2192)v(~man(X)v~different(X, _2068)v(~man(_2192)v~different(X, _2068))))))))).
  1408. % nnf :-
  1409. %       nesc(god(G)v~skolem(G, skFn(god(G)))v(~man(_2068)v(~different(X, _2192)v(~man(X)v~different(X, _2068)v(~man(_2192)v~different(X, _2068)))))).
  1410. % th_nnf_in :-
  1411. %       (   (   tru(god(G))
  1412. %           ;   neg(skolem(G, skFn(god(G))))
  1413. %           )
  1414. %       ;   neg(man(_2068))
  1415. %       ;   neg(different(X, _2192))
  1416. %       ;   (   neg(man(X))
  1417. %           ;   neg(different(X, _2068))
  1418. %           )
  1419. %       ;   neg(man(_2192))
  1420. %       ;   neg(different(X, _2068))
  1421. %       ).
  1422. % th_nnf_out :-
  1423. %       ~ ((n(tru(god(G))), n(neg(skolem(G, skFn(god(G)))))), n(neg(man(_2068))), n(neg(different(X, _2192))), (n(neg(man(X))), n(neg(different(X, _2068)))), n(neg(man(_2192))), n(neg(different(X, _2068)))).
  1424. % proven_tru(god(G)) :-
  1425. %       man(_2068),
  1426. %       different(X, _2192),
  1427. %       man(X),
  1428. %       different(X, _2068),
  1429. %       man(_2192),
  1430. %       skolem(G, skFn(god(G))).
  1431. % proven_neg(skolem(G, skFn(god(G)))) :-
  1432. %       ~god(G),
  1433. %       man(_2068),
  1434. %       different(X, _2192),
  1435. %       man(X),
  1436. %       different(X, _2068),
  1437. %       man(_2192).
  1438. % proven_neg(man(_2068)) :-
  1439. %       different(X, _2192),
  1440. %       man(X),
  1441. %       different(X, _2068),
  1442. %       man(_2192),
  1443. %       ~god(G),
  1444. %       skolem(G, skFn(god(G))).
  1445. % proven_neg(different(X, _2192)) :-
  1446. %       man(X),
  1447. %       different(X, _2068),
  1448. %       man(_2192),
  1449. %       man(_2068),
  1450. %       ~god(G),
  1451. %       skolem(G, skFn(god(G))).
  1452. % proven_neg(man(X)) :-
  1453. %       different(X, _2068),
  1454. %       man(_2192),
  1455. %       different(X, _2192),
  1456. %       man(_2068),
  1457. %       ~god(G),
  1458. %       skolem(G, skFn(god(G))).
  1459. % proven_neg(different(X, _2068)) :-
  1460. %       man(X),
  1461. %       man(_2192),
  1462. %       different(X, _2068),
  1463. %       different(X, _2192),
  1464. %       man(_2068),
  1465. %       ~god(G),
  1466. %       skolem(G, skFn(god(G))).
  1467. % proven_neg(man(_2192)) :-
  1468. %       different(X, _2068),
  1469. %       man(X),
  1470. %       different(X, _2192),
  1471. %       man(_2068),
  1472. %       ~god(G),
  1473. %       skolem(G, skFn(god(G))).
  1474. % proven_neg(different(X, _2068)) :-
  1475. %       man(_2192),
  1476. %       man(X),
  1477. %       different(X, _2068),
  1478. %       different(X, _2192),
  1479. %       man(_2068),
  1480. %       ~god(G),
  1481. %       skolem(G, skFn(god(G))).
  1482. % pfc :-
  1483. %       man(_2068), {dif:dif(X, _2192)}, man(X), {dif:dif(X, _2068)}, man(_2192), {is_unit}==>if_missing(if_missing(proven_tru(god(_113446)), proven_tru(god(skFn(god(G))))), if_missing(proven_tru(god(_113446)), proven_tru(god(skFn(god(skFn(god(G)))))))).
  1484. % pfc :-
  1485. %       ~god(G), man(_2068), {dif:dif(X, _2192)}, man(X), {dif:dif(X, _2068)}, man(_2192), {is_unit(G)}==>if_missing(proven_neg(skolem(_136182, skFn(god(_136182)))), proven_neg(skolem(skFn(god(G)), skFn(god(skFn(god(G))))))).
  1486. % pfc :-
  1487. %       {dif:dif(X, _2192)}, man(X), {dif:dif(X, _2068)}, man(_2192), ~god(G), {ignore(G=skFn(god(G)))}, {is_unit(_2068)}==>proven_neg(man(_2068)).
  1488. % pfc :-
  1489. %       man(X), {dif:dif(X, _2068)}, man(_2192), man(_2068), ~god(G), {ignore(G=skFn(god(G)))}, {is_unit(_2192, X)}==>proven_neg(different(X, _2192)).
  1490. % pfc :-
  1491. %       {dif:dif(X, _2068)}, man(_2192), {dif:dif(X, _2192)}, man(_2068), ~god(G), {ignore(G=skFn(god(G)))}, {is_unit(X)}==>proven_neg(man(X)).
  1492. % pfc :-
  1493. %       man(X), man(_2192), {dif:dif(X, _2068), dif:dif(X, _2192)}, man(_2068), ~god(G), {ignore(G=skFn(god(G)))}, {is_unit(_2068, X)}==>proven_neg(different(X, _2068)).
  1494. % pfc :-
  1495. %       {dif:dif(X, _2068)}, man(X), {dif:dif(X, _2192)}, man(_2068), ~god(G), {ignore(G=skFn(god(G)))}, {is_unit(_2192)}==>proven_neg(man(_2192)).
  1496. % pfc :-
  1497. %       man(_2192), man(X), {dif:dif(X, _2068), dif:dif(X, _2192)}, man(_2068), ~god(G), {ignore(G=skFn(god(G)))}, {is_unit(_2068, X)}==>proven_neg(different(X, _2068)).
  1498. */
  1499.  
  1500.  
  1501. % god(_1298{sk = ...}) :-
  1502. %       skolem(_1358{sk = ...}, skIsManIn_1Fn(_10978, _1298{sk = ...})),
  1503. %       ~man(_1358{sk = ...}),
  1504. %       skolem(_1298{sk = ...}, skIsGodIn_2Fn(_10978)).
  1505. % god(_3110{sk = ...}) :-
  1506. %       man(_11144),
  1507. %       man(_11166),
  1508. %       skolem(_3110{sk = ...}, skIsGodIn_2Fn(_11166)).
  1509. % man(_2204{sk = ...}) :-
  1510. %       skolem(_2204{sk = ...}, skIsManIn_1Fn(_11314, _2224{sk = ...})),
  1511. %       skolem(_2224{sk = ...}, skIsGodIn_2Fn(_11314)),
  1512. %       \+ ~god(_2224{sk = ...}).
  1513. % ~man(_11494) :-
  1514. %       \+ ( man(_11516),
  1515. %            naf(~skolem(_4090{sk = ...}, skIsGodIn_2Fn(_11494))),
  1516. %            god(_4090{sk = ...})
  1517. %          ).
  1518. % ~man(_11656) :-
  1519. %       \+ ( man(_11678),
  1520. %            naf(~skolem(_4504{sk = ...}, skIsGodIn_2Fn(_11678))),
  1521. %            god(_4504{sk = ...})
  1522. %          ).
  1523.  
  1524.  
  1525. % OR?
  1526.  
  1527.  
  1528. % god(G) :-
  1529. %       skolem(_1316_sk, skIsManIn_1Fn(X, G)),
  1530. %       ~man(_1316_sk),
  1531. %       skolem(G, skIsGodIn_1Fn(X)).
  1532. % god(G) :-
  1533. %       man(_2720),
  1534. %       ~equals(_2742, X),
  1535. %       man(X),
  1536. %       skolem(G, skIsGodIn_1Fn(X)).
  1537. % man(_1342_sk) :-
  1538. %       skolem(_1342_sk, skIsManIn_1Fn(X, G)),
  1539. %       skolem(G, skIsGodIn_1Fn(X)),
  1540. %       \+ ~god(G).
  1541. % naf(~equals(_3108, X)) :-
  1542. %       man(_3148),
  1543. %       man(X),
  1544. %       skolem(G, skIsGodIn_1Fn(X)),
  1545. %       \+ ~god(G).
  1546. % ~man(X) :-
  1547. %       man(_3330),
  1548. %       \+ ( \+ ~ (~equals(_3352, X)),
  1549. %            naf(~skolem(G, skIsGodIn_1Fn(X))),
  1550. %            god(G)
  1551. %          ).
  1552. % ~man(_3544) :-
  1553. %       ~equals(_3566, X),
  1554. %       \+ ( man(X),
  1555. %            naf(~skolem(G, skIsGodIn_1Fn(X))),
  1556. %            god(G)
  1557. %          ).
  1558. % ~equals(_1478_sk, X) :-
  1559. %       \+ ( skolem(G, skIsGodIn_1Fn(X)),
  1560. %            god(G)
  1561. %          ).
  1562.  
  1563.  
  1564. % ================================================================================================================
  1565. % A person holding a bird is performing bird holding
  1566. % ================================================================================================================
  1567.  
  1568.  
  1569. :- test_boxlog(implies(and(instance(HOLD, actHoldingAnObject),
  1570.                            objectActedOn(HOLD, BIRD),
  1571.                            instance(BIRD, tClazzBird),
  1572.                            performedBy(HOLD, PER),
  1573.                            instance(PER, mobPerson)),
  1574.                        holdsIn(HOLD, onPhysical(BIRD, PER))),
  1575.                O),
  1576.    maplist(wdmsg, O).
  1577.  
  1578.  /*
  1579. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:460
  1580. % kif :-
  1581. %       all(HOLD,
  1582. %           all(BIRD,
  1583. %               all(PER,
  1584. %                   (actHoldingAnObject(HOLD)&(objectActedOn(HOLD, BIRD)&(tClazzBird(BIRD)&(performedBy(HOLD, PER)&mobPerson(PER))))=>holdsIn(HOLD, onPhysical(BIRD, PER)))))).
  1585. % qualify_nesc :-
  1586. %       all(HOLD,
  1587. %           all(BIRD,
  1588. %               all(PER,
  1589. %                   nesc((actHoldingAnObject(HOLD)&(objectActedOn(HOLD, BIRD)&(tClazzBird(BIRD)&(performedBy(HOLD, PER)&mobPerson(PER))))=>holdsIn(HOLD, onPhysical(BIRD, PER))))))).
  1590. % debugm(user, sc_success(user, user:nnf(KB, all(HOLD, all(BIRD, all(PER, nesc(b_d(KB, nesc, poss),  (actHoldingAnObject(HOLD)&(objectActedOn(HOLD, BIRD)&(tClazzBird(BIRD)&(performedBy(HOLD, PER)&mobPerson(PER))))=>holdsIn(HOLD, onPhysical(BIRD, PER))))))), nesc(b_d(KB, nesc, poss), ~actHoldingAnObject(HOLD)v(~objectActedOn(HOLD, BIRD)v(~tClazzBird(BIRD)v(~performedBy(HOLD, PER)v~mobPerson(PER))))v(~occuring(HOLD)v onPhysical(BIRD, PER)))))).
  1591. % nnf :-
  1592. %       nesc(~actHoldingAnObject(HOLD)v(~objectActedOn(HOLD, BIRD)v(~tClazzBird(BIRD)v(~performedBy(HOLD, PER)v~mobPerson(PER))))v(~occuring(HOLD)v onPhysical(BIRD, PER))).
  1593. % th_nnf_in :-
  1594. %       (   (   neg(actHoldingAnObject(HOLD))
  1595. %           ;   neg(objectActedOn(HOLD, BIRD))
  1596. %           ;   neg(tClazzBird(BIRD))
  1597. %           ;   neg(performedBy(HOLD, PER))
  1598. %           ;   neg(mobPerson(PER))
  1599. %           )
  1600. %       ;   neg(occuring(HOLD))
  1601. %       ;   tru(onPhysical(BIRD, PER))
  1602. %       ).
  1603. % th_nnf_out :-
  1604. %       ~ ((n(neg(actHoldingAnObject(HOLD))), n(neg(objectActedOn(HOLD, BIRD))), n(neg(tClazzBird(BIRD))), n(neg(performedBy(HOLD, PER))), n(neg(mobPerson(PER)))), n(neg(occuring(HOLD))), n(tru(onPhysical(BIRD, PER)))).
  1605. % proven_neg(actHoldingAnObject(HOLD)) :-
  1606. %       objectActedOn(HOLD, BIRD),
  1607. %       tClazzBird(BIRD),
  1608. %       performedBy(HOLD, PER),
  1609. %       mobPerson(PER),
  1610. %       occuring(HOLD),
  1611. %       ~onPhysical(BIRD, PER).
  1612. % proven_neg(objectActedOn(HOLD, BIRD)) :-
  1613. %       tClazzBird(BIRD),
  1614. %       performedBy(HOLD, PER),
  1615. %       mobPerson(PER),
  1616. %       actHoldingAnObject(HOLD),
  1617. %       occuring(HOLD),
  1618. %       ~onPhysical(BIRD, PER).
  1619. % proven_neg(tClazzBird(BIRD)) :-
  1620. %       performedBy(HOLD, PER),
  1621. %       mobPerson(PER),
  1622. %       objectActedOn(HOLD, BIRD),
  1623. %       actHoldingAnObject(HOLD),
  1624. %       occuring(HOLD),
  1625. %       ~onPhysical(BIRD, PER).
  1626. % proven_neg(performedBy(HOLD, PER)) :-
  1627. %       mobPerson(PER),
  1628. %       tClazzBird(BIRD),
  1629. %       objectActedOn(HOLD, BIRD),
  1630. %       actHoldingAnObject(HOLD),
  1631. %       occuring(HOLD),
  1632. %       ~onPhysical(BIRD, PER).
  1633. % proven_neg(mobPerson(PER)) :-
  1634. %       performedBy(HOLD, PER),
  1635. %       tClazzBird(BIRD),
  1636. %       objectActedOn(HOLD, BIRD),
  1637. %       actHoldingAnObject(HOLD),
  1638. %       occuring(HOLD),
  1639. %       ~onPhysical(BIRD, PER).
  1640. % proven_neg(occuring(HOLD)) :-
  1641. %       ~onPhysical(BIRD, PER),
  1642. %       actHoldingAnObject(HOLD),
  1643. %       objectActedOn(HOLD, BIRD),
  1644. %       tClazzBird(BIRD),
  1645. %       performedBy(HOLD, PER),
  1646. %       mobPerson(PER).
  1647. % proven_tru(onPhysical(BIRD, PER)) :-
  1648. %       occuring(HOLD),
  1649. %       actHoldingAnObject(HOLD),
  1650. %       objectActedOn(HOLD, BIRD),
  1651. %       tClazzBird(BIRD),
  1652. %       performedBy(HOLD, PER),
  1653. %       mobPerson(PER).
  1654. */
  1655.  
  1656.  
  1657. % ~occuring(_2056) :-
  1658. %       instance(_2056, actHoldingAnObject),
  1659. %       objectActedOn(_2056, _2078),
  1660. %       instance(_2078, tClazzBird),
  1661. %       \+ ( performedBy(_2056, _2100),
  1662. %            naf(~instance(_2100, mobPerson)),
  1663. %            onPhysical(_2078, _2100)
  1664. %          ).
  1665. % ~instance(_2260, mobPerson) :-
  1666. %       instance(_2282, actHoldingAnObject),
  1667. %       objectActedOn(_2282, _2304),
  1668. %       instance(_2304, tClazzBird),
  1669. %       \+ ( performedBy(_2282, _2260),
  1670. %            naf(~occuring(_2282)),
  1671. %            onPhysical(_2304, _2260)
  1672. %          ).
  1673. % ~instance(_2520, tClazzBird) :-
  1674. %       instance(_2542, actHoldingAnObject),
  1675. %       objectActedOn(_2542, _2520),
  1676. %       performedBy(_2542, _2564),
  1677. %       \+ ( instance(_2564, mobPerson),
  1678. %            naf(~occuring(_2542)),
  1679. %            onPhysical(_2520, _2564)
  1680. %          ).
  1681. % ~instance(_2752, actHoldingAnObject) :-
  1682. %       objectActedOn(_2752, _2774),
  1683. %       instance(_2774, tClazzBird),
  1684. %       performedBy(_2752, _2796),
  1685. %       \+ ( instance(_2796, mobPerson),
  1686. %            naf(~occuring(_2752)),
  1687. %            onPhysical(_2774, _2796)
  1688. %          ).
  1689. % ~objectActedOn(_2984, _3006) :-
  1690. %       instance(_2984, actHoldingAnObject),
  1691. %       instance(_3006, tClazzBird),
  1692. %       performedBy(_2984, _3028),
  1693. %       \+ ( instance(_3028, mobPerson),
  1694. %            naf(~occuring(_2984)),
  1695. %            onPhysical(_3006, _3028)
  1696. %          ).
  1697. % ~performedBy(_3190, _3212) :-
  1698. %       instance(_3190, actHoldingAnObject),
  1699. %       objectActedOn(_3190, _3234),
  1700. %       instance(_3234, tClazzBird),
  1701. %       \+ ( instance(_3212, mobPerson),
  1702. %            naf(~occuring(_3190)),
  1703. %            onPhysical(_3234, _3212)
  1704. %          ).
  1705. % onPhysical(_3396, _3418) :-
  1706. %       instance(_3440, actHoldingAnObject),
  1707. %       objectActedOn(_3440, _3396),
  1708. %       instance(_3396, tClazzBird),
  1709. %       performedBy(_3440, _3418),
  1710. %       instance(_3418, mobPerson),
  1711. %       occuring(_3440).
  1712.  
  1713.  
  1714.  
  1715.  
  1716.  
  1717. :- test_boxlog(sourceSchemaObjectID(SOURCE,
  1718.                                     SCHEMA,
  1719.                                     uU(uSourceSchemaObjectFn, SOURCE, SCHEMA, ID),
  1720.                                     ID)).
  1721.  
  1722.  /*
  1723. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:524
  1724. % :- test_boxlog(sourceSchemaObjectID(SOURCE_VAR,
  1725. %                                   SCHEMA_VAR,
  1726. %                                   uU(uSourceSchemaObjectFn,
  1727. %                                      SOURCE_VAR,
  1728. %                                      SCHEMA_VAR,
  1729. %                                      ID_VAR),
  1730. %                                   ID_VAR)).
  1731. % kif :-
  1732. %       all(SOURCE,
  1733. %           all(SCHEMA,
  1734. %               all(ID,
  1735. %                   sourceSchemaObjectID(SOURCE,
  1736. %                                        SCHEMA,
  1737. %                                        u(uSourceSchemaObjectFn,
  1738. %                                          SOURCE,
  1739. %                                          SCHEMA,
  1740. %                                          ID),
  1741. %                                        ID)))).
  1742. % qualify_nesc :-
  1743. %       all(SOURCE,
  1744. %           all(SCHEMA,
  1745. %               all(ID,
  1746. %                   nesc(sourceSchemaObjectID(SOURCE,
  1747. %                                             SCHEMA,
  1748. %                                             u(uSourceSchemaObjectFn,
  1749. %                                               SOURCE,
  1750. %                                               SCHEMA,
  1751. %                                               ID),
  1752. %                                             ID))))).
  1753. % debugm(user, sc_success(user, user:nnf(KB, all(SOURCE, all(SCHEMA, all(ID, nesc(b_d(KB, nesc, poss), sourceSchemaObjectID(SOURCE, SCHEMA, u(uSourceSchemaObjectFn, SOURCE, SCHEMA, ID), ID))))), nesc(b_d(KB, nesc, poss), sourceSchemaObjectID(SOURCE, SCHEMA, u(uSourceSchemaObjectFn, SOURCE, SCHEMA, ID), ID))))).
  1754. % nnf :-
  1755. %       nesc(sourceSchemaObjectID(SOURCE,
  1756. %                                 SCHEMA,
  1757. %                                 u(uSourceSchemaObjectFn, SOURCE, SCHEMA, ID),
  1758. %                                 ID)).
  1759. % th_nnf_in :-
  1760. %       tru(t(sourceSchemaObjectID,
  1761. %             SOURCE,
  1762. %             SCHEMA,
  1763. %             u(uSourceSchemaObjectFn, SOURCE, SCHEMA, ID),
  1764. %             ID)).
  1765. % th_nnf_out :-
  1766. %       ~n(tru(t(sourceSchemaObjectID, SOURCE, SCHEMA, u(uSourceSchemaObjectFn, SOURCE, SCHEMA, ID), ID))).
  1767. % proven_tru(t(sourceSchemaObjectID, SOURCE, SCHEMA, u(uSourceSchemaObjectFn, SOURCE, SCHEMA, ID), ID)).
  1768. % pfc :-
  1769. %       proven_tru(sourceSchemaObjectID(SOURCE,
  1770. %                                       SCHEMA,
  1771. %                                       u(uSourceSchemaObjectFn,
  1772. %                                         SOURCE,
  1773. %                                         SCHEMA,
  1774. %                                         ID),
  1775. %                                       ID)).
  1776. */
  1777.  
  1778. % ~mudEquals(_1236{???UUUSOURCESCHEMAOBJECTFN1}, uU(uSourceSchemaObjectFn, _2438, _2460, _2482)) :-
  1779. %       ~sourceSchemaObjectID(_2438, _2460, _1280{???UUUSOURCESCHEMAOBJECTFN1}, _2482).
  1780. % sourceSchemaObjectID(_2614, _2636, UUUSOURCESCHEMAOBJECTFN1_VAR, _2658) :-
  1781. %       mudEquals(_1006{???UUUSOURCESCHEMAOBJECTFN1},
  1782. %                 uU(uSourceSchemaObjectFn, _2614, _2636, _2658)).
  1783.  
  1784.  
  1785.  
  1786. :- test_boxlog(sourceSchemaObjectID(SOURCE,
  1787.                                     SCHEMA,
  1788.                                     THING,
  1789.                                     uU(uSourceSchemaObjectIDFn,
  1790.                                        SOURCE,
  1791.                                        SCHEMA,
  1792.                                        THING))).
  1793.  
  1794.  /*
  1795. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:532
  1796. % :- test_boxlog(sourceSchemaObjectID(SOURCE_VAR,
  1797. %                                   SCHEMA_VAR,
  1798. %                                   THING_VAR,
  1799. %                                   uU(uSourceSchemaObjectIDFn,
  1800. %                                      SOURCE_VAR,
  1801. %                                      SCHEMA_VAR,
  1802. %                                      THING_VAR))).
  1803. % kif :-
  1804. %       all(SOURCE,
  1805. %           all(SCHEMA,
  1806. %               all(THING,
  1807. %                   sourceSchemaObjectID(SOURCE,
  1808. %                                        SCHEMA,
  1809. %                                        THING,
  1810. %                                        u(uSourceSchemaObjectIDFn,
  1811. %                                          SOURCE,
  1812. %                                          SCHEMA,
  1813. %                                          THING))))).
  1814. % qualify_nesc :-
  1815. %       all(SOURCE,
  1816. %           all(SCHEMA,
  1817. %               all(THING,
  1818. %                   nesc(sourceSchemaObjectID(SOURCE,
  1819. %                                             SCHEMA,
  1820. %                                             THING,
  1821. %                                             u(uSourceSchemaObjectIDFn,
  1822. %                                               SOURCE,
  1823. %                                               SCHEMA,
  1824. %                                               THING)))))).
  1825. % debugm(user, sc_success(user, user:nnf(KB, all(SOURCE, all(SCHEMA, all(THING, nesc(b_d(KB, nesc, poss), sourceSchemaObjectID(SOURCE, SCHEMA, THING, u(uSourceSchemaObjectIDFn, SOURCE, SCHEMA, THING)))))), nesc(b_d(KB, nesc, poss), sourceSchemaObjectID(SOURCE, SCHEMA, THING, u(uSourceSchemaObjectIDFn, SOURCE, SCHEMA, THING)))))).
  1826. % nnf :-
  1827. %       nesc(sourceSchemaObjectID(SOURCE,
  1828. %                                 SCHEMA,
  1829. %                                 THING,
  1830. %                                 u(uSourceSchemaObjectIDFn,
  1831. %                                   SOURCE,
  1832. %                                   SCHEMA,
  1833. %                                   THING))).
  1834. % th_nnf_in :-
  1835. %       tru(t(sourceSchemaObjectID,
  1836. %             SOURCE,
  1837. %             SCHEMA,
  1838. %             THING,
  1839. %             u(uSourceSchemaObjectIDFn, SOURCE, SCHEMA, THING))).
  1840. % th_nnf_out :-
  1841. %       ~n(tru(t(sourceSchemaObjectID, SOURCE, SCHEMA, THING, u(uSourceSchemaObjectIDFn, SOURCE, SCHEMA, THING)))).
  1842. % proven_tru(t(sourceSchemaObjectID, SOURCE, SCHEMA, THING, u(uSourceSchemaObjectIDFn, SOURCE, SCHEMA, THING))).
  1843. % pfc :-
  1844. %       proven_tru(sourceSchemaObjectID(SOURCE,
  1845. %                                       SCHEMA,
  1846. %                                       THING,
  1847. %                                       u(uSourceSchemaObjectIDFn,
  1848. %                                         SOURCE,
  1849. %                                         SCHEMA,
  1850. %                                         THING))).
  1851. */
  1852.  
  1853. % ~mudEquals(_886{???UUUSOURCESCHEMAOBJECTIDFN1}, uU(uSourceSchemaObjectIDFn, _1072, _1094, _1116)) :-
  1854. %       ~sourceSchemaObjectID(_1072, _1094, _1116, _906{???UUUSOURCESCHEMAOBJECTIDFN1}).
  1855. % sourceSchemaObjectID(_1248, _1270, _1292, UUUSOURCESCHEMAOBJECTIDFN1_VAR) :-
  1856. %       mudEquals(_868{???UUUSOURCESCHEMAOBJECTIDFN1},
  1857. %                 uU(uSourceSchemaObjectIDFn, _1248, _1270, _1292)).
  1858.  
  1859.  
  1860.  
  1861.  
  1862. :- test_defunctionalize(implies(instance(YEAR, tClazzCalendarYear),
  1863.                                 temporallyFinishedBy(YEAR,
  1864.                                                      uU(iTimeOf_SecondFn,
  1865.                                                         59,
  1866.                                                         uU(iTimeOf_MinuteFn,
  1867.                                                            59,
  1868.                                                            uU(iTimeOf_HourFn,
  1869.                                                               23,
  1870.                                                               uU(iTimeOf_DayFn,
  1871.                                                                  31,
  1872.                                                                  uU(iTimeOf_MonthFn,
  1873.                                                                     vDecember,
  1874.                                                                     YEAR)))))))).
  1875.  
  1876.  /*
  1877. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl:541
  1878. % '' :-
  1879. %       mudEquals(UUITIMEOF_SECONDFN1_VAR, uU(iTimeOf_SecondFn, 59, UUITIMEOF_MINUTEFN1_VAR))=>(mudEquals(UUITIMEOF_MINUTEFN1_VAR, uU(iTimeOf_MinuteFn, 59, UUITIMEOF_HOURFN1_VAR))=>(mudEquals(UUITIMEOF_HOURFN1_VAR, uU(iTimeOf_HourFn, 23, UUITIMEOF_DAYFN1_VAR))=>(mudEquals(UUITIMEOF_DAYFN1_VAR, uU(iTimeOf_DayFn, 31, UUITIMEOF_MONTHFN1_VAR))=>(mudEquals(UUITIMEOF_MONTHFN1_VAR, uU(iTimeOf_MonthFn, vDecember, YEAR))=>implies(instance(YEAR, tClazzCalendarYear), temporallyFinishedBy(YEAR, UUITIMEOF_SECONDFN1_VAR)))))).
  1880. */
  1881.  
  1882.  
  1883. % >(mudEquals(UUITIMEOF_SECONDFN1_VAR, uU(iTimeOf_SecondFn, 59, UUITIMEOF_MINUTEFN1_VAR)), =>(mudEquals(UUITIMEOF_MINUTEFN1_VAR, uU(iTimeOf_MinuteFn, 59, UUITIMEOF_HOURFN1_VAR)), =>(mudEquals(UUITIMEOF_HOURFN1_VAR, uU(iTimeOf_HourFn, 23, UUITIMEOF_DAYFN1_VAR)), =>(mudEquals(UUITIMEOF_DAYFN1_VAR, uU(iTimeOf_DayFn, 31, UUITIMEOF_MONTHFN1_VAR)), =>(mudEquals(UUITIMEOF_MONTHFN1_VAR, uU(iTimeOf_MonthFn, vDecember, _200)), implies(instance(_200, tClazzCalendarYear), temporallyFinishedBy(_200, UUITIMEOF_SECONDFN1_VAR))))))).
  1884.  
  1885.  
  1886. % init_why(after('/home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/boxlog_sanity.pl')).
  1887. % start_x_ide
  1888. % Dont forget to ?- logicmoo_i_cyc_xform.
  1889. % after_boot
  1890. % init_why(program).
  1891. baseKB:  ?-
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!