(and(caresForType('$VAR'('M1'),'$VAR'('T1')),isa('$VAR'('P1'),'$VAR'('T1'))),caresFor('$VAR'('M1'),'$VAR'('P1')))) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results in the following 25 entailment(s): poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1))==>nesc(caresFor(M1,P1)). poss(~caresFor(M1,P1))&poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))==>poss(~isa(P1,T1)). poss(~caresFor(M1,P1))&poss(~caresFor(M1,P1))&nesc(isa(P1,T1))==>poss(~caresForType(M1,T1)). poss(~caresFor(M1,P1))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>poss(~caresFor(M1,P1)). poss(~caresForType(M1,T1))&poss(~caresFor(M1,P1))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>poss(~isa(P1,T1)). poss(~caresForType(M1,T1))&((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>poss(~isa(P1,T1)). poss(caresForType(M1,T1))&poss(~caresFor(M1,P1))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))==>nesc(isa(P1,T1)). poss(caresForType(M1,T1))&((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))==>nesc(isa(P1,T1)). (poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1)))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(poss(~isa(P1,T1)),nesc(isa(P1,T1)))==>nesc(caresForType(M1,T1)). (poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1)))==>poss(~caresForType(M1,T1)). (poss(~caresFor(M1,P1))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&poss(isa(P1,T1))==>nesc(caresForType(M1,T1)). (poss(~caresFor(M1,P1))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1))))&poss(~isa(P1,T1))==>poss(~caresForType(M1,T1)). (((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&poss(isa(P1,T1))==>nesc(caresForType(M1,T1)). (((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1))))&poss(~isa(P1,T1))==>poss(~caresForType(M1,T1)). ((v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(poss(~isa(P1,T1)),nesc(isa(P1,T1)))==>nesc(caresForType(M1,T1)). ((v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1)))==>poss(~caresForType(M1,T1)). ((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1))==>nesc(caresFor(M1,P1)). ((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))==>poss(~isa(P1,T1)). ((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&poss(~caresFor(M1,P1))&nesc(isa(P1,T1))==>poss(~caresForType(M1,T1)). ((v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1)))&v(nesc(isa(P1,T1)),poss(~isa(P1,T1))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>poss(~caresFor(M1,P1)). (v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>nesc(caresFor(M1,P1)). (v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))))&poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1))==>nesc(isa(P1,T1)). (v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))))&(v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>nesc(isa(P1,T1)). (v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&poss(~caresFor(M1,P1))&nesc(caresForType(M1,T1))&nesc(isa(P1,T1))==>poss(~isa(P1,T1)). (v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1)))&v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))))&(v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1)))&v(nesc(caresFor(M1,P1)),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),nesc(caresFor(M1,P1)))&v(poss(poss(~caresForType(M1,T1))&nesc(isa(P1,T1))),poss(nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))==>poss(~isa(P1,T1)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?M1 caresFor ?P1 " is possibly false and %~ (" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is necessarily true ) %~ It's Proof that: %~ " ?M1 caresFor ?P1 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( caresFor(M1,P1))) & nesc( caresForType(M1,T1)) & nesc( isa(P1,T1))) ==> nesc( caresFor(M1,P1))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?M1 caresFor ?P1 " is possibly false and %~ (" ?M1 caresFor ?P1 " is possibly false and %~ " ?M1 caresForType ?T1 " is necessarily true ) %~ It's Proof that: %~ " ?P1 isa ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( caresFor(M1,P1))) & poss( ~( caresFor(M1,P1))) & nesc( caresForType(M1,T1))) ==> poss( ~( isa(P1,T1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?M1 caresFor ?P1 " is possibly false and %~ (" ?M1 caresFor ?P1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true ) %~ It's Proof that: %~ " ?M1 caresForType ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( caresFor(M1,P1))) & poss( ~( caresFor(M1,P1))) & nesc( isa(P1,T1))) ==> poss( ~( caresForType(M1,T1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?M1 caresFor ?P1 " is possibly false and %~ (((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible )) %~ It's Proof that: %~ " ?M1 caresFor ?P1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( caresFor(M1,P1))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==> poss( ~( caresFor(M1,P1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?M1 caresForType ?T1 " is possibly false and %~ (" ?M1 caresFor ?P1 " is possibly false and %~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible )))) %~ It's Proof that: %~ " ?P1 isa ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( caresForType(M1,T1))) & poss( ~( caresFor(M1,P1))) & v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( nesc( caresFor(M1,P1)), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==> poss( ~( isa(P1,T1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?M1 caresForType ?T1 " is possibly false and %~ ((((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and %~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and %~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and %~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible )))) %~ It's Proof that: %~ " ?P1 isa ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( caresForType(M1,T1))) & v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) & v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( nesc( caresFor(M1,P1)), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==> poss( ~( isa(P1,T1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?M1 caresForType ?T1 " is possible and %~ (" ?M1 caresFor ?P1 " is possibly false and %~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ))) %~ It's Proof that: %~ " ?P1 isa ?T1 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( caresForType(M1,T1)) & poss( ~( caresFor(M1,P1))) & v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), nesc( caresFor(M1,P1)))) ==> nesc( isa(P1,T1))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?M1 caresForType ?T1 " is possible and %~ ((((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and %~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and %~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and %~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ))) %~ It's Proof that: %~ " ?P1 isa ?T1 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( caresForType(M1,T1)) & v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) & v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), nesc( caresFor(M1,P1)))) ==> nesc( isa(P1,T1))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (" ?M1 caresFor ?P1 " is possibly false and %~ (" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is necessarily true )) and %~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and %~ (" ?P1 isa ?T1 " is possibly false or " ?P1 isa ?T1 " is necessarily true )) %~ It's Proof that: %~ " ?M1 caresForType ?T1 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( caresFor(M1,P1))) & nesc( caresForType(M1,T1)) & nesc( isa(P1,T1)) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & v(poss(~isa(P1,T1)),nesc(isa(P1,T1)))) ==> nesc( caresForType(M1,T1))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (" ?M1 caresFor ?P1 " is possibly false and %~ (" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is necessarily true )) and %~ ((" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false ) and %~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false )) %~ It's Proof that: %~ " ?M1 caresForType ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( caresFor(M1,P1))) & nesc( caresForType(M1,T1)) & nesc( isa(P1,T1)) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & v(nesc(isa(P1,T1)),poss(~isa(P1,T1)))) ==> poss( ~( caresForType(M1,T1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (" ?M1 caresFor ?P1 " is possibly false and %~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible )))) and %~ " ?P1 isa ?T1 " is possible %~ It's Proof that: %~ " ?M1 caresForType ?T1 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( caresFor(M1,P1))) & v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( nesc( caresFor(M1,P1)), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) & poss( isa(P1,T1))) ==> nesc( caresForType(M1,T1))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (" ?M1 caresFor ?P1 " is possibly false and %~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ))) and %~ " ?P1 isa ?T1 " is possibly false %~ It's Proof that: %~ " ?M1 caresForType ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( caresFor(M1,P1))) & v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), nesc( caresFor(M1,P1))) & poss( ~( isa(P1,T1)))) ==> poss( ~( caresForType(M1,T1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ((((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and %~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and %~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and %~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible )))) and %~ " ?P1 isa ?T1 " is possible %~ It's Proof that: %~ " ?M1 caresForType ?T1 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) & v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( nesc( caresFor(M1,P1)), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) & poss( isa(P1,T1))) ==> nesc( caresForType(M1,T1))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ((((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and %~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and %~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and %~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ))) and %~ " ?P1 isa ?T1 " is possibly false %~ It's Proof that: %~ " ?M1 caresForType ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) & v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), nesc( caresFor(M1,P1))) & poss( ~( isa(P1,T1)))) ==> poss( ~( caresForType(M1,T1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible ))) and %~ ((((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible )))) and %~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and %~ (" ?P1 isa ?T1 " is possibly false or " ?P1 isa ?T1 " is necessarily true )) %~ It's Proof that: %~ " ?M1 caresForType ?T1 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( nesc( caresFor(M1,P1)), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), nesc( caresFor(M1,P1))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & v(poss(~isa(P1,T1)),nesc(isa(P1,T1)))) ==> nesc( caresForType(M1,T1))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible ))) and %~ ((((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible )))) and %~ ((" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false ) and %~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false )) %~ It's Proof that: %~ " ?M1 caresForType ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( nesc( caresFor(M1,P1)), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), nesc( caresFor(M1,P1))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & v(nesc(isa(P1,T1)),poss(~isa(P1,T1)))) ==> poss( ~( caresForType(M1,T1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and %~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and %~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and %~ (" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is necessarily true ) %~ It's Proof that: %~ " ?M1 caresFor ?P1 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) & nesc( caresForType(M1,T1)) & nesc( isa(P1,T1))) ==> nesc( caresFor(M1,P1))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and %~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and %~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and %~ (" ?M1 caresFor ?P1 " is possibly false and %~ " ?M1 caresForType ?T1 " is necessarily true ) %~ It's Proof that: %~ " ?P1 isa ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) & poss( ~( caresFor(M1,P1))) & nesc( caresForType(M1,T1))) ==> poss( ~( isa(P1,T1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and %~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and %~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and %~ (" ?M1 caresFor ?P1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true ) %~ It's Proof that: %~ " ?M1 caresForType ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) & poss( ~( caresFor(M1,P1))) & nesc( isa(P1,T1))) ==> poss( ~( caresForType(M1,T1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and %~ ((" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true ) and %~ (" ?P1 isa ?T1 " is necessarily true or " ?P1 isa ?T1 " is possibly false ))) and %~ (((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible )) %~ It's Proof that: %~ " ?M1 caresFor ?P1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & v(nesc(isa(P1,T1)),poss(~isa(P1,T1))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==> poss( ~( caresFor(M1,P1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible ))) and %~ ((((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible ))) %~ It's Proof that: %~ " ?M1 caresFor ?P1 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( nesc( caresFor(M1,P1)), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), nesc( caresFor(M1,P1))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==> nesc( caresFor(M1,P1))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true )) and %~ (" ?M1 caresFor ?P1 " is possibly false and %~ (" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is necessarily true )) %~ It's Proof that: %~ " ?P1 isa ?T1 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & poss( ~( caresFor(M1,P1))) & nesc( caresForType(M1,T1)) & nesc( isa(P1,T1))) ==> nesc( isa(P1,T1))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is necessarily true or " ?P1 isa ?T1 " is necessarily true )) and %~ (((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible ))) and %~ ((((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible )))) %~ It's Proof that: %~ " ?P1 isa ?T1 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(nesc(caresForType(M1,T1)),nesc(isa(P1,T1))) & v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( nesc( caresFor(M1,P1)), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), nesc( caresFor(M1,P1))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==> nesc( isa(P1,T1))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and %~ (" ?M1 caresFor ?P1 " is possibly false and %~ (" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is necessarily true )) %~ It's Proof that: %~ " ?P1 isa ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & poss( ~( caresFor(M1,P1))) & nesc( caresForType(M1,T1)) & nesc( isa(P1,T1))) ==> poss( ~( isa(P1,T1)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ((" ?M1 caresForType ?T1 " is possibly false or " ?M1 caresForType ?T1 " is necessarily true ) and %~ (" ?M1 caresForType ?T1 " is possibly false or " ?P1 isa ?T1 " is possibly false )) and %~ (((" ?M1 caresFor ?P1 " is necessarily true or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (" ?M1 caresFor ?P1 " is necessarily true or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible ))) and %~ ((((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or " ?M1 caresFor ?P1 " is necessarily true ) and %~ (((" ?M1 caresForType ?T1 " is possibly false and %~ " ?P1 isa ?T1 " is necessarily true )is possible ) or ((" ?M1 caresForType ?T1 " is necessarily true and %~ " ?P1 isa ?T1 " is possibly false )is possible )))) %~ It's Proof that: %~ " ?P1 isa ?T1 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( v(poss(~caresForType(M1,T1)),nesc(caresForType(M1,T1))) & v(poss(~caresForType(M1,T1)),poss(~isa(P1,T1))) & v(nesc(caresFor(M1,P1)),nesc(caresFor(M1,P1))) & v( nesc( caresFor(M1,P1)), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1)))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), nesc( caresFor(M1,P1))) & v( poss( poss(~caresForType(M1,T1))&nesc(isa(P1,T1))), poss( nesc(caresForType(M1,T1))&poss(~isa(P1,T1))))) ==> poss( ~( isa(P1,T1)))). ============================================ %~ kif_to_boxlog_attvars2 = necessary((and(caresForType('$VAR'('M1'),'$VAR'('T1')),isa('$VAR'('P1'),'$VAR'('T1'))),caresFor('$VAR'('M1'),'$VAR'('P1')))) ``` totalTime=10.000 FAILED: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k zebra_05.clif (returned 137) Add_LABELS='Errors,Overtime' Rem_LABELS='Skipped,Skipped,Warnings,Skipped']]>