<testcase name="logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_01@Test_0001_Line_0000__Nesc: baseKB:listing(nesc)" classname="logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_01" time="0.006">
<system-err><![CDATA[name=Test_0001_Line_0000__Nesc
JUNIT_CLASSNAME='logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_01'.
JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s lmoo-clif five_leftof_type_01.pl'.
(cd /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof ; timeout --foreground --preserve-status -s SIGKILL -k 10s 10s lmoo-clif five_leftof_type_01.pl)
%
running('/var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl'),
%~ this_test_might_need( :-( use_module( library(logicmoo_plarkc))))
%~ /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test_header.pl:96
%~ this_test_might_need( :-( expects_dialect(pfc)))
:- expects_dialect(clif).
:- kif_compile.
% makes the KB monotonic
% makes the KB monotonic
:- set_kif_option(qualify_modality,simple_nesc).
% There are five houses in a row.
% There are five houses in a row.
nesc(leftof(h1, h2)).
leftof(h2, h3).
%~ kifi = leftof(h2,h3).
%~ kifm = nesc( leftof(h2,h3)).
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl:26
%~ kifm = nesc( leftof(h2,h3)).
%~ debugm(common_logic_loader,show_success(common_logic_loader,common_logic_loader:ain(clif(leftof(h2,h3)))))
%~ kifi = leftof(h2,h3).
%~ kifm = nesc( leftof(h2,h3)).
/*~
%~ kifi=leftof(h2,h3)
%~ kifm=nesc(leftof(h2,h3))
%~ kifm=nesc(leftof(h2,h3))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h2,h3))
=======================================================
leftof(h2,h3)
?- kif_to_boxlog( leftof(h2,h3) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ h2 leftof h3
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kifi=leftof(h2,h3)
%~ kifm=nesc(leftof(h2,h3))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h2,h3))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(leftof(h2,h3)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that h2 leftof h3
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( leftof(h2,h3)).
============================================
~*/
leftof(h3, h4).
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl:27
%~ kifi = leftof(h3,h4).
%~ kifm = nesc( leftof(h3,h4)).
%~ kifm = nesc( leftof(h3,h4)).
%~ debugm(common_logic_loader,show_success(common_logic_loader,common_logic_loader:ain(clif(leftof(h3,h4)))))
%~ kifi = leftof(h3,h4).
%~ kifm = nesc( leftof(h3,h4)).
/*~
%~ kifi=leftof(h3,h4)
%~ kifm=nesc(leftof(h3,h4))
%~ kifm=nesc(leftof(h3,h4))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h3,h4))
=======================================================
leftof(h3,h4)
?- kif_to_boxlog( leftof(h3,h4) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ h3 leftof h4
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kifi=leftof(h3,h4)
%~ kifm=nesc(leftof(h3,h4))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h3,h4))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(leftof(h3,h4)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that h3 leftof h4
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( leftof(h3,h4)).
============================================
~*/
leftof(h4, h5).
% makes the KB non-monotonic
%~ kifi = leftof(h4,h5).
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl:28
%~ kifm = nesc( leftof(h4,h5)).
%~ kifm = nesc( leftof(h4,h5)).
%~ debugm(common_logic_loader,show_success(common_logic_loader,common_logic_loader:ain(clif(leftof(h4,h5)))))
%~ kifi = leftof(h4,h5).
%~ kifm = nesc( leftof(h4,h5)).
/*~
%~ kifi=leftof(h4,h5)
%~ kifm=nesc(leftof(h4,h5))
%~ kifm=nesc(leftof(h4,h5))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h4,h5))
=======================================================
leftof(h4,h5)
?- kif_to_boxlog( leftof(h4,h5) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ h4 leftof h5
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kifi=leftof(h4,h5)
%~ kifm=nesc(leftof(h4,h5))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h4,h5))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(leftof(h4,h5)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that h4 leftof h5
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( leftof(h4,h5)).
============================================
~*/
% makes the KB non-monotonic
:- set_kif_option(qualify_modality,false).
% this should cause h1-h5 to become houses
% this should cause h1-h5 to become houses
leftof(H1, H2) => house(H1) & house(H2).
% intractive_test/1 means only run if interactive
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl:35
%~ kifm = ( leftof(House_Leftof,House_Leftof3) =>
%~ house(House_Leftof)&house(House_Leftof3)).
%~ kifm = ( leftof(House_Leftof8,House_Leftof9) =>
%~ house(House_Leftof8)&house(House_Leftof9)).
%~ debugm( common_logic_loader,
%~ show_success( common_logic_loader,
%~ common_logic_loader : ain( clif( leftof(H1,H2)=>(house(H1)&house(H2))))))
%~ kifm = ( leftof(House_Leftof,House_Leftof3) =>
%~ house(House_Leftof)&house(House_Leftof3)).
%~ kifm = leftof(H1,H2)=>(house(H1)&house(H2)).
/*~
%~ kifm=leftof(House_Leftof,House_Leftof3)=>(house(House_Leftof)&house(House_Leftof3))
%~ kifm=leftof(House_Leftof8,House_Leftof9)=>(house(House_Leftof8)&house(House_Leftof9))
%~ kif_to_boxlog_attvars2 = =>(leftof('$VAR'('House_Leftof8'),'$VAR'('House_Leftof9')),and(house('$VAR'('House_Leftof8')),house('$VAR'('House_Leftof9'))))
=======================================================
=>(leftof('$VAR'('House_Leftof'),'$VAR'('House_Leftof3')),&(house('$VAR'('House_Leftof')),house('$VAR'('House_Leftof3'))))
?- kif_to_boxlog( leftof(House_Leftof,House_Leftof3)=>(house(House_Leftof)&house(House_Leftof3)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ If:
%~ ?House_Leftof leftof ?House_Leftof3 then it is
%~ Implied that:
%~ " ?House_Leftof isa house " and
%~ " ?House_Leftof3 isa house "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kifm=leftof(House_Leftof,House_Leftof3)=>(house(House_Leftof)&house(House_Leftof3))
%~ kif_to_boxlog_attvars2 = =>(leftof('$VAR'('House_Leftof'),'$VAR'('House_Leftof3')),and(house('$VAR'('House_Leftof')),house('$VAR'('House_Leftof3'))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 6 entailment(s):
nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof))==>nesc(~house(House_Leftof3)).
nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof3))==>nesc(~house(House_Leftof)).
nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof))==>nesc(house(House_Leftof3)).
nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof3))==>nesc(house(House_Leftof)).
poss(house(House_Leftof))&nesc(~house(House_Leftof3))==>nesc(~leftof(House_Leftof,House_Leftof3)).
poss(house(House_Leftof3))&nesc(~house(House_Leftof))==>nesc(~leftof(House_Leftof,House_Leftof3)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and
%~ " ?House_Leftof isa house " is necessarily false
%~ It's Proof that:
%~ " ?House_Leftof3 isa house " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof)) ==>
nesc( ~( house(House_Leftof3)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and
%~ " ?House_Leftof3 isa house " is necessarily false
%~ It's Proof that:
%~ " ?House_Leftof isa house " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof3)) ==>
nesc( ~( house(House_Leftof)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and
%~ " ?House_Leftof isa house " is possible
%~ It's Proof that:
%~ " ?House_Leftof3 isa house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof)) ==>
nesc( house(House_Leftof3))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and
%~ " ?House_Leftof3 isa house " is possible
%~ It's Proof that:
%~ " ?House_Leftof isa house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof3)) ==>
nesc( house(House_Leftof))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof isa house " is possible and
%~ " ?House_Leftof3 isa house " is necessarily false
%~ It's Proof that:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( poss(house(House_Leftof))&nesc(~house(House_Leftof3)) ==>
nesc( ~( leftof(House_Leftof,House_Leftof3)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof3 isa house " is possible and
%~ " ?House_Leftof isa house " is necessarily false
%~ It's Proof that:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( poss(house(House_Leftof3))&nesc(~house(House_Leftof)) ==>
nesc( ~( leftof(House_Leftof,House_Leftof3)))).
============================================%~ kifm=leftof(H1,H2)=>(house(H1)&house(H2))
%~ kif_to_boxlog_attvars2 = =>(leftof('$VAR'('H1'),'$VAR'('H2')),and(house('$VAR'('H1')),house('$VAR'('H2'))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H2 isa house " is possible and
%~ " ?H1 isa house " is necessarily false
%~ It's Proof that:
%~ " ?H1 leftof ?H2 " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(house(H2))&nesc(~house(H1))==>nesc(~leftof(H1,H2)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H1 leftof ?H2 " is necessarily true and
%~ " ?H1 isa house " is necessarily false
%~ It's Proof that:
%~ " ?H2 isa house " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(leftof(H1,H2))&nesc(~house(H1))==>nesc(~house(H2)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H1 leftof ?H2 " is necessarily true and
%~ " ?H2 isa house " is possible
%~ It's Proof that:
%~ " ?H1 isa house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(leftof(H1,H2))&poss(house(H2))==>nesc(house(H1)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H1 isa house " is possible and
%~ " ?H2 isa house " is necessarily false
%~ It's Proof that:
%~ " ?H1 leftof ?H2 " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(house(H1))&nesc(~house(H2))==>nesc(~leftof(H1,H2)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H1 leftof ?H2 " is necessarily true and
%~ " ?H2 isa house " is necessarily false
%~ It's Proof that:
%~ " ?H1 isa house " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(leftof(H1,H2))&nesc(~house(H2))==>nesc(~house(H1)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H1 leftof ?H2 " is necessarily true and
%~ " ?H1 isa house " is possible
%~ It's Proof that:
%~ " ?H2 isa house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(leftof(H1,H2))&poss(house(H1))==>nesc(house(H2)).
~*/
% intractive_test/1 means only run if interactive
:- interactive_test(listing(kif_show)).
% mpred_test/1 each become a Junit test that must succeed
/*~
0m1m97m40m?- listing(kif_show).49m0m21m0m
~*/
% mpred_test/1 each become a Junit test that must succeed
:- mpred_test(listing(nesc)).
% ensure our rule worked
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl:41
%~ mpred_test("Test_0001_Line_0000__Nesc",baseKB:listing(nesc))
goal=baseKB:listing(nesc).
time=0.00638270378112793.
passed=passed=info(why_was_true(baseKB:listing(nesc)))
no_proof_for(listing(nesc)).
:- dynamic nesc/1.
:- multifile nesc/1.
:- public nesc/1.
:- module_transparent nesc/1.
nesc(A) :-
zwc,
nesc_lc(baseKB, A).
nesc(leftof(h1, h2)).
nesc(leftof(h2, h3)).
nesc(leftof(h3, h4)).
nesc(leftof(h4, h5)).
nesc(house(h1)).
nesc(house(h2)).
nesc(house(h3)).
nesc(house(h4)).
nesc(house(h5)).
:- public nesc/2.
:- module_transparent nesc/2.
nesc(_M, isNamed(X, Y)) :-
!,
isNamed_impl(X, Y),
!.
nesc(A, B) :-
swc,
first_of([ (loop_check_term(A:proven_tru(B), info(A:proven_tru(B), 'common_logic_exists.pl':318), fail), nop(nrlc0(call(call, +A:proven_neg(B))))),
(A:proven_helper(B), +A:proven_helper(~B)),
A:skolem_tru(B)
]).
no_proof_for(listing(nesc)).
no_proof_for(listing(nesc)).
result=passed.
]]>
JUNIT_CLASSNAME='logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_01'.
JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s lmoo-clif five_leftof_type_01.pl'.
(cd /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof ; timeout --foreground --preserve-status -s SIGKILL -k 10s 10s lmoo-clif five_leftof_type_01.pl)
%
running('/var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl'),
%~ this_test_might_need( :-( use_module( library(logicmoo_plarkc))))
%~ /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test_header.pl:96
%~ this_test_might_need( :-( expects_dialect(pfc)))
:- expects_dialect(clif).
:- kif_compile.
% makes the KB monotonic
% makes the KB monotonic
:- set_kif_option(qualify_modality,simple_nesc).
% There are five houses in a row.
% There are five houses in a row.
nesc(leftof(h1, h2)).
leftof(h2, h3).
%~ kifi = leftof(h2,h3).
%~ kifm = nesc( leftof(h2,h3)).
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl:26
%~ kifm = nesc( leftof(h2,h3)).
%~ debugm(common_logic_loader,show_success(common_logic_loader,common_logic_loader:ain(clif(leftof(h2,h3)))))
%~ kifi = leftof(h2,h3).
%~ kifm = nesc( leftof(h2,h3)).
/*~
%~ kifi=leftof(h2,h3)
%~ kifm=nesc(leftof(h2,h3))
%~ kifm=nesc(leftof(h2,h3))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h2,h3))
=======================================================
leftof(h2,h3)
?- kif_to_boxlog( leftof(h2,h3) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ h2 leftof h3
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kifi=leftof(h2,h3)
%~ kifm=nesc(leftof(h2,h3))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h2,h3))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(leftof(h2,h3)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that h2 leftof h3
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( leftof(h2,h3)).
============================================
~*/
leftof(h3, h4).
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl:27
%~ kifi = leftof(h3,h4).
%~ kifm = nesc( leftof(h3,h4)).
%~ kifm = nesc( leftof(h3,h4)).
%~ debugm(common_logic_loader,show_success(common_logic_loader,common_logic_loader:ain(clif(leftof(h3,h4)))))
%~ kifi = leftof(h3,h4).
%~ kifm = nesc( leftof(h3,h4)).
/*~
%~ kifi=leftof(h3,h4)
%~ kifm=nesc(leftof(h3,h4))
%~ kifm=nesc(leftof(h3,h4))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h3,h4))
=======================================================
leftof(h3,h4)
?- kif_to_boxlog( leftof(h3,h4) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ h3 leftof h4
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kifi=leftof(h3,h4)
%~ kifm=nesc(leftof(h3,h4))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h3,h4))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(leftof(h3,h4)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that h3 leftof h4
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( leftof(h3,h4)).
============================================
~*/
leftof(h4, h5).
% makes the KB non-monotonic
%~ kifi = leftof(h4,h5).
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl:28
%~ kifm = nesc( leftof(h4,h5)).
%~ kifm = nesc( leftof(h4,h5)).
%~ debugm(common_logic_loader,show_success(common_logic_loader,common_logic_loader:ain(clif(leftof(h4,h5)))))
%~ kifi = leftof(h4,h5).
%~ kifm = nesc( leftof(h4,h5)).
/*~
%~ kifi=leftof(h4,h5)
%~ kifm=nesc(leftof(h4,h5))
%~ kifm=nesc(leftof(h4,h5))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h4,h5))
=======================================================
leftof(h4,h5)
?- kif_to_boxlog( leftof(h4,h5) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ h4 leftof h5
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kifi=leftof(h4,h5)
%~ kifm=nesc(leftof(h4,h5))
%~ kif_to_boxlog_attvars2 = necessary(leftof(h4,h5))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(leftof(h4,h5)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that h4 leftof h5
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( leftof(h4,h5)).
============================================
~*/
% makes the KB non-monotonic
:- set_kif_option(qualify_modality,false).
% this should cause h1-h5 to become houses
% this should cause h1-h5 to become houses
leftof(H1, H2) => house(H1) & house(H2).
% intractive_test/1 means only run if interactive
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl:35
%~ kifm = ( leftof(House_Leftof,House_Leftof3) =>
%~ house(House_Leftof)&house(House_Leftof3)).
%~ kifm = ( leftof(House_Leftof8,House_Leftof9) =>
%~ house(House_Leftof8)&house(House_Leftof9)).
%~ debugm( common_logic_loader,
%~ show_success( common_logic_loader,
%~ common_logic_loader : ain( clif( leftof(H1,H2)=>(house(H1)&house(H2))))))
%~ kifm = ( leftof(House_Leftof,House_Leftof3) =>
%~ house(House_Leftof)&house(House_Leftof3)).
%~ kifm = leftof(H1,H2)=>(house(H1)&house(H2)).
/*~
%~ kifm=leftof(House_Leftof,House_Leftof3)=>(house(House_Leftof)&house(House_Leftof3))
%~ kifm=leftof(House_Leftof8,House_Leftof9)=>(house(House_Leftof8)&house(House_Leftof9))
%~ kif_to_boxlog_attvars2 = =>(leftof('$VAR'('House_Leftof8'),'$VAR'('House_Leftof9')),and(house('$VAR'('House_Leftof8')),house('$VAR'('House_Leftof9'))))
=======================================================
=>(leftof('$VAR'('House_Leftof'),'$VAR'('House_Leftof3')),&(house('$VAR'('House_Leftof')),house('$VAR'('House_Leftof3'))))
?- kif_to_boxlog( leftof(House_Leftof,House_Leftof3)=>(house(House_Leftof)&house(House_Leftof3)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ If:
%~ ?House_Leftof leftof ?House_Leftof3 then it is
%~ Implied that:
%~ " ?House_Leftof isa house " and
%~ " ?House_Leftof3 isa house "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kifm=leftof(House_Leftof,House_Leftof3)=>(house(House_Leftof)&house(House_Leftof3))
%~ kif_to_boxlog_attvars2 = =>(leftof('$VAR'('House_Leftof'),'$VAR'('House_Leftof3')),and(house('$VAR'('House_Leftof')),house('$VAR'('House_Leftof3'))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 6 entailment(s):
nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof))==>nesc(~house(House_Leftof3)).
nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof3))==>nesc(~house(House_Leftof)).
nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof))==>nesc(house(House_Leftof3)).
nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof3))==>nesc(house(House_Leftof)).
poss(house(House_Leftof))&nesc(~house(House_Leftof3))==>nesc(~leftof(House_Leftof,House_Leftof3)).
poss(house(House_Leftof3))&nesc(~house(House_Leftof))==>nesc(~leftof(House_Leftof,House_Leftof3)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and
%~ " ?House_Leftof isa house " is necessarily false
%~ It's Proof that:
%~ " ?House_Leftof3 isa house " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof)) ==>
nesc( ~( house(House_Leftof3)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and
%~ " ?House_Leftof3 isa house " is necessarily false
%~ It's Proof that:
%~ " ?House_Leftof isa house " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof3)) ==>
nesc( ~( house(House_Leftof)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and
%~ " ?House_Leftof isa house " is possible
%~ It's Proof that:
%~ " ?House_Leftof3 isa house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof)) ==>
nesc( house(House_Leftof3))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and
%~ " ?House_Leftof3 isa house " is possible
%~ It's Proof that:
%~ " ?House_Leftof isa house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof3)) ==>
nesc( house(House_Leftof))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof isa house " is possible and
%~ " ?House_Leftof3 isa house " is necessarily false
%~ It's Proof that:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( poss(house(House_Leftof))&nesc(~house(House_Leftof3)) ==>
nesc( ~( leftof(House_Leftof,House_Leftof3)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?House_Leftof3 isa house " is possible and
%~ " ?House_Leftof isa house " is necessarily false
%~ It's Proof that:
%~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( poss(house(House_Leftof3))&nesc(~house(House_Leftof)) ==>
nesc( ~( leftof(House_Leftof,House_Leftof3)))).
============================================%~ kifm=leftof(H1,H2)=>(house(H1)&house(H2))
%~ kif_to_boxlog_attvars2 = =>(leftof('$VAR'('H1'),'$VAR'('H2')),and(house('$VAR'('H1')),house('$VAR'('H2'))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H2 isa house " is possible and
%~ " ?H1 isa house " is necessarily false
%~ It's Proof that:
%~ " ?H1 leftof ?H2 " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(house(H2))&nesc(~house(H1))==>nesc(~leftof(H1,H2)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H1 leftof ?H2 " is necessarily true and
%~ " ?H1 isa house " is necessarily false
%~ It's Proof that:
%~ " ?H2 isa house " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(leftof(H1,H2))&nesc(~house(H1))==>nesc(~house(H2)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H1 leftof ?H2 " is necessarily true and
%~ " ?H2 isa house " is possible
%~ It's Proof that:
%~ " ?H1 isa house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(leftof(H1,H2))&poss(house(H2))==>nesc(house(H1)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H1 isa house " is possible and
%~ " ?H2 isa house " is necessarily false
%~ It's Proof that:
%~ " ?H1 leftof ?H2 " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(house(H1))&nesc(~house(H2))==>nesc(~leftof(H1,H2)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H1 leftof ?H2 " is necessarily true and
%~ " ?H2 isa house " is necessarily false
%~ It's Proof that:
%~ " ?H1 isa house " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(leftof(H1,H2))&nesc(~house(H2))==>nesc(~house(H1)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?H1 leftof ?H2 " is necessarily true and
%~ " ?H1 isa house " is possible
%~ It's Proof that:
%~ " ?H2 isa house " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(leftof(H1,H2))&poss(house(H1))==>nesc(house(H2)).
~*/
% intractive_test/1 means only run if interactive
:- interactive_test(listing(kif_show)).
% mpred_test/1 each become a Junit test that must succeed
/*~
0m1m97m40m?- listing(kif_show).49m0m21m0m
~*/
% mpred_test/1 each become a Junit test that must succeed
:- mpred_test(listing(nesc)).
% ensure our rule worked
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_01.pl:41
%~ mpred_test("Test_0001_Line_0000__Nesc",baseKB:listing(nesc))
goal=baseKB:listing(nesc).
time=0.00638270378112793.
passed=passed=info(why_was_true(baseKB:listing(nesc)))
no_proof_for(listing(nesc)).
:- dynamic nesc/1.
:- multifile nesc/1.
:- public nesc/1.
:- module_transparent nesc/1.
nesc(A) :-
zwc,
nesc_lc(baseKB, A).
nesc(leftof(h1, h2)).
nesc(leftof(h2, h3)).
nesc(leftof(h3, h4)).
nesc(leftof(h4, h5)).
nesc(house(h1)).
nesc(house(h2)).
nesc(house(h3)).
nesc(house(h4)).
nesc(house(h5)).
:- public nesc/2.
:- module_transparent nesc/2.
nesc(_M, isNamed(X, Y)) :-
!,
isNamed_impl(X, Y),
!.
nesc(A, B) :-
swc,
first_of([ (loop_check_term(A:proven_tru(B), info(A:proven_tru(B), 'common_logic_exists.pl':318), fail), nop(nrlc0(call(call, +A:proven_neg(B))))),
(A:proven_helper(B), +A:proven_helper(~B)),
A:skolem_tru(B)
]).
no_proof_for(listing(nesc)).
no_proof_for(listing(nesc)).
result=passed.
]]>