PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-rot.b.opb
MD5SUM	c5ca4962151c0e84eeae44e16faee495
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	116
Optimality of the best value was proved	NO
Number of terms in the objective function	1452
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	1452
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1452
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04884
Number of variables	1451
Total number of constraints	2984
Number of constraints which are clauses	2932
Number of constraints which are cardinality constraints (but not clauses)	52
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	81
Trace number 4667

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-13 19:44:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3456 boxname=wulflinc22 idbench=72 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c5ca4962151c0e84eeae44e16faee495  /oldhome/oroussel/tmp/wulflinc22/normalized-rot.b.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc22/normalized-rot.b.opb /oldhome/oroussel/tmp/wulflinc22/normalized-rot.b.opb
IDLAUNCH: 3456
/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:        870548 kB
Buffers:         30704 kB
Cached:          90356 kB
SwapCached:        524 kB
Active:          38508 kB
Inactive:        85932 kB
HighTotal:      131008 kB
HighFree:        36932 kB
LowTotal:       903652 kB
LowFree:        833616 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34172 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:04:40 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 3456 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2722 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    2716    40318 |     905       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 161[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2846   maxlim: 1291   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |   22560   111175 |    7520       4      142    35.5 |  0.000 % |
c |       104 |   22560   111175 |    8272     104      860     8.3 |  0.721 % |
c |       254 |   22516   111052 |    9099     250     1468     5.9 |  0.814 % |
c |       479 |   22516   111052 |   10009     475     2312     4.9 |  0.814 % |
c |       817 |   22516   111052 |   11010     813     3939     4.8 |  0.814 % |
c |      1323 |   22500   111000 |   12111    1316     6241     4.7 |  0.884 % |
c |      2082 |   22500   111000 |   13322    2075    11241     5.4 |  0.884 % |
c |      3226 |   22500   111000 |   14654    3219    48747    15.1 |  0.884 % |
c |      4935 |   22500   111000 |   16119    4928   154321    31.3 |  0.884 % |
c |      7497 |   22500   111000 |   17731    7490   480192    64.1 |  0.884 % |
c |     11342 |   22500   111000 |   19504   11335  1033449    91.2 |  0.884 % |
c |     17109 |   22500   111000 |   21455   17102  1624836    95.0 |  0.884 % |
c |     25759 |   22500   111000 |   23600   14616  1332134    91.1 |  0.884 % |
c |     38734 |   22500   111000 |   25961   15113  1960453   129.7 |  0.884 % |
c |     58198 |   22500   111000 |   28557   20981  2892418   137.9 |  0.884 % |
c |     87390 |   22500   111000 |   31412   19596  3503707   178.8 |  0.884 % |
c |    131180 |   22500   111000 |   34554   27460  5005420   182.3 |  0.884 % |
c ==============================================================================
c [1mFound solution: 156[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1598   maxlim: 1296   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    154438 |   33611   150669 |   11203   31109  4312288   138.6 |  0.884 % |
c |    154538 |   33611   150669 |   12323    7160   740132   103.4 |  0.780 % |
c |    154688 |   33611   150669 |   13555    7310   741170   101.4 |  0.780 % |
c |    154913 |   33594   150610 |   14911    7533   742675    98.6 |  0.831 % |
c |    155250 |   33594   150610 |   16402    7870   746586    94.9 |  0.831 % |
c |    155757 |   33594   150610 |   18042    8377   753730    90.0 |  0.831 % |
c |    156517 |   33594   150610 |   19846    9137   777556    85.1 |  0.831 % |
c |    157656 |   33594   150610 |   21831   10276   869659    84.6 |  0.831 % |
c |    159366 |   33594   150610 |   24014   11986   954673    79.6 |  0.831 % |
c |    161928 |   33594   150610 |   26416   14548  1123712    77.2 |  0.831 % |
c |    165776 |   33594   150610 |   29057   18396  1573582    85.5 |  0.831 % |
c |    171543 |   33594   150610 |   31963   24163  2019875    83.6 |  0.831 % |
c |    180193 |   33594   150610 |   35159   32813  3247914    99.0 |  0.831 % |
c |    193167 |   33587   150587 |   38675   24800  1936801    78.1 |  0.847 % |
c |    212628 |   33578   150558 |   42543   19920  1043410    52.4 |  0.881 % |
c |    241820 |   33578   150558 |   46797   19933  3904981   195.9 |  0.881 % |
c |    285610 |   33578   150558 |   51477   30615  1984954    64.8 |  0.881 % |
c |    351297 |   33578   150558 |   56625   22178  1308780    59.0 |  0.881 % |
c |    449826 |   33578   150558 |   62287   38211  3348974    87.6 |  0.881 % |
c |    597615 |   33578   150558 |   68516   51249  9607545   187.5 |  0.881 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 -x3 -x4 x5 -x6 x7 -x8 x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 x17 -x18 x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 x92 x93 -x94 -x95 -x96 -x97 -x98 x99 x100 -x101 -x102 -x103 -x104 x105 -x106 -x107 x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 x119 x120 -x121 x122 -x123 x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 x144 -x145 -x146 -x147 x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 x177 x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 x192 x193 x194 -x195 -x196 -x197 -x198 -x199 x200 -x201 -x202 -x203 -x204 -x205 x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 x225 x226 -x227 -x228 -x229 x230 -x231 -x232 -x233 x234 -x235 -x236 -x237 -x238 -x239 -x240 x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 x268 -x269 x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 x312 -x313 -x314 x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 x346 x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 x370 -x371 x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 x434 x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 x445 x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 x481 x482 -x483 -x484 -x485 -x486 x487 -x488 x489 x490 x491 x492 -x493 -x494 -x495 -x496 x497 -x498 -x499 -x500 -x501 x502 x503 -x504 x505 x506 -x507 -x508 -x509 -x510 x511 -x512 x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 x583 x584 -x585 -x586 -x587 -x588 x589 -x590 x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 x614 x615 x616 -x617 x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 x707 x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 x728 x729 -x730 -x731 -x732 -x733 -x734 x735 -x736 -x737 -x738 -x739 -x740 x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 x759 x760 -x761 x762 x763 x764 -x765 -x766 -x767 -x768 x769 -x770 x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 x802 -x803 x804 x805 x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 x864 -x865 -x866 -x867 -x868 -x869 x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 x879 x880 -x881 -x882 -x883 -x884 x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 x894 -x895 -x896 x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 -x909 -x910 x911 -x912 -x913 -x914 x915 x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 x972 x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 x1000 x1001 -x1002 -x1003 -x1004 -x1005 -x1006 x1007 -x1008 -x1009 -x1010 x1011 -x1012 -x1013 -x1014 -x1015 x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 x1023 -x1024 -x1025 x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 x1079 -x1080 x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 x1127 -x1128 -x1129 x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 x1150 x1151 -x1152 -x1153 -x1154 x1155 -x1156 x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 x1221 x1222 -x1223 -x1224 -x1225 -x1226 x1227 -x1228 x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 x1249 x1250 -x1251 -x1252 -x1253 x1254 -x1255 x1256 x1257 x1258 x1259 -x1260 x1261 -x1262 -x1263 -x1264 -x1265 x1266 x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 x1282 -x1283 -x1284 x1285 -x1286 x1287 -x1288 x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 x1335 x1336 -x1337 -x1338 -x1339 -x1340 -x1341 x1342 -x1343#### 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.92 0.95 0.69 2/54 27821
Raw data (stat): 27821 (runsolver) R 27820 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478567337 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.95 0.69 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 2175 0 0 0 992 6 0 0 25 0 1 0 478567337 10571776 2153 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2581 2153 603 41 0 2540 0
vsize: 10324
[startup+20.001 s]
Raw data (loadavg): 0.94 0.95 0.69 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 3229 0 0 0 1988 9 0 0 25 0 1 0 478567337 14897152 3207 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3637 3207 603 41 0 3596 0
vsize: 14548
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.96 0.70 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 3681 0 0 0 2987 10 0 0 25 0 1 0 478567337 16777216 3659 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4096 3659 603 41 0 4055 0
vsize: 16384
[startup+40.0013 s]
Raw data (loadavg): 0.96 0.96 0.70 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 4134 0 0 0 3985 12 0 0 25 0 1 0 478567337 18530304 4112 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4524 4112 603 41 0 4483 0
vsize: 18096
[startup+50.002 s]
Raw data (loadavg): 0.96 0.96 0.70 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 4507 0 0 0 4984 13 0 0 25 0 1 0 478567337 20131840 4485 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4915 4485 603 41 0 4874 0
vsize: 19660
[startup+60.002 s]
Raw data (loadavg): 0.97 0.96 0.71 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 4507 0 0 0 5984 13 0 0 25 0 1 0 478567337 20131840 4485 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4915 4485 603 41 0 4874 0
vsize: 19660
[startup+70.0024 s]
Raw data (loadavg): 0.97 0.96 0.71 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 5202 0 0 0 6981 16 0 0 25 0 1 0 478567337 22966272 5180 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5607 5180 603 41 0 5566 0
vsize: 22428
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.96 0.71 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 5404 0 0 0 7981 16 0 0 25 0 1 0 478567337 23769088 5382 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5803 5382 603 41 0 5762 0
vsize: 23212
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.96 0.71 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 5404 0 0 0 8981 16 0 0 25 0 1 0 478567337 23769088 5382 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5803 5382 603 41 0 5762 0
vsize: 23212
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 5881 0 0 0 9980 18 0 0 25 0 1 0 478567337 25772032 5859 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6292 5859 603 41 0 6251 0
vsize: 25168
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 5881 0 0 0 10980 18 0 0 25 0 1 0 478567337 25772032 5859 4294967295 134512640 134672761 3221224576 3221223712 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6292 5859 603 41 0 6251 0
vsize: 25168
[startup+120.004 s]
Raw data (loadavg): 0.99 0.96 0.72 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 6495 0 0 0 11979 19 0 0 25 0 1 0 478567337 28188672 6473 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6882 6473 603 41 0 6841 0
vsize: 27528
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 6549 0 0 0 12979 20 0 0 25 0 1 0 478567337 28459008 6527 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6948 6527 603 41 0 6907 0
vsize: 27792
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 6549 0 0 0 13979 20 0 0 25 0 1 0 478567337 28459008 6527 4294967295 134512640 134672761 3221224576 3221223760 134559607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6948 6527 603 41 0 6907 0
vsize: 27792
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 6549 0 0 0 14980 20 0 0 25 0 1 0 478567337 28459008 6527 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6948 6527 603 41 0 6907 0
vsize: 27792
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 6585 0 0 0 15979 20 0 0 25 0 1 0 478567337 28594176 6563 4294967295 134512640 134672761 3221224576 3221223760 134559583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6981 6563 603 41 0 6940 0
vsize: 27924
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 6585 0 0 0 16980 20 0 0 25 0 1 0 478567337 28594176 6563 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6981 6563 603 41 0 6940 0
vsize: 27924
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 6585 0 0 0 17980 20 0 0 25 0 1 0 478567337 28594176 6563 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6981 6563 603 41 0 6940 0
vsize: 27924
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 6956 0 0 0 18979 21 0 0 25 0 1 0 478567337 30081024 6934 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7344 6934 603 41 0 7303 0
vsize: 29376
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7520 0 0 0 19979 21 0 0 25 0 1 0 478567337 32624640 7498 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7965 7498 603 41 0 7924 0
vsize: 31860
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7520 0 0 0 20979 21 0 0 25 0 1 0 478567337 32624640 7498 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7965 7498 603 41 0 7924 0
vsize: 31860
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7600 0 0 0 21979 21 0 0 25 0 1 0 478567337 33034240 7578 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7578 603 41 0 8024 0
vsize: 32260
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7600 0 0 0 22979 21 0 0 25 0 1 0 478567337 33034240 7578 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7578 603 41 0 8024 0
vsize: 32260
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7600 0 0 0 23979 22 0 0 25 0 1 0 478567337 33034240 7578 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7578 603 41 0 8024 0
vsize: 32260
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7601 0 0 0 24979 22 0 0 25 0 1 0 478567337 33034240 7579 4294967295 134512640 134672761 3221224576 3221223744 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7579 603 41 0 8024 0
vsize: 32260
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7601 0 0 0 25979 22 0 0 25 0 1 0 478567337 33034240 7579 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7579 603 41 0 8024 0
vsize: 32260
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7603 0 0 0 26979 22 0 0 25 0 1 0 478567337 33034240 7581 4294967295 134512640 134672761 3221224576 3221223728 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7581 603 41 0 8024 0
vsize: 32260
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7603 0 0 0 27979 22 0 0 25 0 1 0 478567337 33034240 7581 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7581 603 41 0 8024 0
vsize: 32260
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7603 0 0 0 28979 22 0 0 25 0 1 0 478567337 33034240 7581 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7581 603 41 0 8024 0
vsize: 32260
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7603 0 0 0 29980 22 0 0 25 0 1 0 478567337 33034240 7581 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7581 603 41 0 8024 0
vsize: 32260
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 7606 0 0 0 30980 22 0 0 25 0 1 0 478567337 33034240 7584 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7584 603 41 0 8024 0
vsize: 32260
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8162 0 0 0 31978 24 0 0 25 0 1 0 478567337 35323904 8140 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8624 8140 603 41 0 8583 0
vsize: 34496
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8384 0 0 0 32977 25 0 0 25 0 1 0 478567337 36134912 8362 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8822 8362 603 41 0 8781 0
vsize: 35288
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8390 0 0 0 33977 25 0 0 25 0 1 0 478567337 36278272 8368 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8857 8368 603 41 0 8816 0
vsize: 35428
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8390 0 0 0 34978 25 0 0 25 0 1 0 478567337 36278272 8368 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8857 8368 603 41 0 8816 0
vsize: 35428
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8485 0 0 0 35977 25 0 0 25 0 1 0 478567337 36683776 8463 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8956 8463 603 41 0 8915 0
vsize: 35824
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8933 0 0 0 36976 27 0 0 25 0 1 0 478567337 38424576 8911 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8911 603 41 0 9340 0
vsize: 37524
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8933 0 0 0 37976 27 0 0 25 0 1 0 478567337 38424576 8911 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8911 603 41 0 9340 0
vsize: 37524
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8933 0 0 0 38976 27 0 0 25 0 1 0 478567337 38424576 8911 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8911 603 41 0 9340 0
vsize: 37524
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8938 0 0 0 39977 27 0 0 25 0 1 0 478567337 38424576 8916 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8916 603 41 0 9340 0
vsize: 37524
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8938 0 0 0 40977 27 0 0 25 0 1 0 478567337 38424576 8916 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8916 603 41 0 9340 0
vsize: 37524
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8938 0 0 0 41977 27 0 0 25 0 1 0 478567337 38424576 8916 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8916 603 41 0 9340 0
vsize: 37524
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8938 0 0 0 42977 27 0 0 25 0 1 0 478567337 38424576 8916 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8916 603 41 0 9340 0
vsize: 37524
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8938 0 0 0 43977 27 0 0 25 0 1 0 478567337 38424576 8916 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8916 603 41 0 9340 0
vsize: 37524
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8938 0 0 0 44978 27 0 0 25 0 1 0 478567337 38424576 8916 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8916 603 41 0 9340 0
vsize: 37524
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8938 0 0 0 45978 27 0 0 25 0 1 0 478567337 38424576 8916 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8916 603 41 0 9340 0
vsize: 37524
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8938 0 0 0 46978 27 0 0 25 0 1 0 478567337 38424576 8916 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8916 603 41 0 9340 0
vsize: 37524
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8938 0 0 0 47978 27 0 0 25 0 1 0 478567337 38424576 8916 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8916 603 41 0 9340 0
vsize: 37524
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8942 0 0 0 48978 27 0 0 25 0 1 0 478567337 38424576 8920 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8920 603 41 0 9340 0
vsize: 37524
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8942 0 0 0 49979 27 0 0 25 0 1 0 478567337 38424576 8920 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8920 603 41 0 9340 0
vsize: 37524
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8942 0 0 0 50979 27 0 0 25 0 1 0 478567337 38424576 8920 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8920 603 41 0 9340 0
vsize: 37524
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8944 0 0 0 51979 27 0 0 25 0 1 0 478567337 38424576 8922 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8922 603 41 0 9340 0
vsize: 37524
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8944 0 0 0 52979 27 0 0 25 0 1 0 478567337 38424576 8922 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8922 603 41 0 9340 0
vsize: 37524
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8944 0 0 0 53979 27 0 0 25 0 1 0 478567337 38424576 8922 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8922 603 41 0 9340 0
vsize: 37524
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8944 0 0 0 54979 27 0 0 25 0 1 0 478567337 38424576 8922 4294967295 134512640 134672761 3221224576 3221223760 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8922 603 41 0 9340 0
vsize: 37524
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8945 0 0 0 55979 27 0 0 25 0 1 0 478567337 38424576 8923 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8923 603 41 0 9340 0
vsize: 37524
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8947 0 0 0 56980 27 0 0 25 0 1 0 478567337 38424576 8925 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8925 603 41 0 9340 0
vsize: 37524
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8947 0 0 0 57980 27 0 0 25 0 1 0 478567337 38424576 8925 4294967295 134512640 134672761 3221224576 3221223680 134560316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8925 603 41 0 9340 0
vsize: 37524
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8947 0 0 0 58980 27 0 0 25 0 1 0 478567337 38424576 8925 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8925 603 41 0 9340 0
vsize: 37524
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8947 0 0 0 59980 27 0 0 25 0 1 0 478567337 38424576 8925 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8925 603 41 0 9340 0
vsize: 37524
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 8947 0 0 0 60980 27 0 0 25 0 1 0 478567337 38424576 8925 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8925 603 41 0 9340 0
vsize: 37524
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 9655 0 0 0 61978 30 0 0 25 0 1 0 478567337 41357312 9633 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10097 9633 603 41 0 10056 0
vsize: 40388
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 10399 0 0 0 62976 32 0 0 25 0 1 0 478567337 44326912 10377 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10822 10377 603 41 0 10781 0
vsize: 43288
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 11154 0 0 0 63974 34 0 0 25 0 1 0 478567337 47419392 11132 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11577 11132 603 41 0 11536 0
vsize: 46308
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 11587 0 0 0 64972 35 0 0 25 0 1 0 478567337 49303552 11565 4294967295 134512640 134672761 3221224576 3221223576 1075350787 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12037 11565 603 41 0 11996 0
vsize: 48148
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 11587 0 0 0 65972 35 0 0 25 0 1 0 478567337 49303552 11565 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12037 11565 603 41 0 11996 0
vsize: 48148
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 11587 0 0 0 66973 35 0 0 25 0 1 0 478567337 49303552 11565 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12037 11565 603 41 0 11996 0
vsize: 48148
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 11587 0 0 0 67973 35 0 0 25 0 1 0 478567337 49303552 11565 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12037 11565 603 41 0 11996 0
vsize: 48148
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 11587 0 0 0 68973 35 0 0 25 0 1 0 478567337 49303552 11565 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12037 11565 603 41 0 11996 0
vsize: 48148
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 11587 0 0 0 69973 35 0 0 25 0 1 0 478567337 49303552 11565 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12037 11565 603 41 0 11996 0
vsize: 48148
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 11587 0 0 0 70973 35 0 0 25 0 1 0 478567337 49303552 11565 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12037 11565 603 41 0 11996 0
vsize: 48148
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 11587 0 0 0 71974 35 0 0 25 0 1 0 478567337 49303552 11565 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12037 11565 603 41 0 11996 0
vsize: 48148
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 11918 0 0 0 72972 37 0 0 25 0 1 0 478567337 50642944 11896 4294967295 134512640 134672761 3221224576 3221223680 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12364 11896 603 41 0 12323 0
vsize: 49456
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 12479 0 0 0 73971 38 0 0 25 0 1 0 478567337 52928512 12457 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12922 12457 603 41 0 12881 0
vsize: 51688
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13018 0 0 0 74970 39 0 0 25 0 1 0 478567337 55074816 12996 4294967295 134512640 134672761 3221224576 3221223680 134554625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12996 603 41 0 13405 0
vsize: 53784
[startup+760.008 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13019 0 0 0 75970 39 0 0 25 0 1 0 478567337 55074816 12997 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12997 603 41 0 13405 0
vsize: 53784
[startup+770.007 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13019 0 0 0 76970 39 0 0 25 0 1 0 478567337 55074816 12997 4294967295 134512640 134672761 3221224576 3221223700 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12997 603 41 0 13405 0
vsize: 53784
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13019 0 0 0 77971 39 0 0 25 0 1 0 478567337 55074816 12997 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12997 603 41 0 13405 0
vsize: 53784
[startup+790.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13019 0 0 0 78971 39 0 0 25 0 1 0 478567337 55074816 12997 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12997 603 41 0 13405 0
vsize: 53784
[startup+800.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13019 0 0 0 79971 39 0 0 25 0 1 0 478567337 55074816 12997 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12997 603 41 0 13405 0
vsize: 53784
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13019 0 0 0 80971 39 0 0 25 0 1 0 478567337 55074816 12997 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12997 603 41 0 13405 0
vsize: 53784
[startup+820.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13019 0 0 0 81971 39 0 0 25 0 1 0 478567337 55074816 12997 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12997 603 41 0 13405 0
vsize: 53784
[startup+830.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13019 0 0 0 82971 39 0 0 25 0 1 0 478567337 55074816 12997 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12997 603 41 0 13405 0
vsize: 53784
[startup+840.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13019 0 0 0 83972 39 0 0 25 0 1 0 478567337 55074816 12997 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12997 603 41 0 13405 0
vsize: 53784
[startup+850.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13455 0 0 0 84971 40 0 0 25 0 1 0 478567337 56954880 13433 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13905 13433 603 41 0 13864 0
vsize: 55620
[startup+860.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 13787 0 0 0 85970 41 0 0 25 0 1 0 478567337 58327040 13765 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14240 13765 603 41 0 14199 0
vsize: 56960
[startup+870.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 86969 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+880.007 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 87969 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+890.007 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 88970 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+900.007 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 89970 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+910.007 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 90970 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+920.007 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 27821
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 91970 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+930.007 s]
Raw data (loadavg): 1.07 0.99 0.86 2/58 27864
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 92970 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+940.006 s]
Raw data (loadavg): 1.06 0.99 0.86 2/54 27874
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 93970 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+950.007 s]
Raw data (loadavg): 1.05 0.99 0.86 2/54 27874
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 94970 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+960.007 s]
Raw data (loadavg): 1.04 0.99 0.86 2/54 27874
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 95971 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+970.006 s]
Raw data (loadavg): 1.04 0.99 0.86 2/54 27874
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 96971 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+980.007 s]
Raw data (loadavg): 1.03 0.99 0.86 2/54 27874
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 97971 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+990.007 s]
Raw data (loadavg): 1.03 0.99 0.86 2/54 27874
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 98971 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1000.01 s]
Raw data (loadavg): 1.02 0.99 0.86 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 99971 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1010.01 s]
Raw data (loadavg): 1.02 0.99 0.86 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 100972 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1020.01 s]
Raw data (loadavg): 1.01 0.99 0.86 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 101972 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1030.01 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 102972 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1040.01 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 103972 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1050.01 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 104972 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223680 134555128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1060.01 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 105972 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 106973 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 107973 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 108973 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 109973 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14156 0 0 0 110973 42 0 0 25 0 1 0 478567337 60080128 14134 4294967295 134512640 134672761 3221224576 3221223680 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 14134 603 41 0 14627 0
vsize: 58672
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 14667 0 0 0 111971 44 0 0 25 0 1 0 478567337 62099456 14645 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15161 14645 603 41 0 15120 0
vsize: 60644
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 15184 0 0 0 112970 46 0 0 25 0 1 0 478567337 64258048 15162 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15688 15162 603 41 0 15647 0
vsize: 62752
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 15725 0 0 0 113969 47 0 0 25 0 1 0 478567337 66555904 15703 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16249 15703 603 41 0 16208 0
vsize: 64996
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 16167 0 0 0 114968 48 0 0 25 0 1 0 478567337 68333568 16145 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16683 16145 603 41 0 16642 0
vsize: 66732
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 16649 0 0 0 115966 50 0 0 25 0 1 0 478567337 70356992 16627 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17177 16627 603 41 0 17136 0
vsize: 68708
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 17124 0 0 0 116965 51 0 0 25 0 1 0 478567337 72372224 17102 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17669 17102 603 41 0 17628 0
vsize: 70676
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 17634 0 0 0 117964 52 0 0 25 0 1 0 478567337 74395648 17612 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17612 603 41 0 18122 0
vsize: 72652
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 17803 0 0 0 118964 53 0 0 25 0 1 0 478567337 75071488 17781 4294967295 134512640 134672761 3221224576 3221223744 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18328 17781 603 41 0 18287 0
vsize: 73312
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 27876
Raw data (stat): 27821 (minisat+) R 27820 26298 26297 0 -1 0 17803 0 0 0 119964 53 0 0 25 0 1 0 478567337 75071488 17781 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18328 17781 603 41 0 18287 0
vsize: 73312
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.88 1/54 27876
Raw data (stat): 27821 (minisat+) Z 27820 26298 26297 0 -1 12 17806 0 0 0 119964 56 0 0 25 0 1 0 478567337 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.05
CPU time (s): 1200.22
CPU user time (s): 1199.65
CPU system time (s): 0.567913
CPU usage (%): 100.014
Max. virtual memory (Kb): 73312
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####