![[Jenkins]](/jenkins/static/f0d9078a/images/svgs/logo.svg){kind=logo}
Failed
logicmoo.base.fol.fiveof.FIVE_LEFTOF_02.logicmoo.base.fol.fiveof.FIVE_LEFTOF_02@Test_0001_Line_0004__leftof_2_in_user: user: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)))))) (from logicmoo.base.fol.fiveof.logicmoo.base.fol.fiveof.FIVE_LEFTOF_02)
Error Message
failure = "failure=info((why_was_true(user:(\\+exists(_42392914,exists(_42392936,exists(_42392958,exists(_42392980,exists(_42393002,leftof(_42392914,_42392936)&leftof(_42392936,_42392958)&leftof(_42392958,_42392980)&leftof(_42392980,_42393002)))))))),nop(ftrace(user:exists(_42392914,exists(_42392936,exists(_42392958,exists(_42392980,exists(_42393002,leftof(_42392914,_42392936)&leftof(_42392936,_42392958)&leftof(_42392958,_42392980)&leftof(_42392980,_42393002))))))))))\nno_proof_for(\\+exists(H1,exists(H2,exists(H3,exists(H4,exists(H5,leftof(H1,H2)&leftof(H2,H3)&leftof(H3,H4)&leftof(H4,H5))))))).\n\nno_proof_for(\\+exists(H1,exists(H2,exists(H3,exists(H4,exists(H5,leftof(H1,H2)&leftof(H2,H3)&leftof(H3,H4)&leftof(H4,H5))))))).\n\nno_proof_for(\\+exists(H1,exists(H2,exists(H3,exists(H4,exists(H5,leftof(H1,H2)&leftof(H2,H3)&leftof(H3,H4)&leftof(H4,H5))))))).\n\n". failure = [].
Standard Error
name=Test_0001_Line_0004__leftof_2_in_user
JUNIT_CLASSNAME='logicmoo.base.fol.fiveof.FIVE_LEFTOF_02'.
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_02.pl\']"'.
(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_02.pl']")
```
%~ 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_02.pl'),
%~ this_test_might_need( :-( expects_dialect(pfc)))
%~ /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test_header.pl:96
%~ 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 $
% =============================================
%
:- 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))))))).
/*~
%~ debugm( user,
%~ show_success( user,
%~ user : ain( clif( exists( H1,
%~ exists( H2,
%~ exists( H3,
%~ exists( H4,
%~ exists( H5,
%~ ( leftof(H1,H2) &
%~ leftof(H2,H3) &
%~ leftof(H3,H4) &
%~ leftof(H4,H5)))))))))))
=======================================================
exists('$VAR'('Exists_Leftof'),exists('$VAR'('Exists_Leftof6'),exists('$VAR'('Exists_Leftof7'),exists('$VAR'('Exists_Leftof8'),exists('$VAR'('Leftof13'),&(&(&(leftof('$VAR'('Exists_Leftof'),'$VAR'('Exists_Leftof6')),leftof('$VAR'('Exists_Leftof6'),'$VAR'('Exists_Leftof7'))),leftof('$VAR'('Exists_Leftof7'),'$VAR'('Exists_Leftof8'))),leftof('$VAR'('Exists_Leftof8'),'$VAR'('Leftof13'))))))))
============================================
?- kif_to_boxlog( exists(Exists_Leftof,exists(Exists_Leftof6,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,leftof(Exists_Leftof,Exists_Leftof6)&leftof(Exists_Leftof6,Exists_Leftof7)&leftof(Exists_Leftof7,Exists_Leftof8)&leftof(Exists_Leftof8,Leftof13)))))) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Exists_Leftof
%~ (
%~ There exists ?Exists_Leftof6
%~ (
%~ There exists ?Exists_Leftof7
%~ (
%~ There exists ?Exists_Leftof8
%~ (
%~ There exists ?Leftof13
%~ (((" ?Exists_Leftof leftof ?Exists_Leftof6 " and
%~ " ?Exists_Leftof6 leftof ?Exists_Leftof7 " ) and
%~ " ?Exists_Leftof7 leftof ?Exists_Leftof8 " ) and
%~ " ?Exists_Leftof8 leftof ?Leftof13 " )))))
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kifi = 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))))))).
%~ kifm = exists( Exists_Leftof,
%~ exists( Exists_Leftof6,
%~ exists( Exists_Leftof7,
%~ exists( Exists_Leftof8,
%~ exists( Leftof13,
%~ nesc( ( leftof(Exists_Leftof,Exists_Leftof6) &
%~ leftof(Exists_Leftof6,Exists_Leftof7) &
%~ leftof(Exists_Leftof7,Exists_Leftof8) &
%~ leftof(Exists_Leftof8,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))).
============================================
%~ kifi = exists( H1,
%~ exists( H2,
%~ exists( H3,
%~ exists( H4,
%~ exists( H5,
%~ ( leftof(H1,H2) &
%~ leftof(H2,H3) &
%~ leftof(H3,H4) &
%~ leftof(H4,H5))))))).
%~ kifm = exists( H1,
%~ exists( H2,
%~ exists( H3,
%~ exists( H4,
%~ exists( H5,
%~ nesc( ( leftof(H1,H2) &
%~ leftof(H2,H3) &
%~ leftof(H3,H4) &
%~ leftof(H4,H5)))))))).
%~ 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))).
~*/
:- include(leftof_tests).
% ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/472
% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_02.pl
% JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.fol.fiveof/FIVE_LEFTOF_02/
% ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3AFIVE_LEFTOF_02
/*~
%~ ?-( mpred_test( "Test_0001_Line_0004__leftof_2_in_user",
%~ user : exists( H1,
%~ exists( H2,
%~ exists( H3,
%~ exists( H4,
%~ exists( H5,
%~ ( leftof(H1,H2) &
%~ leftof(H2,H3) &
%~ leftof(H3,H4) &
%~ leftof(H4,H5))))))))).
%~ make_dynamic_here( baseKB,
%~ exists( H1,
%~ exists( H2,
%~ exists( H3,
%~ exists( H4,
%~ exists( H5,
%~ ( leftof(H1,H2) &
%~ leftof(H2,H3) &
%~ leftof(H3,H4) &
%~ leftof(H4,H5))))))))
failure=info((why_was_true(user:(\+exists(_42392914,exists(_42392936,exists(_42392958,exists(_42392980,exists(_42393002,leftof(_42392914,_42392936)&leftof(_42392936,_42392958)&leftof(_42392958,_42392980)&leftof(_42392980,_42393002)))))))),nop(ftrace(user:exists(_42392914,exists(_42392936,exists(_42392958,exists(_42392980,exists(_42393002,leftof(_42392914,_42392936)&leftof(_42392936,_423929
goal=user:exists(_42501278,exists(_42501284,exists(_42501290,exists(_42501296,exists(_42501302,leftof(_42501278,_42501284)&leftof(_42501284,_42501290)&leftof(_42501290,_42501296)&leftof(_42501296,_42501302)))))).
src='/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/fiveof/leftof_tests.pl':4.
url=/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/fiveof/leftof_tests.pl#L4
time=0.006494045257568359.
failure=failure=info((why_was_true(user:(\+exists(_42392914,exists(_42392936,exists(_42392958,exists(_42392980,exists(_42393002,leftof(_42392914,_42392936)&leftof(_42392936,_42392958)&leftof(_42392958,_42392980)&leftof(_42392980,_42393002)))))))),nop(ftrace(user:exists(_42392914,exists(_42392936,exists(_42392958,exists(_42392980,exists(_42393002,leftof(_42392914,_42392936)&leftof(_42392936,_42392958)&leftof(_42392958,_42392980)&leftof(_42392980,_42393002))))))))))
no_proof_for(\+exists(H1,exists(H2,exists(H3,exists(H4,exists(H5,leftof(H1,H2)&leftof(H2,H3)&leftof(H3,H4)&leftof(H4,H5))))))).
no_proof_for(\+exists(H1,exists(H2,exists(H3,exists(H4,exists(H5,leftof(H1,H2)&leftof(H2,H3)&leftof(H3,H4)&leftof(H4,H5))))))).
no_proof_for(\+exists(H1,exists(H2,exists(H3,exists(H4,exists(H5,leftof(H1,H2)&leftof(H2,H3)&leftof(H3,H4)&leftof(H4,H5))))))).
result=failure.