PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-ex5.pi.opb
MD5SUM	ebc55cfc194a279163f52418008eccf2
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	65
Optimality of the best value was proved	NO
Number of terms in the objective function	2460
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	2460
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	2460
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.11783
Number of variables	2459
Total number of constraints	873
Number of constraints which are clauses	873
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	146
Trace number 5801

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-14 01:50:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4203 boxname=wulflinc9 idbench=67 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ebc55cfc194a279163f52418008eccf2  /oldhome/oroussel/tmp/wulflinc9/normalized-ex5.pi.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc9/normalized-ex5.pi.opb /oldhome/oroussel/tmp/wulflinc9/normalized-ex5.pi.opb
IDLAUNCH: 4203
/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:        893484 kB
Buffers:         36204 kB
Cached:          84748 kB
SwapCached:        564 kB
Active:          54132 kB
Inactive:        70224 kB
HighTotal:      131008 kB
HighFree:        42308 kB
LowTotal:       903652 kB
LowFree:        851176 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11124 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:11:00 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 4203 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 845 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ===
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     842    40436 |     280       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 85[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:160772     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  185453   471352 |   61817       0        0     nan |  0.000 % |
c |       103 |  185008   470430 |   67998      91     1588    17.5 |  0.188 % |
c |       257 |  185004   470422 |   74798     244     9876    40.5 |  0.190 % |
c |       482 |  184970   470349 |   82278     466    35153    75.4 |  0.204 % |
c |       824 |  184970   470349 |   90506     808    53521    66.2 |  0.204 % |
c |      1334 |  184970   470349 |   99556    1318    88462    67.1 |  0.204 % |
c |      2093 |  184935   470276 |  109512    2076   162586    78.3 |  0.217 % |
c |      3235 |  184933   470272 |  120463    3216   250257    77.8 |  0.217 % |
c |      4943 |  184933   470272 |  132510    4924   387907    78.8 |  0.217 % |
c |      7506 |  184933   470272 |  145761    7487   897763   119.9 |  0.217 % |
c |     11353 |  184933   470272 |  160337   11334  1357673   119.8 |  0.217 % |
c |     17119 |  184933   470272 |  176371   17100  2361775   138.1 |  0.217 % |
c |     25769 |  184933   470272 |  194008   25750  3970588   154.2 |  0.217 % |
c |     38743 |  184933   470272 |  213409   38724  7058377   182.3 |  0.217 % |
c |     58204 |  184933   470272 |  234749   58185 11487637   197.4 |  0.217 % |
c |     87396 |  184933   470272 |  258224   87377 17933621   205.2 |  0.217 % |
c |    131185 |  184933   470272 |  284047  131166 25171287   191.9 |  0.217 % |
c ==============================================================================
c [1mFound solution: 82[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 |    153439 |  184925   470262 |   61641  152777 30458297   199.4 |  0.217 % |
c |    153539 |  184925   470262 |   67805   16214  3184884   196.4 |  0.238 % |
c |    153689 |  184925   470262 |   74585   16364  3195544   195.3 |  0.238 % |
c |    153914 |  184876   470160 |   82044   16587  3212674   193.7 |  0.258 % |
c |    154252 |  184876   470160 |   90248   16925  3245876   191.8 |  0.258 % |
c |    154758 |  184876   470160 |   99273   17431  3280407   188.2 |  0.258 % |
c |    155520 |  184876   470160 |  109200   18193  3356694   184.5 |  0.258 % |
c |    156659 |  184876   470160 |  120120   19332  3477071   179.9 |  0.258 % |
c |    158367 |  184876   470160 |  132132   21040  3658733   173.9 |  0.258 % |
c |    160929 |  184876   470160 |  145346   23602  4024361   170.5 |  0.258 % |
c |    164773 |  184876   470160 |  159880   27446  4517995   164.6 |  0.258 % |
c |    170539 |  184876   470160 |  175868   33212  5499541   165.6 |  0.258 % |
c |    179189 |  184876   470160 |  193455   41862  7458581   178.2 |  0.258 % |
c |    192163 |  184876   470160 |  212801   54836  9984053   182.1 |  0.258 % |
c |    211624 |  184876   470160 |  234081   74297 13877659   186.8 |  0.258 % |
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 #### 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.98 0.92 2/54 2778
Raw data (stat): 2778 (runsolver) R 2777 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422546226 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.93 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 9446 0 0 0 974 24 0 0 25 0 1 0 422546226 41955328 9151 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10243 9151 603 41 0 10202 0
vsize: 40972
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 9927 0 0 0 1971 26 0 0 25 0 1 0 422546226 43978752 9632 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10737 9632 603 41 0 10696 0
vsize: 42948
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 10562 0 0 0 2968 29 0 0 25 0 1 0 422546226 46530560 10267 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11360 10267 603 41 0 11319 0
vsize: 45440
[startup+40.002 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 10788 0 0 0 3967 31 0 0 25 0 1 0 422546226 47472640 10493 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11590 10493 603 41 0 11549 0
vsize: 46360
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 11336 0 0 0 4966 32 0 0 25 0 1 0 422546226 49750016 11041 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12146 11041 603 41 0 12105 0
vsize: 48584
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 12082 0 0 0 5963 35 0 0 25 0 1 0 422546226 52776960 11787 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12885 11787 603 41 0 12844 0
vsize: 51540
[startup+70.0013 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 12826 0 0 0 6962 37 0 0 25 0 1 0 422546226 55877632 12531 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13642 12532 603 41 0 13601 0
vsize: 54568
[startup+80.0018 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 13393 0 0 0 7960 38 0 0 25 0 1 0 422546226 58163200 13098 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14200 13098 603 41 0 14159 0
vsize: 56800
[startup+90.0016 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 13766 0 0 0 8959 39 0 0 25 0 1 0 422546226 59645952 13471 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14562 13471 603 41 0 14521 0
vsize: 58248
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 14254 0 0 0 9958 41 0 0 25 0 1 0 422546226 61669376 13959 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15056 13959 603 41 0 15015 0
vsize: 60224
[startup+110.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 14846 0 0 0 10956 43 0 0 25 0 1 0 422546226 64065536 14551 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15641 14551 603 41 0 15600 0
vsize: 62564
[startup+120.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 15351 0 0 0 11953 46 0 0 25 0 1 0 422546226 66084864 15056 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16134 15056 603 41 0 16093 0
vsize: 64536
[startup+130.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 15844 0 0 0 12952 47 0 0 25 0 1 0 422546226 68231168 15549 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16658 15549 603 41 0 16617 0
vsize: 66632
[startup+140.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 16372 0 0 0 13950 50 0 0 25 0 1 0 422546226 70381568 16077 4294967295 134512640 134672761 3221224560 3221223664 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17183 16077 603 41 0 17142 0
vsize: 68732
[startup+150.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 16960 0 0 0 14948 51 0 0 25 0 1 0 422546226 72798208 16665 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17773 16665 603 41 0 17732 0
vsize: 71092
[startup+160.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 17222 0 0 0 15947 53 0 0 25 0 1 0 422546226 73867264 16927 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18034 16927 603 41 0 17993 0
vsize: 72136
[startup+170.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 17580 0 0 0 16946 54 0 0 25 0 1 0 422546226 75354112 17285 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18397 17285 603 41 0 18356 0
vsize: 73588
[startup+180.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 17960 0 0 0 17944 56 0 0 25 0 1 0 422546226 76984320 17665 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18795 17666 603 41 0 18754 0
vsize: 75180
[startup+190.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 18329 0 0 0 18943 57 0 0 25 0 1 0 422546226 78467072 18034 4294967295 134512640 134672761 3221224560 3221223664 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19157 18034 603 41 0 19116 0
vsize: 76628
[startup+200.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 18705 0 0 0 19942 58 0 0 25 0 1 0 422546226 79945728 18410 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18410 603 41 0 19477 0
vsize: 78072
[startup+210.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 19140 0 0 0 20941 60 0 0 25 0 1 0 422546226 81694720 18845 4294967295 134512640 134672761 3221224560 3221223664 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19945 18845 603 41 0 19904 0
vsize: 79780
[startup+220.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 19538 0 0 0 21939 61 0 0 25 0 1 0 422546226 83292160 19243 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20335 19243 603 41 0 20294 0
vsize: 81340
[startup+230.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 19910 0 0 0 22938 63 0 0 25 0 1 0 422546226 84910080 19615 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20730 19615 603 41 0 20689 0
vsize: 82920
[startup+240.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 20309 0 0 0 23937 65 0 0 25 0 1 0 422546226 86523904 20014 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21124 20014 603 41 0 21083 0
vsize: 84496
[startup+250.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 20664 0 0 0 24935 66 0 0 25 0 1 0 422546226 88006656 20369 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21486 20369 603 41 0 21445 0
vsize: 85944
[startup+260.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 21005 0 0 0 25934 67 0 0 25 0 1 0 422546226 89354240 20710 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21815 20710 603 41 0 21774 0
vsize: 87260
[startup+270.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 21475 0 0 0 26933 69 0 0 25 0 1 0 422546226 91230208 21180 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22273 21180 603 41 0 22232 0
vsize: 89092
[startup+280.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 21860 0 0 0 27932 70 0 0 25 0 1 0 422546226 92835840 21565 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22665 21565 603 41 0 22624 0
vsize: 90660
[startup+290.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 22153 0 0 0 28932 70 0 0 25 0 1 0 422546226 94044160 21858 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22960 21858 603 41 0 22919 0
vsize: 91840
[startup+300.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 22457 0 0 0 29931 71 0 0 25 0 1 0 422546226 95252480 22162 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23255 22162 603 41 0 23214 0
vsize: 93020
[startup+310.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 22756 0 0 0 30930 72 0 0 25 0 1 0 422546226 96456704 22461 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23549 22461 603 41 0 23508 0
vsize: 94196
[startup+320.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 23092 0 0 0 31929 73 0 0 25 0 1 0 422546226 97800192 22797 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23877 22797 603 41 0 23836 0
vsize: 95508
[startup+330.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 23512 0 0 0 32928 74 0 0 25 0 1 0 422546226 99807232 23217 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24367 23217 603 41 0 24326 0
vsize: 97468
[startup+340.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 23861 0 0 0 33928 75 0 0 25 0 1 0 422546226 101273600 23566 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24725 23567 603 41 0 24684 0
vsize: 98900
[startup+350.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 24192 0 0 0 34926 77 0 0 25 0 1 0 422546226 102612992 23897 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25052 23897 603 41 0 25011 0
vsize: 100208
[startup+360.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 24543 0 0 0 35926 77 0 0 25 0 1 0 422546226 104095744 24248 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25414 24248 603 41 0 25373 0
vsize: 101656
[startup+370.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 24888 0 0 0 36924 79 0 0 25 0 1 0 422546226 105418752 24593 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25737 24593 603 41 0 25696 0
vsize: 102948
[startup+380.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 25250 0 0 0 37924 80 0 0 25 0 1 0 422546226 106893312 24955 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26097 24955 603 41 0 26056 0
vsize: 104388
[startup+390.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 25585 0 0 0 38922 82 0 0 25 0 1 0 422546226 108249088 25290 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26428 25290 603 41 0 26387 0
vsize: 105712
[startup+400.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 26034 0 0 0 39921 83 0 0 25 0 1 0 422546226 110137344 25739 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26889 25739 603 41 0 26848 0
vsize: 107556
[startup+410.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 26499 0 0 0 40920 85 0 0 25 0 1 0 422546226 112013312 26204 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27347 26204 603 41 0 27306 0
vsize: 109388
[startup+420.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 27068 0 0 0 41918 86 0 0 25 0 1 0 422546226 114425856 26773 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27936 26773 603 41 0 27895 0
vsize: 111744
[startup+430.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 27699 0 0 0 42916 88 0 0 25 0 1 0 422546226 116977664 27404 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28559 27404 603 41 0 28518 0
vsize: 114236
[startup+440.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 28082 0 0 0 43916 89 0 0 25 0 1 0 422546226 118444032 27787 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28917 27787 603 41 0 28876 0
vsize: 115668
[startup+450.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 28489 0 0 0 44913 91 0 0 25 0 1 0 422546226 120188928 28194 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29343 28194 603 41 0 29302 0
vsize: 117372
[startup+460.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 28823 0 0 0 45912 92 0 0 25 0 1 0 422546226 121524224 28528 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29669 28528 603 41 0 29628 0
vsize: 118676
[startup+470.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 29111 0 0 0 46911 93 0 0 25 0 1 0 422546226 122732544 28816 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29964 28816 603 41 0 29923 0
vsize: 119856
[startup+480.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 29556 0 0 0 47910 95 0 0 25 0 1 0 422546226 124485632 29261 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30392 29261 603 41 0 30351 0
vsize: 121568
[startup+490.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 29865 0 0 0 48909 96 0 0 25 0 1 0 422546226 125702144 29570 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30689 29570 603 41 0 30648 0
vsize: 122756
[startup+500.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 30153 0 0 0 49908 97 0 0 25 0 1 0 422546226 126906368 29858 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30983 29858 603 41 0 30942 0
vsize: 123932
[startup+510.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 30448 0 0 0 50907 99 0 0 25 0 1 0 422546226 128118784 30153 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31279 30153 603 41 0 31238 0
vsize: 125116
[startup+520.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 30759 0 0 0 51906 100 0 0 25 0 1 0 422546226 129454080 30464 4294967295 134512640 134672761 3221224560 3221223728 134561264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31605 30464 603 41 0 31564 0
vsize: 126420
[startup+530.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 31035 0 0 0 52904 101 0 0 25 0 1 0 422546226 130527232 30740 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31867 30740 603 41 0 31826 0
vsize: 127468
[startup+540.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 2778
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 31334 0 0 0 53903 103 0 0 25 0 1 0 422546226 131731456 31039 4294967295 134512640 134672761 3221224560 3221223664 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32161 31039 603 41 0 32120 0
vsize: 128644
[startup+550.047 s]
Raw data (loadavg): 0.99 0.98 0.92 3/57 2819
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 31627 0 0 0 54905 104 0 0 25 0 1 0 422546226 132939776 31332 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32456 31332 603 41 0 32415 0
vsize: 129824
[startup+560.047 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 2831
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 32048 0 0 0 55904 106 0 0 25 0 1 0 422546226 134672384 31753 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32879 31754 603 41 0 32838 0
vsize: 131516
[startup+570.046 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 2831
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 32473 0 0 0 56903 107 0 0 25 0 1 0 422546226 136392704 32178 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33299 32178 603 41 0 33258 0
vsize: 133196
[startup+580.048 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 2831
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 32722 0 0 0 57902 107 0 0 25 0 1 0 422546226 137469952 32427 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33562 32427 603 41 0 33521 0
vsize: 134248
[startup+590.047 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 2831
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 33023 0 0 0 58902 108 0 0 25 0 1 0 422546226 138674176 32728 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33856 32728 603 41 0 33815 0
vsize: 135424
[startup+600.047 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 2831
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 33346 0 0 0 59900 110 0 0 25 0 1 0 422546226 140013568 33051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34183 33051 603 41 0 34142 0
vsize: 136732
[startup+610.047 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 2831
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 33624 0 0 0 60900 110 0 0 25 0 1 0 422546226 141127680 33329 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34455 33329 603 41 0 34414 0
vsize: 137820
[startup+620.046 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 33924 0 0 0 61899 111 0 0 25 0 1 0 422546226 142340096 33629 4294967295 134512640 134672761 3221224560 3221223664 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34751 33629 603 41 0 34710 0
vsize: 139004
[startup+630.047 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 34215 0 0 0 62899 112 0 0 25 0 1 0 422546226 143548416 33920 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35046 33920 603 41 0 35005 0
vsize: 140184
[startup+640.048 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 34524 0 0 0 63898 113 0 0 25 0 1 0 422546226 144875520 34229 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35370 34229 603 41 0 35329 0
vsize: 141480
[startup+650.048 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 34824 0 0 0 64897 114 0 0 25 0 1 0 422546226 146092032 34529 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35667 34529 603 41 0 35626 0
vsize: 142668
[startup+660.048 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 35106 0 0 0 65896 116 0 0 25 0 1 0 422546226 147165184 34811 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35929 34811 603 41 0 35888 0
vsize: 143716
[startup+670.048 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 35303 0 0 0 66895 116 0 0 25 0 1 0 422546226 148094976 35008 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36156 35008 603 41 0 36115 0
vsize: 144624
[startup+680.049 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 35508 0 0 0 67895 117 0 0 25 0 1 0 422546226 148905984 35213 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36354 35213 603 41 0 36313 0
vsize: 145416
[startup+690.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 35773 0 0 0 68895 117 0 0 25 0 1 0 422546226 149983232 35478 4294967295 134512640 134672761 3221224560 3221223684 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36617 35478 603 41 0 36576 0
vsize: 146468
[startup+700.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 36085 0 0 0 69893 118 0 0 25 0 1 0 422546226 151855104 35790 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37074 35790 603 41 0 37033 0
vsize: 148296
[startup+710.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 36419 0 0 0 70892 119 0 0 25 0 1 0 422546226 153231360 36124 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37410 36124 603 41 0 37369 0
vsize: 149640
[startup+720.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 36720 0 0 0 71891 121 0 0 25 0 1 0 422546226 154439680 36425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37705 36425 603 41 0 37664 0
vsize: 150820
[startup+730.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 37193 0 0 0 72891 121 0 0 25 0 1 0 422546226 156315648 36898 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38163 36898 603 41 0 38122 0
vsize: 152652
[startup+740.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 37700 0 0 0 73890 123 0 0 25 0 1 0 422546226 158474240 37405 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38690 37405 603 41 0 38649 0
vsize: 154760
[startup+750.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 38107 0 0 0 74889 124 0 0 25 0 1 0 422546226 160083968 37812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39083 37812 603 41 0 39042 0
vsize: 156332
[startup+760.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 38491 0 0 0 75888 125 0 0 25 0 1 0 422546226 161693696 38196 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39476 38196 603 41 0 39435 0
vsize: 157904
[startup+770.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 38866 0 0 0 76886 126 0 0 25 0 1 0 422546226 163164160 38571 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39835 38571 603 41 0 39794 0
vsize: 159340
[startup+780.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 39294 0 0 0 77885 128 0 0 25 0 1 0 422546226 164909056 38999 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40261 38999 603 41 0 40220 0
vsize: 161044
[startup+790.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 39680 0 0 0 78885 128 0 0 25 0 1 0 422546226 166510592 39385 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40652 39385 603 41 0 40611 0
vsize: 162608
[startup+800.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 40089 0 0 0 79883 130 0 0 25 0 1 0 422546226 168259584 39794 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41079 39794 603 41 0 41038 0
vsize: 164316
[startup+810.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 40465 0 0 0 80882 131 0 0 25 0 1 0 422546226 169725952 40170 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41437 40170 603 41 0 41396 0
vsize: 165748
[startup+820.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 40768 0 0 0 81882 132 0 0 25 0 1 0 422546226 170938368 40473 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41733 40473 603 41 0 41692 0
vsize: 166932
[startup+830.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41294 0 0 0 82881 133 0 0 25 0 1 0 422546226 173084672 40999 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42257 40999 603 41 0 42216 0
vsize: 169028
[startup+840.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 83879 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+850.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 84879 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+860.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2833
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 85879 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+870.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 86879 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+880.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 87879 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+890.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 88879 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223696 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+900.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 89880 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223644 1075346528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+910.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 90880 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+920.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 91880 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+930.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 92880 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+940.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 93880 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+950.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 94881 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+960.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 95881 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+970.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 96881 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+980.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 97881 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+990.057 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 98881 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 99882 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 100882 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223696 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 101882 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223744 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 102882 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 103883 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 104883 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 105883 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 106883 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 107883 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1090.06 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 108884 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1100.06 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 109884 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1110.06 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 110884 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1120.06 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 111884 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1130.06 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 112884 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1140.06 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 113884 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1150.06 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 114885 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1160.06 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 115885 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1170.06 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 116885 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1180.06 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 117885 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1190.06 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 118885 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
[startup+1200.06 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2835
Raw data (stat): 2778 (minisat+) R 2777 30854 30853 0 -1 0 41974 0 0 0 119886 135 0 0 25 0 1 0 422546226 176402432 41667 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 41667 603 41 0 43026 0
vsize: 172268
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.01 1.01 0.93 1/54 2835
Raw data (stat): 2778 (minisat+) Z 2777 30854 30853 0 -1 12 41977 0 0 0 119886 143 0 0 25 0 1 0 422546226 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.15
CPU time (s): 1200.3
CPU user time (s): 1198.86
CPU system time (s): 1.43578
CPU usage (%): 100.013
Max. virtual memory (Kb): 172268
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####