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 6182

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-14 03:41:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4584 boxname=wulflinc3 idbench=72 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c5ca4962151c0e84eeae44e16faee495  /oldhome/oroussel/tmp/wulflinc3/normalized-rot.b.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc3/normalized-rot.b.opb /oldhome/oroussel/tmp/wulflinc3/normalized-rot.b.opb
IDLAUNCH: 4584
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 2
cpu MHz		: 451.190
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:        850084 kB
Buffers:         36248 kB
Cached:         125240 kB
SwapCached:       3276 kB
Active:          81068 kB
Inactive:        86516 kB
HighTotal:      131008 kB
HighFree:         7364 kB
LowTotal:       903652 kB
LowFree:        842720 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11476 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:01:23 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 4584 7 1200.17 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]---> Sorter-cost:79826     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |  189712   477666 |   63237       4      142    35.5 |  0.000 % |
c |       104 |  189443   477047 |   69560      99      707     7.1 |  0.144 % |
c |       254 |  189375   476891 |   76516     247     1235     5.0 |  0.174 % |
c |       479 |  189375   476891 |   84168     472     2254     4.8 |  0.174 % |
c |       816 |  189089   476233 |   92585     803     8788    10.9 |  0.292 % |
c |      1322 |  188999   476027 |  101843    1308    13182    10.1 |  0.332 % |
c |      2081 |  188900   475798 |  112028    2066    21910    10.6 |  0.373 % |
c |      3220 |  188808   475587 |  123231    3202    34991    10.9 |  0.414 % |
c |      4928 |  188628   475184 |  135554    4907    53220    10.8 |  0.482 % |
c |      7490 |  188380   474609 |  149109    7464    78980    10.6 |  0.589 % |
c |     11334 |  187679   472988 |  164020   11287   117194    10.4 |  0.907 % |
c |     17100 |  187433   472420 |  180422   17039   368360    21.6 |  1.018 % |
c |     25749 |  187300   472113 |  198464   25672   468333    18.2 |  1.075 % |
c |     38723 |  187189   471853 |  218311   38639   668805    17.3 |  1.125 % |
c |     58185 |  186895   471171 |  240142   57779  1162615    20.1 |  1.263 % |
c |     87381 |  186817   470991 |  264156   86954  1807392    20.8 |  1.301 % |
c |    131170 |  186736   470800 |  290572  130678  2990522    22.9 |  1.339 % |
c |    196857 |  186635   470563 |  319629  196333  5381493    27.4 |  1.384 % |
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 #### 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.91 0.96 0.92 2/54 19214
Raw data (stat): 19214 (runsolver) R 19213 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423204657 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.0008 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 5736 0 0 0 982 15 0 0 25 0 1 0 423204657 25935872 5605 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6332 5605 603 41 0 6291 0
vsize: 25328
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 5985 0 0 0 1981 16 0 0 25 0 1 0 423204657 26877952 5854 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6562 5854 603 41 0 6521 0
vsize: 26248
[startup+30.0014 s]
Raw data (loadavg): 1.03 0.98 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 6284 0 0 0 2980 17 0 0 25 0 1 0 423204657 28069888 6153 4294967295 134512640 134672761 3221224576 3221223744 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6853 6153 603 41 0 6812 0
vsize: 27412
[startup+40.0023 s]
Raw data (loadavg): 1.10 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 6404 0 0 0 3978 17 0 0 25 0 1 0 423204657 28606464 6273 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6984 6273 603 41 0 6943 0
vsize: 27936
[startup+50.0025 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 6525 0 0 0 4978 18 0 0 25 0 1 0 423204657 29138944 6394 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7114 6394 603 41 0 7073 0
vsize: 28456
[startup+60.0026 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 6679 0 0 0 5977 18 0 0 25 0 1 0 423204657 29802496 6548 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7276 6548 603 41 0 7235 0
vsize: 29104
[startup+70.0035 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 6754 0 0 0 6977 19 0 0 25 0 1 0 423204657 30072832 6623 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7342 6623 603 41 0 7301 0
vsize: 29368
[startup+80.003 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 6819 0 0 0 7977 19 0 0 25 0 1 0 423204657 30339072 6688 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7407 6688 603 41 0 7366 0
vsize: 29628
[startup+90.0031 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 7032 0 0 0 8976 19 0 0 25 0 1 0 423204657 31150080 6901 4294967295 134512640 134672761 3221224576 3221223744 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7605 6901 603 41 0 7564 0
vsize: 30420
[startup+100.003 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 7277 0 0 0 9975 20 0 0 25 0 1 0 423204657 32104448 7146 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7838 7146 603 41 0 7797 0
vsize: 31352
[startup+110.004 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 7453 0 0 0 10975 21 0 0 25 0 1 0 423204657 32776192 7322 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8002 7322 603 41 0 7961 0
vsize: 32008
[startup+120.004 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 7482 0 0 0 11975 21 0 0 25 0 1 0 423204657 33173504 7351 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8099 7351 603 41 0 8058 0
vsize: 32396
[startup+130.004 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 7553 0 0 0 12975 21 0 0 25 0 1 0 423204657 33443840 7422 4294967295 134512640 134672761 3221224576 3221223744 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8165 7422 603 41 0 8124 0
vsize: 32660
[startup+140.004 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 7638 0 0 0 13975 22 0 0 25 0 1 0 423204657 33849344 7507 4294967295 134512640 134672761 3221224576 3221223744 134560811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8264 7507 603 41 0 8223 0
vsize: 33056
[startup+150.004 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 7725 0 0 0 14975 22 0 0 25 0 1 0 423204657 34119680 7594 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8330 7594 603 41 0 8289 0
vsize: 33320
[startup+160.005 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 7827 0 0 0 15974 22 0 0 25 0 1 0 423204657 34525184 7696 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7696 603 41 0 8388 0
vsize: 33716
[startup+170.005 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 7887 0 0 0 16974 23 0 0 25 0 1 0 423204657 34795520 7756 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8495 7756 603 41 0 8454 0
vsize: 33980
[startup+180.005 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 7920 0 0 0 17974 23 0 0 25 0 1 0 423204657 34930688 7789 4294967295 134512640 134672761 3221224576 3221223744 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8528 7789 603 41 0 8487 0
vsize: 34112
[startup+190.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8003 0 0 0 18974 23 0 0 25 0 1 0 423204657 35196928 7872 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8593 7872 603 41 0 8552 0
vsize: 34372
[startup+200.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8055 0 0 0 19974 23 0 0 25 0 1 0 423204657 35467264 7924 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8659 7924 603 41 0 8618 0
vsize: 34636
[startup+210.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8113 0 0 0 20974 23 0 0 25 0 1 0 423204657 35737600 7982 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8725 7982 603 41 0 8684 0
vsize: 34900
[startup+220.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8154 0 0 0 21974 24 0 0 25 0 1 0 423204657 35872768 8023 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8758 8023 603 41 0 8717 0
vsize: 35032
[startup+230.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8185 0 0 0 22972 25 0 0 25 0 1 0 423204657 36007936 8054 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8791 8054 603 41 0 8750 0
vsize: 35164
[startup+240.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8284 0 0 0 23972 25 0 0 25 0 1 0 423204657 36409344 8153 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8889 8153 603 41 0 8848 0
vsize: 35556
[startup+250.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8379 0 0 0 24972 25 0 0 25 0 1 0 423204657 36679680 8248 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8955 8248 603 41 0 8914 0
vsize: 35820
[startup+260.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8430 0 0 0 25972 26 0 0 25 0 1 0 423204657 36950016 8299 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9021 8299 603 41 0 8980 0
vsize: 36084
[startup+270.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8459 0 0 0 26972 26 0 0 25 0 1 0 423204657 37081088 8328 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9053 8328 603 41 0 9012 0
vsize: 36212
[startup+280.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8505 0 0 0 27972 26 0 0 25 0 1 0 423204657 37216256 8374 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9086 8374 603 41 0 9045 0
vsize: 36344
[startup+290.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8539 0 0 0 28972 26 0 0 25 0 1 0 423204657 37351424 8408 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9119 8408 603 41 0 9078 0
vsize: 36476
[startup+300.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8576 0 0 0 29972 26 0 0 25 0 1 0 423204657 37502976 8445 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9156 8445 603 41 0 9115 0
vsize: 36624
[startup+310.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8605 0 0 0 30971 27 0 0 25 0 1 0 423204657 37638144 8474 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9189 8474 603 41 0 9148 0
vsize: 36756
[startup+320.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8642 0 0 0 31971 27 0 0 25 0 1 0 423204657 37773312 8511 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9222 8511 603 41 0 9181 0
vsize: 36888
[startup+330.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8673 0 0 0 32971 27 0 0 25 0 1 0 423204657 37908480 8542 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9255 8542 603 41 0 9214 0
vsize: 37020
[startup+340.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8710 0 0 0 33972 27 0 0 25 0 1 0 423204657 38043648 8579 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9288 8579 603 41 0 9247 0
vsize: 37152
[startup+350.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8760 0 0 0 34972 27 0 0 25 0 1 0 423204657 38309888 8629 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9353 8629 603 41 0 9312 0
vsize: 37412
[startup+360.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8815 0 0 0 35972 27 0 0 25 0 1 0 423204657 38445056 8684 4294967295 134512640 134672761 3221224576 3221223760 134558925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9386 8684 603 41 0 9345 0
vsize: 37544
[startup+370.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 8928 0 0 0 36971 27 0 0 25 0 1 0 423204657 38985728 8797 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9518 8797 603 41 0 9477 0
vsize: 38072
[startup+380.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 9050 0 0 0 37971 28 0 0 25 0 1 0 423204657 39387136 8919 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9616 8919 603 41 0 9575 0
vsize: 38464
[startup+390.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 9159 0 0 0 38971 28 0 0 25 0 1 0 423204657 39927808 9028 4294967295 134512640 134672761 3221224576 3221223712 134560637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9748 9028 603 41 0 9707 0
vsize: 38992
[startup+400.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 9255 0 0 0 39971 28 0 0 25 0 1 0 423204657 40194048 9124 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9813 9124 603 41 0 9772 0
vsize: 39252
[startup+410.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 9370 0 0 0 40971 29 0 0 25 0 1 0 423204657 40734720 9239 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9945 9239 603 41 0 9904 0
vsize: 39780
[startup+420.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 9541 0 0 0 41970 30 0 0 25 0 1 0 423204657 41398272 9410 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10107 9410 603 41 0 10066 0
vsize: 40428
[startup+430.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 9698 0 0 0 42970 30 0 0 25 0 1 0 423204657 42061824 9567 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10269 9567 603 41 0 10228 0
vsize: 41076
[startup+440.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 9871 0 0 0 43969 31 0 0 25 0 1 0 423204657 43257856 9740 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10561 9740 603 41 0 10520 0
vsize: 42244
[startup+450.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 9925 0 0 0 44968 31 0 0 25 0 1 0 423204657 43393024 9794 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10594 9794 603 41 0 10553 0
vsize: 42376
[startup+460.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 10048 0 0 0 45967 32 0 0 25 0 1 0 423204657 43933696 9917 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10726 9917 603 41 0 10685 0
vsize: 42904
[startup+470.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 10115 0 0 0 46967 32 0 0 25 0 1 0 423204657 44195840 9984 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10790 9984 603 41 0 10749 0
vsize: 43160
[startup+480.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 10196 0 0 0 47968 32 0 0 25 0 1 0 423204657 44462080 10065 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10855 10065 603 41 0 10814 0
vsize: 43420
[startup+490.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 10340 0 0 0 48968 32 0 0 25 0 1 0 423204657 45133824 10209 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11019 10209 603 41 0 10978 0
vsize: 44076
[startup+500.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 10437 0 0 0 49967 32 0 0 25 0 1 0 423204657 45404160 10306 4294967295 134512640 134672761 3221224576 3221223776 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11085 10306 603 41 0 11044 0
vsize: 44340
[startup+510.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 10657 0 0 0 50967 33 0 0 25 0 1 0 423204657 46338048 10526 4294967295 134512640 134672761 3221224576 3221223680 134559922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11313 10526 603 41 0 11272 0
vsize: 45252
[startup+520.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 10920 0 0 0 51966 34 0 0 25 0 1 0 423204657 47398912 10789 4294967295 134512640 134672761 3221224576 3221223644 1075346629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11572 10789 603 41 0 11531 0
vsize: 46288
[startup+530.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 11168 0 0 0 52966 35 0 0 25 0 1 0 423204657 48340992 11037 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11802 11037 603 41 0 11761 0
vsize: 47208
[startup+540.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 11310 0 0 0 53965 35 0 0 25 0 1 0 423204657 49008640 11179 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11965 11179 603 41 0 11924 0
vsize: 47860
[startup+550.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 11614 0 0 0 54965 36 0 0 25 0 1 0 423204657 50212864 11483 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12259 11483 603 41 0 12218 0
vsize: 49036
[startup+560.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 11841 0 0 0 55964 36 0 0 25 0 1 0 423204657 51146752 11710 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12487 11710 603 41 0 12446 0
vsize: 49948
[startup+570.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12104 0 0 0 56964 37 0 0 25 0 1 0 423204657 52215808 11973 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12748 11973 603 41 0 12707 0
vsize: 50992
[startup+580.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12314 0 0 0 57963 38 0 0 25 0 1 0 423204657 53018624 12183 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12944 12183 603 41 0 12903 0
vsize: 51776
[startup+590.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12363 0 0 0 58964 38 0 0 25 0 1 0 423204657 53280768 12232 4294967295 134512640 134672761 3221224576 3221223776 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13008 12232 603 41 0 12967 0
vsize: 52032
[startup+600.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12408 0 0 0 59964 38 0 0 25 0 1 0 423204657 53415936 12277 4294967295 134512640 134672761 3221224576 3221223776 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13041 12277 603 41 0 13000 0
vsize: 52164
[startup+610.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12461 0 0 0 60964 38 0 0 25 0 1 0 423204657 53551104 12330 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13074 12330 603 41 0 13033 0
vsize: 52296
[startup+620.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12518 0 0 0 61964 38 0 0 25 0 1 0 423204657 53821440 12387 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13140 12387 603 41 0 13099 0
vsize: 52560
[startup+630.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12574 0 0 0 62964 38 0 0 25 0 1 0 423204657 54091776 12443 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13206 12443 603 41 0 13165 0
vsize: 52824
[startup+640.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12676 0 0 0 63964 39 0 0 25 0 1 0 423204657 54501376 12545 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13306 12545 603 41 0 13265 0
vsize: 53224
[startup+650.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12744 0 0 0 64963 39 0 0 25 0 1 0 423204657 54767616 12613 4294967295 134512640 134672761 3221224576 3221223760 134559116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13371 12613 603 41 0 13330 0
vsize: 53484
[startup+660.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12765 0 0 0 65963 39 0 0 25 0 1 0 423204657 54898688 12634 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13403 12634 603 41 0 13362 0
vsize: 53612
[startup+670.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12785 0 0 0 66963 39 0 0 25 0 1 0 423204657 54898688 12654 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13403 12654 603 41 0 13362 0
vsize: 53612
[startup+680.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12804 0 0 0 67963 39 0 0 25 0 1 0 423204657 55033856 12673 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13436 12673 603 41 0 13395 0
vsize: 53744
[startup+690.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12823 0 0 0 68963 39 0 0 25 0 1 0 423204657 55033856 12692 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13436 12692 603 41 0 13395 0
vsize: 53744
[startup+700.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12842 0 0 0 69963 40 0 0 25 0 1 0 423204657 55169024 12711 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13469 12711 603 41 0 13428 0
vsize: 53876
[startup+710.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12859 0 0 0 70963 40 0 0 25 0 1 0 423204657 55169024 12728 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13469 12728 603 41 0 13428 0
vsize: 53876
[startup+720.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12880 0 0 0 71964 40 0 0 25 0 1 0 423204657 55304192 12749 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13502 12749 603 41 0 13461 0
vsize: 54008
[startup+730.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12897 0 0 0 72964 40 0 0 25 0 1 0 423204657 55304192 12766 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13502 12766 603 41 0 13461 0
vsize: 54008
[startup+740.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12919 0 0 0 73964 40 0 0 25 0 1 0 423204657 55439360 12788 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13535 12788 603 41 0 13494 0
vsize: 54140
[startup+750.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12937 0 0 0 74964 40 0 0 25 0 1 0 423204657 55570432 12806 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13567 12806 603 41 0 13526 0
vsize: 54268
[startup+760.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12958 0 0 0 75964 40 0 0 25 0 1 0 423204657 55570432 12827 4294967295 134512640 134672761 3221224576 3221223744 134561272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13567 12827 603 41 0 13526 0
vsize: 54268
[startup+770.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12978 0 0 0 76964 40 0 0 25 0 1 0 423204657 55705600 12847 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13600 12847 603 41 0 13559 0
vsize: 54400
[startup+780.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 12995 0 0 0 77964 40 0 0 25 0 1 0 423204657 55705600 12864 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13600 12864 603 41 0 13559 0
vsize: 54400
[startup+790.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13021 0 0 0 78964 40 0 0 25 0 1 0 423204657 55840768 12890 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13633 12890 603 41 0 13592 0
vsize: 54532
[startup+800.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13046 0 0 0 79964 40 0 0 25 0 1 0 423204657 55975936 12915 4294967295 134512640 134672761 3221224576 3221223776 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13666 12915 603 41 0 13625 0
vsize: 54664
[startup+810.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13077 0 0 0 80964 40 0 0 25 0 1 0 423204657 56111104 12946 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13699 12946 603 41 0 13658 0
vsize: 54796
[startup+820.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13102 0 0 0 81964 40 0 0 25 0 1 0 423204657 56246272 12971 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13732 12971 603 41 0 13691 0
vsize: 54928
[startup+830.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13127 0 0 0 82964 40 0 0 25 0 1 0 423204657 56246272 12996 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13732 12996 603 41 0 13691 0
vsize: 54928
[startup+840.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13161 0 0 0 83965 40 0 0 25 0 1 0 423204657 56381440 13030 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13765 13030 603 41 0 13724 0
vsize: 55060
[startup+850.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13188 0 0 0 84965 41 0 0 25 0 1 0 423204657 56512512 13057 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13797 13057 603 41 0 13756 0
vsize: 55188
[startup+860.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13214 0 0 0 85965 41 0 0 25 0 1 0 423204657 56647680 13083 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13830 13083 603 41 0 13789 0
vsize: 55320
[startup+870.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13246 0 0 0 86965 41 0 0 25 0 1 0 423204657 56782848 13115 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13863 13115 603 41 0 13822 0
vsize: 55452
[startup+880.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13276 0 0 0 87965 41 0 0 25 0 1 0 423204657 56913920 13145 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13895 13145 603 41 0 13854 0
vsize: 55580
[startup+890.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13310 0 0 0 88965 41 0 0 25 0 1 0 423204657 57049088 13179 4294967295 134512640 134672761 3221224576 3221223776 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13928 13179 603 41 0 13887 0
vsize: 55712
[startup+900.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13359 0 0 0 89965 41 0 0 25 0 1 0 423204657 57184256 13228 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13961 13228 603 41 0 13920 0
vsize: 55844
[startup+910.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13419 0 0 0 90965 41 0 0 25 0 1 0 423204657 57454592 13288 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14027 13288 603 41 0 13986 0
vsize: 56108
[startup+920.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13478 0 0 0 91965 41 0 0 25 0 1 0 423204657 57724928 13347 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14093 13347 603 41 0 14052 0
vsize: 56372
[startup+930.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13540 0 0 0 92965 42 0 0 25 0 1 0 423204657 57995264 13409 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14159 13409 603 41 0 14118 0
vsize: 56636
[startup+940.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13615 0 0 0 93965 42 0 0 25 0 1 0 423204657 58265600 13484 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14225 13484 603 41 0 14184 0
vsize: 56900
[startup+950.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13682 0 0 0 94965 43 0 0 25 0 1 0 423204657 58531840 13551 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14290 13551 603 41 0 14249 0
vsize: 57160
[startup+960.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13747 0 0 0 95965 43 0 0 25 0 1 0 423204657 58798080 13616 4294967295 134512640 134672761 3221224576 3221223716 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14355 13616 603 41 0 14314 0
vsize: 57420
[startup+970.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13830 0 0 0 96964 43 0 0 25 0 1 0 423204657 59068416 13699 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14421 13699 603 41 0 14380 0
vsize: 57684
[startup+980.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13910 0 0 0 97964 43 0 0 25 0 1 0 423204657 59473920 13779 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14520 13779 603 41 0 14479 0
vsize: 58080
[startup+990.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 13990 0 0 0 98964 44 0 0 25 0 1 0 423204657 59744256 13859 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14586 13859 603 41 0 14545 0
vsize: 58344
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 14085 0 0 0 99964 44 0 0 25 0 1 0 423204657 60145664 13954 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14684 13954 603 41 0 14643 0
vsize: 58736
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 14197 0 0 0 100964 44 0 0 25 0 1 0 423204657 60551168 14066 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14783 14066 603 41 0 14742 0
vsize: 59132
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 14295 0 0 0 101964 45 0 0 25 0 1 0 423204657 60952576 14164 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14881 14164 603 41 0 14840 0
vsize: 59524
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 14399 0 0 0 102964 45 0 0 25 0 1 0 423204657 61358080 14268 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14980 14268 603 41 0 14939 0
vsize: 59920
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 14468 0 0 0 103964 45 0 0 25 0 1 0 423204657 61624320 14337 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15045 14337 603 41 0 15004 0
vsize: 60180
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 14547 0 0 0 104964 45 0 0 25 0 1 0 423204657 62029824 14416 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15144 14416 603 41 0 15103 0
vsize: 60576
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 14635 0 0 0 105964 46 0 0 25 0 1 0 423204657 62296064 14504 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15209 14504 603 41 0 15168 0
vsize: 60836
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 14798 0 0 0 106964 46 0 0 25 0 1 0 423204657 62971904 14667 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15374 14667 603 41 0 15333 0
vsize: 61496
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 15077 0 0 0 107963 46 0 0 25 0 1 0 423204657 64176128 14946 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15668 14946 603 41 0 15627 0
vsize: 62672
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 15213 0 0 0 108963 47 0 0 25 0 1 0 423204657 64708608 15082 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15798 15082 603 41 0 15757 0
vsize: 63192
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 15459 0 0 0 109962 48 0 0 25 0 1 0 423204657 65642496 15328 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16026 15328 603 41 0 15985 0
vsize: 64104
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 15664 0 0 0 110962 48 0 0 25 0 1 0 423204657 66576384 15533 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16254 15533 603 41 0 16213 0
vsize: 65016
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 19214
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 15808 0 0 0 111961 49 0 0 25 0 1 0 423204657 67112960 15677 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16385 15677 603 41 0 16344 0
vsize: 65540
[startup+1130.03 s]
Raw data (loadavg): 1.15 1.03 0.94 2/54 19267
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 16007 0 0 0 112961 49 0 0 25 0 1 0 423204657 67903488 15876 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16578 15876 603 41 0 16537 0
vsize: 66312
[startup+1140.03 s]
Raw data (loadavg): 1.12 1.03 0.94 2/54 19267
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 16229 0 0 0 113960 50 0 0 25 0 1 0 423204657 68833280 16098 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16805 16098 603 41 0 16764 0
vsize: 67220
[startup+1150.03 s]
Raw data (loadavg): 1.10 1.03 0.94 2/54 19267
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 16541 0 0 0 114959 51 0 0 25 0 1 0 423204657 70049792 16410 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17102 16410 603 41 0 17061 0
vsize: 68408
[startup+1160.03 s]
Raw data (loadavg): 1.09 1.03 0.94 2/54 19267
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 16722 0 0 0 115959 52 0 0 25 0 1 0 423204657 70860800 16591 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17300 16591 603 41 0 17259 0
vsize: 69200
[startup+1170.03 s]
Raw data (loadavg): 1.07 1.03 0.94 2/54 19267
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 16953 0 0 0 116959 52 0 0 25 0 1 0 423204657 71798784 16822 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17529 16822 603 41 0 17488 0
vsize: 70116
[startup+1180.03 s]
Raw data (loadavg): 1.06 1.02 0.94 2/54 19267
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 17137 0 0 0 117958 53 0 0 25 0 1 0 423204657 72470528 17006 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17693 17006 603 41 0 17652 0
vsize: 70772
[startup+1190.03 s]
Raw data (loadavg): 1.05 1.02 0.94 2/54 19267
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 17293 0 0 0 118958 53 0 0 25 0 1 0 423204657 73138176 17162 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17856 17162 603 41 0 17815 0
vsize: 71424
[startup+1200.03 s]
Raw data (loadavg): 1.04 1.02 0.94 2/54 19269
Raw data (stat): 19214 (minisat+) R 19213 10720 10719 0 -1 0 17407 0 0 0 119958 54 0 0 25 0 1 0 423204657 73670656 17276 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17986 17276 603 41 0 17945 0
vsize: 71944
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.04 1.02 0.94 1/54 19269
Raw data (stat): 19214 (minisat+) Z 19213 10720 10719 0 -1 12 17410 0 0 0 119958 58 0 0 25 0 1 0 423204657 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.07
CPU time (s): 1200.17
CPU user time (s): 1199.58
CPU system time (s): 0.580911
CPU usage (%): 100.008
Max. virtual memory (Kb): 71944
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####