logicmoo_workspace
logicmoo_workspace copied to clipboard
Published
20 hours ago •
logicmoo
logicmoo
logicmoo.base.examples.fol.EINSTEIN_SIMPLER_03 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 "['einstein_simpler_03.pfc.pl']")
% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_03.pfc.pl % JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.examples.fol/EINSTEIN_SIMPLER_03/ % ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3AEINSTEIN_SIMPLER_03 % ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/426
%~ 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/einstein_simpler_03.pfc.pl'),
%~ this_test_might_need( :-( use_module( library(logicmoo_plarkc))))
:- expects_dialect(pfc).
% :- module(baseKB).
/*~
~*/
% :- module(baseKB).
:- op(600,xfy, (/\)).
/*~
~*/
:- op(0,xfx,'=>').
/*~
~*/
:- op(1150,xfy,('=>')).
/*~
~*/
:- prolog_load_context(source,X),wdmsg(prolog_load_context(source,X)).
% reconsult((pack(logicmoo_base/t/examples/fol/'einstein_simpler_03.pfc'))).
/*~
%~ prolog_load_context(source,'* https://logicmoo.org:2082/gitlab/logicmoo/logicmoo_workspace/-/edit/master@2/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_03.pfc.pl ')
~*/
% reconsult((pack(logicmoo_base/t/examples/fol/'einstein_simpler_03.pfc'))).
never_assert_u(boxlog((lives(A, _):-neighbor(A, _))),singletons).
% add this to our vocab
/*~
~*/
% add this to our vocab
props((/\),ftSentenceOp,tLogicalConjunction).
/*~
~*/
:- set_kif_mode(tell).
% Source http://www.iflscience.com/editors-blog/solving-einsteins-riddle
/*~
t_l:kif_action_mode(tell)
~*/
% Source http://www.iflscience.com/editors-blog/solving-einsteins-riddle
:- expects_dialect(clif).
% Helper functional constraints
%
/*~
~*/
% Helper functional constraints
%
meta_argtypes(lives(person,house)).
/*~
~*/
meta_argtypes(keeps_as_pet(person,animal)).
/*~
~*/
meta_argtypes(position(person,int)).
/*~
~*/
meta_argtypes(smokes(person,brand)).
/*~
~*/
meta_argtypes(drinks(person,beverage)).
/*~
~*/
meta_argtypes(leftof(house,house)).
% Facts: https://udel.edu/~os/riddle.html
%
%= 1. The Brit lives in the red house.
/*~
~*/
% Facts: https://udel.edu/~os/riddle.html
%
%= 1. The Brit lives in the red house.
lives(englishman, red_house).
%= 2. The Swede keeps dogs as pets.
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_03.pfc.pl:83
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(lives(englishman,red_house)))))
% 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: 195 words .. **
** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/lex.xg: 110 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.53 sec, 3 clauses
% /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/debuggery/dmsg compiled into dmsg 0.13 sec, -16 clauses
=======================================================
lives(englishman,red_house)
============================================
?- kif_to_boxlog( lives(englishman,red_house) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ englishman lives red_house
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(lives(englishman,red_house))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(lives(englishman,red_house)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that englishman lives red_house
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( lives(englishman,red_house)).
============================================
~*/
%= 2. The Swede keeps dogs as pets.
keeps_as_pet(swede, dogs).
%= 3. The Dane drinks tea.
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_03.pfc.pl:86
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(keeps_as_pet(swede,dogs)))))
=======================================================
keeps_as_pet(swede,dogs)
============================================
?- kif_to_boxlog( keeps_as_pet(swede,dogs) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ swede keeps_as_pet dogs
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(keeps_as_pet(swede,dogs))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(keeps_as_pet(swede,dogs)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that swede keeps_as_pet dogs
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( keeps_as_pet(swede,dogs)).
============================================
~*/
%= 3. The Dane drinks tea.
drinks(dane, tea).
%= 4. The green house is on the immediate left of the white house.
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(drinks(dane,tea)))))
=======================================================
drinks(dane,tea)
============================================
?- kif_to_boxlog( drinks(dane,tea) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ dane drinks tea
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(drinks(dane,tea))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(drinks(dane,tea)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that dane drinks tea
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( drinks(dane,tea)).
============================================
~*/
%= 4. The green house is on the immediate left of the white house.
leftof(green_house, white_house).
%= 5. The green house's owner drinks coffee.
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(leftof(green_house,white_house)))))
=======================================================
leftof(green_house,white_house)
============================================
?- kif_to_boxlog( leftof(green_house,white_house) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ green_house leftof white_house
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(leftof(green_house,white_house))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(leftof(green_house,white_house)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that green_house leftof white_house
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( leftof(green_house,white_house)).
============================================
~*/
%= 5. The green house's owner drinks coffee.
exists(X, lives(X, green_house) /\ drinks(X, coffee)).
%= 6. The owner who smokes Pall Mall rears birds.
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_480,lives(_480,green_house)/\drinks(_480,coffee))))))
=======================================================
exists('$VAR'('Coffee_Green_house'),/\(lives('$VAR'('Coffee_Green_house'),green_house),drinks('$VAR'('Coffee_Green_house'),coffee)))
============================================
?- kif_to_boxlog( exists(Coffee_Green_house,lives(Coffee_Green_house,green_house)/\drinks(Coffee_Green_house,coffee)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Coffee_Green_house
%~ " ?Coffee_Green_house lives green_house /\ ?Coffee_Green_house drinks coffee "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Coffee_Green_house'),necessary(and(lives('$VAR'('Coffee_Green_house'),green_house),drinks('$VAR'('Coffee_Green_house'),coffee))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 4 entailment(s):
nesc(drinks(Coffee_Green_house,coffee))&'$existential'(Coffee_Green_house,1,nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee)))==>nesc(lives(Coffee_Green_house,green_house)).
nesc(lives(Coffee_Green_house,green_house))&'$existential'(Coffee_Green_house,1,nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee)))==>nesc(drinks(Coffee_Green_house,coffee)).
poss(~drinks(Coffee_Green_house,coffee))&'$existential'(Coffee_Green_house,1,nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee)))==>poss(~lives(Coffee_Green_house,green_house)).
poss(~lives(Coffee_Green_house,green_house))&'$existential'(Coffee_Green_house,1,nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee)))==>poss(~drinks(Coffee_Green_house,coffee)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Coffee_Green_house drinks coffee " is necessarily true and
%~ by default ?Coffee_Green_house nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee))
%~ It's Proof that:
%~ " ?Coffee_Green_house lives green_house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( drinks(Coffee_Green_house,coffee)) &
'$existential'( Coffee_Green_house,
1,
nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee)))) ==>
nesc( lives(Coffee_Green_house,green_house))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Coffee_Green_house lives green_house " is necessarily true and
%~ by default ?Coffee_Green_house nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee))
%~ It's Proof that:
%~ " ?Coffee_Green_house drinks coffee " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( lives(Coffee_Green_house,green_house)) &
'$existential'( Coffee_Green_house,
1,
nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee)))) ==>
nesc( drinks(Coffee_Green_house,coffee))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Coffee_Green_house drinks coffee " is possibly false and
%~ by default ?Coffee_Green_house nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee))
%~ It's Proof that:
%~ " ?Coffee_Green_house lives green_house " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( drinks(Coffee_Green_house,coffee))) &
'$existential'( Coffee_Green_house,
1,
nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee)))) ==>
poss( ~( lives(Coffee_Green_house,green_house)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Coffee_Green_house lives green_house " is possibly false and
%~ by default ?Coffee_Green_house nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee))
%~ It's Proof that:
%~ " ?Coffee_Green_house drinks coffee " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( lives(Coffee_Green_house,green_house))) &
'$existential'( Coffee_Green_house,
1,
nesc(lives(Coffee_Green_house,green_house))&nesc(drinks(Coffee_Green_house,coffee)))) ==>
poss( ~( drinks(Coffee_Green_house,coffee)))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),necessary(and(lives('$VAR'('X'),green_house),drinks('$VAR'('X'),coffee))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X lives green_house " is possibly false and
%~ by default ?X nesc(lives(X,green_house))&nesc(drinks(X,coffee))
%~ It's Proof that:
%~ " ?X drinks coffee " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( lives(X,green_house))) &
'$existential'(X,1,nesc(lives(X,green_house))&nesc(drinks(X,coffee)))) ==>
poss( ~( drinks(X,coffee)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X drinks coffee " is necessarily true and
%~ by default ?X nesc(lives(X,green_house))&nesc(drinks(X,coffee))
%~ It's Proof that:
%~ " ?X lives green_house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( drinks(X,coffee)) &
'$existential'(X,1,nesc(lives(X,green_house))&nesc(drinks(X,coffee)))) ==>
nesc( lives(X,green_house))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X drinks coffee " is possibly false and
%~ by default ?X nesc(lives(X,green_house))&nesc(drinks(X,coffee))
%~ It's Proof that:
%~ " ?X lives green_house " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( drinks(X,coffee))) &
'$existential'(X,1,nesc(lives(X,green_house))&nesc(drinks(X,coffee)))) ==>
poss( ~( lives(X,green_house)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X lives green_house " is necessarily true and
%~ by default ?X nesc(lives(X,green_house))&nesc(drinks(X,coffee))
%~ It's Proof that:
%~ " ?X drinks coffee " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( lives(X,green_house)) &
'$existential'(X,1,nesc(lives(X,green_house))&nesc(drinks(X,coffee)))) ==>
nesc( drinks(X,coffee))).
~*/
%= 6. The owner who smokes Pall Mall rears birds.
exists(X, smokes(X, pallmalls) /\ keeps_as_pet(X, birds)).
%= 7. The owner of the yellow house smokes Dunhill.
/*~
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( exists(X,smokes(X,pallmalls)/\keeps_as_pet(X,birds))))))
=======================================================
exists('$VAR'('Birds_Pallmalls'),/\(smokes('$VAR'('Birds_Pallmalls'),pallmalls),keeps_as_pet('$VAR'('Birds_Pallmalls'),birds)))
============================================
?- kif_to_boxlog( exists(Birds_Pallmalls,smokes(Birds_Pallmalls,pallmalls)/\keeps_as_pet(Birds_Pallmalls,birds)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Birds_Pallmalls
%~ " ?Birds_Pallmalls smokes pallmalls /\ ?Birds_Pallmalls keeps_as_pet birds "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Birds_Pallmalls'),necessary(and(smokes('$VAR'('Birds_Pallmalls'),pallmalls),keeps_as_pet('$VAR'('Birds_Pallmalls'),birds))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 4 entailment(s):
nesc(keeps_as_pet(Birds_Pallmalls,birds))&'$existential'(Birds_Pallmalls,1,nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds)))==>nesc(smokes(Birds_Pallmalls,pallmalls)).
nesc(smokes(Birds_Pallmalls,pallmalls))&'$existential'(Birds_Pallmalls,1,nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds)))==>nesc(keeps_as_pet(Birds_Pallmalls,birds)).
poss(~keeps_as_pet(Birds_Pallmalls,birds))&'$existential'(Birds_Pallmalls,1,nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds)))==>poss(~smokes(Birds_Pallmalls,pallmalls)).
poss(~smokes(Birds_Pallmalls,pallmalls))&'$existential'(Birds_Pallmalls,1,nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds)))==>poss(~keeps_as_pet(Birds_Pallmalls,birds)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Birds_Pallmalls keeps_as_pet birds " is necessarily true and
%~ by default ?Birds_Pallmalls nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds))
%~ It's Proof that:
%~ " ?Birds_Pallmalls smokes pallmalls " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(Birds_Pallmalls,birds)) &
'$existential'( Birds_Pallmalls,
1,
nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds)))) ==>
nesc( smokes(Birds_Pallmalls,pallmalls))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Birds_Pallmalls smokes pallmalls " is necessarily true and
%~ by default ?Birds_Pallmalls nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds))
%~ It's Proof that:
%~ " ?Birds_Pallmalls keeps_as_pet birds " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Birds_Pallmalls,pallmalls)) &
'$existential'( Birds_Pallmalls,
1,
nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds)))) ==>
nesc( keeps_as_pet(Birds_Pallmalls,birds))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Birds_Pallmalls keeps_as_pet birds " is possibly false and
%~ by default ?Birds_Pallmalls nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds))
%~ It's Proof that:
%~ " ?Birds_Pallmalls smokes pallmalls " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( keeps_as_pet(Birds_Pallmalls,birds))) &
'$existential'( Birds_Pallmalls,
1,
nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds)))) ==>
poss( ~( smokes(Birds_Pallmalls,pallmalls)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Birds_Pallmalls smokes pallmalls " is possibly false and
%~ by default ?Birds_Pallmalls nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds))
%~ It's Proof that:
%~ " ?Birds_Pallmalls keeps_as_pet birds " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( smokes(Birds_Pallmalls,pallmalls))) &
'$existential'( Birds_Pallmalls,
1,
nesc(smokes(Birds_Pallmalls,pallmalls))&nesc(keeps_as_pet(Birds_Pallmalls,birds)))) ==>
poss( ~( keeps_as_pet(Birds_Pallmalls,birds)))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),necessary(and(smokes('$VAR'('X'),pallmalls),keeps_as_pet('$VAR'('X'),birds))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X smokes pallmalls " is possibly false and
%~ by default ?X nesc(smokes(X,pallmalls))&nesc(keeps_as_pet(X,birds))
%~ It's Proof that:
%~ " ?X keeps_as_pet birds " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( smokes(X,pallmalls))) &
'$existential'(X,1,nesc(smokes(X,pallmalls))&nesc(keeps_as_pet(X,birds)))) ==>
poss( ~( keeps_as_pet(X,birds)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X keeps_as_pet birds " is necessarily true and
%~ by default ?X nesc(smokes(X,pallmalls))&nesc(keeps_as_pet(X,birds))
%~ It's Proof that:
%~ " ?X smokes pallmalls " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(X,birds)) &
'$existential'(X,1,nesc(smokes(X,pallmalls))&nesc(keeps_as_pet(X,birds)))) ==>
nesc( smokes(X,pallmalls))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X keeps_as_pet birds " is possibly false and
%~ by default ?X nesc(smokes(X,pallmalls))&nesc(keeps_as_pet(X,birds))
%~ It's Proof that:
%~ " ?X smokes pallmalls " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( keeps_as_pet(X,birds))) &
'$existential'(X,1,nesc(smokes(X,pallmalls))&nesc(keeps_as_pet(X,birds)))) ==>
poss( ~( smokes(X,pallmalls)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X smokes pallmalls " is necessarily true and
%~ by default ?X nesc(smokes(X,pallmalls))&nesc(keeps_as_pet(X,birds))
%~ It's Proof that:
%~ " ?X keeps_as_pet birds " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(X,pallmalls)) &
'$existential'(X,1,nesc(smokes(X,pallmalls))&nesc(keeps_as_pet(X,birds)))) ==>
nesc( keeps_as_pet(X,birds))).
~*/
%= 7. The owner of the yellow house smokes Dunhill.
exists(X, lives(X, yellow_house) /\ smokes(X, dunhills)).
%= 8. The owner living in the center house drinks milk.
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_03.pfc.pl:101
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( exists(X,lives(X,yellow_house)/\smokes(X,dunhills))))))
=======================================================
exists('$VAR'('Dunhills_Yellow_house'),/\(lives('$VAR'('Dunhills_Yellow_house'),yellow_house),smokes('$VAR'('Dunhills_Yellow_house'),dunhills)))
============================================
?- kif_to_boxlog( exists(Dunhills_Yellow_house,lives(Dunhills_Yellow_house,yellow_house)/\smokes(Dunhills_Yellow_house,dunhills)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Dunhills_Yellow_house
%~ " ?Dunhills_Yellow_house lives yellow_house /\ ?Dunhills_Yellow_house smokes dunhills "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Dunhills_Yellow_house'),necessary(and(lives('$VAR'('Dunhills_Yellow_house'),yellow_house),smokes('$VAR'('Dunhills_Yellow_house'),dunhills))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 4 entailment(s):
nesc(lives(Dunhills_Yellow_house,yellow_house))&'$existential'(Dunhills_Yellow_house,1,nesc(lives(Dunhills_Yellow_house,yellow_house))&nesc(smokes(Dunhills_Yellow_house,dunhills)))==>nesc(smokes(Dunhills_Yellow_house,dunhills)).
nesc(smokes(Dunhills_Yellow_house,dunhills))&'$existential'(Dunhills_Yellow_house,1,nesc(lives(Dunhills_Yellow_house,yellow_house))&nesc(smokes(Dunhills_Yellow_house,dunhills)))==>nesc(lives(Dunhills_Yellow_house,yellow_house)).
poss(~lives(Dunhills_Yellow_house,yellow_house))&'$existential'(Dunhills_Yellow_house,1,nesc(lives(Dunhills_Yellow_house,yellow_house))&nesc(smokes(Dunhills_Yellow_house,dunhills)))==>poss(~smokes(Dunhills_Yellow_house,dunhills)).
poss(~smokes(Dunhills_Yellow_house,dunhills))&'$existential'(Dunhills_Yellow_house,1,nesc(lives(Dunhills_Yellow_house,yellow_house))&nesc(smokes(Dunhills_Yellow_house,dunhills)))==>poss(~lives(Dunhills_Yellow_house,yellow_house)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Dunhills_Yellow_house lives yellow_house " is necessarily true and
%~ by default ?Dunhills_Yellow_house nesc(lives(Dunhills_Yellow_house,yellow_house))&nesc(smokes(Dunhills_Yellow_house,dunhills))
%~ It's Proof that:
%~ " ?Dunhills_Yellow_house smokes dunhills " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( lives(Dunhills_Yellow_house,yellow_house)) &
'$existential'( Dunhills_Yellow_house,
1,
( nesc( lives(Dunhills_Yellow_house,yellow_house)) &
nesc( smokes(Dunhills_Yellow_house,dunhills))))) ==>
nesc( smokes(Dunhills_Yellow_house,dunhills))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Dunhills_Yellow_house smokes dunhills " is necessarily true and
%~ by default ?Dunhills_Yellow_house nesc(lives(Dunhills_Yellow_house,yellow_house))&nesc(smokes(Dunhills_Yellow_house,dunhills))
%~ It's Proof that:
%~ " ?Dunhills_Yellow_house lives yellow_house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Dunhills_Yellow_house,dunhills)) &
'$existential'( Dunhills_Yellow_house,
1,
( nesc( lives(Dunhills_Yellow_house,yellow_house)) &
nesc( smokes(Dunhills_Yellow_house,dunhills))))) ==>
nesc( lives(Dunhills_Yellow_house,yellow_house))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Dunhills_Yellow_house lives yellow_house " is possibly false and
%~ by default ?Dunhills_Yellow_house nesc(lives(Dunhills_Yellow_house,yellow_house))&nesc(smokes(Dunhills_Yellow_house,dunhills))
%~ It's Proof that:
%~ " ?Dunhills_Yellow_house smokes dunhills " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( lives(Dunhills_Yellow_house,yellow_house))) &
'$existential'( Dunhills_Yellow_house,
1,
( nesc( lives(Dunhills_Yellow_house,yellow_house)) &
nesc( smokes(Dunhills_Yellow_house,dunhills))))) ==>
poss( ~( smokes(Dunhills_Yellow_house,dunhills)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Dunhills_Yellow_house smokes dunhills " is possibly false and
%~ by default ?Dunhills_Yellow_house nesc(lives(Dunhills_Yellow_house,yellow_house))&nesc(smokes(Dunhills_Yellow_house,dunhills))
%~ It's Proof that:
%~ " ?Dunhills_Yellow_house lives yellow_house " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( smokes(Dunhills_Yellow_house,dunhills))) &
'$existential'( Dunhills_Yellow_house,
1,
( nesc( lives(Dunhills_Yellow_house,yellow_house)) &
nesc( smokes(Dunhills_Yellow_house,dunhills))))) ==>
poss( ~( lives(Dunhills_Yellow_house,yellow_house)))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),necessary(and(lives('$VAR'('X'),yellow_house),smokes('$VAR'('X'),dunhills))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X lives yellow_house " is possibly false and
%~ by default ?X nesc(lives(X,yellow_house))&nesc(smokes(X,dunhills))
%~ It's Proof that:
%~ " ?X smokes dunhills " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( lives(X,yellow_house))) &
'$existential'(X,1,nesc(lives(X,yellow_house))&nesc(smokes(X,dunhills)))) ==>
poss( ~( smokes(X,dunhills)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X smokes dunhills " is necessarily true and
%~ by default ?X nesc(lives(X,yellow_house))&nesc(smokes(X,dunhills))
%~ It's Proof that:
%~ " ?X lives yellow_house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(X,dunhills)) &
'$existential'(X,1,nesc(lives(X,yellow_house))&nesc(smokes(X,dunhills)))) ==>
nesc( lives(X,yellow_house))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X smokes dunhills " is possibly false and
%~ by default ?X nesc(lives(X,yellow_house))&nesc(smokes(X,dunhills))
%~ It's Proof that:
%~ " ?X lives yellow_house " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( smokes(X,dunhills))) &
'$existential'(X,1,nesc(lives(X,yellow_house))&nesc(smokes(X,dunhills)))) ==>
poss( ~( lives(X,yellow_house)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X lives yellow_house " is necessarily true and
%~ by default ?X nesc(lives(X,yellow_house))&nesc(smokes(X,dunhills))
%~ It's Proof that:
%~ " ?X smokes dunhills " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( lives(X,yellow_house)) &
'$existential'(X,1,nesc(lives(X,yellow_house))&nesc(smokes(X,dunhills)))) ==>
nesc( smokes(X,dunhills))).
~*/
%= 8. The owner living in the center house drinks milk.
exists(X, position(X, 3) /\ drinks(X, milk)).
%= 9. The Norwegian lives in the first house.
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_46624,position(_46624,3)/\drinks(_46624,milk))))))
=======================================================
exists('$VAR'('Milk'),/\(position('$VAR'('Milk'),3),drinks('$VAR'('Milk'),milk)))
============================================
?- kif_to_boxlog( exists(Milk,position(Milk,3)/\drinks(Milk,milk)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Milk
%~ " ?Milk position 3 /\ ?Milk drinks milk "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Milk'),necessary(and(position('$VAR'('Milk'),3),drinks('$VAR'('Milk'),milk))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 4 entailment(s):
nesc(drinks(Milk,milk))&'$existential'(Milk,1,nesc(position(Milk,3))&nesc(drinks(Milk,milk)))==>nesc(position(Milk,3)).
nesc(position(Milk,3))&'$existential'(Milk,1,nesc(position(Milk,3))&nesc(drinks(Milk,milk)))==>nesc(drinks(Milk,milk)).
poss(~drinks(Milk,milk))&'$existential'(Milk,1,nesc(position(Milk,3))&nesc(drinks(Milk,milk)))==>poss(~position(Milk,3)).
poss(~position(Milk,3))&'$existential'(Milk,1,nesc(position(Milk,3))&nesc(drinks(Milk,milk)))==>poss(~drinks(Milk,milk)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Milk drinks milk " is necessarily true and
%~ by default ?Milk nesc(position(Milk,3))&nesc(drinks(Milk,milk))
%~ It's Proof that:
%~ " ?Milk position 3 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( drinks(Milk,milk)) &
'$existential'(Milk,1,nesc(position(Milk,3))&nesc(drinks(Milk,milk)))) ==>
nesc( position(Milk,3))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Milk position 3 " is necessarily true and
%~ by default ?Milk nesc(position(Milk,3))&nesc(drinks(Milk,milk))
%~ It's Proof that:
%~ " ?Milk drinks milk " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( position(Milk,3)) &
'$existential'(Milk,1,nesc(position(Milk,3))&nesc(drinks(Milk,milk)))) ==>
nesc( drinks(Milk,milk))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Milk drinks milk " is possibly false and
%~ by default ?Milk nesc(position(Milk,3))&nesc(drinks(Milk,milk))
%~ It's Proof that:
%~ " ?Milk position 3 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( drinks(Milk,milk))) &
'$existential'(Milk,1,nesc(position(Milk,3))&nesc(drinks(Milk,milk)))) ==>
poss( ~( position(Milk,3)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Milk position 3 " is possibly false and
%~ by default ?Milk nesc(position(Milk,3))&nesc(drinks(Milk,milk))
%~ It's Proof that:
%~ " ?Milk drinks milk " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( position(Milk,3))) &
'$existential'(Milk,1,nesc(position(Milk,3))&nesc(drinks(Milk,milk)))) ==>
poss( ~( drinks(Milk,milk)))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),necessary(and(position('$VAR'('X'),3),drinks('$VAR'('X'),milk))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X position 3 " is possibly false and
%~ by default ?X nesc(position(X,3))&nesc(drinks(X,milk))
%~ It's Proof that:
%~ " ?X drinks milk " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( position(X,3))) &
'$existential'(X,1,nesc(position(X,3))&nesc(drinks(X,milk)))) ==>
poss( ~( drinks(X,milk)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X drinks milk " is necessarily true and
%~ by default ?X nesc(position(X,3))&nesc(drinks(X,milk))
%~ It's Proof that:
%~ " ?X position 3 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( drinks(X,milk)) &
'$existential'(X,1,nesc(position(X,3))&nesc(drinks(X,milk)))) ==>
nesc( position(X,3))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X drinks milk " is possibly false and
%~ by default ?X nesc(position(X,3))&nesc(drinks(X,milk))
%~ It's Proof that:
%~ " ?X position 3 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( drinks(X,milk))) &
'$existential'(X,1,nesc(position(X,3))&nesc(drinks(X,milk)))) ==>
poss( ~( position(X,3)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X position 3 " is necessarily true and
%~ by default ?X nesc(position(X,3))&nesc(drinks(X,milk))
%~ It's Proof that:
%~ " ?X drinks milk " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( position(X,3)) &
'$existential'(X,1,nesc(position(X,3))&nesc(drinks(X,milk)))) ==>
nesc( drinks(X,milk))).
~*/
%= 9. The Norwegian lives in the first house.
position(norwegian, 1).
%= 10. The owner who smokes Blends lives next to the one who keeps cats.
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(position(norwegian,1)))))
=======================================================
position(norwegian,1)
============================================
?- kif_to_boxlog( position(norwegian,1) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ norwegian position 1
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(position(norwegian,1))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(position(norwegian,1)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that norwegian position 1
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( position(norwegian,1)).
============================================
~*/
%= 10. The owner who smokes Blends lives next to the one who keeps cats.
exists(X,exists(Y, smokes(X, blend) /\ neighbor(X, Y) /\ keeps_as_pet(Y, cat))).
%= 11. The owner who keeps the horse lives next to the one who smokes Dunhill.
/*~
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( exists( X,
%~ exists(Y,smokes(X,blend)/\(neighbor(X,Y)/\keeps_as_pet(Y,cat))))))))
=======================================================
exists('$VAR'('Exists_Blend'),exists('$VAR'('Neighbor_Cat'),/\(smokes('$VAR'('Exists_Blend'),blend),/\(neighbor('$VAR'('Exists_Blend'),'$VAR'('Neighbor_Cat')),keeps_as_pet('$VAR'('Neighbor_Cat'),cat)))))
============================================
?- kif_to_boxlog( exists(Exists_Blend,exists(Neighbor_Cat,smokes(Exists_Blend,blend)/\(neighbor(Exists_Blend,Neighbor_Cat)/\keeps_as_pet(Neighbor_Cat,cat)))) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Exists_Blend
%~ (
%~ There exists ?Neighbor_Cat
%~ " ?Exists_Blend smokes blend /\ ?Exists_Blend neighbor ?Neighbor_Cat /\ ?Neighbor_Cat keeps_as_pet cat " )
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Exists_Blend'),exists('$VAR'('Neighbor_Cat'),necessary(and(smokes('$VAR'('Exists_Blend'),blend),and(neighbor('$VAR'('Exists_Blend'),'$VAR'('Neighbor_Cat')),keeps_as_pet('$VAR'('Neighbor_Cat'),cat))))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 9 entailment(s):
poss(keeps_as_pet(Neighbor_Cat,cat))&(poss(~smokes(Exists_Blend,blend))&'$existential'(Exists_Blend,1,exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))))&'$existential'(Neighbor_Cat,1,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))==>poss(~neighbor(Exists_Blend,Neighbor_Cat)).
poss(neighbor(Exists_Blend,Neighbor_Cat))&(poss(~smokes(Exists_Blend,blend))&'$existential'(Exists_Blend,1,exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))))&'$existential'(Neighbor_Cat,1,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))==>poss(~keeps_as_pet(Neighbor_Cat,cat)).
(nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat)))&'$existential'(Neighbor_Cat,1,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))==>nesc(keeps_as_pet(Neighbor_Cat,cat)).
(nesc(smokes(Exists_Blend,blend))&poss(~neighbor(Exists_Blend,Neighbor_Cat)))&'$existential'(Neighbor_Cat,1,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))==>poss(~keeps_as_pet(Neighbor_Cat,cat)).
(poss(nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))&'$existential'(Exists_Blend,1,exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))))&'$existential'(Neighbor_Cat,1,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))==>nesc(smokes(Exists_Blend,blend)).
((nesc(keeps_as_pet(Neighbor_Cat,cat))&poss(~neighbor(Exists_Blend,Neighbor_Cat)))&'$existential'(Exists_Blend,1,exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))))&'$existential'(Neighbor_Cat,1,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))==>poss(~smokes(Exists_Blend,blend)).
((nesc(neighbor(Exists_Blend,Neighbor_Cat))&poss(~keeps_as_pet(Neighbor_Cat,cat)))&'$existential'(Exists_Blend,1,exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))))&'$existential'(Neighbor_Cat,1,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))==>poss(~smokes(Exists_Blend,blend)).
((nesc(smokes(Exists_Blend,blend))&nesc(keeps_as_pet(Neighbor_Cat,cat)))&'$existential'(Exists_Blend,1,exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))))&'$existential'(Neighbor_Cat,1,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))==>nesc(neighbor(Exists_Blend,Neighbor_Cat)).
((nesc(smokes(Exists_Blend,blend))&poss(~keeps_as_pet(Neighbor_Cat,cat)))&'$existential'(Exists_Blend,1,exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))))&'$existential'(Neighbor_Cat,1,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)))==>poss(~neighbor(Exists_Blend,Neighbor_Cat)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Neighbor_Cat keeps_as_pet cat " is possible and
%~ ((" ?Exists_Blend smokes blend " is possibly false and
%~ by default ?Exists_Blend exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))) ) and
%~ by default ?Neighbor_Cat nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)) )
%~ It's Proof that:
%~ " ?Exists_Blend neighbor ?Neighbor_Cat " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( keeps_as_pet(Neighbor_Cat,cat)) &
poss( ~( smokes(Exists_Blend,blend))) &
'$existential'( Exists_Blend,
1,
exists( Neighbor_Cat,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) &
'$existential'( Neighbor_Cat,
1,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) ==>
poss( ~( neighbor(Exists_Blend,Neighbor_Cat)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Exists_Blend neighbor ?Neighbor_Cat " is possible and
%~ ((" ?Exists_Blend smokes blend " is possibly false and
%~ by default ?Exists_Blend exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))) ) and
%~ by default ?Neighbor_Cat nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat)) )
%~ It's Proof that:
%~ " ?Neighbor_Cat keeps_as_pet cat " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( neighbor(Exists_Blend,Neighbor_Cat)) &
poss( ~( smokes(Exists_Blend,blend))) &
'$existential'( Exists_Blend,
1,
exists( Neighbor_Cat,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) &
'$existential'( Neighbor_Cat,
1,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) ==>
poss( ~( keeps_as_pet(Neighbor_Cat,cat)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Exists_Blend smokes blend " is necessarily true and
%~ " ?Exists_Blend neighbor ?Neighbor_Cat " is necessarily true ) and
%~ by default ?Neighbor_Cat nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))
%~ It's Proof that:
%~ " ?Neighbor_Cat keeps_as_pet cat " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
'$existential'( Neighbor_Cat,
1,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) ==>
nesc( keeps_as_pet(Neighbor_Cat,cat))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Exists_Blend smokes blend " is necessarily true and
%~ " ?Exists_Blend neighbor ?Neighbor_Cat " is possibly false ) and
%~ by default ?Neighbor_Cat nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))
%~ It's Proof that:
%~ " ?Neighbor_Cat keeps_as_pet cat " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Exists_Blend,blend)) &
poss( ~( neighbor(Exists_Blend,Neighbor_Cat))) &
'$existential'( Neighbor_Cat,
1,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) ==>
poss( ~( keeps_as_pet(Neighbor_Cat,cat)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?Exists_Blend neighbor ?Neighbor_Cat " is necessarily true and
%~ " ?Neighbor_Cat keeps_as_pet cat " is necessarily true )is possible ) and
%~ by default ?Exists_Blend exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))) ) and
%~ by default ?Neighbor_Cat nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))
%~ It's Proof that:
%~ " ?Exists_Blend smokes blend " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))) &
'$existential'( Exists_Blend,
1,
exists( Neighbor_Cat,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) &
'$existential'( Neighbor_Cat,
1,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) ==>
nesc( smokes(Exists_Blend,blend))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Neighbor_Cat keeps_as_pet cat " is necessarily true and
%~ " ?Exists_Blend neighbor ?Neighbor_Cat " is possibly false ) and
%~ by default ?Exists_Blend exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))) ) and
%~ by default ?Neighbor_Cat nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))
%~ It's Proof that:
%~ " ?Exists_Blend smokes blend " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(Neighbor_Cat,cat)) &
poss( ~( neighbor(Exists_Blend,Neighbor_Cat))) &
'$existential'( Exists_Blend,
1,
exists( Neighbor_Cat,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) &
'$existential'( Neighbor_Cat,
1,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) ==>
poss( ~( smokes(Exists_Blend,blend)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Exists_Blend neighbor ?Neighbor_Cat " is necessarily true and
%~ " ?Neighbor_Cat keeps_as_pet cat " is possibly false ) and
%~ by default ?Exists_Blend exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))) ) and
%~ by default ?Neighbor_Cat nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))
%~ It's Proof that:
%~ " ?Exists_Blend smokes blend " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
poss( ~( keeps_as_pet(Neighbor_Cat,cat))) &
'$existential'( Exists_Blend,
1,
exists( Neighbor_Cat,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) &
'$existential'( Neighbor_Cat,
1,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) ==>
poss( ~( smokes(Exists_Blend,blend)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Exists_Blend smokes blend " is necessarily true and
%~ " ?Neighbor_Cat keeps_as_pet cat " is necessarily true ) and
%~ by default ?Exists_Blend exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))) ) and
%~ by default ?Neighbor_Cat nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))
%~ It's Proof that:
%~ " ?Exists_Blend neighbor ?Neighbor_Cat " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Exists_Blend,blend)) &
nesc( keeps_as_pet(Neighbor_Cat,cat)) &
'$existential'( Exists_Blend,
1,
exists( Neighbor_Cat,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) &
'$existential'( Neighbor_Cat,
1,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) ==>
nesc( neighbor(Exists_Blend,Neighbor_Cat))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Exists_Blend smokes blend " is necessarily true and
%~ " ?Neighbor_Cat keeps_as_pet cat " is possibly false ) and
%~ by default ?Exists_Blend exists(Neighbor_Cat,nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))) ) and
%~ by default ?Neighbor_Cat nesc(smokes(Exists_Blend,blend))&nesc(neighbor(Exists_Blend,Neighbor_Cat))&nesc(keeps_as_pet(Neighbor_Cat,cat))
%~ It's Proof that:
%~ " ?Exists_Blend neighbor ?Neighbor_Cat " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Exists_Blend,blend)) &
poss( ~( keeps_as_pet(Neighbor_Cat,cat))) &
'$existential'( Exists_Blend,
1,
exists( Neighbor_Cat,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) &
'$existential'( Neighbor_Cat,
1,
( nesc( smokes(Exists_Blend,blend)) &
nesc( neighbor(Exists_Blend,Neighbor_Cat)) &
nesc( keeps_as_pet(Neighbor_Cat,cat))))) ==>
poss( ~( neighbor(Exists_Blend,Neighbor_Cat)))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),exists('$VAR'('Y'),necessary(and(smokes('$VAR'('X'),blend),and(neighbor('$VAR'('X'),'$VAR'('Y')),keeps_as_pet('$VAR'('Y'),cat))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?X neighbor ?Y " is necessarily true and
%~ " ?Y keeps_as_pet cat " is necessarily true )is possible ) and
%~ by default ?X exists(Y,nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))) ) and
%~ by default ?Y nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))
%~ It's Proof that:
%~ " ?X smokes blend " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) ==>
nesc( smokes(X,blend))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Y keeps_as_pet cat " is possible and
%~ ((" ?X smokes blend " is possibly false and
%~ by default ?X exists(Y,nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))) ) and
%~ by default ?Y nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat)) )
%~ It's Proof that:
%~ " ?X neighbor ?Y " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( keeps_as_pet(Y,cat)) &
poss( ~( smokes(X,blend))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) ==>
poss( ~( neighbor(X,Y)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X neighbor ?Y " is possible and
%~ ((" ?X smokes blend " is possibly false and
%~ by default ?X exists(Y,nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))) ) and
%~ by default ?Y nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat)) )
%~ It's Proof that:
%~ " ?Y keeps_as_pet cat " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( neighbor(X,Y)) &
poss( ~( smokes(X,blend))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) ==>
poss( ~( keeps_as_pet(Y,cat)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Y keeps_as_pet cat " is necessarily true and
%~ " ?X neighbor ?Y " is possibly false ) and
%~ by default ?X exists(Y,nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))) ) and
%~ by default ?Y nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))
%~ It's Proof that:
%~ " ?X smokes blend " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(Y,cat)) &
poss( ~( neighbor(X,Y))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) ==>
poss( ~( smokes(X,blend)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?X smokes blend " is necessarily true and
%~ " ?X neighbor ?Y " is possibly false ) and
%~ by default ?Y nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))
%~ It's Proof that:
%~ " ?Y keeps_as_pet cat " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(X,blend)) &
poss( ~( neighbor(X,Y))) &
'$existential'( Y,
1,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) ==>
poss( ~( keeps_as_pet(Y,cat)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?X smokes blend " is necessarily true and
%~ " ?Y keeps_as_pet cat " is necessarily true ) and
%~ by default ?X exists(Y,nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))) ) and
%~ by default ?Y nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))
%~ It's Proof that:
%~ " ?X neighbor ?Y " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(X,blend)) &
nesc( keeps_as_pet(Y,cat)) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) ==>
nesc( neighbor(X,Y))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?X neighbor ?Y " is necessarily true and
%~ " ?Y keeps_as_pet cat " is possibly false ) and
%~ by default ?X exists(Y,nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))) ) and
%~ by default ?Y nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))
%~ It's Proof that:
%~ " ?X smokes blend " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( neighbor(X,Y)) &
poss( ~( keeps_as_pet(Y,cat))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) ==>
poss( ~( smokes(X,blend)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?X smokes blend " is necessarily true and
%~ " ?Y keeps_as_pet cat " is possibly false ) and
%~ by default ?X exists(Y,nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))) ) and
%~ by default ?Y nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))
%~ It's Proof that:
%~ " ?X neighbor ?Y " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(X,blend)) &
poss( ~( keeps_as_pet(Y,cat))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) ==>
poss( ~( neighbor(X,Y)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?X smokes blend " is necessarily true and
%~ " ?X neighbor ?Y " is necessarily true ) and
%~ by default ?Y nesc(smokes(X,blend))&nesc(neighbor(X,Y))&nesc(keeps_as_pet(Y,cat))
%~ It's Proof that:
%~ " ?Y keeps_as_pet cat " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
'$existential'( Y,
1,
( nesc( smokes(X,blend)) &
nesc( neighbor(X,Y)) &
nesc( keeps_as_pet(Y,cat))))) ==>
nesc( keeps_as_pet(Y,cat))).
~*/
%= 11. The owner who keeps the horse lives next to the one who smokes Dunhill.
exists(X,exists(Y ,keeps_as_pet(X, horses) /\ neighbor(X, Y) /\ smokes(Y, dunhill))).
%= 12. The owner who smokes Bluemasters drinks beer.
/*~
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( exists( X,
%~ exists( Y,
%~ ( keeps_as_pet(X,horses) /\
%~ neighbor(X,Y) /\
%~ smokes(Y,dunhill))))))))
=======================================================
exists('$VAR'('Exists_Horses'),exists('$VAR'('Neighbor_Dunhill'),/\(keeps_as_pet('$VAR'('Exists_Horses'),horses),/\(neighbor('$VAR'('Exists_Horses'),'$VAR'('Neighbor_Dunhill')),smokes('$VAR'('Neighbor_Dunhill'),dunhill)))))
============================================
?- kif_to_boxlog( exists(Exists_Horses,exists(Neighbor_Dunhill,keeps_as_pet(Exists_Horses,horses)/\(neighbor(Exists_Horses,Neighbor_Dunhill)/\smokes(Neighbor_Dunhill,dunhill)))) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Exists_Horses
%~ (
%~ There exists ?Neighbor_Dunhill
%~ " ?Exists_Horses keeps_as_pet horses /\ ?Exists_Horses neighbor ?Neighbor_Dunhill /\ ?Neighbor_Dunhill smokes dunhill " )
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Exists_Horses'),exists('$VAR'('Neighbor_Dunhill'),necessary(and(keeps_as_pet('$VAR'('Exists_Horses'),horses),and(neighbor('$VAR'('Exists_Horses'),'$VAR'('Neighbor_Dunhill')),smokes('$VAR'('Neighbor_Dunhill'),dunhill))))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 9 entailment(s):
poss(neighbor(Exists_Horses,Neighbor_Dunhill))&(poss(~keeps_as_pet(Exists_Horses,horses))&'$existential'(Exists_Horses,1,exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))))&'$existential'(Neighbor_Dunhill,1,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))==>poss(~smokes(Neighbor_Dunhill,dunhill)).
poss(smokes(Neighbor_Dunhill,dunhill))&(poss(~keeps_as_pet(Exists_Horses,horses))&'$existential'(Exists_Horses,1,exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))))&'$existential'(Neighbor_Dunhill,1,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))==>poss(~neighbor(Exists_Horses,Neighbor_Dunhill)).
(nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill)))&'$existential'(Neighbor_Dunhill,1,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))==>nesc(smokes(Neighbor_Dunhill,dunhill)).
(nesc(keeps_as_pet(Exists_Horses,horses))&poss(~neighbor(Exists_Horses,Neighbor_Dunhill)))&'$existential'(Neighbor_Dunhill,1,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))==>poss(~smokes(Neighbor_Dunhill,dunhill)).
(poss(nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))&'$existential'(Exists_Horses,1,exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))))&'$existential'(Neighbor_Dunhill,1,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))==>nesc(keeps_as_pet(Exists_Horses,horses)).
((nesc(keeps_as_pet(Exists_Horses,horses))&nesc(smokes(Neighbor_Dunhill,dunhill)))&'$existential'(Exists_Horses,1,exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))))&'$existential'(Neighbor_Dunhill,1,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))==>nesc(neighbor(Exists_Horses,Neighbor_Dunhill)).
((nesc(keeps_as_pet(Exists_Horses,horses))&poss(~smokes(Neighbor_Dunhill,dunhill)))&'$existential'(Exists_Horses,1,exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))))&'$existential'(Neighbor_Dunhill,1,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))==>poss(~neighbor(Exists_Horses,Neighbor_Dunhill)).
((nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&poss(~smokes(Neighbor_Dunhill,dunhill)))&'$existential'(Exists_Horses,1,exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))))&'$existential'(Neighbor_Dunhill,1,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))==>poss(~keeps_as_pet(Exists_Horses,horses)).
((nesc(smokes(Neighbor_Dunhill,dunhill))&poss(~neighbor(Exists_Horses,Neighbor_Dunhill)))&'$existential'(Exists_Horses,1,exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))))&'$existential'(Neighbor_Dunhill,1,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)))==>poss(~keeps_as_pet(Exists_Horses,horses)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Exists_Horses neighbor ?Neighbor_Dunhill " is possible and
%~ ((" ?Exists_Horses keeps_as_pet horses " is possibly false and
%~ by default ?Exists_Horses exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))) ) and
%~ by default ?Neighbor_Dunhill nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)) )
%~ It's Proof that:
%~ " ?Neighbor_Dunhill smokes dunhill " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( neighbor(Exists_Horses,Neighbor_Dunhill)) &
poss( ~( keeps_as_pet(Exists_Horses,horses))) &
'$existential'( Exists_Horses,
1,
exists( Neighbor_Dunhill,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) &
'$existential'( Neighbor_Dunhill,
1,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) ==>
poss( ~( smokes(Neighbor_Dunhill,dunhill)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Neighbor_Dunhill smokes dunhill " is possible and
%~ ((" ?Exists_Horses keeps_as_pet horses " is possibly false and
%~ by default ?Exists_Horses exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))) ) and
%~ by default ?Neighbor_Dunhill nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill)) )
%~ It's Proof that:
%~ " ?Exists_Horses neighbor ?Neighbor_Dunhill " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( smokes(Neighbor_Dunhill,dunhill)) &
poss( ~( keeps_as_pet(Exists_Horses,horses))) &
'$existential'( Exists_Horses,
1,
exists( Neighbor_Dunhill,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) &
'$existential'( Neighbor_Dunhill,
1,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) ==>
poss( ~( neighbor(Exists_Horses,Neighbor_Dunhill)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Exists_Horses keeps_as_pet horses " is necessarily true and
%~ " ?Exists_Horses neighbor ?Neighbor_Dunhill " is necessarily true ) and
%~ by default ?Neighbor_Dunhill nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))
%~ It's Proof that:
%~ " ?Neighbor_Dunhill smokes dunhill " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
'$existential'( Neighbor_Dunhill,
1,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) ==>
nesc( smokes(Neighbor_Dunhill,dunhill))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Exists_Horses keeps_as_pet horses " is necessarily true and
%~ " ?Exists_Horses neighbor ?Neighbor_Dunhill " is possibly false ) and
%~ by default ?Neighbor_Dunhill nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))
%~ It's Proof that:
%~ " ?Neighbor_Dunhill smokes dunhill " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(Exists_Horses,horses)) &
poss( ~( neighbor(Exists_Horses,Neighbor_Dunhill))) &
'$existential'( Neighbor_Dunhill,
1,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) ==>
poss( ~( smokes(Neighbor_Dunhill,dunhill)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?Exists_Horses neighbor ?Neighbor_Dunhill " is necessarily true and
%~ " ?Neighbor_Dunhill smokes dunhill " is necessarily true )is possible ) and
%~ by default ?Exists_Horses exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))) ) and
%~ by default ?Neighbor_Dunhill nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))
%~ It's Proof that:
%~ " ?Exists_Horses keeps_as_pet horses " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))) &
'$existential'( Exists_Horses,
1,
exists( Neighbor_Dunhill,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) &
'$existential'( Neighbor_Dunhill,
1,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) ==>
nesc( keeps_as_pet(Exists_Horses,horses))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Exists_Horses keeps_as_pet horses " is necessarily true and
%~ " ?Neighbor_Dunhill smokes dunhill " is necessarily true ) and
%~ by default ?Exists_Horses exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))) ) and
%~ by default ?Neighbor_Dunhill nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))
%~ It's Proof that:
%~ " ?Exists_Horses neighbor ?Neighbor_Dunhill " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( smokes(Neighbor_Dunhill,dunhill)) &
'$existential'( Exists_Horses,
1,
exists( Neighbor_Dunhill,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) &
'$existential'( Neighbor_Dunhill,
1,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) ==>
nesc( neighbor(Exists_Horses,Neighbor_Dunhill))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Exists_Horses keeps_as_pet horses " is necessarily true and
%~ " ?Neighbor_Dunhill smokes dunhill " is possibly false ) and
%~ by default ?Exists_Horses exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))) ) and
%~ by default ?Neighbor_Dunhill nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))
%~ It's Proof that:
%~ " ?Exists_Horses neighbor ?Neighbor_Dunhill " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(Exists_Horses,horses)) &
poss( ~( smokes(Neighbor_Dunhill,dunhill))) &
'$existential'( Exists_Horses,
1,
exists( Neighbor_Dunhill,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) &
'$existential'( Neighbor_Dunhill,
1,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) ==>
poss( ~( neighbor(Exists_Horses,Neighbor_Dunhill)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Exists_Horses neighbor ?Neighbor_Dunhill " is necessarily true and
%~ " ?Neighbor_Dunhill smokes dunhill " is possibly false ) and
%~ by default ?Exists_Horses exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))) ) and
%~ by default ?Neighbor_Dunhill nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))
%~ It's Proof that:
%~ " ?Exists_Horses keeps_as_pet horses " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
poss( ~( smokes(Neighbor_Dunhill,dunhill))) &
'$existential'( Exists_Horses,
1,
exists( Neighbor_Dunhill,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) &
'$existential'( Neighbor_Dunhill,
1,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) ==>
poss( ~( keeps_as_pet(Exists_Horses,horses)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Neighbor_Dunhill smokes dunhill " is necessarily true and
%~ " ?Exists_Horses neighbor ?Neighbor_Dunhill " is possibly false ) and
%~ by default ?Exists_Horses exists(Neighbor_Dunhill,nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))) ) and
%~ by default ?Neighbor_Dunhill nesc(keeps_as_pet(Exists_Horses,horses))&nesc(neighbor(Exists_Horses,Neighbor_Dunhill))&nesc(smokes(Neighbor_Dunhill,dunhill))
%~ It's Proof that:
%~ " ?Exists_Horses keeps_as_pet horses " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Neighbor_Dunhill,dunhill)) &
poss( ~( neighbor(Exists_Horses,Neighbor_Dunhill))) &
'$existential'( Exists_Horses,
1,
exists( Neighbor_Dunhill,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) &
'$existential'( Neighbor_Dunhill,
1,
( nesc( keeps_as_pet(Exists_Horses,horses)) &
nesc( neighbor(Exists_Horses,Neighbor_Dunhill)) &
nesc( smokes(Neighbor_Dunhill,dunhill))))) ==>
poss( ~( keeps_as_pet(Exists_Horses,horses)))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),exists('$VAR'('Y'),necessary(and(keeps_as_pet('$VAR'('X'),horses),and(neighbor('$VAR'('X'),'$VAR'('Y')),smokes('$VAR'('Y'),dunhill))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?X neighbor ?Y " is necessarily true and
%~ " ?Y smokes dunhill " is necessarily true )is possible ) and
%~ by default ?X exists(Y,nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))) ) and
%~ by default ?Y nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))
%~ It's Proof that:
%~ " ?X keeps_as_pet horses " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))) &
'$existential'( X,
1,
exists( Y,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) &
'$existential'( Y,
1,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) ==>
nesc( keeps_as_pet(X,horses))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Y smokes dunhill " is possible and
%~ ((" ?X keeps_as_pet horses " is possibly false and
%~ by default ?X exists(Y,nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))) ) and
%~ by default ?Y nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill)) )
%~ It's Proof that:
%~ " ?X neighbor ?Y " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( smokes(Y,dunhill)) &
poss( ~( keeps_as_pet(X,horses))) &
'$existential'( X,
1,
exists( Y,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) &
'$existential'( Y,
1,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) ==>
poss( ~( neighbor(X,Y)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X neighbor ?Y " is possible and
%~ ((" ?X keeps_as_pet horses " is possibly false and
%~ by default ?X exists(Y,nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))) ) and
%~ by default ?Y nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill)) )
%~ It's Proof that:
%~ " ?Y smokes dunhill " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( neighbor(X,Y)) &
poss( ~( keeps_as_pet(X,horses))) &
'$existential'( X,
1,
exists( Y,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) &
'$existential'( Y,
1,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) ==>
poss( ~( smokes(Y,dunhill)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Y smokes dunhill " is necessarily true and
%~ " ?X neighbor ?Y " is possibly false ) and
%~ by default ?X exists(Y,nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))) ) and
%~ by default ?Y nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))
%~ It's Proof that:
%~ " ?X keeps_as_pet horses " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Y,dunhill)) &
poss( ~( neighbor(X,Y))) &
'$existential'( X,
1,
exists( Y,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) &
'$existential'( Y,
1,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) ==>
poss( ~( keeps_as_pet(X,horses)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?X keeps_as_pet horses " is necessarily true and
%~ " ?X neighbor ?Y " is possibly false ) and
%~ by default ?Y nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))
%~ It's Proof that:
%~ " ?Y smokes dunhill " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(X,horses)) &
poss( ~( neighbor(X,Y))) &
'$existential'( Y,
1,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) ==>
poss( ~( smokes(Y,dunhill)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?X keeps_as_pet horses " is necessarily true and
%~ " ?Y smokes dunhill " is necessarily true ) and
%~ by default ?X exists(Y,nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))) ) and
%~ by default ?Y nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))
%~ It's Proof that:
%~ " ?X neighbor ?Y " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(X,horses)) &
nesc( smokes(Y,dunhill)) &
'$existential'( X,
1,
exists( Y,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) &
'$existential'( Y,
1,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) ==>
nesc( neighbor(X,Y))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?X neighbor ?Y " is necessarily true and
%~ " ?Y smokes dunhill " is possibly false ) and
%~ by default ?X exists(Y,nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))) ) and
%~ by default ?Y nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))
%~ It's Proof that:
%~ " ?X keeps_as_pet horses " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( neighbor(X,Y)) &
poss( ~( smokes(Y,dunhill))) &
'$existential'( X,
1,
exists( Y,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) &
'$existential'( Y,
1,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) ==>
poss( ~( keeps_as_pet(X,horses)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?X keeps_as_pet horses " is necessarily true and
%~ " ?Y smokes dunhill " is possibly false ) and
%~ by default ?X exists(Y,nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))) ) and
%~ by default ?Y nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))
%~ It's Proof that:
%~ " ?X neighbor ?Y " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(X,horses)) &
poss( ~( smokes(Y,dunhill))) &
'$existential'( X,
1,
exists( Y,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) &
'$existential'( Y,
1,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) ==>
poss( ~( neighbor(X,Y)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?X keeps_as_pet horses " is necessarily true and
%~ " ?X neighbor ?Y " is necessarily true ) and
%~ by default ?Y nesc(keeps_as_pet(X,horses))&nesc(neighbor(X,Y))&nesc(smokes(Y,dunhill))
%~ It's Proof that:
%~ " ?Y smokes dunhill " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
'$existential'( Y,
1,
( nesc( keeps_as_pet(X,horses)) &
nesc( neighbor(X,Y)) &
nesc( smokes(Y,dunhill))))) ==>
nesc( smokes(Y,dunhill))).
~*/
%= 12. The owner who smokes Bluemasters drinks beer.
exists(X, smokes(X, bluemasters) /\ drinks(X, bier)).
%= 13. The German smokes Prince.
/*~
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( exists(X,smokes(X,bluemasters)/\drinks(X,bier))))))
=======================================================
exists('$VAR'('Bier_Bluemasters'),/\(smokes('$VAR'('Bier_Bluemasters'),bluemasters),drinks('$VAR'('Bier_Bluemasters'),bier)))
============================================
?- kif_to_boxlog( exists(Bier_Bluemasters,smokes(Bier_Bluemasters,bluemasters)/\drinks(Bier_Bluemasters,bier)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Bier_Bluemasters
%~ " ?Bier_Bluemasters smokes bluemasters /\ ?Bier_Bluemasters drinks bier "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Bier_Bluemasters'),necessary(and(smokes('$VAR'('Bier_Bluemasters'),bluemasters),drinks('$VAR'('Bier_Bluemasters'),bier))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 4 entailment(s):
nesc(drinks(Bier_Bluemasters,bier))&'$existential'(Bier_Bluemasters,1,nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier)))==>nesc(smokes(Bier_Bluemasters,bluemasters)).
nesc(smokes(Bier_Bluemasters,bluemasters))&'$existential'(Bier_Bluemasters,1,nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier)))==>nesc(drinks(Bier_Bluemasters,bier)).
poss(~drinks(Bier_Bluemasters,bier))&'$existential'(Bier_Bluemasters,1,nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier)))==>poss(~smokes(Bier_Bluemasters,bluemasters)).
poss(~smokes(Bier_Bluemasters,bluemasters))&'$existential'(Bier_Bluemasters,1,nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier)))==>poss(~drinks(Bier_Bluemasters,bier)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Bier_Bluemasters drinks bier " is necessarily true and
%~ by default ?Bier_Bluemasters nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier))
%~ It's Proof that:
%~ " ?Bier_Bluemasters smokes bluemasters " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( drinks(Bier_Bluemasters,bier)) &
'$existential'( Bier_Bluemasters,
1,
nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier)))) ==>
nesc( smokes(Bier_Bluemasters,bluemasters))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Bier_Bluemasters smokes bluemasters " is necessarily true and
%~ by default ?Bier_Bluemasters nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier))
%~ It's Proof that:
%~ " ?Bier_Bluemasters drinks bier " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Bier_Bluemasters,bluemasters)) &
'$existential'( Bier_Bluemasters,
1,
nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier)))) ==>
nesc( drinks(Bier_Bluemasters,bier))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Bier_Bluemasters drinks bier " is possibly false and
%~ by default ?Bier_Bluemasters nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier))
%~ It's Proof that:
%~ " ?Bier_Bluemasters smokes bluemasters " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( drinks(Bier_Bluemasters,bier))) &
'$existential'( Bier_Bluemasters,
1,
nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier)))) ==>
poss( ~( smokes(Bier_Bluemasters,bluemasters)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Bier_Bluemasters smokes bluemasters " is possibly false and
%~ by default ?Bier_Bluemasters nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier))
%~ It's Proof that:
%~ " ?Bier_Bluemasters drinks bier " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( smokes(Bier_Bluemasters,bluemasters))) &
'$existential'( Bier_Bluemasters,
1,
nesc(smokes(Bier_Bluemasters,bluemasters))&nesc(drinks(Bier_Bluemasters,bier)))) ==>
poss( ~( drinks(Bier_Bluemasters,bier)))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),necessary(and(smokes('$VAR'('X'),bluemasters),drinks('$VAR'('X'),bier))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X smokes bluemasters " is possibly false and
%~ by default ?X nesc(smokes(X,bluemasters))&nesc(drinks(X,bier))
%~ It's Proof that:
%~ " ?X drinks bier " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( smokes(X,bluemasters))) &
'$existential'(X,1,nesc(smokes(X,bluemasters))&nesc(drinks(X,bier)))) ==>
poss( ~( drinks(X,bier)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X drinks bier " is necessarily true and
%~ by default ?X nesc(smokes(X,bluemasters))&nesc(drinks(X,bier))
%~ It's Proof that:
%~ " ?X smokes bluemasters " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( drinks(X,bier)) &
'$existential'(X,1,nesc(smokes(X,bluemasters))&nesc(drinks(X,bier)))) ==>
nesc( smokes(X,bluemasters))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X drinks bier " is possibly false and
%~ by default ?X nesc(smokes(X,bluemasters))&nesc(drinks(X,bier))
%~ It's Proof that:
%~ " ?X smokes bluemasters " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( drinks(X,bier))) &
'$existential'(X,1,nesc(smokes(X,bluemasters))&nesc(drinks(X,bier)))) ==>
poss( ~( smokes(X,bluemasters)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X smokes bluemasters " is necessarily true and
%~ by default ?X nesc(smokes(X,bluemasters))&nesc(drinks(X,bier))
%~ It's Proof that:
%~ " ?X drinks bier " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(X,bluemasters)) &
'$existential'(X,1,nesc(smokes(X,bluemasters))&nesc(drinks(X,bier)))) ==>
nesc( drinks(X,bier))).
~*/
%= 13. The German smokes Prince.
smokes(german, prince).
%= 14. The Norwegian lives next to the blue house.
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(smokes(german,prince)))))
=======================================================
smokes(german,prince)
============================================
?- kif_to_boxlog( smokes(german,prince) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ german smokes prince
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(smokes(german,prince))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(smokes(german,prince)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that german smokes prince
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( smokes(german,prince)).
============================================
~*/
%= 14. The Norwegian lives next to the blue house.
exists(X, neighbor(norwegian, X) /\ lives(X, blue_house)).
%= 15. The owner who smokes Blends lives next to the one who drinks water.
/*~
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( exists(X,neighbor(norwegian,X)/\lives(X,blue_house))))))
=======================================================
exists('$VAR'('Neighbor_Blue_house_Norwegian'),/\(neighbor(norwegian,'$VAR'('Neighbor_Blue_house_Norwegian')),lives('$VAR'('Neighbor_Blue_house_Norwegian'),blue_house)))
============================================
?- kif_to_boxlog( exists(Neighbor_Blue_house_Norwegian,neighbor(norwegian,Neighbor_Blue_house_Norwegian)/\lives(Neighbor_Blue_house_Norwegian,blue_house)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Neighbor_Blue_house_Norwegian
%~ " norwegian neighbor ?Neighbor_Blue_house_Norwegian /\ ?Neighbor_Blue_house_Norwegian lives blue_house "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Neighbor_Blue_house_Norwegian'),necessary(and(neighbor(norwegian,'$VAR'('Neighbor_Blue_house_Norwegian')),lives('$VAR'('Neighbor_Blue_house_Norwegian'),blue_house))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 4 entailment(s):
nesc(lives(Neighbor_Blue_house_Norwegian,blue_house))&'$existential'(Neighbor_Blue_house_Norwegian,1,nesc(neighbor(norwegian,Neighbor_Blue_house_Norwegian))&nesc(lives(Neighbor_Blue_house_Norwegian,blue_house)))==>nesc(neighbor(norwegian,Neighbor_Blue_house_Norwegian)).
nesc(neighbor(norwegian,Neighbor_Blue_house_Norwegian))&'$existential'(Neighbor_Blue_house_Norwegian,1,nesc(neighbor(norwegian,Neighbor_Blue_house_Norwegian))&nesc(lives(Neighbor_Blue_house_Norwegian,blue_house)))==>nesc(lives(Neighbor_Blue_house_Norwegian,blue_house)).
poss(~lives(Neighbor_Blue_house_Norwegian,blue_house))&'$existential'(Neighbor_Blue_house_Norwegian,1,nesc(neighbor(norwegian,Neighbor_Blue_house_Norwegian))&nesc(lives(Neighbor_Blue_house_Norwegian,blue_house)))==>poss(~neighbor(norwegian,Neighbor_Blue_house_Norwegian)).
poss(~neighbor(norwegian,Neighbor_Blue_house_Norwegian))&'$existential'(Neighbor_Blue_house_Norwegian,1,nesc(neighbor(norwegian,Neighbor_Blue_house_Norwegian))&nesc(lives(Neighbor_Blue_house_Norwegian,blue_house)))==>poss(~lives(Neighbor_Blue_house_Norwegian,blue_house)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Neighbor_Blue_house_Norwegian lives blue_house " is necessarily true and
%~ by default ?Neighbor_Blue_house_Norwegian nesc(neighbor(norwegian,Neighbor_Blue_house_Norwegian))&nesc(lives(Neighbor_Blue_house_Norwegian,blue_house))
%~ It's Proof that:
%~ " norwegian neighbor ?Neighbor_Blue_house_Norwegian " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( lives(Neighbor_Blue_house_Norwegian,blue_house)) &
'$existential'( Neighbor_Blue_house_Norwegian,
1,
( nesc( neighbor(norwegian,Neighbor_Blue_house_Norwegian)) &
nesc( lives(Neighbor_Blue_house_Norwegian,blue_house))))) ==>
nesc( neighbor(norwegian,Neighbor_Blue_house_Norwegian))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " norwegian neighbor ?Neighbor_Blue_house_Norwegian " is necessarily true and
%~ by default ?Neighbor_Blue_house_Norwegian nesc(neighbor(norwegian,Neighbor_Blue_house_Norwegian))&nesc(lives(Neighbor_Blue_house_Norwegian,blue_house))
%~ It's Proof that:
%~ " ?Neighbor_Blue_house_Norwegian lives blue_house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( neighbor(norwegian,Neighbor_Blue_house_Norwegian)) &
'$existential'( Neighbor_Blue_house_Norwegian,
1,
( nesc( neighbor(norwegian,Neighbor_Blue_house_Norwegian)) &
nesc( lives(Neighbor_Blue_house_Norwegian,blue_house))))) ==>
nesc( lives(Neighbor_Blue_house_Norwegian,blue_house))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Neighbor_Blue_house_Norwegian lives blue_house " is possibly false and
%~ by default ?Neighbor_Blue_house_Norwegian nesc(neighbor(norwegian,Neighbor_Blue_house_Norwegian))&nesc(lives(Neighbor_Blue_house_Norwegian,blue_house))
%~ It's Proof that:
%~ " norwegian neighbor ?Neighbor_Blue_house_Norwegian " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( lives(Neighbor_Blue_house_Norwegian,blue_house))) &
'$existential'( Neighbor_Blue_house_Norwegian,
1,
( nesc( neighbor(norwegian,Neighbor_Blue_house_Norwegian)) &
nesc( lives(Neighbor_Blue_house_Norwegian,blue_house))))) ==>
poss( ~( neighbor(norwegian,Neighbor_Blue_house_Norwegian)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " norwegian neighbor ?Neighbor_Blue_house_Norwegian " is possibly false and
%~ by default ?Neighbor_Blue_house_Norwegian nesc(neighbor(norwegian,Neighbor_Blue_house_Norwegian))&nesc(lives(Neighbor_Blue_house_Norwegian,blue_house))
%~ It's Proof that:
%~ " ?Neighbor_Blue_house_Norwegian lives blue_house " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( neighbor(norwegian,Neighbor_Blue_house_Norwegian))) &
'$existential'( Neighbor_Blue_house_Norwegian,
1,
( nesc( neighbor(norwegian,Neighbor_Blue_house_Norwegian)) &
nesc( lives(Neighbor_Blue_house_Norwegian,blue_house))))) ==>
poss( ~( lives(Neighbor_Blue_house_Norwegian,blue_house)))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),necessary(and(neighbor(norwegian,'$VAR'('X')),lives('$VAR'('X'),blue_house))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " norwegian neighbor ?X " is possibly false and
%~ by default ?X nesc(neighbor(norwegian,X))&nesc(lives(X,blue_house))
%~ It's Proof that:
%~ " ?X lives blue_house " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( neighbor(norwegian,X))) &
'$existential'(X,1,nesc(neighbor(norwegian,X))&nesc(lives(X,blue_house)))) ==>
poss( ~( lives(X,blue_house)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X lives blue_house " is necessarily true and
%~ by default ?X nesc(neighbor(norwegian,X))&nesc(lives(X,blue_house))
%~ It's Proof that:
%~ " norwegian neighbor ?X " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( lives(X,blue_house)) &
'$existential'(X,1,nesc(neighbor(norwegian,X))&nesc(lives(X,blue_house)))) ==>
nesc( neighbor(norwegian,X))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X lives blue_house " is possibly false and
%~ by default ?X nesc(neighbor(norwegian,X))&nesc(lives(X,blue_house))
%~ It's Proof that:
%~ " norwegian neighbor ?X " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( lives(X,blue_house))) &
'$existential'(X,1,nesc(neighbor(norwegian,X))&nesc(lives(X,blue_house)))) ==>
poss( ~( neighbor(norwegian,X)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " norwegian neighbor ?X " is necessarily true and
%~ by default ?X nesc(neighbor(norwegian,X))&nesc(lives(X,blue_house))
%~ It's Proof that:
%~ " ?X lives blue_house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( neighbor(norwegian,X)) &
'$existential'(X,1,nesc(neighbor(norwegian,X))&nesc(lives(X,blue_house)))) ==>
nesc( lives(X,blue_house))).
~*/
%= 15. The owner who smokes Blends lives next to the one who drinks water.
exists(X,exists(Y,smokes(X, blends) /\ neighbor(X,Y) /\ drinks(Y, water))).
%= The five owners drinks a certain type of beverage, smokes a certain brand of
%= cigar and keep a certain keeps_as_pet.
/*~
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( exists( X,
%~ exists(Y,smokes(X,blends)/\(neighbor(X,Y)/\drinks(Y,water))))))))
=======================================================
exists('$VAR'('Exists_Blends'),exists('$VAR'('Neighbor_Water'),/\(smokes('$VAR'('Exists_Blends'),blends),/\(neighbor('$VAR'('Exists_Blends'),'$VAR'('Neighbor_Water')),drinks('$VAR'('Neighbor_Water'),water)))))
============================================
?- kif_to_boxlog( exists(Exists_Blends,exists(Neighbor_Water,smokes(Exists_Blends,blends)/\(neighbor(Exists_Blends,Neighbor_Water)/\drinks(Neighbor_Water,water)))) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Exists_Blends
%~ (
%~ There exists ?Neighbor_Water
%~ " ?Exists_Blends smokes blends /\ ?Exists_Blends neighbor ?Neighbor_Water /\ ?Neighbor_Water drinks water " )
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Exists_Blends'),exists('$VAR'('Neighbor_Water'),necessary(and(smokes('$VAR'('Exists_Blends'),blends),and(neighbor('$VAR'('Exists_Blends'),'$VAR'('Neighbor_Water')),drinks('$VAR'('Neighbor_Water'),water))))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 9 entailment(s):
poss(drinks(Neighbor_Water,water))&(poss(~smokes(Exists_Blends,blends))&'$existential'(Exists_Blends,1,exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))))&'$existential'(Neighbor_Water,1,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))==>poss(~neighbor(Exists_Blends,Neighbor_Water)).
poss(neighbor(Exists_Blends,Neighbor_Water))&(poss(~smokes(Exists_Blends,blends))&'$existential'(Exists_Blends,1,exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))))&'$existential'(Neighbor_Water,1,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))==>poss(~drinks(Neighbor_Water,water)).
(nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water)))&'$existential'(Neighbor_Water,1,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))==>nesc(drinks(Neighbor_Water,water)).
(nesc(smokes(Exists_Blends,blends))&poss(~neighbor(Exists_Blends,Neighbor_Water)))&'$existential'(Neighbor_Water,1,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))==>poss(~drinks(Neighbor_Water,water)).
(poss(nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))&'$existential'(Exists_Blends,1,exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))))&'$existential'(Neighbor_Water,1,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))==>nesc(smokes(Exists_Blends,blends)).
((nesc(drinks(Neighbor_Water,water))&poss(~neighbor(Exists_Blends,Neighbor_Water)))&'$existential'(Exists_Blends,1,exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))))&'$existential'(Neighbor_Water,1,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))==>poss(~smokes(Exists_Blends,blends)).
((nesc(neighbor(Exists_Blends,Neighbor_Water))&poss(~drinks(Neighbor_Water,water)))&'$existential'(Exists_Blends,1,exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))))&'$existential'(Neighbor_Water,1,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))==>poss(~smokes(Exists_Blends,blends)).
((nesc(smokes(Exists_Blends,blends))&nesc(drinks(Neighbor_Water,water)))&'$existential'(Exists_Blends,1,exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))))&'$existential'(Neighbor_Water,1,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))==>nesc(neighbor(Exists_Blends,Neighbor_Water)).
((nesc(smokes(Exists_Blends,blends))&poss(~drinks(Neighbor_Water,water)))&'$existential'(Exists_Blends,1,exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))))&'$existential'(Neighbor_Water,1,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)))==>poss(~neighbor(Exists_Blends,Neighbor_Water)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Neighbor_Water drinks water " is possible and
%~ ((" ?Exists_Blends smokes blends " is possibly false and
%~ by default ?Exists_Blends exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))) ) and
%~ by default ?Neighbor_Water nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)) )
%~ It's Proof that:
%~ " ?Exists_Blends neighbor ?Neighbor_Water " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( drinks(Neighbor_Water,water)) &
poss( ~( smokes(Exists_Blends,blends))) &
'$existential'( Exists_Blends,
1,
exists( Neighbor_Water,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) &
'$existential'( Neighbor_Water,
1,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) ==>
poss( ~( neighbor(Exists_Blends,Neighbor_Water)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Exists_Blends neighbor ?Neighbor_Water " is possible and
%~ ((" ?Exists_Blends smokes blends " is possibly false and
%~ by default ?Exists_Blends exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))) ) and
%~ by default ?Neighbor_Water nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water)) )
%~ It's Proof that:
%~ " ?Neighbor_Water drinks water " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( neighbor(Exists_Blends,Neighbor_Water)) &
poss( ~( smokes(Exists_Blends,blends))) &
'$existential'( Exists_Blends,
1,
exists( Neighbor_Water,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) &
'$existential'( Neighbor_Water,
1,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) ==>
poss( ~( drinks(Neighbor_Water,water)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Exists_Blends smokes blends " is necessarily true and
%~ " ?Exists_Blends neighbor ?Neighbor_Water " is necessarily true ) and
%~ by default ?Neighbor_Water nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))
%~ It's Proof that:
%~ " ?Neighbor_Water drinks water " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
'$existential'( Neighbor_Water,
1,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) ==>
nesc( drinks(Neighbor_Water,water))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Exists_Blends smokes blends " is necessarily true and
%~ " ?Exists_Blends neighbor ?Neighbor_Water " is possibly false ) and
%~ by default ?Neighbor_Water nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))
%~ It's Proof that:
%~ " ?Neighbor_Water drinks water " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Exists_Blends,blends)) &
poss( ~( neighbor(Exists_Blends,Neighbor_Water))) &
'$existential'( Neighbor_Water,
1,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) ==>
poss( ~( drinks(Neighbor_Water,water)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?Exists_Blends neighbor ?Neighbor_Water " is necessarily true and
%~ " ?Neighbor_Water drinks water " is necessarily true )is possible ) and
%~ by default ?Exists_Blends exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))) ) and
%~ by default ?Neighbor_Water nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))
%~ It's Proof that:
%~ " ?Exists_Blends smokes blends " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))) &
'$existential'( Exists_Blends,
1,
exists( Neighbor_Water,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) &
'$existential'( Neighbor_Water,
1,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) ==>
nesc( smokes(Exists_Blends,blends))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Neighbor_Water drinks water " is necessarily true and
%~ " ?Exists_Blends neighbor ?Neighbor_Water " is possibly false ) and
%~ by default ?Exists_Blends exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))) ) and
%~ by default ?Neighbor_Water nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))
%~ It's Proof that:
%~ " ?Exists_Blends smokes blends " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( drinks(Neighbor_Water,water)) &
poss( ~( neighbor(Exists_Blends,Neighbor_Water))) &
'$existential'( Exists_Blends,
1,
exists( Neighbor_Water,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) &
'$existential'( Neighbor_Water,
1,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) ==>
poss( ~( smokes(Exists_Blends,blends)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Exists_Blends neighbor ?Neighbor_Water " is necessarily true and
%~ " ?Neighbor_Water drinks water " is possibly false ) and
%~ by default ?Exists_Blends exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))) ) and
%~ by default ?Neighbor_Water nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))
%~ It's Proof that:
%~ " ?Exists_Blends smokes blends " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( neighbor(Exists_Blends,Neighbor_Water)) &
poss( ~( drinks(Neighbor_Water,water))) &
'$existential'( Exists_Blends,
1,
exists( Neighbor_Water,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) &
'$existential'( Neighbor_Water,
1,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) ==>
poss( ~( smokes(Exists_Blends,blends)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Exists_Blends smokes blends " is necessarily true and
%~ " ?Neighbor_Water drinks water " is necessarily true ) and
%~ by default ?Exists_Blends exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))) ) and
%~ by default ?Neighbor_Water nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))
%~ It's Proof that:
%~ " ?Exists_Blends neighbor ?Neighbor_Water " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Exists_Blends,blends)) &
nesc( drinks(Neighbor_Water,water)) &
'$existential'( Exists_Blends,
1,
exists( Neighbor_Water,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) &
'$existential'( Neighbor_Water,
1,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) ==>
nesc( neighbor(Exists_Blends,Neighbor_Water))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Exists_Blends smokes blends " is necessarily true and
%~ " ?Neighbor_Water drinks water " is possibly false ) and
%~ by default ?Exists_Blends exists(Neighbor_Water,nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))) ) and
%~ by default ?Neighbor_Water nesc(smokes(Exists_Blends,blends))&nesc(neighbor(Exists_Blends,Neighbor_Water))&nesc(drinks(Neighbor_Water,water))
%~ It's Proof that:
%~ " ?Exists_Blends neighbor ?Neighbor_Water " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(Exists_Blends,blends)) &
poss( ~( drinks(Neighbor_Water,water))) &
'$existential'( Exists_Blends,
1,
exists( Neighbor_Water,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) &
'$existential'( Neighbor_Water,
1,
( nesc( smokes(Exists_Blends,blends)) &
nesc( neighbor(Exists_Blends,Neighbor_Water)) &
nesc( drinks(Neighbor_Water,water))))) ==>
poss( ~( neighbor(Exists_Blends,Neighbor_Water)))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),exists('$VAR'('Y'),necessary(and(smokes('$VAR'('X'),blends),and(neighbor('$VAR'('X'),'$VAR'('Y')),drinks('$VAR'('Y'),water))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?X neighbor ?Y " is necessarily true and
%~ " ?Y drinks water " is necessarily true )is possible ) and
%~ by default ?X exists(Y,nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))) ) and
%~ by default ?Y nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))
%~ It's Proof that:
%~ " ?X smokes blends " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( nesc(neighbor(X,Y))&nesc(drinks(Y,water))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) ==>
nesc( smokes(X,blends))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Y drinks water " is possible and
%~ ((" ?X smokes blends " is possibly false and
%~ by default ?X exists(Y,nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))) ) and
%~ by default ?Y nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water)) )
%~ It's Proof that:
%~ " ?X neighbor ?Y " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( drinks(Y,water)) &
poss( ~( smokes(X,blends))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) ==>
poss( ~( neighbor(X,Y)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X neighbor ?Y " is possible and
%~ ((" ?X smokes blends " is possibly false and
%~ by default ?X exists(Y,nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))) ) and
%~ by default ?Y nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water)) )
%~ It's Proof that:
%~ " ?Y drinks water " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( neighbor(X,Y)) &
poss( ~( smokes(X,blends))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) ==>
poss( ~( drinks(Y,water)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?Y drinks water " is necessarily true and
%~ " ?X neighbor ?Y " is possibly false ) and
%~ by default ?X exists(Y,nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))) ) and
%~ by default ?Y nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))
%~ It's Proof that:
%~ " ?X smokes blends " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( drinks(Y,water)) &
poss( ~( neighbor(X,Y))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) ==>
poss( ~( smokes(X,blends)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?X smokes blends " is necessarily true and
%~ " ?X neighbor ?Y " is possibly false ) and
%~ by default ?Y nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))
%~ It's Proof that:
%~ " ?Y drinks water " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(X,blends)) &
poss( ~( neighbor(X,Y))) &
'$existential'( Y,
1,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) ==>
poss( ~( drinks(Y,water)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?X smokes blends " is necessarily true and
%~ " ?Y drinks water " is necessarily true ) and
%~ by default ?X exists(Y,nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))) ) and
%~ by default ?Y nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))
%~ It's Proof that:
%~ " ?X neighbor ?Y " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(X,blends)) &
nesc( drinks(Y,water)) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) ==>
nesc( neighbor(X,Y))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?X neighbor ?Y " is necessarily true and
%~ " ?Y drinks water " is possibly false ) and
%~ by default ?X exists(Y,nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))) ) and
%~ by default ?Y nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))
%~ It's Proof that:
%~ " ?X smokes blends " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( neighbor(X,Y)) &
poss( ~( drinks(Y,water))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) ==>
poss( ~( smokes(X,blends)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((" ?X smokes blends " is necessarily true and
%~ " ?Y drinks water " is possibly false ) and
%~ by default ?X exists(Y,nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))) ) and
%~ by default ?Y nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))
%~ It's Proof that:
%~ " ?X neighbor ?Y " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(X,blends)) &
poss( ~( drinks(Y,water))) &
'$existential'( X,
1,
exists( Y,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) &
'$existential'( Y,
1,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) ==>
poss( ~( neighbor(X,Y)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?X smokes blends " is necessarily true and
%~ " ?X neighbor ?Y " is necessarily true ) and
%~ by default ?Y nesc(smokes(X,blends))&nesc(neighbor(X,Y))&nesc(drinks(Y,water))
%~ It's Proof that:
%~ " ?Y drinks water " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
'$existential'( Y,
1,
( nesc( smokes(X,blends)) &
nesc( neighbor(X,Y)) &
nesc( drinks(Y,water))))) ==>
nesc( drinks(Y,water))).
~*/
%= The five owners drinks a certain type of beverage, smokes a certain brand of
%= cigar and keep a certain keeps_as_pet.
trait(drinks).
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(trait(drinks)))))
=======================================================
trait(drinks)
============================================
?- kif_to_boxlog( trait(drinks) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ drinks isa trait
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(trait(drinks))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(trait(drinks)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that drinks isa trait
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( trait(drinks)).
============================================
~*/
trait(smokes).
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(trait(smokes)))))
=======================================================
trait(smokes)
============================================
?- kif_to_boxlog( trait(smokes) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ smokes isa trait
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(trait(smokes))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(trait(smokes)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that smokes isa trait
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( trait(smokes)).
============================================
~*/
trait(keeps_as_pet).
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_03.pfc.pl:130
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(trait(keeps_as_pet)))))
=======================================================
trait(keeps_as_pet)
============================================
?- kif_to_boxlog( trait(keeps_as_pet) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ keeps_as_pet isa trait
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(trait(keeps_as_pet))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(trait(keeps_as_pet)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that keeps_as_pet isa trait
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( trait(keeps_as_pet)).
============================================
~*/
trait(position). % we add position
% forward chain these into houses
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_03.pfc.pl:131
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(trait(position)))))
=======================================================
trait(position)
============================================
?- kif_to_boxlog( trait(position) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ position isa trait
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(trait(position))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(trait(position)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that position isa trait
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( trait(position)).
============================================
~*/
% we add position
% forward chain these into houses
leftof(HA, HB) ==> (house(HA) , house(HB)).
%= There are five houses in a row.
/*~
~*/
%= There are five houses in a row.
exists(H1,exists(H2,exists(H3,exists(H4,exists(H5,
leftof(H1, H2) /\ leftof(H2, H3) /\ leftof(H3, H4) /\ leftof(H4, H5)))))).
% SANITY count the persons (shouild be 5)
% :- sanity(( findall(P,person(P),L),length(L,5))).
%= In each house lives a person with a unique nationality.
% we write this in SUMO
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_03.pfc.pl:140
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( exists( H1,
%~ exists( H2,
%~ exists( H3,
%~ exists( H4,
%~ exists( H5,
%~ ( leftof(H1,H2) /\
%~ leftof(H2,H3) /\
%~ leftof(H3,H4) /\
%~ leftof(H4,H5)))))))))))
=======================================================
exists('$VAR'('Exists_Leftof'),exists('$VAR'('Exists_Leftof6'),exists('$VAR'('Exists_Leftof7'),exists('$VAR'('Exists_Leftof8'),exists('$VAR'('Leftof13'),/\(leftof('$VAR'('Exists_Leftof'),'$VAR'('Exists_Leftof6')),/\(leftof('$VAR'('Exists_Leftof6'),'$VAR'('Exists_Leftof7')),/\(leftof('$VAR'('Exists_Leftof7'),'$VAR'('Exists_Leftof8')),leftof('$VAR'('Exists_Leftof8'),'$VAR'('Leftof13'))))))))))
============================================
?- kif_to_boxlog( exists(Exists_Leftof,exists(Exists_Leftof6,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,leftof(Exists_Leftof,Exists_Leftof6)/\(leftof(Exists_Leftof6,Exists_Leftof7)/\(leftof(Exists_Leftof7,Exists_Leftof8)/\leftof(Exists_Leftof8,Leftof13)))))))) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Exists_Leftof
%~ (
%~ There exists ?Exists_Leftof6
%~ (
%~ There exists ?Exists_Leftof7
%~ (
%~ There exists ?Exists_Leftof8
%~ (
%~ There exists ?Leftof13
%~ " ?Exists_Leftof leftof ?Exists_Leftof6 /\ ?Exists_Leftof6 leftof ?Exists_Leftof7 /\ ?Exists_Leftof7 leftof ?Exists_Leftof8 /\ ?Exists_Leftof8 leftof ?Leftof13 " ))))
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Exists_Leftof'),exists('$VAR'('Exists_Leftof6'),exists('$VAR'('Exists_Leftof7'),exists('$VAR'('Exists_Leftof8'),exists('$VAR'('Leftof13'),necessary(and(leftof('$VAR'('Exists_Leftof'),'$VAR'('Exists_Leftof6')),and(leftof('$VAR'('Exists_Leftof6'),'$VAR'('Exists_Leftof7')),and(leftof('$VAR'('Exists_Leftof7'),'$VAR'('Exists_Leftof8')),leftof('$VAR'('Exists_Leftof8'),'$VAR'('Leftof13')))))))))))
totalTime=10.000
FAILED: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k einstein_simpler_03.pfc.pl (returned 137) Add_LABELS='Errors,Overtime' Rem_LABELS='Skipped,Skipped,Warnings,Skipped'
