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-ii8b3.opb
MD5SUM	b2547f396d5cd0589545f2e597f6c86a
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	507
Optimality of the best value was proved	NO
Number of terms in the objective function	1632
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	1632
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1632
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06684
Number of variables	1632
Total number of constraints	6924
Number of constraints which are clauses	6924
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 4922

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-13 20:51:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1517 boxname=wulflinc9 idbench=169 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  b2547f396d5cd0589545f2e597f6c86a  /oldhome/oroussel/tmp/wulflinc9/normalized-ii8b3.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc9/normalized-ii8b3.opb
IDLAUNCH: 1517
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        913804 kB
Buffers:         33964 kB
Cached:          67064 kB
SwapCached:        564 kB
Active:          49616 kB
Inactive:        54848 kB
HighTotal:      131008 kB
HighFree:        60004 kB
LowTotal:       903652 kB
LowFree:        853800 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10796 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:11:02 (client local time) WITH STATUS 10 IN 1200.13 SECONDS
stats: 1517 7 1200.13 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6924 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 |    6924    15408 |    2308       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 586[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:91716     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |  121217   282312 |   40405       3       28     9.3 |  0.000 % |
c |       103 |  120801   281426 |   44445      93     1041    11.2 |  0.321 % |
c |       253 |  120753   281322 |   48890     242     3271    13.5 |  0.358 % |
c |       478 |  120703   281212 |   53779     466    10920    23.4 |  0.397 % |
c |       815 |  120703   281212 |   59156     803    17213    21.4 |  0.397 % |
c |      1321 |  120614   281023 |   65072    1307    31748    24.3 |  0.461 % |
c |      2080 |  119956   279579 |   71579    2051    44511    21.7 |  0.971 % |
c |      3219 |  119150   277859 |   78737    3173    67508    21.3 |  1.563 % |
c ==============================================================================
c [1mFound solution: 509[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 |      3701 |  119752   279447 |   39917    3655    75185    20.6 |  1.563 % |
c |      3801 |  119640   279205 |   43908    3726    79232    21.3 |  1.640 % |
c |      3951 |  119360   278605 |   48299    3870    88414    22.8 |  1.847 % |
c |      4176 |  118859   277500 |   53129    4051   100147    24.7 |  2.236 % |
c |      4513 |  118781   277334 |   58442    4387   108040    24.6 |  2.293 % |
c |      5019 |  116903   273158 |   64286    4831   173579    35.9 |  3.775 % |
c |      5778 |  116903   273158 |   70715    5590   183627    32.8 |  3.775 % |
c |      6918 |  116798   272937 |   77786    6039   250271    41.4 |  3.850 % |
c |      8626 |  116364   271997 |   85565    7732   370843    48.0 |  4.176 % |
c |     11188 |  116273   271796 |   94122   10173   638203    62.7 |  4.247 % |
c |     15033 |  116213   271666 |  103534   14017  1278354    91.2 |  4.292 % |
c ==============================================================================
c [1mFound solution: 507[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 |     19144 |  116047   271330 |   38682   18107  1738408    96.0 |  4.292 % |
c |     19245 |  116037   271308 |   42550   18191  1743139    95.8 |  4.452 % |
c |     19396 |  115986   271195 |   46805   18338  1745238    95.2 |  4.492 % |
c |     19621 |  115986   271195 |   51485   18563  1748329    94.2 |  4.492 % |
c |     19958 |  115986   271195 |   56634   18900  1753469    92.8 |  4.492 % |
c |     20464 |  115986   271195 |   62297   19406  1778682    91.7 |  4.492 % |
c |     21224 |  115986   271195 |   68527   20166  1858988    92.2 |  4.492 % |
c |     22364 |  115986   271195 |   75380   21306  1990114    93.4 |  4.492 % |
c |     24074 |  115930   271065 |   82918   22997  2136953    92.9 |  4.540 % |
c |     26637 |  115930   271065 |   91210   25560  2214729    86.6 |  4.540 % |
c |     30481 |  115930   271065 |  100331   29404  2316889    78.8 |  4.540 % |
c |     36247 |  115881   270944 |  110364   35151  3720757   105.9 |  4.586 % |
c |     44897 |  115881   270944 |  121400   43801  4784546   109.2 |  4.586 % |
c |     57871 |  115722   270597 |  133540   56529  6181537   109.4 |  4.707 % |
c |     77333 |  115621   270362 |  146894   75941  8317046   109.5 |  4.794 % |
c |    106525 |  115566   270241 |  161584  105132 11356271   108.0 |  4.836 % |
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 -x1#### 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.90 0.95 0.90 2/54 396
Raw data (stat): 396 (runsolver) R 395 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420746157 1052672 99 4294967295 134512640 135381576 3221224544 3221219788 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+9.99963 s]
Raw data (loadavg): 0.92 0.95 0.90 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 6412 0 0 0 984 14 0 0 25 0 1 0 420746157 30261248 6043 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6043 603 41 0 7347 0
vsize: 29552
[startup+20.0007 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 6462 0 0 0 1983 14 0 0 25 0 1 0 420746157 30531584 6093 4294967295 134512640 134672761 3221224640 3221223776 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7454 6093 603 41 0 7413 0
vsize: 29816
[startup+30.0017 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 6706 0 0 0 2982 16 0 0 25 0 1 0 420746157 31813632 6337 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7767 6337 603 41 0 7726 0
vsize: 31068
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 6808 0 0 0 3980 17 0 0 25 0 1 0 420746157 32206848 6439 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7863 6439 603 41 0 7822 0
vsize: 31452
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 6945 0 0 0 4979 17 0 0 25 0 1 0 420746157 32747520 6576 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7995 6576 603 41 0 7954 0
vsize: 31980
[startup+60.0027 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 7131 0 0 0 5979 17 0 0 25 0 1 0 420746157 33583104 6762 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8199 6762 603 41 0 8158 0
vsize: 32796
[startup+70.0032 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 7324 0 0 0 6979 18 0 0 25 0 1 0 420746157 34381824 6955 4294967295 134512640 134672761 3221224640 3221223824 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8394 6955 603 41 0 8353 0
vsize: 33576
[startup+80.0043 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 7614 0 0 0 7978 19 0 0 25 0 1 0 420746157 35594240 7245 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8690 7245 603 41 0 8649 0
vsize: 34760
[startup+90.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 7930 0 0 0 8976 20 0 0 25 0 1 0 420746157 36802560 7561 4294967295 134512640 134672761 3221224640 3221223812 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8985 7561 603 41 0 8944 0
vsize: 35940
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 8187 0 0 0 9976 21 0 0 25 0 1 0 420746157 37879808 7818 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9248 7818 603 41 0 9207 0
vsize: 36992
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 8348 0 0 0 10976 21 0 0 25 0 1 0 420746157 38658048 7979 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9438 7979 603 41 0 9397 0
vsize: 37752
[startup+120.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 8501 0 0 0 11976 22 0 0 25 0 1 0 420746157 39034880 8103 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9530 8103 603 41 0 9489 0
vsize: 38120
[startup+130.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 8640 0 0 0 12976 22 0 0 25 0 1 0 420746157 39698432 8242 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9692 8242 603 41 0 9651 0
vsize: 38768
[startup+140.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 8772 0 0 0 13975 23 0 0 25 0 1 0 420746157 40222720 8374 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9820 8374 603 41 0 9779 0
vsize: 39280
[startup+150.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 8913 0 0 0 14975 23 0 0 25 0 1 0 420746157 40759296 8515 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9951 8515 603 41 0 9910 0
vsize: 39804
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 9012 0 0 0 15975 24 0 0 25 0 1 0 420746157 41160704 8614 4294967295 134512640 134672761 3221224640 3221223776 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10049 8614 603 41 0 10008 0
vsize: 40196
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 9113 0 0 0 16975 24 0 0 25 0 1 0 420746157 41562112 8715 4294967295 134512640 134672761 3221224640 3221223776 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10147 8715 603 41 0 10106 0
vsize: 40588
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 9299 0 0 0 17974 25 0 0 25 0 1 0 420746157 42377216 8901 4294967295 134512640 134672761 3221224640 3221223744 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 8901 603 41 0 10305 0
vsize: 41384
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 9648 0 0 0 18973 26 0 0 25 0 1 0 420746157 43696128 9250 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10668 9250 603 41 0 10627 0
vsize: 42672
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 10077 0 0 0 19972 27 0 0 25 0 1 0 420746157 45547520 9679 4294967295 134512640 134672761 3221224640 3221223744 134559953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11120 9679 603 41 0 11079 0
vsize: 44480
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 10457 0 0 0 20971 28 0 0 25 0 1 0 420746157 47128576 10059 4294967295 134512640 134672761 3221224640 3221223744 134559824 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11506 10059 603 41 0 11465 0
vsize: 46024
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 10630 0 0 0 21971 29 0 0 25 0 1 0 420746157 47935488 10232 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 10232 603 41 0 11662 0
vsize: 46812
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 10805 0 0 0 22970 30 0 0 25 0 1 0 420746157 48590848 10407 4294967295 134512640 134672761 3221224640 3221223776 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11863 10407 603 41 0 11822 0
vsize: 47452
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 10984 0 0 0 23970 30 0 0 25 0 1 0 420746157 49389568 10586 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12058 10586 603 41 0 12017 0
vsize: 48232
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 11174 0 0 0 24970 30 0 0 25 0 1 0 420746157 50036736 10776 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12216 10776 603 41 0 12175 0
vsize: 48864
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 11367 0 0 0 25969 31 0 0 25 0 1 0 420746157 50827264 10969 4294967295 134512640 134672761 3221224640 3221223744 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12409 10969 603 41 0 12368 0
vsize: 49636
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 11525 0 0 0 26969 31 0 0 25 0 1 0 420746157 51482624 11127 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12569 11127 603 41 0 12528 0
vsize: 50276
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 11687 0 0 0 27969 32 0 0 25 0 1 0 420746157 52133888 11289 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12728 11289 603 41 0 12687 0
vsize: 50912
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 11822 0 0 0 28969 32 0 0 25 0 1 0 420746157 52789248 11424 4294967295 134512640 134672761 3221224640 3221223744 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12888 11424 603 41 0 12847 0
vsize: 51552
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 11966 0 0 0 29969 32 0 0 25 0 1 0 420746157 53321728 11568 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13018 11568 603 41 0 12977 0
vsize: 52072
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 12151 0 0 0 30968 33 0 0 25 0 1 0 420746157 54108160 11753 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13210 11753 603 41 0 13169 0
vsize: 52840
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 12333 0 0 0 31968 33 0 0 25 0 1 0 420746157 54759424 11935 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13369 11935 603 41 0 13328 0
vsize: 53476
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 12535 0 0 0 32968 34 0 0 25 0 1 0 420746157 55685120 12137 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13595 12137 603 41 0 13554 0
vsize: 54380
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 12718 0 0 0 33967 35 0 0 25 0 1 0 420746157 56344576 12320 4294967295 134512640 134672761 3221224640 3221223776 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13756 12320 603 41 0 13715 0
vsize: 55024
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 12909 0 0 0 34966 35 0 0 25 0 1 0 420746157 57114624 12511 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13944 12511 603 41 0 13903 0
vsize: 55776
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 13030 0 0 0 35966 36 0 0 25 0 1 0 420746157 57643008 12632 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14073 12632 603 41 0 14032 0
vsize: 56292
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 13210 0 0 0 36966 37 0 0 25 0 1 0 420746157 58437632 12812 4294967295 134512640 134672761 3221224640 3221223744 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14267 12812 603 41 0 14226 0
vsize: 57068
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 13371 0 0 0 37965 37 0 0 25 0 1 0 420746157 58974208 12973 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14398 12973 603 41 0 14357 0
vsize: 57592
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 13498 0 0 0 38965 38 0 0 25 0 1 0 420746157 59506688 13100 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14528 13100 603 41 0 14487 0
vsize: 58112
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 13624 0 0 0 39965 38 0 0 25 0 1 0 420746157 60035072 13226 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14657 13226 603 41 0 14616 0
vsize: 58628
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 13746 0 0 0 40964 39 0 0 25 0 1 0 420746157 60579840 13348 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14790 13348 603 41 0 14749 0
vsize: 59160
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 13883 0 0 0 41964 39 0 0 25 0 1 0 420746157 61108224 13485 4294967295 134512640 134672761 3221224640 3221223744 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14919 13485 603 41 0 14878 0
vsize: 59676
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 14030 0 0 0 42964 40 0 0 25 0 1 0 420746157 61767680 13632 4294967295 134512640 134672761 3221224640 3221223744 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15080 13632 603 41 0 15039 0
vsize: 60320
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 14167 0 0 0 43964 40 0 0 25 0 1 0 420746157 62291968 13769 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15208 13769 603 41 0 15167 0
vsize: 60832
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 14296 0 0 0 44963 41 0 0 25 0 1 0 420746157 62812160 13898 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15335 13898 603 41 0 15294 0
vsize: 61340
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 14424 0 0 0 45963 42 0 0 25 0 1 0 420746157 63594496 14026 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15526 14026 603 41 0 15485 0
vsize: 62104
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 14563 0 0 0 46963 42 0 0 25 0 1 0 420746157 64114688 14165 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15653 14165 603 41 0 15612 0
vsize: 62612
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 14680 0 0 0 47962 42 0 0 25 0 1 0 420746157 64655360 14282 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15785 14282 603 41 0 15744 0
vsize: 63140
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 14805 0 0 0 48962 42 0 0 25 0 1 0 420746157 65171456 14407 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15911 14407 603 41 0 15870 0
vsize: 63644
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 14932 0 0 0 49962 43 0 0 25 0 1 0 420746157 65695744 14534 4294967295 134512640 134672761 3221224640 3221223744 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16039 14534 603 41 0 15998 0
vsize: 64156
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 15022 0 0 0 50962 43 0 0 25 0 1 0 420746157 66088960 14624 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16135 14624 603 41 0 16094 0
vsize: 64540
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 15185 0 0 0 51962 43 0 0 25 0 1 0 420746157 66748416 14787 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16296 14787 603 41 0 16255 0
vsize: 65184
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 15308 0 0 0 52962 44 0 0 25 0 1 0 420746157 67272704 14910 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16424 14910 603 41 0 16383 0
vsize: 65696
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 396
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 15438 0 0 0 53961 45 0 0 25 0 1 0 420746157 67788800 15040 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16550 15040 603 41 0 16509 0
vsize: 66200
[startup+550.019 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 449
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 15585 0 0 0 54961 45 0 0 25 0 1 0 420746157 68321280 15187 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16680 15187 603 41 0 16639 0
vsize: 66720
[startup+560.019 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 449
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 15732 0 0 0 55960 46 0 0 25 0 1 0 420746157 68984832 15334 4294967295 134512640 134672761 3221224640 3221223824 134558324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16842 15334 603 41 0 16801 0
vsize: 67368
[startup+570.019 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 449
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 15818 0 0 0 56960 46 0 0 25 0 1 0 420746157 69242880 15420 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16905 15420 603 41 0 16864 0
vsize: 67620
[startup+580.019 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 449
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 15922 0 0 0 57960 46 0 0 25 0 1 0 420746157 69763072 15524 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17032 15524 603 41 0 16991 0
vsize: 68128
[startup+590.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 449
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 16044 0 0 0 58960 47 0 0 25 0 1 0 420746157 70156288 15646 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17128 15646 603 41 0 17087 0
vsize: 68512
[startup+600.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 449
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 16138 0 0 0 59960 47 0 0 25 0 1 0 420746157 70553600 15740 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17225 15740 603 41 0 17184 0
vsize: 68900
[startup+610.019 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 449
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 16231 0 0 0 60959 48 0 0 25 0 1 0 420746157 70950912 15833 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17322 15833 603 41 0 17281 0
vsize: 69288
[startup+620.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 16319 0 0 0 61959 48 0 0 25 0 1 0 420746157 71344128 15921 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17418 15921 603 41 0 17377 0
vsize: 69672
[startup+630.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 16429 0 0 0 62959 48 0 0 25 0 1 0 420746157 71737344 16031 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17514 16031 603 41 0 17473 0
vsize: 70056
[startup+640.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 16556 0 0 0 63959 49 0 0 25 0 1 0 420746157 72265728 16158 4294967295 134512640 134672761 3221224640 3221223744 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17643 16158 603 41 0 17602 0
vsize: 70572
[startup+650.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 16681 0 0 0 64959 49 0 0 25 0 1 0 420746157 72794112 16283 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17772 16283 603 41 0 17731 0
vsize: 71088
[startup+660.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 16813 0 0 0 65959 49 0 0 25 0 1 0 420746157 73310208 16415 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17898 16415 603 41 0 17857 0
vsize: 71592
[startup+670.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 16914 0 0 0 66959 50 0 0 25 0 1 0 420746157 73695232 16516 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17992 16516 603 41 0 17951 0
vsize: 71968
[startup+680.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 17026 0 0 0 67959 50 0 0 25 0 1 0 420746157 74211328 16628 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18118 16628 603 41 0 18077 0
vsize: 72472
[startup+690.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 17153 0 0 0 68958 51 0 0 25 0 1 0 420746157 74739712 16755 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18247 16755 603 41 0 18206 0
vsize: 72988
[startup+700.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 17278 0 0 0 69958 51 0 0 25 0 1 0 420746157 75247616 16880 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18371 16880 603 41 0 18330 0
vsize: 73484
[startup+710.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 17411 0 0 0 70958 51 0 0 25 0 1 0 420746157 75767808 17013 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18498 17013 603 41 0 18457 0
vsize: 73992
[startup+720.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 17544 0 0 0 71958 51 0 0 25 0 1 0 420746157 76296192 17146 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18627 17146 603 41 0 18586 0
vsize: 74508
[startup+730.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 17688 0 0 0 72958 52 0 0 25 0 1 0 420746157 76812288 17290 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18753 17290 603 41 0 18712 0
vsize: 75012
[startup+740.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 17832 0 0 0 73957 52 0 0 25 0 1 0 420746157 77471744 17434 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18914 17434 603 41 0 18873 0
vsize: 75656
[startup+750.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 17965 0 0 0 74957 53 0 0 25 0 1 0 420746157 78004224 17567 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19044 17567 603 41 0 19003 0
vsize: 76176
[startup+760.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 18117 0 0 0 75956 54 0 0 25 0 1 0 420746157 78655488 17719 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19203 17719 603 41 0 19162 0
vsize: 76812
[startup+770.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 18253 0 0 0 76956 54 0 0 25 0 1 0 420746157 79192064 17855 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19334 17855 603 41 0 19293 0
vsize: 77336
[startup+780.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 18372 0 0 0 77956 55 0 0 25 0 1 0 420746157 79716352 17974 4294967295 134512640 134672761 3221224640 3221223744 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19462 17974 603 41 0 19421 0
vsize: 77848
[startup+790.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 18497 0 0 0 78955 55 0 0 25 0 1 0 420746157 80244736 18099 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19591 18099 603 41 0 19550 0
vsize: 78364
[startup+800.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 18631 0 0 0 79955 55 0 0 25 0 1 0 420746157 80773120 18233 4294967295 134512640 134672761 3221224640 3221223744 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19720 18233 603 41 0 19679 0
vsize: 78880
[startup+810.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 18747 0 0 0 80955 56 0 0 25 0 1 0 420746157 81174528 18349 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19818 18349 603 41 0 19777 0
vsize: 79272
[startup+820.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 18857 0 0 0 81955 56 0 0 25 0 1 0 420746157 81686528 18459 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19943 18459 603 41 0 19902 0
vsize: 79772
[startup+830.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 18963 0 0 0 82954 57 0 0 25 0 1 0 420746157 82087936 18565 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20041 18565 603 41 0 20000 0
vsize: 80164
[startup+840.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 19105 0 0 0 83953 58 0 0 25 0 1 0 420746157 82731008 18707 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20198 18707 603 41 0 20157 0
vsize: 80792
[startup+850.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 19215 0 0 0 84952 59 0 0 25 0 1 0 420746157 83120128 18817 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20293 18817 603 41 0 20252 0
vsize: 81172
[startup+860.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 451
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 19341 0 0 0 85951 59 0 0 25 0 1 0 420746157 83644416 18943 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20421 18943 603 41 0 20380 0
vsize: 81684
[startup+870.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 19485 0 0 0 86950 60 0 0 25 0 1 0 420746157 84312064 19087 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20584 19087 603 41 0 20543 0
vsize: 82336
[startup+880.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 19628 0 0 0 87949 62 0 0 25 0 1 0 420746157 84848640 19230 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19230 603 41 0 20674 0
vsize: 82860
[startup+890.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 19767 0 0 0 88948 62 0 0 25 0 1 0 420746157 85372928 19369 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20843 19369 603 41 0 20802 0
vsize: 83372
[startup+900.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 19896 0 0 0 89947 63 0 0 25 0 1 0 420746157 85893120 19498 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20970 19498 603 41 0 20929 0
vsize: 83880
[startup+910.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20015 0 0 0 90947 64 0 0 25 0 1 0 420746157 86417408 19617 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21098 19617 603 41 0 21057 0
vsize: 84392
[startup+920.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20105 0 0 0 91946 64 0 0 25 0 1 0 420746157 86798336 19707 4294967295 134512640 134672761 3221224640 3221223744 134555122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21191 19707 603 41 0 21150 0
vsize: 84764
[startup+930.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20190 0 0 0 92946 64 0 0 25 0 1 0 420746157 87056384 19792 4294967295 134512640 134672761 3221224640 3221223744 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21254 19792 603 41 0 21213 0
vsize: 85016
[startup+940.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20259 0 0 0 93945 65 0 0 25 0 1 0 420746157 87441408 19861 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21348 19861 603 41 0 21307 0
vsize: 85392
[startup+950.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20323 0 0 0 94945 65 0 0 25 0 1 0 420746157 87699456 19925 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21411 19925 603 41 0 21370 0
vsize: 85644
[startup+960.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20402 0 0 0 95944 66 0 0 25 0 1 0 420746157 87957504 20004 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21474 20004 603 41 0 21433 0
vsize: 85896
[startup+970.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20484 0 0 0 96943 67 0 0 25 0 1 0 420746157 88223744 20086 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21539 20086 603 41 0 21498 0
vsize: 86156
[startup+980.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20555 0 0 0 97942 68 0 0 25 0 1 0 420746157 88621056 20157 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21636 20157 603 41 0 21595 0
vsize: 86544
[startup+990.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20626 0 0 0 98942 68 0 0 25 0 1 0 420746157 88879104 20228 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21699 20228 603 41 0 21658 0
vsize: 86796
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20739 0 0 0 99940 69 0 0 25 0 1 0 420746157 89272320 20341 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21795 20341 603 41 0 21754 0
vsize: 87180
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20856 0 0 0 100939 70 0 0 25 0 1 0 420746157 89849856 20458 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21936 20458 603 41 0 21895 0
vsize: 87744
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 20969 0 0 0 101938 71 0 0 25 0 1 0 420746157 90238976 20571 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22031 20571 603 41 0 21990 0
vsize: 88124
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 21091 0 0 0 102937 72 0 0 25 0 1 0 420746157 90750976 20693 4294967295 134512640 134672761 3221224640 3221223776 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22156 20693 603 41 0 22115 0
vsize: 88624
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 21186 0 0 0 103937 72 0 0 25 0 1 0 420746157 91152384 20788 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22254 20788 603 41 0 22213 0
vsize: 89016
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 21291 0 0 0 104936 73 0 0 25 0 1 0 420746157 91541504 20893 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22349 20893 603 41 0 22308 0
vsize: 89396
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 21392 0 0 0 105936 73 0 0 25 0 1 0 420746157 91942912 20994 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22447 20994 603 41 0 22406 0
vsize: 89788
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 21497 0 0 0 106935 74 0 0 25 0 1 0 420746157 92459008 21099 4294967295 134512640 134672761 3221224640 3221223744 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22573 21099 603 41 0 22532 0
vsize: 90292
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 21590 0 0 0 107935 74 0 0 25 0 1 0 420746157 92717056 21192 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22636 21192 603 41 0 22595 0
vsize: 90544
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 21684 0 0 0 108934 75 0 0 25 0 1 0 420746157 93110272 21286 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22732 21286 603 41 0 22691 0
vsize: 90928
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 21779 0 0 0 109934 75 0 0 25 0 1 0 420746157 93495296 21381 4294967295 134512640 134672761 3221224640 3221223744 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22826 21381 603 41 0 22785 0
vsize: 91304
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 21886 0 0 0 110933 76 0 0 25 0 1 0 420746157 94023680 21488 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22955 21488 603 41 0 22914 0
vsize: 91820
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 21984 0 0 0 111932 76 0 0 25 0 1 0 420746157 94973952 21586 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23187 21586 603 41 0 23146 0
vsize: 92748
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 22079 0 0 0 112932 77 0 0 25 0 1 0 420746157 95367168 21681 4294967295 134512640 134672761 3221224640 3221223840 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23283 21681 603 41 0 23242 0
vsize: 93132
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 22155 0 0 0 113931 77 0 0 25 0 1 0 420746157 95621120 21757 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23345 21757 603 41 0 23304 0
vsize: 93380
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 22246 0 0 0 114930 78 0 0 25 0 1 0 420746157 96010240 21848 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23440 21848 603 41 0 23399 0
vsize: 93760
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 22338 0 0 0 115930 78 0 0 25 0 1 0 420746157 96403456 21940 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23536 21940 603 41 0 23495 0
vsize: 94144
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 22418 0 0 0 116929 79 0 0 25 0 1 0 420746157 96796672 22020 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23632 22020 603 41 0 23591 0
vsize: 94528
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 22524 0 0 0 117928 80 0 0 25 0 1 0 420746157 97189888 22126 4294967295 134512640 134672761 3221224640 3221223744 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23728 22126 603 41 0 23687 0
vsize: 94912
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 22623 0 0 0 118928 80 0 0 25 0 1 0 420746157 97587200 22225 4294967295 134512640 134672761 3221224640 3221223776 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23825 22225 603 41 0 23784 0
vsize: 95300
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 453
Raw data (stat): 396 (minisat+) R 395 30854 30853 0 -1 0 22709 0 0 0 119927 81 0 0 25 0 1 0 420746157 97976320 22311 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23920 22311 603 41 0 23879 0
vsize: 95680
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 453
Raw data (stat): 396 (minisat+) Z 395 30854 30853 0 -1 12 22712 0 0 0 119927 85 0 0 25 0 1 0 420746157 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.1
CPU time (s): 1200.13
CPU user time (s): 1199.27
CPU system time (s): 0.858869
CPU usage (%): 100.003
Max. virtual memory (Kb): 95680
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####