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 4662

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-13 19:43:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3451 boxname=wulflinc6 idbench=67 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ebc55cfc194a279163f52418008eccf2  /oldhome/oroussel/tmp/wulflinc6/normalized-ex5.pi.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc6/normalized-ex5.pi.opb /oldhome/oroussel/tmp/wulflinc6/normalized-ex5.pi.opb
IDLAUNCH: 3451
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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	: 2
cpu MHz		: 451.042
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:        922320 kB
Buffers:         34144 kB
Cached:          56304 kB
SwapCached:       2644 kB
Active:          48456 kB
Inactive:        47500 kB
HighTotal:      131008 kB
HighFree:        70728 kB
LowTotal:       903652 kB
LowFree:        851592 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10732 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:03:50 (client local time) WITH STATUS 10 IN 1200.45 SECONDS
stats: 3451 7 1200.45 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 |   34737   161466 |   11579       0        0     nan |  0.000 % |
c |       100 |   34618   161056 |   12736      82      481     5.9 |  0.806 % |
c |       250 |   34540   160790 |   14010     220      989     4.5 |  0.998 % |
c |       475 |   34531   160761 |   15411     444     1750     3.9 |  1.025 % |
c |       812 |   34531   160761 |   16952     781     2965     3.8 |  1.025 % |
c |      1318 |   34531   160761 |   18648    1287     4992     3.9 |  1.025 % |
c |      2078 |   34531   160761 |   20512    2047     8518     4.2 |  1.025 % |
c |      3217 |   34508   160682 |   22564    3183    47615    15.0 |  1.080 % |
c |      4926 |   34508   160682 |   24820    4892   191719    39.2 |  1.080 % |
c |      7489 |   34508   160682 |   27302    7455   425632    57.1 |  1.080 % |
c |     11333 |   34508   160682 |   30032   11299  1258375   111.4 |  1.080 % |
c |     17099 |   34508   160682 |   33036   17065  2287130   134.0 |  1.080 % |
c |     25749 |   34508   160682 |   36339   25715  4245539   165.1 |  1.080 % |
c |     38725 |   34508   160682 |   39973   16115  3362710   208.7 |  1.080 % |
c |     58186 |   34431   160415 |   43971   35563  7169613   201.6 |  1.257 % |
c |     87378 |   34379   160235 |   48368   35570  8100106   227.7 |  1.366 % |
c |    131167 |   34379   160235 |   53205   46080 12000220   260.4 |  1.366 % |
c |    196852 |   34379   160235 |   58525   37411  9993767   267.1 |  1.366 % |
c |    295378 |   34356   160156 |   64378   48374 12065931   249.4 |  1.421 % |
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.84 0.94 0.69 2/54 31437
Raw data (stat): 31437 (runsolver) R 31436 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420342389 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.87 0.94 0.70 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 1802 0 0 0 992 6 0 0 25 0 1 0 420342389 9027584 1780 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2204 1780 603 41 0 2163 0
vsize: 8816
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.94 0.70 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 3175 0 0 0 1989 9 0 0 25 0 1 0 420342389 14675968 3153 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3583 3153 603 41 0 3542 0
vsize: 14332
[startup+30.0014 s]
Raw data (loadavg): 0.90 0.94 0.70 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 4426 0 0 0 2986 13 0 0 25 0 1 0 420342389 19824640 4404 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4840 4404 603 41 0 4799 0
vsize: 19360
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.94 0.71 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 5511 0 0 0 3984 15 0 0 25 0 1 0 420342389 24256512 5489 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5922 5490 603 41 0 5881 0
vsize: 23688
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.94 0.71 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 6630 0 0 0 4981 18 0 0 25 0 1 0 420342389 28827648 6608 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7038 6608 603 41 0 6997 0
vsize: 28152
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.94 0.71 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 7637 0 0 0 5978 21 0 0 25 0 1 0 420342389 32993280 7615 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8055 7615 603 41 0 8014 0
vsize: 32220
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.95 0.72 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 8506 0 0 0 6976 24 0 0 25 0 1 0 420342389 36618240 8484 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8940 8484 603 41 0 8899 0
vsize: 35760
[startup+80.0035 s]
Raw data (loadavg): 0.96 0.95 0.72 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 9094 0 0 0 7975 25 0 0 25 0 1 0 420342389 39038976 9072 4294967295 134512640 134672761 3221224576 3221223760 134559514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9531 9072 603 41 0 9490 0
vsize: 38124
[startup+90.0033 s]
Raw data (loadavg): 0.96 0.95 0.72 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 9094 0 0 0 8976 25 0 0 25 0 1 0 420342389 39038976 9072 4294967295 134512640 134672761 3221224576 3221223680 134560201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9531 9072 603 41 0 9490 0
vsize: 38124
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.72 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 9094 0 0 0 9976 25 0 0 25 0 1 0 420342389 39038976 9072 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9531 9072 603 41 0 9490 0
vsize: 38124
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.73 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 9094 0 0 0 10976 25 0 0 25 0 1 0 420342389 39038976 9072 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9531 9072 603 41 0 9490 0
vsize: 38124
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 9551 0 0 0 11976 26 0 0 25 0 1 0 420342389 40923136 9529 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9991 9529 603 41 0 9950 0
vsize: 39964
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 10484 0 0 0 12974 28 0 0 25 0 1 0 420342389 44699648 10462 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10913 10462 603 41 0 10872 0
vsize: 43652
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 11057 0 0 0 13972 31 0 0 25 0 1 0 420342389 46972928 11035 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11468 11035 603 41 0 11427 0
vsize: 45872
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.74 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 11057 0 0 0 14972 31 0 0 25 0 1 0 420342389 46972928 11035 4294967295 134512640 134672761 3221224576 3221223680 134560322 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11468 11035 603 41 0 11427 0
vsize: 45872
[startup+160.006 s]
Raw data (loadavg): 0.99 0.95 0.74 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 11057 0 0 0 15973 31 0 0 25 0 1 0 420342389 46972928 11035 4294967295 134512640 134672761 3221224576 3221223712 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11468 11035 603 41 0 11427 0
vsize: 45872
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 11057 0 0 0 16973 31 0 0 25 0 1 0 420342389 46972928 11035 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11468 11035 603 41 0 11427 0
vsize: 45872
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 11057 0 0 0 17973 31 0 0 25 0 1 0 420342389 46972928 11035 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11468 11035 603 41 0 11427 0
vsize: 45872
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 11057 0 0 0 18974 31 0 0 25 0 1 0 420342389 46972928 11035 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11468 11035 603 41 0 11427 0
vsize: 45872
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 11057 0 0 0 19974 31 0 0 25 0 1 0 420342389 46972928 11035 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11468 11035 603 41 0 11427 0
vsize: 45872
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 11057 0 0 0 20974 31 0 0 25 0 1 0 420342389 46972928 11035 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11468 11035 603 41 0 11427 0
vsize: 45872
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 11057 0 0 0 21974 31 0 0 25 0 1 0 420342389 46972928 11035 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11468 11035 603 41 0 11427 0
vsize: 45872
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 11543 0 0 0 22973 33 0 0 25 0 1 0 420342389 48979968 11521 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11958 11521 603 41 0 11917 0
vsize: 47832
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 12135 0 0 0 23971 35 0 0 25 0 1 0 420342389 51388416 12113 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12546 12113 603 41 0 12505 0
vsize: 50184
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 12844 0 0 0 24968 38 0 0 25 0 1 0 420342389 54353920 12822 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13270 12822 603 41 0 13229 0
vsize: 53080
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.76 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13599 0 0 0 25967 40 0 0 25 0 1 0 420342389 57450496 13577 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14026 13577 603 41 0 13985 0
vsize: 56104
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13884 0 0 0 26966 41 0 0 25 0 1 0 420342389 58527744 13862 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14289 13862 603 41 0 14248 0
vsize: 57156
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13884 0 0 0 27966 41 0 0 25 0 1 0 420342389 58527744 13862 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14289 13862 603 41 0 14248 0
vsize: 57156
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13884 0 0 0 28967 41 0 0 25 0 1 0 420342389 58527744 13862 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14289 13862 603 41 0 14248 0
vsize: 57156
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13884 0 0 0 29967 41 0 0 25 0 1 0 420342389 58527744 13862 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14289 13862 603 41 0 14248 0
vsize: 57156
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13884 0 0 0 30967 41 0 0 25 0 1 0 420342389 58527744 13862 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14289 13862 603 41 0 14248 0
vsize: 57156
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13884 0 0 0 31968 41 0 0 25 0 1 0 420342389 58527744 13862 4294967295 134512640 134672761 3221224576 3221223760 134559665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14289 13862 603 41 0 14248 0
vsize: 57156
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13884 0 0 0 32967 41 0 0 25 0 1 0 420342389 58527744 13862 4294967295 134512640 134672761 3221224576 3221223680 134555093 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14289 13862 603 41 0 14248 0
vsize: 57156
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13884 0 0 0 33967 41 0 0 25 0 1 0 420342389 58527744 13862 4294967295 134512640 134672761 3221224576 3221223744 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14289 13862 603 41 0 14248 0
vsize: 57156
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13884 0 0 0 34968 41 0 0 25 0 1 0 420342389 58527744 13862 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14289 13862 603 41 0 14248 0
vsize: 57156
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13884 0 0 0 35968 41 0 0 25 0 1 0 420342389 58527744 13862 4294967295 134512640 134672761 3221224576 3221223680 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14289 13862 603 41 0 14248 0
vsize: 57156
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 13884 0 0 0 36968 41 0 0 25 0 1 0 420342389 58527744 13862 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14289 13862 603 41 0 14248 0
vsize: 57156
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 14267 0 0 0 37968 42 0 0 25 0 1 0 420342389 60145664 14245 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14684 14245 603 41 0 14643 0
vsize: 58736
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 14952 0 0 0 38966 44 0 0 25 0 1 0 420342389 62955520 14930 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15370 14930 603 41 0 15329 0
vsize: 61480
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 15779 0 0 0 39964 46 0 0 25 0 1 0 420342389 66306048 15757 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16188 15757 603 41 0 16147 0
vsize: 64752
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16402 0 0 0 40962 49 0 0 25 0 1 0 420342389 68849664 16380 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16809 16380 603 41 0 16768 0
vsize: 67236
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16890 0 0 0 41961 50 0 0 25 0 1 0 420342389 70868992 16868 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16868 603 41 0 17261 0
vsize: 69208
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16890 0 0 0 42961 50 0 0 25 0 1 0 420342389 70868992 16868 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16868 603 41 0 17261 0
vsize: 69208
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16890 0 0 0 43962 50 0 0 25 0 1 0 420342389 70868992 16868 4294967295 134512640 134672761 3221224576 3221223760 134559575 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16868 603 41 0 17261 0
vsize: 69208
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16890 0 0 0 44962 50 0 0 25 0 1 0 420342389 70868992 16868 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16868 603 41 0 17261 0
vsize: 69208
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16890 0 0 0 45962 50 0 0 25 0 1 0 420342389 70868992 16868 4294967295 134512640 134672761 3221224576 3221223760 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16868 603 41 0 17261 0
vsize: 69208
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16891 0 0 0 46963 50 0 0 25 0 1 0 420342389 70868992 16869 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16869 603 41 0 17261 0
vsize: 69208
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16891 0 0 0 47963 50 0 0 25 0 1 0 420342389 70868992 16869 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16869 603 41 0 17261 0
vsize: 69208
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16891 0 0 0 48963 50 0 0 25 0 1 0 420342389 70868992 16869 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16869 603 41 0 17261 0
vsize: 69208
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16891 0 0 0 49964 50 0 0 25 0 1 0 420342389 70868992 16869 4294967295 134512640 134672761 3221224576 3221223680 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16869 603 41 0 17261 0
vsize: 69208
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16891 0 0 0 50964 50 0 0 25 0 1 0 420342389 70868992 16869 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16869 603 41 0 17261 0
vsize: 69208
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16891 0 0 0 51965 50 0 0 25 0 1 0 420342389 70868992 16869 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16869 603 41 0 17261 0
vsize: 69208
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16891 0 0 0 52965 50 0 0 25 0 1 0 420342389 70868992 16869 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16869 603 41 0 17261 0
vsize: 69208
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16891 0 0 0 53965 50 0 0 25 0 1 0 420342389 70868992 16869 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16869 603 41 0 17261 0
vsize: 69208
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16891 0 0 0 54966 50 0 0 25 0 1 0 420342389 70868992 16869 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16869 603 41 0 17261 0
vsize: 69208
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16891 0 0 0 55966 50 0 0 25 0 1 0 420342389 70868992 16869 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16869 603 41 0 17261 0
vsize: 69208
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 16891 0 0 0 56966 50 0 0 25 0 1 0 420342389 70868992 16869 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 16869 603 41 0 17261 0
vsize: 69208
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 17302 0 0 0 57965 52 0 0 25 0 1 0 420342389 72605696 17280 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17726 17280 603 41 0 17685 0
vsize: 70904
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 17816 0 0 0 58964 53 0 0 25 0 1 0 420342389 74739712 17794 4294967295 134512640 134672761 3221224576 3221223712 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18247 17794 603 41 0 18206 0
vsize: 72988
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 59964 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 60965 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 61965 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 62965 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 63966 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 64966 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 65966 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 66967 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 67967 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 68967 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 69967 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 70968 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223680 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 71968 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 72969 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+740.027 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 73969 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18058 0 0 0 74969 53 0 0 25 0 1 0 420342389 75673600 18036 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18475 18036 603 41 0 18434 0
vsize: 73900
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18126 0 0 0 75969 54 0 0 25 0 1 0 420342389 75939840 18104 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18540 18104 603 41 0 18499 0
vsize: 74160
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 18747 0 0 0 76968 56 0 0 25 0 1 0 420342389 78483456 18725 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19161 18725 603 41 0 19120 0
vsize: 76644
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19263 0 0 0 77967 57 0 0 25 0 1 0 420342389 80633856 19241 4294967295 134512640 134672761 3221224576 3221223680 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19686 19242 603 41 0 19645 0
vsize: 78744
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19818 0 0 0 78965 59 0 0 25 0 1 0 420342389 82894848 19796 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20238 19796 603 41 0 20197 0
vsize: 80952
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19863 0 0 0 79966 59 0 0 25 0 1 0 420342389 83025920 19841 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19841 603 41 0 20229 0
vsize: 81080
[startup+810.03 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19863 0 0 0 80966 59 0 0 25 0 1 0 420342389 83025920 19841 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19841 603 41 0 20229 0
vsize: 81080
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19864 0 0 0 81967 59 0 0 25 0 1 0 420342389 83025920 19842 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19842 603 41 0 20229 0
vsize: 81080
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19864 0 0 0 82967 59 0 0 25 0 1 0 420342389 83025920 19842 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19842 603 41 0 20229 0
vsize: 81080
[startup+840.03 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19864 0 0 0 83967 59 0 0 25 0 1 0 420342389 83025920 19842 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19842 603 41 0 20229 0
vsize: 81080
[startup+850.03 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19864 0 0 0 84968 59 0 0 25 0 1 0 420342389 83025920 19842 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19842 603 41 0 20229 0
vsize: 81080
[startup+860.032 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19865 0 0 0 85968 59 0 0 25 0 1 0 420342389 83025920 19843 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19843 603 41 0 20229 0
vsize: 81080
[startup+870.033 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19865 0 0 0 86968 59 0 0 25 0 1 0 420342389 83025920 19843 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19843 603 41 0 20229 0
vsize: 81080
[startup+880.033 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19865 0 0 0 87969 59 0 0 25 0 1 0 420342389 83025920 19843 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19843 603 41 0 20229 0
vsize: 81080
[startup+890.033 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19865 0 0 0 88969 59 0 0 25 0 1 0 420342389 83025920 19843 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19843 603 41 0 20229 0
vsize: 81080
[startup+900.034 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19865 0 0 0 89970 59 0 0 25 0 1 0 420342389 83025920 19843 4294967295 134512640 134672761 3221224576 3221223672 1075347271 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19843 603 41 0 20229 0
vsize: 81080
[startup+910.034 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19865 0 0 0 90970 59 0 0 25 0 1 0 420342389 83025920 19843 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19843 603 41 0 20229 0
vsize: 81080
[startup+920.035 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19865 0 0 0 91970 59 0 0 25 0 1 0 420342389 83025920 19843 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19843 603 41 0 20229 0
vsize: 81080
[startup+930.036 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 19865 0 0 0 92971 59 0 0 25 0 1 0 420342389 83025920 19843 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 19843 603 41 0 20229 0
vsize: 81080
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 20164 0 0 0 93970 60 0 0 25 0 1 0 420342389 84246528 20142 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20568 20142 603 41 0 20527 0
vsize: 82272
[startup+950.036 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 20872 0 0 0 94969 62 0 0 25 0 1 0 420342389 87212032 20850 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21292 20850 603 41 0 21251 0
vsize: 85168
[startup+960.036 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21564 0 0 0 95968 63 0 0 25 0 1 0 420342389 90038272 21542 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21982 21543 603 41 0 21941 0
vsize: 87928
[startup+970.037 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 31437
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 96967 64 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+980.038 s]
Raw data (loadavg): 1.07 0.99 0.86 2/54 31490
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 97962 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+990.039 s]
Raw data (loadavg): 1.06 0.99 0.86 2/54 31490
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 98962 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1000.04 s]
Raw data (loadavg): 1.05 0.99 0.87 2/54 31490
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 99963 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1010.04 s]
Raw data (loadavg): 1.04 0.99 0.87 2/54 31490
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 100963 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1020.04 s]
Raw data (loadavg): 1.04 0.99 0.87 2/54 31490
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 101963 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1030.04 s]
Raw data (loadavg): 1.03 0.99 0.87 2/54 31490
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 102964 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1040.04 s]
Raw data (loadavg): 1.03 0.99 0.87 2/54 31490
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 103964 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1050.04 s]
Raw data (loadavg): 1.02 0.99 0.87 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 104964 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1060.04 s]
Raw data (loadavg): 1.02 0.99 0.87 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 105965 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1070.04 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 106965 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1080.04 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 107965 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1090.05 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 108966 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1100.05 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 109966 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1110.05 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 110967 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21953 0 0 0 111967 69 0 0 25 0 1 0 420342389 91652096 21931 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21931 603 41 0 22335 0
vsize: 89504
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21955 0 0 0 112967 69 0 0 25 0 1 0 420342389 91652096 21933 4294967295 134512640 134672761 3221224576 3221223744 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21933 603 41 0 22335 0
vsize: 89504
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 21956 0 0 0 113968 69 0 0 25 0 1 0 420342389 91652096 21934 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22376 21934 603 41 0 22335 0
vsize: 89504
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 22145 0 0 0 114968 69 0 0 25 0 1 0 420342389 92454912 22123 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22572 22123 603 41 0 22531 0
vsize: 90288
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 22569 0 0 0 115967 71 0 0 25 0 1 0 420342389 94466048 22547 4294967295 134512640 134672761 3221224576 3221223816 134564425 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 22547 603 41 0 23022 0
vsize: 92252
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 22569 0 0 0 116968 71 0 0 25 0 1 0 420342389 94466048 22547 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 22547 603 41 0 23022 0
vsize: 92252
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 22571 0 0 0 117968 71 0 0 25 0 1 0 420342389 94466048 22549 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 22549 603 41 0 23022 0
vsize: 92252
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 22572 0 0 0 118968 71 0 0 25 0 1 0 420342389 94466048 22550 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 22550 603 41 0 23022 0
vsize: 92252
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 31492
Raw data (stat): 31437 (minisat+) R 31436 29653 29652 0 -1 0 22572 0 0 0 119969 71 0 0 25 0 1 0 420342389 94466048 22550 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 22550 603 41 0 23022 0
vsize: 92252
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.88 1/54 31492
Raw data (stat): 31437 (minisat+) Z 31436 29653 29652 0 -1 12 22575 0 0 0 119969 75 0 0 25 0 1 0 420342389 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.45
CPU user time (s): 1199.7
CPU system time (s): 0.754885
CPU usage (%): 100.029
Max. virtual memory (Kb): 92252
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####