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 4836

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-13 20:29:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=599 boxname=wulflinc12 idbench=67 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  ebc55cfc194a279163f52418008eccf2  /oldhome/oroussel/tmp/wulflinc12/normalized-ex5.pi.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc12/normalized-ex5.pi.opb
IDLAUNCH: 599
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        920960 kB
Buffers:         34628 kB
Cached:          59944 kB
SwapCached:         16 kB
Active:          58920 kB
Inactive:        38528 kB
HighTotal:      131008 kB
HighFree:        67144 kB
LowTotal:       903652 kB
LowFree:        853816 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10912 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:49:47 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 599 7 1200.15 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.92 0.97 0.90 2/54 27836
Raw data (stat): 27836 (runsolver) R 27835 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420615607 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0006 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 3465 0 0 0 988 9 0 0 25 0 1 0 420615607 15929344 3195 4294967295 134512640 134672761 3221224640 3221223776 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3889 3195 603 41 0 3848 0
vsize: 15556
[startup+20.0019 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 4911 0 0 0 1984 13 0 0 25 0 1 0 420615607 21856256 4641 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5336 4641 603 41 0 5295 0
vsize: 21344
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 6126 0 0 0 2981 16 0 0 25 0 1 0 420615607 26923008 5856 4294967295 134512640 134672761 3221224640 3221223744 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6573 5856 603 41 0 6532 0
vsize: 26292
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 7253 0 0 0 3978 19 0 0 25 0 1 0 420615607 31514624 6983 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7694 6983 603 41 0 7653 0
vsize: 30776
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 8334 0 0 0 4976 22 0 0 25 0 1 0 420615607 35938304 8064 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8774 8064 603 41 0 8733 0
vsize: 35096
[startup+60.0037 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 9402 0 0 0 5973 25 0 0 25 0 1 0 420615607 40493056 9132 4294967295 134512640 134672761 3221224640 3221223744 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9886 9132 603 41 0 9845 0
vsize: 39544
[startup+70.0036 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 10247 0 0 0 6971 27 0 0 25 0 1 0 420615607 43855872 9977 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10707 9977 603 41 0 10666 0
vsize: 42828
[startup+80.0049 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 10948 0 0 0 7969 29 0 0 25 0 1 0 420615607 46804992 10678 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11427 10678 603 41 0 11386 0
vsize: 45708
[startup+90.0047 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 10948 0 0 0 8968 29 0 0 25 0 1 0 420615607 46804992 10678 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11427 10678 603 41 0 11386 0
vsize: 45708
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 10948 0 0 0 9968 29 0 0 25 0 1 0 420615607 46804992 10678 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11427 10678 603 41 0 11386 0
vsize: 45708
[startup+110.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 10948 0 0 0 10967 30 0 0 25 0 1 0 420615607 46804992 10678 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11427 10678 603 41 0 11386 0
vsize: 45708
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 11282 0 0 0 11967 30 0 0 25 0 1 0 420615607 48156672 11012 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11757 11012 603 41 0 11716 0
vsize: 47028
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 12215 0 0 0 12963 34 0 0 25 0 1 0 420615607 51924992 11945 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12677 11945 603 41 0 12636 0
vsize: 50708
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 12913 0 0 0 13961 35 0 0 25 0 1 0 420615607 54743040 12643 4294967295 134512640 134672761 3221224640 3221223596 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13365 12643 603 41 0 13324 0
vsize: 53460
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 12913 0 0 0 14961 36 0 0 25 0 1 0 420615607 54743040 12643 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13365 12643 603 41 0 13324 0
vsize: 53460
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 12913 0 0 0 15960 36 0 0 25 0 1 0 420615607 54743040 12643 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13365 12643 603 41 0 13324 0
vsize: 53460
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 12913 0 0 0 16960 37 0 0 25 0 1 0 420615607 54743040 12643 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13365 12643 603 41 0 13324 0
vsize: 53460
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 12913 0 0 0 17960 37 0 0 25 0 1 0 420615607 54743040 12643 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13365 12643 603 41 0 13324 0
vsize: 53460
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 12913 0 0 0 18960 37 0 0 25 0 1 0 420615607 54743040 12643 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13365 12643 603 41 0 13324 0
vsize: 53460
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 12913 0 0 0 19959 37 0 0 25 0 1 0 420615607 54743040 12643 4294967295 134512640 134672761 3221224640 3221223744 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13365 12643 603 41 0 13324 0
vsize: 53460
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 12913 0 0 0 20959 37 0 0 25 0 1 0 420615607 54743040 12643 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13365 12643 603 41 0 13324 0
vsize: 53460
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 12913 0 0 0 21959 38 0 0 25 0 1 0 420615607 54743040 12643 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13365 12643 603 41 0 13324 0
vsize: 53460
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 13271 0 0 0 22958 39 0 0 25 0 1 0 420615607 56209408 13001 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13723 13001 603 41 0 13682 0
vsize: 54892
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 13894 0 0 0 23956 41 0 0 25 0 1 0 420615607 58757120 13624 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14345 13624 603 41 0 14304 0
vsize: 57380
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 14572 0 0 0 24954 43 0 0 25 0 1 0 420615607 61579264 14302 4294967295 134512640 134672761 3221224640 3221223764 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15034 14302 603 41 0 14993 0
vsize: 60136
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15341 0 0 0 25951 45 0 0 25 0 1 0 420615607 64667648 15071 4294967295 134512640 134672761 3221224640 3221223808 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15788 15071 603 41 0 15747 0
vsize: 63152
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15739 0 0 0 26950 46 0 0 25 0 1 0 420615607 66289664 15469 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16184 15469 603 41 0 16143 0
vsize: 64736
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15739 0 0 0 27950 47 0 0 25 0 1 0 420615607 66289664 15469 4294967295 134512640 134672761 3221224640 3221223808 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16184 15469 603 41 0 16143 0
vsize: 64736
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15739 0 0 0 28949 47 0 0 25 0 1 0 420615607 66289664 15469 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16184 15469 603 41 0 16143 0
vsize: 64736
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15739 0 0 0 29949 48 0 0 25 0 1 0 420615607 66289664 15469 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16184 15469 603 41 0 16143 0
vsize: 64736
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15739 0 0 0 30948 48 0 0 25 0 1 0 420615607 66289664 15469 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16184 15469 603 41 0 16143 0
vsize: 64736
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15739 0 0 0 31948 49 0 0 25 0 1 0 420615607 66289664 15469 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16184 15469 603 41 0 16143 0
vsize: 64736
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15739 0 0 0 32948 49 0 0 25 0 1 0 420615607 66289664 15469 4294967295 134512640 134672761 3221224640 3221223808 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16184 15469 603 41 0 16143 0
vsize: 64736
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15739 0 0 0 33947 49 0 0 25 0 1 0 420615607 66289664 15469 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16184 15469 603 41 0 16143 0
vsize: 64736
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15739 0 0 0 34947 50 0 0 25 0 1 0 420615607 66289664 15469 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16184 15469 603 41 0 16143 0
vsize: 64736
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15739 0 0 0 35947 50 0 0 25 0 1 0 420615607 66289664 15469 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16184 15469 603 41 0 16143 0
vsize: 64736
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15739 0 0 0 36947 50 0 0 25 0 1 0 420615607 66289664 15469 4294967295 134512640 134672761 3221224640 3221223744 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16184 15469 603 41 0 16143 0
vsize: 64736
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 15999 0 0 0 37946 51 0 0 25 0 1 0 420615607 67371008 15729 4294967295 134512640 134672761 3221224640 3221223808 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16448 15729 603 41 0 16407 0
vsize: 65792
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 16621 0 0 0 38944 53 0 0 25 0 1 0 420615607 69935104 16351 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17074 16351 603 41 0 17033 0
vsize: 68296
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 17452 0 0 0 39942 55 0 0 25 0 1 0 420615607 73428992 17182 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17927 17182 603 41 0 17886 0
vsize: 71708
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18094 0 0 0 40940 57 0 0 25 0 1 0 420615607 75968512 17824 4294967295 134512640 134672761 3221224640 3221223776 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18547 17824 603 41 0 18506 0
vsize: 74188
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18688 0 0 0 41938 59 0 0 25 0 1 0 420615607 78389248 18418 4294967295 134512640 134672761 3221224640 3221223824 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19138 18418 603 41 0 19097 0
vsize: 76552
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 42938 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223744 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 43938 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 44938 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 45939 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 46939 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223824 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 47939 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 48939 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 49939 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 50939 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 51939 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 52940 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 53940 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 54940 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 55940 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18742 0 0 0 56940 59 0 0 25 0 1 0 420615607 78659584 18472 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19204 18472 603 41 0 19163 0
vsize: 76816
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 18943 0 0 0 57940 60 0 0 25 0 1 0 420615607 79458304 18673 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19399 18673 603 41 0 19358 0
vsize: 77596
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19454 0 0 0 58938 62 0 0 25 0 1 0 420615607 81580032 19184 4294967295 134512640 134672761 3221224640 3221223744 134559771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19917 19184 603 41 0 19876 0
vsize: 79668
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19914 0 0 0 59938 63 0 0 25 0 1 0 420615607 83451904 19644 4294967295 134512640 134672761 3221224640 3221223744 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19644 603 41 0 20333 0
vsize: 81496
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19914 0 0 0 60938 63 0 0 25 0 1 0 420615607 83451904 19644 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19644 603 41 0 20333 0
vsize: 81496
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19914 0 0 0 61938 63 0 0 25 0 1 0 420615607 83451904 19644 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19644 603 41 0 20333 0
vsize: 81496
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19914 0 0 0 62938 63 0 0 25 0 1 0 420615607 83451904 19644 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19644 603 41 0 20333 0
vsize: 81496
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19914 0 0 0 63938 63 0 0 25 0 1 0 420615607 83451904 19644 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19644 603 41 0 20333 0
vsize: 81496
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19914 0 0 0 64939 63 0 0 25 0 1 0 420615607 83451904 19644 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19644 603 41 0 20333 0
vsize: 81496
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19914 0 0 0 65939 63 0 0 25 0 1 0 420615607 83451904 19644 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19644 603 41 0 20333 0
vsize: 81496
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19915 0 0 0 66939 63 0 0 25 0 1 0 420615607 83451904 19645 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19645 603 41 0 20333 0
vsize: 81496
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19915 0 0 0 67939 63 0 0 25 0 1 0 420615607 83451904 19645 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19645 603 41 0 20333 0
vsize: 81496
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19915 0 0 0 68939 63 0 0 25 0 1 0 420615607 83451904 19645 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20374 19645 603 41 0 20333 0
vsize: 81496
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19915 0 0 0 69939 63 0 0 25 0 1 0 420615607 83451904 19645 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20374 19645 603 41 0 20333 0
vsize: 81496
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19915 0 0 0 70937 63 0 0 25 0 1 0 420615607 83451904 19645 4294967295 134512640 134672761 3221224640 3221223824 134558901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19645 603 41 0 20333 0
vsize: 81496
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19915 0 0 0 71938 63 0 0 25 0 1 0 420615607 83451904 19645 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19645 603 41 0 20333 0
vsize: 81496
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19915 0 0 0 72938 63 0 0 25 0 1 0 420615607 83451904 19645 4294967295 134512640 134672761 3221224640 3221223808 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19645 603 41 0 20333 0
vsize: 81496
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19915 0 0 0 73938 63 0 0 25 0 1 0 420615607 83451904 19645 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19645 603 41 0 20333 0
vsize: 81496
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19915 0 0 0 74938 63 0 0 25 0 1 0 420615607 83451904 19645 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19645 603 41 0 20333 0
vsize: 81496
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 19916 0 0 0 75938 63 0 0 25 0 1 0 420615607 83451904 19646 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20374 19646 603 41 0 20333 0
vsize: 81496
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 20264 0 0 0 76937 64 0 0 25 0 1 0 420615607 84922368 19994 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20733 19994 603 41 0 20692 0
vsize: 82932
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 20856 0 0 0 77936 66 0 0 25 0 1 0 420615607 87330816 20586 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21321 20586 603 41 0 21280 0
vsize: 85284
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21375 0 0 0 78935 67 0 0 25 0 1 0 420615607 89464832 21105 4294967295 134512640 134672761 3221224640 3221223808 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21842 21105 603 41 0 21801 0
vsize: 87368
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21733 0 0 0 79934 68 0 0 25 0 1 0 420615607 90804224 21463 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21463 603 41 0 22128 0
vsize: 88676
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21733 0 0 0 80934 68 0 0 25 0 1 0 420615607 90804224 21463 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21463 603 41 0 22128 0
vsize: 88676
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21734 0 0 0 81934 68 0 0 25 0 1 0 420615607 90804224 21464 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21464 603 41 0 22128 0
vsize: 88676
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21734 0 0 0 82934 68 0 0 25 0 1 0 420615607 90804224 21464 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21464 603 41 0 22128 0
vsize: 88676
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21734 0 0 0 83935 68 0 0 25 0 1 0 420615607 90804224 21464 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21464 603 41 0 22128 0
vsize: 88676
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21734 0 0 0 84935 68 0 0 25 0 1 0 420615607 90804224 21464 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21464 603 41 0 22128 0
vsize: 88676
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21735 0 0 0 85935 68 0 0 25 0 1 0 420615607 90804224 21465 4294967295 134512640 134672761 3221224640 3221223808 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21465 603 41 0 22128 0
vsize: 88676
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21735 0 0 0 86935 68 0 0 25 0 1 0 420615607 90804224 21465 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21465 603 41 0 22128 0
vsize: 88676
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21735 0 0 0 87935 68 0 0 25 0 1 0 420615607 90804224 21465 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21465 603 41 0 22128 0
vsize: 88676
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21735 0 0 0 88935 68 0 0 25 0 1 0 420615607 90804224 21465 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21465 603 41 0 22128 0
vsize: 88676
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21735 0 0 0 89936 68 0 0 25 0 1 0 420615607 90804224 21465 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21465 603 41 0 22128 0
vsize: 88676
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21735 0 0 0 90936 68 0 0 25 0 1 0 420615607 90804224 21465 4294967295 134512640 134672761 3221224640 3221223744 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21465 603 41 0 22128 0
vsize: 88676
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21735 0 0 0 91936 68 0 0 25 0 1 0 420615607 90804224 21465 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21465 603 41 0 22128 0
vsize: 88676
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21735 0 0 0 92936 68 0 0 25 0 1 0 420615607 90804224 21465 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21465 603 41 0 22128 0
vsize: 88676
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 21735 0 0 0 93936 68 0 0 25 0 1 0 420615607 90804224 21465 4294967295 134512640 134672761 3221224640 3221223808 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21465 603 41 0 22128 0
vsize: 88676
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 22208 0 0 0 94935 69 0 0 25 0 1 0 420615607 92844032 21938 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22667 21938 603 41 0 22626 0
vsize: 90668
[startup+960.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 22905 0 0 0 95934 71 0 0 25 0 1 0 420615607 95703040 22635 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23365 22635 603 41 0 23324 0
vsize: 93460
[startup+970.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23586 0 0 0 96932 73 0 0 25 0 1 0 420615607 98549760 23316 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24060 23316 603 41 0 24019 0
vsize: 96240
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 97932 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+990.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 98932 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 99932 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 100932 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 101933 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 102933 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 103933 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 104933 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 105933 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 106934 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223744 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 107933 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 108933 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 109933 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 110934 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 111934 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23803 0 0 0 112934 73 0 0 25 0 1 0 420615607 99360768 23533 4294967295 134512640 134672761 3221224640 3221223808 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23533 603 41 0 24217 0
vsize: 97032
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23805 0 0 0 113934 73 0 0 25 0 1 0 420615607 99360768 23535 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23535 603 41 0 24217 0
vsize: 97032
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 23806 0 0 0 114934 73 0 0 25 0 1 0 420615607 99360768 23536 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 23536 603 41 0 24217 0
vsize: 97032
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 24021 0 0 0 115934 74 0 0 25 0 1 0 420615607 100311040 23751 4294967295 134512640 134672761 3221224640 3221223808 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24490 23751 603 41 0 24449 0
vsize: 97960
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 24417 0 0 0 116933 75 0 0 25 0 1 0 420615607 102203392 24147 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24952 24147 603 41 0 24911 0
vsize: 99808
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 24417 0 0 0 117933 75 0 0 25 0 1 0 420615607 102203392 24147 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24952 24147 603 41 0 24911 0
vsize: 99808
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 24419 0 0 0 118933 75 0 0 25 0 1 0 420615607 102203392 24149 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24952 24149 603 41 0 24911 0
vsize: 99808
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27836
Raw data (stat): 27836 (minisat+) R 27835 25285 25284 0 -1 0 24420 0 0 0 119933 75 0 0 25 0 1 0 420615607 102203392 24150 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24952 24150 603 41 0 24911 0
vsize: 99808
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27836
Raw data (stat): 27836 (minisat+) Z 27835 25285 25284 0 -1 12 24423 0 0 0 119934 80 0 0 25 0 1 0 420615607 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.15
CPU user time (s): 1199.34
CPU system time (s): 0.804877
CPU usage (%): 100.006
Max. virtual memory (Kb): 99808
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####