[FORMULA 27 14 e 1 0 a 2 0 e 3 4 5 6 0 a 7 0 e 8 9 10 11 0 a 12 0 e 13 14 15 16 0 0 0 c show clause numbers 1: 13 1 0 2: 14 1 0 3: 15 -1 0 4: 16 -1 0 5: -4 -3 2 0 6: -6 -5 -2 0 7: -9 -8 3 -7 0 8: -9 -8 4 7 0 9: -11 -10 5 -7 0 10: -11 -10 6 7 0 11: -14 -13 8 12 0 12: -14 -13 9 -12 0 13: -16 -15 10 12 0 14: -16 -15 11 -12 0 ] [NOGOOD 15 15 -1 0 6 -6 -5 -2 0 9 5 0 10 6 0 13 10 0 14 11 0 4 16 0 3 15 0 ] c Use res_q as left-associative infix operator c 6 res_{-5} 9 = [-2 -6 -7 -10 -11] ... c res_{-6} 10 = [-2 7 -7 -10 -11] ... c res_{-10} 13 = [-2 7 -7 -11 12 -15 -16] ... c res_{-11} 14 = [-2 7 -7 12 -12 -15 -16] c ^^^ Notice that universals 7, -7 are outer to the clashing variable! c Suppose clause 14 had 7 or -7. Would this be safe?? c c res_{-16} 4 res_{-15} 3 = [-1 -2 7 -7 12 -12] unrd_{many} = [-1]. [NOGOOD 0 0 0 5 -4 -3 2 0 7 3 0 8 4 0 11 8 0 12 9 0 2 14 0 1 13 0 15 1 0 ] c 15 1 0 looks wrong at first because clause 15 (learned) is [-1]. c However, the clashing VARIABLE is shown, rather than the clashing LITERAL c in the left operand. [END qdpllexp_1.qdimacs ]