nesc(leftof(Exists_Leftof6,Exists_Leftof7)). (((poss(~leftof(Exists_Leftof,Exists_Leftof6))&'$existential'(Exists_Leftof6,1,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))))&'$existential'(Exists_Leftof7,1,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))))&'$existential'(Exists_Leftof8,1,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))&'$existential'(Leftof13,1,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))==>poss(~leftof(Exists_Leftof6,Exists_Leftof7)). ((((nesc(leftof(Exists_Leftof6,Exists_Leftof7))&'$existential'(Exists_Leftof,1,exists(Exists_Leftof6,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))))))&'$existential'(Exists_Leftof6,1,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))))&'$existential'(Exists_Leftof7,1,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))))&'$existential'(Exists_Leftof8,1,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))&'$existential'(Leftof13,1,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))==>nesc(leftof(Exists_Leftof,Exists_Leftof6)). ((((poss(~leftof(Exists_Leftof6,Exists_Leftof7))&'$existential'(Exists_Leftof,1,exists(Exists_Leftof6,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))))))&'$existential'(Exists_Leftof6,1,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))))&'$existential'(Exists_Leftof7,1,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))))&'$existential'(Exists_Leftof8,1,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))&'$existential'(Leftof13,1,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))==>poss(~leftof(Exists_Leftof,Exists_Leftof6)). ('$existential'(Exists_Leftof7,1,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))&'$existential'(Exists_Leftof8,1,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))&'$existential'(Leftof13,1,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))==>nesc(leftof(Exists_Leftof7,Exists_Leftof8)). '$existential'(Exists_Leftof8,1,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))&'$existential'(Leftof13,1,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))==>nesc(leftof(Exists_Leftof8,Leftof13)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (((" ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true and %~ by default ?Exists_Leftof6 exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))) ) and %~ by default ?Exists_Leftof7 exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))) ) and %~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) ) and %~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)) %~ It's Proof that: %~ " ?Exists_Leftof6 leftof ?Exists_Leftof7 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & '$existential'( Exists_Leftof6, 1, exists( Exists_Leftof7, exists( Exists_Leftof8, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))))) & '$existential'( Exists_Leftof7, 1, exists( Exists_Leftof8, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13)))))) & '$existential'( Exists_Leftof8, 1, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) & '$existential'( Leftof13, 1, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) ==> nesc( leftof(Exists_Leftof6,Exists_Leftof7))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (((" ?Exists_Leftof leftof ?Exists_Leftof6 " is possibly false and %~ by default ?Exists_Leftof6 exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))) ) and %~ by default ?Exists_Leftof7 exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))) ) and %~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) ) and %~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)) %~ It's Proof that: %~ " ?Exists_Leftof6 leftof ?Exists_Leftof7 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( leftof(Exists_Leftof,Exists_Leftof6))) & '$existential'( Exists_Leftof6, 1, exists( Exists_Leftof7, exists( Exists_Leftof8, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))))) & '$existential'( Exists_Leftof7, 1, exists( Exists_Leftof8, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13)))))) & '$existential'( Exists_Leftof8, 1, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) & '$existential'( Leftof13, 1, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) ==> poss( ~( leftof(Exists_Leftof6,Exists_Leftof7)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ((((" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is necessarily true and %~ by default ?Exists_Leftof exists(Exists_Leftof6,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))) ) and %~ by default ?Exists_Leftof6 exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))) ) and %~ by default ?Exists_Leftof7 exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))) ) and %~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) ) and %~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)) %~ It's Proof that: %~ " ?Exists_Leftof leftof ?Exists_Leftof6 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & '$existential'( Exists_Leftof, 1, exists( Exists_Leftof6, exists( Exists_Leftof7, exists( Exists_Leftof8, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13)))))))) & '$existential'( Exists_Leftof6, 1, exists( Exists_Leftof7, exists( Exists_Leftof8, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))))) & '$existential'( Exists_Leftof7, 1, exists( Exists_Leftof8, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13)))))) & '$existential'( Exists_Leftof8, 1, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) & '$existential'( Leftof13, 1, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) ==> nesc( leftof(Exists_Leftof,Exists_Leftof6))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ((((" ?Exists_Leftof6 leftof ?Exists_Leftof7 " is possibly false and %~ by default ?Exists_Leftof exists(Exists_Leftof6,exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))))) ) and %~ by default ?Exists_Leftof6 exists(Exists_Leftof7,exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))))) ) and %~ by default ?Exists_Leftof7 exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))) ) and %~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) ) and %~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)) %~ It's Proof that: %~ " ?Exists_Leftof leftof ?Exists_Leftof6 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( leftof(Exists_Leftof6,Exists_Leftof7))) & '$existential'( Exists_Leftof, 1, exists( Exists_Leftof6, exists( Exists_Leftof7, exists( Exists_Leftof8, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13)))))))) & '$existential'( Exists_Leftof6, 1, exists( Exists_Leftof7, exists( Exists_Leftof8, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))))) & '$existential'( Exists_Leftof7, 1, exists( Exists_Leftof8, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13)))))) & '$existential'( Exists_Leftof8, 1, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) & '$existential'( Leftof13, 1, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) ==> poss( ~( leftof(Exists_Leftof,Exists_Leftof6)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ( by default ?Exists_Leftof7 exists(Exists_Leftof8,exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)))) and %~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) ) and %~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)) %~ It's Proof that: %~ " ?Exists_Leftof7 leftof ?Exists_Leftof8 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( '$existential'( Exists_Leftof7, 1, exists( Exists_Leftof8, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13)))))) & '$existential'( Exists_Leftof8, 1, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) & '$existential'( Leftof13, 1, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) ==> nesc( leftof(Exists_Leftof7,Exists_Leftof8))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ by default ?Exists_Leftof8 exists(Leftof13,((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13))) and %~ by default ?Leftof13 ((nesc(leftof(Exists_Leftof,Exists_Leftof6))&nesc(leftof(Exists_Leftof6,Exists_Leftof7)))&nesc(leftof(Exists_Leftof7,Exists_Leftof8)))&nesc(leftof(Exists_Leftof8,Leftof13)) %~ It's Proof that: %~ " ?Exists_Leftof8 leftof ?Leftof13 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( '$existential'( Exists_Leftof8, 1, exists( Leftof13, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) & '$existential'( Leftof13, 1, ( nesc( leftof(Exists_Leftof,Exists_Leftof6)) & nesc( leftof(Exists_Leftof6,Exists_Leftof7)) & nesc( leftof(Exists_Leftof7,Exists_Leftof8)) & nesc( leftof(Exists_Leftof8,Leftof13))))) ==> nesc( leftof(Exists_Leftof8,Leftof13))). ============================================ %~ kif_to_boxlog_attvars2 = exists('$VAR'('H1'),exists('$VAR'('H2'),exists('$VAR'('H3'),exists('$VAR'('H4'),exists('$VAR'('H5'),necessary(and(and(and(leftof('$VAR'('H1'),'$VAR'('H2')),leftof('$VAR'('H2'),'$VAR'('H3'))),leftof('$VAR'('H3'),'$VAR'('H4'))),leftof('$VAR'('H4'),'$VAR'('H5'))))))))) %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) and %~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)) %~ It's Proof that: %~ " ?H4 leftof ?H5 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( '$existential'( H4, 1, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) & '$existential'( H5, 1, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) ==> nesc( leftof(H4,H5))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ( by default ?H3 exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))) and %~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) ) and %~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)) %~ It's Proof that: %~ " ?H3 leftof ?H4 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( '$existential'( H3, 1, exists( H4, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5)))))) & '$existential'( H4, 1, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) & '$existential'( H5, 1, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) ==> nesc( leftof(H3,H4))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (((" ?H1 leftof ?H2 " is possibly false and %~ by default ?H2 exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))))) ) and %~ by default ?H3 exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))) ) and %~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) ) and %~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)) %~ It's Proof that: %~ " ?H2 leftof ?H3 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( leftof(H1,H2))) & '$existential'( H2, 1, exists( H3, exists( H4, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))))) & '$existential'( H3, 1, exists( H4, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5)))))) & '$existential'( H4, 1, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) & '$existential'( H5, 1, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) ==> poss( ~( leftof(H2,H3)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ((((" ?H2 leftof ?H3 " is necessarily true and %~ by default ?H1 exists(H2,exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))))) ) and %~ by default ?H2 exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))))) ) and %~ by default ?H3 exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))) ) and %~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) ) and %~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)) %~ It's Proof that: %~ " ?H1 leftof ?H2 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( nesc( leftof(H2,H3)) & '$existential'( H1, 1, exists( H2, exists( H3, exists( H4, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5)))))))) & '$existential'( H2, 1, exists( H3, exists( H4, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))))) & '$existential'( H3, 1, exists( H4, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5)))))) & '$existential'( H4, 1, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) & '$existential'( H5, 1, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) ==> nesc( leftof(H1,H2))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ((((" ?H2 leftof ?H3 " is possibly false and %~ by default ?H1 exists(H2,exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))))) ) and %~ by default ?H2 exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))))) ) and %~ by default ?H3 exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))) ) and %~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) ) and %~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)) %~ It's Proof that: %~ " ?H1 leftof ?H2 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( leftof(H2,H3))) & '$existential'( H1, 1, exists( H2, exists( H3, exists( H4, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5)))))))) & '$existential'( H2, 1, exists( H3, exists( H4, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))))) & '$existential'( H3, 1, exists( H4, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5)))))) & '$existential'( H4, 1, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) & '$existential'( H5, 1, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) ==> poss( ~( leftof(H1,H2)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (((" ?H1 leftof ?H2 " is necessarily true and %~ by default ?H2 exists(H3,exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))))) ) and %~ by default ?H3 exists(H4,exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)))) ) and %~ by default ?H4 exists(H5,((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5))) ) and %~ by default ?H5 ((nesc(leftof(H1,H2))&nesc(leftof(H2,H3)))&nesc(leftof(H3,H4)))&nesc(leftof(H4,H5)) %~ It's Proof that: %~ " ?H2 leftof ?H3 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( nesc( leftof(H1,H2)) & '$existential'( H2, 1, exists( H3, exists( H4, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))))) & '$existential'( H3, 1, exists( H4, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5)))))) & '$existential'( H4, 1, exists( H5, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) & '$existential'( H5, 1, ( nesc( leftof(H1,H2)) & nesc( leftof(H2,H3)) & nesc( leftof(H3,H4)) & nesc( leftof(H4,H5))))) ==> nesc( leftof(H2,H3))). ~*/ %~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_up_down_02.pl:28 %~ unused(no_junit_results) %~ test_completed_exit(0) ``` totalTime=5.000 FAILED: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k five_leftof_up_down_02.pl (returned 0) Add_LABELS='' Rem_LABELS='Skipped,Skipped,Errors,Warnings,Overtime,Skipped,Skipped']]>