SHARE
TWEET

Untitled

a guest Oct 9th, 2019 125 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  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. }
RAW Paste Data
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
 
Top