rm: cannot remove `/tmp/part*': No such file or directory rm: cannot remove `/tmp/res*': No such file or directory c found empty clause in proof and put it in core c finished parsing c 23090 of 25142 clauses in core c 5757105 of 6812396 lemmas in core using 469808891 resolution steps c 16023 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 55m33.734s user 55m28.280s sys 0m2.490s 13299804 real 0m2.910s user 0m0.312s sys 0m2.330s c printing post-CNF file with 8414 variables and 108258 clauses c printing post-CNF file with 8414 variables and 161824 clauses c printing post-CNF file with 8414 variables and 212586 clauses c printing post-CNF file with 8414 variables and 233532 clauses c printing post-CNF file with 8414 variables and 224110 clauses c printing post-CNF file with 8414 variables and 272068 clauses c printing post-CNF file with 8414 variables and 214450 clauses c printing post-CNF file with 8414 variables and 300514 clauses c printing post-CNF file with 8414 variables and 339732 clauses c printing post-CNF file with 8414 variables and 332168 clauses c printing post-CNF file with 8414 variables and 277798 clauses c printing post-CNF file with 8414 variables and 270642 clauses c printing post-CNF file with 8414 variables and 360274 clauses c printing post-CNF file with 8414 variables and 292170 clauses c printing post-CNF file with 8414 variables and 312752 clauses c printing post-CNF file with 8414 variables and 350130 clauses real 1m25.704s user 1m23.129s sys 0m2.234s /work/02055/marijn/sbp/EDP2_1161.cnf c reading proof from stdin c empty clause not found in proof, put 191374 lemmas in core c placed 81965 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 24446 of 25142 clauses in core c 412249 of 565435 lemmas in core using 22595852 resolution steps c 16825 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res00 c reading proof from stdin c empty clause not found in proof, put 227622 lemmas in core c placed 57697 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 35495 of 108258 clauses in core c 357095 of 604226 lemmas in core using 28254935 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res01 c reading proof from stdin c empty clause not found in proof, put 310842 lemmas in core c placed 76274 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 44218 of 161824 clauses in core c 360987 of 653586 lemmas in core using 28794196 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res02 c reading proof from stdin c empty clause not found in proof, put 339923 lemmas in core c placed 78864 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 50346 of 212586 clauses in core c 371064 of 659624 lemmas in core using 30047147 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res03 c reading proof from stdin c empty clause not found in proof, put 309990 lemmas in core c placed 71829 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 54769 of 233532 clauses in core c 372921 of 635018 lemmas in core using 30131097 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res04 c reading proof from stdin c empty clause not found in proof, put 397728 lemmas in core c placed 96267 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 58621 of 224110 clauses in core c 395087 of 711666 lemmas in core using 32330591 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res05 c reading proof from stdin c empty clause not found in proof, put 274021 lemmas in core c placed 47711 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 61100 of 272068 clauses in core c 340713 of 601260 lemmas in core using 28800234 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res06 c reading proof from stdin c empty clause not found in proof, put 438759 lemmas in core c placed 100683 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 66010 of 214450 clauses in core c 410901 of 759165 lemmas in core using 34096560 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res07 c reading proof from stdin c empty clause not found in proof, put 509365 lemmas in core c placed 121994 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 69862 of 300514 clauses in core c 405045 of 774960 lemmas in core using 34034112 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res08 c reading proof from stdin c empty clause not found in proof, put 486872 lemmas in core c placed 110405 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 71551 of 339732 clauses in core c 389907 of 744005 lemmas in core using 33393274 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res09 c reading proof from stdin c empty clause not found in proof, put 373298 lemmas in core c placed 70389 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 71639 of 332168 clauses in core c 358107 of 666232 lemmas in core using 31351851 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res10 c reading proof from stdin c empty clause not found in proof, put 353076 lemmas in core c placed 71869 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 75077 of 277798 clauses in core c 382211 of 682683 lemmas in core using 34076512 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res11 c reading proof from stdin c empty clause not found in proof, put 527798 lemmas in core c placed 121331 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 78893 of 270642 clauses in core c 430000 of 820709 lemmas in core using 39909286 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res12 c reading proof from stdin c empty clause not found in proof, put 384260 lemmas in core c placed 78251 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 76287 of 360274 clauses in core c 357538 of 673737 lemmas in core using 33245322 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res13 c reading proof from stdin c empty clause not found in proof, put 424597 lemmas in core c placed 76122 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 79760 of 292170 clauses in core c 399267 of 738662 lemmas in core using 38776254 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res14 c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 73785 of 312752 clauses in core c 395029 of 784436 lemmas in core using 42585702 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 54m48.781s user 54m46.064s sys 0m4.216s c reading proof from stdin c empty clause not found in proof, put 191374 lemmas in core c placed 81965 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 24446 of 25142 clauses in core c 412249 of 565435 lemmas in core using 22595852 resolution steps c 16825 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 310842 lemmas in core c placed 76274 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 44218 of 161824 clauses in core c 360987 of 653586 lemmas in core using 28794196 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 227622 lemmas in core c placed 57697 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 35495 of 108258 clauses in core c 357095 of 604226 lemmas in core using 28254935 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 339923 lemmas in core c placed 78864 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 50346 of 212586 clauses in core c 371064 of 659624 lemmas in core using 30047147 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 309990 lemmas in core c placed 71829 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 54769 of 233532 clauses in core c 372921 of 635018 lemmas in core using 30131097 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 397728 lemmas in core c placed 96267 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 58621 of 224110 clauses in core c 395087 of 711666 lemmas in core using 32330591 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 274021 lemmas in core c placed 47711 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 61100 of 272068 clauses in core c 340713 of 601260 lemmas in core using 28800234 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 373298 lemmas in core c placed 70389 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 71639 of 332168 clauses in core c 358107 of 666232 lemmas in core using 31351851 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 438759 lemmas in core c placed 100683 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 66010 of 214450 clauses in core c 410901 of 759165 lemmas in core using 34096560 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 353076 lemmas in core c placed 71869 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 75077 of 277798 clauses in core c 382211 of 682683 lemmas in core using 34076512 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 73785 of 312752 clauses in core c 395029 of 784436 lemmas in core using 42585702 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 384260 lemmas in core c placed 78251 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 76287 of 360274 clauses in core c 357538 of 673737 lemmas in core using 33245322 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 486872 lemmas in core c placed 110405 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 71551 of 339732 clauses in core c 389907 of 744005 lemmas in core using 33393274 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 509365 lemmas in core c placed 121994 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 69862 of 300514 clauses in core c 405045 of 774960 lemmas in core using 34034112 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 424597 lemmas in core c placed 76122 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 79760 of 292170 clauses in core c 399267 of 738662 lemmas in core using 38776254 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 527798 lemmas in core c placed 121331 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 78893 of 270642 clauses in core c 430000 of 820709 lemmas in core using 39909286 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 7m38.264s user 80m48.409s sys 0m5.131s c found empty clause in proof and put it in core c finished parsing c 6120 of 6120 clauses in core c 275370 of 275373 lemmas in core using 1648216 resolution steps c 8576 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m2.555s user 0m2.409s sys 0m0.073s 556412 real 0m0.047s user 0m0.005s sys 0m0.029s c printing post-CNF file with 285 variables and 6212 clauses c printing post-CNF file with 417 variables and 6276 clauses c printing post-CNF file with 516 variables and 6304 clauses c printing post-CNF file with 648 variables and 6312 clauses c printing post-CNF file with 747 variables and 6270 clauses c printing post-CNF file with 879 variables and 6342 clauses c printing post-CNF file with 978 variables and 6272 clauses c printing post-CNF file with 1110 variables and 6268 clauses c printing post-CNF file with 1209 variables and 5672 clauses c printing post-CNF file with 1341 variables and 5870 clauses c printing post-CNF file with 1473 variables and 5694 clauses c printing post-CNF file with 1605 variables and 5304 clauses c printing post-CNF file with 1770 variables and 3864 clauses c printing post-CNF file with 2067 variables and 1836 clauses c printing post-CNF file with 2595 variables and 2078 clauses c printing post-CNF file with 2594 variables and 455 clauses real 0m1.910s user 0m1.189s sys 0m0.702s /work/02055/marijn/sbp/R_4_4_18.cnf c reading proof from stdin c empty clause not found in proof, put 11719 lemmas in core c placed 5506 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5415 of 6120 clauses in core c 17435 of 23646 lemmas in core using 77741 resolution steps c 516 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res00 c reading proof from stdin c empty clause not found in proof, put 11863 lemmas in core c placed 5587 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5525 of 6212 clauses in core c 17421 of 23696 lemmas in core using 77943 resolution steps c 516 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res01 c reading proof from stdin c empty clause not found in proof, put 11881 lemmas in core c placed 5577 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5616 of 6276 clauses in core c 17403 of 23706 lemmas in core using 78247 resolution steps c 387 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res02 c reading proof from stdin c empty clause not found in proof, put 11884 lemmas in core c placed 5572 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5574 of 6304 clauses in core c 17393 of 23704 lemmas in core using 77840 resolution steps c 516 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res03 c reading proof from stdin c empty clause not found in proof, put 11783 lemmas in core c placed 5513 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5579 of 6312 clauses in core c 17368 of 23637 lemmas in core using 78581 resolution steps c 387 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res04 c reading proof from stdin c empty clause not found in proof, put 11891 lemmas in core c placed 5549 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5510 of 6270 clauses in core c 17425 of 23766 lemmas in core using 78589 resolution steps c 516 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res05 c reading proof from stdin c empty clause not found in proof, put 11751 lemmas in core c placed 5479 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5640 of 6342 clauses in core c 17354 of 23625 lemmas in core using 78446 resolution steps c 387 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res06 c reading proof from stdin c empty clause not found in proof, put 11772 lemmas in core c placed 5503 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5558 of 6272 clauses in core c 17387 of 23654 lemmas in core using 79175 resolution steps c 516 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res07 c reading proof from stdin c empty clause not found in proof, put 10681 lemmas in core c placed 5009 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5706 of 6268 clauses in core c 17091 of 22762 lemmas in core using 81989 resolution steps c 378 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res08 c reading proof from stdin c empty clause not found in proof, put 11164 lemmas in core c placed 5293 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5212 of 5672 clauses in core c 17488 of 23357 lemmas in core using 79774 resolution steps c 512 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res09 c reading proof from stdin c empty clause not found in proof, put 10807 lemmas in core c placed 5112 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5372 of 5870 clauses in core c 17301 of 22994 lemmas in core using 78692 resolution steps c 512 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res10 c reading proof from stdin c empty clause not found in proof, put 9852 lemmas in core c placed 4547 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4982 of 5694 clauses in core c 17193 of 22497 lemmas in core using 79005 resolution steps c 511 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res11 c reading proof from stdin c empty clause not found in proof, put 7363 lemmas in core c placed 3499 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5000 of 5304 clauses in core c 16669 of 20532 lemmas in core using 80249 resolution steps c 620 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res12 c reading proof from stdin c empty clause not found in proof, put 3370 lemmas in core c placed 1534 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 3716 of 3864 clauses in core c 16375 of 18210 lemmas in core using 76449 resolution steps c 1020 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res13 c reading proof from stdin c empty clause not found in proof, put 3901 lemmas in core c placed 1776 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1764 of 1836 clauses in core c 17509 of 19587 lemmas in core using 174793 resolution steps c 1282 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res14 c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 1743 of 2078 clauses in core c 16571 of 17029 lemmas in core using 379224 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m4.196s user 0m3.516s sys 0m0.729s c reading proof from stdin c empty clause not found in proof, put 11783 lemmas in core c placed 5513 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5579 of 6312 clauses in core c 17368 of 23637 lemmas in core using 78581 resolution steps c 387 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 11719 lemmas in core c placed 5506 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5415 of 6120 clauses in core c 17435 of 23646 lemmas in core using 77741 resolution steps c 516 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 11881 lemmas in core c placed 5577 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5616 of 6276 clauses in core c 17403 of 23706 lemmas in core using 78247 resolution steps c 387 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 11863 lemmas in core c placed 5587 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5525 of 6212 clauses in core c 17421 of 23696 lemmas in core using 77943 resolution steps c 516 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 11772 lemmas in core c placed 5503 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5558 of 6272 clauses in core c 17387 of 23654 lemmas in core using 79175 resolution steps c 516 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 11164 lemmas in core c placed 5293 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5212 of 5672 clauses in core c 17488 of 23357 lemmas in core using 79774 resolution steps c 512 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 7363 lemmas in core c placed 3499 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5000 of 5304 clauses in core c 16669 of 20532 lemmas in core using 80249 resolution steps c 620 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 10807 lemmas in core c placed 5112 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5372 of 5870 clauses in core c 17301 of 22994 lemmas in core using 78692 resolution steps c 512 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 10681 lemmas in core c placed 5009 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5706 of 6268 clauses in core c 17091 of 22762 lemmas in core using 81989 resolution steps c 378 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 1743 of 2078 clauses in core c 16571 of 17029 lemmas in core using 379224 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 11891 lemmas in core c placed 5549 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5510 of 6270 clauses in core c 17425 of 23766 lemmas in core using 78589 resolution steps c 516 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 9852 lemmas in core c placed 4547 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4982 of 5694 clauses in core c 17193 of 22497 lemmas in core using 79005 resolution steps c 511 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 3370 lemmas in core c placed 1534 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 3716 of 3864 clauses in core c 16375 of 18210 lemmas in core using 76449 resolution steps c 1020 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 11751 lemmas in core c placed 5479 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5640 of 6342 clauses in core c 17354 of 23625 lemmas in core using 78446 resolution steps c 387 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 11884 lemmas in core c placed 5572 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5574 of 6304 clauses in core c 17393 of 23704 lemmas in core using 77840 resolution steps c 516 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 3901 lemmas in core c placed 1776 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1764 of 1836 clauses in core c 17509 of 19587 lemmas in core using 174793 resolution steps c 1282 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m0.429s user 0m3.755s sys 0m0.730s c found empty clause in proof and put it in core c finished parsing c 1729 of 1729 clauses in core c 61356 of 61559 lemmas in core using 220801 resolution steps c 4862 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m0.614s user 0m0.502s sys 0m0.056s 124541 real 0m0.014s user 0m0.002s sys 0m0.005s c printing post-CNF file with 164 variables and 1855 clauses c printing post-CNF file with 240 variables and 1959 clauses c printing post-CNF file with 308 variables and 2065 clauses c printing post-CNF file with 380 variables and 2151 clauses c printing post-CNF file with 469 variables and 2325 clauses c printing post-CNF file with 543 variables and 2443 clauses c printing post-CNF file with 614 variables and 2529 clauses c printing post-CNF file with 706 variables and 2741 clauses c printing post-CNF file with 776 variables and 2799 clauses c printing post-CNF file with 869 variables and 2925 clauses c printing post-CNF file with 938 variables and 3055 clauses c printing post-CNF file with 1031 variables and 3107 clauses c printing post-CNF file with 1118 variables and 3137 clauses c printing post-CNF file with 1248 variables and 2987 clauses c printing post-CNF file with 1537 variables and 2629 clauses c printing post-CNF file with 1537 variables and 306 clauses real 0m1.246s user 0m0.554s sys 0m0.675s /work/02055/marijn/sbp/tph6.cnf c reading proof from stdin c empty clause not found in proof, put 3197 lemmas in core c placed 1342 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1216 of 1729 clauses in core c 3947 of 5810 lemmas in core using 11073 resolution steps c 262 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res00 c reading proof from stdin c empty clause not found in proof, put 3521 lemmas in core c placed 1562 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1464 of 1855 clauses in core c 3943 of 5903 lemmas in core using 11399 resolution steps c 254 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res01 c reading proof from stdin c empty clause not found in proof, put 3720 lemmas in core c placed 1655 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1563 of 1959 clauses in core c 3944 of 6010 lemmas in core using 11765 resolution steps c 224 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res02 c reading proof from stdin c empty clause not found in proof, put 3827 lemmas in core c placed 1676 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1599 of 2065 clauses in core c 3925 of 6086 lemmas in core using 11468 resolution steps c 240 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res03 c reading proof from stdin c empty clause not found in proof, put 3970 lemmas in core c placed 1644 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1476 of 2151 clauses in core c 3979 of 6304 lemmas in core using 11828 resolution steps c 298 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res04 c reading proof from stdin c empty clause not found in proof, put 4027 lemmas in core c placed 1584 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1478 of 2325 clauses in core c 3945 of 6394 lemmas in core using 11413 resolution steps c 236 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res05 c reading proof from stdin c empty clause not found in proof, put 4199 lemmas in core c placed 1670 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1593 of 2443 clauses in core c 3915 of 6464 lemmas in core using 11662 resolution steps c 242 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res06 c reading proof from stdin c empty clause not found in proof, put 4389 lemmas in core c placed 1648 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1455 of 2529 clauses in core c 3998 of 6739 lemmas in core using 11639 resolution steps c 316 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res07 c reading proof from stdin c empty clause not found in proof, put 4444 lemmas in core c placed 1645 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1611 of 2741 clauses in core c 3899 of 6720 lemmas in core using 11474 resolution steps c 236 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res08 c reading proof from stdin c empty clause not found in proof, put 4490 lemmas in core c placed 1565 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1442 of 2799 clauses in core c 3955 of 6880 lemmas in core using 11775 resolution steps c 279 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res09 c reading proof from stdin c empty clause not found in proof, put 4660 lemmas in core c placed 1605 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1475 of 2925 clauses in core c 3919 of 7012 lemmas in core using 11600 resolution steps c 291 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res10 c reading proof from stdin c empty clause not found in proof, put 4565 lemmas in core c placed 1458 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1408 of 3055 clauses in core c 3912 of 7025 lemmas in core using 11720 resolution steps c 334 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res11 c reading proof from stdin c empty clause not found in proof, put 4517 lemmas in core c placed 1380 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1380 of 3107 clauses in core c 3896 of 7044 lemmas in core using 11938 resolution steps c 316 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res12 c reading proof from stdin c empty clause not found in proof, put 4079 lemmas in core c placed 1092 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1243 of 3137 clauses in core c 3811 of 6804 lemmas in core using 11040 resolution steps c 489 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res13 c reading proof from stdin c empty clause not found in proof, put 3184 lemmas in core c placed 553 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1066 of 2987 clauses in core c 3693 of 6342 lemmas in core using 19893 resolution steps c 845 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res14 c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 2581 of 2629 clauses in core c 2688 of 3035 lemmas in core using 40477 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m2.035s user 0m1.307s sys 0m0.741s c reading proof from stdin c empty clause not found in proof, put 3521 lemmas in core c placed 1562 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1464 of 1855 clauses in core c 3943 of 5903 lemmas in core using 11399 resolution steps c 254 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 2581 of 2629 clauses in core c 2688 of 3035 lemmas in core using 40477 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 4027 lemmas in core c placed 1584 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1478 of 2325 clauses in core c 3945 of 6394 lemmas in core using 11413 resolution steps c 236 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 3197 lemmas in core c placed 1342 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1216 of 1729 clauses in core c 3947 of 5810 lemmas in core using 11073 resolution steps c 262 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 4199 lemmas in core c placed 1670 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1593 of 2443 clauses in core c 3915 of 6464 lemmas in core using 11662 resolution steps c 242 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 4444 lemmas in core c placed 1645 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1611 of 2741 clauses in core c 3899 of 6720 lemmas in core using 11474 resolution steps c 236 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 4565 lemmas in core c placed 1458 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1408 of 3055 clauses in core c 3912 of 7025 lemmas in core using 11720 resolution steps c 334 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 3970 lemmas in core c placed 1644 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1476 of 2151 clauses in core c 3979 of 6304 lemmas in core using 11828 resolution steps c 298 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 4660 lemmas in core c placed 1605 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1475 of 2925 clauses in core c 3919 of 7012 lemmas in core using 11600 resolution steps c 291 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 4490 lemmas in core c placed 1565 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1442 of 2799 clauses in core c 3955 of 6880 lemmas in core using 11775 resolution steps c 279 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 3184 lemmas in core c placed 553 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1066 of 2987 clauses in core c 3693 of 6342 lemmas in core using 19893 resolution steps c 845 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 3720 lemmas in core c placed 1655 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1563 of 1959 clauses in core c 3944 of 6010 lemmas in core using 11765 resolution steps c 224 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 4517 lemmas in core c placed 1380 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1380 of 3107 clauses in core c 3896 of 7044 lemmas in core using 11938 resolution steps c 316 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 3827 lemmas in core c placed 1676 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1599 of 2065 clauses in core c 3925 of 6086 lemmas in core using 11468 resolution steps c 240 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 4389 lemmas in core c placed 1648 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1455 of 2529 clauses in core c 3998 of 6739 lemmas in core using 11639 resolution steps c 316 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 4079 lemmas in core c placed 1092 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1243 of 3137 clauses in core c 3811 of 6804 lemmas in core using 11040 resolution steps c 489 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m0.222s user 0m1.616s sys 0m0.701s c found empty clause in proof and put it in core c finished parsing c 3200 of 3200 clauses in core c 125743 of 126219 lemmas in core using 453736 resolution steps c 7535 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m1.304s user 0m1.183s sys 0m0.055s 255227 real 0m0.020s user 0m0.001s sys 0m0.011s c printing post-CNF file with 226 variables and 3362 clauses c printing post-CNF file with 330 variables and 3416 clauses c printing post-CNF file with 457 variables and 3542 clauses c printing post-CNF file with 583 variables and 3710 clauses c printing post-CNF file with 690 variables and 3912 clauses c printing post-CNF file with 816 variables and 4034 clauses c printing post-CNF file with 919 variables and 4172 clauses c printing post-CNF file with 1048 variables and 4476 clauses c printing post-CNF file with 1173 variables and 4588 clauses c printing post-CNF file with 1297 variables and 4800 clauses c printing post-CNF file with 1426 variables and 4994 clauses c printing post-CNF file with 1549 variables and 5152 clauses c printing post-CNF file with 1700 variables and 4944 clauses c printing post-CNF file with 1866 variables and 4562 clauses c printing post-CNF file with 2388 variables and 4136 clauses c printing post-CNF file with 2388 variables and 413 clauses real 0m1.386s user 0m0.661s sys 0m0.707s /work/02055/marijn/sbp/tph7.cnf c reading proof from stdin c empty clause not found in proof, put 5558 lemmas in core c placed 2196 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2034 of 3200 clauses in core c 8043 of 11419 lemmas in core using 23226 resolution steps c 366 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res00 c reading proof from stdin c empty clause not found in proof, put 6129 lemmas in core c placed 2713 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2691 of 3362 clauses in core c 8001 of 11419 lemmas in core using 23264 resolution steps c 314 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res01 c reading proof from stdin c empty clause not found in proof, put 6520 lemmas in core c placed 2977 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2855 of 3416 clauses in core c 8029 of 11581 lemmas in core using 23670 resolution steps c 390 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res02 c reading proof from stdin c empty clause not found in proof, put 6807 lemmas in core c placed 3097 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2932 of 3542 clauses in core c 8048 of 11770 lemmas in core using 23687 resolution steps c 402 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res03 c reading proof from stdin c empty clause not found in proof, put 6905 lemmas in core c placed 2993 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2804 of 3710 clauses in core c 8074 of 11989 lemmas in core using 24358 resolution steps c 356 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res04 c reading proof from stdin c empty clause not found in proof, put 6974 lemmas in core c placed 2940 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2830 of 3912 clauses in core c 8017 of 12071 lemmas in core using 23551 resolution steps c 402 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res05 c reading proof from stdin c empty clause not found in proof, put 7228 lemmas in core c placed 3056 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2938 of 4034 clauses in core c 8022 of 12217 lemmas in core using 23978 resolution steps c 344 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res06 c reading proof from stdin c empty clause not found in proof, put 7519 lemmas in core c placed 3043 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2753 of 4172 clauses in core c 8128 of 12604 lemmas in core using 24777 resolution steps c 456 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res07 c reading proof from stdin c empty clause not found in proof, put 7474 lemmas in core c placed 2886 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2791 of 4476 clauses in core c 7987 of 12620 lemmas in core using 23625 resolution steps c 402 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res08 c reading proof from stdin c empty clause not found in proof, put 7897 lemmas in core c placed 3097 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2897 of 4588 clauses in core c 8036 of 12882 lemmas in core using 24340 resolution steps c 450 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res09 c reading proof from stdin c empty clause not found in proof, put 7876 lemmas in core c placed 2882 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2695 of 4800 clauses in core c 8062 of 13067 lemmas in core using 23869 resolution steps c 438 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res10 c reading proof from stdin c empty clause not found in proof, put 8094 lemmas in core c placed 2942 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2808 of 4994 clauses in core c 7997 of 13207 lemmas in core using 24308 resolution steps c 450 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res11 c reading proof from stdin c empty clause not found in proof, put 7362 lemmas in core c placed 2418 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2628 of 5152 clauses in core c 7855 of 12816 lemmas in core using 23687 resolution steps c 544 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res12 c reading proof from stdin c empty clause not found in proof, put 6429 lemmas in core c placed 1867 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2285 of 4944 clauses in core c 7770 of 12347 lemmas in core using 24179 resolution steps c 585 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res13 c reading proof from stdin c empty clause not found in proof, put 5327 lemmas in core c placed 1190 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1753 of 4562 clauses in core c 7757 of 11899 lemmas in core using 28588 resolution steps c 1643 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res14 c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 4056 of 4136 clauses in core c 5940 of 6524 lemmas in core using 93217 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m2.704s user 0m1.983s sys 0m0.752s c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 4056 of 4136 clauses in core c 5940 of 6524 lemmas in core using 93217 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 6129 lemmas in core c placed 2713 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2691 of 3362 clauses in core c 8001 of 11419 lemmas in core using 23264 resolution steps c 314 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 6807 lemmas in core c placed 3097 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2932 of 3542 clauses in core c 8048 of 11770 lemmas in core using 23687 resolution steps c 402 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 5558 lemmas in core c placed 2196 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2034 of 3200 clauses in core c 8043 of 11419 lemmas in core using 23226 resolution steps c 366 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 6905 lemmas in core c placed 2993 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2804 of 3710 clauses in core c 8074 of 11989 lemmas in core using 24358 resolution steps c 356 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 6974 lemmas in core c placed 2940 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2830 of 3912 clauses in core c 8017 of 12071 lemmas in core using 23551 resolution steps c 402 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 7474 lemmas in core c placed 2886 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2791 of 4476 clauses in core c 7987 of 12620 lemmas in core using 23625 resolution steps c 402 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 8094 lemmas in core c placed 2942 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2808 of 4994 clauses in core c 7997 of 13207 lemmas in core using 24308 resolution steps c 450 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 7897 lemmas in core c placed 3097 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2897 of 4588 clauses in core c 8036 of 12882 lemmas in core using 24340 resolution steps c 450 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 7876 lemmas in core c placed 2882 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2695 of 4800 clauses in core c 8062 of 13067 lemmas in core using 23869 resolution steps c 438 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 6520 lemmas in core c placed 2977 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2855 of 3416 clauses in core c 8029 of 11581 lemmas in core using 23670 resolution steps c 390 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 7519 lemmas in core c placed 3043 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2753 of 4172 clauses in core c 8128 of 12604 lemmas in core using 24777 resolution steps c 456 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 7228 lemmas in core c placed 3056 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2938 of 4034 clauses in core c 8022 of 12217 lemmas in core using 23978 resolution steps c 344 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 5327 lemmas in core c placed 1190 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 1753 of 4562 clauses in core c 7757 of 11899 lemmas in core using 28588 resolution steps c 1643 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 7362 lemmas in core c placed 2418 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2628 of 5152 clauses in core c 7855 of 12816 lemmas in core using 23687 resolution steps c 544 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 6429 lemmas in core c placed 1867 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 2285 of 4944 clauses in core c 7770 of 12347 lemmas in core using 24179 resolution steps c 585 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m0.289s user 0m2.268s sys 0m0.717s c found empty clause in proof and put it in core c finished parsing c 5457 of 5457 clauses in core c 251101 of 253958 lemmas in core using 956313 resolution steps c 11277 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m2.978s user 0m2.849s sys 0m0.061s 512808 real 0m0.030s user 0m0.005s sys 0m0.016s c printing post-CNF file with 322 variables and 5624 clauses c printing post-CNF file with 491 variables and 5801 clauses c printing post-CNF file with 682 variables and 6042 clauses c printing post-CNF file with 850 variables and 6267 clauses c printing post-CNF file with 1042 variables and 6618 clauses c printing post-CNF file with 1233 variables and 6977 clauses c printing post-CNF file with 1405 variables and 7206 clauses c printing post-CNF file with 1596 variables and 7499 clauses c printing post-CNF file with 1786 variables and 7884 clauses c printing post-CNF file with 1984 variables and 8289 clauses c printing post-CNF file with 2148 variables and 8482 clauses c printing post-CNF file with 2337 variables and 8921 clauses c printing post-CNF file with 2558 variables and 8606 clauses c printing post-CNF file with 2796 variables and 8151 clauses c printing post-CNF file with 3505 variables and 6718 clauses c printing post-CNF file with 3505 variables and 565 clauses real 0m1.617s user 0m0.919s sys 0m0.681s /work/02055/marijn/sbp/tph8.cnf c reading proof from stdin c empty clause not found in proof, put 9476 lemmas in core c placed 3852 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 3685 of 5457 clauses in core c 16093 of 21733 lemmas in core using 46164 resolution steps c 552 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res00 c reading proof from stdin c empty clause not found in proof, put 10168 lemmas in core c placed 4366 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4195 of 5624 clauses in core c 16107 of 21915 lemmas in core using 48080 resolution steps c 531 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res01 c reading proof from stdin c empty clause not found in proof, put 11095 lemmas in core c placed 5053 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4821 of 5801 clauses in core c 16128 of 22188 lemmas in core using 47557 resolution steps c 603 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res02 c reading proof from stdin c empty clause not found in proof, put 11562 lemmas in core c placed 5294 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5073 of 6042 clauses in core c 16108 of 22405 lemmas in core using 48364 resolution steps c 558 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res03 c reading proof from stdin c empty clause not found in proof, put 12082 lemmas in core c placed 5464 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5116 of 6267 clauses in core c 16150 of 22819 lemmas in core using 49197 resolution steps c 658 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res04 c reading proof from stdin c empty clause not found in proof, put 12333 lemmas in core c placed 5356 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5002 of 6618 clauses in core c 16206 of 23182 lemmas in core using 49279 resolution steps c 652 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res05 c reading proof from stdin c empty clause not found in proof, put 12397 lemmas in core c placed 5191 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4964 of 6977 clauses in core c 16095 of 23346 lemmas in core using 48549 resolution steps c 558 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res06 c reading proof from stdin c empty clause not found in proof, put 12894 lemmas in core c placed 5395 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5117 of 7206 clauses in core c 16116 of 23671 lemmas in core using 48919 resolution steps c 636 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res07 c reading proof from stdin c empty clause not found in proof, put 13381 lemmas in core c placed 5497 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5123 of 7499 clauses in core c 16170 of 24102 lemmas in core using 49254 resolution steps c 678 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res08 c reading proof from stdin c empty clause not found in proof, put 13613 lemmas in core c placed 5324 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4926 of 7884 clauses in core c 16222 of 24517 lemmas in core using 48556 resolution steps c 708 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res09 c reading proof from stdin c empty clause not found in proof, put 13683 lemmas in core c placed 5201 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5086 of 8289 clauses in core c 16025 of 24604 lemmas in core using 48950 resolution steps c 559 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res10 c reading proof from stdin c empty clause not found in proof, put 14321 lemmas in core c placed 5400 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4971 of 8482 clauses in core c 16184 of 25166 lemmas in core using 49792 resolution steps c 739 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res11 c reading proof from stdin c empty clause not found in proof, put 13038 lemmas in core c placed 4432 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4750 of 8921 clauses in core c 15815 of 24474 lemmas in core using 48018 resolution steps c 744 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res12 c reading proof from stdin c empty clause not found in proof, put 12000 lemmas in core c placed 3849 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4329 of 8606 clauses in core c 15754 of 23949 lemmas in core using 49940 resolution steps c 867 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res13 c reading proof from stdin c empty clause not found in proof, put 8622 lemmas in core c placed 1896 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 3406 of 8151 clauses in core c 15292 of 22027 lemmas in core using 53161 resolution steps c 2245 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res14 c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 6625 of 6718 clauses in core c 12381 of 13510 lemmas in core using 232318 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m4.293s user 0m3.599s sys 0m0.739s c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 6625 of 6718 clauses in core c 12381 of 13510 lemmas in core using 232318 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 9476 lemmas in core c placed 3852 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 3685 of 5457 clauses in core c 16093 of 21733 lemmas in core using 46164 resolution steps c 552 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 11562 lemmas in core c placed 5294 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5073 of 6042 clauses in core c 16108 of 22405 lemmas in core using 48364 resolution steps c 558 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 11095 lemmas in core c placed 5053 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4821 of 5801 clauses in core c 16128 of 22188 lemmas in core using 47557 resolution steps c 603 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 12397 lemmas in core c placed 5191 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4964 of 6977 clauses in core c 16095 of 23346 lemmas in core using 48549 resolution steps c 558 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 12082 lemmas in core c placed 5464 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5116 of 6267 clauses in core c 16150 of 22819 lemmas in core using 49197 resolution steps c 658 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 12333 lemmas in core c placed 5356 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5002 of 6618 clauses in core c 16206 of 23182 lemmas in core using 49279 resolution steps c 652 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 12894 lemmas in core c placed 5395 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5117 of 7206 clauses in core c 16116 of 23671 lemmas in core using 48919 resolution steps c 636 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 13683 lemmas in core c placed 5201 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5086 of 8289 clauses in core c 16025 of 24604 lemmas in core using 48950 resolution steps c 559 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 13381 lemmas in core c placed 5497 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5123 of 7499 clauses in core c 16170 of 24102 lemmas in core using 49254 resolution steps c 678 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 13613 lemmas in core c placed 5324 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4926 of 7884 clauses in core c 16222 of 24517 lemmas in core using 48556 resolution steps c 708 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 13038 lemmas in core c placed 4432 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4750 of 8921 clauses in core c 15815 of 24474 lemmas in core using 48018 resolution steps c 744 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 12000 lemmas in core c placed 3849 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4329 of 8606 clauses in core c 15754 of 23949 lemmas in core using 49940 resolution steps c 867 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 10168 lemmas in core c placed 4366 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4195 of 5624 clauses in core c 16107 of 21915 lemmas in core using 48080 resolution steps c 531 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 14321 lemmas in core c placed 5400 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 4971 of 8482 clauses in core c 16184 of 25166 lemmas in core using 49792 resolution steps c 739 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 8622 lemmas in core c placed 1896 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 3406 of 8151 clauses in core c 15292 of 22027 lemmas in core using 53161 resolution steps c 2245 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m0.457s user 0m4.017s sys 0m0.719s c found empty clause in proof and put it in core c finished parsing c 8740 of 8740 clauses in core c 454851 of 459333 lemmas in core using 1783973 resolution steps c 15940 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m6.174s user 0m6.024s sys 0m0.081s 926690 real 0m0.040s user 0m0.008s sys 0m0.028s c printing post-CNF file with 435 variables and 9199 clauses c printing post-CNF file with 678 variables and 9376 clauses c printing post-CNF file with 946 variables and 9645 clauses c printing post-CNF file with 1217 variables and 10028 clauses c printing post-CNF file with 1460 variables and 10449 clauses c printing post-CNF file with 1730 variables and 10972 clauses c printing post-CNF file with 2000 variables and 11475 clauses c printing post-CNF file with 2247 variables and 11952 clauses c printing post-CNF file with 2516 variables and 12299 clauses c printing post-CNF file with 2785 variables and 12672 clauses c printing post-CNF file with 3053 variables and 13161 clauses c printing post-CNF file with 3355 variables and 13754 clauses c printing post-CNF file with 3623 variables and 13579 clauses c printing post-CNF file with 3945 variables and 12898 clauses c printing post-CNF file with 4924 variables and 9193 clauses c printing post-CNF file with 4924 variables and 716 clauses real 0m1.976s user 0m1.261s sys 0m0.699s /work/02055/marijn/sbp/tph9.cnf c reading proof from stdin c empty clause not found in proof, put 15108 lemmas in core c placed 5909 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5450 of 8740 clauses in core c 29176 of 38388 lemmas in core using 86743 resolution steps c 889 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res00 c reading proof from stdin c empty clause not found in proof, put 16424 lemmas in core c placed 7048 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 6874 of 9199 clauses in core c 29019 of 38424 lemmas in core using 85872 resolution steps c 726 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res01 c reading proof from stdin c empty clause not found in proof, put 17483 lemmas in core c placed 7838 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 7577 of 9376 clauses in core c 29074 of 38739 lemmas in core using 87093 resolution steps c 842 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res02 c reading proof from stdin c empty clause not found in proof, put 18449 lemmas in core c placed 8421 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8039 of 9645 clauses in core c 29110 of 39179 lemmas in core using 87367 resolution steps c 872 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res03 c reading proof from stdin c empty clause not found in proof, put 19175 lemmas in core c placed 8726 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8315 of 10028 clauses in core c 29120 of 39619 lemmas in core using 88593 resolution steps c 835 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res04 c reading proof from stdin c empty clause not found in proof, put 19894 lemmas in core c placed 8922 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8402 of 10449 clauses in core c 29150 of 40193 lemmas in core using 88811 resolution steps c 925 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res05 c reading proof from stdin c empty clause not found in proof, put 20384 lemmas in core c placed 8909 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8410 of 10972 clauses in core c 29140 of 40686 lemmas in core using 89059 resolution steps c 925 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res06 c reading proof from stdin c empty clause not found in proof, put 20652 lemmas in core c placed 8700 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8248 of 11475 clauses in core c 29182 of 41150 lemmas in core using 88984 resolution steps c 840 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res07 c reading proof from stdin c empty clause not found in proof, put 21058 lemmas in core c placed 8759 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8437 of 11952 clauses in core c 29062 of 41432 lemmas in core using 88396 resolution steps c 896 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res08 c reading proof from stdin c empty clause not found in proof, put 21392 lemmas in core c placed 8720 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8362 of 12299 clauses in core c 29047 of 41818 lemmas in core using 88614 resolution steps c 924 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res09 c reading proof from stdin c empty clause not found in proof, put 21877 lemmas in core c placed 8716 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8235 of 12672 clauses in core c 29085 of 42365 lemmas in core using 90113 resolution steps c 991 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res10 c reading proof from stdin c empty clause not found in proof, put 22264 lemmas in core c placed 8510 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 7929 of 13161 clauses in core c 29218 of 43010 lemmas in core using 88997 resolution steps c 1059 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res11 c reading proof from stdin c empty clause not found in proof, put 21410 lemmas in core c placed 7831 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8056 of 13754 clauses in core c 28664 of 42451 lemmas in core using 88524 resolution steps c 931 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res12 c reading proof from stdin c empty clause not found in proof, put 19716 lemmas in core c placed 6818 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 7510 of 13579 clauses in core c 28574 of 41517 lemmas in core using 89880 resolution steps c 1205 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res13 c reading proof from stdin c empty clause not found in proof, put 11555 lemmas in core c placed 2356 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 6183 of 12898 clauses in core c 27092 of 36300 lemmas in core using 88951 resolution steps c 3092 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res14 c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 9045 of 9193 clauses in core c 23103 of 25430 lemmas in core using 471769 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m7.337s user 0m6.642s sys 0m0.768s c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 9045 of 9193 clauses in core c 23103 of 25430 lemmas in core using 471769 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 15108 lemmas in core c placed 5909 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 5450 of 8740 clauses in core c 29176 of 38388 lemmas in core using 86743 resolution steps c 889 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 17483 lemmas in core c placed 7838 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 7577 of 9376 clauses in core c 29074 of 38739 lemmas in core using 87093 resolution steps c 842 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 16424 lemmas in core c placed 7048 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 6874 of 9199 clauses in core c 29019 of 38424 lemmas in core using 85872 resolution steps c 726 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 20384 lemmas in core c placed 8909 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8410 of 10972 clauses in core c 29140 of 40686 lemmas in core using 89059 resolution steps c 925 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 18449 lemmas in core c placed 8421 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8039 of 9645 clauses in core c 29110 of 39179 lemmas in core using 87367 resolution steps c 872 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 21058 lemmas in core c placed 8759 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8437 of 11952 clauses in core c 29062 of 41432 lemmas in core using 88396 resolution steps c 896 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 21392 lemmas in core c placed 8720 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8362 of 12299 clauses in core c 29047 of 41818 lemmas in core using 88614 resolution steps c 924 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 21410 lemmas in core c placed 7831 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8056 of 13754 clauses in core c 28664 of 42451 lemmas in core using 88524 resolution steps c 931 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 21877 lemmas in core c placed 8716 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8235 of 12672 clauses in core c 29085 of 42365 lemmas in core using 90113 resolution steps c 991 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 19716 lemmas in core c placed 6818 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 7510 of 13579 clauses in core c 28574 of 41517 lemmas in core using 89880 resolution steps c 1205 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 19175 lemmas in core c placed 8726 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8315 of 10028 clauses in core c 29120 of 39619 lemmas in core using 88593 resolution steps c 835 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 19894 lemmas in core c placed 8922 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8402 of 10449 clauses in core c 29150 of 40193 lemmas in core using 88811 resolution steps c 925 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 20652 lemmas in core c placed 8700 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8248 of 11475 clauses in core c 29182 of 41150 lemmas in core using 88984 resolution steps c 840 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 22264 lemmas in core c placed 8510 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 7929 of 13161 clauses in core c 29218 of 43010 lemmas in core using 88997 resolution steps c 1059 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 11555 lemmas in core c placed 2356 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 6183 of 12898 clauses in core c 27092 of 36300 lemmas in core using 88951 resolution steps c 3092 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m0.828s user 0m6.950s sys 0m0.773s c found empty clause in proof and put it in core c finished parsing c 13321 of 13321 clauses in core c 768132 of 774985 lemmas in core using 3120727 resolution steps c 21532 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m11.783s user 0m11.616s sys 0m0.099s 1562362 real 0m0.061s user 0m0.013s sys 0m0.044s c printing post-CNF file with 562 variables and 13579 clauses c printing post-CNF file with 922 variables and 13901 clauses c printing post-CNF file with 1285 variables and 14481 clauses c printing post-CNF file with 1642 variables and 14745 clauses c printing post-CNF file with 1973 variables and 15147 clauses c printing post-CNF file with 2333 variables and 15715 clauses c printing post-CNF file with 2693 variables and 16369 clauses c printing post-CNF file with 3053 variables and 17047 clauses c printing post-CNF file with 3442 variables and 17789 clauses c printing post-CNF file with 3810 variables and 18459 clauses c printing post-CNF file with 4167 variables and 19047 clauses c printing post-CNF file with 4555 variables and 19555 clauses c printing post-CNF file with 4943 variables and 20057 clauses c printing post-CNF file with 5361 variables and 18819 clauses c printing post-CNF file with 6681 variables and 12209 clauses c printing post-CNF file with 6681 variables and 930 clauses real 0m2.526s user 0m1.803s sys 0m0.702s /work/02055/marijn/sbp/tph10.cnf c reading proof from stdin c empty clause not found in proof, put 22593 lemmas in core c placed 9014 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8756 of 13321 clauses in core c 48923 of 62532 lemmas in core using 142700 resolution steps c 1032 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res00 c reading proof from stdin c empty clause not found in proof, put 24746 lemmas in core c placed 10845 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 10525 of 13579 clauses in core c 48938 of 62886 lemmas in core using 145894 resolution steps c 1080 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res01 c reading proof from stdin c empty clause not found in proof, put 26256 lemmas in core c placed 11775 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 11200 of 13901 clauses in core c 49073 of 63595 lemmas in core using 147919 resolution steps c 1140 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res02 c reading proof from stdin c empty clause not found in proof, put 27330 lemmas in core c placed 12585 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12344 of 14481 clauses in core c 48859 of 63701 lemmas in core using 147551 resolution steps c 1116 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res03 c reading proof from stdin c empty clause not found in proof, put 28106 lemmas in core c placed 12959 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12570 of 14745 clauses in core c 48969 of 64172 lemmas in core using 148294 resolution steps c 1063 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res04 c reading proof from stdin c empty clause not found in proof, put 29066 lemmas in core c placed 13351 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12790 of 15147 clauses in core c 49009 of 64823 lemmas in core using 149344 resolution steps c 1198 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res05 c reading proof from stdin c empty clause not found in proof, put 30001 lemmas in core c placed 13632 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12986 of 15715 clauses in core c 49046 of 65520 lemmas in core using 150415 resolution steps c 1243 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res06 c reading proof from stdin c empty clause not found in proof, put 30659 lemmas in core c placed 13612 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12938 of 16369 clauses in core c 49029 of 66210 lemmas in core using 150060 resolution steps c 1263 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res07 c reading proof from stdin c empty clause not found in proof, put 31429 lemmas in core c placed 13640 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12903 of 17047 clauses in core c 49064 of 66984 lemmas in core using 150775 resolution steps c 1354 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res08 c reading proof from stdin c empty clause not found in proof, put 31815 lemmas in core c placed 13356 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12693 of 17789 clauses in core c 49144 of 67618 lemmas in core using 151284 resolution steps c 1319 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res09 c reading proof from stdin c empty clause not found in proof, put 32185 lemmas in core c placed 13138 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12613 of 18459 clauses in core c 48980 of 68165 lemmas in core using 151416 resolution steps c 1206 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res10 c reading proof from stdin c empty clause not found in proof, put 32711 lemmas in core c placed 13156 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12666 of 19047 clauses in core c 48878 of 68633 lemmas in core using 150852 resolution steps c 1357 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res11 c reading proof from stdin c empty clause not found in proof, put 32957 lemmas in core c placed 12900 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12412 of 19555 clauses in core c 48844 of 69132 lemmas in core using 152570 resolution steps c 1431 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res12 c reading proof from stdin c empty clause not found in proof, put 29659 lemmas in core c placed 10840 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12084 of 20057 clauses in core c 48154 of 67024 lemmas in core using 150324 resolution steps c 1608 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res13 c reading proof from stdin c empty clause not found in proof, put 15272 lemmas in core c placed 3058 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 9732 of 18819 clauses in core c 45455 of 57728 lemmas in core using 146201 resolution steps c 4136 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res14 c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 12031 of 12209 clauses in core c 39929 of 44111 lemmas in core using 905507 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m12.672s user 0m11.960s sys 0m0.825s c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 12031 of 12209 clauses in core c 39929 of 44111 lemmas in core using 905507 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 22593 lemmas in core c placed 9014 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 8756 of 13321 clauses in core c 48923 of 62532 lemmas in core using 142700 resolution steps c 1032 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 24746 lemmas in core c placed 10845 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 10525 of 13579 clauses in core c 48938 of 62886 lemmas in core using 145894 resolution steps c 1080 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 27330 lemmas in core c placed 12585 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12344 of 14481 clauses in core c 48859 of 63701 lemmas in core using 147551 resolution steps c 1116 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 30001 lemmas in core c placed 13632 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12986 of 15715 clauses in core c 49046 of 65520 lemmas in core using 150415 resolution steps c 1243 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 30659 lemmas in core c placed 13612 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12938 of 16369 clauses in core c 49029 of 66210 lemmas in core using 150060 resolution steps c 1263 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 31429 lemmas in core c placed 13640 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12903 of 17047 clauses in core c 49064 of 66984 lemmas in core using 150775 resolution steps c 1354 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 32185 lemmas in core c placed 13138 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12613 of 18459 clauses in core c 48980 of 68165 lemmas in core using 151416 resolution steps c 1206 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 32711 lemmas in core c placed 13156 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12666 of 19047 clauses in core c 48878 of 68633 lemmas in core using 150852 resolution steps c 1357 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 26256 lemmas in core c placed 11775 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 11200 of 13901 clauses in core c 49073 of 63595 lemmas in core using 147919 resolution steps c 1140 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 31815 lemmas in core c placed 13356 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12693 of 17789 clauses in core c 49144 of 67618 lemmas in core using 151284 resolution steps c 1319 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 28106 lemmas in core c placed 12959 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12570 of 14745 clauses in core c 48969 of 64172 lemmas in core using 148294 resolution steps c 1063 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 29066 lemmas in core c placed 13351 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12790 of 15147 clauses in core c 49009 of 64823 lemmas in core using 149344 resolution steps c 1198 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 29659 lemmas in core c placed 10840 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12084 of 20057 clauses in core c 48154 of 67024 lemmas in core using 150324 resolution steps c 1608 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 32957 lemmas in core c placed 12900 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12412 of 19555 clauses in core c 48844 of 69132 lemmas in core using 152570 resolution steps c 1431 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 15272 lemmas in core c placed 3058 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 9732 of 18819 clauses in core c 45455 of 57728 lemmas in core using 146201 resolution steps c 4136 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m1.321s user 0m12.328s sys 0m0.763s c found empty clause in proof and put it in core c finished parsing c 19504 of 19504 clauses in core c 1243907 of 1252478 lemmas in core using 5382007 resolution steps c 28932 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m22.521s user 0m22.305s sys 0m0.128s 2523325 real 0m0.095s user 0m0.028s sys 0m0.063s c printing post-CNF file with 740 variables and 20296 clauses c printing post-CNF file with 1200 variables and 20656 clauses c printing post-CNF file with 1665 variables and 21192 clauses c printing post-CNF file with 2158 variables and 21794 clauses c printing post-CNF file with 2622 variables and 22488 clauses c printing post-CNF file with 3118 variables and 23324 clauses c printing post-CNF file with 3581 variables and 23984 clauses c printing post-CNF file with 4076 variables and 24976 clauses c printing post-CNF file with 4571 variables and 25950 clauses c printing post-CNF file with 5066 variables and 26870 clauses c printing post-CNF file with 5560 variables and 27710 clauses c printing post-CNF file with 6053 variables and 28390 clauses c printing post-CNF file with 6580 variables and 29180 clauses c printing post-CNF file with 7150 variables and 26710 clauses c printing post-CNF file with 8812 variables and 16456 clauses c printing post-CNF file with 8812 variables and 1137 clauses real 0m3.386s user 0m2.666s sys 0m0.701s /work/02055/marijn/sbp/tph11.cnf c reading proof from stdin c empty clause not found in proof, put 33095 lemmas in core c placed 12799 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12007 of 19504 clauses in core c 79186 of 99546 lemmas in core using 240000 resolution steps c 1564 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res00 c reading proof from stdin c empty clause not found in proof, put 36097 lemmas in core c placed 15441 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 15098 of 20296 clauses in core c 78990 of 99690 lemmas in core using 238830 resolution steps c 1474 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res01 c reading proof from stdin c empty clause not found in proof, put 38141 lemmas in core c placed 16949 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 16414 of 20656 clauses in core c 79073 of 100314 lemmas in core using 236288 resolution steps c 1449 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res02 c reading proof from stdin c empty clause not found in proof, put 40147 lemmas in core c placed 18353 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 17764 of 21192 clauses in core c 79061 of 100949 lemmas in core using 239135 resolution steps c 1558 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res03 c reading proof from stdin c empty clause not found in proof, put 41429 lemmas in core c placed 18941 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 18251 of 21794 clauses in core c 79105 of 101689 lemmas in core using 240201 resolution steps c 1511 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res04 c reading proof from stdin c empty clause not found in proof, put 42815 lemmas in core c placed 19491 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 18663 of 22488 clauses in core c 79162 of 102596 lemmas in core using 241747 resolution steps c 1645 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res05 c reading proof from stdin c empty clause not found in proof, put 43632 lemmas in core c placed 19648 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 19011 of 23324 clauses in core c 79070 of 103168 lemmas in core using 241912 resolution steps c 1565 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res06 c reading proof from stdin c empty clause not found in proof, put 45019 lemmas in core c placed 20043 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 19067 of 23984 clauses in core c 79205 of 104326 lemmas in core using 243095 resolution steps c 1728 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res07 c reading proof from stdin c empty clause not found in proof, put 46069 lemmas in core c placed 20119 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 19158 of 24976 clauses in core c 79196 of 105291 lemmas in core using 244511 resolution steps c 1758 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res08 c reading proof from stdin c empty clause not found in proof, put 46868 lemmas in core c placed 19998 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 19108 of 25950 clauses in core c 79106 of 106184 lemmas in core using 244413 resolution steps c 1757 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res09 c reading proof from stdin c empty clause not found in proof, put 47511 lemmas in core c placed 19801 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 19001 of 26870 clauses in core c 79030 of 106984 lemmas in core using 244397 resolution steps c 1797 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res10 c reading proof from stdin c empty clause not found in proof, put 47734 lemmas in core c placed 19344 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 18691 of 27710 clauses in core c 78941 of 107584 lemmas in core using 244089 resolution steps c 1809 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res11 c reading proof from stdin c empty clause not found in proof, put 48139 lemmas in core c placed 18959 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 18173 of 28390 clauses in core c 79014 of 108429 lemmas in core using 244634 resolution steps c 1972 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res12 c reading proof from stdin c empty clause not found in proof, put 41796 lemmas in core c placed 15086 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 17559 of 29180 clauses in core c 77526 of 104329 lemmas in core using 240650 resolution steps c 2071 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res13 c reading proof from stdin c empty clause not found in proof, put 20139 lemmas in core c placed 3671 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 14298 of 26710 clauses in core c 73516 of 90183 lemmas in core using 326888 resolution steps c 5290 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res14 c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 16142 of 16456 clauses in core c 65222 of 72329 lemmas in core using 1695080 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m22.635s user 0m21.999s sys 0m0.816s c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 16142 of 16456 clauses in core c 65222 of 72329 lemmas in core using 1695080 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 33095 lemmas in core c placed 12799 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 12007 of 19504 clauses in core c 79186 of 99546 lemmas in core using 240000 resolution steps c 1564 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 36097 lemmas in core c placed 15441 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 15098 of 20296 clauses in core c 78990 of 99690 lemmas in core using 238830 resolution steps c 1474 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 38141 lemmas in core c placed 16949 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 16414 of 20656 clauses in core c 79073 of 100314 lemmas in core using 236288 resolution steps c 1449 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 42815 lemmas in core c placed 19491 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 18663 of 22488 clauses in core c 79162 of 102596 lemmas in core using 241747 resolution steps c 1645 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 43632 lemmas in core c placed 19648 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 19011 of 23324 clauses in core c 79070 of 103168 lemmas in core using 241912 resolution steps c 1565 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 40147 lemmas in core c placed 18353 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 17764 of 21192 clauses in core c 79061 of 100949 lemmas in core using 239135 resolution steps c 1558 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 45019 lemmas in core c placed 20043 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 19067 of 23984 clauses in core c 79205 of 104326 lemmas in core using 243095 resolution steps c 1728 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 46868 lemmas in core c placed 19998 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 19108 of 25950 clauses in core c 79106 of 106184 lemmas in core using 244413 resolution steps c 1757 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 41429 lemmas in core c placed 18941 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 18251 of 21794 clauses in core c 79105 of 101689 lemmas in core using 240201 resolution steps c 1511 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 46069 lemmas in core c placed 20119 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 19158 of 24976 clauses in core c 79196 of 105291 lemmas in core using 244511 resolution steps c 1758 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 41796 lemmas in core c placed 15086 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 17559 of 29180 clauses in core c 77526 of 104329 lemmas in core using 240650 resolution steps c 2071 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 47511 lemmas in core c placed 19801 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 19001 of 26870 clauses in core c 79030 of 106984 lemmas in core using 244397 resolution steps c 1797 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 48139 lemmas in core c placed 18959 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 18173 of 28390 clauses in core c 79014 of 108429 lemmas in core using 244634 resolution steps c 1972 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 47734 lemmas in core c placed 19344 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 18691 of 27710 clauses in core c 78941 of 107584 lemmas in core using 244089 resolution steps c 1809 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 20139 lemmas in core c placed 3671 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 14298 of 26710 clauses in core c 73516 of 90183 lemmas in core using 326888 resolution steps c 5290 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m2.852s user 0m22.627s sys 0m0.844s c found empty clause in proof and put it in core c finished parsing c 27625 of 27625 clauses in core c 1948286 of 1966472 lemmas in core using 9258720 resolution steps c 36972 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m39.433s user 0m39.150s sys 0m0.185s 3959136 real 0m0.152s user 0m0.034s sys 0m0.114s c printing post-CNF file with 902 variables and 28086 clauses c printing post-CNF file with 1552 variables and 28659 clauses c printing post-CNF file with 2164 variables and 29534 clauses c printing post-CNF file with 2811 variables and 30553 clauses c printing post-CNF file with 3462 variables and 31642 clauses c printing post-CNF file with 4080 variables and 32673 clauses c printing post-CNF file with 4718 variables and 33746 clauses c printing post-CNF file with 5367 variables and 34907 clauses c printing post-CNF file with 5979 variables and 35946 clauses c printing post-CNF file with 6627 variables and 37099 clauses c printing post-CNF file with 7311 variables and 38334 clauses c printing post-CNF file with 7958 variables and 39439 clauses c printing post-CNF file with 8641 variables and 40624 clauses c printing post-CNF file with 9372 variables and 36829 clauses c printing post-CNF file with 11353 variables and 20858 clauses c printing post-CNF file with 11353 variables and 1434 clauses real 0m4.729s user 0m4.017s sys 0m0.688s /work/02055/marijn/sbp/tph12.cnf c reading proof from stdin c empty clause not found in proof, put 46362 lemmas in core c placed 18276 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 17815 of 27625 clauses in core c 123894 of 152040 lemmas in core using 363089 resolution steps c 1750 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res00 c reading proof from stdin c empty clause not found in proof, put 50280 lemmas in core c placed 21621 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 21051 of 28086 clauses in core c 123950 of 152669 lemmas in core using 371761 resolution steps c 1956 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res01 c reading proof from stdin c empty clause not found in proof, put 53784 lemmas in core c placed 24250 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 23383 of 28659 clauses in core c 124031 of 153695 lemmas in core using 376935 resolution steps c 1984 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res02 c reading proof from stdin c empty clause not found in proof, put 56725 lemmas in core c placed 26172 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 25165 of 29534 clauses in core c 124079 of 154786 lemmas in core using 380295 resolution steps c 2207 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res03 c reading proof from stdin c empty clause not found in proof, put 58460 lemmas in core c placed 26818 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 25737 of 30553 clauses in core c 124155 of 155910 lemmas in core using 379599 resolution steps c 2141 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res04 c reading proof from stdin c empty clause not found in proof, put 60055 lemmas in core c placed 27382 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 26390 of 31642 clauses in core c 124142 of 156912 lemmas in core using 384342 resolution steps c 2132 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res05 c reading proof from stdin c empty clause not found in proof, put 61758 lemmas in core c placed 28012 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 26966 of 32673 clauses in core c 124000 of 158006 lemmas in core using 378671 resolution steps c 2152 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res06 c reading proof from stdin c empty clause not found in proof, put 63271 lemmas in core c placed 28364 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 27205 of 33746 clauses in core c 124065 of 159211 lemmas in core using 381227 resolution steps c 2230 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res07 c reading proof from stdin c empty clause not found in proof, put 64288 lemmas in core c placed 28342 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 27320 of 34907 clauses in core c 123994 of 160189 lemmas in core using 381890 resolution steps c 2126 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res08 c reading proof from stdin c empty clause not found in proof, put 65449 lemmas in core c placed 28350 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 27203 of 35946 clauses in core c 124008 of 161399 lemmas in core using 383635 resolution steps c 2272 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res09 c reading proof from stdin c empty clause not found in proof, put 66555 lemmas in core c placed 28221 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 26992 of 37099 clauses in core c 124009 of 162675 lemmas in core using 382824 resolution steps c 2417 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res10 c reading proof from stdin c empty clause not found in proof, put 67251 lemmas in core c placed 27812 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 26729 of 38334 clauses in core c 123948 of 163715 lemmas in core using 382993 resolution steps c 2346 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res11 c reading proof from stdin c empty clause not found in proof, put 68038 lemmas in core c placed 27414 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 26230 of 39439 clauses in core c 124117 of 164940 lemmas in core using 385944 resolution steps c 2521 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res12 c reading proof from stdin c empty clause not found in proof, put 58711 lemmas in core c placed 21882 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 25677 of 40624 clauses in core c 121610 of 158655 lemmas in core using 377263 resolution steps c 2614 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res13 c reading proof from stdin c empty clause not found in proof, put 25675 lemmas in core c placed 4785 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 21385 of 36829 clauses in core c 114968 of 136596 lemmas in core using 729693 resolution steps c 6291 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED /tmp/res14 c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 19949 of 20858 clauses in core c 104077 of 115437 lemmas in core using 3273641 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m39.074s user 0m38.484s sys 0m0.874s c reading proof from stdin c empty clause not found in proof, put 46362 lemmas in core c placed 18276 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 17815 of 27625 clauses in core c 123894 of 152040 lemmas in core using 363089 resolution steps c 1750 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 50280 lemmas in core c placed 21621 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 21051 of 28086 clauses in core c 123950 of 152669 lemmas in core using 371761 resolution steps c 1956 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 60055 lemmas in core c placed 27382 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 26390 of 31642 clauses in core c 124142 of 156912 lemmas in core using 384342 resolution steps c 2132 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 53784 lemmas in core c placed 24250 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 23383 of 28659 clauses in core c 124031 of 153695 lemmas in core using 376935 resolution steps c 1984 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c found empty clause in proof and put it in core c finished parsing c 19949 of 20858 clauses in core c 104077 of 115437 lemmas in core using 3273641 resolution steps c 0 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 64288 lemmas in core c placed 28342 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 27320 of 34907 clauses in core c 123994 of 160189 lemmas in core using 381890 resolution steps c 2126 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 58460 lemmas in core c placed 26818 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 25737 of 30553 clauses in core c 124155 of 155910 lemmas in core using 379599 resolution steps c 2141 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 61758 lemmas in core c placed 28012 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 26966 of 32673 clauses in core c 124000 of 158006 lemmas in core using 378671 resolution steps c 2152 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 58711 lemmas in core c placed 21882 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 25677 of 40624 clauses in core c 121610 of 158655 lemmas in core using 377263 resolution steps c 2614 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 65449 lemmas in core c placed 28350 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 27203 of 35946 clauses in core c 124008 of 161399 lemmas in core using 383635 resolution steps c 2272 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 68038 lemmas in core c placed 27414 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 26230 of 39439 clauses in core c 124117 of 164940 lemmas in core using 385944 resolution steps c 2521 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 56725 lemmas in core c placed 26172 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 25165 of 29534 clauses in core c 124079 of 154786 lemmas in core using 380295 resolution steps c 2207 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 63271 lemmas in core c placed 28364 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 27205 of 33746 clauses in core c 124065 of 159211 lemmas in core using 381227 resolution steps c 2230 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 67251 lemmas in core c placed 27812 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 26729 of 38334 clauses in core c 123948 of 163715 lemmas in core using 382993 resolution steps c 2346 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 66555 lemmas in core c placed 28221 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 26992 of 37099 clauses in core c 124009 of 162675 lemmas in core using 382824 resolution steps c 2417 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED c reading proof from stdin c empty clause not found in proof, put 25675 lemmas in core c placed 4785 lemmas in core for checking c finished parsing c WARNING: no conflict detected c continue backward checking assuming to check all lemmas c 21385 of 36829 clauses in core c 114968 of 136596 lemmas in core using 729693 resolution steps c 6291 RAT lemmas in core; 0 redundant literals in core lemmas s VERIFIED real 0m3.891s user 0m39.567s sys 0m0.878s