logicmoo_workspace
logicmoo_workspace copied to clipboard
Published
20 hours ago •
logicmoo
logicmoo
logicmoo.base.examples.fol.SANITY_ATLEAST_01 JUnit
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_atleast_01.pfc.pl']")
% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/sanity_atleast_01.pfc.pl % JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.examples.fol/SANITY_ATLEAST_01/ % ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3ASANITY_ATLEAST_01 % ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/439
%~ 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_atleast_01.pfc.pl'),
%~ 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:54 2021
% 1.267 seconds cpu time for 2,327,018 inferences
% 941,560 atoms, 32,345 functors, 31,565 predicates, 752 modules, 15,989,914 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 471,024 bytes in 0.000 seconds.
% 6 atom garbage collections gained 3,223 atoms in 0.095 seconds.
% 10 clause garbage collections gained 1,789 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]],atleast(1,[[Heart,tHeart]],hasOrgan(Human,Heart))))).
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/sanity_atleast_01.pfc.pl:26
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ test_boxlog(t121)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ make_dynamic_here( t123,
%~ '$nt'(
%~ wid( rule1 : 0,
%~ rule,
%~ all(
%~ [ [HasOrgan,tAnimal]],
%~ atleast(1,[[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)))
%~ kifi = all(
%~ [ [Human,tAnimal]],
%~ atleast(1,[[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(t121a, (atleast(1,[[Heart,tHeart]],all([[Human,tAnimal]],hasOrgan(Human,Heart))))).
/*~
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ test_boxlog(t121a)
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/sanity_atleast_01.pfc.pl:27
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ correct_special_quantifiers :- exists( Heart,
%~ ( all(Human,isa(Human,tAnimal)=>hasOrgan(Human,Heart)) &
%~ isa(Heart,tHeart))).
%~ %~ correct_special_quantifiers:-exists(Heart,all(Human,isa(Human,tAnimal)=>hasOrgan(Human,Heart))&isa(Heart,tHeart))
%~ kifi = atleast( 1,
%~ [ [Heart,tHeart]],
%~ all([[Human,tAnimal]],hasOrgan(Human,Heart))).
%~ kifm = exists( Heart,
%~ nesc( ( all(Human,isa(Human,tAnimal)=>hasOrgan(Human,Heart)) &
%~ isa(Heart,tHeart)))).
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Heart'),necessary(and(forall('$VAR'('Human'),=>(isa('$VAR'('Human'),tAnimal),hasOrgan('$VAR'('Human'),'$VAR'('Heart')))),isa('$VAR'('Heart'),tHeart))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Human hasOrgan ?Heart " is possibly false and
%~ " ?Human isa tAnimal " is necessarily true ) and
%~ by default ?Heart all(Human,nesc(isa(Human,tAnimal))=>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,
( all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart))) &
nesc( isa(Heart,tHeart))))) ==>
poss( ~( 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:
%~ by default ?Heart all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart)))&nesc(isa(Heart,tHeart)) and
%~ (" ?Heart isa tHeart " is necessarily true and
%~ " ?Human isa tAnimal " is necessarily true )
%~ It's Proof that:
%~ " ?Human hasOrgan ?Heart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( '$existential'( Heart,
1,
( all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart))) &
nesc( isa(Heart,tHeart)))) &
nesc( isa(Heart,tHeart)) &
nesc( isa(Human,tAnimal))) ==>
nesc( hasOrgan(Human,Heart))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Human hasOrgan ?Heart " is possibly false and
%~ " ?Human isa tAnimal " is possibly false )is possible ) and
%~ by default ?Heart all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart)))&nesc(isa(Heart,tHeart))
%~ It's Proof that:
%~ " ?Heart isa tHeart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( poss(~hasOrgan(Human,Heart))&poss(~isa(Human,tAnimal))) &
'$existential'( Heart,
1,
( all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart))) &
nesc( isa(Heart,tHeart))))) ==>
nesc( isa(Heart,tHeart))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ( by default ?Heart all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart)))&nesc(isa(Heart,tHeart)) and
%~ " ?Heart isa tHeart " is possibly false ) and
%~ " ?Human isa tAnimal " is possibly false
%~ It's Proof that:
%~ " ?Human hasOrgan ?Heart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( '$existential'( Heart,
1,
( all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart))) &
nesc( isa(Heart,tHeart)))) &
poss( ~( isa(Heart,tHeart))) &
poss( ~( isa(Human,tAnimal)))) ==>
nesc( hasOrgan(Human,Heart))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Human hasOrgan ?Heart " is possibly false and
%~ ( by default ?Heart all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart)))&nesc(isa(Heart,tHeart)) and
%~ " ?Heart isa tHeart " is possibly false )
%~ It's Proof that:
%~ " ?Human isa tAnimal " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( hasOrgan(Human,Heart))) &
'$existential'( Heart,
1,
( all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart))) &
nesc( isa(Heart,tHeart)))) &
poss( ~( isa(Heart,tHeart)))) ==>
nesc( isa(Human,tAnimal))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Human hasOrgan ?Heart " is necessarily true and
%~ " ?Human isa tAnimal " is necessarily true )is possible ) and
%~ by default ?Heart all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart)))&nesc(isa(Heart,tHeart))
%~ It's Proof that:
%~ " ?Heart isa tHeart " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( nesc(hasOrgan(Human,Heart))&nesc(isa(Human,tAnimal))) &
'$existential'( Heart,
1,
( all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart))) &
nesc( isa(Heart,tHeart))))) ==>
nesc( isa(Heart,tHeart))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ( by default ?Heart all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart)))&nesc(isa(Heart,tHeart)) and
%~ " ?Heart isa tHeart " is possibly false ) and
%~ " ?Human isa tAnimal " is possible
%~ It's Proof that:
%~ " ?Human hasOrgan ?Heart " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( '$existential'( Heart,
1,
( all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart))) &
nesc( isa(Heart,tHeart)))) &
poss( ~( isa(Heart,tHeart))) &
poss( isa(Human,tAnimal))) ==>
poss( ~( hasOrgan(Human,Heart)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Human hasOrgan ?Heart " is possible and
%~ ( by default ?Heart all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart)))&nesc(isa(Heart,tHeart)) and
%~ " ?Heart isa tHeart " is possibly false )
%~ It's Proof that:
%~ " ?Human isa tAnimal " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( hasOrgan(Human,Heart)) &
'$existential'( Heart,
1,
( all(Human,nesc(isa(Human,tAnimal))=>nesc(hasOrgan(Human,Heart))) &
nesc( isa(Heart,tHeart)))) &
poss( ~( isa(Heart,tHeart)))) ==>
poss( ~( isa(Human,tAnimal)))).
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ completed_test_boxlog(t121a)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
~*/
:- add_test(t122,
(all(Human,
isa(Human,tAnimal)
=> atleast(1,Heart,(isa(Heart,tHeart) & hasOrgan(Human,Heart)))))).
/*~
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/sanity_atleast_01.pfc.pl:32
%~ test_boxlog(t122)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ correct_special_quantifiers :- all( Human,
%~ =>( isa(Human,tAnimal),
%~ exists(Heart,isa(Heart,tHeart)&hasOrgan(Human,Heart)))).
%~ %~ correct_special_quantifiers:-all(Human,isa(Human,tAnimal)=>exists(Heart,isa(Heart,tHeart)&hasOrgan(Human,Heart)))
%~ kifi = all( Human,
%~ =>( isa(Human,tAnimal),
%~ atleast(1,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'),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(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(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(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(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(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(t122)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
~*/
:- add_test(t122a,
(atleast(1,Heart,
(all(Human,
isa(Human,tAnimal)
=> (isa(Heart,tHeart) & hasOrgan(Human,Heart))))))).
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/sanity_atleast_01.pfc.pl:38
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ test_boxlog(t122a)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ correct_special_quantifiers :- exists( Heart,
%~ all( Human,
%~ isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart)))).
%~ %~ correct_special_quantifiers:-exists(Heart,all(Human,isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart))))
%~ kifi = atleast( 1,
%~ Heart,
%~ all( Human,
%~ isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart)))).
%~ kifm = exists( Heart,
%~ all( Human,
%~ nesc( isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart))))).
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Heart'),forall('$VAR'('Human'),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 all(Human,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,
all( Human,
=>(
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 all(Human,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,
all( Human,
=>(
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 all(Human,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,
all( Human,
=>(
nesc( isa(Human,tAnimal)),
nesc(isa(Heart,tHeart))&nesc(hasOrgan(Human,Heart)))))) ==>
poss( ~( isa(Heart,tHeart)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Heart all(Human,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,
all( Human,
=>(
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(t122a)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
~*/
:- add_test(t123,
(all(Human,
atleast(1,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_atleast_01.pfc.pl:45
%~ test_boxlog(t123)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ correct_special_quantifiers :- all( Human,
%~ exists( Heart,
%~ isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart)))).
%~ %~ correct_special_quantifiers:-all(Human,exists(Heart,isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart))))
%~ kifi = all( Human,
%~ atleast( 1,
%~ 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(t123)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
~*/
:- add_test(t123a,
atleast(1,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_atleast_01.pfc.pl:50
%~ test_boxlog(t123a)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ correct_special_quantifiers :- exists( Heart,
%~ isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart))).
%~ %~ correct_special_quantifiers:-exists(Heart,isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart)))
%~ kifi = atleast( 1,
%~ Heart,
%~ isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart))).
%~ kifm = exists( Heart,
%~ nesc( isa(Human,tAnimal)=>(isa(Heart,tHeart)&hasOrgan(Human,Heart)))).
%~ kif_to_boxlog_attvars2 = 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(t123a)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
~*/
:- add_test(t124,
(all(Human,
isa(Human,tAnimal) =>
atleast(1, Heart, (isa(Heart,tHeart) => hasOrgan(Human,Heart)))))).
/*~
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ test_boxlog(t124)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ correct_special_quantifiers :- all( Human,
%~ =>( isa(Human,tAnimal),
%~ exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart)))).
%~ %~ correct_special_quantifiers:-all(Human,isa(Human,tAnimal)=>exists(Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart)))
%~ kifi = all( Human,
%~ =>( isa(Human,tAnimal),
%~ atleast(1,Heart,isa(Heart,tHeart)=>hasOrgan(Human,Heart)))).
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/sanity_atleast_01.pfc.pl:56
%~ 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(t124)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
~*/
:- add_test(t124a,
(atleast(1, Heart,
all(Human,
isa(Human,tAnimal) =>
(isa(Heart,tHeart) => hasOrgan(Human,Heart)))))).
/*~
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ test_boxlog(t124a)
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ message_hook_type(error)
%~ message_hook(
%~ error( syntax_error(operator_clash),
%~ string("wid(rule8:0,rule,atleast(1,Heart,all(Human,isa(Human,tAnimal)=>isa(Heart,tHeart)=>hasOrgan(Human,Heart)))) . ",62)),
%~ error,
%~ [ 'Syntax error: ', 'Operator priority clash',nl,
%~ '~w'-["wid(rule8:0,rule,atleast(1,Heart,all(Human,isa(Human,tAnimal)="], nl,'** here **',nl,
%~ '~w'-[">isa(Heart,tHeart)=>hasOrgan(Human,Heart)))) . "]])
Syntax error: Operator priority clash
wid(rule8:0,rule,atleast(1,Heart,all(Human,isa(Human,tAnimal)=
** here **
>isa(Heart,tHeart)=>hasOrgan(Human,Heart)))) .
ERROR: Syntax error: Operator priority clash
ERROR: wid(rule8:0,rule,atleast(1,Heart,all(Human,isa(Human,tAnimal)=
ERROR: ** here **
ERROR: >isa(Heart,tHeart)=>hasOrgan(Human,Heart)))) .
%~ message_hook_type(warning)
%~ message_hook(
%~ goal_failed( directive,
%~ t123 : add_test( t124a,
%~ atleast( 1,
%~ Heart,
%~ all( Human,
%~ isa(Human,tAnimal)=>isa(Heart,tHeart)=>hasOrgan(Human,Heart))))),
%~ warning,
%~ [ 'Goal (~w) failed: ~p' - [ directive,
%~ t123 : add_test( t124a,
%~ atleast( 1,
%~ Heart,
%~ all( Human,
%~ isa(Human,tAnimal)=>isa(Heart,tHeart)=>hasOrgan(Human,Heart))))]])
Goal (directive) failed: t123:add_test(t124a,atleast(1,_580,all(_582,isa(_582,tAnimal)=>isa(_580,tHeart)=>hasOrgan(_582,_580))))
Warning: Goal (directive) failed: t123:add_test(t124a,atleast(1,_580,all(_582,isa(_582,tAnimal)=>isa(_580,tHeart)=>hasOrgan(_582,_580))))
~*/
:- 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: 216 words .. **
** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/lex.xg: -256 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.75 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_atleast_01.pfc.pl:70
%~ '%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'.
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Human'),necessary(=>(isa('$VAR'('Human'),tAnimal),exists('$VAR'('Heart'),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(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(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(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(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(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_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(_37484))
passed=info(why_was_true(t123:(\+tHeart(_37484))))
no_proof_for(\+tHeart(Heart1)).
no_proof_for(\+tHeart(Heart1)).
no_proof_for(\+tHeart(Heart1)).
name = 'logicmoo.base.examples.fol.SANITY_ATLEAST_01-Test_0001_Line_0000__naf_tHeart_1_in_t123'.
JUNIT_CLASSNAME = 'logicmoo.base.examples.fol.SANITY_ATLEAST_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_atleast_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_ATLEAST_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).
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/sanity_atleast_01.pfc.pl:75
%~ ?-( mpred_test("Test_0002_Line_0000__tHeart_1_in_t123",t123:tHeart(Heart))).
failure=info((why_was_true(t123:(\+tHeart(_302466))),nop(ftrace(t123:tHeart(_302466)))))
no_proof_for(\+tHeart(Heart1)).
no_proof_for(\+tHeart(Heart1)).
no_proof_for(\+tHeart(Heart1)).
name = 'logicmoo.base.examples.fol.SANITY_ATLEAST_01-Test_0002_Line_0000__tHeart_1_in_t123'.
JUNIT_CLASSNAME = 'logicmoo.base.examples.fol.SANITY_ATLEAST_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_atleast_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_ATLEAST_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')).
/*~
%~ ?-( mpred_test("Test_0003_Line_0000__IBob_in_t123",t123:hasOrgan(iBob,HasOrgan_Bob))).
%~ make_dynamic_here(t123,hasOrgan(iBob,_931394))
failure=info((why_was_true(t123:(\+hasOrgan(iBob,_931394))),nop(ftrace(t123:hasOrgan(iBob,_931394)))))
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_ATLEAST_01-Test_0003_Line_0000__IBob_in_t123'.
JUNIT_CLASSNAME = 'logicmoo.base.examples.fol.SANITY_ATLEAST_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_atleast_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_ATLEAST_01_Test_0003_Line_0000_IBob_in_t123-junit.xml
~*/
%~ unused(no_junit_results)
logicmoo.base.examples.fol.SANITY_ATLEAST_01 JUnit error = Syntax error: Operator priority clash
wid(rule8:0,rule,atleast(1,Heart,all(Human,isa(Human,tAnimal)=
** here **
>isa(Heart,tHeart)=>hasOrgan(Human,Heart)))) .
logicmoo.base.examples.fol.SANITY_ATLEAST_01 JUnit warning = Goal (directive) failed: t123:add_test(t124a,atleast(1,_580,all(_582,isa(_582,tAnimal)=>isa(_580,tHeart)=>hasOrgan(_582,_580))))
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(56)
totalTime=6.000
FAILED: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k sanity_atleast_01.pfc.pl (returned 56) Add_LABELS='Errors,Warnings' Rem_LABELS='Skipped,Overtime,Skipped'
