PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-p0548.opb
MD5SUM	10547c6c0f11ab5df74fcaff6ba6d160
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
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 numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1244.18
Number of variables	548
Total number of constraints	724
Number of constraints which are clauses	40
Number of constraints which are cardinality constraints (but not clauses)	550
Number of constraints which are nor clauses,nor cardinality constraints	134
Minimum length of a constraint	1
Maximum length of a constraint	143
Trace number 15004

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 02:34:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18730 boxname=wulflinc3 idbench=1441 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-p0548.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-p0548.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-p0548.opb
IDLAUNCH: 18730
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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		: 451.190
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:        286496 kB
Buffers:         34484 kB
Cached:         690192 kB
SwapCached:          0 kB
Active:         208252 kB
Inactive:       519248 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        286244 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6840 kB
Slab:            14928 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 02:54:13 (client local time) WITH STATUS 0 IN 1200.15 SECONDS
stats: 18730 7 1200.15 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.85 0.97 0.93 2/54 3627
Raw data (stat): 3627 (runsolver) R 3626 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483289271 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.0004 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 1987 0 0 0 993 4 0 0 25 0 1 0 483289271 9945088 1964 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2428 1964 603 41 0 2387 0
vsize: 9712
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 2769 0 0 0 1991 7 0 0 25 0 1 0 483289271 13299712 2746 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3247 2746 603 41 0 3206 0
vsize: 12988
[startup+30.002 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 3219 0 0 0 2990 8 0 0 25 0 1 0 483289271 15048704 3196 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3674 3196 603 41 0 3633 0
vsize: 14696
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 3269 0 0 0 3990 8 0 0 25 0 1 0 483289271 15319040 3246 4294967295 134512640 134672761 3221224544 3221223712 134561008 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.0029 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 3269 0 0 0 4990 8 0 0 25 0 1 0 483289271 15319040 3246 4294967295 134512640 134672761 3221224544 3221223712 134560895 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.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 3365 0 0 0 5990 9 0 0 25 0 1 0 483289271 15716352 3342 4294967295 134512640 134672761 3221224544 3221223648 134559796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3837 3342 603 41 0 3796 0
vsize: 15348
[startup+70.0033 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 3741 0 0 0 6989 10 0 0 25 0 1 0 483289271 17182720 3718 4294967295 134512640 134672761 3221224544 3221223728 134559363 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.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 3741 0 0 0 7989 10 0 0 25 0 1 0 483289271 17182720 3718 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.003 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 3741 0 0 0 8989 10 0 0 25 0 1 0 483289271 17182720 3718 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.003 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4097 0 0 0 9988 11 0 0 25 0 1 0 483289271 18665472 4074 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4557 4074 603 41 0 4516 0
vsize: 18228
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4191 0 0 0 10988 11 0 0 25 0 1 0 483289271 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4191 0 0 0 11987 11 0 0 25 0 1 0 483289271 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4654 4168 603 41 0 4613 0
vsize: 18616
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4191 0 0 0 12988 11 0 0 25 0 1 0 483289271 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4654 4168 603 41 0 4613 0
vsize: 18616
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4192 0 0 0 13988 11 0 0 25 0 1 0 483289271 19062784 4169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4654 4169 603 41 0 4613 0
vsize: 18616
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4197 0 0 0 14988 11 0 0 25 0 1 0 483289271 19062784 4174 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4654 4174 603 41 0 4613 0
vsize: 18616
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4421 0 0 0 15988 12 0 0 25 0 1 0 483289271 20013056 4398 4294967295 134512640 134672761 3221224544 3221223712 134559733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4886 4398 603 41 0 4845 0
vsize: 19544
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4450 0 0 0 16988 12 0 0 25 0 1 0 483289271 20148224 4427 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4427 603 41 0 4878 0
vsize: 19676
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4450 0 0 0 17987 12 0 0 25 0 1 0 483289271 20148224 4427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4427 603 41 0 4878 0
vsize: 19676
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4460 0 0 0 18988 12 0 0 25 0 1 0 483289271 20148224 4437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4437 603 41 0 4878 0
vsize: 19676
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4461 0 0 0 19988 12 0 0 25 0 1 0 483289271 20148224 4438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4438 603 41 0 4878 0
vsize: 19676
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4468 0 0 0 20988 12 0 0 25 0 1 0 483289271 20148224 4445 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4445 603 41 0 4878 0
vsize: 19676
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4471 0 0 0 21988 12 0 0 25 0 1 0 483289271 20148224 4448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4448 603 41 0 4878 0
vsize: 19676
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4757 0 0 0 22987 13 0 0 25 0 1 0 483289271 21348352 4734 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5212 4734 603 41 0 5171 0
vsize: 20848
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4974 0 0 0 23987 13 0 0 25 0 1 0 483289271 22282240 4951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5440 4951 603 41 0 5399 0
vsize: 21760
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4984 0 0 0 24987 13 0 0 25 0 1 0 483289271 22282240 4961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5440 4961 603 41 0 5399 0
vsize: 21760
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4986 0 0 0 25987 13 0 0 25 0 1 0 483289271 22282240 4963 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5440 4963 603 41 0 5399 0
vsize: 21760
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4996 0 0 0 26987 13 0 0 25 0 1 0 483289271 22462464 4973 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5484 4973 603 41 0 5443 0
vsize: 21936
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 4998 0 0 0 27988 13 0 0 25 0 1 0 483289271 22462464 4975 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5484 4975 603 41 0 5443 0
vsize: 21936
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 5002 0 0 0 28988 13 0 0 25 0 1 0 483289271 22462464 4979 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5484 4979 603 41 0 5443 0
vsize: 21936
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 5155 0 0 0 29987 14 0 0 25 0 1 0 483289271 23109632 5132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5642 5132 603 41 0 5601 0
vsize: 22568
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 5453 0 0 0 30987 15 0 0 25 0 1 0 483289271 24301568 5430 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5933 5430 603 41 0 5892 0
vsize: 23732
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 5716 0 0 0 31986 16 0 0 25 0 1 0 483289271 25362432 5693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6192 5693 603 41 0 6151 0
vsize: 24768
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 5960 0 0 0 32986 16 0 0 25 0 1 0 483289271 26431488 5937 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6453 5937 603 41 0 6412 0
vsize: 25812
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6206 0 0 0 33986 16 0 0 25 0 1 0 483289271 27439104 6183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6699 6183 603 41 0 6658 0
vsize: 26796
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6284 0 0 0 34986 17 0 0 25 0 1 0 483289271 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134561190 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.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6284 0 0 0 35986 17 0 0 25 0 1 0 483289271 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.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6284 0 0 0 36986 17 0 0 25 0 1 0 483289271 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+380.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6284 0 0 0 37986 17 0 0 25 0 1 0 483289271 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134561118 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.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6291 0 0 0 38986 17 0 0 25 0 1 0 483289271 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.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6291 0 0 0 39986 17 0 0 25 0 1 0 483289271 27885568 6268 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6291 0 0 0 40986 17 0 0 25 0 1 0 483289271 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6294 0 0 0 41986 17 0 0 25 0 1 0 483289271 27885568 6271 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6300 0 0 0 42986 17 0 0 25 0 1 0 483289271 28147712 6277 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6277 603 41 0 6831 0
vsize: 27488
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6301 0 0 0 43986 17 0 0 25 0 1 0 483289271 28147712 6278 4294967295 134512640 134672761 3221224544 3221223712 134560999 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.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6301 0 0 0 44986 17 0 0 25 0 1 0 483289271 28147712 6278 4294967295 134512640 134672761 3221224544 3221223648 134560260 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6301 0 0 0 45986 17 0 0 25 0 1 0 483289271 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.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6318 0 0 0 46987 17 0 0 25 0 1 0 483289271 28299264 6295 4294967295 134512640 134672761 3221224544 3221223712 134560996 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.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6319 0 0 0 47987 17 0 0 25 0 1 0 483289271 28299264 6296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6296 603 41 0 6868 0
vsize: 27636
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6339 0 0 0 48987 17 0 0 25 0 1 0 483289271 28299264 6316 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6316 603 41 0 6868 0
vsize: 27636
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6373 0 0 0 49987 17 0 0 25 0 1 0 483289271 28463104 6350 4294967295 134512640 134672761 3221224544 3221223712 134560912 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.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6384 0 0 0 50987 17 0 0 25 0 1 0 483289271 28626944 6361 4294967295 134512640 134672761 3221224544 3221223648 134554642 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.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6385 0 0 0 51987 17 0 0 25 0 1 0 483289271 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6385 0 0 0 52987 17 0 0 25 0 1 0 483289271 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134560942 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.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6385 0 0 0 53988 17 0 0 25 0 1 0 483289271 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134561001 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.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6387 0 0 0 54988 17 0 0 25 0 1 0 483289271 28626944 6364 4294967295 134512640 134672761 3221224544 3221223608 1075349616 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.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6387 0 0 0 55988 17 0 0 25 0 1 0 483289271 28626944 6364 4294967295 134512640 134672761 3221224544 3221223744 134557836 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.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6387 0 0 0 56988 17 0 0 25 0 1 0 483289271 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+580.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6388 0 0 0 57988 17 0 0 25 0 1 0 483289271 28626944 6365 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6400 0 0 0 58988 18 0 0 25 0 1 0 483289271 28626944 6377 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6377 603 41 0 6948 0
vsize: 27956
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6421 0 0 0 59988 18 0 0 25 0 1 0 483289271 28823552 6398 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6435 0 0 0 60988 18 0 0 25 0 1 0 483289271 28823552 6412 4294967295 134512640 134672761 3221224544 3221223376 134565852 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.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6435 0 0 0 61988 18 0 0 25 0 1 0 483289271 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.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6435 0 0 0 62989 18 0 0 25 0 1 0 483289271 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560937 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.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6435 0 0 0 63989 18 0 0 25 0 1 0 483289271 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.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6435 0 0 0 64989 18 0 0 25 0 1 0 483289271 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+660.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6435 0 0 0 65989 18 0 0 25 0 1 0 483289271 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.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6435 0 0 0 66989 18 0 0 25 0 1 0 483289271 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560909 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.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6435 0 0 0 67989 18 0 0 25 0 1 0 483289271 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+690.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6436 0 0 0 68989 18 0 0 25 0 1 0 483289271 28823552 6413 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6413 603 41 0 6996 0
vsize: 28148
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6441 0 0 0 69989 18 0 0 25 0 1 0 483289271 28823552 6418 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6418 603 41 0 6996 0
vsize: 28148
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6447 0 0 0 70990 18 0 0 25 0 1 0 483289271 28823552 6424 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6424 603 41 0 6996 0
vsize: 28148
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6450 0 0 0 71990 18 0 0 25 0 1 0 483289271 28823552 6427 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6427 603 41 0 6996 0
vsize: 28148
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6467 0 0 0 72990 18 0 0 25 0 1 0 483289271 28987392 6444 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6467 0 0 0 73990 18 0 0 25 0 1 0 483289271 28987392 6444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7077 6444 603 41 0 7036 0
vsize: 28308
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6474 0 0 0 74990 18 0 0 25 0 1 0 483289271 28987392 6451 4294967295 134512640 134672761 3221224544 3221223712 134560964 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.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6479 0 0 0 75990 18 0 0 25 0 1 0 483289271 28987392 6456 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7077 6456 603 41 0 7036 0
vsize: 28308
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6496 0 0 0 76991 18 0 0 25 0 1 0 483289271 29151232 6473 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7117 6473 603 41 0 7076 0
vsize: 28468
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6510 0 0 0 77991 18 0 0 25 0 1 0 483289271 29151232 6487 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7117 6487 603 41 0 7076 0
vsize: 28468
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6540 0 0 0 78991 18 0 0 25 0 1 0 483289271 29347840 6517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7165 6517 603 41 0 7124 0
vsize: 28660
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6662 0 0 0 79990 19 0 0 25 0 1 0 483289271 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.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6662 0 0 0 80990 19 0 0 25 0 1 0 483289271 29904896 6639 4294967295 134512640 134672761 3221224544 3221223712 134561008 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.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6662 0 0 0 81990 19 0 0 25 0 1 0 483289271 29904896 6639 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6663 0 0 0 82990 19 0 0 25 0 1 0 483289271 29904896 6640 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6640 603 41 0 7260 0
vsize: 29204
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6674 0 0 0 83991 19 0 0 25 0 1 0 483289271 29904896 6651 4294967295 134512640 134672761 3221224544 3221223712 134560876 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.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6680 0 0 0 84991 19 0 0 25 0 1 0 483289271 29904896 6657 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6657 603 41 0 7260 0
vsize: 29204
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6697 0 0 0 85991 19 0 0 25 0 1 0 483289271 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.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6703 0 0 0 86991 19 0 0 25 0 1 0 483289271 30040064 6680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7334 6680 603 41 0 7293 0
vsize: 29336
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6704 0 0 0 87991 19 0 0 25 0 1 0 483289271 30040064 6681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7334 6681 603 41 0 7293 0
vsize: 29336
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6720 0 0 0 88992 19 0 0 25 0 1 0 483289271 30203904 6697 4294967295 134512640 134672761 3221224544 3221223712 134561188 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.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6725 0 0 0 89992 19 0 0 25 0 1 0 483289271 30203904 6702 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6702 603 41 0 7333 0
vsize: 29496
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6734 0 0 0 90992 19 0 0 25 0 1 0 483289271 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.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6734 0 0 0 91992 19 0 0 25 0 1 0 483289271 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6734 0 0 0 92992 19 0 0 25 0 1 0 483289271 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6734 0 0 0 93992 19 0 0 25 0 1 0 483289271 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+950.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6734 0 0 0 94993 19 0 0 25 0 1 0 483289271 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.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6734 0 0 0 95993 19 0 0 25 0 1 0 483289271 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+970.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6734 0 0 0 96993 19 0 0 25 0 1 0 483289271 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134561118 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.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6734 0 0 0 97993 19 0 0 25 0 1 0 483289271 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560988 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.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6734 0 0 0 98993 19 0 0 25 0 1 0 483289271 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.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 6797 0 0 0 99993 19 0 0 25 0 1 0 483289271 30605312 6774 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7472 6774 603 41 0 7431 0
vsize: 29888
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7070 0 0 0 100993 20 0 0 25 0 1 0 483289271 31678464 7047 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7734 7047 603 41 0 7693 0
vsize: 30936
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7325 0 0 0 101992 22 0 0 25 0 1 0 483289271 32747520 7302 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7995 7302 603 41 0 7954 0
vsize: 31980
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7570 0 0 0 102990 22 0 0 25 0 1 0 483289271 33685504 7547 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8224 7547 603 41 0 8183 0
vsize: 32896
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7815 0 0 0 103988 24 0 0 25 0 1 0 483289271 34762752 7792 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8487 7792 603 41 0 8446 0
vsize: 33948
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7939 0 0 0 104987 24 0 0 25 0 1 0 483289271 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 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.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7939 0 0 0 105987 24 0 0 25 0 1 0 483289271 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134561154 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.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7939 0 0 0 106987 24 0 0 25 0 1 0 483289271 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134561188 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.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7939 0 0 0 107987 24 0 0 25 0 1 0 483289271 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.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7939 0 0 0 108987 24 0 0 25 0 1 0 483289271 35164160 7916 4294967295 134512640 134672761 3221224544 3221223808 134562196 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.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7939 0 0 0 109987 24 0 0 25 0 1 0 483289271 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+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7951 0 0 0 110988 24 0 0 25 0 1 0 483289271 35315712 7928 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8622 7928 603 41 0 8581 0
vsize: 34488
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 7971 0 0 0 111987 24 0 0 25 0 1 0 483289271 35315712 7948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8622 7948 603 41 0 8581 0
vsize: 34488
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 8005 0 0 0 112987 24 0 0 25 0 1 0 483289271 35479552 7982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8662 7982 603 41 0 8621 0
vsize: 34648
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 8008 0 0 0 113987 24 0 0 25 0 1 0 483289271 35479552 7985 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 8009 0 0 0 114987 24 0 0 25 0 1 0 483289271 35479552 7986 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8662 7986 603 41 0 8621 0
vsize: 34648
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 8022 0 0 0 115988 24 0 0 25 0 1 0 483289271 35676160 7999 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 7999 603 41 0 8669 0
vsize: 34840
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 8034 0 0 0 116988 25 0 0 25 0 1 0 483289271 35676160 8011 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 8011 603 41 0 8669 0
vsize: 34840
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 8035 0 0 0 117988 25 0 0 25 0 1 0 483289271 35676160 8012 4294967295 134512640 134672761 3221224544 3221223712 134561167 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.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 8035 0 0 0 118988 25 0 0 25 0 1 0 483289271 35676160 8012 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 8012 603 41 0 8669 0
vsize: 34840
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 3627
Raw data (stat): 3627 (minisat+) R 3626 10720 10719 0 -1 0 8036 0 0 0 119988 25 0 0 25 0 1 0 483289271 35676160 8013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 8013 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.93 1/54 3627
Raw data (stat): 3627 (minisat+) Z 3626 10720 10719 0 -1 12 8038 0 0 0 119988 26 0 0 25 0 1 0 483289271 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.15
CPU user time (s): 1199.89
CPU system time (s): 0.265959
CPU usage (%): 100.009
Max. virtual memory (Kb): 34840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####