Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb40-19-opb/normalized-frb40-19-3.opb |
MD5SUM | 3acd642471b3f4559739eef7eb2e9b58 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -31 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 760 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 760 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 760 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.06 |
Number of variables | 760 |
Total number of constraints | 41095 |
Number of constraints which are clauses | 41095 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc22 THE 2005-04-14 00:57:46 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4086 boxname=wulflinc22 idbench=326 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3acd642471b3f4559739eef7eb2e9b58 /oldhome/oroussel/tmp/wulflinc22/normalized-frb40-19-3.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc22/normalized-frb40-19-3.opb /oldhome/oroussel/tmp/wulflinc22/normalized-frb40-19-3.opb IDLAUNCH: 4086 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 852304 kB Buffers: 32164 kB Cached: 106712 kB SwapCached: 524 kB Active: 49384 kB Inactive: 92900 kB HighTotal: 131008 kB HighFree: 20552 kB LowTotal: 903652 kB LowFree: 831752 kB SwapTotal: 2097892 kB SwapFree: 2097368 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6924 kB Slab: 34616 kB Committed_AS: 63488 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 01:17:48 (client local time) WITH STATUS 10 IN 1200.26 SECONDS stats: 4086 7 1200.26 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 41095 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 41095 82190 | 12328 0 0 nan | 0.000 % | c -- subsuming c | 0 | 41095 82190 | 16438 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 1.73774 s) c ============================================================================== c [1mFound solution: -31[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:35010 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 77395 167462 | 23218 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/24844 c -- var.elim.: 2000/24844 c -- var.elim.: 3000/24844 c -- var.elim.: 4000/24844 c -- var.elim.: 5000/24844 c -- var.elim.: 6000/24844 c -- var.elim.: 7000/24844 c -- var.elim.: 8000/24844 c -- var.elim.: 9000/24844 c -- var.elim.: 10000/24844 c -- var.elim.: 11000/24844 c -- var.elim.: 12000/24844 c -- var.elim.: 13000/24844 c -- var.elim.: 14000/24844 c -- var.elim.: 15000/24844 c -- var.elim.: 16000/24844 c -- var.elim.: 17000/24844 c -- var.elim.: 18000/24844 c -- var.elim.: 19000/24844 c -- var.elim.: 20000/24844 c -- var.elim.: 21000/24844 c -- var.elim.: 22000/24844 c -- var.elim.: 23000/24844 c -- var.elim.: 24000/24844 c -- var.elim.: 24844/24844 c -- var.elim.: 1000/12626 c -- var.elim.: 2000/12626 c -- var.elim.: 3000/12626 c -- var.elim.: 4000/12626 c -- var.elim.: 5000/12626 c -- var.elim.: 6000/12626 c -- var.elim.: 7000/12626 c -- var.elim.: 8000/12626 c -- var.elim.: 9000/12626 c -- var.elim.: 10000/12626 c -- var.elim.: 11000/12626 c -- var.elim.: 12000/12626 c -- var.elim.: 12626/12626 c -- var.elim.: 1000/2962 c -- var.elim.: 2000/2962 c -- var.elim.: 2962/2962 c -- var.elim.: 50/50 c -- var.elim.: 21/21 c -- subsuming c -- var.elim.: 1000/5765 c -- var.elim.: 2000/5765 c -- var.elim.: 3000/5765 c -- var.elim.: 4000/5765 c -- var.elim.: 5000/5765 c -- var.elim.: 5765/5765 c -- var.elim.: 686/686 c | 0 | 51743 168583 | -- 0 -- -- | -- | -25652/1122 c | 0 | 51743 168583 | 20697 0 0 nan | 0.000 % | c | 100 | 51743 168583 | 22766 100 19093 190.9 | 52.865 % | c | 250 | 51723 168040 | 25033 248 48782 196.7 | 52.936 % | c | 475 | 51723 168040 | 27537 473 86345 182.5 | 52.936 % | c | 812 | 51723 168040 | 30291 810 147493 182.1 | 52.936 % | c | 1318 | 51695 167782 | 33302 1314 219989 167.4 | 53.040 % | c | 2078 | 51581 166823 | 36551 2066 341255 165.2 | 53.446 % | c | 3217 | 51581 166823 | 40206 3205 602863 188.1 | 53.446 % | c | 4925 | 51431 165490 | 44098 4899 976976 199.4 | 54.004 % | c | 7487 | 51330 164601 | 48413 7449 1587998 213.2 | 54.370 % | c | 11332 | 50968 161720 | 52879 11233 2474385 220.3 | 55.613 % | c | 17098 | 50512 157849 | 57646 16881 4070367 241.1 | 57.430 % | c ============================================================================== c (current CPU-time: 98.87 s) c ============================================================================== c [1mFound solution: -32[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 17418 | 52425 162689 | 15727 17194 4240180 246.6 | 57.430 % | c -- subsuming c -- var.elim.: 1000/7069 c -- var.elim.: 2000/7069 c -- var.elim.: 3000/7069 c -- var.elim.: 4000/7069 c -- var.elim.: 5000/7069 c -- var.elim.: 6000/7069 c -- var.elim.: 7000/7069 c -- var.elim.: 7069/7069 c -- var.elim.: 1000/1530 c -- var.elim.: 1530/1530 c -- var.elim.: 4/4 c | 17418 | 50449 157209 | -- 17194 -- -- | -- | -1966/-1715 c | 17418 | 50449 157209 | 20179 17194 4240180 246.6 | 57.430 % | c | 17518 | 50449 157209 | 22197 17294 4268368 246.8 | 63.002 % | c | 17669 | 50449 157209 | 24417 17445 4310181 247.1 | 63.002 % | c | 17894 | 50449 157209 | 26859 17670 4380041 247.9 | 63.001 % | c | 18231 | 50449 157209 | 29544 18007 4472859 248.4 | 63.002 % | c | 18737 | 50353 156386 | 32437 15095 1758843 116.5 | 63.337 % | c | 19496 | 50317 156048 | 35655 15846 1948739 123.0 | 63.455 % | c | 20635 | 50317 156048 | 39221 16985 2339583 137.7 | 63.455 % | c | 22344 | 50241 155318 | 43078 18672 2822869 151.2 | 63.720 % | c | 24906 | 50211 155028 | 47357 21206 3686024 173.8 | 63.825 % | c | 28750 | 50155 154479 | 52035 25040 5161400 206.1 | 64.021 % | c | 34516 | 50012 153185 | 57076 30747 7157687 232.8 | 64.508 % | c | 43165 | 49763 151012 | 62471 39353 10196132 259.1 | 65.353 % | c | 56140 | 49385 147353 | 68196 52164 15219381 291.8 | 66.629 % | c | 75603 | 48867 142967 | 74228 71398 23110390 323.7 | 68.416 % | c ============================================================================== c (current CPU-time: 490.477 s) c ============================================================================== c [1mFound solution: -34[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 87780 | 50343 146567 | 15102 83543 28238188 338.0 | 68.416 % | c -- subsuming c -- var.elim.: 1000/5936 c -- var.elim.: 2000/5936 c -- var.elim.: 3000/5936 c -- var.elim.: 4000/5936 c -- var.elim.: 5000/5936 c -- var.elim.: 5936/5936 c -- var.elim.: 1000/1491 c -- var.elim.: 1491/1491 c | 87780 | 48790 143358 | -- 83543 -- -- | -- | -1547/-2855 c | 87780 | 48790 143358 | 19516 67676 12276485 181.4 | 68.416 % | c | 87881 | 48730 142855 | 21441 18329 2417043 131.9 | 71.231 % | c | 88031 | 48730 142855 | 23585 18479 2450861 132.6 | 71.230 % | c | 88256 | 48730 142855 | 25943 18704 2509697 134.2 | 71.231 % | c | 88594 | 48730 142855 | 28538 19042 2613295 137.2 | 71.231 % | c | 89100 | 48728 142838 | 31390 19544 2749283 140.7 | 71.237 % | c | 89859 | 48728 142838 | 34529 20303 2956198 145.6 | 71.237 % | c | 90998 | 48676 142457 | 37942 21434 3264118 152.3 | 71.406 % | c | 92706 | 48650 142222 | 41714 23132 3671591 158.7 | 71.490 % | c | 95268 | 48588 141702 | 45827 25688 4560560 177.5 | 71.691 % | c | 99112 | 48554 141413 | 50374 29508 5867298 198.8 | 71.801 % | c | 104878 | 48448 140532 | 55291 35258 7742606 219.6 | 72.138 % | c | 113529 | 48352 139752 | 60699 43890 10745333 244.8 | 72.449 % | c | 126503 | 47924 136245 | 66178 56789 14764942 260.0 | 73.804 % | c | 145966 | 47612 133570 | 72322 76043 21826512 287.0 | 74.796 % | c | 175158 | 47340 131304 | 79100 41492 11142911 268.6 | 75.658 % | c c *** TERMINATED *** s SATISFIABLE v -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 C400 -C399 C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -#### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.84 0.94 0.90 2/54 30639 Raw data (stat): 30639 (runsolver) R 30638 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480446407 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99963 s] Raw data (loadavg): 0.87 0.94 0.90 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5015 0 0 0 980 18 0 0 25 0 1 0 480446407 22413312 4725 4294967295 134512640 134672761 3221224560 3221222992 134604055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5472 4725 603 41 0 5431 0 vsize: 21888 [startup+20 s] Raw data (loadavg): 0.89 0.94 0.90 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5032 0 0 0 1980 18 0 0 25 0 1 0 480446407 22597632 4742 4294967295 134512640 134672761 3221224560 3221222928 134603527 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5517 4742 603 41 0 5476 0 vsize: 22068 [startup+29.9997 s] Raw data (loadavg): 0.90 0.94 0.90 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5037 0 0 0 2980 18 0 0 25 0 1 0 480446407 22597632 4747 4294967295 134512640 134672761 3221224560 3221223008 134643483 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5517 4747 603 41 0 5476 0 vsize: 22068 [startup+40.0007 s] Raw data (loadavg): 0.92 0.94 0.90 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5058 0 0 0 3980 19 0 0 25 0 1 0 480446407 22597632 4768 4294967295 134512640 134672761 3221224560 3221223008 134643624 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5517 4768 603 41 0 5476 0 vsize: 22068 [startup+50.0012 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5210 0 0 0 4980 19 0 0 25 0 1 0 480446407 23654400 4920 4294967295 134512640 134672761 3221224560 3221223024 134644240 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5775 4920 603 41 0 5734 0 vsize: 23100 [startup+60.0009 s] Raw data (loadavg): 0.94 0.95 0.90 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 5325 0 0 0 5979 19 0 0 25 0 1 0 480446407 23121920 4883 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5645 4883 603 41 0 5604 0 vsize: 22580 [startup+70.0019 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 6537 0 0 0 6977 22 0 0 25 0 1 0 480446407 27975680 6095 4294967295 134512640 134672761 3221224560 3221223684 134566031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6830 6095 603 41 0 6789 0 vsize: 27320 [startup+80.0023 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 7466 0 0 0 7975 25 0 0 25 0 1 0 480446407 31780864 7024 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7759 7024 603 41 0 7718 0 vsize: 31036 [startup+90.003 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 8297 0 0 0 8973 27 0 0 25 0 1 0 480446407 35209216 7855 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8596 7855 603 41 0 8555 0 vsize: 34384 [startup+100.003 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 10250 0 0 0 9966 33 0 0 25 0 1 0 480446407 41537536 9317 4294967295 134512640 134672761 3221224560 3221223104 134621041 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10141 9317 603 41 0 10100 0 vsize: 40564 [startup+110.002 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 10278 0 0 0 10960 38 0 0 25 0 1 0 480446407 40476672 9193 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9882 9193 603 41 0 9841 0 vsize: 39528 [startup+120.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 10280 0 0 0 11961 38 0 0 25 0 1 0 480446407 40476672 9195 4294967295 134512640 134672761 3221224560 3221223600 134612646 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9882 9195 603 41 0 9841 0 vsize: 39528 [startup+130.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 30639 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 10283 0 0 0 12961 38 0 0 25 0 1 0 480446407 40476672 9198 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9882 9198 603 41 0 9841 0 vsize: 39528 [startup+140.005 s] Raw data (loadavg): 0.98 0.95 0.91 3/57 30680 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 11504 0 0 0 13958 40 0 0 25 0 1 0 480446407 45428736 10419 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11091 10419 603 41 0 11050 0 vsize: 44364 [startup+150.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 30692 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 12521 0 0 0 14949 50 0 0 25 0 1 0 480446407 49688576 11436 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12131 11436 603 41 0 12090 0 vsize: 48524 [startup+160.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30692 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 13253 0 0 0 15947 52 0 0 25 0 1 0 480446407 52613120 12168 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12845 12168 603 41 0 12804 0 vsize: 51380 [startup+170.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30692 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 14131 0 0 0 16945 54 0 0 25 0 1 0 480446407 56381440 13046 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13765 13046 603 41 0 13724 0 vsize: 55060 [startup+180.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30692 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 14934 0 0 0 17943 56 0 0 25 0 1 0 480446407 59645952 13849 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14562 13849 603 41 0 14521 0 vsize: 58248 [startup+190.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30692 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 15686 0 0 0 18942 57 0 0 25 0 1 0 480446407 62672896 14601 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15301 14601 603 41 0 15260 0 vsize: 61204 [startup+200.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30692 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 16386 0 0 0 19941 58 0 0 25 0 1 0 480446407 65515520 15301 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15995 15301 603 41 0 15954 0 vsize: 63980 [startup+210.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 17140 0 0 0 20939 61 0 0 25 0 1 0 480446407 68620288 16055 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16753 16056 603 41 0 16712 0 vsize: 67012 [startup+220.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 18094 0 0 0 21936 64 0 0 25 0 1 0 480446407 72499200 17009 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17700 17009 603 41 0 17659 0 vsize: 70800 [startup+230.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 19070 0 0 0 22935 66 0 0 25 0 1 0 480446407 76496896 17985 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18676 17985 603 41 0 18635 0 vsize: 74704 [startup+240.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 19487 0 0 0 23934 66 0 0 25 0 1 0 480446407 78180352 18402 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19087 18402 603 41 0 19046 0 vsize: 76348 [startup+250.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 20215 0 0 0 24933 68 0 0 25 0 1 0 480446407 81215488 19130 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19828 19130 603 41 0 19787 0 vsize: 79312 [startup+260.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 20684 0 0 0 25932 69 0 0 25 0 1 0 480446407 83058688 19599 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19599 603 41 0 20237 0 vsize: 81112 [startup+270.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 21342 0 0 0 26930 71 0 0 25 0 1 0 480446407 85774336 20257 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20941 20257 603 41 0 20900 0 vsize: 83764 [startup+280.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 22150 0 0 0 27928 73 0 0 25 0 1 0 480446407 89133056 21065 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21761 21065 603 41 0 21720 0 vsize: 87044 [startup+290.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 22779 0 0 0 28928 73 0 0 25 0 1 0 480446407 91619328 21694 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22368 21694 603 41 0 22327 0 vsize: 89472 [startup+300.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 23558 0 0 0 29926 76 0 0 25 0 1 0 480446407 94842880 22473 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23155 22473 603 41 0 23114 0 vsize: 92620 [startup+310.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 24123 0 0 0 30924 77 0 0 25 0 1 0 480446407 97185792 23038 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23727 23038 603 41 0 23686 0 vsize: 94908 [startup+320.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 24680 0 0 0 31923 79 0 0 25 0 1 0 480446407 99409920 23595 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24270 23595 603 41 0 24229 0 vsize: 97080 [startup+330.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 25207 0 0 0 32922 80 0 0 25 0 1 0 480446407 101629952 24122 4294967295 134512640 134672761 3221224560 3221223704 134616139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24812 24122 603 41 0 24771 0 vsize: 99248 [startup+340.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 25883 0 0 0 33921 81 0 0 25 0 1 0 480446407 104386560 24798 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25485 24798 603 41 0 25444 0 vsize: 101940 [startup+350.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 26519 0 0 0 34920 83 0 0 25 0 1 0 480446407 106987520 25434 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26120 25434 603 41 0 26079 0 vsize: 104480 [startup+360.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 27182 0 0 0 35917 86 0 0 25 0 1 0 480446407 109940736 26097 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26841 26097 603 41 0 26800 0 vsize: 107364 [startup+370.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 27701 0 0 0 36916 87 0 0 25 0 1 0 480446407 112087040 26616 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27365 26616 603 41 0 27324 0 vsize: 109460 [startup+380.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 28215 0 0 0 37915 88 0 0 25 0 1 0 480446407 114151424 27130 4294967295 134512640 134672761 3221224560 3221223704 134616233 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27869 27130 603 41 0 27828 0 vsize: 111476 [startup+390.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 28784 0 0 0 38914 89 0 0 25 0 1 0 480446407 116514816 27699 4294967295 134512640 134672761 3221224560 3221223760 134610511 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28446 27699 603 41 0 28405 0 vsize: 113784 [startup+400.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 29056 0 0 0 39913 91 0 0 25 0 1 0 480446407 117579776 27971 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28706 27971 603 41 0 28665 0 vsize: 114824 [startup+410.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 29632 0 0 0 40912 92 0 0 25 0 1 0 480446407 119930880 28547 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29280 28547 603 41 0 29239 0 vsize: 117120 [startup+420.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 30221 0 0 0 41911 93 0 0 25 0 1 0 480446407 122294272 29136 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29857 29136 603 41 0 29816 0 vsize: 119428 [startup+430.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 30807 0 0 0 42909 95 0 0 25 0 1 0 480446407 124796928 29722 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30468 29722 603 41 0 30427 0 vsize: 121872 [startup+440.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 31500 0 0 0 43908 96 0 0 25 0 1 0 480446407 127647744 30415 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31164 30415 603 41 0 31123 0 vsize: 124656 [startup+450.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 32438 0 0 0 44906 98 0 0 25 0 1 0 480446407 131424256 31353 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32086 31353 603 41 0 32045 0 vsize: 128344 [startup+460.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 33220 0 0 0 45905 100 0 0 25 0 1 0 480446407 134664192 32135 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32877 32135 603 41 0 32836 0 vsize: 131508 [startup+470.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 33842 0 0 0 46904 101 0 0 25 0 1 0 480446407 137228288 32757 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33503 32757 603 41 0 33462 0 vsize: 134012 [startup+480.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 34116 0 0 0 47903 102 0 0 25 0 1 0 480446407 138264576 33031 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33756 33031 603 41 0 33715 0 vsize: 135024 [startup+490.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 34511 0 0 0 48903 102 0 0 25 0 1 0 480446407 139948032 33426 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34167 33426 603 41 0 34126 0 vsize: 136668 [startup+500.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30694 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 49896 109 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+510.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 50896 109 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+520.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 51896 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+530.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 52896 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+540.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 53896 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+550.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 54896 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+560.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 55896 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+570.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 56897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615635 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+580.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 57897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+590.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 58897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+600.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 59897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+610.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 60897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+620.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 61897 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+630.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35642 0 0 0 62898 110 0 0 25 0 1 0 480446407 142512128 34081 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34081 603 41 0 34752 0 vsize: 139172 [startup+640.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 63898 110 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223704 134616247 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34082 603 41 0 34752 0 vsize: 139172 [startup+650.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 64898 110 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34082 603 41 0 34752 0 vsize: 139172 [startup+660.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 65898 110 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34082 603 41 0 34752 0 vsize: 139172 [startup+670.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 66898 110 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34082 603 41 0 34752 0 vsize: 139172 [startup+680.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 67898 110 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34082 603 41 0 34752 0 vsize: 139172 [startup+690.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 68898 111 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34082 603 41 0 34752 0 vsize: 139172 [startup+700.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 69898 111 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34082 603 41 0 34752 0 vsize: 139172 [startup+710.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 70898 111 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34082 603 41 0 34752 0 vsize: 139172 [startup+720.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 71898 111 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34082 603 41 0 34752 0 vsize: 139172 [startup+730.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35643 0 0 0 72899 111 0 0 25 0 1 0 480446407 142512128 34082 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34082 603 41 0 34752 0 vsize: 139172 [startup+740.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 73899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34083 603 41 0 34752 0 vsize: 139172 [startup+750.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 74899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34083 603 41 0 34752 0 vsize: 139172 [startup+760.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 75899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34083 603 41 0 34752 0 vsize: 139172 [startup+770.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 76899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34083 603 41 0 34752 0 vsize: 139172 [startup+780.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 77899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34083 603 41 0 34752 0 vsize: 139172 [startup+790.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 78899 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34083 603 41 0 34752 0 vsize: 139172 [startup+800.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35644 0 0 0 79900 111 0 0 25 0 1 0 480446407 142512128 34083 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34083 603 41 0 34752 0 vsize: 139172 [startup+810.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35645 0 0 0 80900 111 0 0 25 0 1 0 480446407 142512128 34084 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34084 603 41 0 34752 0 vsize: 139172 [startup+820.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35645 0 0 0 81900 112 0 0 25 0 1 0 480446407 142512128 34084 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34084 603 41 0 34752 0 vsize: 139172 [startup+830.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35645 0 0 0 82900 112 0 0 25 0 1 0 480446407 142512128 34084 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34084 603 41 0 34752 0 vsize: 139172 [startup+840.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35645 0 0 0 83900 112 0 0 25 0 1 0 480446407 142512128 34084 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34084 603 41 0 34752 0 vsize: 139172 [startup+850.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35645 0 0 0 84900 112 0 0 25 0 1 0 480446407 142512128 34084 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34084 603 41 0 34752 0 vsize: 139172 [startup+860.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 85900 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+870.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 86900 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+880.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 87900 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223704 134616126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+890.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 88900 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223552 134565137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+900.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 89901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+910.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 90901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+920.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 91901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+930.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 92901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+940.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 93901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223552 134565137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+950.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 94901 112 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+960.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 95901 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+970.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 96901 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+980.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 97901 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+990.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 98901 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+1000.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 99902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+1010.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 100902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+1020.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 101902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+1030.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 102902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+1040.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 103902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+1050.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 104902 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+1060.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 105903 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+1070.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35647 0 0 0 106903 113 0 0 25 0 1 0 480446407 142512128 34086 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34086 603 41 0 34752 0 vsize: 139172 [startup+1080.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 107903 113 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1090.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 108903 113 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1100.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 109903 113 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1110.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 110903 113 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1120.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 111903 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1130.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 112903 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1140.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 113903 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1150.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 114903 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1160.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 115903 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1170.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 116904 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1180.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 117904 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1190.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 118904 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 [startup+1200.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 30696 Raw data (stat): 30639 (minisat+) R 30638 26298 26297 0 -1 0 35648 0 0 0 119904 114 0 0 25 0 1 0 480446407 142512128 34087 4294967295 134512640 134672761 3221224560 3221223744 134615523 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34793 34087 603 41 0 34752 0 vsize: 139172 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 30696 Raw data (stat): 30639 (minisat+) Z 30638 26298 26297 0 -1 12 35649 0 0 0 119904 121 0 0 25 0 1 0 480446407 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.1 CPU time (s): 1200.26 CPU user time (s): 1199.05 CPU system time (s): 1.21681 CPU usage (%): 100.014 Max. virtual memory (Kb): 139172 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####