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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-p0548.opb
MD5SUM10547c6c0f11ab5df74fcaff6ba6d160
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 14938
Optimality of the best value was proved NO
Number of terms in the objective function 416
Biggest coefficient in the objective function 11000
Number of bits for the biggest coefficient in the objective function 14
Sum of the numbers in the objective function 96797
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 11000
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 96797
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1230.87
Number of variables548
Total number of constraints724
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)550
Number of constraints which are nor clauses,nor cardinality constraints134
Minimum length of a constraint1
Maximum length of a constraint143

Trace number 21110 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 22:49:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13738 boxname=wulflinc19 idbench=1057 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-p0548.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-p0548.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-p0548.opb
IDLAUNCH: 13738
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        618152 kB
Buffers:         29508 kB
Cached:         363380 kB
SwapCached:        560 kB
Active:         134804 kB
Inactive:       260052 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        617900 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5168 kB
Slab:            15908 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:09:14 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 13738 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 156 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssss.s..ssss........................................
c ---[ 164]---> Adder-cost: 66   maxlim: 856   bits: 11/10
c ---[ 163]---> Adder-cost: 73   maxlim: 258   bits: 10/9
c ---[ 162]---> Adder-cost: 56   maxlim: 650   bits: 11/10
c ---[ 161]---> Adder-cost: 64   maxlim: 847   bits: 11/10
c ---[ 160]---> Adder-cost: 69   maxlim: 354   bits: 10/9
c ---[ 159]---> Adder-cost: 50   maxlim: 668   bits: 11/10
c ---[ 157]---> Adder-cost: 73   maxlim: 419   bits: 10/9
c ---[ 156]---> Adder-cost: 61   maxlim: 227   bits: 9/8
c ---[ 154]---> Adder-cost: 67   maxlim: 479   bits: 10/9
c ---[ 153]---> Adder-cost: 34   maxlim: 106   bits: 8/7
c ---[ 152]---> Adder-cost: 92   maxlim: 333   bits: 10/9
c ---[ 151]---> Adder-cost: 77   maxlim: 407   bits: 10/9
c ---[ 150]---> Adder-cost: 82   maxlim: 615   bits: 11/10
c ---[ 149]---> Adder-cost: 96   maxlim: 1156   bits: 12/11
c ---[ 148]---> Adder-cost: 34   maxlim: 332   bits: 10/9
c ---[ 147]---> Adder-cost: 86   maxlim: 433   bits: 10/9
c ---[ 146]---> Adder-cost: 77   maxlim: 385   bits: 10/9
c ---[ 145]---> Adder-cost: 88   maxlim: 1134   bits: 12/11
c ---[ 144]---> Adder-cost: 93   maxlim: 249   bits: 9/8
c ---[ 143]---> Adder-cost: 100   maxlim: 295   bits: 10/9
c ---[ 142]---> Adder-cost: 97   maxlim: 249   bits: 9/8
c ---[ 141]---> Adder-cost: 108   maxlim: 494   bits: 10/9
c ---[ 140]---> Adder-cost: 98   maxlim: 506   bits: 10/9
c ---[ 139]---> Adder-cost: 53   maxlim: 259   bits: 10/9
c ---[ 138]---> Adder-cost: 55   maxlim: 439   bits: 10/9
c ---[ 136]---> Adder-cost: 61   maxlim: 393   bits: 10/9
c ---[ 135]---> Adder-cost: 94   maxlim: 1081   bits: 12/11
c ---[ 134]---> Adder-cost: 86   maxlim: 681   bits: 11/10
c ---[ 133]---> Adder-cost: 82   maxlim: 512   bits: 11/10
c ---[ 131]---> Adder-cost: 88   maxlim: 558   bits: 11/10
c ---[ 130]---> Adder-cost: 36   maxlim: 441   bits: 10/9
c ---[ 129]---> Adder-cost: 67   maxlim: 430   bits: 10/9
c ---[ 128]---> Adder-cost: 61   maxlim: 482   bits: 10/9
c ---[ 127]---> Adder-cost: 46   maxlim: 819   bits: 11/10
c ---[ 126]---> Adder-cost: 47   maxlim: 275   bits: 10/9
c ---[ 125]---> Adder-cost: 51   maxlim: 308   bits: 10/9
c ---[ 123]---> Adder-cost: 53   maxlim: 894   bits: 11/10
c ---[ 121]---> Adder-cost: 36   maxlim: 131   bits: 9/8
c ---[ 120]---> Adder-cost: 45   maxlim: 730   bits: 11/10
c ---[ 119]---> Adder-cost: 38   maxlim: 121   bits: 8/7
c ---[ 118]---> Adder-cost: 64   maxlim: 932   bits: 11/10
c ---[ 117]---> Adder-cost: 53   maxlim: 733   bits: 11/10
c ---[ 116]---> Adder-cost: 43   maxlim: 751   bits: 11/10
c ---[ 115]---> Adder-cost: 58   maxlim: 837   bits: 11/10
c ---[ 114]---> Adder-cost: 41   maxlim: 605   bits: 11/10
c ---[ 112]---> Adder-cost: 22   maxlim: 405   bits: 10/9
c ---[ 111]---> Adder-cost: 62   maxlim: 1052   bits: 12/11
c ---[ 110]---> Adder-cost: 53   maxlim: 811   bits: 11/10
c ---[ 109]---> Adder-cost: 47   maxlim: 603   bits: 11/10
c ---[ 107]---> Adder-cost: 18   maxlim: 360   bits: 10/9
c ---[ 106]---> Adder-cost: 47   maxlim: 785   bits: 11/10
c ---[ 105]---> Adder-cost: 49   maxlim: 833   bits: 11/10
c ---[ 104]---> Adder-cost: 49   maxlim: 0   bits: 1/0
c ---[ 103]---> Adder-cost: 59   maxlim: 1277   bits: 12/11
c ---[ 102]---> Adder-cost: 60   maxlim: 1324   bits: 12/11
c ---[ 101]---> Adder-cost: 67   maxlim: 1287   bits: 12/11
c ---[ 100]---> Adder-cost: 62   maxlim: 1125   bits: 12/11
c ---[  99]---> Adder-cost: 61   maxlim: 933   bits: 11/10
c ---[  98]---> Adder-cost: 41   maxlim: 715   bits: 11/10
c ---[  97]---> Adder-cost: 47   maxlim: 374   bits: 10/9
c ---[  96]---> Adder-cost: 72   maxlim: 972   bits: 11/10
c ---[  95]---> Adder-cost: 50   maxlim: 684   bits: 11/10
c ---[  93]---> Adder-cost: 64   maxlim: 390   bits: 10/9
c ---[  92]---> Adder-cost: 55   maxlim: 731   bits: 11/10
c ---[  91]---> Adder-cost: 61   maxlim: 866   bits: 11/10
c ---[  90]---> Adder-cost: 88   maxlim: 1313   bits: 12/11
c ---[  89]---> Adder-cost: 59   maxlim: 888   bits: 11/10
c ---[  88]---> Adder-cost: 28   maxlim: 141   bits: 9/8
c ---[  87]---> Adder-cost: 39   maxlim: 694   bits: 11/10
c ---[  86]---> Adder-cost: 25   maxlim: 447   bits: 10/9
c ---[  83]---> Adder-cost: 39   maxlim: 751   bits: 11/10
c ---[  81]---> Adder-cost: 28   maxlim: 646   bits: 11/10
c ---[  80]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[  79]---> Adder-cost: 126   maxlim: 381   bits: 10/9
c ---[  78]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  77]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  76]---> Adder-cost: 48   maxlim: 173   bits: 8/8
c ---[  75]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  73]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  71]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  69]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  67]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  61]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  59]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  57]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  55]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  53]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  47]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  41]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  33]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  31]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  29]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  27]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  25]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  21]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  19]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  17]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  15]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  13]---> Adder-cost: 98   maxlim: 48   bits: 7/6
c ---[  12]---> Adder-cost: 98   maxlim: 48   bits: 7/6
c ---[  11]---> Adder-cost: 52   maxlim: 25   bits: 6/5
c ---[  10]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[   9]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[   8]---> Adder-cost: 28   maxlim: 114   bits: 8/7
c ---[   7]---> Adder-cost: 24   maxlim: 141   bits: 9/8
c ---[   6]---> Adder-cost: 26   maxlim: 105   bits: 8/7
c ---[   5]---> Adder-cost: 50   maxlim: 158   bits: 9/8
c ---[   4]---> Adder-cost: 21   maxlim: 83   bits: 8/7
c ---[   3]---> Adder-cost: 4   maxlim: 68   bits: 8/7
c ---[   2]---> Adder-cost: 33   maxlim: 122   bits: 8/7
c ---[   1]---> Adder-cost: 4   maxlim: 68   bits: 8/7
c ---[   0]---> Adder-cost: 16   maxlim: 82   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   38053   135144 |   12684       0        0     nan |  0.000 % |
c |       100 |   38046   135121 |   13952      98      344     3.5 |  6.965 % |
c |       250 |   38046   135121 |   15347     248     1172     4.7 |  6.965 % |
c |       475 |   38046   135121 |   16882     473     2437     5.2 |  6.965 % |
c |       813 |   38046   135121 |   18570     811     5286     6.5 |  6.965 % |
c |      1319 |   38046   135121 |   20427    1317    11341     8.6 |  6.965 % |
c |      2079 |   38046   135121 |   22470    2077    26694    12.9 |  6.965 % |
c |      3218 |   38000   134951 |   24717    3211    50668    15.8 |  6.979 % |
c |      4926 |   38000   134951 |   27189    4919    95762    19.5 |  6.979 % |
c |      7494 |   38000   134951 |   29908    7487   192830    25.8 |  6.979 % |
c |     11338 |   38000   134951 |   32899   11331   351409    31.0 |  6.979 % |
c |     17105 |   38000   134951 |   36188   17098   551679    32.3 |  6.979 % |
c |     25757 |   38000   134951 |   39807   25750   903072    35.1 |  6.979 % |
c |     38731 |   37995   134935 |   43788   38723  1593201    41.1 |  6.993 % |
c |     58193 |   37995   134935 |   48167   27938   973445    34.8 |  6.993 % |
c |     87387 |   37995   134935 |   52984   22059  1143015    51.8 |  6.993 % |
c |    131176 |   37995   134935 |   58282   26575  1093824    41.2 |  6.993 % |
c |    196860 |   37995   134935 |   64110   50068  2036691    40.7 |  6.993 % |
c |    295386 |   37995   134935 |   70521   51695  3048990    59.0 |  6.993 % |
c |    443176 |   37995   134935 |   77574   40603  1677127    41.3 |  6.993 % |
c |    664859 |   37927   134690 |   85331   73978  4091325    55.3 |  7.022 % |
#### 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.84 0.94 0.90 2/55 10269
Raw data (stat): 10269 (runsolver) R 10268 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548800935 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 10269
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 1982 0 0 0 994 4 0 0 25 0 1 0 548800935 9945088 1959 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2428 1959 603 41 0 2387 0
vsize: 9712
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 10269
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 2767 0 0 0 1991 7 0 0 25 0 1 0 548800935 13299712 2744 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3247 2744 603 41 0 3206 0
vsize: 12988
[startup+30.0011 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 10269
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 3221 0 0 0 2991 8 0 0 25 0 1 0 548800935 15048704 3198 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3674 3198 603 41 0 3633 0
vsize: 14696
[startup+40.0012 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 3269 0 0 0 3991 8 0 0 25 0 1 0 548800935 15319040 3246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3740 3246 603 41 0 3699 0
vsize: 14960
[startup+50.002 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 3269 0 0 0 4991 8 0 0 25 0 1 0 548800935 15319040 3246 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3740 3246 603 41 0 3699 0
vsize: 14960
[startup+60.0025 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 3382 0 0 0 5991 9 0 0 25 0 1 0 548800935 15716352 3359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3837 3359 603 41 0 3796 0
vsize: 15348
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 3741 0 0 0 6990 9 0 0 25 0 1 0 548800935 17182720 3718 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4195 3718 603 41 0 4154 0
vsize: 16780
[startup+80.0035 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 3741 0 0 0 7990 9 0 0 25 0 1 0 548800935 17182720 3718 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4195 3718 603 41 0 4154 0
vsize: 16780
[startup+90.0039 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 3741 0 0 0 8991 9 0 0 25 0 1 0 548800935 17182720 3718 4294967295 134512640 134672761 3221224544 3221223648 134555084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4195 3718 603 41 0 4154 0
vsize: 16780
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4128 0 0 0 9990 10 0 0 25 0 1 0 548800935 18796544 4105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4589 4105 603 41 0 4548 0
vsize: 18356
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4191 0 0 0 10990 10 0 0 25 0 1 0 548800935 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4654 4168 603 41 0 4613 0
vsize: 18616
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4191 0 0 0 11990 10 0 0 25 0 1 0 548800935 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4654 4168 603 41 0 4613 0
vsize: 18616
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4191 0 0 0 12990 11 0 0 25 0 1 0 548800935 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4654 4168 603 41 0 4613 0
vsize: 18616
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4192 0 0 0 13990 11 0 0 25 0 1 0 548800935 19062784 4169 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4654 4169 603 41 0 4613 0
vsize: 18616
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4197 0 0 0 14990 11 0 0 25 0 1 0 548800935 19062784 4174 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4654 4174 603 41 0 4613 0
vsize: 18616
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4439 0 0 0 15989 12 0 0 25 0 1 0 548800935 20013056 4416 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4886 4416 603 41 0 4845 0
vsize: 19544
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4450 0 0 0 16989 12 0 0 25 0 1 0 548800935 20148224 4427 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4919 4427 603 41 0 4878 0
vsize: 19676
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4450 0 0 0 17988 13 0 0 25 0 1 0 548800935 20148224 4427 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4919 4427 603 41 0 4878 0
vsize: 19676
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4460 0 0 0 18988 13 0 0 25 0 1 0 548800935 20148224 4437 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4919 4437 603 41 0 4878 0
vsize: 19676
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4461 0 0 0 19988 13 0 0 25 0 1 0 548800935 20148224 4438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4919 4438 603 41 0 4878 0
vsize: 19676
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4468 0 0 0 20988 13 0 0 25 0 1 0 548800935 20148224 4445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4919 4445 603 41 0 4878 0
vsize: 19676
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4495 0 0 0 21988 14 0 0 25 0 1 0 548800935 20279296 4472 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4951 4472 603 41 0 4910 0
vsize: 19804
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4782 0 0 0 22987 15 0 0 25 0 1 0 548800935 21483520 4759 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5245 4759 603 41 0 5204 0
vsize: 20980
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4974 0 0 0 23986 16 0 0 25 0 1 0 548800935 22282240 4951 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5440 4951 603 41 0 5399 0
vsize: 21760
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4984 0 0 0 24986 17 0 0 25 0 1 0 548800935 22282240 4961 4294967295 134512640 134672761 3221224544 3221223648 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5440 4961 603 41 0 5399 0
vsize: 21760
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4986 0 0 0 25986 17 0 0 25 0 1 0 548800935 22282240 4963 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5440 4963 603 41 0 5399 0
vsize: 21760
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4997 0 0 0 26985 17 0 0 25 0 1 0 548800935 22462464 4974 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5484 4974 603 41 0 5443 0
vsize: 21936
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 4998 0 0 0 27985 18 0 0 25 0 1 0 548800935 22462464 4975 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5484 4975 603 41 0 5443 0
vsize: 21936
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 5002 0 0 0 28985 18 0 0 25 0 1 0 548800935 22462464 4979 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5484 4979 603 41 0 5443 0
vsize: 21936
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 5162 0 0 0 29984 19 0 0 25 0 1 0 548800935 23109632 5139 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5642 5139 603 41 0 5601 0
vsize: 22568
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 5465 0 0 0 30983 20 0 0 25 0 1 0 548800935 24301568 5442 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5933 5442 603 41 0 5892 0
vsize: 23732
[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 5723 0 0 0 31982 21 0 0 25 0 1 0 548800935 25362432 5700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6192 5700 603 41 0 6151 0
vsize: 24768
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10271
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 5965 0 0 0 32981 22 0 0 25 0 1 0 548800935 26431488 5942 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6453 5942 603 41 0 6412 0
vsize: 25812
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6209 0 0 0 33981 23 0 0 25 0 1 0 548800935 27439104 6186 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6699 6186 603 41 0 6658 0
vsize: 26796
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6284 0 0 0 34980 23 0 0 25 0 1 0 548800935 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6284 0 0 0 35981 23 0 0 25 0 1 0 548800935 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6284 0 0 0 36981 23 0 0 25 0 1 0 548800935 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6284 0 0 0 37981 23 0 0 25 0 1 0 548800935 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6291 0 0 0 38981 23 0 0 25 0 1 0 548800935 27885568 6268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6268 603 41 0 6767 0
vsize: 27232
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6291 0 0 0 39981 24 0 0 25 0 1 0 548800935 27885568 6268 4294967295 134512640 134672761 3221224544 3221223728 134557980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6268 603 41 0 6767 0
vsize: 27232
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6291 0 0 0 40981 24 0 0 25 0 1 0 548800935 27885568 6268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6268 603 41 0 6767 0
vsize: 27232
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6294 0 0 0 41981 24 0 0 25 0 1 0 548800935 27885568 6271 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6271 603 41 0 6767 0
vsize: 27232
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6301 0 0 0 42981 24 0 0 25 0 1 0 548800935 28147712 6278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6278 603 41 0 6831 0
vsize: 27488
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6301 0 0 0 43981 24 0 0 25 0 1 0 548800935 28147712 6278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6278 603 41 0 6831 0
vsize: 27488
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6301 0 0 0 44981 24 0 0 25 0 1 0 548800935 28147712 6278 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6278 603 41 0 6831 0
vsize: 27488
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6301 0 0 0 45981 24 0 0 25 0 1 0 548800935 28147712 6278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6278 603 41 0 6831 0
vsize: 27488
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6318 0 0 0 46981 24 0 0 25 0 1 0 548800935 28299264 6295 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6295 603 41 0 6868 0
vsize: 27636
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6324 0 0 0 47981 24 0 0 25 0 1 0 548800935 28299264 6301 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6301 603 41 0 6868 0
vsize: 27636
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6345 0 0 0 48981 24 0 0 25 0 1 0 548800935 28299264 6322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6322 603 41 0 6868 0
vsize: 27636
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6373 0 0 0 49982 24 0 0 25 0 1 0 548800935 28463104 6350 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6949 6350 603 41 0 6908 0
vsize: 27796
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6384 0 0 0 50982 24 0 0 25 0 1 0 548800935 28626944 6361 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6361 603 41 0 6948 0
vsize: 27956
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6385 0 0 0 51982 24 0 0 25 0 1 0 548800935 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6362 603 41 0 6948 0
vsize: 27956
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6385 0 0 0 52982 24 0 0 25 0 1 0 548800935 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6362 603 41 0 6948 0
vsize: 27956
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6385 0 0 0 53982 24 0 0 25 0 1 0 548800935 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6362 603 41 0 6948 0
vsize: 27956
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6387 0 0 0 54982 24 0 0 25 0 1 0 548800935 28626944 6364 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6364 603 41 0 6948 0
vsize: 27956
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6387 0 0 0 55982 24 0 0 25 0 1 0 548800935 28626944 6364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6364 603 41 0 6948 0
vsize: 27956
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6388 0 0 0 56983 24 0 0 25 0 1 0 548800935 28626944 6365 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6365 603 41 0 6948 0
vsize: 27956
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6388 0 0 0 57983 24 0 0 25 0 1 0 548800935 28626944 6365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6365 603 41 0 6948 0
vsize: 27956
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6419 0 0 0 58983 24 0 0 25 0 1 0 548800935 28823552 6396 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6396 603 41 0 6996 0
vsize: 28148
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6421 0 0 0 59983 24 0 0 25 0 1 0 548800935 28823552 6398 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6398 603 41 0 6996 0
vsize: 28148
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6435 0 0 0 60983 24 0 0 25 0 1 0 548800935 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6435 0 0 0 61983 24 0 0 25 0 1 0 548800935 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10273
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6435 0 0 0 62983 24 0 0 25 0 1 0 548800935 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10275
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6435 0 0 0 63984 24 0 0 25 0 1 0 548800935 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10275
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6435 0 0 0 64983 25 0 0 25 0 1 0 548800935 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10328
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6435 0 0 0 65983 25 0 0 25 0 1 0 548800935 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10328
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6435 0 0 0 66983 25 0 0 25 0 1 0 548800935 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10328
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6435 0 0 0 67983 26 0 0 25 0 1 0 548800935 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10328
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6438 0 0 0 68983 26 0 0 25 0 1 0 548800935 28823552 6415 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6415 603 41 0 6996 0
vsize: 28148
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10328
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6442 0 0 0 69982 27 0 0 25 0 1 0 548800935 28823552 6419 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6419 603 41 0 6996 0
vsize: 28148
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10328
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6449 0 0 0 70982 27 0 0 25 0 1 0 548800935 28823552 6426 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6426 603 41 0 6996 0
vsize: 28148
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10328
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6455 0 0 0 71982 28 0 0 25 0 1 0 548800935 28823552 6432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6432 603 41 0 6996 0
vsize: 28148
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6467 0 0 0 72981 28 0 0 25 0 1 0 548800935 28987392 6444 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7077 6444 603 41 0 7036 0
vsize: 28308
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6473 0 0 0 73981 29 0 0 25 0 1 0 548800935 28987392 6450 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7077 6450 603 41 0 7036 0
vsize: 28308
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6474 0 0 0 74980 29 0 0 25 0 1 0 548800935 28987392 6451 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7077 6451 603 41 0 7036 0
vsize: 28308
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6491 0 0 0 75980 30 0 0 25 0 1 0 548800935 29151232 6468 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7117 6468 603 41 0 7076 0
vsize: 28468
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6497 0 0 0 76980 30 0 0 25 0 1 0 548800935 29151232 6474 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7117 6474 603 41 0 7076 0
vsize: 28468
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6515 0 0 0 77979 31 0 0 25 0 1 0 548800935 29151232 6492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7117 6492 603 41 0 7076 0
vsize: 28468
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6632 0 0 0 78979 31 0 0 25 0 1 0 548800935 29769728 6609 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7268 6609 603 41 0 7227 0
vsize: 29072
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6662 0 0 0 79979 32 0 0 25 0 1 0 548800935 29904896 6639 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6639 603 41 0 7260 0
vsize: 29204
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6662 0 0 0 80979 32 0 0 25 0 1 0 548800935 29904896 6639 4294967295 134512640 134672761 3221224544 3221223728 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6639 603 41 0 7260 0
vsize: 29204
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6662 0 0 0 81979 32 0 0 25 0 1 0 548800935 29904896 6639 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6639 603 41 0 7260 0
vsize: 29204
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6664 0 0 0 82978 33 0 0 25 0 1 0 548800935 29904896 6641 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6641 603 41 0 7260 0
vsize: 29204
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6674 0 0 0 83978 33 0 0 25 0 1 0 548800935 29904896 6651 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6651 603 41 0 7260 0
vsize: 29204
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6681 0 0 0 84978 34 0 0 25 0 1 0 548800935 29904896 6658 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6658 603 41 0 7260 0
vsize: 29204
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6697 0 0 0 85977 34 0 0 25 0 1 0 548800935 30040064 6674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7334 6674 603 41 0 7293 0
vsize: 29336
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6704 0 0 0 86977 35 0 0 25 0 1 0 548800935 30040064 6681 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7334 6681 603 41 0 7293 0
vsize: 29336
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6709 0 0 0 87977 35 0 0 25 0 1 0 548800935 30040064 6686 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7334 6686 603 41 0 7293 0
vsize: 29336
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6720 0 0 0 88977 36 0 0 25 0 1 0 548800935 30203904 6697 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6697 603 41 0 7333 0
vsize: 29496
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6734 0 0 0 89976 36 0 0 25 0 1 0 548800935 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6734 0 0 0 90976 37 0 0 25 0 1 0 548800935 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6734 0 0 0 91976 37 0 0 25 0 1 0 548800935 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10330
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6734 0 0 0 92975 38 0 0 25 0 1 0 548800935 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10332
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6734 0 0 0 93975 38 0 0 25 0 1 0 548800935 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10332
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6734 0 0 0 94975 39 0 0 25 0 1 0 548800935 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10332
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6734 0 0 0 95975 39 0 0 25 0 1 0 548800935 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10332
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6734 0 0 0 96974 39 0 0 25 0 1 0 548800935 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+980.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10332
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6734 0 0 0 97974 40 0 0 25 0 1 0 548800935 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10332
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6734 0 0 0 98974 40 0 0 25 0 1 0 548800935 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10332
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 6986 0 0 0 99973 42 0 0 25 0 1 0 548800935 31281152 6963 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7637 6963 603 41 0 7596 0
vsize: 30548
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10332
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 7234 0 0 0 100971 43 0 0 25 0 1 0 548800935 32342016 7211 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7896 7211 603 41 0 7855 0
vsize: 31584
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10332
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 7479 0 0 0 101971 43 0 0 25 0 1 0 548800935 33415168 7456 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8158 7456 603 41 0 8117 0
vsize: 32632
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 7740 0 0 0 102970 45 0 0 25 0 1 0 548800935 34357248 7717 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8388 7717 603 41 0 8347 0
vsize: 33552
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 7939 0 0 0 103969 46 0 0 25 0 1 0 548800935 35164160 7916 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 7939 0 0 0 104969 46 0 0 25 0 1 0 548800935 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 7939 0 0 0 105969 47 0 0 25 0 1 0 548800935 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 7939 0 0 0 106968 47 0 0 25 0 1 0 548800935 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 7939 0 0 0 107968 48 0 0 25 0 1 0 548800935 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 7939 0 0 0 108968 48 0 0 25 0 1 0 548800935 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 7950 0 0 0 109968 48 0 0 25 0 1 0 548800935 35315712 7927 4294967295 134512640 134672761 3221224544 3221223696 134541821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8622 7927 603 41 0 8581 0
vsize: 34488
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 7970 0 0 0 110967 49 0 0 25 0 1 0 548800935 35315712 7947 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8622 7947 603 41 0 8581 0
vsize: 34488
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 8003 0 0 0 111967 50 0 0 25 0 1 0 548800935 35479552 7980 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8662 7980 603 41 0 8621 0
vsize: 34648
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 8007 0 0 0 112967 50 0 0 25 0 1 0 548800935 35479552 7984 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8662 7984 603 41 0 8621 0
vsize: 34648
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 8008 0 0 0 113967 50 0 0 25 0 1 0 548800935 35479552 7985 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8662 7985 603 41 0 8621 0
vsize: 34648
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 8022 0 0 0 114966 51 0 0 25 0 1 0 548800935 35676160 7999 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 7999 603 41 0 8669 0
vsize: 34840
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 8033 0 0 0 115966 51 0 0 25 0 1 0 548800935 35676160 8010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 8010 603 41 0 8669 0
vsize: 34840
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 8035 0 0 0 116966 51 0 0 25 0 1 0 548800935 35676160 8012 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 8012 603 41 0 8669 0
vsize: 34840
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 8035 0 0 0 117966 52 0 0 25 0 1 0 548800935 35676160 8012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 8012 603 41 0 8669 0
vsize: 34840
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 8036 0 0 0 118966 52 0 0 25 0 1 0 548800935 35676160 8013 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 8013 603 41 0 8669 0
vsize: 34840
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10334
Raw data (stat): 10269 (minisat+) R 10268 22929 22928 0 -1 0 8045 0 0 0 119966 52 0 0 25 0 1 0 548800935 35676160 8022 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 8022 603 41 0 8669 0
vsize: 34840
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 10334
Raw data (stat): 10269 (minisat+) Z 10268 22929 22928 0 -1 12 8047 0 0 0 119966 54 0 0 25 0 1 0 548800935 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.04
CPU time (s): 1200.21
CPU user time (s): 1199.66
CPU system time (s): 0.542917
CPU usage (%): 100.013
Max. virtual memory (Kb): 34840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####