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:leftof(h1,h2)&leftof(h2,h3)&leftof(h3,h4)&leftof(h4,h5). src='/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/fiveof/leftof_tests.pl':12. url=/var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/fiveof/leftof_tests.pl#L12 time=0.0008192062377929688. failure=failure=info((why_was_true(user:(\+leftof(h1,h2)&leftof(h2,h3)&leftof(h3,h4)&leftof(h4,h5))),nop(ftrace(user:leftof(h1,h2)&leftof(h2,h3)&leftof(h3,h4)&leftof(h4,h5))))) no_proof_for(\+leftof(h1,h2)&leftof(h2,h3)&leftof(h3,h4)&leftof(h4,h5)). no_proof_for(\+leftof(h1,h2)&leftof(h2,h3)&leftof(h3,h4)&leftof(h4,h5)). no_proof_for(\+leftof(h1,h2)&leftof(h2,h3)&leftof(h3,h4)&leftof(h4,h5)). result=failure. ]]>