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/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-sentoy.opb
MD5SUM	4df3e7eb358d27d446e34b975724a6c1
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-7772
Optimality of the best value was proved	NO
Number of terms in the objective function	60
Biggest coefficient in the objective function	974
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	9460
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	6000
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	26162
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	60
Total number of constraints	90
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	30
Minimum length of a constraint	1
Maximum length of a constraint	60
Trace number 31116

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-05-25 22:09:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22512 boxname=wulflinc20 idbench=1328 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  4df3e7eb358d27d446e34b975724a6c1  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-sentoy.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-sentoy.opb
IDLAUNCH: 22512
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        868520 kB
Buffers:         34172 kB
Cached:         105892 kB
SwapCached:        696 kB
Active:          21824 kB
Inactive:       125052 kB
HighTotal:      131008 kB
HighFree:        72268 kB
LowTotal:       903652 kB
LowFree:        796252 kB
SwapTotal:     2097892 kB
SwapFree:      2096304 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5064 kB
Slab:            13552 kB
Committed_AS:    63568 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 22:30:13 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 22512 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  29]---> Adder-cost: 448   maxlim: 11620   bits: 15/14
c ---[  28]---> Adder-cost: 408   maxlim: 6087   bits: 14/13
c ---[  27]---> Adder-cost: 432   maxlim: 9310   bits: 14/14
c ---[  26]---> Adder-cost: 468   maxlim: 11096   bits: 15/14
c ---[  25]---> Adder-cost: 444   maxlim: 10275   bits: 14/14
c ---[  24]---> Adder-cost: 458   maxlim: 10302   bits: 14/14
c ---[  23]---> Adder-cost: 436   maxlim: 13436   bits: 15/14
c ---[  22]---> Adder-cost: 428   maxlim: 9755   bits: 14/14
c ---[  21]---> Adder-cost: 412   maxlim: 6448   bits: 14/13
c ---[  20]---> Adder-cost: 464   maxlim: 10002   bits: 14/14
c ---[  19]---> Adder-cost: 426   maxlim: 9583   bits: 14/14
c ---[  18]---> Adder-cost: 424   maxlim: 9848   bits: 14/14
c ---[  17]---> Adder-cost: 364   maxlim: 5722   bits: 14/13
c ---[  16]---> Adder-cost: 452   maxlim: 10594   bits: 15/14
c ---[  15]---> Adder-cost: 434   maxlim: 10081   bits: 14/14
c ---[  14]---> Adder-cost: 442   maxlim: 9196   bits: 14/14
c ---[  13]---> Adder-cost: 456   maxlim: 12391   bits: 15/14
c ---[  12]---> Adder-cost: 450   maxlim: 14161   bits: 15/14
c ---[  11]---> Adder-cost: 418   maxlim: 12220   bits: 15/14
c ---[  10]---> Adder-cost: 420   maxlim: 12782   bits: 15/14
c ---[   9]---> Adder-cost: 460   maxlim: 11486   bits: 15/14
c ---[   8]---> Adder-cost: 436   maxlim: 8903   bits: 14/14
c ---[   7]---> Adder-cost: 456   maxlim: 10103   bits: 14/14
c ---[   6]---> Adder-cost: 380   maxlim: 6238   bits: 14/13
c ---[   5]---> Adder-cost: 430   maxlim: 10469   bits: 15/14
c ---[   4]---> Adder-cost: 438   maxlim: 9149   bits: 14/14
c ---[   3]---> Adder-cost: 420   maxlim: 13773   bits: 15/14
c ---[   2]---> Adder-cost: 448   maxlim: 9436   bits: 14/14
c ---[   1]---> Adder-cost: 456   maxlim: 8907   bits: 14/14
c ---[   0]---> Adder-cost: 408   maxlim: 13608   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   89253   318894 |   29751       0        0     nan |  0.000 % |
c |       100 |   89253   318894 |   32726     100     1024    10.2 |  1.712 % |
c ==============================================================================
c [1mFound solution: -1341[0m
c ---[   0]---> Sorter-cost: 6599     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       191 |  106220   358591 |   35406     191     1682     8.8 |  1.712 % |
c |       291 |  106220   358591 |   38946     291     5111    17.6 |  1.192 % |
c |       443 |  106220   358591 |   42841     443     9280    20.9 |  1.192 % |
c |       669 |  106220   358591 |   47125     669    14719    22.0 |  1.192 % |
c |      1007 |  106214   358574 |   51837    1006    19436    19.3 |  1.197 % |
c ==============================================================================
c [1mFound solution: -1485[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1190 |  106519   359320 |   35506    1189    21596    18.2 |  1.197 % |
c |      1293 |  106519   359320 |   39056    1292    22436    17.4 |  1.191 % |
c |      1445 |  106519   359320 |   42962    1444    24976    17.3 |  1.191 % |
c |      1670 |  106519   359320 |   47258    1669    29751    17.8 |  1.191 % |
c |      2007 |  106519   359320 |   51984    2006    35780    17.8 |  1.191 % |
c ==============================================================================
c [1mFound solution: -1703[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2104 |  106596   359531 |   35532    2103    37022    17.6 |  1.191 % |
c |      2204 |  106596   359531 |   39085    2203    38425    17.4 |  1.194 % |
c |      2357 |  106596   359531 |   42993    2356    40994    17.4 |  1.194 % |
c |      2582 |  106596   359531 |   47293    2581    48161    18.7 |  1.194 % |
c |      2920 |  106596   359531 |   52022    2919    55040    18.9 |  1.194 % |
c ==============================================================================
c [1mFound solution: -2044[0m
c ---[   0]---> Sorter-cost:    8     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3041 |  106710   359836 |   35570    3040    59039    19.4 |  1.194 % |
c |      3141 |  106710   359836 |   39127    3140    59910    19.1 |  1.195 % |
c |      3291 |  106704   359819 |   43039    3289    62063    18.9 |  1.200 % |
c |      3516 |  106704   359819 |   47343    3514    64855    18.5 |  1.200 % |
c ==============================================================================
c [1mFound solution: -2051[0m
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3838 |  106709   359842 |   35569    3836    75916    19.8 |  1.200 % |
c |      3938 |  106709   359842 |   39125    3936    77693    19.7 |  1.205 % |
c |      4088 |  106709   359842 |   43038    4086    78884    19.3 |  1.205 % |
c ==============================================================================
c [1mFound solution: -2441[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4105 |  106730   359904 |   35576    4103    79182    19.3 |  1.205 % |
c |      4205 |  106730   359904 |   39133    4203    85074    20.2 |  1.209 % |
c |      4356 |  106730   359904 |   43046    4354    87121    20.0 |  1.209 % |
c ==============================================================================
c [1mFound solution: -2545[0m
c ---[   0]---> Sorter-cost:    8     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4437 |  106743   359939 |   35581    4435    91419    20.6 |  1.209 % |
c |      4537 |  106743   359939 |   39139    4535    93846    20.7 |  1.214 % |
c |      4687 |  106743   359939 |   43053    4685    97645    20.8 |  1.214 % |
c |      4912 |  106743   359939 |   47358    4910   102902    21.0 |  1.214 % |
c |      5249 |  106743   359939 |   52094    5247   110257    21.0 |  1.213 % |
c |      5755 |  106743   359939 |   57303    5753   131413    22.8 |  1.214 % |
c |      6514 |  106743   359939 |   63033    6512   170601    26.2 |  1.214 % |
c |      7653 |  106743   359939 |   69337    7651   215921    28.2 |  1.214 % |
c ==============================================================================
c [1mFound solution: -2651[0m
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7953 |  106748   359952 |   35582    7951   223593    28.1 |  1.214 % |
c |      8055 |  106748   359952 |   39140    8053   225854    28.0 |  1.218 % |
c |      8205 |  106748   359952 |   43054    8203   228739    27.9 |  1.218 % |
c ==============================================================================
c [1mFound solution: -2952[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8246 |  106757   359976 |   35585    8244   230421    28.0 |  1.218 % |
c |      8346 |  106757   359976 |   39143    8344   232767    27.9 |  1.223 % |
c |      8496 |  106757   359976 |   43057    8494   236015    27.8 |  1.223 % |
c |      8721 |  106757   359976 |   47363    8719   243030    27.9 |  1.223 % |
c |      9058 |  106757   359976 |   52099    9056   255321    28.2 |  1.223 % |
c |      9566 |  106757   359976 |   57309    9564   270673    28.3 |  1.223 % |
c ==============================================================================
c [1mFound solution: -3309[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9599 |  106798   360082 |   35599    9597   271200    28.3 |  1.223 % |
c |      9699 |  106798   360082 |   39158    9697   276476    28.5 |  1.227 % |
c |      9849 |  106798   360082 |   43074    9847   279294    28.4 |  1.227 % |
c |     10074 |  106798   360082 |   47382   10072   291867    29.0 |  1.227 % |
c |     10412 |  106798   360082 |   52120   10410   298988    28.7 |  1.227 % |
c |     10919 |  106798   360082 |   57332   10917   331053    30.3 |  1.227 % |
c |     11680 |  106792   360065 |   63065   11677   353489    30.3 |  1.232 % |
c |     12819 |  106792   360065 |   69372   12816   416224    32.5 |  1.232 % |
c |     14527 |  106792   360065 |   76309   14524   500281    34.4 |  1.232 % |
c |     17090 |  106786   360048 |   83940   17086   621843    36.4 |  1.237 % |
c |     20934 |  106786   360048 |   92334   20930   766604    36.6 |  1.237 % |
c |     26700 |  106786   360048 |  101568   26696   976667    36.6 |  1.237 % |
c |     35352 |  106786   360048 |  111724   35348  1373187    38.8 |  1.237 % |
c |     48326 |  106786   360048 |  122897   48322  2301426    47.6 |  1.237 % |
c ==============================================================================
c [1mFound solution: -5491[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49564 |  106852   360209 |   35617   49560  2348470    47.4 |  1.237 % |
c |     49664 |  106852   360209 |   39178   13139   877063    66.8 |  1.239 % |
c |     49815 |  106852   360209 |   43096   13290   878830    66.1 |  1.239 % |
c |     50040 |  106852   360209 |   47406   13515   892196    66.0 |  1.239 % |
c |     50379 |  106852   360209 |   52146   13854   895991    64.7 |  1.239 % |
c |     50887 |  106852   360209 |   57361   14362   901416    62.8 |  1.239 % |
c |     51646 |  106852   360209 |   63097   15121   912500    60.3 |  1.239 % |
c |     52787 |  106852   360209 |   69407   16262   956151    58.8 |  1.239 % |
c |     54495 |  106852   360209 |   76348   17970  1040942    57.9 |  1.239 % |
c |     57057 |  106852   360209 |   83983   20532  1211813    59.0 |  1.239 % |
c |     60902 |  106852   360209 |   92381   24377  1475337    60.5 |  1.239 % |
c |     66669 |  106846   360192 |  101619   30143  1911942    63.4 |  1.245 % |
c |     75319 |  106846   360192 |  111781   38793  2562755    66.1 |  1.245 % |
c |     88295 |  106846   360192 |  122959   51769  3109322    60.1 |  1.245 % |
c |    107756 |  106846   360192 |  135255   71230  4469811    62.8 |  1.245 % |
c |    136950 |  106846   360192 |  148781  100424  6087573    60.6 |  1.245 % |
c |    180739 |  106840   360175 |  163659  144212  8423431    58.4 |  1.250 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 10304 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 10300
Raw data (stat): 10300 (runsolver) R 10299 25399 25398 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842368366 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0035 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0043 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0046 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0057 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.8 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 10304
Raw data (stat): 10300 (minisat+_script) S 10299 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842368366 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.8
CPU time (s): 1229.86
CPU user time (s): 1229.1
CPU system time (s): 0.765883
CPU usage (%): 100.005
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####