logicmoo_workspace
logicmoo_workspace copied to clipboard
Published
20 hours ago •
logicmoo
logicmoo
logicmoo.base.examples.fol.ZEBRA_05 JUnit
trafficstars
(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 "['zebra_05.clif']")
% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/zebra_05.clif % JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.examples.fol/ZEBRA_05/ % ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3AZEBRA_05 % ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/459
%~ init_phase(after_load)
%~ init_phase(restore_state)
%
%~ init_why(after_boot,program)
%~ after_boot.
%~ Dont forget to ?- logicmoo_i_cyc_xform.
%~ comment("; Module zebra5 - Test Zerbra Puzzle in CLIF for SWI-Prolog")
%~ comment("; Maintainer: Douglas Miles")
%~ comment("; Load with ?- load_clif(pack('logicmoo_base/t/examples/fol/zebra5.clif'))")
%~ comment("; causes deduction of argument types")
%~ debugm(common_logic_loader,show_success(common_logic_loader,common_logic_loader:maplist(zebra5:export,[])))
%~ error( missing_kif_process(call,zebra5:ensure_loaded(library(logicmoo_clif))))
%~ 'set-kif-option'('assume-wff')
t_l:kif_action_mode(tell)
%~ /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test_header.pl:30
%~ comment("; PROGRAM A")
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(livesIn,1,tHuman)))))
** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/clone.xg: -60 words .. **
** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/lex.xg: 143 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.49 sec, 1 clauses
% /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/debuggery/dmsg compiled into dmsg 0.12 sec, -16 clauses
=======================================================
domain(livesIn,1,tHuman)
============================================
?- kif_to_boxlog( domain(livesIn,1,tHuman) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(livesIn,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(livesIn,1,tHuman))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(livesIn,1,tHuman)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(livesIn,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(livesIn,1,tHuman)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(livesIn,2,tHouse)))))
=======================================================
domain(livesIn,2,tHouse)
============================================
?- kif_to_boxlog( domain(livesIn,2,tHouse) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(livesIn,2,tHouse)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(livesIn,2,tHouse))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(livesIn,2,tHouse)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(livesIn,2,tHouse)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(livesIn,2,tHouse)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(natOrigin,1,tHuman)))))
=======================================================
domain(natOrigin,1,tHuman)
============================================
?- kif_to_boxlog( domain(natOrigin,1,tHuman) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(natOrigin,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(natOrigin,1,tHuman))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(natOrigin,1,tHuman)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(natOrigin,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(natOrigin,1,tHuman)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(natOrigin,2,tCountry)))))
=======================================================
domain(natOrigin,2,tCountry)
============================================
?- kif_to_boxlog( domain(natOrigin,2,tCountry) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(natOrigin,2,tCountry)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(natOrigin,2,tCountry))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(natOrigin,2,tCountry)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(natOrigin,2,tCountry)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(natOrigin,2,tCountry)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(colorOf,1,tPhysical)))))
=======================================================
domain(colorOf,1,tPhysical)
============================================
?- kif_to_boxlog( domain(colorOf,1,tPhysical) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(colorOf,1,tPhysical)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(colorOf,1,tPhysical))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(colorOf,1,tPhysical)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(colorOf,1,tPhysical)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(colorOf,1,tPhysical)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(colorOf,2,vtColor)))))
=======================================================
domain(colorOf,2,vtColor)
============================================
?- kif_to_boxlog( domain(colorOf,2,vtColor) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(colorOf,2,vtColor)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(colorOf,2,vtColor))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(colorOf,2,vtColor)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(colorOf,2,vtColor)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(colorOf,2,vtColor)).
============================================
%~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/zebra_05.clif:333
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(address,1,tHouse)))))
=======================================================
domain(address,1,tHouse)
============================================
?- kif_to_boxlog( domain(address,1,tHouse) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(address,1,tHouse)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(address,1,tHouse))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(address,1,tHouse)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(address,1,tHouse)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(address,1,tHouse)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(address,2,tAddress)))))
=======================================================
domain(address,2,tAddress)
============================================
?- kif_to_boxlog( domain(address,2,tAddress) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(address,2,tAddress)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(address,2,tAddress))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(address,2,tAddress)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(address,2,tAddress)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(address,2,tAddress)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(argQuotedIsa(address,2,ftInt)))))
=======================================================
argQuotedIsa(address,2,ftInt)
============================================
?- kif_to_boxlog( argQuotedIsa(address,2,ftInt) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ argQuotedIsa(address,2,ftInt)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argQuotedIsa(address,2,ftInt))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argQuotedIsa(address,2,ftInt)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argQuotedIsa(address,2,ftInt)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argQuotedIsa(address,2,ftInt)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(caresFor,1,tHuman)))))
=======================================================
domain(caresFor,1,tHuman)
============================================
?- kif_to_boxlog( domain(caresFor,1,tHuman) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(caresFor,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(caresFor,1,tHuman))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(caresFor,1,tHuman)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(caresFor,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(caresFor,1,tHuman)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(caresFor,2,tAnimal)))))
=======================================================
domain(caresFor,2,tAnimal)
============================================
?- kif_to_boxlog( domain(caresFor,2,tAnimal) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(caresFor,2,tAnimal)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(caresFor,2,tAnimal))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(caresFor,2,tAnimal)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(caresFor,2,tAnimal)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(caresFor,2,tAnimal)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(subclass(tNonHumanAnimal,tAnimal)))))
=======================================================
subclass(tNonHumanAnimal,tAnimal)
============================================
?- kif_to_boxlog( subclass(tNonHumanAnimal,tAnimal) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ tNonHumanAnimal subclass tAnimal
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(genls(tNonHumanAnimal,tAnimal))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(genls(tNonHumanAnimal,tAnimal)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that tNonHumanAnimal genls tAnimal
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( genls(tNonHumanAnimal,tAnimal)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(subclass(tHuman,tAnimal)))))
=======================================================
subclass(tHuman,tAnimal)
============================================
?- kif_to_boxlog( subclass(tHuman,tAnimal) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ tHuman subclass tAnimal
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(genls(tHuman,tAnimal))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(genls(tHuman,tAnimal)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that tHuman genls tAnimal
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( genls(tHuman,tAnimal)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(disjointWith(tHuman,tNonHumanAnimal)))))
=======================================================
disjointWith(tHuman,tNonHumanAnimal)
============================================
?- kif_to_boxlog( disjointWith(tHuman,tNonHumanAnimal) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ tHuman disjointWith tNonHumanAnimal
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(disjointWith(tHuman,tNonHumanAnimal))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(disjointWith(tHuman,tNonHumanAnimal)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that tHuman disjointWith tNonHumanAnimal
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( disjointWith(tHuman,tNonHumanAnimal)).
============================================
%~ debugm(common_logic_loader,show_success(common_logic_loader,common_logic_loader:ain(clif(domain(drinks,1,tHuman)))))
=======================================================
domain(drinks,1,tHuman)
============================================
?- kif_to_boxlog( domain(drinks,1,tHuman) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(drinks,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(drinks,1,tHuman))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(drinks,1,tHuman)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(drinks,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(drinks,1,tHuman)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(drinks,2,tBeverage)))))
=======================================================
domain(drinks,2,tBeverage)
============================================
?- kif_to_boxlog( domain(drinks,2,tBeverage) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(drinks,2,tBeverage)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(drinks,2,tBeverage))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(drinks,2,tBeverage)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(drinks,2,tBeverage)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(drinks,2,tBeverage)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(typeGenls(ttBeverageType,tBeverage)))))
=======================================================
typeGenls(ttBeverageType,tBeverage)
============================================
?- kif_to_boxlog( typeGenls(ttBeverageType,tBeverage) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ ttBeverageType typeGenls tBeverage
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(typeGenls(ttBeverageType,tBeverage))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(typeGenls(ttBeverageType,tBeverage)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that ttBeverageType typeGenls tBeverage
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( typeGenls(ttBeverageType,tBeverage)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(instance(tCoffee,ttBeverageType)))))
=======================================================
instance(tCoffee,ttBeverageType)
============================================
?- kif_to_boxlog( instance(tCoffee,ttBeverageType) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ tCoffee instance ttBeverageType
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(ttBeverageType(tCoffee))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(ttBeverageType(tCoffee)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that tCoffee isa ttBeverageType
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( ttBeverageType(tCoffee)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(smokesBrand,1,tHuman)))))
=======================================================
domain(smokesBrand,1,tHuman)
============================================
?- kif_to_boxlog( domain(smokesBrand,1,tHuman) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(smokesBrand,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(smokesBrand,1,tHuman))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(smokesBrand,1,tHuman)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(smokesBrand,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(smokesBrand,1,tHuman)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(smokesBrand,2,tBrandName)))))
=======================================================
domain(smokesBrand,2,tBrandName)
============================================
?- kif_to_boxlog( domain(smokesBrand,2,tBrandName) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(smokesBrand,2,tBrandName)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(smokesBrand,2,tBrandName))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(smokesBrand,2,tBrandName)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(smokesBrand,2,tBrandName)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(smokesBrand,2,tBrandName)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(argQuotedIsa(smokesBrand,2,ftString)))))
=======================================================
argQuotedIsa(smokesBrand,2,ftString)
============================================
?- kif_to_boxlog( argQuotedIsa(smokesBrand,2,ftString) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ argQuotedIsa(smokesBrand,2,ftString)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argQuotedIsa(smokesBrand,2,ftString))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argQuotedIsa(smokesBrand,2,ftString)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argQuotedIsa(smokesBrand,2,ftString)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argQuotedIsa(smokesBrand,2,ftString)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domain(caresForType,1,tHuman)))))
=======================================================
domain(caresForType,1,tHuman)
============================================
?- kif_to_boxlog( domain(caresForType,1,tHuman) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domain(caresForType,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(caresForType,1,tHuman))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argIsa(caresForType,1,tHuman)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argIsa(caresForType,1,tHuman)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argIsa(caresForType,1,tHuman)).
============================================
%~ debugm( common_logic_loader,
%~ show_success(common_logic_loader,common_logic_loader:ain(clif(domainSubclass(caresForType,2,tAnimal)))))
=======================================================
domainSubclass(caresForType,2,tAnimal)
============================================
?- kif_to_boxlog( domainSubclass(caresForType,2,tAnimal) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ domainSubclass(caresForType,2,tAnimal)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argGenl(caresForType,2,tAnimal))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(argGenl(caresForType,2,tAnimal)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that argGenl(caresForType,2,tAnimal)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( argGenl(caresForType,2,tAnimal)).
============================================
%~ debugm( common_logic_loader,
%~ show_success( common_logic_loader,
%~ common_logic_loader : ain( clif( iff(
%~ and(caresForType(M1,T1),instance(P1,T1)),
%~ caresFor(M1,P1))))))
=======================================================
iff(and(caresForType('$VAR'('M1'),'$VAR'('T1')),instance('$VAR'('P1'),'$VAR'('T1'))),caresFor('$VAR'('M1'),'$VAR'('P1')))
============================================
?- kif_to_boxlog( iff(and(caresForType(M1,T1),instance(P1,T1)),caresFor(M1,P1)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ ?M1 caresForType ?T1 and ?P1 instance ?T1 iff ?M1 caresFor ?P1
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(<gt;=>(and(caresForType('$VAR'('M1'),'$VAR'('T1')),isa('$VAR'('P1'),'$VAR'('T1'))),caresFor('$VAR'('M1'),'$VAR'('P1'))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 25 entailment(s):
poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1))==>nesc(caresFor(M1,P1)).
poss(~caresFor(M1,P1))&poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))==>poss(~isa(P1,T1)).
poss(~caresFor(M1,P1))&poss(~caresFor(M1,P1))&nesc(isa(P1,T1))==>poss(~caresForType(M1,T1)).
poss(~caresFor(M1,P1))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>poss(~caresFor(M1,P1)).
poss(~caresForType(M1,T1))&poss(~caresFor(M1,P1))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>poss(~isa(P1,T1)).
poss(~caresForType(M1,T1))&((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>poss(~isa(P1,T1)).
poss(caresForType(M1,T1))&poss(~caresFor(M1,P1))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))==>nesc(isa(P1,T1)).
poss(caresForType(M1,T1))&((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))==>nesc(isa(P1,T1)).
(poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1)))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(poss(~isa(P1,T1)),nesc(isa(P1,T1)))==>nesc(caresForType(M1,T1)).
(poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1)))==>poss(~caresForType(M1,T1)).
(poss(~caresFor(M1,P1))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&poss(isa(P1,T1))==>nesc(caresForType(M1,T1)).
(poss(~caresFor(M1,P1))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1))))&poss(~isa(P1,T1))==>poss(~caresForType(M1,T1)).
(((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&poss(isa(P1,T1))==>nesc(caresForType(M1,T1)).
(((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1))))&poss(~isa(P1,T1))==>poss(~caresForType(M1,T1)).
((v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(poss(~isa(P1,T1)),nesc(isa(P1,T1)))==>nesc(caresForType(M1,T1)).
((v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1)))==>poss(~caresForType(M1,T1)).
((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1))==>nesc(caresFor(M1,P1)).
((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))==>poss(~isa(P1,T1)).
((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&poss(~caresFor(M1,P1))&nesc(isa(P1,T1))==>poss(~caresForType(M1,T1)).
((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>poss(~caresFor(M1,P1)).
(v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>nesc(caresFor(M1,P1)).
(v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))))&poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1))==>nesc(isa(P1,T1)).
(v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))))&(v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>nesc(isa(P1,T1)).
(v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1))==>poss(~isa(P1,T1)).
(v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&(v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>poss(~isa(P1,T1)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?M1 caresFor ?P1 " is possibly false and
%~ (" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is necessarily true )
%~ It's Proof that:
%~ " ?M1 caresFor ?P1 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( caresFor(M1,P1))) &
nesc( caresForType(M1,T1)) &
nesc( isa(P1,T1))) ==>
nesc( caresFor(M1,P1))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?M1 caresFor ?P1 " is possibly false and
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ " ?M1 caresForType ?T1 " is necessarily true )
%~ It's Proof that:
%~ " ?P1 isa ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( caresFor(M1,P1))) &
poss( ~( caresFor(M1,P1))) &
nesc( caresForType(M1,T1))) ==>
poss( ~( isa(P1,T1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?M1 caresFor ?P1 " is possibly false and
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )
%~ It's Proof that:
%~ " ?M1 caresForType ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( caresFor(M1,P1))) &
poss( ~( caresFor(M1,P1))) &
nesc( isa(P1,T1))) ==>
poss( ~( caresForType(M1,T1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?M1 caresFor ?P1 " is possibly false and
%~ (((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible ))
%~ It's Proof that:
%~ " ?M1 caresFor ?P1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( caresFor(M1,P1))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==>
poss( ~( caresFor(M1,P1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?M1 caresForType ?T1 " is possibly false and
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible ))))
%~ It's Proof that:
%~ " ?P1 isa ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( caresForType(M1,T1))) &
poss( ~( caresFor(M1,P1))) &
v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( nesc( caresFor(M1,P1)),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==>
poss( ~( isa(P1,T1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?M1 caresForType ?T1 " is possibly false and
%~ ((((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and
%~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and
%~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and
%~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible ))))
%~ It's Proof that:
%~ " ?P1 isa ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( caresForType(M1,T1))) &
v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( nesc( caresFor(M1,P1)),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==>
poss( ~( isa(P1,T1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?M1 caresForType ?T1 " is possible and
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true )))
%~ It's Proof that:
%~ " ?P1 isa ?T1 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( caresForType(M1,T1)) &
poss( ~( caresFor(M1,P1))) &
v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
nesc( caresFor(M1,P1)))) ==>
nesc( isa(P1,T1))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?M1 caresForType ?T1 " is possible and
%~ ((((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and
%~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and
%~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and
%~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true )))
%~ It's Proof that:
%~ " ?P1 isa ?T1 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( caresForType(M1,T1)) &
v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
nesc( caresFor(M1,P1)))) ==>
nesc( isa(P1,T1))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ (" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is necessarily true )) and
%~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and
%~ (" ?P1 isa ?T1 " is possibly false or " ?P1 isa ?T1 " is necessarily true ))
%~ It's Proof that:
%~ " ?M1 caresForType ?T1 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( caresFor(M1,P1))) &
nesc( caresForType(M1,T1)) &
nesc( isa(P1,T1)) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
v(poss(~isa(P1,T1)),nesc(isa(P1,T1)))) ==>
nesc( caresForType(M1,T1))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ (" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is necessarily true )) and
%~ ((" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false ) and
%~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))
%~ It's Proof that:
%~ " ?M1 caresForType ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( caresFor(M1,P1))) &
nesc( caresForType(M1,T1)) &
nesc( isa(P1,T1)) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
v(nesc(isa(P1,T1)),poss(~isa(P1,T1)))) ==>
poss( ~( caresForType(M1,T1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible )))) and
%~ " ?P1 isa ?T1 " is possible
%~ It's Proof that:
%~ " ?M1 caresForType ?T1 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( caresFor(M1,P1))) &
v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( nesc( caresFor(M1,P1)),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) &
poss( isa(P1,T1))) ==>
nesc( caresForType(M1,T1))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ))) and
%~ " ?P1 isa ?T1 " is possibly false
%~ It's Proof that:
%~ " ?M1 caresForType ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( caresFor(M1,P1))) &
v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
nesc( caresFor(M1,P1))) &
poss( ~( isa(P1,T1)))) ==>
poss( ~( caresForType(M1,T1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and
%~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and
%~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and
%~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible )))) and
%~ " ?P1 isa ?T1 " is possible
%~ It's Proof that:
%~ " ?M1 caresForType ?T1 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( nesc( caresFor(M1,P1)),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) &
poss( isa(P1,T1))) ==>
nesc( caresForType(M1,T1))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and
%~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and
%~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and
%~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ))) and
%~ " ?P1 isa ?T1 " is possibly false
%~ It's Proof that:
%~ " ?M1 caresForType ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
nesc( caresFor(M1,P1))) &
poss( ~( isa(P1,T1)))) ==>
poss( ~( caresForType(M1,T1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible ))) and
%~ ((((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible )))) and
%~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and
%~ (" ?P1 isa ?T1 " is possibly false or " ?P1 isa ?T1 " is necessarily true ))
%~ It's Proof that:
%~ " ?M1 caresForType ?T1 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( nesc( caresFor(M1,P1)),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
nesc( caresFor(M1,P1))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
v(poss(~isa(P1,T1)),nesc(isa(P1,T1)))) ==>
nesc( caresForType(M1,T1))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible ))) and
%~ ((((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible )))) and
%~ ((" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false ) and
%~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))
%~ It's Proof that:
%~ " ?M1 caresForType ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( nesc( caresFor(M1,P1)),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
nesc( caresFor(M1,P1))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
v(nesc(isa(P1,T1)),poss(~isa(P1,T1)))) ==>
poss( ~( caresForType(M1,T1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and
%~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and
%~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and
%~ (" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is necessarily true )
%~ It's Proof that:
%~ " ?M1 caresFor ?P1 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) &
nesc( caresForType(M1,T1)) &
nesc( isa(P1,T1))) ==>
nesc( caresFor(M1,P1))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and
%~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and
%~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ " ?M1 caresForType ?T1 " is necessarily true )
%~ It's Proof that:
%~ " ?P1 isa ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) &
poss( ~( caresFor(M1,P1))) &
nesc( caresForType(M1,T1))) ==>
poss( ~( isa(P1,T1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and
%~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and
%~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )
%~ It's Proof that:
%~ " ?M1 caresForType ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) &
poss( ~( caresFor(M1,P1))) &
nesc( isa(P1,T1))) ==>
poss( ~( caresForType(M1,T1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and
%~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and
%~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and
%~ (((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible ))
%~ It's Proof that:
%~ " ?M1 caresFor ?P1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==>
poss( ~( caresFor(M1,P1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible ))) and
%~ ((((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible )))
%~ It's Proof that:
%~ " ?M1 caresFor ?P1 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( nesc( caresFor(M1,P1)),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
nesc( caresFor(M1,P1))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==>
nesc( caresFor(M1,P1))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true )) and
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ (" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is necessarily true ))
%~ It's Proof that:
%~ " ?P1 isa ?T1 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
poss( ~( caresFor(M1,P1))) &
nesc( caresForType(M1,T1)) &
nesc( isa(P1,T1))) ==>
nesc( isa(P1,T1))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true )) and
%~ (((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible ))) and
%~ ((((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible ))))
%~ It's Proof that:
%~ " ?P1 isa ?T1 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) &
v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( nesc( caresFor(M1,P1)),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
nesc( caresFor(M1,P1))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==>
nesc( isa(P1,T1))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and
%~ (" ?M1 caresFor ?P1 " is possibly false and
%~ (" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is necessarily true ))
%~ It's Proof that:
%~ " ?P1 isa ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
poss( ~( caresFor(M1,P1))) &
nesc( caresForType(M1,T1)) &
nesc( isa(P1,T1))) ==>
poss( ~( isa(P1,T1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and
%~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and
%~ (((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible ))) and
%~ ((((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ) and
%~ (((" ?M1 caresForType ?T1 " is possibly false and
%~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and
%~ " ?P1 isa ?T1 " is possibly false )is possible ))))
%~ It's Proof that:
%~ " ?P1 isa ?T1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) &
v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) &
v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) &
v( nesc( caresFor(M1,P1)),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
nesc( caresFor(M1,P1))) &
v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),
poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==>
poss( ~( isa(P1,T1)))).
============================================
%~ kif_to_boxlog_attvars2 = necessary(<gt;=>(and(caresForType('$VAR'('M1'),'$VAR'('T1')),isa('$VAR'('P1'),'$VAR'('T1'))),caresFor('$VAR'('M1'),'$VAR'('P1'))))
totalTime=10.000
FAILED: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k zebra_05.clif (returned 137) Add_LABELS='Errors,Overtime' Rem_LABELS='Skipped,Skipped,Warnings,Skipped'
