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-ii8e2.opb
MD5SUM	66ef5c48f4a7492e24281157b7778ffb
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	514
Optimality of the best value was proved	NO
Number of terms in the objective function	1740
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	1740
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	1740
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.04884
Number of variables	1740
Total number of constraints	6991
Number of constraints which are clauses	6991
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	10
Trace number 6278

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-14 04:07:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4688 boxname=wulflinc25 idbench=176 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  66ef5c48f4a7492e24281157b7778ffb  /oldhome/oroussel/tmp/wulflinc25/normalized-ii8e2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc25/normalized-ii8e2.opb /oldhome/oroussel/tmp/wulflinc25/normalized-ii8e2.opb
IDLAUNCH: 4688
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        870748 kB
Buffers:         35096 kB
Cached:          94272 kB
SwapCached:         36 kB
Active:          51080 kB
Inactive:        81144 kB
HighTotal:      131008 kB
HighFree:        33040 kB
LowTotal:       903652 kB
LowFree:        837708 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26052 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:27:46 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 4688 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6991 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 |    6991    16290 |    2330       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 590[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:98402     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |  249535   583306 |   83178       4       22     5.5 |  0.000 % |
c |       104 |  249416   583040 |   91495     101      727     7.2 |  0.054 % |
c |       255 |  244152   570939 |  100645     117     2646    22.6 |  2.071 % |
c |       480 |  241515   564939 |  110709     308    20850    67.7 |  2.946 % |
c |       817 |  236320   552951 |  121780     562    28504    50.7 |  4.921 % |
c |      1323 |  229039   536249 |  133959     878    39458    44.9 |  7.607 % |
c |      2082 |  219731   514814 |  147354    1506    63607    42.2 | 11.089 % |
c |      3221 |  205847   482804 |  162090    2444   134229    54.9 | 16.360 % |
c |      4929 |  189163   444347 |  178299    3781   180718    47.8 | 22.709 % |
c |      7491 |  182172   428172 |  196129    6186   225214    36.4 | 25.438 % |
c |     11335 |  163838   385783 |  215742    8261   296562    35.9 | 32.545 % |
c |     17101 |  134626   318183 |  237316   13424   461996    34.4 | 43.919 % |
c |     25750 |  130370   308302 |  261048   21878   775526    35.4 | 45.594 % |
c |     38724 |  118531   280905 |  287153   34290  1125654    32.8 | 50.219 % |
c |     58185 |  109813   260743 |  315868   53056  4729770    89.1 | 53.611 % |
c |     87377 |  106345   252726 |  347455   82033  6425389    78.3 | 54.960 % |
c |    131167 |  104885   249361 |  382200  125714 13293997   105.7 | 55.514 % |
c ==============================================================================
c [1mFound solution: 589[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 |    134787 |  104694   248947 |   34898  129315 13472617   104.2 | 55.514 % |
c |    134888 |  104694   248947 |   38387   25412  2324104    91.5 | 55.602 % |
c |    135038 |  104454   248396 |   42226   25443  2327688    91.5 | 55.691 % |
c |    135263 |  104250   247923 |   46449   25628  2330772    90.9 | 55.772 % |
c |    135600 |  104236   247891 |   51094   25904  2350366    90.7 | 55.777 % |
c |    136106 |  104236   247891 |   56203   26410  2360128    89.4 | 55.777 % |
c |    136865 |  104236   247891 |   61823   27169  2386390    87.8 | 55.777 % |
c |    138004 |  104236   247891 |   68006   28308  2457904    86.8 | 55.777 % |
c |    139713 |  104236   247891 |   74806   30017  2550518    85.0 | 55.777 % |
c |    142275 |  104236   247891 |   82287   32579  2738069    84.0 | 55.777 % |
c |    146119 |  104230   247877 |   90516   36421  2904268    79.7 | 55.780 % |
c |    151885 |  103812   246918 |   99568   42052  3378865    80.3 | 55.934 % |
c |    160534 |  103812   246918 |  109524   50701  3800574    75.0 | 55.934 % |
c |    173508 |  103812   246918 |  120477   63675  4404058    69.2 | 55.934 % |
c |    192969 |  103489   246172 |  132525   83108  5480293    65.9 | 56.060 % |
c ==============================================================================
c [1mFound solution: 583[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 |    197151 |  103679   246652 |   34559   87290  5634775    64.6 | 56.060 % |
c |    197251 |  103679   246652 |   38014   25680   817912    31.9 | 56.027 % |
c |    197401 |  103580   246422 |   41816   25829   821986    31.8 | 56.067 % |
c |    197627 |  103580   246422 |   45998   26055   860234    33.0 | 56.067 % |
c |    197964 |  103580   246422 |   50597   26392   867096    32.9 | 56.067 % |
c |    198473 |  103580   246422 |   55657   26901   880498    32.7 | 56.067 % |
c |    199232 |  103301   245773 |   61223   27633   890453    32.2 | 56.181 % |
c |    200371 |  103301   245773 |   67345   28772   993849    34.5 | 56.181 % |
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 -#### 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.93 0.97 0.91 1/54 2622
Raw data (stat): 2622 (runsolver) R 2621 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481597838 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7464 0 0 0 979 18 0 0 25 0 1 0 481597838 34242560 7168 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8360 7168 603 41 0 8319 0
vsize: 33440
[startup+20.0013 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7481 0 0 0 1979 18 0 0 25 0 1 0 481597838 34373632 7185 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8392 7185 603 41 0 8351 0
vsize: 33568
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7487 0 0 0 2979 18 0 0 25 0 1 0 481597838 34373632 7191 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8392 7191 603 41 0 8351 0
vsize: 33568
[startup+40.002 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7532 0 0 0 3979 18 0 0 25 0 1 0 481597838 34508800 7236 4294967295 134512640 134672761 3221224576 3221223748 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8425 7236 603 41 0 8384 0
vsize: 33700
[startup+50.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7563 0 0 0 4979 18 0 0 25 0 1 0 481597838 34770944 7267 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8489 7267 603 41 0 8448 0
vsize: 33956
[startup+60.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7593 0 0 0 5979 19 0 0 25 0 1 0 481597838 34906112 7297 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8522 7297 603 41 0 8481 0
vsize: 34088
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7616 0 0 0 6979 19 0 0 25 0 1 0 481597838 34906112 7320 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8522 7320 603 41 0 8481 0
vsize: 34088
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7640 0 0 0 7979 19 0 0 25 0 1 0 481597838 35061760 7344 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8560 7344 603 41 0 8519 0
vsize: 34240
[startup+90.0033 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7678 0 0 0 8979 19 0 0 25 0 1 0 481597838 35188736 7382 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8591 7382 603 41 0 8550 0
vsize: 34364
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7712 0 0 0 9979 19 0 0 25 0 1 0 481597838 35323904 7416 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8624 7416 603 41 0 8583 0
vsize: 34496
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7742 0 0 0 10979 19 0 0 25 0 1 0 481597838 35487744 7446 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8664 7446 603 41 0 8623 0
vsize: 34656
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7751 0 0 0 11979 19 0 0 25 0 1 0 481597838 35487744 7455 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8664 7455 603 41 0 8623 0
vsize: 34656
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7789 0 0 0 12980 19 0 0 25 0 1 0 481597838 35622912 7493 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8697 7493 603 41 0 8656 0
vsize: 34788
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7851 0 0 0 13980 19 0 0 25 0 1 0 481597838 35889152 7555 4294967295 134512640 134672761 3221224576 3221223680 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8762 7555 603 41 0 8721 0
vsize: 35048
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 7947 0 0 0 14980 19 0 0 25 0 1 0 481597838 36294656 7651 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8861 7651 603 41 0 8820 0
vsize: 35444
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 8044 0 0 0 15980 20 0 0 25 0 1 0 481597838 36814848 7748 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8988 7748 603 41 0 8947 0
vsize: 35952
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 8142 0 0 0 16979 20 0 0 25 0 1 0 481597838 37085184 7846 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9054 7846 603 41 0 9013 0
vsize: 36216
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 8219 0 0 0 17979 20 0 0 25 0 1 0 481597838 37490688 7923 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9153 7923 603 41 0 9112 0
vsize: 36612
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 8284 0 0 0 18979 20 0 0 25 0 1 0 481597838 37756928 7988 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9218 7988 603 41 0 9177 0
vsize: 36872
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 8363 0 0 0 19979 21 0 0 25 0 1 0 481597838 38027264 8067 4294967295 134512640 134672761 3221224576 3221223792 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9284 8067 603 41 0 9243 0
vsize: 37136
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 8490 0 0 0 20979 21 0 0 25 0 1 0 481597838 38559744 8194 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9414 8194 603 41 0 9373 0
vsize: 37656
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 8535 0 0 0 21979 21 0 0 25 0 1 0 481597838 38694912 8239 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9447 8239 603 41 0 9406 0
vsize: 37788
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 8606 0 0 0 22979 22 0 0 25 0 1 0 481597838 39088128 8310 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9543 8310 603 41 0 9502 0
vsize: 38172
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 8715 0 0 0 23978 22 0 0 25 0 1 0 481597838 39481344 8419 4294967295 134512640 134672761 3221224576 3221223680 134560180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9639 8419 603 41 0 9598 0
vsize: 38556
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 8808 0 0 0 24979 22 0 0 25 0 1 0 481597838 39878656 8512 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9736 8512 603 41 0 9695 0
vsize: 38944
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 8858 0 0 0 25978 22 0 0 25 0 1 0 481597838 40148992 8562 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9802 8562 603 41 0 9761 0
vsize: 39208
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 9002 0 0 0 26978 23 0 0 25 0 1 0 481597838 40685568 8706 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9933 8706 603 41 0 9892 0
vsize: 39732
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 9380 0 0 0 27977 24 0 0 25 0 1 0 481597838 42287104 9084 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10324 9084 603 41 0 10283 0
vsize: 41296
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 9762 0 0 0 28976 25 0 0 25 0 1 0 481597838 43757568 9466 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10683 9466 603 41 0 10642 0
vsize: 42732
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 10093 0 0 0 29976 25 0 0 25 0 1 0 481597838 45105152 9797 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11012 9798 603 41 0 10971 0
vsize: 44048
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 10400 0 0 0 30975 26 0 0 25 0 1 0 481597838 46436352 10104 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11337 10104 603 41 0 11296 0
vsize: 45348
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 10757 0 0 0 31975 27 0 0 25 0 1 0 481597838 47796224 10461 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11669 10461 603 41 0 11628 0
vsize: 46676
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 11121 0 0 0 32974 28 0 0 25 0 1 0 481597838 49442816 10825 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12071 10825 603 41 0 12030 0
vsize: 48284
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 11437 0 0 0 33974 28 0 0 25 0 1 0 481597838 50642944 11141 4294967295 134512640 134672761 3221224576 3221223744 134561272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12364 11141 603 41 0 12323 0
vsize: 49456
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 11715 0 0 0 34973 29 0 0 25 0 1 0 481597838 51830784 11419 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12654 11419 603 41 0 12613 0
vsize: 50616
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 12045 0 0 0 35972 30 0 0 25 0 1 0 481597838 53166080 11749 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12980 11749 603 41 0 12939 0
vsize: 51920
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 12316 0 0 0 36971 31 0 0 25 0 1 0 481597838 54231040 12020 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13240 12020 603 41 0 13199 0
vsize: 52960
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 12441 0 0 0 37970 32 0 0 25 0 1 0 481597838 54771712 12145 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13372 12145 603 41 0 13331 0
vsize: 53488
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 12607 0 0 0 38969 33 0 0 25 0 1 0 481597838 55439360 12311 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13535 12311 603 41 0 13494 0
vsize: 54140
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 12697 0 0 0 39969 33 0 0 25 0 1 0 481597838 55836672 12401 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13632 12401 603 41 0 13591 0
vsize: 54528
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 12770 0 0 0 40969 33 0 0 25 0 1 0 481597838 56369152 12474 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13762 12474 603 41 0 13721 0
vsize: 55048
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 12847 0 0 0 41970 33 0 0 25 0 1 0 481597838 56639488 12551 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13828 12551 603 41 0 13787 0
vsize: 55312
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 12960 0 0 0 42969 33 0 0 25 0 1 0 481597838 57040896 12664 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13926 12664 603 41 0 13885 0
vsize: 55704
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 13103 0 0 0 43969 34 0 0 25 0 1 0 481597838 57704448 12807 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14088 12807 603 41 0 14047 0
vsize: 56352
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 13195 0 0 0 44969 34 0 0 25 0 1 0 481597838 58105856 12899 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 12899 603 41 0 14145 0
vsize: 56744
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 13315 0 0 0 45969 34 0 0 25 0 1 0 481597838 58503168 13019 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14283 13019 603 41 0 14242 0
vsize: 57132
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 13563 0 0 0 46969 34 0 0 25 0 1 0 481597838 59559936 13267 4294967295 134512640 134672761 3221224576 3221223680 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14541 13267 603 41 0 14500 0
vsize: 58164
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 13812 0 0 0 47968 35 0 0 25 0 1 0 481597838 60493824 13516 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14769 13516 603 41 0 14728 0
vsize: 59076
[startup+490.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 14045 0 0 0 48968 36 0 0 25 0 1 0 481597838 61550592 13749 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15027 13749 603 41 0 14986 0
vsize: 60108
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 14133 0 0 0 49968 36 0 0 25 0 1 0 481597838 61816832 13837 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15092 13837 603 41 0 15051 0
vsize: 60368
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 14210 0 0 0 50968 36 0 0 25 0 1 0 481597838 62222336 13914 4294967295 134512640 134672761 3221224576 3221223680 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15191 13914 603 41 0 15150 0
vsize: 60764
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 14338 0 0 0 51966 37 0 0 25 0 1 0 481597838 62623744 14042 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15289 14042 603 41 0 15248 0
vsize: 61156
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 14505 0 0 0 52966 38 0 0 25 0 1 0 481597838 63299584 14209 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15454 14209 603 41 0 15413 0
vsize: 61816
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 14573 0 0 0 53966 38 0 0 25 0 1 0 481597838 63569920 14277 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15520 14277 603 41 0 15479 0
vsize: 62080
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 14694 0 0 0 54966 38 0 0 25 0 1 0 481597838 64106496 14398 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15651 14398 603 41 0 15610 0
vsize: 62604
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 14823 0 0 0 55965 39 0 0 25 0 1 0 481597838 64638976 14527 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15781 14527 603 41 0 15740 0
vsize: 63124
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 15018 0 0 0 56965 40 0 0 25 0 1 0 481597838 65441792 14722 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15977 14722 603 41 0 15936 0
vsize: 63908
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 15225 0 0 0 57965 40 0 0 25 0 1 0 481597838 66240512 14929 4294967295 134512640 134672761 3221224576 3221223744 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16172 14929 603 41 0 16131 0
vsize: 64688
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 15447 0 0 0 58964 41 0 0 25 0 1 0 481597838 67178496 15151 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16401 15151 603 41 0 16360 0
vsize: 65604
[startup+600.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 15677 0 0 0 59963 42 0 0 25 0 1 0 481597838 68112384 15381 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16629 15381 603 41 0 16588 0
vsize: 66516
[startup+610.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 15883 0 0 0 60963 42 0 0 25 0 1 0 481597838 68894720 15587 4294967295 134512640 134672761 3221224576 3221223680 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16820 15587 603 41 0 16779 0
vsize: 67280
[startup+620.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 16090 0 0 0 61962 44 0 0 25 0 1 0 481597838 69836800 15794 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17050 15794 603 41 0 17009 0
vsize: 68200
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 16271 0 0 0 62961 44 0 0 25 0 1 0 481597838 70500352 15975 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17212 15975 603 41 0 17171 0
vsize: 68848
[startup+640.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 16433 0 0 0 63960 45 0 0 25 0 1 0 481597838 71168000 16137 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17375 16137 603 41 0 17334 0
vsize: 69500
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 16589 0 0 0 64961 45 0 0 25 0 1 0 481597838 71827456 16293 4294967295 134512640 134672761 3221224576 3221223744 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17536 16293 603 41 0 17495 0
vsize: 70144
[startup+660.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 16718 0 0 0 65960 46 0 0 25 0 1 0 481597838 72359936 16422 4294967295 134512640 134672761 3221224576 3221223680 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17666 16422 603 41 0 17625 0
vsize: 70664
[startup+670.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 16900 0 0 0 66960 46 0 0 25 0 1 0 481597838 73158656 16604 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17861 16604 603 41 0 17820 0
vsize: 71444
[startup+680.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 17075 0 0 0 67960 47 0 0 25 0 1 0 481597838 73826304 16779 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18024 16779 603 41 0 17983 0
vsize: 72096
[startup+690.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 17225 0 0 0 68960 47 0 0 25 0 1 0 481597838 74493952 16929 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18187 16929 603 41 0 18146 0
vsize: 72748
[startup+700.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 17414 0 0 0 69959 48 0 0 25 0 1 0 481597838 75153408 17118 4294967295 134512640 134672761 3221224576 3221223744 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18348 17118 603 41 0 18307 0
vsize: 73392
[startup+710.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 17593 0 0 0 70959 48 0 0 25 0 1 0 481597838 75952128 17297 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18543 17297 603 41 0 18502 0
vsize: 74172
[startup+720.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 17747 0 0 0 71959 49 0 0 25 0 1 0 481597838 76492800 17451 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18675 17451 603 41 0 18634 0
vsize: 74700
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 17867 0 0 0 72958 49 0 0 25 0 1 0 481597838 77012992 17571 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18802 17571 603 41 0 18761 0
vsize: 75208
[startup+740.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 17995 0 0 0 73958 49 0 0 25 0 1 0 481597838 77541376 17699 4294967295 134512640 134672761 3221224576 3221223712 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18931 17699 603 41 0 18890 0
vsize: 75724
[startup+750.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 18158 0 0 0 74958 50 0 0 25 0 1 0 481597838 78221312 17862 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19097 17862 603 41 0 19056 0
vsize: 76388
[startup+760.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 18264 0 0 0 75958 50 0 0 25 0 1 0 481597838 78626816 17968 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19196 17968 603 41 0 19155 0
vsize: 76784
[startup+770.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 18450 0 0 0 76958 51 0 0 25 0 1 0 481597838 79441920 18154 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19395 18154 603 41 0 19354 0
vsize: 77580
[startup+780.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 18755 0 0 0 77958 51 0 0 25 0 1 0 481597838 80646144 18459 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19689 18459 603 41 0 19648 0
vsize: 78756
[startup+790.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 19043 0 0 0 78957 51 0 0 25 0 1 0 481597838 81833984 18747 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19979 18747 603 41 0 19938 0
vsize: 79916
[startup+800.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 19203 0 0 0 79957 52 0 0 25 0 1 0 481597838 82497536 18907 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20141 18907 603 41 0 20100 0
vsize: 80564
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 19314 0 0 0 80957 53 0 0 25 0 1 0 481597838 82903040 19018 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20240 19018 603 41 0 20199 0
vsize: 80960
[startup+820.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 19464 0 0 0 81956 53 0 0 25 0 1 0 481597838 83578880 19168 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20405 19168 603 41 0 20364 0
vsize: 81620
[startup+830.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 19678 0 0 0 82956 53 0 0 25 0 1 0 481597838 84381696 19382 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20601 19382 603 41 0 20560 0
vsize: 82404
[startup+840.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 19988 0 0 0 83956 54 0 0 25 0 1 0 481597838 85721088 19692 4294967295 134512640 134672761 3221224576 3221223760 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20928 19692 603 41 0 20887 0
vsize: 83712
[startup+850.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 20234 0 0 0 84955 55 0 0 25 0 1 0 481597838 86659072 19938 4294967295 134512640 134672761 3221224576 3221223680 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21157 19938 603 41 0 21116 0
vsize: 84628
[startup+860.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 20499 0 0 0 85955 55 0 0 25 0 1 0 481597838 87728128 20203 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21418 20203 603 41 0 21377 0
vsize: 85672
[startup+870.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 20805 0 0 0 86954 56 0 0 25 0 1 0 481597838 89071616 20509 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21746 20509 603 41 0 21705 0
vsize: 86984
[startup+880.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21075 0 0 0 87953 57 0 0 25 0 1 0 481597838 90128384 20779 4294967295 134512640 134672761 3221224576 3221223680 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22004 20779 603 41 0 21963 0
vsize: 88016
[startup+890.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21345 0 0 0 88953 58 0 0 25 0 1 0 481597838 91209728 21049 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22268 21049 603 41 0 22227 0
vsize: 89072
[startup+900.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21478 0 0 0 89951 59 0 0 25 0 1 0 481597838 91742208 21182 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22398 21182 603 41 0 22357 0
vsize: 89592
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 90949 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 91949 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+930.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 92949 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 93950 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+950.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 94950 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+960.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 95950 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+970.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 96950 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+980.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 97954 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+990.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 98954 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 99954 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 100954 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 101955 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 102955 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 103955 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 104955 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 105955 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 106956 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 107956 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 108956 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 109956 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 110956 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 111956 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 112957 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 113957 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 114957 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 115957 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 116958 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 117958 61 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 118957 62 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223724 1074754736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2622
Raw data (stat): 2622 (minisat+) R 2621 28099 28098 0 -1 0 21746 0 0 0 119957 62 0 0 25 0 1 0 481597838 93257728 21450 4294967295 134512640 134672761 3221224576 3221223760 134558768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22768 21450 603 41 0 22727 0
vsize: 91072
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 2622
Raw data (stat): 2622 (minisat+) Z 2621 28099 28098 0 -1 12 21749 0 0 0 119957 66 0 0 25 0 1 0 481597838 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.24
CPU user time (s): 1199.58
CPU system time (s): 0.661899
CPU usage (%): 100.012
Max. virtual memory (Kb): 91072
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####