nesc( leftof(H1,H2))). ~*/ :- break. /*~ %~ skipped(blocks_on_input,break) ~*/ :- test_boxlog( exists(H1,exists(H2, (leftof(H1, H2) & different(H1, H2))))). /*~ %~ ?-( mpred_test( "Test_0001_Line_0000__leftof_2_in_user", %~ user : test_boxlog( exists(H1,exists(H2,leftof(H1,H2)&different(H1,H2)))))). %~ kifi = exists( H1, %~ exists(H2,leftof(H1,H2)&different(H1,H2))). %~ kifm = exists( H1, %~ exists(H2,nesc(leftof(H1,H2)&different(H1,H2)))). %~ kif_to_boxlog_attvars2 = exists('$VAR'('H1'),exists('$VAR'('H2'),necessary(and(leftof('$VAR'('H1'),'$VAR'('H2')),different('$VAR'('H1'),'$VAR'('H2')))))) %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (" ?H1 leftof ?H2 " is possibly false and %~ by default ?H1 exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2))) ) and %~ by default ?H2 nesc(leftof(H1,H2))&nesc(different(H1,H2)) %~ It's Proof that: %~ " ?H1 different ?H2 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( leftof(H1,H2))) & '$existential'( H1, 1, exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2)))) & '$existential'( H2, 1, nesc(leftof(H1,H2))&nesc(different(H1,H2)))) ==> poss( ~( different(H1,H2)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ( by default ?H1 exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2))) and %~ " ?H1 different ?H2 " is necessarily true ) and %~ by default ?H2 nesc(leftof(H1,H2))&nesc(different(H1,H2)) %~ It's Proof that: %~ " ?H1 leftof ?H2 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( '$existential'( H1, 1, exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2)))) & nesc( different(H1,H2)) & '$existential'( H2, 1, nesc(leftof(H1,H2))&nesc(different(H1,H2)))) ==> nesc( leftof(H1,H2))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ( by default ?H1 exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2))) and %~ " ?H1 different ?H2 " is possibly false ) and %~ by default ?H2 nesc(leftof(H1,H2))&nesc(different(H1,H2)) %~ It's Proof that: %~ " ?H1 leftof ?H2 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( '$existential'( H1, 1, exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2)))) & poss( ~( different(H1,H2))) & '$existential'( H2, 1, nesc(leftof(H1,H2))&nesc(different(H1,H2)))) ==> poss( ~( leftof(H1,H2)))). % AN goal=user:test_boxlog(exists(_9419500,exists(_9419506,leftof(_9419500,_9419506)&different(_9419500,_9419506)))). time=0.18021559715270996. passed=passed=info(why_was_true(user:test_boxlog(exists(_387410,exists(_387432,leftof(_387410,_387432)&different(_387410,_387432)))))) no_proof_for(test_boxlog(exists(H1,exists(H2,leftof(H1,H2)&different(H1,H2))))). %~ kifi=exists(H1,exists(H2,leftof(H1,H2)&different(H1,H2))) %~ kifm=exists(H1,exists(H2,nesc(leftof(H1,H2)&different(H1,H2)))) %~ kif_to_boxlog_attvars2 = exists('$VAR'('H1'),exists('$VAR'('H2'),necessary(and(leftof('$VAR'('H1'),'$VAR'('H2')),different('$VAR'('H1'),'$VAR'('H2')))))) %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (" ?H1 leftof ?H2 " is possibly false and %~ by default ?H1 exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2))) ) and %~ by default ?H2 nesc(leftof(H1,H2))&nesc(different(H1,H2)) %~ It's Proof that: %~ " ?H1 different ?H2 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( poss( ~( leftof(H1,H2))) & '$existential'( H1, 1, exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2)))) & '$existential'( H2, 1, nesc(leftof(H1,H2))&nesc(different(H1,H2)))) ==> poss( ~( different(H1,H2)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ( by default ?H1 exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2))) and %~ " ?H1 different ?H2 " is necessarily true ) and %~ by default ?H2 nesc(leftof(H1,H2))&nesc(different(H1,H2)) %~ It's Proof that: %~ " ?H1 leftof ?H2 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( '$existential'( H1, 1, exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2)))) & nesc( different(H1,H2)) & '$existential'( H2, 1, nesc(leftof(H1,H2))&nesc(different(H1,H2)))) ==> nesc( leftof(H1,H2))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ ( by default ?H1 exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2))) and %~ " ?H1 different ?H2 " is possibly false ) and %~ by default ?H2 nesc(leftof(H1,H2))&nesc(different(H1,H2)) %~ It's Proof that: %~ " ?H1 leftof ?H2 " is possibly false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( '$existential'( H1, 1, exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2)))) & poss( ~( different(H1,H2))) & '$existential'( H2, 1, nesc(leftof(H1,H2))&nesc(different(H1,H2)))) ==> poss( ~( leftof(H1,H2)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ (" ?H1 leftof ?H2 " is necessarily true and %~ by default ?H1 exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2))) ) and %~ by default ?H2 nesc(leftof(H1,H2))&nesc(different(H1,H2)) %~ It's Proof that: %~ " ?H1 different ?H2 " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( ( nesc( leftof(H1,H2)) & '$existential'( H1, 1, exists(H2,nesc(leftof(H1,H2))&nesc(different(H1,H2)))) & '$existential'( H2, 1, nesc(leftof(H1,H2))&nesc(different(H1,H2)))) ==> nesc( different(H1,H2))). no_proof_for(test_boxlog(exists(H1,exists(H2,leftof(H1,H2)&different(H1,H2))))). no_proof_for(test_boxlog(exists(H1,exists(H2,leftof(H1,H2)&different(H1,H2))))). result=passed. ]]>