Failed

logicmoo.base.examples.fol.SANITY_EXISTS_02.logicmoo.base.examples.fol.SANITY_EXISTS_02@Test_0007_Line_0000__tHeart_1_in_t123: t123:tHeart(Heart1) (from logicmoo.base.examples.fol.logicmoo.base.examples.fol.SANITY_EXISTS_02)

Failing for the past 1 build (Since #9 )
Took 0 ms.

Error Message

failure = "failure=info((why_was_true(t123:(\\+tHeart(_1098758))),nop(ftrace(t123:tHeart(_1098758)))))\nno_proof_for(\\+tHeart(Heart1)).\n\nno_proof_for(\\+tHeart(Heart1)).\n\nno_proof_for(\\+tHeart(Heart1)).\n\n". failure = []. 

Standard Error

name=Test_0007_Line_0000__tHeart_1_in_t123
JUNIT_CLASSNAME='logicmoo.base.examples.fol.SANITY_EXISTS_02'.
JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'sanity_exists_02.pfc.pl\']"'.
 (cd /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol ; timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "['sanity_exists_02.pfc.pl']")

```
%~ init_phase(after_load)
%~ init_phase(restore_state)
%
%~ init_why(after_boot,program)
%~ after_boot.
%~ Dont forget to ?- logicmoo_i_cyc_xform.
running('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl'),
%~ this_test_might_need( :-( use_module( library(logicmoo_plarkc))))
%~ message_hook(
%~    error( permission_error(redefine,module,logicmoo_test),
%~      context(module/2,'Already loaded from /root/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test.pl')),
%~    error,
%~    [ '~q/~w: '-[module,2],
%~      'No permission to ~w ~w `~p\''-[redefine,module,logicmoo_test],
%~      ' (~w)'-['Already loaded from /root/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test.pl']])
%~ /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test_header.pl:98
%~ source_location('/var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test_header.pl',98)
module/2: No permission to redefine module `logicmoo_test' (Already loaded from /root/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test.pl)
ERROR: /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test_header.pl:98:
ERROR:    module/2: No permission to redefine module `logicmoo_test' (Already loaded from /root/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test.pl)
%~ message_hook(
%~    error( permission_error(redefine,module,logicmoo_clif),
%~      context(
%~         prolog_stack( [ frame( 61,
%~                           call( system : '$declare_module'/6),
%~                           '$declare_module'( logicmoo_clif,
%~                             user,
%~                              user, '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl', 1, false)),
%~                         frame( 60,
%~                           clause(<gt;clause>(0x55ed73c8ec00),61),
%~                           '$start_module'( logicmoo_clif,
%~                             [],
%~                             state( true,
%~                               logicmoo_clif, true,false,
%~                                '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl', -),
%~                             [ if(not_loaded),
%~                               true])),
%~                         frame( 59,
%~                           clause(<gt;clause>(0x55ed73a7b000),65),
%~                           '$first_term'(
%~                              :-( module(logicmoo_clif,[])),
%~                              _22528,
%~                              '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',
%~                              state( true,
%~                                logicmoo_clif, true,false,
%~                                 '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl', -),
%~                              [ if(not_loaded),
%~                                true])),
%~                         frame( 58,
%~                           clause(<gt;clause>(0x55ed73a7b400),60),
%~                           '$load_file'( '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',
%~                             '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',
%~                             Var_c47_lib_c47_jenkins_c47_workspace_c47_logicmoo_workspace_c47_packs_sys_c47_logicmoo_base_c47_prolog_c47_logicmoo_clif_c46_pl,
%~                             [ if(not_loaded),
%~                               true])),
%~                         frame( 57,
%~                           clause(<gt;clause>(0x55ed73cd1980),5),
%~                           setup_call_catcher_cleanup(
%~                              system : '$start_consult'('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',1632432905.770371),
%~                              system : '$load_file'( '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',
%~                                         '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',
%~                                         Var_c47_lib_c47_jenkins_c47_workspace_c47_logicmoo_workspace_c47_packs_sys_c47_logicmoo_base_c47_prolog_c47_logicmoo_clif_c46_pl1,
%~                                         [ if(not_loaded),
%~                                           true]),
%~                              Kw,
%~                              system : '$end_consult'( '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',
%~                                         lexstate(202,pfc),
%~                                         t123))),
%~                         frame( 53,
%~                           clause(<gt;clause>(0x55ed73ece000),221),
%~                           '$do_load_file_2'( library(logicmoo_clif),
%~                             '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl', t123,compiled,
%~                             [ if(not_loaded),
%~                               true])),
%~                         frame( 50,
%~                           clause(<gt;clause>(0x55ed73ca4840),10),
%~                           '$qdo_load_file'( library(logicmoo_clif),
%~                             '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl', t123,[if(not_loaded),true])),
%~                         frame( 48,
%~                           clause(<gt;clause>(0x55ed73cd1980),5),
%~                           setup_call_catcher_cleanup(
%~                              system : with_mutex( '$load_file',
%~                                         '$mt_start_load'( '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',
%~                                           <gt;clause>(0x55ed7534c580),
%~                                           [ if(not_loaded),
%~                                             true])),
%~                              system : '$mt_do_load'( <gt;clause>(0x55ed7534c580),
%~                                         library(logicmoo_clif),
%~                                         '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl', t123,[if(not_loaded),true]),
%~                              Kw3,
%~                              system : '$mt_end_load'(<gt;clause>(0x55ed7534c580)))),
%~                         frame(46,meta_call,0),
%~                         frame( 45,
%~                           foreign( system : '$sig_atomic'/1),
%~                           $sig_atomic( setup_call_cleanup(
%~                                           with_mutex( '$load_file',
%~                                             '$mt_start_load'( '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',
%~                                               <gt;clause>(0x55ed7534c580),
%~                                               [ if(not_loaded),
%~                                                 true])),
%~                                           '$mt_do_load'( <gt;clause>(0x55ed7534c580),
%~                                             library(logicmoo_clif),
%~                                             '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl', t123,[if(not_loaded),true]),
%~                                           '$mt_end_load'(<gt;clause>(0x55ed7534c580))))),
%~                         frame( 42,
%~                           clause(<gt;clause>(0x55ed73caac80),12),
%~                           '$load_file'(library(logicmoo_clif),t123,[if(not_loaded),true])),
%~                         frame( 37,
%~                           clause(<gt;clause>(0x55ed87a0ac80),31),
%~                           clif_dialect : clif_expects_dialect(clif,'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',pfc,t123)),
%~                         frame(36,clause(<gt;clause>(0x55ed87a25b00),49),clif_dialect:clif_expects_dialect(clif)),
%~                         frame(34,clause(<gt;clause>(0x55ed85f1c480),60),prolog_dialect:attach_dialect(clif)),
%~                         frame(33,clause(<gt;clause>(0x55ed85f0b200),20),prolog_dialect:expects_dialect(clif)),
%~                         frame( 32,
%~                           clause(<gt;clause>(0x55ed73ca1380),2),
%~                           catch(
%~                              t123 : expects_dialect(clif),
%~                              error(Error,Error18),
%~                              system : $exception_in_directive( error(Error5,Error19)))),
%~                         frame(31,clause(<gt;clause>(0x55ed73c6e580),55),'$execute_directive_3'(expects_dialect(clif))),
%~                         frame( 26,
%~                           clause(<gt;clause>(0x55ed73a7b400),77),
%~                           '$load_file'( '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',
%~                             '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',
%~                             Var_c47_lib_c47_jenkins_c47_workspace_c47_logicmoo_workspace_c47_packs_sys_c47_logicmoo_base_c47_t_c47_examples_c47_fol_c47_sanity_exists_02_c46_pfc_c46_pl,
%~                             [ expand(false),
%~                               expand(true)])),
%~                         frame( 25,
%~                           clause(<gt;clause>(0x55ed73cd1980),5),
%~                           setup_call_catcher_cleanup(
%~                              system : '$start_consult'('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',1632225669.4831774),
%~                              system : '$load_file'( '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',
%~                                         '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',
%~                                         Var_c47_lib_c47_jenkins_c47_workspace_c47_logicmoo_workspace_c47_packs_sys_c47_logicmoo_base_c47_t_c47_examples_c47_fol_c47_sanity_exists_02_c46_pfc_c46_pl7,
%~                                         [ expand(false),
%~                                           expand(true)]),
%~                              Kw8,
%~                              system : '$end_consult'( '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',
%~                                         lexstate(202,swi),
%~                                         user))),
%~                         frame( 21,
%~                           clause(<gt;clause>(0x55ed73ece000),221),
%~                           '$do_load_file_2'( 'sanity_exists_02.pfc.pl',
%~                             '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl', user,compiled,
%~                             [ expand(false),
%~                               expand(true)])),
%~                         frame( 18,
%~                           clause(<gt;clause>(0x55ed73ca4840),10),
%~                           '$qdo_load_file'( 'sanity_exists_02.pfc.pl',
%~                             '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl', user,[expand(false),expand(true)])),
%~                         frame( 16,
%~                           clause(<gt;clause>(0x55ed73cd1980),5),
%~                           setup_call_catcher_cleanup(
%~                              system : with_mutex( '$load_file',
%~                                         '$mt_start_load'( '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',
%~                                           <gt;clause>(0x55ed7534ca80),
%~                                           [ expand(false),
%~                                             expand(true)])),
%~                              system : '$mt_do_load'( <gt;clause>(0x55ed7534ca80),
%~                                         'sanity_exists_02.pfc.pl',
%~                                         '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',
%~                                         user,
%~                                         [ expand(false),
%~                                           expand(true)]),
%~                              Kw9,
%~                              system : '$mt_end_load'(<gt;clause>(0x55ed7534ca80)))),
%~                         frame(14,meta_call,0),
%~                         frame( 13,
%~                           foreign( system : '$sig_atomic'/1),
%~                           $sig_atomic( setup_call_cleanup(
%~                                           with_mutex( '$load_file',
%~                                             '$mt_start_load'( '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',
%~                                               <gt;clause>(0x55ed7534ca80),
%~                                               [ expand(false),
%~                                                 expand(true)])),
%~                                           '$mt_do_load'( <gt;clause>(0x55ed7534ca80),
%~                                             'sanity_exists_02.pfc.pl',
%~                                             '/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl', user,[expand(false),expand(true)]),
%~                                           '$mt_end_load'(<gt;clause>(0x55ed7534ca80))))),
%~                         frame(10,clause(<gt;clause>(0x55ed73caac80),12),'$load_file'('sanity_exists_02.pfc.pl',user,'<gt;garbage_collected>'))]),
%~         'Already loaded from /root/.local/share/swi-prolog/pack/logicmoo_base/prolog/logicmoo_clif.pl')),
%~    error,
%~    [ 'No permission to ~w ~w `~p\''-[redefine,module,logicmoo_clif],
%~      ' (~w)'-['Already loaded from /root/.local/share/swi-prolog/pack/logicmoo_base/prolog/logicmoo_clif.pl'], nl,...(_10498)])
%~ source_location('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/test_header.pl',5)
No permission to redefine module `logicmoo_clif' (Already loaded from /root/.local/share/swi-prolog/pack/logicmoo_base/prolog/logicmoo_clif.pl)
In:
  [61] $declare_module(logicmoo_clif,user,user,'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',1,false)
  [60] $start_module(logicmoo_clif,[],state(true,logicmoo_clif,true,false,'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',-),[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:3166
  [59] $first_term((:-module(logicmoo_clif,[])),_706,'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',state(true,logicmoo_clif,true,false,'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',-),[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:3055
  [58] $load_file('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',_784,[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:3007
  [57] setup_call_catcher_cleanup(system: $start_consult('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',1632432905.770371),system: $load_file('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',_862,[if(not_loaded),must_be_module(true)]),_834,system: $end_consult('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',lexstate(202,pfc),t123)) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:646
  [53] $do_load_file_2(library(logicmoo_clif),'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',t123,compiled,[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2592
  [50] $qdo_load_file(library(logicmoo_clif),'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',t123,[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2547
  [48] setup_call_catcher_cleanup(system:with_mutex($load_file,$mt_start_load('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',<gt;clause>(0x55ed7534c580),[if(not_loaded),must_be_module(true)])),system: $mt_do_load(<gt;clause>(0x55ed7534c580),library(logicmoo_clif),'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',t123,[if(not_loaded),must_be_module(true)]),_1042,system: $mt_end_load(<gt;clause>(0x55ed7534c580))) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:646
  [46] <gt;meta call>
  [45] $sig_atomic(setup_call_cleanup(with_mutex($load_file,$mt_start_load('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',<gt;clause>(0x55ed7534c580),[if(not_loaded),must_be_module(true)])),$mt_do_load(<gt;clause>(0x55ed7534c580),library(logicmoo_clif),'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',t123,[if(not_loaded),must_be_module(true)]),$mt_end_load(<gt;clause>(0x55ed7534c580)))) <gt;foreign>
  [42] $load_file(library(logicmoo_clif),t123,[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2355
  [37] clif_dialect:clif_expects_dialect(clif,'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',pfc,t123) at /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/dialect/clif.pl:283
  [36] clif_dialect:clif_expects_dialect(clif) at /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/dialect/clif.pl:122
  [34] prolog_dialect:attach_dialect(clif) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/library/dialect.pl:87
  [33] prolog_dialect:expects_dialect(clif) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/library/dialect.pl:73
  [32] catch(t123:expects_dialect(clif),error(_1486,_1488),system: $exception_in_directive(error(_1502,_1504))) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:546
  [31] $execute_directive_3(expects_dialect(clif)) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:3574
  [26] $load_file('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',_1560,[expand(false),expand(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:3007
  [25] setup_call_catcher_cleanup(system: $start_consult('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',1632225669.4831774),system: $load_file('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',_1638,[expand(false),expand(true)]),_1610,system: $end_consult('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',lexstate(202,swi),user)) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:646
  [21] $do_load_file_2('sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',user,compiled,[expand(false),expand(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2592
  [18] $qdo_load_file('sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',user,[expand(false),expand(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2547
  [16] setup_call_catcher_cleanup(system:with_mutex($load_file,$mt_start_load('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',<gt;clause>(0x55ed7534ca80),[expand(false),expand(true)])),system: $mt_do_load(<gt;clause>(0x55ed7534ca80),'sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',user,[expand(false),expand(true)]),_1810,system: $mt_end_load(<gt;clause>(0x55ed7534ca80))) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:646
  [14] <gt;meta call>
  [13] $sig_atomic(setup_call_cleanup(with_mutex($load_file,$mt_start_load('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',<gt;clause>(0x55ed7534ca80),[expand(false),expand(true)])),$mt_do_load(<gt;clause>(0x55ed7534ca80),'sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',user,[expand(false),expand(true)]),$mt_end_load(<gt;clause>(0x55ed7534ca80)))) <gt;foreign>
  [10] $load_file('sanity_exists_02.pfc.pl',user,<gt;garbage_collected>) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2355

Note: some frames are missing due to last-call optimization.
Re-run your program in debug mode (:- debug.) to get more detail.
ERROR: /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/test_header.pl:5:
ERROR:    No permission to redefine module `logicmoo_clif' (Already loaded from /root/.local/share/swi-prolog/pack/logicmoo_base/prolog/logicmoo_clif.pl)
ERROR:    In:
ERROR:      [61] $declare_module(logicmoo_clif,user,user,'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',1,false)
ERROR:      [60] $start_module(logicmoo_clif,[],state(true,logicmoo_clif,true,false,'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',-),[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:3166
ERROR:      [59] $first_term((:-module(logicmoo_clif,[])),_706,'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',state(true,logicmoo_clif,true,false,'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',-),[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:3055
ERROR:      [58] $load_file('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',_784,[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:3007
ERROR:      [57] setup_call_catcher_cleanup(system: $start_consult('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',1632432905.770371),system: $load_file('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',_862,[if(not_loaded),must_be_module(true)]),_834,system: $end_consult('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',lexstate(202,pfc),t123)) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:646
ERROR:      [53] $do_load_file_2(library(logicmoo_clif),'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',t123,compiled,[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2592
ERROR:      [50] $qdo_load_file(library(logicmoo_clif),'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',t123,[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2547
ERROR:      [48] setup_call_catcher_cleanup(system:with_mutex($load_file,$mt_start_load('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',<gt;clause>(0x55ed7534c580),[if(not_loaded),must_be_module(true)])),system: $mt_do_load(<gt;clause>(0x55ed7534c580),library(logicmoo_clif),'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',t123,[if(not_loaded),must_be_module(true)]),_1042,system: $mt_end_load(<gt;clause>(0x55ed7534c580))) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:646
ERROR:      [46] <gt;meta call>
ERROR:      [45] $sig_atomic(setup_call_cleanup(with_mutex($load_file,$mt_start_load('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',<gt;clause>(0x55ed7534c580),[if(not_loaded),must_be_module(true)])),$mt_do_load(<gt;clause>(0x55ed7534c580),library(logicmoo_clif),'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/logicmoo_clif.pl',t123,[if(not_loaded),must_be_module(true)]),$mt_end_load(<gt;clause>(0x55ed7534c580)))) <gt;foreign>
ERROR:      [42] $load_file(library(logicmoo_clif),t123,[if(not_loaded),must_be_module(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2355
ERROR:      [37] clif_dialect:clif_expects_dialect(clif,'/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',pfc,t123) at /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/dialect/clif.pl:283
ERROR:      [36] clif_dialect:clif_expects_dialect(clif) at /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/prolog/dialect/clif.pl:122
ERROR:      [34] prolog_dialect:attach_dialect(clif) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/library/dialect.pl:87
ERROR:      [33] prolog_dialect:expects_dialect(clif) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/library/dialect.pl:73
ERROR:      [32] catch(t123:expects_dialect(clif),error(_1486,_1488),system: $exception_in_directive(error(_1502,_1504))) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:546
ERROR:      [31] $execute_directive_3(expects_dialect(clif)) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:3574
ERROR:      [26] $load_file('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',_1560,[expand(false),expand(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:3007
ERROR:      [25] setup_call_catcher_cleanup(system: $start_consult('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',1632225669.4831774),system: $load_file('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',_1638,[expand(false),expand(true)]),_1610,system: $end_consult('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',lexstate(202,swi),user)) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:646
ERROR:      [21] $do_load_file_2('sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',user,compiled,[expand(false),expand(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2592
ERROR:      [18] $qdo_load_file('sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',user,[expand(false),expand(true)]) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2547
ERROR:      [16] setup_call_catcher_cleanup(system:with_mutex($load_file,$mt_start_load('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',<gt;clause>(0x55ed7534ca80),[expand(false),expand(true)])),system: $mt_do_load(<gt;clause>(0x55ed7534ca80),'sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',user,[expand(false),expand(true)]),_1810,system: $mt_end_load(<gt;clause>(0x55ed7534ca80))) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:646
ERROR:      [14] <gt;meta call>
ERROR:      [13] $sig_atomic(setup_call_cleanup(with_mutex($load_file,$mt_start_load('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',<gt;clause>(0x55ed7534ca80),[expand(false),expand(true)])),$mt_do_load(<gt;clause>(0x55ed7534ca80),'sanity_exists_02.pfc.pl','/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl',user,[expand(false),expand(true)]),$mt_end_load(<gt;clause>(0x55ed7534ca80)))) <gt;foreign>
ERROR:      [10] $load_file('sanity_exists_02.pfc.pl',user,<gt;garbage_collected>) at /var/lib/jenkins/workspace/logicmoo_workspace/lib/swipl/boot/init.pl:2355
ERROR:   
ERROR:    Note: some frames are missing due to last-call optimization.
ERROR:    Re-run your program in debug mode (:- debug.) to get more detail.
%~ message_hook(
%~    goal_failed(directive,t123:expects_dialect(clif)),
%~    warning,
%~    [ 'Goal (~w) failed: ~p' - [ directive,
%~                                 t123 : expects_dialect(clif)]])
%~ source_location('/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/test_header.pl',5)
Goal (directive) failed: t123:expects_dialect(clif)
Warning: /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/test_header.pl:5:
Warning:    Goal (directive) failed: t123:expects_dialect(clif)

:- module(t123).

/*~
~*/

:- dynamic(t123:ttExpressionType/1).

% :- process_this_script.

/*~
~*/


% :- process_this_script.

:- statistics.

/*~
% Started at Mon Sep 27 03:39:46 2021
% 1.576 seconds cpu time for 6,677,634 inferences
% 942,554 atoms, 32,373 functors, 31,586 predicates, 751 modules, 15,991,676 VM-codes
%
%                     Limit   Allocated      In use
% Local  stack:           -      116 Kb    3,920  b
% Global stack:           -      512 Kb      148 Kb
% Trail  stack:           -      130 Kb      488  b
%        Total:    1,024 Mb      758 Kb      152 Kb
%
% 27 garbage collections gained 10,386,720 bytes in 0.005 seconds.
% 14 atom garbage collections gained 4,301 atoms in 0.179 seconds.
% 18 clause garbage collections gained 3,837 clauses in 0.001 seconds.
% Stack shifts: 2 local, 3 global, 2 trail in 0.001 seconds
% 3 threads, 0 finished threads used 0.000 seconds
~*/


subtest_assert(I):-kif_assert(I).

/*~
No source location!?
~*/

subtest([subtest_assert(tAnimal(joe)),
        mpred_test(isa(_,tHeart))]).

/*~
%~ make_dynamic_here( t123,
%~   '$nt'(
%~      subtest( [ subtest_assert( tAnimal(joe)),
%~                 mpred_test( tHeart(Heart))]), Subtest,Nt))
~*/

subtest([subtest_assert(tAnimal(joe)),
        mpred_test(hasOrgan(joe,_))]).

/*~
~*/

subtest([subtest_assert(tHeart(_)),
        mpred_test(~hasOrgan(jack,_))]).

/*~
~*/

add_test(Name,Assert):-
   test_boxlog(Assert),
   assert(( Name:- cls,test_assert(Assert))).

/*~
No source location!?
~*/

test_assert(A):-
  kif_assert(A),
  nop(forall(subtest(T),do_subtest(T))).

/*~
No source location!?
~*/


do_subtest(List):- must_maplist(call,List).

/*~
No source location!?
~*/


:- add_test(t121, (all([[Human,tAnimal]],exists([[Heart,tHeart]],hasOrgan(Human,Heart))))).

/*~
%~ ?-( mpred_test( "Test_0001_Line_0000__TAnimal_in_t123",
%~       t123 : test_boxlog( all(
%~                              [ [Human,tAnimal]],
%~                              exists([[Heart,tHeart]],hasOrgan(Human,Heart)))))).
%~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl:39
%~ correct_special_quantifiers :- all( Human,
%~                                  ( isa(Human,tAnimal) =>
%~                                    exists(Heart,hasOrgan(Human,Heart)&isa(Heart,tHeart)))).
%~ %~ correct_special_quantifiers:-all(Human,isa(Human,tAnimal)=>exists(Heart,hasOrgan(Human,Heart)&isa(Heart,tHeart)))
%~ kifi = all(
%~           [ [Human,tAnimal]],
%~           exists([[Heart,tHeart]],hasOrgan(Human,Heart))).
%~ kifm = all( Human,
%~          nesc( ( isa(Human,tAnimal) =>
%~                  exists(Heart,hasOrgan(Human,Heart)&isa(Heart,tHeart))))).
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Human'),necessary(=>(isa('$VAR'('Human'),tAnimal),exists('$VAR'('Heart'),and(hasOrgan('$VAR'('Human'),'$VAR'('Heart')),isa('$VAR'('Heart'),tHeart))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Heart isa tHeart " is necessarily true
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( poss(~hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( ~( hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'( Heart,
      1,
      nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)))) ==>
  poss( ~( isa(Heart,tHeart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is necessarily true )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'(Heart,1,nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)))  &
    nesc( isa(Human,tAnimal)) &
    nesc( isa(Heart,tHeart))) ==>
  nesc( hasOrgan(Human,Heart))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is necessarily true  and
%~    " ?Heart isa tHeart " is possibly false
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( nesc(hasOrgan(Human,Heart))&poss(~isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is possibly false )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'(Heart,1,nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)))  &
    nesc( isa(Human,tAnimal)) &
    poss( ~( isa(Heart,tHeart)))) ==>
  poss( ~( hasOrgan(Human,Heart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is necessarily true  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( hasOrgan(Human,Heart))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'( Heart,
      1,
      nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)))) ==>
  nesc( isa(Heart,tHeart))).

%~ correct_special_quantifiers :- all( HasOrgan,
%~                                  ( isa(HasOrgan,tAnimal) =>
%~                                    exists(HasOrgan5,hasOrgan(HasOrgan,HasOrgan5)&isa(HasOrgan5,tHeart)))).
%~ kifi = all(
%~           [ [HasOrgan,tAnimal]],
%~           exists(
%~              [ [HasOrgan5,tHeart]],
%~              hasOrgan(HasOrgan,HasOrgan5))).
%~ kifm = all( HasOrgan,
%~          nesc( ( isa(HasOrgan,tAnimal) =>
%~                  exists(HasOrgan5,hasOrgan(HasOrgan,HasOrgan5)&isa(HasOrgan5,tHeart))))).
passed=info(why_was_true(t123:test_boxlog(all([[_530,tAnimal]],exists([[_532,tHeart]],hasOrgan(_530,_532))))))
no_proof_for(test_boxlog(all([ [HasOrgan,tAnimal]],exists([ [HasOrgan5,tHeart]],hasOrgan(HasOrgan,HasOrgan5))))).

%~ %~ correct_special_quantifiers:-all(HasOrgan,isa(HasOrgan,tAnimal)=>exists(HasOrgan5,hasOrgan(HasOrgan,HasOrgan5)&isa(HasOrgan5,tHeart)))
%~ kifi=all([[HasOrgan,tAnimal]],exists([[HasOrgan5,tHeart]],hasOrgan(HasOrgan,HasOrgan5)))
%~ kifm=all(HasOrgan,nesc(isa(HasOrgan,tAnimal)=>exists(HasOrgan5,hasOrgan(HasOrgan,HasOrgan5)&isa(HasOrgan5,tHeart))))
%~ kif_to_boxlog_attvars2 = forall('$VAR'('HasOrgan'),necessary(=>(isa('$VAR'('HasOrgan'),tAnimal),exists('$VAR'('HasOrgan5'),and(hasOrgan('$VAR'('HasOrgan'),'$VAR'('HasOrgan5')),isa('$VAR'('HasOrgan5'),tHeart))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?HasOrgan hasOrgan ?HasOrgan5 " is possibly false  and
%~    " ?HasOrgan5 isa tHeart " is necessarily true
%~  It's Proof that:
%~    " ?HasOrgan isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( poss(~hasOrgan(HasOrgan,HasOrgan5))&nesc(isa(HasOrgan5,tHeart)) ==>
  poss( ~( isa(HasOrgan,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?HasOrgan hasOrgan ?HasOrgan5 " is possibly false  and
%~    " ?HasOrgan isa tAnimal " is necessarily true ) and
%~     by default ?HasOrgan5 nesc(hasOrgan(HasOrgan,HasOrgan5))&nesc(isa(HasOrgan5,tHeart))
%~  It's Proof that:
%~    " ?HasOrgan5 isa tHeart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( ~( hasOrgan(HasOrgan,HasOrgan5)))  &
    nesc( isa(HasOrgan,tAnimal)) &
    '$existential'( HasOrgan5,
      1,
      nesc(hasOrgan(HasOrgan,HasOrgan5))&nesc(isa(HasOrgan5,tHeart)))) ==>
  poss( ~( isa(HasOrgan5,tHeart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?HasOrgan5 nesc(hasOrgan(HasOrgan,HasOrgan5))&nesc(isa(HasOrgan5,tHeart))  and
%~    (" ?HasOrgan isa tAnimal " is necessarily true  and
%~    " ?HasOrgan5 isa tHeart " is necessarily true )
%~  It's Proof that:
%~    " ?HasOrgan hasOrgan ?HasOrgan5 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'( HasOrgan5,
      1,
      nesc(hasOrgan(HasOrgan,HasOrgan5))&nesc(isa(HasOrgan5,tHeart)))  &
    nesc( isa(HasOrgan,tAnimal)) &
    nesc( isa(HasOrgan5,tHeart))) ==>
  nesc( hasOrgan(HasOrgan,HasOrgan5))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?HasOrgan hasOrgan ?HasOrgan5 " is necessarily true  and
%~    " ?HasOrgan5 isa tHeart " is possibly false
%~  It's Proof that:
%~    " ?HasOrgan isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( nesc(hasOrgan(HasOrgan,HasOrgan5))&poss(~isa(HasOrgan5,tHeart)) ==>
  poss( ~( isa(HasOrgan,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?HasOrgan5 nesc(hasOrgan(HasOrgan,HasOrgan5))&nesc(isa(HasOrgan5,tHeart))  and
%~    (" ?HasOrgan isa tAnimal " is necessarily true  and
%~    " ?HasOrgan5 isa tHeart " is possibly false )
%~  It's Proof that:
%~    " ?HasOrgan hasOrgan ?HasOrgan5 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'( HasOrgan5,
      1,
      nesc(hasOrgan(HasOrgan,HasOrgan5))&nesc(isa(HasOrgan5,tHeart)))  &
    nesc( isa(HasOrgan,tAnimal)) &
    poss( ~( isa(HasOrgan5,tHeart)))) ==>
  poss( ~( hasOrgan(HasOrgan,HasOrgan5)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?HasOrgan hasOrgan ?HasOrgan5 " is necessarily true  and
%~    " ?HasOrgan isa tAnimal " is necessarily true ) and
%~     by default ?HasOrgan5 nesc(hasOrgan(HasOrgan,HasOrgan5))&nesc(isa(HasOrgan5,tHeart))
%~  It's Proof that:
%~    " ?HasOrgan5 isa tHeart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( hasOrgan(HasOrgan,HasOrgan5))  &
    nesc( isa(HasOrgan,tAnimal)) &
    '$existential'( HasOrgan5,
      1,
      nesc(hasOrgan(HasOrgan,HasOrgan5))&nesc(isa(HasOrgan5,tHeart)))) ==>
  nesc( isa(HasOrgan5,tHeart))).

no_proof_for(test_boxlog(all([ [HasOrgan8,tAnimal]],exists([ [HasOrgan9,tHeart]],hasOrgan(HasOrgan8,HasOrgan9))))).

no_proof_for(test_boxlog(all([ [HasOrgan8,tAnimal]],exists([ [HasOrgan9,tHeart]],hasOrgan(HasOrgan8,HasOrgan9))))).

name='logicmoo.base.examples.fol.SANITY_EXISTS_02-Test_0001_Line_0000__TAnimal_in_t123'.
JUNIT_CLASSNAME='logicmoo.base.examples.fol.SANITY_EXISTS_02'.
JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'sanity_exists_02.pfc.pl\']"'.
% saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-base-examples-fol-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_examples_fol_SANITY_EXISTS_02_Test_0001_Line_0000_TAnimal_in_t123-junit.xml
~*/

:- add_test(t122,
 (isa(Human,tAnimal)=>all(Human,exists([[Heart,tHeart]],hasOrgan(Human,Heart))))).

/*~
%~ ?-( mpred_test( "Test_0002_Line_0000__THeart_in_t123",
%~       t123 : test_boxlog( ( isa(Human,tAnimal) =>
%~                             all( Human,
%~                               exists([[Heart,tHeart]],hasOrgan(Human,Heart))))))).
%~ correct_special_quantifiers :- ( isa(Human,tAnimal) =>
%~                                  all( Human,
%~                                    exists(Heart,hasOrgan(Human,Heart)&isa(Heart,tHeart)))).
%~ %~ correct_special_quantifiers:-isa(Human,tAnimal)=>all(Human,exists(Heart,hasOrgan(Human,Heart)&isa(Heart,tHeart)))
%~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl:42
%~ kifi = ( isa(Human,tAnimal) =>
%~          all( Human,
%~            exists([[Heart,tHeart]],hasOrgan(Human,Heart)))).
%~ kifm = nesc( ( isa(Human,tAnimal) =>
%~                all(Human,exists(Heart,hasOrgan(Human,Heart)&isa(Heart,tHeart))))).
%~ kif_to_boxlog_attvars2 = necessary(=>(isa('$VAR'('Human'),tAnimal),forall('$VAR'('Human'),exists('$VAR'('Heart'),and(hasOrgan('$VAR'('Human'),'$VAR'('Heart')),isa('$VAR'('Heart'),tHeart))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Heart isa tHeart " is necessarily true
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( poss(~hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( ~( hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'( Heart,
      1,
      nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)))) ==>
  poss( ~( isa(Heart,tHeart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is necessarily true )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'(Heart,1,nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)))  &
    nesc( isa(Human,tAnimal)) &
    nesc( isa(Heart,tHeart))) ==>
  nesc( hasOrgan(Human,Heart))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is necessarily true  and
%~    " ?Heart isa tHeart " is possibly false
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( nesc(hasOrgan(Human,Heart))&poss(~isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is possibly false )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'(Heart,1,nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)))  &
    nesc( isa(Human,tAnimal)) &
    poss( ~( isa(Heart,tHeart)))) ==>
  poss( ~( hasOrgan(Human,Heart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is necessarily true  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( hasOrgan(Human,Heart))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'( Heart,
      1,
      nesc(hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)))) ==>
  nesc( isa(Heart,tHeart))).

%~ correct_special_quantifiers :- ( isa(Exists_Animal_Animal,tAnimal) =>
%~                                  all( Exists_Animal_Animal,
%~                                    exists( HasOrgan,
%~                                      hasOrgan(Exists_Animal_Animal,HasOrgan)&isa(HasOrgan,tHeart)))).
%~ kifi = ( isa(Exists_Animal_Animal,tAnimal) =>
%~          all( Exists_Animal_Animal,
%~            exists(
%~               [ [HasOrgan,tHeart]],
%~               hasOrgan(Exists_Animal_Animal,HasOrgan)))).
%~ kifm = nesc( ( isa(Exists_Animal_Animal,tAnimal) =>
%~                all( Exists_Animal_Animal,
%~                  exists( HasOrgan,
%~                    hasOrgan(Exists_Animal_Animal,HasOrgan)&isa(HasOrgan,tHeart))))).
passed=info(why_was_true(t123:test_boxlog(isa(_518,tAnimal)=>all(_518,exists([[_520,tHeart]],hasOrgan(_518,_520))))))
no_proof_for(test_boxlog(isa(Exists_Animal_Animal_Animal_Animal,tAnimal)=>all(Exists_Animal_Animal_Animal_Animal,exists([
  [HasOrgan,tHeart]],hasOrgan(Exists_Animal_Animal_Animal_Animal,HasOrgan))))).

%~ %~ correct_special_quantifiers:-isa(Exists_Animal_Animal,tAnimal)=>all(Exists_Animal_Animal,exists(HasOrgan,hasOrgan(Exists_Animal_Animal,HasOrgan)&isa(HasOrgan,tHeart)))
%~ kifi=isa(Exists_Animal_Animal,tAnimal)=>all(Exists_Animal_Animal,exists([[HasOrgan,tHeart]],hasOrgan(Exists_Animal_Animal,HasOrgan)))
%~ kifm=nesc(isa(Exists_Animal_Animal,tAnimal)=>all(Exists_Animal_Animal,exists(HasOrgan,hasOrgan(Exists_Animal_Animal,HasOrgan)&isa(HasOrgan,tHeart))))
%~ kif_to_boxlog_attvars2 = necessary(=>(isa('$VAR'('Exists_Animal_Animal'),tAnimal),forall('$VAR'('Exists_Animal_Animal'),exists('$VAR'('HasOrgan'),and(hasOrgan('$VAR'('Exists_Animal_Animal'),'$VAR'('HasOrgan')),isa('$VAR'('HasOrgan'),tHeart))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Exists_Animal_Animal hasOrgan ?HasOrgan " is possibly false  and
%~    " ?HasOrgan isa tHeart " is necessarily true
%~  It's Proof that:
%~    " ?Exists_Animal_Animal isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( poss(~hasOrgan(Exists_Animal_Animal,HasOrgan))&nesc(isa(HasOrgan,tHeart)) ==>
  poss( ~( isa(Exists_Animal_Animal,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Exists_Animal_Animal hasOrgan ?HasOrgan " is possibly false  and
%~    " ?Exists_Animal_Animal isa tAnimal " is necessarily true ) and
%~     by default ?HasOrgan nesc(hasOrgan(Exists_Animal_Animal,HasOrgan))&nesc(isa(HasOrgan,tHeart))
%~  It's Proof that:
%~    " ?HasOrgan isa tHeart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( ~( hasOrgan(Exists_Animal_Animal,HasOrgan)))  &
    nesc( isa(Exists_Animal_Animal,tAnimal)) &
    '$existential'( HasOrgan,
      1,
      nesc(hasOrgan(Exists_Animal_Animal,HasOrgan))&nesc(isa(HasOrgan,tHeart)))) ==>
  poss( ~( isa(HasOrgan,tHeart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?HasOrgan nesc(hasOrgan(Exists_Animal_Animal,HasOrgan))&nesc(isa(HasOrgan,tHeart))  and
%~    (" ?Exists_Animal_Animal isa tAnimal " is necessarily true  and
%~    " ?HasOrgan isa tHeart " is necessarily true )
%~  It's Proof that:
%~    " ?Exists_Animal_Animal hasOrgan ?HasOrgan " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'( HasOrgan,
      1,
      nesc(hasOrgan(Exists_Animal_Animal,HasOrgan))&nesc(isa(HasOrgan,tHeart)))  &
    nesc( isa(Exists_Animal_Animal,tAnimal)) &
    nesc( isa(HasOrgan,tHeart))) ==>
  nesc( hasOrgan(Exists_Animal_Animal,HasOrgan))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Exists_Animal_Animal hasOrgan ?HasOrgan " is necessarily true  and
%~    " ?HasOrgan isa tHeart " is possibly false
%~  It's Proof that:
%~    " ?Exists_Animal_Animal isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( nesc(hasOrgan(Exists_Animal_Animal,HasOrgan))&poss(~isa(HasOrgan,tHeart)) ==>
  poss( ~( isa(Exists_Animal_Animal,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?HasOrgan nesc(hasOrgan(Exists_Animal_Animal,HasOrgan))&nesc(isa(HasOrgan,tHeart))  and
%~    (" ?Exists_Animal_Animal isa tAnimal " is necessarily true  and
%~    " ?HasOrgan isa tHeart " is possibly false )
%~  It's Proof that:
%~    " ?Exists_Animal_Animal hasOrgan ?HasOrgan " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'( HasOrgan,
      1,
      nesc(hasOrgan(Exists_Animal_Animal,HasOrgan))&nesc(isa(HasOrgan,tHeart)))  &
    nesc( isa(Exists_Animal_Animal,tAnimal)) &
    poss( ~( isa(HasOrgan,tHeart)))) ==>
  poss( ~( hasOrgan(Exists_Animal_Animal,HasOrgan)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Exists_Animal_Animal hasOrgan ?HasOrgan " is necessarily true  and
%~    " ?Exists_Animal_Animal isa tAnimal " is necessarily true ) and
%~     by default ?HasOrgan nesc(hasOrgan(Exists_Animal_Animal,HasOrgan))&nesc(isa(HasOrgan,tHeart))
%~  It's Proof that:
%~    " ?HasOrgan isa tHeart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( hasOrgan(Exists_Animal_Animal,HasOrgan))  &
    nesc( isa(Exists_Animal_Animal,tAnimal)) &
    '$existential'( HasOrgan,
      1,
      nesc(hasOrgan(Exists_Animal_Animal,HasOrgan))&nesc(isa(HasOrgan,tHeart)))) ==>
  nesc( isa(HasOrgan,tHeart))).

no_proof_for(test_boxlog(isa(Exists_Animal10_Animal_Animal_Animal,tAnimal)=>all(Exists_Animal10_Animal_Animal_Animal,exists(
    [ [HasOrgan13,tHeart]],hasOrgan(Exists_Animal10_Animal_Animal_Animal,HasOrgan13))))).

no_proof_for(test_boxlog(isa(Exists_Animal10_Animal_Animal_Animal,tAnimal)=>all(Exists_Animal10_Animal_Animal_Animal,exists(
    [ [HasOrgan13,tHeart]],hasOrgan(Exists_Animal10_Animal_Animal_Animal,HasOrgan13))))).

name='logicmoo.base.examples.fol.SANITY_EXISTS_02-Test_0002_Line_0000__THeart_in_t123'.
JUNIT_CLASSNAME='logicmoo.base.examples.fol.SANITY_EXISTS_02'.
JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'sanity_exists_02.pfc.pl\']"'.
% saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-base-examples-fol-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_examples_fol_SANITY_EXISTS_02_Test_0002_Line_0000_THeart_in_t123-junit.xml
~*/

:- add_test(t123,
 (isa(Human,tAnimal)=>all(Human,(isa(Heart,tHeart)=>exists(Heart,hasOrgan(Human,Heart)))))).

/*~
%~ ?-( mpred_test( "Test_0003_Line_0000__TAnimal_in_t123",
%~       t123 : test_boxlog( ( isa(Human,tAnimal) =>
%~                             all( Human,
%~                               isa(Heart,tHeart)=>exists(Heart,hasOrgan(Human,Heart))))))).
%~ kifi = ( isa(Human,tAnimal) =>
%~          all( Human,
%~            isa(Heart,tHeart)=>exists(Heart,hasOrgan(Human,Heart)))).
%~ kifm = nesc( ( isa(Human,tAnimal) =>
%~                all( Human,
%~                  isa(Heart,tHeart)=>exists(Heart,hasOrgan(Human,Heart))))).
%~ kif_to_boxlog_attvars2 = necessary(=>(isa('$VAR'('Human'),tAnimal),forall('$VAR'('Human'),=>(isa('$VAR'('Heart'),tHeart),exists('$VAR'('Heart'),hasOrgan('$VAR'('Human'),'$VAR'('Heart')))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Heart isa tHeart " is necessarily true
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( poss(~hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(hasOrgan(Human,Heart))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( ~( hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'(Heart,1,nesc(hasOrgan(Human,Heart)))) ==>
  poss( ~( isa(Heart,tHeart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(hasOrgan(Human,Heart))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is necessarily true )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'(Heart,1,nesc(hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    nesc( isa(Heart,tHeart))) ==>
  nesc( hasOrgan(Human,Heart))).

%~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_02.pfc.pl:45
%~ kifi = ( isa(Human,tAnimal) =>
%~          all( Human,
%~            isa(Heart,tHeart)=>exists(Heart,hasOrgan(Human,Heart)))).
%~ kifm = nesc( ( isa(Human,tAnimal) =>
%~                all( Human,
%~                  isa(Heart,tHeart)=>exists(Heart,hasOrgan(Human,Heart))))).
passed=info(why_was_true(t123:test_boxlog(isa(_650,tAnimal)=>all(_650,isa(_652,tHeart)=>exists(_652,hasOrgan(_650,_652))))))
no_proof_for(test_boxlog(isa(Human,tAnimal)=>all(Human,isa(Heart,tHeart)=>exists(Heart,hasOrgan(Human,Heart))))).

%~ kifi=isa(Human,tAnimal)=>all(Human,isa(Heart,tHeart)=>exists(Heart,hasOrgan(Human,Heart)))
%~ kifm=nesc(isa(Human,tAnimal)=>all(Human,isa(Heart,tHeart)=>exists(Heart,hasOrgan(Human,Heart))))
%~ kif_to_boxlog_attvars2 = necessary(=>(isa('$VAR'('Human'),tAnimal),forall('$VAR'('Human'),=>(isa('$VAR'('Heart'),tHeart),exists('$VAR'('Heart'),hasOrgan('$VAR'('Human'),'$VAR'('Heart')))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Heart isa tHeart " is necessarily true
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( poss(~hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(hasOrgan(Human,Heart))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( ~( hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'(Heart,1,nesc(hasOrgan(Human,Heart)))) ==>
  poss( ~( isa(Heart,tHeart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(hasOrgan(Human,Heart))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is necessarily true )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'(Heart,1,nesc(hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    nesc( isa(Heart,tHeart))) ==>
  nesc( hasOrgan(Human,Heart))).

no_proof_for(test_boxlog(isa(Human,tAnimal)=>all(Human,isa(Heart,tHeart)=>exists(Heart,hasOrgan(Human,Heart))))).

no_proof_for(test_boxlog(isa(Human,tAnimal)=>all(Human,isa(Heart,tHeart)=>exists(Heart,hasOrgan(Human,Heart))))).

name='logicmoo.base.examples.fol.SANITY_EXISTS_02-Test_0003_Line_0000__TAnimal_in_t123'.
JUNIT_CLASSNAME='logicmoo.base.examples.fol.SANITY_EXISTS_02'.
JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'sanity_exists_02.pfc.pl\']"'.
% saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-base-examples-fol-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_examples_fol_SANITY_EXISTS_02_Test_0003_Line_0000_TAnimal_in_t123-junit.xml
~*/

:- add_test(t124,
 (all(Human,exists(Heart,isa(Human,tAnimal)
     => (isa(Heart,tHeart)
      & hasOrgan(Human,Heart)))))).

/*~
%~ ?-( mpred_test( "Test_0004_Line_0000__TAnimal_in_t123",
%~       t123 : test_boxlog( all( Human,
%~                             exists( Heart,
%~                               isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart))))))).
%~ kifi = all( Human,
%~          exists( Heart,
%~            isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart)))).
%~ kifm = all( Human,
%~          exists( Heart,
%~            nesc( isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart))))).
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Human'),exists('$VAR'('Heart'),necessary(=>(isa('$VAR'('Human'),tAnimal),and(isa('$VAR'('Heart'),tHeart),hasOrgan('$VAR'('Human'),'$VAR'('Heart')))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is necessarily true  and
%~    " ?Heart isa tHeart " is possibly false
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( nesc(hasOrgan(Human,Heart))&poss(~isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(isa(Human,tAnimal))=>(nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart)))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is possibly false )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'( Heart,
      1,
      ( nesc( isa(Human,tAnimal)) =>
        nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart))))  &
    nesc( isa(Human,tAnimal)) &
    poss( ~( isa(Heart,tHeart)))) ==>
  poss( ~( hasOrgan(Human,Heart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is necessarily true  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(isa(Human,tAnimal))=>(nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart)))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( hasOrgan(Human,Heart))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'( Heart,
      1,
      ( nesc( isa(Human,tAnimal)) =>
        nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart))))) ==>
  nesc( isa(Heart,tHeart))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Heart isa tHeart " is necessarily true
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( poss(~hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(isa(Human,tAnimal))=>(nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart)))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( ~( hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'( Heart,
      1,
      ( nesc( isa(Human,tAnimal)) =>
        nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart))))) ==>
  poss( ~( isa(Heart,tHeart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(isa(Human,tAnimal))=>(nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart)))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is necessarily true )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'( Heart,
      1,
      ( nesc( isa(Human,tAnimal)) =>
        nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart))))  &
    nesc( isa(Human,tAnimal)) &
    nesc( isa(Heart,tHeart))) ==>
  nesc( hasOrgan(Human,Heart))).

%~ kifi = all( Human,
%~          exists( Heart,
%~            isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart)))).
%~ kifm = all( Human,
%~          exists( Heart,
%~            nesc( isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart))))).
passed=info(why_was_true(t123:test_boxlog(all(_650,exists(_652,isa(_650,tAnimal)=>(isa(_652,tHeart)&hasOrgan(_650,_652)))))))
no_proof_for(test_boxlog(all(Human,exists(Heart,isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart)))))).

%~ kifi=all(Human,exists(Heart,isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart))))
%~ kifm=all(Human,exists(Heart,nesc(isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart)))))
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Human'),exists('$VAR'('Heart'),necessary(=>(isa('$VAR'('Human'),tAnimal),and(isa('$VAR'('Heart'),tHeart),hasOrgan('$VAR'('Human'),'$VAR'('Heart')))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is necessarily true  and
%~    " ?Heart isa tHeart " is possibly false
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( nesc(hasOrgan(Human,Heart))&poss(~isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(isa(Human,tAnimal))=>(nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart)))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is possibly false )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'( Heart,
      1,
      ( nesc( isa(Human,tAnimal)) =>
        nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart))))  &
    nesc( isa(Human,tAnimal)) &
    poss( ~( isa(Heart,tHeart)))) ==>
  poss( ~( hasOrgan(Human,Heart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is necessarily true  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(isa(Human,tAnimal))=>(nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart)))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( hasOrgan(Human,Heart))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'( Heart,
      1,
      ( nesc( isa(Human,tAnimal)) =>
        nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart))))) ==>
  nesc( isa(Heart,tHeart))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Heart isa tHeart " is necessarily true
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( poss(~hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(isa(Human,tAnimal))=>(nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart)))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( ~( hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'( Heart,
      1,
      ( nesc( isa(Human,tAnimal)) =>
        nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart))))) ==>
  poss( ~( isa(Heart,tHeart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(isa(Human,tAnimal))=>(nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart)))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is necessarily true )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'( Heart,
      1,
      ( nesc( isa(Human,tAnimal)) =>
        nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart))))  &
    nesc( isa(Human,tAnimal)) &
    nesc( isa(Heart,tHeart))) ==>
  nesc( hasOrgan(Human,Heart))).

no_proof_for(test_boxlog(all(Human,exists(Heart,isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart)))))).

no_proof_for(test_boxlog(all(Human,exists(Heart,isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart)))))).

name='logicmoo.base.examples.fol.SANITY_EXISTS_02-Test_0004_Line_0000__TAnimal_in_t123'.
JUNIT_CLASSNAME='logicmoo.base.examples.fol.SANITY_EXISTS_02'.
JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'sanity_exists_02.pfc.pl\']"'.
% saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-base-examples-fol-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_examples_fol_SANITY_EXISTS_02_Test_0004_Line_0000_TAnimal_in_t123-junit.xml
~*/

:- add_test(t125,
  (all(Human,isa(Human,tAnimal) => exists(Heart, (isa(Heart,tHeart)  =>  hasOrgan(Human,Heart)))))).

/*~
%~ ?-( mpred_test( "Test_0005_Line_0000__TAnimal_in_t123",
%~       t123 : test_boxlog( all( Human,
%~                             ( isa(Human,tAnimal) =>
%~                               exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart))))))).
%~ kifi = all( Human,
%~          ( isa(Human,tAnimal) =>
%~            exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart)))).
%~ kifm = all( Human,
%~          nesc( ( isa(Human,tAnimal) =>
%~                  exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart))))).
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Human'),necessary(=>(isa('$VAR'('Human'),tAnimal),exists('$VAR'('Heart'),=>(isa('$VAR'('Heart'),tHeart),hasOrgan('$VAR'('Human'),'$VAR'('Heart')))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Heart isa tHeart " is necessarily true
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( poss(~hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(isa(Heart,tHeart))=>nesc(hasOrgan(Human,Heart))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( ~( hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'( Heart,
      1,
      nesc(isa(Heart,tHeart))=>nesc(hasOrgan(Human,Heart)))) ==>
  poss( ~( isa(Heart,tHeart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(isa(Heart,tHeart))=>nesc(hasOrgan(Human,Heart))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is necessarily true )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'(Heart,1,nesc(isa(Heart,tHeart))=>nesc(hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    nesc( isa(Heart,tHeart))) ==>
  nesc( hasOrgan(Human,Heart))).

%~ kifi = all( Human,
%~          ( isa(Human,tAnimal) =>
%~            exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart)))).
%~ kifm = all( Human,
%~          nesc( ( isa(Human,tAnimal) =>
%~                  exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart))))).
passed=info(why_was_true(t123:test_boxlog(all(_656,isa(_656,tAnimal)=>exists(_660,isa(_660,tHeart)=>hasOrgan(_656,_660))))))
no_proof_for(test_boxlog(all(Human,isa(Human,tAnimal)=>exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart))))).

%~ kifi=all(Human,isa(Human,tAnimal)=>exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart)))
%~ kifm=all(Human,nesc(isa(Human,tAnimal)=>exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart))))
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Human'),necessary(=>(isa('$VAR'('Human'),tAnimal),exists('$VAR'('Heart'),=>(isa('$VAR'('Heart'),tHeart),hasOrgan('$VAR'('Human'),'$VAR'('Heart')))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Heart isa tHeart " is necessarily true
%~  It's Proof that:
%~    " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( poss(~hasOrgan(Human,Heart))&nesc(isa(Heart,tHeart)) ==>
  poss( ~( isa(Human,tAnimal)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    (" ?Human hasOrgan ?Heart " is possibly false  and
%~    " ?Human isa tAnimal " is necessarily true ) and
%~     by default ?Heart nesc(isa(Heart,tHeart))=>nesc(hasOrgan(Human,Heart))
%~  It's Proof that:
%~    " ?Heart isa tHeart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( ~( hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    '$existential'( Heart,
      1,
      nesc(isa(Heart,tHeart))=>nesc(hasOrgan(Human,Heart)))) ==>
  poss( ~( isa(Heart,tHeart)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~     by default ?Heart nesc(isa(Heart,tHeart))=>nesc(hasOrgan(Human,Heart))  and
%~    (" ?Human isa tAnimal " is necessarily true  and
%~    " ?Heart isa tHeart " is necessarily true )
%~  It's Proof that:
%~    " ?Human hasOrgan ?Heart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( '$existential'(Heart,1,nesc(isa(Heart,tHeart))=>nesc(hasOrgan(Human,Heart)))  &
    nesc( isa(Human,tAnimal)) &
    nesc( isa(Heart,tHeart))) ==>
  nesc( hasOrgan(Human,Heart))).

no_proof_for(test_boxlog(all(Human,isa(Human,tAnimal)=>exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart))))).

no_proof_for(test_boxlog(all(Human,isa(Human,tAnimal)=>exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart))))).

name='logicmoo.base.examples.fol.SANITY_EXISTS_02-Test_0005_Line_0000__TAnimal_in_t123'.
JUNIT_CLASSNAME='logicmoo.base.examples.fol.SANITY_EXISTS_02'.
JUNIT_CMD='timeout --foreground --preserve-status -s SIGKI
goal=t123:tHeart(_1158312).
time=0.00015234947204589844.
failure=failure=info((why_was_true(t123:(\+tHeart(_1098758))),nop(ftrace(t123:tHeart(_1098758)))))
no_proof_for(\+tHeart(Heart1)).

no_proof_for(\+tHeart(Heart1)).

no_proof_for(\+tHeart(Heart1)).

result=failure.