((t(P,X,Y),t(P,Y,Z)/(dif(X,Y),dif(Y,Z),dif(X,Z)))==> t(P, X, Z)). /*~ ~*/ taxinomicPair(E,P) ==> (t(P,X,Y),t(E,Y,Z) ==> t(P, X, Z)). /*~ ~*/ subRelation(E,P) ==> ((t(E,X,Y)/(dif(X,Y))) ==> t(P,X,Y)). /*~ ~*/ edge(1,2). /*~ ~*/ edge(2,3). /*~ ~*/ edge(3,4). /*~ ~*/ subRelation(edge,hop). /*~ ~*/ subRelation(hop,path). /*~ ~*/ symmetric(hop). /*~ ~*/ symmetric(P) ==> (t(P,X,Y) ==> t(P,Y,X)). /*~ ~*/ antisymmetric(P)/fail ==> (t(P,X,Y) ~t(P,Y,X)). /*~ ~*/ reflexive(P) ==> t(P,X,X). /*~ ~*/ antireflexive(P) ==> ~t(P,X,X). /*~ ~*/ :- cls. % things that cannot be true are removed % unneeded when loaded from main system: ~t(P,X,X) ==> \+ t(P,X,X). /*~ %~ skipped(messy_on_output,cls) ~*/ % things that cannot be true are removed % unneeded when loaded from main system: ~t(P,X,X) ==> \+ t(P,X,X). :- mpred_why(edge(X,Y)==>hop(X,Y)). % bug .. giving the wrong proof! /*~ %~ ?-( mpred_test( "Test_0001_Line_0000__edge_2_in_user", %~ user : edge(X,Y)==>hop(X,Y))). failure=info((why_was_true(user:(\+ (edge(_4066,_4088)==>hop(_4066,_4088)))),nop(ftrace(user:(edge(_4066,_4088)==>hop(_4066,_4088)))))) no_proof_for(\+ (edge(X,Y)==>hop(X,Y))). no_proof_for(\+ (edge(X,Y)==>hop(X,Y))). no_proof_for(\+ (edge(X,Y)==>hop(X,Y))). name='logicmoo.pfc.test.sanity_base.TML_01E-Test_0001_Line_0000__edge_2_in_user'. JUNIT_CLASSNAME='logicmoo.pfc.test.sanity_base.TML_01E'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'tml_01e.pfc\']"'. % saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-pfc-test-sanity_base-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_pfc_test_sanity_base_TML_01E_Test_0001_Line_0000_edge_2_in_user-junit.xml ~*/ % bug .. giving the wrong proof! :- mpred_why(edge(X,Y)==>hop(Y,X)). % bug .. not giving any proof! /*~ %~ ?-( mpred_test( "Test_0002_Line_0000__edge_2_in_user", %~ user : edge(X,Y)==>hop(Y,X))). failure=info((why_was_true(user:(\+ (edge(_846,_868)==>hop(_868,_846)))),nop(ftrace(user:(edge(_846,_868)==>hop(_868,_846)))))) no_proof_for(\+ (edge(X,Y)==>hop(Y,X))). no_proof_for(\+ (edge(X,Y)==>hop(Y,X))). no_proof_for(\+ (edge(X,Y)==>hop(Y,X))). name='logicmoo.pfc.test.sanity_base.TML_01E-Test_0002_Line_0000__edge_2_in_user'. JUNIT_CLASSNAME='logicmoo.pfc.test.sanity_base.TML_01E'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'tml_01e.pfc\']"'. % saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-pfc-test-sanity_base-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_pfc_test_sanity_base_TML_01E_Test_0002_Line_0000_edge_2_in_user-junit.xml ~*/ % bug .. not giving any proof! :- dif(X,Y), mpred_why(edge(X,Y)==>hop(Y,X)). /*~ %~ ?-( mpred_test( "Test_0003_Line_0000__edge_2_in_user", %~ user : edge(X,Y)==>hop(Y,X))). failure=info((why_was_true(user:(\+ (edge(_52384,_52416)==>hop(_52416,_52384)))),nop(ftrace(user:(edge(_52384,_52416)==>hop(_52416,_52384)))))) no_proof_for(\+ (edge(X,Y)==>hop(Y,X))). no_proof_for(\+ (edge(X,Y)==>hop(Y,X))). no_proof_for(\+ (edge(X,Y)==>hop(Y,X))). name='logicmoo.pfc.test.sanity_base.TML_01E-Test_0003_Line_0000__edge_2_in_user'. JUNIT_CLASSNAME='logicmoo.pfc.test.sanity_base.TML_01E'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'tml_01e.pfc\']"'. % saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-pfc-test-sanity_base-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_pfc_test_sanity_base_TML_01E_Test_0003_Line_0000_edge_2_in_user-junit.xml ~*/ reflexive(reachable). /*~ ~*/ antisymmetric(reachable). /*~ ~*/ transitive(reachable). /*~ ~*/ antireflexive(path). /*~ ~*/ transitive(path). /*~ ~*/ path(X,Y)==>reachable(X,Y). % provably not a subrelation of equality % antireflexive(P) ~subRelation(P,equals). /*~ ~*/ % provably not a subrelation of equality % antireflexive(P) ~subRelation(P,equals).ls). :- statistics(runtime,[_|MS]), dmsg(assert_time_took_with_printing=ms(MS)). /*~ %~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/pfc/t/sanity_base/tml_01e.pfc:69 %~ assert_time_took_with_printing = ms([238]). ~*/ :- listing(edge/2). /*~ %~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/pfc/t/sanity_base/tml_01e.pfc:71 %~ skipped( listing( edge/2)) ~*/ :- listing(hop/2). /*~ %~ skipped( listing( hop/2)) ~*/ :- listing(path/2). /*~ %~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/pfc/t/sanity_base/tml_01e.pfc:73 %~ skipped( listing( path/2)) ~*/ :- listing(reachable/2). % thus this is true /*~ %~ skipped( listing( reachable/2)) ~*/ % thus this is true :- mpred_why(~path(X,X)). /*~ %~ ?-( mpred_test("Test_0004_Line_0000__path_2_in_user",user: ~path(X,X))). failure=info((why_was_true(user:(\+ ~path(_10794,_10794))),nop(ftrace(user: ~path(_10794,_10794))))) no_proof_for(\+ ~path(X,X)). no_proof_for(\+ ~path(X,X)). no_proof_for(\+ ~path(X,X)). name='logicmoo.pfc.test.sanity_base.TML_01E-Test_0004_Line_0000__path_2_in_user'. JUNIT_CLASSNAME='logicmoo.pfc.test.sanity_base.TML_01E'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'tml_01e.pfc\']"'. % saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-pfc-test-sanity_base-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-p goal=user:hop(2,3). time=0.0006084442138671875. passed=passed=info(why_was_true(user:hop(2,3))) no_proof_for(hop(2,3)). no_proof_for(hop(2,3)). no_proof_for(hop(2,3)). result=passed. ]]>