API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Oct 9th, 2019
174
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 135.41 KB | None | 0 0
raw download clone embed print report
  1. fork {
  2. and {
  3. punc((".","."))
  4. fork {
  5. and {
  6. DoublePremise(("."),punc)
  7. fork {
  8. and {
  9. IsHas(taskTerm,("-->",volMin(3)))
  10. fork {
  11. and {
  12. IsHas(beliefTerm,("-->",volMin(3)))
  13. fork {
  14. and {
  15. unifyIf(task((0)),neqRCom,belief((0)))
  16. fork {
  17. and {
  18. unifyIf(task((0)),neq,belief((0)))
  19. Has(taskTerm((0)),(".",any,volMin(0)))
  20. Has(beliefTerm((0)),(".",any,volMin(0)))
  21. forkable({14,23,51}) {
  22. 26 ==> {
  23. unify(((%1-->%2),(%3-->%2))) ==> {
  24. (Termify((%3-->%1),truth(punc((".",".")),Abduction,(),Compose)),26)
  25. }
  26. }
  27. 35 ==> {
  28. unify(((%1-->%2),(%3-->%2))) ==> {
  29. (Termify((%1-->%3),truth(punc((".",".")),Induction,(),Compose)),35)
  30. }
  31. }
  32. 63 ==> {
  33. unify(((%1-->%2),(%3-->%2))) ==> {
  34. (Termify((%1<->%3),truth(punc((".",".")),Comparison,(),Compose)),63)
  35. }
  36. }
  37. }
  38. }
  39. and {
  40. (--,Is(taskTerm((1)),"1111000000000"))
  41. unifyIf(task((0)),neq,belief((0)))
  42. unifyIf(task((0)),notSetsOrDifferentSets,belief((0)))
  43. forkable({96}) {
  44. 108 ==> {
  45. unify(((%1-->%2),(%3-->%2))) ==> {
  46. (Termify((interSect(polarizeTask(%1),polarizeBelief(%3))-->%2),truth(punc((".",".")),IntersectionDD,(),Compose)),108)
  47. }
  48. }
  49. }
  50. }
  51. }
  52. }
  53. and {
  54. unifyIf(task((0)),Eventable,(()))
  55. Is(beliefTerm((0)),"&&")
  56. unifyIf(belief((0)),VolumeCompare,task((0)))
  57. unifyIf(belief((0)),neq,task((0)))
  58. fork {
  59. and {
  60. unifyIf(belief((0)),"Event->(+)",task((0)))
  61. forkable({114}) {
  62. 126 ==> {
  63. unify(((%1-->%2),(%3-->%2))) ==> {
  64. (Termify((--,(conjWithout(%3,%1)-->%2)),truth(punc((".",".")),DeductionPN,(),Task)),126)
  65. }
  66. }
  67. }
  68. }
  69. and {
  70. unifyIf(belief((0)),"Event->(-)",task((0)))
  71. forkable({116}) {
  72. 128 ==> {
  73. unify(((%1-->%2),(%3-->%2))) ==> {
  74. (Termify((--,(conjWithout(%3,(--,%1))-->%2)),truth(punc((".",".")),DeductionNN,(),Task)),128)
  75. }
  76. }
  77. }
  78. }
  79. }
  80. }
  81. and {
  82. unifyIf(belief((0)),Eventable,(()))
  83. Is(taskTerm((0)),"&&")
  84. unifyIf(task((0)),VolumeCompare,belief((0)))
  85. unifyIf(task((0)),neq,belief((0)))
  86. fork {
  87. and {
  88. unifyIf(task((0)),"Event->(+)",belief((0)))
  89. forkable({113}) {
  90. 125 ==> {
  91. unify(((%1-->%2),(%3-->%2))) ==> {
  92. (Termify((--,(conjWithout(%1,%3)-->%2)),truth(punc((".",".")),DeductionNP,(),Task)),125)
  93. }
  94. }
  95. }
  96. }
  97. and {
  98. unifyIf(task((0)),"Event->(-)",belief((0)))
  99. forkable({115}) {
  100. 127 ==> {
  101. unify(((%1-->%2),(%3-->%2))) ==> {
  102. (Termify((--,(conjWithout(%1,(--,%3))-->%2)),truth(punc((".",".")),DeductionNN,(),Task)),127)
  103. }
  104. }
  105. }
  106. }
  107. }
  108. }
  109. and {
  110. unifyIf(task((1)),Eventable,(()))
  111. Is(beliefTerm((1)),"&&")
  112. unifyIf(belief((1)),VolumeCompare,task((1)))
  113. unifyIf(belief((1)),neq,task((1)))
  114. fork {
  115. and {
  116. unifyIf(belief((1)),"Event->(+)",task((1)))
  117. forkable({110}) {
  118. 122 ==> {
  119. unify(((%1-->%2),(%1-->%3))) ==> {
  120. (Termify((--,(%1-->conjWithout(%3,%2))),truth(punc((".",".")),DeductionPN,(),Task)),122)
  121. }
  122. }
  123. }
  124. }
  125. and {
  126. unifyIf(belief((1)),"Event->(-)",task((1)))
  127. forkable({112}) {
  128. 124 ==> {
  129. unify(((%1-->%2),(%1-->%3))) ==> {
  130. (Termify((--,(%1-->conjWithout(%3,(--,%2)))),truth(punc((".",".")),DeductionNN,(),Task)),124)
  131. }
  132. }
  133. }
  134. }
  135. }
  136. }
  137. and {
  138. unifyIf(belief((1)),Eventable,(()))
  139. Is(taskTerm((1)),"&&")
  140. unifyIf(task((1)),VolumeCompare,belief((1)))
  141. unifyIf(task((1)),neq,belief((1)))
  142. fork {
  143. and {
  144. unifyIf(task((1)),"Event->(+)",belief((1)))
  145. forkable({109}) {
  146. 121 ==> {
  147. unify(((%1-->%2),(%1-->%3))) ==> {
  148. (Termify((--,(%1-->conjWithout(%2,%3))),truth(punc((".",".")),DeductionNP,(),Task)),121)
  149. }
  150. }
  151. }
  152. }
  153. and {
  154. unifyIf(task((1)),"Event->(-)",belief((1)))
  155. forkable({111}) {
  156. 123 ==> {
  157. unify(((%1-->%2),(%1-->%3))) ==> {
  158. (Termify((--,(%1-->conjWithout(%2,(--,%3)))),truth(punc((".",".")),DeductionNN,(),Task)),123)
  159. }
  160. }
  161. }
  162. }
  163. }
  164. }
  165. and {
  166. unifyIf(task((1)),neq,belief((1)))
  167. Has(taskTerm((1)),(".",any,volMin(0)))
  168. Has(beliefTerm((1)),(".",any,volMin(0)))
  169. unifyIf(task((1)),neqRCom,belief((1)))
  170. forkable({15,22,52}) {
  171. 27 ==> {
  172. unify(((%1-->%2),(%1-->%3))) ==> {
  173. (Termify((%2-->%3),truth(punc((".",".")),Abduction,(),Compose)),27)
  174. }
  175. }
  176. 34 ==> {
  177. unify(((%1-->%2),(%1-->%3))) ==> {
  178. (Termify((%3-->%2),truth(punc((".",".")),Induction,(),Compose)),34)
  179. }
  180. }
  181. 64 ==> {
  182. unify(((%1-->%2),(%1-->%3))) ==> {
  183. (Termify((%2<->%3),truth(punc((".",".")),Comparison,(),Compose)),64)
  184. }
  185. }
  186. }
  187. }
  188. and {
  189. unifyIf(task((0)),neq,belief((1)))
  190. Has(taskTerm((0)),(".",any,volMin(0)))
  191. Has(beliefTerm((1)),(".",any,volMin(0)))
  192. unifyIf(task((0)),neqRCom,belief((1)))
  193. forkable({1,8}) {
  194. 13 ==> {
  195. unify(((%1-->%2),(%2-->%3))) ==> {
  196. (Termify((%1-->%3),truth(punc((".",".")),Deduction,(),Compose)),13)
  197. }
  198. }
  199. 20 ==> {
  200. unify(((%1-->%2),(%2-->%3))) ==> {
  201. (Termify((%3-->%1),truth(punc((".",".")),Exemplification,(),Compose)),20)
  202. }
  203. }
  204. }
  205. }
  206. and {
  207. unifyIf(task((1)),neq,belief((0)))
  208. Has(beliefTerm((0)),(".",any,volMin(0)))
  209. Has(taskTerm((1)),(".",any,volMin(0)))
  210. unifyIf(task((1)),neqRCom,belief((0)))
  211. forkable({0,9}) {
  212. 12 ==> {
  213. unify(((%1-->%2),(%3-->%1))) ==> {
  214. (Termify((%3-->%2),truth(punc((".",".")),Deduction,(),Compose)),12)
  215. }
  216. }
  217. 21 ==> {
  218. unify(((%1-->%2),(%3-->%1))) ==> {
  219. (Termify((%2-->%3),truth(punc((".",".")),Exemplification,(),Compose)),21)
  220. }
  221. }
  222. }
  223. }
  224. and {
  225. (--,Is(taskTerm((0)),"1111000000000"))
  226. unifyIf(task((1)),neq,belief((1)))
  227. unifyIf(task((1)),notSetsOrDifferentSets,belief((1)))
  228. unifyIf(task((1)),neqRCom,belief((1)))
  229. forkable({98}) {
  230. 110 ==> {
  231. unify(((%1-->%2),(%1-->%3))) ==> {
  232. (Termify((%1-->interSect(polarizeTask(%2),polarizeBelief(%3))),truth(punc((".",".")),IntersectionDD,(),Compose)),110)
  233. }
  234. }
  235. }
  236. }
  237. and {
  238. Is(taskTerm((0)),"[")
  239. Is(beliefTerm((0)),"[")
  240. unifyIf(task((0)),neq,belief((0)))
  241. forkable({78,79,80}) {
  242. 90 ==> {
  243. unify(((%1-->%2),(%3-->%2))) ==> {
  244. (Termify((union(%1,%3)-->%2),truth(punc((".",".")),Union,(),Compose)),90)
  245. }
  246. }
  247. 91 ==> {
  248. unify(((%1-->%2),(%3-->%2))) ==> {
  249. (Termify((intersect(%1,%3)-->%2),truth(punc((".",".")),Intersection,(),Compose)),91)
  250. }
  251. }
  252. 92 ==> {
  253. unify(((%1-->%2),(%3-->%2))) ==> {
  254. (Termify((differ(%1,%3)-->%2),truth(punc((".",".")),Difference,(),Compose)),92)
  255. }
  256. }
  257. }
  258. }
  259. and {
  260. Is(taskTerm((0)),"{")
  261. Is(beliefTerm((0)),"{")
  262. unifyIf(task((0)),neq,belief((0)))
  263. forkable({75,76,77}) {
  264. 87 ==> {
  265. unify(((%1-->%2),(%3-->%2))) ==> {
  266. (Termify((intersect(%1,%3)-->%2),truth(punc((".",".")),Union,(),Compose)),87)
  267. }
  268. }
  269. 88 ==> {
  270. unify(((%1-->%2),(%3-->%2))) ==> {
  271. (Termify((union(%1,%3)-->%2),truth(punc((".",".")),Intersection,(),Compose)),88)
  272. }
  273. }
  274. 89 ==> {
  275. unify(((%1-->%2),(%3-->%2))) ==> {
  276. (Termify((differ(%1,%3)-->%2),truth(punc((".",".")),Difference,(),Compose)),89)
  277. }
  278. }
  279. }
  280. }
  281. and {
  282. Is(taskTerm((1)),"[")
  283. Is(beliefTerm((1)),"[")
  284. unifyIf(task((1)),neq,belief((1)))
  285. forkable({72,73,74}) {
  286. 84 ==> {
  287. unify(((%1-->%2),(%1-->%3))) ==> {
  288. (Termify((%1-->union(%2,%3)),truth(punc((".",".")),Intersection,(),Compose)),84)
  289. }
  290. }
  291. 85 ==> {
  292. unify(((%1-->%2),(%1-->%3))) ==> {
  293. (Termify((%1-->intersect(%2,%3)),truth(punc((".",".")),Union,(),Compose)),85)
  294. }
  295. }
  296. 86 ==> {
  297. unify(((%1-->%2),(%1-->%3))) ==> {
  298. (Termify((%1-->differ(%2,%3)),truth(punc((".",".")),Difference,(),Compose)),86)
  299. }
  300. }
  301. }
  302. }
  303. and {
  304. Is(taskTerm((1)),"{")
  305. Is(beliefTerm((1)),"{")
  306. unifyIf(task((1)),neq,belief((1)))
  307. forkable({69,70,71}) {
  308. 81 ==> {
  309. unify(((%1-->%2),(%1-->%3))) ==> {
  310. (Termify((%1-->union(%2,%3)),truth(punc((".",".")),Union,(),Compose)),81)
  311. }
  312. }
  313. 82 ==> {
  314. unify(((%1-->%2),(%1-->%3))) ==> {
  315. (Termify((%1-->intersect(%2,%3)),truth(punc((".",".")),Intersection,(),Compose)),82)
  316. }
  317. }
  318. 83 ==> {
  319. unify(((%1-->%2),(%1-->%3))) ==> {
  320. (Termify((%1-->differ(%2,%3)),truth(punc((".",".")),Difference,(),Compose)),83)
  321. }
  322. }
  323. }
  324. }
  325. and {
  326. Has(taskTerm((0)),(".",any,volMin(0)))
  327. Has(taskTerm((1)),(".",any,volMin(0)))
  328. forkable({48}) {
  329. 60 ==> {
  330. unify(((%1-->%2),(%2-->%1))) ==> {
  331. (Termify((%1<->%2),truth(punc((".",".")),Intersection,(),Compose)),60)
  332. }
  333. }
  334. }
  335. }
  336. }
  337. }
  338. and {
  339. IsHas(beliefTerm,("<->",volMin(3)))
  340. fork {
  341. and {
  342. Has(taskTerm((0)),(".",any,volMin(0)))
  343. forkable({40}) {
  344. 52 ==> {
  345. and {
  346. unifyIf(%1,{(neq,%3),(neqRCom,%3)})
  347. unifyIf(%3,{(Has,((".",any,volMin(0)))),(neq,%1),(neqRCom,%1)})
  348. unify(((%1-->%2),(%2<->%3))) ==> {
  349. (Termify((%1-->%3),truth(punc((".",".")),Analogy,(),Compose)),52)
  350. }
  351. }
  352. }
  353. }
  354. }
  355. and {
  356. Has(taskTerm((1)),(".",any,volMin(0)))
  357. forkable({36}) {
  358. 48 ==> {
  359. and {
  360. unifyIf(%2,{(neq,%3),(neqRCom,%3)})
  361. unifyIf(%3,{(Has,((".",any,volMin(0)))),(neq,%2),(neqRCom,%2)})
  362. unify(((%1-->%2),(%1<->%3))) ==> {
  363. (Termify((%3-->%2),truth(punc((".",".")),Analogy,(),Compose)),48)
  364. }
  365. }
  366. }
  367. }
  368. }
  369. }
  370. }
  371. }
  372. }
  373. and {
  374. IsHas(taskTerm,("==>",volMin(3)))
  375. fork {
  376. and {
  377. IsHas(beliefTerm,("==>",volMin(3)))
  378. fork {
  379. and {
  380. unifyIf(task((1)),Eventable,(()))
  381. fork {
  382. and {
  383. Is(beliefTerm((1)),"&&")
  384. fork {
  385. and {
  386. unifyIf(belief((1)),Eventable,(()))
  387. Is(taskTerm((1)),"&&")
  388. unifyIf(task((0)),neq,task((1)))
  389. unifyIf(task((0)),neq,belief((1)))
  390. unifyIf(task((1)),neq,belief((1)))
  391. unifyIf(belief((1)),neq,task((1)))
  392. forkable({-29,-28}) {
  393. 239 ==> {
  394. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  395. (Termify((conjWithout(%2,%3) ==>+- conjWithout(%3,%2)),truth(punc((".",".")),AbductionPB,(),Compose)),239)
  396. }
  397. }
  398. 240 ==> {
  399. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  400. (Termify((conjWithout(%3,%2) ==>+- conjWithout(%2,%3)),truth(punc((".",".")),AbductionPB,(),Compose)),240)
  401. }
  402. }
  403. }
  404. }
  405. and {
  406. unifyIf(belief((1)),VolumeCompare,task((1)))
  407. fork {
  408. and {
  409. unifyIf(belief((1)),"Event->(+)",task((1)))
  410. forkable({251,257}) {
  411. 263 ==> {
  412. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  413. (Termify((--,(%1 ==>+- conjWithoutUnify(%3,%2))),truth(punc((".",".")),DeductionNP,(),Compose)),263)
  414. }
  415. }
  416. 269 ==> {
  417. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  418. (Termify((%1 ==>+- conjWithoutUnify(%3,%2)),truth(punc((".",".")),Deduction,(),Compose)),269)
  419. }
  420. }
  421. }
  422. }
  423. and {
  424. unifyIf(belief((1)),"Event->(-)",task((1)))
  425. forkable({-3,-1}) {
  426. 265 ==> {
  427. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  428. (Termify((--,(%1 ==>+- conjWithoutUnify(%3,(--,%2)))),truth(punc((".",".")),DeductionNN,(),Compose)),265)
  429. }
  430. }
  431. 267 ==> {
  432. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  433. (Termify((%1 ==>+- conjWithoutUnify(%3,(--,%2))),truth(punc((".",".")),DeductionNP,(),Compose)),267)
  434. }
  435. }
  436. }
  437. }
  438. }
  439. }
  440. }
  441. }
  442. and {
  443. (--,Is(taskTerm((1)),"1111000000000"))
  444. Is(beliefTerm((0)),"&&")
  445. unifyIf(belief((0)),VolumeCompare,task((1)))
  446. unifyIf(belief((0)),neq,task((1)))
  447. fork {
  448. and {
  449. unifyIf(belief((0)),"Event->(+)",task((1)))
  450. forkable({202}) {
  451. 214 ==> {
  452. unify(((%1 ==>+- %2),(%3 ==>+- %4))) ==> {
  453. (Termify(polarizeBelief(((conjWithout(%3,%2) &&+- %1) ==>+- %4)),truth(punc((".",".")),DeductionPD,(),Compose)),214)
  454. }
  455. }
  456. }
  457. }
  458. and {
  459. unifyIf(belief((0)),"Event->(-)",task((1)))
  460. forkable({203}) {
  461. 215 ==> {
  462. unify(((%1 ==>+- %2),(%3 ==>+- %4))) ==> {
  463. (Termify(polarizeBelief(((conjWithout(%3,(--,%2)) &&+- %1) ==>+- %4)),truth(punc((".",".")),DeductionND,(),Compose)),215)
  464. }
  465. }
  466. }
  467. }
  468. }
  469. }
  470. }
  471. }
  472. fork {
  473. and {
  474. unifyIf(task((0)),Eventable,(()))
  475. unifyIf(belief((0)),Eventable,(()))
  476. Is(taskTerm((0)),"&&")
  477. Is(beliefTerm((0)),"&&")
  478. unifyIf(task((0)),neq,belief((0)))
  479. unifyIf(task((0)),neq,task((1)))
  480. unifyIf(belief((0)),neq,task((0)))
  481. unifyIf(task((1)),neq,belief((0)))
  482. forkable({-31,-30}) {
  483. 237 ==> {
  484. unify(((%1 ==>+- %2),(%3 ==>+- %2))) ==> {
  485. (Termify((conjWithout(%1,%3) ==>+- conjWithout(%3,%1)),truth(punc((".",".")),InductionPB,(),Compose)),237)
  486. }
  487. }
  488. 238 ==> {
  489. unify(((%1 ==>+- %2),(%3 ==>+- %2))) ==> {
  490. (Termify((conjWithout(%3,%1) ==>+- conjWithout(%1,%3)),truth(punc((".",".")),InductionPB,(),Compose)),238)
  491. }
  492. }
  493. }
  494. }
  495. forkable({167}) {
  496. 179 ==> {
  497. unify(((%1 ==>+- %2),(%2 ==>+- %3))) ==> {
  498. (Termify((--,(%1 ==>+- %3)),truth(punc((".",".")),DeductionNP,(),Compose)),179)
  499. }
  500. }
  501. }
  502. }
  503. fork {
  504. and {
  505. unifyIf(belief((0)),Eventable,(()))
  506. Is(taskTerm((0)),"&&")
  507. unifyIf(task((0)),VolumeCompare,belief((0)))
  508. unifyIf(task((0)),neq,belief((0)))
  509. unifyIf(task((0)),"Event->(+)",belief((0)))
  510. fork {
  511. and {
  512. unifyIf(task((1)),Unifiability,(belief((1)),false,6144))
  513. forkable({217}) {
  514. 229 ==> {
  515. unify(((%1 ==>+- %2),(%3 ==>+- %4))) ==> {
  516. (Termify(unisubst((--,conjWithout(%1,%3)),%2,%4),truth(punc((".",".")),AbductionXOR,(),BeliefEvent)),229)
  517. }
  518. }
  519. }
  520. }
  521. forkable({276}) {
  522. 288 ==> {
  523. unify(((%1 ==>+- %2),(%3 ==>+- %4))) ==> {
  524. (Termify(conjWithout(%1,%3),truth(punc((".",".")),AbductionPB,(),Compose)),288)
  525. }
  526. }
  527. }
  528. }
  529. }
  530. forkable({166}) {
  531. 178 ==> {
  532. unify(((%1 ==>+- %2),(%2 ==>+- %3))) ==> {
  533. (Termify((--,(%1 ==>+- %3)),truth(punc((".",".")),DeductionPN,(),Compose)),178)
  534. }
  535. }
  536. }
  537. }
  538. and {
  539. unifyIf(belief((1)),Eventable,(()))
  540. Is(taskTerm((1)),"&&")
  541. unifyIf(task((1)),VolumeCompare,belief((1)))
  542. fork {
  543. and {
  544. unifyIf(task((1)),"Event->(+)",belief((1)))
  545. forkable({250,256}) {
  546. 262 ==> {
  547. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  548. (Termify((--,(%1 ==>+- conjWithoutUnify(%2,%3))),truth(punc((".",".")),DeductionPN,(),Compose)),262)
  549. }
  550. }
  551. 268 ==> {
  552. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  553. (Termify((%1 ==>+- conjWithoutUnify(%2,%3)),truth(punc((".",".")),Deduction,(),Compose)),268)
  554. }
  555. }
  556. }
  557. }
  558. and {
  559. unifyIf(task((1)),"Event->(-)",belief((1)))
  560. forkable({-4,-2}) {
  561. 264 ==> {
  562. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  563. (Termify((--,(%1 ==>+- conjWithoutUnify(%2,(--,%3)))),truth(punc((".",".")),DeductionNN,(),Compose)),264)
  564. }
  565. }
  566. 266 ==> {
  567. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  568. (Termify((%1 ==>+- conjWithoutUnify(%2,(--,%3))),truth(punc((".",".")),DeductionPN,(),Compose)),266)
  569. }
  570. }
  571. }
  572. }
  573. }
  574. }
  575. forkable({-94,-93,-82,-81,-78,-77,-70,-69,-64,-63,-58,-57,-50,-49}) {
  576. 174 ==> {
  577. unify(((%1 ==>+- %2),(%2 ==>+- %3))) ==> {
  578. (Termify((%1 ==>+- %3),truth(punc((".",".")),Deduction,(),Compose)),174)
  579. }
  580. }
  581. 175 ==> {
  582. unify(((%1 ==>+- %2),(%3 ==>+- %1))) ==> {
  583. (Termify((%3 ==>+- %2),truth(punc((".",".")),Deduction,(),Compose)),175)
  584. }
  585. }
  586. 186 ==> {
  587. unify(((%1 ==>+- %2),(%3 ==>+- %1))) ==> {
  588. (Termify((%2 ==>+- %3),truth(punc((".",".")),Exemplification,(),Compose)),186)
  589. }
  590. }
  591. 187 ==> {
  592. unify(((%1 ==>+- %2),(%2 ==>+- %3))) ==> {
  593. (Termify((%3 ==>+- %1),truth(punc((".",".")),Exemplification,(),Compose)),187)
  594. }
  595. }
  596. 190 ==> {
  597. unify(((%1 ==>+- %2),(%3 ==>+- %1))) ==> {
  598. (Termify(((--,%2) ==>+- %3),truth(punc((".",".")),ExemplificationNP,(),Compose)),190)
  599. }
  600. }
  601. 191 ==> {
  602. unify(((%1 ==>+- %2),(%2 ==>+- %3))) ==> {
  603. (Termify(((--,%3) ==>+- %1),truth(punc((".",".")),ExemplificationPN,(),Compose)),191)
  604. }
  605. }
  606. 198 ==> {
  607. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  608. (Termify((%2 ==>+- %3),truth(punc((".",".")),Abduction,(),Compose)),198)
  609. }
  610. }
  611. 199 ==> {
  612. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  613. (Termify((--,((--,%2) ==>+- %3)),truth(punc((".",".")),AbductionNN,(),Compose)),199)
  614. }
  615. }
  616. 204 ==> {
  617. unify(((%1 ==>+- %2),(%3 ==>+- %2))) ==> {
  618. (Termify((%1 ==>+- %3),truth(punc((".",".")),Induction,(),Compose)),204)
  619. }
  620. }
  621. 205 ==> {
  622. unify(((%1 ==>+- %2),(%3 ==>+- %2))) ==> {
  623. (Termify((%1 ==>+- %3),truth(punc((".",".")),InductionNN,(),Compose)),205)
  624. }
  625. }
  626. 210 ==> {
  627. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  628. (Termify((%1 ==>+- (polarizeTask(%2) &&+- polarizeBelief(%3))),truth(punc((".",".")),IntersectionDD,(),Compose)),210)
  629. }
  630. }
  631. 211 ==> {
  632. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  633. (Termify((--,(%1 ==>+- ((--,polarizeTask(%2)) &&+- (--,polarizeBelief(%3))))),truth(punc((".",".")),UnionDD,(),Compose)),211)
  634. }
  635. }
  636. 218 ==> {
  637. unify(((%1 ==>+- %2),(%2 ==>+- %1))) ==> {
  638. (Termify((--,((--,%1) ==>+- %2)),truth(punc((".",".")),Intersection,(),Compose)),218)
  639. }
  640. }
  641. 219 ==> {
  642. unify(((%1 ==>+- %2),(%2 ==>+- %1))) ==> {
  643. (Termify((--,((--,%2) ==>+- %1)),truth(punc((".",".")),Intersection,(),Compose)),219)
  644. }
  645. }
  646. }
  647. }
  648. }
  649. and {
  650. (--,Is(beliefTerm,"==>"))
  651. (--,Is(taskTerm((0)),"--"))
  652. (--,Is(taskTerm((1)),"1111000000000"))
  653. unifyIf(task((0)),Unifiability,(belief(()),false,2048))
  654. forkable({-115,-113}) {
  655. 153 ==> {
  656. unify(((%1 ==>+- %2),%3)) ==> {
  657. (Termify(unisubst(%2,%1,%3,"$"),truth(punc((".",".")),Deduction,(),BeliefEvent)),153)
  658. }
  659. }
  660. 155 ==> {
  661. unify(((%1 ==>+- %2),%3)) ==> {
  662. (Termify((--,unisubst(%2,%1,%3,"$")),truth(punc((".",".")),DeductionNP,(),BeliefEvent)),155)
  663. }
  664. }
  665. }
  666. }
  667. }
  668. }
  669. and {
  670. unifyIf(belief(()),Eventable,(()))
  671. fork {
  672. and {
  673. unifyIf(task(()),neq,belief(()))
  674. fork {
  675. and {
  676. Is(taskTerm,"&&")
  677. unifyIf(task(()),VolumeCompare,(belief(()),onlyIfConstants))
  678. fork {
  679. and {
  680. (--,ConjParallel(taskTerm))
  681. fork {
  682. and {
  683. Has(taskTerm,("--",any,volMin(0)))
  684. unifyIf(task(()),EventUnifiability,(belief(()),true,true))
  685. forkable({240}) {
  686. 252 ==> {
  687. unify((%1,%2)) ==> {
  688. (Termify(conjBefore(%1,(--,%2)),truth(punc((".",".")),DeductionPN,(),BeliefEvent)),252)
  689. }
  690. }
  691. }
  692. }
  693. and {
  694. unifyIf(task(()),EventUnifiability,(belief(()),false,true))
  695. forkable({238}) {
  696. 250 ==> {
  697. unify((%1,%2)) ==> {
  698. (Termify(conjBefore(%1,%2),truth(punc((".",".")),Deduction,(),BeliefEvent)),250)
  699. }
  700. }
  701. }
  702. }
  703. }
  704. }
  705. and {
  706. Has(taskTerm,("--",any,volMin(0)))
  707. unifyIf(task(()),EventUnifiability,(belief(()),true,true))
  708. forkable({233}) {
  709. 245 ==> {
  710. unify((%1,%2)) ==> {
  711. (Termify(conjAfter(%1,(--,%2)),truth(punc((".",".")),DeductionPN,(),BeliefEvent)),245)
  712. }
  713. }
  714. }
  715. }
  716. and {
  717. unifyIf(task(()),EventUnifiability,(belief(()),false,true))
  718. forkable({231}) {
  719. 243 ==> {
  720. unify((%1,%2)) ==> {
  721. (Termify(conjAfter(%1,%2),truth(punc((".",".")),Deduction,(),BeliefEvent)),243)
  722. }
  723. }
  724. }
  725. }
  726. }
  727. }
  728. and {
  729. (--,Is(beliefTerm,"1111000000000"))
  730. Is(taskTerm,"&&")
  731. unifyIf(task(()),VolumeCompare,(belief(()),onlyIfConstants))
  732. fork {
  733. and {
  734. Has(taskTerm,("--",any,volMin(0)))
  735. unifyIf(task(()),EventUnifiability,(belief(()),true,true))
  736. forkable({235}) {
  737. 247 ==> {
  738. unify((%1,%2)) ==> {
  739. (Termify((--,conjAfter(%1,(--,%2))),truth(punc((".",".")),DeductionNN,(),BeliefEvent)),247)
  740. }
  741. }
  742. }
  743. }
  744. and {
  745. unifyIf(task(()),EventUnifiability,(belief(()),false,true))
  746. forkable({236}) {
  747. 248 ==> {
  748. unify((%1,%2)) ==> {
  749. (Termify((--,conjAfter(%1,%2)),truth(punc((".",".")),DeductionNP,(),BeliefEvent)),248)
  750. }
  751. }
  752. }
  753. }
  754. }
  755. }
  756. }
  757. }
  758. and {
  759. IsHas(taskTerm,("==>",volMin(3)))
  760. (--,Is(beliefTerm,"1111000000000"))
  761. Is(taskTerm((0)),"&&")
  762. unifyIf(task((0)),VolumeCompare,belief(()))
  763. fork {
  764. and {
  765. unifyIf(task((0)),"Event->(+)",belief(()))
  766. forkable({264}) {
  767. 276 ==> {
  768. unify(((%1 ==>+- %2),%3)) ==> {
  769. (Termify(polarizeTask((conjWithoutUnify(%1,%3) ==>+- %2)),truth(punc((".",".")),DeductionDP,(),BeliefEvent)),276)
  770. }
  771. }
  772. }
  773. }
  774. and {
  775. unifyIf(task((0)),"Event->(-)",belief(()))
  776. forkable({265}) {
  777. 277 ==> {
  778. unify(((%1 ==>+- %2),%3)) ==> {
  779. (Termify(polarizeTask((conjWithoutUnify(%1,(--,%3)) ==>+- %2)),truth(punc((".",".")),DeductionDN,(),BeliefEvent)),277)
  780. }
  781. }
  782. }
  783. }
  784. }
  785. }
  786. }
  787. }
  788. and {
  789. IsHas(beliefTerm,("==>","--",volMin(4)))
  790. IsHas(beliefTerm((0)),("--",volMin(2)))
  791. fork {
  792. and {
  793. IsHas(taskTerm,("==>",volMin(3)))
  794. fork {
  795. and {
  796. unifyIf(task((1)),Eventable,(()))
  797. (--,Is(taskTerm((1)),"1111000000000"))
  798. Is(beliefTerm((0,0)),"&&")
  799. unifyIf(belief((0,0)),VolumeCompare,task((1)))
  800. unifyIf(belief((0,0)),neq,task((1)))
  801. fork {
  802. and {
  803. unifyIf(belief((0,0)),"Event->(+)",task((1)))
  804. forkable({204}) {
  805. 216 ==> {
  806. unify(((%1 ==>+- %2),((--,%3) ==>+- %4))) ==> {
  807. (Termify(polarizeBelief((((--,conjWithout(%3,%2)) &&+- %1) ==>+- %4)),truth(punc((".",".")),DeductionPD,(),Compose)),216)
  808. }
  809. }
  810. }
  811. }
  812. and {
  813. unifyIf(belief((0,0)),"Event->(-)",task((1)))
  814. forkable({205}) {
  815. 217 ==> {
  816. unify(((%1 ==>+- %2),((--,%3) ==>+- %4))) ==> {
  817. (Termify(polarizeBelief((((--,conjWithout(%3,(--,%2))) &&+- %1) ==>+- %4)),truth(punc((".",".")),DeductionND,(),Compose)),217)
  818. }
  819. }
  820. }
  821. }
  822. }
  823. }
  824. and {
  825. unifyIf(belief((0,0)),Eventable,(()))
  826. Is(taskTerm((0)),"&&")
  827. unifyIf(task((0)),VolumeCompare,belief((0,0)))
  828. unifyIf(task((0)),neq,belief((0,0)))
  829. unifyIf(task((0)),"Event->(-)",belief((0,0)))
  830. forkable({277}) {
  831. 289 ==> {
  832. unify(((%1 ==>+- %2),((--,%3) ==>+- %4))) ==> {
  833. (Termify(conjWithout(%1,(--,%3)),truth(punc((".",".")),AbductionPB,(),Compose)),289)
  834. }
  835. }
  836. }
  837. }
  838. forkable({-88,-84,-75,-71}) {
  839. 180 ==> {
  840. unify(((%1 ==>+- %2),((--,%2) ==>+- %3))) ==> {
  841. (Termify((%1 ==>+- %3),truth(punc((".",".")),DeductionNP,(),Compose)),180)
  842. }
  843. }
  844. 184 ==> {
  845. unify(((%1 ==>+- %2),((--,%2) ==>+- %3))) ==> {
  846. (Termify((--,(%1 ==>+- %3)),truth(punc((".",".")),DeductionNN,(),Compose)),184)
  847. }
  848. }
  849. 193 ==> {
  850. unify(((%1 ==>+- %2),((--,%2) ==>+- %3))) ==> {
  851. (Termify((%3 ==>+- %1),truth(punc((".",".")),ExemplificationNP,(),Compose)),193)
  852. }
  853. }
  854. 197 ==> {
  855. unify(((%1 ==>+- %2),((--,%2) ==>+- %3))) ==> {
  856. (Termify(((--,%3) ==>+- %1),truth(punc((".",".")),ExemplificationNN,(),Compose)),197)
  857. }
  858. }
  859. }
  860. }
  861. }
  862. and {
  863. (--,Is(taskTerm,"==>"))
  864. fork {
  865. and {
  866. (--,Is(beliefTerm((1)),"1111000000000"))
  867. (--,Is(beliefTerm((0,0)),"--"))
  868. unifyIf(belief((0,0)),Unifiability,(task(()),false,2048))
  869. forkable({-112,-110}) {
  870. 156 ==> {
  871. unify((%1,((--,%2) ==>+- %3))) ==> {
  872. (Termify(unisubst(%3,%2,%1,"$"),truth(punc((".",".")),DeductionNP,(),TaskEvent)),156)
  873. }
  874. }
  875. 158 ==> {
  876. unify((%1,((--,%2) ==>+- %3))) ==> {
  877. (Termify((--,unisubst(%3,%2,%1,"$")),truth(punc((".",".")),DeductionNN,(),TaskEvent)),158)
  878. }
  879. }
  880. }
  881. }
  882. and {
  883. Is(beliefTerm((0,0)),"&&")
  884. forkable({-97,-96}) {
  885. 171 ==> {
  886. unify((%1,((--,%2) ==>+- %3))) ==> {
  887. (Termify(unisubst(beliefTerm,chooseUnifiableSubEvent(%2,polarizeTask(%1)),polarizeTask(%1),novel),truth(punc((".",".")),DeductionDP,(),TaskEvent)),171)
  888. }
  889. }
  890. 172 ==> {
  891. unify((%1,((--,%2) ==>+- %3))) ==> {
  892. (Termify((--,unisubst(beliefTerm,chooseUnifiableSubEvent(%2,polarizeTask(%1)),polarizeTask(%1),novel)),truth(punc((".",".")),DeductionDN,(),TaskEvent)),172)
  893. }
  894. }
  895. }
  896. }
  897. }
  898. }
  899. }
  900. }
  901. and {
  902. IsHas(taskTerm,("==>","--",volMin(4)))
  903. IsHas(taskTerm((0)),("--",volMin(2)))
  904. fork {
  905. and {
  906. unifyIf(belief(()),Eventable,(()))
  907. (--,Is(beliefTerm,"1111000000000"))
  908. Is(taskTerm((0,0)),"&&")
  909. unifyIf(task((0,0)),VolumeCompare,belief(()))
  910. fork {
  911. and {
  912. unifyIf(task((0,0)),"Event->(+)",belief(()))
  913. forkable({267}) {
  914. 279 ==> {
  915. unify((((--,%1) ==>+- %2),%3)) ==> {
  916. (Termify(polarizeTask(((--,conjWithoutUnify(%1,%3)) ==>+- %2)),truth(punc((".",".")),DeductionDP,(),BeliefEvent)),279)
  917. }
  918. }
  919. }
  920. }
  921. and {
  922. unifyIf(task((0,0)),"Event->(-)",belief(()))
  923. forkable({266}) {
  924. 278 ==> {
  925. unify((((--,%1) ==>+- %2),%3)) ==> {
  926. (Termify(polarizeTask(((--,conjWithoutUnify(%1,(--,%3))) ==>+- %2)),truth(punc((".",".")),DeductionDN,(),BeliefEvent)),278)
  927. }
  928. }
  929. }
  930. }
  931. }
  932. }
  933. and {
  934. (--,Is(beliefTerm,"==>"))
  935. (--,Is(taskTerm((1)),"1111000000000"))
  936. (--,Is(taskTerm((0,0)),"--"))
  937. unifyIf(task((0,0)),Unifiability,(belief(()),false,2048))
  938. forkable({-111,-109}) {
  939. 157 ==> {
  940. unify((((--,%1) ==>+- %2),%3)) ==> {
  941. (Termify(unisubst(%2,%1,%3,"$"),truth(punc((".",".")),DeductionPN,(),BeliefEvent)),157)
  942. }
  943. }
  944. 159 ==> {
  945. unify((((--,%1) ==>+- %2),%3)) ==> {
  946. (Termify((--,unisubst(%2,%1,%3,"$")),truth(punc((".",".")),DeductionNN,(),BeliefEvent)),159)
  947. }
  948. }
  949. }
  950. }
  951. and {
  952. IsHas(beliefTerm,("==>",volMin(3)))
  953. forkable({-87,-83,-76,-72,-48,-47}) {
  954. 181 ==> {
  955. unify((((--,%1) ==>+- %2),(%3 ==>+- %1))) ==> {
  956. (Termify((%3 ==>+- %2),truth(punc((".",".")),DeductionPN,(),Compose)),181)
  957. }
  958. }
  959. 185 ==> {
  960. unify((((--,%1) ==>+- %2),(%3 ==>+- %1))) ==> {
  961. (Termify((--,(%3 ==>+- %2)),truth(punc((".",".")),DeductionNN,(),Compose)),185)
  962. }
  963. }
  964. 192 ==> {
  965. unify((((--,%1) ==>+- %2),(%3 ==>+- %1))) ==> {
  966. (Termify((%2 ==>+- %3),truth(punc((".",".")),ExemplificationPN,(),Compose)),192)
  967. }
  968. }
  969. 196 ==> {
  970. unify((((--,%1) ==>+- %2),(%3 ==>+- %1))) ==> {
  971. (Termify(((--,%2) ==>+- %3),truth(punc((".",".")),ExemplificationNN,(),Compose)),196)
  972. }
  973. }
  974. 220 ==> {
  975. unify((((--,%1) ==>+- %2),(%2 ==>+- %1))) ==> {
  976. (Termify((--,(%1 ==>+- %2)),truth(punc((".",".")),IntersectionPN,(),Compose)),220)
  977. }
  978. }
  979. 221 ==> {
  980. unify((((--,%1) ==>+- %2),(%2 ==>+- %1))) ==> {
  981. (Termify(((--,%2) ==>+- %1),truth(punc((".",".")),IntersectionPN,(),Compose)),221)
  982. }
  983. }
  984. }
  985. }
  986. }
  987. }
  988. and {
  989. IsHas(taskTerm,("==>","&&",volMin(5)))
  990. fork {
  991. and {
  992. IsHas(beliefTerm,("==>","&&",volMin(5)))
  993. fork {
  994. and {
  995. IsHas(taskTerm((0)),("&&",volMin(3)))
  996. IsHas(beliefTerm((0)),("&&",volMin(3)))
  997. fork {
  998. and {
  999. (--,Is(taskTerm((1)),"#"))
  1000. forkable({214}) {
  1001. 226 ==> {
  1002. and {
  1003. unifyIf(%4,{(neq,%1),(eqNeg,%1)})
  1004. unifyIf(%1,{(neq,%4),(eqNeg,%4)})
  1005. unify((((%1 &&+- %2..+) ==>+- %3),((%4 &&+- %2..+) ==>+- %3))) ==> {
  1006. (Termify((( &&+- ,%2..+) ==>+- %3),truth(punc((".",".")),IntersectionPB,(),Compose)),226)
  1007. }
  1008. }
  1009. }
  1010. }
  1011. }
  1012. forkable({212}) {
  1013. 224 ==> {
  1014. unify((((%1 &&+- %2..+) ==>+- %3),((%4 &&+- %2..+) ==>+- %3))) ==> {
  1015. (Termify((%4 ==>+- %1),truth(punc((".",".")),InductionPB,(),Compose)),224)
  1016. }
  1017. }
  1018. }
  1019. }
  1020. }
  1021. and {
  1022. IsHas(taskTerm((1)),("&&",volMin(3)))
  1023. IsHas(beliefTerm((1)),("&&",volMin(3)))
  1024. (--,Is(taskTerm((0)),"#"))
  1025. forkable({216}) {
  1026. 228 ==> {
  1027. and {
  1028. unifyIf(%4,{(neq,%2),(eqNeg,%2)})
  1029. unifyIf(%2,{(neq,%4),(eqNeg,%4)})
  1030. unify(((%1 ==>+- (%2 &&+- %3..+)),(%1 ==>+- (%4 &&+- %3..+)))) ==> {
  1031. (Termify((%1 ==>+- ( &&+- ,%3..+)),truth(punc((".",".")),IntersectionPB,(),Compose)),228)
  1032. }
  1033. }
  1034. }
  1035. }
  1036. }
  1037. }
  1038. }
  1039. and {
  1040. IsHas(beliefTerm,("==>",volMin(3)))
  1041. IsHas(taskTerm((0)),("&&",volMin(3)))
  1042. ellipsisCommutativeConstant((0),(0),task)
  1043. forkable({-46,-45}) {
  1044. 222 ==> {
  1045. unify((((%1 &&+- %2..+) ==>+- %3),(%1 ==>+- %4))) ==> {
  1046. (Termify(((%4 &&+- %2..+) ==>+- %3),truth(punc((".",".")),Induction,(),Compose)),222)
  1047. }
  1048. }
  1049. 223 ==> {
  1050. unify((((%1 &&+- %2..+) ==>+- %3),(%1 ==>+- %4))) ==> {
  1051. (Termify((((--,%4) &&+- %2..+) ==>+- %3),truth(punc((".",".")),InductionPN,(),Compose)),223)
  1052. }
  1053. }
  1054. }
  1055. }
  1056. }
  1057. }
  1058. and {
  1059. unifyIf(task(()),Eventable,(()))
  1060. Is(beliefTerm,"&&")
  1061. unifyIf(belief(()),VolumeCompare,(task(()),onlyIfConstants))
  1062. unifyIf(belief(()),neq,task(()))
  1063. fork {
  1064. and {
  1065. (--,ConjParallel(beliefTerm))
  1066. fork {
  1067. and {
  1068. Has(beliefTerm,("--",any,volMin(0)))
  1069. unifyIf(belief(()),EventUnifiability,(task(()),true,true))
  1070. forkable({239}) {
  1071. 251 ==> {
  1072. unify((%1,%2)) ==> {
  1073. (Termify(conjBefore(%2,(--,%1)),truth(punc((".",".")),DeductionNP,(),TaskEvent)),251)
  1074. }
  1075. }
  1076. }
  1077. }
  1078. and {
  1079. unifyIf(belief(()),EventUnifiability,(task(()),false,true))
  1080. forkable({237}) {
  1081. 249 ==> {
  1082. unify((%1,%2)) ==> {
  1083. (Termify(conjBefore(%2,%1),truth(punc((".",".")),Deduction,(),TaskEvent)),249)
  1084. }
  1085. }
  1086. }
  1087. }
  1088. }
  1089. }
  1090. and {
  1091. Has(beliefTerm,("--",any,volMin(0)))
  1092. unifyIf(belief(()),EventUnifiability,(task(()),true,true))
  1093. forkable({234}) {
  1094. 246 ==> {
  1095. unify((%1,%2)) ==> {
  1096. (Termify(conjAfter(%2,(--,%1)),truth(punc((".",".")),DeductionNP,(),TaskEvent)),246)
  1097. }
  1098. }
  1099. }
  1100. }
  1101. and {
  1102. unifyIf(belief(()),EventUnifiability,(task(()),false,true))
  1103. forkable({232}) {
  1104. 244 ==> {
  1105. unify((%1,%2)) ==> {
  1106. (Termify(conjAfter(%2,%1),truth(punc((".",".")),Deduction,(),TaskEvent)),244)
  1107. }
  1108. }
  1109. }
  1110. }
  1111. }
  1112. }
  1113. and {
  1114. IsHas(beliefTerm,("==>",volMin(3)))
  1115. fork {
  1116. and {
  1117. (--,Is(taskTerm,"==>"))
  1118. fork {
  1119. and {
  1120. (--,Is(beliefTerm((0)),"--"))
  1121. (--,Is(beliefTerm((1)),"1111000000000"))
  1122. unifyIf(belief((0)),Unifiability,(task(()),false,2048))
  1123. forkable({-116,-114}) {
  1124. 152 ==> {
  1125. unify((%1,(%2 ==>+- %3))) ==> {
  1126. (Termify(unisubst(%3,%2,%1,"$"),truth(punc((".",".")),Deduction,(),TaskEvent)),152)
  1127. }
  1128. }
  1129. 154 ==> {
  1130. unify((%1,(%2 ==>+- %3))) ==> {
  1131. (Termify((--,unisubst(%3,%2,%1,"$")),truth(punc((".",".")),DeductionPN,(),TaskEvent)),154)
  1132. }
  1133. }
  1134. }
  1135. }
  1136. and {
  1137. (--,Is(beliefTerm((0)),"1111000000000"))
  1138. unifyIf(belief((1)),Unifiability,(task(()),false,2048))
  1139. forkable({-120,-119}) {
  1140. 148 ==> {
  1141. unify((%1,(%2 ==>+- %3))) ==> {
  1142. (Termify(unisubst(%2,%3,%1,"$"),truth(punc((".",".")),Abduction,(),TaskEvent)),148)
  1143. }
  1144. }
  1145. 149 ==> {
  1146. unify((%1,(%2 ==>+- %3))) ==> {
  1147. (Termify(unisubst(%2,%3,%1,"$"),truth(punc((".",".")),AbductionNN,(),TaskEvent)),149)
  1148. }
  1149. }
  1150. }
  1151. }
  1152. and {
  1153. Is(beliefTerm((0)),"&&")
  1154. forkable({-99,-98}) {
  1155. 169 ==> {
  1156. unify((%1,(%2 ==>+- %3))) ==> {
  1157. (Termify(unisubst(beliefTerm,chooseUnifiableSubEvent(%2,polarizeTask(%1)),polarizeTask(%1),novel),truth(punc((".",".")),DeductionDP,(),TaskEvent)),169)
  1158. }
  1159. }
  1160. 170 ==> {
  1161. unify((%1,(%2 ==>+- %3))) ==> {
  1162. (Termify((--,unisubst(beliefTerm,chooseUnifiableSubEvent(%2,polarizeTask(%1)),polarizeTask(%1),novel)),truth(punc((".",".")),DeductionDN,(),TaskEvent)),170)
  1163. }
  1164. }
  1165. }
  1166. }
  1167. and {
  1168. Is(beliefTerm((1)),"&&")
  1169. forkable({-101,-100}) {
  1170. 167 ==> {
  1171. unify((%1,(%2 ==>+- %3))) ==> {
  1172. (Termify(unisubst(beliefTerm,chooseUnifiableSubEvent(%3,polarizeTask(%1)),polarizeTask(%1),novel),truth(punc((".",".")),DeductionDP,(),TaskEvent)),167)
  1173. }
  1174. }
  1175. 168 ==> {
  1176. unify((%1,(%2 ==>+- %3))) ==> {
  1177. (Termify((--,unisubst(beliefTerm,chooseUnifiableSubEvent(%3,polarizeTask(%1)),polarizeTask(%1),novel)),truth(punc((".",".")),DeductionDN,(),TaskEvent)),168)
  1178. }
  1179. }
  1180. }
  1181. }
  1182. }
  1183. }
  1184. and {
  1185. Is(beliefTerm((0)),"&&")
  1186. forkable({161}) {
  1187. 173 ==> {
  1188. unify((%1,(%2 ==>+- %3))) ==> {
  1189. (Termify(conjWithoutUnify((polarizeBelief(%3) &&+- %2),polarizeTask(%1)),truth(punc((".",".")),DeductionDD,(),TaskEvent)),173)
  1190. }
  1191. }
  1192. }
  1193. }
  1194. }
  1195. }
  1196. and {
  1197. IsHas(taskTerm,("==>","100010",volMin(6)))
  1198. IsHas(beliefTerm,("==>","100010",volMin(6)))
  1199. IsHas(taskTerm((0)),("--","&&",volMin(4)))
  1200. IsHas(beliefTerm((0)),("--","&&",volMin(4)))
  1201. IsHas(beliefTerm((0,0)),("&&",volMin(3)))
  1202. fork {
  1203. and {
  1204. (--,Is(taskTerm((1)),"#"))
  1205. IsHas(taskTerm((0,0)),("&&",volMin(3)))
  1206. forkable({215}) {
  1207. 227 ==> {
  1208. and {
  1209. unifyIf(%4,{(neq,%1),(eqNeg,%1)})
  1210. unifyIf(%1,{(neq,%4),(eqNeg,%4)})
  1211. unify((((--,(%1 &&+- %2..+)) ==>+- %3),((--,(%4 &&+- %2..+)) ==>+- %3))) ==> {
  1212. (Termify(((--,( &&+- ,%2..+)) ==>+- %3),truth(punc((".",".")),IntersectionPB,(),Compose)),227)
  1213. }
  1214. }
  1215. }
  1216. }
  1217. }
  1218. and {
  1219. IsHas(taskTerm((0,0)),("&&",volMin(3)))
  1220. forkable({213}) {
  1221. 225 ==> {
  1222. unify((((--,(%1 &&+- %2..+)) ==>+- %3),((--,(%4 &&+- %2..+)) ==>+- %3))) ==> {
  1223. (Termify((%4 ==>+- %1),truth(punc((".",".")),InductionPB,(),Compose)),225)
  1224. }
  1225. }
  1226. }
  1227. }
  1228. }
  1229. }
  1230. and {
  1231. IsHas(taskTerm,("<->",volMin(3)))
  1232. fork {
  1233. and {
  1234. IsHas(beliefTerm,("-->",volMin(3)))
  1235. fork {
  1236. and {
  1237. Has(beliefTerm((0)),(".",any,volMin(0)))
  1238. fork {
  1239. and {
  1240. Has(beliefTerm((1)),(".",any,volMin(0)))
  1241. forkable({44}) {
  1242. 56 ==> {
  1243. unify(((%1<->%2),(%1-->%2))) ==> {
  1244. (Termify((%2-->%1),truth(punc((".",".")),Undesire,(),Compose)),56)
  1245. }
  1246. }
  1247. }
  1248. }
  1249. forkable({38}) {
  1250. 50 ==> {
  1251. and {
  1252. unifyIf(%3,{(neq,%2),(neqRCom,%2)})
  1253. unifyIf(%2,{(Has,((".",any,volMin(0)))),(neq,%3),(neqRCom,%3)})
  1254. unify(((%1<->%2),(%3-->%1))) ==> {
  1255. (Termify((%3-->%2),truth(punc((".",".")),AnalogyX,(),Compose)),50)
  1256. }
  1257. }
  1258. }
  1259. }
  1260. }
  1261. }
  1262. and {
  1263. Has(beliefTerm((1)),(".",any,volMin(0)))
  1264. forkable({42}) {
  1265. 54 ==> {
  1266. and {
  1267. unifyIf(%3,{(neq,%2),(neqRCom,%2)})
  1268. unifyIf(%2,{(Has,((".",any,volMin(0)))),(neq,%3),(neqRCom,%3)})
  1269. unify(((%1<->%2),(%1-->%3))) ==> {
  1270. (Termify((%2-->%3),truth(punc((".",".")),AnalogyX,(),Compose)),54)
  1271. }
  1272. }
  1273. }
  1274. }
  1275. }
  1276. }
  1277. }
  1278. and {
  1279. IsHas(beliefTerm,("<->",volMin(3)))
  1280. forkable({50}) {
  1281. 62 ==> {
  1282. and {
  1283. unifyIf(%3,{(Has,((".",any,volMin(0)))),(neq,%2),(neqRCom,%2)})
  1284. unifyIf(%2,{(Has,((".",any,volMin(0)))),(neq,%3),(neqRCom,%3)})
  1285. unify(((%1<->%2),(%1<->%3))) ==> {
  1286. (Termify((%2<->%3),truth(punc((".",".")),Resemblance,(),Compose)),62)
  1287. }
  1288. }
  1289. }
  1290. }
  1291. }
  1292. }
  1293. }
  1294. and {
  1295. (--,Is(beliefTerm,"1111000000000"))
  1296. Is(taskTerm,"&&")
  1297. unifyIf(task(()),neq,belief(()))
  1298. Has(taskTerm,("#",any,volMin(0)))
  1299. fork {
  1300. and {
  1301. Has(taskTerm,("--",any,volMin(0)))
  1302. forkable({274}) {
  1303. 286 ==> {
  1304. unify((%1,%2)) ==> {
  1305. (Termify(conjWithoutUnify(%1,chooseUnifiableSubEvent(%1,(--,%2))),truth(punc((".",".")),AnonymousAnalogyPN,(),BeliefEvent)),286)
  1306. }
  1307. }
  1308. }
  1309. }
  1310. forkable({273}) {
  1311. 285 ==> {
  1312. unify((%1,%2)) ==> {
  1313. (Termify(conjWithoutUnify(%1,chooseUnifiableSubEvent(%1,%2)),truth(punc((".",".")),AnonymousAnalogy,(),BeliefEvent)),285)
  1314. }
  1315. }
  1316. }
  1317. }
  1318. }
  1319. and {
  1320. IsHas(taskTerm,("&&","--",volMin(5)))
  1321. IsHas(beliefTerm,("&&","--",volMin(5)))
  1322. forkable({-34,-33,-32}) {
  1323. 234 ==> {
  1324. and {
  1325. unifyIf(%1,neq,%2)
  1326. unifyIf(%2,neq,%1)
  1327. unify((( &&+- ,(--,%1),%2,%3..*),( &&+- ,(--,%2),%1,%3..*))) ==> {
  1328. (Termify(((--,(%1 &&+- %2)) &&+- %3..*),truth(punc((".",".")),IntersectionPB,(),Compose)),234)
  1329. }
  1330. }
  1331. }
  1332. 235 ==> {
  1333. and {
  1334. unifyIf(%1,neq,%2)
  1335. unifyIf(%2,neq,%1)
  1336. unify((( &&+- ,(--,%1),%2,%3..*),( &&+- ,(--,%2),%1,%3..*))) ==> {
  1337. (Termify((--,(%2 ==>+- %1)),truth(punc((".",".")),AbductionPB,(),Compose)),235)
  1338. }
  1339. }
  1340. }
  1341. 236 ==> {
  1342. and {
  1343. unifyIf(%1,neq,%2)
  1344. unifyIf(%2,neq,%1)
  1345. unify((( &&+- ,(--,%1),%2,%3..*),( &&+- ,(--,%2),%1,%3..*))) ==> {
  1346. (Termify(((--,%1) ==>+- %2),truth(punc((".",".")),InductionPB,(),Compose)),236)
  1347. }
  1348. }
  1349. }
  1350. }
  1351. }
  1352. and {
  1353. IsHas(taskTerm,("&&","--",volMin(4)))
  1354. IsHas(beliefTerm,("&&",volMin(3)))
  1355. forkable({-36,-35}) {
  1356. 232 ==> {
  1357. unify((((--,%1) &&+- %2..+),(%1 &&+- %2..+))) ==> {
  1358. (Termify(( &&+- ,%2..+),truth(punc((".",".")),Union,(),Compose)),232)
  1359. }
  1360. }
  1361. 233 ==> {
  1362. unify((((--,%1) &&+- %2..+),(%1 &&+- %2..+))) ==> {
  1363. (Termify((--,( &&+- ,%2..+)),truth(punc((".",".")),UnionNN,(),Compose)),233)
  1364. }
  1365. }
  1366. }
  1367. }
  1368. and {
  1369. IsHas(beliefTerm,("&&","--",volMin(4)))
  1370. IsHas(taskTerm,("&&",volMin(3)))
  1371. forkable({-38,-37}) {
  1372. 230 ==> {
  1373. unify(((%1 &&+- %2..+),((--,%1) &&+- %2..+))) ==> {
  1374. (Termify(( &&+- ,%2..+),truth(punc((".",".")),Union,(),Compose)),230)
  1375. }
  1376. }
  1377. 231 ==> {
  1378. unify(((%1 &&+- %2..+),((--,%1) &&+- %2..+))) ==> {
  1379. (Termify((--,( &&+- ,%2..+)),truth(punc((".",".")),UnionNN,(),Compose)),231)
  1380. }
  1381. }
  1382. }
  1383. }
  1384. and {
  1385. (--,Is(taskTerm,"==>"))
  1386. fork {
  1387. and {
  1388. (--,Is(beliefTerm,"==>"))
  1389. forkable({-122,-121}) {
  1390. 146 ==> {
  1391. unify((%1,%2)) ==> {
  1392. (Termify((polarizeTask(%1) &&+- polarizeBelief(%2)),truth(punc((".",".")),IntersectionDD,(),Sequence)),146)
  1393. }
  1394. }
  1395. 147 ==> {
  1396. unify((%1,%2)) ==> {
  1397. (Termify(varIntro((polarizeTask(%1) &&+- polarizeBelief(%2))),truth(punc((".",".")),IntersectionDD,(),Sequence)),147)
  1398. }
  1399. }
  1400. }
  1401. }
  1402. forkable({-124,-123}) {
  1403. 144 ==> {
  1404. unify((%1,%2)) ==> {
  1405. (Termify(polarizeBelief((polarizeTask(%1) ==>+- %2)),truth(punc((".",".")),AbductionDD,(),TaskRelative)),144)
  1406. }
  1407. }
  1408. 145 ==> {
  1409. unify((%1,%2)) ==> {
  1410. (Termify(polarizeBelief(varIntro((polarizeTask(%1) ==>+- %2))),truth(punc((".",".")),AbductionDD,(),TaskRelative)),145)
  1411. }
  1412. }
  1413. }
  1414. }
  1415. }
  1416. and {
  1417. IsHas(beliefTerm,("<->",volMin(3)))
  1418. forkable({57,58,60,61}) {
  1419. 69 ==> {
  1420. and {
  1421. unifyIf(%3,{(Is,(--,("1111000000000"))),(neq,%1)})
  1422. unifyIf(%2,{(Unifiability,(%1,true,2048)),(Is,(--,("1111000000000"))),(neq,%1)})
  1423. unifyIf(%1,{(Unifiability,(%2,true,2048)),(neq,%2),(neq,%3)})
  1424. unify((%1,(%2<->%3))) ==> {
  1425. (Termify(unisubst(%3,%2,%1,"$",novel),truth(punc((".",".")),DesireWeak,(),TaskEvent)),69)
  1426. }
  1427. }
  1428. }
  1429. 70 ==> {
  1430. and {
  1431. unifyIf(%3,{(Is,(--,("1111000000000"))),(neq,%1)})
  1432. unifyIf(%2,{(Unifiability,(%1,true,2048)),(Is,(--,("1111000000000"))),(neq,%1)})
  1433. unifyIf(%1,{(Unifiability,(%2,true,2048)),(neq,%2),(neq,%3)})
  1434. unify((%1,(%2<->%3))) ==> {
  1435. (Termify((--,unisubst(%3,%2,%1,"$",novel)),truth(punc((".",".")),DesireWeakPN,(),TaskEvent)),70)
  1436. }
  1437. }
  1438. }
  1439. 72 ==> {
  1440. and {
  1441. unifyIf(%3,neq,%1)
  1442. unifyIf(%2,{(neq,%1),(VolumeCompare,%1),("Recursive<-(+)",%1)})
  1443. unifyIf(%1,{(neq,%2),(neq,%3),(VolumeCompare,%2),("Recursive->(+)",%2)})
  1444. unify((%1,(%2<->%3))) ==> {
  1445. (Termify(substitute(%1,%2,%3,"$",novel),truth(punc((".",".")),DesireWeak,(),Task)),72)
  1446. }
  1447. }
  1448. }
  1449. 73 ==> {
  1450. and {
  1451. unifyIf(%3,neq,%1)
  1452. unifyIf(%2,{(neq,%1),(VolumeCompare,%1),("Recursive<-(+)",%1)})
  1453. unifyIf(%1,{(neq,%2),(neq,%3),(VolumeCompare,%2),("Recursive->(+)",%2)})
  1454. unify((%1,(%2<->%3))) ==> {
  1455. (Termify(substitute(%1,%2,(--,%3),"$",novel),truth(punc((".",".")),DesireWeakPN,(),Task)),73)
  1456. }
  1457. }
  1458. }
  1459. }
  1460. }
  1461. and {
  1462. (--,Is(beliefTerm,"==>"))
  1463. forkable({-126,-125}) {
  1464. 142 ==> {
  1465. unify((%1,%2)) ==> {
  1466. (Termify(polarizeTask((polarizeBelief(%2) ==>+- %1)),truth(punc((".",".")),InductionDD,(),BeliefRelative)),142)
  1467. }
  1468. }
  1469. 143 ==> {
  1470. unify((%1,%2)) ==> {
  1471. (Termify(polarizeTask(varIntro((polarizeBelief(%2) ==>+- %1))),truth(punc((".",".")),InductionDD,(),BeliefRelative)),143)
  1472. }
  1473. }
  1474. }
  1475. }
  1476. }
  1477. }
  1478. and {
  1479. (--,Is(beliefTerm,"1111000000000"))
  1480. fork {
  1481. and {
  1482. IsHas(taskTerm,("==>","--",volMin(4)))
  1483. unifyIf(belief(()),Eventable,(()))
  1484. IsHas(taskTerm((0)),("--",volMin(2)))
  1485. {(--,Is(taskTerm((0,0)),"--")),Is(taskTerm((0,0)),"&&")}
  1486. unifyIf(task((0,0)),VolumeCompare,belief(()))
  1487. unifyIf(task((0,0)),neq,belief(()))
  1488. unifyIf(task((0,0)),"Event->(+|-)",belief(()))
  1489. forkable({261}) {
  1490. 273 ==> {
  1491. unify((((--,%1) ==>+- %2),%3)) ==> {
  1492. (Termify(((--,conjWithoutPN(%1,%3)) ==>+- %2),truth(punc((".",".")),StructuralReduction,(),Task)),273)
  1493. }
  1494. }
  1495. }
  1496. }
  1497. and {
  1498. unifyIf(belief(()),Eventable,(()))
  1499. IsHas(taskTerm,("==>",volMin(3)))
  1500. Is(taskTerm((1)),"&&")
  1501. unifyIf(task((1)),VolumeCompare,belief(()))
  1502. unifyIf(task((1)),neq,belief(()))
  1503. unifyIf(task((1)),"Event->(+|-)",belief(()))
  1504. forkable({262}) {
  1505. 274 ==> {
  1506. unify(((%1 ==>+- %2),%3)) ==> {
  1507. (Termify(polarizeTask((%1 ==>+- conjWithoutPN(%2,%3))),truth(punc((".",".")),StructuralDeductionDD,(),Task)),274)
  1508. }
  1509. }
  1510. }
  1511. }
  1512. }
  1513. }
  1514. }
  1515. }
  1516. and {
  1517. punc(("?","."))
  1518. DoublePremise(({"?","@"}),punc)
  1519. fork {
  1520. and {
  1521. IsHas(beliefTerm,("-->",volMin(3)))
  1522. fork {
  1523. and {
  1524. IsHas(taskTerm,("-->",volMin(3)))
  1525. {Is(taskTerm((0)),"*"),SubsMin(taskTerm((0)),1)}
  1526. Is(taskTerm((1)),"*")
  1527. unifyIf(task((0)),VolumeCompare,belief((0)))
  1528. unifyIf(task((1)),VolumeCompare,belief((1)))
  1529. SubsMin(taskTerm((1)),1)
  1530. unifyIf(task((0)),neq,belief((0)))
  1531. unifyIf(task((1)),neq,belief((1)))
  1532. fork {
  1533. and {
  1534. unifyIf(task((0)),"Subterm->(+)",belief((0)))
  1535. fork {
  1536. and {
  1537. unifyIf(task((1)),"Subterm->(+)",belief((1)))
  1538. forkable({123}) {
  1539. 135 ==> {
  1540. unify(((%1-->%2),(%3-->%4))) ==> {
  1541. (Termify(taskTerm,truth(punc(("?",".")),BeliefStructuralReduction,(),Task)),135)
  1542. }
  1543. }
  1544. }
  1545. }
  1546. and {
  1547. unifyIf(task((1)),"SubtermNeg->(+)",belief((1)))
  1548. forkable({126}) {
  1549. 138 ==> {
  1550. unify(((%1-->%2),(%3-->%4))) ==> {
  1551. (Termify((--,taskTerm),truth(punc(("?",".")),BeliefStructuralReduction,(),Task)),138)
  1552. }
  1553. }
  1554. }
  1555. }
  1556. }
  1557. }
  1558. and {
  1559. unifyIf(task((0)),"SubtermNeg->(+)",belief((0)))
  1560. fork {
  1561. and {
  1562. unifyIf(task((1)),"Subterm->(+)",belief((1)))
  1563. forkable({125}) {
  1564. 137 ==> {
  1565. unify(((%1-->%2),(%3-->%4))) ==> {
  1566. (Termify((--,taskTerm),truth(punc(("?",".")),BeliefStructuralReduction,(),Task)),137)
  1567. }
  1568. }
  1569. }
  1570. }
  1571. and {
  1572. unifyIf(task((1)),"SubtermNeg->(+)",belief((1)))
  1573. forkable({124}) {
  1574. 136 ==> {
  1575. unify(((%1-->%2),(%3-->%4))) ==> {
  1576. (Termify(taskTerm,truth(punc(("?",".")),BeliefStructuralReduction,(),Task)),136)
  1577. }
  1578. }
  1579. }
  1580. }
  1581. }
  1582. }
  1583. }
  1584. }
  1585. and {
  1586. IsHas(taskTerm,("-->","[",volMin(4)))
  1587. fork {
  1588. and {
  1589. IsHas(taskTerm((0)),("[",volMin(2)))
  1590. Is(beliefTerm((0)),"[")
  1591. unifyIf(belief((0)),VolumeCompare,task((0,0)))
  1592. unifyIf(belief((0)),neq,task((0,0)))
  1593. unifyIf(belief((0)),"Subterm->(+)",task((0,0)))
  1594. forkable({84}) {
  1595. 96 ==> {
  1596. unify((([%1]-->%2),(%3-->%2))) ==> {
  1597. (Termify(taskTerm,truth(punc(("?",".")),BeliefStructuralDeduction,(),Belief)),96)
  1598. }
  1599. }
  1600. }
  1601. }
  1602. and {
  1603. IsHas(taskTerm((1)),("[",volMin(2)))
  1604. Is(beliefTerm((1)),"[")
  1605. unifyIf(belief((1)),VolumeCompare,task((1,0)))
  1606. unifyIf(belief((1)),neq,task((1,0)))
  1607. unifyIf(belief((1)),"Subterm->(+)",task((1,0)))
  1608. forkable({86}) {
  1609. 98 ==> {
  1610. unify(((%1-->[%2]),(%1-->%3))) ==> {
  1611. (Termify(taskTerm,truth(punc(("?",".")),BeliefStructuralDeduction,(),Belief)),98)
  1612. }
  1613. }
  1614. }
  1615. }
  1616. }
  1617. }
  1618. and {
  1619. IsHas(taskTerm,("-->","{",volMin(4)))
  1620. fork {
  1621. and {
  1622. IsHas(taskTerm((0)),("{",volMin(2)))
  1623. Is(beliefTerm((0)),"{")
  1624. unifyIf(belief((0)),VolumeCompare,task((0,0)))
  1625. unifyIf(belief((0)),neq,task((0,0)))
  1626. unifyIf(belief((0)),"Subterm->(+)",task((0,0)))
  1627. forkable({83}) {
  1628. 95 ==> {
  1629. unify((({%1}-->%2),(%3-->%2))) ==> {
  1630. (Termify(taskTerm,truth(punc(("?",".")),BeliefStructuralDeduction,(),Belief)),95)
  1631. }
  1632. }
  1633. }
  1634. }
  1635. and {
  1636. IsHas(taskTerm((1)),("{",volMin(2)))
  1637. Is(beliefTerm((1)),"{")
  1638. unifyIf(belief((1)),VolumeCompare,task((1,0)))
  1639. unifyIf(belief((1)),neq,task((1,0)))
  1640. unifyIf(belief((1)),"Subterm->(+)",task((1,0)))
  1641. forkable({85}) {
  1642. 97 ==> {
  1643. unify(((%1-->{%2}),(%1-->%3))) ==> {
  1644. (Termify(taskTerm,truth(punc(("?",".")),BeliefStructuralDeduction,(),Belief)),97)
  1645. }
  1646. }
  1647. }
  1648. }
  1649. }
  1650. }
  1651. and {
  1652. IsHas(taskTerm,("-->","*",volMin(5)))
  1653. fork {
  1654. and {
  1655. IsHas(taskTerm((0)),("*",volMin(2)))
  1656. IsHas(taskTerm((1)),("*",volMin(2)))
  1657. forkable({119}) {
  1658. 131 ==> {
  1659. unify((((%1)-->(%2)),(%1-->%2))) ==> {
  1660. (Termify(polarizeBelief(taskTerm),truth(punc(("?",".")),BeliefStructuralReductionDD,(),Belief)),131)
  1661. }
  1662. }
  1663. }
  1664. }
  1665. and {
  1666. IsHas(taskTerm((0)),("*",volMin(3)))
  1667. Is(taskTerm((1)),"?")
  1668. forkable({128}) {
  1669. 140 ==> {
  1670. unify((((%1,%2)-->%3),(%1-->%4))) ==> {
  1671. (Termify(((%1,%2)-->(%4,%2)),truth(punc(("?",".")),BeliefStructuralReduction,(),Belief)),140)
  1672. }
  1673. }
  1674. }
  1675. }
  1676. and {
  1677. IsHas(taskTerm((1)),("*",volMin(3)))
  1678. Is(taskTerm((0)),"?")
  1679. forkable({129}) {
  1680. 141 ==> {
  1681. unify(((%1-->(%2,%3)),(%4-->%2))) ==> {
  1682. (Termify(((%4,%3)-->(%2,%3)),truth(punc(("?",".")),BeliefStructuralReduction,(),Belief)),141)
  1683. }
  1684. }
  1685. }
  1686. }
  1687. }
  1688. }
  1689. }
  1690. }
  1691. and {
  1692. DoublePremise()
  1693. fork {
  1694. and {
  1695. IsHas(taskTerm,("==>","--",volMin(4)))
  1696. (--,Is(beliefTerm((1)),"1111000000000"))
  1697. fork {
  1698. and {
  1699. IsHas(beliefTerm,("==>","--",volMin(4)))
  1700. IsHas(taskTerm((0)),("--",volMin(2)))
  1701. IsHas(beliefTerm((0)),("--",volMin(2)))
  1702. (--,Is(taskTerm((1)),"1111000000000"))
  1703. forkable({301}) {
  1704. 313 ==> {
  1705. unify((((--,%1) ==>+- %2),((--,%2) ==>+- %1))) ==> {
  1706. (Termify((--,((--,%1) ==>+- %2)),truth(punc(("?",".")),ConversionPN,(),Compose)),313)
  1707. }
  1708. }
  1709. }
  1710. }
  1711. and {
  1712. IsHas(beliefTerm,("==>",volMin(3)))
  1713. IsHas(taskTerm((0)),("--",volMin(2)))
  1714. (--,Is(taskTerm((1)),"1111000000000"))
  1715. forkable({299}) {
  1716. 311 ==> {
  1717. unify((((--,%1) ==>+- %2),(%2 ==>+- %1))) ==> {
  1718. (Termify(((--,%1) ==>+- %2),truth(punc(("?",".")),ConversionPN,(),Compose)),311)
  1719. }
  1720. }
  1721. }
  1722. }
  1723. }
  1724. }
  1725. and {
  1726. (--,Is(taskTerm((1)),"1111000000000"))
  1727. fork {
  1728. and {
  1729. IsHas(beliefTerm,("==>","--",volMin(4)))
  1730. IsHas(taskTerm,("==>",volMin(3)))
  1731. IsHas(beliefTerm((0)),("--",volMin(2)))
  1732. (--,Is(taskTerm((0)),"1111000000000"))
  1733. forkable({300}) {
  1734. 312 ==> {
  1735. unify(((%1 ==>+- %2),((--,%2) ==>+- %1))) ==> {
  1736. (Termify((--,(%1 ==>+- %2)),truth(punc(("?",".")),Conversion,(),Compose)),312)
  1737. }
  1738. }
  1739. }
  1740. }
  1741. and {
  1742. IsHas(taskTerm,("==>",volMin(3)))
  1743. IsHas(beliefTerm,("==>",volMin(3)))
  1744. (--,Is(taskTerm((0)),"1111000000000"))
  1745. forkable({298}) {
  1746. 310 ==> {
  1747. unify(((%1 ==>+- %2),(%2 ==>+- %1))) ==> {
  1748. (Termify((%1 ==>+- %2),truth(punc(("?",".")),Conversion,(),Compose)),310)
  1749. }
  1750. }
  1751. }
  1752. }
  1753. }
  1754. }
  1755. and {
  1756. IsHas(taskTerm,("-->",volMin(3)))
  1757. IsHas(beliefTerm,("<->",volMin(3)))
  1758. forkable({34}) {
  1759. 46 ==> {
  1760. unify(((%1-->%2),(%1<->%2))) ==> {
  1761. (Termify(taskTerm,truth(punc(("?",".")),BeliefStructuralIntersection,(),Belief)),46)
  1762. }
  1763. }
  1764. }
  1765. }
  1766. and {
  1767. IsHas(taskTerm,("<->",volMin(3)))
  1768. IsHas(beliefTerm,("-->",volMin(3)))
  1769. forkable({35}) {
  1770. 47 ==> {
  1771. unify(((%1<->%2),(%2-->%1))) ==> {
  1772. (Termify(taskTerm,truth(punc(("?",".")),BeliefStructuralAbduction,(),Belief)),47)
  1773. }
  1774. }
  1775. }
  1776. }
  1777. }
  1778. }
  1779. and {
  1780. IsHas(taskTerm,("-->","[",volMin(5)))
  1781. IsHas(taskTerm((1)),("[",volMin(2)))
  1782. fork {
  1783. and {
  1784. IsHas(beliefTerm,("-->",volMin(3)))
  1785. IsHas(taskTerm((0)),("[",volMin(2)))
  1786. ellipsisCommutativeConstant((0),(0),task)
  1787. ellipsisCommutativeConstant((1),(1),task)
  1788. forkable({92}) {
  1789. 104 ==> {
  1790. unify((([%1]-->[%2]),(%1-->%2))) ==> {
  1791. (Termify(polarizeBelief(taskTerm),truth(punc(("?",".")),BeliefStructuralDeductionDD,(),Belief)),104)
  1792. }
  1793. }
  1794. }
  1795. }
  1796. and {
  1797. IsHas(beliefTerm,("<->",volMin(3)))
  1798. IsHas(taskTerm((0)),("[",volMin(2)))
  1799. forkable({90}) {
  1800. 102 ==> {
  1801. unify((([%1]-->[%2]),(%1<->%2))) ==> {
  1802. (Termify(polarizeBelief(taskTerm),truth(punc(("?",".")),BeliefStructuralDeductionDD,(),Belief)),102)
  1803. }
  1804. }
  1805. }
  1806. }
  1807. }
  1808. }
  1809. and {
  1810. IsHas(taskTerm,("-->","{",volMin(5)))
  1811. IsHas(taskTerm((0)),("{",volMin(2)))
  1812. fork {
  1813. and {
  1814. IsHas(beliefTerm,("-->",volMin(3)))
  1815. IsHas(taskTerm((1)),("{",volMin(2)))
  1816. ellipsisCommutativeConstant((0),(0),task)
  1817. ellipsisCommutativeConstant((1),(1),task)
  1818. forkable({93}) {
  1819. 105 ==> {
  1820. unify((({%1}-->{%2}),(%1-->%2))) ==> {
  1821. (Termify(polarizeBelief(taskTerm),truth(punc(("?",".")),BeliefStructuralDeductionDD,(),Belief)),105)
  1822. }
  1823. }
  1824. }
  1825. }
  1826. and {
  1827. IsHas(beliefTerm,("<->",volMin(3)))
  1828. IsHas(taskTerm((1)),("{",volMin(2)))
  1829. forkable({91}) {
  1830. 103 ==> {
  1831. unify((({%1}-->{%2}),(%1<->%2))) ==> {
  1832. (Termify(polarizeBelief(taskTerm),truth(punc(("?",".")),BeliefStructuralDeductionDD,(),Belief)),103)
  1833. }
  1834. }
  1835. }
  1836. }
  1837. }
  1838. }
  1839. and {
  1840. unifyIf(belief(()),Eventable,(()))
  1841. Is(taskTerm,"&&")
  1842. unifyIf(task(()),VolumeCompare,belief(()))
  1843. fork {
  1844. and {
  1845. Has(taskTerm,("--",any,volMin(0)))
  1846. unifyIf(task(()),"Event->(-)",belief(()))
  1847. forkable({230}) {
  1848. 242 ==> {
  1849. unify((%1,%2)) ==> {
  1850. (Termify(%1,truth(punc(("?",".")),BeliefStructuralDeduction,(),BeliefEvent)),242)
  1851. }
  1852. }
  1853. }
  1854. }
  1855. and {
  1856. unifyIf(task(()),"Event->(+)",belief(()))
  1857. forkable({229}) {
  1858. 241 ==> {
  1859. unify((%1,%2)) ==> {
  1860. (Termify((--,%1),truth(punc(("?",".")),BeliefStructuralDeductionPN,(),BeliefEvent)),241)
  1861. }
  1862. }
  1863. }
  1864. }
  1865. }
  1866. }
  1867. and {
  1868. IsHas(beliefTerm,("-->","*",volMin(5)))
  1869. IsHas(taskTerm,("-->",volMin(3)))
  1870. IsHas(beliefTerm((0)),("*",volMin(2)))
  1871. IsHas(beliefTerm((1)),("*",volMin(2)))
  1872. forkable({121}) {
  1873. 133 ==> {
  1874. unify(((%1-->%2),((%1)-->(%2)))) ==> {
  1875. (Termify(polarizeBelief(taskTerm),truth(punc(("?",".")),BeliefStructuralReductionDD,(),Belief)),133)
  1876. }
  1877. }
  1878. }
  1879. }
  1880. and {
  1881. IsHas(beliefTerm,("==>",volMin(3)))
  1882. (--,Is(taskTerm,"1111000000000"))
  1883. fork {
  1884. and {
  1885. IsUnneg(beliefTerm((0)),"#")
  1886. forkable({247}) {
  1887. 259 ==> {
  1888. unify((%1,(%2 ==>+- %1))) ==> {
  1889. (Termify(%1,truth(punc(("?",".")),BeliefStructuralReduction,(),TaskEvent)),259)
  1890. }
  1891. }
  1892. }
  1893. }
  1894. and {
  1895. Is(beliefTerm((1)),"#")
  1896. forkable({248}) {
  1897. 260 ==> {
  1898. unify((%1,(%1 ==>+- %2))) ==> {
  1899. (Termify(%1,truth(punc(("?",".")),BeliefStructuralAbduction,(),TaskEvent)),260)
  1900. }
  1901. }
  1902. }
  1903. }
  1904. }
  1905. }
  1906. and {
  1907. IsHas(beliefTerm,("==>","--",volMin(4)))
  1908. (--,Is(taskTerm,"1111000000000"))
  1909. IsHas(beliefTerm((0)),("--",volMin(2)))
  1910. Is(beliefTerm((1)),"#")
  1911. forkable({249}) {
  1912. 261 ==> {
  1913. unify((%1,((--,%1) ==>+- %2))) ==> {
  1914. (Termify((--,%1),truth(punc(("?",".")),BeliefStructuralAbduction,(),TaskEvent)),261)
  1915. }
  1916. }
  1917. }
  1918. }
  1919. and {
  1920. IsHas(beliefTerm,("<->",volMin(3)))
  1921. fork {
  1922. and {
  1923. IsHas(taskTerm,("<->","[",volMin(5)))
  1924. forkable({88}) {
  1925. 100 ==> {
  1926. unify((([%1]<->[%2]),(%1<->%2))) ==> {
  1927. (Termify(polarizeBelief(taskTerm),truth(punc(("?",".")),BeliefStructuralDeductionDD,(),Belief)),100)
  1928. }
  1929. }
  1930. }
  1931. }
  1932. and {
  1933. IsHas(taskTerm,("<->",volMin(3)))
  1934. forkable({127}) {
  1935. 139 ==> {
  1936. and {
  1937. unifyIf(%3,{(neq,%1),(VolumeCompare,%1),("Subterm<-(+)",%1)})
  1938. unifyIf(%4,{(neq,%2),(VolumeCompare,%2),("Subterm<-(+)",%2)})
  1939. unifyIf(%1,{(Is,("*")),(SubsMin,(1)),(neq,%3),(VolumeCompare,%3),("Subterm->(+)",%3)})
  1940. unifyIf(%2,{(Is,("*")),(SubsMin,(1)),(neq,%4),(VolumeCompare,%4),("Subterm->(+)",%4)})
  1941. unify(((%1<->%2),(%3<->%4))) ==> {
  1942. (Termify(taskTerm,truth(punc(("?",".")),BeliefStructuralReduction,(),Task)),139)
  1943. }
  1944. }
  1945. }
  1946. }
  1947. }
  1948. }
  1949. }
  1950. and {
  1951. IsHas(taskTerm,("<->","*",volMin(5)))
  1952. IsHas(beliefTerm,("<->",volMin(3)))
  1953. forkable({120}) {
  1954. 132 ==> {
  1955. unify((((%1)<->(%2)),(%1<->%2))) ==> {
  1956. (Termify(polarizeBelief(taskTerm),truth(punc(("?",".")),BeliefStructuralReductionDD,(),Belief)),132)
  1957. }
  1958. }
  1959. }
  1960. }
  1961. and {
  1962. IsHas(taskTerm,("<->","{",volMin(5)))
  1963. IsHas(beliefTerm,("<->",volMin(3)))
  1964. forkable({89}) {
  1965. 101 ==> {
  1966. unify((({%1}<->{%2}),(%1<->%2))) ==> {
  1967. (Termify(polarizeBelief(taskTerm),truth(punc(("?",".")),BeliefStructuralDeductionDD,(),Belief)),101)
  1968. }
  1969. }
  1970. }
  1971. }
  1972. and {
  1973. IsHas(beliefTerm,("<->","*",volMin(5)))
  1974. IsHas(taskTerm,("<->",volMin(3)))
  1975. forkable({122}) {
  1976. 134 ==> {
  1977. unify(((%1<->%2),((%1)<->(%2)))) ==> {
  1978. (Termify(polarizeBelief(taskTerm),truth(punc(("?",".")),BeliefStructuralReductionDD,(),Belief)),134)
  1979. }
  1980. }
  1981. }
  1982. }
  1983. }
  1984. }
  1985. and {
  1986. punc({("?","?"),("@","@")})
  1987. fork {
  1988. and {
  1989. DoublePremise()
  1990. fork {
  1991. and {
  1992. IsHas(beliefTerm,("==>",volMin(3)))
  1993. fork {
  1994. and {
  1995. unifyIf(task(()),Eventable,(()))
  1996. fork {
  1997. and {
  1998. Is(beliefTerm((0)),"&&")
  1999. unifyIf(belief((0)),VolumeCompare,task(()))
  2000. unifyIf(belief((0)),neq,task(()))
  2001. unifyIf(belief((0)),"Event->(+|-)",task(()))
  2002. forkable({271}) {
  2003. 283 ==> {
  2004. unify((%1,(%2 ==>+- %3))) ==> {
  2005. (Termify((conjWithoutPN(%2,%1) ==>+- %3),truth(punc({("?","?"),("@","@")}),(),(),TaskEvent)),283)
  2006. }
  2007. }
  2008. }
  2009. }
  2010. and {
  2011. Is(beliefTerm((1)),"&&")
  2012. unifyIf(belief((1)),VolumeCompare,task(()))
  2013. unifyIf(belief((1)),neq,task(()))
  2014. unifyIf(belief((1)),"Event->(+|-)",task(()))
  2015. forkable({270}) {
  2016. 282 ==> {
  2017. unify((%1,(%2 ==>+- %3))) ==> {
  2018. (Termify((%2 ==>+- conjWithoutPN(%3,%1)),truth(punc({("?","?"),("@","@")}),(),(),TaskEvent)),282)
  2019. }
  2020. }
  2021. }
  2022. }
  2023. }
  2024. }
  2025. fork {
  2026. and {
  2027. (--,Is(beliefTerm((0)),"1111000000000"))
  2028. unifyIf(belief((1)),Unifiability,(task(()),false,6144))
  2029. forkable({282}) {
  2030. 294 ==> {
  2031. unify((%1,(%2 ==>+- %3))) ==> {
  2032. (Termify(unisubst(%2,%3,%1),truth(punc({("?","?"),("@","@")}),(),(),BeliefEvent)),294)
  2033. }
  2034. }
  2035. }
  2036. }
  2037. and {
  2038. (--,Is(beliefTerm((1)),"1111000000000"))
  2039. unifyIf(belief((0)),Unifiability,(task(()),false,6144))
  2040. forkable({278}) {
  2041. 290 ==> {
  2042. unify((%1,(%2 ==>+- %3))) ==> {
  2043. (Termify(unisubst(%3,%2,%1),truth(punc({("?","?"),("@","@")}),(),(),BeliefEvent)),290)
  2044. }
  2045. }
  2046. }
  2047. }
  2048. }
  2049. }
  2050. }
  2051. and {
  2052. IsHas(beliefTerm,("==>","--",volMin(4)))
  2053. IsHas(beliefTerm((0)),("--",volMin(2)))
  2054. fork {
  2055. and {
  2056. unifyIf(task(()),Eventable,(()))
  2057. Is(beliefTerm((0,0)),"&&")
  2058. unifyIf(belief((0,0)),VolumeCompare,task(()))
  2059. unifyIf(belief((0,0)),neq,task(()))
  2060. unifyIf(belief((0,0)),"Event->(+|-)",task(()))
  2061. forkable({272}) {
  2062. 284 ==> {
  2063. unify((%1,((--,%2) ==>+- %3))) ==> {
  2064. (Termify(((--,conjWithoutPN(%2,%1)) ==>+- %3),truth(punc({("?","?"),("@","@")}),(),(),TaskEvent)),284)
  2065. }
  2066. }
  2067. }
  2068. }
  2069. and {
  2070. (--,Is(beliefTerm((1)),"1111000000000"))
  2071. unifyIf(belief((0,0)),Unifiability,(task(()),false,6144))
  2072. forkable({280}) {
  2073. 292 ==> {
  2074. unify((%1,((--,%2) ==>+- %3))) ==> {
  2075. (Termify(unisubst(%3,%2,%1),truth(punc({("?","?"),("@","@")}),(),(),BeliefEvent)),292)
  2076. }
  2077. }
  2078. }
  2079. }
  2080. }
  2081. }
  2082. and {
  2083. IsHas(taskTerm,("-->",volMin(3)))
  2084. IsHas(beliefTerm,("-->",volMin(3)))
  2085. fork {
  2086. and {
  2087. unifyIf(task((0)),neq,belief((0)))
  2088. unifyIf(task((0)),notSetsOrDifferentSets,belief((0)))
  2089. unifyIf(task((0)),neqRCom,belief((0)))
  2090. forkable({95}) {
  2091. 107 ==> {
  2092. unify(((%1-->%2),(%3-->%2))) ==> {
  2093. (Termify((interSect(%1,polarizeBelief(%3))-->%2),truth(punc({("?","?"),("@","@")}),(),(),Compose)),107)
  2094. }
  2095. }
  2096. }
  2097. }
  2098. and {
  2099. unifyIf(task((1)),neq,belief((1)))
  2100. unifyIf(task((1)),notSetsOrDifferentSets,belief((1)))
  2101. unifyIf(task((1)),neqRCom,belief((1)))
  2102. forkable({94}) {
  2103. 106 ==> {
  2104. unify(((%1-->%2),(%1-->%3))) ==> {
  2105. (Termify((%1-->interSect(%2,polarizeBelief(%3))),truth(punc({("?","?"),("@","@")}),(),(),Compose)),106)
  2106. }
  2107. }
  2108. }
  2109. }
  2110. }
  2111. }
  2112. and {
  2113. IsHas(taskTerm,("==>",volMin(3)))
  2114. fork {
  2115. and {
  2116. (--,Is(taskTerm((0)),"1111000000000"))
  2117. unifyIf(task((1)),Unifiability,(belief(()),false,6144))
  2118. forkable({283}) {
  2119. 295 ==> {
  2120. unify(((%1 ==>+- %2),%3)) ==> {
  2121. (Termify(unisubst(%1,%2,%3),truth(punc({("?","?"),("@","@")}),(),(),TaskEvent)),295)
  2122. }
  2123. }
  2124. }
  2125. }
  2126. and {
  2127. (--,Is(taskTerm((1)),"1111000000000"))
  2128. unifyIf(task((0)),Unifiability,(belief(()),false,6144))
  2129. forkable({279}) {
  2130. 291 ==> {
  2131. unify(((%1 ==>+- %2),%3)) ==> {
  2132. (Termify(unisubst(%2,%1,%3),truth(punc({("?","?"),("@","@")}),(),(),TaskEvent)),291)
  2133. }
  2134. }
  2135. }
  2136. }
  2137. }
  2138. }
  2139. and {
  2140. IsHas(taskTerm,("==>","--",volMin(4)))
  2141. IsHas(taskTerm((0)),("--",volMin(2)))
  2142. (--,Is(taskTerm((1)),"1111000000000"))
  2143. unifyIf(task((0,0)),Unifiability,(belief(()),false,6144))
  2144. forkable({281}) {
  2145. 293 ==> {
  2146. unify((((--,%1) ==>+- %2),%3)) ==> {
  2147. (Termify(unisubst(%2,%1,%3),truth(punc({("?","?"),("@","@")}),(),(),TaskEvent)),293)
  2148. }
  2149. }
  2150. }
  2151. }
  2152. }
  2153. }
  2154. and {
  2155. IsHas(taskTerm,("-->",volMin(3)))
  2156. fork {
  2157. and {
  2158. IsHas(beliefTerm,("-->",volMin(3)))
  2159. fork {
  2160. and {
  2161. unifyIf(task((0)),neq,belief((0)))
  2162. fork {
  2163. and {
  2164. unifyIf(task((0)),neqRCom,belief((0)))
  2165. forkable({5,19,24}) {
  2166. 17 ==> {
  2167. unify(((%1-->%2),(%3-->%2))) ==> {
  2168. (Termify((%1-->%3),truth(punc({("?","?"),("@","@")}),(),(),Task)),17)
  2169. }
  2170. }
  2171. 31 ==> {
  2172. unify(((%1-->%2),(%3-->%2))) ==> {
  2173. (Termify((%3-->%1),truth(punc({("?","?"),("@","@")}),(),(),Task)),31)
  2174. }
  2175. }
  2176. 36 ==> {
  2177. unify(((%1-->%2),(%3-->%2))) ==> {
  2178. (Termify((%3-->%1),truth(punc({("?","?"),("@","@")}),(),(),Task)),36)
  2179. }
  2180. }
  2181. }
  2182. }
  2183. and {
  2184. Is(taskTerm((0)),"?")
  2185. forkable({30,31}) {
  2186. 42 ==> {
  2187. unify(((%1-->%2),(%3-->%2))) ==> {
  2188. (Termify((%3-->?4),truth(punc({("?","?"),("@","@")}),(),(),Task)),42)
  2189. }
  2190. }
  2191. 43 ==> {
  2192. unify(((%1-->%2),(%3-->%2))) ==> {
  2193. (Termify((?4-->%3),truth(punc({("?","?"),("@","@")}),(),(),Task)),43)
  2194. }
  2195. }
  2196. }
  2197. }
  2198. }
  2199. }
  2200. and {
  2201. Has(taskTerm((0)),(".",any,volMin(0)))
  2202. Has(taskTerm((1)),(".",any,volMin(0)))
  2203. forkable({45}) {
  2204. 57 ==> {
  2205. unify(((%1-->%2),(%2-->%1))) ==> {
  2206. (Termify((%1<->%2),truth(punc({("?","?"),("@","@")}),(),(),Task)),57)
  2207. }
  2208. }
  2209. }
  2210. }
  2211. and {
  2212. unifyIf(task((0)),neq,belief((1)))
  2213. unifyIf(task((0)),neqRCom,belief((1)))
  2214. forkable({12,16,27}) {
  2215. 24 ==> {
  2216. unify(((%1-->%2),(%2-->%3))) ==> {
  2217. (Termify((%3-->%1),truth(punc({("?","?"),("@","@")}),(),(),Task)),24)
  2218. }
  2219. }
  2220. 28 ==> {
  2221. unify(((%1-->%2),(%2-->%3))) ==> {
  2222. (Termify((%1-->%3),truth(punc({("?","?"),("@","@")}),(),(),Task)),28)
  2223. }
  2224. }
  2225. 39 ==> {
  2226. unify(((%1-->%2),(%2-->%3))) ==> {
  2227. (Termify((%1-->%3),truth(punc({("?","?"),("@","@")}),(),(),Task)),39)
  2228. }
  2229. }
  2230. }
  2231. }
  2232. and {
  2233. unifyIf(task((1)),neq,belief((0)))
  2234. unifyIf(task((1)),neqRCom,belief((0)))
  2235. forkable({13,18,25}) {
  2236. 25 ==> {
  2237. unify(((%1-->%2),(%3-->%1))) ==> {
  2238. (Termify((%2-->%3),truth(punc({("?","?"),("@","@")}),(),(),Task)),25)
  2239. }
  2240. }
  2241. 30 ==> {
  2242. unify(((%1-->%2),(%3-->%1))) ==> {
  2243. (Termify((%3-->%2),truth(punc({("?","?"),("@","@")}),(),(),Task)),30)
  2244. }
  2245. }
  2246. 37 ==> {
  2247. unify(((%1-->%2),(%3-->%1))) ==> {
  2248. (Termify((%3-->%2),truth(punc({("?","?"),("@","@")}),(),(),Task)),37)
  2249. }
  2250. }
  2251. }
  2252. }
  2253. and {
  2254. unifyIf(task((1)),neq,belief((1)))
  2255. unifyIf(task((1)),neqRCom,belief((1)))
  2256. forkable({4,17,26}) {
  2257. 16 ==> {
  2258. unify(((%1-->%2),(%1-->%3))) ==> {
  2259. (Termify((%3-->%2),truth(punc({("?","?"),("@","@")}),(),(),Task)),16)
  2260. }
  2261. }
  2262. 29 ==> {
  2263. unify(((%1-->%2),(%1-->%3))) ==> {
  2264. (Termify((%2-->%3),truth(punc({("?","?"),("@","@")}),(),(),Task)),29)
  2265. }
  2266. }
  2267. 38 ==> {
  2268. unify(((%1-->%2),(%1-->%3))) ==> {
  2269. (Termify((%2-->%3),truth(punc({("?","?"),("@","@")}),(),(),Task)),38)
  2270. }
  2271. }
  2272. }
  2273. }
  2274. and {
  2275. Is(taskTerm((1)),"?")
  2276. unifyIf(task((1)),neq,belief((1)))
  2277. forkable({32,33}) {
  2278. 44 ==> {
  2279. unify(((%1-->%2),(%1-->%3))) ==> {
  2280. (Termify((?4-->%3),truth(punc({("?","?"),("@","@")}),(),(),Task)),44)
  2281. }
  2282. }
  2283. 45 ==> {
  2284. unify(((%1-->%2),(%1-->%3))) ==> {
  2285. (Termify((%3-->?4),truth(punc({("?","?"),("@","@")}),(),(),Task)),45)
  2286. }
  2287. }
  2288. }
  2289. }
  2290. }
  2291. }
  2292. and {
  2293. Is(beliefTerm,"B")
  2294. Has(taskTerm((0)),(".",any,volMin(0)))
  2295. Has(taskTerm((1)),(".",any,volMin(0)))
  2296. forkable({46}) {
  2297. 58 ==> {
  2298. unify(((%1-->%2),true)) ==> {
  2299. (Termify(beliefTerm,truth(punc({("?","?"),("@","@")}),(),(),Task)),58)
  2300. }
  2301. }
  2302. }
  2303. }
  2304. }
  2305. }
  2306. and {
  2307. unifyIf(belief(()),Eventable,(()))
  2308. fork {
  2309. and {
  2310. IsHas(taskTerm,("-->",volMin(3)))
  2311. fork {
  2312. and {
  2313. Is(taskTerm((0)),"&&")
  2314. unifyIf(task((0)),VolumeCompare,belief(()))
  2315. unifyIf(task((0)),neq,belief(()))
  2316. unifyIf(task((0)),"Event->(+|-)",belief(()))
  2317. forkable({107}) {
  2318. 119 ==> {
  2319. unify(((%1-->%2),%3)) ==> {
  2320. (Termify((conjWithoutPN(%1,%3)-->%2),truth(punc({("?","?"),("@","@")}),(),(),Task)),119)
  2321. }
  2322. }
  2323. }
  2324. }
  2325. and {
  2326. Is(taskTerm((1)),"&&")
  2327. unifyIf(task((1)),VolumeCompare,belief(()))
  2328. unifyIf(task((1)),neq,belief(()))
  2329. unifyIf(task((1)),"Event->(+|-)",belief(()))
  2330. forkable({106}) {
  2331. 118 ==> {
  2332. unify(((%1-->%2),%3)) ==> {
  2333. (Termify((%1-->conjWithoutPN(%2,%3)),truth(punc({("?","?"),("@","@")}),(),(),Task)),118)
  2334. }
  2335. }
  2336. }
  2337. }
  2338. }
  2339. }
  2340. and {
  2341. Is(taskTerm,"&&")
  2342. unifyIf(task(()),VolumeCompare,belief(()))
  2343. unifyIf(task(()),neq,belief(()))
  2344. ConjParallel(taskTerm)
  2345. unifyIf(task(()),"Event->(+|-)",belief(()))
  2346. forkable({259}) {
  2347. 271 ==> {
  2348. unify((%1,%2)) ==> {
  2349. (Termify(conjWithoutPN(%1,%2),truth(punc({("?","?"),("@","@")}),(),(),Task)),271)
  2350. }
  2351. }
  2352. }
  2353. }
  2354. and {
  2355. IsHas(taskTerm,("<->",volMin(3)))
  2356. forkable({108}) {
  2357. 120 ==> {
  2358. and {
  2359. unifyIf(%3,{(neq,%1),(VolumeCompare,%1),("Event<-(+|-)",%1)})
  2360. unifyIf(%1,{(Is,("&&")),(neq,%3),(VolumeCompare,%3),("Event->(+|-)",%3)})
  2361. unify(((%1<->%2),%3)) ==> {
  2362. (Termify((conjWithoutPN(%1,%3)<->%2),truth(punc({("?","?"),("@","@")}),(),(),Task)),120)
  2363. }
  2364. }
  2365. }
  2366. }
  2367. }
  2368. }
  2369. }
  2370. and {
  2371. (--,Is(taskTerm,"==>"))
  2372. fork {
  2373. and {
  2374. IsHas(beliefTerm,("==>",volMin(3)))
  2375. fork {
  2376. and {
  2377. (--,Is(beliefTerm((0)),"--"))
  2378. unifyIf(belief((0)),Unifiability,(task(()),true,2048))
  2379. forkable({152}) {
  2380. 164 ==> {
  2381. unify((%1,(%2 ==>+- %3))) ==> {
  2382. (Termify(unisubst(beliefTerm,%2,%1,"$",novel),truth(punc({("?","?"),("@","@")}),(),(),TaskEvent)),164)
  2383. }
  2384. }
  2385. }
  2386. }
  2387. and {
  2388. unifyIf(belief((1)),Unifiability,(task(()),true,2048))
  2389. forkable({154}) {
  2390. 166 ==> {
  2391. unify((%1,(%2 ==>+- %3))) ==> {
  2392. (Termify(unisubst(beliefTerm,%3,%1,"$",novel),truth(punc({("?","?"),("@","@")}),(),(),TaskEvent)),166)
  2393. }
  2394. }
  2395. }
  2396. }
  2397. }
  2398. }
  2399. and {
  2400. IsHas(beliefTerm,("==>","--",volMin(4)))
  2401. IsHas(beliefTerm((0)),("--",volMin(2)))
  2402. (--,Is(beliefTerm((0,0)),"--"))
  2403. unifyIf(belief((0,0)),Unifiability,(task(()),true,2048))
  2404. forkable({153}) {
  2405. 165 ==> {
  2406. unify((%1,((--,%2) ==>+- %3))) ==> {
  2407. (Termify(unisubst(beliefTerm,%2,%1,"$",novel),truth(punc({("?","?"),("@","@")}),(),(),TaskEvent)),165)
  2408. }
  2409. }
  2410. }
  2411. }
  2412. }
  2413. }
  2414. and {
  2415. unifyIf(task(()),Eventable,(()))
  2416. Is(beliefTerm,"&&")
  2417. unifyIf(belief(()),VolumeCompare,task(()))
  2418. unifyIf(belief(()),neq,task(()))
  2419. ConjParallel(beliefTerm)
  2420. unifyIf(belief(()),"Event->(+|-)",task(()))
  2421. forkable({260}) {
  2422. 272 ==> {
  2423. unify((%1,%2)) ==> {
  2424. (Termify(conjWithoutPN(%2,%1),truth(punc({("?","?"),("@","@")}),(),(),Task)),272)
  2425. }
  2426. }
  2427. }
  2428. }
  2429. and {
  2430. IsHas(taskTerm,("==>",volMin(3)))
  2431. IsHas(beliefTerm,("==>",volMin(3)))
  2432. forkable({-60,-59,-56,-55}) {
  2433. 208 ==> {
  2434. unify(((%1 ==>+- %2),(%3 ==>+- %2))) ==> {
  2435. (Termify(((%1 &&+- %3) ==>+- %2),truth(punc({("?","?"),("@","@")}),(),(),Task)),208)
  2436. }
  2437. }
  2438. 209 ==> {
  2439. unify(((%1 ==>+- %2),(%3 ==>+- %2))) ==> {
  2440. (Termify(((%1 ||+- %3) ==>+- %2),truth(punc({("?","?"),("@","@")}),(),(),Task)),209)
  2441. }
  2442. }
  2443. 212 ==> {
  2444. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  2445. (Termify((%1 ==>+- (polarizeTask(%2) &&+- polarizeBelief(%3))),truth(punc({("?","?"),("@","@")}),(),(),Task)),212)
  2446. }
  2447. }
  2448. 213 ==> {
  2449. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  2450. (Termify((--,(%1 ==>+- ((--,polarizeTask(%2)) &&+- (--,polarizeBelief(%3))))),truth(punc({("?","?"),("@","@")}),(),(),Task)),213)
  2451. }
  2452. }
  2453. }
  2454. }
  2455. and {
  2456. IsHas(beliefTerm,("<->",volMin(3)))
  2457. forkable({59}) {
  2458. 71 ==> {
  2459. and {
  2460. unifyIf(%3,neq,%1)
  2461. unifyIf(%2,{(neq,%1),(VolumeCompare,%1),("Recursive<-(+)",%1)})
  2462. unifyIf(%1,{(neq,%2),(neq,%3),(VolumeCompare,%2),("Recursive->(+)",%2)})
  2463. unify((%1,(%2<->%3))) ==> {
  2464. (Termify(substitute(%1,%2,polarizeBelief(%3),novel),truth(punc({("?","?"),("@","@")}),(),(),Task)),71)
  2465. }
  2466. }
  2467. }
  2468. }
  2469. }
  2470. }
  2471. }
  2472. and {
  2473. punc(("!","!"))
  2474. fork {
  2475. and {
  2476. DoublePremise(("!"),punc)
  2477. fork {
  2478. and {
  2479. IsHas(taskTerm,("-->",volMin(3)))
  2480. fork {
  2481. and {
  2482. IsHas(beliefTerm,("-->",volMin(3)))
  2483. fork {
  2484. and {
  2485. Has(taskTerm((0)),(".",any,volMin(0)))
  2486. fork {
  2487. and {
  2488. unifyIf(task((0)),neq,belief((1)))
  2489. Has(beliefTerm((1)),(".",any,volMin(0)))
  2490. unifyIf(task((0)),neqRCom,belief((1)))
  2491. forkable({3,10}) {
  2492. 15 ==> {
  2493. unify(((%1-->%2),(%2-->%3))) ==> {
  2494. (Termify((%1-->%3),truth(punc(("!","!")),(),Desire,Task)),15)
  2495. }
  2496. }
  2497. 22 ==> {
  2498. unify(((%1-->%2),(%2-->%3))) ==> {
  2499. (Termify((%3-->%1),truth(punc(("!","!")),(),DesireWeak,Task)),22)
  2500. }
  2501. }
  2502. }
  2503. }
  2504. and {
  2505. Has(taskTerm((1)),(".",any,volMin(0)))
  2506. forkable({49}) {
  2507. 61 ==> {
  2508. unify(((%1-->%2),(%2-->%1))) ==> {
  2509. (Termify((%1<->%2),truth(punc(("!","!")),(),DesireWeak,Task)),61)
  2510. }
  2511. }
  2512. }
  2513. }
  2514. }
  2515. }
  2516. and {
  2517. unifyIf(task((1)),neq,belief((0)))
  2518. Has(beliefTerm((0)),(".",any,volMin(0)))
  2519. Has(taskTerm((1)),(".",any,volMin(0)))
  2520. unifyIf(task((1)),neqRCom,belief((0)))
  2521. forkable({2,11}) {
  2522. 14 ==> {
  2523. unify(((%1-->%2),(%3-->%1))) ==> {
  2524. (Termify((%3-->%2),truth(punc(("!","!")),(),Desire,Task)),14)
  2525. }
  2526. }
  2527. 23 ==> {
  2528. unify(((%1-->%2),(%3-->%1))) ==> {
  2529. (Termify((%2-->%3),truth(punc(("!","!")),(),DesireWeak,Task)),23)
  2530. }
  2531. }
  2532. }
  2533. }
  2534. }
  2535. }
  2536. and {
  2537. IsHas(beliefTerm,("<->",volMin(3)))
  2538. fork {
  2539. and {
  2540. Has(taskTerm((0)),(".",any,volMin(0)))
  2541. forkable({41}) {
  2542. 53 ==> {
  2543. and {
  2544. unifyIf(%1,{(neq,%3),(neqRCom,%3)})
  2545. unifyIf(%3,{(Has,((".",any,volMin(0)))),(neq,%1),(neqRCom,%1)})
  2546. unify(((%1-->%2),(%2<->%3))) ==> {
  2547. (Termify((%1-->%3),truth(punc(("!","!")),(),DesireWeak,Task)),53)
  2548. }
  2549. }
  2550. }
  2551. }
  2552. }
  2553. and {
  2554. Has(taskTerm((1)),(".",any,volMin(0)))
  2555. forkable({37}) {
  2556. 49 ==> {
  2557. and {
  2558. unifyIf(%2,{(neq,%3),(neqRCom,%3)})
  2559. unifyIf(%3,{(Has,((".",any,volMin(0)))),(neq,%2),(neqRCom,%2)})
  2560. unify(((%1-->%2),(%1<->%3))) ==> {
  2561. (Termify((%3-->%2),truth(punc(("!","!")),(),DesireWeak,Task)),49)
  2562. }
  2563. }
  2564. }
  2565. }
  2566. }
  2567. }
  2568. }
  2569. }
  2570. }
  2571. and {
  2572. unifyIf(task(()),Eventable,(()))
  2573. Is(beliefTerm,"&&")
  2574. unifyIf(belief(()),VolumeCompare,(task(()),onlyIfConstants))
  2575. unifyIf(belief(()),neq,task(()))
  2576. fork {
  2577. and {
  2578. (--,ConjParallel(beliefTerm))
  2579. fork {
  2580. and {
  2581. Has(beliefTerm,("--",any,volMin(0)))
  2582. unifyIf(belief(()),EventUnifiability,(task(()),true,true))
  2583. (--,unifyIf(belief(()),"Event->(+)",task(())))
  2584. forkable({246}) {
  2585. 258 ==> {
  2586. unify((%1,%2)) ==> {
  2587. (Termify(conjAfter(%2,(--,%1)),truth(punc(("!","!")),(),DeductionWeakNP,TaskEvent)),258)
  2588. }
  2589. }
  2590. }
  2591. }
  2592. and {
  2593. unifyIf(belief(()),EventUnifiability,(task(()),false,true))
  2594. (--,unifyIf(belief(()),"Event->(-)",task(())))
  2595. forkable({245}) {
  2596. 257 ==> {
  2597. unify((%1,%2)) ==> {
  2598. (Termify(conjAfter(%2,%1),truth(punc(("!","!")),(),DeductionWeak,TaskEvent)),257)
  2599. }
  2600. }
  2601. }
  2602. }
  2603. }
  2604. }
  2605. and {
  2606. Has(beliefTerm,("--",any,volMin(0)))
  2607. unifyIf(belief(()),EventUnifiability,(task(()),true,true))
  2608. forkable({244}) {
  2609. 256 ==> {
  2610. unify((%1,%2)) ==> {
  2611. (Termify(conjBefore(%2,(--,%1)),truth(punc(("!","!")),(),DeductionNP,TaskEvent)),256)
  2612. }
  2613. }
  2614. }
  2615. }
  2616. and {
  2617. unifyIf(belief(()),EventUnifiability,(task(()),false,true))
  2618. forkable({243}) {
  2619. 255 ==> {
  2620. unify((%1,%2)) ==> {
  2621. (Termify(conjBefore(%2,%1),truth(punc(("!","!")),(),Deduction,TaskEvent)),255)
  2622. }
  2623. }
  2624. }
  2625. }
  2626. }
  2627. }
  2628. and {
  2629. (--,Is(taskTerm,"==>"))
  2630. fork {
  2631. and {
  2632. IsHas(beliefTerm,("==>",volMin(3)))
  2633. fork {
  2634. and {
  2635. (--,Is(beliefTerm((0)),"--"))
  2636. (--,Is(beliefTerm((1)),"1111000000000"))
  2637. unifyIf(belief((0)),Unifiability,(task(()),false,2048))
  2638. forkable({-108,-106}) {
  2639. 160 ==> {
  2640. unify((%1,(%2 ==>+- %3))) ==> {
  2641. (Termify(unisubst(%3,%2,%1,"$"),truth(punc(("!","!")),(),DeductionWeak,TaskEvent)),160)
  2642. }
  2643. }
  2644. 162 ==> {
  2645. unify((%1,(%2 ==>+- %3))) ==> {
  2646. (Termify((--,unisubst(%3,%2,%1,"$")),truth(punc(("!","!")),(),DeductionWeakPN,TaskEvent)),162)
  2647. }
  2648. }
  2649. }
  2650. }
  2651. and {
  2652. (--,Is(beliefTerm((0)),"1111000000000"))
  2653. unifyIf(belief((1)),Unifiability,(task(()),false,2048))
  2654. forkable({-118,-117}) {
  2655. 150 ==> {
  2656. unify((%1,(%2 ==>+- %3))) ==> {
  2657. (Termify(unisubst(%2,%3,%1,"$"),truth(punc(("!","!")),(),Deduction,TaskEvent)),150)
  2658. }
  2659. }
  2660. 151 ==> {
  2661. unify((%1,(%2 ==>+- %3))) ==> {
  2662. (Termify(unisubst(%2,%3,%1,"$"),truth(punc(("!","!")),(),DeductionNN,TaskEvent)),151)
  2663. }
  2664. }
  2665. }
  2666. }
  2667. }
  2668. }
  2669. and {
  2670. IsHas(beliefTerm,("==>","--",volMin(4)))
  2671. IsHas(beliefTerm((0)),("--",volMin(2)))
  2672. (--,Is(beliefTerm((1)),"1111000000000"))
  2673. (--,Is(beliefTerm((0,0)),"--"))
  2674. unifyIf(belief((0,0)),Unifiability,(task(()),false,2048))
  2675. forkable({-107,-105}) {
  2676. 161 ==> {
  2677. unify((%1,((--,%2) ==>+- %3))) ==> {
  2678. (Termify(unisubst(%3,%2,%1,"$"),truth(punc(("!","!")),(),DeductionWeakNP,TaskEvent)),161)
  2679. }
  2680. }
  2681. 163 ==> {
  2682. unify((%1,((--,%2) ==>+- %3))) ==> {
  2683. (Termify((--,unisubst(%3,%2,%1,"$")),truth(punc(("!","!")),(),DeductionWeakNN,TaskEvent)),163)
  2684. }
  2685. }
  2686. }
  2687. }
  2688. }
  2689. }
  2690. and {
  2691. IsHas(taskTerm,("<->",volMin(3)))
  2692. IsHas(beliefTerm,("-->",volMin(3)))
  2693. fork {
  2694. and {
  2695. Has(beliefTerm((0)),(".",any,volMin(0)))
  2696. forkable({39}) {
  2697. 51 ==> {
  2698. and {
  2699. unifyIf(%3,{(neq,%2),(neqRCom,%2)})
  2700. unifyIf(%2,{(Has,((".",any,volMin(0)))),(neq,%3),(neqRCom,%3)})
  2701. unify(((%1<->%2),(%3-->%1))) ==> {
  2702. (Termify((%3-->%2),truth(punc(("!","!")),(),DesireWeak,Task)),51)
  2703. }
  2704. }
  2705. }
  2706. }
  2707. }
  2708. and {
  2709. Has(beliefTerm((1)),(".",any,volMin(0)))
  2710. forkable({43}) {
  2711. 55 ==> {
  2712. and {
  2713. unifyIf(%3,{(neq,%2),(neqRCom,%2)})
  2714. unifyIf(%2,{(Has,((".",any,volMin(0)))),(neq,%3),(neqRCom,%3)})
  2715. unify(((%1<->%2),(%1-->%3))) ==> {
  2716. (Termify((%2-->%3),truth(punc(("!","!")),(),DesireWeak,Task)),55)
  2717. }
  2718. }
  2719. }
  2720. }
  2721. }
  2722. }
  2723. }
  2724. and {
  2725. Is(taskTerm,"&&")
  2726. fork {
  2727. and {
  2728. Has(taskTerm,("--",any,volMin(0)))
  2729. forkable({242}) {
  2730. 254 ==> {
  2731. unify((%1,%2)) ==> {
  2732. (Termify(conjWithoutUnify(%1,(--,%2)),truth(punc(("!","!")),(),DesirePN,BeliefEvent)),254)
  2733. }
  2734. }
  2735. }
  2736. }
  2737. forkable({241}) {
  2738. 253 ==> {
  2739. unify((%1,%2)) ==> {
  2740. (Termify(conjWithoutUnify(%1,%2),truth(punc(("!","!")),(),Desire,BeliefEvent)),253)
  2741. }
  2742. }
  2743. }
  2744. }
  2745. }
  2746. }
  2747. }
  2748. and {
  2749. IsHas(taskTerm,("<->",volMin(3)))
  2750. forkable({47}) {
  2751. 59 ==> {
  2752. unify(((%1<->%2),%1)) ==> {
  2753. (Termify((%2-->%1),truth(punc(("!","!")),(),StructuralReduction,Task)),59)
  2754. }
  2755. }
  2756. }
  2757. }
  2758. }
  2759. }
  2760. and {
  2761. punc({("!","!"),(".",".")})
  2762. fork {
  2763. and {
  2764. unifyIf(belief(()),Eventable,(()))
  2765. fork {
  2766. and {
  2767. IsHas(taskTerm,("-->",volMin(3)))
  2768. fork {
  2769. and {
  2770. Is(taskTerm((0)),"&&")
  2771. unifyIf(task((0)),VolumeCompare,belief(()))
  2772. unifyIf(task((0)),neq,belief(()))
  2773. unifyIf(task((0)),"Event->(+|-)",belief(()))
  2774. forkable({102,103}) {
  2775. 114 ==> {
  2776. unify(((%1-->%2),%3)) ==> {
  2777. (Termify((conjWithoutPN(%1,%3)-->%2),truth(punc({("!","!"),(".",".")}),StructuralDeduction,StructuralDeduction,Task)),114)
  2778. }
  2779. }
  2780. 115 ==> {
  2781. unify(((%1-->%2),%3)) ==> {
  2782. (Termify((--,(conjWithoutPN(%1,%3)-->%2)),truth(punc({("!","!"),(".",".")}),StructuralDeductionN,StructuralDeductionN,Task)),115)
  2783. }
  2784. }
  2785. }
  2786. }
  2787. and {
  2788. Is(taskTerm((1)),"&&")
  2789. unifyIf(task((1)),VolumeCompare,belief(()))
  2790. unifyIf(task((1)),neq,belief(()))
  2791. unifyIf(task((1)),"Event->(+|-)",belief(()))
  2792. forkable({100,101}) {
  2793. 112 ==> {
  2794. unify(((%1-->%2),%3)) ==> {
  2795. (Termify((%1-->conjWithoutPN(%2,%3)),truth(punc({("!","!"),(".",".")}),StructuralDeduction,StructuralDeduction,Task)),112)
  2796. }
  2797. }
  2798. 113 ==> {
  2799. unify(((%1-->%2),%3)) ==> {
  2800. (Termify((--,(%1-->conjWithoutPN(%2,%3))),truth(punc({("!","!"),(".",".")}),StructuralDeductionN,StructuralDeductionN,Task)),113)
  2801. }
  2802. }
  2803. }
  2804. }
  2805. }
  2806. }
  2807. and {
  2808. Is(taskTerm,"&&")
  2809. unifyIf(task(()),VolumeCompare,belief(()))
  2810. unifyIf(task(()),neq,belief(()))
  2811. ConjParallel(taskTerm)
  2812. unifyIf(task(()),"Event->(+|-)",belief(()))
  2813. forkable({258}) {
  2814. 270 ==> {
  2815. unify((%1,%2)) ==> {
  2816. (Termify(conjWithoutPN(%1,%2),truth(punc({("!","!"),(".",".")}),StructuralDeduction,StructuralDeduction,Task)),270)
  2817. }
  2818. }
  2819. }
  2820. }
  2821. }
  2822. }
  2823. and {
  2824. IsHas(taskTerm,("-->",volMin(3)))
  2825. fork {
  2826. and {
  2827. {Is(taskTerm((0)),"11000000"),SubsMin(taskTerm((0)),2)}
  2828. unifyIf(task((0)),VolumeCompare,belief(()))
  2829. unifyIf(task((0)),neq,belief(()))
  2830. unifyIf(task((0)),"Subterm->(+|-)",belief(()))
  2831. forkable({82}) {
  2832. 94 ==> {
  2833. unify(((%1-->%2),%3)) ==> {
  2834. (Termify((withoutPN(%1,%3)-->%2),truth(punc({("!","!"),(".",".")}),StructuralDeduction,StructuralDeduction,Task)),94)
  2835. }
  2836. }
  2837. }
  2838. }
  2839. and {
  2840. {Is(taskTerm((1)),"11000000"),SubsMin(taskTerm((1)),2)}
  2841. unifyIf(task((1)),VolumeCompare,belief(()))
  2842. unifyIf(task((1)),neq,belief(()))
  2843. unifyIf(task((1)),"Subterm->(+|-)",belief(()))
  2844. forkable({81}) {
  2845. 93 ==> {
  2846. unify(((%1-->%2),%3)) ==> {
  2847. (Termify((%1-->withoutPN(%2,%3)),truth(punc({("!","!"),(".",".")}),StructuralDeduction,StructuralDeduction,Task)),93)
  2848. }
  2849. }
  2850. }
  2851. }
  2852. }
  2853. }
  2854. and {
  2855. IsHas(taskTerm,("-->","[",volMin(4)))
  2856. IsHas(beliefTerm,("[",volMin(2)))
  2857. IsHas(taskTerm((1)),("[",volMin(2)))
  2858. ellipsisCommutativeConstant((1),(0),task)
  2859. forkable({68}) {
  2860. 80 ==> {
  2861. unify(((%1-->[%2]),[%2])) ==> {
  2862. (Termify(polarizeTask((%1-->%2)),truth(punc({("!","!"),(".",".")}),StructuralReduction,StructuralReduction,Task)),80)
  2863. }
  2864. }
  2865. }
  2866. }
  2867. and {
  2868. IsHas(taskTerm,("-->","{",volMin(4)))
  2869. IsHas(beliefTerm,("{",volMin(2)))
  2870. IsHas(taskTerm((0)),("{",volMin(2)))
  2871. ellipsisCommutativeConstant((0),(0),task)
  2872. forkable({67}) {
  2873. 79 ==> {
  2874. unify((({%1}-->%2),{%1})) ==> {
  2875. (Termify(polarizeTask((%1-->%2)),truth(punc({("!","!"),(".",".")}),StructuralReduction,StructuralReduction,Task)),79)
  2876. }
  2877. }
  2878. }
  2879. }
  2880. and {
  2881. IsHas(beliefTerm,("<->",volMin(3)))
  2882. fork {
  2883. and {
  2884. IsHas(taskTerm,("&&","<->",volMin(5)))
  2885. forkable({62}) {
  2886. 74 ==> {
  2887. unify((((%1<->%2) &&+- %3..+),(%1<->%2))) ==> {
  2888. (Termify(substitute(( &&+- ,%3..+),%1,%2,novel),truth(punc({("!","!"),(".",".")}),StructuralReduction,StructuralReduction,TaskEvent)),74)
  2889. }
  2890. }
  2891. }
  2892. }
  2893. and {
  2894. DoublePremise(({"!","."}),punc)
  2895. forkable({55,56}) {
  2896. 67 ==> {
  2897. and {
  2898. unifyIf(%2,Is,(--,("1111000000000")))
  2899. unify((%1,(%1<->%2))) ==> {
  2900. (Termify(%2,truth(punc({("!","!"),(".",".")}),Desire,Desire,Task)),67)
  2901. }
  2902. }
  2903. }
  2904. 68 ==> {
  2905. and {
  2906. unifyIf(%2,Is,(--,("1111000000000")))
  2907. unify((%1,(%1<->%2))) ==> {
  2908. (Termify((--,%2),truth(punc({("!","!"),(".",".")}),DesirePN,DesirePN,Task)),68)
  2909. }
  2910. }
  2911. }
  2912. }
  2913. }
  2914. }
  2915. }
  2916. and {
  2917. IsHas(taskTerm,("-->","10000100",volMin(7)))
  2918. IsHas(taskTerm((0)),("{","-->",volMin(5)))
  2919. forkable({87}) {
  2920. 99 ==> {
  2921. unify((({(%1-->%2),%3..*}-->%4),%4)) ==> {
  2922. (Termify(({%1}-->(%4,%2)),truth(punc({("!","!"),(".",".")}),StructuralDeduction,StructuralDeduction,Task)),99)
  2923. }
  2924. }
  2925. }
  2926. }
  2927. and {
  2928. IsHas(taskTerm,("<->","[",volMin(5)))
  2929. IsHas(beliefTerm,("<->","{",volMin(5)))
  2930. forkable({64}) {
  2931. 76 ==> {
  2932. unify((([%1]<->[%2]),({%1}<->{%2}))) ==> {
  2933. (Termify((%1<->%2),truth(punc({("!","!"),(".",".")}),Identity,Identity,Task)),76)
  2934. }
  2935. }
  2936. }
  2937. }
  2938. and {
  2939. IsHas(taskTerm,("<->","[",volMin(4)))
  2940. forkable({66}) {
  2941. 78 ==> {
  2942. unify((([%1]<->%2),%2)) ==> {
  2943. (Termify(([%1]-->%2),truth(punc({("!","!"),(".",".")}),Identity,Identity,Task)),78)
  2944. }
  2945. }
  2946. }
  2947. }
  2948. and {
  2949. IsHas(taskTerm,("<->","{",volMin(4)))
  2950. forkable({65}) {
  2951. 77 ==> {
  2952. unify((({%1}<->%2),%2)) ==> {
  2953. (Termify((%2-->{%1}),truth(punc({("!","!"),(".",".")}),Identity,Identity,Task)),77)
  2954. }
  2955. }
  2956. }
  2957. }
  2958. }
  2959. }
  2960. and {
  2961. TaskBeliefTermsEqual
  2962. fork {
  2963. and {
  2964. punc((".","."))
  2965. fork {
  2966. and {
  2967. IsHas(taskTerm,("-->",volMin(3)))
  2968. IsHas(beliefTerm,("-->",volMin(3)))
  2969. unifyIf(task((0)),Eventable,(()))
  2970. unifyIf(task((1)),Eventable,(()))
  2971. Is(taskTerm((0)),"&&")
  2972. Is(taskTerm((1)),"&&")
  2973. unifyIf(task((0)),neq,task((1)))
  2974. unifyIf(task((1)),neq,task((0)))
  2975. unifyIf(task((0)),eventCommon,task((1)))
  2976. forkable({104}) {
  2977. 116 ==> {
  2978. unify(((%1-->%2),(%1-->%2))) ==> {
  2979. (Termify(polarizeTask((conjWithout(%1,%2)-->conjWithout(%2,%1))),truth(punc((".",".")),StructuralReduction,(),Task)),116)
  2980. }
  2981. }
  2982. }
  2983. }
  2984. and {
  2985. IsHas(taskTerm,("<->",volMin(3)))
  2986. IsHas(beliefTerm,("<->",volMin(3)))
  2987. forkable({105}) {
  2988. 117 ==> {
  2989. and {
  2990. unifyIf(%2,{(Is,("&&")),(Eventable,(())),(neq,%1),(eventCommon,%1)})
  2991. unifyIf(%1,{(Is,("&&")),(Eventable,(())),(neq,%2),(eventCommon,%2)})
  2992. unify(((%1<->%2),(%1<->%2))) ==> {
  2993. (Termify(polarizeTask((conjWithout(%1,%2)<->conjWithout(%2,%1))),truth(punc((".",".")),StructuralReduction,(),Task)),117)
  2994. }
  2995. }
  2996. }
  2997. }
  2998. }
  2999. }
  3000. }
  3001. and {
  3002. punc({("!","@"),(".","?")})
  3003. fork {
  3004. and {
  3005. IsHas(taskTerm,("&&","110",volMin(8)))
  3006. IsHas(beliefTerm,("&&","110",volMin(8)))
  3007. forkable({291,292,295,296}) {
  3008. 303 ==> {
  3009. and {
  3010. unifyIf(%3,{(neq,%1),(neqRCom,%1)})
  3011. unifyIf(%1,{(neq,%3),(neqRCom,%3)})
  3012. unify((((--,(%1-->%2)) &&+- (%3-->%2)),((--,(%1-->%2)) &&+- (%3-->%2)))) ==> {
  3013. (Termify((((--,%1)&&%3)-->%2),truth(punc({("!","@"),(".","?")}),(),(),Task)),303)
  3014. }
  3015. }
  3016. }
  3017. 304 ==> {
  3018. and {
  3019. unifyIf(%3,{(neq,%1),(neqRCom,%1)})
  3020. unifyIf(%1,{(neq,%3),(neqRCom,%3)})
  3021. unify((((--,(%1-->%2)) &&+- (%3-->%2)),((--,(%1-->%2)) &&+- (%3-->%2)))) ==> {
  3022. (Termify((((--,%1)&&%3)-->%2),truth(punc({("!","@"),(".","?")}),(),(),Task)),304)
  3023. }
  3024. }
  3025. }
  3026. 307 ==> {
  3027. and {
  3028. unifyIf(%3,{(neq,%2),(neqRCom,%2)})
  3029. unifyIf(%2,{(neq,%3),(neqRCom,%3)})
  3030. unify((((--,(%1-->%2)) &&+- (%1-->%3)),((--,(%1-->%2)) &&+- (%1-->%3)))) ==> {
  3031. (Termify((%1-->((--,%2)&&%3)),truth(punc({("!","@"),(".","?")}),(),(),Task)),307)
  3032. }
  3033. }
  3034. }
  3035. 308 ==> {
  3036. and {
  3037. unifyIf(%3,{(neq,%2),(neqRCom,%2)})
  3038. unifyIf(%2,{(neq,%3),(neqRCom,%3)})
  3039. unify((((--,(%1-->%2)) &&+- (%1-->%3)),((--,(%1-->%2)) &&+- (%1-->%3)))) ==> {
  3040. (Termify((%1-->((--,%2)&&%3)),truth(punc({("!","@"),(".","?")}),(),(),Task)),308)
  3041. }
  3042. }
  3043. }
  3044. }
  3045. }
  3046. and {
  3047. IsHas(taskTerm,("&&","-->",volMin(7)))
  3048. IsHas(beliefTerm,("&&","-->",volMin(7)))
  3049. forkable({290,294}) {
  3050. 302 ==> {
  3051. and {
  3052. unifyIf(%3,{(neq,%1),(neqRCom,%1)})
  3053. unifyIf(%1,{(neq,%3),(neqRCom,%3)})
  3054. unify((((%1-->%2) &&+- (%3-->%2)),((%1-->%2) &&+- (%3-->%2)))) ==> {
  3055. (Termify(((%1&&%3)-->%2),truth(punc({("!","@"),(".","?")}),(),(),Task)),302)
  3056. }
  3057. }
  3058. }
  3059. 306 ==> {
  3060. and {
  3061. unifyIf(%3,{(neq,%2),(neqRCom,%2)})
  3062. unifyIf(%2,{(neq,%3),(neqRCom,%3)})
  3063. unify((((%1-->%2) &&+- (%1-->%3)),((%1-->%2) &&+- (%1-->%3)))) ==> {
  3064. (Termify((%1-->(%2&&%3)),truth(punc({("!","@"),(".","?")}),(),(),Task)),306)
  3065. }
  3066. }
  3067. }
  3068. }
  3069. }
  3070. and {
  3071. IsHas(taskTerm,("&&","110",volMin(9)))
  3072. IsHas(beliefTerm,("&&","110",volMin(9)))
  3073. forkable({293,297}) {
  3074. 305 ==> {
  3075. and {
  3076. unifyIf(%3,{(neq,%1),(neqRCom,%1)})
  3077. unifyIf(%1,{(neq,%3),(neqRCom,%3)})
  3078. unify((((--,(%1-->%2)) &&+- (--,(%3-->%2))),((--,(%1-->%2)) &&+- (--,(%3-->%2))))) ==> {
  3079. (Termify((((--,%1)&&(--,%3))-->%2),truth(punc({("!","@"),(".","?")}),(),(),Task)),305)
  3080. }
  3081. }
  3082. }
  3083. 309 ==> {
  3084. and {
  3085. unifyIf(%3,{(neq,%2),(neqRCom,%2)})
  3086. unifyIf(%2,{(neq,%3),(neqRCom,%3)})
  3087. unify((((--,(%1-->%2)) &&+- (--,(%1-->%3))),((--,(%1-->%2)) &&+- (--,(%1-->%3))))) ==> {
  3088. (Termify((%1-->((--,%2)&&(--,%3))),truth(punc({("!","@"),(".","?")}),(),(),Task)),309)
  3089. }
  3090. }
  3091. }
  3092. }
  3093. }
  3094. }
  3095. }
  3096. and {
  3097. punc({("!","!"),(".",".")})
  3098. fork {
  3099. and {
  3100. IsHas(taskTerm,("<->","-->",volMin(7)))
  3101. IsHas(beliefTerm,("<->","-->",volMin(7)))
  3102. forkable({53,54}) {
  3103. 65 ==> {
  3104. and {
  3105. unifyIf(%3,{(Has,((".",any,volMin(0)))),(neq,%2),(neqRCom,%2)})
  3106. unifyIf(%2,{(Has,((".",any,volMin(0)))),(neq,%3),(neqRCom,%3)})
  3107. unify((((%1-->%2)<->(%1-->%3)),((%1-->%2)<->(%1-->%3)))) ==> {
  3108. (Termify((%2<->%3),truth(punc({("!","!"),(".",".")}),StructuralReductionWeak,StructuralReductionWeak,Task)),65)
  3109. }
  3110. }
  3111. }
  3112. 66 ==> {
  3113. and {
  3114. unifyIf(%3,{(Has,((".",any,volMin(0)))),(neq,%1),(neqRCom,%1)})
  3115. unifyIf(%1,{(Has,((".",any,volMin(0)))),(neq,%3),(neqRCom,%3)})
  3116. unify((((%1-->%2)<->(%3-->%2)),((%1-->%2)<->(%3-->%2)))) ==> {
  3117. (Termify((%1<->%3),truth(punc({("!","!"),(".",".")}),StructuralReductionWeak,StructuralReductionWeak,Task)),66)
  3118. }
  3119. }
  3120. }
  3121. }
  3122. }
  3123. and {
  3124. IsHas(taskTerm,("<->","{",volMin(5)))
  3125. IsHas(beliefTerm,("<->","{",volMin(5)))
  3126. forkable({63}) {
  3127. 75 ==> {
  3128. unify((({%1}<->{%2}),({%1}<->{%2}))) ==> {
  3129. (Termify((%1<->%2),truth(punc({("!","!"),(".",".")}),Identity,Identity,Task)),75)
  3130. }
  3131. }
  3132. }
  3133. }
  3134. }
  3135. }
  3136. and {
  3137. SinglePremise()
  3138. fork {
  3139. and {
  3140. punc({"!",".","?","@"})
  3141. fork {
  3142. and {
  3143. (--,Is(taskTerm,"==>"))
  3144. forkable({305}) {
  3145. 317 ==> {
  3146. ("nars.op.Factorize$FactorIntroduction","wx1my9")
  3147. }
  3148. }
  3149. }
  3150. forkable({303,304,306}) {
  3151. 315 ==> {
  3152. ("nars.op.stm.STMLinker","brhuh1")
  3153. }
  3154. 316 ==> {
  3155. ("nars.op.Arithmeticize$ArithmeticIntroduction","9kzkx1")
  3156. }
  3157. 318 ==> {
  3158. ("nars.op.mental.Inperience","6qelsh")
  3159. }
  3160. }
  3161. }
  3162. }
  3163. and {
  3164. punc("!")
  3165. forkable({308}) {
  3166. 320 ==> {
  3167. ("nars.op.stm.ConjClustering","mq0hwz")
  3168. }
  3169. }
  3170. }
  3171. and {
  3172. punc(".")
  3173. forkable({307}) {
  3174. 319 ==> {
  3175. ("nars.op.stm.ConjClustering","5352a9")
  3176. }
  3177. }
  3178. }
  3179. }
  3180. }
  3181. and {
  3182. punc(("!","@"))
  3183. IsHas(taskTerm,("-->",volMin(3)))
  3184. IsHas(beliefTerm,("-->",volMin(3)))
  3185. forkable({117,118}) {
  3186. 129 ==> {
  3187. unify(((%1-->%2),(%1-->%2))) ==> {
  3188. (Termify(((polarizeTask(%1)&&?3)-->%2),truth(punc(("!","@")),(),(),Task)),129)
  3189. }
  3190. }
  3191. 130 ==> {
  3192. unify(((%1-->%2),(%1-->%2))) ==> {
  3193. (Termify((%1-->(polarizeTask(%2)&&?3)),truth(punc(("!","@")),(),(),Task)),130)
  3194. }
  3195. }
  3196. }
  3197. }
  3198. and {
  3199. punc(("!","?"))
  3200. forkable({302}) {
  3201. 314 ==> {
  3202. unify((%1,%1)) ==> {
  3203. (Termify((?2 ==>+- %1),truth(punc(("!","?")),(),(),Task)),314)
  3204. }
  3205. }
  3206. }
  3207. }
  3208. }
  3209. }
  3210. and {
  3211. punc(("?","?"))
  3212. fork {
  3213. and {
  3214. IsHas(taskTerm,("==>",volMin(3)))
  3215. fork {
  3216. and {
  3217. unifyIf(belief(()),Eventable,(()))
  3218. (--,Is(beliefTerm,"1111000000000"))
  3219. fork {
  3220. and {
  3221. Is(taskTerm((0)),"&&")
  3222. unifyIf(task((0)),VolumeCompare,belief(()))
  3223. unifyIf(task((0)),neq,belief(()))
  3224. unifyIf(task((0)),"Event->(+|-)",belief(()))
  3225. forkable({268}) {
  3226. 280 ==> {
  3227. unify(((%1 ==>+- %2),%3)) ==> {
  3228. (Termify((conjWithoutPN(%1,%3) ==>+- %2),truth(punc(("?","?")),(),(),Task)),280)
  3229. }
  3230. }
  3231. }
  3232. }
  3233. and {
  3234. Is(taskTerm((1)),"&&")
  3235. unifyIf(task((1)),VolumeCompare,belief(()))
  3236. unifyIf(task((1)),neq,belief(()))
  3237. unifyIf(task((1)),"Event->(+|-)",belief(()))
  3238. forkable({263}) {
  3239. 275 ==> {
  3240. unify(((%1 ==>+- %2),%3)) ==> {
  3241. (Termify((%1 ==>+- conjWithoutPN(%2,%3)),truth(punc(("?","?")),(),(),Task)),275)
  3242. }
  3243. }
  3244. }
  3245. }
  3246. }
  3247. }
  3248. and {
  3249. IsHas(beliefTerm,("==>","--",volMin(4)))
  3250. IsHas(beliefTerm((0)),("--",volMin(2)))
  3251. forkable({-86,-74}) {
  3252. 182 ==> {
  3253. unify(((%1 ==>+- %2),((--,%3) ==>+- %2))) ==> {
  3254. (Termify((%1 ==>+- %3),truth(punc(("?","?")),(),(),Compose)),182)
  3255. }
  3256. }
  3257. 194 ==> {
  3258. unify(((%1 ==>+- %2),((--,%3) ==>+- %1))) ==> {
  3259. (Termify((%2 ==>+- %3),truth(punc(("?","?")),(),(),Compose)),194)
  3260. }
  3261. }
  3262. }
  3263. }
  3264. and {
  3265. IsHas(beliefTerm,("==>",volMin(3)))
  3266. forkable({-92,-91,-85,-80,-79,-73,-68,-67,-62,-61}) {
  3267. 176 ==> {
  3268. unify(((%1 ==>+- %2),(%3 ==>+- %2))) ==> {
  3269. (Termify((%1 ==>+- %3),truth(punc(("?","?")),(),(),Compose)),176)
  3270. }
  3271. }
  3272. 177 ==> {
  3273. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  3274. (Termify((%3 ==>+- %2),truth(punc(("?","?")),(),(),Compose)),177)
  3275. }
  3276. }
  3277. 183 ==> {
  3278. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  3279. (Termify(((--,%3) ==>+- %2),truth(punc(("?","?")),(),(),Compose)),183)
  3280. }
  3281. }
  3282. 188 ==> {
  3283. unify(((%1 ==>+- %2),(%3 ==>+- %1))) ==> {
  3284. (Termify((%2 ==>+- %3),truth(punc(("?","?")),(),(),Compose)),188)
  3285. }
  3286. }
  3287. 189 ==> {
  3288. unify(((%1 ==>+- %2),(%2 ==>+- %3))) ==> {
  3289. (Termify((%3 ==>+- %1),truth(punc(("?","?")),(),(),Compose)),189)
  3290. }
  3291. }
  3292. 195 ==> {
  3293. unify(((%1 ==>+- %2),(%2 ==>+- %3))) ==> {
  3294. (Termify(((--,%3) ==>+- %1),truth(punc(("?","?")),(),(),Compose)),195)
  3295. }
  3296. }
  3297. 200 ==> {
  3298. unify(((%1 ==>+- %2),(%3 ==>+- %2))) ==> {
  3299. (Termify((%3 ==>+- %1),truth(punc(("?","?")),(),(),Compose)),200)
  3300. }
  3301. }
  3302. 201 ==> {
  3303. unify(((%1 ==>+- %2),(%3 ==>+- %1))) ==> {
  3304. (Termify((%3 ==>+- %2),truth(punc(("?","?")),(),(),Compose)),201)
  3305. }
  3306. }
  3307. 206 ==> {
  3308. unify(((%1 ==>+- %2),(%2 ==>+- %3))) ==> {
  3309. (Termify((%1 ==>+- %3),truth(punc(("?","?")),(),(),Compose)),206)
  3310. }
  3311. }
  3312. 207 ==> {
  3313. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  3314. (Termify((%2 ==>+- %3),truth(punc(("?","?")),(),(),Compose)),207)
  3315. }
  3316. }
  3317. }
  3318. }
  3319. }
  3320. }
  3321. and {
  3322. IsHas(taskTerm,("==>","--",volMin(4)))
  3323. IsHas(taskTerm((0)),("--",volMin(2)))
  3324. fork {
  3325. and {
  3326. unifyIf(belief(()),Eventable,(()))
  3327. (--,Is(beliefTerm,"1111000000000"))
  3328. Is(taskTerm((0,0)),"&&")
  3329. unifyIf(task((0,0)),VolumeCompare,belief(()))
  3330. unifyIf(task((0,0)),neq,belief(()))
  3331. unifyIf(task((0,0)),"Event->(+|-)",belief(()))
  3332. forkable({269}) {
  3333. 281 ==> {
  3334. unify((((--,%1) ==>+- %2),%3)) ==> {
  3335. (Termify(((--,conjWithoutPN(%1,%3)) ==>+- %2),truth(punc(("?","?")),(),(),Task)),281)
  3336. }
  3337. }
  3338. }
  3339. }
  3340. and {
  3341. IsHas(beliefTerm,("==>",volMin(3)))
  3342. forkable({-66,-65}) {
  3343. 202 ==> {
  3344. unify((((--,%1) ==>+- %2),(%3 ==>+- %2))) ==> {
  3345. (Termify((%3 ==>+- %1),truth(punc(("?","?")),(),(),Compose)),202)
  3346. }
  3347. }
  3348. 203 ==> {
  3349. unify((((--,%1) ==>+- %2),(%3 ==>+- %1))) ==> {
  3350. (Termify((%3 ==>+- %2),truth(punc(("?","?")),(),(),Compose)),203)
  3351. }
  3352. }
  3353. }
  3354. }
  3355. }
  3356. }
  3357. }
  3358. }
  3359. and {
  3360. punc(("!","@"))
  3361. IsHas(taskTerm,("-->",volMin(3)))
  3362. IsHas(beliefTerm,("-->",volMin(3)))
  3363. fork {
  3364. and {
  3365. (--,Is(taskTerm((0)),"1111000000000"))
  3366. unifyIf(task((1)),neq,belief((1)))
  3367. unifyIf(task((1)),notSetsOrDifferentSets,belief((1)))
  3368. unifyIf(task((1)),neqRCom,belief((1)))
  3369. forkable({99}) {
  3370. 111 ==> {
  3371. unify(((%1-->%2),(%1-->%3))) ==> {
  3372. (Termify((%1-->interSect(polarizeTask(%2),polarizeBelief(%3))),truth(punc(("!","@")),(),(),Compose)),111)
  3373. }
  3374. }
  3375. }
  3376. }
  3377. and {
  3378. (--,Is(taskTerm((1)),"1111000000000"))
  3379. unifyIf(task((0)),neq,belief((0)))
  3380. unifyIf(task((0)),notSetsOrDifferentSets,belief((0)))
  3381. unifyIf(task((0)),neqRCom,belief((0)))
  3382. forkable({97}) {
  3383. 109 ==> {
  3384. unify(((%1-->%2),(%3-->%2))) ==> {
  3385. (Termify((interSect(polarizeTask(%1),polarizeBelief(%3))-->%2),truth(punc(("!","@")),(),(),Compose)),109)
  3386. }
  3387. }
  3388. }
  3389. }
  3390. and {
  3391. unifyIf(task((0)),neq,task((1)))
  3392. unifyIf(task((0)),neqRCom,task((1)))
  3393. forkable({20,21}) {
  3394. 32 ==> {
  3395. unify(((%1-->%2),(%3-->%2))) ==> {
  3396. (Termify(beliefTerm,truth(punc(("!","@")),(),(),Compose)),32)
  3397. }
  3398. }
  3399. 33 ==> {
  3400. unify(((%1-->%2),(%1-->%3))) ==> {
  3401. (Termify(beliefTerm,truth(punc(("!","@")),(),(),Compose)),33)
  3402. }
  3403. }
  3404. }
  3405. }
  3406. and {
  3407. unifyIf(task((0)),neq,belief((1)))
  3408. unifyIf(task((0)),neqRCom,belief((1)))
  3409. forkable({7,28}) {
  3410. 19 ==> {
  3411. unify(((%1-->%2),(%2-->%3))) ==> {
  3412. (Termify(beliefTerm,truth(punc(("!","@")),(),(),Compose)),19)
  3413. }
  3414. }
  3415. 40 ==> {
  3416. unify(((%1-->%2),(%1-->%3))) ==> {
  3417. (Termify(beliefTerm,truth(punc(("!","@")),(),(),Compose)),40)
  3418. }
  3419. }
  3420. }
  3421. }
  3422. and {
  3423. unifyIf(task((1)),neq,belief((0)))
  3424. unifyIf(task((1)),neqRCom,belief((0)))
  3425. forkable({6,29}) {
  3426. 18 ==> {
  3427. unify(((%1-->%2),(%3-->%1))) ==> {
  3428. (Termify(beliefTerm,truth(punc(("!","@")),(),(),Compose)),18)
  3429. }
  3430. }
  3431. 41 ==> {
  3432. unify(((%1-->%2),(%3-->%2))) ==> {
  3433. (Termify(beliefTerm,truth(punc(("!","@")),(),(),Compose)),41)
  3434. }
  3435. }
  3436. }
  3437. }
  3438. }
  3439. }
  3440. and {
  3441. punc((".","?"))
  3442. DoublePremise()
  3443. IsHas(taskTerm,("==>",volMin(3)))
  3444. IsHas(beliefTerm,("==>",volMin(3)))
  3445. fork {
  3446. and {
  3447. unifyIf(task((0)),neqPN,belief((0)))
  3448. forkable({284,285}) {
  3449. 296 ==> {
  3450. unify(((%1 ==>+- %2),(%3 ==>+- %2))) ==> {
  3451. (Termify((((--,%3) &&+- %1) ==>+- %2),truth(punc((".","?")),(),(),Compose)),296)
  3452. }
  3453. }
  3454. 297 ==> {
  3455. unify(((%1 ==>+- %2),(%3 ==>+- %2))) ==> {
  3456. (Termify((((--,%1) &&+- %3) ==>+- %2),truth(punc((".","?")),(),(),Compose)),297)
  3457. }
  3458. }
  3459. }
  3460. }
  3461. and {
  3462. unifyIf(task((1)),neqPN,belief((1)))
  3463. forkable({286,287}) {
  3464. 298 ==> {
  3465. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  3466. (Termify((%1 ==>+- ((--,%3) &&+- %2)),truth(punc((".","?")),(),(),Compose)),298)
  3467. }
  3468. }
  3469. 299 ==> {
  3470. unify(((%1 ==>+- %2),(%1 ==>+- %3))) ==> {
  3471. (Termify((%1 ==>+- ((--,%2) &&+- %3)),truth(punc((".","?")),(),(),Compose)),299)
  3472. }
  3473. }
  3474. }
  3475. }
  3476. }
  3477. }
  3478. and {
  3479. punc({("!","@"),(".","?"),("?","?"),("@","@")})
  3480. unifyIf(belief(()),Eventable,(()))
  3481. Is(taskTerm,"&&")
  3482. unifyIf(task(()),VolumeCompare,belief(()))
  3483. unifyIf(task(()),"Event->(+)",belief(()))
  3484. unifyIf(task(()),"Event->(-)",belief(()))
  3485. forkable({275}) {
  3486. 287 ==> {
  3487. unify((%1,%2)) ==> {
  3488. (Termify((conjWithoutPN(%2) ==>+- %2),truth(punc({("!","@"),(".","?"),("?","?"),("@","@")}),(),(),Task)),287)
  3489. }
  3490. }
  3491. }
  3492. }
  3493. and {
  3494. punc({("!","@"),(".","?")})
  3495. DoublePremise()
  3496. IsHas(taskTerm,("&&",volMin(3)))
  3497. IsHas(beliefTerm,("&&",volMin(3)))
  3498. forkable({288,289}) {
  3499. 300 ==> {
  3500. and {
  3501. unifyIf(%2,{(neq,%1),(neq,%3)})
  3502. unifyIf(%3,{(neq,%2),(neqPN,%1)})
  3503. unifyIf(%1,{(neq,%2),(neqPN,%3)})
  3504. unify(((%1 &&+- %2),(%2 &&+- %3))) ==> {
  3505. (Termify(((--,%3) &&+- %1),truth(punc({("!","@"),(".","?")}),(),(),Compose)),300)
  3506. }
  3507. }
  3508. }
  3509. 301 ==> {
  3510. and {
  3511. unifyIf(%2,{(neq,%1),(neq,%3)})
  3512. unifyIf(%3,{(neq,%2),(neqPN,%1)})
  3513. unifyIf(%1,{(neq,%2),(neqPN,%3)})
  3514. unify(((%1 &&+- %2),(%2 &&+- %3))) ==> {
  3515. (Termify(((--,%1) &&+- %3),truth(punc({("!","@"),(".","?")}),(),(),Compose)),301)
  3516. }
  3517. }
  3518. }
  3519. }
  3520. }
  3521. and {
  3522. punc({"!",".","?","@"})
  3523. Is(beliefTerm,"111111111")
  3524. (--,unifyIf(task(()),VolumeCompare,belief(())))
  3525. forkable({311}) {
  3526. 323 ==> {
  3527. ("nars.derive.action.AdjacentLinks","qla7w1")
  3528. }
  3529. }
  3530. }
  3531. and {
  3532. SubsMin(taskTerm,1)
  3533. forkable({310}) {
  3534. 322 ==> {
  3535. ("nars.derive.action.CompoundDecompose","kcbgdc")
  3536. }
  3537. }
  3538. }
  3539. and {
  3540. punc(";")
  3541. forkable({309}) {
  3542. 321 ==> {
  3543. ("nars.derive.action.TaskResolve","joad6h")
  3544. }
  3545. }
  3546. }
  3547. }
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!