#backward-chaining

A rule system has these rules (?x, ?y are variables) and assertions:

P0: IF (?x is a noob) OR (?x is disenchanted)        THEN ?x visits The Oracle
P1: IF ?x visits The Oracle                          THEN ?x picks The One
P2: IF ?x is a noob AND ?x visits The Oracle         THEN The Oracle says ?x is not The One,
                                                          ?x is disenchanted
P3: IF (?x is disenchanted OR ?x is a noob)
       AND The Oracle says ?x is not The One         THEN ?x practices Kung Fu
P4: IF ?x is disenchanted AND ?x loves ?y            THEN ?x proclaims love for ?y
P5: IF The Oracle says ?x is not The One
       AND ?y proclaims love for ?x
       AND ?y picks The One                          THEN ?x is The One

A0: Neo is a noob            A1: Trinity is disenchanted
A2: Trinity loves Neo        A3: Trinity proclaims love for Neo

A backward chainer checks the assertions first, then tries rules whose consequent matches, in order, and evaluates antecedents in order with short-circuiting. What happens with the hypothesis "Neo is The One"?