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 5419

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-13 23:50:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3827 boxname=wulflinc23 idbench=67 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ebc55cfc194a279163f52418008eccf2  /oldhome/oroussel/tmp/wulflinc23/normalized-ex5.pi.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc23/normalized-ex5.pi.opb /oldhome/oroussel/tmp/wulflinc23/normalized-ex5.pi.opb
IDLAUNCH: 3827
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        895052 kB
Buffers:         34344 kB
Cached:          62364 kB
SwapCached:        192 kB
Active:          49116 kB
Inactive:        50632 kB
HighTotal:      131008 kB
HighFree:        64792 kB
LowTotal:       903652 kB
LowFree:        830260 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34340 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:10:19 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 3827 7 1200.27 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |     775    36379 |     232       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |     767    35985 |      --       0       --      -- |     --   | -8/-394
c |         0 |     767    35985 |     306       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.530919 s)
c ==============================================================================
c [1mFound solution: 85[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4858   maxlim: 2375   bits: 12/12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   34687   157096 |   10406       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7264          
c   -- var.elim.:  2000/7264          
c   -- var.elim.:  3000/7264          
c   -- var.elim.:  4000/7264          
c   -- var.elim.:  5000/7264          
c   -- var.elim.:  6000/7264          
c   -- var.elim.:  7000/7264          
c   -- var.elim.:  7264/7264          
c   -- var.elim.:  26/26          
c |         0 |   34536   156507 |      --       0       --      -- |     --   | -124/-478
c |         0 |   34536   156507 |   13814       0        0     nan |  0.000 % |
c |       101 |   34536   156507 |   15195     101      424     4.2 |  0.739 % |
c |       253 |   34505   156401 |   16700     252      928     3.7 |  0.793 % |
c |       479 |   34505   156401 |   18370     478     1750     3.7 |  0.793 % |
c |       816 |   34412   156081 |   20153     814     2904     3.6 |  0.972 % |
c |      1322 |   34412   156081 |   22168    1320     4927     3.7 |  0.971 % |
c |      2081 |   34412   156081 |   24385    2079    11154     5.4 |  0.971 % |
c |      3220 |   34412   156081 |   26823    3218    43014    13.4 |  0.971 % |
c |      4931 |   34412   156081 |   29506    4929   124914    25.3 |  0.971 % |
c |      7493 |   34412   156081 |   32456    7491   378578    50.5 |  0.971 % |
c |     11338 |   34412   156081 |   35702   11336  1216748   107.3 |  0.971 % |
c |     17104 |   34412   156081 |   39272   17102  2923172   170.9 |  0.971 % |
c |     25756 |   34380   155972 |   43159   25753  4799285   186.4 |  1.026 % |
c |     38730 |   34370   155933 |   47461   38726  8318615   214.8 |  1.040 % |
c |     58191 |   34370   155933 |   52208   25922  6742131   260.1 |  1.040 % |
c |     87383 |   34370   155933 |   57428   16879  5387020   319.2 |  1.040 % |
c |    131174 |   34370   155933 |   63171   19453  4676795   240.4 |  1.040 % |
c |    196859 |   34339   155826 |   69426   37704 13935611   369.6 |  1.094 % |
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 #### 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.94 0.97 0.91 2/54 6669
Raw data (stat): 6669 (runsolver) R 6668 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480042126 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.0002 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 3964 0 0 0 988 10 0 0 25 0 1 0 480042126 18382848 3694 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4488 3694 603 41 0 4447 0
vsize: 17952
[startup+20.0006 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 5572 0 0 0 1984 13 0 0 25 0 1 0 480042126 24985600 5302 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6100 5303 603 41 0 6059 0
vsize: 24400
[startup+30.0009 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 6899 0 0 0 2982 17 0 0 25 0 1 0 480042126 30412800 6629 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7425 6629 603 41 0 7384 0
vsize: 29700
[startup+40.0009 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 8385 0 0 0 3978 20 0 0 25 0 1 0 480042126 36474880 8115 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8905 8115 603 41 0 8864 0
vsize: 35620
[startup+50.0015 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 9385 0 0 0 4976 23 0 0 25 0 1 0 480042126 40579072 9115 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9907 9115 603 41 0 9866 0
vsize: 39628
[startup+60.0019 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 10496 0 0 0 5972 27 0 0 25 0 1 0 480042126 45305856 10226 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11061 10226 603 41 0 11020 0
vsize: 44244
[startup+70.0015 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 11796 0 0 0 6969 30 0 0 25 0 1 0 480042126 50573312 11526 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12347 11526 603 41 0 12306 0
vsize: 49388
[startup+80.0024 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 12825 0 0 0 7967 32 0 0 25 0 1 0 480042126 54784000 12555 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13375 12555 603 41 0 13334 0
vsize: 53500
[startup+90.0018 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 14118 0 0 0 8963 36 0 0 25 0 1 0 480042126 60051456 13848 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14661 13848 603 41 0 14620 0
vsize: 58644
[startup+100.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 15229 0 0 0 9961 39 0 0 25 0 1 0 480042126 64659456 14959 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15786 14959 603 41 0 15745 0
vsize: 63144
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 15366 0 0 0 10961 39 0 0 25 0 1 0 480042126 64917504 15048 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15849 15048 603 41 0 15808 0
vsize: 63396
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 15366 0 0 0 11961 39 0 0 25 0 1 0 480042126 64917504 15048 4294967295 134512640 134672761 3221224576 3221223760 134615679 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15849 15048 603 41 0 15808 0
vsize: 63396
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 15366 0 0 0 12960 39 0 0 25 0 1 0 480042126 64917504 15048 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15849 15048 603 41 0 15808 0
vsize: 63396
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 15366 0 0 0 13960 39 0 0 25 0 1 0 480042126 64917504 15048 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15849 15048 603 41 0 15808 0
vsize: 63396
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 15366 0 0 0 14960 39 0 0 25 0 1 0 480042126 64917504 15048 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15849 15048 603 41 0 15808 0
vsize: 63396
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 15366 0 0 0 15960 39 0 0 25 0 1 0 480042126 64917504 15048 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15849 15048 603 41 0 15808 0
vsize: 63396
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 16376 0 0 0 16957 43 0 0 25 0 1 0 480042126 69140480 16058 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16880 16058 603 41 0 16839 0
vsize: 67520
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 17289 0 0 0 17955 45 0 0 25 0 1 0 480042126 72835072 16971 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17782 16971 603 41 0 17741 0
vsize: 71128
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 18135 0 0 0 18953 47 0 0 25 0 1 0 480042126 76259328 17817 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18618 17817 603 41 0 18577 0
vsize: 74472
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 18986 0 0 0 19951 49 0 0 25 0 1 0 480042126 79835136 18668 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19491 18668 603 41 0 19450 0
vsize: 77964
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 19773 0 0 0 20950 51 0 0 25 0 1 0 480042126 83005440 19455 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20265 19455 603 41 0 20224 0
vsize: 81060
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 20642 0 0 0 21948 53 0 0 25 0 1 0 480042126 86564864 20324 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21134 20324 603 41 0 21093 0
vsize: 84536
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21347 0 0 0 22945 56 0 0 25 0 1 0 480042126 89481216 21029 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21846 21029 603 41 0 21805 0
vsize: 87384
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 23944 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 24945 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 25945 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 26945 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 27945 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 28945 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 29945 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 30945 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 31946 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 32946 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 33946 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 34946 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 35946 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 36947 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 37947 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 38947 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21592 0 0 0 39947 57 0 0 25 0 1 0 480042126 90427392 21252 4294967295 134512640 134672761 3221224576 3221223760 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21252 603 41 0 22036 0
vsize: 88308
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 21785 0 0 0 40947 57 0 0 25 0 1 0 480042126 91353088 21445 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22303 21445 603 41 0 22262 0
vsize: 89212
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 22199 0 0 0 41946 58 0 0 25 0 1 0 480042126 92946432 21859 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22692 21859 603 41 0 22651 0
vsize: 90768
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 22657 0 0 0 42946 59 0 0 25 0 1 0 480042126 94826496 22317 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23151 22317 603 41 0 23110 0
vsize: 92604
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23183 0 0 0 43944 61 0 0 25 0 1 0 480042126 97124352 22843 4294967295 134512640 134672761 3221224576 3221223616 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23712 22843 603 41 0 23671 0
vsize: 94848
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 44944 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 45944 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223736 134614557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 46944 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 47945 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223724 134614482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 48945 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 49945 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 50945 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 51945 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 52945 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 53946 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 54946 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 55946 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 56946 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6669
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 57946 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+590.01 s]
Raw data (loadavg): 1.15 1.00 0.92 2/56 6708
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 58946 61 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+600.01 s]
Raw data (loadavg): 1.13 1.00 0.92 2/54 6722
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 59942 66 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+610.009 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 6722
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 60942 66 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+620.009 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 6722
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23467 0 0 0 61942 66 0 0 25 0 1 0 480042126 97902592 23069 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23069 603 41 0 23861 0
vsize: 95608
[startup+630.01 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 6722
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23468 0 0 0 62942 66 0 0 25 0 1 0 480042126 97902592 23070 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23902 23070 603 41 0 23861 0
vsize: 95608
[startup+640.009 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 6722
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 23877 0 0 0 63942 67 0 0 25 0 1 0 480042126 99655680 23479 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24330 23479 603 41 0 24289 0
vsize: 97320
[startup+650.009 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 6722
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 24381 0 0 0 64941 68 0 0 25 0 1 0 480042126 101789696 23983 4294967295 134512640 134672761 3221224576 3221223760 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24851 23983 603 41 0 24810 0
vsize: 99404
[startup+660.009 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 6722
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 24916 0 0 0 65940 69 0 0 25 0 1 0 480042126 103886848 24518 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25363 24518 603 41 0 25322 0
vsize: 101452
[startup+670.009 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25482 0 0 0 66938 71 0 0 25 0 1 0 480042126 106291200 25084 4294967295 134512640 134672761 3221224576 3221223732 134614480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25950 25084 603 41 0 25909 0
vsize: 103800
[startup+680.01 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 67938 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+690.011 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 68938 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+700.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 69938 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+710.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 70938 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+720.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 71938 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+730.011 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 72939 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+740.011 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 73939 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+750.01 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 74939 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+760.011 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 75939 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223616 134603565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+770.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 76939 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+780.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 77940 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+790.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 78940 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+800.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 79940 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+810.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 80940 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+820.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 81940 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+830.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 82941 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+840.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 83941 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223712 134614800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+850.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25791 0 0 0 84941 72 0 0 25 0 1 0 480042126 107200512 25329 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 25329 603 41 0 26131 0
vsize: 104688
[startup+860.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 25991 0 0 0 85941 72 0 0 25 0 1 0 480042126 108118016 25529 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26396 25529 603 41 0 26355 0
vsize: 105584
[startup+870.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 26844 0 0 0 86939 74 0 0 25 0 1 0 480042126 111542272 26382 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27232 26382 603 41 0 27191 0
vsize: 108928
[startup+880.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 27628 0 0 0 87937 76 0 0 25 0 1 0 480042126 114819072 27166 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28032 27166 603 41 0 27991 0
vsize: 112128
[startup+890.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 28394 0 0 0 88935 79 0 0 25 0 1 0 480042126 117972992 27932 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28802 27932 603 41 0 28761 0
vsize: 115208
[startup+900.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6724
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 29032 0 0 0 89933 81 0 0 25 0 1 0 480042126 120496128 28570 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29418 28570 603 41 0 29377 0
vsize: 117672
[startup+910.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 29722 0 0 0 90932 82 0 0 25 0 1 0 480042126 123658240 29260 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30190 29260 603 41 0 30149 0
vsize: 120760
[startup+920.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 30353 0 0 0 91930 84 0 0 25 0 1 0 480042126 126291968 29891 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30833 29891 603 41 0 30792 0
vsize: 123332
[startup+930.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 31082 0 0 0 92929 85 0 0 25 0 1 0 480042126 129191936 30620 4294967295 134512640 134672761 3221224576 3221223616 134614286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31541 30621 603 41 0 31500 0
vsize: 126164
[startup+940.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 31649 0 0 0 93928 87 0 0 25 0 1 0 480042126 131579904 31187 4294967295 134512640 134672761 3221224576 3221223760 134616006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32124 31187 603 41 0 32083 0
vsize: 128496
[startup+950.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32232 0 0 0 94926 89 0 0 25 0 1 0 480042126 133951488 31770 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32703 31770 603 41 0 32662 0
vsize: 130812
[startup+960.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32584 0 0 0 95926 89 0 0 25 0 1 0 480042126 134975488 32052 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32052 603 41 0 32912 0
vsize: 131812
[startup+970.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32584 0 0 0 96926 89 0 0 25 0 1 0 480042126 134975488 32052 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32052 603 41 0 32912 0
vsize: 131812
[startup+980.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32584 0 0 0 97926 89 0 0 25 0 1 0 480042126 134975488 32052 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32052 603 41 0 32912 0
vsize: 131812
[startup+990.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32584 0 0 0 98926 89 0 0 25 0 1 0 480042126 134975488 32052 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32052 603 41 0 32912 0
vsize: 131812
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32585 0 0 0 99926 90 0 0 25 0 1 0 480042126 134975488 32053 4294967295 134512640 134672761 3221224576 3221223712 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32053 603 41 0 32912 0
vsize: 131812
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32588 0 0 0 100926 90 0 0 25 0 1 0 480042126 134975488 32056 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32056 603 41 0 32912 0
vsize: 131812
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32588 0 0 0 101926 90 0 0 25 0 1 0 480042126 134975488 32056 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32056 603 41 0 32912 0
vsize: 131812
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32588 0 0 0 102926 90 0 0 25 0 1 0 480042126 134975488 32056 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32056 603 41 0 32912 0
vsize: 131812
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32588 0 0 0 103927 90 0 0 25 0 1 0 480042126 134975488 32056 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32056 603 41 0 32912 0
vsize: 131812
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32588 0 0 0 104927 90 0 0 25 0 1 0 480042126 134975488 32056 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32056 603 41 0 32912 0
vsize: 131812
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32588 0 0 0 105927 90 0 0 25 0 1 0 480042126 134975488 32056 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32056 603 41 0 32912 0
vsize: 131812
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32589 0 0 0 106927 90 0 0 25 0 1 0 480042126 134975488 32057 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32057 603 41 0 32912 0
vsize: 131812
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32589 0 0 0 107928 90 0 0 25 0 1 0 480042126 134975488 32057 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32057 603 41 0 32912 0
vsize: 131812
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32589 0 0 0 108928 90 0 0 25 0 1 0 480042126 134975488 32057 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32057 603 41 0 32912 0
vsize: 131812
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32589 0 0 0 109928 90 0 0 25 0 1 0 480042126 134975488 32057 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32057 603 41 0 32912 0
vsize: 131812
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32590 0 0 0 110928 90 0 0 25 0 1 0 480042126 134975488 32058 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32058 603 41 0 32912 0
vsize: 131812
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32590 0 0 0 111928 90 0 0 25 0 1 0 480042126 134975488 32058 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32058 603 41 0 32912 0
vsize: 131812
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32590 0 0 0 112928 90 0 0 25 0 1 0 480042126 134975488 32058 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32058 603 41 0 32912 0
vsize: 131812
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32590 0 0 0 113929 90 0 0 25 0 1 0 480042126 134975488 32058 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32058 603 41 0 32912 0
vsize: 131812
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32590 0 0 0 114929 90 0 0 25 0 1 0 480042126 134975488 32058 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32058 603 41 0 32912 0
vsize: 131812
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32590 0 0 0 115929 90 0 0 25 0 1 0 480042126 134975488 32058 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32058 603 41 0 32912 0
vsize: 131812
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32590 0 0 0 116929 90 0 0 25 0 1 0 480042126 134975488 32058 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32058 603 41 0 32912 0
vsize: 131812
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32590 0 0 0 117930 90 0 0 25 0 1 0 480042126 134975488 32058 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32058 603 41 0 32912 0
vsize: 131812
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32590 0 0 0 118930 90 0 0 25 0 1 0 480042126 134975488 32058 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32058 603 41 0 32912 0
vsize: 131812
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6726
Raw data (stat): 6669 (minisat+) R 6668 3260 3259 0 -1 0 32590 0 0 0 119930 90 0 0 25 0 1 0 480042126 134975488 32058 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32953 32058 603 41 0 32912 0
vsize: 131812
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 6726
Raw data (stat): 6669 (minisat+) Z 6668 3260 3259 0 -1 12 32591 0 0 0 119930 96 0 0 25 0 1 0 480042126 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.09
CPU time (s): 1200.27
CPU user time (s): 1199.31
CPU system time (s): 0.961853
CPU usage (%): 100.015
Max. virtual memory (Kb): 131812
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####