((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)/dif(X,Y) ==> t(P,Y,X)). /*~ ~*/ antisymmetric(P)/fail ==> (t(P,X,Y)/dif(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). /*~ %~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/pfc/t/sanity_base/why_bug_01e.pfc:41 %~ 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(_39008,_39030)==>hop(_39008,_39030)))),nop(ftrace(user:(edge(_39008,_39030)==>hop(_39008,_39030)))))) 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.WHY_BUG_01E-Test_0001_Line_0000__edge_2_in_user'. JUNIT_CLASSNAME='logicmoo.pfc.test.sanity_base.WHY_BUG_01E'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lm goal=user:(edge(_86010,_86012)==>hop(_86012,_86010)). time=0.0005054473876953125. failure=failure=info((why_was_true(user:(\+ (edge(_55204,_55236)==>hop(_55236,_55204)))),nop(ftrace(user:(edge(_55204,_55236)==>hop(_55236,_55204)))))) 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))). result=failure. ]]>