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/primes-dimacs-cnf/normalized-ii8d2.opb
MD5SUM	44910688b6ba81ef96bbced304e8624c
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	540
Optimality of the best value was proved	NO
Number of terms in the objective function	1860
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	1860
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	1860
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.07284
Number of variables	1860
Total number of constraints	7477
Number of constraints which are clauses	7477
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	10
Trace number 4933

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-13 20:53:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1562 boxname=wulflinc26 idbench=174 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  44910688b6ba81ef96bbced304e8624c  /oldhome/oroussel/tmp/wulflinc26/normalized-ii8d2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc26/normalized-ii8d2.opb
IDLAUNCH: 1562
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        858272 kB
Buffers:         33644 kB
Cached:         102600 kB
SwapCached:       2476 kB
Active:          49760 kB
Inactive:        91872 kB
HighTotal:      131008 kB
HighFree:        25256 kB
LowTotal:       903652 kB
LowFree:        833016 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6944 kB
Slab:            29152 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:13:57 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 1562 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 7477 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 |    7477    16950 |    2492       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 709[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:105556     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |  137881   321485 |   45960       4       21     5.2 |  0.000 % |
c |       104 |  137709   321131 |   50556      99     1548    15.6 |  0.104 % |
c |       254 |  137709   321131 |   55611     249     4059    16.3 |  0.104 % |
c |       479 |  137568   320832 |   61172     471     8575    18.2 |  0.194 % |
c |       819 |  137568   320832 |   67290     811    15379    19.0 |  0.194 % |
c |      1326 |  137568   320832 |   74019    1318    26145    19.8 |  0.194 % |
c |      2085 |  137568   320832 |   81420    2077    40302    19.4 |  0.194 % |
c |      3224 |  136500   318484 |   89563    3194   110435    34.6 |  0.921 % |
c ==============================================================================
c [1mFound solution: 697[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4250 |  136626   318866 |   45542    4219   137495    32.6 |  0.921 % |
c |      4351 |  136626   318866 |   50096    4320   139555    32.3 |  0.930 % |
c |      4501 |  136225   318005 |   55105    4454   143550    32.2 |  1.191 % |
c |      4726 |  136225   318005 |   60616    4679   167067    35.7 |  1.191 % |
c |      5063 |  136201   317955 |   66678    5015   178042    35.5 |  1.205 % |
c |      5569 |  135788   317068 |   73345    5513   206664    37.5 |  1.474 % |
c |      6328 |  135531   316505 |   80680    6266   229339    36.6 |  1.648 % |
c |      7467 |  134528   314282 |   88748    7384   281946    38.2 |  2.339 % |
c ==============================================================================
c [1mFound solution: 566[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8000 |  135183   315890 |   45061    7907   292680    37.0 |  2.339 % |
c |      8101 |  135183   315890 |   49567    8008   294394    36.8 |  2.480 % |
c |      8251 |  135183   315890 |   54523    8158   301076    36.9 |  2.480 % |
c |      8476 |  135183   315890 |   59976    8383   318224    38.0 |  2.480 % |
c |      8814 |  134690   314801 |   65973    8713   325097    37.3 |  2.815 % |
c |      9320 |  134609   314626 |   72571    9143   344664    37.7 |  2.868 % |
c |     10079 |  134571   314542 |   79828    9901   390620    39.5 |  2.894 % |
c |     11218 |  133982   313243 |   87811   11028   477163    43.3 |  3.294 % |
c |     12926 |  133982   313243 |   96592   12736   563399    44.2 |  3.294 % |
c |     15488 |  133269   311642 |  106251   15268   738334    48.4 |  3.795 % |
c |     19334 |  132567   310100 |  116876   19043  1046710    55.0 |  4.268 % |
c |     25101 |  132552   310069 |  128564   24809  1632768    65.8 |  4.277 % |
c |     33752 |  132487   309924 |  141420   33448  2747636    82.1 |  4.322 % |
c |     46727 |  132487   309924 |  155562   46423  6035521   130.0 |  4.322 % |
c |     66189 |  131798   308365 |  171119   65730  7852816   119.5 |  4.813 % |
c |     95382 |  131135   306916 |  188230   94804 12371469   130.5 |  5.255 % |
c |    139171 |  131087   306810 |  207054  138592 18486533   133.4 |  5.288 % |
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 -x1344 -x1345 -x1346 x1347 -x1348 -x1349 x1350 -x1351 -x1352 -x1353 x1354 -x1355 x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 x1367 -x1368 -x1369 x1370 -x1371 -x1372 -x1373 x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x13#### 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.90 2/54 25558
Raw data (stat): 25558 (runsolver) R 25557 22612 22611 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 478989687 1052672 97 4294967295 134512640 135381576 3221224528 3221219968 134514522 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 7072 0 0 0 979 19 0 0 25 0 1 0 478989687 33017856 6816 4294967295 134512640 134672761 3221224640 3221223836 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8061 6816 603 41 0 8020 0
vsize: 32244
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 7419 0 0 0 1978 20 0 0 25 0 1 0 478989687 34824192 7163 4294967295 134512640 134672761 3221224640 3221223808 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8502 7163 603 41 0 8461 0
vsize: 34008
[startup+30.0034 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 7473 0 0 0 2978 20 0 0 25 0 1 0 478989687 35094528 7217 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8568 7217 603 41 0 8527 0
vsize: 34272
[startup+40.0035 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 7550 0 0 0 3977 20 0 0 25 0 1 0 478989687 35364864 7294 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8634 7294 603 41 0 8593 0
vsize: 34536
[startup+50.0035 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 7675 0 0 0 4977 20 0 0 25 0 1 0 478989687 35860480 7419 4294967295 134512640 134672761 3221224640 3221223808 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8755 7419 603 41 0 8714 0
vsize: 35020
[startup+60.0041 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 7820 0 0 0 5976 21 0 0 25 0 1 0 478989687 36397056 7564 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8886 7564 603 41 0 8845 0
vsize: 35544
[startup+70.0049 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 7990 0 0 0 6976 22 0 0 25 0 1 0 478989687 37199872 7734 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9082 7734 603 41 0 9041 0
vsize: 36328
[startup+80.0056 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 8115 0 0 0 7975 23 0 0 25 0 1 0 478989687 37715968 7859 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9208 7859 603 41 0 9167 0
vsize: 36832
[startup+90.0062 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 8227 0 0 0 8975 24 0 0 25 0 1 0 478989687 38223872 7971 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9332 7971 603 41 0 9291 0
vsize: 37328
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 8403 0 0 0 9974 24 0 0 25 0 1 0 478989687 38883328 8147 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9493 8147 603 41 0 9452 0
vsize: 37972
[startup+110.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 8540 0 0 0 10974 25 0 0 25 0 1 0 478989687 39415808 8284 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9623 8284 603 41 0 9582 0
vsize: 38492
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 8752 0 0 0 11974 25 0 0 25 0 1 0 478989687 40349696 8496 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 8496 603 41 0 9810 0
vsize: 39404
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 8910 0 0 0 12974 25 0 0 25 0 1 0 478989687 40882176 8654 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9981 8654 603 41 0 9940 0
vsize: 39924
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 9161 0 0 0 13973 26 0 0 25 0 1 0 478989687 41959424 8905 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10244 8905 603 41 0 10203 0
vsize: 40976
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 9427 0 0 0 14973 27 0 0 25 0 1 0 478989687 43036672 9171 4294967295 134512640 134672761 3221224640 3221223744 134560316 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10507 9171 603 41 0 10466 0
vsize: 42028
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 9667 0 0 0 15973 27 0 0 25 0 1 0 478989687 44081152 9411 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10762 9411 603 41 0 10721 0
vsize: 43048
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 9855 0 0 0 16972 28 0 0 25 0 1 0 478989687 44752896 9599 4294967295 134512640 134672761 3221224640 3221223744 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10926 9599 603 41 0 10885 0
vsize: 43704
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 10091 0 0 0 17972 29 0 0 25 0 1 0 478989687 45694976 9835 4294967295 134512640 134672761 3221224640 3221223840 134557806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11156 9835 603 41 0 11115 0
vsize: 44624
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 10265 0 0 0 18971 29 0 0 25 0 1 0 478989687 46706688 10009 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11403 10009 603 41 0 11362 0
vsize: 45612
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 10356 0 0 0 19971 30 0 0 25 0 1 0 478989687 46968832 10100 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11467 10100 603 41 0 11426 0
vsize: 45868
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 10589 0 0 0 20971 30 0 0 25 0 1 0 478989687 47906816 10333 4294967295 134512640 134672761 3221224640 3221223744 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11696 10333 603 41 0 11655 0
vsize: 46784
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 10742 0 0 0 21970 31 0 0 25 0 1 0 478989687 48578560 10486 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 10486 603 41 0 11819 0
vsize: 47440
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 10878 0 0 0 22970 31 0 0 25 0 1 0 478989687 49115136 10622 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11991 10622 603 41 0 11950 0
vsize: 47964
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 11180 0 0 0 23970 32 0 0 25 0 1 0 478989687 50323456 10924 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12286 10924 603 41 0 12245 0
vsize: 49144
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 11571 0 0 0 24969 33 0 0 25 0 1 0 478989687 51937280 11315 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12680 11315 603 41 0 12639 0
vsize: 50720
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 11978 0 0 0 25968 34 0 0 25 0 1 0 478989687 53551104 11722 4294967295 134512640 134672761 3221224640 3221223808 134561264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13074 11722 603 41 0 13033 0
vsize: 52296
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 12415 0 0 0 26967 35 0 0 25 0 1 0 478989687 55418880 12159 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13530 12159 603 41 0 13489 0
vsize: 54120
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 12831 0 0 0 27966 36 0 0 25 0 1 0 478989687 57044992 12575 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13927 12575 603 41 0 13886 0
vsize: 55708
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 13249 0 0 0 28965 37 0 0 25 0 1 0 478989687 58793984 12993 4294967295 134512640 134672761 3221224640 3221223744 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14354 12993 603 41 0 14313 0
vsize: 57416
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 13633 0 0 0 29965 38 0 0 25 0 1 0 478989687 60407808 13377 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14748 13378 603 41 0 14707 0
vsize: 58992
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 13826 0 0 0 30965 38 0 0 25 0 1 0 478989687 61198336 13570 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13570 603 41 0 14900 0
vsize: 59764
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 14077 0 0 0 31964 39 0 0 25 0 1 0 478989687 62115840 13821 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15165 13821 603 41 0 15124 0
vsize: 60660
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 14297 0 0 0 32964 39 0 0 25 0 1 0 478989687 63037440 14041 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15390 14041 603 41 0 15349 0
vsize: 61560
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 14369 0 0 0 33964 40 0 0 25 0 1 0 478989687 63307776 14113 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15456 14113 603 41 0 15415 0
vsize: 61824
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 14534 0 0 0 34963 40 0 0 25 0 1 0 478989687 63975424 14278 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15619 14278 603 41 0 15578 0
vsize: 62476
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25558
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 14623 0 0 0 35964 41 0 0 25 0 1 0 478989687 64376832 14367 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15717 14367 603 41 0 15676 0
vsize: 62868
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25566
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 14783 0 0 0 36963 41 0 0 25 0 1 0 478989687 65052672 14527 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15882 14527 603 41 0 15841 0
vsize: 63528
[startup+380.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 25611
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 15030 0 0 0 37963 42 0 0 25 0 1 0 478989687 65982464 14774 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16109 14774 603 41 0 16068 0
vsize: 64436
[startup+390.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 25611
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 15190 0 0 0 38962 43 0 0 25 0 1 0 478989687 66658304 14934 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16274 14934 603 41 0 16233 0
vsize: 65096
[startup+400.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 25611
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 15344 0 0 0 39962 43 0 0 25 0 1 0 478989687 67313664 15088 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16434 15088 603 41 0 16393 0
vsize: 65736
[startup+410.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 25611
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 15467 0 0 0 40962 43 0 0 25 0 1 0 478989687 67854336 15211 4294967295 134512640 134672761 3221224640 3221223824 134559424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16566 15211 603 41 0 16525 0
vsize: 66264
[startup+420.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 25611
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 15600 0 0 0 41961 44 0 0 25 0 1 0 478989687 68390912 15344 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16697 15344 603 41 0 16656 0
vsize: 66788
[startup+430.021 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 25611
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 15720 0 0 0 42960 44 0 0 25 0 1 0 478989687 69058560 15464 4294967295 134512640 134672761 3221224640 3221223796 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16860 15464 603 41 0 16819 0
vsize: 67440
[startup+440.021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 15884 0 0 0 43958 45 0 0 25 0 1 0 478989687 69730304 15628 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17024 15628 603 41 0 16983 0
vsize: 68096
[startup+450.021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 16032 0 0 0 44958 45 0 0 25 0 1 0 478989687 70385664 15776 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17184 15776 603 41 0 17143 0
vsize: 68736
[startup+460.021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 16231 0 0 0 45958 45 0 0 25 0 1 0 478989687 71192576 15975 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17381 15975 603 41 0 17340 0
vsize: 69524
[startup+470.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 16427 0 0 0 46958 46 0 0 25 0 1 0 478989687 71991296 16171 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17576 16171 603 41 0 17535 0
vsize: 70304
[startup+480.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 16553 0 0 0 47958 46 0 0 25 0 1 0 478989687 72499200 16297 4294967295 134512640 134672761 3221224640 3221223812 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17700 16297 603 41 0 17659 0
vsize: 70800
[startup+490.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 16735 0 0 0 48958 47 0 0 25 0 1 0 478989687 73293824 16479 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17894 16479 603 41 0 17853 0
vsize: 71576
[startup+500.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 16962 0 0 0 49958 47 0 0 25 0 1 0 478989687 74100736 16706 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18091 16706 603 41 0 18050 0
vsize: 72364
[startup+510.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 17156 0 0 0 50957 47 0 0 25 0 1 0 478989687 74903552 16900 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18287 16900 603 41 0 18246 0
vsize: 73148
[startup+520.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 17350 0 0 0 51957 48 0 0 25 0 1 0 478989687 75698176 17094 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18481 17094 603 41 0 18440 0
vsize: 73924
[startup+530.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 17529 0 0 0 52957 48 0 0 25 0 1 0 478989687 76500992 17273 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18677 17273 603 41 0 18636 0
vsize: 74708
[startup+540.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 17683 0 0 0 53956 49 0 0 25 0 1 0 478989687 77033472 17427 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18807 17427 603 41 0 18766 0
vsize: 75228
[startup+550.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 17797 0 0 0 54956 49 0 0 25 0 1 0 478989687 77570048 17541 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18938 17541 603 41 0 18897 0
vsize: 75752
[startup+560.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 17951 0 0 0 55956 50 0 0 25 0 1 0 478989687 78245888 17695 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 17695 603 41 0 19062 0
vsize: 76412
[startup+570.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 18118 0 0 0 56955 50 0 0 25 0 1 0 478989687 78913536 17862 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19266 17862 603 41 0 19225 0
vsize: 77064
[startup+580.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 18380 0 0 0 57955 51 0 0 25 0 1 0 478989687 79966208 18124 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19523 18124 603 41 0 19482 0
vsize: 78092
[startup+590.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 18648 0 0 0 58954 52 0 0 25 0 1 0 478989687 81039360 18392 4294967295 134512640 134672761 3221224640 3221223744 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19785 18392 603 41 0 19744 0
vsize: 79140
[startup+600.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 18866 0 0 0 59954 53 0 0 25 0 1 0 478989687 81977344 18610 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20014 18610 603 41 0 19973 0
vsize: 80056
[startup+610.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 19120 0 0 0 60953 53 0 0 25 0 1 0 478989687 82890752 18864 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20237 18864 603 41 0 20196 0
vsize: 80948
[startup+620.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 19354 0 0 0 61952 54 0 0 25 0 1 0 478989687 83951616 19098 4294967295 134512640 134672761 3221224640 3221223744 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20496 19098 603 41 0 20455 0
vsize: 81984
[startup+630.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 19559 0 0 0 62952 55 0 0 25 0 1 0 478989687 84746240 19303 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20690 19303 603 41 0 20649 0
vsize: 82760
[startup+640.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 19732 0 0 0 63952 55 0 0 25 0 1 0 478989687 85413888 19476 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20853 19476 603 41 0 20812 0
vsize: 83412
[startup+650.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 19890 0 0 0 64952 55 0 0 25 0 1 0 478989687 86073344 19634 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21014 19634 603 41 0 20973 0
vsize: 84056
[startup+660.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 20038 0 0 0 65951 56 0 0 25 0 1 0 478989687 86728704 19782 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21174 19782 603 41 0 21133 0
vsize: 84696
[startup+670.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 20143 0 0 0 66951 56 0 0 25 0 1 0 478989687 87130112 19887 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21272 19887 603 41 0 21231 0
vsize: 85088
[startup+680.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 20405 0 0 0 67950 57 0 0 25 0 1 0 478989687 88190976 20149 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21531 20149 603 41 0 21490 0
vsize: 86124
[startup+690.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 20486 0 0 0 68950 57 0 0 25 0 1 0 478989687 88461312 20230 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21597 20230 603 41 0 21556 0
vsize: 86388
[startup+700.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 20624 0 0 0 69950 57 0 0 25 0 1 0 478989687 89133056 20368 4294967295 134512640 134672761 3221224640 3221223824 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21761 20368 603 41 0 21720 0
vsize: 87044
[startup+710.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25613
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 20723 0 0 0 70950 58 0 0 25 0 1 0 478989687 89526272 20467 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21857 20467 603 41 0 21816 0
vsize: 87428
[startup+720.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 20873 0 0 0 71950 58 0 0 25 0 1 0 478989687 90062848 20617 4294967295 134512640 134672761 3221224640 3221223824 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21988 20617 603 41 0 21947 0
vsize: 87952
[startup+730.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 20972 0 0 0 72950 59 0 0 25 0 1 0 478989687 90464256 20716 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22086 20716 603 41 0 22045 0
vsize: 88344
[startup+740.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 21109 0 0 0 73950 59 0 0 25 0 1 0 478989687 90996736 20853 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22216 20853 603 41 0 22175 0
vsize: 88864
[startup+750.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 21244 0 0 0 74950 59 0 0 25 0 1 0 478989687 91533312 20988 4294967295 134512640 134672761 3221224640 3221223808 134561394 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22347 20988 603 41 0 22306 0
vsize: 89388
[startup+760.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 21383 0 0 0 75950 59 0 0 25 0 1 0 478989687 92205056 21127 4294967295 134512640 134672761 3221224640 3221223792 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22511 21127 603 41 0 22470 0
vsize: 90044
[startup+770.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 21552 0 0 0 76950 59 0 0 25 0 1 0 478989687 92856320 21296 4294967295 134512640 134672761 3221224640 3221223808 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22670 21296 603 41 0 22629 0
vsize: 90680
[startup+780.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 21667 0 0 0 77950 60 0 0 25 0 1 0 478989687 93257728 21411 4294967295 134512640 134672761 3221224640 3221223744 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22768 21411 603 41 0 22727 0
vsize: 91072
[startup+790.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 21795 0 0 0 78949 60 0 0 25 0 1 0 478989687 93790208 21539 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22898 21539 603 41 0 22857 0
vsize: 91592
[startup+800.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 21968 0 0 0 79949 61 0 0 25 0 1 0 478989687 94461952 21712 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23062 21712 603 41 0 23021 0
vsize: 92248
[startup+810.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 22138 0 0 0 80949 61 0 0 25 0 1 0 478989687 95260672 21882 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23257 21882 603 41 0 23216 0
vsize: 93028
[startup+820.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 22244 0 0 0 81949 62 0 0 25 0 1 0 478989687 95657984 21988 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23354 21988 603 41 0 23313 0
vsize: 93416
[startup+830.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 22378 0 0 0 82948 62 0 0 25 0 1 0 478989687 96202752 22122 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23487 22122 603 41 0 23446 0
vsize: 93948
[startup+840.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 22570 0 0 0 83948 62 0 0 25 0 1 0 478989687 97005568 22314 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23683 22314 603 41 0 23642 0
vsize: 94732
[startup+850.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 22728 0 0 0 84948 62 0 0 25 0 1 0 478989687 97542144 22472 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23814 22472 603 41 0 23773 0
vsize: 95256
[startup+860.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 22854 0 0 0 85949 62 0 0 25 0 1 0 478989687 98066432 22598 4294967295 134512640 134672761 3221224640 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23942 22598 603 41 0 23901 0
vsize: 95768
[startup+870.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 22978 0 0 0 86948 63 0 0 25 0 1 0 478989687 98582528 22722 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24068 22722 603 41 0 24027 0
vsize: 96272
[startup+880.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 23092 0 0 0 87948 63 0 0 25 0 1 0 478989687 99110912 22836 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24197 22836 603 41 0 24156 0
vsize: 96788
[startup+890.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 23214 0 0 0 88948 64 0 0 25 0 1 0 478989687 99516416 22958 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24296 22958 603 41 0 24255 0
vsize: 97184
[startup+900.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 23476 0 0 0 89947 65 0 0 25 0 1 0 478989687 100593664 23220 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24559 23220 603 41 0 24518 0
vsize: 98236
[startup+910.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 23710 0 0 0 90946 65 0 0 25 0 1 0 478989687 101535744 23454 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 23454 603 41 0 24748 0
vsize: 99156
[startup+920.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 23937 0 0 0 91946 66 0 0 25 0 1 0 478989687 102465536 23681 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25016 23681 603 41 0 24975 0
vsize: 100064
[startup+930.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 24094 0 0 0 92946 66 0 0 25 0 1 0 478989687 103129088 23838 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25178 23838 603 41 0 25137 0
vsize: 100712
[startup+940.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 24278 0 0 0 93946 67 0 0 25 0 1 0 478989687 103931904 24022 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25374 24022 603 41 0 25333 0
vsize: 101496
[startup+950.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 24470 0 0 0 94945 67 0 0 25 0 1 0 478989687 104730624 24214 4294967295 134512640 134672761 3221224640 3221223824 134559559 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25569 24214 603 41 0 25528 0
vsize: 102276
[startup+960.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 24669 0 0 0 95945 67 0 0 25 0 1 0 478989687 105541632 24413 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25767 24413 603 41 0 25726 0
vsize: 103068
[startup+970.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 24873 0 0 0 96945 68 0 0 25 0 1 0 478989687 106344448 24617 4294967295 134512640 134672761 3221224640 3221223744 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25963 24617 603 41 0 25922 0
vsize: 103852
[startup+980.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 25115 0 0 0 97945 68 0 0 25 0 1 0 478989687 107278336 24859 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26191 24859 603 41 0 26150 0
vsize: 104764
[startup+990.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 25293 0 0 0 98945 68 0 0 25 0 1 0 478989687 108605440 25037 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26515 25037 603 41 0 26474 0
vsize: 106060
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 25487 0 0 0 99945 69 0 0 25 0 1 0 478989687 109400064 25231 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26709 25231 603 41 0 26668 0
vsize: 106836
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 25670 0 0 0 100944 69 0 0 25 0 1 0 478989687 110059520 25414 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25414 603 41 0 26829 0
vsize: 107480
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 25841 0 0 0 101944 69 0 0 25 0 1 0 478989687 110858240 25585 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27065 25585 603 41 0 27024 0
vsize: 108260
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 26024 0 0 0 102944 70 0 0 25 0 1 0 478989687 111534080 25768 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27230 25768 603 41 0 27189 0
vsize: 108920
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 26233 0 0 0 103943 71 0 0 25 0 1 0 478989687 112463872 25977 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27457 25977 603 41 0 27416 0
vsize: 109828
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 26408 0 0 0 104943 71 0 0 25 0 1 0 478989687 113131520 26152 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27620 26152 603 41 0 27579 0
vsize: 110480
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 26639 0 0 0 105942 72 0 0 25 0 1 0 478989687 114069504 26383 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27849 26383 603 41 0 27808 0
vsize: 111396
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 26827 0 0 0 106942 72 0 0 25 0 1 0 478989687 114872320 26571 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28045 26571 603 41 0 28004 0
vsize: 112180
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 26977 0 0 0 107941 73 0 0 25 0 1 0 478989687 115396608 26721 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28173 26721 603 41 0 28132 0
vsize: 112692
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 27127 0 0 0 108941 73 0 0 25 0 1 0 478989687 116060160 26871 4294967295 134512640 134672761 3221224640 3221223744 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28335 26871 603 41 0 28294 0
vsize: 113340
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 27238 0 0 0 109941 73 0 0 25 0 1 0 478989687 116461568 26982 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28433 26982 603 41 0 28392 0
vsize: 113732
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 27365 0 0 0 110941 74 0 0 25 0 1 0 478989687 116994048 27109 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28563 27109 603 41 0 28522 0
vsize: 114252
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 27464 0 0 0 111941 74 0 0 25 0 1 0 478989687 117391360 27208 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28660 27208 603 41 0 28619 0
vsize: 114640
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 27600 0 0 0 112941 75 0 0 25 0 1 0 478989687 118050816 27344 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28821 27344 603 41 0 28780 0
vsize: 115284
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 27718 0 0 0 113940 76 0 0 25 0 1 0 478989687 118439936 27462 4294967295 134512640 134672761 3221224640 3221223776 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28916 27462 603 41 0 28875 0
vsize: 115664
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 27867 0 0 0 114940 76 0 0 25 0 1 0 478989687 119107584 27611 4294967295 134512640 134672761 3221224640 3221223840 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29079 27611 603 41 0 29038 0
vsize: 116316
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 27995 0 0 0 115940 76 0 0 25 0 1 0 478989687 119644160 27739 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29210 27739 603 41 0 29169 0
vsize: 116840
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 28115 0 0 0 116939 77 0 0 25 0 1 0 478989687 120041472 27859 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29307 27859 603 41 0 29266 0
vsize: 117228
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 28227 0 0 0 117939 77 0 0 25 0 1 0 478989687 120573952 27971 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29437 27971 603 41 0 29396 0
vsize: 117748
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 28336 0 0 0 118939 77 0 0 25 0 1 0 478989687 120971264 28080 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29534 28080 603 41 0 29493 0
vsize: 118136
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25615
Raw data (stat): 25558 (minisat+) R 25557 22612 22611 0 -1 0 28496 0 0 0 119939 78 0 0 25 0 1 0 478989687 121643008 28240 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29698 28240 603 41 0 29657 0
vsize: 118792
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 25615
Raw data (stat): 25558 (minisat+) Z 25557 22612 22611 0 -1 12 28499 0 0 0 119939 83 0 0 25 0 1 0 478989687 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.08
CPU time (s): 1200.23
CPU user time (s): 1199.4
CPU system time (s): 0.835872
CPU usage (%): 100.013
Max. virtual memory (Kb): 118792
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####