Test Report : Report-logicmoo-base-fol-quick_test-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-junitCombined-rollup.tmp

Test Suite: logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01

Package: logicmoo.base.fol.quick_test

Results

Duration0.0 sec
Tests1
Failures0

Tests

logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01

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
FailedNone
None
Stderr
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.

Test Suite: logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01

Package: logicmoo.base.fol.quick_test

Results

Duration1.1 sec
Tests1
Failures0

Tests

logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01

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
FailedNone
None
Stderr
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.

Test Suite: logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01

Package: logicmoo.base.fol.quick_test

Results

Duration0.0 sec
Tests1
Failures0

Tests

logicmoo.base.fol.quick_test.FIVE_LEFTOF_TYPE_01

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
FailedNone
None
Stderr
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.