REFUTATION ========== policy policy.co sha256 470bfaea5ca9297edde3c6f9dd1287ac090b0db94091edd9bf067c4d63c22ec5 parse clean: the circuit carries every edge the file describes unroll none question can respond with permitted pension answer fire with is_pension_transfer_specialist false? pin respond with permitted pension answer = 1 (action) pin is_pension_transfer_specialist = 0 (obligation) pin has_safeguarded_benefits = 1 (conditioning) pin transfer_value_over_30k = 1 (conditioning) origin derived replayable yes Every row below follows from the policy and the pins. Replay the steps and the contradiction appears. VARIABLES --------- ask pension transfer advice intent, policy.co:128 | define user ask pension transfer advice $is_factual_information_only context, policy.co:209, flow investment specific product | if $is_factual_information_only and not $personal_recommendation and not $is_inducement $personal_recommendation context, policy.co:209, flow investment specific product | if $is_factual_information_only and not $personal_recommendation and not $is_inducement $has_advising_permission context, policy.co:219, flow investment specific product | if not $firm_is_authorised or not $has_advising_permission $suitability_assessment_done context, policy.co:229, flow investment specific product | if not $suitability_assessment_done or not $risk_profile_assessed or not $capacity_for_loss_assessed $has_safeguarded_benefits context, policy.co:378, flow pension transfer gate | if $has_safeguarded_benefits $transfer_value_over_30k context, policy.co:379, flow pension transfer gate | if $transfer_value_over_30k and not $is_pension_transfer_specialist x8 gate, policy.co:379, flow pension transfer gate | if $transfer_value_over_30k and not $is_pension_transfer_specialist defined as x8 + $transfer_value_over_30k*aux_20 = 0 introduced quadratic-split note Both inputs of an XOR were AND gates, which would have put two quadratic terms in one equation; the first was split into its own variable to keep exactly one. x9 gate, policy.co:385, flow pension transfer gate | stop defined as x9 + $personal_recommendation*aux_20 + x8 = 0 x10 gate, policy.co:385, flow pension transfer gate | stop defined as x10 + x8*aux_21 + x9 = 0 x11 gate, policy.co:389, flow pension transfer gate | stop defined as x11 + x10 + aux_20*aux_22 = 0 x12 gate, policy.co:389, flow pension transfer gate | stop defined as x12 + x10*aux_23 + x11 = 0 x13 gate, policy.co:393, flow pension transfer gate | stop defined as x13 + x12 + aux_20*aux_24 = 0 x14 gate, policy.co:393, flow pension transfer gate | stop defined as x14 + x12*aux_25 + x13 = 0 x15 gate, policy.co:396, flow pension transfer gate | stop defined as x15 + ask pension transfer advice*$has_safeguarded_benefits + x14 = 0 x16 gate, policy.co:396, flow pension transfer gate | stop defined as x16 + x14*aux_20 + x15 = 0 x17 gate, policy.co:400, flow pension transfer gate | stop defined as x17 + ask pension transfer advice*aux_26 + x16 = 0 x18 gate, policy.co:400, flow pension transfer gate | stop defined as x18 + x16*aux_27 + x17 = 0 respond with permitted pension answer action, policy.co:402, flow pension transfer gate | bot respond with permitted pension answer defined as respond with permitted pension answer + ask pension transfer advice + ask pension transfer advice*x18 = 0 introduced forced-materialisation note This wire is protected or pinned, so it could not be absorbed into the equation that uses it; it stayed an explicit variable with a defining equation of its own. aux_20 aux defined as aux_20 + ask pension transfer advice*$has_safeguarded_benefits = 0 introduced degree3-materialisation because An AND gate fed another AND gate, which would have made the equation cubic; the inner one was given its own variable to keep the system quasilinear. aux_21 aux defined as aux_21 + $personal_recommendation*aux_20 = 0 introduced degree3-materialisation because An AND gate fed another AND gate, which would have made the equation cubic; the inner one was given its own variable to keep the system quasilinear. aux_22 aux defined as aux_22 + $personal_recommendation + $personal_recommendation*$suitability_assessment_done = 0 introduced degree3-materialisation because An AND gate fed another AND gate, which would have made the equation cubic; the inner one was given its own variable to keep the system quasilinear. aux_23 aux defined as aux_23 + aux_20*aux_22 = 0 introduced degree3-materialisation because An AND gate fed another AND gate, which would have made the equation cubic; the inner one was given its own variable to keep the system quasilinear. aux_24 aux defined as aux_24 + $is_factual_information_only + $is_factual_information_only*$personal_recommendation = 0 introduced degree3-materialisation because An AND gate fed another AND gate, which would have made the equation cubic; the inner one was given its own variable to keep the system quasilinear. aux_25 aux defined as aux_25 + aux_20*aux_24 = 0 introduced degree3-materialisation because An AND gate fed another AND gate, which would have made the equation cubic; the inner one was given its own variable to keep the system quasilinear. aux_26 aux defined as aux_26 + $personal_recommendation + $personal_recommendation*$has_advising_permission = 0 introduced degree3-materialisation because An AND gate fed another AND gate, which would have made the equation cubic; the inner one was given its own variable to keep the system quasilinear. aux_27 aux defined as aux_27 + ask pension transfer advice*aux_26 = 0 introduced degree3-materialisation because An AND gate fed another AND gate, which would have made the equation cubic; the inner one was given its own variable to keep the system quasilinear. aux_33 aux defined as aux_33 + x15 + x16 + x17 = 0 introduced expandability-padding because Padding introduced by the compiler so that every variable appears in the linear set, which the solver requires. It stands for nothing in the policy. aux_34 aux defined as aux_34 + x18 + respond with permitted pension answer + aux_20 = 0 introduced expandability-padding because Padding introduced by the compiler so that every variable appears in the linear set, which the solver requires. It stands for nothing in the policy. DERIVATION ---------- 1 aux_34 + aux_20 + respond with permitted pension answer + x18 = 0 compiler padding, so that every variable appears linearly (not policy logic) 2 multiply step 1 by x14 3 x14*aux_20 + x16 + x15 = 0 policy.co:396, flow pension transfer gate | stop 4 add step 2 to step 3 5 respond with permitted pension answer = 1 reads as respond with permitted pension answer holds pinned by this run: respond with permitted pension answer = 1 (not a line of the policy) 6 multiply step 5 by x14 7 add step 4 to step 6 8 multiply step 1 by ask pension transfer advice 9 ask pension transfer advice*$has_safeguarded_benefits + aux_20 = 0 compiled from the policy; no position recorded 10 add step 8 to step 9 11 ask pension transfer advice*x18 + respond with permitted pension answer + ask pension transfer advice = 0 policy.co:402, flow pension transfer gate | bot respond with permitted pension answer 12 add step 10 to step 11 13 multiply step 5 by ask pension transfer advice 14 add step 12 to step 13 15 multiply step 9 by ask pension transfer advice 16 add step 14 to step 15 17 multiply step 16 by aux_34 18 multiply step 1 by aux_20 19 add step 17 to step 18 20 multiply step 1 by respond with permitted pension answer 21 add step 19 to step 20 22 ask pension transfer advice*$has_safeguarded_benefits + x15 + x14 = 0 policy.co:396, flow pension transfer gate | stop 23 add step 22 to step 9 24 multiply step 23 by x18 25 add step 21 to step 24 26 multiply step 5 by x18 27 add step 25 to step 26 28 aux_33 + x17 + x16 + x15 = 0 compiler padding, so that every variable appears linearly (not policy logic) 29 multiply step 28 by x16 30 add step 29 to step 3 31 multiply step 3 by x14 32 add step 31 to step 3 33 add step 30 to step 32 34 multiply step 3 by aux_20 35 multiply step 23 by x16 36 add step 34 to step 35 37 multiply step 23 by x15 38 add step 36 to step 37 39 add step 33 to step 38 40 ask pension transfer advice*aux_26 + aux_27 = 0 compiled from the policy; no position recorded 41 ask pension transfer advice*aux_26 + x17 + x16 = 0 policy.co:400, flow pension transfer gate | stop 42 add step 40 to step 41 43 multiply step 42 by x16 44 x16*aux_27 + x18 + x17 = 0 policy.co:400, flow pension transfer gate | stop 45 add step 43 to step 44 46 add step 39 to step 45 47 multiply step 46 by aux_33 48 multiply step 28 by x18 49 add step 47 to step 48 50 multiply step 28 by x17 51 add step 49 to step 50 52 multiply step 44 by aux_27 53 multiply step 42 by x18 54 add step 52 to step 53 55 multiply step 42 by x17 56 add step 54 to step 55 57 add step 51 to step 56 58 add step 57 to step 29 59 add step 58 to step 44 60 add step 59 to step 45 61 multiply step 28 by x15 62 add step 60 to step 61 63 add step 27 to step 62 64 add step 7 to step 63 65 multiply step 64 by aux_34 66 add step 65 to step 18 67 add step 66 to step 20 68 multiply step 1 by x18 69 add step 67 to step 68 70 multiply step 1 by x16 71 add step 69 to step 70 72 add step 71 to step 35 73 multiply step 5 by x16 74 add step 72 to step 73 75 multiply step 44 by x16 76 add step 75 to step 44 77 add step 74 to step 76 78 add step 77 to step 45 79 add step 78 to step 38 80 add step 79 to step 3 81 multiply step 23 by x14 82 add step 81 to step 3 83 add step 80 to step 82 84 add step 83 to step 8 85 add step 84 to step 15 86 add step 85 to step 13 87 add step 86 to step 11 88 add step 87 to step 9 89 multiply step 11 by x18 90 add step 89 to step 26 91 add step 88 to step 90 92 $has_safeguarded_benefits = 1 reads as $has_safeguarded_benefits holds pinned by this run: has_safeguarded_benefits = 1 (not a line of the policy) 93 multiply step 92 by ask pension transfer advice 94 add step 93 to step 9 95 add step 94 to step 23 96 add step 91 to step 95 97 multiply step 11 by ask pension transfer advice 98 add step 97 to step 13 99 add step 98 to step 11 100 add step 99 to step 5 final add step 96 to step 100 -> 0 = 1 WHAT THIS ESTABLISHES --------------------- The derivation is valid: the listed steps really do combine the listed rows into 0 = 1. It does not establish that those rows are the policy. The citations above say where each row was compiled from, and they are the compiler's own record rather than an independent check of it -- closing that second hop means re-deriving the circuit and comparing.