PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8b4.opb
MD5SUM	4958e72bfea6f430972589733eb52991
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	654
Optimality of the best value was proved	NO
Number of terms in the objective function	2136
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	2136
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	2136
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.09983
Number of variables	2136
Total number of constraints	9282
Number of constraints which are clauses	9282
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 5898

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 02:13:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4306 boxname=wulflinc21 idbench=170 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4958e72bfea6f430972589733eb52991  /oldhome/oroussel/tmp/wulflinc21/normalized-ii8b4.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc21/normalized-ii8b4.opb /oldhome/oroussel/tmp/wulflinc21/normalized-ii8b4.opb
IDLAUNCH: 4306
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        879288 kB
Buffers:         28104 kB
Cached:         107352 kB
SwapCached:          0 kB
Active:          35128 kB
Inactive:       103232 kB
HighTotal:      131008 kB
HighFree:        20076 kB
LowTotal:       903652 kB
LowFree:        859212 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11492 kB
Committed_AS:    63784 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:33:38 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 4306 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 9282 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9282    20580 |    3094       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 821[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:140426     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |  178080   415014 |   59360       4       37     9.2 |  0.000 % |
c |       104 |  178062   414978 |   65296     103     4574    44.4 |  0.009 % |
c |       254 |  177755   414329 |   71825     242    12039    49.7 |  0.159 % |
c |       479 |  177694   414202 |   79008     465    14387    30.9 |  0.188 % |
c |       816 |  177434   413644 |   86908     797    33082    41.5 |  0.319 % |
c |      1322 |  176974   412642 |   95599    1293    60806    47.0 |  0.556 % |
c ==============================================================================
c [1mFound solution: 659[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1802 |  178678   416908 |   59559    1770    71517    40.4 |  0.556 % |
c |      1903 |  178678   416908 |   65514    1871    91612    49.0 |  0.654 % |
c |      2053 |  178191   415821 |   72066    2002   103329    51.6 |  0.914 % |
c |      2278 |  177590   414488 |   79273    2218   113897    51.4 |  1.232 % |
c |      2618 |  177556   414418 |   87200    2556   117567    46.0 |  1.248 % |
c |      3124 |  176020   411036 |   95920    3025   152459    50.4 |  2.049 % |
c |      3883 |  175586   410096 |  105512    3774   219312    58.1 |  2.265 % |
c |      5022 |  175227   409309 |  116063    4896   378682    77.3 |  2.450 % |
c |      6730 |  174873   408537 |  127670    6586   625551    95.0 |  2.631 % |
c |      9292 |  174873   408537 |  140437    9148   786933    86.0 |  2.631 % |
c |     13138 |  174792   408366 |  154480   12985   955164    73.6 |  2.670 % |
c |     18904 |  174176   407046 |  169928   18612  1450994    78.0 |  2.970 % |
c |     27554 |  173555   405677 |  186921   27005  2253639    83.5 |  3.292 % |
c |     40533 |  173447   405435 |  205613   39966  3844481    96.2 |  3.350 % |
c ==============================================================================
c [1mFound solution: 654[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55853 |  173510   405642 |   57836   55077  5513214   100.1 |  3.350 % |
c |     55953 |  173464   405536 |   63619   55157  5521049   100.1 |  3.386 % |
c |     56103 |  173464   405536 |   69981   55307  5543073   100.2 |  3.386 % |
c |     56328 |  173464   405536 |   76979   55532  5550981   100.0 |  3.386 % |
c |     56665 |  173464   405536 |   84677   55869  5603422   100.3 |  3.386 % |
c |     57174 |  173464   405536 |   93145   56378  5617871    99.6 |  3.386 % |
c |     57933 |  173464   405536 |  102460   57137  5684990    99.5 |  3.386 % |
c |     59076 |  173464   405536 |  112706   58280  5787844    99.3 |  3.386 % |
c |     60784 |  173464   405536 |  123976   59988  6054675   100.9 |  3.386 % |
c |     63346 |  173464   405536 |  136374   62550  6653964   106.4 |  3.386 % |
c |     67190 |  173464   405536 |  150011   66394  7114027   107.1 |  3.386 % |
c |     72958 |  173464   405536 |  165012   72162  8258887   114.4 |  3.386 % |
c |     81612 |  173464   405536 |  181514   80816  9846446   121.8 |  3.386 % |
c |     94586 |  173464   405536 |  199665   93790 12124232   129.3 |  3.386 % |
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 -x1919 x1920 -x1921 -x1922 x1923 -x1924 -x1925 -x1926 -x1927 x1928 -x1929 -x1930 -x1931 -x1932 x1933 -x1934 -x1935 x1936 -x1937 x1938 -x1939 -x1940 -x1941 x1942 -x1943 x1944 -x1945 x1946 -x1947 -x1948 x1949 -x1950 -x1951 x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 x1970 -x1971 -x1972 -x1973 -x1974 x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 -x1983 -x1984 x1985 -x1986 -x1987 x1988 -x1989 -x1990 -x1991 -x1992 x1993 -x1994 -x1995 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/55 3544
Raw data (stat): 3544 (runsolver) R 3543 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 358166622 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 8909 0 0 0 977 22 0 0 25 0 1 0 358166622 40550400 8578 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9900 8578 603 41 0 9859 0
vsize: 39600
[startup+20.0013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 8972 0 0 0 1977 22 0 0 25 0 1 0 358166622 40833024 8641 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9969 8641 603 41 0 9928 0
vsize: 39876
[startup+30.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 9288 0 0 0 2976 23 0 0 25 0 1 0 358166622 42618880 8946 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10405 8946 603 41 0 10364 0
vsize: 41620
[startup+40.0008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 9378 0 0 0 3975 24 0 0 25 0 1 0 358166622 43020288 9036 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9036 603 41 0 10462 0
vsize: 42012
[startup+50.0014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 9543 0 0 0 4975 25 0 0 25 0 1 0 358166622 43700224 9201 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10669 9201 603 41 0 10628 0
vsize: 42676
[startup+60.0025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 9736 0 0 0 5974 25 0 0 25 0 1 0 358166622 44498944 9394 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10864 9394 603 41 0 10823 0
vsize: 43456
[startup+70.0028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 9860 0 0 0 6974 26 0 0 25 0 1 0 358166622 44892160 9518 4294967295 134512640 134672761 3221224560 3221223744 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10960 9518 603 41 0 10919 0
vsize: 43840
[startup+80.0025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 10003 0 0 0 7973 26 0 0 25 0 1 0 358166622 45559808 9661 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11123 9661 603 41 0 11082 0
vsize: 44492
[startup+90.0032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 10093 0 0 0 8973 26 0 0 25 0 1 0 358166622 45957120 9751 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11220 9751 603 41 0 11179 0
vsize: 44880
[startup+100.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 10250 0 0 0 9973 27 0 0 25 0 1 0 358166622 46608384 9908 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11379 9908 603 41 0 11338 0
vsize: 45516
[startup+110.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 10355 0 0 0 10973 27 0 0 25 0 1 0 358166622 46981120 10013 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11470 10013 603 41 0 11429 0
vsize: 45880
[startup+120.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 10458 0 0 0 11973 27 0 0 25 0 1 0 358166622 47386624 10116 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11569 10116 603 41 0 11528 0
vsize: 46276
[startup+130.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 10581 0 0 0 12972 28 0 0 25 0 1 0 358166622 47915008 10239 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11698 10239 603 41 0 11657 0
vsize: 46792
[startup+140.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 10719 0 0 0 13972 28 0 0 25 0 1 0 358166622 48574464 10377 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11859 10377 603 41 0 11818 0
vsize: 47436
[startup+150.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 10810 0 0 0 14972 28 0 0 25 0 1 0 358166622 48955392 10468 4294967295 134512640 134672761 3221224560 3221223760 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11952 10468 603 41 0 11911 0
vsize: 47808
[startup+160.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 10949 0 0 0 15972 29 0 0 25 0 1 0 358166622 49467392 10607 4294967295 134512640 134672761 3221224560 3221223664 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12077 10607 603 41 0 12036 0
vsize: 48308
[startup+170.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 11063 0 0 0 16971 30 0 0 25 0 1 0 358166622 49860608 10721 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12173 10721 603 41 0 12132 0
vsize: 48692
[startup+180.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 11168 0 0 0 17971 30 0 0 25 0 1 0 358166622 50397184 10826 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12304 10826 603 41 0 12263 0
vsize: 49216
[startup+190.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 11283 0 0 0 18971 30 0 0 25 0 1 0 358166622 50794496 10941 4294967295 134512640 134672761 3221224560 3221223744 134558497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12401 10941 603 41 0 12360 0
vsize: 49604
[startup+200.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 11399 0 0 0 19971 31 0 0 25 0 1 0 358166622 51326976 11057 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12531 11057 603 41 0 12490 0
vsize: 50124
[startup+210.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 11440 0 0 0 20970 31 0 0 25 0 1 0 358166622 51458048 11098 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12563 11098 603 41 0 12522 0
vsize: 50252
[startup+220.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 11563 0 0 0 21970 32 0 0 25 0 1 0 358166622 51965952 11221 4294967295 134512640 134672761 3221224560 3221223664 134560313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12687 11221 603 41 0 12646 0
vsize: 50748
[startup+230.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 11644 0 0 0 22969 32 0 0 25 0 1 0 358166622 52232192 11302 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12752 11302 603 41 0 12711 0
vsize: 51008
[startup+240.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 11796 0 0 0 23969 33 0 0 25 0 1 0 358166622 52895744 11454 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12914 11454 603 41 0 12873 0
vsize: 51656
[startup+250.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 11908 0 0 0 24968 33 0 0 25 0 1 0 358166622 53297152 11566 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13012 11566 603 41 0 12971 0
vsize: 52048
[startup+260.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 12091 0 0 0 25968 34 0 0 25 0 1 0 358166622 54071296 11749 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13201 11749 603 41 0 13160 0
vsize: 52804
[startup+270.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 12259 0 0 0 26967 35 0 0 25 0 1 0 358166622 54734848 11917 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13363 11917 603 41 0 13322 0
vsize: 53452
[startup+280.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 12388 0 0 0 27967 35 0 0 25 0 1 0 358166622 55250944 12046 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13489 12046 603 41 0 13448 0
vsize: 53956
[startup+290.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 12510 0 0 0 28966 36 0 0 25 0 1 0 358166622 55902208 12168 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13648 12168 603 41 0 13607 0
vsize: 54592
[startup+300.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 12627 0 0 0 29966 36 0 0 25 0 1 0 358166622 56434688 12285 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13778 12285 603 41 0 13737 0
vsize: 55112
[startup+310.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 12763 0 0 0 30966 37 0 0 25 0 1 0 358166622 56942592 12421 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13902 12421 603 41 0 13861 0
vsize: 55608
[startup+320.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 12910 0 0 0 31965 37 0 0 25 0 1 0 358166622 57597952 12568 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14062 12568 603 41 0 14021 0
vsize: 56248
[startup+330.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 12990 0 0 0 32965 38 0 0 25 0 1 0 358166622 57868288 12648 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14128 12648 603 41 0 14087 0
vsize: 56512
[startup+340.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 13122 0 0 0 33965 38 0 0 25 0 1 0 358166622 58396672 12780 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 12780 603 41 0 14216 0
vsize: 57028
[startup+350.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 13215 0 0 0 34964 39 0 0 25 0 1 0 358166622 58793984 12873 4294967295 134512640 134672761 3221224560 3221223760 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14354 12873 603 41 0 14313 0
vsize: 57416
[startup+360.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 13306 0 0 0 35964 39 0 0 25 0 1 0 358166622 59183104 12964 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14449 12964 603 41 0 14408 0
vsize: 57796
[startup+370.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 13380 0 0 0 36963 40 0 0 25 0 1 0 358166622 59449344 13038 4294967295 134512640 134672761 3221224560 3221223664 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14514 13038 603 41 0 14473 0
vsize: 58056
[startup+380.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 13458 0 0 0 37963 40 0 0 25 0 1 0 358166622 59834368 13116 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14608 13116 603 41 0 14567 0
vsize: 58432
[startup+390.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 13524 0 0 0 38963 40 0 0 25 0 1 0 358166622 60104704 13182 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14674 13182 603 41 0 14633 0
vsize: 58696
[startup+400.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 13592 0 0 0 39963 41 0 0 25 0 1 0 358166622 60342272 13250 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14732 13250 603 41 0 14691 0
vsize: 58928
[startup+410.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 13670 0 0 0 40963 41 0 0 25 0 1 0 358166622 60600320 13328 4294967295 134512640 134672761 3221224560 3221223664 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14795 13328 603 41 0 14754 0
vsize: 59180
[startup+420.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 13757 0 0 0 41962 41 0 0 25 0 1 0 358166622 60989440 13415 4294967295 134512640 134672761 3221224560 3221223684 134566120 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 13415 603 41 0 14849 0
vsize: 59560
[startup+430.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 13841 0 0 0 42962 42 0 0 25 0 1 0 358166622 61390848 13499 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 13499 603 41 0 14947 0
vsize: 59952
[startup+440.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 13927 0 0 0 43963 42 0 0 25 0 1 0 358166622 61652992 13585 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15052 13585 603 41 0 15011 0
vsize: 60208
[startup+450.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 14020 0 0 0 44962 42 0 0 25 0 1 0 358166622 62050304 13678 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15149 13678 603 41 0 15108 0
vsize: 60596
[startup+460.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 14107 0 0 0 45962 42 0 0 25 0 1 0 358166622 62431232 13765 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15242 13765 603 41 0 15201 0
vsize: 60968
[startup+470.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 14194 0 0 0 46962 43 0 0 25 0 1 0 358166622 62816256 13852 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15336 13852 603 41 0 15295 0
vsize: 61344
[startup+480.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 14259 0 0 0 47961 43 0 0 25 0 1 0 358166622 63053824 13917 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15394 13917 603 41 0 15353 0
vsize: 61576
[startup+490.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 14322 0 0 0 48961 44 0 0 25 0 1 0 358166622 63303680 13980 4294967295 134512640 134672761 3221224560 3221223696 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15455 13980 603 41 0 15414 0
vsize: 61820
[startup+500.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 14397 0 0 0 49961 44 0 0 25 0 1 0 358166622 63565824 14055 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15519 14055 603 41 0 15478 0
vsize: 62076
[startup+510.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 14495 0 0 0 50961 44 0 0 25 0 1 0 358166622 63967232 14153 4294967295 134512640 134672761 3221224560 3221223684 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15617 14153 603 41 0 15576 0
vsize: 62468
[startup+520.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 14608 0 0 0 51960 45 0 0 25 0 1 0 358166622 64479232 14266 4294967295 134512640 134672761 3221224560 3221223728 134559675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15742 14266 603 41 0 15701 0
vsize: 62968
[startup+530.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 14716 0 0 0 52959 46 0 0 25 0 1 0 358166622 64843776 14374 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15831 14374 603 41 0 15790 0
vsize: 63324
[startup+540.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 14843 0 0 0 53959 46 0 0 25 0 1 0 358166622 65359872 14501 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15957 14501 603 41 0 15916 0
vsize: 63828
[startup+550.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 15010 0 0 0 54959 47 0 0 25 0 1 0 358166622 66027520 14668 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16120 14668 603 41 0 16079 0
vsize: 64480
[startup+560.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 15190 0 0 0 55957 48 0 0 25 0 1 0 358166622 66678784 14832 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16279 14832 603 41 0 16238 0
vsize: 65116
[startup+570.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 15251 0 0 0 56957 49 0 0 25 0 1 0 358166622 66945024 14893 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16344 14893 603 41 0 16303 0
vsize: 65376
[startup+580.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 15339 0 0 0 57957 49 0 0 25 0 1 0 358166622 67346432 14981 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16442 14981 603 41 0 16401 0
vsize: 65768
[startup+590.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 15440 0 0 0 58956 50 0 0 25 0 1 0 358166622 67743744 15082 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16539 15082 603 41 0 16498 0
vsize: 66156
[startup+600.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 15566 0 0 0 59956 50 0 0 25 0 1 0 358166622 68308992 15208 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16677 15208 603 41 0 16636 0
vsize: 66708
[startup+610.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 15704 0 0 0 60956 50 0 0 25 0 1 0 358166622 68845568 15346 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16808 15346 603 41 0 16767 0
vsize: 67232
[startup+620.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 15793 0 0 0 61955 51 0 0 25 0 1 0 358166622 69242880 15435 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16905 15435 603 41 0 16864 0
vsize: 67620
[startup+630.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 15926 0 0 0 62955 51 0 0 25 0 1 0 358166622 69779456 15568 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17036 15568 603 41 0 16995 0
vsize: 68144
[startup+640.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 16115 0 0 0 63954 52 0 0 25 0 1 0 358166622 70574080 15757 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17230 15757 603 41 0 17189 0
vsize: 68920
[startup+650.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 16317 0 0 0 64954 52 0 0 25 0 1 0 358166622 71385088 15959 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17428 15959 603 41 0 17387 0
vsize: 69712
[startup+660.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 16439 0 0 0 65953 53 0 0 25 0 1 0 358166622 71905280 16081 4294967295 134512640 134672761 3221224560 3221223664 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17555 16081 603 41 0 17514 0
vsize: 70220
[startup+670.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 16555 0 0 0 66953 54 0 0 25 0 1 0 358166622 72286208 16197 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17648 16197 603 41 0 17607 0
vsize: 70592
[startup+680.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 16671 0 0 0 67953 54 0 0 25 0 1 0 358166622 72826880 16313 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17780 16313 603 41 0 17739 0
vsize: 71120
[startup+690.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 16827 0 0 0 68952 55 0 0 25 0 1 0 358166622 73719808 16469 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17998 16469 603 41 0 17957 0
vsize: 71992
[startup+700.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 16943 0 0 0 69952 55 0 0 25 0 1 0 358166622 74117120 16585 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 16585 603 41 0 18054 0
vsize: 72380
[startup+710.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 17138 0 0 0 70952 55 0 0 25 0 1 0 358166622 74919936 16780 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18291 16780 603 41 0 18250 0
vsize: 73164
[startup+720.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 17334 0 0 0 71950 57 0 0 25 0 1 0 358166622 75722752 16976 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18487 16976 603 41 0 18446 0
vsize: 73948
[startup+730.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 17425 0 0 0 72950 57 0 0 25 0 1 0 358166622 76124160 17067 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18585 17067 603 41 0 18544 0
vsize: 74340
[startup+740.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 17485 0 0 0 73950 57 0 0 25 0 1 0 358166622 76382208 17127 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18648 17127 603 41 0 18607 0
vsize: 74592
[startup+750.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 17595 0 0 0 74950 58 0 0 25 0 1 0 358166622 76779520 17237 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18745 17237 603 41 0 18704 0
vsize: 74980
[startup+760.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 17659 0 0 0 75949 58 0 0 25 0 1 0 358166622 77045760 17301 4294967295 134512640 134672761 3221224560 3221223664 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18810 17301 603 41 0 18769 0
vsize: 75240
[startup+770.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 17770 0 0 0 76949 58 0 0 25 0 1 0 358166622 77586432 17412 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18942 17412 603 41 0 18901 0
vsize: 75768
[startup+780.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 17897 0 0 0 77949 59 0 0 25 0 1 0 358166622 77991936 17539 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19041 17539 603 41 0 19000 0
vsize: 76164
[startup+790.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18018 0 0 0 78949 59 0 0 25 0 1 0 358166622 78508032 17660 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19167 17660 603 41 0 19126 0
vsize: 76668
[startup+800.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18101 0 0 0 79949 59 0 0 25 0 1 0 358166622 78901248 17743 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19263 17743 603 41 0 19222 0
vsize: 77052
[startup+810.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18183 0 0 0 80949 59 0 0 25 0 1 0 358166622 79171584 17825 4294967295 134512640 134672761 3221224560 3221223664 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19329 17825 603 41 0 19288 0
vsize: 77316
[startup+820.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18257 0 0 0 81948 60 0 0 25 0 1 0 358166622 79572992 17899 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19427 17899 603 41 0 19386 0
vsize: 77708
[startup+830.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18307 0 0 0 82948 60 0 0 25 0 1 0 358166622 79704064 17949 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19459 17949 603 41 0 19418 0
vsize: 77836
[startup+840.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18374 0 0 0 83948 61 0 0 25 0 1 0 358166622 79970304 18016 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19524 18016 603 41 0 19483 0
vsize: 78096
[startup+850.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18441 0 0 0 84948 61 0 0 25 0 1 0 358166622 80232448 18083 4294967295 134512640 134672761 3221224560 3221223664 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19588 18083 603 41 0 19547 0
vsize: 78352
[startup+860.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18512 0 0 0 85948 61 0 0 25 0 1 0 358166622 80633856 18154 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19686 18154 603 41 0 19645 0
vsize: 78744
[startup+870.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18588 0 0 0 86947 62 0 0 25 0 1 0 358166622 80900096 18230 4294967295 134512640 134672761 3221224560 3221223664 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19751 18230 603 41 0 19710 0
vsize: 79004
[startup+880.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18682 0 0 0 87947 62 0 0 25 0 1 0 358166622 81285120 18324 4294967295 134512640 134672761 3221224560 3221223616 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19845 18324 603 41 0 19804 0
vsize: 79380
[startup+890.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18793 0 0 0 88946 63 0 0 25 0 1 0 358166622 81678336 18435 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19941 18435 603 41 0 19900 0
vsize: 79764
[startup+900.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 18906 0 0 0 89946 63 0 0 25 0 1 0 358166622 82202624 18548 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20069 18548 603 41 0 20028 0
vsize: 80276
[startup+910.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 19003 0 0 0 90946 63 0 0 25 0 1 0 358166622 82599936 18645 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20166 18645 603 41 0 20125 0
vsize: 80664
[startup+920.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 19091 0 0 0 91946 63 0 0 25 0 1 0 358166622 82862080 18733 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20230 18733 603 41 0 20189 0
vsize: 80920
[startup+930.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 19174 0 0 0 92947 63 0 0 25 0 1 0 358166622 83263488 18816 4294967295 134512640 134672761 3221224560 3221223664 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20328 18816 603 41 0 20287 0
vsize: 81312
[startup+940.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 19251 0 0 0 93946 64 0 0 25 0 1 0 358166622 83529728 18893 4294967295 134512640 134672761 3221224560 3221223664 134559976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20393 18893 603 41 0 20352 0
vsize: 81572
[startup+950.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 19343 0 0 0 94946 64 0 0 25 0 1 0 358166622 83918848 18985 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20488 18985 603 41 0 20447 0
vsize: 81952
[startup+960.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 19412 0 0 0 95946 64 0 0 25 0 1 0 358166622 84176896 19054 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20551 19054 603 41 0 20510 0
vsize: 82204
[startup+970.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 19496 0 0 0 96945 65 0 0 25 0 1 0 358166622 84570112 19138 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20647 19138 603 41 0 20606 0
vsize: 82588
[startup+980.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 19600 0 0 0 97945 65 0 0 25 0 1 0 358166622 84951040 19242 4294967295 134512640 134672761 3221224560 3221223664 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20740 19242 603 41 0 20699 0
vsize: 82960
[startup+990.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 19695 0 0 0 98945 65 0 0 25 0 1 0 358166622 85331968 19337 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20833 19337 603 41 0 20792 0
vsize: 83332
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 19821 0 0 0 99945 65 0 0 25 0 1 0 358166622 85852160 19463 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20960 19463 603 41 0 20919 0
vsize: 83840
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 19926 0 0 0 100945 66 0 0 25 0 1 0 358166622 86380544 19568 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21089 19568 603 41 0 21048 0
vsize: 84356
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 20033 0 0 0 101945 66 0 0 25 0 1 0 358166622 86781952 19675 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21187 19675 603 41 0 21146 0
vsize: 84748
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 20130 0 0 0 102944 67 0 0 25 0 1 0 358166622 87183360 19772 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21285 19772 603 41 0 21244 0
vsize: 85140
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 20249 0 0 0 103944 67 0 0 25 0 1 0 358166622 87572480 19891 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21380 19891 603 41 0 21339 0
vsize: 85520
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 20358 0 0 0 104944 68 0 0 25 0 1 0 358166622 88092672 20000 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21507 20000 603 41 0 21466 0
vsize: 86028
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 20455 0 0 0 105944 68 0 0 25 0 1 0 358166622 88485888 20097 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21603 20097 603 41 0 21562 0
vsize: 86412
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 20573 0 0 0 106944 68 0 0 25 0 1 0 358166622 89001984 20215 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21729 20215 603 41 0 21688 0
vsize: 86916
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 20671 0 0 0 107943 68 0 0 25 0 1 0 358166622 89391104 20313 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21824 20313 603 41 0 21783 0
vsize: 87296
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 20773 0 0 0 108943 69 0 0 25 0 1 0 358166622 89784320 20415 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21920 20415 603 41 0 21879 0
vsize: 87680
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 20932 0 0 0 109943 69 0 0 25 0 1 0 358166622 90456064 20574 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22084 20574 603 41 0 22043 0
vsize: 88336
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 21070 0 0 0 110943 69 0 0 25 0 1 0 358166622 90992640 20712 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22215 20712 603 41 0 22174 0
vsize: 88860
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 21152 0 0 0 111942 70 0 0 25 0 1 0 358166622 91258880 20794 4294967295 134512640 134672761 3221224560 3221223664 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22280 20794 603 41 0 22239 0
vsize: 89120
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 21338 0 0 0 112942 70 0 0 25 0 1 0 358166622 92061696 20980 4294967295 134512640 134672761 3221224560 3221223664 134560408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22476 20980 603 41 0 22435 0
vsize: 89904
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 21505 0 0 0 113942 71 0 0 25 0 1 0 358166622 92717056 21147 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22636 21147 603 41 0 22595 0
vsize: 90544
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 21642 0 0 0 114942 71 0 0 25 0 1 0 358166622 93380608 21284 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22798 21284 603 41 0 22757 0
vsize: 91192
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 21796 0 0 0 115942 71 0 0 25 0 1 0 358166622 93904896 21438 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22926 21438 603 41 0 22885 0
vsize: 91704
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 21933 0 0 0 116942 71 0 0 25 0 1 0 358166622 94437376 21575 4294967295 134512640 134672761 3221224560 3221223744 134559033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23056 21575 603 41 0 23015 0
vsize: 92224
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 21998 0 0 0 117942 72 0 0 25 0 1 0 358166622 94703616 21640 4294967295 134512640 134672761 3221224560 3221223664 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23121 21640 603 41 0 23080 0
vsize: 92484
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 22117 0 0 0 118941 72 0 0 25 0 1 0 358166622 95232000 21759 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23250 21759 603 41 0 23209 0
vsize: 93000
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 3544
Raw data (stat): 3544 (minisat+) R 3543 30927 30926 0 -1 0 22243 0 0 0 119941 73 0 0 25 0 1 0 358166622 95768576 21885 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23381 21885 603 41 0 23340 0
vsize: 93524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.97 0.91 1/55 3544
Raw data (stat): 3544 (minisat+) Z 3543 30927 30926 0 -1 12 22246 0 0 0 119941 77 0 0 25 0 1 0 358166622 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.06
CPU time (s): 1200.19
CPU user time (s): 1199.41
CPU system time (s): 0.771882
CPU usage (%): 100.01
Max. virtual memory (Kb): 93524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####