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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare1_1.opb
MD5SUM	f88781e3d6e9a5487d13eaa213c27b55
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4272
Optimality of the best value was proved	NO
Number of terms in the objective function	120
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	6291450
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	6291450
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	205
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	45
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	105
Trace number 31291

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-05-25 23:52:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22683 boxname=wulflinc10 idbench=1499 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  f88781e3d6e9a5487d13eaa213c27b55  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-markshare1_1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-markshare1_1.opb
IDLAUNCH: 22683
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        547032 kB
Buffers:         35752 kB
Cached:         430024 kB
SwapCached:         92 kB
Active:          68416 kB
Inactive:       400028 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        546780 kB
SwapTotal:     2097136 kB
SwapFree:      2096752 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6392 kB
Slab:            13520 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:12:33 (client local time) WITH STATUS 152 IN 1229.84 SECONDS
stats: 22683 7 1229.84 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[  10]---> Adder-cost: 554   maxlim: 438520   bits: 20/19
c ---[   8]---> Adder-cost: 562   maxlim: 469716   bits: 20/19
c ---[   6]---> Adder-cost: 644   maxlim: 485238   bits: 20/19
c ---[   4]---> Adder-cost: 446   maxlim: 425237   bits: 20/19
c ---[   2]---> Adder-cost: 494   maxlim: 433357   bits: 20/19
c ---[   0]---> Adder-cost: 474   maxlim: 432725   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   21500    76369 |    7166       0        0     nan |  0.000 % |
c |       101 |   21500    76369 |    7882     101      468     4.6 |  7.165 % |
c |       251 |   21500    76369 |    8670     251     3196    12.7 |  7.165 % |
c |       480 |   21492    76343 |    9537     479     7965    16.6 |  7.194 % |
c ==============================================================================
c [1mFound solution: 552006[0m
c ---[   0]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       620 |   25213    85029 |    8404     619     9130    14.7 |  7.194 % |
c |       721 |   25213    85029 |    9244     720    18323    25.4 |  5.272 % |
c |       873 |   25213    85029 |   10168     872    38194    43.8 |  5.272 % |
c |      1099 |   25205    85003 |   11185    1097    44770    40.8 |  5.293 % |
c |      1436 |   25205    85003 |   12304    1434    50426    35.2 |  5.293 % |
c ==============================================================================
c [1mFound solution: 326866[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1527 |   25232    85100 |    8410    1525    51894    34.0 |  5.293 % |
c |      1628 |   25224    85074 |    9251    1625    53036    32.6 |  5.315 % |
c |      1779 |   25216    85048 |   10176    1775    55394    31.2 |  5.335 % |
c |      2004 |   25208    85022 |   11193    1999    58767    29.4 |  5.356 % |
c |      2341 |   25192    84970 |   12313    2334    62861    26.9 |  5.398 % |
c |      2847 |   25184    84944 |   13544    2839    69965    24.6 |  5.418 % |
c |      3608 |   25184    84944 |   14898    3600    95435    26.5 |  5.418 % |
c |      4747 |   25184    84944 |   16388    4739   144758    30.5 |  5.418 % |
c ==============================================================================
c [1mFound solution: 90720[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4797 |   25161    84848 |    8387    4722   138574    29.3 |  5.418 % |
c |      4897 |   25161    84848 |    9225    4822   142605    29.6 |  5.550 % |
c |      5047 |   25161    84848 |   10148    4972   144103    29.0 |  5.550 % |
c |      5272 |   25161    84848 |   11163    5197   147996    28.5 |  5.550 % |
c |      5609 |   25161    84848 |   12279    5534   162224    29.3 |  5.550 % |
c |      6115 |   25161    84848 |   13507    6040   167189    27.7 |  5.550 % |
c |      6874 |   25161    84848 |   14858    6799   192943    28.4 |  5.550 % |
c |      8013 |   25161    84848 |   16343    7938   219858    27.7 |  5.550 % |
c |      9722 |   25161    84848 |   17978    9647   293177    30.4 |  5.550 % |
c |     12285 |   25161    84848 |   19776   12210   421505    34.5 |  5.550 % |
c ==============================================================================
c [1mFound solution: 71680[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13517 |   25175    84879 |    8391   13442   503492    37.5 |  5.550 % |
c |     13617 |   25175    84879 |    9230    6821   271301    39.8 |  5.566 % |
c |     13767 |   25175    84879 |   10153    6971   274301    39.3 |  5.566 % |
c |     13993 |   25175    84879 |   11168    7197   278686    38.7 |  5.566 % |
c |     14330 |   25175    84879 |   12285    7534   287188    38.1 |  5.566 % |
c |     14837 |   25167    84861 |   13513    8040   298611    37.1 |  5.607 % |
c |     15596 |   25167    84861 |   14865    8799   324504    36.9 |  5.607 % |
c |     16737 |   25167    84861 |   16351    9940   380508    38.3 |  5.607 % |
c |     18445 |   25159    84835 |   17986   11647   441573    37.9 |  5.628 % |
c |     21010 |   25159    84835 |   19785   14212   538347    37.9 |  5.628 % |
c |     24854 |   25159    84835 |   21764   18056   694983    38.5 |  5.628 % |
c |     30620 |   25151    84809 |   23940   12175   440850    36.2 |  5.649 % |
c |     39270 |   25151    84809 |   26334   20825   861201    41.4 |  5.649 % |
c |     52244 |   25143    84787 |   28968   19364  1066264    55.1 |  5.690 % |
c |     71706 |   25143    84787 |   31864   21785   832604    38.2 |  5.690 % |
c |    100898 |   25143    84787 |   35051   30864  1585633    51.4 |  5.690 % |
c |    144688 |   25127    84735 |   38556   30209  1934568    64.0 |  5.731 % |
c ==============================================================================
c [1mFound solution: 57194[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    156428 |   24849    84050 |    8283   16798   793938    47.3 |  5.731 % |
c |    156528 |   24849    84050 |    9111    8499   353305    41.6 |  7.456 % |
c |    156678 |   24849    84050 |   10022    8649   356887    41.3 |  7.456 % |
c |    156906 |   24849    84050 |   11024    8877   362140    40.8 |  7.456 % |
c |    157244 |   24841    84024 |   12127    9213   367653    39.9 |  7.786 % |
c |    157750 |   24791    83912 |   13339    9716   380059    39.1 |  7.786 % |
c |    158510 |   24791    83912 |   14673   10476   402291    38.4 |  7.786 % |
c |    159650 |   24791    83912 |   16141   11616   445572    38.4 |  7.786 % |
c |    161358 |   24791    83912 |   17755   13324   500491    37.6 |  7.786 % |
c |    163922 |   24633    83548 |   19530   15878   584275    36.8 |  8.963 % |
c |    167767 |   24633    83548 |   21483   19723   717286    36.4 |  8.963 % |
c |    173533 |   24633    83548 |   23632   14127   524723    37.1 |  8.963 % |
c |    182182 |   24615    83508 |   25995   22775   900769    39.6 |  9.067 % |
c |    195157 |   24615    83508 |   28595   22368   947167    42.3 |  9.067 % |
c |    214618 |   24609    83494 |   31454   25616  1241598    48.5 |  9.108 % |
c |    243810 |   24609    83494 |   34600   15970  1161777    72.7 |  9.108 % |
c |    287599 |   24609    83494 |   38060   17320   924662    53.4 |  9.108 % |
c |    353284 |   24609    83494 |   41866   33078  2000413    60.5 |  9.108 % |
c ==============================================================================
c [1mFound solution: 50892[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    357437 |   24626    83535 |    8208   37231  2195337    59.0 |  9.108 % |
c |    357538 |   24626    83535 |    9028    7749   343658    44.3 |  9.110 % |
c |    357688 |   24626    83535 |    9931    7899   346693    43.9 |  9.110 % |
c |    357913 |   24626    83535 |   10924    8124   351062    43.2 |  9.110 % |
c |    358250 |   24626    83535 |   12017    8461   353734    41.8 |  9.110 % |
c |    358756 |   24626    83535 |   13219    8967   373042    41.6 |  9.110 % |
c |    359516 |   24626    83535 |   14540    9727   389280    40.0 |  9.110 % |
c |    360655 |   24626    83535 |   15995   10866   432959    39.8 |  9.110 % |
c |    362365 |   24626    83535 |   17594   12576   498251    39.6 |  9.110 % |
c |    364927 |   24626    83535 |   19354   15138   598074    39.5 |  9.110 % |
c |    368772 |   24626    83535 |   21289   18983   932407    49.1 |  9.110 % |
c |    374538 |   24626    83535 |   23418   13599   607840    44.7 |  9.110 % |
c |    383187 |   24626    83535 |   25760   22248  1058848    47.6 |  9.110 % |
c |    396162 |   24626    83535 |   28336   20986  1245980    59.4 |  9.110 % |
c |    415623 |   24619    83519 |   31169   22739  1211865    53.3 |  9.171 % |
c |    444817 |   24619    83519 |   34286   33541  1608075    47.9 |  9.171 % |
c |    488606 |   24602    83481 |   37715   16382   727364    44.4 |  9.275 % |
c |    554292 |   24602    83481 |   41487   31383  2050371    65.3 |  9.275 % |
c ==============================================================================
c [1mFound solution: 48690[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    558165 |   24611    83506 |    8203   35256  2301853    65.3 |  9.275 % |
c |    558266 |   24611    83506 |    9023    7352   361671    49.2 |  9.286 % |
c |    558416 |   24611    83506 |    9925    7502   363308    48.4 |  9.286 % |
c |    558641 |   24611    83506 |   10918    7727   367204    47.5 |  9.286 % |
c |    558978 |   24611    83506 |   12010    8064   374027    46.4 |  9.286 % |
c |    559485 |   24611    83506 |   13211    8571   390397    45.5 |  9.286 % |
c |    560245 |   24611    83506 |   14532    9331   411224    44.1 |  9.286 % |
c |    561384 |   24611    83506 |   15985   10470   451355    43.1 |  9.286 % |
c |    563093 |   24611    83506 |   17583   12179   555621    45.6 |  9.286 % |
c |    565655 |   24611    83506 |   19342   14741   639049    43.4 |  9.286 % |
c |    569500 |   24611    83506 |   21276   18586   781212    42.0 |  9.286 % |
c |    575266 |   24611    83506 |   23404   13076   496567    38.0 |  9.286 % |
c |    583917 |   24611    83506 |   25744   21727   836747    38.5 |  9.286 % |
c |    596891 |   24611    83506 |   28318   21220   824464    38.9 |  9.286 % |
c |    616352 |   24611    83506 |   31150   24464  1080641    44.2 |  9.286 % |
c |    645545 |   24611    83506 |   34265   15444   790113    51.2 |  9.286 % |
c |    689337 |   24611    83506 |   37692   15693   616696    39.3 |  9.286 % |
c |    755022 |   24611    83506 |   41461   30159  3542491   117.5 |  9.286 % |
c |    853548 |   24611    83506 |   45608   18346   925859    50.5 |  9.286 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  3362 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.95 0.91 2/54 3358
Raw data (stat): 3358 (runsolver) R 3357 15547 15546 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784774770 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.0001 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0006 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0011 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0018 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0027 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3362
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 3363
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.022 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 3415
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.022 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 3415
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.022 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 3415
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.022 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 3415
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.021 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 3415
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.021 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 3415
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.022 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 3415
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.022 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.022 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3417
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.7 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 3419
Raw data (stat): 3358 (minisat+_script) S 3357 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784774770 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.7
CPU time (s): 1229.84
CPU user time (s): 1229.57
CPU system time (s): 0.273958
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####