lever:rc2:contrapositive:trail01:stop06 lever pipeline verify ../message/coverage/contrapositive/01_not_mortal -v
Verifying: 01_not_mortal
    KB: 1 entities, 2 clauses
    Grounded: 2 clauses
    Query: man(theme: zeus)
[QBBN] from_query: query='man(theme: zeus)'
[QBBN] add_proposition: NEW p1 = 'man(theme: zeus)'
[QBBN] from_query: 2 grounded clauses
[QBBN]   clause: HornClause(premises=(), conclusion=Predicate(function_name='mortal', roles=((RoleLabel(name='theme'), Constant(entity=Entity(id='zeus'), type=Type(name='e'))),), negated=True), variables=(), weight=1.0)
[QBBN]     is_fact: formula='not mortal(theme: zeus)', negated=True
[QBBN]     negative_fact: pos_formula='mortal(theme: zeus)'
[QBBN] add_proposition: NEW p2 = 'not mortal(theme: zeus)'
[QBBN] set_evidence: 'not mortal(theme: zeus)' = True
[QBBN]   clause: HornClause(premises=(Predicate(function_name='man', roles=((RoleLabel(name='theme'), Constant(entity=Entity(id='zeus'), type=Type(name='e'))),), negated=False),), conclusion=Predicate(function_name='mortal', roles=((RoleLabel(name='theme'), Constant(entity=Entity(id='zeus'), type=Type(name='e'))),), negated=False), variables=(), weight=99.0)
[QBBN]     is_rule: conclusion='mortal(theme: zeus)'
[QBBN]       premise: 'man(theme: zeus)'
[QBBN] from_query: positive_facts=set()
[QBBN] from_query: negative_facts={'mortal(theme: zeus)'}
[QBBN] from_query: clauses_by_conclusion keys=['mortal(theme: zeus)']
[QBBN] from_query: clauses_by_premise keys=['man(theme: zeus)']
[QBBN] from_query: depth=0, to_expand=['man(theme: zeus)']
[QBBN]   expanding: 'man(theme: zeus)'
[QBBN] add_proposition: already exists: man(theme: zeus) -> p1
[QBBN]     BACKWARD: 0 clauses conclude 'man(theme: zeus)'
[QBBN]     FORWARD: 1 clauses have 'man(theme: zeus)' as premise
[QBBN]       clause: ['man(theme: zeus)'] -> mortal(theme: zeus)
[QBBN] add_rule: r1 = ['man(theme: zeus)'] -> mortal(theme: zeus), weight=99.0
[QBBN] add_grounded_rule: ['man(theme: zeus)'] -> mortal(theme: zeus)
[QBBN] add_proposition: already exists: man(theme: zeus) -> p1
[QBBN] add_proposition: NEW p3 = 'mortal(theme: zeus)'
[QBBN] add_group: g1 = (['p1']) -> p3
[QBBN] add_and_factor: and1 = (['p1']) -> g1
[QBBN]       queue conclusion: 'mortal(theme: zeus)'
[QBBN] from_query: depth=1, to_expand=['mortal(theme: zeus)']
[QBBN]   expanding: 'mortal(theme: zeus)'
[QBBN] add_proposition: already exists: mortal(theme: zeus) -> p3
[QBBN]     -> negative evidence (X is false because 'not X' is true)
[QBBN] set_evidence: 'mortal(theme: zeus)' = False
[QBBN]     BACKWARD: 1 clauses conclude 'mortal(theme: zeus)'
[QBBN]     FORWARD: 0 clauses have 'mortal(theme: zeus)' as premise
[QBBN] build_or_factors: starting
[QBBN] add_or_factor: or1 = (['g1']) -> p3, weights={'g1': 99.0}
[QBBN] build_neg_factors: starting
[QBBN]   all formulas: ['man(theme: zeus)', 'not mortal(theme: zeus)', 'mortal(theme: zeus)']
[QBBN]   checking formula: 'man(theme: zeus)', is_negated=False
[QBBN]   checking formula: 'not mortal(theme: zeus)', is_negated=True
[QBBN]     positive form: 'mortal(theme: zeus)', exists=True
[QBBN]     linking: p3 (mortal(theme: zeus)) <-> p2 (not mortal(theme: zeus))
[QBBN] add_neg_factor: neg1 = p3 <-> p2
[QBBN]   checking formula: 'mortal(theme: zeus)', is_negated=False
[QBBN] from_query: final graph stats = {'propositions': 3, 'groups': 1, 'and_factors': 1, 'or_factors': 1, 'neg_factors': 1, 'rules': 1, 'evidence': 2}
    Graph: 3 props, 1 groups, 2 evidence
[BP] === Starting BP ===
[BP]   init p1: π=[0.5, 0.5], λ=[1.0, 1.0]
[BP]   init p2 (evidence=True): π=[0.0, 1.0], λ=[0.0, 1.0]
[BP]   init p3 (evidence=False): π=[1.0, 0.0], λ=[1.0, 0.0]
[BP]   init g1: π=[0.5, 0.5], λ=[1.0, 1.0]
[BP]   factors: 1 AND, 1 OR, 1 NEG
[BP] 
=== Iteration 1 ===
[BP]   AND and1: π(g1) = [0.5, 0.5] from inputs [0.5]
[BP]   OR or1 backward: λ(g1) = [1.0, 0.0] from λ(p3) = [1.0, 0.0]
[BP]   AND and1 backward: λ(p1) = [1.0, 0.0] from λ(g1) = [1.0, 0.0], others_prob=1.0
[BP]   belief p1: π=[0.5, 0.5], λ=[1.0, 0.0] -> P=0.0000, damped=0.2500
[BP]   belief g1: π=[0.5, 0.5], λ=[1.0, 0.0] -> P=0.0000, damped=0.2500
[BP]   max_diff = 0.250000
[BP] 
=== Iteration 2 ===
[BP]   AND and1: π(g1) = [0.5, 0.5] from inputs [0.5]
[BP]   OR or1 backward: λ(g1) = [1.0, 0.0] from λ(p3) = [1.0, 0.0]
[BP]   AND and1 backward: λ(p1) = [1.0, 0.0] from λ(g1) = [1.0, 0.0], others_prob=1.0
[BP]   belief p1: π=[0.5, 0.5], λ=[1.0, 0.0] -> P=0.0000, damped=0.0000
[BP]   belief g1: π=[0.5, 0.5], λ=[1.0, 0.0] -> P=0.0000, damped=0.0000
[BP]   max_diff = 0.000000
[BP]   CONVERGED at iteration 2
  ✅ no (P=0.0000)