c rupToRes based on: zChaff SAT05 SE Certified UNSAT c (modified by AVG for conversion of RUP to RES L32) c Solving fudge05-04.cnf ...... c WARNING: 256-byte header absent on fudge05-04.rup c __nvars, __ncls, __debug_len 54 46 54 c CONSISTENT during preprocess c Begin proving c max_clauses 194 c max_conflict_clauses 148 c max_proof_value_dbl 308 c max_proof_value 308 c Proof label of last input clause is 46 c Proof label of last phase1 clause is 193 c Empty clause generated. c Proof label of last phase2 clause is 205 s UNSATISFIABLE c Max Decision Level 1 c Num. of Decisions 196 c Original Num Variables 54 c Original Num Clauses 46 c Original Num Literals 102 c Added Conflict Clauses 148 c Number of Implication 1357 c Total Run Time 0.006998 c RESULT: UNSAT Command exited with non-zero status 20 real 0.18 user 0.00 sys 0.00 -rw-r--r-- 1 avg users 7828 Apr 23 01:17 fudge05-04.proof -rw-r--r-- 1 avg users 4711 Mar 12 03:34 fudge05-04.rup FOUND 46 378 205 2336 in fudge05-04.log sysMmap 0 8192 4096 200112 4 4 4 16384 fmla 1957 0 206 sysMmap 2048 206 = pt.allocLines, 824 = callocBytes BEGIN loading cnf file; up to 5 comments and p-line are echoed. c 5 pigeons and 4 holes p cnf 54 46 553 = p.allocCnf, 2212 = mallocBytes, 7828 = mmapBytes END loading cnf file. 256-byte header of input_proof_file: %RESL32 54 46 fudge05-04.proof generated by rupToRes, based on zChaff SAT05 SE Contact: avg@cs.ucsc.edu END of header BEGIN loadProof END loadProof BEGIN proof check Final: Clause has label 205 and 0 literals. REFUTATION IS VALID END proof check real 0.00 user 0.00 sys 0.00 c rupToRes based on: zChaff SAT05 SE Certified UNSAT c (modified by AVG for conversion of RUP to RES L32) c Solving testeq.cnf ...... c WARNING: 256-byte header absent on testeq.rup c __nvars, __ncls, __debug_len 5 9 5 c CONSISTENT during preprocess c Begin proving c max_clauses 13 c max_conflict_clauses 4 c max_proof_value_dbl 12 c max_proof_value 12 c Proof label of last input clause is 9 c Proof label of last phase1 clause is 12 c Empty clause generated. c Proof label of last phase2 clause is 17 s UNSATISFIABLE c Max Decision Level 1 c Num. of Decisions 3 c Original Num Variables 5 c Original Num Clauses 9 c Original Num Literals 22 c Added Conflict Clauses 4 c Number of Implication 14 c Total Run Time 0.000999 c RESULT: UNSAT Command exited with non-zero status 20 real 0.01 user 0.00 sys 0.00 -rw-r--r-- 1 avg users 504 Apr 23 01:17 testeq.proof -rw-r--r-- 1 avg users 118 Mar 11 22:29 testeq.rup FOUND 9 76 17 203 in testeq.log sysMmap 0 4096 4096 200112 4 4 4 16384 fmla 126 0 18 sysMmap 1024 18 = pt.allocLines, 72 = callocBytes BEGIN loading cnf file; up to 5 comments and p-line are echoed. p cnf 5 9 109 = p.allocCnf, 436 = mallocBytes, 504 = mmapBytes END loading cnf file. 256-byte header of input_proof_file: %RESL32 5 9 testeq.proof generated by rupToRes, based on zChaff SAT05 SE Contact: avg@cs.ucsc.edu END of header BEGIN loadProof END loadProof BEGIN proof check Final: Clause has label 17 and 0 literals. REFUTATION IS VALID END proof check real 0.00 user 0.00 sys 0.00 c rupToRes based on: zChaff SAT05 SE Certified UNSAT c (modified by AVG for conversion of RUP to RES L32) c Solving 5pipe.cnf ...... c WARNING: 256-byte header absent on 5pipe.rup c __nvars, __ncls, __debug_len 9471 195452 10 c CONSISTENT during preprocess c Begin proving c max_clauses 206720 c max_conflict_clauses 11268 c max_proof_value_dbl 156730 c max_proof_value 156730 c Proof label of last input clause is 195452 c Proof label of last phase1 clause is 268441 c Empty clause generated. c Proof label of last phase2 clause is 268877 s UNSATISFIABLE c Max Decision Level 1 c Num. of Decisions 11310 c Original Num Variables 9471 c Original Num Clauses 195452 c Original Num Literals 569976 c Added Conflict Clauses 11268 c Number of Implication 18299519 c Total Run Time 18.9571 c RESULT: UNSAT Command exited with non-zero status 20 real 25.70 user 18.54 sys 0.41 -rw-r--r-- 1 avg users 77360896 Apr 23 01:17 5pipe.proof -rw-r--r-- 1 avg users 4227711 Mar 18 10:02 5pipe.rup FOUND 195452 1742688 268877 21082913 in 5pipe.log sysMmap 0 77361152 4096 200112 4 4 4 16384 fmla 19340224 0 268878 sysMmap 19340288 268878 = pt.allocLines, 1075512 = callocBytes BEGIN loading cnf file; up to 5 comments and p-line are echoed. p cnf 9471 195452 2345425 = p.allocCnf, 9381700 = mallocBytes, 77360896 = mmapBytes END loading cnf file. 256-byte header of input_proof_file: %RESL32 9471 195452 5pipe.proof generated by rupToRes, based on zChaff SAT05 SE Contact: avg@cs.ucsc.edu END of header BEGIN loadProof END loadProof BEGIN proof check Final: Clause has label 268877 and 0 literals. REFUTATION IS VALID END proof check real 1.18 user 1.11 sys 0.06