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-ex5.pi.opb
MD5SUM	ebc55cfc194a279163f52418008eccf2
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	65
Optimality of the best value was proved	NO
Number of terms in the objective function	2460
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	2460
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	2460
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.11783
Number of variables	2459
Total number of constraints	873
Number of constraints which are clauses	873
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	1
Maximum length of a constraint	146
Trace number 6173

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-14 03:39:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4579 boxname=wulflinc29 idbench=67 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ebc55cfc194a279163f52418008eccf2  /oldhome/oroussel/tmp/wulflinc29/normalized-ex5.pi.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc29/normalized-ex5.pi.opb /oldhome/oroussel/tmp/wulflinc29/normalized-ex5.pi.opb
IDLAUNCH: 4579
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        816960 kB
Buffers:         36768 kB
Cached:         143148 kB
SwapCached:         12 kB
Active:          65128 kB
Inactive:       117652 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        816708 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            29116 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:59:09 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 4579 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 845 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ===
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     842    40436 |     280       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 85[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4858   maxlim: 2375   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   34747   161500 |   11582       0        0     nan |  0.000 % |
c |       100 |   34625   161078 |   12740      82      553     6.7 |  0.806 % |
c |       250 |   34538   160783 |   14014     220     1070     4.9 |  1.025 % |
c |       476 |   34538   160783 |   15415     446     1962     4.4 |  1.025 % |
c |       813 |   34538   160783 |   16957     783     3179     4.1 |  1.025 % |
c |      1319 |   34538   160783 |   18652    1289     5202     4.0 |  1.025 % |
c |      2078 |   34538   160783 |   20518    2048     8968     4.4 |  1.025 % |
c |      3217 |   34538   160783 |   22570    3187    41044    12.9 |  1.025 % |
c |      4925 |   34538   160783 |   24827    4895   148848    30.4 |  1.025 % |
c |      7488 |   34529   160752 |   27309    7454   375261    50.3 |  1.039 % |
c |     11332 |   34529   160752 |   30040   11298   970376    85.9 |  1.039 % |
c |     17098 |   34529   160752 |   33044   17064  1482512    86.9 |  1.039 % |
c |     25750 |   34529   160752 |   36349   25716  3886945   151.1 |  1.039 % |
c |     38725 |   34480   160583 |   39984   15272  2809105   183.9 |  1.148 % |
c |     58186 |   34435   160420 |   43982   34726  7848884   226.0 |  1.244 % |
c |     87378 |   34435   160420 |   48380   33293  9730259   292.3 |  1.244 % |
c |    131171 |   34435   160420 |   53218   43028 10414269   242.0 |  1.244 % |
c |    196858 |   34429   160400 |   58540   32182  8102604   251.8 |  1.257 % |
c |    295386 |   34374   160217 |   64394   45361 15385286   339.2 |  1.394 % |
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 x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 -x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 x1466 -x1467 -x1468 -x1469 x1470 -x1471 -x1472 -x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 -x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 x1518 -x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 -x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 -x1567 -x1568 -x1569 -x1570 -x1571 -x1572 -x1573 x1574 -x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 -x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 -x1634 -x1635 -x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 x1651 x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 -x1709 -x1710 -x1711 -x1712 -x1713 -x1714 -x1715 x1716 x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 x1761 -x1762 -x1763 -x1764 -x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 -x1787 -x1788 -x1789 -x1790 -x1791 x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 -x1818 -x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 -x1827 -x1828 -x1829 -x1830 -x1831 -x1832 -x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 x1844 -x1845 -x1846 -x1847 -x1848 -x1849 -x1850 x1851 x1852 x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 -x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 x1910 -x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 x#### 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.85 0.95 0.90 2/54 1476
Raw data (stat): 1476 (runsolver) R 1475 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481413767 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.0014 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 3524 0 0 0 990 9 0 0 25 0 1 0 481413767 16318464 3254 4294967295 134512640 134672761 3221224576 3221223632 134565039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3984 3254 603 41 0 3943 0
vsize: 15936
[startup+20.0018 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 4876 0 0 0 1986 13 0 0 25 0 1 0 481413767 21827584 4606 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5329 4606 603 41 0 5288 0
vsize: 21316
[startup+30.0019 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 6308 0 0 0 2982 17 0 0 25 0 1 0 481413767 27738112 6038 4294967295 134512640 134672761 3221224576 3221223760 134558937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6772 6038 603 41 0 6731 0
vsize: 27088
[startup+40.0031 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 7321 0 0 0 3978 20 0 0 25 0 1 0 481413767 31772672 7051 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 7051 603 41 0 7716 0
vsize: 31028
[startup+50.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 8329 0 0 0 4975 24 0 0 25 0 1 0 481413767 35942400 8059 4294967295 134512640 134672761 3221224576 3221223680 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8775 8059 603 41 0 8734 0
vsize: 35100
[startup+60.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 9204 0 0 0 5973 26 0 0 25 0 1 0 481413767 39567360 8934 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9660 8934 603 41 0 9619 0
vsize: 38640
[startup+70.0049 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 10032 0 0 0 6970 30 0 0 25 0 1 0 481413767 43044864 9762 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10509 9762 603 41 0 10468 0
vsize: 42036
[startup+80.0043 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 10244 0 0 0 7969 30 0 0 25 0 1 0 481413767 43851776 9974 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 9974 603 41 0 10665 0
vsize: 42824
[startup+90.0044 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 10244 0 0 0 8969 30 0 0 25 0 1 0 481413767 43851776 9974 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 9974 603 41 0 10665 0
vsize: 42824
[startup+100.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 10244 0 0 0 9969 30 0 0 25 0 1 0 481413767 43851776 9974 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 9974 603 41 0 10665 0
vsize: 42824
[startup+110.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 10285 0 0 0 10970 30 0 0 25 0 1 0 481413767 43986944 10015 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10739 10015 603 41 0 10698 0
vsize: 42956
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 11158 0 0 0 11968 32 0 0 25 0 1 0 481413767 47624192 10888 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11627 10888 603 41 0 11586 0
vsize: 46508
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 12150 0 0 0 12965 35 0 0 25 0 1 0 481413767 51646464 11880 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12609 11880 603 41 0 12568 0
vsize: 50436
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 13125 0 0 0 13963 37 0 0 25 0 1 0 481413767 55668736 12855 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13591 12855 603 41 0 13550 0
vsize: 54364
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 14153 0 0 0 14961 40 0 0 25 0 1 0 481413767 59834368 13883 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14608 13883 603 41 0 14567 0
vsize: 58432
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 14712 0 0 0 15959 41 0 0 25 0 1 0 481413767 62111744 14442 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15164 14442 603 41 0 15123 0
vsize: 60656
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 14712 0 0 0 16959 41 0 0 25 0 1 0 481413767 62111744 14442 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15164 14442 603 41 0 15123 0
vsize: 60656
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 14712 0 0 0 17959 41 0 0 25 0 1 0 481413767 62111744 14442 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15164 14442 603 41 0 15123 0
vsize: 60656
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 14712 0 0 0 18960 41 0 0 25 0 1 0 481413767 62111744 14442 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15164 14442 603 41 0 15123 0
vsize: 60656
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 14712 0 0 0 19960 41 0 0 25 0 1 0 481413767 62111744 14442 4294967295 134512640 134672761 3221224576 3221223680 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15164 14442 603 41 0 15123 0
vsize: 60656
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 14712 0 0 0 20960 41 0 0 25 0 1 0 481413767 62111744 14442 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15164 14442 603 41 0 15123 0
vsize: 60656
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 14712 0 0 0 21960 41 0 0 25 0 1 0 481413767 62111744 14442 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14442 603 41 0 15123 0
vsize: 60656
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 14712 0 0 0 22960 42 0 0 25 0 1 0 481413767 62111744 14442 4294967295 134512640 134672761 3221224576 3221223680 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15164 14442 603 41 0 15123 0
vsize: 60656
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 15665 0 0 0 23958 44 0 0 25 0 1 0 481413767 66002944 15395 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16114 15395 603 41 0 16073 0
vsize: 64456
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 16641 0 0 0 24954 48 0 0 25 0 1 0 481413767 70033408 16371 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17098 16371 603 41 0 17057 0
vsize: 68392
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 17403 0 0 0 25952 50 0 0 25 0 1 0 481413767 73117696 17133 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17851 17133 603 41 0 17810 0
vsize: 71404
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18196 0 0 0 26950 52 0 0 25 0 1 0 481413767 76468224 17926 4294967295 134512640 134672761 3221224576 3221223680 134555084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18669 17926 603 41 0 18628 0
vsize: 74676
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18779 0 0 0 27948 54 0 0 25 0 1 0 481413767 78745600 18509 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19225 18509 603 41 0 19184 0
vsize: 76900
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18779 0 0 0 28949 54 0 0 25 0 1 0 481413767 78745600 18509 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19225 18509 603 41 0 19184 0
vsize: 76900
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18779 0 0 0 29949 54 0 0 25 0 1 0 481413767 78745600 18509 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19225 18509 603 41 0 19184 0
vsize: 76900
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18779 0 0 0 30949 54 0 0 25 0 1 0 481413767 78745600 18509 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19225 18509 603 41 0 19184 0
vsize: 76900
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18779 0 0 0 31949 54 0 0 25 0 1 0 481413767 78745600 18509 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19225 18509 603 41 0 19184 0
vsize: 76900
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18779 0 0 0 32949 54 0 0 25 0 1 0 481413767 78745600 18509 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19225 18509 603 41 0 19184 0
vsize: 76900
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18779 0 0 0 33950 54 0 0 25 0 1 0 481413767 78745600 18509 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19225 18509 603 41 0 19184 0
vsize: 76900
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18779 0 0 0 34950 54 0 0 25 0 1 0 481413767 78745600 18509 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19225 18509 603 41 0 19184 0
vsize: 76900
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18779 0 0 0 35950 54 0 0 25 0 1 0 481413767 78745600 18509 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19225 18509 603 41 0 19184 0
vsize: 76900
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18781 0 0 0 36950 54 0 0 25 0 1 0 481413767 78745600 18511 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19225 18511 603 41 0 19184 0
vsize: 76900
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 37950 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 38950 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 39951 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 40951 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223680 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 41951 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 42951 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 43951 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 44952 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 45952 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 46952 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 47952 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 48952 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 49953 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223712 134565058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 18783 0 0 0 50953 54 0 0 25 0 1 0 481413767 78708736 18510 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 18510 603 41 0 19175 0
vsize: 76864
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19060 0 0 0 51952 55 0 0 25 0 1 0 481413767 79908864 18787 4294967295 134512640 134672761 3221224576 3221223760 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18787 603 41 0 19468 0
vsize: 78036
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19061 0 0 0 52953 55 0 0 25 0 1 0 481413767 79908864 18788 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18788 603 41 0 19468 0
vsize: 78036
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19061 0 0 0 53953 55 0 0 25 0 1 0 481413767 79908864 18788 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18788 603 41 0 19468 0
vsize: 78036
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19061 0 0 0 54953 55 0 0 25 0 1 0 481413767 79908864 18788 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18788 603 41 0 19468 0
vsize: 78036
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19061 0 0 0 55953 55 0 0 25 0 1 0 481413767 79908864 18788 4294967295 134512640 134672761 3221224576 3221223680 134554907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18788 603 41 0 19468 0
vsize: 78036
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19061 0 0 0 56953 55 0 0 25 0 1 0 481413767 79908864 18788 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18788 603 41 0 19468 0
vsize: 78036
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19061 0 0 0 57953 55 0 0 25 0 1 0 481413767 79908864 18788 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18788 603 41 0 19468 0
vsize: 78036
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19061 0 0 0 58953 55 0 0 25 0 1 0 481413767 79908864 18788 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18788 603 41 0 19468 0
vsize: 78036
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19061 0 0 0 59953 55 0 0 25 0 1 0 481413767 79908864 18788 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18788 603 41 0 19468 0
vsize: 78036
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19061 0 0 0 60954 55 0 0 25 0 1 0 481413767 79908864 18788 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18788 603 41 0 19468 0
vsize: 78036
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19061 0 0 0 61954 55 0 0 25 0 1 0 481413767 79908864 18788 4294967295 134512640 134672761 3221224576 3221223680 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18788 603 41 0 19468 0
vsize: 78036
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19061 0 0 0 62954 55 0 0 25 0 1 0 481413767 79908864 18788 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18788 603 41 0 19468 0
vsize: 78036
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19062 0 0 0 63954 55 0 0 25 0 1 0 481413767 79908864 18789 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18789 603 41 0 19468 0
vsize: 78036
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19063 0 0 0 64954 55 0 0 25 0 1 0 481413767 79908864 18790 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18790 603 41 0 19468 0
vsize: 78036
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19115 0 0 0 65954 55 0 0 25 0 1 0 481413767 80175104 18842 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19574 18842 603 41 0 19533 0
vsize: 78296
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 66953 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 67953 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 68953 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 69953 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 70953 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 71953 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 72954 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 73954 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 74954 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 75954 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 76954 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 77954 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223760 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 78955 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223760 134558918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19509 0 0 0 79955 57 0 0 25 0 1 0 481413767 81784832 19236 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19236 603 41 0 19926 0
vsize: 79868
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 19626 0 0 0 80955 57 0 0 25 0 1 0 481413767 82186240 19353 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20065 19353 603 41 0 20024 0
vsize: 80260
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 20420 0 0 0 81953 59 0 0 25 0 1 0 481413767 85413888 20147 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20853 20147 603 41 0 20812 0
vsize: 83412
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 21167 0 0 0 82952 61 0 0 25 0 1 0 481413767 88514560 20894 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21610 20894 603 41 0 21569 0
vsize: 86440
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 21983 0 0 0 83950 63 0 0 25 0 1 0 481413767 91865088 21710 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22428 21710 603 41 0 22387 0
vsize: 89712
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 22734 0 0 0 84947 66 0 0 25 0 1 0 481413767 94957568 22461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23183 22461 603 41 0 23142 0
vsize: 92732
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 23455 0 0 0 85944 69 0 0 25 0 1 0 481413767 97910784 23182 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23904 23182 603 41 0 23863 0
vsize: 95616
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24182 0 0 0 86942 71 0 0 25 0 1 0 481413767 100859904 23909 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24624 23909 603 41 0 24583 0
vsize: 98496
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24257 0 0 0 87942 72 0 0 25 0 1 0 481413767 101265408 23984 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23984 603 41 0 24682 0
vsize: 98892
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24257 0 0 0 88942 72 0 0 25 0 1 0 481413767 101265408 23984 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23984 603 41 0 24682 0
vsize: 98892
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 89942 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 90942 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 91943 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 92943 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 93943 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 94943 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 95944 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 96944 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 97944 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 98944 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 99944 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 100944 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223680 134554919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 101944 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223776 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 102944 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 103944 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24258 0 0 0 104945 72 0 0 25 0 1 0 481413767 101265408 23985 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23985 603 41 0 24682 0
vsize: 98892
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24270 0 0 0 105945 72 0 0 25 0 1 0 481413767 101265408 23997 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 23997 603 41 0 24682 0
vsize: 98892
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 24937 0 0 0 106943 73 0 0 25 0 1 0 481413767 103948288 24664 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25378 24664 603 41 0 25337 0
vsize: 101512
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 25641 0 0 0 107941 76 0 0 25 0 1 0 481413767 106913792 25368 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26102 25368 603 41 0 26061 0
vsize: 104408
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26096 0 0 0 108940 77 0 0 25 0 1 0 481413767 108920832 25823 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26592 25823 603 41 0 26551 0
vsize: 106368
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26292 0 0 0 109940 77 0 0 25 0 1 0 481413767 109727744 26019 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26789 26019 603 41 0 26748 0
vsize: 107156
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26292 0 0 0 110940 77 0 0 25 0 1 0 481413767 109727744 26019 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26789 26019 603 41 0 26748 0
vsize: 107156
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26292 0 0 0 111940 77 0 0 25 0 1 0 481413767 109727744 26019 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26789 26019 603 41 0 26748 0
vsize: 107156
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26292 0 0 0 112941 77 0 0 25 0 1 0 481413767 109727744 26019 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26789 26019 603 41 0 26748 0
vsize: 107156
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26292 0 0 0 113941 77 0 0 25 0 1 0 481413767 109727744 26019 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26789 26019 603 41 0 26748 0
vsize: 107156
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26292 0 0 0 114941 77 0 0 25 0 1 0 481413767 109727744 26019 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26789 26019 603 41 0 26748 0
vsize: 107156
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26293 0 0 0 115941 77 0 0 25 0 1 0 481413767 109727744 26020 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26789 26020 603 41 0 26748 0
vsize: 107156
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26293 0 0 0 116941 77 0 0 25 0 1 0 481413767 109727744 26020 4294967295 134512640 134672761 3221224576 3221223744 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26789 26020 603 41 0 26748 0
vsize: 107156
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26293 0 0 0 117941 77 0 0 25 0 1 0 481413767 109727744 26020 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26789 26020 603 41 0 26748 0
vsize: 107156
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26293 0 0 0 118942 77 0 0 25 0 1 0 481413767 109727744 26020 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26789 26020 603 41 0 26748 0
vsize: 107156
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1476
Raw data (stat): 1476 (minisat+) R 1475 27222 27221 0 -1 0 26293 0 0 0 119942 77 0 0 25 0 1 0 481413767 109727744 26020 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26789 26020 603 41 0 26748 0
vsize: 107156
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 1476
Raw data (stat): 1476 (minisat+) Z 1475 27222 27221 0 -1 12 26296 0 0 0 119942 82 0 0 25 0 1 0 481413767 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.08
CPU time (s): 1200.25
CPU user time (s): 1199.43
CPU system time (s): 0.824874
CPU usage (%): 100.014
Max. virtual memory (Kb): 107156
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####