|
|
Duration | 0.0 sec |
---|---|
Tests | 1 |
Failures | 0 |
Test case: | logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01@Test_0001_Line_0000__True_in_user: user:true |
---|---|
Outcome: | Passed |
Duration: | 0.0 sec |
Failed | None |
None
name=Test_0001_Line_0000__True_in_user JUNIT_CLASSNAME='logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'five_leftof_type_01.pl\']"'. (cd /var/lib/jenkins/workspace/logicmoo_workspace@2/back_sys/logicmoo_base/t/examples/fol/quick_test ; timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "['five_leftof_type_01.pl']") ``` goal=user:true. time=0.0007140636444091797. passed=passed=info(why_was_true(user:true)) no_proof_for(true). no_proof_for(true). no_proof_for(true). result=passed.
Duration | 1.1 sec |
---|---|
Tests | 1 |
Failures | 0 |
Test case: | logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01@Test_0002_Line_0000__Kif_compile_in_user: user:kif_compile |
---|---|
Outcome: | Passed |
Duration: | 0.4 sec |
Failed | None |
None
name=Test_0002_Line_0000__Kif_compile_in_user JUNIT_CLASSNAME='logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'five_leftof_type_01.pl\']"'. (cd /var/lib/jenkins/workspace/logicmoo_workspace@2/back_sys/logicmoo_base/t/examples/fol/quick_test ; timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "['five_leftof_type_01.pl']") ``` Warning: import/1: parser_lexical_plkb:(cyc_lex/1) is not exported (still imported into system) %~ init_phase(after_load). %~ init_phase(restore_state). % %~ init_why(after_boot,program). %~ READONLY PACKAGES %~ READONLY PACKAGES %~ READONLY PACKAGES %~ after_boot. %~ Dont forget to ?- logicmoo_i_cyc_xform. %~ skipped(blocks_on_input,prolog). running('/var/lib/jenkins/workspace/logicmoo_workspace@2/back_sys/logicmoo_base/t/examples/fol/quick_test/five_leftof_type_01.pl'), %~ this_test_might_need((:-expects_dialect(pfc))). %~ this_test_might_need((:-use_module(library(logicmoo_plarkc)))). % ============================================= % File 'mpred_builtin.pfc' % Purpose: Agent Reactivity for SWI-Prolog % Maintainer: Douglas Miles % Contact: $Author: dmiles $@users.sourceforge.net % % Version: 'interface' 1.0.0 % Revision: $Revision: 1.9 $ % Revised At: $Date: 2002/06/27 14:13:20 $ % ============================================= % :- mpred_test(true). % There are five houses in a row. /*~ %~ ?-mpred_test("Test_0001_Line_0000__True_in_user",user:true). passed=info(why_was_true(user:true)) no_proof_for(true). no_proof_for(true). no_proof_for(true). name='logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01-Test_0001_Line_0000__True_in_user'. JUNIT_CLASSNAME='logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'five_leftof_type_01.pl\']"'. % saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace@2/test_results/jenkins/Report-logicmoo-base-fol-quick_test-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_fol_quick_test_FIVE_LEFTOF_TYPE_01_Test_0001_Line_0000_True_in_user-junit.xml ~*/ % There are five houses in a row. :- nop(module( baseKB)). % makes the KB monotonic /*~ ~*/ % makes the KB monotonic :- set_kif_option(qualify_modality,simple_nesc). /*~ ~*/ leftof(h1, h2). /*~ %~ debugm(user,show_success(user,user:ain(clif(leftof(h1,h2))))). ======================================================= leftof(h1,h2) ============================================ ?- kif_to_boxlog( leftof(h1,h2) ). % In English: %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ h1 leftof h2 %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ kifi=leftof(h1,h2). %~ kifm=nesc(leftof(h1,h2)). %~ kif_to_boxlog_attvars2 = necessary(leftof(h1,h2)) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results in the following 1 entailment(s): nesc(leftof(h1,h2)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ it is necessarily true that h1 leftof h2 %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% nesc(leftof(h1,h2)). . ============================================ ~*/ leftof(h2, h3). /*~ %~ /var/lib/jenkins/workspace/logicmoo_workspace@2/back_sys/logicmoo_base/t/examples/fol/quick_test/five_leftof_type_01.pl:22 %~ debugm(user,show_success(user,user:ain(clif(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). /*~ %~ debugm(user,show_success(user,user:ain(clif(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). % this should cause h1-h5 to become houses /*~ %~ debugm(user,show_success(user,user:ain(clif(leftof(h4,h5))))). ======================================================= leftof(h4,h5) ============================================ ?- kif_to_boxlog( leftof(h4,h5) ). % In English: %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ h4 leftof h5 %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ kifi=leftof(h4,h5). %~ /var/lib/jenkins/workspace/logicmoo_workspace@2/back_sys/logicmoo_base/t/examples/fol/quick_test/five_leftof_type_01.pl:24 %~ 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)). . ============================================ ~*/ % this should cause h1-h5 to become houses leftof(H1, H2) => house(H1) & house(H2). /*~ %~ debugm(user,show_success(user,user:ain(clif((leftof(_590908,_590930)=>house(_590908)&house(_590930)))))). ======================================================= =>(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 " %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ /var/lib/jenkins/workspace/logicmoo_workspace@2/back_sys/logicmoo_base/t/examples/fol/quick_test/five_leftof_type_01.pl:27 %~ 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)). . ~*/ :- mpred_test(kif_compile). % intractive_test/1 means only run if inter goal=user:kif_compile. time=0.39657068252563477. passed=passed=info(why_was_true(user:kif_compile)) no_proof_for(kif_compile). no_proof_for(kif_compile). no_proof_for(kif_compile). result=passed.
Duration | 0.0 sec |
---|---|
Tests | 1 |
Failures | 0 |
Test case: | logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01@Test_0003_Line_0000__Pfclog_compile_in_user: user:pfclog_compile |
---|---|
Outcome: | Passed |
Duration: | 0.0 sec |
Failed | None |
None
name=Test_0003_Line_0000__Pfclog_compile_in_user JUNIT_CLASSNAME='logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'five_leftof_type_01.pl\']"'. (cd /var/lib/jenkins/workspace/logicmoo_workspace@2/back_sys/logicmoo_base/t/examples/fol/quick_test ; timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "['five_leftof_type_01.pl']") ``` Warning: import/1: parser_lexical_plkb:(cyc_lex/1) is not exported (still imported into system) %~ init_phase(after_load). %~ init_phase(restore_state). % %~ init_why(after_boot,program). %~ READONLY PACKAGES %~ READONLY PACKAGES %~ READONLY PACKAGES %~ after_boot. %~ Dont forget to ?- logicmoo_i_cyc_xform. %~ skipped(blocks_on_input,prolog). running('/var/lib/jenkins/workspace/logicmoo_workspace@2/back_sys/logicmoo_base/t/examples/fol/quick_test/five_leftof_type_01.pl'), %~ this_test_might_need((:-expects_dialect(pfc))). %~ this_test_might_need((:-use_module(library(logicmoo_plarkc)))). % ============================================= % File 'mpred_builtin.pfc' % Purpose: Agent Reactivity for SWI-Prolog % Maintainer: Douglas Miles % Contact: $Author: dmiles $@users.sourceforge.net % % Version: 'interface' 1.0.0 % Revision: $Revision: 1.9 $ % Revised At: $Date: 2002/06/27 14:13:20 $ % ============================================= % :- mpred_test(true). % There are five houses in a row. /*~ %~ ?-mpred_test("Test_0001_Line_0000__True_in_user",user:true). passed=info(why_was_true(user:true)) no_proof_for(true). no_proof_for(true). no_proof_for(true). name='logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01-Test_0001_Line_0000__True_in_user'. JUNIT_CLASSNAME='logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'five_leftof_type_01.pl\']"'. % saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace@2/test_results/jenkins/Report-logicmoo-base-fol-quick_test-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_fol_quick_test_FIVE_LEFTOF_TYPE_01_Test_0001_Line_0000_True_in_user-junit.xml ~*/ % There are five houses in a row. :- nop(module( baseKB)). % makes the KB monotonic /*~ ~*/ % makes the KB monotonic :- set_kif_option(qualify_modality,simple_nesc). /*~ ~*/ leftof(h1, h2). /*~ %~ debugm(user,show_success(user,user:ain(clif(leftof(h1,h2))))). ======================================================= leftof(h1,h2) ============================================ ?- kif_to_boxlog( leftof(h1,h2) ). % In English: %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ h1 leftof h2 %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ kifi=leftof(h1,h2). %~ kifm=nesc(leftof(h1,h2)). %~ kif_to_boxlog_attvars2 = necessary(leftof(h1,h2)) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results in the following 1 entailment(s): nesc(leftof(h1,h2)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ it is necessarily true that h1 leftof h2 %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% nesc(leftof(h1,h2)). . ============================================ ~*/ leftof(h2, h3). /*~ %~ /var/lib/jenkins/workspace/logicmoo_workspace@2/back_sys/logicmoo_base/t/examples/fol/quick_test/five_leftof_type_01.pl:22 %~ debugm(user,show_success(user,user:ain(clif(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). /*~ %~ debugm(user,show_success(user,user:ain(clif(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). % this should cause h1-h5 to become houses /*~ %~ debugm(user,show_success(user,user:ain(clif(leftof(h4,h5))))). ======================================================= leftof(h4,h5) ============================================ ?- kif_to_boxlog( leftof(h4,h5) ). % In English: %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ h4 leftof h5 %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ kifi=leftof(h4,h5). %~ /var/lib/jenkins/workspace/logicmoo_workspace@2/back_sys/logicmoo_base/t/examples/fol/quick_test/five_leftof_type_01.pl:24 %~ 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)). . ============================================ ~*/ % this should cause h1-h5 to become houses leftof(H1, H2) => house(H1) & house(H2). /*~ %~ debugm(user,show_success(user,user:ain(clif((leftof(_590908,_590930)=>house(_590908)&house(_590930)))))). ======================================================= =>(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 " %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ /var/lib/jenkins/workspace/logicmoo_workspace@2/back_sys/logicmoo_base/t/examples/fol/quick_test/five_leftof_type_01.pl:27 %~ 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)). . ~*/ :- mpred_test(kif_compile). % intractive_test/1 means only run if inter goal=user:pfclog_compile. time=0.0013432502746582031. passed=passed=info(why_was_true(user:pfclog_compile)) no_proof_for(pfclog_compile). no_proof_for(pfclog_compile). no_proof_for(pfclog_compile). result=passed.