logicmoo_workspace icon indicating copy to clipboard operation
logicmoo_workspace copied to clipboard

logicmoo.base.examples.fol.SANITY_EXISTS_01 JUnit

Open TeamSPoon opened this issue 4 years ago • 0 comments
trafficstars

(cd /var/lib/jenkins/workspace/logicmoo_workspace@2/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_01.pfc.pl']")

% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_01.pfc.pl % JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.examples.fol/SANITY_EXISTS_01/ % ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3ASANITY_EXISTS_01 % ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/436

%~ 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@2/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_01.pfc.pl'),
%~ /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test_header.pl:93 
%~ this_test_might_need( :-( use_module( library(logicmoo_plarkc))))

:- module(t123).   
/*~
~*/
   
:- '$set_source_module'(t123).

% :- process_this_script.

/*~
~*/


% :- process_this_script.

:- statistics.



/*~
% Started at Sat Sep 25 22:53:17 2021
% 1.275 seconds cpu time for 2,327,072 inferences
% 942,175 atoms, 32,345 functors, 31,566 predicates, 752 modules, 15,990,206 VM-codes
% 
%                     Limit   Allocated      In use
% Local  stack:           -       52 Kb    3,920  b
% Global stack:           -      256 Kb      101 Kb
% Trail  stack:           -       66 Kb      488  b
%        Total:    1,024 Mb      374 Kb      105 Kb
% 
% 5 garbage collections gained 472,088 bytes in 0.000 seconds.
% 5 atom garbage collections gained 2,616 atoms in 0.073 seconds.
% 9 clause garbage collections gained 1,745 clauses in 0.000 seconds.
% Stack shifts: 1 local, 2 global, 1 trail in 0.000 seconds
% 3 threads, 0 finished threads used 0.000 seconds
~*/




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

/*~
No source location!?
~*/


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

/*~
No source location!?
~*/


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


/*~
No source location!?
~*/



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

/*~


%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ test_boxlog(t121)


%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ make_dynamic_here( t123,
%~   '$nt'(
%~      wid( rule1 : 0,
%~        rule,
%~        all(
%~           [ [HasOrgan,tAnimal]],
%~           exists([[HasOrgan6,tHeart]],hasOrgan(HasOrgan,HasOrgan6)))), Wid,Nt))
%~ 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)))
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_01.pfc.pl:25 
%~ 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))).



%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ completed_test_boxlog(t121)


%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


~*/


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

/*~


%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_01.pfc.pl:31 
%~ test_boxlog(t122)


%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ 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))).



%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ completed_test_boxlog(t122)


%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


~*/


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

/*~


%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ test_boxlog(t123)


%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ kifi = all( Human,
%~          =>( isa(Human,tAnimal),
%~            exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart)))).
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_01.pfc.pl:34 
%~ 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))).



%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ completed_test_boxlog(t123)


%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


~*/


:- cls.

/*~
%~ skipped(messy_on_output,cls)
~*/


:- expects_dialect(pfc).

/*~
~*/


:- t122.

/*~
%   xgrun compiled into parser_chat80 0.00 sec, 0 clauses
%   xgproc compiled into parser_chat80 0.02 sec, 0 clauses


** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/clone.xg: 161 words .. **



** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/lex.xg: -218 words .. **

%  chatops compiled into parser_chat80 0.00 sec, 0 clauses
%  chatops compiled into parser_chat80 0.00 sec, 0 clauses
% :- share_mfa_pt2(parser_chat80,test_chat80,1).
% :- share_mfa_pt2(parser_chat80,hi80,0).
% :- share_mfa_pt2(parser_chat80,hi80,1).
% :- share_mfa_pt2(parser_chat80,control80,1).
% :- share_mfa_pt2(parser_chat80,trace_chat80,1).
%  /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/load compiled into parser_chat80 2.77 sec, 3 clauses
%  library(dif) compiled into dif 0.02 sec, 5 clauses
%  library(ctypes) compiled into ctypes 0.02 sec, 50 clauses
% /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/debuggery/dmsg compiled into dmsg 0.17 sec, -14 clauses


%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ running_test(t122)


%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_01.pfc.pl:40 
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ 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))).



%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


%~ completed_running_test(t122)


%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.


~*/


:- mpred_test(\+ tHeart(_)).
/*~
%~ ?-( mpred_test("Test_0001_Line_0000__naf_tHeart_1_in_t123",t123:(\+tHeart(Heart)))).
%~ make_dynamic_here(t123,tHeart(_64590))
passed=info(why_was_true(t123:(\+tHeart(_64590))))
no_proof_for(\+tHeart(Heart1)).

no_proof_for(\+tHeart(Heart1)).

no_proof_for(\+tHeart(Heart1)).

	name	=	'logicmoo.base.examples.fol.SANITY_EXISTS_01-Test_0001_Line_0000__naf_tHeart_1_in_t123'. 
	JUNIT_CLASSNAME	=	'logicmoo.base.examples.fol.SANITY_EXISTS_01'. 
	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_01.pfc.pl\']"'. 
% saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace@2/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_01_Test_0001_Line_0000_naf_tHeart_1_in_t123-junit.xml
~*/

:- ain(tAnimal(iBob)).

/*~
~*/


:- mpred_test(tHeart(_)).
% :- mpred_why(tHeart(skIsAnimalInHeartArg2ofHasorgan_1FnSk(iBob))).
% '' :-
%       \+ tHeart(skIsAnimalInHeartArg2ofHasorgan_1FnSk(iBob)).
% '' :-
%       tAnimal(iBob).
% '' :-
%       tAnimal(_32725602), (\+tHeart(skIsAnimalInHeartArg2ofHasorgan_1FnSk(_32725602));\+hasOrgan(_32725602, skIsAnimalInHeartArg2ofHasorgan_1FnSk(_32725602))), {_32725654=skIsAnimalInHeartArg2ofHasorgan_1FnSk(_32725602)}, {is_unit(_32725654)}==>tHeart(_32725654).
% '' :-
%       mfl(t123,
%           '/home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/sanity_exists_01.pl',
%           40).

/*~
%~ ?-( mpred_test("Test_0002_Line_0000__tHeart_1_in_t123",t123:tHeart(Heart))).
failure=info((why_was_true(t123:(\+tHeart(_215364))),nop(ftrace(t123:tHeart(_215364)))))
no_proof_for(\+tHeart(Heart1)).

no_proof_for(\+tHeart(Heart1)).

no_proof_for(\+tHeart(Heart1)).

	name	=	'logicmoo.base.examples.fol.SANITY_EXISTS_01-Test_0002_Line_0000__tHeart_1_in_t123'. 
	JUNIT_CLASSNAME	=	'logicmoo.base.examples.fol.SANITY_EXISTS_01'. 
	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_01.pfc.pl\']"'. 
% saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace@2/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_01_Test_0002_Line_0000_tHeart_1_in_t123-junit.xml
~*/

% :- mpred_why(tHeart(skIsAnimalInHeartArg2ofHasorgan_1FnSk(iBob))).
% '' :-
%       \+ tHeart(skIsAnimalInHeartArg2ofHasorgan_1FnSk(iBob)).
% '' :-
%       tAnimal(iBob).
% '' :-
%       tAnimal(_32725602), (\+tHeart(skIsAnimalInHeartArg2ofHasorgan_1FnSk(_32725602));\+hasOrgan(_32725602, skIsAnimalInHeartArg2ofHasorgan_1FnSk(_32725602))), {_32725654=skIsAnimalInHeartArg2ofHasorgan_1FnSk(_32725602)}, {is_unit(_32725654)}==>tHeart(_32725654).
% '' :-
%       mfl(t123,
%           '/home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/sanity_exists_01.pl',
%           40).

:- mpred_test(hasOrgan(iBob,_)).

% /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/sanity_exists_01.pl:45
% :- mpred_why(hasOrgan(iBob, skIsAnimalInHeartArg2ofHasorgan_1FnSk(iBob))).
% '' :-
%       \+ tHeart(skIsAnimalInHeartArg2ofHasorgan_1FnSk(iBob)).
% '' :-
%       tAnimal(iBob).
% '' :-
%       tAnimal(_32734660), (\+tHeart(skIsAnimalInHeartArg2ofHasorgan_1FnSk(_32734660));\+hasOrgan(_32734660, skIsAnimalInHeartArg2ofHasorgan_1FnSk(_32734660))), {_32734712=skIsAnimalInHeartArg2ofHasorgan_1FnSk(_32734660)}, {is_unit(_32734712, _32734660)}==>hasOrgan(_32734660, _32734712).
% '' :-
%       mfl(t123,
%           '/home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/sanity_exists_01.pl',
%           40).
% '' :-
%       \+ tHeart(skIsAnimalInHeartArg2ofHasorgan_1FnSk(iBob)).
% '' :-
%       tAnimal(iBob).
% '' :-
%       tAnimal(_32734522), {_32734536=skIsAnimalInHeartArg2ofHasorgan_1FnSk(_32734522)}, (\+tHeart(_32734536);\+hasOrgan(_32734522, _32734536)), {is_unit(_32734522)}==>hasOrgan(_32734522, skIsAnimalInHeartArg2ofHasorgan_1FnSk(_32734522)).
% '' :-
%       mfl(t123,
%           '/home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/sanity_exists_01.pl',
%           40).
% init_why(after('/home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/sanity_exists_01.pl')).




/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/sanity_exists_01.pfc.pl:58 
%~ ?-( mpred_test("Test_0003_Line_0000__IBob_in_t123",t123:hasOrgan(iBob,HasOrgan_Bob))).
%~ make_dynamic_here(t123,hasOrgan(iBob,_172502))
failure=info((why_was_true(t123:(\+hasOrgan(iBob,_172502))),nop(ftrace(t123:hasOrgan(iBob,_172502)))))
no_proof_for(\+hasOrgan(iBob,HasOrgan_Bob2)).

no_proof_for(\+hasOrgan(iBob,HasOrgan_Bob2)).

no_proof_for(\+hasOrgan(iBob,HasOrgan_Bob2)).

	name	=	'logicmoo.base.examples.fol.SANITY_EXISTS_01-Test_0003_Line_0000__IBob_in_t123'. 
	JUNIT_CLASSNAME	=	'logicmoo.base.examples.fol.SANITY_EXISTS_01'. 
	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_01.pfc.pl\']"'. 
% saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace@2/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_01_Test_0003_Line_0000_IBob_in_t123-junit.xml
~*/
%~ unused(no_junit_results)
Test_0001_Line_0000__naf_tHeart_1_in_t123	result	=	passed. 
Test_0002_Line_0000__tHeart_1_in_t123	result	=	failure. 
Test_0003_Line_0000__IBob_in_t123	result	=	failure. 

%~ test_completed_exit(8)

totalTime=5.000

FAILED: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k sanity_exists_01.pfc.pl (returned 8) Add_LABELS='' Rem_LABELS='Skipped,Skipped,Errors,Warnings,Overtime,Skipped'

TeamSPoon avatar Sep 18 '21 22:09 TeamSPoon