logicmoo_workspace logicmoo.base.examples.fol.EINSTEIN_SIMPLER

logicmoo.base.examples.fol.EINSTEIN_SIMPLER_05 JUnit

Open TeamSPoon opened this issue 4 years ago • 0 comments
trafficstars
(cd /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol ; timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "['einstein_simpler_05.pfc.pl']")
% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_05.pfc.pl % JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.examples.fol/EINSTEIN_SIMPLER_05/ % ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3AEINSTEIN_SIMPLER_05 % ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/454
%~ 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@2/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_05.pfc.pl'),
%~ /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test_header.pl:93 
%~ this_test_might_need( :-( use_module( library(logicmoo_plarkc))))


:- uses_dialect(pfc).

% :- module(baseKB).

/*~
%~ message_hook_type(error)
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_05.pfc.pl:49 
%~ message_hook(
%~    error(existence_error(procedure,baseKB:uses_dialect/1),context(system:catch/3,Context_Kw)),
%~    error,
%~    [ '~q/~w: '-[catch,3],
%~      'Unknown procedure: ~q' - [ baseKB : uses_dialect/1]])
catch/3: Unknown procedure: baseKB:uses_dialect/1
ERROR: catch/3: Unknown procedure: baseKB:uses_dialect/1
%~ message_hook_type(warning)
%~ message_hook(
%~    goal_failed(directive,baseKB:uses_dialect(pfc)),
%~    warning,
%~    [ 'Goal (~w) failed: ~p' - [ directive,
%~                                 baseKB : uses_dialect(pfc)]])
Goal (directive) failed: baseKB:uses_dialect(pfc)
Warning: Goal (directive) failed: baseKB:uses_dialect(pfc)
~*/


% :- module(baseKB).

:- op(600,xfy, (/\)).
/*~
~*/

:- op(0,xfx,'=>').
/*~
~*/

:- op(1150,xfy,'=>').

/*~
~*/


:- wdmsg([pack(logicmoo_base/t/examples/fol/'einstein_simpler_03.pfc')]).

/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/einstein_simpler_05.pfc.pl:57 
%~ [ pack( ( logicmoo_base  /
%~           t /
%~           examples /
%~           fol /
%~           'einstein_simpler_03.pfc'))]
~*/


never_assert_u(boxlog((lives(A, _):-neighbor(A, _))),singletons).

% add this to our vocab
/*~
%~ debugm( baseKB,
%~   show_success( baseKB,
%~     baseKB : ain( clif( never_assert_u(
%~                            boxlog( lives(A,Lives_A5) :-
%~ 
%~                                      neighbor(A,Neighbor_A6)),
%~                            singletons)))))
%   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: 207 words .. **



** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/lex.xg: -199 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.68 sec, 3 clauses
% /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/debuggery/dmsg compiled into dmsg 0.13 sec, -16 clauses




=======================================================
never_assert_u(boxlog(:-(lives('$VAR'('Lives'),'$VAR'('Lives6')),neighbor('$VAR'('Lives'),'$VAR'('Neighbor')))),singletons)
============================================


?- kif_to_boxlog( never_assert_u(boxlog((lives(Lives,Lives6):-neighbor(Lives,Neighbor))),singletons) ).



% In English: 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  ?Lives lives ?Lives6 :- ?Lives neighbor ?Neighbor isa boxlog never_assert_u singletons
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(never_assert_u(boxlog(:-(lives('$VAR'('Lives'),'$VAR'('Lives6')),neighbor('$VAR'('Lives'),'$VAR'('Neighbor')))),singletons))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s): 
nesc(never_assert_u(boxlog((lives(Lives,Lives6)<gt;-neighbor(Lives,Neighbor))),singletons)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  it is necessarily true that ?Lives lives ?Lives6 <gt;- ?Lives neighbor ?Neighbor isa boxlog never_assert_u singletons
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc( never_assert_u( 
         boxlog( lives(Lives,Lives6)<gt;-neighbor(Lives,Neighbor)), 
         singletons)).

============================================
~*/


% add this to our vocab
props((/\),ftSentenceOp,tLogicalConjunction).

% Source http://www.iflscience.com/editors-blog/solving-einsteins-riddle
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif((ftSentenceOp(/\),tLogicalConjunction(/\))))))




=======================================================
','(ftSentenceOp(/\),tLogicalConjunction(/\))
============================================


?- kif_to_boxlog( ftSentenceOp(/\),tLogicalConjunction(/\) ).



% In English: 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  /\ isa ftSentenceOp ',' /\ isa tLogicalConjunction
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(and(ftSentenceOp(and),tLogicalConjunction(and)))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 4 entailment(s): 
nesc(ftSentenceOp(&))==>nesc(tLogicalConjunction(&)).
nesc(tLogicalConjunction(&))==>nesc(ftSentenceOp(&)).
poss(~ftSentenceOp(&))==>poss(~tLogicalConjunction(&)).
poss(~tLogicalConjunction(&))==>poss(~ftSentenceOp(&)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    & isa ftSentenceOp is necessarily true
%~  It's Proof that:
%~    & isa tLogicalConjunction is necessarily true
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(ftSentenceOp(&))==>nesc(tLogicalConjunction(&)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    & isa tLogicalConjunction is necessarily true
%~  It's Proof that:
%~    & isa ftSentenceOp is necessarily true
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(tLogicalConjunction(&))==>nesc(ftSentenceOp(&)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    & isa ftSentenceOp is possibly false
%~  It's Proof that:
%~    & isa tLogicalConjunction is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

poss(~ftSentenceOp(&))==>poss(~tLogicalConjunction(&)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    & isa tLogicalConjunction is possibly false
%~  It's Proof that:
%~    & isa ftSentenceOp is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

poss(~tLogicalConjunction(&))==>poss(~ftSentenceOp(&)).

============================================
~*/


% Source http://www.iflscience.com/editors-blog/solving-einsteins-riddle
:- expects_dialect(clif).

%= 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)))))).

%= In each house lives a person with a unique nationality.
% we write this in SUMO
% all(H,exists(P,exists(U,(house(H) => (person(P) /\ lives(P, H) /\ unique(U,nationality(P,U))))))).
% SANITY count the persons (shouild be 5)
% :- sanity(( findall(P,person(P),L),length(L,5))).

% Helper functions
% 
/*~
%~ 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)))))))))))




=======================================================
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 /\ ?Exists_Leftof6 leftof ?Exists_Leftof7 /\ ?Exists_Leftof7 leftof ?Exists_Leftof8 /\ ?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(leftof('$VAR'('Exists_Leftof'),'$VAR'('Exists_Leftof6')),and(leftof('$VAR'('Exists_Leftof6'),'$VAR'('Exists_Leftof7')),and(leftof('$VAR'('Exists_Leftof7'),'$VAR'('Exists_Leftof8')),leftof('$VAR'('Exists_Leftof8'),'$VAR'('Leftof13')))))))))))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 16 entailment(s): 
poss(nesc(leftof(Exists_Leftof7,Exists_Leftof8))&nesc(leftof(Exists_Leftof8,Leftof13)))&(((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)).
poss(leftof(Exists_Leftof7,Exists_Leftof8))&poss(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_Leftof8,Leftof13)).
poss(leftof(Exists_Leftof7,Exists_Leftof8))&((((nesc(leftof(Exists_Leftof,Exists_Leftof6))&poss(~leftof(Exists_Leftof6,Exists_Leftof7)))&'$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_Leftof8,Leftof13)).
poss(leftof(Exists_Leftof8,Leftof13))&poss(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_Leftof7,Exists_Leftof8)).
poss(leftof(Exists_Leftof8,Leftof13))&((((nesc(leftof(Exists_Leftof,Exists_Leftof6))&poss(~leftof(Exists_Leftof6,Exists_Leftof7)))&'$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_Leftof7,Exists_Leftof8)).
((((nesc(leftof(Exists_Leftof,Exists_Leftof6))&poss(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_Leftof6,Exists_Leftof7)).
((((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&'$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_Leftof8,Leftof13)).
((((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7))&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_Leftof7,Exists_Leftof8)).
((((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7))&poss(~leftof(Exists_Leftof7,Exists_Leftof8)))&'$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_Leftof8,Leftof13)).
((((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7))&poss(~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_Leftof7,Exists_Leftof8)).
((((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof7,Exists_Leftof8))&poss(~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_Leftof6,Exists_Leftof7)).
((((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof8,Leftof13))&poss(~leftof(Exists_Leftof7,Exists_Leftof8)))&'$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)).
((((poss(nesc(leftof(Exists_Leftof6,Exists_Leftof7))&nesc(leftof(Exists_Leftof7,Exists_Leftof8))&nesc(leftof(Exists_Leftof8,Leftof13)))&'$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)).
(((((nesc(leftof(Exists_Leftof6,Exists_Leftof7))&nesc(leftof(Exists_Leftof7,Exists_Leftof8))&poss(~leftof(Exists_Leftof8,Leftof13)))&'$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)).
(((((nesc(leftof(Exists_Leftof6,Exists_Leftof7))&nesc(leftof(Exists_Leftof8,Leftof13))&poss(~leftof(Exists_Leftof7,Exists_Leftof8)))&'$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)).
(((((poss(~leftof(Exists_Leftof6,Exists_Leftof7))&poss(nesc(leftof(Exists_Leftof7,Exists_Leftof8))&nesc(leftof(Exists_Leftof8,Leftof13))))&'$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)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    ((" ?Exists_Leftof7 leftof ?Exists_Leftof8 " is necessarily true  and
%~    " ?Exists_Leftof8 leftof ?Leftof13 " is necessarily true )is possible ) and
%~    ((((" ?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( ( nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & 
            nesc( leftof(Exists_Leftof8,Leftof13))))  &
    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_Leftof7 leftof ?Exists_Leftof8 " is possible  and
%~    (" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is possible  and
%~    ((((" ?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_Leftof8 leftof ?Leftof13 " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( leftof(Exists_Leftof7,Exists_Leftof8))  &
    poss( 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_Leftof8,Leftof13)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Exists_Leftof7 leftof ?Exists_Leftof8 " is possible  and
%~    (((((" ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true  and
%~    " ?Exists_Leftof6 leftof ?Exists_Leftof7 " 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_Leftof8 leftof ?Leftof13 " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( leftof(Exists_Leftof7,Exists_Leftof8))  &
    nesc( leftof(Exists_Leftof,Exists_Leftof6)) & 
    poss( ~( leftof(Exists_Leftof6,Exists_Leftof7))) & 
    '$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_Leftof8,Leftof13)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Exists_Leftof8 leftof ?Leftof13 " is possible  and
%~    (" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is possible  and
%~    ((((" ?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_Leftof7 leftof ?Exists_Leftof8 " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( leftof(Exists_Leftof8,Leftof13))  &
    poss( 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_Leftof7,Exists_Leftof8)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Exists_Leftof8 leftof ?Leftof13 " is possible  and
%~    (((((" ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true  and
%~    " ?Exists_Leftof6 leftof ?Exists_Leftof7 " 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_Leftof7 leftof ?Exists_Leftof8 " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( leftof(Exists_Leftof8,Leftof13))  &
    nesc( leftof(Exists_Leftof,Exists_Leftof6)) & 
    poss( ~( leftof(Exists_Leftof6,Exists_Leftof7))) & 
    '$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_Leftof7,Exists_Leftof8)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    ((((" ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true  and
%~    ((" ?Exists_Leftof7 leftof ?Exists_Leftof8 " is necessarily true  and
%~    " ?Exists_Leftof8 leftof ?Leftof13 " is necessarily true )is possible )) 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))  &
    poss( ( 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_Leftof6,Exists_Leftof7))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    ((((" ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true  and
%~    (" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is necessarily true  and
%~    " ?Exists_Leftof7 leftof ?Exists_Leftof8 " 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_Leftof8 leftof ?Leftof13 " is necessarily true
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( leftof(Exists_Leftof,Exists_Leftof6))  &
    nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & 
    nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & 
    '$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_Leftof8,Leftof13))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    ((((" ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true  and
%~    (" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is necessarily true  and
%~    " ?Exists_Leftof8 leftof ?Leftof13 " 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_Leftof7 leftof ?Exists_Leftof8 " is necessarily true
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( leftof(Exists_Leftof,Exists_Leftof6))  &
    nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & 
    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_Leftof7,Exists_Leftof8))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    ((((" ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true  and
%~    (" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is necessarily true  and
%~    " ?Exists_Leftof7 leftof ?Exists_Leftof8 " 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_Leftof8 leftof ?Leftof13 " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( leftof(Exists_Leftof,Exists_Leftof6))  &
    nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & 
    poss( ~( leftof(Exists_Leftof7,Exists_Leftof8))) & 
    '$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_Leftof8,Leftof13)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    ((((" ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true  and
%~    (" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is necessarily true  and
%~    " ?Exists_Leftof8 leftof ?Leftof13 " 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_Leftof7 leftof ?Exists_Leftof8 " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( leftof(Exists_Leftof,Exists_Leftof6))  &
    nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & 
    poss( ~( 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_Leftof7,Exists_Leftof8)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    ((((" ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true  and
%~    (" ?Exists_Leftof7 leftof ?Exists_Leftof8 " is necessarily true  and
%~    " ?Exists_Leftof8 leftof ?Leftof13 " 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
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( leftof(Exists_Leftof,Exists_Leftof6))  &
    nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & 
    poss( ~( 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_Leftof6,Exists_Leftof7)))).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    ((((" ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true  and
%~    (" ?Exists_Leftof8 leftof ?Leftof13 " is necessarily true  and
%~    " ?Exists_Leftof7 leftof ?Exists_Leftof8 " 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
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( leftof(Exists_Leftof,Exists_Leftof6))  &
    nesc( leftof(Exists_Leftof8,Leftof13)) & 
    poss( ~( leftof(Exists_Leftof7,Exists_Leftof8))) & 
    '$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
%~    (" ?Exists_Leftof7 leftof ?Exists_Leftof8 " is necessarily true  and
%~    " ?Exists_Leftof8 leftof ?Leftof13 " is necessarily true ))is possible ) 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
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( poss( ( nesc( leftof(Exists_Leftof6,Exists_Leftof7))  &
            nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & 
            nesc( leftof(Exists_Leftof8,Leftof13))))  &
    '$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 necessarily true  and
%~    (" ?Exists_Leftof7 leftof ?Exists_Leftof8 " is necessarily true  and
%~    " ?Exists_Leftof8 leftof ?Leftof13 " 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
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( leftof(Exists_Leftof6,Exists_Leftof7))  &
    nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & 
    poss( ~( leftof(Exists_Leftof8,Leftof13))) & 
    '$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:
%~    (((((" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is necessarily true  and
%~    (" ?Exists_Leftof8 leftof ?Leftof13 " is necessarily true  and
%~    " ?Exists_Leftof7 leftof ?Exists_Leftof8 " 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
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

( ( nesc( leftof(Exists_Leftof6,Exists_Leftof7))  &
    nesc( leftof(Exists_Leftof8,Leftof13)) & 
    poss( ~( leftof(Exists_Leftof7,Exists_Leftof8))) & 
    '$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:
%~    (((((" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is possibly false  and
%~    ((" ?Exists_Leftof7 leftof ?Exists_Leftof8 " is necessarily true  and
%~    " ?Exists_Leftof8 leftof ?Leftof13 " is necessarily true )is possible )) 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)))  &
    poss( ( nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & 
            nesc( leftof(Exists_Leftof8,Leftof13)))) & 
    '$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)))).

============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('H1'),exists('$VAR'('H2'),exists('$VAR'('H3'),exists('$VAR'('H4'),exists('$VAR'('H5'),necessary(and(leftof('$VAR'('H1'),'$VAR'('H2')),and(leftof('$VAR'('H2'),'$VAR'('H3')),and(leftof('$VAR'('H3'),'$VAR'('H4')),leftof('$VAR'('H4'),'$VAR'('H5')))))))))))
totalTime=10.000
FAILED: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k einstein_simpler_05.pfc.pl (returned 137) Add_LABELS='Errors,Overtime' Rem_LABELS='Skipped,Skipped,Warnings,Skipped'
Sep 18 '21 22:09 TeamSPoon
logicmoo_workspace logicmoo_workspace copied to clipboard

logicmoo.base.examples.fol.EINSTEIN_SIMPLER_05 JUnit

logicmoo_workspace
logicmoo_workspace copied to clipboard
