Glucose4 () valid proof: s VERIFIED
Glucose4 () formula minus clause 0: s NOT VERIFIED: lemma 1 (proof line ~1) is not RUP
Glucose4 () formula minus clause 50: s NOT VERIFIED: lemma 208 (proof line ~208) is not RUP
Glucose4 () formula minus clause 150: s NOT VERIFIED: lemma 3 (proof line ~3) is not RUP
Glucose4 () formula minus clause 203: s NOT VERIFIED: lemma 471 (proof line ~471) is not RUP
Glucose4 ('-d',) valid proof: s VERIFIED
Glucose4 ('-d',) formula minus clause 0: s NOT VERIFIED: lemma 1 (proof line ~1) is not RUP
Glucose4 ('-d',) formula minus clause 50: s NOT VERIFIED: lemma 208 (proof line ~208) is not RUP
Glucose4 ('-d',) formula minus clause 150: s NOT VERIFIED: lemma 3 (proof line ~3) is not RUP
Glucose4 ('-d',) formula minus clause 203: s NOT VERIFIED: lemma 471 (proof line ~471) is not RUP
Glucose4 truncated proof: s NOT VERIFIED: the proof does not derive the empty clause
Lingeling () valid proof: s VERIFIED
Lingeling () formula minus clause 0: s NOT VERIFIED: lemma 1 (proof line ~1) is not RUP
Lingeling () formula minus clause 50: s NOT VERIFIED: lemma 217 (proof line ~217) is not RUP
Lingeling () formula minus clause 150: s NOT VERIFIED: lemma 7 (proof line ~7) is not RUP
Lingeling () formula minus clause 203: s NOT VERIFIED: lemma 166 (proof line ~166) is not RUP
Lingeling ('-d',) valid proof: s VERIFIED
Lingeling ('-d',) formula minus clause 0: s NOT VERIFIED: lemma 1 (proof line ~1) is not RUP
Lingeling ('-d',) formula minus clause 50: s NOT VERIFIED: lemma 217 (proof line ~217) is not RUP
Lingeling ('-d',) formula minus clause 150: s NOT VERIFIED: lemma 7 (proof line ~7) is not RUP
Lingeling ('-d',) formula minus clause 203: s NOT VERIFIED: lemma 166 (proof line ~166) is not RUP
Lingeling truncated proof: s NOT VERIFIED: the proof does not derive the empty clause
n7_D6 valid: s VERIFIED
n7_D6 with one formula clause removed (every 97th of 7722): rejected 9, still verified 71
n7_D6 proof with a random unit lemma inserted near the start: rejected 17 of 20
satisfiable formula, proof "0": s NOT VERIFIED: lemma 1 (proof line ~1) is not RUP
SELFTEST PASS
