logicmoo_workspace
logicmoo_workspace copied to clipboard
Published
20 hours ago •
logicmoo
logicmoo
logicmoo.base.fol.fiveof.FIVE_LEFTOF_SKOLLEM_02 JUnit
trafficstars
(cd /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/fiveof ; timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "['five_leftof_skollem_02.pl']")
% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_skollem_02.pl % JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.fol.fiveof/FIVE_LEFTOF_SKOLLEM_02/ % ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3AFIVE_LEFTOF_SKOLLEM_02 % ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/620
%~ 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/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_skollem_02.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 [email protected] %
% Version: 'interface' 1.0.0
% Revision: $Revision: 1.9 $
% Revised At: $Date: 2002/06/27 14:13:20 $
% =============================================
%
:- expects_dialect(clif).
/*~
~*/
:- set_prolog_flag(gc,false).
% 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))))))).
% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_skollem_02.pl
% JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.fol.fiveof/FIVE_LEFTOF_SKOLLEM_02/logicmoo_base_fol_fiveof_FIVE_LEFTOF_SKOLLEM_02_JUnit/
% ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3AFIVE_LEFTOF_SKOLLEM_02
% ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/620
/*~
%~ 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)))))))))))
% 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: 1597 words .. **
** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/lex.xg: 357 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.27 sec, 3 clauses
% /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/debuggery/dmsg compiled into dmsg 0.12 sec, -16 clauses
=======================================================
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 " and
%~ " ?Exists_Leftof6 leftof ?Exists_Leftof7 " ) and
%~ " ?Exists_Leftof7 leftof ?Exists_Leftof8 " ) and
%~ " ?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(and(and(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')))))))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 6 entailment(s):
(((nesc(leftof(Exists_Leftof,Exists_Leftof6))&'$existential'(Exists_Leftof6,1,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))))&'$existential'(Exists_Leftof7,1,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))))&'$existential'(Exists_Leftof8,1,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))&'$existential'(Leftof13,1,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))==>nesc(leftof(Exists_Leftof6,Exists_Leftof7)).
(((poss(~leftof(Exists_Leftof,Exists_Leftof6))&'$existential'(Exists_Leftof6,1,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))))&'$existential'(Exists_Leftof7,1,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))))&'$existential'(Exists_Leftof8,1,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))&'$existential'(Leftof13,1,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))==>poss(~leftof(Exists_Leftof6,Exists_Leftof7)).
((((nesc(leftof(Exists_Leftof6,Exists_Leftof7))&'$existential'(Exists_Leftof,1,exists(Exists_Leftof6,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))))))&'$existential'(Exists_Leftof6,1,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))))&'$existential'(Exists_Leftof7,1,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))))&'$existential'(Exists_Leftof8,1,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))&'$existential'(Leftof13,1,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))==>nesc(leftof(Exists_Leftof,Exists_Leftof6)).
((((poss(~leftof(Exists_Leftof6,Exists_Leftof7))&'$existential'(Exists_Leftof,1,exists(Exists_Leftof6,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))))))&'$existential'(Exists_Leftof6,1,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))))&'$existential'(Exists_Leftof7,1,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))))&'$existential'(Exists_Leftof8,1,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))&'$existential'(Leftof13,1,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))==>poss(~leftof(Exists_Leftof,Exists_Leftof6)).
('$existential'(Exists_Leftof7,1,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))&'$existential'(Exists_Leftof8,1,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))&'$existential'(Leftof13,1,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))==>nesc(leftof(Exists_Leftof7,Exists_Leftof8)).
'$existential'(Exists_Leftof8,1,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))&'$existential'(Leftof13,1,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))==>nesc(leftof(Exists_Leftof8,Leftof13)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true and
%~ by default ?Exists_Leftof6 exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))) ) and
%~ by default ?Exists_Leftof7 exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))) ) and
%~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) ) and
%~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))
%~ It's Proof that:
%~ " ?Exists_Leftof6 leftof ?Exists_Leftof7 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
'$existential'( Exists_Leftof6,
1,
exists( Exists_Leftof7,
exists( Exists_Leftof8,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))))) &
'$existential'( Exists_Leftof7,
1,
exists( Exists_Leftof8,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13)))))) &
'$existential'( Exists_Leftof8,
1,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) &
'$existential'( Leftof13,
1,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) ==>
nesc( leftof(Exists_Leftof6,Exists_Leftof7))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?Exists_Leftof leftof ?Exists_Leftof6 " is possibly false and
%~ by default ?Exists_Leftof6 exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))) ) and
%~ by default ?Exists_Leftof7 exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))) ) and
%~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) ) and
%~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))
%~ It's Proof that:
%~ " ?Exists_Leftof6 leftof ?Exists_Leftof7 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( leftof(Exists_Leftof,Exists_Leftof6))) &
'$existential'( Exists_Leftof6,
1,
exists( Exists_Leftof7,
exists( Exists_Leftof8,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))))) &
'$existential'( Exists_Leftof7,
1,
exists( Exists_Leftof8,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13)))))) &
'$existential'( Exists_Leftof8,
1,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) &
'$existential'( Leftof13,
1,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) ==>
poss( ~( leftof(Exists_Leftof6,Exists_Leftof7)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((((" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is necessarily true and
%~ by default ?Exists_Leftof exists(Exists_Leftof6,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))) ) and
%~ by default ?Exists_Leftof6 exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))) ) and
%~ by default ?Exists_Leftof7 exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))) ) and
%~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) ) and
%~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))
%~ It's Proof that:
%~ " ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
'$existential'( Exists_Leftof,
1,
exists( Exists_Leftof6,
exists( Exists_Leftof7,
exists( Exists_Leftof8,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13)))))))) &
'$existential'( Exists_Leftof6,
1,
exists( Exists_Leftof7,
exists( Exists_Leftof8,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))))) &
'$existential'( Exists_Leftof7,
1,
exists( Exists_Leftof8,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13)))))) &
'$existential'( Exists_Leftof8,
1,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) &
'$existential'( Leftof13,
1,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) ==>
nesc( leftof(Exists_Leftof,Exists_Leftof6))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((((" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is possibly false and
%~ by default ?Exists_Leftof exists(Exists_Leftof6,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))) ) and
%~ by default ?Exists_Leftof6 exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))) ) and
%~ by default ?Exists_Leftof7 exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))) ) and
%~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) ) and
%~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))
%~ It's Proof that:
%~ " ?Exists_Leftof leftof ?Exists_Leftof6 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( leftof(Exists_Leftof6,Exists_Leftof7))) &
'$existential'( Exists_Leftof,
1,
exists( Exists_Leftof6,
exists( Exists_Leftof7,
exists( Exists_Leftof8,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13)))))))) &
'$existential'( Exists_Leftof6,
1,
exists( Exists_Leftof7,
exists( Exists_Leftof8,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))))) &
'$existential'( Exists_Leftof7,
1,
exists( Exists_Leftof8,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13)))))) &
'$existential'( Exists_Leftof8,
1,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) &
'$existential'( Leftof13,
1,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) ==>
poss( ~( leftof(Exists_Leftof,Exists_Leftof6)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ( by default ?Exists_Leftof7 exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))) and
%~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) ) and
%~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))
%~ It's Proof that:
%~ " ?Exists_Leftof7 leftof ?Exists_Leftof8 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( '$existential'( Exists_Leftof7,
1,
exists( Exists_Leftof8,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13)))))) &
'$existential'( Exists_Leftof8,
1,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) &
'$existential'( Leftof13,
1,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) ==>
nesc( leftof(Exists_Leftof7,Exists_Leftof8))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) and
%~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))
%~ It's Proof that:
%~ " ?Exists_Leftof8 leftof ?Leftof13 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( '$existential'( Exists_Leftof8,
1,
exists( Leftof13,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) &
'$existential'( Leftof13,
1,
( nesc( leftof(Exists_Leftof,Exists_Leftof6)) &
nesc( leftof(Exists_Leftof6,Exists_Leftof7)) &
nesc( leftof(Exists_Leftof7,Exists_Leftof8)) &
nesc( leftof(Exists_Leftof8,Leftof13))))) ==>
nesc( leftof(Exists_Leftof8,Leftof13))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('H1'),exists('$VAR'('H2'),exists('$VAR'('H3'),exists('$VAR'('H4'),exists('$VAR'('H5'),necessary(and(and(and(leftof('$VAR'('H1'),'$VAR'('H2')),leftof('$VAR'('H2'),'$VAR'('H3'))),leftof('$VAR'('H3'),'$VAR'('H4'))),leftof('$VAR'('H4'),'$VAR'('H5')))))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) and
%~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))
%~ It's Proof that:
%~ " ?H4 leftof ?H5 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( '$existential'( H4,
1,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) &
'$existential'( H5,
1,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) ==>
nesc( leftof(H4,H5))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ( by default ?H3 exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))) and
%~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) ) and
%~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))
%~ It's Proof that:
%~ " ?H3 leftof ?H4 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( '$existential'( H3,
1,
exists( H4,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5)))))) &
'$existential'( H4,
1,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) &
'$existential'( H5,
1,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) ==>
nesc( leftof(H3,H4))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?H1 leftof ?H2 " is possibly false and
%~ by default ?H2 exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))))) ) and
%~ by default ?H3 exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))) ) and
%~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) ) and
%~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))
%~ It's Proof that:
%~ " ?H2 leftof ?H3 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( leftof(H1,H2))) &
'$existential'( H2,
1,
exists( H3,
exists( H4,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))))) &
'$existential'( H3,
1,
exists( H4,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5)))))) &
'$existential'( H4,
1,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) &
'$existential'( H5,
1,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) ==>
poss( ~( leftof(H2,H3)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((((" ?H2 leftof ?H3 " is necessarily true and
%~ by default ?H1 exists(H2,exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))))) ) and
%~ by default ?H2 exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))))) ) and
%~ by default ?H3 exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))) ) and
%~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) ) and
%~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))
%~ It's Proof that:
%~ " ?H1 leftof ?H2 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( leftof(H2,H3)) &
'$existential'( H1,
1,
exists( H2,
exists( H3,
exists( H4,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5)))))))) &
'$existential'( H2,
1,
exists( H3,
exists( H4,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))))) &
'$existential'( H3,
1,
exists( H4,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5)))))) &
'$existential'( H4,
1,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) &
'$existential'( H5,
1,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) ==>
nesc( leftof(H1,H2))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((((" ?H2 leftof ?H3 " is possibly false and
%~ by default ?H1 exists(H2,exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))))) ) and
%~ by default ?H2 exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))))) ) and
%~ by default ?H3 exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))) ) and
%~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) ) and
%~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))
%~ It's Proof that:
%~ " ?H1 leftof ?H2 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( leftof(H2,H3))) &
'$existential'( H1,
1,
exists( H2,
exists( H3,
exists( H4,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5)))))))) &
'$existential'( H2,
1,
exists( H3,
exists( H4,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))))) &
'$existential'( H3,
1,
exists( H4,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5)))))) &
'$existential'( H4,
1,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) &
'$existential'( H5,
1,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) ==>
poss( ~( leftof(H1,H2)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (((" ?H1 leftof ?H2 " is necessarily true and
%~ by default ?H2 exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))))) ) and
%~ by default ?H3 exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))) ) and
%~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) ) and
%~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))
%~ It's Proof that:
%~ " ?H2 leftof ?H3 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( leftof(H1,H2)) &
'$existential'( H2,
1,
exists( H3,
exists( H4,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))))) &
'$existential'( H3,
1,
exists( H4,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5)))))) &
'$existential'( H4,
1,
exists( H5,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) &
'$existential'( H5,
1,
( nesc( leftof(H1,H2)) &
nesc( leftof(H2,H3)) &
nesc( leftof(H3,H4)) &
nesc( leftof(H4,H5))))) ==>
nesc( leftof(H2,H3))).
~*/
%~ unused(no_junit_results)
%~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_skollem_02.pl:28
%~ test_completed_exit(0)
totalTime=5.000
FAILED: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k five_leftof_skollem_02.pl (returned 0) Add_LABELS='' Rem_LABELS='Skipped,Skipped,Errors,Warnings,Overtime,Skipped,Skipped'
